User Tools

Site Tools


untypedlambda

Differences

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

Link to this comparison view

untypedlambda [2015/10/08 15:20] (current)
Line 1: Line 1:
 +====== Normal order evaluation of λ-terms ======
 +
 +
 +===== Syntax of λ-terms =====
 +
 +<code ocaml>
 +# type term = Var of string ​
 +            | Abs of (string * term) 
 +            | App of term * term;;
 +</​code>​
 +
 +== Examples ==
 +
 +<code ocaml>
 +# let id = Abs("​x",​Var "​x"​);;​
 +# let k = Abs("​x",​Abs("​y",​Var "​x"​));;​
 +# let omega = App(Abs("​x",​App(Var "​x",​Var "​x"​)),​Abs("​x",​App(Var "​x",​Var "​x"​)));;​
 +# let const z = Abs("​x",​Var z);;
 +</​code>​
 +
 +== Pretty-printing functions ==
 +
 +<code ocaml>
 +# let rec string_of_term t = match t with
 +    Var x -> x
 +  | Abs (x,t') -> "​\\"​ ^ x ^ "​."​ ^ string_of_term t'
 +  | App (t0,t1) -> "​("​ ^ (string_of_term t0) ^ " " ^ (string_of_term t1) ^ "​)";;​
 +</​code>​
 +
 +<code ocaml>
 +# print_string (string_of_term id);;
 +# print_string (string_of_term k);;
 +# print_string (string_of_term omega);;
 +</​code>​
 +
 +\\
 +
 +
 +===== Free variables and substitutions =====
 +
 +== Sets ==
 +
 +<code ocaml>
 +# type 'a set = Set of 'a list;;
 +
 +# let emptyset = Set [];;
 +
 +# let rec member x s = match s with
 +    Set [] -> false
 +  | Set (y::​s'​) -> x=y or (member x (Set s'));;
 +
 +# let rec union s t = match s with
 +    Set [] -> t
 +  | Set (x::​s'​) -> (match union (Set s') t with Set t' ->
 +      if member x t then Set t' else Set (x::​t'​));;​
 +
 +# let rec diff s x = match s with
 +    Set [] -> s
 +  | Set (y::​s'​) -> (match diff (Set s') x with Set t' ->
 +      if x=y then Set s' else Set (y::​t'​));;​
 +</​code>​
 +
 +== Free variables ==
 +
 +<code ocaml>
 +# let rec fv t = match t with
 +    Var x -> Set [x]
 +  | App(t0,t1) -> union (fv t0) (fv t1)
 +  | Abs(x,t0) -> diff (fv t0) x;;
 +</​code>​
 +
 +<code ocaml>
 +# fv omega;;
 +# fv (const "​z"​);;​
 +# fv (Abs ("​x",​ App(Var "​x",​Var "​y"​)));;​
 +</​code>​
 +
 +== Substitutions ==
 +
 +<code ocaml>
 +# let count = ref(-1);;
 +# let gensym = fun () -> count := !count +1; "​x"​ ^ string_of_int (!count);;
 +
 +# let rec subst x t' t = match t with
 +    Var y -> if x=y then t' else Var y
 +  | App(t0,t1) -> App(subst x t' t0, subst x t' t1)
 +  | Abs(y,t0) when y=x -> Abs(x,t0)
 +  | Abs(y,t0) when y!=x && not (member y (fv t')) -> Abs(y, subst x t' t0)
 +  | Abs(y,t0) when y!=x && member y (fv t') -> 
 +      let z = gensym() in Abs(z,subst x t' (subst z (Var y) t0));;
 +</​code>​
 +
 +\\
 +
 +
 +===== Leftmost-outermost reduction =====
 +
 +<code ocaml>
 +# let isredex t = match t with 
 +    App(Abs(x,​t0),​t1) -> true
 +  | _ -> false;;
 +
 +# let rec hasredex t = match t with 
 +    Var x -> false
 +  | Abs(x,​t'​) -> hasredex t'
 +  | App(t0,t1) -> isredex t or hasredex t0 or hasredex t1;;
 +
 +# exception Error;;
 +
 +# let rec reduce1 t = if not (hasredex t) then t else match t with
 +    Abs(x,​t'​) -> Abs(x,​reduce1 t')
 +  | App(Abs(x,​t0),​t1) -> subst x t1 t0 
 +  | App(t0,t1) -> if hasredex t0 then App(reduce1 t0,t1) else App(t0,​reduce1 t1);;
 +
 +# let rec reduce t k = if k=0 then t else let t' = reduce1 t in reduce t' (k-1);;
 +
 +# let rec reducefix t = let t' = reduce1 t in if t'=t then t' else reducefix t';;
 +
 +# reduce (App((const "​z"​),​omega)) 1;;
 +</​code>​
 +
 +\\
  
untypedlambda.txt · Last modified: 2015/10/08 15:20 (external edit)