第14回 前半：ラムダ計算（演習付） 後半：小テスト プログラミング言語論 第14回 前半：ラムダ計算（演習付） 後半：小テスト 情報工学科 木村昌臣 篠埜 功
今後のスケジュール 12/24（水）第１４回 ラムダ計算（導入） 1/14（水）は月曜日の講義が行われるので無し。 期末試験は試験期間中に行う。日時、場所については掲示を見てください。持ち込み不可。
今日のトピック：ラムダ計算 ラムダ計算とは： プログラミング言語の核となる部分を取り出した言語 計算可能な関数をすべて表現可能。 3
ラムダ式 ラムダ式の定義 <ラムダ式> ::= <定数> | <変数> | (<変数> . <ラムダ式>) | (<ラムダ式> <ラムダ式>) <定数> ::= 0 | 1 | 2 | 3 | … <変数> ::= x | y | z | w | … 4
ラムダ式 ラムダ式の構文木を以下のように定義する。 M ::= c 定数（0, 1, 2, 3,等） | x 変数（x, y, z, w, 等） | (x .M) ラムダ抽象 | (M M) 関数適用 5
ラムダ式 ラムダ式を表記する場合の約束事項 関数適用は左結合する。 ラムダ抽象x .MにおけるMはできるだけ大きくとる。 括弧を省略した場合、1, 2の約束に従う。 例 x y z は、(x y) zを表す。 例 x. y. z. x y z は、 x. (y. (z. ((x y) z))) を表す。 6
ラムダ式 計算の本質を追究する過程で考えられた言語 ラムダ記法は直感的には関数の表記法。 g ( x ) = x + 1 で定義される関数g : Z Z を、 g = x Z . x + 1 のように表記する。Zが明らかな場合省略して g = x. x + 1 のように書く。 7
型無しラムダ計算 形式的な式変形（変換、次ページで説明）を行うのが型無しラムダ計算。 8
変換 ラムダ式 M, N, P, 変数xについて、 変換を以下のように再帰的に定義する。 (x. M) N M [N / x] (x. M) (x. N) MP NP PM PN M [N / x]はラムダ式M中のxをNで置き換えたラムダ式を表す。ただし、束縛変数が自由変数とかぶらないように、束縛変数の名前の付け替えを行う。 9
置換の定義 置換 M [ N / x ] の定義 Mが定数の場合 c [ N / x ] = c Mが変数の場合 x [ N / x ] = N y [ N / x ] = y ( x y ) Mがラムダ抽象の場合 (y. M) [ N / x ] = y. M (x = y) y. (M [N / x]) (x y, y FV (N)) z. ((M [ z / y ]) [N / x] ) ( x y, z x, y FN (N), z FV (M), z FV(N) ) Mが関数適用の場合 (M1 M2) [N / x] = ( M1 [ N / x ] ) ( M2 [N / x] ) 10
自由変数 ラムダ式 Mの自由変数の集合FV(M)を以下のように定義する。 FV( c ) = { } FV ( x ) = { x } FV ( x. M ) = FV (M) \ { x } （\ は集合の差をとる演算を表すものとする。） FV (M1 M2) = FV (M1) FV (M2) 11
変換列 ラムダ式M1に変換を有限回（0回以上）繰り返してラムダ式Mnが得られるとき、 M1 M2 … Mn と表せる。 また、M N かつ N M のとき、 M N と書く。 12
例 ラムダ式 (x. y. x y) z w に対して、以下のは以下の変換列が存在する。 (x. y. x y) z w (y. z y) w z w 13
練習問題 ラムダ式 (x. y. x y) (z. z) w は、何度か変換を行うことによってwに変換できるが、その過程を示せ。 14
解答 黒板で説明。 15
Church-Rosserの定理 M * M1 かつM * M2 ならばあるラムダ式Nが 存在して M1 * N かつM2 * N が成り立つ。 16
小テスト 17