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.