↓これの続きでっせ。
cut-elimination.hatenablog.com
3章は型とは何かという哲学的な考察を含んでいる。4章は正規化定理を解説したテクニカルな内容である。
Chapter 3 カリー=ハワード同型
命題を型と対応させる。型付項のシステムにおいても sense と denotation の二項対立が現れる。denotation はプログラムの denotational semantics（表示的意味論）の背景にある。もちろん。それは denotation の等式を与える静的なものである。対して sense の方は操作的意味論をもたらす。こちらは書換えを与える動的なものである。
スコット意味論など表示的意味論は栄えているが、操作的意味論はまだ十分ではないとジラール先生は考えている。「アルゴリズムの真に操作的な意味論を確立することがコンピュータ科学における最も重要な問題かもしれない」とすら述べている（14ページ）。
続いて型付ラムダ計算が定義される *1。複合型は と
の二つなので、命題論理の
断片と対応する。
3.3の "Operational significance" という節で型についての哲学的考察が展開されている。項はプログラムを表し、プログラムは denotation を計算する。そしてプログラムの型はプログラムの仕様だという。とすると型はプログラムの情報をどれくらい詳細に含むべきかということになる。本書ではかなり原始的なものでしかないが、もっと情報量豊富な型のシステムを作ることもできるらしい。
更に、型はプログラムのモジュールをプラグする（plugging）ための取り決めであると考えることができる。これはナルホドである。型のマッチはモジュールの挿入が失敗しないためのものと考えると分りやすい。またこう考えるとインプットとアウトプットも対称的なものと見做せるという。この考え方は萌芽的だというが、(see appendix B)とあり、このappendix B は線形論理の解説である。線形論理は相互作用的な計算を表現するといわれる（照井一成先生）が、それがここに現れているようだ。
変換の定義をした後、自然変換との同型が示される。これが単なる全単射でなく同型であるというのは、構造まで同じということだ。Chapter 2 で証明間の"equal"とされていたものがここでは"rewriting"と言い直される。これは変換に対応するからである。
関数と証明はそれぞれ別に生れたものであるから異なる点があるはずだが、同型性によって相手側にその対応物を考えられるということが重要であるという。関数は操作的なものである。ということは良い (構成的)論理は操作的であるべきだ。逆に論理は暗に対称性を持つのであるから、型付計算体系もそれを意識すべきだ、とのこと。関数→論理の方向は私もよく考えるが、論理→関数はあんまり考えたことがなかったなあ。
この同型性は、論理と計算が同じ物を別の仕方で表現したものであることを示している！
Chapter 4 正規化定理
チャーチ=ロッサー定理の簡単な解説と正規化定理のやや詳しい証明が書かれている。
私は型無ラムダ計算の正規化定理と型付ラムダ計算の強正規化定理の証明は見たことがあるが、本章のような型付ラムダ計算の(弱)正規化定理の証明は初めて見たかもしれない。
正規化定理の証明では degree というのを定義している。正規化定理を証明するには、必ず正規形を導ける変換戦略を発見すれば十分である。ここの証明では「最も degree が大きくしかもそこに含まれているリデックスはどれも degree がより小さい」ようなリデックスから変換していくとしている。しかしこのようなリデックスが存在することもちゃんと証明しなければならないような気がしてならない！ だがそれが存在しない項が存在すると仮定するとそれは長さが無限になってしまうからいいのか（背理法）。ちょっと自信無し。そしてこの変換をすると最大の degree を持つリデックスが減ることがレンマで示されたので最大の degree とその数で二重帰納法にすれば正規化定理が証明できる。
という感じ。
ジラール先生はこれが「弱」正規化定理であることをやや強調気味な感じがする。
感想
ジラール先生はカット除去を論理の「対称性」と表現しているが、それがまだあまりピンときていない。
