ラムダ計算とは
ラムダ計算とは、簡単に言ってしまうと関数だけから成り立つ計算モデルで、すべての計算可能な関数が表現でき、正しく評価できるものらしいです。
関数型言語の理解も深まるだろうということで、最近勉強しています。
やってみると、なかなか面白く、なるほどの連続です。
では、実際どのように表現できるのか見ていこうかと思います。
チャーチ数
ラムダ計算において、自然数をどのように表現するのか？
そこで登場するのがチャーチ数と呼ばれる、関数の適用回数で表現するものです。
例えば、０はどのように表現されるか？OCamlを使って書くと
# let zero = fun f -> fun x -> x ;;
となります。
fは任意の関数、xは任意の値で、上記のzeroは任意の関数fを任意の値xに０回適用、つまり何もせずに返す、ということになります。
これは自然数０の「どんな数も０回足しても元の数になるという性質」に対応しているということらしいです。
確かにそのとおりですね。学者の方はすごいことを考えるものです。
ではチャーチ数を自然数に変換するにはどうすればよいのでしょうか？
チャーチ数を自然数に変換するto_intという関数を作ってみましょう。
# let to_int = fun n -> n (fun k -> k + 1) 0 ;;
(fun k -> k + 1)はインクリメントする関数、0は初期値です。
これをzeroに適用すると
# to_int zero ;;
(**
=> (fun n -> n (fun k -> k + 1) 0) zero
=> zero (fun k -> k + 1) 0
=> (fun f -> fun x -> x) (fun k -> k + 1) 0
=> 0
*)
0
ということになり、自然数０に変換されます。
その他のチャーチ数も試してみたいので、succという関数を作ってみましょう。
# let succ = fun n -> fun f -> fun x -> f (n f x) ;;
このsucc関数を使って、チャーチ数１を作ってみます。
# let one = succ zero ;;
(**
=> (fun n -> fun f -> fun x -> f (n f x)) zero
=> f (zero f x)
=> f x
*)
上記の場合、任意の値xに任意の関数fを１回適用しているので、チャーチ数的には１を表すことになります。
ではチャーチ数２はどうでしょうか？
# let two = succ one ;;
(**
=> (fun n -> fun f -> fun x -> f (n f x)) one
=> f (one f x)
=> f ((f x) f x)
=> f (f x)
*)
確かに任意の関数fを２回適用しています。
これが関数適用の回数で自然数を表現するということなのでしょう。なるほど
では先程のチャーチ数１を自然数に変換
# to_int one ;;
(**
=> (fun n -> n (fun k -> k + 1) 0) one
=> one (fun k -> k + 1) 0
=> (f x) (fun k -> k + 1) 0
=> (fun k -> k + 1) 0
=> 1
*)
1
ちゃんと自然数に変換できました。
チャーチブール値
ブール値はどのように表現するのでしょう。
# let true' = fun x -> fun y -> x ;;
# let false' = fun x -> fun y -> y ;;
なるほど、xのほうがthen節にあたり、y節のほうがelse節にあたるというわけです。
こちらもまた通常のtrueとfalseに変換できる関数を作っておきます。
# let to_bool = fun church_bool -> church_bool true false ;;
# to_bool true' ;;
(**
to_bool true'
=> (fun church_bool -> church_bool true false) true'
=> true' true false
=> (fun x -> fun y -> x) true false
=> true
*)
true
# to_bool false' ;;
(**
to_bool false'
=> (fun church_bool -> church_bool true false) false'
=> false' true false
=> (fun x -> fun y -> y) true false
=> false
*)
false
ブール値が表現できたら、If文も使いたい。
# let if' = fun cond -> fun thn -> fun els -> (cond thn) els ;;
では、さっそく使ってみましょう。もしtrueならoneをfalseならzeroを、という式にしてみます。
# let result = if' true' one zero ;;
(**
if' true' one zero
=> (fun cond -> fun thn -> fun els -> cond thn els) true' one zero
=> true' one zero
=> (fun x -> fun y -> x) one zero
=> one
*)
# to_int result ;;
1
うまくいきました。なるほどな
まとめ
今回はラムダ計算の勉強の途中経過を書きました。
ラムダ計算を勉強してみると、なんとなくアハ体験的なものがありました。もちろん、まだまだ序章に過ぎませんが。
ちなみにYコンビネータ及びZコンビネータは、OCamlでは素直にはできませんでした。どうやらひと工夫する必要がありそうです。