In Dale's Proof Search Foundations for Logic Programming talk, he gives a great minimalist example of an interactive system: toggling a switch. The encoding in Forum, a logic programming language based on full linear logic, goes like this:

or in logic,

\[

\exists u,v.[sw\ v\otimes flip\ v\ u \otimes (sw\ u \multimap G)]

\multimap

toggle\ G

\]

(Yes, I mainly did that to test the $$\LaTeX$$ rendering script I'm using.)

The talk I linked to gives a derivation (which I won't painstakingly copy here) illustrating the execution of the program: the goal sequent $$\Gamma; \Delta, sw\ on \longrightarrow toggle\ G$$ evolves through proof search into $$\Gamma; \Delta, sw\ off \longrightarrow G$$.

But this is something of a counterintuitive, higher-order encoding. The "action" by a hypothetical user of toggling the switch must be indexed by $$G$$, the goal that continues the program. Here, the action (together with the continuation) is a

If instead we did this Twelf-style, we might make "toggle" a

We now need to invent a distinguished atomic goal ("end") to use this as an action on contexts:

\[

\frac

{

\Gamma; sw\ on \longrightarrow sw\ on

\qquad

\Gamma; \cdot \longrightarrow flip\ on\ off

}

\]

\[

\frac

{

\Gamma; sw\ on \longrightarrow (sw\ on)\otimes(flip\ on\ off)

\qquad

\frac{\vdots}{

\Gamma; \Delta, sw\ off \longrightarrow end}

}

\]

\[

\frac

{

\Gamma; \Delta, sw\ on, (sw\ on)\otimes (flip\ on\ off)\multimap sw\ off

\longrightarrow end

}

{}

\]

\[

\frac

{

\Gamma; \Delta, sw\ on, \forall(v,u).((sw\ v)\otimes (flip\ v\ u)\multimap sw\ u)

\longrightarrow end

}

{

\Gamma; \Delta, sw\ on \longrightarrow end

}

copy

\]

(Sorry for the horrendous formatting; perhaps typesetting derivations with \frac is not really worth it...)

Here $\Gamma$ represents the signature where we've written our rules, and the interactive choice is performed not by selecting a goal, but by selecting a

There's not necessarily an advantage to looking at things this way, but it is the way of looking at things that is more in line with my slogans.

flip on off. flip off on. toggle G o- sw V * flip V U * (sw U -o G)

or in logic,

\[

\exists u,v.[sw\ v\otimes flip\ v\ u \otimes (sw\ u \multimap G)]

\multimap

toggle\ G

\]

(Yes, I mainly did that to test the $$\LaTeX$$ rendering script I'm using.)

The talk I linked to gives a derivation (which I won't painstakingly copy here) illustrating the execution of the program: the goal sequent $$\Gamma; \Delta, sw\ on \longrightarrow toggle\ G$$ evolves through proof search into $$\Gamma; \Delta, sw\ off \longrightarrow G$$.

But this is something of a counterintuitive, higher-order encoding. The "action" by a hypothetical user of toggling the switch must be indexed by $$G$$, the goal that continues the program. Here, the action (together with the continuation) is a

*logical proposition*that becomes the goal clause of proof search.If instead we did this Twelf-style, we might make "toggle" a

*term constructor*-- a rule for proof search -- rather than a proposition (type) constructor, leading to the following encoding:flip1 : flip on off. flip2 : flip off on. toggle : sw v * flip v u -o sw u.

We now need to invent a distinguished atomic goal ("end") to use this as an action on contexts:

\[

\frac

{

\Gamma; sw\ on \longrightarrow sw\ on

\qquad

\Gamma; \cdot \longrightarrow flip\ on\ off

}

\]

\[

\frac

{

\Gamma; sw\ on \longrightarrow (sw\ on)\otimes(flip\ on\ off)

\qquad

\frac{\vdots}{

\Gamma; \Delta, sw\ off \longrightarrow end}

}

\]

\[

\frac

{

\Gamma; \Delta, sw\ on, (sw\ on)\otimes (flip\ on\ off)\multimap sw\ off

\longrightarrow end

}

{}

\]

\[

\frac

{

\Gamma; \Delta, sw\ on, \forall(v,u).((sw\ v)\otimes (flip\ v\ u)\multimap sw\ u)

\longrightarrow end

}

{

\Gamma; \Delta, sw\ on \longrightarrow end

}

copy

\]

(Sorry for the horrendous formatting; perhaps typesetting derivations with \frac is not really worth it...)

Here $\Gamma$ represents the signature where we've written our rules, and the interactive choice is performed not by selecting a goal, but by selecting a

*rule*(a term from the signature, via "copy") to prove a goal.There's not necessarily an advantage to looking at things this way, but it is the way of looking at things that is more in line with my slogans.

(I'm just playing "that makes me think of" because I suspect this is already familiar to you, but...)

ReplyDeleteThis is also the view that's in like with multiset rewriting, the nice least-common-denominator of a lot of proof search strategies that can be described in CLF (monadic intuitionistic linear logic), LO/Forum (classical linear logic), and LLF (mostly-vanilla dual intuitionstic linear logic).

The last one leads to the most annoying encoding, but it's at least very uniform one; I think I'd prefer it to Dale's formulation. As in Dale's formulation, we make things higher-order in the sense of left-nested arrows, but not higher-order in the sense of "toggle" taking a proposition G as an argument.

flip1 : flip on off.

flip2 : flip off on.

toggle : (sw U -o end)

-o (sw V -o flip V U -o end)

You should be able to convince yourself that this gives rise to a very different intermediate derivation than the one you gave, but one with the exact same "top sequent" and "bottom sequent" that you gave.