engboris
/
large-star-collider
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

working parser but app must be used with (), working notation of \x y. for \x. \y.

master
julia 2 years ago
parent
ae34fa688d
commit
31c9a45265
4 changed files with 7 additions and 153 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 137
      lambda.ml
  2. 5
      lambda/lambda.ml
  3. 2
      lambda/lexer.mll
  4. 16
      lambda/parser.mly

137
lambda.ml
Unescape View File

@ -1,137 +0,0 @@
(*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"
(* ---------------------------------------
Exemples
--------------------------------------- *)
let x = Var "x";;
let y = Var "y";;
let a = Var "a" ;;
let b = Var "b" ;;
let i = Lambda ("x", x);;
(*(λx. x x) a — duplication*)
let n1 = App (Lambda ("x", App (x, x)), a);;
(*(λx. x x) (λa. a) — passage de fonction / ordre supérieur*)
let n2 = App (Lambda ("x", App (x, x)), Lambda (("a"), a));;
(*(λx. x (λx.x)) y — variable libres/liées*)
let n3 = App (Lambda ("x", App (x, Lambda ("x", x) ) ), y) ;;
(*(λx. x (λy. x y)) y — capture de variable*)
let n4 = App (Lambda ("x", App(x, Lambda ("y", App (x, y)))), y);;
(*(λxy. x) a b — fonction à deux entrées et effacement*)
let n5 = App ( App ( Lambda ("x", ( Lambda ("y", x))), a), b);;
(*(λxy. x) a — application partielle pour deux entrées*)
let n6 = App ( Lambda ("x", ( Lambda ("y", x))), a);;
(*(λxy. x) I a b — sur application pour deux entrées*)
let n7 = App (App ( App (Lambda ("x", ( Lambda ("y", x))), i), a), b);;
(*(λx. x x) (I I) — duplication inutile dans une stratégie*)
let n8 = App ( Lambda ("x", App (x, x)), App ( i, i));;
(*(λxy. y) (I I) I — différence de complexité selon la stratégie*)
let n9 = App ( App (Lambda ("x", ( Lambda ("y", y))), App (i, i)), i);;
(* ---------------------------------------
Display
--------------------------------------- *)
let rec string_of_list printer sep = function
| [] -> ""
| [x] -> printer x
| h::t ->
(printer h) ^ sep ^ (string_of_list printer sep t)
let rec string_of_term = function
| Var x -> x
| Lambda (x, Lambda (y, t)) -> "λ" ^ x ^ y ^ ". " ^ string_of_term t ^ ""
| Lambda (x, t) -> "λ" ^ x ^ ". " ^ string_of_term t ^ ""
| App (Var x, Var y) -> x ^ " " ^ y
| App (t, Var x) -> "(" ^ string_of_term t ^ ") " ^ x
| App ( App ( t, u), v) -> "(" ^ string_of_term (App (t, u)) ^ ") " ^ string_of_term v
| App ( u, App ( t, v)) -> string_of_term u ^ " (" ^ string_of_term (App (t, v)) ^ ")"
| App ( Lambda (x, App (t, y)), v) -> "(" ^ string_of_term (Lambda (x, App (t, y))) ^ ") " ^ string_of_term v
| App ( Lambda (x, t), u) -> string_of_term (Lambda (x,t)) ^ " (" ^ string_of_term u ^")"
| App (t, u) -> string_of_term t ^ " (" ^ string_of_term u ^ ")"
(* ---------------------------------------
Réduction
--------------------------------------- *)
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
(* 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 *)
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 (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
(* 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) when is_value u -> (App (cbv t, u))
| App (t, u) -> (App (t, cbv u))
| Lambda (x, t) -> raise Irreductible
| Var x -> raise Irreductible
(* 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 -> 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

5
lambda/lambda.ml
Unescape View File

@ -7,7 +7,10 @@ type term =
let to_var x = Var x
let to_lambda x t = Lambda (x, t)
let rec to_lambda l t =
match l with
| h::tail -> Lambda (h, to_lambda tail t)
| [] -> t
let to_app t u = App (t, u)

2
lambda/lexer.mll
Unescape View File

@ -13,6 +13,6 @@ rule read = parse
| ')' { RIGHT_PAR }
| '.' { DOT }
| '\\' { LAMBDA }
| space { SPACE }
| space { read lexbuf }
| newline { read lexbuf }
| eof { exit 0 }

16
lambda/parser.mly
Unescape View File

@ -2,24 +2,12 @@
%token <string> VAR
%token DOT
%token LAMBDA
%token SPACE
%left SPACE
%token END
%start <Lambda.term> termc
%%
(*
mainc:
| t = termc END { t }*)
termc:
| x = VAR { Lambda.to_var x }
| LAMBDA ; x = VAR ; DOT; SPACE; t = termc { Lambda.to_lambda x t }
| LEFT_PAR ; t = termc ; SPACE ; u = termc ; RIGHT_PAR { Lambda.to_app t u }
| LAMBDA ; l = nonempty_list(VAR) ; DOT; t = termc { Lambda.to_lambda l t }
| LEFT_PAR ; t = termc ; u = termc ; RIGHT_PAR { Lambda.to_app t u }
| LEFT_PAR ; t = termc ; RIGHT_PAR { t }
(*| tu = separated_pair (termc, SPACE, termc) {let (t, u) = tu in Lambda.to_app t u }*)
(* %inline sp:
| SPACE { ( ) } *)
Write Preview
Loading…
Cancel
Save