lambda

計算モデル特論 型なし λ 計算 国立情報学研究所所長補佐 / 教授佐藤一郎 E-mail: ichiro@ii.ac.jp ( 型なし ) ラムダ計算. はじめに. 関数と型 3. ラムダ記法 4. ラムダ計算 5. 変換例 6. チャーチロッサ性 7. 正規形の求め方 8. ラムダ計算の計算能力

ラムダ計算 (Lambda Calculus) 930 年代に数学基礎論の研究から生まれた (A.Church) 一般に数学で扱われる関数概念に伴う計算的要素を抽出して作られる計算体系 関数型プログラミング言語の基礎理論 Lisp Scheme ML Haskell など プログラムの意味論 型理論の基礎の一つ Java のプロジェクトラムダ JDK 8 に導入されたラムダ計算風の記述 ic = #(it x) (x+); (λ 計算の場合 λx:it.(x+)) Java にラムダ式を導入するメリット クラス単位のモジュールから 細粒度のコードの再利用が可能になる 細粒度な ( 関数型 ) コードによる並列処理

Java ラムダ式 関数型インターフェース ( つのインターフェースに実装が必要なメソッドを つだけ持つインターフェース ) のメソッドを容易に実装 従来記法 Butto butto = ew Butto(); butto.addactiolisteer(ew ActioListeer(){ public void actioperformed(actioevet e) { } }); System.out.pritl(" ボタンが押された "); Java ラムダ式による記法 Butto butto = ew Butto(); butto.addactiolisteer(e -> System.out.pritl(" ボタンが押された ")); Java ラムダ式の例 Javaラムダ式の例 (it ) -> { retur + ; } (it ) -> + () -> + -> + (it, it ) -> { retur + ; } (it, it ) -> + (, ) -> + 備考 引数が 個の場合の基本形 文が つだけの場合 波括弧 ( と retur) を省略可能 引数の型を省略 引数が 個の場合は丸括弧を省略可能 引数が 個の場合の基本形 文が つだけの場合 波括弧 ( と retur) を省略可能 引数の型を省略 3

関数と型 関数 : 与えられた引数に適用して値を得るための操作 f(x): 関数 f を x に適用して得られた値 x のとりうる値の領域 A( 定義域と呼ぶ ) f(x) のとりうる領域 B( 値域と呼ぶ ) このような関数の集合は A B と書き f の型と呼ぶ 例 : square(x) = x * x x のとりうる領域は自然数 N のとき square の型は N N である これを square N N とかく 疑問 N (N N) はどんな関数か? つの自然数を与えると関数が得られる関数 f x (y)=x y で x をある値 k に決めれば f k (y)=k y で N N の型を持つ関数となる (N N) (N N) はどんな関数か? 関数を引数として 関数が得られる関数 twice f(x)=f(f(x)) なる関数 twice を考える f(x) のところに square を引数として与えれば twice square(x)=square(square(x)) として関数を作り出す f: (N N m ) (M M k ) に関数名 f はいるのか 関数名がなくても関数 4

高階関数 (higher-order fuctio) 関数を引数とする関数や関数を結果とする関数 例 : twice (f (x)) = f(f(x)) 関数を引数とする関数 関数の関数などを取り扱っていくうえで 関数を値と同様に取り扱えると便利 例 : 関数の関数 twice f(x)=f(f(x)) を考える f(x) のところに square を引数として与えれば twice square(x)=square(square(x))=x x x x 従って 値域は N の型を持つ f(x) のところに f x (y)=x y を引数として与えれば twice f x (y)=f x f x (y)=(x y) y 従って 値域は N N の型を持つ... 5

例 :Google MapReduce Google の検索エンジンを支える超大規模分散処理技術 関数型計算モデルがベース 大規模データを多数のサーバーで処理 入力ファイルと map(), reduce() の二つの関数を定義して MapReduce システムに処理を依頼 MapReduce が入力ファイルに対して複数サーバーに分散させて map() reduce() を処理 実装は C++ で記述された並列分散システム ( 関数型言語ではない ) Hadoop (MapReduce 互換システム ) は Java で記述 MapReduce は Web 検索 DNA 解析では極めて有効 ( 関数型 ) 計算モデルの考え方を理解できないと MapReduce は使えない Amazo の MapReduce サービスならサーバ 000 台 時間でも 万円強 ラムダ記法の必要性 関数として計算を扱うため 余計なものは取り除く 例 :f(x) = x * x とするとき f(x) とは x を変数とする関数 f を表すのか それとも 関数 f の x における値を表しているのかが不明確 関数に名前を付けず 関数も一つのモノ (first class object) として扱う λx.(x*x) ここで λx とは x が (x*x) の引数であることを示す 6

ラムダ式 ラムダ式 λx.m を関数とみると x は仮引数 M が関数本体 ラムダ式 N M (N と M ラムダ式 例えば N は例えば λx.m ) を N M は N の仮引数を M に置き換える (N を M に適用する読む ) 例 : (λx.x+) は (λx.x+) を に適用する となり + となる ラムダ記法の例 例 :f(x) = x +y+ のラムダ記法 λx.(x +y+) 関数 (x +y+) の引数は x であり y は固定値と扱う c.f. λy.(x +y+) 関数 (x +y+) の引数はyであり xは固定値と扱う λx.(λy.(x +y+)) 関数 (x +y+) の引数はxとyであること 7

ラムダ抽象 (Lambda Abstractio) 式 M の中の固定値を表す名前を変数にすること λx.m M は x を変数とする関数となる ( ラムダ抽象 ) ラムダ抽象の逆操作 ラムダ適用 部分計算 定数畳み込み ラムダ適用 (Lambda Applicatio) 関数 M 中の変数 x に値 ( または関数 ) d を代入すること ((λx.m)d) 引数 N に関数 M を適用する ( ラムダ適用 ) (M N) 例 : ((λx.(x +y+))3) 3 +y+ ((λy.(x +y+))4) x + 4+ ((λx.(λy.(x+y+))4)3) 3 + 4+ 8

関数の自己適用 関数 twice のラムダ記法 twice=λf.(λx.f(f x)) 関数 twice に関数 g を引数として適用すると twice g =(λf.(λx.f(f x))g) =(λx.g(g x)) = g(g ) g を twice に置き換えてみる twice twice g =((twice twice)g) =(twice(twice g))=(twice g)((twice g)) =(g(g((twice g))))=g(g(g(g ))) ラムダ式 BNF 文法による定義 M ::= x (λx.m) (M M ) ラムダ抽象 ラムダ適用 ラムダ計算とは規則に従って ラムダ式を順次変形していくこと 9

ラムダ式の例 x (λx.x) (λx.y) (λx. (λy.x)) ((λx.(x x)) y) ((λx.(x x)) (λy.y)) ラムダ式 ラムダ式の定義 () 変数 x,y,z..., 定数,,3,... はラムダ式 ()M がラムダ式 x が変数なら λx.m もラムダ式 ( ラムダ抽象 ) (3)M,N がラムダ式なら MN もラムダ式 ( 関数適用 ) 表記 ( 括弧の省略 ) λx x x.m=λx.(λx.( (λx.m) )) M M M 3 M =( ((M M )M 3 ) )M ( 括弧表記が自然に補えるようになる頃には ラムダ計算は詳しくなっているはず ) 0

ラムダ式の省略形 省略の規則 : 一番外側の括弧は外してよい (λx.(λx...(λx.m)...)) はλx x...x.mと書いてよい (...(M M )...M ) はM M... M と書いてよい 例題 : (λx.(λy.((xy)(zu)))) = λx.(λy.((xy)(zu))) = λxy.((xy)(zu)) = λxy.xy(zu) 自由変数 ラムダ式 Mに含まれる自由変数の集合 FV(M) FV(x) = {x} FV(M M ) = FV(M ) FV(M ) FV(λx.M) = FV(M) - {x} 自由変数でない変数を束縛変数

変数 束縛変数 ラムダ式の x を変数としてラムダ抽象 自由変数 式に含まれる変数と抽象化の対象が結びついているかどうか x(λxy.xyz)xy このとき 青字変数は自由変数 赤字変数は束縛変数 ラムダ式 M,M, M で それらの束縛変数と自由変数が重ならないように置き換えができる 重なりがない状態 = 変数条件を満たす という 変換規則 α- 規則 ( 束縛変数の名前を置換 ) (λx.m)=(λy.[y/x]m) ただし y が M の自由変数ではないとする β- 規則 ( ラムダ式における計算 ) ((λx.m) N) [N/x]M ここで [b/a]m とは M 中の自由変数 a を b で置き換える β 変換によるラムダ式の書き換えをリダクションという リダクションが可能な部分をリデックスと呼ぶ リデックスが含まれていないとき そのラムダ式は正規形であるという

α 変換の例 (λx.x) = (λy.y) ((λx.x) (λx.xy)) = ((λy.y) (λz.zw)) (λx. (λx.x)) = (λy. (λz.z)) リダクションの練習問題 ()(λxy.y)3 ()(λxy.xy)(λw.w w)9 (3)(λxy.x)(λx.xx)(λz.z) (4)(λxy.y)(λx.xx)(λz.z) (5)(λx.x(λxy.x))(λx.x) (6)(λx.x(λxy.x))(λx.x(λxy.y))(λx.x) 3

リダクションの練習問題 ( 解答 ) ()(λxy.y)3 (λy.y) ()(λxy.xy)(λw.w w)9 (λy.(λw.w w)y)9 (λy.y y)9 9 9 (3)(λxy.x)(λx.xx)(λz.z) (λy.(λx.xx))(λz.z) λx.xx (4)(λxy.y)(λx.xx)(λz.z) (λy.y)(λz.z) λz.z リダクションの練習問題 ( 解答 ) (5)(λx.x(λxy.x))(λx.x) (λx.x)(λxy.x) (λxy.x) (6)(λx.x(λxy.x))(λx.x(λxy.y))(λx.x) (λx.x(λxy.y))(λxy.x)(λx.x) (λxy.x)(λxy.y)(λx.x) (λy.(λxy.y))(λx.x) (λxy.y) 4

変換 ( リダクション ) の例 () 自由変数と束縛変数が衝突する場合は 書き換えておく (λxy.x)yz (λy.y)z z ( 誤り ) (λxy.x)yz (λxy.x)yz (λy.y)z y () リダクションを行うと複雑になってしまう例 (λx.xxx)(λx.xxx) (λx.xxx)(λx.xxx)(λx.xxx) (λx.xxx)(λx.xxx)(λx.xxx)(λx.xxx) 変換 ( リダクション ) の例 ( 続き ) (3) 自分に戻ってしまうリダクション (λx.xx)(λx.xx) (λx.xx)(λx.xx) (4) 異なる部分から始めて同じ結果が出るリダクション I λx.x とする I(I x) は二つのリデックス I(I x) と I x を持つ I(I x) I x x I(I x) I x x 5

正規形の求め方 正規形を計算する戦略 つのリデックスがあるとき どちらを選ぶか? M (λx.y)((λx.xx)(λx.xx)) では M M の無限のリダクションが続く では M y となり 回で完了 リダクション戦略 () ラムダ式が M 正規形を持つならば 最も左側のリデックスを常にリダクションすることで 必ず正規形が得られる () 最も左側のリデックスとは 最も外側のリデックスのうちで 最も左側のものであること チャーチ ロッサ性 ラムダ式にリデックスが複数あるとき そのどれに注目するかにより 何通りかのリダクションの可能性がある 場合によっては 正規形にならないリダクションもある 複数のリダクション列ができるとき その結果得られる正規形は途中のリダクションの道筋によらず一意に決まる N * * M Q * * P M N * M P * のとき (0 回以上のリダクションで MからNに到達する意味 ) (MからP) 適当なリダクションで Qに合流できる 6

チャーチ ロッサ性の利点 リダクションの順序に気を使う必要がない どんな方法でリダクションを行っても 得られた結果 ( 正規形 ) が唯一であることが保証される ( 通常の並列計算や 非決定的な計算では 計算の順序を保つため 同期が必要となる ) コード化 : 論理値 論理値の真 (true) と偽 (false) は次のようなラムダ式に対応 true λxy.x (T と略記することもある ) false λxy.y (F と略記することもある ) 条件判定式に対応するラムダ式 (A と B はプログラム分に相当 ) cod λb λa. λb.bab 例 : 任意の A と B に対して Cod true A B A Cod false A B B 7

コード化 : 論理値の例 定義 : true = λxy.x (λx.(λy.x)) false = λxy.y (λx.(λy.y)) if cod the P else Q = cod P Q 例 :if true the A else B = (λxy.x) A B (λy.a) B A 例 :if false the A else B = (λxy.y) A B (λy.y) B B コード化 : 論理値の取り扱い AND (λxy.xy)false OR (λxy.y True x) NOT 例 :AND True False (λx.x False True) ((λxy.xy)false)true False True False False = (λxy.x)false False False 参考 : ゼロ判定 ( 自然数についてはこのあと ) ISZERO: λ. (λx.true) False 8

コード化 : 自然数 自然数 に対応する λ 式 0 と 次の自然数 という概念からコード化 0 λf.λz.z λf.λz.f z λf.λz.f (f z)... N λf. λz.f z 次の自然数を求める関数のコード化 Succ λ. λf. λz.f( f z) コード化 : 自然数演算 自然数演算に対応する λ 式 足し算のコード化 Add λm. λ.m Succ かけ算のコード化 Mul λm. λ.m (Add ) 0 ゼロ判定関数のコード化 IsZero λ. (λ. false ) true 9

不動点定理 任意の λ 項 H に対して HX=X これを満たす X として H (λx.h (x x)) (λx.h (x x)) をとると X は H X となる H を X に作用させて X となることから X を H の不動点という f = g (f) となるような関数を g の不動点と呼ぶ 不動点は不動点コンビネータとして知られるものによってラムダ計算で表現することができる 不動点オペレータ ループは再帰呼び出しとして表現 ただし 再帰呼び出し構文がないので 不動点コンビネータ Y を導入 Y λf.(λx.f (x x)) (λx.f (x x)) 例 : Y を任意のラムダ式 F に適用すると YF (λx.f(x x))(λx.f(x x)) F((λx.F(x x))(λx.f(x x))) F(YF) β 変換を等式とみなすと F(YF)=YF ラムダ式 F の不動点は YF となる ( 関数 f の不動点とは f(x)=x となる x のこと ) 0

ループと再帰 ループは基本的に再帰呼出しで書く ただし 再帰呼出しの構文は無いことから 不動点コンビネータ (fixed-poit combiator) を使う 不動点コンビネータの例 :Y コンビネータ Y = λf.(λx.f (x x)) (λx.f (x x)) 再帰関数は第 引数に自分自身が渡されるとして定義 F = λf.λx.... (f x)... # (f x) は再帰呼出し (Y F) とすると f が (Y F) 自身に置き換わった再帰関数となる (Y F) を引数に適用したものを簡約して正規形が得られるならば, F (Y F) を引数に適用したものも同じ正規形に簡約される性質を利用 再帰計算と Y コンビネータ fac() :=, if = 0; ad fac( - ), if > 0 を λ 式に基づくと fac = λ. If (IZERO ) (Mult (fac (Sub ))) fac を未知とする λ 式に変えると H = λf. If (IZERO ) (Mult (f (Sub ))) H を抽象化した λ 式を導入する 不動点コンビニネータ Y を利用して Y = λg. (λx. g (x x)) (λx. g (x x)) をおくと g (Y g) は Y g となる 上述の fac は fac = Y H 不動点は不動点コンビネータとして知られるものによってラムダ計算で表現することができる

ラムダ計算の計算能力 ラムダ計算モデルによるプログラム 各自然数 k を正規形のラムダ式 k で表す g:n N に対して g(k,k,,k )=k G k k k k を満たすラムダ式 G を 関数 g を計算するためのプログラムとみなす k, k,, k はこのプログラムの入力とみなす このプログラム G を入力 k, k,, k に対して β 変換を次々と行うことを 計算過程としてとらえる 変換が終結して k が得られたとき プログラムの計算結果が k であると考える 変換が終結しない場合 プログラムの計算結果は未定義となる 計算モデル特論 型つき λ 計算 国立情報学研究所所長補佐 / 教授佐藤一郎 E-mail: ichiro@ii.ac.jp

型とは プログラミングにおけるデータ型 Pascal: var x,y: iteger, a:real 型の必要性 プログラム設計を明確化 プログラムの誤り防止 関数やモジュールの仕様 コンパイラ最適化への補助情報 プログラム停止性への補助保証 可読性の向上 3

プログラミング言語の型 基本データ型 整数 浮動小数点 文字 真偽値 構造データ型 配列 直積型 直和型 レコード型 ストラクチャ型 ユーザ定義型 型付プログラミング言語 型なしプログラミング言語 プロトタイピング インタープリタ実行 弱い型付プログラミング言語 手っ取り早く設計 記述 信頼性が低い 強い型付プログラミング言語 安全なプログラム 慎重な設計と冗長な記述 型検査 静的検査 動的検査 4

型推論 強い型付プログラミング言語を利用しながら簡潔な記述を実現するには 型は文面から推定可能 例 : f(x) = if x == 0 the else x * f(x-) 推定により冗長な記述を現象 形式的な体型により型を厳密に決定 型推論の例 式要素の型と式全体の型 例 : if e 0 the e else e もし e 0 が真偽値型 (bool 型 ) で e と e が T という型を持つことが示されれば if e 0 the e else e は T という型を持つ ( ことがわかる ) 型推論の目的 与えられた式がある型を持つことを証明する 与えられた式がもつ型を求める 推論規則 e 0 : bool 型かつ e :T 型かつ e :T 型 (if e 0 the e else e ):T 型 仮定 結論 5

型理論体系 項 (term) 型 (type) 判定 (judgmet) 推論規則 (iferece) 型付ラムダ式 ( 基本 ) BNF 文法による型 ::= b ( ) ここで b は基底型 は組 は関数 BNF 文法による型付ラムダ式 M ::= c x (λx:.m) (M M ) 6

型付ラムダ式 型 ::= b ( ) ( ) ここで b は基底型 は組 は関数 型付ラムダ式 M ::= c x (λx:.m) (M M ) (M,...,M ) M.i 型付ラムダ式 BNF 文法による型 基本型 : b 直積型 : 関数型 : ( ) ( ) 括弧の省略 型における矢印は右結合 例 : ( ( ( 3 4 ) = 3 4 7

型付ラムダ式の直感的意味 基本式 : (M M ) 関数 M に引数 M を与えたときの値 (λx:.m) 型が である仮引数 x をもつ 関数本体を M と定義される関数 型付きラムダ式の例 f(x)=x+ なる関数 f は λx:it.x+ f に実引数 3 を与えた式 f(3) は (λx:it.x+)(3 it ) 8

自由変数 ラムダ式 Mに含まれる自由変数の集合 FV(M) FV(c) = 0 FV(x) = {x} FV(M M ) = FV(M ) FV(M ) FV(λx:t.M) = FV(M) - {x} FV((M,..,M )) = FV(M ).. FV(M ) FV(M.i) = FV(M) 自由変数でない変数を束縛変数と呼ぶ 型付ラムダの計算 簡約規則 [N/x]c = c [N/x](M,...,M ) = ([N/x]M,...,[N/x]M ) [N/x](M.i) = ([N/x]M).I (λx:.m)=(λy:.[y/x]m) ((λx:.m) N:) [N/x]M 9

記法 前提 (assumptio): e:t ある式 e が型 t を持つこと 判定 (judgemet): A e:t (0 個以上の ) 前提 A( 型環境 ) から ある式 e が型 t を持つことが示される 推論 (iferece): A M : A M : A M: 式 M i がそれぞれの前提 A i において型 を持つならば 結論が示される 型推論規則 (var) 型推論規則 (cost) Γ c : Γ x : ( Γ( x) = ) (abs) Γ + { x : } M : Γ λx :. M : (app) Γ M (prod) : Γ M M Γ M :! Γ ( M,", M (proj) Γ M : : Γ M : ):! Γ M :! ( i ) Γ M. i : i 30

型推論規則の記法 前提への操作と表記 Γ+{x:} 前提 Γ に x: を追加 ただし Γ に変数 x に関する勝たし体があった場合は もっとも右側を優先する Γ(x)= 前提 Γ のもとで 定数あるいは変数 x が型 を持つことをあわす 型推論規則 ( 詳細 ) 型推論規則 (cost) (var) Γ c : Γ x : ( Γ( x) = ) (abs) Γ + { x : } M : Γ λx :. M : 関数 λx:.m が関数型 を持つのは 仮引数の型 と仮定したとき 関数 M が型 をもつときである 3

3 型推論規則 ( 詳細 ) 型推論規則 : : : M M M M Γ Γ Γ M M M M Γ Γ Γ! "! ):,, ( : : ) ( :. : i M i M i Γ Γ! (app) (prod) (proj) 関数は 関数がその定められた値にのみ適用可能であり その結果は関数の値の型を持つこと関数の組 (M,...,M ) は M,...,M の直積となる関数の組 (M,...,M ) から I 番目の要素を取り出したときは M の型となる 型推論の例 型推論では推論規則により変形していく 型付ラムダ式 K=λx.(λy.x) ) ( ):. :.( : :. : } : { : } : { λ λ λ Γ x y x x y x x x

型推論の性質 健全性 型推論できるならば その結果が正しい ( 型安全 ) ことを意味する 完全性 正しいことはすべての型において推論することができる 有用性 決定可能かつ効率がよいこと 多相型 プログラム中に現れる同一の式やデータが複数の型をもつこと L.Cardelli と P.Weger による分類 アドホックな多相型 文脈によって型を決定 例 等号 オーバーローディング演算子 系統的な多相型 共通の性質をもった型に作用 例 : パラメトリック多相型 パラメトリック多相型の例 : twice 関数 (twice f(3)) = f(f(3)) f が it 型ときの twice 関数の型 : (it it) it it f が float 型ときの twice 関数の型 : (float float) float float 33