第14回 前半：ラムダ計算（演習付） 後半：小テスト

Presentation on theme: "第14回 前半：ラムダ計算（演習付） 後半：小テスト"— Presentation transcript:

1 第14回 前半：ラムダ計算（演習付） 後半：小テスト
プログラミング言語論 第14回　 前半：ラムダ計算（演習付） 後半：小テスト 情報工学科　木村昌臣 　 篠埜　功

2 今後のスケジュール 12/24（水）第１４回 ラムダ計算（導入） 1/14（水）は月曜日の講義が行われるので無し。 期末試験は試験期間中に行う。日時、場所については掲示を見てください。持ち込み不可。

3 今日のトピック：ラムダ計算 ラムダ計算とは： プログラミング言語の核となる部分を取り出した言語 計算可能な関数をすべて表現可能。 3

4 ラムダ式 ラムダ式の定義 <ラムダ式> ::= <定数> | <変数>
| (<変数> . <ラムダ式>) | (<ラムダ式> <ラムダ式>) <定数> ::= 0 | 1 | 2 | 3 | … <変数> ::= x | y | z | w | … 4

5 ラムダ式 ラムダ式の構文木を以下のように定義する。 M ::= c 定数（0, 1, 2, 3,等）
| x 　　　　　　　変数（x, y, z, w, 等） | (x .M) 　　　ラムダ抽象 | (M M)　　　　関数適用 5

6 ラムダ式 ラムダ式を表記する場合の約束事項 関数適用は左結合する。 ラムダ抽象x .MにおけるMはできるだけ大きくとる。
括弧を省略した場合、1, 2の約束に従う。 例 x y z は、(x y) zを表す。 例 x. y. z. x y z は、 x. (y. (z. ((x y) z))) を表す。 6

7 ラムダ式 計算の本質を追究する過程で考えられた言語 ラムダ記法は直感的には関数の表記法。 g ( x ) = x + 1
で定義される関数g : Z  Z を、 g =  x  Z . x + 1 のように表記する。Zが明らかな場合省略して g =  x. x + 1 のように書く。 7

8 型無しラムダ計算 形式的な式変形（変換、次ページで説明）を行うのが型無しラムダ計算。 8

9 変換 ラムダ式 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

10 置換の定義 置換 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

11 自由変数 ラムダ式 Mの自由変数の集合FV(M)を以下のように定義する。 FV( c ) = { } FV ( x ) = { x }
FV ( x. M ) = FV (M) \ { x } （\ は集合の差をとる演算を表すものとする。） FV (M1 M2) = FV (M1)  FV (M2) 11

12 変換列 ラムダ式M1に変換を有限回（0回以上）繰り返してラムダ式Mnが得られるとき、 M1  M2  …  Mn
と表せる。 また、M  N かつ N  M のとき、 M  N と書く。 12

13 例 ラムダ式 (x. y. x y) z w に対して、以下のは以下の変換列が存在する。 (x. y. x y) z w
(y. z y) w z w 13

14 練習問題 ラムダ式 (x. y. x y) (z. z) w は、何度か変換を行うことによってwに変換できるが、その過程を示せ。
14

15 解答 黒板で説明。 15

16 Church-Rosserの定理 M * M1 かつM * M2 ならばあるラムダ式Nが
存在して M1 * N かつM2 * N が成り立つ。 16

17 小テスト 17