\section{Introduction}

Specifications in linear logic involve complex, interdependent state
transformations that are not always easy to reason about, especially as
programs grow. Many programs implicitly encode {\em invariants} that the
programmer holds in their head while adding complexity. 
For instance, in the interactive fiction example described
Section~\ref{sec:inform}, the programmer must take great care not to write
any rules that discard an atom of the form \verb|at player Room|.
The whole program's correctness hinges on the implict assumption that the
player is always \verb|at| some location in the world, and we can very
easily create programs that break such assumptions.
When the language permits writing such fragile code, we cannot make a
strong claim about its usability, due to the potential for novices to make
errors like these without the ability to know what they did wrong.

On the other end of a spectrum of expressive power for constraints, we can
also consider full verification of high-level properties of a game such as
solvability. Such constraints have been used in generative
methods~\cite{smith2011answer}, including the automatic generation of
playable games. Extending invariant checking to these domains would mean
not only producing well-formed starting configurations (such as level
configuration) but also proving that everything the player can {\em do} in
a generated game or level does not break its well-formedness.

To these ends, we propose constructing automated reasoning tools for linear
logic programs that enable the explicit statement and automatic checking of
program invariants. In this chapter, we present partial progress toward
this goal and discuss challenges to solving it in full generality.  We
present three candidate logics for stating invariants, several manual
proofs illustrating each approach, and a decidability result for
automatically verifying a fragment of the language.

\subsection{Example: Blocks World}
  
Consider the following specification of the ``blocks world'' domain from AI
planning~\cite{nilsson2014principles}: the domain includes blocks stacked
on a table and a robotic arm that can pick up blocks and set them down on
top of one another or on the table.

\begin{verbatim}
block : type.
on block block : pred.    % one block on top of another.
on_table block : pred.    % the block is on the table.
clear block : pred.       % the block has nothing on it.
arm_holding block : pred. % robot arm holds the block.
arm_free : pred.          % robot arm holds nothing.

% pick up a block from the table.
pickup_from_table : on_table B * clear B * arm_free -o arm_holding B.

% put down a block on the table.
putdown_on_table  : arm_holding B -o on_table B * clear B * arm_free.

% pick up a block from atop another block.
pickup_from_block : on BHi BLow * clear BHi * arm_free
                      -o clear BLow * arm_holding BHi.

% put down a block on top of another block.
putdown_on_block  : clear BLow * arm_holding BHi
                      -o on BHi BLow * clear BHi * arm_free.
\end{verbatim}

To fully specify the domain, we state some assumptions about well-formed
states and interactions. For instance, we assume that blocks are arranged
in linear stacks with the table at the bottom, we assume that the arm
always holds at most one block, and we assume that there is a unique top
block of every stack that is marked as ``clear.'' In order for us to verify
all of these assumptions, we need to know that they hold of any initial
configuration of blocks, and we need to know that the rules in the program
{\em preserve} the same assumptions.  If this were a terminating program
rather than a potentially-infinite simulation, we might also want to state
and prove properties of its execution in terms of what {\em final}
configurations look like, possibly as a function of initial configurations.

The hardest problem in the collection of problems just described seems to
be {\em invariant preservation}, i.e. a property of a program that says its
rules preserve some constraint on the shape of the context. The problem
bears some similarity to that of specifying well-formedness constraints on
LF contexts, which are expressed with {\em regular worlds} in the Twelf
implementation~\cite{pfenning1998twelf}, in that we want to specify general
patterns or schema for predicates that must appear alongside one another
pertaining to specific terms. Ideally, checking invariant preservation
should not depend on a {\em domain instance}. An example of a domain
instance for blocks world is a specification of the particular blocks and
starting configuration in a given simulation, such as the following:

\begin{verbatim}
a : block.
b : block.
c : block.

context init =
{ on_table a, clear a,
  on_table b, on c b, clear c,
  arm_free}.
\end{verbatim}

This part of the program can be thought of as {\em input} to the rule set,
in the sense that the rules should make sense {\em for any} well-formed set
of blocks and initial configuration. Thus a checking algorithm for
invariant preservation ought not to depend on this part of the
specification.~\footnote{However, see Section ~\ref{sec:instance} for an
example of a specification that might break this assumption.}

To check initial states, final states, and invariants, we need a way of
describing context schema (sets of configurations representing a property
of interest) and a framework in which to express and prove the program's
relationship to those schema. This chapter describes three candidate logics
for stating and proving these properties: {\em meta-linear logic}, {\em
generative signatures}, and {\em consumptive signatures}. We show examples
of proofs carried out in each of these logics for domains and properties of
interest to this thesis. We describe the limitations and potential for each
approach's automatability, and for the case of generative signatures, we
describe a decidability result for the propositional case of Ceptre. We
conclude by suggesting avenues for further investigation of this still-open
problem.

% Finally, we describe some preliminary and
% future work investigating empirical analysis of programs via querying trace
%sets.

\section{Meta-Linear Logic}
\label{sec:metaLLic}

The well-formedness conditions of the Blocks World domain can be decomposed
into two constraints on blocks and one on the robot arm, which may be
informally stated as follows:

\begin{enumerate}
  \item The first
constraint says a block must have a well-formed base: either it is on the
table, it is on top of another block, or it is held by the robot arm. 
  \item The second constraint says a block must have a well-formed top:
    either it is clear, there is another block on top of it, or it is held
    by the robot arm.
  \item The third constraint says that the robot arm must either be free or
    holding a block.
\end{enumerate}

Note that each of these descriptions independently seem to describe some
mutual exclusion between resources, which could be described through linear
logic's additive disjunction operator $\oplus$. These properties do not
{\em partition} the context, however. For instance, the robot arm holding a
block can satisfy all three of them, but we do not want to suggest that
there should be three robot arm-related resources, when in fact we intend
there to be exactly one.

We can describe these possibly-overlapping properties independently in
terms of {\em restrictions} of the context $\Delta$ to certain predicate
sets related to certain entities (usually predicate indices) over which
properties are described, written 
$\Delta{\restrictset{p_1,\dots,p_n}}$ where $p_i$ are predicate patterns
(predicates where each index either refers to a variable bound by a
quantifier or a wildcard $\_$ satisfied by any index).
We can also quantify over these entities in the
formula, universally at the outside and existentially on the inside. For
instance, the three properties above map onto the following formal
statements defining what it means for an argument context $\Delta$ to
satisfy the invariant (abbreviating \verb|on_table| to 
$\mathsf{ot}$, \verb|arm_holding| to $\mathsf{ah}$, \verb|arm_free| to
$\mathsf{af}$, and \verb|clear| to $\mathsf{cl}$):

\begin{itemize}
\item Invariant $BW_1$ (block bottom well-formedness):
\[
\forall b:\mathsf{block}.  \Delta{\restrictset{\pr{ot} b,\ \pr{on} b\ \_,\
\pr{ah} b}} \sats (\pr{ot} b) \oplus (\exists b'.\pr{on} b\ b') \oplus
(\pr{ah} b)
\]

\item Invariant $BW_2$ (block top well-formedness):
\[
  \forall b:\mathsf{block}. \Delta{\restrictset{\pr{cl} b,\ \pr{on} \_\ v,\ 
  \pr{ah} b}}
    \sats
    (\pr{cl} b) \oplus (\exists b'. \pr{on} b'\ b) \oplus
      (\pr{ah} b)
\]

\item Invariant $BW_3$ (arm well-formedness):
\[
  \Delta{\restrictset{\pr{ah} \_,\ \pr{af}}}
    \sats
      (\exists b. \pr{ah} b) \oplus \pr{af}
\]
\end{itemize}

Once a specific ground term index is plugged into this formula and the
restriction is calculated, satisfiability $\sats$ is determined simply by
producing a derivation in linear logic.
% XXX we don't actually do this... they are defined by the precondition to
% the rule. maybe assumes something about well-modedness?
% The domain specification gives us a finite enumeration of all terms to plug
% in for the quantified variables in these formulas. (Even if the domain is
% infinite, the initial context specification allows us to check only those
% indices that actually appear as ground terms in the context.)

To check a {\em program rule}, we must parameterize over frame contexts in
which the rule might apply. For example, consider the ``pick up from table''
rule, which has the form
\begin{verbatim}
ontable B * clear B * arm_free -o arm_holding B
\end{verbatim}

In order for this rule to apply to a context $\Delta$, that context must
have the form

\[ 
  \Delta',\ \pr{ontable} b,\ \pr{clear} b,\ \pr{arm\_free}
\] 

(where $b$ is a ground term), and the state after application of the rule
will be

\[
  \Delta',\ \pr{arm\_holding}\ b
\]

We quantify universally over the context $\Delta'$, which must be reasoned
about parametrically. The invariant itself quantifies over block terms
$B$, and to show that it holds of the resulting state, we must reason
parametrically over those as well.
The {\em locality} or frame property of linear logic transitions means that 
whichever ones might appear in $\Delta'$ but not in the rule will remain
unchanged and easy to reason about. That leaves reasoning about the indices
that do appear in the rule with respect to the invariant.
\footnote{
This convenience depends crucially on the ``well-moded'' nature of rules:
any variables mentioned in the consequent of the rule must relate somehow
to variables in the antecedent. This means that even with infinite term
domains, we never need to reason inductively over all inhabitants.
}

An invariant $I$ is preserved by a given rule
taking a state $\Delta$ to a state $\Delta'$ exactly when $I(\Delta)$
implies $I(\Delta')$. We can show that each of the three parts of the
blocks world invariant described above apply to the 
\verb|pickup_from_table| rule as follows.

\begin{proposition}[Rule preserves blocks world invariants]
Given any $\Delta'$,\\ 
let
$\Delta = \Delta', \ \pr{ontable} b,\ \pr{clear} b,\pr{arm\_free}$.\\
For each $I\in\{BW_1, BW_2, BW_3\}$,
if $I(\Delta)$ then $I(\Delta',\ \pr{arm\_holding} b)$.
\end{proposition}

\begin{proof}
\textbf{Invariant $BW_1$: \lstinline{pickup_from_table} preserves block
  bottom well-formedness}\\
Intuitively, this property holds because the only block affected is the one
manipulated by the rule, and its bottom's initial $\mathsf{ontable}$
property is simply replaced by an equally satisfactory $\mathsf{arm\_holding}$
property. The proof follows.

By assumption ($BW_1$ holds of the input context), 
\[
  \forall b'{:}\mathsf{block}. 
  (\Delta', \ \pr{ontable} b,\ \pr{clear} b,\pr{arm\_free})
  {\restrictset{\pr{ot}b', \pr{on} b'\ \_, \pr{ah} b'}}
  \sats 
  (\pr{ot}b') \oplus (\exists b''. \pr{on} b'\ b'') \oplus (\pr{ah} b')
\]

Let $S$ be the restriction set given above,
$\{\pr{ot}b', \pr{on} b'\ \_, \pr{ah} b'\}$.

What we need to show is that for all blocks $c$,

\[
  (\Delta', \ \pr{arm\_holding} b)
  {\restrictset{\pr{ot}c, \pr{on} c\ \_, \pr{ah} c}}
  \sats 
  (\pr{ot}c) \oplus (\exists b''. \pr{on} c\ b'') \oplus (\pr{ah} c)
\]

Assume an arbitrary block $c$ for which to prove this fact. 

There are two cases: $c=b$ (the block referred to in the particular
transition) or $c\neq b$. In the case where $b$ and $c$ are distinct,
$\Delta{\restrict{S}} = \Delta'{\restrict{S}}$, and also
$(\Delta', \ \pr{arm\_holding} b){\restrict{S}} = \Delta'{\restrict{S}}$.
Then, what we know and need to show are the same, so the case is satisfied.

In the case where $b=c$, then we know
$\Delta{\restrict{S}} 
= \Delta'{\restrict{S}}, \pr{on\_table} b$.

By inversion, the proof that
$\Delta'{\restrict{S}}, \pr{on\_table} b
  \sats 
  \pr{ontable} b \vdash (\pr{ot} b) \oplus (\exists b'.\pr{on} b\ b') \oplus
  (\pr{ah} b)$ can only take the following form 
(according to the semantic interpretation of satisfiability given in
  ~\ref{sec:metalauto}, which essentially reduces to linear sequent
  provability):

\[
  \infer[\oplus R_1]
  {
  \pr{ontable} b \vdash (\pr{ot} b) \oplus (\exists b'.\pr{on} b\ b') \oplus
  (\pr{ah} b)
  }
  {
    \infer[\mathsf{init}]
    {
      \pr{ontable} b \vdash \pr{ontable} b
    }
    {}
  }
\]

Thus, $\Delta'{\restrict{S}}$ must be empty.

Now we need to show 

\[(\Delta',\ \pr{arm\_holding} b){\restrict{S}} 
    \sats (\pr{ot} b) \oplus (\exists b'.\pr{on} b\ b') \oplus (\pr{ah} b)
\]

Since $\Delta'\restrict{S}$ is empty,
\begin{eqnarray*}
  (\Delta',\ \pr{arm\_holding} b){\restrict{S}} 
    &=& \Delta'{\restrict{S}}, \pr{arm\_holding} b\\
    &=& \pr{arm\_holding} b
\end{eqnarray*}

So we equivalently need to show
$\pr{arm\_holding} b \sats 
(\pr{ot} b) \oplus (\exists b'.\pr{on} b\ b') \oplus (\pr{ah} b)$

which holds by derivation from $\oplus R$ rules. \qed

\textbf{Invariant $BW_2$: 
  The rule \lstinline{pickup_from_table} preserves block top
  well-formedness}

Intutitively, this property holds because the only block affected is the one
manipulated by the rule ($B$), and its bottom's initial $\mathsf{ontable}$
property is simply replaced by an equally satisfactory $\mathsf{arm\_holding}$
property. The proof follows.

By assumption and expansion of $BW_1$, for all $b:block$, and in particular
for the block $b$ specified by the transition, 
$\Delta{\restrictset{\pr{ot} b,\ \pr{on} b\ \_,\
\pr{ah} b}} \sats (\pr{ot} b) \oplus (\exists b'.\pr{on} b\ b') \oplus
(\pr{ah} b)$.
Intuitively, this property holds because the only block affected is the one
manipulated by the rule, and its top's initial $\mathsf{clear}$ property is
simply replaced by an equally satisfactory $\mathsf{arm\_holding}$
property. The proof follows.

Let $b$ be the block index chosen by the transition. 
Let the restriction set $S$ be $\{\pr{cl} b, \pr{ah} b, \pr{on} \_\ b\}$.

We know by assumption that
\[
  \Delta{\restrict{S}} \sats
    (\pr{cl} b)\oplus(\pr{ah} b)\oplus(\exists b'.\pr{on} b'\ b)
\]

and since $\pr{clear} b$ satisfies the disjunction,
$\Delta'{\restrict{S}}$ is empty by the same inversion reasoning as
previously.

We need to show 
$(\Delta', \pr{ah} b){\restrict{S}} \sats
    (\pr{cl} b)\oplus(\pr{ah} b)\oplus(\exists b'.\pr{on} b'\ b)$.

Since $\Delta'{\restrict{S}}$ is empty, it suffices to show
$\pr{ah} b \vdash 
    (\pr{cl} b)\oplus(\pr{ah} b)\oplus(\exists b'.\pr{on} b'\ b)$, which is
    derivable by rules. \qed


\textbf{Proof for $BW_3$ (\lstinline{pickup_from_table} 
  preserves arm well-formedness):}\\
Intuitively, this property holds because the arm's initial
$\mathsf{arm\_free}$ property is replaced by an equally satisfactory 
$\mathsf{arm\_holding}$ property. The proof follows.

Let $S$ be the restriction set $\{\pr{af,} \pr{ah}\_ \}$.

We know by assumption that 
\[
  \Delta{\restrict{S}} \sats
      (\exists b.\pr{ah} b)\oplus\pr{af}
\]

and since $\pr{arm\_free}$ satisfies the disjunction,
$\Delta'{\restrict{S}}$ is empty by the same inversion reasoning as
previously.

We need to show
$(\Delta', \pr{ah}){\restrict{S}} \sats  
      (\exists b.\pr{ah} b)\oplus\pr{af}
$

Since $\Delta'{\restrict{S}}$ is empty, it suffices to show
$\pr{ah} b \vdash 
      (\exists b.\pr{ah} b)\oplus\pr{af}$, which is derivable by rules.
\end{proof}

So far we have only proven the invariant for one rule, intentionally chosen
as one of the simpler ones in the program. In order to give a
representative sample of this method, we now show consider
a rule manipulating the {\em interaction} between two blocks, which we also 
want to preserve the invariants.  Below, we give the intuition for the
proof of invariant preservation for the \lstinline{putdown_on_block} rule.
There is one case that differs in format from the cases in the previous
proof: in particular, invariant $BW_1$ for block $b'$, the preservation of
the bottom block's bottom well-formedness.

\begin{proposition}
For any $\Delta'$,
let $\Delta = \Delta', \ \pr{ah} b,\ \pr{cl} b'$.
For each $I\in\{BW_1, BW_2, BW_3\}$,
if $I(\Delta)$ then $I(\Delta',\ \pr{on} b\ b',\ \pr{cl} b,\ \pr{af})$.
\end{proposition}

\begin{proofsketch}
We need to reason about each of the two blocks mentioned in this rule, $b$
and $b'$, and ensure that $BW_1$ and $BW_2$ holds for each of them.

\textbf{Invariant $BW_1$ (bottom well-formedness) for block $b$:}\\
This property holds because $\pr{ah} b$ is replaced by 
$\pr{on}b\ b'$.

\textbf{Invariant $BW_2$ (top well-formedness) for block $b$:}\\
This property holds because $\pr{ah} b$ is replaced by 
$\pr{clear}b$.

\textbf{Invariant $BW_1$ (bottom well-formedness) for block $b'$:}\\
This property holds because the rule does not manipulate this
property, i.e. predicates concerning it are not mentioned to the right nor
the left of the rule.

\textbf{Invariant $BW_2$ (top well-formedness) for block $b'$:}\\
This property holds because $\pr{clear} b'$ is replaced by
$\pr{on} b\ b'$.

\textbf{Invariant $BW_3$ (arm well-formedness)}\\
This property holds because $\pr{ah} b$ is replaced by $\pr{af}$.
\end{proofsketch}

\subsection{Example: Tower of Hanoi}
We continue to illustrate this meta-logical approach by example, this time
with a variation on the blocks world domain that is closer to a games
application: Tower of Hanoi. This example also involves the persistent,
backward-chaining component of the language and allows us to illustrate our
treatment of such constructs in program rules.

Define the Tower of Hanoi domain as follows: there is a finite number of
posts on which rings can be placed. A robot arm may either be holding a
ring or free. A ring $R$ may only be placed on top of another ring $R'$ if
$R$ is smaller than $R'$. To make our encoding more concise, we introduce a
general \verb|place| type to represent either an empty post or the top of a
ring. The code follows:

\begin{verbatim}
ring : type.
smaller ring ring : bwd.

place : type.
post : type.
top_of ring : place.
bottom post : place.

on ring place : pred.
clear place : pred.
arm_free : pred.
arm_holding ring : pred.

pickup : clear (top_of R) * on R P * arm_free 
      -o arm_holding R * clear P.

putdown_on_ring : arm_holding R * clear (top_of R') * smaller R R'
      -o arm_free * on R (top_of R') * clear (top_of R).

putdown_on_post : arm_holding R * clear (bottom P)
      -o arm_free * on R (bottom P) * clear (top_of R).
\end{verbatim}

An example instantiation of this domain is:

\begin{verbatim}
p1 : post.  p2 : post.  p3 : post.
r1 : ring.  r2 : ring.  r3 : ring.

smaller r1 r2.
smaller r1 r3.
smaller r2 r3.

context init =
{clear (bottom p2), clear (bottom p3),
    on r3 (bottom p1), on r2 (top_of r3), on r1 (top_of r2), 
    clear (top_of r1), arm_free}.
\end{verbatim}

Runnable Ceptre code for this example can be found in
Appendix~\ref{sec:hanoi}. 

The invariant we want to show preserved is that whenever a ring is on
another ring, the top ring is smaller. 
Here is a candidate statement of this invariant in the meta-logic:
\[
  I_{ToH^*}(\Delta) =
  \forall r,r'. \Delta{\restrictset{ \pr{on}r\ (\pr{top\_of}r') }}
  \sats ((\pr{on}r\ (\pr{top\_of}r'))\tensor\bang{\pr{smaller} r\ r'})
        \oplus \one
\]

This invariant says that any two rings in the program are either
in the \verb|on| relation, in which case they are accompanied by a provable
\verb|smaller| relation between them, or there is no such relationship
between them.\footnote{
  This invariant may seem awkward compared to a similar
  implication-flavored statement: 
  $\pr{on}r\ (\pr{top\_of}r') \limplies \bang{\pr{smaller}r\ r'}$.  
  However, this implication sits at the meta-logical
  level, and we do not wish to include such a connective in our restricted
  metalogic for the sake of potential automation. On the other hand, in
  classical logic we have the equivalence $A\limplies B \equiv (\lnot
  A)\lor B$, which gives us a {\em positive} (in the focusing sense; see
  Chapter~\ref{chapter:llns})
% XXX after writing that chapter, make sure that reference actually makes
  % sense.
characterization of implication more suitable to automatic search. This
invariant statement is essentially a reflection of this equivalence, which
is valid in this logic because we consider the presence or absence of an
atom in the context to be decidable---i.e. in a context restricted to
the set $\{a\}$, the proposition $a^k\oplus 1$ will always hold for some
$k$, which is analogous to the law of excluded middle in classical logic.  }

In order to make our proofs go through, however, we will need to strengthen
the invariant to include one of the original properties of the blocks world
program: in particular, the fact that rings have mutually exclusive
predicates referring to what is under them and what is atop them. It
suffices to supply just one of these properties, e.g.:

\[
\begin{split}
  I_{ToH}(\Delta) =\\
  \forall r. \Delta{\restrictset{ \pr{on}r\ \_,\ \pr{ah}r}}
  & \sats
    (\exists r'.(\pr{on}r\ (\pr{top\_of}r'))\tensor\bang{\pr{smaller} r\ r'})
  \\& \oplus
        (\exists p.(\pr{on}r\ (\pr{bottom}p)))
        \\& \oplus
        (\pr{arm\_holding}r)
\end{split}
\]

The proof that this invariant holds of the program is given rule-by-rule.
For rule \verb|pickup|:
\begin{proposition}[Rule preserves Tower of Hanoi invariant]
  For all $\Delta'$, $r:\mathsf{ring}$, and $p:\mathsf{place}$,
  if $I_{ToH}(\Delta',\ \pr{clear} (\pr{top\_of} r),\ \pr{on}r\ p,\ \pr{arm\_free})$,
  then $I_{ToH}(\Delta',\ \pr{arm\_holding}r,\ \pr{clear}p)$.
\end{proposition}
  
\begin{proof}
  Let $\Delta = 
        \Delta',\ \pr{clear} (\pr{top\_of} r),\ \pr{on}r\ p,\ \pr{arm\_free}$. 
  For most instantiations of the restriction set, the proof will be
  trivial, since the rule does not manipulate any instances of the restriction
  set unless the argument is $r$.
  In that case,
  let $S$ be the restriction set $\{\pr{on}r\ \_, \pr{ah}r\}$, and let
  $A$ be the formula
  \[
    \begin{split}
      &(\exists r'.(\pr{on}r\ (\pr{top\_of}r'))\tensor\bang{\pr{smaller} r\ r'})
  \\& \oplus
        (\exists p'.(\pr{on}r\ (\pr{bottom}p')))
        \\& \oplus
        (\pr{arm\_holding}r)
    \end{split}
  \]
  By assumption,
  $\Delta{\restrict{S}} \sats A$.
  The restriction $\Delta{\restrict{S}}$ computes to
$\Delta'{\restrict{S}}, \pr{on}r\ p$, and since $\pr{on}r\ p$ suffices
to prove the disjunction (either the first or second disjunct), 
$\Delta'{\restrict{S}}=\cdot$.

Need to show: $(\Delta', \pr{ah}r, \pr{cl}p){\restrict{S}}\sats A$.
$(\Delta', \pr{ah}r, \pr{cl}p){\restrict{S}} = 
    \pr{ah}r$ by reduction.
$\pr{ah}r\vdash A$ by rules (the single assumption satisfies the right disjunct).


% this is all obsolete afaik
%   There are two cases for how the restriction set computes: either
%   $p = \pr{top\_of}r'$ or they are distinct (i.e. either the
%   initially-bound ring $r$ is on top of the ring under scrutiny $r'$,
%   or $r'$ is irrelevant to this transition).
% 
%   \begin{itemize}
%     \item
%   In the first case, the restriction set reduces to
%     $\Delta'{\restrict{S}}, \pr{on}r\ (\pr{top\_of}\ r')$
%   which we know by inversion must satisfy the invariant by satisfying the left 
%   disjunct\\
%   $(\pr{on}r\ (\pr{top\_of}r'))\tensor\bang{\pr{smaller} r\ r'}$.\\
%   Then by inversion of $\bang$ we know $\Delta'{\restrict{S}} = \cdot$.
% 
%   We need to show
%   $(\Delta',\ \pr{arm\_holding}r,\ \pr{clear}p){\restrict{S}}
%     \sats
%     ((\pr{on}r\ (\pr{top\_of}r'))\tensor\bang{\pr{smaller} r\ r'})
%         \oplus \one$.\\
%   Since  $\Delta'{\restrict{S}} = \cdot$, this assertion is equivalent
%   to $\cdot \vdash
%     ((\pr{on}r\ (\pr{top\_of}r'))\tensor\bang{\pr{smaller} r\ r'})
%         \oplus \one$, which holds by $\oplus R$.
% 
%   \item
%   In the second case, the restriction set reduces to
%   $\Delta'{\restrict{S}}$, so we know\\
%   $\Delta'{\restrict{S}} \sats
%     ((\pr{on}r\ (\pr{top\_of}r'))\tensor\bang{\pr{smaller} r\ r'})
%         \oplus \one$.\\
%   We need to show
%   $\Delta',\ \pr{arm\_holding}r,\ \pr{clear}p){\restrict{S}}
%     \sats
%     ((\pr{on}r\ (\pr{top\_of}r'))\tensor\bang{\pr{smaller} r\ r'})
%         \oplus \one$.\\
%   Equivalently, since none of the new atoms are in the restriction set, we
%   need to show 
%   $\Delta'{\restrict{S}} \sats
%     ((\pr{on}r\ (\pr{top\_of}r'))\tensor\bang{\pr{smaller} r\ r'})
%         \oplus \one$, which we know by assumption.
%   \end{itemize}

\end{proof}

For rule \verb|putdown_on_ring|:\footnote{Note: since this rule involves a
  persistent premise, we must explicitly mention the signature $\Sigma$
  supplying the backward-chaining rules defining persistent propositions,
which we had previously been leaving silent. This treatment emerges from
what it means for a transition to apply; see Chapter~\ref{chapter:llpng}
% XXX when i write that chapter, make sure it mentions this.
for details.} 
\begin{proposition}
  For all $\Delta'$ and $r:\mathsf{ring}$,
  if $I_{ToH}(\Delta',\ \pr{arm\_holding}r, \pr{clear} (\pr{top\_of} r'))$
       and $\Sigma \vdash \pr{smaller}r\ r'$,
      then $I_{ToH}(\Delta',\ \pr{arm\_free},\ \pr{on}r\ (\pr{top\_of}r'),
      \ \pr{clear} (\pr{top\_of}r))$.
\end{proposition}

\begin{proof}
Let $\Delta = \Delta',\ \pr{arm\_holding}r, \pr{clear} (\pr{top\_of} r')$.
The proof is trivial for all instantiations of the invariant except in
cases where the restriction set mentions $r$, so let us consider the
instantiation of the invariant at $r$ for which the proof is nontrivial. 
Let $S$ be the restriction set  $\{\pr{on}r\ \_,\ \pr{ah}r\}$.
Let $A$ be the formula
\[
    \begin{split}
      &(\exists r'.(\pr{on}r\ (\pr{top\_of}r'))\tensor\bang{\pr{smaller} r\ r'})
  \\& \oplus
        (\exists p'.(\pr{on}r\ (\pr{bottom}p')))
        \\& \oplus
        (\pr{arm\_holding}r)
    \end{split}
\]

We know $\Delta{\restrict{S}} \sats A$, and in particular the premise
$\pr{ah}r$ satisfies the third disjunct, so $\Delta'{\restrict{S}}$ is
constrained to be empty. We need to show

\[
  (\Delta', \pr{af}, \pr{on}r\ (\pr{top\_of}r'),\ \pr{clear} (\pr{top\_of}r))
\restrict{S} \sats A
\]

The context restriction computes to  $\pr{on}r\ (\pr{top\_of}r')$
which together with the assumption $\bang\pr{smaller}r\ r'$
satifies the first disjunct.
\end{proof} 

%%%
  For rule \verb|putdown_on_post|:
\begin{proposition}
  For all $\Delta'$, $r:\mathsf{ring}$, and $p:\mathsf{post}$,
  if $I_{ToH}(\Delta',\ \pr{clear} (\pr{bottom} p),\ \pr{arm\_holding} r)$,
  then $I_{ToH}(\Delta',\ \pr{arm\_free},\ \pr{on}r\ (\pr{bottom} p),\
  \pr{clear} (\pr{top\_of} r))$.
\end{proposition}

\begin{proof}
Let $\Delta = \Delta',\ \pr{arm\_holding}r,\ \pr{clear} (\pr{bottom}p)$.
The invariant holds of $\Delta$ instantiated at $r$ because of the
$\pr{arm\_holding}r$ premise, which is straightforwardly replaced by the
$\pr{on}r\ (\pr{bottom}p)$ consequent. This proof follows the same pattern
we have now seen several times.
\end{proof}


\subsection{Potential for Automation}
\label{sec:metalauto}

In order to discuss potential algorithms for deciding a fragment of this
meta-logic, we need to define that fragment.  To do so, we constrain the
grammar of the meta-logic to formulas $\phi$ of the following form:

\begin{eqnarray*}
  \phi &::=& \lambda{\delta}.\gamma\\
  \gamma &::=& \forall{x{:}\tau}.\gamma \mid \Delta{\restrict{S}}\sats\psi\\
  \psi &::=& a \mid \psi \tensor \psi \mid \psi \oplus \psi
            \mid \exists{x{:}\tau}.\psi \mid \one\\
  S &::=& \cdot \mid \mathsf{pat}, S\\
  \mathsf{pat} &::=& a\ \mathsf{tpat}_1\dots\mathsf{tpat}_n\\
  \mathsf{tpat} &::=& \_ \mid t \mid c\ \mathsf{tpat}_1\dots\mathsf{tpat}_n
\end{eqnarray*}

% XXX !A

The grammar for terms $t$, term constants $c$, and atomic predicates $a$ is
borrowed from Ceptre's grammar, given in Chapter~\ref{chapter:ceptre}.

Then we give an interpretation of each component when a formula $\phi$ is 
applied to a context $\Delta$ (with respect to some type header $\Sigma$):

\begin{eqnarray*}
  \meaningof{\forall{x{:}\tau}.\gamma} &=& 
    \Sigma \vdash t:\tau \mathrm{\ implies\ }
    \Delta\sats[t/x]\gamma \\
  \meaningof{\Delta\sats a} &=& \Delta = \{a\}\\
  \meaningof{\Delta\sats \psi_1\tensor\psi_2} &=& \Delta = \Delta_1,\Delta_2
    \mathrm{\ and\ }\Delta_1\sats\psi_1\mathrm{\ and\ }\Delta_2\sats\psi_2
    \\
  \meaningof{\Delta\sats \psi_1\oplus\psi_2} &=&
      \Delta\sats\psi_1 \mathrm{\ or\ }\Delta\sats\psi_2\\
      \meaningof{\Delta\sats \exists{x{:}\tau}.\psi} &=&
        \mathrm{there\ exists\ }t\mathrm{\ s.t.\ } \Sigma \vdash
        t : \tau\mathrm{\ and\ } \Delta \sats [t/x]\psi\\
  \meaningof{\Delta\sats \one} &=& \Delta = \cdot
\end{eqnarray*}

\newcommand{\match}{\triangleright}
Pattern restriction $\Delta{\restrict{S}}$ computes another context
$\Delta'$, defined approximately as the intersection of $\Delta$ and $S$
where any wildcard patterns $\_$ in $S$ are considered equivalent to any
term. We write that an atom $p$ {\em matches} a pattern $\mathsf{pat}$ with
the notation $p\match\mathsf{pat}$, which is defined next.

Pattern restriction:
\begin{eqnarray*}
  \cdot{\restrict{S}} &=& \cdot\\
  (\Delta, p)\restrict{S}
  &=& \Delta{\restrict{S}}, p\quad\mathrm{\ if\ } p \in^* S\\
  &=& \Delta{\restrict{S}} \quad\mathrm{\ otherwise}\\
p \in^* S &\mathrm{iff}& \exists \mathsf{pat}\in S. p\match\mathsf{pat}
\end{eqnarray*}

Pattern matching:
\begin{eqnarray*}
  t &\match& t\\
  t &\match& \_\\
  c\ t_1\ldots t_n &\match& c\ \mathsf{tpat}_1\dots\mathsf{tpat}_n
    \mathrm{\ iff\ } t_1\match\mathsf{tpat}_1\mathrm{\ and\ }\dots\mathrm{\
    and\ }t_n\match\mathsf{tpat}_n\\
  a\ t_1\ldots t_n &\match& a\ \mathsf{tpat}_1\dots\mathsf{tpat}_n
    \mathrm{\ iff\ } t_1\match\mathsf{tpat}_1\mathrm{\ and\ }\dots\mathrm{\
    and\ }t_n\match\mathsf{tpat}_n
\end{eqnarray*}

Checking that a given context matches a formula in
this fragment of the logic for a given context has a
straightforward correspondence to the positive fragment of first-order
linear logic, which is a subset of MALL and thus decidable. 
Including the exponential operator $\bang$ in the limited fashion
demonstrated by the Tower of Hanoi example, i.e. to express constraints on
indices whose provability can be fully extricated from the linear
components, does not seem to affect this decidability in any obvious way,
but we currently leave its decidability as conjecture.

For invariant checking, i.e. checking that a given transition 
$\Delta \to \Delta'$ enabled by the program under scrutiny preserves a
property given in this language, we would need to codify the proof
technique embodied by the manual proofs given above in such a way that were
guaranteed to terminate, including inversion of
assumed derivations.

Here is a sketch of the algorithm, generalized from the previous examples:

To check an invariant 
$\phi = \lambda\delta.\forall \vec{x{:}\tau}.\delta{\restrict{S}}\sats\psi$ 
of a transition $\Delta\to\Delta'$:
\begin{enumerate}
  \item Expand $\phi(\Delta)$. 
    Generate fresh symbols for each $\forall$-quantified variable
    $x_i$ in $\phi(\Delta')$.
  \item Enumerate cases for terms in $\Delta$ being equal or not equal to
    those symbols.
  \item For each case, compute the restriction set $S$ and 
    determine possible inversions based on the rules for decomposing the
    inner formula $\psi$ (analogous to linear sequent calculus right
    rules). These introduce equality constraints on the restriction set of
    the input context $\Delta$ and on the part it shares with $\Delta'$.
  \item Using those constraints and, again, decomposition rules for the
    invariant formula, determine satisfiability of $\Delta'\sats \psi$.
\end{enumerate}

This process does not straightforwardly correspond to a known-decidable
procedure, but since the satisfiability semantics obey a subformula
property in the same sense as their corresponding linear logic rules, we
expect that inversion is a computable process.  We also have not yet
encountered examples in this fragment that require inductive lemmas.  Thus,
we conjecture that checking preservation of invariants described in this
meta-logic is decidable. It remains to prove that this is the case, as well
as to prove soundness and completeness with the logical derivability-based
notion of invariant preservation.  We leave further formalization and proof
to future work.

\subsection{Limitation: Recursive Predicates}
\label{sec:recursive}

Working in a restricted meta-logic to specify program invariants has some
drawbacks. For instance, some specifications of well-formed states are
simply inaccessible. Consider an encoding of linked lists in linear logic
wherein memory areas are encoded as abstract {\em destinations}
(terminology borrowed from the idea of ``destination-passing
style''~\cite{CLF2}) used as indices to a predicate describing data at a
location as well as a reference to the next location:

\begin{verbatim}
data : type.
location : type.
node location data location : pred.
\end{verbatim}

The list \verb|[a,b,c]| would be encoded as the domain instance:

\begin{verbatim}
a : data. b : data. c : data.
l1 : location. l2 : location. l3 : location.
end : location.
context list_abc = {node l1 a l2, node l2 b l3, node l3 c end}.
\end{verbatim}

We can write programs over this data that, for instance, delete a node from
the list (at location \verb|L'|):

\begin{verbatim}
delete : at L V L' * at L' _ L'' -o at L V L''.
\end{verbatim}

A common verification problem for reasoning about programs at a memory
layout level is {\em shape
analysis}~\cite{sagiv2002parametric,distefano2006local}: can we reason
that a given segment of memory has a particular shape (for instance binary
tree or linked list) and that a program that manipulates it, possibly
dynamically allocating memory, preserves that shape? Previously, linear
logic has been investigated as a candidate for expressing these program
constraints in terms more abstract than memory locations~\cite{jia2006ilc},
and it seems that such analyses should also extend to linear logic programs
themselves.

In particular, for this example, we might like to state that the linear,
non-circular, linked list structure of our memory layout encoding is
preserved by the deletion rule.  But such a property cannot be given by
local characterization of a single index; it must refer to the structure of
how indices are shared between predicates in the context. We also cannot
give it as a persistent property defined outside the state evolution rules,
since it refers to facts (like the way nodes are linked) that fundamentally
change during execution.

Instead, such a property is more naturally given
recursively, by saying either the list is empty, or contains a node
pointing to another well-formed linked list. 
One candidate approach for stating this kind of invariant is to extend the
meta-logic with a notion of recursive predicate. Such extensions to
first-order linear logic have been explored and proven
sound~\cite{baelde2008linear}.  However, this extension may complicate
decidability of the approach, and does not offer clear means for
automation. We describe a related approach more fully as part of a
different technique in Section~\ref{sec:consumptive}.


\section{Consumptive Invariants}
\label{sec:consumptive}

Aside from automation concerns, we also hope to extend the expressiveness
of the meta-logic by allowing the description of recursive invariants, such
as those described in the shape analysis literature. We describe a
technique that can {\em dynamically} check such invariants next.

This technique hinges on the observation that descriptors of context
properties resemble grammars that themselves can be expressed in linear
logic. And we can write recursive linear logic programs to express those
properties via backward-chaining. % XXX this is clunky, edit it

\subsection{Backward-Chaining Linear Logic Programs}

Linear logic programs may be given a backward-chaining interpretation so
long as each clause only has a single, atomic consequent, i.e. takes the
form $A \lolli p$. In concrete syntax, instead of 
\lstinline|p1 * ... * pn -o p|
for such a rule we will write the backwards, curried form
\lstinline|p o- p1 o- ... pn|, mimicking the syntax for persistent backward
chaining programs.

We refer to $p$ as the {\em head} of such a clause, and proof search may be
carried out on a particular atom by matching it against the heads of all
logic program clauses, then matching their premises as new goals,
backtracking when search along a particular branch fails, just like
persistent backward chaining. But linear rules still have a resource-based
meaning, i.e. for a rule \lstinline|p o- p1 o- p2| to succeed at
establishing \lstinline|p| in a context $\Delta$ means that $\Delta$ must
be partitionable into $\Delta_1$, $\Delta_2$ such that \lstinline|p1|
consumes all of $\Delta_1$ and \lstinline|p2| consumes all of $\Delta_2$. 

\subsection{Example: Linked List Shape Analysis}

Consider the linked list example given in Section ~\ref{sec:recursive}.
We can write a simple recursive predicate defining a well-formed
linked list {\em segment} with two arguments, $s$ for the beginning
location of the list and $e$ for the ending location. The linked list
segment is well formed if either $s\doteq e$ (the segment is empty) or
there is some node at $s$ with ``next'' field $l$ such that $l$ and $e$
define a well-formed segment. 

This definition can be represented by the following backward-chaining
linear logic program:

\begin{verbatim}
ll location location : bwd.
ll X X.
ll S E o- at S V L
       o- ll L E.
\end{verbatim}

Simmons~\cite{simmons12thesis} refers to this kind of specification as a
{\em consumptive} signature, because to use it as a verification tool, we
would supply a context $\Delta$ and attempt to prove $\Delta \vdash
\exists{s,e}.\pr{ll}s\ e$, which works operationally by using the rules
defining \verb|ll| to {\em consume} elements of $\Delta$ until none are
left.

% \subsection{Example: Sorted Lists}
% % ??? what was the deal w/this example
% \begin{verbatim}
% sorted_min (cons X nil) X.
% sorted_min (cons X L) X
%   <- sorted_min L M
%   <- X < M.
% \end{verbatim}

\subsection{Potential for Automation}

By combining the restriction mechanism from the meta-linear logic approach
with predicates defined recursively in linear logic, we can
straightforwardly extract a {\em dynamic} checking algorithm: after every
rule application, check that the resultant context $\Delta$ (or whatever
restriction of it) satisfies the formula by simply running linear logic
proof search. We have not determined to what extent such invariants can be
checked of a program statically, nor to what extent the dynamic process
described can be optimized not to re-compute full provability between every
transition in the program.

\subsection{Limitation: Apartness Constraints}

Apart from a lack of a known static decision procedure for preservation,
consumptive invariants have the following limitation: they cannot enforce
that a given predicate holds only for distinct term indices. For instance,
consider this candidate representation of the blocks world well-formedness
property.

\begin{verbatim}
wf_bw
  o- wf_arm
  o- wf_stacks.

wf_arm o- arm_free.
wf_arm o- arm_holding X.

wf_stacks o- 1.

wf_stacks o- on_table B
          o- wf_stack B
          o- wf_stacks.

wf_stack B o- clear B.

wf_stack B o- on B' B
           o- wf_stack B'.
\end{verbatim}

This specification does not suffice to rule out ill-formed blocks world
configurations as specified in Section~\ref{sec:metaLLic}, because it does
not enforce that a given block $B$ is not, say, simultaneously held by the
arm and on the table (or appearing in multiple stacks). The term indices of
the rules may be instantiated with any substitutions, including ones that
unify them with otherwise-existing terms.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Generative Invariants}

A {\em generative} signature, in contrast to a consumptive signature, is
one that describes a context property through rules that {\em generate} all
permissible contexts, again using the analogy between logic programs and
grammars.  Generative signatures and their use for specifying logic program
invariants were also first described in ~\cite{simmons12thesis}.

Generative signatures are collections of forward-chaining rules together
with a {\em seed} context $\Delta_0$, usually containing a distinguished
\verb|gen| atom which is expanded by the signature. By convention, we will
assume that all seed contexts take this form such that the signature itself
suffices to specify the property.

At first glance, generative signatures look like consumptive signatures
``with the arrows turned around:'' instead of distinct \verb|wf|
(well-formedness) predicates for each portion of the context, we have
distinct {\em generators}, analogous to nonterminals in a grammar, for each
portion of the context. A complete well-formed context $\Delta$, then, is
one for which there is a transition sequence $\Delta_0\to \Delta$ along
rules given in the generative signature $\Sigma_{gen}$, where $\Delta$
contains no nonterminals. An extremely simple example is given
below:

\begin{verbatim}
gen -o {a * gen}.
gen -o {1}.
\end{verbatim}

This signature, equipped with the seed context $\{$\verb|gen|$\}$, describes contexts
containing zero or more instances of \verb|a|. Formally, the set of
contexts that a signature $\Sigma$ and a seed $\Delta_0$ describes is the
set of reachable contexts from $\Delta_0$ following rules in $\Sigma$.
We call such a signature and seed pair $(\Sigma, \Delta_0)$ a 
{\em generative invariant} of a  program signature $\Sigma'$ if all rules
in $\Sigma'$ maintain the program state's membership in the set generated
by $\Sigma$ seeded with $\Delta_0$. We make this notion more precise later.

In addition to universally-quantified indices (standard logic variables),
generative invariants may also include {\em existentially generated}
variables via rules of the form \verb|A -o exists x.B|. The existential
quantifier has completely standard treatment from a forward-chaining proof
search perspective; see the CLF paper~\cite{CLF} for a formal treatment.

\subsection{Example: Generative Signature for Blocks World}

\newcommand{\siggenbw}{\Sigma_{\mathsf{bwgen}}}
Below we give a generative signature characterizing the blocks world
domain, effectively by ``turning the arrows around'' in the consumptive
signature. Let $\siggenbw =$

\begin{verbatim}
gen/bw : gen -o gen_arm * gen_stacks.
gen_arm/af : gen_arm -o arm_free.
gen_arm/ah : gen_arm -o exists b. arm_holding b.
gen_stacks/done : gen_stacks -o 1.
gen_stacks/more : 
  gen_stacks -o exists b. on_table b * gen_stack b * gen_stacks.
gen_stack/clear : gen_stack B -o clear B.
gen_stack/more  : gen_stack B -o exists b. on b B' * gen_stack b. 
\end{verbatim}

This signature says: in order to build a blocks world, build an arm and a
set of block stacks. The arm can either be free or holding a block. A set
of block stacks can be empty, or it can contain a block stack starting with
a new block index, where that block is on the table, along with the rest 
of the set of block stacks. A block stack is indexed by its top block, and
that block can either be clear, or have another block on top of it that
becomes the new block stack index.

\subsection{Generative Property Preservation}

We now define what it means for program transitions to preserve
generative properties.

\begin{definition}
  A transition $\Delta, A \to \Delta, B$ preserves a generative
property $\langle \Sigma_{gen}, \Delta_0 \rangle$ 
iff for all $\Delta$, whenever $\Delta_0 \stepsto_{\Sigma_{gen}} \Delta,
A^*$, it is also the case that $\Delta_0 \stepsto_{\Sigma_{gen}} \Delta,
B^*$.
\end{definition}

\newcommand{\genseed}{\{\mathsf{gen}\}}

In particular, for the blocks world example, we can show how to reason that
the \verb|pickup_from_table| rule, enabling the transition
$\Delta, \pr{ot}b,\ \mathsf{af},\ \pr{cl}b
\to
\Delta, \pr{ah}b$, preserves the invariant by showing that:

\begin{proposition}
If
\[
  \genseed \to_{\siggenbw} 
  \Delta, \pr{on\_table}b,\ \mathsf{arm\_free},\ \pr{clear}b
\]
then
\[
  \genseed \to_{\siggenbw} 
  \Delta, \pr{arm\_holding}b
\]
\end{proposition}

\begin{proofsketch}
  The signature $\siggenbw$ can generate 
  $\Delta, \pr{on\_table}b, \mathsf{arm\_free}, \pr{clear} b$ in only the following way, up
  to concurrent equality:\\
  \begin{enumerate}
    \item Apply rule \verb|gen/bw| to get context \verb|{gen_arm, gen_stacks}|.
    \item\label{armchoice} Apply rule \verb|gen_arm/af| to get context \verb|{arm_free, gen_stacks}|.
    \item Apply some unknown rule sequence to \verb|gen_stacks| to yield an
    unknown context \verb|D1| along with another copy of \verb|gen_stacks|.
\item\label{bstackchoice} Apply \verb|gen_stacks/more| to create $b$ along with its
    \verb|on_table| property.  
    Context is now \verb|{arm_free, D1, on_table b, gen_stack b, gen_stacks}|.
  \item\label{bclearchoice} Apply \verb|gen_stack/clear| to \verb|gen_stack b| to get 
  \verb|clear B|.
  \item Apply some unknown rule sequence to \verb|gen_stacks| to get a side
  effect nonterminal context \verb|D2|, and eventually eliminate all
  nonterminals.\\
  The context is now \verb|{arm_free, D1, on_table b, clear b, D2}|.\\
  The original frame context $\Delta$ must equal \verb|D1, D2|.
  \end{enumerate}


  \textbf{Need to show:} 
  $\genseed \to_{\siggenbw} \Delta, \pr{arm\_holding}b$.\\
  Given the proof trace above, we can modify it selectively to produce the
  context we need.
  We modify step \ref{armchoice} to replace \verb|gen_arm/af| with an
  application of \verb|gen_arm/ah|, which generates a block $b$ that is
  indistinguishable from the specific $b$ in question up to alpha renaming,
  and the predicate \verb|arm_holding b|. We modify steps \ref{bstackchoice}
  and \ref{bclearchoice} to be the null transition, simply linking together
  the trace that generated \verb|D1| to the trace that uses
  \verb|gen_stacks| to generate \verb|D2|, eliminating the terminals that
  were produced as a side-effect. \qed

\end{proofsketch}

To make the above proof sketch formal, we need to give the input trace in
terms of $\epsilon$ notation (a sequence of let-bindings $\llet\ \langle
x_1\dots x_n\rangle = r\ R$ witnessing the transformation
$\genseed \to_{\siggenbw} \Delta, \pr{on\_table}b,\ \mathsf{arm\_free},\ \pr{clear}b$) 
and prove that it really is the only possibility, up to concurrent
equality.  Simmons~\cite{simmons12thesis} carries out such proofs by
proving {\em permutability} lemmas, which say that in any trace, we can
permute the generation of the terminals we care about to the end, then
reason inductively on the remaining trace prefix.  The tediousness and
surfeit of cases in these proofs suggest that formal argument over traces
is the wrong level of abstraction for these proofs---in the case of
generative well-formedness, we do not care about the {\em order} in which
things are generated by the signature but rather only about reachability
between intermediate states of the generative program. An attempt at
visualizing the structure of a generative trace is given in
Figure~\ref{fig:gentraces}.

\begin{figure}
  \caption{Generative trace structure}
  \label{fig:gentraces}
  
  These diagrams depics the generative trace structure for blocks world
  well-formedness of precondition and postcondition of the rule 
  \begin{verbatim}
  pickup_from_table : on_table B * clear B * arm_free -o arm_holding B.
  \end{verbatim}

Precondition trace:

\includegraphics[width=0.8\textwidth]{generative-trace-pre.pdf}

Postcondition trace:

\includegraphics[width=0.7\textwidth]{generative-trace-post.pdf}
\end{figure}

The ability to draw the trace this way makes several assumptions that we
would need to prove about a given generative signature, such as
non-interference between \verb|gen_arm| and \verb|gen_stacks|, and for that
matter the fact that terminals cannot interfere with the trace structure.
All of these assumptions suggest constraining the grammar of generative
signatures themselves in such a way that their traces always have this
tree-like structure, which we will do when we formalize them in an attempt
to automate proof search.

\subsection{Potential for Automation}

We have not yet devised a general algorithm for checking preservation of
generative invariants, and we suggest that without a better layer of
abstraction for reasoning about generative traces, such a task is
intractable: the by-hand proofs frequently involve inductively-proven
lemmas and careful scrutiny of the particular generative signature at hand.
However, generative signatures so far yield the most definitive result of
the three approaches: if we limit programs and generative signatures to
{\em atomic propositions}, invariant preservation is decidable. We give a
proof of this fact in Section~\ref{sec:decide}.

\subsection{Limitations}

Generative signatures resolve the major limitation of consumptive
signatures, the expression of apartness constraints, through the
existential quantifier, which always generates a fresh term distinct from
any others previously in existence. However, this approach is not without
its limitations.

For one thing, we suspect that generative signatures are a substantially
less intuitive way to write specifications than, for instance, the
first-order formulas of meta-linear logic discussed in
Section~\ref{sec:metaLLic}. While meta-linear logic is a fairly direct way
of translating a constraint on a program into a logical formula, generative
invariants require the programmer to {\em operationalize} their understanding 
of the constraint by specifying how to generate contexts that satisfy it.

Second, there is another large class of constraints we cannot describe with
generative invariants: consider describing {\em well-formed graphs} where
edges between nodes are predicates in the program, but we do not want to
create self-loops or multi-edges. However, a new node created may refer
back to an old node. A candidate signature is:

\begin{verbatim}
gen/nodes : gen -o exists n:node. gen_edges n * gen.
gen_edges/edge : gen_edges N * gen_edges N' 
    -o edge N N' * gen_edges N * gen_edges N'.
gen_edges/done : gen_edges N -o 1.
\end{verbatim}

This specification has two problems: first of all, it has a rule with two
nonterminals on the left, which even in the propositional case falls
outside the known-decidable fragment. Second, it cannot avoid generating
self-edges or multi-edges, since nothing stops \verb|N| and \verb|N'| from
having the same node substituted for them. The existential ``fresh
generation'' property does not help us here, because it cannot promise to
keep indices apart in a non-local way, i.e. in a rule other than the one
where the existential appears.

In general, there does not appear to be a way to specify formation
properties in which indices can be shared arbitrarily between predicates
while also enforcing certain apartness constraints. Even with meta-linear
logic, we would need to introduce new apartness primitives on terms in
order to handle such a specification.

\section{Decidability of Invariant Checking for the Propositional Fragment}
\label{sec:decide}

In this section we prove that checking whether a (propositional) generative
invariant holds of a (propositional) linear logic program is decidable.
We do so by modeling propositional generative signatures and programs as
{\em vector addition systems} (first introduced by that name by Karp and
Miller~\cite{karp1969parallel}, although the equivalent Petri nets were
devised earlier~\cite{petri1966communication}) in a way that they can be
treated using known techniques. Specifically, we show how invariant
preservation can be modeled in Presburger Arithmetic, the first-order
theory of natural numbers with inequality and addition, which (despite
impractical computational complexity) happens to be
decidable~\cite{Stansifer1984PAIA}.

\subsection{The Propositional Fragment}

Propositional Ceptre programs are those which do not have any logic
variables ($\Pi$-bound variables), and thus the available transitions at
any point in the program does not depend on the term language available.
Formally, it is simply a restriction of the grammar of rules to

\begin{eqnarray*}
A &::=& S \lolli S \\
S &::=& \one \mid a \mid S \tensor S
\end{eqnarray*}

Instead of refering to these programs as propositional {\em Ceptre}
programs, we will refer to them as propositional {\em Horn} programs by
analogy with Horn clauses in standard logic programming (i.e. ones with no
left-nested implication)~\cite{kowalski1974predicate}, which we believe is
consistent with prior definitions of the Horn fragment of linear
logic~\cite{kanovich1992horn,kanovich1995petri}.

Below is an example of a propositional Ceptre program modeling coin
exchange---\verb|r1| exchances a dime for two nickels, and \verb|r2|
exchanges a quarter for two dimes and a nickel.

\begin{verbatim}
r1 : d -o n * n.
r2 : q -o d * d * n.
\end{verbatim}

Even with such a limited specification, we can already ask all of the
same questions we asked in the beginning:
\begin{itemize}
\item {\bf What is the set of well-formed states?} In this case, it is
  simply any number of quarters, dimes, and nickels.
\item {\bf Which states do we take to be well-formed {\em initial} states?} For
  instance, we might specify that we start with entirely quarters, or we
  might allow any configuration of coins.
\item {\bf What is the set of possible states at {\em quiescence} (termination)
  of the program?} This depends on the set of initial states. If we take the
  initial states to be those with only quarters, then we expect to have a
  multiple of five nickels at the end and no other coins. If we allow any
  set of coins initially, then we will have an arbitrary number of nickels
  (and no other coins) at the end.
\end{itemize}

Indeed, the propositional fragment corresponds with Petri
nets~\cite{murata1989petri} and has been used for quite sophisticated
specifications in the games and interactive storytelling literature as
well as for modeling concurrent and distributed programs. For instance,
Dang et al.~\cite{DangHCS11} specify a slapstick interactive storytelling
scenario in which the player character is attending a party and may take
various actions that have cascading effects, such as lighting a woman's
cigarette:

\begin{verbatim}
light_cig : bored_woman * woman_has_cig * cig_not_lit
            -o woman_has_cig * cig_lit.
\end{verbatim}

...which can lead to objects and animals catching fire. Because the scenes
are all entirely hand-authored and specific to certain characters and
objects, the whole interactive space can be described with atomic
propositions.

Furthermore, first-order logic programs may be expanded to
propositional ones through the process of {\em grounding}, if their term
domains are finite. For instance, if we have the type header

\begin{verbatim}
char : type.
loc  : type.
at char loc : pred.

alice : char.
bob   : char.

den   : loc.
foyer : loc.
\end{verbatim}

Then the rule
\lstinline|rule : at C L -o 1| may be expanded into the following four
rules:

\begin{verbatim}
at alice den   -o 1.
at alice foyer -o 1.
at bob   den   -o 1.
at bob   foyer -o 1.
\end{verbatim}

Such a process is typically not considered computationally practical, since
the number of rules needed to represent a single rule grows combinatorially
with the number of logic variables it has, and checking Presburger formulas
is doubly-exponential in complexity~\cite{fischer1998super}. However, since
our only aim with this proof is to establish decidability (rather than a
tractable algorithm), we note that our proof extends to these programs as
well.

Thus we consider decidability of invariant checking for propositional
programs to be a valuable and novel contribution to the space of validating
interactive media.


\subsection{A Tricky Example}
\label{sec:pathological}

To see why the problem of invariant preservation is a challenge,
consider the following generative signature $\Sigma_{\mathsf{abc}}$.

\begin{verbatim}
g1 : gen -o {a * cs}.
g2 : gen -o {b * c * c}.
g3 : cs -o {c * cs}.
g4 : cs -o {1}.
\end{verbatim}

Note that the class of contexts ($\Sigma_{abc}$, \verb|gen|) describes is
one where an \verb|a| can appear alongside arbitrarily many \verb|c|s, but
a \verb|b| requires {\em exactly two} \verb|c|s alongside it.

Here are two rules that should pass (preserve the invariant):
\begin{enumerate}
\item \verb|a -o {a * c}.|
\item \verb|a * c -o {a}.|
\end{enumerate}

That is, if there is an \verb|a| in the context, we should be able to add
or subtract arbitrarily many \verb|c|s.

On the other hand, here are two rules that should fail (do not preserve the
invariant):
\begin{enumerate}
\item \verb|1 -o {c}|.
\item \verb|c -o {1}|.
\end{enumerate}

That is, we may not arbitrarily remove or generate a \verb|c|. The second
generative rule \verb|g2| permits a context with {\em exactly} one \verb|b|
and two \verb|c|s. Rules are {\em context-sensitive} with respect to
generative invariants; they cannot be reasoned about in isolation.

Thus, our algorithm needs to be able to account for preservation not on a
purely local, or context-free, basis, but rather in a sense that takes into
account {\em all the possible ways} an atom on the left-hand side of the
rule could be generated---which may impose some constraints on the
context---and conclude that, in all of those scenarios, including their
constraints, the right-hand side of the rule could have been generated in
its place.

\subsection{Vector Addition Systems}

In order to draw on prior work in algorithms for validating these systems,
we need to understand them in terms of the formalisms chosen by that prior
work. In particular, a number of useful properties have been shown of 
{\em vector addition systems}, which we employ to obtain decidability.

% (XXX scripty font?)
A {\em vector addition system} (VAS) $V$ is an initial
configuration $v_0 \in \mathbb{N}^n$ for a fixed dimension $n$,
along with a set $T$ of {\em transitions} describing how a configuration
$v$ may evolve. Transitions can be described as vectors $t \in
\mathbb{Z}^n$ along with side conditions of the form $k \in
\mathbb{N}^n$, which imposes the inequality constraint 
$v \geq {k}$.
If the conditions hold of a configuration $v$ (i.e. $v \geq
k$) {\em and} $v + t \geq 0$, the transition
$t$ is said to be {\em applicable} or {\em fireable}, and the
configuration may evolve to $v+t$.

For a transition $(t,k)\in T$ that is applicable in $v$, we
notate a transition relation $\stepsto$, i.e. $v \stepsto v+t$,
which we use in addition to its transitive closure $\stepsto^*$. The set of
configurations $\{ x \mid v \stepsto^* x\}$ is called the {\em reachability
set} of $v$, and can be extended to sets of starting configurations as
well.  VASes are equivalent to Petri nets (see e.g.
~\cite{Leroux2010VASReach,kanovich1995petri}), and for both systems, the
central problem is computing reachability sets: given a set of starting
configurations, what are all of the possible states the system might wind
up in? This problem is known to be decidable
~\cite{peterson1977petri,SacerdoteTenney1977} (however, we do not make
direct use of this fact for our proof).

The correspondence also extends to provability of a sequent in the
propositional Horn fragment of linear logic. Simply put, a VAS transition
rule of the form $(t, k)$ can be interpreted as a forward-chaining linear
logic rule

\[
a_1^{c_1} \tensor \dots \tensor a_n^{c_n} \lolli
  a_1^{c_1+t_1}\tensor \dots \tensor a_n^{c_n+t_n} 
\]

Where $c_i = \mathsf{max}(k_i, -t_i)$ and $a^c$ means $a\tensor \dots
\tensor a$ with $c$ repetitions.

In the other direction, a linear logic program with rules of the form

\[
  a_1^{c_1}\tensor \dots \tensor a_n^{c_n} \lolli
  b_1^{d_1}\tensor \dots \tensor b_m^{d_m}
\]

(with like atoms grouped together without loss of generality)
can be interpreted as a VAS by the following process:
\begin{enumerate}
\item Give an arbitrary canonical ordering for all atoms in the program to
  form the space of possible vectors. Thus each atom $a$ corresponds with an
  index $i_a$ of the vector.
\item For each rule in the above form, create a transition 
  $({t},{k})$ where $t_i=c_i-d_i$ and $k_i=c_i$.
\end{enumerate}

By way of example, all of the rules in $\Sigma_{\mathsf{abc}}$
may be translated to the following vector addition rules
over \verb|<gen, cs, a, b, c>|:
\begin{verbatim}
g1 : <-1,  1, 1, 0, 0>   ; <1, 0, 0, 0, 0>
g2 : <-1,  0, 0, 1, 2>   ; <1, 0, 0, 0, 0>
g3 : < 0,  0, 0, 0, 1>   ; <0, 1, 0, 0, 0>
g4 : < 0, -1, 0, 0, 0>   ; <0, 1, 0, 0, 0>
\end{verbatim}

The initial configuration $\{\mathsf{gen}\}$ is represented by the vector 
$\langle 1, 0, 0, 0, 0 \rangle$.

As mentioned previously, the decidability of this problem does not help us
directly with deciding if a given program rule preserves a generative
invariant. We can, however, recast the preservation problem as a VAS
problem: if we want to check whether a rule $r : A\lolli B$ satisfies a
generative invariant $I$, reformulate $I$ as a vector addition system
$V_I = (i_0, T_I)$. The rule $r$ will correspond to some transition
$(t,k)$ (in a different vector addition system, whose full definition is
not needed).

\begin{definition}
A transition $(t,k)$ {\em preserves the invariant} given by VAS $V_I$ with
starting configuration $i_0$ iff for all configurations $v\geq k$

\[
  i_0 \stepsto^*_{V_I} v
\]

implies

\[
  i_0 \stepsto^*_{V_G} v + t
\]
\end{definition}

The vector $v$ in this definition represents an arbitrary frame
context $\Delta, A$ in which the rule fires.
\footnote{
Note that, in general, the arity of vectors for a generative invariant will
be higher than the arity for the VAS corresponding to the program we want
to check---invariants contain nonterminals that do not appear in program
configurations. So to make this definition more precise, the transition
$i_0 \stepsto v$ should really be $i_0 \stepsto v'$ where $v'_i = v_i$ when
$i$ is within bounds for $v$ and $v'_i=0$ everywhere else.  }

We can make a few more definitions to simplify this characterization:

\newcommand{\reach}[2]{\mathsf{reach}_{#1}(#2)}
\begin{definition}
  The {\em reachability set} of a vector $v$ under a particular VAS $V$ is
  the set of all vectors $v'$ such that the transitive closure of all
  transitions in $V$ can take $v$ to $v'$:
  \[
    \reach{V}{v} = \{v'\mid  v\stepsto^*_V v' \}
  \]
\end{definition}

% XXX numbered definitions?
\begin{definition}
The {\em postset} of a given vector set $S$ along a transition $(t,k)$,
denoted $\mathsf{post}_{(t,k)}(S)$, is the set of all vectors $v'$ such
that there exists a $v \in S$ where $(t,k)$ is fireable on $v$ and $v' = v
+ t$.
\end{definition}

Now we can reword the above criterion for preservation as simply
\[
\mathsf{post}_{(tk_r)}(S) \subseteq S
\]

where $S=\reach{V_G}{c_0}$.

In general, computing the reachability set does not help us answer this
question. However, some (not all) VASes can be expressed as {\em Presburger
Arithmetic formulas}, a subset of first-order logic propositions that may
refer to multiplicaiton and addition of natural numbers (but not
exponentiation). Presburger Arithmetic is known to be decidable, as shown
by Presburger in 1929 (simultaneously with his presentation of the system).
And if the reachability set $S$ of a vector addition system $V_I$
representing an invariant corresponds to a Presburger formula, then the
question of whether a given rule $r$ preserves it ($\mathsf{post}_{(r)}(S)
\subseteq S$) can also be expressed as a Presburger formula.  Thus, what
remains is to show that the particular subset of VASes that correspond with
generative invariants are {\em all} expressible as Presburger formulas.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Presburger Vector Addition Systems}

In general, VASes are not expressible as Presburger Arithmetic formulas.
An explanation of this fact and a characterization of the Presburger
fragment is given in~\cite{Leroux2013PresburgerVAS}.  Briefly speaking, one
can encode exponentiation as a VAS, which is not within the bounds of
Presburger Arithmetic. In this section, we recapitulate Leroux's
characterization of Presburger Vector Addition Systems in terms of how we
use them for generative invariants.

In order to show that generative invariant preservation is decidable, we
need to isolate a fragment of the VAS language that is both suitable to use
for our generative invariants of interest {\em and} expressible in
Presburger Arithmetic.

Leroux shows that the Presburger-expressible VASes are exactly those which
have an equivalent ``flat'' representation. A {\em flat} VAS is one
that can be characterized as a finite sequence of arbitrarily-repeated
finite transition sequences. More formally, consider a {\em word} $w$ to be
a sequence of transitions $t_1\dots t_k$ such that $t_{i+1}$ may always
follow $t_i$. The Kleene closure operator on words $w^*$ means ``$w$
repeated 0 or more times, so long as it applies.'' For instance, the
closure $t^*$ of a transition $t$ corresponding to the linear logic rule $a
\lolli b$ means that $t$ may be applied as many times as there are copies
of $a$ in the configuration it starts with.

A flat language, then is one that can be written as

\[
(w_1)^*\dots(w_n)^*
\]
 
for some finite set of words $w_1 \dots w_n$.

A {\em flatable} VAS is one with the same reachability set as a flat VAS.
One known class of flatable VASs are so-called Basic Parallel Processes, or
BPPs~\cite{esparza1997petri}, which are those corresponding to sets of Horn
linear logic rules with a single premise (or Petri nets where every
transition has a single input). Although this class may sound limiting,
every generative invariant we have studied so far meets this
criterion.~\footnote{Generative invariants for specifying the operational
semantics of programming languages~\cite{simmons12thesis} occasionally
include a second premise, but always a persistent one (premise of the
form $\bang A$). This kind of rule may still be expressible as a BPP so
long as the persistent premise can be represented as a side condition, but
we currently exclude these examples from our proofs.}

There exist published, proven terminating, and implemented methods to
decompose VASs such as BPPs into flat 
languages~\cite{fribourg2000petri,fribourg1997proving}.
These techniques involve iteratively disentangling cyclic rule
dependencies.

As an alternative to automatically finding an equivalent flat
language, we can simply stipulate that a given generative invariant must be
flat. We note that prior to this investigation, there was no rigorous
characterization of what differentiates a {\em generative signature} from
any other linear logic program, and a constraint like this one serves as a
candidate for characterizing the space of suitable signatures.

\subsection{Flat(able) Generative Invariants}

Here is a generative invariant that is {\em not} flat, corresponding
loosely to a propositional erasure of a well-formedness specification for
blocks world.

\begin{verbatim}
g1 : gen -o {t * gen'}.  %% t ~= "on table"; construct a new stack
g2 : gen' -o {b * gen'}. %% b ~= "on"; add a block to a stack
g3 : gen' -o {c * gen}.  %% c ~= "clear"; finish a stack and return
g4 : gen -o {f}.         %% f ~= "arm free"
g5 : gen -o {h}.         %% h ~= "arm holding a block"
\end{verbatim}

If we try to characterize the allowable traces generated by this program as
a grammar, we would write something like $(g_1g_2^*g_3)^*g_4^*g_5^*$,
meaning basically: generate an arbitrary number of stacks of blocks by first generating
a block on the table, then generating an arbitrary number of blocks atop
it, then designating the last one as clear; finally, designate the arm as
either free or holding a block.
\footnote{
We could give a more precise characterization of the signature with
additional regular language constructs, such as $(g_1g_2^*g_3)^*(g_4|g_5|1)$,
since exactly one of $g_4$ or $g_5$ will fire at the end exactly once (or
neither of them will).  However, prior work makes use of only the regular
language constructs of concatenation and repetition, which affects their
mapping into Presburger formulas. The Kleene star can be used to express
this same thing because after $g_4$ fires, neither $g_4$ nor $g_5$ can, and
if $g_4$ fires 0 times, then $g_5$ may fire 0 or 1 times.  }

This specification is not flat because there is ``nested'' looping of the
rule \verb|g2| within the wider loop formed by \verb|g1| and \verb|g3|.
This introduces the constraint that a \verb|t| and \verb|c| both {\em must}
be generated in order for there to be more than zero \verb|b|s. It also
means that, if there are no nonterminals \verb|gen| and \verb|gen'|, the
number of \verb|t|s and \verb|c|s must be the same.

% As a VAS, these rules correspond to transitions (XXX)

% The output of the automatic decomposition technique on this VAS is
% XXX Deco output

However, the set of contexts generated by this signature is equivalent to
those creatable by a flat specification. In fact, the flat specification is
closer to the one we have already seen:

\begin{verbatim}
g1 : gen -o {t * gen * gen'}  %% begin a new stack
g2 : gen' -o {b * gen'}.      %% add a block to a stack
g3 : gen' -o {c}.             %% finish a block stack
g4 : gen -o {f}.        
g4 : gen -o {h}.       
\end{verbatim}


The flat language representing the reachability set is:

\[
(g_1)^*(g_2)^*(g_3)^*(g_4)^*(g_5)^*
\]

In other words, the generative signature can be read operationally as
follows: First, create an arbitrary number of seeds for new block stacks.
Then, if applicable, we add blocks to all of those stacks. Then finish all 
of those stacks by marking their tops as clear. Then optionally generate a
free arm, and if applicable (i.e. if we opted not to generate a free arm)
generate an arm holding a block.

% It is notable that this reading suggests multiple block stacks created
% concurrently, compared to the non-flat specification, which generates
% block stacks in a sequential, iterated process. There also seems to be some
% relationship to tail-call optimization in functional programming, in the
% sense that at no point in the program do we need to refer to a prior word;
% we only need to remember the current (XXX is this useful at all)

%-----------------------------------------------------------%
% \subsection{Results}
% \label{sec:results}

\subsection{Computing Presburger reachability sets}

In general, the postset of a vector set under an iterated word $w^*$ can be
given by binding an existential variable for the number of iterations, then
computing an inductive definition of the union of those sets. 
% XXX check acceleration/fribourg? paper to determine this

More precisely, to recapitulate Leroux's
result~\cite{Leroux2013PresburgerVAS}, define the {\em displacement} of a
word $w = t_1\dots t_k$ to be the vector $\delta(w) = \sum_{j=1}^l t_j$.
Define also for $w$ a configuration $c_w$ such that
$c_w(i) = \mathsf{max}\{ -(t_1+\dots +t_j)(i)\mid 0\leq j \leq k \}$.
This value $c_w$ denotes the minimal configuration for which there exists a
run (applicable transition sequence) labeled by $w$.

Then, the postset of a set $S$ under a single repeated word $w$ is given by
the following Presburger formula:

\[
\mathsf{post}(S, w^*) =
\{x \mid \exists v\in S.
  \exists n\in\mathbb{N}. v \geq c_w \land v + n\delta(w) = x 
\}
\]

Then, for a VAS with starting configuration $c_0$ and represented as the
flat language $w_1^*\dots w_n^*$, a sequence of Presburger sets
$C_i$ denoting the reachability set for the entire system is computed inductively:
\begin{eqnarray*}
C_0 &=& \{c_0\} \\
C_i &=& \mathsf{post}(C_{i-1}, (w_i)^*)
\end{eqnarray*}

The reachability set is given by 
$v\in\mathsf{post^*}(\{c_0\}) = C_n$ where $n$ is the number of words
in the flat sequence.

\subsection{The Algorithm}

% \begin{eqnarray}
% | (\Sigma, \Delta_0) | &=& ...
% \end{eqnarray}

Now that we have a Presburger characterization of the reachability sets of
generative invariants, we can describe what it means for a rule $r : A
\lolli \mon{B}$ to preserve an invariant $(\Sigma, \Delta_0)$ as a
Presburger formula itself. We denote by $|\Delta_0|$, $|\Sigma|$, and so on
the compilation of each of these linear logic program components into their
corresponding vector addition system components.

Let $S = \mathsf{post}^*_{|\Sigma|}(|\Delta_0|)$. The rule $r$ preserves $\Sigma$ iff

\[
\mathsf{post}_{|r|}(S) \subseteq S
\]

In general, a postset $\mathsf{post}_{(t,k)}(S)$ can be denoted logically
as the Presburger set $\{v\mid \exists x\in S. x\geq k \land x+t=v\}$.

And we can write the above subset condition as an implication; in
particular, if $q$ is the number of constants in the specification (i.e.
the width of the vector):

\[
  \forall x,v\in \mathbb{Z}^q. 
  (x\in S \land x \geq k \land x+t = v)
      \limplies v \in S
\]

Whether a given vector is in $S$ is decidable since the set itself is
Presburger computable.


\subsection{End-to-End Example}

Let's revisit the tricky case from Section~\ref{sec:pathological}.

\begin{verbatim}
g1 : gen -o {a * cs}.
g2 : gen -o {b * c * c}.
g3 : cs -o {c * cs}.
g4 : cs -o {1}.
\end{verbatim}

As a vector addition system over \verb|<gen, cs, a, b, c>|, we write this
as a sequence of vector pairs \verb|t ; k|:
\begin{verbatim}
g1 : <-1,  1, 1, 0, 0>   ; <1, 0, 0, 0, 0>
g2 : <-1,  0, 0, 1, 2>   ; <1, 0, 0, 0, 0>
g3 : < 0,  0, 0, 0, 1>   ; <0, 1, 0, 0, 0>
g4 : < 0, -1, 0, 0, 0>   ; <0, 1, 0, 0, 0>
\end{verbatim}

The corresponding flat language is:
\begin{verbatim}
g2*g1*g3*g4*
\end{verbatim}

% As a more precise flat language:
% \begin{verbatim}
% (g2 | (g1(g3*)g4))
% \end{verbatim}

The language compiles to the Presburger formula $C_4$, where

\begin{eqnarray*}
C_0     &=& \{ \verb|<1,0,0,0,0>| \}\\
C_{1}  &=& \mathsf{post}(C_0, \verb|g2|^*)\\
C_{2}  &=& \mathsf{post}(C_1, \verb|g1|^*)\\
C_{3}  &=& \mathsf{post}(C_2, \verb|g3|^*)\\
C_{4}  &=& \mathsf{post}(C_3, \verb|g4|^*)
\end{eqnarray*}

If we omit needless existential quantification over rules that only apply a
fixed number of times, we can easily generate this set by hand:

\begin{eqnarray*}
C_0     &=& \{ \verb|<1,0,0,0,0>| \}\\
C_{1}  &=& \mathsf{post}(C_0, \verb|g2|^*)\\
       &=& \{ \verb|<1,0,0,0,0>|,\\
       & &    \verb|<0,0,0,1,2>| \}\\
C_{2}  &=& \mathsf{post}(C_1, \verb|g1|^*)\\
       &=& \{ \verb|<1,0,0,0,0>|,\\
       & &    \verb|<0,0,0,1,2>|,\\
       & &    \verb|<0,1,1,0,0>|\}\\
C_{3}  &=& \mathsf{post}(C_2, \verb|g3|^*)\\
       &=& \{ \verb|<1,0,0,0,0>|,\\
       & &    \verb|<0,0,0,1,2>|,\\
       & &    \verb|<0,1,1,0,0>|\} \cup \\
       & &  \{v\mid \exists n\in\mathbb{N}. v = \verb|<0,0,1,0,n>|\}\\  
C_{4}  &=& \mathsf{post}(C_3, \verb|g4|^*)\\
       &=& \{ \verb|<1,0,0,0,0>|,\\
       & &    \verb|<0,0,0,1,2>|,\\
       & &    \verb|<0,1,1,0,0>|\} \cup \\
       & &  \{v\mid \exists n\in\mathbb{N}. v = \verb|<0,1,1,0,n>|\}
                \cup\\
       & &  \{v\mid \exists n\in\mathbb{N}. v = \verb|<0,0,1,0,n>|\}
\end{eqnarray*}

If we further restrict this set to exclude states with nonterminals by
intersecting with the set $\{v \mid v_0=0\land v_1=0\}$, we get the set of
well-formed states

\[
  \{\verb|<0,0,0,1,2>|\}\cup
  \{v\mid \exists n \in \mathbb{N}. v = \verb|<0,0,1,0,n>|\}
\]

Or in other words, the contexts $\{b, c, c\}$ and $\{a, c^n\}$ for
arbitrary $n$, as expected.


% The only piece of this formula requiring a quantifier is the repeated
% \verb|g3*|. The reachability set involving \verb|g3*| can be described as:
% 
% \begin{eqnarray*}
%   C_{2B} &=& \mathsf{post}(C_{1B}, \verb|g3*|)\\
%          &=& \{ 
%               x' \mid
%                 \exists n. \verb|<0,1,1,0,0>| + n\verb|<0,0,0,0,1>| = x'
%               \}\\
%         &=& \{
%               x' \mid
%                 \exists n. x' = \verb|<0,0,1,0,n>| \}
% \end{eqnarray*}
% 
% Thus the final solution for the original GI as a Presburger formula is:
% \[
% C = \{ \verb|<0,0,0,1,2>| \} \cup
%     \{\vec{x} \mid \exists n. \vec{x} = \verb|<0,0,1,0,n>|\}
% \]


\subsubsection*{Checking Program Rules}

Now we can work out the decision procedure for the example on a couple of
different program rules. We revisit two examples from 
Section~\ref{sec:pathological}, one that preserves the invariant and one
that does not:

\begin{enumerate}
\item \verb|a -o {a * c}.| (should pass)
\item \verb|1 -o {c}.| (should fail)
\end{enumerate}

Consider the postset of $C$ along each rule: for rule 1, the only part
affected is the second disjunct. $C' = \mathsf{post}_1(C) =$

\[
    \{ \verb|<0,0,0,1,2>| \} \cup
    \{x \mid \exists n. x = \verb|<0,0,1,0,n>|\} \cup
    \{x \mid \exists n. x \ \verb|<0,0,1,0,n+1|\}
\]

But this last unioned set is a subset of 
$\{{x} \mid \exists n. {x} = \verb|<0,0,1,0,n>|\}$
(which can be determined in Presburger Arithmetic by modeling subsethood as
implication).

For rule 2, 

\begin{eqnarray*}
  C'' &=& \mathsf{post}_2(C)\\
      &=& \{ \verb|<0,0,0,1,2>| \} \cup\\
      & & \{{x} \mid \exists n. \verb|<0,0,0,1,n+2>| \} \cup\\
      & & \{{x} \mid \exists n. {x} = \verb|<0,0,1,0,n>|\} \cup\\
      & & \{{x} \mid \exists n. {x} \ \verb|<0,0,1,0,n+1>|\}
\end{eqnarray*}

This set is not a subset of the original, so it fails, as expected.


\subsection{Adequacy and Correctness}

The following lemmas serve as basic sensibility checks on the encoding we
have used to devise our decidability proof.

\begin{proposition}[Adequacy]
Modeling generative invariants as vector
addition systems is sound and complete with respect to derivability (in the
logic) and reachability (in the VAS). That is, formally,
  if $|\Sigma_{gen}, \Delta_0| = \langle V, c_0\rangle$
  then
  $\Delta_0 \to*_{\Sigma_{gen}} \theta$, 
  if and only if
  $c_0 \stepsto^*_{V} |\theta|$.
\end{proposition}

  This property follows by the standard correspondence between linear logic
  derivability and vector addition reachability~\cite{kanovich1995petri}.

\begin{proposition}[Soundness]
If the Presburger formula representing a
rule $r : A \lolli B$ 
preserving a flat generative invariant $\langle \Sigma, \Delta_0 \rangle$ 
has a proof, then for all $\Delta$,
$
\Delta_0 \stepsto^*_{\Sigma} \Delta, A 
$ 
implies 
$
\Delta_0 \stepsto^*_{\Sigma} \Delta, B 
$.
\end{proposition}

\begin{proofsketch}
  Let $S=\mathsf{post^*}_{|\Sigma|}(|\Delta_0|)$.
  Let $(t,k)$ be the transition and constraint of $|r|$.
  By correspondence with vector addition systems, the Presburger formula
  has a proof if and only if
  $\mathsf{post}_{|r|}(S) \subseteq S$.

  The postset along $|r|$ is 
  $\{ v | \exists x\in S. x\geq k \land x + t = v\}$.

  If we consider the vector respresentation of each side of the rule
  $|A|$ and $|B|$, we can write $t$ as $|B|-|A|$ and $k$ as $|A|$.
  So this postset can be written alternatively:
  $\{ v | \exists x\in S. x\geq |A| \land x + |B| - |A| = v\}$.
  \\
  We know $|\Delta, A|\in S$, and we need to show $|\Delta,B|\in S$.\\
  $\Delta$ is in the set of vectors $\{v\}$ specified by the postset,
  because $|\Delta, A|$  is in $S$, is greater than $|A|$ by translation of
  contexts into vectors, and $|\Delta,A|+|B|-|A| = |\Delta, B|$. Thus
  $|\Delta,B| \in S$, as required.\qed

\end{proofsketch}

\begin{proposition}[Completeness]
  Converse of soundness.
  If, for all $\Delta$,
  ($
\Delta_0 \stepsto^*_{\Sigma} \Delta, A 
$) 
implies
($
\Delta_0 \stepsto^*_{\Sigma} \Delta, B 
$)
and there is a flat representation of $\Sigma$, then 
the Presburger formula representing invariant preservation of
$\langle \Sigma, \Delta_0 \rangle$ along $r : A\lolli B$
has a proof.
\end{proposition}

\begin{proofsketch}
  Let $S=\mathsf{post^*}_{|\Sigma|}(|\Delta_0|)$.
The Presburger formula has a proof if and only if 
$\mathsf{post}_r(S) \subseteq S$, i.e. for all $v$,
\[
  (\exists x\in S. x \geq |A|\land x+|B|-|A|=v)
  \limplies
  v \in S
\]
which is what we need to show.

What we know is that 
$\forall \Delta. (\Delta_0\to_{\Sigma}^* \Delta, A)
       \limplies (\Delta_0 \to_{\Sigma}^* \Delta, B)$, 
or in VAS terms,
\[
  |\Delta, A|\in S \limplies |\Delta, B| \in S
\]
Assume a given vector $v$, and
assume of it the premise of what we need to show: that there exists an $x$
such that $x\in S \land x \geq |A|\land x+|B|-|A|=v)$.

Now instantiate the $|\Delta|$ quantified over in our assumption at
$x-|A|$. Now we know $x-|A|+|A| \in S \limplies x-|A|+|B| \in S$. We know
$x \in S$, so now we know $v\in S$, as required. \qed
\end{proofsketch}

% XXX this probably isn't gonna make it into the thesis - just mention it
% in the conclusion.
% \section{Empirical Analysis of Trace Sets}

\section{Conclusion}

We have presented three methods for specifying program invariants, and for
each discussed their potential for automation and their limitations. We 
have also presented a decidability proof for checking invariants of
programs within a large fragment describing most of the programs we have
considered in this thesis. 

We close this chapter with a discussion of a limitation of all three of
these systems, suggesting that there is still a great deal of investigation
to do both in terms of automating specification checks and extending the
expressiveness of specification languages.

\subsection{Limitation: Instance-Dependent Invariants}
\label{sec:instance}

One of our motivating examples for investigating program property proof is
allowing the author to state and enforce {\em playability} constraints. For
an example of a playability constraint, consider spatial navigation
puzzles, such as the dungeon layouts in which locked doors separate some
rooms and keys may be found in some rooms. Gareth Rees has studied this
dungeon structure~\footnote{Article available at
\url{http://garethrees.org/2004/12/01/ocarina-of-time/}.}
in the context of The Legend of Zelda: Ocarina of
Time~\cite{nintendo1998legend}; we replicate their diagram from Figure 3
here:

\includegraphics[width=\textwidth]{zelda-dungeon-solvable.png}

In this diagram, rooms (depicted with capidal letters) with ``Key'' labels
require a key (any small key, indistinguishable) to open them, and rooms
with ``Small key'' labels contain such a key.  For the dungeon to be {\em
solvable} means that every room can eventually be reached by a player
starting in the ``Start'' node.

We can easily give a program specifying the space of player actions for
such a dungeon, which presumably include moving from room to room, picking
up keys, and unlocking rooms that require a key when we have one:

\begin{verbatim}
door : type.
room : type.

entity : type.
player : entity.
small_key : entity.

adjacent room door room : bwd.
% defined by domain instance

locked door : pred.
open door : pred.

at entity room : pred.
holding entity entity : pred.

move : at player R * adjacent R D R' * open D -o at player R'.
open_door : $at player R * adjacent R D R' * locked D 
            * holding player small_key
              -o open D.
pickup_key : $at player R * at small_key R
              -o holding player small_key.
\end{verbatim}

Defining ``accessibility'' between locations requires some kind of
recursive specification, which could perhaps be stated as a
backward-chaining linear logic program or as a generative invariant of some
kind.  But note that any invariant that would describe solvability of a
dungeon depends crucially on the specific initial configuration, since it
is really a property of that configuration as well as of the program---and
none of the techniques we have discussed so far encompass such a statement.
Temporal logics, such as those used in model checking, present promising
techniques that could account for properties like these, wherein it is
feasible to exhaustively check the possible configuration
space~\cite{clarke1999model}.  In lieu of a concrete solution, however, we
posit this example as a potential benchmark for game invariant
specification techniques going forward.

% \subsection{Summary}
% 
% In summary, we have presented three techniques for stating and proving
% invariants of linear logic programs: meta-linear logic, consumptive
% invariants, and generative invariants. For meta-linear logic,
% we have isolated a fragment for which we conjecture that an algorithm for
% checking first-order programs is easily devisable. Such an algorithm could
% check simple well-formedness constraints such as ``The player in a game is
% always at some location'' and ''Blocks in the blocks world domain are
% always in linear stacks.'' We have also given a decidability proof for
% checking generative invariants in the propositional fragment of the
% language, which we conjecture extends to many interesting examples in the
% literature even if it does not cover our entire space of use cases.
% 

