プログラミング言語論

プログラミング言語論
第１３回
情報工学科篠埜功
今後のスケジュール
1/14（木）第１４回小テスト等
1/18（月）第１５回期末試験 3402教室
期末試験出題範囲：第１回から１４回まで、全部
今日のトピック：ラムダ計算
ラムダ計算とは：
関数型言語の核となる部分を取り出した言語
計算可能な関数をすべて表現可能。
ラムダ式
ラムダ式の定義
<ラムダ式> ::= <定数>
| <変数>
| (<変数> . <ラムダ式>)
| (<ラムダ式> <ラムダ式>)
<定数> ::= 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
のように書く。
ラムダ計算
ラムダ式に対し、形式的な式変形（変換、次
ページ以降で説明）を行うことが計算である
という考えに従った計算体系がラムダ計算。
変換の例
(例) (x. x) z  z
(例) (y. y) z  z
直感的には、x. xはxを受け取ってxを返す関数で
あり、このxをyに変えても意味は同じである。
g ( x ) = x と g ( y ) = yは同じ意味であるのと同じ。
変換の例２
(例) (x. x y) (z. z)  (z. z) y
(x. x y)は、xを受け取って、それをyに適用する関
数である。(z. z)を受け取った場合は、それをy
に適用する関数適用式になる。(これをさらにβ
変換するとyになる)
(例) (x. x) (y. y)  (y. y)
(x. x)はxを受け取ってxを返す関数であり、 (y. y)
を受けとった場合、 (y. y)になる。
メタ変数
以下でラムダ式の変換を定義する。その際に、
ラムダ式、定数、変数を表すための変数（メタ
変数）として以下のものを用いる。
M, N, P, M1, M2 等: ラムダ式
c: 定数
x, y, z : 変数（x, y, z, w等。このスライドでは、
立体か斜体かで区別している。）
変換
ラムダ式 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で置き換えた
ラムダ式を表す。ただし、束縛変数が自由
変数とかぶらないように、束縛変数の名前
の付け替えを行う。
置換の例
さきほどの例 (x. x) z は、定義に従ってβ変換す
ると、x [ z / x ] になる。x [ z / x ]は、式x中のxをzに
置き換えた式、すなわちzを表す。
(x. x y) (z. z) の例では、β変換すると、
(x y) [ (z. z) / x ] になる。 (x y) [ (z. z) / x ]は、式
(x y)中のxを(z. z)に置き換えた式、すなわち
(z. z) yを表す。
置換で名前がかぶる例
例えば、(λx. y) [x / y]のような置換は、(λx . x)にな
るべきではない。 (λx. y) 中のxは仮の名前であり、
[x / y] のxと同じではない。
よって、 (λx. y)中の仮の名前xをまず何らかの未
使用の名前に付け替える。例えば(λz . y)としてか
ら、[ x / y ]の置き換えを行う。すると、(λz . x)とな
る。このようになるように置換を次ページで定義
する。
置換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  FV (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)
例
（例１）ラムダ式 (λx . x)の自由変数を計算してみる。
FVの定義により、
FV (λx. x) = FV (x) \ {x} = {x} \ {x} = { }
である。（ラムダ式(λx . x)には自由変数はない。）
（例２）ラムダ式 (λx. x y)の自由変数は、
FV (λx. x y) = FV (x y) \ {x} = (FV (x) U FV(y)) \ {x}
= ({x} U {y}) \ {x} = {x, y} \ {x} = {y}
となり、y１つである。
変換列
ラムダ式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
z w
練習問題
ラムダ式 (x. y. x y) (z. z) w は、何度か変
換を行うことによってwに変換できるが、そ
の過程を示せ。
解答
(x. y. x y) (z. z) w
 (λy. (λz. z) y) w
 (λy. y) w
w
または
(x. y. x y) (z. z) w
 (λy. (λz. z) y) w
 (λz. z) w
w
Church-Rosserの定理
M * M1 かつM * M2 ならばあるラムダ式Nが
存在して M1 * N かつM2 * N が成り立つ。
例
ラムダ式 (x. y. x y) (z. z) w は、
(x. y. x y) (z. z) w  (λy. (λz. z) y) w
のようにまずβ変換される。このλ式に対し、２
通りのβ変換の適用が可能である。
(1) (λy. (λz. z) y) w  (λy. y) w
(2) (λy. (λz. z) y) w  (λz. z) w
(1), (2)に対してβ変換を一度適用すると、どち
らもwになる。
このように、β変換で一度枝分かれした後、必
ず合流するルートがあるというのがChurchRosser定理である。
練習問題
ラムダ式 (x. y. x y) (λx. x y) wに対して、β変
換を適用する箇所のないラムダ式になるま
でβ変換を適用せよ。また、この例では途中
で、２通りの適用可能性のあるラムダ式が
出てくる。２通りのβ変換列を示せ。
解答
(x. y. x y) (λx. x y) w
 (λz. (λx. x y) z) w
 (λz. z y) w
wy
または、
(x. y. x y) (λx. x y) w
 (λz. (λx. x y) z) w
 (λx. x y) w
wy

Download Report