プログラミング言語論1

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

Download Report