That Logic Blog

August 09, 2005

Computability Logic 1

In between much excitement, I have started teaching myself computability logic. As I mentioned before, this logic is semantically motivated and, as yet, does not have a completely satisfactory proof theory.

The idea behind computability logic is to model interactive computation. In order to do this, we set up the situation as a game between the user and the computer. In this scenario, we want the computer to win, since this means that the problem is computable and there is an algorithm for solving it. Play proceeds via a sequence of labelled moves, or labmoves. These are strings representing the move, labelled with which player made the move. A run is a finite or infinite sequence of labmoves and a position is a finite run.

It is quite easy to define one of the simplest notions of game involved, that of a constant game. This consists of a set of runs not containing a special symbol, say ♠. This set satisfies the condition that a run is contained within it iff all of its nonempty finite initial segments are there too. These runs code up the legal runs for the game. We force each player to play according to the rules by stipulating that the first player to make an illegal move immediately loses. That is, say the game is in position Γ and I make the move α. If Γ is a legal run but (Γ, α) is not then I lose. Boo!

Together with this collection of legal runs, a constant game also contains a function which sends each run to one of the players, indicating who has won. There are various finiteness conditions that one can stipulate on the set of runs, but I will introduce these as and when they are needed.

One important point to note is that we have not stipulated that, at any given stage of the game, only one player can move. If this happens to be the case, we say that the game is strict. In general, we will not restrict ourselves to strict games as these do not model all the sorts of interactive computation we may find ourselves performing.

One way to think of what is going on is to imagine interacting with a server. We keep sending it queries and it keeps replying. Of course, nothing is stopping, say, Bob from being annoying and sending lots of requests before receiving any replies from the server. Moreover, at any given stage the server may reply to any of Bob's previous queries or Bob could send yet another request. No sweat, we can model that, since we do not require the game to be strict.

Let's look at how to recover classical logic and Church-Turing style computablity. If every legal run in a constant game has length at most k, then we say that the game has depth k. Classical propositional logic corresponds to depth 0 games. There are precisely two of these. One of them returns the computer as the winner immediately and the other returns me as the winner immediately. If we model one of these as truth and the other as falsity, then we have classical logic. That is, all that matters is the input - we immediately get an answer. This is not particularly interesting but will eventually lead to classical logic being an elementary fragment of computability logic.

Modelling traditional computation is slightly trickier, though not too hard. What we do is model it as a depth 2 game. If we do nothing, then the computer has won (since it has nothing to answer for!). The next level consists of us handing the computer an input. At this stage, we are at depth 1 and we have won the game! The next level consists of all of the computer's possible responses. Now, what does it mean for the computer to have a winning strategy for this game? Precisely that no matter what our input, one of the computer's possible replies is the correct one. So, traditional computation is a depth 2 game, in this setup. This is not to be confused with how we traditionally model nondeterministic computation by building a tree or somesuch. In this situation, the tree represents the actual computation steps that the computer is performing. In Computability Logic, we are only interested in the interaction going on, not in the actual computation steps.

Next time: Non-constant games and operations on games.


Anonymous Anonymous said...

This comment may be premature, but it seems from your summary that Computability Logic makes an implicit assumption that interaction and computation are temporally separated, ie, that the two participants interact in some way (eg, one sends the other a message), and then one or both of them may compute somthing, after which another interaction takes place, and so on. While this is an advance on the Turing model, it still is unrealistic of present-day computation, where interaction and computation may arguably happen in parallel.

Also, how does this model extend to more than two participants?


Posted by Peter

6:16 PM  
Anonymous Anonymous said...

I'm not sure that I completely understand your objection, Peter. Do you mean something like an online algorithm? At any rate, once operations are defined on these games it starts actually modelling computation. Apparently. I haven't read that far yet!

The model generalises trivially to a client/server architecture with multiple clients. I suppose more interesting is something like a peer-peer architecture, where the agents can arbitarily interact with each other. In this setup we would lose the elementary embedding of classical logic, though it should be possible to push through most of the machinery by using a multi-valued logic. Something to think about! 

Posted by Jon

7:08 PM  
Anonymous Anonymous said...

Jon, my question concerned the assumption of modularity (or separability) between computation and communication, which seems implicit in what you've described so far of Computability Logic. In other words, how does this framework deal with cases such as the following:

- where computation by one party is interrupted by communication from another, or

- where computation by one party requires an interruption by communication from another (eg, an intermediate input), or

- where computation is undertaken by several parties acting jointly, with communication between them to co-ordinate this, or

- where computation is undertaken by several parties acting jointly, with communication through a third party or artefact (eg, a blackboard) to co-ordinate this, or

- where the computation might be thought to occur THROUGH the communication itself (eg, if the communicative acts update the states of the system, these utterances may be considered as programming commands acting on some virtual machine, as in Plotkin's Structural Operational Semantics)

- etc.

This is not intended as a criticism of the framework, merely a question as to its scope of applicability. Maybe you won't be able to answer till you're further along.


Posted by Peter

6:29 PM  
Anonymous Anonymous said...

Thanks for the clarification, Peter. I'll come back to your questions once I know more about CL. 

Posted by Jon

4:13 PM  

Post a Comment

<< Home