構造化プログラミングとデータ抽象

Size: px

Start display at page:

Download "構造化プログラミングとデータ抽象"

ともあきみうら
4 years ago
Views:

1 計算の理論後半第 3 回 λ 計算と型システム

2 本日の内容 λ 計算の表現力 ( 前回の復習 ) データの表現不動点演算子と再帰 λ 計算の重要な性質チャーチロッサー性簡約戦略型付き λ 計算

3 ブール値組ブール値と組の表現 true, false を受け取り対応する要素を返す関数として表現 T = λt.λf.t F = λt.λf.f if e 1 then e 2 else e 3 = e 1 e 2 e 3 とすると... if T then e 2 else e 3 * e 2 makepair = λx.λy.λf.f x y fst = λp.p(λx.λy.x) : 組の 1 番目の要素の取り出し snd = λp.p(λx.λy.y) : 組の 2 番目の要素の取り出しとすると... fst(makepair M N) * M

4 自然数の表現基本構成子 (zero と successor) を受け取り対応する値を返す関数として表現 n = λs.λz. s (s... (s z)...) n Plus = λm. λn. λs.λz. m s (n s z) Mult= λm. λn. n (Plus m) 0 Exp = λm. λn. n (Mult m) 1 eqzero? = λn. n (λb.f) T Pred = λn. snd(n (λ(x,y).(x+1,x)) (0,0)) Minus = λm. λn. n Pred m

5 本日の内容 λ 計算の表現力 ( 前回の復習 ) データの表現不動点演算子と再帰 λ 計算の重要な性質チャーチロッサー性簡約戦略型付き λ 計算

6 無限簡約列を持つ項 (λx. x x) (λx. x x) [(λx. x x) / x] (x x) = (λx. x x) (λx. x x) (λx. x x) (λx. x x) (λx. x x) (λx. x x)...

7 (λx. x x) (λx. x x) の変種 (λx. F (x x)) (λx. F(x x)) [(λx. F (x x)) / x] F(x x) = F((λx. F(x x)) (λx. F(x x))) M F = (λx. F (x x)) (λx. F(x x)) とおくと... M F F (M F ) = β をβ 簡約を含む最小の同値関係とすると M F = β F (M F ) すなわち M F は関数 Fの不動点

8 不動点演算子 Y = λf. M f = λf. (λx. f (x x)) (λx. f(x x)) とおくと Y F = β M F なので前のページの議論から Y F = β F (Y F) つまり Y F は F の不動点! Y は任意の関数 F を引数にとりその F の不動点を与える関数なのでと呼ぶ不動点演算子これを使うと再帰が表現可能

9 再帰関数と不動点再帰関数の例 : fact(n) = if n=0 then 1 else n * fact(n-1) fact は等式 f = λn. if n=0 then 1 else n * f(n-1) を満たす関数 f factgen = λf. λn. if n=0 then 1 else n * f(n-1) とおけば factは f = factgen f を満たすf つまりfactgen の不動点! よって不動点演算子 Y を用いれば fact = Y factgen と書ける

10 再帰関数の表現 ( 一般の場合 ) 再帰関数定義 f x = e によって定義される関数 f は Y (λf.λx.e) と ( 再帰を使わないで ) 表現可能

11 本日の内容 λ 計算の表現力 ( 前回の復習 ) データの表現不動点演算子と再帰 λ 計算の重要な性質チャーチロッサー性簡約戦略型付き λ 計算

12 チャーチロッサーの定理 If M then N 1 N 2 0 ステップ以上の簡約

13 チャーチロッサーの定理 If M then N 1 N 2 L 0 ステップ以上の簡約

14 例 (λf.λx.f(f x)) ((λx.x)(λx.x)) λx.(λx.x)(λx.x)((λx.x)(λx.x)x) (λf.λx.f(f x))(λx.x) λx.(λx.x)((λx.x)(λx.x)x) M λx.(λx.x)((λx.x)x) N 1 N 2 L

15 注意 M M N 1 N 2 や N 1 N 2 は成り立つが L L M N 1 N 2 は成り立たない ( 前ページの例参照 ) L 1 ステップの簡約 0 ステップ以上の簡約

16 系 : 正規系の一意性定義 :M * N のとき N を M の (β) 正規形と呼ぶ定理 ( チャーチロッサー性の系 ): N 1, N 2 が M の β 正規形なら ( 束縛変数の付け替えを除いて )N 1 =N 2 証明 : M * N 1 かつ M * N 2 と仮定するチャーチロッサーの定理よりある L が存在して N 1 * L かつ N 2 * L ところが N 1, N 2 ともに簡約できないので N 1 =L= N 2

17 系 : 正規系の一意性定義 :M * N のとき N を M の (β) 正規形と呼ぶ定理 ( チャーチロッサー性の系 ): N 1, N 2 が M の β 正規形なら ( 束縛変数の付け替えを除いて )N 1 =N 2 注意 : 上の定理は簡約が停止するならば得られる正規形は一意であることを述べているだけでありどのような簡約列を選んでも正規形が得られることは保証しない例 :(λx.y) ((λx.xx)(λx.xx))

18 本日の内容 λ 計算の表現力 ( 前回の復習 ) データの表現不動点演算子と再帰 λ 計算の重要な性質チャーチロッサー性簡約戦略型付き λ 計算

19 簡約戦略簡約の各ステップでどの β 簡約基 ((λx.m)n の形をした部分項 ) について簡約を行うかを決める戦略最左簡約 :β 簡約基のうち最も左から始まるものを簡約 e.g. (λx.y) ((λx.xx)(λx.xx)) (λf.λx.f(f x)) ((λx.x)(λx.x)) 定理 : M が β 正規形を持つなら最左簡約によって得られる

20 本日の内容 λ 計算の表現力 ( 前回の復習 ) データの表現不動点演算子と再帰 λ 計算の重要な性質チャーチロッサー性簡約戦略型付き λ 計算

21 型付き λ 計算値の種類を表す型を各項に割り当てて無意味な項を排除 λx:int.x+1 : int int (λx:int.x)+1 :?? 型付きプログラミング言語の基礎論理学との密接な対応 (Curry-Howard 同型対応 ) ( 再帰を加えないかぎり ) チューリングマシンと同等の表現力は必ずしも持たない

22 単純型付き λ 計算構文簡約 τ ( 型 ) ::= b τ 1 τ 2 b ( 基本型 ) ::= int bool... M ( 項 ) ::= c b1... bk b ( 定数 ) x λx:τ.m M 1 M 2 β 簡約 + 定数の簡約 : c b1... bk b c 1 b1... c k bk [c](c 1,...,c k ) ( ただし [c] は c が表す数学的な関数例えば [+] 1 2 = 3)

23 型判断 (type judgment) x 1 :τ 1,..., x n :τ n M: τ 型環境 ( 変数の有限集合から型集合への写像 ) 型環境 x 1 :τ 1,..., x n :τ n のもとで項 M は型 τ を持つ各変数 x i が型 τ i の値に束縛されている下で M を評価すると評価結果は τ 型の値になる e.g. f:int int, x:int f x : int y:int + int int int y 1 int : int 次のスライドの型付け規則により定義

24 型付け規則 Γ c τ :τ Γ(x)=τ Γ x:τ Γ, x:τ 1 M:τ 2 Γ λx:τ 1.M: τ 1 τ 2 Γ M: τ 1 τ 2 Γ N: τ 1 Γ M N: τ 2

25 型の導出例黒板で - (λf:int int.λy:int.f(f(y))) (λz:int. + int int int z 1 int ) : int int

26 単純型付き λ 計算の性質型の一意性 Γ - M:τ かつ Γ -M:τ ならば τ=τ 強正規化定理 Γ - M:τ ならば無限簡約列 M M 1 M 2 M 3... は存在しない => 型なし λ 計算やチューリングマシンに比べて表現力が劣る型保存 (subject reduction) Γ - M:τ かつ M N ならば Γ - N:τ 系 : Γ - M:τ かつ M * C[(λx:σ.L)N] ならば N の型は σ ( すなわち関数が要求する引数の型と実際の引数の型は一致する )

27 単純型付き λ 計算の性質型の一意性 Γ - M:τ かつ Γ -M:τ ならば τ=τ 強正規化定理 Γ - M:τ ならば無限簡約列 M M 1 M 2 M 3... は存在しない => 型なし λ 計算やチューリングマシンに比べて表現力が劣る型保存 (subject reduction) Γ - M:τ かつ M N ならば Γ - N:τ 系 : Γ - M:τ かつ M * C[(λx:σ.L)N] ならば N の型は σ ( すなわち関数が要求する引数の型と実際の引数の型は一致する ) ほとんどの型付き計算モデル言語で成り立つ性質

28 型の一意性単純型付き λ 計算の性質 Γ - M:τ かつ Γ -M:τ ならば τ=τ 強正規化定理 Γ - M:τ ならば無限簡約列 M M 1 M 2 M 3... は存在しない => 型なし λ 計算やチューリングマシンに比べて表現力が劣る型保存 (subject reduction) Γ - M:τ かつ M N ならば Γ - N:τ 一部の型付き計算モデルのみで成り立つ性質系 : Γ - M:τ かつ M * C[(λx:σ.L)N] ならば N の型は σ ( すなわち関数が要求する引数の型と実際の引数の型は一致する )

29 以下のアウトライン型検査アルゴリズム型推論単純型つき λ 計算の拡張

30 型検査アルゴリズム TC TC: Γ, M を入力として Γ - M:τ を満たす τ を ( あれば ) 出力 TC(Γ, c τ ) = τ TC(Γ, x) = if x in dom(γ) then Γ(x) else fail TC(Γ, λx:τ 1.M) = τ 1 TC(Γ{x:τ 1 }, M) TC(Γ, MN) = let τ 0 = TC(Γ, M) in let τ 1 = TC(Γ, N) in if τ 0 is of the form τ 1 τ 2 then τ 2 else fail Γ c τ :τ Γ(x)=τ Γ x:τ Γ, x:τ 1 M:τ 2 Γ λx:τ 1.M: τ 1 τ 2 Γ M: τ 1 τ 2 Γ N: τ 1 Γ M N: τ 2

31 以下のアウトライン型検査アルゴリズム型推論単純型つき λ 計算の拡張

32 型推論 (1) 各変数や式に型を表す変数を割り当てる (2) 型付け規則に従って型に関する方程式をたてる (3) 型の方程式を解く

33 型推論の例 let twice f x = f (f x) α f = α x α f x α M : 部分式 M の型

34 型推論の例 let twice f x = f (f x) α f = α x α f x α f = α f x α f(f x) α M : 部分式 M の型

35 型推論の例 let twice f x = f (f x) α f = α x α f x α f = α f x α f(f x) α twice = α f α x α f(f x) α M : 部分式 M の型

36 型推論の例 let twice f x = f (f x) α f = α x α f x α f = α f x α f(f x) α twice = α f α x α f(f x) 型方程式を解く α f = α x α x α f x = α f(f x) = α x α twice = (α x α x ) α x α x α M : 部分式 M の型

37 以下のアウトライン型検査アルゴリズム型推論単純型つき λ 計算の拡張

38 構文組型を加えた拡張簡約 τ ( 型 ) ::= b τ 1 τ 2 τ 1 τ 2 b ( 基本型 ) ::= int bool... M ( 項 ) 型付け... fst(m 1, M 2 ) M 1 snd(m 1, M 2 ) M 2 ::=... (M 1, M 2 ) fst(m) snd(m) Γ M: τ 1 Γ N: τ 2 Γ (M, N): τ 1 τ 2 Γ M: τ 1 τ 2 Γ fst(m): τ 1 Γ M: τ 1 τ 2 Γ snd(m): τ 2

39 構文直和型を加えた拡張 τ ( 型 ) ::=... τ 1 +τ 2 M ( 項 ) ::=... inl(m) inr(m) case M 0 of inl(x)=>m 1 inr(y)=>m 2 簡約 case inl(m) of inl(x)=>m 1 inr(y)=>m 2 [M/x]M 1 型付け case inr(m) of inl(x)=>m 1 inr(y)=>m 2 [M/x]M 2 Γ M: τ 1 Γ inl(m): τ 1 +τ 2 Γ M: τ 2 Γ inr(m): τ 1 +τ 2 Γ L: τ 1 +τ 2 Γ,x: τ 1 M: τ Γ,y: τ 2 N: τ Γ case L of inl(x)=>m inr(y)=>n: τ

40 単純型つき λ 計算の様々な拡張 Sysytem F ( 型つき λ 計算の一種 ) 型も関数の引数に τ ( 型 ) ::= b α τ 1 τ 2 α.τ M ::= x λx:τ.m MN Λ α.m M[τ] - 型推論は決定不能再帰型 τ ( 型 ) ::= b α τ 1 τ 2 µα.τ 不動点演算子が表現可能 (=> 再帰を表現できる ) 部分型 (Subyping) σ < τ: σ 型の値は τ 型の値として使える e.g. int < real, 依存型型が値に依存できる real int < int real e.g. int array[n] : サイズ n の配列の型 n:int -> int array[n]: 整数 n をうけとりサイズ n の配列を返す関数の型

構造化プログラミングとデータ抽象

構造化プログラミングとデータ抽象計算の理論後半第 3 回 λ 計算と型システム本日の内容 λ 計算の表現力 ( 前回のつづき ) 前回の復習不動点演算子と再帰 λ 計算の重要な性質チャーチロッサー性簡約戦略型付き λ 計算ブール値組ブール値と組の表現 ( 復習 ) true, false を受け取り対応する要素を返す関数として表現 T = λt.λf.t F = λt.λf.f if e 1 then e

構造化プログラミングと データ抽象

構造化プログラミングとデータ抽象