lopro.tex

\renewcommand{\implies}{\supset}

In functional programming, we like to think of propositions as
types and proofs as programs. In what the authors coin the Miller
Correspondence~\cite{millertalk}, logic {\em programs} correspond to propositions
and {\em traces} correspond to proofs. If we want to write a game as an
{\em interactive logic program}, then running that program (playing that
game) should somehow correspond to {\em interactive proof search}, or
interactive theorem proving, not terribly unlike what many PL researchers
do regularly in systems like Coq, Isabelle, and Agda. Important questions
to ask in ITP come up in IF as well: at what point should reasoning be
filled in automatically? What proof strategy should that automatic
reasoning employ? In the talk we will argue that the proof theoretic
ideas of {\em forward chaining} and {\em left focus} play a key role in the
IF setting.

A logic program is a set of initial facts (typically general and
hypothetical) from which new facts can be generated and queries on the
space of facts can be made. It can be viewed as an inference system and its
execution as proof search.

As a small example, consider the following
Prolog~\cite{Covington:1996:PPD:230996} program to
find paths between nodes in a graph:

\begin{verbatim}
    path X X.
    path X Z :- edge X Y, path Y Z.
\end{verbatim}

\noindent
Each block of code preceding a period is a {\em clause} of the program, and
the capital-letter variables are implicitly universally quantified.
The logical interpretation of this program is one in which there are atomic
predicates \verb|path(-,-)| and \verb|edge(-,-)|, and two axiomatic
propositions, 
\[\forall x.\verb|path|(x, x)\] 
and 
\[\forall x,y,z.\verb|edge|(x, y) \land \verb|path|(y, z) \implies 
\verb|path|(x, z)\]

\noindent
We can create a graph by adding an additional clause for each edge (with
lowercase identifiers for specific nodes), then run a query such as
\verb|path a X| to get the  set of all the nodes reachable from $a$. The
execution of that program resembles constructing derivations of facts like
\verb|path a b| from rules in the program along with its core rules for
implication and quantification.

We can imagine beginning to design a world with the basic logic
programming toolset: we would introduce predicates (or types) for each kind of
thing in the world, like rooms and objects and people, and we could write
predicates like \verb|visible| to determine whether the player can see an
object. But as soon as we want to talk about state change, standard logic
programming fails us. For example, if we want to turn off a light, the
visibility of certain objects goes away---but treating the action as an
ordinary implication, the old facts stay around. Ordinary propositional
logics (such as the basis of Prolog) are {\em monotonic}: learning new facts
can never erase old ones. This brings us to linear logic.