ラムダ計算と計算可能性
Jacques Garrigue, 2011 年 1 月 17 日

4

ラムダ計算

ドイツの論理学者 Schönfinkel が 1920 年代に作った論理コンビネータは元々論理の証明論のための道具だった。1930 年代に Curry と Church がそれをλ計算に発展させると、論理的な意味と同時に計算的な意味を持つようになった。その後、計算機科学との関係がだんだん深くなり、1950年代からリスプから始まる関数型言語の重要な基礎となった。簡単な定義で表現力が強いので、一般的にプログラミング言語のモデルとして使われる。

4.1

項書換系

元々はそうではなかったが、λ計算は項書換系によって定義される。計算を項の一部の書き換えとして見る、ということだ。例えば、数式の書換系を次のように定義できる。
項 (term)

E ::= R | (E + E) | (E − E) | (E × E) | (E/E)

書換規則

x, y は R の実数ならば、(x + y)(x − y)(x × y)
(x/y)

→→→→

x+yx−yx×yx/y((x + y) は数式だが、 x + y は実数である)
上の規則を簡約規則ともいう。
簡約の例(15 + (1/3)) × (5 − 2) → (15 + 0.3333) × (5 − 2) → (15.3333) × 3 → 46

4.2

λ計算の構文 (syntax)

定義 4.1 λ項 (λ-term) は次の三つの構文からできている。

M::= x| λx.M| M M

変数 (variable)
抽象 (abstraction)
適用 (application)x は文脈 (環境) で定義されている値 (別のλ項) を指す。
λx.M は項 M の中に使われている変数 x を束縛する。関数として見れば f = λx.M という定義は、普段の f (x) = M 。ただし、λx.M と書くとき、名前をつける必要がないという便利さがある。

M1 M2 は関数の適用である。普段の M1 (M2 ) にあたるが、M1 は名前 (変数) だけでなく、どのλ項でもよい。
上の文法を普段の数式と混ぜると、
f (x) = x + 1 のとき f (2)が 1 回で書ける。

(λx.x + 1) 2
構文では括弧を書かなかったが、曖昧性のを解決するに適宜
自由変数と代入 λx.M では、M の中の全ての x の出現は「束縛されている」という。ある項 Mの中で、x が使われながら、束縛されていないのであれば、x は M の自由変数である。M の自由変数の集合 F V (M ) は再起的に次の三条で定義される。

F V (x)= {x}F V (λx.M ) = F V (M ) \ {x}F V (M N ) = F V (M ) ∪ F V (N )代入はそういう自由変数の値を定義する。([N/x]M ) は項 M の中に出現するすべての自由な xを N と置き換える。

([N/x]x)([N/x]y)([N/x]λx.M )([N/x]λy.M )([N/x](M M 0 ))

=
=
=
=
=

N
y
λx.M
λy.([N/x]M )y 6∈ F V (N )0(([N/x]M ) ([N/x]M ))4 条目では、y は N の自由変数であってはならない。そのためには、次のα変換が許される。z はN の自由変数でなければ、λy.N ↔ λz.([z/y]N )こういう束縛変数の改称は常に許される。

4.3

簡約規則

定義 4.2 λ項、α変換と次のβ簡約で構成される項書き換え系はλ計算という。

((λx.M ) N ) → ([N/x]M )例題 4.1 簡約の例

(λf.λg.λx.f x (g x)) (λx.λy.x) (λx.λy.x)→ λx.((λx.λy.x) x ((λx.λy.x) x))→ λx.((λy.x) (λy.x))→ λx.x(λx.(x x)) (λx.(x x))→ (λx.(x x)) (λx.(x x))→ ...
2

定理 4.1 λ計算は合流性を持つ。M → . . . → N と M → . . . → P という二つの簡約があれば、N → . . . → T , P → . . . → T となるような T が存在する。

4.4

λ計算は万能である

全てのプログラムはλ計算で書ける。
自然数

チャーチによるエンコーディングがある (Church numeral)。

cn = λf.λx.(f . . . (f x) . . .)f を n 回適用する
c+ = λm.λn.λf.λx.(m f (n f x)) 加算
c× = λm.λn.λf.(m (n f ))積算
練習問題 4.1

1. (c3 (λx.x x) y) の標準形を計算せよ。

2. (c2 (λx.x x) s) の標準形を計算せよ。
3. 指数のλ項を与えよ。
ブール環

次のエンコーディングを使う。

t = λx.λy.x

f = λx.λy.y

not = λb.λx.λy.(b y x)数の区別も可能で、例えば次の項が引き数に数をもらい、真偽値を返す。

if0 = λn.(n (λx.f) t)組

λ計算では組が簡単に表現できる。

pair = λx.λy.λf.(f x y)

fst = λp.(p t)snd = λp.(p f)

計算して見ると、fst (pair a b) → pair a b t → (t a b) → a
引き算

チャーチエンコーディングによる引き算は比較的に難しい。ここに一つの定義を与える。

c−ss’
p=
=
=
=

λm.λn.(n p m)
λn.λf.λx.(f (n f x))
λx.(pair (snd x) (s (fst x)))λn.(fst (n s’ (pair c0 c0 )))s は足す 1 を計算し、p は引く 1 を計算する。足し算は既に定義したので、s はすぐ定義できる
が、p のためには補助関数 s’ を使う。
s’ は自然数の組 (m, n) に対して (n, m + 1) を返す関数である。それを (0, 0) に繰り返し適用す
ると、順番に (0, 1), (1, 2), (2, 3). . . が得られる。第一要素がちょうど適用回数引く 1 という値になるので、それを返すと前者関数になる。
最後に、m − n を計算するために、m に n 回 p を適用すればいい。よって、m ≥ n ならば、
∗c− cm cn → cm−n3

不動点演算子 再起的な関数を定義するのに、不動点演算子 Y が必要になる。その基本的な属性は、(Y M ) が (M (Y M )) に簡約できることである。

Y = (λf.λx.(x (f f x))) (λf.λx.(x (f f x)))Y はループを回す回数が分からないとき必要になる。例えば、階数の再帰的な定義は次の通りである。
0! = 1n! = n × (n − 1)! if n > 0
それをλ計算に翻訳するとこうなる。

c! = λn.if0 n c1 (c× n (c! (p n)))
こういう再帰的な定義は (c! は右にも出ている) λ計算では直接にできないので、Y を使う。

c! = Y (λf.λn.if0 n c1 (c× n (f (p n)))Y M → M (Y M ) ということを思い出せば、上の方程式が成り立つことが分かる。
c! → (λf.λn.if0 n c1 (c× n (f (p n)))) c! → λn.if0 n c1 (c× n (c! (p n)))

4.5

評価戦略

ラムダ計算は計算機械ではない。なぜかといえば、簡約という計算機構があっても、それをどの順番で行うか、あるいはいつ計算が終わるか、が定まっていない。標準形と戦略はちょうどそれを決める役割をはたしている。
標準形 簡約できる個所を全く残さない (既約) 標準形以外にも、先頭の部分だけが簡約できない
弱冠頭標準形も定義できる。例えば (x ((λy.y) z)) や λx.((λy.y) z) は既約標準形でない (y がまだ簡約できる) が弱冠頭標準形である。形式化すると、λx.M または (x M1 . . . Mn ) のどちらかの形をしたものが弱冠頭標準形である。
最左戦略 最も左にある簡約できる個所を先に簡約する。名前呼び出し (call-by-name) に当る。関数の引数を評価せずに、そのまま代入する。(λx.x) ((λy.y) z) → ((λy.y) z)。ある戦略で M →∗ N (N標準形) のとき、最左戦略でも M →∗ N 。
最右最内戦略 最も右にある簡約できる個所の中で、最も中にあるものを選ぶ。値呼び出し (callby-value) に当る。関数の引数を標準形に落してから代入する。(λx.x) ((λy.y) z) → ((λx.x) z)。
ある戦略で M →∗ . . .(無限に続く簡約) のとき、最右最内戦略でも無限な簡約になる。
λ機械 標準形と戦略の組み合わせを選ぶと、任意のλ項をあるλ機械によって決定的に実行されるプログラムとしてみることができる。

45チューリング機械とラムダ計算の同値性

5.1

チューリング機械をλ項に組とリスト構造 既に 2 組の作り方を見ている。同様に n 組が作れる。(a1 , . . . an ) = λf.(f a1 . . . an ).
長さの分からないリストは 2 組で構成する。[a1 , a2 , . . . , an ] は(a1 , [a2 , . . . , an ]) = λf.(f a1 [a2 , . . . , an ]) になる。
規則性のある無限なデータ構造も無限リストとして表現できる。例えば、同じ値の繰り返し[a, a, . . .] を Y (λx.(pair a x)) と書ける。
状態と記号 M = (K, Σ, q0 , H, δ), |K| = k, |Σ| = l とする。各状態と記号に番号をふっておき、K = {q0 , . . . , qk−1 }, Σ = {σ0 = B, . . . , σl−1 }。次の翻訳を定義する。

qi = λx0 . . . xk−1 .xi
σi = λx0 . . . xl−1 .xi
時点

時点 (T, n, q) を

(q, T (n), [T (n − 1), T (n − 2), . . .], [T (n + 1), T (n + 2), . . .])の 4 つ組で表す。無限リストを使うことになるが、B でしか構成されていない末端の部分を Y を使って表現する。[B, . . .] = Y (λy.(B, y)) →∗ (B, Y (λy.(B, y))) →∗ . . .
遷移関数

ある時点から次の時点への遷移関数を関数の l 組の k 組で表す。

∆ = λt.t((δ(q0 , σ0 ), δ(q0 , σ1 ), . . . , δ(q0 , σl−1 )), . . . , (δ(qk−1 , σ0 ), . . .))00 λtl .λtr .f (q , fst tl , snd tl , (σ , tr ))when δ(q, σ) = (σ 0 , 左, q 0 )δ(q, σ) =λtl .λtr .f (q 0 , fst tr , (σ 0 , tl ), snd tr ) when δ(q, σ) = (σ 0 , 右, q 0 )
λtl .λtr .(q, σ, tl , tr )when q ∈ H
この中の f を恒等関数 λx.x と定めると、抽象的に見る ∆ の型は (K, Σ, Σ list, Σ list) →(K, Σ, Σ list, Σ list) であり、時点から時点への遷移関数に対応している。
実行 ∆ は 1 回分の動作しか行わないので、その不動点を取ればよい。そのために f を抽象化する。
λf.∆ : ((K, Σ, Σ list, Σ list) → (K, Σ, Σ list, Σ list)) →((K, Σ, Σ list, Σ list) → (K, Σ, Σ list, Σ list))(Y (λf.∆)) : (K, Σ, Σ list, Σ list) → (K, Σ, Σ list, Σ list)
それを初期状態に適用すると、T . (T 0 , n, q 0 ) が算出される。しかし無限リストを使っているので、既約標準形まで計算すると止らない。弱冠頭標準形では正しい結果が得られる。

(Y (λf.∆)) (q0 , T (0), [T (−1), . . .], [T (1), . . .]) →∗(q 0 , T 0 (n), [T 0 (n − 1), . . .], [T 0 (n + 1), . . .])55.2

λ項を実行できるチューリング機械

この節の目的はλ項をテープに書き、実行することである。
テープを実行するチューリング機械を考える前に、λ項を実行しやすい形でテープに書き込まなければならない。特に変数名とα変換は省きたい。そのために De Bruijn 添数を導入する。
定義 5.1 De Bruijn 添数

変数名を使わないラムダ計算を定義する。

M ::= n | λM | (M M )添数はこの変数が何番目の抽象 (中から数えて) で束縛されたかを表す。例えば λx.λy.x = λλ2,λx.(x x) = λ(1 1)。代入を新しく定義する。

⇑n k⇑n k⇑n λM= k+1k≥n= kk<n= λ(⇑n+1 M )β 簡約

λM N → [N/1]M[N/n]n[N/n]k[N/n]k[N/n]λM[N/n](M M 0 )

=
=
=
=
=

Nk−1k>nkk<nλ([⇑n N/n + 1]M )([N/n]M [N/n]M 0 )例題 5.1 対から 1 つ目の値を出す。

fst λ(1 a b) = λ(1 λλ2) λ(1 a b) → λ(1 a b) λλ2 → λλ2 a b → λa b → a
テープの形式5 つの記号 {0, 1, E, λ, @} を使い、テープへの変換 M を定義する。
n = (n の 2 進法記述) E
λM = λ M(M M 0 ) = @ M M 0

チューリング機械 Λ 上のテープを実行する機械 Λ はここで定義しないが、加算等の簡単な動作でできるので、そういうチューリング機械の存在は明かであろう。ここで弱冠頭標準形を最左戦略で計算する。

5.3

万能チューリング機械

任意のチューリング機械をλ項で表現できる、任意のλ項はある特定のチューリング機械が実行するテープに変換できる。そういう二つの定理に面白い系がある。
系 5.1 任意のチューリング機械を模擬できる万能チューリング機械が存在する。その機械は模擬する機械の定義をテープで与えられ、それを実行する。
証明 模擬したいチューリング機械をλ項に変換し、それを Λ に与えればよい。

6