依存型による定理証明Tips: coherenceは型で表せ

この記事はTheorem Prover Advent Calendar 2016 12日目の記事です。

この記事は定理証明初心者向けの記事です。
普段から依存型を用いた定理証明をされている方は読む必要がありません。

"coherence condition"と呼ばれる条件があり、訳すと「一貫性条件」となるようです。
これはちゃんと定義があるものではないのですが[要出典]、一貫性が保たれているならば当然成り立っているべき条件あるいは定理のことを、一般にcoherence conditionと呼んだりします。

例えば、型がついた言語での関数適用を考えます。

この時、P(Q,R)という項がwell-typedならば、
直感的にはPは2変数であり、QとRを引数に受け取っている、ということになります。
この時、実際にP : A -> B -> C, Q : A, R : Bという型が付くはずですが、この条件がcoherenceです。

ここで重要なのはwell-typednessであり、正しい仕方で構成された項は異常な項を持たない、みたいな性質が効いていて上のようなことが成り立ちます。

もちろんcoherenceはこれだけではなく、至るところに現れます。

こういうcoherenceが成り立つかどうかを判定するために必要な情報は、
全て型に持たせましょう、というのが今回のTipsです。

先程の例では、"well-typed termに含まれる関数適用は、関数の引数の数があっているはずだ"というのが
coherenceでした。
このことを示したい、あるいは関数の引数の数についての命題を証明する必要があるのならば、
関数の引数は型に乗せておくのが便利です。

つまり、この言語の項のなす型Termは、Term (n:N) : Typeとなり、
先のcoherenceは、
P(Q,R): well-typed ==> exists n. P: Term (n+2)のようにかけます。

あるいは、existsと言った扱いが面倒な型を登場させたくなければ、
P(Q,R): Term n ==> P: Term (n+2)
とすればよいです。

これによって、Mがwell-typedな項であるというのは、M: Term nとかける型のことだ、という了解が得られます。

実際に証明をする過程で、coherence conditionは何か？というのを考えることは重要です。
ひとたびcoherenceがわかれば、それに関連する情報は全て型に持たせてやれば、少しだけ証明は楽になると思います。

あるいは自分で型を新たに作らなくとも、既存の型を使うほうが便利なことも多いです。
この場合、例えばListではなくVectorを使うことで、「コンテナの長さ」に関するcoherenceを扱いやすくなります。

最近私は型付きλ計算についての証明を書いたのですが、
context(自由変数に割り当てる型の集まり)の中に変数が出現するかどうか、あるいは出現したものの型は何になるか、
といったcoherenceがよく出てくるので、contextの型に「自由変数の個数」「自由変数のシンボルの集合」
などをのせることで、自由変数の振る舞いによる場合分けが簡単になったりしています。

このように、coherenceが何かを考え、それに対応する情報を型にのせることで
不要な場合分けや細かいチェックなどが省ける場合があるので、よければ参考にしてください。

ということを、1-2年前に知りたかったな〜〜〜と最近思ったので記事にしました。