Jason (jcreed) wrote,

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


  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded