%for a more compact document, add the option openany to avoid
%starting all chapters on odd numbered pages
\documentclass[12pt,openany]{cmuthesis}

% This is a template for a CMU thesis.  It is 18 pages without any content :-)
% The source for this is pulled from a variety of sources and people.
% Here's a partial list of people who may or may have not contributed:
%
%        bnoble   = Brian Noble
%        caruana  = Rich Caruana
%        colohan  = Chris Colohan
%        jab      = Justin Boyan
%        josullvn = Joseph O'Sullivan
%        jrs      = Jonathan Shewchuk
%        kosak    = Corey Kosak
%        mjz      = Matt Zekauskas (mattz@cs)
%        pdinda   = Peter Dinda
%        pfr      = Patrick Riley
%        dkoes = David Koes (me)

% My main contribution is putting everything into a single class files and small
% template since I prefer this to some complicated sprawling directory tree with
% makefiles.

% some useful packages
\usepackage{times}
\usepackage{fullpage}
\usepackage{graphicx}
\usepackage{amsmath}
\usepackage[numbers,sort]{natbib}
\usepackage[backref,pageanchor=true,plainpages=false, pdfpagelabels, bookmarks,bookmarksnumbered,
%pdfborder=0 0 0,  %removes outlines around hyper links in online display
]{hyperref}
\usepackage{subfigure}

% Approximately 1" margins, more space on binding side
%\usepackage[letterpaper,twoside,vscale=.8,hscale=.75,nomarginpar]{geometry}
%for general printing (not binding)
\usepackage[letterpaper,twoside,vscale=.8,hscale=.75,nomarginpar,hmarginratio=1:1]{geometry}

% Provides a draft mark at the top of the document. 
\draftstamp{\today}{DRAFT}

% custom macros
\input{cm-macros.tex}

\begin {document} 
\frontmatter

%initialize page style, so contents come out right (see bot) -mjz
\pagestyle{empty}

\title{ %% {\it \huge Thesis Proposal}\\
{\bf Programming Interactive Worlds\\ with Linear Logic}}
\author{Chris Martens}
% \date{June 2015}
\date{\today}
\Year{2015}
\trnumber{}

\committee{
Frank Pfenning, Chair \\
Karl Crary \\
Andr\'{e} Platzer \\
Roger Dannenberg\\
Anne-Gwenn Bosser
}

\support{}
\disclaimer{}

% copyright notice generated automatically from Year and author.
% permission added if \permission{} given.

\keywords{Programming Languages, Game Design, Interactive Simulation,
  Interactive Storytelling, Interactive Fiction}

\maketitle

% \begin{dedication}
% For my dog
% \end{dedication}

\pagestyle{plain} % for toc, was empty

%% Obviously, it's probably a good idea to break the various sections of your thesis
%% into different files and input them into this file...

\begin{abstract}
XXX A short summary.
\end{abstract}

\begin{acknowledgments}
XXX write this last.
\end{acknowledgments}



\tableofcontents
\listoffigures
\listoftables

\mainmatter

%% Double space document for easy review:
%\renewcommand{\baselinestretch}{1.66}\normalsize

% The other requirements Catherine has:
%
%  - avoid large margins.  She wants the thesis to use fewer pages, 
%    especially if it requires colour printing.
%
%  - The thesis should be formatted for double-sided printing.  This
%    means that all chapters, acknowledgements, table of contents, etc.
%    should start on odd numbered (right facing) pages.
%
%  - You need to use the department standard tech report title page.  I
%    have tried to ensure that the title page here conforms to this
%    standard.
%
%  - Use a nice serif font, such as Times Roman.  Sans serif looks bad.
%
% Other than that, just make it look good...

\chapter{Introduction}

\part{Linear Logic Programming for Narrative Generation}

\chapter{Programming With Linear Logic}

A citation to CLF:~\cite{CLF}

This chapter should explain via INT paper example.


\chapter{Generating Narratives with Proof Search}

\section{Proofs as Stories}

\section{Concurrent Traces}

\section{Playable Traces}




\part{Interactive Linear Logic Programs}

\chapter{Language Design}

\section{Introduction}

Both planning and linear logic have been used
previously to study games, especially in the interactive storytelling
domain~\cite{mateas2003faccade, Porteous10, DangHCS11,  medler2006scribe}.  For
instance, Dang et. al. model story choices as linear logic propositions and use
a theorem prover to validate the space of possible story outcomes.  Bosser et.
al.~\cite{Bosser11} use the Coq theorem prover to carry out similar analyses,
based on a {\em constructive} formulation of linear logic that allows them to
equate a proof with a structured narrative. We built on that work by using the
Celf linear logic language to encode story-world models for Madame Bovary and
a more general ``Shakespearean tragedy'' world, generating stories using
proof search~\cite{Martens13:LPNMR, martens2014generative}.  Most of this
work on representing stories as proofs or plans through an encoding of
state-changing actions has the limitation that the story model is not
itself executable as an interactive artifact, although the planner or proof
engine may be used as a subprocess within a running game. In this paper, we
integrate interaction with the specification language itself.

Another line of work has explored formal ``game description languages''
that can be used to generate executable prototypes. Our work has very
similar goals to those listed in the Dagshtul paper proposing VGDL (a video
game description language)~\cite{towardsVGDL}, except that we de-emphasize the
ability to constrain the design space to the point where a process could
automatically generate games. Additionally, our formalism is more flexible
in terms of entity relationships, explicitly aiming to support abstract
mechanics such as narrative and dialogue rather than focusing on object
collisions in 2D space.  Smith et. al. have investigated computer-aided
authoring of games through such means as constraint specification and
procedural content generation~\cite{smith2009computational, Smith12}, which
shares with our approach a use of logic programming as its foundation. In
this setting, game rules are treated as {\em term-level objects} over which
program rules are written.  This treatment separates the semantics of the
logic program itself from the semantics of the game, meaning as a
consequence that the object of formal analysis is distinct from the
playable artifact.
% This formulation of game specification seems suitable when one is
% primarily interested in games with concretely-specifiable {\em
  % solutions}, such as puzzle games, which can be exhaustively validated. 
Ceptre aims to create a closer link between the logic itself and the game
specification, making the language semantics itself the target of
programmatic analysis as well as informal reasoning and playtesting. 
Our work also prioritizes the expression of exploratory mechanics
rather than goal-driven ones (such as puzzle games), making exhaustive
search over the rules for the sake of validation or game generation less of
a concern for us. (That said, we do discuss the possibility of checking
invariants over game states in Section~\ref{sec:ongoing}.)
A third endeavor in the sphere of executable formalisms for games is
Versu~\cite{evansversu}, which we note as a useful reference point in
terms of our approach, defining Ceptre as a core formalism (c.f. Versu's
Praxis) atop which a friendlier user interface (c.f. Prompter) might be
built. Of course, our approach with Ceptre favors breadth (generality)
  rather than the depth of story- and text-specific tools of Versu.

Finally, several game creation tools have gained popularity among hobby
and novice game designers, making them attractive to our goals of striking
a balance between expressive power and minimality of core concepts. These
tools include Inform 7~\cite{inform7}, Kodu~\cite{KoduDesign}, and
PuzzleScript\footnote{Documentation available at
  \url{http://www.puzzlescript.net}}. In this paper, we identify an
essential core of each of these languages, formalize it, and show how it
can be expressed in Ceptre. What this work suggests is that each encoding
could be packaged as a separate module or context {\em within Ceptre} --
in which a novice designer could work exclusively, while the wider
affordances of the language remain available to extend, combine, or
reinvent such models.

To summarize, the core contributions described in this chapter are:
\begin{enumerate}
\item Progress toward a computational and conceptual framework for creating
games in a high-level, rule-based way without constraint by a particular
underlying world logic;
\item An account of several existing rule-based design frameworks in terms
of this core language;
\item A proof-based account of playtests that enables debugging and
analysis in terms of causal dependencies between game components.
\end{enumerate}

\section{Sensing and Acting Predicates}

The first step toward introducing interaction into this program is deciding
{\em when it should happen}. One sensible answer is to allow interaction at
every rule selection step, allowing the latent nondeterminism of the
program to be mediated by the actor's choices. This answer corresponds to
the {\em branching story} interpretation of linear logic programs as
described by Bosser~\cite{bosser2010linear}.

However, to allow for a larger space of interaction models, including ones
where the player must discover the space of reasonable actions, we borrow
an abstraction from the Meld language~\cite{Meld}: {\em sensing} and 
{\em acting} predicates. These predicates mediate input and output,
respectively, to or from the runtime environment. 

In our story-world model, we declare a new term for actions and a new
predicate \verb|do| indicating player intent:\\
\verb|do(verb) : sense|.
Now we add this predicate, indexed by the appropriate verb, on the
left-hand side of every rule; for example

\begin{verbatim}
do/murder 
: do (murder C C') *
  anger C C' * anger C C' * anger C C' * anger C C' *
  $at C L * at C' L  * $has C weapon
                -o !dead C'.
\end{verbatim}

Action predicates may be used for output: for example, reporting that this
rule successfully fired might involve a new predicate 
\verb|report status verb : action| and the rule could be rewritten as

\begin{verbatim}
do/murder : ...  -o !dead C' * report success (murder C C').
\end{verbatim}

\section{Stages}
\label{sec:stages}

Finally, in order to coordinate the two halves of the program---one that
waits for player input, and the other to process that input---we introduce
{\em stages}, which are a way to delineate rules into different sets and
switch control between them. Our interactive story world divided into stages
looks like this:

\begin{verbatim}
stage process_action = {
  rulename : do (some_action C1 C2) * ...
               -o ...
  ...
}
stage accept_action = {
  wait * do Action -o do Action.
}
\end{verbatim}


Stages may transfer control at {\em quiescence}, i.e. when no more rules in
the current stage may fire. We enable control flow rules through a special
sensing predicate \verb|qui| indicating quiescence. Then, rules such as
the following can be written without attachment to a particular stage:

\begin{verbatim}
qui * stage process_action -o
  stage accept_action * wait.

qui * stage accept_action * wait
  -o stage accept_action * wait.

qui * stage accept_action * $do Action
  -o stage process_action.
\end{verbatim}

Reading these rules in order, they say that when the process stage has
quiesced, move to the accept stage along with a \verb|wait| token. Then, if
the accept stage finishes without consuming the \verb|wait| token, return
to the accept stage. Finally, if the accept stage quiesces and emits an
action intent, go into the process stage and process the intent. In other
words, this program implements a simple blocking input loop.

Note that we are not guaranteed that every \verb|do| predicate issued by the
player will result in a successful action. A character won't be able to
murder someone unless they also have the required quantity of anger, for
example. This problem of {\em coverage} of the possible action space comes
up in all rule-based action systems, and it can be handled in several
possible ways:
\begin{enumerate}
\item Require (and check) that the program satisfy coverage, i.e. that
for every action \verb|A| there is a rule that will consume \verb|do A|.
\item Check after-the-fact whether the action was consumed in rule
processing, via quiescence rules, and enter a second ``failure'' pass,
which then may offer feedback to the player about the reason for failure. This
approach approximates Inform 7's rule processing, which we discuss further
in Section~\ref{sec:inform}.
\item Model player input not as effectful {\em actions} but effectless
{\em intents}, which are then pre-processed to determine the effects that
really take place, all of which should be expected to succeed. This method
more closely matches PuzzleScript's approach, discussed in
Section~\ref{sec:puzzlescript}.
\end{enumerate}

We refer to these three interaction approaches as {\em total coverage}, 
{\em failure feedback}, and {\em intent handling}, respectively. Failure
feedback and intent handling can both be implemented via the stage system;
total coverage would require a meta-program check that we believe would be
feasible to implement, but is not currently part of Ceptre's design.

Having now established Ceptre's mechanisms---predicates, rules, sensing and
acting predicates, and stages---we will show how to use them to interpret
other rule-based systems.

\chapter{Interpreting Other Systems}
\label{sec:interp}
% PAGE NUMBER TARGET: 2 (total: 5)

%% topic sentence
Ceptre can be understood as an underlying framework in which more
specialized, simpler authoring tools can be embedded. To illustrate this
property, we illustrate how to recover the central idioms of three
successful rule-based, game-logic-specific tools: Kodu, PuzzleScript, and
Inform 7. (See the introduction for citations of publications and
documentation for these tools.) 
% With unlimited time and pages, we would
% like to account for each of these systems in terms of a formal semantics, a
% compilation function, and a proof that the compilation preserves
% semantics---but without pre-existing formal semantics nor the space to
% carry out the details of a full and sound compilation, we instead rely on the
% reader's intuition that the examples we show capture the ``spirit'' of
% their meaning in the original tool.

% {\bf A note about rule ordering:} each of these systems imposes some
% assumptions about the order in which rules occur in the program.
% Their semantics try each rule in order, and if multiple rules apply, then
% whichever one occurs first is selected. We have deliberately made the
% opposite choice in Ceptre, making the semantics of our programs agnostic to
% the order in which rules are considered. We did this to enable {\em local
% reasoning}: when a rule applies only when all prior rules have been shown
% not to apply, its meaning is dependent on all of the rules that came before
% it. To make sense of a single rule means reading the entire prefix of the
% program up to that point.
% We recover some of the necessary rule ordering semantics through stages,
% though for the sake of simple presentation, though in many cases ...

% We observe that it is possible to account for rule
% ordering with {\em stages} in the sense that one can elaborate a designated
% ``ordered stage'' into a series of stages linked together at quiescence,
% but we do not provide the full translation here.

\section{Kodu}

Kodu is a rule-based programming language designed for children to make
movement-based games on an Xbox 360. The language takes inspiration from
behavior-based robotics, which closely reflects Ceptre's ``sensing and
acting'' model described above: the language includes {\em sensors}, {\em
filters}, {\em selectors}, {\em actuators}, and {\em modifiers}. A rule
is simply one element of each of these categories, some of which are
optional, associated with a specific game entity (such as the player
character). For example, a rule directing an entity to move quickly
toward green objects is:
\begin{verbatim}
see - green - move - towards - quickly
\end{verbatim}
In this rule, {\em see} is a sensor, {\em green} is a filter, 
{\em move} is an actuator, {\em toward} is a selector, and
{\em quickly} is a modifier (according to the formal grammar given by
    Stolee~\cite{stolee2010kodu}). 

Interpreting Kodu programs in Ceptre is essentially a matter of
interpreting sensors and selectors as sensing predicates, actuators as
acting predicates, filters as ordinary predicates, and all the rest as 
term-level arguments to these predicates. Additionally,
instead of explicitly associating rules with a single actor, we index
each predicate with an actor term. Thus the above rule can be written in
Ceptre as follows:

\begin{verbatim}
see X Y * $property Y green -o move X Y toward quickly. 
\end{verbatim}

The type header associated with the predicates in this rule is
\begin{verbatim}
see entity entity : sensor.
property entity filter : pred.
move entity entity selector modifier : action.
\end{verbatim}

One of the observations one can make in the collections Kodu examples
presented in papers is that, with certain exceptions, they {\em come in
pairs}: a rule whose actuator is movement, for example, can be thought of
as connecting to (or causing) a rule whose sensor involves location, such
as \verb|bump|, which triggers when the actor is right next to something
described by the filter. For instance, an actor that moves toward green
things and eats them could be modeled by pairing the above rule with

\begin{verbatim}
bump - green - eat
\end{verbatim}

Or in Ceptre:

\begin{verbatim}
bump X Y * $color Y green -o eat X Y.
\end{verbatim}

One of the things that gets in the way of reasoning about these
specifications in Kodu is that these causal relationships are not explicit
in the rule syntax: it's not obvious that actuating \verb|move toward|
would eventually result in a \verb|bump|. That fact only exists within the
implementation of the sensors and actuators, which are black boxes with
respect to the programmer's view. They transform the program constructs
into a change to the underlying implementation, then produce new program
constructs. In Cepter we can use this same ``cheat'' by passing the state
update to the runtime through sensing and acting predicates--but on the
other hand, we might find it more informative to elaborate some of the
movement predicates as a logic program:

\begin{verbatim}
sense/bump : $loc X L * $loc Y L' * !adj L L' -o bump X Y.
sense/see  : $loc X L * $loc Y L' * !visible L L' -o see X Y.
act/eat    : eat X Y * loc X L * loc Y L' -o loc X L'.
act/move_t : move toward X Y * loc X L * $loc Y L' *
              !adj L Ngh * !dist L L' D1 * !dist Ngh L' D2 *
              !lt D2 D1
              -o loc X Ngh.
act/move_a : move away X Y * loc X Y * $loc Y L' *
              !adj L Ngh * !dist L L' D1 * !dist Ngh L' D2 * 
              !lt D1 D2
              -o loc X Ngh.
\end{verbatim}

This program appeals to a number of geometric constructs such as \verb|adj|
for adjacency of locations, \verb|visible| for visibility between
locations, and \verb|dist| for the distance between locations. Writing the
rules this way forces us to expose more assumptions, such as the
discretizability of game space, which are not the only sensible
model for the rules given. This attempt to explicate the ``black box''
processes can help us understand the relationships between sets of rules in
terms of the predicates that they consume and produce, and it can also
reveal the underlying operational logic, exposing it to the possibility of
modification.

Extensions to Kodu have investigated its potential to support richer
operational logics. For example, Fristoe et. al.~\cite{Fristoe11}
investigated the possibility of enabling social simulation mechanics by
incorporating emotional state and dialogue sensors and actuators into the
system. We note that these modifications are trivial to integrate in Ceptre
and require only minimal extensions to the runtime processes, since the
logic programming environment already supports the maintenance of state
such as designations of friendship and fear between entities (see
section~\ref{sec:lang}). In contrast, formal definitions of Kodu such
as that given by Stolee~\cite{stolee2010kodu} attempt to encapsulate all of
the language constructs at the same, hard-coded level, failing to
distinguish the essential language structure (conditions and actions) from
the highly contingent domain constructs (such as scoring and shooting).

One of Kodu's program structuring tools is the notions of ``pages,'' or
different sets of rules that can be switched between, which closely
resembles Ceptre's stages. Every rule belongs to a page, and a rule can
trigger a ``flip'' to a different page.  While Ceptre rules don't include
the ability to change stages prior to program quiescence, the way we model
sensing and acting means that the program will quiesce after every actor
takes its turn, introducing an opportunity for a page-turning rule. That
is, the Kodu rule belonging to page \verb|p|

\begin{verbatim}
Condition Action switch page PageNumber
\end{verbatim}

can be interpreted by generating a unique token \verb|uniqtok| as a
consequence of the corresponding rule, and changing pages at quiescence in
the presence of that token:

\begin{verbatim}
stage p = {
  ...
  |Condition| -o |Action| * uniqtok
}
qui * stage p * uniqtok -o stage |PageNumber|
\end{verbatim}

where \verb[|-|[ is the mapping from Kodu construct to Ceptre predicate
outlined above.

\section{PuzzleScript}
\label{sec:puzzlescript}

PuzzleScript is a browser-based scripting language created by independent
game creator Stephen Lavelle. Its target domain is 2D, tile-based puzzle
games, whose rules transform sections of tiles related through the geometry
of the grid, such as adjacency and row or column alignment.
  
The ``hello world'' example of PuzzleScript is {\em Sokoban}, in which the
player controls an avatar that can push crates into empty spaces and
typically advances by pushing crates onto targets. Blocks cannot pass
through walls or other crates, nor can the player. It is codified in
PuzzleScript through a single rule:

\begin{verbatim}
[> player | crate] -> [> player | > crate]
\end{verbatim}

The \verb|>| symbol represents a movement intent (in the present author's
language, not Lavelle's) and the rule can be seen as propagating the
player's intent (expressed through pressing a movement control key) on to
a crate immediately adjacent in the intended direction. (The rule is
generic over directions). 

The avatar's free movement through empty space, and correspondingly, the
disallowing of passage through blocks and walls, are codified not as rules
but in the interpretation of {\em layers} of tile maps: entities on
distinct layers may be superimposed and thus share a tile, but entities on the
same layer cannot share a tile:

\begin{verbatim}
================
COLLISIONLAYERS
================
Background
Target
Player, Wall, Crate
\end{verbatim}

By default, movement intents result in movement, as long as they are not
blocked by the presence of some entity in the same layer.

Putting all these ideas together, the game can be codified in Ceptre as
follows:

\begin{verbatim}
at layer location entity intention : predicate.
adjacent location direction location : predicate.

stage ProcessIntentions = {
  push_crate :
    $at _ Loc player (go Dir) * adjacent Loc Dir Loc' 
      * at _ Loc' crate _
    -o at L' crate (go Dir).
}
stage CarryOutIntentions = {
  move : at Layer L Ent (go Dir) * adjacent L Dir L' 
           * empty Layer L' -o at Layer L' Ent stationary.
}
\end{verbatim}

% To do:
% Do another example

Next, we illustrate one of PuzzleScript's ``intermediate'' examples, a game
called Lime Rick in which the player navigates an avatar to targets, and
the avatar leaves behind a trail of solid entities, is subject to gravity,
and has an upward reach of three tiles. (This game is available in
PuzzleScript's built-in example collection through the web-based
editor). We implement these rules in Ceptre using direct movement
manipulation, rather than intentions, as it is done in the PuzzleScript
implementation as well. For brevity we omit the phase structure of this
example.

\begin{verbatim}
move/up/1 : move up * at L (player_head red) 
                -o at L (player_head red).
move/up/2 : move up * at L (player_head orange) * adj L up L'
                * empty L'
                -o at L player_body * at L' (player_head red).
move/up/3 : move up * at L (player_head yellow) * adj L up L'
                * empty L'
                -o at L player_body * at L' (player_head orange).
move/up/4 : move up * at L (player_head lime) * adj L up L'
                * empty L'
                -o at L player_body * at L' (player_head yellow).

move/r : move right * at L (player_head C) * adj L right L'
             * empty L'
             -o at L player_body * at L' (player_head lime).
% similarly move left

gravity : at L (player_head C) * adj L down L' * empty L'
              -o at L player_body * at L' (player_head C).
\end{verbatim}

This example illustrates how Ceptre enables codifying ``mechanics'' in the
sense of player-triggerable rules at the same level as internal game logic
rules, such as gravity, with the only difference being that the rule for
gravity does not consume a player-induced sensing predicate.

% Discuss win conditions/quantification
% include the following?:
% Another way to implement this specific small example in Ceptre would be to
% use a single phase, losing the nuance of layers and intentions:
% 
% \begin{verbatim}
% push : go Dir * at Loc player * adjacent Loc Dir Loc' 
%   * at Loc' crate * adjacent Loc' Dir Loc'' * empty Loc''
%   -o empty Loc * at Loc' player * at Loc'' crate.
% 
% move : go Dir * at Loc player * adjacent Loc Dir Loc' * empty Loc' 
%   -o empty Loc * at Loc' player.
% \end{verbatim}


%%%%%%%%%

% Core puzzlescript:

% We identify a grammar for the essentials of PuzzleScript as follows:
% 
% \begin{eqnarray*}
% \mathsf{Rule} &::=& LHS \to RHS
% \end{eqnarray*}
% 
% \begin{verbatim}
% RULE ::= LHS -> RHS
% LHS ::= LPAT^n
% RHS ::= RPAT^n
% LPAT ::= RPAT | ORIENTATION RPAT
% RPAT ::= [CELL] | [CELL|^n|CELL] | [CELL...CELL]
% CELL ::= entity | INTENTION entity | CELL^n
% INTENTION ::= stationary | > | < | DIR
% ORIENTATION ::= up | down | left | right | horizontal | vertical
% \end{verbatim}
% 
% In general, compile a rule \verb|LHS -> RHS| as a Ceptre rule
% \verb|L -o R| where for each \verb|LPAT| in \verb|LHS|,
% 
% If \verb|LPAT| is \verb|RPAT|, then
% if \verb|RPAT| is \verb|[CELL]|, then \verb|L| $=$ 
%   \verb|compile(CELL)|
% if \verb|RPAT| is \verb![CELL1|^n-1|CELLn]!, and \verb|CELL1| compiles to 
%   \verb|at(L1,entity1,INT1)|, then \verb|L| $=$
%   \verb|at(L1,entity1,INT1) * !adjacent(L1,DIR,L2) * ... * !adjacent(Ln-1,DIR,Ln) at(L1,entityn,INTn)|
%    
% When instead \verb|LPAT| is an oriented pattern, \verb|DIR| in the above is
% replaced with the particular specified direction.
% 
% (XXX cite destination-passing style as a compilation from a similar thing,
%  ordered logic, into the linear logic way of encoding adjacency
%  relationships as predicates)
% 

\section{Featherweight Inform 7}
\label{sec:inform}

Our final example is a boiled-down (``featherweight'') version of the
Inform 7 language for creating command-based interactive fiction (referred
    to as ``Parser IF'' by hobbyists). The language was designed to support
authoring of works inspired by those released by Infocom in the 1980s, and
accordingly it supports several verbs common to that genre, such as looking
around, examining an object, taking an object, moving in cardinal
directions, speaking to non-player characters, and inspecting one's
inventory (see Montfort~\cite{montfort2005twisty} for a description of
these games' conventions). Items in one's inventory often had game-specific
verbs associated with them, such as ``wield'' or ``attack [someone] with''
a weapon, or ``drink'' a potion. In some cases, entities have their own
internal state, such as a door being open or closed; entity-specific verbs
like ``open'' and ``close'' affect this state. Inform 7 supports a large
library of common verbs and entity types natively, and it also provides
authors with mechanisms for creating new ones. 

In the present author's experience, a great deal of Inform 7's power comes
from the tremendous library of defaults, as well as the great care it takes
to provide authors with options for seamless natural language processing
and generation as well as other aspects of player experience. Although we
recognize the importance of sensible defaults and polished aesthetics, we
do not claim that Ceptre can capture these aspects of the tool. We instead
describe a minimal target language capable of representing the range of
verbs described above, purely in terms of the underlying world model.

Even ignoring the substantial natural language tooling, there is still
quite a bit of complexity in faithfully describing Inform 7's rule
processing pipeline, as might be inferred by a glance at its diagram (XXX
cite). As before, the most subtle part is handling failure: how should
the engine respond when the player types a command that fails to apply in
the current world state? The answer will depend on what sort of failure we
mean.

In parser IF, one form of failure is a parse error. That is, before we can
determine whether a command is {\em applicable}, we need to determine
whether it is {\em sensible}. We punt this form of failure to the
implementation of the \verb|do| sensing predicate, which is indexed by an
abstract action, already in the form that our program can make sense of.

First we will give a type header for the world entities. Aside from verbs,
another form of sensing predicate is {\em visibility}, which could be
implemented in terms of the player's location relative to an object, the
open or closed states of containers, darkness, and so on. We choose to
leave it abstract to allow for variety in its implementation. We also
include an action predicate called \verb|success| for reporting the
consequences of a player's action.

\begin{verbatim}
visible object : sense.
do verb : sense.
success verb message : action.
portable object : predicate.
at object location : predicate.
description object message : predicate.
adjacent object direction object : predicate.
  % rooms are objects
\end{verbatim}

Now we can give some verb implementations, assuming success:
\begin{verbatim}
stage DoVerbs = {
  do/take : do (take Thing) * visible Thing 
          * $portable Thing * at Thing Location
            -o at Thing player_inventory * success (take Thing) taken.
  do/look : do look * $at player Room 
          * $description Room Description
            -o success look Description.
  do/examine/visible
          : do (examine Thing) * $visible Thing 
          * $description Thing Description
            -o success (examine Thing) Description.
  do/examine/inventory
          : do (examine Thing) * $at Thing player_inventory 
            * $description Thing Description
            -o success (examine Thing) Description.
  do/go   : do (go Direction) * at player Room 
          * $adjacent Room Direction Room' * $description Room' Desc
            -o at player Room' * success (go Direction) Desc.
}
\end{verbatim}

Some of the above rules should fail if certain circumstances apply. We
  implement those early failures as a stage that takes place before 
\verb|doVerbs| (and introduce another action predicate for failure):
\begin{verbatim}
stage PreCheck = {
  check/take/already : do (take Thing) * at Thing player inventory
    -o fail (take Thing) alreadyHave.
  check/take/fixed : do (take Thing) * $visible Thing *
      $fixed Thing -o fail (take Thing) fixedInPlace.
  check/look : do look * at player Room * state Room dark
    -o fail look (darkness Room).
  check/examine : do (examine Thing) * at Player Room 
    * state Room dark
    -o fail (examine Thing) (darkness Room).
  check/go : do (go Dir) * $at player R * $at R Door
    * door Door Dir closed -o fail (go Dir) (closedDoor Door).
}
qui * stage PreCheck * $do V -o stage DoVerbs.
qui * stage PreCheck * $fail V Msg -o stage Report.
\end{verbatim}

On the other hand, some of the failure modes are only describable as the
{\em negation} of certain things, such as visibility, which we cannot
easily negate. (A sensing predicate is fundamentally {\em positive}
information, and it would be impractical to enumerate everything one cannot
see.) We address these failures by also including a {\em post}-processing
failure stage, which we enter whenever \verb|doVerbs| failed to consume the
\verb|do| predicate:

\begin{verbatim}
qui * stage DoVerbs * $success Verb Msg -o stage Report.
qui * stage DoVerbs * $do Verb -o stage PostCheck.

stage postCheck = {
  check/take/notHere : do (take Thing)
    -o fail (take Thing) notHere.
  check/go : do (go Dir) -o fail (go Dir) noExit.
  check/default : do V * default -o fail V defaultFail.
}

qui * stage postCheck * $do V -o default * stage postCheck.
qui * stage postCheck * $fail Verb Msg -o stage Report.
\end{verbatim}

% XXX see if i can get this to work
% One other mechanism that Inform 7 allows is the ability to {\em fall back}
% to other commands if one command fails. For example, if a player tries to
% go north, but there is a closed door to the north, the system may
% automatically try to open it first (usually with the message, ``(first
% opening the door)''). We can implement this behavior. First, we need to
% introduce a compound verb for the sake of chaining two actions: 
% \verb|after verb verb : verb|. Then we need to implement the chaining
% behavior as part of the \verb|doVerbs| stage:
% 
% \begin{verbatim}
% qui * stage DoVerbs * $success Verb Msg * wait C2 -o stage
% {...
%   do/after : do (after Command1 Command2) -o do Command1 * wait Command2
%   do/wait/s : wait Command1 * success _ _ -o do Command2
%   do/wait/f : wait Command1 * fail V M -o fail V M.
% }
% \end{verbatim}
% ( XXX does the above work?)
% 
% \begin{verbatim}
%   check/go : do (go Dir) * $at player R * $at R Door
%       * door Door Dir closed
%     -o report_try (open Door) * do (after (open Door) (go Dir)). 
% \end{verbatim}

Although this is a drastically simplified version of the Inform 7 rules
processing engine, we expose its structure in such a way that the IF author
may change and potentially enrich it, in addition to simply adding new verb
implementations and failure conditions. Furthermore, we have implemented
standard interactive fiction verbs in the same framework in which we
implemented Kodu's robot-like sensors and action rules, and PuzzleScript's
grid-based tile manipulation rules. What we hope to have demonstrated by
this point is that Ceptre offers a very flexible and composable way of
writing rules for a variety of representative game types.

\chapter{Implementation}

\chapter{Case Studies}

\input{case_studies}


\part{Reasoning Tools}

\chapter{The Propositional Fragment}

\chapter{First-Order Programs}


\chapter{Conclusion}

%\appendix
%\include{appendix}

\backmatter

%\renewcommand{\baselinestretch}{1.0}\normalsize

% By default \bibsection is \chapter*, but we really want this to show
% up in the table of contents and pdf bookmarks.
\renewcommand{\bibsection}{\chapter{\bibname}}
%\newcommand{\bibpreamble}{This text goes between the ``Bibliography''
%  header and the actual list of references}
\bibliographystyle{plainnat}
\bibliography{main} %your bib file

\end{document}
