Interactivity, week 3
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.
Consider a simplified Lights Out puzzle, a 2x2 grid of lights where toggling one also toggles its neighbors. Here's an implementation of the game (modulo its win condition, which I'll get to later) in puredata, a visual language where boxes represent signal-varying values, and edges represent the paths that signals follow. A human can send a (unit) signal to a box by clicking on it.
(Does a screenshot count as source in a visual language? Should I also post the inscrutable text format it saves to? Oh well, here it is.)
A line between the bottom of box A and the top of box B means that whenever box A outputs a signal, box B receives it. The square (circleless) boxes are "toggles", i.e. they can be on or off, and the circles (boxes with circles in) are "bangs", which just send a unit signal on their output line when they receive any signal on their input line. In this sense, the toggles are the indicators of the light state, whereas the bangs are the switches. To see why this separation is necessary, consider just wiring the input and output lines between all the neighboring boxes directly (text source):
Clicking on a toggle changes its value and sends a signal on its output lines, which then toggles its neighbors, which then send signals on their output lines... which inclue one back to the source. This creates an infinite loop; Pd's stack overflows, and the rendering never (visibly) changes. The level of indirection -- the separation of switch and indicator -- is necessary to stop the control flow after one signal propagation.
Another way to view this problem is to consider its encoding in CLF (eliding initial type declarations):
handle_sighuman : sighuman N -o {sigin N}.
handle_sigin : sigin N * light N S * opp S S'
-o {light N S' * sigout N}.
handle_sigout : sigout N * udnbr N N1 * lrnbr N N2 -o
{sigin N1 * sigin N2}.
Most of the predicates are indexed by a light identifier usually written with prefix N. I expect most of the predicates to be self-explanatory except that the "udnbr" and "lrnbr" predicates indicate the "up/down neighbor" and "left/right neighbor" of the indicated light.
Indeed, a query such as
#query * * * 3
(light l1 on * light l2 on * light l3 on * light l4 on
* sighuman l1 * sighuman l3 * sighuman l2 * sighuman l4)
-o {light l1 X1 * light l2 X2 * light l3 X3 * light l4 X4}.
loops infinitely: the simulation never saturates.
The working version (corresponding to the working pd program) is encoded as follows:
handle_sighuman : sighuman N * lrnbr N N1 * udnbr N N2
-o {sigin N * sigin N1 * sigin N2}.
handle_sigin : sigin N * light N S * opp S S'
-o {light N S'}.
Output signals from toggles are no longer needed; the human signal just directly toggles each neighbor. The input signal then just flips the indicator and emits no output (it could do so, but it would never be used).
This encoding has made a seemingly complicated interaction pattern much less interesting: it's now just a bunch of broadcasts from a single source that affect overlapping sets of receivers.
But there's still a component of this interaction pattern that's difficult to express in linear logic/CLF, which has to do with the fact that I've gotten away with a pretty big cheat by limiting the puzzle to a 2x2 grid: every cell uniformly has one udnbr and one lrnbr. In a bigger puzzle, cells can have two, three, or four neighbors. Ideally, we could program the neighbor relation separately, and have a toggle trigger the input signals of all its neighbors.
This is a sort of message copying, but it isn't the standard repeat described by ! in linear logic. Instead, it's a broadcast:
Instead of indicating infinitary nature of the message itself, we'd like to be able to describe the set of recipients infinitarily (even if they are in fact finite). We might think to use a universal quantifier, and write something like the following CLF (read Pi as forall) to broadcast to all neighbors:
handle : sigout N -o {Pi x. nbr x N -o sigin x}.
...but in the semantics of proof search, all this does is let us nondeterministically pick one neighbor to propagate an input signal to. We can instantiate the quantifier with any node N', and supposing we have that nbr N' N, the quantified statement will be replaced with sigin N', its original form discarded, unable to be used by other neighbors. (Furthermore, the quantifier might even be applied to a node that isn't a neighbor, leaving a useless implication in the context indefinitely!) And making the quantified statement replicating (with !) would be no better: since nbr facts are persistent, the same neighbor could instantiate the quantifier arbitrarily many times, making the message both repeated and broadcast.
In the sense that a universal quantifier is a form of infinitary conjunction, this suggests to me that CLF's Pi is like infinitary & ("with", additive conjunction in linear logic), in that proof search can choose how to quantify it, but it can't make several simultaneous choices. What we want for this behavior is something like an infinitary \[
\otimes
\], i.e. a positive universal quantifier. Jeff Sarnat informed me that some literature on bunched implications explores such a quantifier, but that it is folklorically known broken; I'm afraid I'm not well-versed enough in BI to understand why, but would be interested to try if someone can explain. (My
understanding of BI itself is pretty limited.)
Another slightly kludgy thing about the CLF implementation -- although it's a cute dependent types hack -- is the instance parameters, i.e. the fact that every predicate takes an argument to indicate which toggle it's talking about. Again (and this goes back to my initial comments about modularity and interface boundaries) it would be nice if we could describe the lightswitch interface generically and indicate separately the relationships between several instances of them. This begins to sound suspiciously similar to (my nebulous understanding of) the early, message-passing-based part of object oriented languages' history, and I believe puredata itself is based on an object model. Accounting for some limited use cases of objects like this might not be outside the scope of this project.
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.
Lights Out
A line between the bottom of box A and the top of box B means that whenever box A outputs a signal, box B receives it. The square (circleless) boxes are "toggles", i.e. they can be on or off, and the circles (boxes with circles in) are "bangs", which just send a unit signal on their output line when they receive any signal on their input line. In this sense, the toggles are the indicators of the light state, whereas the bangs are the switches. To see why this separation is necessary, consider just wiring the input and output lines between all the neighboring boxes directly (text source):
Another way to view this problem is to consider its encoding in CLF (eliding initial type declarations):
handle_sighuman : sighuman N -o {sigin N}.
handle_sigin : sigin N * light N S * opp S S'
-o {light N S' * sigout N}.
handle_sigout : sigout N * udnbr N N1 * lrnbr N N2 -o
{sigin N1 * sigin N2}.
Most of the predicates are indexed by a light identifier usually written with prefix N. I expect most of the predicates to be self-explanatory except that the "udnbr" and "lrnbr" predicates indicate the "up/down neighbor" and "left/right neighbor" of the indicated light.
Indeed, a query such as
#query * * * 3
(light l1 on * light l2 on * light l3 on * light l4 on
* sighuman l1 * sighuman l3 * sighuman l2 * sighuman l4)
-o {light l1 X1 * light l2 X2 * light l3 X3 * light l4 X4}.
loops infinitely: the simulation never saturates.
The working version (corresponding to the working pd program) is encoded as follows:
handle_sighuman : sighuman N * lrnbr N N1 * udnbr N N2
-o {sigin N * sigin N1 * sigin N2}.
handle_sigin : sigin N * light N S * opp S S'
-o {light N S'}.
Output signals from toggles are no longer needed; the human signal just directly toggles each neighbor. The input signal then just flips the indicator and emits no output (it could do so, but it would never be used).
Programmatic Broadcast: use case for positive ∀?
This encoding has made a seemingly complicated interaction pattern much less interesting: it's now just a bunch of broadcasts from a single source that affect overlapping sets of receivers.
But there's still a component of this interaction pattern that's difficult to express in linear logic/CLF, which has to do with the fact that I've gotten away with a pretty big cheat by limiting the puzzle to a 2x2 grid: every cell uniformly has one udnbr and one lrnbr. In a bigger puzzle, cells can have two, three, or four neighbors. Ideally, we could program the neighbor relation separately, and have a toggle trigger the input signals of all its neighbors.
This is a sort of message copying, but it isn't the standard repeat described by ! in linear logic. Instead, it's a broadcast:
Instead of indicating infinitary nature of the message itself, we'd like to be able to describe the set of recipients infinitarily (even if they are in fact finite). We might think to use a universal quantifier, and write something like the following CLF (read Pi as forall) to broadcast to all neighbors:
handle : sigout N -o {Pi x. nbr x N -o sigin x}.
...but in the semantics of proof search, all this does is let us nondeterministically pick one neighbor to propagate an input signal to. We can instantiate the quantifier with any node N', and supposing we have that nbr N' N, the quantified statement will be replaced with sigin N', its original form discarded, unable to be used by other neighbors. (Furthermore, the quantifier might even be applied to a node that isn't a neighbor, leaving a useless implication in the context indefinitely!) And making the quantified statement replicating (with !) would be no better: since nbr facts are persistent, the same neighbor could instantiate the quantifier arbitrarily many times, making the message both repeated and broadcast.
In the sense that a universal quantifier is a form of infinitary conjunction, this suggests to me that CLF's Pi is like infinitary & ("with", additive conjunction in linear logic), in that proof search can choose how to quantify it, but it can't make several simultaneous choices. What we want for this behavior is something like an infinitary \[
\otimes
\], i.e. a positive universal quantifier. Jeff Sarnat informed me that some literature on bunched implications explores such a quantifier, but that it is folklorically known broken; I'm afraid I'm not well-versed enough in BI to understand why, but would be interested to try if someone can explain. (My
understanding of BI itself is pretty limited.)
Alternative to instance parameters?
Another slightly kludgy thing about the CLF implementation -- although it's a cute dependent types hack -- is the instance parameters, i.e. the fact that every predicate takes an argument to indicate which toggle it's talking about. Again (and this goes back to my initial comments about modularity and interface boundaries) it would be nice if we could describe the lightswitch interface generically and indicate separately the relationships between several instances of them. This begins to sound suspiciously similar to (my nebulous understanding of) the early, message-passing-based part of object oriented languages' history, and I believe puredata itself is based on an object model. Accounting for some limited use cases of objects like this might not be outside the scope of this project.
I keep thinking about this idea that you should be able to gain insight into positive forall by thinking about how it would encode finitary tensor, e.g., A \otimes B := All x:2. if(x, A, B). And then I wonder if negative ("usual"?) Sigma can give us insight into par!
ReplyDeleteBut this is kind of a big proof-theoretic detour :)
Using Lights Out as an example gets at something that worries me about using this sort of logic programming. I'm going to see if I can articulate it clearly.
ReplyDeleteI think the goal of using the logic programming style of encoding is so that one can reason more cleanly about the program, and better understand (and prove) properties of the underlying system.
But, in this case, there's a property (local influence of switches) that the Pd picture makes very clear, and the logical encoding hides in a mysterious neighbor predicate.
And, going further, say you want to know if a given Lights Out position is winnable (and -- say -- what the shortest path is to that win). The Pd view gives you no help, sure, but the logic encoding makes this question look like an (potentially exponential-time) search problem.
Indeed, if you want to reason about winnability of Lights Out, it makes more sense to express the game as a sum of vectors over Z mod 2. Then the problem boils down to straightforward linear equation solving ( + some null space trickery, if needed).
I definitely agree about the neighbor predicate -- I think that's actually the primary thing I'm interested in extending the language with, some facility for "connecting nodes" (where a node is a collection of predicates) of a logic program. I don't think it's antithetical to logic programming in any way, it just implies a need for more structure.
DeleteIn a backward-chaining logic programming setting, you'd be right about the exponential time win condition check. But in CLF, it's a matter of just tracking some additional state. One way to do it would be to generate an "offt" token every time a light is turned off and consuming it every time one is turned on, by changing
handle_sigin : sigin N * light N S * opp S S'
-o {light N S'}.
to two rules
off2on : sigin N * light N off * offt
-o {light N on}.
on2off : sigin N * light N on
-o {light N off * offt}.
Then you could add a rule
winrule : offt * offt * offt * offt -o {win}.
(for however many lights are there. this could vary with the number of lights too, but that's some additional trickery.)
With a clever indexing mechanism, a logic program need only increment & check the count of identical predicates, so it could determine the fireability of that rule without examining the whole database.
(You could also do it just by incrementing/decrementing a number, but that's annoying because it forces sequentialization of the neighbor lights firing.)