53ningen.com53ningen.com
Loading...

ラムダ計算について調べた（前編）

2014/11/28 11:36
2024/12/30 17:53
Programming
ラムダ計算
関数プログラミングとその背景にある数学的なお話を理解する上でラムダ計算の知識が必要そうなので，確認していきます． というかなんかよくよく調べていくと，「計算機科学の理論としては常識」とか書いてあったりするので，あせって基礎をさらいました． まずは型なしのラムダ計算まで． 間違ったところがあったらご指摘頂けると嬉しいです．

ラムダ計算とは何か？

Wikipediaによるとラムダ計算とは次のようなものとされています．
ラムダ計算（lambda calculus）は、計算模型のひとつで、計算の実行を関数への引数の評価（evaluation）と適用（apply）としてモデル化・抽象化した計算体系である。ラムダ算法とも言う。
ラムダ計算では，関数をラムダ抽象を使って記述します． たとえば f(x)=2x+1 なる関数は f=λx.2x+1 というように書きます． こうすることにより，関数を返す関数などを定義することができるようになります． また名前をつけずに値のように関数を取り扱えるようになりました．
たとえば， g(x,y)=x+2y+1 は g=λx.(λy.x+2y+1) といったように 2変数関数は，1変数を返す関数として定義することができます．このような変換をカリー化(currying)とよびます． また関数を値として受け取ったり，返したりする関数のことを高階関数(higher-order function)とよびます．
関数に値を適用したい場合はラムダ抽象の後ろに値を書けば良いです． たとえば f(x)=2x+1 に x=2 を適用するときは ((λx.2x+1)2) と書きます． これを関数適用といいます．
またλx.x+y についてx は束縛されているといい y は自由であるといいます．
[amazon template=wishlist&asin=4781911358]

型なしラムダ計算（lambda calculus）

ラムダ式の構文

型なしラムダ計算の抽象構文は e::=x|λx.e|e1e2 のように定義されます． 単純にいうとラムダ式は，変数か，ラムダ抽象か，関数適用から構成されるということです．

ラムダ計算の実行

ラムダ計算の実行はα-変換，β-簡約，η-変換の３つの操作に抽象化できます．
  • α-変換（α-conversion）
    • λx.M→αλy.M[x:=y]
    • 束縛変数の名前はMの中に自由なyがなければ置き換えられる：λx.f⇒λy.f[x→y]
  • β-簡約（β-reduction）
    • (λx.M)N→βM[x:=N]
    • 関数適用そのものを指す：λx.fy⇒f[x→y]
  • η-変換（η-conversion）
    • λx.Mx→ηM
    • 関数の外延性を表す：λx.fx⇒λy.f

ラムダによるデータの表現

自然数

以下のように自然数をラムダ式で表せる．このようなラムダ式をチャーチ数（Church Number）とよびます．
  • 0 を λs.λz.z
  • 1 を λs.λz.sz
  • 2 を λs.λz.s(sz)
これは足し算を plus=λg1.λg2.λs.λz.g2sg1z を定義して， plus 1 2 などを計算してみると納得がいくと思います

論理値

論理値 true は λt,λf.t ，false は λt.λf.f とすると， if e1 then e2 else e3 を e1e2e3 としてうまい具合にif-elseの構造を表せる． これは if true then e1 else e2 = true e1 e2 = (λt.λf.t)e2e3 →(λt.e2)e3→e2 かつ if false then e1 else e2 = false e1 e2 = (λt.λf.f)e2e3 →(λf.g)e3→e3 となることから納得がいくと思います．
その他 この資料 が結構良い感じにまとまっています
あと以下の本あたりがわかりやすくておすすめです。
[amazon template=wishlist&asin=487311697X]