Working lo_reduction, cbv and cbn

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
+  | 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