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 (…

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 (…