λμのTypeCheckerの実装
λμのtypecheckerを実装したので
(ソースコードは参考文献[3]を参照)
λμ[1]はλ→に継続(callCC)を入れたもの(CCC + Continuation monad)。
syntax的にはμ-abstractionとnaming(termに名前をつける)が追加される。
型なしの項を受け取って、それにうまく型をつけることを考える。
アルゴリズム(合ってる保証はない):
typing : Context -> UntypedTerm -> Type (var) typing(G,x) = G(x) (lam) typing(G,λx.M) = ?n -> typing(G;x:?n, M) (app) typing(G,MN) = let U -> V = typing(G,M); W = typing(G,N) in unify(U -> V, W -> ?n); V (mu) typing(G,μα.M) = let U = typing(G,M) in unify(U,⊥); G(α) (name) typing(G,[α]M) = let U = typing(G;α:?n, M) in unify(U,G(α)); ⊥
ここで?nはhole(まだ決定されていない型)を表していて、
unifyは与えられた型を合わせる作業をしてくれる。
厳密にはunifyは型の等式からなる集合({?0 = M, ?1 = ?2 -> ?3}のようなもの)をより簡単な形に変えてかつ無駄を省いていく。途中で必要があれば型エラーを吐いてそれをユーザーに見せることもある。
unification algorithmは[2]をそのまま実装した。
で、肝心のコードについては、
必要なデータをState Environmentで引きずり回して随所でEitherを返すようにしたら最高にめんどくさくなったので、エラーメッセージのハンドリングはEitherTを使うなり(モナドトランスフォーマー重ねたくねぇ)MonadErrorでやるなりしたいなーと思いつつやってない。
とりあえず良い練習にはなったので他の型システムも随時実装していきたい。
参考文献
依存型による定理証明Tips: coherenceは型で表せ
この記事はTheorem Prover Advent Calendar 2016 12日目の記事です。
この記事は定理証明初心者向けの記事です。
普段から依存型を用いた定理証明をされている方は読む必要がありません。
"coherence condition"と呼ばれる条件があり、訳すと「一貫性条件」となるようです。
これはちゃんと定義があるものではないのですが[要出典]、一貫性が保たれているならば当然成り立っているべき条件あるいは定理のことを、一般にcoherence conditionと呼んだりします。
例えば、型がついた言語での関数適用を考えます。
この時、P(Q,R)という項がwell-typedならば、
直感的にはPは2変数であり、QとRを引数に受け取っている、ということになります。
この時、実際にP : A -> B -> C, Q : A, R : Bという型が付くはずですが、この条件がcoherenceです。
ここで重要なのはwell-typednessであり、正しい仕方で構成された項は異常な項を持たない、みたいな性質が効いていて上のようなことが成り立ちます。
もちろんcoherenceはこれだけではなく、至るところに現れます。
こういうcoherenceが成り立つかどうかを判定するために必要な情報は、
全て型に持たせましょう、というのが今回のTipsです。
先程の例では、"well-typed termに含まれる関数適用は、関数の引数の数があっているはずだ"というのが
coherenceでした。
このことを示したい、あるいは関数の引数の数についての命題を証明する必要があるのならば、
関数の引数は型に乗せておくのが便利です。
つまり、この言語の項のなす型Termは、Term (n:N) : Typeとなり、
先のcoherenceは、
P(Q,R): well-typed ==> exists n. P: Term (n+2)のようにかけます。
あるいは、existsと言った扱いが面倒な型を登場させたくなければ、
P(Q,R): Term n ==> P: Term (n+2)
とすればよいです。
これによって、Mがwell-typedな項であるというのは、M: Term nとかける型のことだ、という了解が得られます。
実際に証明をする過程で、coherence conditionは何か？というのを考えることは重要です。
ひとたびcoherenceがわかれば、それに関連する情報は全て型に持たせてやれば、少しだけ証明は楽になると思います。
あるいは自分で型を新たに作らなくとも、既存の型を使うほうが便利なことも多いです。
この場合、例えばListではなくVectorを使うことで、「コンテナの長さ」に関するcoherenceを扱いやすくなります。
最近私は型付きλ計算についての証明を書いたのですが、
context(自由変数に割り当てる型の集まり)の中に変数が出現するかどうか、あるいは出現したものの型は何になるか、
といったcoherenceがよく出てくるので、contextの型に「自由変数の個数」「自由変数のシンボルの集合」
などをのせることで、自由変数の振る舞いによる場合分けが簡単になったりしています。
このように、coherenceが何かを考え、それに対応する情報を型にのせることで
不要な場合分けや細かいチェックなどが省ける場合があるので、よければ参考にしてください。
ということを、1-2年前に知りたかったな〜〜〜と最近思ったので記事にしました。
鬱モード全開だったときに
今から大体3年くらい前の、大学学部2回生の頃に唐突に精神が死んだことがあった。
という話をするけど、この先読んでも特にオチはありません。
ただの身の上話なので。
非常に運がよかったため自分は3回生の進路振り分け的なものに必要な単位を前期で全て揃えていたので
これによる留年及び進路が狭められるといった良くない結果が将来にもたらされることは一切なかった。
これがもう2-3ヶ月早く発症していたら、専門も2回目の語学も落として無事留年が確定していたので運がよいというレベルではなかった。
で、精神が死んでいた頃、毎日大学にも行かず、家でずっとつらいつらいと思いながら日々を過ごしていた。
具体的に言うと次のような一日を過ごしていた。
- 朝11時前後に起床する。今日も2限に寝坊したという絶望感と、そのくせに全く疲れが取れておらず、眠いし体中のだるさに悲しくなる。
- ﾂｲｯﾀｰ等を眺めるが眠いしどうでもいいツイートが並んでいてつまらない。けれど何もやる気が起きないので30分くらい見てる。
- 起きるのが遅いので昼ごはんも遅くなる。12時半くらいにご飯を食べながら、いやいやもう3限目今更行ってもしょうがなくないか…という気持ちになる*1。
- 13時を過ぎてやはり3限目に行かなかったことにじわじわ罪悪感を覚え始める。
- 暇すぎて趣味(絵/プログラミング/ゲーム/勉強etc)をするが眠いし全く脳が働かず、集中できず10分も持たない。どうでも良いことをネットで調べたりぼーっと動画を見たりして時間を潰す。
- 気がつくと4限・5限もぶっちしている
- 19時を回り「今日も何もしなかった…」と思う。
- 22時を回り段々目が冴えてくるが「今じゃないんだよ」という気持ちになる
- 2時ごろになって「そろそろ寝ようかな」と思う
- 布団に入るが全く眠れない。布団の中で「明日もまたこの無意味な一日を繰り返すのか」と思って悲しくなる。
- 実際に眠るのは布団に入って2-3時間後
自分は趣味が多いほうだと思っていたのだけれど、どれも全く楽しめず、集中力も持たないのですぐやめていた。
結局自分から何も考えなくても時間が潰れる動画サイト等に行き着くのだけれど「自分は何でこんな無駄なことをしているのだろう」という気持ちがあるのでそちらでもあまり楽しむことはできなかった。
そもそも睡眠の質が低すぎて日中ずっと眠いというのが一番キツかったけれど、ずっと引きこもっているので体力が有り余った状態で布団に入っても眠れないのでどんどん睡眠のリズムが崩れるというのを繰り返していた気がする。
可能なら外に出れる状態のうちに毎日少しでも外に出るというのをやってみるといいと思う。あるいは太陽の光を直接浴びるとか。これをやるかどうかはかなり重要だと思うので今は割とそうしてる。
一応他の人につらいという愚痴をこぼしてみたりもしたことがあるが、あんまり解決はしなかったのと自分のゴミっぷりを再確認することで余計つらい気持ちになれたのであまりおすすめはしない。
で、結局どうやって解決したかというと多分外に出れたのがきっかけだったように思う。
そもそもこの生活を始めてしばらくしてから、外に出るのも怖く、大学はおろか近所のコンビニに行くために玄関に立つだけで何か恐ろしくなって行くのをやめるという感じで、一切家の外に出ることができなかった。
しかし流石にこのままではまずいと思い、大学のカウンセリングセンター的なところを訪れようと決意したのだった。
当然、カウンセリングセンターに行くには大学に行かねばならず、これは自分にとって非常に高いハードルだったので、カウンセリングを受けることを決心するのにn日、カウンセリングセンターの場所を調べることを決意するのにn日、センターの人に伝えるべき自分の今の状況を頭の中でまとめるのにまたn日というすごい時間をかけていた気がする。
まぁとにかくカウンセリングを受ける決意は固まり、しかしいきなり大学に行ってカウンセリングを受けるのは難しそうだったので、
「まずは大学に行ってセンターの前を通過し、そして改めて後日訪れよう」という感じの決意を固めて家を出たのだった。
結論から言うとこの「今日は建物の前を通過するだけで中には入らないぞ」という決意は自分の心を非常に軽くしてくれるとても良い決意だったみたいで、
結局その日は大学に行くのだけれど、大学に着いてから「あれ、でも大学来れたなら授業出ればいいじゃん」となって、その翌日から普通に授業に出始めたのであっさりと治ってしまうのだった。
まぁとにかく、この「まずは前を通過するぞ」というつらい行動を2ステップに分けるタイプの決意は非常に有効なので、
困っている人はよければ参考にしてください。
ちなみにコレ以降、ひきこもりから抜けれなくなって精神がやられるタイプの精神的なつらみはほぼなくなるのだった。
今では規則正しい睡眠リズムと毎日外に出るのは重要だなと思ってる。
おわり
*1:補足しておくとその頃とっていた授業は2限目に講義、3限目に演習というタイプのやつが多かった
