Jason (jcreed) wrote,
Jason
jcreed

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 %%

Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 0 comments