読者です 読者をやめる 読者になる 読者になる

ラムダ計算基礎文法最速マスター

ラムダ計算は, 多くのプログラミング言語, とくに関数型言語の原形になっています. ラムダ計算について理解しておくことは, 多くのプログラミング言語の習得に役立つでしょう.

ラムダ計算チューリング完全で, 計算能力としてはふつうのプログラミング言語と同じです. ラムダ計算で計算を書く訓練をしておくことは, 任意の計算を関数のみを使って(他の制御構文を用いずに)書くときに役立ちます. ふつうに書いたら煩雑な処理を, 関数型言語のやり方で書くとすっきりすることが多々あり, コードを自由自在に書くためには必須の考え方と言えるでしょう.

ラムダ計算の式を項(term)と言います. 項は変数, 抽象, 適用のいずれかです.

変数

変数(variable)はふつう1文字で書きます. 変数には関数内の束縛変数(bound variable)自由変数(free variable)かという区別があります. 関数を値に適用する以外のやり方で変数に値を代入することはできません.

x      # 変数は項
λx.x   # xは束縛変数
λx.y   # yは自由変数
抽象

関数を作る構文を抽象(abstraction)と言います. 抽象はλx.Mという形で, 「本体がMで1引数xを取る関数」という意味になります.

λx.x       # 受け取った引数をそのまま返す関数
λx.(λy.x)  # xを受け取って, (何か引数を受け取ってxをそのまま返す関数)を返す関数

2つ目のように関数が入れ子になっているものを高階関数(higher-order function)と言います. 高階関数ではしばしば括弧を省略し, λの連続も省略して, 複数の引数を取る関数のように書きます.

λx.λy.x   # 括弧を省略
λxy.x     # λを省略
適用

関数を呼び出すことを適用(application)と言います. 適用はM Nという形で, 「引数Nに関数Mを適用する」という意味になります.

(λx.x) y         # yにλx.xを適用
((λx.λy.x) a) b  # aにλx.λy.xを適用したものをbに適用

適用の場合もしばしば括弧を省略します. 抽象と適用の両方がある場合, 適用は左に結合し, 抽象はできるだけ右に伸ばして読みます.

(λx.λy.x) a b  # 括弧はこれ以上省略できない
(λxy.x) a b    # λも省略
その他の約束

束縛変数は, 自由変数や他の束縛変数と重ならないように適宜名前を替えます. 束縛変数の名前が違うだけの項は同じ項として扱われます. たとえば, 以下の項はすべて同値に扱われます. これをα同値(α-equivalence)と言い, 同値な項に書き換えることをα変換(α-conversion)と言います.

λxyz.x z (y z)
λzyx.z x (y x)
λabc.a c (b c)

簡約

ラムダ計算の式を実行することを簡約(reduction)と言います. 左辺が抽象になっている適用があれば, 抽象の本体の束縛変数適用の右辺で置き換えたものへと簡約することができます*1.

(λx.x) a
  → a
(λx.λy.x) a
  → λy.a
(λxy.x) a b
  → (λy.a) b
  → a
(λxyz.x z (y z)) (λxy.x) λxy.x
  = (λxyz.x z (y z)) (λxw.x) λxy.x  # yが重ならないようにα変換
  → (λyz.(λxw.x) z (y z)) λxy.x
  → λz.(λxw.x) z ((λxy.x) z)
  → λz.(λw.z) ((λxy.x) z)
  → λz.z

簡約できる部分が複数あるときは, どこから簡約しても構いません. これ以上簡約できない項のことを正規形(normal form)と言い, どのような順序で簡約しても正規形は必ず同じ形になります*2. ただし, どんな項でも簡約していけば正規形になるというわけではありません. たとえば, 無限ループするような項もあります.

(λx.x) a
  → a          # 変数はこれ以上簡約できないので正規形
(λxy.x) a
  → λy.a       # λが残っていてもこれ以上簡約できないので正規形
(λxyz.x z (y z)) a (λxy.x) c
  → (λyz.a z (y z)) (λxy.x) c
  → (λz.a z ((λxy.x) z)) c
  → (λz.a z λy.z) c
  → a c λy.c   # 適用の形でもこれ以上簡約できないので正規形
(λx.x x c) (λx.x x c)
  → (λx.x x c) (λx.x x c) c
  → (λx.x x c) (λx.x x c) c c
  → (λx.x x c) (λx.x x c) c c c
  → ...        # 無限ループ
(λxy.x) a ((λx.x x c) (λx.x x c))
  → (λy.a) ((λx.x x c) (λx.x x c))       # 一番左の抽象を先に簡約
  → a          # 正規形に簡約できる
(λxy.x) a ((λx.x x c) (λx.x x c))
  → (λxy.x) a ((λx.x x c) (λx.x x c) c)  # 引数の抽象を先に簡約
  → (λxy.x) a ((λx.x x c) (λx.x x c) c c)
  → (λxy.x) a ((λx.x x c) (λx.x x c) c c c)
  → ...        # 無限ループ(正規形にならない順序を選択したため同じ形に簡約されない)

自然数

ラムダ計算自然数はありません. 「ありません」では困るので, 項を使って自然数を定義します. 以下のように定義された自然数チャーチ数(Church numeral)と言います.

0 = λsz.z
1 = λsz.s z
2 = λsz.s (s z)
3 = λsz.s (s (s z))
・
・
・
n = λsz.sn z  # snはsをn回適用

演算も定義できます.

M+N = (λmnsz.m s (n s z)) M N  # M, Nの和
M*N = (λmnsz.n (m s) z) M N    # M, Nの積
M^N = (λmnsz.n m s z) M N      # MのN乗

2 + 3
  = (λmnsz.m s (n s z)) (λsz.s (s z)) (λsz.s (s (s z)))
  = (λmnsz.m s (n s z)) (λxy.x (x y)) (λxy.x (x (x y)))
  → (λnsz.(λxy.x (x y)) s (n s z)) (λxy.x (x (x y)))
  → λsz.(λxy.x (x y)) s ((λxy.x (x (x y))) s z)
  → λsz.(λy.s (s y)) ((λxy.x (x (x y))) s z)
  → λsz.(λy.s (s y)) ((λy.s (s (s y))) z)
  → λsz.(λy.s (s y)) (s (s (s z)))
  → λsz.s (s (s (s (s z))))
  = 5

2つ組

ラムダ計算にデータ構造はないので, 項を使って作ります.

[P, Q] = λx.x P Q  # cons
fst = λp.p λxy.x   # car
snd = λp.p λxy.y   # cdr

p1 = [ [a, b], [c, d] ]
fst (snd p1)
  = (λp.p λxy.x) ((λp.p λxy.y) (λx.x (λy.y a b) (λz.z c d)))
  = (λp.p λxy.x) ((λp.p λwv.v) (λx.x (λy.y a b) (λz.z c d)))
  → (λp.p λxy.x) ((λx.x (λy.y a b) (λz.z c d)) λwv.v)
  → (λp.p λxy.x) ((λwv.v) (λy.y a b) (λz.z c d))
  → (λp.p λxy.x) ((λv.v) (λz.z c d))
  → (λp.p λxy.x) (λz.z c d)
  → (λz.z c d) λxy.x
  → (λxy.x) c d
  → (λy.c) d
  → c

条件分岐

ラムダ計算には真偽値もifもないので, 項を使って作ります.

true = λxy.x
false = λxy.y
if B then P else Q = B P Q

if true then a else b
  = (λxy.x) a b
  → (λy.a) b
  → a

ループ

ループは基本的に再帰呼出しで書きます. ただし, 再帰呼出しの構文は無いので, 不動点コンビネータ(fixed-point combinator)を使います. 有名なものはYコンビネータで, 次のような項です.

Y = λf.(λx.f (x x)) (λx.f (x x))

再帰したい関数は第1引数に自分自身が渡されてくると思って定義しておきます.

F = λf.λx. ... (f x) ...  # (f x)は再帰呼出し

実際に使うときは, (Y F)とすると, fが(Y F)自身に置き換わった再帰関数として使えます. これは, (Y F)を引数に適用したものを簡約して正規形が得られるなら, F (Y F)を引数に適用したものも同じ正規形に簡約される性質を利用しています.

処理系

ラムダ計算の定義はとても単純なので, 自分で処理系を書いてみると理解の助けになります. 既存の処理系としては以下のものがあります.

他にもObjective CamlHaskellなどの言語では型付ラムダ計算に相当する式が書けます. ラムダ計算について理解した後には, これらのプログラミング言語を実際に使いながら単純型付ラムダ計算について学ぶとよいでしょう.

追記

2010-02-08T14:30+0000 ブックマークコメントへの返信

1.「左(右)結合」というのは同一の演算子が続くときにどちらから結合するかの話ではなかったか 2.λxyz.x z (y z)の(y z)の意味がわからず

1.について, 「結合」はその通りです(ただし, 結合は演算についての話であって, 必ずしも演算子についてではなく, 適用は演算子がない, あるいは演算子が空白の演算です). 抽象と適用の両方が出てくる場合は, 適用に関しては左から右に読むのではなく, 右から左に結合して読んでいくと混乱が少ない, という意味です.

2.について, (y z)はzにyを適用するという意味です. yに抽象が代入されれば(y z)は簡約できます. そうでなければ(y z)は適用の形のまま残ります.

2010-02-09T09:09+0000

正規形に関する例を追加.

2010-02-15T03:01+0000

α変換で名前を替えようとしている変数をで, 簡約しようとしている適用を下線で, 簡約しようとしている適用の左辺の抽象のλと束縛変数をで強調.

2010-02-16T08:09+0000

下線を適用の右辺のみにしました. また, α変換を1ステップの=で明示するようにしました.

2010-03-25T08:50+0000

JavaScriptの構文での入出力、簡約過程の可視化が可能なラムダ計算インタプリタを作りました:


2012-01-29T22:06+0000

1つ目の参考文献の型付ラムダ計算の章の前半について, 某所で輪講の発表を担当する機会があったので, その時のスライドを置いておきます:

あとがき


参考文献

論理と計算のしくみ

論理と計算のしくみ

Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics)

Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics)

*1:正確にはこれはβ簡約(β-reduction)と呼ばれるもので, 数ある簡約のうちの一つです.

*2:これをChurch-Rosserの定理と言います.

広告を非表示にする