diff --git a/lambda.ml b/lambda.ml index 72a028b..8f59141 100644 --- a/lambda.ml +++ b/lambda.ml @@ -1,17 +1,20 @@ +(*Terme du Lambda-Calcul*) type term = | Var of string | Lambda of string * term | App of term * term - +(*Applique une substitution de x par sub à un terme t*) let rec apply x sub = function | Var (y) -> if y = x then sub else Var (y) | Lambda (y,t) -> Lambda (y, apply x sub t) | App (t1, t2) -> App (apply x sub t1, apply x sub t2) +(*Applique une liste de substition à un terme*) let rec subst t sub_list = List.fold_left (fun t (x, sub) -> apply x sub t) t sub_list +(* Applique la beta réduction, qui transforme (lambda x. t)u en t[x:=u] *) let rec beta = function | App (Lambda (x, t), u) -> subst t [(x, u)] | _ -> failwith "This term is not a redex" @@ -74,39 +77,48 @@ let rec string_of_term = function --------------------------------------- *) exception Irreductible - +(* Vérifie si un terme est une valeur, c'est à dire qu'on ne peut plus le réduire *) let is_value = function | Lambda (_, _) -> true | Var _ -> true | _ -> false +(* Réduit d'un pas les termes par l'extérieur puis l'intérieur *) let rec lo_reduction = function | App ( Lambda (x, t), u) as redex -> (beta redex) | App (Var x, (_ as t)) -> App (Var x, lo_reduction t) | App (App (_,_) as t, Var x) -> App (lo_reduction t, Var x) - | App (t, u) -> (App (lo_reduction t, lo_reduction u)) + | App (App (_,_) as t, (_ as u)) -> App (lo_reduction t, u) + (*| App (t, u) -> (App (lo_reduction t, lo_reduction u))*) | Lambda (x, t) -> Lambda (x, lo_reduction t) | _ -> raise Irreductible - +(* Boucle sur la lo_reduction pour appliquer cette stratégie de réduction jusqu'à la fin *) let rec lo_eval t = try let t' = lo_reduction t in lo_eval t' with Irreductible -> t - -let (*cbv*) cbv = function +(* Réduit d'un pas les termes en commençant par l'argument puis réduit les fonctions *) +let rec cbv = function | App ( Lambda (x, t), v) as redex when is_value v -> (*cbv*) (beta redex) - | App (t, u) -> (App (t, (*cbv*) u)) - | Lambda (x, t) as l -> l - | Var x -> Var x + | App (t, u) when is_value u -> (App (cbv t, u)) + | App (t, u) -> (App (t, cbv u)) + | Lambda (x, t) -> raise Irreductible + | Var x -> raise Irreductible -let rec cbv_loop t = - let t' = cbv t in - if t' = t then t' - else cbv_loop t' +(* Boucle sur call_by_value pour appliquer cette stratégie de réduction jusqu'à la fin *) +let rec cbv_eval t = + try let t' = cbv t in + cbv_eval t' with Irreductible -> t +(* Réduit d'un pas les termes en commençant par la fonction puis passe à l'argument*) let rec cbn = function - | App ( Lambda (x, t), v) as redex -> cbn (beta redex) - | App (t, u) -> cbn (App (cbn t, u)) - | Lambda (x, t) -> Lambda (x, t) - | Var x -> Var x \ No newline at end of file + | App ( Lambda (x, t), v) as redex -> beta redex + | App (t, u) -> (App (cbn t, u)) + | Lambda (x, t) -> raise Irreductible + | Var x -> raise Irreductible + +(* Boucle sur call_by_name pour appliquer cette stratégie de réduction jusqu'à la fin *) +let rec cbn_eval t = + try let t' = cbv t in + cbn_eval t' with Irreductible -> t