|
[Aug. 19th, 2003|03:40 pm]
Jason
|
Well my first guess definitely wasn't right, but I wrote up some thoughts on strict occurrences and things, and I feel pretty confident that the second guess works.
Wait, no. The twelf code examples in there are totally wrong-headed. Argh. Got my quantifiers mixed up. Hmm.
Yeah, but
nat : type.
z : nat.
s : nat -> nat.
tm : type.
hd : type.
sp : type.
lam : (hd -> tm) -> tm.
app : hd -> sp -> tm.
nil : sp.
cons : tm -> sp -> sp.
coe : hd -> tm = [x] app x nil.
pat : nat -> sp -> type.
pat_nil : pat z nil.
tm_strict : (hd -> tm) -> type.
sp_strict : (hd -> sp) -> type.
sp_strict_cons : sp_strict ([x] cons (M x) (S x)) <- sp_strict S.
sp_strict_cons : sp_strict ([x] cons (M x) (S x)) <- tm_strict M.
tm_strict_app : tm_strict ([x] app Y (S x)) <- sp_strict S.
tm_strict_lam : {N : nat} tm_strict ([x] lam ([y] M x y))
<- ({y : hd} ({S : sp} pat N S -> pat (s N) (cons (coe y) S))
-> tm_strict [x] M x y).
tm_strict_var : tm_strict ([x] (app x S)) <- pat N S.
%query 0 0
D : tm_strict [x] (lam [y] lam [z] app x (cons (coe y) (cons (coe y) nil))).
%query 0 0
D : tm_strict [x] (lam [y] lam [z] app x (cons (coe z) (cons (coe z) nil))).
%query 1 1
D : tm_strict [x] (lam [y] lam [z] app x (cons (coe y) (cons (coe z) nil))).
%query 1 1
D : tm_strict [x] (lam [y] lam [z] app x (cons (coe z) (cons (coe y) nil))).
...
[Closing file /home/godel/sb/encoding-strictness/enc.elf]
%% OK %%
|
|
