5. The Untyped Lambda-Calculus

型なしラムダ計算。3章で簡単な言語を設計したが、これをさらにラムダ計算という枠組みに落とし込むことができる。実のところ複雑なプログラミング言語も、その本質をついたラムダ計算という小さな言語で表し、理解することができる。

ラムダ計算の重要な点は、

ラムダ計算が計算を行うものであるのと同時に、
ラムダ計算における命題が厳密に証明可能な数学的対象である、

ということ。

5.1 Basics

Operational Semantics

\([x \mapsto t_2]t_{12}\) とかいうよくわからん記法が出てきたがこれもひとつの関数。そういって悪ければ厳密に定義された手続きである。

5.2 Programming in the Lambda-Calculus

Multiple Arguments

定期的に話題になるカリー化について。そもそも要求としては、計算を表すものであるラムダ式では（ラムダ抽象の定義を見ればわかるように）1引数の関数しか直接には表わせなそうであるところ、複数引数の関数をラムダ式で表したい。ラムダ計算において（1引数の）関数は項の中の自由変数の出現を書き換えることのできるラムダ抽象で表わされたから、複数引数の関数というのは複数の自由変数出現を書き換えることのできるラムダ抽象だ。複数の引数を一度に与える代わりに、複数回適用を行うということにする。この複数引数関数から高階関数への変換をカリー化と呼ぶ。

Church Booleans

ラムダ計算にブーリアンを持ち込む。このシンプルな言語がこれだけの表現力を持っていることに注目。ここで tru, fls を定義しただけでは意味がなくて、test （if 相当）を定義してはじめてこれらの値がブーリアンとして意味を持つことにも注意。tru や test といった項それ自身がその意味を知っている、内包しているわけではなく、ある真っ当な意味論のもとでこれらの組み合わせが期待した挙動を示す（人間の脳内モデルに対応した意味が導出される）のである。pair と fst, snd の場合も同様に、値（の組み立て）とそれに対する演算の両方があってはじめて意味が現われる。

Ex. 5.2.4

plus, times と定義してきたところで、冪乗を定義する。

\[pow = λm.λn.n \; (\mathrm{times} \; m) \; c_1\]

Ex. 5.2.8

リスト [x,y,z] を λc. λn. c x (c y (c z n)) という式で表すことにするとき、nil, isnil, head, tail はそれぞれどうなるか。

\[nil = λ c.λ n.n \\ cons = λ x.λ xs.λ c.λ n.c \; x \; (xs \; c \; n) \\ head = λ xs.xs \; \mathrm{tru} \; \mathrm{tru}\]

head の確認（\(head \; [A,B] \longrightarrow^* A\)）

tail はちょっと工夫がいる。テキストの pred をそのまま真似すると:

\[nn = \mathrm{pair} \; \mathrm{nil} \; \mathrm{nil} \\ cc = λ x.λ xs.\mathrm{pair} \; (\mathrm{snd} \; xs) \; (\mathrm{cons} \; x \; (\mathrm{snd} \; xs)) \\ tail = λ xs.\mathrm{fst} \; (xs \; cc \; nn)\]

tail の確認（\(tail \; [A,B] \longrightarrow^* [B]\)）

Enriching the Calculus

真偽値、数値といった概念をラムダ計算により表せることがわかったとはいえ、簡便さのため以前に定義した真偽値、数値とそれに対する演算をラムダ計算に組み込んだ言語を考えることもある（厳密な定義は記されていないけれど、λ抽象、λ適用と並んで NB の項があるような文法だろう）。純粋なラムダ計算λと区別するためλNBと表記する。

realnat の解説。

\[realnat = λ m. m \; \mathrm{succ} \; 0\]

と定義することはできない。文法的に succ は何かに適用する形でしか存在しえないからだ。

Recursion

待ってました！　みんな大好きYコンビネータ。

今取り扱っているラムダ計算では式に名前をつけるようなことができないので、当然、項の中からその項自身を参照するという、普通に想像するようなやり方で再帰を行うことはできない。ここで登場する fix と名付けられた項は、引数を与えて簡約するとうまい具合にその引数を複製する性質があり、これを利用して再帰を実現することができる。この式の形は天下り的に登場するので、あまり深く考える必要はないかも。ただ自分で簡約してみるとちょっとわかったような気持ちになれる。

fix = λf.(λx.(f (λy. (x x) y))) (λx.(f (λy. (x x) y))) は有名なYコンビネータ Y = λf.(λx.(f (x x))) (λx.(f (x x))) とは少し違った形をしているが、これは call-by-value では Y が発散してしまうのを修正したバージョンだということらしい。

Representation

さてここで、チャーチ数を用いて普通の数を表すことができるとはどういうことだろうか？　という話。そもそもここで考えてる数ってなんだろうか？　ということから考える。

0 は数である。
iszero という、数から真偽値への関数がある。
succ, pred という、数から数への関数がある。

iszero, succ, pred の意味論については Figure 3-2 にある通り。このそれぞれをチャーチ数の定義が満たしているので、数が実現できているという話。

5.3 Formalities

このラムダ計算の文法および操作的意味論の定義を考える。

Syntax

Def 5.3.2 で項 \(t\) 中の自由変数（free variables）\(FV(t)\)が定義される。

Substitution

項の書き換えは実際に定義しようとすると少し工夫がいる。テキストでは誤りのある定義を踏まえながら、正しい定義に誘導している。

ここのポイントは以下の通り。

\([x \mapsto y](λx.x)\) の結果が \(λx.y\) であってはいけない（束縛変数を書き換えてはいけない）
\([x \mapsto z](λz.x)\) の結果が \(λz.z\) であってはいけない（自由変数を書き換えた結果束縛変数になってしまってはいけない）

人間が意味を考えると間違えようのないところだけれど、きちんと定式化するならこういう落とし穴を避けられる必要がある。結局このテキストではどうしているかというと、上記2例のような事態にならないときについてだけ書き換えの操作を定義し、それ以外の場合については登場する束縛変数の名前を新しいものに書き換えることとしている。チャーチの言葉によるとこれをα変換（alpha-conversion）と呼ぶ。束縛変数の名前だけが異なるラムダ項は同じものとして扱う（Convention 5.3.4）ことによって、この書き換えが、すべてのラムダ項に対して定義されることになる。

書き換える先の名前の候補は無限にあるから上手くいくのは確かだが、名前の決め方が定義されていないのっていいのかな……とモヤモヤするが、次の章では別の方法が紹介され、そちらは完全にアルゴリズムが決まっているので心配しなくともよい。

Operational Semantics

見慣れた意味論だけれど、ここでは数値や真偽値ではなく、ラムダ抽象が最終的な評価結果、値となる。