Chris Martens

Programming Interactive Worlds with Linear Logic Degree Type: Ph.D. in Computer Science
Advisor(s): Karl Crary, Frank Pfenning
Graduated: December 2015

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. 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 generate narratives; (2) a new programming language for authoring 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.

Thesis Committee:
Frank Pfenning (Co-Chair)
Karl Crary (Co-Chair)
André Platzer
Roger Dannenberg
Anne-Gwenn Bosser (Harvard University)

Frank Pfenning, Head, Computer Science Department
Andrew W. Moore, Dean, School of Computer Science

Keywords:
Programming Languages, Computational Logic, Game Design, Interactive Simulation, Interactive Storytelling, Interactive Fiction