For a terminating rewrite system R, and a ground term t1, two players alternate in doing R-reductions t_1 →_R t_2 →_R t_3 →_R ... That is, player 1 choses the redex in t_1, t_3,..., and player 2 choses the redex in t_2, t_4,... The player who cannot move (because tn is a normal form), loses. In this note, we propose some challenging problems related to certain rewrite games. In particular, we re-formulate an open problem from combinatorial game theory (do all finite octal games have an ultimately periodic Sprague-Grundy sequence?) as a question about rationality of some tree languages. We propose to attack this question by methods from set constraint systems, and show some cases where this works directly. Finally we present rewrite games from to combinatory logic, and their relation to algebraic tree languages.
展开▼
