PowerPoint Presentation

Transcription

1 言語モデル論 (4) ー λ 計算その 1 ー 米澤明憲

2 始めに 関数について 持つ個々の数学的領域 ( 型等 ) に依存しない 関数の一般的な性質を調べる目的 1940 年代にA. Churchが始めた計算の理論体系 作用型プログラミングの基礎 式はλ 式 (λexpression, λterm) と呼ばれ 関数を表す (denoteする) 基本的に文字列の書き換え ( 簡約 ) が計算とみなされる体系であるが その数学的なモデルは 1970 年代半ばにD. Scottに構築された 彼はこれでTuring 賞

3 通常の関数表記 : λ 記法 f(x) > 3, f(x) = (x 2 +x) 2, f(x) = g(x) f (x ) は x という変数を持つ関数を表すのか 関数 f の x における値を表すのか曖昧 同様に (x 2 +x) 2 という表現も x に (x 2 +x) 2 という数を対応させる (x を変数とする ) 関数を表しているのか 単に (x 2 +x) 2 という量を表しているのか曖昧なことがある このため 関数の値と関数自身を区別に明確にする必要あり この区別を明確にするため :λ 記号 λ 変数の導入により名前の無い関数を表記し 対象物として扱える λx.f(x) λx.(x 2 +x) 2 ( プログラムをデータとして扱う )

4 λ 抽象 (λ-abstraction) λy.(x 2 +2y+1) これは y を変数とする関数をあらわすが このなかの x は固定した値と見なされる この式の前に λx.. を付けて :λx.λy.(x 2 +2y+1) とすると x y を変数とする関数にすることができる これを (y を変数とする )λ 抽象と呼ぶ 適用 (application): λ 抽象の逆操作 即ち λ 抽象した変数の値を固定する (λx.(x 2 +x) 2 2) において x の値を 2 に固定する操作 あるいは 2 を適用する操作と 36 が得られる 一方 (λx.λy.(y+x) 1) に 1 を適用するとその結果は λy.(y+1)

5 普通の数学での関数記法では 高階関数 : 関数 twice を例にとる 集合 Xから集合 Yへの関数全体を (X Y) = {f f : X Y} で表す いま 集合 (N N) から集合 (N N) への高階関数 twice を次のように定義する twice(f) = λx N. f(f(x)), ( f (N N)).

6 形式的体系へ 括弧や領域指定の省略 : twice = λf (N N). (λx N.f(f(x))) と表される この例のように λ 記法を多重に組み合わせて使う場合 表現を簡潔にするため括弧を省略して twice = λf (N N). λx N. f(f(x)) と書く この式は twice に関数 f (N N) を与えて twice(f) は λx N. f(f(x)) となり さらにこの関数に x N を与えると (twice(f))(x) = f(f(x)) となることを示している なお (twice(f))(x) を略して twice(f)(x) ともかく ( 例えば twice(suc) (5) = suc(suc(5)) = 7) さらに もし前後の文脈から変数 f と x の動く範囲が明らかであればそれらも省略して twice = λf. λx. f(f(x)) と書くこともある

7 Curry 化 (Currying) 多変数関数を 高階関数を活用して 多変数関数を 1 変数の λ 記法だけで表現できる この方法として curry 化がある fx,y=λz N. f(x,y,z) の例を使ってそのことを説明する いま x の値を固定し y の値を変化させたとき 自然数 y と関数 fx,y の間の対応関係を示す関数を fx : N (N N) とすると fx は λ 記法で fx == λy N.fx,y == λy N.λz N.f(x,y,z) と表される この関数 fx は x の値が決まるとはじめて具体的な関数となるが 自然数 x にこの関数 fx を対応させる関数をさらに f * : N (N (N N)) とおくと f * ==λx N.λy N.λz N.f(x,y,z) である このとき 例えば f * (3) == λy N.λz N.f(3,y,z) f * (3)(5) == λz N.f(3,5,z) f * (3)(5)(7) == F(3,5,7). Curry は米国の論理学者

8 Curry 化とは より一般的には 任意の N 変数関数 f : X 1 X 2 X n X に対して f * = λx 1 X 1,λx 2 X 2, λx n X n.f(x 1,x 2,,x n ) : X 1 (X 2 (X n X) ) とおくと 高階関数 f * と f の間に f * (x 1 )(x 2 ) (x n ) = f(x 1,x 2,,x n ) の関係が成り立つ 言い換えれば f * と f は形式が違うが与えられた x 1,x 2,,x n に対して同じ値を対応させる関数である この f * と f を同一視すれば 任意の多変数関数が 1 変数関数に対する λ 記法を使って表されること

9 このあと λ 計算で学ぶこと 型なしの λ 計算 Church-Rosser の定理 正規化定理 算術計算等の λ 計算による表現 Y- コンビネータ 再帰プログラムの表現 計算可能性 ( 型なし λ 計算数学的モデルの話 D. Scott)

10 λ 式 (λterm) の定義 定義 :(1) 変数 x 0,x 1, は λ 式である (2) M が λ 式で x が変数のとき (λx.m) は λ 式である (3) M と N が λ 式のとき (MN) は λ 式である 例えば x,y,f が変数のとき (λx.(f(fx))) や ((λf.(fx))(λy.y)) は λ 式である (2) による λ 式の構成 (λx.m) を x に関する M の関数抽象 (functional abstraction) あるいは λ 抽象と呼ぶ (3) による λ 式の構成 (MN) を M の N に対する関数適用 (functional application) とよぶ *λ 式は変数に関数抽象と関数適用を繰り返し行うことによって得られる 省略記法 : (1) λx 1 x 2 x n.m (λx 1.(λx 2.( (λx n.m) ))) (n 1) (2) M 1 M 2 M 3 M n (( ((M 1 M 2 )M 3 ) )M n ) (n 2).

11 自由変数と束縛変数 λ 式 M の中に (λx. ) という形に部分式があるとき x はこの部分式の中で束縛 (bound) されているという 変数の中で束縛された形で現われる変数を束縛変数 その出現を bound occurrence と呼ぶ 束縛されない形で現れる変数を自由変数 (free variable). その出現を free occurrence と呼ぶ M の自由変数 ( 出現 ) 全体の集合を FV(M) で表す FV(M)=Φ の時 M を閉式 (closed term) と呼ぶ (λx. ) の中の束縛変数 x の全ての出現を完全に新しい ( この式に現われない ) 変数に置き換えた式を もとの式と同一視する ( ことが出来る ) 例えば λxy.x λuy.u λvy.v

12 変数条件 一般に 同じ λ 式の中に 同じ名前の束縛変数と自由変数が出現することは可能 ( なぜ?) 必要なら 束縛変数を置き換えて 自由変数と束縛変数を異なるようにできる さらに一般に 異なる λ 式群 M1, M2,, Mn の間で それらの束縛変数と自由変数が全く重ならないようにすることが常に可能である 自由変数と束縛変数が文字列として同じものがないことを M1, M2,, Mn が満たすしているとき M1, M2,, Mn は変数条件を満たすという

13 変換 λ 計算の基本的 唯一の 計算 操作である λ 記法で表された関数を λ 記法で表されたデータに適用し 関数値を得る操作に対応 定義 : 変換 ((λx. M) N) の形の λ 式を (M[x :=N]) に変換する ただし (M[x := N]) は M の中の全ての x に N を代入 ( 置換 ) した結果表す 実際 変数条件を満たす M,x,N に対して M の中の全ての ( 自由な )x を N で置き換えた結果を M[x:=N] とおく この記法を用いて λ 式の 変換 を次のように再帰的に定義する (1) (λx.m)n M[x:=N]. (2) M N ならば λx.m λx.n, MP NP, PM PN が成立 変換の対象となる (λx. M) N の形のλ 式を 基 (-redex) と呼ぶ

14 正規形 λ 式 M が 基を持たない 即ちこれ以上 変換ができないとき Mは正規形 (normal form) となっているという λ 式 Mへ変換を繰り返し施し これ以上 変換が出来なくなるならば λ 式 Mは正規形を持つという 但し 全てのλ 式 M が正規形を持つわけではない 例えば : X λx.xxx の時 XX XXX XXXX はXXで始まるただ一つの 変換列であり したがってこの式は正規形をもたない また 正規形を持つλ 式でも 変換の仕方によって変換列が無限に続く可能性のあるものもある

15 記法 : 変換の繰り返しとその記法 P Qは 次の意味 : P P 1 P 2 P n Q ( ただし n 1) 変換可能なλ 式同士を同一視することによって得られるλ 式間の等号関係を=で表す すなわち λ 式 P,Qに対して P P 1 P 2 P n Q def ( ただし M N (M N または N M)) を満たす N 1と P 1,P 2,,P n があるとき P = Qとかく

16 変換の繰り返しとその記法 例 (1) (λx 1 x 2 x n.m)n 1 N 2 N n (λx 2 x n.m[x 1 :=N 1 ])N 2 N n (λx 3 x n.m[x 1 :=N 1 ][x 2 :=N 2 ])N 3 N n M[x 1 :=N 1 ][x 2 :=N 2 ] [x n :=N n ]. 特に (λx 1 x 2 x n.m)x 1 x 2 x n M (2) I λx.xのとき IM (λx.x)m M (3) K λxy.xのとき KMN (λy.m)n M (4) S λxyz.xz(yz) のとき SPQR (λxyz.xz(yz))pqr PR(QR) S(λx.M)(λx.N) λz.(λx.m)z((λx.n)z) λz.m[x:=z]n[x:=z] λx.mn また S, K, Iの間に次の関係がある SKK λz.kz(kz) λz.z I.

17 SK 式の普遍性 問変数と S と K と関数適用のみを使って構成される λ 式を SK 式とよぶ ( より正確にいうと SK 式を再帰的に次のように定義する ( イ ) 変数と S と K はそれぞれ SK 式である ( ロ )X 1 と X 2 が SK 式のとき (X 1 X 2 ) は SK 式である ) (1) 任意の λ 式 M に対して SK 式 X が存在して X M が成り立つことを 次の (1.1) と (1.2) を確かめることによって証明せよ (1.1)SK 式 Xと変数 xに対して Ax,Xを次のように再帰的に定義する 任意に λ 式 SKK (X xのとき) に対して そ Ax.X KX (Xがx 以外の変数かSまたはKのとき ) れに 変換 S(Ax.X される SK 式 1 )(Ax.X 2 ) が必ず存在 (X X 1 X 2 のとき ただしX 1 とX 2 はSK 式 ) このときAx.XはSK 式で かつAx.X λx.xを満たす (1.2) 一般のλ 式 Mに対して Mの中に現れる全てのλをAに置き換えた結果をXとすると XはX Mを満たすSK 式である (2) M λxy.xy に対して X M を満たす SK 式 X を求めよ

18 不動点演算子 λ 式 M に対して M M M 但し M λx. M(xx) とすると M (λx.m(xx))m M(M M ) MM 即ちM はMの不動点である 通常の関数の場合と同様に X = MX を満たす X を M の不動点 という Y λy.(λx.y(xx))(λx.y(xx)) により定義すると Y は任意の λ 式 M に対して上記の不動点 M, 即ち M の不動点を対応させる関数を表す 実際 YM (λx.m(xx))(λx.m(xx)) M であるから Mの不動点を YM = M = MM = M(YM) 求めてくれる! この Y を Curry の不動点演算子と呼ぶ

19 Turing の不動点演算子 問 Y XX ( ただし X λxy.y(xxy)) のとき 全てのMについてY M M(Y M) が成り立つことを示せ ( このY をTuringの不動点演算子とよ ぶ )

20 変換の戦略 λ 式 Mに 変換を施すとき Mの中に 基が複数ある時 どの順番で 変換するかは大きな問題である (λx.xx)((λy.y)z) (λx.xx)z (λx.xx)((λy.y)z) ((λy.y)z)((λy.y)z). のように 変換結果が変わってくることがある つぎの場合にように 基の選び方に依っては変換列が有限で終わるか不明なことがある (λx.xx)(λx.xxy) (λx.xxy)(λx.xxy) 次に変換する 基の選択を一般に戦略と呼ぶことがある ( 戦略によっては同じ λ 式 M が正規形に到達しないことがある )

21 Church-Rosser 定理 変換列は収束するか? 収束した時 得られる λ 式は同じものか? 定理 (Church-Rosser/ 合流性 ): 一つのλ 式から によって得られた二つのλ 式は必ずに よって再び一つの式に合流されることができる 言い換えれば M M i (i = 1,2) ならば あるNについてM i N(i = 1,2) が成り 立つ この定理により 同じλ 式 Mから始めて有限のステップで止まる ( すなわち 基がなくなりそれ以上変換が続けられなくなる ) 変換列がいくつかあれば それらの最終結果はみな一致することが分かる 変換が無限に続くときでも無限列の途中でいつでも分かれて正規形のほうに合流できるという主張でもある

22 正規化定理 定理 : もし M が正規形をもつならば 常に最も左 ( かつ最も外側 ) にある 基に注目して 変換を繰り返してゆけば その正規形に到達できる この λ 式の変換に関する戦略を正規順序による戦略と呼ぶ 正規順序による変換は普通のプログラミング言語の call-by-name に相当する ( なぜか?) call-by-value に相当する λ 式の変換の順序は 作用的順序と呼ばれる Church-Rosser 定理は古典的な結果であるが 当初その証明が複雑なものであったが 70 年代に Taite により見通しのものが得られた