Commit 130e9597 authored by Samuel Frontull's avatar Samuel Frontull
Browse files

Merge branch 'master' into 'main'

Master

See merge request !3
parents a69eda6a d352cbd8
open Wltrs
(* ((/x.x x) (/y z.y z)) ((/x.x x) (/y z.y z)) *)
let str_to_term s = Grammar.input Lexer.token (Lexing.from_string s)
let () =
......@@ -7,7 +9,6 @@ let () =
failwith "Usage: dune exec bin/main.exe term_str"
else
let term =
try str_to_term (Sys.argv.(1) ^ "\n")
with _ -> failwith "Syntax error"
try str_to_term (Sys.argv.(1) ^ "\n") with _ -> failwith "Syntax error"
in
Core.reduction_print term
......@@ -13,36 +13,92 @@ let rec _term_to_string term =
| _, Var _ -> "(" ^ _term_to_string e1 ^ ") " ^ _term_to_string e2
| _, _ -> "(" ^ _term_to_string e1 ^ ") (" ^ _term_to_string e2 ^ ")" )
let label = ref 0
let next_label () =
label := !label + 1;
"C" ^ string_of_int !label
type l_term =
| LVar of string
| LLam of string * l_term list * string * l_term
| LApp of l_term * l_term
let rec l_term_to_term = function
| LVar v -> Var v
| LLam (_, _, v, t) -> Lam (v, l_term_to_term t)
| LApp (e1, e2) -> App (l_term_to_term e1, l_term_to_term e2)
let rec _l_term_to_string term c =
match term with
| LVar v -> v
| LLam (l, fvs, v, t) ->
"λ" ^ v ^ "_" ^ l ^ "["
^ String.concat " " (L.map (fun k -> _l_term_to_string k 0) fvs)
^ "]."
^ _l_term_to_string t (c + 1)
| LApp (e1, e2) -> (
match (e1, e2) with
| LVar _, LVar _ -> _l_term_to_string e1 c ^ " " ^ _l_term_to_string e2 c
| LVar _, _ ->
_l_term_to_string e1 c ^ " (" ^ _l_term_to_string e2 c ^ ")"
| _, LVar _ ->
"(" ^ _l_term_to_string e1 c ^ ") " ^ _l_term_to_string e2 c
| _, _ ->
"(" ^ _l_term_to_string e1 c ^ ") (" ^ _l_term_to_string e2 c ^ ")" )
(* _term_to_string (l_term_to_term term) *)
let l_term_to_string term = _l_term_to_string term 0
(** Extract the name of a variable from a {e a_term} *)
let vname = function Var n -> n | _ -> ""
let remove l1 f x =
L.fold_left (fun acc hd -> if f hd = x then acc else hd :: acc) [] l1
let rec fvars = function
| Var x -> [ Var x ]
| Lam (x, e) -> remove (fvars e) vname x
| App (e1, e2) -> fvars e1 @ fvars e2
(* lift : term -> TRS *)
let rec term_to_l_term term =
match term with
| Var x -> LVar x
| Lam (x, e) ->
let l = next_label () in
let fvs = L.map term_to_l_term (fvars term) in
LLam (l, fvs, x, term_to_l_term e)
| App (e1, e2) -> LApp (term_to_l_term e1, term_to_l_term e2)
let rec rename_fv term x y =
match term with
| Var s -> if s = x then Var y else term
| Lam (s, t) ->
if s = x then term else Lam (s, rename_fv t x y)
| App (e1, e2) ->
App (rename_fv e1 x y, rename_fv e2 x y)
| LVar s -> if s = x then LVar y else term
| LLam (l, fvs, s, t) ->
let fvs' = L.map (fun t -> rename_fv t x y) fvs in
if s = x then term else LLam (l, fvs', s, rename_fv t x y)
| LApp (e1, e2) -> LApp (rename_fv e1 x y, rename_fv e2 x y)
let rec default_names_r term pos =
match term with
| Var v -> Var v
| Lam (v, t) ->
| LVar v -> LVar v
| LLam (l, fvs, v, t) ->
let vf = "x_" ^ pos in
Lam (vf, default_names_r (rename_fv t v vf) (pos ^ "0"))
| App (e1, e2) ->
App (default_names_r e1 (pos ^ "0"), default_names_r e2 (pos ^ "1"))
LLam (l, fvs, vf, default_names_r (rename_fv t v vf) (pos ^ "0"))
| LApp (e1, e2) ->
LApp (default_names_r e1 (pos ^ "0"), default_names_r e2 (pos ^ "1"))
let default_names term = default_names_r term "e"
let remove l1 f x =
L.fold_left (fun acc hd -> if f hd = x then acc else hd :: acc) [] l1
(** Extract the name of a variable from a {e a_term} *)
let vname = function Var n -> n | _ -> ""
let lvname = function LVar n -> n | _ -> ""
(** Extract the free variables in a {e a_term} *)
let rec free_variables = function
| Var x -> [ Var x ]
| Lam (x, e) -> remove (free_variables e) vname x
| App (e1, e2) -> free_variables e1 @ free_variables e2
| LVar x -> [ LVar x ]
| LLam (_, _, x, e) -> remove (free_variables e) lvname x
| LApp (e1, e2) -> free_variables e1 @ free_variables e2
let counter = ref 0
......@@ -53,39 +109,46 @@ let next_fresh () =
(** replace every var occurrence by fresh var *)
let rec subst m x y =
match m with
| Var z -> if z = x then Var y else m
| Lam (z, e) ->
| LVar z -> if z = x then LVar y else m
| LLam (l, fvs, z, e) ->
let z' = if z = x then y else z in
Lam (z', subst e x y)
| App (e1, e2) -> App (subst e1 x y, subst e2 x y)
let fvs' = L.map (fun t -> subst t x y) fvs in
LLam (l, fvs', z', subst e x y)
| LApp (e1, e2) -> LApp (subst e1 x y, subst e2 x y)
(** capture-avoiding substitution *)
let rec _casubst m x n fvn =
match m with
| Var y -> if x = y then n else m
| Lam (y, e) ->
| LVar y -> if x = y then n else m
| LLam (l, fvs, y, e) -> (
if y = x then m
else if L.mem y fvn && L.mem x (L.map vname (free_variables e)) then
(* rename x to fresh *)
let f = next_fresh () in
let m' = subst m y f in
_casubst m' x n fvn
else Lam (y, _casubst e x n fvn)
| App (e1, e2) -> App (_casubst e1 x n fvn, _casubst e2 x n fvn)
let casubst m x n = _casubst m x n (L.map vname (free_variables n))
else
(* get intersection of fvn and fvs variable names *)
let fvs_vars = L.map lvname (L.flatten (L.map free_variables fvs)) in
let inters = List.filter (fun x -> List.mem x (y :: fvs_vars)) fvn in
match inters with
| [] ->
LLam
(l, L.map (fun z -> _casubst z x n fvn) fvs, y, _casubst e x n fvn)
| hd :: _ ->
let f = next_fresh () in
let m' = subst m hd f in
_casubst m' x n fvn )
| LApp (e1, e2) -> LApp (_casubst e1 x n fvn, _casubst e2 x n fvn)
let casubst m x n = _casubst m x n (L.map lvname (free_variables n))
let beta term =
match term with
| App (Lam (x, m), n) ->
| LApp (LLam (_, _, x, m), n) ->
let res = casubst m x n in
res
| _ -> failwith "beta: Not a redex."
let rec _weak_redexpos term pos =
match term with
| App (Lam (_, _), _) -> pos
| App (e1, e2) ->
| LApp (LLam (_, _, _, _), _) -> pos
| LApp (e1, e2) ->
let posl = _weak_redexpos e1 (pos ^ "1") in
if posl != "" then posl else _weak_redexpos e2 (pos ^ "2")
| _ -> ""
......@@ -94,40 +157,14 @@ let weak_redexpos term = _weak_redexpos term ""
let rec _weak_step term pos p =
match term with
| App (Lam (_, _), _) -> if p = pos then beta term else term
| App (e1, e2) ->
App (_weak_step e1 pos (p ^ "1"), _weak_step e2 pos (p ^ "2"))
| LApp (LLam (_, _, _, _), _) -> if p = pos then beta term else term
| LApp (e1, e2) ->
LApp (_weak_step e1 pos (p ^ "1"), _weak_step e2 pos (p ^ "2"))
| _ -> term
let weak_step term = _weak_step term (weak_redexpos term) ""
let label = ref 0
let next_label () =
label := !label + 1;
"C" ^ string_of_int !label
type l_term =
| LVar of string
| LLam of string * l_term list * string * l_term
| LApp of l_term * l_term
let rec l_term_to_term = function
| LVar v -> Var v
| LLam (_, _, v, t) -> Lam (v, l_term_to_term t)
| LApp (e1, e2) -> App (l_term_to_term e1, l_term_to_term e2)
let l_term_to_string term = _term_to_string (l_term_to_term term)
(* lift : term -> TRS *)
let rec label term =
match term with
| Var x -> LVar x
| Lam (x, e) ->
let l = next_label () in
let fvs = L.map label (free_variables term) in
LLam (l, fvs, x, label e)
| App (e1, e2) -> LApp (label e1, label e2)
let weak_step_pos term pos = _weak_step term pos ""
type trs_term =
| TVar of string
......@@ -147,17 +184,11 @@ let rec trs_term_to_string term =
let term_print term = Printf.printf "%s" (trs_term_to_string term)
let rec lterm_to_trsterm lterm =
let rec l_term_to_trsterm lterm =
match lterm with
| LVar x -> TVar x
| LLam (l, fvs, _, _) -> TCon (l, L.map lterm_to_trsterm fvs)
| LApp (e1, e2) -> TDes (lterm_to_trsterm e1, lterm_to_trsterm e2)
let rec lterm_to_term lterm =
match lterm with
| LVar x -> Var x
| LLam (_, _, x, t) -> Lam (x, lterm_to_term t)
| LApp (e1, e2) -> App (lterm_to_term e1, lterm_to_term e2)
| LLam (l, fvs, _, _) -> TCon (l, L.map l_term_to_trsterm fvs)
| LApp (e1, e2) -> TDes (l_term_to_trsterm e1, l_term_to_trsterm e2)
type trs_rule = RR of trs_term * trs_term
......@@ -169,26 +200,23 @@ let rec rules lterm =
match lterm with
| LVar _ -> []
| LLam (_, _, x, e) ->
RR (TDes (lterm_to_trsterm lterm, TVar x), lterm_to_trsterm e) :: rules e
RR (TDes (l_term_to_trsterm lterm, TVar x), l_term_to_trsterm e)
:: rules e
| LApp (e1, e2) -> rules e1 @ rules e2
let rules_to_string xs = String.concat ".\n" (L.map trs_rule_to_string xs)
type trs = TRS of trs_rule list * trs_term
let trs_to_string = function
| TRS (xs, t) ->
"Rules:\n" ^ rules_to_string xs ^ ".\n\nTerm:\n" ^ trs_term_to_string t
let trs_rules = function TRS (xs, _) -> xs
let trs_term = function TRS (_, t) -> t
let term_to_trs x =
let lx = label x in
TRS (rules lx, lterm_to_trsterm lx)
let lx = term_to_l_term x in
TRS (rules lx, l_term_to_trsterm lx)
let term_trs_print term = Printf.printf "%s" (trs_to_string (term_to_trs term))
let l_term_to_trs x = TRS (rules x, l_term_to_trsterm x)
let rec _redexpos trsterm pos =
match trsterm with
......@@ -200,13 +228,14 @@ let rec _redexpos trsterm pos =
let redexpos trsterm = _redexpos trsterm ""
let rec search_pairs v = function
| (x, n) :: xs -> if vtname v = vtname x then n else search_pairs v xs
let rec search_pairs v f = function
| (x, n) :: xs -> if f v = f x then n else search_pairs v f xs
| [] -> v
let rec subst m pairs =
(* Printf.printf "subst\n"; *)
match m with
| TVar _ -> search_pairs m pairs
| TVar _ -> search_pairs m vtname pairs
| TCon (l, fvs) -> TCon (l, L.map (fun z -> subst z pairs) fvs)
| TDes (e1, e2) -> TDes (subst e1 pairs, subst e2 pairs)
......@@ -229,15 +258,31 @@ let rec _rstep trsterm trsrules pos p =
let rstep trs =
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs (redexpos t) "")
let rstep_pos trs pos =
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs pos "")
let rec all_vars vs =
match vs with TVar _ :: xs -> all_vars xs | _ :: _ -> false | [] -> true
(* project : TRS -> term *)
let rec trs_rule trsrules label =
(* Printf.printf "---\ntrs_rule %s\n" label;
Printf.printf "trs_rules:\n %s\n---\n"
(String.concat "\n" (L.map trs_rule_to_string trsrules)); *)
match trsrules with
| RR (TDes (TCon (l, _ ), _), _) :: xs ->
if l = label then L.hd trsrules else trs_rule xs label
| RR (TDes (TCon (l, fvs), _), _) :: xs ->
if l = label && all_vars fvs then L.hd trsrules else trs_rule xs label
| _ :: xs -> trs_rule xs label
| [] -> failwith "No rule with such label."
let counter_projection = ref 0
let next_fresh_2 () =
counter_projection := !counter_projection + 1;
"v" ^ string_of_int !counter_projection
let rec trs_to_term trs =
(* Printf.printf "trs_to_term\n"; *)
match trs with
| TRS (xs, t) -> (
match t with
......@@ -246,25 +291,32 @@ let rec trs_to_term trs =
LApp (trs_to_term (TRS (xs, e1)), trs_to_term (TRS (xs, e2)))
| TCon (label, fvs) -> (
let rr = trs_rule xs label in
(* Printf.printf "trs_rule rr:%s\n" (trs_rule_to_string rr);
Printf.printf "mapping term:%s\n" (trs_term_to_string t); *)
match rr with
| RR (TDes (TCon (_, fvs_r), var), r) ->
LLam
( label,
L.map trs_to_term (L.map (fun st -> TRS (xs, st)) fvs),
vtname var,
trs_to_term (TRS (xs, subst r (L.combine fvs_r fvs))) )
if L.mem var fvs then
let fresh = next_fresh_2 () in
let rfresh = subst r [ (var, TVar fresh) ] in
LLam
( label,
L.map trs_to_term (L.map (fun st -> TRS (xs, st)) fvs),
fresh,
trs_to_term (TRS (xs, subst rfresh (L.combine fvs_r fvs)))
)
else
LLam
( label,
L.map trs_to_term (L.map (fun st -> TRS (xs, st)) fvs),
vtname var,
trs_to_term (TRS (xs, subst r (L.combine fvs_r fvs))) )
| _ -> failwith "Not a RR found." ) )
let trs_print trs =
Printf.printf "%s\n===========================\n%s\n" (trs_to_string trs)
(l_term_to_string (trs_to_term trs))
let lift_project_print term =
let trs = term_to_trs term in
Printf.printf
"%s\n\n--------[lift]--------\n\n%s\n\n-------[project]-------\n\n%s\n"
(_term_to_string term) (trs_to_string trs)
(l_term_to_string (trs_to_term trs))
let trs_to_string trs =
(* Printf.printf "%s\n" (trs_term_to_string (trs_term trs)); *)
match trs with
| TRS (xs, t) ->
"Rules:\n" ^ rules_to_string xs ^ ".\n\nTerm:\n" ^ trs_term_to_string t
let rec _weak_reduction term =
let wt = weak_step term in
......@@ -278,60 +330,66 @@ let rec _trs_reduction trs =
let trs_reduction trs = trs :: _trs_reduction trs
let prepend_index xs = L.mapi (fun i x -> "[" ^ string_of_int i ^ "] " ^ x) xs
let reduction_print term =
let trs = term_to_trs term in
let weak_reductions = weak_reduction term in
let l_term = term_to_l_term term in
let trs = l_term_to_trs l_term in
let weak_reductions = weak_reduction l_term in
let trs_reductions = trs_reduction trs in
let trs_reductions_t = L.map trs_term trs_reductions in
let bisim = L.combine weak_reductions trs_reductions in
let trs_str =
match trs with
| TRS (xs, _) ->
"Rules:\n" ^ rules_to_string xs ^ ".\n\nReductions:\n"
^ String.concat "\n" (L.map trs_term_to_string trs_reductions_t)
| TRS (xs, t) ->
"Rules:\n" ^ rules_to_string xs ^ ".\n\nTerm:\n" ^ trs_term_to_string t
in
Printf.printf
"\n\
------[Lambda Calculus]------\n\n\
%s\n\n\
----------[TRS]----------\n\n\
-------[TRS]----------------\n\n\
%s\n\n\
-------[Reductions]---------\n\n\
LC:\n\
\ %s\n\n\
TRS:\n\
\ %s\n\n\
-------[Bisimulation]-------\n\n\
%s\n"
(String.concat "\n" (L.map _term_to_string weak_reductions))
(l_term_to_string (trs_to_term trs))
trs_str
(String.concat " ->\n "
(prepend_index
(L.map _term_to_string (L.map l_term_to_term weak_reductions))))
(String.concat " ->\n "
(prepend_index (L.map trs_term_to_string trs_reductions_t)))
(String.concat "\n"
(L.map
(fun (a, b) ->
let b_ts = trs_term_to_string (trs_term b) in
let b_t = l_term_to_term (trs_to_term b) in
(if default_names a = default_names b_t then "(v)" else "(X)")
^ " " ^ (_term_to_string a) ^ " ~ " ^ b_ts ^ " ≡ " ^ (_term_to_string b_t))
(L.mapi
(fun i (a_term, b_trs) ->
let a_term_default = a_term in
let a_term_trs = l_term_to_trs a_term_default in
let b_trs_term = trs_to_term b_trs in
(* let b_term_trs = l_term_to_trs b_trs_term in *)
let s =
if
l_term_to_string (default_names a_term)
= l_term_to_string (default_names b_trs_term)
&& trs_term a_term_trs = trs_term b_trs
then
"\n---------------------\n" ^ "TRS_" ^ string_of_int i ^ " ~ "
^ "LC_" ^ string_of_int i ^ "\n---------------------\n"
else
"\n---------------------\n" ^ "! TRS_" ^ string_of_int i
^ " ≁ " ^ "LC_" ^ string_of_int i
^ "\n---------------------\n"
in
s
^ l_term_to_string a_term_default
^ "\n\n" ^ trs_to_string a_term_trs
^ "\n\n++++++++++++++++++++++\n\n" ^ trs_to_string b_trs ^ "\n\n"
^ l_term_to_string b_trs_term
^ "\n\n"
(* ^ trs_to_string b_term_trs ^ "\n\n" *)
^ "=====================\n")
(* "LC_" ^ string_of_int i ^ " ~ " ^ "TRS_" ^ string_of_int i *)
bisim))
let example = App (Lam ("x", Var "y"), Var "z")
let example2 =
App
( Lam ("x", App (Var "x", Var "x")),
Lam ("y", Lam ("z", App (Var "y", Var "z"))) )
let example3 =
App
( Lam ("x", App (App (Var "x", Var "x"), Var "x")),
Lam ("y", Lam ("z", App (Var "y", Var "z"))) )
let example4 =
App
( Lam ("x", App (App (Var "x", Var "x"), Var "x")),
Lam ("y", Lam ("z", App (Var "y", Var "z"))) )
let trs = term_to_trs example
let trs2 = term_to_trs example2
let trs3 = term_to_trs example3
(* let () = reduction_print example3 *)
(* lift_project_print example3 *)
(library
(name wltrs)
(public_name wltrs))
(name wltrs)
(public_name wltrs))
(ocamllex lexer)
......
......@@ -11,7 +11,7 @@ rule token = parse
['\t'] { token lexbuf } (* skip blanks *)
| ['\n' ] { EOF }
| ' ' { BLANK }
| '/' { LAM }
| '\\' { LAM }
| '(' { LPAREN }
| ')' { RPAREN }
| '.' { DOT }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment