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
System.Control.Print.printDepth := 25; System.Control.Print.stringDepth := 256; infixr -->; datatype Ty = O | --> of Ty*Ty; type Co = Ty list; datatype Tm = var of int | lam of Tm | app of Tm*Tm; fun weak n = let fun weak1 l (var i) = if l<=i then (var (i+n)) else (var i) | weak1 l (app(M1,M2)) = app(weak1 l M1,weak1 l M2) | weak1 l (lam M) = lam (weak1 (l+1) M) in weak1 0 end; datatype Vl = v_o of Tm | v_arr of int->Vl->Vl; fun weak_vl n (v_o M) = v_o (weak n M) | weak_vl n (v_arr f) = v_arr (fn i => fn x => f (n+i) x); fun q O (v_o M) = M | q (S --> T) (v_arr f) = lam (q T (f 1 (u S (var 0)))) and u O M = v_o M | u (S --> T) M = v_arr(fn n => fn x => (u T (app (weak n M,q S x)))); fun eval (var i) xs = nth(xs,i) | eval (lam M) xs = v_arr (fn n => fn x => eval M (x::(map (weak_vl n) xs))) | eval (app (M1,M2)) xs = case (eval M1 xs) of (v_arr f) => f 0 (eval M2 xs); fun id [] = [] | id (S::G) = (u S (var 0))::(map (weak_vl 1) (id G)); fun nf G S M = q S (eval M (id G)); (* val I = lam (var 0); val comp = lam (lam (lam (app (var 2,app(var 1,var 0))))); (* [f,g][x]f(g x) *) val nat = (O --> O) --> (O --> O); val zero = lam I; (* [g]I *) val succ = lam (lam (app (app(comp,var 0),app(var 1,var 0)))); (* [f][g]g o (f g) *) fun int2nat n = if n = 0 then zero else app(succ,int2nat (n-1)); fun test_mult i j = nf [] nat (app (app(comp,int2nat i),int2nat j)); fun test_pow i j = nf [] nat (app (int2nat j,int2nat i)); fun subst l (var i) N = if i