User Tools

Site Tools


untypedlambda-prog

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

untypedlambda-prog [2015/10/08 15:20] (current)
Line 1: Line 1:
 +====== Programming in the untyped λ-calculus ======
 +
 +
 +===== Booleans =====
 +
 +<code ocaml>
 +let ift = Abs("​x",​Var "​x"​);;​
 +
 +let t = Abs("​x",​Abs("​y",​Var "​x"​));;​
 +
 +let f = Abs("​x",​Abs("​y",​Var "​y"​));;​
 +</​code>​
 +
 +\\
 +
 +
 +===== Church numerals =====
 +
 +
 +<code ocaml>
 +let rec iter f x n = if n=0 then x else App(f,(iter f x (n-1)));;
 +
 +let church n = Abs("​f",​Abs("​x",​iter (Var "​f"​) (Var "​x"​) n));;
 +
 +print_string (string_of_term (church 0));;
 +print_string (string_of_term (church 1));;
 +print_string (string_of_term (church 2));;
 +
 +let succ = 
 +  Abs("​n",​Abs("​f",​Abs("​x",​
 +    App(Var "​f",​(App(App(Var "​n",​Var "​f"​),​Var "​x"​))))));;​
 +
 +let iszero = 
 +  Abs("​n",​Abs("​x",​Abs("​y",​
 +    App(App(Var "​n",​Abs("​z",​Var "​y"​)),​Var "​x"​))));;​
 +
 +reducefix (App(iszero,​(church 0)));;
 +reducefix (App(iszero,​(church 1)));;
 +
 +let rec unchurch t = match t with
 +  Abs(f,​Abs(x,​t'​)) -> (match t' with 
 +    Var x -> 0
 +  | App(Var f,s) -> 1 + unchurch (Abs(f,​Abs(x,​s)))
 +  | _ -> raise Error)
 +  | _ -> raise Error;;
 +
 +unchurch (church 2);;
 +
 +unchurch (reducefix (App(succ,​(church 1))));;
 +</​code>​
 +
 +\\
 +
 +===== Pairs =====
 +
 +
 +Pairs and their accessor functions, as well as tuples,
 +can also be encoded in the untypedlambda|untyped lambda calculus.
 +Yet, their type is much less informative than the type of primitive OCaml tuples.
 +
 +<code ocaml>
 +# let untyped_true = fun x y -> x;;
 +val untyped_true : 'a -> 'b -> 'a = <fun>
 +
 +# let untyped_false = fun x y -> y;;
 +val untyped_false : 'a -> 'b -> 'b = <fun>
 +
 +# let untyped_pair = fun f s b -> b f s;;
 +val untyped_pair : 'a -> 'b -> ('a -> 'b -> 'c) -> 'c = <fun>
 +
 +# let untyped_fst = fun p -> p untyped_true;;​
 +val untyped_fst : (('a -> 'b -> 'a) -> 'c) -> 'c = <fun>
 +
 +# let untyped_snd = fun p -> p untyped_false;;​
 +val untyped_snd : (('a -> 'b -> 'b) -> 'c) -> 'c = <fun>
 +
 +# untyped_fst (untyped_pair 1 "​alice"​);;​
 +- : int = 1
 +
 +# untyped_snd (untyped_pair 1 "​alice"​);;​
 +- : string = "​alice"​
 +</​code>​
 +
 +
 +<code ocaml>
 +let pair = Abs("​x",​Abs("​y",​Abs("​z",​App(App(Var "​z",​Var "​x"​),​Var "​y"​))));;​
 +let fst = Abs("​x",​App(Var "​x",​t));;​
 +let snd = Abs("​x",​App(Var "​x",​f));;​
 +
 +let t1 = App(snd,​App(App(pair,​church 0),church 1));;
 +
 +unchurch (reducefix t1);;
 +</​code>​
 +
 +\\
 +
 +
 +===== Predecessor =====
 +
 +<code ocaml>
 +let z = App(App(pair,​church 0),church 0);;
 +let s = Abs("​x",​App(App(pair,​App(snd,​Var "​x"​)),​App(succ,​App(snd,​Var "​x"​))));;​
 +
 +unchurch (reducefix (App(snd,​App(s,​App(s,​z)))));;​
 +
 +let pred = Abs("​n",​App(fst,​App(App(Var "​n",​s),​z)));;​
 +
 +unchurch (reducefix (App(pred,​church 9)));;
 +</​code>​
 +
 +\\
 +
 +
 +===== Fixed points =====
 +
 +<code ocaml>
 +let u = Abs("​x",​Abs("​y",​App(Var "​y",​App(App(Var "​x",​Var "​x"​),​Var "​y"​))));;​
 +let theta = App(u,u);;
 +</​code>​
 +
 +\\
 +
 +
 +===== Addition =====
 +
 +<code ocaml>
 +let fadd = Abs("​f",​Abs("​n",​Abs("​m",​App(App(App(ift,​App(iszero,​Var "​n"​)),​Var "​m"​),​App(succ,​App(App(Var "​f",​App(pred,​Var "​n"​)),​Var "​m"​))))));;​
 +
 +let add = App(theta,​fadd);;​
 +
 +unchurch (reducefix (App(App(add,​church 3),church 5)));;
 +</​code>​
  
untypedlambda-prog.txt · Last modified: 2015/10/08 15:20 (external edit)