calculus of constructions (CoC) の勉強

論理体系のうちの一つとしてのCoCではなくて、ラムダキューブの位置頂点であるλCと言った方が適切かもしれません。

λCは、全称型・型演算子・依存型をすべて含む、非常に表現力の高い型付きラムダ計算の体系です。 表現力が高いにもかかわらず、型検査が通ればそのプログラムは 必ず 停止することが知られています。

これはすごいことですが、逆に言うと、停止しないようなプログラムは書けない、つまりチューリング完全ではない、ということになります。 ほとんどの実用的なプログラミング言語チューリング完全であることを考えると、λCは表現力が高いとは言っても、十分ではないということになってしまいそうです。

一方、Curry-Howard対応を考えると、停止しないようなプログラムに型をつけてしまう型理論は、矛盾した論理体系に対応しています。 そういう型理論では、型パズルを無理やり解くために次のようなことができてしまい、しかも型検査も通ってしまいますが、役に立つプログラムになっていないことは明らかです。

  1. ある関数を呼び出すために必要な、型Tのオブジェクトが欲しい。
  2. 「止まれば型Tを返す(実際には無限ループする)」みたいな関数を書く。この関数を実行し、型Tの変数を手に入れる。
  3. さっきの関数の引数にする。

こんなことをしても、目的の関数を呼んでいるような雰囲気のソースコードは書けますが、実行時に目的の関数に到達することはありません。

λCは、こういった無意味なことはできないという一種の安心感があります。もちろん、必ず停止するとはいっても非常に長い時間動き続けるようなプログラムは書けるため、実用上止まらないようなプログラムも存在します。

CoCの文法

ラムダ抽象・全称型・型演算子・依存型の四つを含むにもかかわらず、文法はいたって単純です。依存型を表すために導入した依存積型(Π)は、縮退したパターンとして矢印型(→)を含みます。また、全称型を作るときの型抽象(Λ)は特別扱いせず、ラムダ抽象(λ)にまとめられています。このようになっているため、シンプルです。

 T = x \ | \ * \ | \ T \ T \ | \ \lambda x^T. T \ | \ \Pi x^T. T

ここで、上付き文字は束縛引数xの型を意味します。普通はコロンを使った定義が一般的ですが、型付け規則の中のメタ文字としてのコロンと見分けがつきづらいのを嫌って上付き文字としました。

観察

簡単な導出で雰囲気をつかむ

まず、リテラルっぽいものが*しかありません。とりあえず、型検査器がOKというものをいくつか列挙してみます。 \vdashの左側が型環境で、右側が型検査にとおる項とその型付けです。

  •  \vdash * : \Box
  •  \vdash \lambda x^*. x : * → *
  •  \vdash \lambda x^*. * : * → \Box
  •  \vdash \Pi x^*. x : *
  •  \vdash \Pi x^*. * : \Box

ここで、 \Box *の"型"です。文法には入っていないため、書くことはできません。 また、 \alpha → \betaは、 \Pi x^\alpha. \betaの略記です。ただし、 \betaの中に束縛した xが含まれていないときに限ります。

単純型付きラムダ計算をシミュレート

とりあえず、以下のようにすることで、単純型付きラムダ計算と同じことができます。

 \lambda f^{ * → * → * }.\lambda x^*. f \ x \ x

実際には型ではなくカインドなのですが、『型システム入門』p.363によれば、

「本質的に単純型付きラムダ計算の「1レベル上」の複製」

値と型の区別がない

実は、以下のようなものが書けます。

 \lambda nat^ * . \lambda succ^{nat → nat}. \lambda zero^ {nat} . succ \ (succ \ zero)

 natはラムダ抽象で導入した変数なので項だと思っていましたが、実はその後に出てくるラムダ抽象で導入する succ zeroの型付けに使えます。最初、このことに気づかず、先ほどの単純型付きラムダ計算以上のことができず、悩みました。

この入れ子は何回でも繰り返せます。つまり、型・カインド・カインドの一レベル上の"型"・……のように無限の階層構造を作れるため、高階多相が実現されます。

依存型

依存型も使えるようなのですが、依存型を使わないと書けない例が特に思いつきませんでした(とはいえ、さっきの高階多相は単なる依存型とも読めます。しかし、高階多相もどう役に立つのかよくわかりません)。そもそも、λCは非常に高い表現力を持つ体系ということになっていますが、具体的にはどのように表現力が高いのでしょうか?以下で考えてみます。

表現力

単純型

多項式くらいの物しか書けないらしく、あまり高い表現力を持っているわけではないようです。

全称型

全称型を持つSystem F(二階ラムダ計算)では、型に関する抽象が導入されます。これにより、今までは型がつかなかった*1 \lambda x. xに型がつきます*2

 \vdash \lambda x. x : \forall X. X→X

これを使うと、一見再帰的な使い方のプログラムである (\lambda f. f f)(\lambda x.x)にも正しい型がつき、停止するプログラムであることが分かります。

つまり、全称型を導入すると、型のつく項が増えます。

一方、単純型付きラムダ計算のような、型を書かなくてもその使われ方から自動で型再構築されるという性質は失われてしまいます。ラムダ抽象で導入する変数の型は、プログラマが明示する必要があります。また、多相型をどの型で具体化するかも指定する必要があります。

これらの、プログラマが書かなければいけない型は、実行時には使われないことからアノテーションに近いものとも取れますが、実際には 誤動作せず止まることの証明 を書いていると解釈するべきではないでしょうか。

全称型を使ってチャーチエンコーディング

単純型付きラムダ計算では、体系に組み込みの自然数が入っていなければ計算ができません*3が、全称型を使うと自然数(と解釈できるラムダ項)が作れます。

自然数と解釈できるラムダ項の型は、以下のようになっています。

 \forall T. (T→T)→T→T

この型を持つラムダ項は、以下のようなものがあります。

  •  \Lambda T^ * . \lambda s^{T→T}. \lambda z^{T}. z
  •  \Lambda T^ * . \lambda s^{T→T}. \lambda z^{T}. s \ z
  •  \Lambda T^ * . \lambda s^{T→T}. \lambda z^{T}. s \ (s \ z)
  •  \Lambda T^ * . \lambda s^{T→T}. \lambda z^{T}. s \ (s \ (s \ z))

これらは、順に0、1、2、3、と解釈できるラムダ項であり、以下同様につづけられます。

そのほか、Bool, Tuple, Listのような有用なデータ構造もチャーチエンコーディングを用いて記述することができることが知られていますが、全称型を使うことでそれらを適切に型付けすることができます。

わからなかったこと

 \lambda x. x \ xという項には、 (\forall X. X→X)→(\forall X. X→X)という型がつきます。また、 \lambda y.\lambda z. zという項には \forall Y. Y→\forall Z. Z→Zという型がつきます。この二つを組み合わせた (\lambda x. x \ x)(\lambda y.\lambda z. z)は、簡約が停止します。しかし、どうも型検査には通らないような気がします。これが意味することはなんでしょう?

  • (可能性1) 全称型だけでは、型付けできない。もっと強力な型システムが必要となる。
  • (可能性2) 確かに止まるが、if true then 1 else falseのような項と同様に、静的にはどんな型も持たない(『型システム入門』p.70)。
    • 同じ型を持ち、止まらない、あるいは結果の型が異なる、そういった項が存在するということ?
      • 少なくとも、型 \forall Y. Y→\forall Z. Z→Zを持つ項は \lambda y.\lambda z. zと外延的に等しい項しか存在しない(パラメータ性と呼ばれる強力な原理。『型システム入門』p.282)はずで、 (\forall X. X→X)→(\forall X. X→X)という型が付く別の項があるということになる?
        •  id [\forall X. X→X ]みたいなものは確かにこの型を持つけれど、結果は同じになるような?

演算子

List XやPair A BなどにあらわれるListやPairは、型に関する関数、つまり型演算子になっています。

さらに高階の型演算子まですべてを入れた体系は、 \lambda_\underline{\omega}と呼ばれます。

わからなかったこと

演算子があると、型付けできるラムダ項が増えるか?(List, Pairなどは全称型を使った型付けも可能でした)

  • (可能性1) 型付けできるラムダ項は増えない。
    • (可能性1a) 単に、List Xなどと読みやすい記述ができるようになるだけである。もちろん、読みやすい記述は重要です。
    • (可能性1b) fls : Boolzro : Natnil : List Xなど、 \lambda x. \lambda y. yという同じ形無し項になってしまうものたちに対する型付けが取り違えられる可能性を消すことに有用(むしろ型付けできるラムダ項は減る)。
    • (可能性1c) 全称型を含む場合、プログラマが型を記述する必要がある。この記述量が指数的に増加することを防ぐ。とはいっても、型検査器は展開する必要がある気がします(特に、依存型と組み合わせた場合)。
  • (可能性2) 型付けできるラムダ項は増える。
    • 『型システム入門』p.365 演習30.4.2「F_4なら書けるプログラムで、有用なものは存在するだろうか。」とあるので、暗に(有用ではないにしろ)存在することが示唆されている。

依存型

依存型とは、項に依存した型のことです。たとえば、リストを結合するmerge関数は、IntList n→IntList m→IntList (n+m)のような型を持つみたいなことが書けるようになります。

依存型を持つ体系は、Curry-Howard対応では述語論理に対応します。全称型のところで \forallが出てきたのは、述語論理の \forallではありません。あれは、 型=命題論理式に関する量化 になっています。依存型は、 項=議論領域の要素に関する量化 です。(全称型を含む体系が二階ラムダ計算と呼ばれるのも混乱の元です。対応するのは二階論理ですが、二階論理と言ったら、普通は二階述語論理のことを意味します。本当は二階命題論理のことなのですが、二階命題論理という単語は聞きなれません。)

わからなかったこと

依存型があると、型付けできるラムダ項が増えるか?

  • (可能性1) 依存型は、型付けできるラムダ項を増やさない。
    • プログラムの性質を記述することができるようになるだけ?
    • Wikipediaにそんなことが書いてあったような気がしました。
  • (可能性2) 依存型は、型付けできるラムダ項を増やす。
    • 依存型を使うと、特定の入力に対しては止まらない関数(部分関数)について、止まると証明できる入力しか来ないことを保証できる。依存型がなければ、そのような項は止まらないことから型付けできないことが従うが、依存型があれば(必ず止まるので)型付けできるという可能性がかなりありそうな気がします。

*1:使われ方によってはInt→Intみたいな具体的な型として型再構築される場合もありますが、下の例のような多相的な使い方は不可能です

*2:実際はΛXを書く必要がありますが、これはあくまで型の注釈であり、型を消去すればλx.xになります

*3:特に、型環境が空の場合、型の付く項は一つもありません。全称型がある場合、型環境が空であってもいろいろな項に型がつきます。