%XXX sort through

In this appendix, we briefly discuss CLF/Celf's proof-theoretic basis for
stratifying forward and backward chaining search.

Recall from Chapter~\ref{chapter:llns}: $\Gamma; \Delta \to \Gamma';
\Delta'$ is a permissible program step whenever it is the case that

\[
\infer
{\Gamma; \Delta \vdash \gamma}
{\Gamma'; \Delta' \vdash \gamma}
\]

is a permissible inference for an arbitrary conclusion $\gamma$. 

We can rewrite the left sequent rules for connectives as transition rules
in this fashion, as shown in prior work~\cite{deng2012relating}:
% (XXX actually compare this to theirs)

$\tensor L$: 
\[
(\Gamma; \Delta, A\tensor B) \to (\Gamma; \Delta, A, B)
\]

$\bang L$: 
\[
(\Gamma; \Delta, \bang A) \to (\Gamma, A; \Delta) 
\]

$\mathsf{copy}$:
\[
(\Gamma, A; \Delta) \to (\Gamma, A; \Delta, A)
\]


$\lolli L$: 
\[
\infer
{(\Gamma; \Delta, \Delta', A\lolli B) \to (\Gamma; \Delta, B)}
{\Gamma; \Delta' \vdash A}
\]

Note that this last rule appeals to the standard judgment
$\Gamma; \Delta \vdash A$ to solve for the antecedent of the rule, which
might be immediately available in $\Gamma; \Delta$, or it might require
backward-chaining search. 

In a {\em purely forward chaining} system, we
would require that all atoms in $A$ appear already in the context at the
time of selecting the rule; that is, we can rewrite the transition

$\lolli L'$:
\[
(\Gamma; \Delta, a_1,\dots,a_n, a_1\tensor\dots\tensor a_n\lolli B)
  \to (\Gamma; \Delta, B)
\]

If we further restrict the logic program so that {\em rules}
$A \lolli B$ only appear in the program signature $\Sigma$, never the
context, then we may understand rules of the form $a_1\dots a_n \lolli
b_1\dots b_m$ (where, again, atoms $a_1\dots a_n$ {\em only} arise as the
consequents of forward-chaining rules) as inducing a corresponding
transition

\[\Delta, a_1, \dots, a_n \to \Delta, b_1, \dots, b_m\]

for any $\Delta$.
\footnote{
Note that parametricity over the context $\Delta$, representing the ambient state that is
irrelevant to the specific rule $r$, stays the same across the transition.
This fact evades the {\em frame problem} present in other settings, such as
event and situation calculi~\cite{hayes1971frame}.
}

If, further, no quantification over terms is permitted, then what we have
produced is a fragment of the logic corresponding exactly to {\em multiset
rewriting}~\cite{cervesato2009relating}: a program is simply a set of
rewrite rules and an initial multiset, and executions of the program
correspond to ways that the initial multiset may be rewritten into stable
(quiescent) multisets.  Note that such a rewrite system is still {\em
nondeterministic} in that multiple rules may apply; so too, then, is the
semantics of the program: the same program and initial configuration may
result in distinct states during distinct runs. For this reason, multiset
rewriting systems have sometimes been considered a good basis for modeling
concurrent and distributed computation~\cite{meseguer1990rewriting}. In the
narrative generation setting, the nondeterminism of program semantics is
what gives rise to variable story generation from a given story world.

In Celf, the semantics are slightly more complicated than this multiset
rewriting depiction, because forward and backward chaining may be used in
combination. CLF, Celf's theoretical basis, introduces a connective
$\mon{A}$ to specify forward chaining. We next give the concrete syntax of
Celf and overview its semantics on an intuitive level.

% \section{Celf}
 
An idealized version of Celf stratifies propositions into two categories,
{\em positive} propositions $S$ and {\em negative} propositions $A,B$,
based on a theory called focusing~\cite{andreoli1992logic}.  Using this
stratification together with the connective $\mon{S}$ for casting a
positive proposition as a negative one, it effectively permits two kinds of
rules, one each corresponding to forward and backward chaining: rules $A
\lolli B$ are available in backward- {\em or} forward-chaining phases of
the program, and rules $A \lolli \mon{S}$ are available only in
forward-chaining phases. 

As an example, consider a program with the rules
$r_1 : a \lolli b$, $r_2 : b \lolli \mon{c}$. Given the goal sequent
$\cdot; a \vdash c$, proof search will not succeed: since $c$ is not of
the form $\mon{A}$, proof search will use backward chaining, and
backward chaining on the goal $c$ does not turn up any rules it can use
(because $r_2$ is only available in forward-chaining). 

If, however, we initialize the program with the sequent $\cdot; a \vdash
\mon{c}$, the proof will succeed: we will enter forward chaining, notice
that a forward chaining rule ($r_2$) is available if only we can prove its
antecedent $b$, which then initiates a {\em backward} chaining phase of
search for the goal $b$. The rule $r_1$ is available in backward chaining,
so we will try it (since its head matches the goal $b$), recursively
solving for the goal $a$, which is available in the context, so search
succeeds. Now we can use the rule $r_2$ to evolve the context to $c$, which
is quiescent. At that point, we check whether the context matches the goal:
in this case, the goal is $c$, which does indeed match.


