型付きλ計算とHaskell
MenuHaskell を動かしながら、型付きλ計算を理解しよう。
項の構築
primitive data type がいくつかあり、それは項(term)である。
1 'a'次に、変数を導入する。変数は項である。 変数には primitive data が入る。例えば整数とか、例えば文字列とか。あるいは、任意の項とか。
x = 'a'(Haskell では let x = 'a' を使う)
次にλ式を導入する。変数 x を含む(あるいは含まない)項 R x があった時に、 \ x -> R x は項である。項なので変数に代入することができる。
id = \ x -> x
\x -> R x は入力を一つ受け取る関数である。 関数を作る方法はここまでではこれしかない。
ある項からλ項を作るのは、項の変換になる。これを以下のように横線を使って書く。この作り方を→Iと名付ける。I は introduction である。
R x ------------------ →I \ x -> R x関数fを呼び出すには、関数の項に後ろに引数となる項xを書く。
f xここまでで、項は、primitive data type と変数とλ式しかない。これらを組み合わせたものが項になる。
α変換
λ式 \ x -> R x に引数 'a' を渡すと、後ろの項の x を、その値で置き換えた R 'a' を返す。これをα変換という。あるいは、λ式の関数適用である。これが、λ式の意味だと思っても良い。(操作的意味)これは二つの項から一つの項を作る、つまり、項を減らす操作になる。これを以下のように書く。この作り方を→Eと名付ける。E は Elimination である。
( \ x -> R x ) y --------------------------- -→E R yここで R x は変数xを含む、あるいは含まない任意の項である。あるいは、その項を表すメタ変数である。
id '1'を Haskell で実行してみよう。また、
( \ x -> x ) '1'を実行してみよう。
型の構築
型は、λ計算の整合性を保証するために必要となる。まず、primive な data 型がある。ある値が型を持つことを :: で表す。
'a' :: Char二つの型 a b があった時に、a を入力として b を返す関数の型を、
a -> bと書く。二つの入力 a と b があって、型 c を返す場合は、
a -> b -> cと書く。
a -> ( b -> c )これは、a を受けとって、b -> c という関数を返す関数である。
( a -> b ) -> cこれは、関数を受けとって、c という型を返す関数である。この関数の入力は一つである。
型 a を持つ項 x を含む型 b を持つ項 R x : b に対して、λ式を作ると、a -> b が作られる。
b ----------------------------------- →I a -> ba -> b は関数で、これに型 a の値を引数として与えると、
a -> b a ----------------------------------- →E bとなる。これは→の導入と削除になっている。
型と項は同時に操作される
この操作は、型と値と両方同時に起きている。つまり、
x : a と r x : bから、
\ x -> r x : a -> bが作られる。あるいは、
\ x -> r x : a -> b と y : aから、
r y : bが作られる。
id : a -> a という型を持つ項を作りたいとする。その項をλ項として構築するのを以下のように記述する。
id : a -> a id = \x -> xこれは Haskell のプログラムそのものである。
論理式としての型
型 a を命題変数だと思う。
a -> bは「a ならば b 」である。
b が成立していれば、
a -> bが常に正しい。つまり、
b ----------------------------------- →I a -> bまた、a -> b が常に正しくて、a が正しければ b が成立する。
a -> b a ----------------------------------- →E bここまでの範囲で、λ計算の型と論理式のとが対応していることがわかる。この変換はλ項の構築に対応しているので、論理式の証明がλ項の対応することになる。
論理式 ⇔ 型 証明 ⇔ λ項
しかし、∧とかが出てこない。この対応を維持したまた、論理を拡張できるのかというのが問題になる。
直積
∧ は型を二つとる二項演算子である。a と b が型なら、 a ∧ b も型になる。
a b ----------------------------------- ∧I a ∧ bもし、a ∧ b が正しければ、 a は正しい
a ∧ b ----------------------------------- ∧E1 ab の方もある。
a ∧ b ----------------------------------- ∧E1 bこの∧I, ∧E1, ∧E1 に相当するλ項を新しく導入したい
p1 : a, p2 : b があった時に、
p1 × p2 : a ∧ bとなって欲しい。そして、p : a ∧ b があった時に、
π1 p : a π2 p : bとなって欲しい。× と π1 と π2 が新しく導入する項になる。この項に対応する操作を定義する。
p1 : a p2 : b ----------------------------------- ∧I p1 × p2 : a ∧ b p : a ∧ b ----------------------------------- ∧E1 π1 p : a p : a ∧ b ----------------------------------- ∧E2 π2 p : bこれらは Haskell では以下のような構文を使う
data Product a b = P { x :: a , y :: b } let p = P 'a' 1 x p y pそれぞれの型を確認してみよう。
直積を使った証明
Sum 排他的和
∧ はできたが、∨ はどうしよう? ∧の上下をひっくり返すと良さそうに思える。
a ----------------------------------- ∨E1 a ∨ b b ----------------------------------- ∨E2 a ∨ bこっちは良さそう。
a ∨ b ----------------------------------- a bこれはよろしくない。下は一つでないと。
a ∨ b ----------------------------------- : : ----------------------------------- cとなるのが望ましい。
a ∨ b a -> c b -> c -------------------------------------- ∨I cというのが正しそう。この∨は、命題論理の∨と少し違う。
これに対応する項は、
x : a ----------------------------------- ∨E1 L x : a ∨ b y : b ----------------------------------- ∨E1 R y : a ∨ b s : a ∨ b i1 : a -> c i2 : b -> c -------------------------------------------------------------- ∨I ?