Jason (jcreed) wrote,

Wrangled a bit with the logic programming project with Tom, and thought about it some more after he went off for to see a talk. I keep updating my notion of which fragment of LF I try to advocate as the right one, but I am currently feeling somewhat comfortable with the plus/minus-moded output-free fragment. Because even without patterns, assuming plus/minus (and no star) modes really ought to mean that one never does full unification but only matching. I'm straining to think where unification should ever occur except on inputs and outputs, and the inputs are required to be ground going in, and the outputs are guaranteed to be ground coming out, even for wacky examples like

bool: type. t : bool. f: bool.
lemma : bool -> type.
%mode lemma +B.
thm : type.
%mode thm.
- : thm <- (lemma Z -> lemma t) <- (lemma Z -> lemma f).

Then output-freeness should save us from ever having to make outputs effectively inputs and using unification on them.

So this would mean doing more than patterns during unification, so one would have to handle postponing equations, but one side would always be ground, so no mucking about with computing intersection and restriction in deBruijn form.

A successful compilation of some clause should line up, I think, with a constructive witness that the clause is well-moded. If the inputs are ground, then one should be able to create a functional expression of what ground terms the outputs are instantiated with.

In other news I went to D's and it was above-average fun. And watched S03E03 of Lost. "We killed a polar bear".
Tags: compilation, twelf, work
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded