## Friday, June 24, 2011

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:

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.

#### 1 comment:

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

This 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.