Computation and Deduction 2009/20090223
From The Twelf Project
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')).