ML λ λ 1 λ 1.1 λ λ λ e (λ ) ::= x ( ) λx.e (λ ) e 1 e 2 ( ) ML λx.e Objective Caml fun x -> e x e let 1

2005 sumii@ecei.tohoku.ac.jp 2005 6 24 ML λ λ 1 λ 1.1 λ λ λ e (λ ) ::= x ( ) λx.e (λ ) e 1 e 2 ( ) ML λx.e Objective Caml fun x -> e x e let 1

let λ 1 let x = e1 in e2 (λx.e 2 )e 1 e 1 x e 2 λ 3 λx.(λy.e) λx.λy.e λx.(e 1 e 2 ) λx.e 1 e 2 λ (e 1 e 2 )e 3 e 1 e 2 e 3 10 3 7 10 (3 7) (10 3) 7 1.2 β λ small-step λ λ λ λx.e 1 e 2 x e 2 e 1 (λx.e 1 )e 2 [e 2 /x]e 1 (R-Beta) λ λ [e 2 /x]e 1 e 1 x e 2 λ 1 β (λx.e 1 )e 2 [e 2 /x]e 1 1 β 1 λ λ λ 2

(λx.x)y y (λx.λy.x)z λy.z (λx.x)(λy.y) λy.y 1. 1 β 1.3 β (λa.b)cd λ (λa.b)cd e e 2 (R-Beta) λ (λa.b)c (R-Beta) (R-Beta) (λa.b)cd Objective Caml (fun a -> b) c d e 1 e 2 e 1 (R-App1) e 1 e 1 e 1 e 2 e 1e 2 (R-App1) λ (λa.b)cd bd 2 (λa.b)cd (λa.b)(cd) ((λa.b)c)d (λa.b)cd = (λa.b)(cd) b 3

(λa.b)c b R-Beta (λa.b)cd bd R-App1 (R-App1) e 1 e 2 e 2 (R- App2) e 2 e 2 e 1 e 2 e 1 e 2 (R-App2) 2. (R-App2) 1. (R-App1) (R-App2) e 1 e 2 e 1 e 2 λ λx.e e (R-Abs) e e λx.e λx.e (R-Abs) ML fun x -> e e (R-Abs) (R-Abs) λx.(λy.y)x λx.x (R-Abs) 1.4 α (λx.λy.xy)y??? (R-Beta) (λx.λy.xy)y λy.yy 4

(λx.λy.xy)y y y λy.yy (λx.λy.xy)y y y y y (λx.λy.xy )y (λx.λy.xy )y λy.yy y λ (λx.λy.xy )y y λy (λx.λy.xy )y y λ λx.xx λy.yy α λ e 1 e 2 α e 1 e 2 α λ λx.y λx.z # let y = (fun a -> fun b -> a) ;; (* y val y : a -> b -> a = <fun> # let z = (fun a -> fun b -> b) ;; (* z val z : a -> b -> b = <fun> 5

# let e1 = (fun x -> y) ;; (* x. y val e1 : a -> b -> c -> b = <fun> # let e2 = (fun x -> z) ;; (* x. z val e2 : a -> b -> c -> c = <fun> # e1 "xxx" "yyy" "zzz" ;; - : string = "yyy" # e2 "xxx" "yyy" "zzz" ;; - : string = "zzz" 2. λ f f(x) = x + 1 g(y) = y + 1 g x, y 1 x2 dx 1 y 2 dy x y α β [e 2 /x]e 1 e 1 e 2 e 1 α e 1 [e 2 /x]y = e 2 (x = y ) y (x y ) [e 2 /x](λy.e) = λy.[e 2 /x]([y /y]e) ( y ) [e 2 /x](ee ) = ([e 2 /x]e)([e 2 /x]e ) 6

1.5 Objective Caml λ Objective Caml type exp = (* Var of string Abs of string * exp (* App of exp * exp (* (* (* let gensym = (* let counter = ref 0 in fun () -> incr counter; (* 0 counter (* () (* counter "g" ^ string_of_int!counter (* g1, g2, g3,... let rec subst e2 x e1 = (* [e2/x]e1 match e1 with Var(y) -> if x = y then e2 else Var(y) Abs(y, e) -> let y = gensym () in Abs(y, subst e2 x (subst (Var(y )) y e)) App(e, e ) -> App(subst e2 x e, subst e2 x e ) let rec step e = (* e e -> e e match e with Var(x) -> [] Abs(x, e0) -> (* (R-Abs) List.map (fun e0 -> Abs(x, e0 )) (step e0) 7

App(e1, e2) -> (* (R-Beta) (match e1 with Abs(x, e0) -> [subst e2 x e0] _ -> []) @ (* (R-App1) List.map (fun e1 -> App(e1, e2)) (step e1) @ (* (R-App2) List.map (fun e2 -> App(e1, e2 )) (step e2) let rec repeat e = (* step match step e with [] -> e e :: _ -> repeat e : # let e1 = Abs("x", Var("x")) ;; (* ( x. x) val e1 : exp = Abs ("x", Var "x") # step e1 ;; - : exp list = [] # let e2 = App(e1, e1) ;; (* ( x. x) ( x. x) val e2 : exp = App (Abs ("x", Var "x"), Abs ("x", Var "x")) # step e2 ;; - : exp list = [Abs ("x", Var "x")] # let e3 = App(e2, e2) ;; (* (( x. x) ( x. x)) (( x. x) ( x. x)) val e3 : exp = App (App (Abs ("x", Var "x"), Abs ("x", Var "x")), App (Abs ("x", Var "x"), Abs ("x", Var "x"))) 8

# step e3 ;; - : exp list = [App (Abs ("x", Var "x"), App (Abs ("x", Var "x"), Abs ("x", Var "x"))); App (App (Abs ("x", Var "x"), Abs ("x", Var "x")), Abs ("x", Var "x"))] # repeat e3 ;; - : exp = Abs ("x", Var "x") 3. step e 2 repeat e 1.6 λ e e e e 0 2 0 λ e 1 e 2 OK 2 λ 1 ( ). λ e e e 1 e e 2 e 1 = e 2 0 e 0 e n e 0 e 1 e 2... e n 1 e n (n 0) e 1, e 2,..., e n 1 e e e 1 e 2 e 2 e 3 e 1 e 3 9

e e e e 2 ( ). λ e e e 1 e e 2 e 1 e e 2 e e 4. 2 1 Ω = (λx.xx)(λx.xx) Ω Ω Ω... (λx.y)ω (λx.y)ω y (λx.y)ω (λx.y)ω (λx.y)ω... λ X X X (λx.y)ω Ω (λx.y)ω λ repeat step e step 5. 10

ML # let rec loop x = loop x ;; (* val loop : a -> b = <fun> # let y = (fun z -> z) ;; (* y val y : a -> a = <fun> # (fun x -> y) (loop ()) ;; Interrupted. λx.y (call-by-value) (call-by-name) Haskell (call-by-need) 1.7 λ λ λ 1.7.1 true, false if e 1 then e 2 else e 3 true = λt.λf.t false = λt.λf.f if e 1 then e 2 else e 3 = e 1 e 2 e 3 if true then e 2 else e 3 = true e 2 e 3 = (λt.λf.t)e 2 e 3 (λf.e 2 )e 3 e 2 11

if false then e 2 else e 3 = false e 2 e 3 = (λt.λf.f)e 2 e 3 (λf.f)e 3 e 3 b if b then e 2 else e 3 b then e 2 else e 3 b true e 2 e 3 e 2 λt.λf.t false e 2 e 3 e 3 λt.λf.f b if b then else 1.7.2 (e 1, e 2 ) = λc.ce 1 e 2 match e 1 with (f, s) -> e 2 = e 1 (λf.λs.e 2 ) c e 1 e 2 λc.ce 1 e 2 (e 1, e 2 ) match 12

6. match (e 1, e 2 ) with (x, y) -> e 3 [e 2 /y][e 1 /x]e 3 1.7.3 0 = λs.λz.z 1 = λs.λz.sz 2 = λs.λz.s(sz) 3 = λs.λz.s(s(sz)). λ (Church encoding) z s 0 z 1 s(z) 2 s(s(z)) 3 s(s(s(z))) s z s z λ 0 = λs.λz.z 1 = λs.λz.sz 2 = λs.λz.s(sz) 3 = λs.λz.s(s(sz)). 13

m + n m + n = λs.λz.ns(msz) msz z s m msz s n m + n s 1 + 2 = λs.λz.1s(2sz) = λs.λz.(λs.λz.sz)s(2sz) λs.λz.(λz.sz)(2sz) λs.λz.s(2sz) = λs.λz.s((λs.λz.s(sz))sz) λs.λz.s((λz.s(sz))z) λs.λz.s(s(sz)) = 3 # let one = Abs("s", Abs("z", App(Var("s"), Var("z")))) ;; val one : exp = Abs ("s", Abs ("z", App (Var "s", Var "z"))) # let two = Abs("s", Abs("z", App(Var("s"), App(Var("s"), Var("z")))));; val two : exp = Abs ("s", Abs ("z", App (Var "s", App (Var "s", Var "z")))) # let plus m n = Abs ("s", Abs ("z", 14

App (App (m, Var("s")), App(App(n, Var("s")), Var("z"))))) ;; val plus : exp -> exp -> exp = <fun> # repeat (plus one two) ;; - : exp = Abs ("s", Abs ("z", App (Var "s", App (Var "s", App (Var "s", Var "z"))))) m n m n = λs.λz.n(λz.msz )z s m n s m n s m λz.msz n n(λz.msz )z z z 7. 1 + 2 3 2 3 6 8. m + n m n λ m n λ m < n m n = 0 1.7.4 g(y) = e fix f = (λx.f(xx))(λx.f(xx)) λ g = fix λg.λy.e 3 3 e g g = λy.e 15

λ f fix f fix f = (λx.f(xx))(λx.f(xx)) f((λx.f(xx))(λx.f(xx))) = f(fix f ) fix f f g(y) g(y) = (fix λg.λy.e )y (λg.λy.e)(fix λg.λy.e )y = (λg.λy.e)gy (λy.e)y e 4 g(y) = e 2 λ λ false 2 false + 2 false + 2 = (λt.λf.f) + 2 = (λs.λz.z) + 2 = 0 + 2 2 4 g g = fix λg.λy.e g λ fix λg.λy.e α fix λg.λy.[g /g]e 16

λ if 3 + 7 then 10 else false λ 2.1 τ τ ( ) ::= b ( ) τ 1 τ 2 ( ) bool nat τ ( ) ::= τ 1 τ 2 ( ) τ 2.2 τ e τ λx.x x x τ τ λx.x τ τ λx.x : τ τ e τ 17

e : τ λx.y y y τ λx.y τ τ y : τ λx.y : τ τ x 1, x 2,..., x n τ 1, τ 2,..., τ n e τ x 1 : τ 1, x 2 : τ 2,..., x n : τ n e : τ m : nat, n : nat, plus : nat nat nat plus m n : nat nat nat nat nat (nat nat) x 1 : τ 1, x 2 : τ 2,..., x n : τ n Γ x 1, x 2,..., x n τ 1, τ 2,..., τ n 2.3 Γ, e, τ Γ e : τ 18

λ Γ(x) = τ Γ x : τ (T-Var) Γ, x : τ 1 e : τ 2 Γ λx.e : τ 1 τ 2 Γ e 1 : τ τ Γ e 2 : τ Γ e 1 e 2 : τ (T-Abs) (T-App) (T-Var) Γ x : τ Γ x τ (T-App) Γ e 1 τ τ e 2 τ e 1 e 2 τ (T-Abs) Γ λx.e τ 1 τ 2 Γ x : τ 1 Γ, x : τ 1 e τ 2 x τ 1 e τ 2 : s : nat nat, z : nat s : nat nat T-Var s : nat nat, z : nat z : nat T-Var s : nat nat, z : nat sz : nat s : nat nat λz.sz : nat nat λs.λz.sz : (nat nat) nat nat T-App T-Abs T-Abs 2.4 false + 5 if 3 + 7 then 10 else false λ λ λ 19

λ λ = v ( ) ::= λx.e ( ) λ 3 ( ). e : τ e e e 1 ( ). e : τ e e e e 2 ( ). e : τ e e e : τ e : τ 3 ( ). Γ e 1 : τ 1 Γ, x : τ 1 e 2 : τ 2 Γ [e 1 /x]e 2 : τ 2. Γ, x : τ 1 e 2 : τ 2 9. 1 2 3 2.5 1.7.1 true = λt.λf.t false = λt.λf.f if e 1 then e 2 else e 3 = e 1 e 2 e 3 20

λ true = λf.λt.t false = λf.λt.f if e 1 then e 2 else e 3 = e 1 e 3 e 2 true false true : bool, false : bool, if : bool nat nat nat e : nat true, false, if λ e [λt.λf.t/true][λt.λf.f/false][λb.λt.λf.btf/if]e 1 [λf.λt.t/true][λf.λt.f/false][λb.λt.λf.bf t/if]e 2 e true 2 e (T-App) Objective Caml # let ht = Hashtbl.create 10 ;; (* ht val ht : ( _a, _b) Hashtbl.t = <abstr> # ht ;; (* ht - : (string, int) Hashtbl.t = <abstr> 21

# Hashtbl.add ht "abc" 123 ;; (* "abc" 123 ht - : unit = () # Hashtbl.add ht "de" 456 ;; (* "de" 456 - : unit = () # Hashtbl.add ht "f" 789 ;; (* "f" 789 - : unit = () # Hashtbl.find ht "de" ;; (* "de" - : int = 456 # Hashtbl.find ht "g" ;; (* "g" Exception: Not_found. # ht + 1 ;; (* Hashtbl ht Characters 0-2: ht + 1 ;; (* Hashtbl ht ^^ This expression has type (string, int) Hashtbl.t but is here used with type int λ 9,,, ISBN 4-320-02659-4. 5 Types and Programming Languages. Benjamin C. Pierce. The MIT Press. ISBN 0-262-16209-1. 5 22