ラムダ計算
(λ-calculus)

ラムダ計算とは？

ラムダ記法 —関数を簡潔に記述するための記法
ラムダ計算 —ラムダ記法を用いて関数の性質について論じるための体系

ギリシャ🇬🇷文字のλを用いることに由来する

型付きの (typed) ラムダ計算もあるが、ここでは型無しの (untyped) ラムダ計算を紹介する

ラムダ計算の特徴

とても単純な形式的体系である
他の計算モデルと同等の計算能力を有する
- チューリングマシン (Turing machine)
- 部分帰納関数 (partial recursive function)

問

次の言葉の意味を調べてみよう

チャーチの提唱（チャーチ＝チューリングの提唱） (Church-Turing thesis)
チューリング完全 (Turing complete)

ラムダ計算は単純で、しかも形式的な扱いが可能な計算体系です。なお、「形式的」とは「心がこもっていない」など、悪い意味に使われることもありますが、ここでの「形式的」(formal) とは「きちんと定義されて曖昧さが（ほとんど）ない」「誰が解釈しても違いが出ない」というような意味です。ラムダ計算はとても単純ですが、チューリングマシンや部分帰納関数など他の計算機科学でよく知られている計算モデルと同等の計算能力を有することが知られています。ではここで、「チャーチの提唱」あるいは「チャーチ＝チューリングの提唱」(Church-Turing thesis) 、という言葉の意味、を調べてみましょう。大雑把に言うと、「チャーチの提唱」とは「計算可能な関数はすべてラムダ計算で表現できる」という主張です。「計算可能」という言葉は定義が難しいのですが、「水晶玉」とか「霊魂」のように人に説明できない方法ではなく、誰もが言葉で説明できる方法で計算できる、という意味で使われます。これまで誰もラムダ計算あるいはチューリングマシンあるいは部分帰納関数で表現できない「計算可能な」関数を見つけたことがない。だから、ラムダ計算あるいはチューリングマシンあるいは部分帰納関数で定義できるものを「計算可能」と呼ぶことにしよう、というのが「チャーチの提唱」です。また、「チューリング完全」(Turing complete)とは、ある計算モデルがチューリングマシンあるいはラムダ計算あるいは部分帰納関数と同じ計算能力を持つことを意味します。

ラムダ式のかたち（文法）

変数を表す記号が \(x\), \(y\), \(x'\), \(y'\), \(x_1\), \(x_2\), … のように定められているとする

以下の形はラムダ式である

変数 — 任意の変数記号 \(x\), \(y\), …
関数適用 — \(M\), \(N\) をラムダ式とするとき \((MN)\)
関数抽象 — \(M\) をラムダ式、\(x\) を変数とするとき \((\lambda x.M)\)

それでは、ここからラムダ式のかたち（文法）を紹介します。ラムダ式は、変数、関数適用、関数抽象の 3 つの要素から構成されます。まず、変数については x, y, x', y', x1, x2 のように使える文字・記号が定められているとします。ラムダ計算はプログラミング言語ではなくて数学なので、通常は一文字の変数記号を使います。あるいは一文字にプライムや添え字などをつけた変数名も使います。すると、まず任意の変数記号 x, y, などはラムダ式です。次に、M, N をラムダ式とするとき、M と N を単に並べて書いて、その周りを丸括弧で囲ったカタチもラムダ式です。これは関数 M を引数 N に適用したものを表します。最後に、M をラムダ式、x を変数とするとき、λ x ドット M と書いて、その周りを丸括弧で囲ったカタチもラムダ式です。これは引数 x を受け取り、M を返す関数を表します。

関数適用 \((MN)\)

直観的には、関数 \(M\) を引数 \(N\) に適用したもの（関数 \(M\) を引数 \(N\) で呼び出した結果）

プログラミング言語では関数適用は f(a) のように書くことが多い

関数抽象 \((\lambda x.M)\)

直観的には、引数 \(x\) を受け取り、\(M\) を返す関数

JavaScript などでは

  function(x) { return M; }

あるいは

  x => M

のように書く

ラムダ式の BNF

BNF で表現すると以下の \(M\) がラムダ式を表す

\(M\)	\(::=\)	\(V\) \| \(\texttt{(} M M \texttt{)}\) \| \(\texttt{(} \lambda V \texttt{.} M \texttt{)}\)
\(V\)	\(::=\)	\(x\) \| \(y\) \| \(z\) \| \(\cdots\)

1, 2, 3, … や +, - などの定数を導入する場合もある

しかし以降は変数・関数適用・関数抽象の 3 つのみからなる純ラムダ計算を紹介する

ラムダ式の例 (1)

\((\lambda x. x)\) — \(x\) という引数を受け取り、\(x\) をそのまま返す関数

C ならば

  int id(int x) { return x; }

という関数 id に相当する

ラムダ式では \(x\) が int 型に限らないが、C では便宜上 int 型にしている

ラムダ式の例 (2)

\((\lambda x. (\lambda y. x))\) — \(x\) という引数を受け取り、\((\lambda y. x)\) という関数を返す関数

\((\lambda y. x)\) という関数は、\(y\) という引数を受け取り（これを無視して）\(x\) を返す関数

つまり式全体は関数を返す関数である

カリー化

ラムダ記法では“関数を返す関数”で、多引数関数の代用とする

つまり \((\lambda x. (\lambda y. x))\) は C の記法では、

  int foo(int x, int y) { return x; }

と表す 2 引数の関数である

このように、多引数関数を“関数を返す関数”として表現することを、カリー化 (currying)と言う

ラムダ計算では多引数の関数を表す記法はないので、このように「関数を返す関数」で多引数関数の代用とします。つまり、C の記法では 2 引数の関数をここの foo のように表すところを、ラムダ計算では (λ x . (λ y . x)) と書きます。このように、多引数関数を「関数を返す関数」として表現することをカリー化 (currying) と言います。カリー (Curry) は、著名な数理論理学者 Haskell B. Curry (1900–1982) の名にちなんでいます。カリー化 (currying) は、Haskell など多くの関数型プログラミング言語でも採用されています。

ラムダ式の例 (3)

\((\lambda f. (\lambda x. (f (f x))))\)
— 関数 \(f\) とデータ \(x\) を受け取って、\(f\) を \(x\) に 2 回適用する関数

ラムダ計算のきまり
（計算規則）

では、ここからはラムダ計算における計算規則を紹介します。算数で例えば 1 + 2 × 3 は 1 + 6 イコール 7 というように計算の規則があるように、ラムダ計算も計算規則（書き換え規則）が決められています。これらの規則を使ってラムダ式を変形・簡約していきます。例えば (λ x . x) というラムダ式は恒等関数 (identity function) だと説明しましたが、この直観に合うように計算規則が定められています。ラムダ計算の文法には 3 つの構成要素がありましたが、計算規則は 1 つしかありません。それは β 簡約 (beta reduction) という規則です。 β 簡約を説明するまえに、準備のためにいくつかの用語を説明します。

束縛変数・自由変数

\((\lambda x. M)\) という部分式があるとき \(x\) はこの部分式で束縛されているという

このとき \(M\) の中で出現する変数 \(x\) を束縛変数 (bound variable) という
束縛変数でない変数を自由変数 (free variable) という

なお \(\lambda\) のすぐあとに書かれている下線部の箇所:
\((\lambda \underline{x}. (x y))\), \(((\lambda \underline{z}. z) z)\) は、そもそも変数の出現と言わない（束縛とも自由とも言わない）

ラムダ式の中で、関数抽象の (λ x. M) という部分式があるとき x はこの部分式で束縛されていると言います。そして、このとき M の中で出現する変数 x を束縛変数 (bound variable) と呼びます。束縛変数でない（つまり λ なんとかというカタチに入っていない）変数を自由変数 (free variable) と呼びます。なお、λ のすぐあとに書かれる変数、スライド上では下線が引かれている箇所は、プログラミング言語でいう仮引数の宣言に相当するので、そもそも変数の出現にカウントしません。つまり、束縛変数とも自由変数とも言いません。

束縛変数・自由変数の例

\((\lambda x. (\textcolor{#5076ea}{x} \textcolor{#009c56}{y}))\) の \(\textcolor{#5076ea}{x}\) は束縛変数だが \(\textcolor{#009c56}{y}\) は自由変数である
\(((\lambda z. \textcolor{#5076ea}{z}) \textcolor{#009c56}{z})\) の \(z\) は束縛された形でも自由にも出現している
- 後ろの \(\textcolor{#009c56}{z}\) は \((\lambda z.{\cdots})\) という形の中に入っていない

Q

以下のラムダ式の変数の出現のうち、どれが自由変数で、どれが束縛変数か？

\((\lambda x. (y x))\)
\((a (\lambda b. b))\)
\(((\lambda w. w) w)\)
\((\lambda x. (\lambda y. ((x y) (z y))))\)

α変換

一般のプログラミング言語で仮引数の名前は、他の変数とぶつからない限り、替えても良い
例: C では以下の 2 つの関数は同じものである
```
int f(int x, int y) { return x + y; }
int f(int dog, int cat) { return dog + cat; }
```
ラムダ計算でも以下の 2 つは同じと見なされる
- \((\lambda x. (y x))\)
- \((\lambda z. (y z))\)

このような関数の仮引数の名前の付け替えを
α変換 (alpha conversion) と呼ぶ

先ほどの ((λ z . z) z) の例では束縛変数と自由変数に同じ名前が使われていました。このような名前の付け方は混乱の元です。そこで、以下では束縛変数は自由変数と名前がぶつからないように、適宜、名前の付け替えをします。一般のプログラミング言語では、仮引数の名前は他の変数とぶつからない限り、替えても良いことになっています。例えば C では、ここに挙げた 2 つの関数は同じものです。ラムダ計算でも (λ x . (y x)) と (λ z . (y z)) は同じものと見なされます。このように関数の仮引数の名前を替えることを α 変換 (alpha conversion) と呼びます。

α変換に関する注意

ただし、以下の 2 つの式は同じではない

\((\lambda x. (\textcolor{#5076ea}{y} x))\)
\((\lambda y. (\textcolor{#5076ea}{y} y))\)

名前が衝突する場合は α変換は許されない

Q

以下のうち α変換によって同等となるラムダ式を選べ

\((\lambda x. (x y))\) と \((\lambda z. (z y))\)
\((\lambda x. (\lambda y. (x y)))\) と \((\lambda y. (\lambda x. (y x)))\)
\((\lambda x. (\lambda y. y))\) と \((\lambda z. (\lambda y. y))\)
\((\lambda a. (\lambda b. b))\) と \((\lambda b. (\lambda a. b))\)

置換

ラムダ式 \(M\), \(N\) と変数 \(x\) があるとき

\[M[x:=N]\]

は\(M\) の中の自由な \(x\) の出現をすべて \(N\) で置き換えて得られるラムダ式を表す

（この \(\_[\_:=\_]\) という記法自体はラムダ式の枠外の、 “メタ”な記法である）

置換の例

例1: \((\lambda y. (x y))[x := (\lambda z.z)] = (\lambda y. (\textcolor{#d64557}{(\lambda z.z)} y))\)

例2: \((\lambda y. (x y))[y := (\lambda z.z)] = (\lambda y. (x y))\)
（変わらない）

β簡約

ラムダ式の中の

\(((\lambda \textcolor{#009c56}{x}. \textcolor{#5076ea}{M}) \textcolor{#d64557}{N})\)

という形をした部分式を

\(\textcolor{#5076ea}{M}[\textcolor{#009c56}{x} := \textcolor{#d64557}{N}]\)

に書き換える変換をβ簡約 (beta reduction) と呼ぶ

β基 (\(\beta\) redex)

β簡約できるカタチのラムダ式の部分式

\[((\lambda \textcolor{#009c56}{x}. \textcolor{#5076ea}{M}) \textcolor{#d64557}{N})\]

をβ基 (\(\beta\) redex) と呼ぶ

β簡約の例

例1: \((((\lambda \textcolor{#009c56}{f}. \textcolor{#5076ea}{(\lambda x. (f (f x)))}) \textcolor{#d64557}{(\lambda y. y)}) z)\) \(\ \ \stackrel{\beta}{\rightarrow} ((\lambda \textcolor{#009c56}{x}. \textcolor{#5076ea}{((\lambda y. y) ((\lambda y. y) x))}) \textcolor{#d64557}{z})\) \(\ \ \stackrel{\beta}{\rightarrow} ((\lambda y. y) ((\lambda \textcolor{#009c56}{y}. \textcolor{#5076ea}{y}) \textcolor{#d64557}{z}))\) \(\stackrel{\beta}{\rightarrow} ((\lambda \textcolor{#009c56}{y}. \textcolor{#5076ea}{y}) \textcolor{#d64557}{z})\) \(\stackrel{\beta}{\rightarrow} z\)

例2: \(((\lambda \textcolor{#009c56}{x}. \textcolor{#5076ea}{(x x)})\textcolor{#d64557}{(\lambda x. (x x))})\)
\(\ \ \stackrel{\beta}{\rightarrow} ((\lambda x. (x x))(\lambda x. (x x)))\)
\(\ \ \stackrel{\beta}{\rightarrow} \ldots\)

β 簡約の例をいくつか示します。例えば、1 番目の例の (((λ f . (λ x . (f (f x)))) (λ y . y)) z) は β 簡約を何回か繰り返すと最終的に z になります。まず、最初は f を (λ y . y) と置き換えて、((λ x . ((λ y . y) ((λ y . y) x))) z) になります。次に、x を z と置き換えて、((λ y . y) ((λ y . y) z)) になります。さらに、y を z に置き換えて、((λ y . y) z) になり、さらに y を z に置き換えて、最終的に z になります。また、2 番目の例の ((λ x . (x x)) (λ x . (x x))) は β 簡約を施すと、 x を (λ x . (x x)) に置き換えて、((λ x . (x x)) (λ x . (x x))) になります。結局、同じ式に戻ってしまいます。このように、β 簡約を施しても簡単な形にならないラムダ式も存在します。ラムダ計算には、通常のプログラミング言語にあるような繰り返し文や再帰はありませんが、それでも止まらない計算を表現することができるということがわかります。あとで、止まる繰り返しが表現できることも紹介します。また、このラムダ式は x を関数として自分自身に適用するという変な式を表していることがわかります。このような変な式を除外するために型付きのラムダ計算というものも考えられていて、型付きラムダ計算では、このような式は作れないようになっています。

Q

次のラムダ式を（1 ステップ）\(\beta\) 簡約せよ。

\(((\lambda x. (x y)) (\lambda z. (z y)))\)
\(((\lambda x. (\lambda y. x)) (\lambda z. z))\)
\(((\lambda x. (x y)) (\lambda w. w))\)
\(((\lambda y. (x y)) (\lambda w. w))\)

正規形 (normal form)

これ以上 \(\beta\) 簡約を施すことができないラムダ式を正規形 (normal form) という。
\(M\) から \(\beta\) 簡約を繰り返して、\(N\) という正規形に到達するとき、\(N\) を \(M\) の正規形と呼ぶ。

ラムダ式の略記法

ここまで説明したラムダ式の文法は、

β 簡約の説明のためには都合がよい
- 括弧をつけたり外したりする必要がない
しかし、括弧が多くなりすぎる

そこで、略記法を導入する

ラムダ式の略記法（続き）

\(\begin{array}[t]{l}\lambda x_1 x_2 \cdots x_n. M \\ \equiv (\lambda x_1. (\lambda x_2. (\cdots (\lambda x_n. M)\cdots))) \end{array}\)
つまりλ抽象が続く場合はλを1つだけ書く
\(\begin{array}[t]{l}M_1 M_2 M_3 \cdots M_n\\ \equiv ((\cdots((M_1 M_2) M_3)\cdots)M_n) \end{array}\)
つまり関数適用は左に結合する
\(\begin{array}[t]{l}\lambda x_1 \cdots x_m. M_1 M_2 \cdots M_n \\ \equiv \lambda x_1 \cdots x_m. (M_1 M_2 \cdots M_n) \end{array}\)
つまりλ抽象よりも関数適用のほうが優先する

略記法の注意点

\((\lambda x. M_1) M_2\)

は括弧を省略してしまうと、

\(\lambda x. M_1 M_2\)

となってしまい、

\(\lambda x. (M_1 M_2)\)

と区別がつかないので、括弧は省略できない

（参考）ラムダ式の略記法の BNF

BNF で表現すると以下のようになる。

\(M\)	\(::=\)	\(F\) \| \(\lambda\ W\ \texttt{.}\ M\)
\(F\)	\(::=\)	\(A\) \| \(F\ A\)
\(A\)	\(::=\)	\(V\) \| \(\texttt{(}\ M\ \texttt{)}\)
\(W\)	\(::=\)	\(V\) \| \(V\ W\)
\(V\)	\(::=\)	\(x\) \| \(y\) \| \(z\) \| \(\cdots\)

ラムダ式の略記法の例

\[\begin{align*} \lambda f x. f (f x) & \stackrel{略}{\leftarrow} (\lambda f. (\lambda x. (f (f x))))\\ (\lambda x. x x)(\lambda x. x x) & \stackrel{略}{\leftarrow} ((\lambda x. (x x))(\lambda x. (x x))) \end{align*}\]

\(\beta\) 簡約をするときには、略記法をいちど（頭の中で）正式な記法に戻して \(\beta\) 簡約し、再度略記法にする必要がある

Q

次のラムダ記法の正式記法を、できるだけ括弧を少なくした略記法に変換せよ

\((\lambda x. (\lambda y. ((x y) (x y))))\)
\((\lambda x. (((\lambda y. x) (\lambda z. z)) x))\)

Q

次のラムダ記法の略記法を正式記法に変換せよ。

\(\lambda x . (\lambda y. y) x\)
\(\lambda x y. x x y\)

ラムダ計算の性質

有名なラムダ計算の性質を証明なしで紹介する

チャーチ・ロッサー (Church-Rosser) の定理
最左戦略

チャーチ・ロッサーの定理
(Church-Rosser theorem)

一つのラムダ式に幾通りもの \(\beta\) 簡約が可能なとき、別の\(\beta\) 基を選ぶと別の形に枝分かれする

チャーチ・ロッサーの定理（続き）

しかし、うまく何回か \(\beta\) 簡約すると再び合流させることができる

特に、ラムダ式に正規形が存在するならば、それは一つしかない

最左戦略

正規形を持つラムダ式でも、下手に \(\beta\) 基を選べば、無限に \(\beta\) 簡約をし続けうる

\((\lambda x y. y) \underline{((\lambda x. x x) (\lambda x. x x))} \rightarrow (\lambda x y. y) \underline{((\lambda x. x x) (\lambda x. x x))}\)
\( \rightarrow \cdots\)

しかし、最も左から始まる \(\beta\) 基を選べば、正規形を持つラムダ式ならば、必ず正規形に到達する

\(\underline{(\lambda x y. y) ((\lambda x. x x) (\lambda x. x x))} \rightarrow (\lambda y. y) \)

最左戦略は、ラムダ式の評価戦略、つまり β 基の選び方に関するものです。正規形を持つラムダ式でも、下手な β 基の選び方をすれば、無限に β 簡約をし続けうることがあります。例えば、(λ x y . y) ((λ x . x x) (λ x . x x)) は正規形を持ちますが、最初に右側の β 基を選んでしまうと、無限に β 簡約を続けてしまいます。しかし、最も左から始まる β 基を選べば、正規形を持つラムダ式ならば、必ず正規形に到達することが証明されています。ただし、最左戦略が正規形に到達するために最も効率の良い（つまり β 簡約の少ない）方法とは限らないことは注意が必要です。むしろ、そうでないことのほうが多いのです。

最左戦略の例

\((\lambda x . f x x)((\lambda y z. z) w)\)
最左 \(\beta\) 基 🡗		🡖 右側の \(\beta\) 基
\(f ((\lambda y z. z) w) ((\lambda y z. z) w)\)		\((\lambda x . f x x)(\lambda z. z)\)
_{\(\beta\) × 2}🡖		🡗_\(\beta\)
\(f (\lambda z. z) (\lambda z. z)\)

Q

以下のラムダ式を（1 ステップ）最左簡約せよ。

\(((\lambda x. ((\lambda y. x) x)) (\lambda z. z))\)
\(((\lambda x. (x x))((\lambda y. y) z))\)

おもしろいラムダ式

真偽値・整数・組などのデータ型は純ラムダ計算の中で表現できる

真偽値
チャーチの数 (Church numeral)
組、リスト、…
\(Y\) コンビネーター

真偽値の表現

以下のように定義する、

\(\begin{align*} \textit{true} & \stackrel{\textrm{def}}{\equiv} \lambda t f. t \\ \textit{false} & \stackrel{\textrm{def}}{\equiv} \lambda t f. f \\ \textit{if} & \stackrel{\textrm{def}}{\equiv} \lambda c t e. c t e \end{align*}\)

すると \(\textit{if}\:\textit{true}\: M_1\:M_2 \stackrel{\beta}{\twoheadrightarrow} M_1\) であり、
すると\(\textit{if}\:\textit{false}\: M_1\:M_2 \stackrel{\beta}{\twoheadrightarrow} M_2\) である

問

上記の \(\beta\) 簡約を 1 ステップずつ書いて確かめよ。つまり、

\[\begin{align*} \textit{if}\:\textit{true}\: M_1\:M_2 & \equiv (\lambda c t e. c t e)\:\textit{true}\:M_1\:M_2\\ & \rightarrow (\lambda t e. \textit{true}\:t\:e)\:M_1\:M_2 \\ & \rightarrow …\\ & \rightarrow M_1 \end{align*}\]

であることを示せ

チャーチの数 (Church numeral)

自然数 \(n\) に対してチャーチの数 \(c_n\) を以下のように定義する

\(\begin{align*} c_0 & \stackrel{\textrm{def}}{\equiv} \lambda f x. x \\ c_1 & \stackrel{\textrm{def}}{\equiv} \lambda f x. f x \\ c_2 & \stackrel{\textrm{def}}{\equiv} \lambda f x. f (f x) \\ c_3 & \stackrel{\textrm{def}}{\equiv} \lambda f x. f (f (f x)) \\ & \vdots \\ c _n & \stackrel{\textrm{def}}{\equiv} \lambda f x. \underbrace{f (f (\cdots (f}_{n個} x)\cdots)) \end{align*}\)

チャーチの数（続き）

さらに以下のように定義する

\(\begin{align*} \textit{plus} & \stackrel{\textrm{def}}{\equiv} \lambda m n f x. m f (n f x) \end{align*}\)

すると \(\textit{plus}\:c_m\:c_n \stackrel{\beta}{\twoheadrightarrow} c_{m+n}\) である

問

先ほどの \(\beta\) 簡約を、m = 3, n = 2 などの具体例を用いて 1 ステップずつ書いて確かめよ。つまり、

\[\begin{align*} &\phantom{\rightarrow} (\lambda m n f x. m f (n f x)) (\lambda f x. f (f (f x))) (\lambda f x. f (f x)) \\ &\rightarrow \cdots \\ &\rightarrow \lambda f x. f (f (f (f (f x)))) \end{align*}\]

となることを示せ

問

次の関数をチャーチの数に対するラムダ式として定義せよ

\(\textit{zero}\) — 0 であるかどうかを判定する述語
\(\textit{mult}\) — かけ算
\(\textit{pred}\) — 1 を引く関数（難）
\(\textit{sub}\) — 引き算（\(\textit{pred}\) を使えば簡単）

組

\(\begin{align*} \textit{pair} & \stackrel{\textrm{def}}{\equiv} \lambda f s d. d f s \\ \textit{fst} & \stackrel{\textrm{def}}{\equiv} \lambda p. p\:(\lambda f s. f) \\ \textit{snd} & \stackrel{\textrm{def}}{\equiv} \lambda p. p\:(\lambda f s. s) \end{align*}\)

すると次が成り立つ

\(\begin{align*} \textit{fst}\:(\textit{pair}\:M_1\:M_2) & \stackrel{\beta}{\twoheadrightarrow} M_1 \\ \textit{snd}\:(\textit{pair}\:M_1\:M_2) & \stackrel{\beta}{\twoheadrightarrow} M_2 \end{align*}\)

問: 確かめよ

問

リスト型を表現するために、

\(\textit{cons}\)	— Haskell の `(:)`
\(\textit{nil}\)	— Haskell の `[]`
\(\textit{isNull}\)	— Haskell の `null`
\(\textit{head}\)	— Haskell の `head`
\(\textit{tail}\)	— Haskell の `tail`

に対応するラムダ式を定義せよ

\(Y\) コンビネーター

以下のようなラムダ式を \(Y\) コンビネーターと呼ぶ

\(\begin{align*} Y & \stackrel{\textrm{def}}{\equiv} \lambda f. (\lambda x. f (x x)) (\lambda x. f (x x)) \end{align*}\)

すると、任意のラムダ式 \(F\) に対して、以下が成り立つ

\(Y F \stackrel{\beta}{\rightarrow} (\lambda x. F (x x)) (\lambda x. F (x x))\)

この右辺を \(U\) と置くと、以下の変換列が得られる

\(U\stackrel{\beta}{\rightarrow} F U \stackrel{\beta}{\rightarrow} F (F U) \stackrel{\beta}{\rightarrow} \cdots \stackrel{\beta}{\rightarrow} F (F (\cdots (F U) \cdots))\)

\(Y\) コンビネーター（続き）

\(U\) は \(F\) の不動点と考えられるため、\(Y\) を不動点演算子 (fixed point operator) とも呼ぶ

この \(Y\) を使うとラムダ計算の中で再帰を表せる

例えば \(\textit{fact}\)というラムダ式を次のように定義する

\(\textit{fact} \stackrel{\textrm{def}}{\equiv} Y\:\underbrace{(\lambda f x. \textit{if}\:(\textit{zero}\:x)\:c_1\:(\textit{mult}\:x\:(f\:(\textit{pred}\:x))))}_{F\:とおく}\)

\(Y\) コンビネーター（続き 2）

\(F\), \(U\) を次のように定義する

\(\begin{align*} F &\stackrel{\textrm{def}}{\equiv} \lambda f x. \textit{if}\:(\textit{zero}\:x)\:c_1\:(\textit{mult}\:x\:(f\:(\textit{pred}\:x))) \\ U &\stackrel{\textrm{def}}{\equiv} (\lambda x. F (x x))(\lambda x. F (x x))\\ \end{align*}\)

すると、

\(\textit{fact}\:c_3\)	\(\equiv\)	\(Y\:F\:c_3\)	\(\stackrel{\beta}{\rightarrow}\)	\(U\:c_3\)	\(\stackrel{\beta}{\rightarrow}\)	\(F\:U\:c_3\)
	\(\stackrel{\beta}{\rightarrow}\)	\(\textit{if}\:(\textit{zero}\:c_3)\:c_1\:(\textit{mult}\:c_3\:(U\:(\textit{pred}\:c_3)))\)
	\(\stackrel{\beta}{\rightarrow}\)	\(\cdots\)	\(\stackrel{\beta}{\rightarrow}\)	\(\textit{mult}\:c_3\:(U\:c_2)\)
	\(\stackrel{\beta}{\rightarrow}\)	\(\cdots\)

問

上の \(\beta\) 簡約の続きを 1 ステップずつ確かめよ

\(Y\) コンビネーターまとめ

ラムダ式は再帰関数を表すことができる
- つまり、止まらない計算を表すことができる
任意のラムダ式が停止する（つまり正規形を持つ）かどうかを判定することは不可能であることが知られている
（c.f. チューリングマシンの停止性問題）

この章のまとめ

ラムダ計算は単純な体系ながら、強力なプログラミング言語とみなせる
真偽値・整数や組などのデータ型、条件分岐と再帰などの制御構造、をラムダ計算の中で表現できる

この章のまとめ（続き）

実際にすべての計算を純粋なラムダ計算で記述すると、長くなりすぎる
Haskell は、ラムダ計算に便利な構文（構文上の糖衣）と高度な型システムを導入したプログラミング言語である

終

お疲れさまでした