Proofs and Types

学生と一緒に読みなおしてます。

ゲンツェンのシーケント代数の辺りから「あれ? こんなこと書いてあったかな」みたいなのが。一度、読んでるはずなんだけどな〜 こんなに Linear logic の話書いてあったっけ。

ちゃんと、ホワイトボードで計算やらせるからだな。そうそう、手で計算してみるまでは、何言ってるのかわからないものさ。

結構、飛ばしながらゲーデルのSystem Tまで来たんですが、最後に、

R は、It で定義できる

とか、さらっと書いてある。R も It も再帰を表す関数なんだけど、R は U -> Int -> U を使って次に行くのに対して、It は U -> U しかない。

f(n+1) = g(n, f(n))

と、

f(n+1) = g(f(n))

の違いみたいなものらしです。で、pair を使って、

<n+1, f (n+1)> = g(<n, f(n)>)

みたいにすれば良いってな話らしい。

これが結構面倒。で、Agda で、System T を書き始めたら、あっというまに数時間経ってました。玉手箱か Agda は。

うちに戻ってから、さらに、4時間ぐらいで証明できました。でも、System T と Agda の相性が良いというのはわかりました。

今回は System F まで、行きつけるのだろうか。

Proofs and Types (Cambridge Tracts in Theoretical Computer Science) by Jean-Yves Girard et al.
http://amzn.com/0521371813