1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
| (* Définir le type expression du lambda calcul : exp *)
type expr = Var of char
| Abs of char * expr
| App of expr * expr
(* Définir FreeVar *)
let freevar var exp =
let rec freevarIter var = function
Var x -> true
|App (u,v) -> (freevarIter var u) || (freevarIter var v)
|Abs (x,u) when x = var -> false
|Abs (x,u) when x !=var -> freevarIter var u
in freevarIter var exp;;
let x = Var 'x';;
let t = Var 't';;
let y = Var 'y';;
let z = Var 'z';;
let v = Var 'v';;
(* expressions du jeu d'essais *)
let exp0 = App(Abs('x',App(x,t)),v);;
let exp1 = App(Abs('x',App(Abs('y',App(y,x)),z)),v);;
let exp2 = Abs('x',App(x,x));;
let exp3 = App(Abs('x',t),App(exp2,exp2));;
(* definir substitution valide , manque la gestion du problème de capture*)
let rec subst (var:char) (n:expr) (exp:expr) = match exp with
Var x when x = var -> n
| Var y -> exp
| App (u,v) -> App((subst var n u),(subst var n v))
| Abs (x,u) when x = var -> Abs(x,u)
| Abs (y,u) -> Abs(y,subst var n u)
(* definir red_name, renvoie FN si existe avec un appel par nom *)
let rec red_name exp=match exp with
Var x -> exp
| Abs(y,u) -> Abs(y,red_name u)
| App(Abs(z,v),w) -> red_name (subst z w v)
| App(a,b) -> App(red_name a,red_name b);;
(* definir red_value , renvoie FN si existe avec un appel par valeur*)
let rec red_value exp=match exp with
Var x -> exp
| Abs(y,u) -> Abs(y,red_value u)
| App(Abs(z,v),w) -> red_value (subst z (red_value w) v)
| App(a,b) -> App(red_value a,red_value b);; |
Partager