プログラミング言語論 第１０回 情報工学科　篠埜　功.

Presentation on theme: "プログラミング言語論 第１０回 情報工学科　篠埜　功."— Presentation transcript:

1 プログラミング言語論 第１０回 情報工学科　篠埜　功

2 ラムダ計算 ラムダ計算は1930年代（計算機ができる前）に考え出された。現在では、関数型言語の核となっている。
計算可能な関数をすべて表現可能。 [ラムダ式の定義] <ラムダ式> ::= <定数> | <変数> | (<変数> . <ラムダ式>) | (<ラムダ式> <ラムダ式>) <定数> ::= 0 | 1 | 2 | 3 | … <変数> ::= x | y | z | w | … 2

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

4 ラムダ式 計算の本質を追究する過程で考えられた言語 ラムダ記法は直感的には関数の表記法。 g ( x ) = x + 1
のように書く。 4

5 ラムダ計算 ラムダ式に対し、形式的な式変形（β変換、次ページ以降で説明）を行うことが計算であるという考えに従った計算体系がラムダ計算。 5

6 変換の例 （例１） (x. x) z  z （例２） (y. y) z  z
直感的には、λx. xはxを受け取ってxを返す関数であり、このxをyに変えても意味は同じである。 g ( x ) = x と g ( y ) = yは同じ意味であるのと同じ。 6

7 変換の例（続き） （例３） (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)になる。 7

8 メタ変数 以下でラムダ式の変換を定義する。その際に、ラムダ式、定数、変数を表すための変数（メタ変数）として以下のものを用いる。
M, N, P, M1, M2 等: ラムダ式 c: 定数 x, y, z : 変数（x, y, z, w等。このスライドでは、立体か斜体かでメタ変数かどうかを区別している。） 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 置換の例 さきほどの例 (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を表す。 10

11 置換で名前がかぶる例 例えば、(λx. y) [x / y]のような置換は、(λx . x)になるべきではない。 (λx. y) 中のxは仮の名前であり、 [x / y] のxと同じではない。 よって、 (λx. y)中の仮の名前xをまず何らかの未使用の名前に付け替える。例えば(λz . y)としてから、[ x / y ]の置き換えを行う。すると、(λz . x)となる。このようになるように置換を次ページで定義する。 11

12 置換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] ) 12

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

14 例 （例１）ラムダ式 (λ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１つである。 14

15 練習問題１ （問１） ラムダ式 (z. z) w 中の自由変数を求めよ。
（問２） ラムダ式 (λz. z y) ((λz. z) w) 中の自由変数を求めよ。

16 練習問題２ （問１） 置換 (x y) [z/x] を計算せよ。 （問２） 置換 (λy. x y) [z/x] を計算せよ。
（問３） 置換 (λy. x y) [y/x] を計算せよ。 （問４） 置換 (λy. x y) [λz. z y/x] を計算せよ。

17 練習問題３ （問１） ラムダ式 (λx. x y) (λz. z) にβ変換を適用せよ。
（問２） ラムダ式 (λx. (λy. x y)) (λz. y z) にβ変換を適用せよ。 （注意）この問題では、β変換を一度だけ適用するものとする。

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

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

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

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

22 例 ラムダ式 (x. y. x y) (z. z) w は、
(x. y. x y) (z. z) w  (λy. (λz. z) y) w のようにまずβ変換される。このλ式に対し、２通りのβ変換の適用が可能である。 (λy. (λz. z) y) w  (λy. y) w (λy. (λz. z) y) w  (λz. z) w (1), (2)に対してβ変換を一度適用すると、どちらもwになる。 このように、β変換で一度枝分かれした後、必ず合流する経路があるというのがChurch-Rosser定理である。 22

23 練習問題５ ラムダ式 (λx. λy. x y) (λx. x y) wに対して、β変換を適用する箇所のないラムダ式になるまでβ変換を適用せよ。また、この例では途中で、２通りの適用可能性のあるラムダ式が出てくる。２通りのβ変換列を示せ。 23

24 参考文献 Alonzo Church, “An unsolvable problem of elementary number theory”, American Journal of Mathematics, vol. 58 , pp , 1936.