ラムダ計算 #1 公理系 - 気まぐれエンジニア日記

いやはや, 試験というものはいつになっても嫌ですね. 試験勉強をほっぽり出して研究をしています. 今日も平常運転, くまちゃんです.
いい加減試験勉強をしなくてはいけないのだけど, 全くやる気が起きないので, こうしてブログにまとめることで自分の勉強を進めようと思います. ラムダ計算についてまとめます. 同じ科目の試験を受ける人の参考になれば一石二鳥といったところですしおすし.

ラムダ計算について勉強をするためには, まずラムダ式とは何かということを定義として定めておくべきでしょうから, 形式的に(といってもこれが重要なのだけれど)定義を述べておきましょう.

定義1.1. ラムダ式
変数全体の集合を1つ固定して $V$ とする. ラムダ式全体の集合 $\Lambda$ は, 次を満たすものとして定義する.

$x \in V \Rightarrow x \in \Lambda$
$L, M \in \Lambda \Rightarrow (L~M) \in \Lambda$
$x \in V, L \in \Lambda \Rightarrow (\lambda x.L) \in \Lambda$ . このとき, $x$ を $L$ の束縛変数という.

また, ラムダ式の略記法を次のように定めておきます.

定義1.2. ラムダ式の略記法

$L_1, L_2, \cdots, L_n \in \Lambda$ に対し, $(L_1~L_2 \cdots L_n)$ とは, $((L_1~L_2) \cdots L_n)$ のことである.
$x_1, x_2, \cdots, x_n \in V, L \in \Lambda$ に対し, $(\lambda x_1x_2\cdots x_n.L)$ とは, $(\lambda x_1.(\lambda x_2.\cdots(\lambda x_n.L)))$ のことである.
$x\in V, L_1, L_2, \cdots, L_n \in \Lambda$ に対し, $(\lambda x.L_1~L_2 \cdots L_n)$ とは, $(\lambda x.( (L_1~L_2) \cdots L_n))$ のことである.
$L, M \in \Lambda$ に対し, $L~M$ とは, $(L~M)$ のことである.
$x \in V, L \in \Lambda$ に対し, $\lambda x.L$ とは, $(\lambda x.L)$ のことである.