Socially Responsive, Environmentally Friendly Logic

Socially Responsive, Environmentally Friendly Logic
by Samson Abramsky

We consider the following questions: What kind of logic has a natural semantics in
multi-player (rather than 2-player) games? How can we express branching quantifiers, and
other partial-information constructs, with a properly compositional syntax and semantics?
We develop a logic in answer to these questions, with a formal semantics based on multiple
concurrent strategies, formalized as closure operators on Kahn-Plotkin concrete domains.
Partial information constraints are represented as co-closure operators. We address the
syntactic issues by treating syntactic constituents, including quantifiers, as arrows in a
category, with arities and co-arities. This enables a fully compositional account of a wide
range of features in a multi-agent, concurrent setting, including IF-style quantifiers.

This paper seems to unify multiple interesting directions - logic, game semantics, concurrent constraint programming (and concurrent programming in general).

At the same time it remains very accessible, without overwhelming amount of math, so can be hopefully useful not only for academics. I, for one, was waiting for exactly this kind of paper for two years (and my interest is very practical).

Multiplayer Curry-Howard correspondence, anyone? Or Curry-Howard for web services?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Some links

See A Revolution in Logic? for a discussion on IF, and Introduction to computability logic for an introduction to another project that builds logic of computation.

[on edit: note that IF paper suggests a way of living with Gödel's first incompleteness
theorem, thus winning my simpathy for IF itself and any adopters of it]

Please expand short, rarely-used acronyms ...

... especially when they're ambiguous. Last time "I.F." showed up on LtU, it meant "interactive fiction". This time, it took a couple of clicks to locate the expansion as "Independence-Friendly". Thanks for the link, Andris.

What does it do for you?

I, for one, was waiting for exactly this kind of paper for two years (and my interest is very practical).

I'd be interested to hear more about your practical interests in this style of logic, and what it does for you that you find lacking in other formalisms.

Ever since that "Revolution in Logic?" thread, I've been trying to determine if there is something deep going on here or if it is just another formulation of certain substructural logics and proof-theoretic ideas. (Abramsky's comment about the relationship with Linear Logic and the surprising treatment of implication are the kinds of things that lead me in this direction.)

Understanding why it works for you might help me work this out for myself.

It does not work yet

Understanding why it works for you might help me work this out for myself.

I didn't put it into good use yet, but I have some ideas. Prepare for a brain dump.

On my day job I worked for several years on BPM and similar topics, and the state of the art amazed me (and not because of its great achievements). Abundance of standards for definition of business processes, orchestrations, and choreography is probably even more pronounced than in other parts of IT industry. I tried to use some formalism instead of standard, and found that pi and join calculi are far from satisfying requirements. As strange as it may sound I needed types, even more - I needed contracts or protocols. I played with linear logic a bit (Curry-Howard to the rescue). It seemed almost the right thing. Then I stumbled upon computational logic (CL). At about the same time I got interested with the notion of computability, Turing machines of all sorts, Gödel's theorems, ..., so CL looked very interesting. Another attractive property of CL was its approach of starting from semantic (unlike linear logic). I had some sentiments about CL not covering multiplayer games, as that would be handy in business cases.

Having said that, I plan to try and extend the ideas from OP paper a bit (as far as non-academic can :) ). One thing is reflection and interpretation (particularly reflective towers) - how can it be described by game semantics? Who are the players?
Another thing is not of practical interest for me, but more of a hobby (though it might help me to understand distributed computing) - what constraints on the structure of the game make it compatible with relativistic physics, thus yielding the notion of relativistic computability?
The last thing is quite minor, but looks useful for practice: I consider to replace permutation of roles by a function (probably not even injective) of role mapping for purpose of modularity and reuse. The question is, how this would affect the properties of the logic?
[on edit: almost forgot about this important feature - cancellation and "garbage collection" of cancelled (irrelevant) moves]

As you can see, my interest, while avid, is based on very raw ideas.
Hope some of them might be interesting to somebody else.

PS: I speculate that at least couple of LtU readers might find the OP ideas useful for game development :)


I so don't see what this has to do with anything.

Rough Guesses

I suspect, but am not competent to prove, that this is related to Modal Logics, particularly those discussed in Reasoning About Knowledge. If so, there are several potential application domains, e.g. economics and distributed systems generally. I'm also reminded of the two-envelope problem, about which these authors say "We conclude that the two-envelope problem does not allow a satisfactory solution," which seems to me to be addressed by Pollock in Thinking about Acting: Logical Foundations for Rational Decision Making, where he notes:

In chapter eight, it is argued first that actions cannot be evaluated in terms of their expected values as ordinarily defined, because that does not take account of the fact that a cognizer may be unable to perform an action, and may even be unable to try to perform it. An alternative notion of "expected utility" is defined to be used in place of expected values. In chapter nine it is argued that individual actions cannot be the proper objects of decision-theoretic evaluation. We must instead choose plans, and select actions indirectly on the grounds that they are prescribed by the plans we adopt. However, our objective cannot be to find plans with maximal expected utilities. Plans cannot be meaningfully compared in that way.

Of course, it's worth noting the last comment in the paper above:

The logic and semantics we have developed appears to flow from very natural intuitions.
These should be supported by a range of convincing examples and applications.

Yes. Yes, they should.


Way of topic: reading the title, I guess it should have been posted to the Community Enforcement Discussion thread.

Me too...

Me too...


Is it criticism of the title, or of its appearance on the front page?

Do you suggest I change the title of the paper? :)

Just in case somebody have responded without reading at least the first page of the paper - it IS about logic, game semantics, and concurrency. And some category theory is used, as well.
It just happens to have a bit too frivolous title.

No, no. It just tells you

No, no. It just tells you something about the state LtU at the moment, that the title was a bit confusing.