Calculus of Constructions で遊ぶ
※この記事は間違っているかもしれないので、注意深く読んでください
※気力があれば追記するかも
※なんか定義なしにいきなり使った場合は Wikipedia に書いてあるかも
Calculus of Constructions (CoC) は型付きラムダ計算の一種で、多相型、多相関数、依存型の機能を持つ
カリー゠ハワード同型対応によると、命題↔型、証明↔プログラムである
つまり、命題を型にエンコードしてその型を持つ項を作れば証明になる
ここでは、さまざまなものを CoC 上で扱ってみる(予定)
なお、型付け規則については Wikipedia を参照のこと
項
CoC の項は以下(なお、CoC では型と値を同列に扱う)
$ \mathbf P: 命題の型
$ \mathbf T: $ \mathbf Pの型 それ以外の用途ってある?
$ \lambda x: A.\ N: ラムダ抽象
変数$ xに型$ Aの値を束縛するという意味
$ \forall x: A.\ B: ラムダ抽象$ \lambda x: A.\ Nの型(ただし$ N: Bとする)
単純型付きラムダ計算では$ A \to Bと書かれがちだが、 CoC では依存型があるので$ xを使える
$ Bが$ xを含まないときは単に$ A \to Bと書くことが多い
これ自体にも型はあって、$ B: Kのとき$ (\forall x: A.\ B): K
$ N\ M: 関数適用
論理演算
型を命題とみなすと、それに対する演算は型から型への演算ということになる
含意$ P \to Q \quad\equiv\quad \forall x: P.\ Q
否定$ \neg P \quad\equiv\quad \forall Q: \mathbf P.\ P \to Q
「矛盾からはすべてを導ける」
「外は雨が降っており、かつ、雨は降っていない」という前提から、「源義経の母親はナポレオンである」という結論を導ける
論理積$ P \wedge Q \quad\equiv\quad \forall R: \mathbf P.\ (P \to Q \to R) \to R
論理和$ P \vee Q \quad \equiv \quad \forall R: \mathbf P. (P \to R) \to (Q \to R) \to R
存在量化$ \exist x: A.\ P \quad\equiv\quad \forall Q: \mathbf P.\ (\forall x: A.\ P \to Q) \to Q
また、これらの演算はデータ型にもなる(例:論理積→$ P \times Q、存在量化→トレイト)
自然数
CoC では、自然数はチャーチ数を使って以下のように表現される
(これは、自然数の型$ Aと後者関数$ s、零$ zを受け取り$ sを$ zに適用する関数である)
$ \text{Nat}{\color{lightgray}: \mathbf P} := \forall A {\color{lightgray}: \mathbf P}.\ (A \to A) \to A \to A
$ 0{\color{lightgray}: \text{Nat}} := \lambda A{\color{lightgray}: \mathbf P}.\ \lambda s{\color{lightgray}: A \to A}.\ \lambda z{\color{lightgray}: A}.\ z
$ 1{\color{lightgray}: \text{Nat}} := \lambda A{\color{lightgray}: \mathbf P}.\ \lambda s{\color{lightgray}: A \to A}.\ \lambda z{\color{lightgray}: A}.\ s\ z
$ 2{\color{lightgray}: \text{Nat}} := \lambda A{\color{lightgray}: \mathbf P}.\ \lambda s{\color{lightgray}: A \to A}.\ \lambda z{\color{lightgray}: A}.\ s\ (s\ z)
$ 3{\color{lightgray}: \text{Nat}} := \lambda A{\color{lightgray}: \mathbf P}.\ \lambda s{\color{lightgray}: A \to A}.\ \lambda z{\color{lightgray}: A}.\ s\ (s\ (s\ z))
$ \vdots
自然数の後者関数は次のように定義できる
$ \text{succ}{\color{lightgray}: \text{Nat} \to \text{Nat}} := \lambda n{\color{lightgray}: \text{Nat}}.\ \lambda A{\color{lightgray}: \mathbf P}.\ \lambda s{\color{lightgray}: A \to A}.\ \lambda z{\color{lightgray}: A}.\ n\ (A\ s\ (s\ z))
加算、乗算
$ \text{add}{\color{lightgray}: \text{Nat} \to \text{Nat} \to \text{Nat}} := \lambda m{\color{lightgray}: \text{Nat}}.\ \lambda n{\color{lightgray}: \text{Nat}}.\ \lambda A{\color{lightgray}: \mathbf P}.\ \lambda s{\color{lightgray}: A \to A}.\ \lambda z{\color{lightgray}: A}.\ m\ A\ s\ (n\ A\ s\ z)
$ \text{mult}{\color{lightgray}: \text{Nat} \to \text{Nat} \to \text{Nat}} := \lambda m{\color{lightgray}: \text{Nat}}.\ \lambda n{\color{lightgray}: \text{Nat}}.\ \lambda A{\color{lightgray}: \mathbf P}.\ \lambda s{\color{lightgray}: A \to A}.\ \lambda z{\color{lightgray}: A}.\ m\ A\ (n\ A\ s)\ z
ブール値
ブール値は、チャーチエンコーディングでは、二つの変数を受け取ってどちらかを返す射影関数として定義される
$ \text{Bool}{\color{lightgray}: \mathbf P} := \forall A{\color{lightgray}: \mathbf P}.\ A \to A \to A
$ \text{true}{\color{lightgray}: \text{Bool}} := \lambda A{\color{lightgray}: \mathbf P}.\ \lambda x{\color{lightgray}: A}.\ \lambda y{\color{lightgray}: A}.\ x
$ \text{false}{\color{lightgray}: \text{Bool}} := \lambda A{\color{lightgray}: \mathbf P}.\ \lambda x{\color{lightgray}: A}.\ \lambda y{\color{lightgray}: A}.\ y
ブール値に対する演算
$ \text{not}{\color{lightgray}: \text{Bool} \to \text{Bool}} := \lambda t{\color{lightgray}: \text{Bool}}.\ t\ \text{Bool}\ \text{false}\ \text{true}
$ \text{and}{\color{lightgray}: \text{Bool} \to \text{Bool} \to \text{Bool}} := \lambda t{\color{lightgray}: \text{Bool}}.\ \lambda u{\color{lightgray}: \text{Bool}}.\ t\ \text{Bool}\ u\ \text{false}
$ \text{or}{\color{lightgray}: \text{Bool} \to \text{Bool} \to \text{Bool}} := \lambda t{\color{lightgray}: \text{Bool}}.\ \lambda u{\color{lightgray}: \text{Bool}}.\ t\ \text{Bool}\ \text{true}\ u
$ \text{xor}{\color{lightgray}: \text{Bool} \to \text{Bool} \to \text{Bool}} := \lambda t{\color{lightgray}: \text{Bool}}.\ \lambda u{\color{lightgray}: \text{Bool}}.\ t\ \text{Bool}\ (\text{not}\ u)\ u
$ \text{thus}{\color{lightgray}: \text{Bool} \to \text{Bool} \to \text{Bool}} := \lambda t{\color{lightgray}: \text{Bool}}.\ \lambda u{\color{lightgray}: \text{Bool}}.\ t\ \text{Bool}\ u\ \text{true}
命題論理
命題論理における命題を証明してみる
証明は、前提の証明、つまり前提を型とする値を受け取って証明を返す関数という形で書く
まずは、モーダス・ポネンスを証明してみる
「$ Pならば$ Q、かつ、$ Pであるならば、$ Qである」
これを証明する前に、$ P, Qの型を定義しておく
$ P: \mathbf P
$ Q: \mathbf P
証明したい命題を定式化する
$ \text{modusPonens}: (P \to Q) \to P \to Q
この命題を証明するには、この型に合う値を見つける必要がある
まず、$ \text{modusPonens}は$ P \to Q型の値と$ P型の値を受け取って、$ Q型の値を返す関数であると言える
$ P \to Q型の値は、$ P型の値を受け取って、$ Q型の値を返す関数
ここまでくれば簡単だと思われる
$ \text{modusPonens} := \lambda f{\color{lightgray}: P \to Q}.\ \lambda x{\color{lightgray}: P}.\ f\ x
関数と値を受け取って、関数に値を適用する関数 これがモーダス・ポネンスの証明になる
アリストテレスの三段論法を証明してみる
アリストテレスの三段論法は、「$ Pならば$ Q」と「$ Qならば$ R」という前提から「$ Pならば$ R」を導く
まずは$ P, Q, Rの型を定義
$ P, Q, R: \mathbf P
命題を定式化する
$ \text{syllogism} : (P \to Q) \to (Q \to R) \to (P \to R)
この型に合う値は何か?
$ P \to Qは、型$ Pの値を受け取って型$ Qの値を返す関数の型である
$ Q \to Rも、同様に関数の型である
これらの関数を使って、$ P \to Rという関数を作れないか?→作れる
$ \text{syllogism} := \lambda f{\color{lightgray}: P \to Q}.\ \lambda g{\color{lightgray}: Q \to R}.\ \lambda x{\color{lightgray}: P}.\ g\ (f\ x)
↑これは何をしているか?
最後に返しているのは、$ x: Pを受け取って、それを$ fに適用した結果を$ gに適用したもの
$ f\ xは$ Q、なぜなら$ f: P \to Qだから
$ g\ (f\ x)は$ R、なぜなら$ g: Q \to Rだから
このように証明できた
述語論理
カリー゠ハワード同型対応では、命題が型に対応している
ならば、型に変数を入れることができれば、表現できる命題の種類が大幅に増えるのでは?
これが依存型であり、依存型を使うと述語論理を表現できる
良くある例題の「ソクラテスは死ぬ」を証明してみる
まず、物の型や、人であるや死ぬといった述語を事前に定義しておく
$ A: \mathbf P
$ \text{isHuman}: A \to \mathbf P
$ \text{isMortal}: A \to \mathbf P
また、ソクラテスを定義する
$ \text{socrates}: A
では、証明する
まずは定義から「もし、すべての人が死に、ソクラテスが人であるのなら、ソクラテスは死ぬ」
$ \text{socratesIsMortal}: (\forall x: A.\ \text{isHuman}\ x \to \text{isMortal}\ x) \to \text{isHuman}\ \text{socrates} \to \text{isMortal}\ \text{socrates}\
これを満たす値を考える
$ \text{socratesIsMortal} := \lambda h{\color{lightgray}: \forall x: A.\ \text{isHuman}\ x \to \text{isMortal}\ x}.\ \lambda p{\color{lightgray}: \text{isHuman}\ \text{socrates}}.\ h\ \text{socrates}\ p
このように、項が定義できたので、証明できた
二階述語論理
依存型に加えて多相型を使うと、述語自体を量化の対象にすることができる
自然数に対する数学的帰納法を証明
数学的帰納法とは、ある述語$ P(n)が以下の条件をどちらも満たすとき、すべての自然数$ nに対し$ P(n)がいえるというもの
$ P(0)
$ \forall n: \text{Nat}.\ P(n) \to P(\text{succ}\ n)
↑長いので$ \text{Next}\ P := \forall n{\color{lightgray}: \text{Nat}}.\ P\ n \to P\ (\text{succ}\ n)と置くことにする
数学的帰納法を定式化する
$ \text{induction} : \forall P{\color{lightgray}: \text{Nat} \to \mathbf P}.\ P\ 0 \to \text{Next}\ P \to (\forall n{\color{lightgray}: \text{Nat}}.\ P\ n)
これに対応する証明は
$ \text{induction} := \lambda P{\color{lightgray}: \text{Nat} \to \mathbf P}.\ \lambda p{\color{lightgray}: P\ 0}.\ \lambda h{\color{lightgray}: \text{Next}\ P}.\ \lambda n{\small\color{lightgray}: \text{Nat}}.\ n\ \mathbf P\ h\ p
$ n: \text{Nat}が与えられた関数を与えられた値に対して$ n回適用する関数ということを思い出す
ジェネリクス
多相型と多相関数を使うとジェネリクス(二階の型)が実現できる
ジェネリックなPair型を定義する
$ \text{Pair}\ A\ B := \forall C{\color{lightgray}: \mathbf P}.\ (A \to B \to C) \to C
Pair型を構築する関数は次のように定義できる
$ \text{pair}{\color{lightgray}: \forall A: \mathbf P.\ \forall B: \mathbf P.\ A \to B \to \text{Pair}\ A\ B} := \lambda A{\color{lightgray}: \mathbf P}.\ \lambda B{\color{lightgray}: \mathbf P}.\ \lambda x{\color{lightgray}: A}.\ \lambda y{\color{lightgray}: B}.\ \lambda C{\color{lightgray}: \mathbf P}.\ \lambda f{\color{lightgray}: A \to B \to C}.\ f\ x\ y
また、要素を取り出す関数は次のように定義できる
$ \text{first}{\color{lightgray}: \forall A: \mathbf P.\ \forall B: \mathbf P.\ \text{Pair}\ A\ B \to A} := \lambda A{\color{lightgray}: \mathbf P}.\ \lambda B{\color{lightgray}: \mathbf P}.\ \lambda p{\color{lightgray}: \text{Pair}\ A\ B}.\ p\ A\ (\lambda x{\color{lightgray}: A}.\ \lambda y{\color{lightgray}: B}.\ x)
$ \text{second}{\color{lightgray}: \forall A: \mathbf P.\ \forall B: \mathbf P.\ \text{Pair}\ A\ B \to A} := \lambda A{\color{lightgray}: \mathbf P}.\ \lambda B{\color{lightgray}: \mathbf P}.\ \lambda p{\color{lightgray}: \text{Pair}\ A\ B}.\ p\ B\ (\lambda x{\color{lightgray}: A}.\ \lambda y{\color{lightgray}: B}.\ y)
ジェネリックなOption型を定義する
$ \text{Option}\ A := \forall C{\color{lightgray}: \mathbf P}.\ (A \to C) \to C \to C
$ \text{some}{\color{lightgray}: \forall A: \mathbf P.\ A \to \text{Option}\ A} := \lambda A{\color{lightgray}: \mathbf P}.\ \lambda x{\color{lightgray}: A}.\ \lambda C{\color{lightgray}: \mathbf P}.\ \lambda f{\color{lightgray}: A \to C}.\ \lambda c{\color{lightgray}: C}.\ f\ x
$ \text{none}{\color{lightgray}: \forall A: \mathbf P.\ \text{Option}\ A} := \lambda A{\color{lightgray}: \mathbf P}.\ \lambda C{\color{lightgray}: \mathbf P}.\ \lambda f{\color{lightgray}: A \to C}.\ \lambda c{\color{lightgray}: C}.\ c
$ \text{unwrapOr}{\color{lightgray}: \forall A: \mathbf P.\ \text{Option}\ A \to A \to A} := \lambda A{\color{lightgray}: \mathbf P}.\ \lambda o{\color{lightgray}: \text{Option}\ A}.\ \lambda a{\color{lightgray}: A}.\ o\ A\ (\lambda x{\color{lightgray}: A}.\ x)\ a
参考
https://en.wikipedia.org/wiki/Calculus_of_constructions
Types and Programming Languages (日本語版)