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

% 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.

\usepackage{times}
\usepackage{fullpage}
\usepackage{graphicx}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{proof,graphicx,listings}
\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}
\usepackage{enumitem}

% verbatim and fixed-width fonts
% begin copied from palatino.sty
\renewcommand{\rmdefault}{ppl}
\renewcommand{\sfdefault}{phv}
% \renewcommand{\ttdefault}{pcr}
\renewcommand{\ttdefault}{cmtt}
% end copied from palatino.sty

\usepackage{fancyvrb}
\fvset{fontsize=\small,fontfamily=tt}
\fvset{xleftmargin=5mm}
\RecustomVerbatimEnvironment{verbatim}{Verbatim}{}


% sets \lstinline font
\lstset{basicstyle=\ttfamily}

% 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}

% theorem stuff XXX possibly supplied by amsthm?
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}

\newenvironment{proofsketch}[1][Proof Sketch:]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
% \newenvironment{proof}[1][Proof]{\begin{trivlist}
% \item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
\newenvironment{definition}[1][Definition:]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
% \newenvironment{example}[1][Example]{\begin{trivlist}
% \item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
% \newenvironment{remark}[1][Remark]{\begin{trivlist}
% \item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
% 
% \newcommand{\qed}{\nobreak \ifvmode \relax \else
%       \ifdim\lastskip<1.5em \hskip-\lastskip
%       \hskip1.5em plus0em minus0.5em \fi \nobreak
%       \vrule height0.75em width0.5em depth0.25em\fi}

\begin {document} 
\frontmatter

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

\title{
{\bf Programming Interactive Worlds\\ with Linear Logic}
% \\
% {\it Second committee draft
% }
}
\author{Chris Martens}
\date{September 2015}
\Year{2015}
\trnumber{CMU-CS-15-134}

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

\support{\footnotesize 
This research was sponsored by the National Science Foundation under grant
numbers CCF-0546550, CNS-0716469, DGE-0750271; Qatar National Research Fund
under grant number NPRP-096671100; and Commission of the European
Communities under grant number FP-6506909.  The views and conclusions
contained in this document are those of the author and should not be
interpreted as representing the official policies, either expressed or
implied, of any sponsoring institution, the U.S. government or any other
entity.}

\disclaimer{}

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

\keywords{Programming Languages, Computational Logic, 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} 
Interactive storytelling weaves together deep computational ideas with
humanity's rich history of story and play, providing an important context
for tools and languages to be built. At the same time, formal specification
languages offer a palette of representation and inference techniques
typically reserved for the analysis of programming languages and complex
deductive systems. This thesis connects problems in the interactive
storytelling domain to solutions in formal specification.

Specifically, we examine narrative from a structural point of view and
observe that alternative narrative paths play a complementary role to
simultaneous interacting timelines. {\em Linear logic} provides the
representational tools necessary to investigate this structure, and by
extending the correspondence to proofs and proof construction, we find a
suite of computational possibilities. We present three efforts toward
realizing those possibilities: (1) the use of linear logic programming to
{\em generate} narratives; (2) a new programming language for authoring
{\em interactive} narratives, games, and simulations; and (3) techniques
for stating and proving design-level program properties.

We find that linear logic programming, enriched with a minimal extension to
its logical semantics, enables a wide range of programming idioms and
domain encodings. As evidence, we give five case studies, including social
simulation, combat-based adventure games, and board games.  To support
reasoning about design correctness, we present techniques for stating and
proving program invariants, as well as a decidability proof for
automatically checking those invariants for a large fragment of the
language.

These findings show that linear logic is a fruitful representation
language to serve as the basis for modeling and executing interactive worlds,
and they invite future investigations on using proof-theoretic
methodologies for creative systems.
\end{abstract}

\newpage

\begin{acknowledgments}
I am tremendously privileged to have been able to do a Ph.D. thesis on the
beautiful subjects of logic and game design, and a tremendous number of
people contributed toward my ability to do this strange and wonderful
thing.

My advisors Frank and Karl have been instrumental every step of the way:
from supporting my case for admission to CMU's graduate program, to
training me in the foundations of my field, to keeping their minds open as
I began to explore these highly unconventional applications of said
foundations. Bob Harper's lectures and writings have also been a crucial
part of my programming languages education.

Gwenn Bosser's work on linear logic for narrative structure gave me the
solid stepping-stone I needed to bring this thesis to fruition, and her
collaboration and encouragement has been critical for sustaining my
optimism around the project. I also thank David Renshaw for pointing out
her papers to me in the first place.

My other collaborators in papers, programs, and creative media, have given
me so much energy and inspiration: Jo\~{a}o Ferreira, William Lovas, Rob
Simmons, Vincent Zeng, Elizabeth Davis, Will Byrd, Claire Alvis, Philip
Gianfortoni, Ben Blum, Lea Albaugh, Jamie Perconti, Tom Murphy VII, Salil Joshi,
Andrew Cave, Kaustuv Chaudhuri, Dale Miller, Daniel Spoonhower: I thank you
all for your patience with me as an often-fickle collaborative partner, and
for the joy you've shared with me in what we created.

I thank the many attentive readers of this work (and its predecessors),
including, of course, my thesis committee members---Andr\'{e} and Roger in
particular have contributed insightful advice on accessibility to audiences
outside of logic.  Other readers I thank include William Cohen, Nico
Feltman, Adam Smith, Joe Osborn, Jurie Horneman, Paul Mazaitis, and several
anonymous reviewers, whose feedback has invariably strengthened my
understanding of prior work, communication of my own work, and inspiration
for future work.

The CMU POP/ConcertRG student group has provided valuable discussion of papers,
talks, and their own research, as well as attentive feedback on my own talks
and papers. In particular, my classmates Arbob Ahmed and Henry DeYoung have
motivated me with their fascinating research and deep analytical insights, and
Ian Voysey provided incredibly thorough and helpful feedback on practice talks.
The crew that graduated early in my time in grad school---Neel Krishnaswami,
Noam Zeilberger, Jason Reed, William Lovas, Rob Simmons, and Dan Licata---set
an admirable tone for humble and patient research discussions that I tried to
emulate after they graduated (it's harder than it looks). Current students like
Nico Feltman, Joe Tassarotti, and Anna Gommerstadt have spiritually succeeded
them with the proactive collaboration and careful thoughtfulness they bring to
the group---I can't wait to see what they do next. 

Ron Garcia, Ed Morehouse, and Stephanie Balzer, during their postdocs at
CMU, have all provided valuable mentorship and research discussions.
Gillian Smith and Jessica Hammer, although my relationships with both of
them are relatively new, have been immensely helpful in me considering my
career trajectory and imagining the sort of professor I might be someday.
I feel incredibly lucky to have benefited from the mentorship of these
wonderful people.

Will Byrd approached me at OPLSS in 2010 and, out of the blue, asked if I
``knew anything about interactive fiction'' because I came from CMU like
(renowned IF author) Andrew Plotkin. We then shared hunches about logical
formalisms for IF and put together a paper for OBT about it---long before I
pursued the possibility of a thesis about the idea.  Will has since been a
wonderful collaborator and mentor, emailing me unprompted and frequently
with opportunities, suggestions, and encouragement.

Independently-created games by Emily Short, Porpentine, Stephen Lavelle,
Terry Cavanaugh, Squinky, Lydia Neon, Tom 7, Sam Barlow, Andrew Plotkin,
Andi McClure, Michael Brough, Aaron Reed, and Merritt Kopas, have provided a
great deal of creative inspiration for this thesis work.  My students in
98-228 Interactive Fiction helped me, too, with their appreciation and
insight for the works I assigned them to play, and the wonderful games they
turned in as final assignments.

The UC Santa Cruz EIS lab, and the INT and FDG conference attendees, have
helped me understand what games research can be, and that it is full of
wonderful people. Conversations, papers, and talks by Kate Compton, Gillian
Smith, Squinky, Clara Fernandez-Vara, Joe Osborn, James Ryan, Aaron Reed,
Jacob Garbe, April Grow, Michael Mateas, Noah Wardrip-Fruin, Ian Horswill,
Gail Carmichael, R. Michael Young, and Ben Kybartas, have been crucial to
the joy I find in games and creativity research.

Back at home in Pittsburgh, there are a few who've stuck with me across the
years: Lea Albaugh, who met me 11 years ago and lived with me for 6, patiently
taught me things about Inform 7, sewing, soldering, and intersectional
feminism. Lea's thumb on the pulse of local art and theater projects is also
what led me to see the play {\em Tamara}, the study of which has been my
favorite application of this thesis work.  William Lovas, who persuaded me
during one pivotal bike ride in 2012 to pursue my ``linear logic for
games'' idea, despite my doubts that my advisor would take it seriously, has
been there for me in countless ways, over countless drinks and meals, in
countless cities across the world.

There have been several people in my life who pushed me to meet a higher
bar of excellence than I was meeting before their intervention, but the
first person to push me beyond what I thought I was capable of was Jamie
Morgenstern, all but dragging me across the finish line of my first 5k race
in 2010 to finish in under 26 minutes. She then proceeded to achieve elite
status in her own running career and finish her Ph.D. in under 5 years,
providing an inspirational (if unattainable) watermark for achievement.

For someone like me who's often timid about face-to-face interaction,
internet communication channels are absolutely priceless, and the
friendships I've made and/or maintained through LiveJournal and Twitter
deserve just as much recognition as the few I've grown close to in physical
space. Kat Hagan, Lindsey Kuper, Cass Sparks, Jason Reed, Danielle Kefford,
Greg Hanneman, Katie Mazaitis, Tim Chevalier, Joshua Dunfield, Mym Johnson,
Akiva Leffert, Annie Ogborn: your words have helped me in so, so many ways.
And then there's Philip ``8'' Gianfortoni, whose weekly video calls are the
only form of regular long-distance, voice-based contact I've ever
maintained, and I'm so grateful for his part in sustaining them.

There's still an unfortunate stigma against addressing mental health in
academia, and I'm going to try to do my part to break it here: I would
unquestionably not have finished my Ph.D. without therapy for anxiety
and depression. Thanks to Dr. W for her incredible skills.

I also would not have been able to afford my undergraduate education at CMU
(an undeniably critical stepping stone to grad school there) without almost
full grant support from the US Department of Education, for which I am
immensely grateful. Furthermore, I doubt I would have been admitted in the
first place without the groundbreaking work of Allan Fisher and Jane
Margolis, 20 years ago, to identify and excise the irrelevant
gender-correlated criteria previously associated with computer science
talent in CMU's undergraduate admissions.

My paternal grandmother died in 2013, after she gave me 27 years of
unwavering love; a brilliant, hilarious spirit as a role model; and stories
and artifacts pertaining to my father, who died a few months after my
birth. I only wish she could be here to see me graduate.

My mother has been the one constant in my life, and she has made her love
known the whole way. Growing up, my ``village'' consisted of grandparents,
aunts and uncles, teachers, and my mother's romantic partners, all of whose
love and guidance deserve my profound thanks. But my mother shaped who I am
today more than anyone else; it's hard to thank her without a touch of
narcissism. Mom: thanks for showing me how to be fearless, opinionated,
independent, creative, hard-working, vulnerable, selfless and selfish (as
the situation warrants).

Finally, while it is clearly {\em possible} to be a successful academic
without a partner who shoulders a large burden of domestic and emotional
labor, it is abundantly clear to me that Rob's efforts to be an equitable
and generous partner to me while juggling his own teaching career have made a
huge difference in my productivity, creativity, and happiness. And
furthermore, I am in the rare position to have a partner who understands
and enjoys my thesis work, even to the point of putting up with my rambling
about narrative structure after every television show, movie, and play we
see together. 

Thanks, everyone, for your patience, insight, love, and support.
\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.
%

\chapter{Introduction}
\label{chapter:intro}
\input{chapter-intro}

\chapter{Linear Logic for Narrative Structure}
\label{chapter:llns}
\input{chapter-llns}

\chapter{Linear Logic Programming for Narrative Generation}
\label{chapter:llpng}
\input{chapter-llpng}

\chapter{Ceptre: A Linear Logic Language for Interactive Programs}
\label{chapter:ceptre}
\input{chapter-ceptre}

\chapter{Case Studies}
\label{chapter:casestudies}
\input{chapter-casestudies}

\chapter{Reasoning About Linear Logic Programs}
\label{chapter:reasoning}
\input{chapter-reasoning}

\chapter{Conclusion}
\label{chapter:conclusion}
\input{chapter-conclusion}

\appendix

\chapter{CLF Semantics}
\label{appendix:clf}
\input{appendix-clf}

\chapter{Ceptre Typing and Kinding Rules}
\label{appendix:typing}
\input{appendix-typing-rules}

%\include{appendix}
\chapter{Code Listings}
\input{appendix-code}


\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{alphaurl}
\bibliography{main} %your bib file

\end{document}
