Tarski Games with "backtracking" (with irreversible backtracking).
Defining irreversible backtracking. Tarski Game for t.A (or f.B) with irreversible backtracking is played over the judgement tree of t.A (of f.B). The goal of Eloise is to convince Abelard that A is true (that B is false). The goal of Abelard is always the opposite of the goal of Eloise. In t.A, we say that Eloise defends A and Abelard attacks A. In f.B, we say that Eloise attacks B and Abelard defends B.
The play runs as Tarski play (see the section ``Tarski plays''), except that Eloise has a new kind of moves: backtracking moves. Instead of moving from the position i of the play, Eloise can come back, or ``backtrack'' to some position number j<i, retracting the positions j+1, ..., i-1 from the history of Tarski play. What happens next depends on which player made the move from position j. If Eloise moved from position j, now Eloise makes the move number i from the previous position j, instead from position i-1, as she would in a Tarski Game. If Abelard moved from position j, now Abelard makes move number i from the position j, instead from position i-1, as he would in a Tarski Game. The obvious yet relevant feature of backtracking is: the new move i from position j can be different from the original move j from position j. In games with irreversible backtracking, retracting a move is irreversible: Eloise cannot backtrack any more to the retracted positions j+1, ..., i-1. As in Tarski play, the first player who should move, and cannot, loses. There is an additional rule: Eloise cannot change a move infinitely many times, that is, she cannot come back infinitely many times to the same position j. We express this by the following rule:
Eloise loses all infinite plays
Irreversible backtracking and Monotonic Learning. Irreversible backtracking is a sound translation of the notion of learning by ``trial-and-error'',taken from everyday life. Irreversible backtracking is no complete translation of learning by ``trial-and-error'', though. Indeed, if we learn by trial-and-error, we may later find out we were wrong, but also find out that we were wrong in believing we were wrong. In this case, in everyday life, we can recover an hypothesis we retracted for a while. This is not possible with irreversible backtracking. With irreversible backtracking, we can only retract an hypothesis, we never recover it. This restricted notion of "learning" is called Monotonic Learning in computer Science.
Abelard cannot backtrack. We assume Abelard is "omniscient", and knows the better move without learning it by "trial-and-error". In other word, we do not allow Abelard to backtrack, but also, we do not bound Abelard to have an effective strategy, expressible by a program. Eloise, instead, can retract a move finitely many times, but she is bounded to have an effective strategy, expressible by a program.
Limit Computable Mathematics or LCM. The set of formulas for which there is some computable winning strategy for Eloise, in the game with irreversible backtracking, is called Limit Computable Mathematics, and denoted with LCM.
In which case is backtracking useful? Eloise can use backtracking in order to change a move which turned out to be wrong. Let us consider again the Minimum Principle ∀x.∃y.∀z.f(x,y)≤f(x,z). In the section about Tarski plays, we remarked that Eloise has a winning strategy, but no computable winning strategy. If Eloise can retract finitely many times each move, instead, Eloise has a computable winning strategy. Here it is.
(position 1) Abelard chooses some x=a and attacks ∃y.∀z.f(a,y)≤f(a,z).
(position 2) Eloise replies by selecting some y=b and defending ∀z.f(a,b)≤f(a,z). This move is winning if and only if b is indeed a minimum point of z|→f(a,z).
(position 3) Then Abelard chooses some z=c.
(position 4) If f(a,c)>f(b,c), Abelard moves to t.F. Abelard wins the Tarski play, but not the play with 1-backtracking.
(position 5) In a play with 1-backtracking, Eloise knows that y=b was a wrong choice. y=c would have been a better one, because f(b,c) is smaller, hence closer to the minimum value, than f(a,c). In 1-backtracking, Eloise can retract a move if later on she discover the move is wrong. Eloise backtracks from position 5 to position 2, retracting the positions 3,4,5 from the history of Tarski play. This time, Eloise chooses y=c. The result of this new move from position 2 is the position 6 of the play.
(position 6) The play continues in the same way. Abelard chooses some z=d.
(position 7) If f(a,c)>f(a,d), Abelard wins the Tarski play, but not the play with 1-backtracking.
(position 8) Eloise can backtracks from position 8 to position 2, retracting the positions 6,7,8 from the history of Tarski play. This time, Eloise chooses y=d. The result of this new move from position 2 is the position 9 of the play.
(position 9) .....................................
Positions 3,6,9,12, ... of the play are all the result of some move of Eloise from positions 2. The only way Eloise can lose is by playing forever (i.e., by backtracking infinitely many times to the position 2). However, this cannot be. The reason is that f(a,b) > f(a,c)>f(a,d) > ... is a decreasing sequence in N, which must stops in some f(a,e). In some position (say, in position 13), Abelard must replay with some z=e' such that f(a,e)≤f(a,e') is true. Then Eloise selects t.T, the only subjudgement of t.f(a,e)≤f(a,e') (position 14). Abelard cannot move and he loses. Eloise has "learned" some value y=e looking convincing to Abelard, and Abelard gives up.
Created by Mathematica (October 20, 2006)