\newcommand{\pig}{\mathpr{pig}}
\newcommand{\wolf}{\mathpr{wolf}}
\newcommand{\straw}{\mathpr{straw}}
\newcommand{\sticks}{\mathpr{sticks}}
\newcommand{\bricks}{\mathpr{bricks}}
\newcommand{\strawhouse}{\mathpr{straw\_house}}
\newcommand{\stickhouse}{\mathpr{stick\_house}}
\newcommand{\brickhouse}{\mathpr{brick\_house}}
\newcommand{\pigwins}{\mathpr{pig\_wins}}
\newcommand{\wolfwins}{\mathpr{wolf\_wins}}


\section{Introduction}

%% XXX some kind of cute quote would be good here. lewis carrol?

{\em What makes up a story?} 
In computer science research, this question has been invoked repeatedly by
artificial intelligence and computational linguistics researchers. The
motivation for answering it includes several potential applications:
autonomous agents that can collaborate on building stories with
people ({\em interactive
storytelling})~\cite{Cavazza2002,mateas1999narrative}; computational
understanding of narrative structure from natural language text ({\em
narrative extraction})~\cite{chambers2008unsupervised}; and the automatic
generation of stories, a kind of investigation on the boundaries of
computational creativity ({\em narrative
generation})~\cite{meehan1976metanovel}.

Besides these computational applications, understanding narratives can lend
insight into human learning and cognition: narratives are an important way
that humans make sense of the world around
us~\cite{herman2003narrative,bruner1990acts}.  Narrative researchers have
achieved consensus that {\em causality} is an important aspect of stories
for narrative models to
capture~\cite{trabasso1985causal,adams1989causality,mallon2000structure,dahlstrom2012persuasive},
even if it only barely scratches the surface of interesting facets of
narrative~\cite{richards2009advancing}.  To understand causality in
stories, we first need to be able to break them apart into events between
which causal relationship may be found.

As described in Chapter~\ref{chapter:intro}, we are interested not only in
the structure of existing stories but in systems that allow or describe 
{\em collaborative construction} of story. Understanding a story as made of
separable pieces is a good first step for this purpose, too, since
narrative play involves at least one human mediating between story
components.
 
In this chapter, we aim to give a foundational account of narrative
systems. We are interested in representations of narrative that can be
interpreted by a computer for the sake of analysis, generation, and
interaction, while also using high-level language constructs that are not
bound by particular machine models. 

We present {\em intuitionistic linear logic} (ILL) as a formalism to serve
as the foundation for modeling narratives and their structure. Linear
logic, first devised by Girard~\cite{girard87linear}, was originally
suggested as a suitable representation for narratives by Bosser et
al.~\cite{bosser2010linear}, whose work we largely recapitulate here. 


\section{Modeling Narratives}

We aim to give a composable formalism for narrative, so we must make clear
what aspects of narrative we aim to make formal. In particular, we make the
distinction between {\em fabula} and {\em sujet} made by Russian formalists
in the 1920s~\cite{brown1974formalist}: the fabula is the plot events, the
``what happens'' part of a story, whereas the {\em sujet} is the {\em
telling} or orchestration of story elements into a (usually linear)
digestible tale. In this work we aim only to formalize the {\em fabula},
while recognizing that there are many interesting research questions in the
formalization of sujet and relating fabula to sujet (see, for example, the
conflicting structure between the two in the film {\em
Memento})~\cite{nolan2000memento} (see Figure ~\ref{fig:memento}).

\begin{figure}
  \caption{Fabula versus Sujet in Memento}
  \label{fig:memento}

  \includegraphics[width=\textwidth]{fabula-sujet-memento.png}

  \footnotesize{Diagram created by Steve Aprahamian, from
  \url{https://en.wikipedia.org/wiki/File:Memento\_Timeline.png},
  used on the conditions of the Creative Commons license described
  therein.}

\end{figure}

The formal modeling of fabula has a long history in AI research, but until
recently has depended on ad-hoc, genre-specific ontologies such as Propp's
``morphology of a folktale''~\cite{propp2010morphology}. Instead, we would
like the particular genre or conflict structure to be {\em reflected} in
the formalism, but not {\em constrained} by it. The core structure we would
like to constrain with the formalism instead includes things like
causality, action, and change.  These properties are essential to enforcing
{\em coherence} of a narrative~\cite{young1999notes}.

Folktales as a domain contain many interesting examples for the study of
fabula, since their tellings vary with every storyteller, but their
component events remain relatively consistent. 
Let us consider as an example the folktale {\em The Three Little Pigs}.
This folktale consists of the following narrative events:

\begin{enumerate}
  \item The mother pig sends her three baby pigs away from home, warning
    them about a big bad wolf.
  \item The first pig builds a house out of straw.
  \item The second pig builds a house out of sticks.
  \item The third pig builds a house out of bricks.
  \item The big bad wolf visits the straw house and blows the house down.
  \item The big bad wolf visits the stick house and blows the house down.
  \item The big bad wolf visits the brick house and attempts to blow it
    down, but cannot.
\end{enumerate}

Even within formalization of fabula, there are many conflicting ideas about
what parts of this story to include in narrative state and how to model
relationships between these narrative elements. Some candidates for
narrative components include:

\begin{itemize}
\item Characters in the story: the three little pigs, their mother, and the
big bad wolf.
\item Resources or props in the story that are needed to drive the story
forward, such as the straw, sticks, and bricks that the pigs use to build
their houses, and subsequently the houses themselves.
\item Relationships between any of the above entities: feelings of family
and allyship between the pigs; feelings of enmity between the pigs and the
wolf; locations and possessions of characters.
\item Scenes, or story events, which require availability of the above
story elements and may change them. {\em The first pig builds a house out
of straw} might be understood as changing the state of the pig, the straw,
and the house.
\item Establishment of initial configurations for characters, resources,
and relationships. The first line of the story establishes the three little
pigs, their mother, and the wolf as characters in the story.
\item Endings, or narrative goals established by the author. ``Happily ever
after'' is a common goal ending for fairy tales; in variants of 
The Three Little Pigs, the defeat of the wolf is an important constant.
\end{itemize}

Finally, we may also need to represent relationships between {\em scenes}.
These relationships may not be represented explicitly by an author, but
they are important for computational applications of story.  For instance,
in the context of interactive stories, we may need to include or derive
links between story scenes to represent alternatives. In the context of
story {\em analysis}, we may care about the ability to determine {\em
causal} relationships between scenes, as mentioned in the introduction.

\subsection{Linear Logic by Example}
\label{sec:llbe}

Modeling a story in logic means mapping the above concepts to the
constructs of logic, which is to say {\em propositions} and the notion of
{\em derivability} between propositions. Propositions can either be
{\em atomic} or {\em compound}. An atomic proposition is something like
``The straw house is standing,'' which we might abbreviate with the
notation $\strawhouse$. Compound propositions are how we combine atomic
propositions into more complex statements, analogous to English usage of
{\em and}, {\em or}, and {\em implies} to combine statements. The logical
analog of these conjoning words are the {\em connectives}.

The following linear logic proposition could model the story event of the
wolf blowing down the straw house:

\[
\wolf \tensor \strawhouse \lolli \wolf
\]

The atomic propositions shown here are $\wolf$ and $\strawhouse$.  The
connectives are $\lolli$ (``lolli,'' linear logic implication) and
$\tensor$ (``tensor,'' linear logic conjunction). $\tensor$ binds more
tightly than $\lolli$, so the rule can be read as, ``If the wolf is present
and the straw house is standing, then transition to a state where (only)
the wolf is present.''

Note that this reading avoids the word {\em implies} or an {\em if-then}
reading, although we asserted that $\lolli$ is linear logic's form of
implication. In linear logic, derivability is defined in such a way that it
represents {\em state change} more than inference about permanent truth.
This mechanism lets us treat propositions as {\em resources}, or in this
case, slices of narrative state, and implication (embodied by derivability)
can be read as replacement of one piece of state with another.

Logical connectives need not always form compound propositions: for
instance, the ``connective'' $\one$ represents the empty or null resource,
and we can use it to model the removal, rather than replacement, of a piece
of state. For instance, the following proposition models removing the wolf
from the story:

\[
\wolf \lolli \one
\]

On the other hand, this proposition models introducing the wolf into the
story from out of thin air:

\[
\one \lolli \wolf
\]

Another connective in linear logic, $\with$ (``with''), allows us to
represent choices between alternatives. The following proposition models
a transition from the $\pig$ state (representing a pig with no house) to
either a straw, stick, or brick house:

\[
\pig \lolli 
  \strawhouse\ \with\ \stickhouse\ \with\ \brickhouse
\]

Note that we could equally well represent this choice-yielding event as
instead a choice between events:

\[
(\pig \lolli \strawhouse)\ \with\ (\pig \lolli \stickhouse)
  \ \with\ (\pig \lolli \brickhouse)
\]


So far, all of these propositions are just syntax; we have not attempted to
explain what they mean in terms of logical derivability, except at an
intuitive level. But one of the more important omissions we have made is
the status of these propositions that represent story events: how do we
intend to compose them?

Linear logical implications do not really accurately model concrete story
events: they instead describe a {\em possible} event that could occur given
the fulfillment of the antecedent. We are instead describing a story {\em
world}, a set of possibilities that we intend to give rise to a story or
set of stories through logical deduction.

In this sense, we can imagine composing implications $E_1\dots E_n$ 
representing story events as the compound proposition

\[
E_1 \tensor \dots \tensor E_n
\]

meaning that all events are simultaneously available for use. However, if we
have two events $A \lolli B$ and $A \lolli C$, and $A$ is some narrative
state that we only expect to happen once, then one of the events will go
unused, which is disallowed in linear logic.

Sometimes we {\em want} to enforce the usage of a given event because we
are interested in {\em narrative drive}: the idea that an author needs
certain scenes to occur to fulfill certain dramatic intent. In this case,
the tensoring-together of narrative events should suffice, and any
conflicting scenes would need to be carefully crafted as alternatives
(e.g. $A \lolli B\ \with\ C)$.

On the other hand, sometimes we are interested in modeling a more
exploratory possibility space where some events may not take place at all,
and others may take place multiple times. The unary connective $\bang$
gives us exactly this meaning: $\bang A$ is a proposition $A$ that may be
ignored or repeated. Thus, we can represent the more exploratory story
world as follows:

\[
\bang E_1 \tensor \dots \tensor \bang E_n
\]

We hereafter refer to a proposition of the form $\bang (A \lolli B)$
% (or $\bang (\forall x. A \lolli B)$) 
as a {\em rule}. Since we may refer to rules multiple times in a story, we
will often name them using the syntax $r : R$, where $r$ is a name and $R$
is a rule.

In the next section, we seek to clarify the meaning of these propositions
and simplify our representations by explaining them in terms of a few
carefully-considered, meta-logical principles.


\section{Linear Logic}

Any representation of fabula needs to include models of {\em action} and
{\em change}, phenomena for which many formalisms have been investigated
over several
decades~\cite{mccarthy1969some,kowalski1989logic,lamport1994temporal}.  The
cited works effectively solve the variability problem by indexing every
proposition with a time parameter and modeling actions as incrementing that
parameter. As a consequence, they all need to explicitly manage {\em
inertia}, or the fact that when a rule describes changes of one part of the
world state from time $t$ to $t+1$, the remaining parts of the world state
are updated in $t+1$ to retain their state at time $t$.

Linear logic is an approach to the logical modeling of action and change
that does not depend on explicit time indexing. This approach has the
advantage that it is possible to conceive of distinct parts of the state
changing independently of one another.  

We note that, unlike Girard's original formulation of logic, our chosen
formulation is {\em intuitionistic} in that we only consider sequents
$\Delta\vdash A$ where $A$ is a single proposition, rather than a
disjunction of multiple propositions. The intuitionistic version of linear
logic (ILL) was first presented by Girard and Lafont~\cite{girard87ill}.
We select it mainly for its computational interpretations as described by
Andreoli~\cite{andreoli1992logic}, although we note that this choice may
not be canonical, and classical linear logic bears investigating as an
alternative in future work.

Intuitionistic linear logic was later
reformulated~\cite{chang2003judgmental} according to the methodology of
logic design espoused by Gentzen and
Martin-L{\"{o}}f~\cite{gentzen1935untersuchungen,martin1996meanings} in
which inference rules operate over {\em judgments}, or meta-logical syntax
pertaining to propositions, and inference rules also obey certain
meta-theoretic properties that make soundness of the logic easy to
establish, and proof search within the logic easy to automate. This
methodology, which includes giving a {\em sequent calculus} formulation of
the logic, is described below.

First, we assert that to be a {\em logic} means to have a notion of
{\em consequence}:

\[
A_1,\dots, A_n \vdash A
\]

The above syntax can be read, ``$A$ is a consequence of $A_1,\dots, A_n$,''
where $A$ and all $A_i$ are propositions (defined by the particular logic).
Such a statement is called a {\em sequent}, and an arbitrary collection of
assumptions $A_1,\dots,A_n$ is often notated as $\Delta$ and called the
{\em context}.

A logic may have {\em inference rules} of the form

\[
\infer
{J}
{J_1 & \dots & J_n}
\]

where each $J$ and $J_i$ is a sequent, the $J$ at the root of the rule is
the {\em conclusion} sequent, and each $J_i$ is a {\em premise} that must
be satisfied in order for the inference to be valid.

A {\em proof} of sequent $J$ is a composition of inference rules forming a
tree whose leaves are rules with no premises and whose root is $J$.

Finally, to count as a logic, the notion of consequence must be {\em
transitive}; that is, if it is possible to build proofs of 
$\Delta \vdash A$ and $\Delta', A \vdash C$, then we can also build a proof
of $\Delta', \Delta \vdash C$.

This property, having a transitive notion of consequence, is also known as
Admissibility of Cut~\cite{gentzen1935untersuchungen}.
It is a meta-property of a system of inference rules and part of what gives
it meaning. There are other such properties, called structural properties,
that have often been previously considered part of what it means to be a
logic:\footnote{In the literature, the terminology
``consequence relation'' has sometimes implied these properties. We
depart from this tradition by using ``consequence'' without including
weakening and contraction by default.}

\textbf{Weakening}.
If $\Delta \vdash C$ then $\Delta, A \vdash C$: in other words, adding
unneeded assumptions does not affect derivability.

\textbf{Contraction}.
If $\Delta, A, A \vdash C$ then $\Delta, A \vdash C$: in other words,
having two copies of a proposition available is not any better than a
single copy.

These properties encapsulate the idea that in a proof from assumptions,
each assumption may be used arbitrarily many times to reach the goal.
Linear logic, however, denies these properties, leading to a ``use exactly
once'' treatment of assumptions in a proof. Put another way, if ordinary
logic treats the context $\Delta$ as a {\em set} of assumptions, in linear
logic $\Delta$ can be thought of as a 
{\em multiset}~\cite{girard1995linear} i.e. the multiplicity of assumptions
matters.

Thus linear logic's notion of consequence $\Delta \vdash A$ embodies a sort
of conservation property, and can be read ``Resources $\Delta$ may be
transformed into $A$.'' Connecting this notion back to narrative, we can
think of $\Delta$ as an initial narrative situation and $A$ as a narrative
ending.

To include the $\bang$ connective in linear logic, we need to reintroduce a
context that {\em is} subject to weakening and contraction. If we change
our basic judgment (sequent form) to

\[
\Gamma; \Delta \vdash A
\]

where assumptions in $\Gamma$ may be weakened and contracted, then we have
the machinery we need to define $\bang$, effectively reintroducing
ordinary, persistent notions of logical fact into the by-default
resource-oriented logic. In this sense, intuitionistic linear logic can be
thought of as a refinement on ordinary intuitionistic logic.

In this more foundational account of the logic, we can rewrite our story
world representation from Section~\ref{sec:llbe} as simply a specification
for the context $\Gamma$: instead of imagining

\[
\bang E_1 \tensor \dots \tensor \bang E_n
\]

as an assumed proposition in $\Delta$, we can instead stipulate that

\[
\Gamma = E_1, \dots, E_n
\]

We can now describe the mapping between story world and logical sequent
that we will use as our primary model of representation going forward. The
sequent $\Gamma; \Delta \vdash A$
represents a story world with rules (and persistent facts) in $\Gamma$,
initial narrative configuration described by $\Delta$, and narrative goal
(or story ending) $A$. 

Now that we have sketched the judgmental framework in which we intend to
model story worlds, we can finally give the formal definition of linear
logic as a sequent calculus.

\subsection{Intuitionistic Linear Logic: Sequent Calculus}
\label{sec:ill}

In a sequent calculus, every connective is defined by two rules:
instructions for how to prove it when it appears on the right-hand side of
the turnstile ($\vdash$) in a sequent, and instructions for how to {\em
use} it when it appears on the left-hand side of the turnstile. These
instructions come in the form of {\em left} and {\em right} inference
rules. We now present the inference rules of linear logic that define the
connectives we need for narrative modeling.

The $\tensor$ connective models simultaneous conjunction between two
resources:

\[
\infer[\tensor R]
{
\Gamma; \Delta_1,\Delta_2 \vdash A \tensor B
}
{
\Gamma; \Delta_1 \vdash A
&
\Gamma; \Delta_2 \vdash B
}
\qquad
\infer[\tensor L]
{
\Gamma; \Delta, A \tensor B \vdash \gamma
}
{
\Gamma; \Delta, A, B \vdash \gamma
}
\]

From a proof search perspective, we read these inference rules from the
bottom up. So the right rule says that a proof of $A\tensor B$ can be
formed from a context that can be partitioned into pieces $\Delta_1$ and
$\Delta_2$, which can prove $A$ and $B$ respectively.  The left rule says
that an assumption of $A\tensor B$ can be interpreted as two separate
assumptions, $A$ and $B$.

Note that the persistent context $\Gamma$ is simply repeated in every
sequent in this rule (i.e. from a proof search perspective, it is passed
unchanged to both subgoal sequents). The $\Gamma$ context will be
``carried through'' in this manner for all inference rules that do not
refer to it; that is, all rules except those defining $\bang$.

The rules for the tensorial unit, $\one$, are as follows:
% one
\[
\infer[\one R]
{
\Gamma; \cdot \vdash \one
}
{
}
\qquad
% \mathrm{(no\ }\one L\mathrm{)}
\infer[\one L]
{
\Gamma; \Delta, \one \vdash \gamma
}
{
\Gamma; \Delta \vdash \gamma
}
\]
The null resource may be proven only when the linear context $\Delta$ is
empty, and it may be used by simply removing it from the context.


The rules for implication ($\lolli$) follow a similar pattern to those for
$\tensor$, except inverted with respect the the left and right rule:
% lolli
\[
\infer[\lolli R]
{
\Gamma; \Delta \vdash A \lolli B
}
{
\Gamma; \Delta, A \vdash B
}
\qquad
\infer[\lolli L]
{
\Gamma; \Delta_1, \Delta_2, A\lolli B\vdash \gamma
}
{
\Gamma; \Delta_1 \vdash A
&
\Gamma; \Delta_2, B \vdash \gamma
}
\]
The right rule for $\lolli$ says that to prove $A\lolli B$, add $A$ to our
set of assumptions and work on proving $B$. The left rule requires again
that we {\em partition} the context into the part that proves the
antecedent $A$, and another part that, when given the consequent $B$,
continues to prove the original goal.

% plus
% \[
% \infer[\oplus R_1]
% {
% \Gamma; \Delta \vdash A \oplus B
% }
% {
% \Gamma; \Delta \vdash A
% }
% \qquad
% \infer[\oplus R_2]
% {
% \Gamma; \Delta \vdash A \oplus B
% }
% {
% \Gamma; \Delta \vdash B
% }
% \qquad
% \infer[\oplus L]
% {
% \Gamma; \Delta, A\oplus B\vdash \gamma
% }
% {
% \Gamma; \Delta, A \vdash \gamma
% &
% \Gamma; \Delta, B \vdash \gamma
% }
% \]

The inference rules for $\with$ are given below -- but note that we do not
use this connective in the remaining chapters of the thesis, so
understanding it is optional.

% with
\[
\infer[\with R]
{\Gamma; \Delta \vdash A \with B}
{\Gamma; \Delta \vdash A & \Gamma; \Delta \vdash B}
\qquad
\infer[\with L_1]
{\Gamma; \Delta, A\with B \vdash \gamma}
{\Gamma; \Delta, A \vdash \gamma}
\qquad
\infer[\with L_2]
{\Gamma; \Delta, A \with B \vdash \gamma}
{\Gamma; \Delta, B \vdash \gamma}
\]

The right rule says that to prove $A\with B$, we need to be able to prove
$A$ and $B$ {\em from the same context} $\Delta$. The left rule says that
if we have a choice $A\with B$, we can make either selection to continue
the proof.


The rules for $\bang$ are the ones that interact with the persistent
context $\Gamma$:

% bang
\[
\infer[\bang R]
{
\Gamma; \cdot \vdash \bang A
}
{
\Gamma; \cdot \vdash A
}
\qquad
\infer[\bang L]
{
\Gamma; \Delta, \bang A \vdash \gamma
}
{
\Gamma, A; \Delta \vdash \gamma
}
\]

The $\bang R$ rule says that a resource $A$ can be thought of as a fact
$\bang A$ so long as it is proven {\em only} with factual propositions (the
ones in $\Gamma$). Thus the rule enforces that the linear context $\Delta$
must be empty.

The left rule allows us to move a $\bang A$ from the linear context into
the persistent context as just $A$.

Finally, there are two structural rules that interact with the contexts
$\Delta$ and $\Gamma$.
One of these is the $\mathsf{copy}$ rule:

% copy
\[
\infer[\mathsf{copy}]
{
\Gamma, A; \Delta \vdash \gamma
}
{
\Gamma, A; \Delta, A \vdash \gamma
}
\]

This rule allows us to copy any persistent assumption $A$ into $\Delta$
(without also removing it from $\Gamma$, meaning we may do this as many
times as needed).

Finally, we need a structural rule for proving (and equivalently
using) atomic propositions:

\[
\infer[\mathsf{init}]
{\Gamma; p \vdash p}{}
\]

This rule allows us to finish a branch of proof search by observing that
the context and goal match up exactly (modulo persistent assumptions
$\Gamma$).

We could imagine a more general $\mathsf{init}$ rule

\[
\infer[\mathsf{init}']
{\Gamma; A \vdash A}{}
\]

where $A$ can be any proposition, not just atomic $p$, but it turns out
that this rule is {\em admissible} in a well-designed logic, i.e. the rules
already allow it for any given $A$. Furthermore, testing for its
admissibility is a way to determine that the logic is well-designed; it is
considered an internal completeness property.

\subsection{Some Derivation Examples}

We can see each of the connectives $\lolli$, $\tensor$, $\with$, and
$\bang$ as internalizing some property of the judgmental framework:
$\lolli$ internalizes consequence, $\tensor$ internalizes the comma for
conjoining contexts, $\with$ internalizes a choice between two
alternatives, and $\bang$ internalizes persistence.

In future chapters of this thesis, we will use all of these connectives
frequently except for $\with$; in fact, refinements on this formalism will
not include $\with$. We omit $\with$ because in settings where all
implications are rules (live in the persistent context), occurrences of
$\with$ to the right of a rule can be accounted for by adding multiple
rules. In other words, a rule of the form $A \lolli B\ \with\ C$ can be
replaced by two rules, $A \lolli B$ and $A \lolli C$, in a sound and
complete way.~\footnote{Rules of the form $A\with B\lolli C$, on the other
hand, do not have a direct translation into the $\with$-less fragment.
However, we have not encountered a need for such rules in any of the
examples we investigate.}

We now prove this fact---that $\with$ is an unneeded connective in the
context of persistent rules---which will also serve as an example of how to
put the inference rules above together into proofs.

Claim:
\[
\bang (A \lolli B\ \with\ C)
\]
is interderivable with
\[
\bang(A\lolli B)\tensor\bang(A \lolli C)
\]

That is, we need to show that 

\[
\bang (A \lolli B\ \with\ C) \vdash \bang(A\lolli B)\tensor\bang(A \lolli C)
\]

is derivable, as is its converse

\[
\bang(A\lolli B)\tensor\bang(A \lolli C) \vdash \bang (A \lolli B\with C)
\]


Recall that a {\em proof} is a composition of inference rules forming a
tree whose leaves are rules with no subgoals and whose root is the sequent
being proved. We form a proof by applying inference rules to the current
goal sequent, resulting in a new set of goal sequents (the premises to the
rule), until there are no more premises.

The first derivation works as follows:

Let $\Gamma = A \lolli B\ \with\ C$.

\[
\infer[\bang L]
{
\cdot; \bang (A \lolli B\ \with\ C) \vdash \bang(A\lolli B)\tensor\bang(A \lolli C)
}
{ \infer[\tensor R]
  {
    A \lolli B\ \with\ C; \cdot 
      \vdash \bang(A\lolli B)\tensor\bang(A \lolli C)
  }
  { \infer[\bang R]
    { \Gamma; \cdot 
      \vdash \bang(A\lolli B)
    }
    { \infer[\lolli R]
      {\Gamma; \cdot 
        \vdash A\lolli B
      }
      { \infer[\mathsf{copy}]
        { \Gamma; A \vdash B
        }
        {\infer[\lolli L]
          {\Gamma; A\lolli B\with C, A \vdash B}
          { \infer
            {\Gamma; A \vdash A}{}
            &
            \infer[\with L_1]
            {\Gamma; B \with C \vdash B}
            {\infer{\Gamma; B \vdash B}{} 
            }
          }
        }
      }
    }
    &
    \infer[\bang R]
    { \Gamma; \cdot 
      \vdash \bang(A \lolli C)
    }
    {\infer[\lolli R]
      { \Gamma; \cdot
        \vdash A \lolli C
      }
      {\infer[\mathsf{copy}]
        { \Gamma; A \vdash C }
        { \infer[\lolli L]
          {\Gamma; A \lolli B\with C, A \vdash C}
          {\infer
            {\Gamma; A \vdash A}{}
            &
            \infer[\with L_2]
            {\Gamma; B\with C\vdash C}
            {\infer{\Gamma; C \vdash C}{}
            }
          }
        }
      }
    }
  }
}
\]

The leaves of this derivation are all of the form $\Gamma; A \vdash A$
which we know to be derivable for any proposition $A$ by way of the
identity admissibility theorem.

The second derivation works as follows:

Let $\Gamma = A\lolli B, A \lolli C$ in the derivation below.

\[
\infer[\tensor L]
{ \cdot; \bang(A\lolli B)\tensor\bang(A\lolli C)
    \vdash
      \bang (A \lolli B\ \with\ C)
}
{
  \infer[\bang L^2]
  { \cdot; \bang(A\lolli B), \bang(A\lolli C)
    \vdash
      \bang (A \lolli B\ \with\ C)
  }
  {
    \infer[\bang R]
    {A\lolli B, A\lolli C;\cdot
      \vdash
      \bang (A \lolli B\ \with\ C)
    }
    {
      \infer[\lolli R]
      {\Gamma;\cdot \vdash A \lolli B\ \with\ C}
      {
        \infer[\with R]
        {\Gamma;A \vdash B\ \with\ C}
        {
          \infer[\mathsf{copy}] 
          {\Gamma; A \vdash B}
          {
            \infer[\lolli L]
            {\Gamma; A\lolli B, A \vdash B}
            {
              \infer{\Gamma; A \vdash A}{}
              &
              \infer{\Gamma; B \vdash B}{}
            }
          }
          &
          \infer[\mathsf{copy}]
          {\Gamma; A \vdash C}
          {
            \infer[\lolli L]
            {\Gamma; A \lolli C, A \vdash C}
            {
              \infer{\Gamma; A \vdash A}{}
              &
              \infer{\Gamma; C \vdash C}{}
            }
          }
        }
      }
    }
  }
}
\]




\section{Alternative and Simultaneous Story Structure}
\label{sec:altsim}

Linear logic provides the tools we need to specify story worlds in such a
way that we can define relationships of interest between story events, but
there are still quite a few choices about which components to model in the
story world that give rise to different event relationships.  Let us now
be more specific about what kinds of event relationships we would like to
aim to model, and explain how we can use linear logic to model them.

\subsection{Alternative Storylines}

One kind of narrative structure of interest to interactive storytelling is
{\em alternative storylines}. This structure is present in any Choose Your
Own Adventure or Twine game: a reader is presented with multiple choices
and, upon selecting one, is cut off from the other choices until replay (or
until that scene is presented again, in the case of cyclic stories).  These
stories have a natural representation as a {\em graph}, with story scenes
(or {\em passages} in Twine parlance) modeled by graph vertices, and
possible consequences $y$ of a scene vertex $x$ modeled as directed edges
from $x$ to $y$.  Sometimes this kind of narrative structure is called {\em
branching}, but by calling attention to {\em alternatives} rather than
branching, we aim to include story graphs that are not simply trees: paths
that diverge (branch) may converge in a later scene, and divergence is not
given any priority over convergence.

% \begin{figure}
%   \caption{Depiction of alternative storyline structure in Twine.}
%   \label{fig:twinegraph}
%   \centering
% 
%   \includegraphics[width=0.5\textwidth]{tamara-twine.png}
% \end{figure}

The graph structure just described is depicted in the Twine editor for the
sake of the author to visualize their story structure. 
% An example Twine graph (or ``node map'') is shown in
% Figure~\ref{fig:twinegraph}.
To relate this idea to our example, we can render the Three Little Pigs
fabula as a Twine story in which the choices represent the alternatives
between building a house out of straw, sticks, or bricks:

\begin{centering}
\includegraphics[width=0.8\textwidth]{tlp-twine.png}
\end{centering}

This depiction of the story structure can be seen as containing three
alternative storylines, each corresponding to one ``playthrough'' of the
game. Two of those playthroughs end in the ``bad'' passage in which the
wolf blows down the house, and the third ends in the ``good'' passage in
which the wolf cannot blow down the house. The story graph is a more
compact representation of these three stories that makes use of the shared
structure between the first and second story, as well as their shared
beginning. It can be understood as a {\em potential narrative} because each
interaction with a player generates one of the three stories.

\begin{figure}
  \caption{Four structural patterns in branching narrative.}
  \label{fig:branching}

  Diagrams created by Sam Kabo Ashwell, used with permission.

  Color key: red nodes are endings representing failure; green nodes are
  endings representing success; blue nodes are the start of the story;
  orange nodes are choice points; yellow nodes are waypoints (they only
  have a single out-edge).

  \centering

  The {\em time cave}, in which branches never converge and every path is
  distinct:
\includegraphics[width=0.9\textwidth]{cyoa-timecave.png}

The {\em branch-and-bottleneck}, in which outward-branching alternatives
  occasionally re-converge on common passages:
\includegraphics[width=0.9\textwidth]{cyoa-bottlebranch.png}

  The {\em gauntlet}, in which one particular path serves as the backbone
  for the story, and all other paths lead to dead ends:
\includegraphics[width=0.9\textwidth]{cyoa-gauntlet.png}

  The {\em open map}, in which symmetric connections are made between
  nodes, often used to simulate reversible movement through physical space:
\includegraphics[width=0.5\textwidth]{cyoa-openmap.png}
\end{figure}

Alternative structure in stories already yields many interesting authoring
choices. In an online article, Sam Kabo Ashwell reviews several patterns in the
edges-as-alternatives graph structure for interactive storytelling, such as
those in Figure~\ref{fig:branching}.
~\footnote{The article is available at\\
\url{https://heterogenoustasks.wordpress.com/2015/01/26/standard-patterns-in-choice-based-games/}.}

However, many rich interactive storytelling examples make use of complex
state tracking, such as inventories in parser interactive fiction. These
graphs do not depict how the story will vary depending on that state.

\subsection{Simultaneous Storylines}
\label{sec:simultaneous}

Alternative structures are one way to conceptualize a story in terms of
constituent pieces, but they are not the only way.
Rather than imagining making choices from the perspective of one of the
three little pigs, we might like to model all of the characters' actions
and interactions together. We can map a narrative onto a graph in a
different way: edges are characters in certain states of the narrative, and
nodes are scenes where those characters interact.

In one strip of the online comic XKCD, Randall Munroe depicts several
popular movie plots in this style, such as this plot graph for The Lord of
the Rings:~\footnote{Larger version can be found at
\url{https://xkcd.com/657/}.}

\includegraphics[width=\textwidth]{lotr-large.png}

Along the vertical axis, characters are placed near one another to
represent sharing a scene or far apart to represent independent activity.
The horizontal axis is the forward progression of time. The {\em ring}, an
imporant narrative resource, is drawn as an overlay atop the character
holding it.

This version of narrative structure lends itself to the {\em analysis} of
a plot more readily than alternative structure: we can see, for instance,
that climactic moments correspond to the convergence of a large number of
characters, and we can trace the thread of a particular character or group
of characters to examine their overall influence on the plot. More
relevantly to narrative play, we can envision the story in terms of
autonomous, interacting characters who might have independent motives,
interiority, and relationships.

To model the Three Little Pigs narrative in this way, we need to break down
our story into smaller component pieces: one for each pig and the wolf, and
perhaps also the building materials they use for their houses. If we are
more precise than Munroe's drawing about what exactly a ``scene'' does, in
terms of how it transforms these narrative resources, then we can draw the
story's simultaneous structure as follows:

\includegraphics[width=\textwidth]{3lp-concurrent.pdf}

This diagram represents something more {\em static} than the Twine game
version: it does not present clear affordances for interaction. However, it
is also more {\em systematic}, in that it forces us to imagine a world
model in which the events in the story could logically and physically take
place.  What we present in the next sections is a formal setting in which
{\em both} of these valuable aspects of structural expression are
available.

\subsection{Alternatives and Simultaneity in Linear Logic}

Linear logic's resource-oriented mechanisms enables connectives that neatly
map onto alternative ($A\with B$) and simultaneity ($A\tensor B$).  Due to
the ``use once'' principle of assumptions in linear logic, these manifest
as two forms of logical conjunction (``and''). The first one of these we
will explain is $A\tensor B$, which means that resources $A$ and $B$ are
available simultaneously.

The $\tensor$ and $\lolli$ connectives together give us the ability to
write propositions such as $\pig \tensor \bricks \lolli \brickhouse$,
modeling a resource exchange that characterizes the ``pig builds a brick
house'' scene in The Three Little Pigs. Here, the $\tensor$ connective
serves to conjoin the two atomic $\pig$ and $\bricks$ propositions into a
more complex proposition. There is a {\em unit} of the $\tensor$ connective
indicating the null resource, spelled $\one$.\footnote{For $\one$ to be a
unit of $\tensor$ means that, for any $A$, $A\tensor \one$ is equivalent to
(interprovable with) $A$ and $\one \tensor A$.}

The other form of conjunction, $A\with B$, means that a choice
between $A$ and $B$ is available. This connective lets us model the first
passage in our Twine game representation of The Three Little Pigs as
$\pig \lolli \brickhouse \with \strawhouse \with \stickhouse$.
~\footnote{There is a unit of $\with$ as well, spelled $\top$, which we do
not include here because it is not needed for our examples.}

To model stories in linear logic, we map atomic propositions onto pieces of
narrative state. In the case of purely alternative story structures, a single
piece of narrative state representing each scene/passage will suffice. In
the case of narratives with simultaneous structure, propositions will model
potentially more complex narrative elements and their relationships.

Here is a model of the additive story world for Three Little Pigs:

Let $\Delta = $

\begin{eqnarray*}
&\{
 \pig \lolli (\strawhouse\ \with\ \stickhouse\ \with\ \brickhouse),\\
&\strawhouse \lolli \wolfwins,\\
&\stickhouse \lolli \wolfwins,\\
&\brickhouse \lolli \pigwins,\\
&\pig
\}
\end{eqnarray*}

Stories will be proofs of the sequent

\[
\Delta \vdash \wolfwins
\]

or

\[
\Delta \vdash \pigwins
\]

Here is a model of the simultaneous story world, in which we make use of
linear logic's notion of simultaneity ($\tensor$) to introduce three copies
of the {\em pig} narrative resource, and we also represent finer-grained
narrative resources such as the building materials for the pigs' houses:

Let $\Delta = $

\begin{eqnarray*}
&\{
   \pig \tensor \straw \lolli \strawhouse,\\
 & \pig \tensor \sticks \lolli \stickhouse,\\
 & \pig \tensor \bricks \lolli \brickhouse,\\
 & \wolf \tensor \strawhouse \lolli \wolf,\\
 & \wolf \tensor \stickhouse \lolli \wolf,\\
 & \wolf \tensor \brickhouse \lolli \brickhouse,\\
 & \wolf, \pig, \pig, \pig, \straw, \sticks, \bricks
\}
\end{eqnarray*}

Stories will be proofs of the sequent

\[
\Delta \vdash \brickhouse
\]

Note that in both of these models, scenes (represented as propositions of
the form $A \lolli B$) appear on the same level as atomic narrative
resources like $\pig$. This means that the logic will enforce a {\em use
exactly once} semantics for those scenes, embodying a kind of {\em
narrative drive} (we are required to include those scenes to prove the
sequent). If we want to make a scene $A$ optional, all we need to do is
create a choice between that scene and the null resource: $A \with \one$.
Persistence ($\bang A$) can be used to model stories where scenes may
repeat an arbitrary number of times.

% \begin{itemize}
% \item Story state: what pieces are relevant? Characters, items, feelings,
% knowledge? ( XXX Emphasize that these can be concrete and abstract.)
% ({\em narrative resources})
% \item Scenes, or events that cause state transitions. 
%   A scene specification needs to say what prompts it (causes it to happen) and 
%   what changes it makes to the story state.
% \end{itemize}
% 

\subsection{Proofs as Stories}
\label{sec:proofs-as-stories}

Finally, we can present concretely the mapping of stories onto proofs. 
For the Twine-based version of the story, where story events are related as
alternatives, we can model the story world with $\Gamma =$

\begin{eqnarray*}
  r_1 &:& \pig \lolli (\strawhouse\ \with\ \stickhouse\ \with\ \brickhouse)\\
  r_2 &:& \strawhouse \lolli \wolfwins\\
  r_3 &:& \stickhouse \lolli \wolfwins\\
  r_4 &:& \brickhouse \lolli \pigwins
\end{eqnarray*}

The initial state $\Delta_0$ will be the single resource $\pig$,
corresponding to the initial Twine passage.

Here is a derivation corresponding to the story of the pig that builds the
straw house in the additive story world:
\[
  \infer[\lolli L (r_1)]
{\Gamma; \pig \vdash \wolfwins}
{
  \infer
  {\pig \vdash \pig}
  {}
  &
  \infer[\with L_1]
  {\strawhouse\ \with\ \stickhouse\ \with\ \brickhouse \vdash \wolfwins}
  {
    \infer[\lolli L (r_2)]
    {\strawhouse \vdash \wolfwins }
    {
      \infer{\strawhouse\vdash\strawhouse}{}
      &
      \infer{\wolfwins\vdash\wolfwins}{}
    }
  }
}
\]

The above derivation can also be thought of as a proof that the wolf can
win (against a pig who makes a straw or stick house). Below is a proof that
the pig can win , representing the story in which the pig builds the brick
house:

\[
  \infer[\lolli L (r_1)]
{\pig \vdash \pigwins}
{
  \infer
  {\pig \vdash \pig}
  {}
  &
  \infer[\with L_3]
  {\strawhouse\ \with\ \stickhouse\ \with\ \brickhouse \vdash \pigwins}
  {
    \infer[\lolli L (r_4)]
    {\brickhouse \vdash \pigwins }
    {
      \infer{\brickhouse\vdash\brickhouse}{}
      &
      \infer{\pigwins\vdash\pigwins}{}
    }
  }
}
\]

Every different proof with $\Gamma; \Delta_0 \vdash \gamma$ at its root
corresponds to a different potential narrative embodied by the alternative
structure.

To describe {\em simultaneous} relationships between story events, we need
to divide up the monolithic state of ``which Twine passage are we in'' into
smaller pieces, such as each pig, the wolf, the building materials the pigs
use to make their houses, and the completed houses.

The story ending is now not a a single fact (the wolf or the pig winning) 
but rather some composition (specifically, a $\tensor$ conjunction) of
outcomes for different narrative resources.

In this version of the story, $\Gamma =$
\begin{eqnarray*}
  r_1 &:& \pig \tensor \straw \lolli \strawhouse\\
  r_2 &:& \pig \tensor \sticks \lolli \stickhouse\\
  r_3 &:& \pig \tensor \bricks \lolli \brickhouse\\
  % \smallskip\\
  r_4 &:& \wolf \tensor \strawhouse \lolli \wolf\\
  r_5 &:& \wolf \tensor \stickhouse \lolli \wolf\\
  r_6 &:& \wolf \tensor \brickhouse \lolli \brickhouse
\end{eqnarray*}

The initial configuration for the story is the state
\[ \Delta_0 = \{\pig,\pig,\pig,\straw,\bricks,\sticks,\wolf\}
\]

And we can create proofs of the sequent

\[
\Delta_0 \vdash \brickhouse
\]

to represent stories ending with just the brick house standing, i.e. the
canonical Three Little Pigs folktale ending.
Here is a proof that the brick house can be the only one left standing,
representing the canonical Three Little Pigs story:

Let $\DD_1 =$

\[
    \infer[\tensor R]
    {\pig,\bricks\vdash \pig\tensor\bricks}
    {\pig \vdash \pig & \bricks \vdash \bricks}
\]

Let $\DD_2 =$
\[
  \infer[\tensor R]
      { \pig,\straw \vdash \pig \tensor \straw }
      { \infer{\pig \vdash \pig}{} & \infer{\straw \vdash \straw}{} }
\]

Let $\DD_3 =$
\[
  \infer[\tensor R]
    { \pig, \sticks \vdash \pig\tensor\sticks }
    {\infer{\pig \vdash \pig}{} & \infer{\sticks \vdash \sticks}{}}
\] 

Let $\DD_4 =$
\[
\infer[\tensor R]
          {\wolf, \strawhouse \vdash \wolf \tensor \strawhouse}
          {\infer{\wolf \vdash \wolf}{} &
           \infer{\strawhouse\vdash\strawhouse}{}}
\]

Let $\DD_5 =$
\[
\infer[\tensor R]
          {\wolf, \stickhouse \vdash \wolf \tensor \stickhouse}
          {\infer{\wolf \vdash \wolf}{} &
           \infer{\stickhouse\vdash\stickhouse}{}}
\]



in

\[
  \infer[\lolli L (r_3)]
  {
    \Delta_0 \vdash \brickhouse
  }
  { \DD_1
    &
    \infer[\lolli L (r_1)]
    { \brickhouse, \pig, \pig, \straw, \sticks, \wolf \vdash \brickhouse
    } 
    { \DD_2
      &
      \infer[\lolli L (r_2)]
      {
        \strawhouse, \brickhouse, \pig, \sticks, \wolf \vdash \brickhouse
      }
      { \DD_3
        &
        \infer[\lolli L (r_4)]
        {
          \stickhouse, \strawhouse, \brickhouse, \wolf \vdash \brickhouse
        }
        {
          \DD_4
          &
          \infer[\lolli L (r_5)]
          {
            \stickhouse, \brickhouse, \wolf \vdash \brickhouse
          }
          {
            \DD_5
            &
            \infer[\lolli L (r_6)]
            {
              \brickhouse, \wolf \vdash \brickhouse
            }
            {
              \infer
              {
                \brickhouse,\wolf \vdash \wolf\tensor\brickhouse
              }
              {
                \infer{\wolf\vdash\wolf}{} &
                \infer{\brickhouse\vdash\brickhouse}{}
              }
              &
              \infer
              {
                \brickhouse\vdash\brickhouse
              }
              {}
            }
          }
        }
      }
    }
  }
\]

Note the lopsided structure of the above proof: we only apply 
$\lolli L$ rules up the entire tree except to derive rules' premises from
the context. The proof could almost be read as a sequence of rule
applications $r_3; r_1; r_2; r_4; r_5; r_6$ that navigate from the bottom
sequent (in which the context represents the initial story configuration)
to the top-right sequent (in which the context represents the final story
configuration). 
On the other hand, by tracking exactly {\em which} resources in the context
are consumed and produced by each rule application, we can extract a
partial ordering between these rule applications, yielding the diagram
depicted in Section~\ref{sec:simultaneous}.
The rule sequence plus its input-output dependency links with other rules
is exactly the information captured in the formal proof term syntax that we
interpret as stories in Chapter~\ref{chapter:llpng}.


Another note about the above proof is that it is not the only one that may
follow from the story world rules and initial configuration $\Gamma;
\Delta_0$.  We can derive different outcomes where two or three of the
houses are left standing, i.e.

\[
\Delta_0 \vdash \brickhouse \tensor \stickhouse
\]

and

\[
\Delta_0 \vdash \brickhouse \tensor \stickhouse \tensor \strawhouse
\]

That these sequents are provable suggests that even in our ``simultaneous''
story world, there is some alternative structure to consider---i.e. there
is nondeterminism in the system of inference rules, and several might
apply.

To see what stories these unconventional endings might give rise to, let us
examine a proof of the sequent $\Delta \vdash
\brickhouse\tensor\strawhouse\tensor\stickhouse$ (where we abbreviate the
right-hand side of the sequent $A$).

Let $\DD_6 =$

\[
\infer[\tensor R]
{
  \brickhouse,\strawhouse,\strawhouse\vdash A
}
{
  \infer{\brickhouse \vdash \brickhouse}{}
  &
  \infer[\tensor R]
  {
    \strawhouse,\stickhouse 
        \vdash \strawhouse\tensor\stickhouse
  }
  {  
    \infer{\strawhouse \vdash \strawhouse}{}
    &
    \infer{\stickhouse \vdash \stickhouse}{}
  }
}
\]

in

\[
  \infer[\lolli L (r_3)]
  {
    \Delta \vdash A
  }
  { \DD_1
    &
    \infer[\lolli L (r_1)]
    { \brickhouse, \pig, \pig, \straw, \sticks, \wolf \vdash A
    } 
    { \DD_2
      &
      \infer[\lolli L (r_2)]
      {
        \strawhouse, \brickhouse, \pig, \sticks, \wolf \vdash A
      }
      { \DD_3
        &
        \infer[\lolli L (r_6)]
        {
          \strawhouse,\brickhouse,\stickhouse,\wolf \vdash A
        }
        {
          \infer[\tensor R]
          {
            \brickhouse,\wolf \vdash \wolf\tensor\brickhouse
          }
          {
            \infer{\wolf\vdash\wolf}{} &
            \infer{\brickhouse\vdash\brickhouse}{}
          }
          &
          \DD_6
        }
      }
    }
  }
\]

Again reading the named rules used in the proof from bottom to top, we can
see we have a shorter story wherein after each pig builds their house, the
wolf simply visits the brick house first and is eliminated from the
narrative state there, leaving all three houses standing.

Some computational narrative researchers would consider such a story to be
poorly formed, particularly according to popular Western story aesthetics:
it can hardly be argued that this narrative has any {\em conflict}.
Furthermore, two characters in the story (the straw house and brick house
pig) are seemingly only referred to once, when they build their houses, and
never interact with the narrative again, making their role in the story
seem inessential.  Riedl and Young ~\cite{riedl2004intent} have
investigated means of manipulating similar inference systems (planning) to
introduce conflict by way of individual character goals that compete over
shared resources. In future work we would like to investigate the
applicability of their techniques to linear logic.



\section{First-Order Linear Logic}

One advantage of working with the logical methodology we have chosen is
that it is easy to enrich the logic with orthogonal constructs.
For instance, we can enrich our logic of atomic propositions to allow us to
state more complex relationships between entities, such as $\mathsf{at}\
\pig\ \strawhouse$ to represent location or $\mathsf{has}\ \pig\ \straw$ to
represent possession. If we additionally introduce a {\em quantifier}
connective $\forall$ (``for all''), we can write a proposition modeling a
{\em parametric} action where a pig in {\em any} location $L$ where there
is a building material $M$ can be replaced by the pig possessing $M$:

\[
\forall L,M. 
  \mathsf{at}\ \pig\ L \tensor \mathsf{at}\ M\ L\ 
    \lolli\ \mathsf{has}\ \pig\ M
\]

For modeling pre-established narratives like The Three Little Pigs,
modeling the story world at this level of detail and parametricity seems
unnecessary. However, for the invention of more flexible story worlds prone
to expressive collaboration from a human interactor, parametric rules like
this one become essential.

The creators of social physics systems like Prom Week emphasize that 
creating a wide possibility space for narrative unfoldings is essential to
the player's discovery of ``emergent solutions and surprising, yet
satisfying, outcomes.''~\cite{mccoy2011prom} Expressing the kinds of rules
that make up Prom Week's social physics engine (Comme il
Faut~\cite{mccoy2010comme}) requires that they not be specialized to any
particular character in the story but depend only on certain properties of
characters and their relationships. The first-order extension of linear
logic enables us to express rules of this form.

Most prior work on the use of linear logic to model stories and games focus
{\em only} on the non-parametric, or {\em propositional}, fragment of the
logic (see Section~\ref{sec:petri}), and so its range of considered
examples has mostly been limited to hand-authored, branching narratives.
In Chapter~\ref{chapter:llpng}, we will show how first-order linear logic
scales to account for a richer narrative possibility space. We note that,
as a side-effect, we will be able to use the same formalism to describe
Twine games, command-line (``parser'') interactive fiction, and multi-agent
social models like Comme il Faut, and compare the narrative structures that
arise from them.


\section{Related Work}

Bosser et al.~\cite{Bosser11} similarly identify structures in stories that
can be identified as simultaneous and alternative, also modeled in linear
lofic. In their case, simultaneous structure is represented by proof terms
that record uses of the $\tensor R$ rule as ``stories in parallel.''
However, such proofs still sequentialize story events that we identify as
formally independent from one another. Our notion of independence aligns
better with the permutability of proof rules than with the commutative
structure of the linear context.

We identify two other formalisms that are very closely related to linear
logic for story formalization: planning and Petri nets.

\subsection{Planning}

Interactive storytelling research communities have historically used
planners (such as STRIPS~\cite{Fikes1971STRIPS} and
IPOCL~\cite{young1994decomposition}) to model and generate
stories~\cite{young1999notes,charles2001character,riedl2010narrative}. The planning
approach to modeling actions, i.e. by designating facts as {\em
preconditions}, {\em deleted} by the action, and {\em added} by the action,
has a great deal in common with modeling actions as linear logic
implications. In fact, Masseron et al.~\cite{Masseron93a} have shown how
linear logic can be used to support planning and equate a proof to a plan.
Others have demonstrated the use of linear logic for specific problems
thought of as typical planning problems~\cite{Dixon09b,Dixon2009}.

So, in the interactive storytelling domain, linear logic can effectively be
seen as a logic-based alternative to planning. We see the advantages to a
basis in logic as twofold: first, that a long tradition of logics
connecting to human epistemology means a wide range of epistemological
extensions are available, and there is vast precedent for designing logics
so that their different judgments (and corresponding connectives) may fit
together, composing into richer formalisms. For example, this precedent is
what allows us to seamlessly extend propositional linear logic with
first-order quantification. Another, less-explored example is combining
linear logic's resource orientation with logical connectives for {\em
knowledge} of specific actors~\cite{garg2006linear}, which we
hypothesize could be quite fruitful for narrative modeling.

% The second advantage we identify is by analogy with the power of 
% {\em proofs-as-programs} as a basis for developing theories of 
% computation and programming languages~\cite{Wadler14PropsAsTypes}: there is
% valuable knowledge transfer between the fields of logic and type theory due
% to investigating the applicability of techniques in one field to the other;
% accounting for these theories in other formalisms like algebra and category
% theory yields yet more insights. We propose that, by
% mapping constructs from narratology into logic, similarly fruitful insights
% may be found on both sides of the mapping. 
% XXX maybe this is too vague/confusing. % XXX cite more stuff?

There are a few more technical differences between the expressivity of
linear logic and planning as formalisms. For instance, in linear logic, the
{\em multiplicity} of a fact matters: we cannot write $\brickhouse \lolli
\wolf$ to represent ``deleting'' the $\brickhouse$ fact in the same way we
can in planning, because there may be other copies of the $\brickhouse$
resource available that we do not account for. (We would consider these
statements equivalent, though, when an {\em invariant} of the program
includes having exactly zero or one of a certain resource.) A consequence
of this fact is that linear logic {\em can} refer to multiple instances of
something (like money) without propositions indexed by a natural number,
while planning cannot.

Another (related) difference is that fact deletion in planning does not
require that the fact being deleted is actually {\em present} for the rule
to fire. In linear logic, all ``deleted'' facts are also ``preconditions.''
Finally, planners typically support {\em negation} of facts as
preconditions for actions. Both of these constructs (unconditional
deletion, and negation as failure) are inexpressible in linear logic,
and in fact are inconsistent with purely logical characterization in
general, because they do not maintain the transitivity of the consequence
relation. However, when we consider the extension of our approach into a
more practical programming language, we do add support for similar idioms 
(see Chapter~\ref{chapter:ceptre}).

\subsection{Petri Nets}
\label{sec:petri}

Petri nets~\cite{murata1989petri} are a formalism studied in the 1970s
primarily for concurrent computation. They are easily interpreted in a
graphical languages of nodes and arcs, where nodes may be either {\em
places} (represented with a circle) or {\em transitions} (represented as a
rectangle), where arcs connect places to transitions and transtions to
place. Each place may have zero or more {\em markings} on it.

A given Petri net and configuration of markings may evolve to a new
configuration as follows: if all of the places that point to (have an arc
to) a given transition are marked, the transiton may {\em fire}, or remove
one marking from each input place and add a marking to each output place.
Places may have arcs to multiple transitions, suggesting nondeterminism
in the system.

Petri nets may be understood as a restricted fragment of linear logic: a
Petri net place is modeled by an atomic linear logic proposition, and a
Petri net transition matches up to a linear logic implication of the form
$\bang(a_1\tensor\dots\tensor a_n\lolli b_1\tensor\dots\tensor b_m)$, where
each $a_i$ is an input place to the transition and $b_i$s are output
places. Every rule must be persistent (thus the $\bang$ in front) so that
it can model a transition that may fire arbitrarily many times.

The {\em reachability} problem in Petri nets---whether it is possible for a
given configuration to evolve through arbitrarily many rule firings to
another configuration---was shown equivalent to provability in this
fragment of linear logic by Kanovich.~\cite{kanovich1995petri}

Note that this correspondence does not take into account the first-order
extension of linear logic. For some first-order programs, it may be
possible to {\em ground} them, i.e. give an equivalent propositional
program, by instantiating every rule with every possible term given in the
domain (assuming the domain is finite, which it may not be), but even when
this is possible it results in a combinatorial explosion of the state
space. This may make Petri nets as a formalism less scalable than
first-order linear logic as an authoring tool.

Despite this limit in expressiveness, quite a few applications of
Petri nets to games and interactive storytelling have been explored:
first, Vega et al. investigate their use in game
design~\cite{natkin2004new}; Ara{\'u}jo and Lic{\'\i}nio use them to model
game mechanics~\cite{araujo2009modeling}; Dang et al. use the equivalent
fragment of linear logic to validate interactive story
scenarios~\cite{DangHCS11,DangCA13}; and my coauthors and I use that same
fragment for generation of story variants~\cite{Martens13:LPNMR} on the
fabula of Flaubert's novel {\em Madame Bovary}~\cite{Emma}.  The main {\em
benefit} of the limited expressiveness is that it is possible to do
exhaustive analysis, since proof search on that fragment (i.e.
reachability for Petri nets) is decidable.~\cite{mayr1984algorithm}

Petri nets also have the advantage of enjoying a direct visual
representation that nicely illustrates the relationship between alternative
and simultaneous structure. The Petri net in Figure~\ref{fig:petripig} illustrates the Three
Little Pigs story world given in Section~\ref{sec:simultaneous}, and to find
potential alternative structure we simply look for places (circles) with
multiple out-edges.

\begin{figure}
\caption{Petri net for the simultaneous Three Little Pigs story world.}
\label{fig:petripig}
\centering
\includegraphics[width=0.8\textwidth]{3lp-petri-net.pdf}
\end{figure}

Finally, we note that a Petri net-inspired system of markings and
transitions, called Machinations, has been built as a visual game design
tool ~\cite{dormans2011simulating}. Later work formalized the core of this
system and its semantics (``micro-machinations'')~\cite{van2014adapting} to
find that they differ substantially from Petri nets, losing the
correspondence with linear logic.


\section{Conclusion}

We have presented linear logic as a formalism that supports two kinds of
structure in narrative fabula, namely {\em alternatives} and 
{\em simultaneity}. We have built upon prior narrative modeling
methodologies to map entities, relationships, states, events, stories, and
story outcomes onto corresponding logical and proof-theoretic notions,
completing the conceptual basis on which the remainder of this thesis
builds.

In particular, we have demonstrated several core properties of narrative
structure that correspond to the fundamental mechanisms of linear logic.
Bosser et al.~\cite{bosser2010linear} point out three such characteristics 
of computational stories: \textbf{\emph{generativity}}, or the derivability of a
variety of different story unfoldings given the same beginning and ending
conditions; \textbf{\emph{variability}}, or the open world assumption
characterized by the story rules' independence from the initial story
configuration; and \textbf{\emph{narrative drive}}, or the enforcement of certain
story rules (scenes) being used in the proof. These properties emerge from
the logic in the form of a nondeterministic inference system, the 
{\em hypothetical judgment} (i.e.  presence of the context $\Delta$ as an
essential part of sequents), and the absence of {\em weakening} making it
possible to enforce the usage of assumptions.

We additionally observe the correspondence between linear logic connectives
and {\em alternative} and {\em simultaneous} relationships between story
events. Our observation of the logic's ability to model alternatives is
effectively the same as the {\em variability} property mentioned above, but
the {\em simultaneity} observation was mainly portrayed as causality in
prior work. We posit that simultaneity offers a more operational reading of
the narrative structure, in which we can imagine several moving parts to a
complex interactive narrative, whose independent evolutions compose into a
coherent story. Many works of interactive fiction already use such ideas by
incorporating persistent state (such as player inventory and tracking of
game history), but the simple alternative models of these fictions (e.g.
Ashwell's diagrams in Section~\ref{sec:altsim}) do not depict the more
complex story variability that arises from them.  Reed and
Garbe~\cite{reed2014ice} introduce the term {\em combinatorial narrative}
to suggest centralizing the idea of complex narrative states in interactive
story authoring, and we posit that linear logic would make a good candidate
for modeling and reasoning about those works.

In the next chapter, we will show how to put computers to use on the
mathematical formalism presented here in the form of {\em logic
programming} to extract a computational interpretation of story modeling in
linear logic. Namely, we extend our mapping to account for story world (or
potential narrative) as a program that, when run, generates coherent
stories according to the authored rules. 


