BarendregtのLambda calculi with typesのintroについての非常に不正確なメモ（自分用）

lambda

http://d.hatena.ne.jp/kgbu/20080617/1213685112
でひっかかっていたので、BarendregtのLambda calculi with typesを少し読んでみた。
以下、自分にもよくわからないメモなので、もし間違って検索でここに来た人は、すみませんが無視してください。
ちなみに、Postscriptのファイルはhttp://www.informatik.uni-ulm.de/ki/Edu/Vorlesungen/Typentheorie/SS98/HBKJ.ps.gz
から取ってきた。他にも各所にあるらしい。
PostscriptのファイルのViewerがWindos上になくて、VMware上のUbuntuで開いたりして、妙に手間取ってしまった。おかげで、PostscriptのファイルをPDFに変換するサービスを見つけたりもした。でもここは使ってくれるフォントがイマイチ、かな。結局、Windows XP上のFirefox2.0のPDF readerのプラグインでは検索はうまくできるようにならなかったし。
（追記：Ubuntu上のPDFリーダー:Evinceだとうまくいく）

Introの部分

型付きλ計算を導入したのはHaskell B. Curryと A. Churchだったそれぞれ流儀が違っていて、

  • Curryのケース:明示的に型は指定しない。型チェックはコンパイラが行う→ML言語

（lambda calculi with type assingment)

  • Churchのケース:すべての項(term)について、明示的に型を指定する→ALGOL68, Pascal言語（systems of typed lambda calculus)

Churchのケースの場合、項は常に正規形を持つ点が重要である。ただし、プログラムの停止問題が解けないことから、逆に、Churchのタイプの型付きλ計算では、ある種の（例えば、停止しない）プログラムが実装可能ではないこともわかる。

（以下：自註：つまり M(YM) = YMのように不動点をなすようなプログラムは無限にβreductionできるケースとも考えられ、型付きλ計算には含まれないという見方もできる）

これについてBarendregtの1990年の論文の定理4.2.15を参照

計算できない関数というのは、どういうものか？二階の型付きλ計算(λ2）では、計算できない再帰関数はあるが、それは数学的な分析（二階の計算）を行う場合には回避できる(←訳がおかしいな）

型付きのλ計算のプログラムへの応用
型Ａは述語とみなすことができ、ある項Ｍが型Ａを持つということは、述語を証明するということになる。これが定理証明系に応用された。(AUTOMATHシステム)
項の正規化はformula-as-types （型による公式の表現）

最近(1990年代まで）、たくさんの型付システムがでてきたが、この論文で扱うのは。

  • もっともシンプルなバージョン
  • βリダクションだけで、ηリダクション等は含まず
  • Churchタイプの型付けoperatorとして、→(関数)とIIは扱うが、×（直積）やΣ(直和？）は扱わない
  • Curryタイプの型付けでは→、∩、μだけを扱う

しがって、Martin-Lof(1984)の型理論とかは扱わない。

上記のようなシンプルなスタイルでも、十分に興味深い例がある。

この論文では、型付λ計算の意味論(semantics)には踏み込まない。
というのは、Churchタイプの型付きラムダ計算のモデルの記述(notion)についてはこの論文執筆当時も議論が続いていたからだ。notionについては、Jacobs(1991)によってfibre(束)カテゴリーを使ってまとめられている(←自信無し）

参考になる本
Girard 編の(1989)が、semanticsも扱っている。

この論文の第2章は、型無しのλ計算についての紹介
第3章は型付きλ計算についての解説
第4章はCurryの型付きラムダ計算についての解説
第5章はChurchの型付きラムダ計算についての解説