A generic position of the play in tree form.

Drawing a position in tree form. We draw one node for the current position of the play, and one node for each previous position. Nodes are numbered 1, ..., n, as the positions in the play. The usual moves of Tarski plays are denoted by edges. Moves leading to retracted positions are thin edges. Moves leading to non-retracted position are thick edges. Each node and each move has the color of the player it belongs to. Non-retracted moves form a Tarski play we call the current Tarski play, which, for irreversible backtracking, is always the rightmost branch in the view-tree. The golden ball marks the current position of the current Tarski play. This node, for irreversible backtracking, is always the "rightmost and innermost" node of the current tree. Thick edges form the current Tarski play. We call this picture, describing all retracking done by Eloise: Eloise's view-tree. The background of the picture is a pale pink, Eloise's color. Here is Eloise's view-tree at step 14 of the play of the previous subsection.

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. The only forking in the tree above is below position 2, the judgement t.∃y.∀z.f(a,y)≤f(a,z). Eloise plays 4 times: y=b, y=c, y=d, y=e, moving from position 2 to positions 3, 6, 9, 12. The first three times, Abelard provides some evidence of the fact that y=b, y=c, y=d are not a minimum point of z|→f(a,z). The evidence is, each time, some z such that f(x,y) > f(x,z): the first time is z=c, the second time is z=d, the third time is z=e. Three times in a row, Abelard proves that Eloise is wrong. However, Eloise can learn from her mistakes. She chooses a better value for z each time, in the next node to the right. Eventually, Abelard cannot provide any more an evidence that ∀z.f(a,y)≤f(a,z) is false, for the current value e of y. Abelard plays some e' such that f(a,e)≤f(a,e') is true, and Eloise wins.

The current Tarski play is the only part of the play which matters to Abelard, who cannot backtrack to a previous node. We call Abelard's view-tree the current Tarski play, represented as a branch of a tree. This is a picture of Abelard's view-tree, at step 14 of the play. The background is a pale blue, Abelard's color.

View-trees for Eloise and Abelard are asymmetric. Whenever Eloise backtracks, 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.

Created by Mathematica  (October 20, 2006)