Linear logic proof sets as split-screen hypertext
There is often some confusion when I discuss using linear logic to capture narrative structure. There are two interesting kinds of branching in linear logic, but we usually only talking about branching structure in narrative if it's interactive narrative, i.e. if the branches represent choices or alternatives between outcomes in a story scene. But there is also branching structure in many non-participatory narratives: there is a causal order of events, which is usually not a strictly total ordering. For example, scenes with different sets of characters, whose proceedings don't depend on one another's outcome, may be told in arbitrary order and still be coherent (though of course coherence isn't necessarily a narrative's goal, or its only goal).
The latter kind of branching can be thought of as spatial branching (for a sufficiently metaphorical notion of space), in the sense that different components of the narrative universe can evolve independently, then join together when they need to interact.
Spatial branching contrasts with temporal branching, which is the sort you get from hypertext and other narrative forms typically described as "branching." Choices are made, which determines one linear path through the narrative. Typically the experience of traversing such a path is oblivious to the alternative paths, just as real temporal experiences are oblivious to timelines in which we'd made different choices -- although a great deal of hypertext is designed with the intent of multiple traversals, which imparts a sort of metaexperience evocative of time travel.
In standard logical terms, spatial branching is conjunctive while temporal branching is disjunctive. Multiple independent events can happen "at once" -- "Lola asks her father for money and Manni asks his friend for money" -- but only one event from a set of alternatives can apply to a given piece of narrative state: "Lola dodges the dog on the stairs or she trips on the dog and injures her leg."
In linear logical terms, the more relevant distinction is additive vs. multiplicative branching: additive branching maps to sets of alternative routes from a single narrative state, where multiplicative branching refers to partitions of the state evolving independently.
The distinction also comes up in discussions of nondeterminism and concurrency: a program which asks for a random coin flip and says "heads" or "tails" depending on the answer can be seen as nondeterministic in a different way from a program with two threads, one of which prints "heads" and the other "tails."
Linear logic programs can have both kinds of nondeterminism/branching, but what's interesting is that after you run them -- i.e. after you create a proof a given linear logic formula -- you've selected a choice for all of the temporal branching points, but the resulting proof can still be seen as containing conjunctive, or spatial, branching structure. (I've elaborated previously on the idea of linear logic proofs' concurrent structure.)
One way of connecting linear logic to branching stories, then, is to take the one kind of branching that's left in proofs and map it to the one kind of branching in hypertext stories, which is exactly what we did for Quiescent Theater. The odd thing about this project is that there's a mismatch: we generated disjunctively branching stories from the conjunctively structured proofs. This has the kind of interesting effect that choices in the resulting stories act like "following" particular characters through their experience of the events of the story, with the ability to jump to new characters when the one you're currently following interacts with them. This is also the mechanic in the participatory theater experience Tamara, which partly inspired the experiment -- in fact, when Rob initially proposed the concept, I didn't understand it precisely because of the mismatch between types of branching; only after attending a performance of Tamara did I see the potential for that mismatch to make a kind of sense.
But I've recently been thinking about how to make a more precise correspondence between both kinds of branching structure present in branching + multi-agent narratives, and both kinds of concurrency in linear logic. I think I figured out how today. It requires that we extend traditional hypertext with a notion of compositional components that can be rendered simultaneously -- e.g. by splitting the screen. I've experimented with split-screen hypertext before, but this would require something quite a bit more sophisticated: any click in any panel of the screen could introduce new splits, merge arbitrary panels together, and depend on the state of other panels (in addition to its own state).
With that interpretation, a forward-chaining linear logic program -- or perhaps more precisely, a set of proofs generated from such a logic program -- can be rendered as follows: initialize the page with as many panels as there are atomic resources in the initial context. Provide an interface for selecting any subset of panels. For each selected subset, display a (possibly empty) set of clickable links corresponding to the set of transitions that apply to that resource set. (I originally imagined those links appearing in every relevant panel, but they could equally well appear in a completely separate global panel, modulo UX concerns.) For example, a par of rules [ r1 : a * b -o c ] and [ r2 : a * b -o d ] would render as 2 links when the [ a ] and [ b ] panels are both selected. Then a link click on [ r1 ] would merge [ a ] and [ b ] into a single panel with contents [ c ]. For first-order logic programs (i.e. ones with logic variables), we would need to disjunctively-nondeterministically generate several alternative structures and do a similar transformation on proof steps rather than on whole programs.
I think this idea has been explored in academic study of hypertext from a literary point of view before: this paper on conjunctive hypertext seems relevant, though I'm not entirely sure the structural observations I'm describing are as deep as whatever narratological points they are making.
P.S. If anyone wants to help me build the target interface I described, please let me know. My skills at making visual interfaces look the way I want are... probably not as good as someone else's reading this. ;)
The latter kind of branching can be thought of as spatial branching (for a sufficiently metaphorical notion of space), in the sense that different components of the narrative universe can evolve independently, then join together when they need to interact.
Spatial branching contrasts with temporal branching, which is the sort you get from hypertext and other narrative forms typically described as "branching." Choices are made, which determines one linear path through the narrative. Typically the experience of traversing such a path is oblivious to the alternative paths, just as real temporal experiences are oblivious to timelines in which we'd made different choices -- although a great deal of hypertext is designed with the intent of multiple traversals, which imparts a sort of metaexperience evocative of time travel.
In standard logical terms, spatial branching is conjunctive while temporal branching is disjunctive. Multiple independent events can happen "at once" -- "Lola asks her father for money and Manni asks his friend for money" -- but only one event from a set of alternatives can apply to a given piece of narrative state: "Lola dodges the dog on the stairs or she trips on the dog and injures her leg."
In linear logical terms, the more relevant distinction is additive vs. multiplicative branching: additive branching maps to sets of alternative routes from a single narrative state, where multiplicative branching refers to partitions of the state evolving independently.
The distinction also comes up in discussions of nondeterminism and concurrency: a program which asks for a random coin flip and says "heads" or "tails" depending on the answer can be seen as nondeterministic in a different way from a program with two threads, one of which prints "heads" and the other "tails."
Linear logic programs can have both kinds of nondeterminism/branching, but what's interesting is that after you run them -- i.e. after you create a proof a given linear logic formula -- you've selected a choice for all of the temporal branching points, but the resulting proof can still be seen as containing conjunctive, or spatial, branching structure. (I've elaborated previously on the idea of linear logic proofs' concurrent structure.)
One way of connecting linear logic to branching stories, then, is to take the one kind of branching that's left in proofs and map it to the one kind of branching in hypertext stories, which is exactly what we did for Quiescent Theater. The odd thing about this project is that there's a mismatch: we generated disjunctively branching stories from the conjunctively structured proofs. This has the kind of interesting effect that choices in the resulting stories act like "following" particular characters through their experience of the events of the story, with the ability to jump to new characters when the one you're currently following interacts with them. This is also the mechanic in the participatory theater experience Tamara, which partly inspired the experiment -- in fact, when Rob initially proposed the concept, I didn't understand it precisely because of the mismatch between types of branching; only after attending a performance of Tamara did I see the potential for that mismatch to make a kind of sense.
But I've recently been thinking about how to make a more precise correspondence between both kinds of branching structure present in branching + multi-agent narratives, and both kinds of concurrency in linear logic. I think I figured out how today. It requires that we extend traditional hypertext with a notion of compositional components that can be rendered simultaneously -- e.g. by splitting the screen. I've experimented with split-screen hypertext before, but this would require something quite a bit more sophisticated: any click in any panel of the screen could introduce new splits, merge arbitrary panels together, and depend on the state of other panels (in addition to its own state).
With that interpretation, a forward-chaining linear logic program -- or perhaps more precisely, a set of proofs generated from such a logic program -- can be rendered as follows: initialize the page with as many panels as there are atomic resources in the initial context. Provide an interface for selecting any subset of panels. For each selected subset, display a (possibly empty) set of clickable links corresponding to the set of transitions that apply to that resource set. (I originally imagined those links appearing in every relevant panel, but they could equally well appear in a completely separate global panel, modulo UX concerns.) For example, a par of rules [ r1 : a * b -o c ] and [ r2 : a * b -o d ] would render as 2 links when the [ a ] and [ b ] panels are both selected. Then a link click on [ r1 ] would merge [ a ] and [ b ] into a single panel with contents [ c ]. For first-order logic programs (i.e. ones with logic variables), we would need to disjunctively-nondeterministically generate several alternative structures and do a similar transformation on proof steps rather than on whole programs.
I think this idea has been explored in academic study of hypertext from a literary point of view before: this paper on conjunctive hypertext seems relevant, though I'm not entirely sure the structural observations I'm describing are as deep as whatever narratological points they are making.
P.S. If anyone wants to help me build the target interface I described, please let me know. My skills at making visual interfaces look the way I want are... probably not as good as someone else's reading this. ;)
Comments
Post a Comment