A generic position of the play in tree form.
The view-tree for plays with irreversible and reversible backtracking are defined in the same way. The only difference, if you imagine that in each retracted position there is one Abelard waiting to face Eloise, is that each Abelard has a different view of the play, according to the position he is in. At each step, we only consider the view of Eloise, and of the particular Abelard facing Eloise in the current position. When Eloise recovers some retracted position, we switch to the view of the Abelard waiting for Eloise in this position
We include here the definition of view-tree from the section about irreversible backtracking only in order to make the section about reversible backtracking self-contained.
Drawing a position in tree form. For each position we draw the current node and all previous nodes, numbered as they are in the play. The usual moves of Tarski plays are denoted by edges. Edges leading to (temporarily) retracted positions are thin edges. Edges leading to non-retracted positions are thick edges. Each node and each move has the color of the player it belongs to. Non-retracted positions form a Tarski play we call the current Tarski play, which can be any branch of the view-tree. The golden ball marks the current position of the current Tarski play, which can be any node of the view-tree. Thick edges form the current Tarski play, that is, the branch of the view-tree leading to the current goal (the golden ball). We call this picture, describing all backtracking done by Eloise: Eloise's view-tree. The background of the picture is a pale pink, Eloise's color. With respect to a Tarski play, a BCK-play is a tree, not a single branch. A forking in the tree correspond to a move changed by Eloise.
Here is Eloise's view-tree at step 11 of some play of this section.
Abelard's view-tree. The current Tarski play is the only part of the play which matters to Abelard, who cannot backtrack to any previous node. We call the tree form of the current Tarski play Abelard's view-tree. This is a picture of it, at step 11 of the same play. All edges are thick. The background is a pale blue, Abelard's color.
View-trees for Eloise and Abelard are asymmetric. Whenever Eloise retracts a move, all moves after the retracted move are cleared from the view of Abelard, but not form the view of Eloise. Eloise remembers all retracted moves, and use them to improve her moves. Abelard is assumed to be "omniscient", he knows the best move without having to learn it, and therefore does not need to remember retracted moves.
Whenever Eloise recovers a retracted position, then we switch the view of the current Abelard with the view of the Abelard waiting for Eloise in this position.
Created by Mathematica (October 20, 2006)