diff --git a/lambda.ml b/lambda.ml index 8f59141..43221ca 100644 --- a/lambda.ml +++ b/lambda.ml @@ -82,8 +82,21 @@ let is_value = function | Lambda (_, _) -> true | Var _ -> true | _ -> false + +(* Vérifie si un lambda est linéaire, i.e. qu'il n'y a qu'une seule occurence de son paramètre *) + +let rec count_freevars x = function + | Lambda (y, t) -> count_freevars x t + | App (t, u) -> (count_freevars x t) + (count_freevars x u) + | Var y -> if x = y then 1 else 0 + + let rec is_linear = function + | Lambda (x, t) -> (count_freevars x t) = 1 && is_linear t + | App(t, u) -> is_linear t && is_linear u + | Var x -> true -(* Réduit d'un pas les termes par l'extérieur puis l'intérieur *) +(* 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)