diff --git a/lambda/lambda.ml b/lambda/lambda.ml index ac9063d..e00291d 100644 --- a/lambda/lambda.ml +++ b/lambda/lambda.ml @@ -29,6 +29,25 @@ let rec beta = function | App (Lambda (x, t), u) -> subst t [(x, u)] | _ -> failwith "This term is not a redex" +(* return i where i is the smallest suffix needed so that "x ^ i" isn't in l *) +let rec var_counter i x l = + if List.mem (x ^ (string_of_int i)) l then var_counter (i+1) x l + else i + +(* Alpha Conversion : renames lambda variables duplicates by adding a number to them*) +let alpha_conv t = + let rec aux l = function + | Var x when List.mem x l -> + let i = string_of_int ( (var_counter 0 x l) - 1) in + if i = "-1" then Var x + else Var (x^i) + | Var x -> Var x + | Lambda(x, t) when List.mem x l -> + let i = string_of_int (var_counter 0 x l) in + Lambda (x^i, aux ((x^i)::l) t) + | Lambda(x, t) -> Lambda (x, aux (x::l) t) + | App (t, u) -> App (aux l t, aux l u) + in aux [] t (* --------------------------------------- Exemples --------------------------------------- *) @@ -145,3 +164,5 @@ let rec cbn = function let rec cbn_eval t = try let t' = cbv t in cbn_eval t' with Irreductible -> t + + diff --git a/lambda/main.ml b/lambda/main.ml index 9aa36bc..07833c8 100644 --- a/lambda/main.ml +++ b/lambda/main.ml @@ -49,6 +49,12 @@ let _ = let t = termc Lexer.read lexbuf in print_endline (string_of_term t) with _ -> print_endline "Syntax error. Please try again.") + | "alpha"::string_list -> + let lexbuf = Lexing.from_string (String.concat " " string_list) in + (try + let t = termc Lexer.read lexbuf in + print_endline (string_of_term (alpha_conv t)) + with _ -> print_endline "Syntax error. Please try again.") | ["cbn"; "-f"; filename] -> begin try let lexbuf = Lexing.from_channel (open_in filename) in diff --git a/lambda/tab1.png b/lambda/tab1.png new file mode 100644 index 0000000..91c2e8e Binary files /dev/null and b/lambda/tab1.png differ diff --git a/lambda/tab2.png b/lambda/tab2.png new file mode 100644 index 0000000..4e2e72b Binary files /dev/null and b/lambda/tab2.png differ