Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* ========================================================================= *) (* Untyped lambda calculus. *) (* *) (* Freek Wiedijk, University of Nijmegen *) (* ========================================================================= *) open List;; let id x = x;; let ( ** ) f g x = f (g x);; let rec index s l = match l with [] -> raise Not_found | t::k -> if s = t then 0 else (index s k) + 1;; (* ------------------------------------------------------------------------- *) (* Type of lambda terms. *) (* ------------------------------------------------------------------------- *) type term = Const of string | App of term * term | Abstr of string * term | Var of int;; (* ------------------------------------------------------------------------- *) (* Reading lambda terms. *) (* ------------------------------------------------------------------------- *) let explode s = let rec explode1 n = try let s1 = String.make 1 s.[n] in s1::(explode1 (n + 1)) with Invalid_argument _ -> [] in explode1 0;; let implode l = fold_right (^) l "";; let lex l = let rec lex1 l = match l with [] -> [] | c::k -> if mem c [" "; "\t"; "\n"] then lex1 k else if mem c ["^"; "."; "("; ")"] then c::(lex1 k) else if c = "'" then failwith "lex" else lex2 [c] k and lex2 v l = match l with [] -> [implode v] | c::k -> if c = "'" then lex2 (v@[c]) k else (implode v)::(lex1 l) in lex1 l;; let parse l = let rec apps l = match l with [] -> failwith "parse" | [t] -> t | t::u::v -> apps (App(t,u)::v) in let rec parse1 c l = let t,k = parse2 c l in (apps t),k and parse2 c l = match l with [] -> [],[] | "^"::k -> let t,j = parse3 c k in [t],j | "."::_ -> failwith "parse" | "("::k -> (let t,j = parse1 c k in match j with ")"::i -> let u,h = parse2 c i in (t::u),h | _ -> failwith "parse") | ")"::_ -> [],l | s::k -> (let t = try Var(index s c) with Not_found -> Const(s) in let u,j = parse2 c k in (t::u),j) and parse3 c l = match l with [] -> failwith "parse" | "."::k -> parse1 c k | s::k -> if mem s ["^"; "("; ")"] then failwith "parse" else let t,j = parse3 (s::c) k in Abstr(s,t),j in let t,k = parse1 [] l in if k = [] then t else failwith "parse";; let term = parse ** lex ** explode;; (* ------------------------------------------------------------------------- *) (* Writing lambda terms. *) (* ------------------------------------------------------------------------- *) let term_to_string t = let rec term_to_string1 b1 b2 c t = match t with Const(s) -> s | Var(n) -> (try nth c n with Failure "nth" -> failwith "term_to_string") | App(f,x) -> let s = (term_to_string1 false true c f)^ (term_to_string1 true (not b1 & b2) c x) in if b1 then "("^s^")" else s | Abstr(v,a) -> let s = "^"^(term_to_string2 c t) in if b2 then "("^s^")" else s and term_to_string2 c t = match t with Abstr(v,a) -> v^(term_to_string2 (v::c) a) | _ -> "."^(term_to_string1 false false c t) in term_to_string1 false false [] t;; let alpha t = let rec occurs c t n v = match t with Const(w) -> v = w | Var(m) -> m > n & v = nth c m | App(f,x) -> (occurs c f n v) or (occurs c x n v) | Abstr(w,a) -> occurs (w::c) a (n + 1) v in let rec alpha1 c t = match t with App(f,x) -> App(alpha1 c f,alpha1 c x) | Abstr(v,a) -> alpha2 c a v | _ -> t and alpha2 c t v = if occurs (v::c) t 0 v then alpha2 c t (v^"'") else Abstr(v,alpha1 (v::c) t) in alpha1 [] t;; let print_term f t = Format.pp_print_string f ("term \""^(term_to_string (alpha t))^"\"");; #install_printer print_term;; (* ------------------------------------------------------------------------- *) (* Combinators. *) (* ------------------------------------------------------------------------- *) let combinators = ["I", term "^x.x"; "K", term "^xy.x"; "S", term "^xyz.(xz)(yz)"; "B", term "^xyz.x(yz)"; "C", term "^xyz.xzy"; "1", term "^xy.xy"; "Y", term "^f.(^x.f(xx))(^x.f(xx))"; "T", term "^xy.x"; "F", term "^xy.y"; "J", term "^abcd.ab(adc)"];; let unfold f = match f with Const(s) -> (try assoc s combinators with Not_found -> f) | _ -> f;; (* ------------------------------------------------------------------------- *) (* Reduction. *) (* ------------------------------------------------------------------------- *) let rec lift d n t = match t with Var(m) -> if m >= n then Var(m + d) else Var(m) | App(f,x) -> App(lift d n f,lift d n x) | Abstr(v,a) -> Abstr(v,lift d (n + 1) a) | _ -> t;; let rec subst n u t = match t with Var(m) -> if m = n then lift n 0 u else if m > n then Var(m - 1) else t | App(f,x) -> App(subst n u f,subst n u x) | Abstr(v,a) -> Abstr(v,subst (n + 1) u a) | _ -> t;; exception Normal;; let maybe f x = try f x with Normal -> x;; let beta i t = match t with App(f,x) -> (match unfold f with Abstr(_,a) -> subst 0 (maybe i x) (maybe i a) | _ -> raise Normal) | _ -> raise Normal;; let rec leftmost_innermost t = match t with App(f,x) -> (try App(leftmost_innermost f,x) with Normal -> try App(f,leftmost_innermost x) with Normal -> beta id t) | Abstr(v,a) -> Abstr(v,leftmost_innermost a) | _ -> raise Normal;; let rec leftmost_outermost t = match t with App(f,x) -> (try beta id t with Normal -> try App(leftmost_outermost f,x) with Normal -> App(f,leftmost_outermost x)) | Abstr(v,a) -> Abstr(v,leftmost_outermost a) | _ -> raise Normal;; let rec parallel_outermost t = match t with App(f,x) -> (try beta id t with Normal -> try let g = parallel_outermost f in App(g,maybe parallel_outermost x) with Normal -> App(f,parallel_outermost x)) | Abstr(v,a) -> Abstr(v,parallel_outermost a) | _ -> raise Normal;; let rec gross_knuth t = match t with App(f,x) -> (try beta gross_knuth t with Normal -> try let g = gross_knuth f in App(g,maybe gross_knuth x) with Normal -> App(f,gross_knuth x)) | Abstr(v,a) -> Abstr(v,gross_knuth a) | _ -> raise Normal;; let rec reduce x z n t = if n = 0 then z else try let u = x t in t::(reduce x z (n - 1) u) with Normal -> [t];; let rec normal_form x t = try normal_form x (x t) with Normal -> t;; (* ------------------------------------------------------------------------- *) (* Abbrevs. *) (* ------------------------------------------------------------------------- *) let etc = [Const("...")];; let all = -1;; let nf = normal_form leftmost_outermost ** term;; let red n = reduce leftmost_outermost etc n ** term;; let red_eager n = reduce leftmost_innermost etc n ** term;; let red_par n = reduce parallel_outermost etc n ** term;; let red_gk n = reduce gross_knuth etc n ** term;; (* ------------------------------------------------------------------------- *) (* Examples. *) (* ------------------------------------------------------------------------- *) nf "(^x.fx)a";; nf "(KISS)(KISS)";; red_gk all "SKK";; red 7 "(^x.xx)(^x.xx)";; (* ------------------------------------------------------------------------- *) (* Usage: *) (* *) (* 1. Run "ocaml" (I used version 3.04, but other versions will work). *) (* 2. At the prompt type: *) (* *) (* #use "lambda.ml";; *) (* *) (* and expect the output to look like the output below. *) (* 3. Type expressions like in the examples above. *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* # #use "lambda.ml";; *) (* val id : 'a -> 'a = *) (* val ( ** ) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b = *) (* val index : 'a -> 'a list -> int = *) (* type term = *) (* Const of string *) (* | App of term * term *) (* | Abstr of string * term *) (* | Var of int *) (* val explode : string -> string list = *) (* val implode : string list -> string = *) (* val lex : string list -> string list = *) (* val parse : string list -> term = *) (* val term : string -> term = *) (* val term_to_string : term -> string = *) (* val alpha : term -> term = *) (* val print_term : term -> unit = *) (* val combinators : (string * term) list = *) (* [("I", term "^x.x"); ("K", term "^xy.x"); ("S", term "^xyz.xz(yz)"); *) (* ("B", term "^xyz.x(yz)"); ("C", term "^xyz.xzy"); ("1", term "^xy.xy") *) (* ("Y", term "^f.(^x.f(xx))^x.f(xx)"); ("T", term "^xy.x"); *) (* ("F", term "^xy.y"); ("J", term "^abcd.ab(adc)")] *) (* val unfold : term -> term = *) (* val lift : int -> int -> term -> term = *) (* val subst : int -> term -> term -> term = *) (* exception Normal *) (* val maybe : ('a -> 'a) -> 'a -> 'a = *) (* val beta : (term -> term) -> term -> term = *) (* val leftmost_innermost : term -> term = *) (* val leftmost_outermost : term -> term = *) (* val parallel_outermost : term -> term = *) (* val gross_knuth : term -> term = *) (* val reduce : ('a -> 'a) -> 'a list -> int -> 'a -> 'a list = *) (* val normal_form : ('a -> 'a) -> 'a -> 'a = *) (* val etc : term list = [term "..."] *) (* val all : int = -1 *) (* val nf : string -> term = *) (* val red : int -> string -> term list = *) (* val red_eager : int -> string -> term list = *) (* val red_par : int -> string -> term list = *) (* val red_gk : int -> string -> term list = *) (* - : term = term "fa" *) (* - : term = term "^yzz'.zz'(yzz')" *) (* - : term list = *) (* [term "SKK"; term "(^yz.Kz(yz))K"; term "^z.(^y.z)(Kz)"; term "^z.z"] *) (* - : term list = *) (* [term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx"; *) (* term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx"; *) (* term "(^x.xx)^x.xx"; term "..."] *) (* # *) (* ------------------------------------------------------------------------- *)