Locally Cartesian Closed Category
|
...2006/08/23 23:14...
Structual Proof Thery と Martin-Lof Type Theory は 密接に結びつく。このことが、Natural Deduction の正規化の過程と Typed Lambda Calculus における beta reduction との Structual なアナロジーとなるのか。Typed Lambda Calculus は、Cartesian Closed Category でモデル化できる。ならば、Martin-Lof Type Theory も Cartesian Closed Category でモデル化できのかなと思った。そこでちょっと Wikipedia を調べてみた。どうも Seely が locally cartesian closed category という概念を導入して Martin-Lof type theory をモデル化しているそう。Seely は、*autonomous category を使って Linear Logic のモデル化もしている。凄い人なんだなあ。
|
Martin Lof Type Theory
|
...2006/08/22 23:55...
ML などと戯れていると必ず Martin-Lof の Type Theory というのが出てくる。こう言われると、それ以外の Type Theory ってあるのとか、そもそも Martin-Lof の Type Theory ってどういうものという疑問が素朴に湧いてくる。（B.Russel が所謂ラッセルのパラドックスの解決のために Type Theory を使ったと聞いたことはあるけど厳密なものはみたことがないし知らない。）たまたま良い本を見つけた。
Programming in Martin-Lof Type Theory
Cambiridge University Press
という本。Constructive Mathematics で何かの分類に（なんの分類かはよくわからないが）Type Theory が使われていたそう。当然のことながら集合の言葉で書かれている。これを Curry-Howard 対応で Proposition を Type と考え、Type が Set であるから Set を Poroposition と見なして logic の言葉で構築し直したのが Martin-Lof の仕事。最終的に Dependent Type を伴って１階の命題論理で体系化している。（途中いろいろある。）Polymorpic Set というのがあってこれが Polymorphic Type になるようだ。論理で体系化されたのでコンピュータの上に載せて計算できるようになるから使えるようになった素晴らしいということになるわけか。Unification を使えばよいのかなと思っていると実際には Well-ordering の概念を使って term rewrite よろしく計算する（所謂 Milner の W algorism）。論理をちゃんと勉強する意欲が湧く。
|
