Everything in Context

My last post described the idea of concurrent storytelling  to encapsulate the idea of narrative structures where simultaneous action can lead to multiple experiences of a story, either through nondeterminism or through differing sequential traversals of the story graph. Since then, I have obtained a copy of the Tamara  script (which is written like a really bizarre choose-your-own-adventure book) and begun transcribing its scene structure as a deterministic Celf program such that the output trace models the scene dependency graph. To do this, I model each of the 10 characters as a predicate over a location and a scene identifier, e.g. tamara : scene -> location -> type. The scene IDs roughly correspond to the letter-and-numbered scenes in the script, except that they are slightly finer grained to accommodate the different perspectives induced by character entrances and exits, although those entrances/exits are contained within a single script-scene. In the si...

Last week  I discussed some newly-explored proof-theoretic relationships between reasoning about process calculi and substructural logics, and vaguely mentioned some other programming models that I wanted to compare. Since then, I think I've come up with a way to phrase my research objective with this project:  to relate the programming and reasoning methodologies surrounding interactivity through a common medium of proof theory. That's not a thesis statement, but I figure it's better than "*waves hands excitedly* interactivity! Processes! Linear logic! Focusing!" Anyway. What I've done so far has given me more questions than answers, but I like the questions a lot. The first of these questions I want to discuss in this post is "How can proof theory capture an appropriate notion of broadcast  message replication?" To explain what I mean by that, I'll describe an example which I think captures some common interactive communication patterns. ...

My post about week 1 established a new research project I'm working on involving programming interactivity with substructural logic. This past week, I've been working on digesting some background and related work. One thing I did was spend a good long stretch working through the core ideas in Yuxin, Iliano, and Rob's paper  Relating Reasoning Methods in Linear Logic and Process Algebra . Linear contexts as processes The point of the paper is to establish that a so-called "logical preorder" on contexts \[ \Delta \preceq_l \Delta' \] defined (I'm simplifying to the strictly linear case 1 ) as \[ {For}\ {all}\ C, \Delta \vdash C \ {implies}\  \Delta' \vdash C \] where \[ \vdash \] is entailment in linear logic, corresponds to traditional notions of contextual preorder  in CCS/process algebras, which are defined coinductively by a reduction relation extended over a laundry list of structure-preserving properties. The symmetric closure of th...

This will be the first of four posts in which I attempt to organize my thoughts about an idea for a project. It's related to  logic programming interactive fiction  and the  OBT talk  I gave this past January, but I'm trying to extend the ideas beyond interactive fiction -- which represents one particular interaction pattern -- into more general process-calculus-ish terms. Rob Simmons, who just defended a thesis that I take a great deal of inspiration from, has a  good primer on substructural logic programming  over on his blog. To review briefly, the key concepts I'm building on are: logic programming , in which a program is specified by declaring several atomic base types and a collection of logical propositions describing how they relate to one another, and a particular proof search strategy determines the semantics of its execution; forward-chaining  or bottom-up  logic programming, a particular proof search (i.e. execution strategy) wh...