linlo.tex

\newcommand{\lolli}{\multimap}

Linear logic~\cite{Girard87} lets us reason locally about state. Hypotheses
must be used exactly once, though they can be reordered. For example, using
$\otimes$ as linear conjunction and $\lolli$ as linear implication, the
proposition $A \otimes B \lolli B \otimes A$ is derivable, but neither $A
\otimes B \lolli A$ nor $A \lolli A \otimes A$ is derivable.

A minimal example of an interactable object encoded as a linear logic
program is toggling a switch:

\begin{verbatim}
    flip on off.
    flip off on.
    toggle : sw v * flip v u -o sw u.
\end{verbatim}

\noindent
Implicitly, we have two contexts: $\delta$, the ephemeral context, is where
we put resources that can be consumed, whereas $\Gamma$, the persistent
context, is where we put facts such as the rules defined above.

Supposing a distinguished proposition \verb|end|, a standard linear sequent
calculus for DILL (linear logic with $!$), and a desire to toggle the
switch from on to off, we could construct the following derivation
corresponding to a trace of the program:

{\small
\[
\infer
{
  \Gamma; \Delta, sw\ on \longrightarrow end
}
{
  \infer
  {
    \Gamma; \Delta, sw\ on, \forall(v,u).((sw\ v)\otimes (flip\ v\
    u)\multimap sw\ u)
    \longrightarrow end
  }
  {
  \infer
    {
    \Gamma; \Delta, sw\ on, (sw\ on)\otimes (flip\ on\ off)\multimap sw\
    off
    \longrightarrow end
    }
    {
        \infer{
          \Gamma; sw\ on \longrightarrow (sw\ on)\otimes(flip\ on\ off)
          }
          {
            \infer
            {\Gamma; sw\ on \longrightarrow sw\ on}
            {}
            \qquad
            \infer
            {\Gamma; \cdot \longrightarrow flip\ on\ off}
            {}
          }
        \qquad
        \infer{
          \Gamma; sw\ off \longrightarrow end
          }
          {\vdots
          }
    }
  }
}
\]
}

\noindent
The unfinished derivation is the continuation of the program after toggling
the switch. It represents a new choice point in the program where the human
part of the interactive theorem prover could select a persistent rule from
$\Gamma$.  Supposing we had many switches, levers, and knobs, this
component of choice could be a lot like a gameplay interaction.

%At least one game creator has made linear logic proof search fun
%~\cite{theatrics}.


 \subsection{Known issues}
 
 An important aspect of this problem arises when you want to add {\em
 persistently learnable facts} over ephemeral facts. In the previous
 section, we mentioned the possibility of having a {\em visibility}
 predicate, which is clearly ephemeral but which we may wish to use as a
 precondition to a rule without consuming it. In the talk we may go into
 further detail.