August 31st, 2012

beartato phd

(no subject)

Over breakfast noticed a few things about Polakow and Pfenning's LFM paper "Properties of terms in continuation-passing style in an ordered logical framework" from 2000:

(1) I can't see why the triv argument to kapp (defined on page 6) is ordered rather than unrestricted.
(2) In fact, I don't see why you can't completely keep separate the trivs that are closed, non-substructural values, (all those mentioned in the types of kapp and lam) from the trivs that are ordered and act as intermediate values on the stack. (all those mentioned in the types of app and vlam). Like, make them totally separate types.

I tried to twelf this up, using my thesis-hammer to view it as a nail and extract out the ordered logic stuff as world manipulations. Since I don't have an HLF implementation for ordered logic, I wasn't expecting this to work without hacks. I started out by manually defining a world-type and a star like
w : type.
* : w -> w -> w. %infix none 30 *.

and I thought I'd eventually need to put in some bullshit terms like
terrible_hack : type_family (A * (B * C)) ->  type_family ((A * B) * C).

for a type family or two to take care of the fact that I can't really represent associativity correctly.

But, a miracle (well, actually, a "stack discipline") occurred, and I observed
(3) I don't need associativity! Or a unit, come to think of it! Apparently the whole Polakow-Pfenning idea also works in (to use Bourbaki's term for an algebra with a binary operator and nothing else) "magma logic". Which I can already reason about in vanilla twelf!

Specifically, the following twelf code SERVER OKs:
Collapse )

Anyway, I wish it had occurred to me to think of this example when I was working on thesis. It would have been a nice addition.