We associate with any game G another game, which is a variant of it, and which we call bck(G). Winning strategies for bck(G) have a lower recursive degree than winning strategies for G: if a player has a winning strategy of recursive degree 1 over G, then it has a recursive winning strategy over bck(G), and vice versa. Through bck(G) we can express in algorithmic form, as a recursive winning strategy, many (but not all) common proofs of non-constructive Mathematics, namely exactly the theorems of the sub-classical logic Limit Computable Mathematics (Hayashi (2006), Hayashi and Nakata (2001)).

Games with 1-backtracking

BERARDI, Stefano;
2010-01-01

Abstract

We associate with any game G another game, which is a variant of it, and which we call bck(G). Winning strategies for bck(G) have a lower recursive degree than winning strategies for G: if a player has a winning strategy of recursive degree 1 over G, then it has a recursive winning strategy over bck(G), and vice versa. Through bck(G) we can express in algorithmic form, as a recursive winning strategy, many (but not all) common proofs of non-constructive Mathematics, namely exactly the theorems of the sub-classical logic Limit Computable Mathematics (Hayashi (2006), Hayashi and Nakata (2001)).
2010
161
1254
1269
http://www.sciencedirect.com/science/article/pii/S0168007210000345
game semantics; backtracking; proof theory
Stefano Berardi; Thierry Coquand; Susumu Hayashi
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/135531
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 5
social impact