Computation and Deduction 2009/20090223

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% ABORT %%
Output: here.

Code from class, February 23.

ttp : type. %name ttp T.

tnum : ttp.
tnot : ttp -> ttp.
tprod : ttp -> ttp -> ttp.

texp : type. %name texp E.
tval : type. %name tval V.

tlet : tval -> (tval -> texp) -> texp.
tpi1 : tval -> (tval -> texp) -> texp.
tpi2 : tval -> (tval -> texp) -> texp.
tifz : tval -> texp -> (tval -> texp) -> texp.
tapp : tval -> tval -> texp.

tz : tval.
ts : tval -> tval.
tpair : tval -> tval -> tval.
tlam : ttp -> (tval -> texp) -> tval.

tof : tval -> ttp -> type.
twf : texp -> type.

tof/z : tof tz tnum.

tof/s : tof (ts V) tnum
	 <- tof V tnum.

tof/pair : tof (tpair V1 V2) (tprod T1 T2)
	    <- tof V1 T1
	    <- tof V2 T2.

tof/lam : tof (tlam T ([x] E x)) (tnot T)
	   <- ({x} tof x T -> twf (E x)).

twf/let : twf (tlet V ([x] E x))
	   <- tof V T
	   <- ({x} tof x T -> twf (E x)).

twf/pi1 : twf (tpi1 V ([x] E x))
	   <- tof V (tprod T1 T2)
	   <- ({x} tof x T1 -> twf (E x)).

twf/pi2 : twf (tpi2 V ([x] E x))
	   <- tof V (tprod T1 T2)
	   <- ({x} tof x T2 -> twf (E x)).

twf/ifz : twf (tifz V E0 ([x] E1 x))
	   <- tof V tnum
	   <- twf E0
	   <- ({x} tof x tnum -> twf (E1 x)).

twf/app : twf (tapp V1 V2)
	   <- tof V1 (tnot T)
	   <- tof V2 T.

ttrans : tp -> ttp -> type.

ttrans/num : ttrans num tnum.

ttrans/arr : ttrans (arr T1 T2) (tnot (tprod T1' (tnot T2')))
	      <- ttrans T1 T1'
	      <- ttrans T2 T2'.

trans : term -> tp -> tval -> type.

trans/z : trans z num (tlam (tnot tnum) ([f] tapp f tz)).

trans/s : trans (s E) num (tlam (tnot tnum) ([f] tapp V (tlam tnum ([x] tapp f (ts x)))))
	   <- trans E num V.

trans/ifz : trans (ifz E E0 ([x] E1 x)) T
	     (tlam (tnot T')
		([f] tapp V (tlam tnum ([y] tifz y (tapp V0 f)
					  ([y'] tlet (tlam (tnot tnum) ([g] tapp g y'))
					     ([x'] tapp (V1 x') f))))))
	     <- ttrans T T'
	     <- trans E num V
	     <- trans E0 T V0
	     <- ({x} {x'} trans x num x' -> trans (E1 x) T (V1 x')).

trans/lam : trans (lam T1 ([x] E x)) (arr T1 T2)
	     (tlam (tnot (tnot (tprod T1' (tnot T2'))))
		([f] tapp f (tlam (tprod T1' (tnot T2'))
			       ([y] tpi1 y
				  ([y'] (tpi2 y
					   ([g] tlet (tlam (tnot T1') ([w] tapp w y'))
					      ([x'] tapp (V x') g))))))))
	     <- ttrans T1 T1'
	     <- ttrans T2 T2'
	     <- ({x} {x'} trans x T1 x' -> trans (E x) T2 (V x')).