From 1df7aa3bfc6fbd40fb4ddb7f1649a30e364f83f3 Mon Sep 17 00:00:00 2001
From: julia <juliavonkreutzer@protonmail.com>
Date: Wed, 31 May 2023 15:21:27 +0200
Subject: [PATCH] Working lo_reduction, cbv and cbn
---
lambda.ml | 46 +++++++++++++++++++++++++++++-----------------
1 file changed, 29 insertions(+), 17 deletions(-)
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