koba/class/soft-kiso/ 1 λ if λx.λy.y false 0 λ typed λ-calculus λ λ 1.1 λ λ, syntax τ (types) ::= b τ 1 τ 2 τ 1

Size: px

Start display at page:

Download "koba/class/soft-kiso/ 1 λ if λx.λy.y false 0 λ typed λ-calculus λ λ 1.1 λ λ, syntax τ (types) ::= b τ 1 τ 2 τ 1"

ことこたかはし
4 years ago
Views:

1 koba/class/soft-kiso/ 1 λ if λx.λy.y false 0 λ typed λ-calculus λ λ 1.1 λ λ, syntax τ (types) ::= b τ 1 τ 2 τ 1 τ 2 M (terms) ::= c τ x M 1 M 2 λx : τ.m (M 1,M 2 ) fst(m) snd(m) b int bool τ 1 τ 2 τ 1 τ 2 (1, true) int bool λ c τ 1 c τ τ τ b b 1 b 2, b 1 b 2 b b 1 b 2 c b 1 b 2 b 1 b 2 [[c b 1 b 2 ]] b 1 b 2 b c b 1 b 2 b b 1 b 2 b [[c b 1 b 2 b ]] b c b c b b 1 λ false 0 λ λx.λy.x 1

2 c τ τ c 1 int 1 λx : τ.m x C Java ML (M 1,M 2 ) M 1 M 2 fst(m) M snd(m) M call-by-value call-by-name V (value) ::= c τ λx.m (V 1,V 2 ) (λx.m)v cbv [V/x]M (R-Beta) c b 1 b c b 1 1 cbv [[c b 1 b ]] (c b 1 1 ) (R-Const1) c b 1 b 2 b (c b 1 1,c b 2 2 ) cbv [[c b 1 b 2 b ]] (c b 1 1,c b 2 2 ) (R-Const2) M cbv M MN cbv M N N cbv N VN cbv VN (R-App1) (R-App2) M 1 cbv M 1 (M 1,M 2 ) cbv (M 1,M 2) (R-Pair1) M 2 cbv M 2 (V,M 2 ) cbv (V,M 2 ) M cbv M fst(m) cbv fst(m ) fst(v 1,V 2 ) cbv V 1 M cbv M snd(m) cbv snd(m ) snd(v 1,V 2 ) cbv V 2 (R-Pari2) (R-Fst1) (R-Fst2) (R-Snd1) (R-Snd2) 2

3 1.1.3 λ, syntax term syntax (λx : int.x)true formal Γ M : τ Γ Γ M : τ Γ M τ Γ M τ inductive T-Var T-Abs Γ,x: τ Γ x τ Γ c τ : τ Γ,x: τ x : τ (T-Const) (T-Var) Γ M 1 : τ 1 τ 2 Γ M 2 : τ 1 Γ M 1 M 2 : τ 2 (T-App) Γ,x: τ 1 M : τ 2 Γ λx : τ 1.M : τ 1 τ 2 (T-Abs) Γ M 1 : τ 1 Γ M 2 : τ 2 Γ (M 1,M 2 ):τ 1 τ 2 (T-Pair) Γ M : τ 1 τ 2 Γ fst(m) :τ 1 (T-Fst) Γ M : τ 1 τ 2 Γ snd(m) :τ 2 (T-Snd) Γ M : τ M Γ (well-typed) Remark 1.1: α λx:int.λx: bool.x x : int,y: bool y : bool x : int λy : bool.y(= λx : bool.x) :bool bool λx : int.λx : bool.x : int bool bool 3

4 Exercise term Γ M : τ Γ,τ 1. λx : int.yx 2. xx 3. λz :(int int int).zxy 4. (xy)(xz) 5. (yx)(zx) Γ M Γ M : τ τ unique Theorem 1.2: Γ M : τ 1 Γ M : τ 2 τ 1 = τ 2. Exercise (Type Soundness) λ 1(2) + int int int (true, 1) fst snd fst(1) fst(1) 1.3 M 1.4, subject reduction M M 1.10 Theorem 1.3 [Progress]: M : τ M M M cbv M Proof: M M = c τ M 2 C 4

5 M = x M : τ M = M 1 M 2 M : τ τ 1 M 1 : τ 1 τ M 2 : τ 1 M 1 M 1 cbv M 1 M 1 M = M 1 M 2 M cbv M M 1 M 1 = c τ1 τ M 1 = λx.m 1 M 2 M 2 : M 2 cbv M 2 M 2 M = M 1 M 2 M cbv M M 2 M 1 = λx.m 1 M =[M 2 /x]m 1 R-Beta M cbv M M 1 = c τ1 τ τ 1 τ = b 1 b 2 b τ 1 τ = b 1 b M 2 : b 1 b 2 M 2 M 2 =(c b 1 1,c b 2 2 ) M =[[c b 1 b 2 b ]] (c b 1 1,c b 2 2 ) R-Const2 M cbv M M 2 : b 1 M 2 M 2 = c b 1 1 M =[[c b1 b ]] (c b 1 1 ) R-Const1 M cbv M M = λx : τ.m 1 M M =(M 1,M 2 ) M : τ M M 1 M 2 τ = τ 1 τ 2 M 1 : τ 1 M 2 : τ 2 M 1 M 1 cbv M 1 M 1 M =(M 1,M 2) M cbv M M 1 M 2 M 2 cbv M 2 M 2 M =(M 1,M 2 ) R-Pair2 M cbv M M = fst(m 1 ) M : τ M 1 : τ τ 2 M 1 M 1 cbv M 1 M 1 M = fst(m 1 ) M cbv M M 1 M 1 =(V 1,V 2 ) M = V 1 R-Fst2 M cbv M M = snd(m 1 ) M = fst(m 1 ) Theorem 1.4 [ (Type Preservation)]: Γ M : τ M cbv Γ M : τ M Γ Γ Γ, Γ x. τ.(γ(x) =τ Γ (x) =τ) Lemma 1.5 [weakening]: Γ M : τ Γ Γ Γ M : τ Proof: Γ M : τ 5

6 Exercise 1.6: Lemma 1.7 [substitution lemma]: Γ M 1 : τ 1 Γ,x : τ 1 M 2 : τ 2 Γ [M 1 /x]m 2 : τ 2 Proof: M 2 M 2 = x [M 1 /x]m 2 = M 1 M 2 = y( x) [M 1 /x]m 2 = y Γ,x : τ 1 M 2 : τ 2 Γ(y) =τ 2 Γ [M 1 /x]m 2 : τ 2 M 2 = λy : τ 21.M 2 Γ,x : τ 1 M 2 : τ 2 Γ,x : τ 1,y : τ 21 M 2 : τ 22 τ 2 = τ 21 τ 22 Lemma 1.5 Γ,y : τ 21 M 1 : τ 1 Γ,y: τ 21 [M 1 /x]m 2 : τ 22 T-Abs Γ λy : τ 21.[M 1 /x]m 2 : τ 21 τ 22 Γ [M 1 /x]m 2 : τ 2 Exercise 1.8: Proof of Theorem 1.4: M cbv M R-Beta M =(λx.m 1 )M 2 M =[M 2 /x]m 1 Γ M : τ Γ,x: τ 1 M 1 : τ Γ M 2 : τ 1 Lemma 1.7 Γ M : τ R-Const1 M = c b1 b c b 1 1 M =[[c b1 b ]] (c b 1 1 )=c b 2 τ = b T-Const Γ M : τ R-App1 M = M 1 M 2 M = M 1 M 2 M 1 cbv M 1 Γ M : τ Γ M 1 : τ 1 τ Γ M 2 : τ 1 Γ M 1 : τ 1 τ T-App Γ M : τ Exercise 1.9: Corollary 1.10 [Type Soundness]: M : τ M cbv M cbv M Exercise 1.4 M cbv M induction 6

7 1.1.5 Strong Normalization λ, β-reduction call-by-value cbv normal form Theorem 1.11 [strong normalization]: Γ M : τ β M β M 2 [2] β M 1 β strong normalization λ, total function strong normalization fixed point operator fix (τ 1 τ 2 ) (τ 1 τ 2 ) Principal Typing λ, λx : τ.m e (terms) ::= c τ x e 1 e 2 λx.e (e 1,e 2 ) fst(e) snd(e) e Γ M : τ Γ,M,τ M e e Γ,M,τ e = x τ x : τ M : τ e = λx.x τ λx : τ.x : τ τ reasonable syntax Γ M : τ Γ,M,τ syntax τ (types) ::= α (type variables) b τ 1 τ 2 τ 1 τ 2 λ, M Erase(M) e Γ,M,τ Definition 1.12 [principal typing]: (Γ,M,τ) e principal typing 1. Erase(M) =e 2. Γ M : τ 3. Γ M : τ, Erase(M )=e Γ,M,τ θ 7

8 (a) θγ Γ (b) θm = M (c) θτ = τ Γ,M,τ, principal typing λ, principal typing unification mgu 3 PT(c τ ) = (,c τ,τ) PT(x) = (x : α, x, α) where α is fresh PT(e 1 e 2 ) = let (Γ 1,M 1,τ 1 )=PT(e 1 ) (Γ 2,M 2,τ 2 )=PT(e 2 ) θ = mgu({(τ 1,τ 2 α)} {(Γ 1 (x), Γ 2 (x)) x dom(γ 1 ) dom(γ 2 )}) where α is fresh in ((θγ 1 ) (θγ 2 ),θ(m 1 M 2 ),θα) PT(λx.e) = let (Γ,M,τ)=PT(e) in if x dom(γ) then (Γ\x, λx :Γ(x).M, Γ(x) τ) else (Γ,λx: α.m, α τ) where α is fresh PT((e 1,e 2 )) = let (Γ 1,M 1,τ 1 )=PT(e 1 ) (Γ 2,M 2,τ 2 )=PT(e 2 ) θ = {(Γ 1 (x), Γ 2 (x)) x dom(γ 1 ) dom(γ 2 )}) in ((θγ 1 ) (θγ 2 ),θ((m 1,M 2 )),θ(τ 1 τ 2 )) PT(fst(e)) = let (Γ,M,τ)=PT(e) θ = mgu({(τ,α β)} where α,β are fresh in (θγ,θ(fst(m)),θα) PT(snd(e)) = let (Γ,M,τ)=PT(e) θ = mgu({(τ,α β)} where α,β are fresh in (θγ,θ(snd(m)),θβ) 3 {(τ 11,τ 12),...,(τ n1,τ n2)} τ 11 = τ 12,...,τ n1 = τ n2 (most general unifier) 8

9 Exercise principal typing ML Prolog 1.2 Polymorphism λ, λx.x λx : τ.x (monomorphic) (polymorphic) ML parametric polymorphism λ, λx : τ.x λx.x λx : τ.x (λx.xx)(λx.x) λ, λx : τ.x τ λ λx : τ.x (Λα : U 1.λx : α.x)τ Id =Λα : U 1.λx : α.x Id τ = λx : τ.x Id τ Id[τ] Id compose compose =Λα : U 1.Λβ : U 1.Λγ : U 1.λf : β γ.λg : α β.λx : α.f(g(x)) U 1 τ : U 1 τ U 1 τ ::= α b τ 1 τ 2 τ 1 τ 2 Id compose U 1 Id τ τ τ α : U 1.(α α) compose α : U 1. β : U 1. γ : U 1.((β γ) (α β) α γ) U 1 α 1 : U 1. α n : U 1.τ U 2 U 2 σ 9

10 Remark 1.13: U 2 U impredicative polymorphism τ ::= α b τ 1 τ 2 τ 1 τ 2 α : U.τ ( α.α) ( α.α) U 2 syntax, :U 1 Definition 1.14 [λ, -term]: M ::= c σ x M 1 M 2 λx : τ.m Λα.M M[τ] Γ c σ : σ Γ,x: σ x : σ (TPoly-Const) (TPoly-Var) Γ M 1 : τ 1 τ 2 Γ M 2 : τ 1 Γ M 1 M 2 : τ 2 (TPoly-App) Γ,x: τ 1 M : τ 2 Γ λx : τ 1.M : τ 1 τ 2 Γ M : σ α not free in Γ Γ Λα.M : α.σ Γ M : α.σ Γ M[τ]:[τ/α]σ (TPoly-Abs) (TPoly- -Intro) (TPoly- -Elim) λ,,let λ, untyped λ-calculus (λx.xx)(λx.x) term (λx : α.(α α).(x[τ τ])(x[τ]))(λα.λx : α.x)) λx : α.(α α).(x[τ τ])(x[τ]) α.(α α) τ τ ( α.(α α)) (τ τ) U 1 U 2 σ ::= α b σ 1 σ 2 α.σ 10

11 α.σ impredicative polymorphsim Girard Reynolds construct ML[1] syntax let M ::= x M 1 M 2 λx : τ.m Λα.M M[τ] let x : σ = M 1 in M 2 end let Γ M 1 : σ Γ,x: σ M 2 : τ Γ let x : σ = M 1 in M 2 end : τ (TPoly-Let) x M 2 U 2 σ let bind body polymorphic let x : α.(α α) =Λα.λx : α.x in (x[τ τ])(x[τ]) end λ bind monomorphic λ,,let λ e Γ M : σ, Erase(M) = e (Γ,M,σ) syntax Erase e ::= x e 1 e 2 λx.e let x = e 1 in e 2 end Erase(x) = x Erase(M 1 M 2 ) = Erase(M 1 )Erase(M 2 ) Erase(λx : τ.m) = λx.erase(m) Erase(Λα.M) = Erase(M) Erase(M[τ]) = Erase(M) Erase(let x : σ = M 1 in M 2 end) = let x = Erase(M 1 ) in Erase(M 2 ) end syntax ML ML λ,,let λ,,let λ, M Erase(M) Γ e : σ α not free in Γ Γ e : α.σ (T-ML- -Intro) 11

12 Γ e : α.σ Γ e :[τ/α]σ (T-ML- -Elim) λ, M T-ML- -Intro, T-ML- -Elim T-ML- -Elim U 2 T-ML- -Elim U 2 TPoly-Var T-ML- -Elim, T-ML- -Intro T-ML- -Intro Γ e : σ Γ e : α.σ Γ e :[τ/α]σ Γ e : σ α τ Γ e :[τ/α]σ T-ML- -Elim TPoly-Var T-ML- -Intro TPoly-Let λ,,let Γ e : τ type judgement Γ,x: α.τ x[ τ]:[ τ/ α]τ (T-ML-Var) Γ M 1 : τ 1 τ 2 Γ M 2 : τ 1 Γ M 1 M 2 : τ 2 (T-ML-App) Γ,x: τ 1 M : τ 2 Γ λx : τ 1.M : τ 1 τ 2 (T-ML-Abs) Γ M 1 : τ 1 Γ,x: α.τ 1 M 2 : τ 2 { α} τ 1 Γ Γ let x : α.τ 1 =Λ α.m 1 in M 2 end : τ 2 (T-ML-Let) 12

13 λ,,let λ, principal typing principal typing e (Γ,M,σ) Γ,σ U 1 e (Γ,M,σ) M,τ λ,,let principal typing A let U 2 e principal typing PT(e, ) PT(c α.τ,a) = (,c α.τ [ β], [ β/ α]τ) where β are fresh. PT(x, A) = if A(x) = α.τ then (x : α.τ, x[ β], [ β/ α]τ) where β are fresh. else({x : α},x,α) where α is fresh PT(e 1 e 2,A) = let (Γ 1,M 1,τ 1 )=PT(e 1,A) (Γ 2,M 2,τ 2 )=PT(e 2,A) θ = mgu({(τ 1,τ 2 α)}) {(Γ 1 (x), Γ 2 (x)) x dom(γ 1 ) dom(γ 2 )}) where α is fresh in ((θγ 1 ) (θγ 2 ),θ(m 1 M 2 ),θα) PT(λx.e, A) = let (Γ, M, τ)=pt(e, A) in if x dom(γ) then (Γ\x, λx :Γ(x).M, Γ(x) τ) else (Γ,λx: α.m, α τ) where α is fresh PT(let x = e 1 in e 2 end,a) = let (Γ 1,M 1,τ 1 )=PT(e 1,A) (Γ 2,M 2,τ 2 )=PT(e 2,A {x: α.τ 1 }) where α appears in τ 1 but not in Γ 1 θ = mgu({(γ 1 (y), Γ 2 (y)) x dom(γ 1 ) dom(γ 2 )}) in ((θγ 1 ) (θ(γ 2 \x)),θ(let x : α.τ 1 =Λ αm 1 in M 2 end),θτ 2 ) [1] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). The MIT Press, [2].. 9.,

Int Int 29 print Int fmt tostring 2 2 [19] ML ML [19] ML Emacs Standard ML M M ::= x c λx.m M M let x = M in M end (M) x c λx.

Int Int 29 print Int fmt tostring 2 2 [19] ML ML [19] ML Emacs Standard ML M M ::= x c λx.m M M let x = M in M end (M) x c λx. 1, 2 1 m110057@shibaura-it.ac.jp 2 sasano@sic.shibaura-it.ac.jp Eclipse Visual Studio ML Standard ML Emacs 1 ( IDE ) IDE C C++ Java IDE IDE IDE IDE Eclipse Java IDE Java Standard ML 1 print (Int. 1 Int