Switch to: References

Citations of:

Games with 1-backtracking

Stefano Berardi, Thierry Coquand & Susumu Hayashi

Annals of Pure and Applied Logic 161 (10):1254-1269 (2010)

Add citations

You must login to add citations.

Learning based realizability for HA + EM1 and 1-Backtracking games: Soundness and completeness.Federico Aschieri - 2013 - Annals of Pure and Applied Logic 164 (6):591-617.details We prove a soundness and completeness result for Aschieri and Berardiʼs learning based realizability for Heyting Arithmetic plus Excluded Middle over semi-decidable statements with respect to 1-Backtracking Coquand game semantics. First, we prove that learning based realizability is sound with respect to 1-Backtracking Coquand game semantics. In particular, any realizer of an implication-and-negation-free arithmetical formula embodies a winning recursive strategy for the 1-Backtracking version of Tarski games. We also give examples of realizers and winning strategy extraction for some classical proofs. (...) Download Export citation Bookmark 3 citations
Fluctuations, effective learnability and metastability in analysis.Ulrich Kohlenbach & Pavol Safarik - 2014 - Annals of Pure and Applied Logic 165 (1):266-304.details This paper discusses what kind of quantitative information one can extract under which circumstances from proofs of convergence statements in analysis. We show that from proofs using only a limited amount of the law-of-excluded-middle, one can extract functionals , where L is a learning procedure for a rate of convergence which succeeds after at most B-many mind changes. This -learnability provides quantitative information strictly in between a full rate of convergence and a rate of metastability in the sense of Tao (...) Download Export citation Bookmark 2 citations
A sequent calculus for Limit Computable Mathematics.Stefano Berardi & Yoriyuki Yamagata - 2008 - Annals of Pure and Applied Logic 153 (1-3):111-126.details We introduce an implication-free fragment image of ω-arithmetic, having Exchange rule for sequents dropped. Exchange rule for formulas is, instead, an admissible rule in image. Our main result is that cut-free proofs of image are isomorphic with recursive winning strategies of a set of games called “1-backtracking games” in [S. Berardi, Th. Coquand, S. Hayashi, Games with 1-backtracking, Games for Logic and Programming Languages, Edinburgh, April 2005].We also show that image is a sound and complete formal system for the implication-free (...) Download Export citation Bookmark 2 citations
Inside the Muchnik degrees I: Discontinuity, learnability and constructivism.K. Higuchi & T. Kihara - 2014 - Annals of Pure and Applied Logic 165 (5):1058-1114.details Every computable function has to be continuous. To develop computability theory of discontinuous functions, we study low levels of the arithmetical hierarchy of nonuniformly computable functions on Baire space. First, we classify nonuniformly computable functions on Baire space from the viewpoint of learning theory and piecewise computability. For instance, we show that mind-change-bounded learnability is equivalent to finite View the MathML source2-piecewise computability 2 denotes the difference of two View the MathML sourceΠ10 sets), error-bounded learnability is equivalent to finite View (...) Download Export citation Bookmark 3 citations
Game semantics and the geometry of backtracking: A new complexity analysis of interaction.Federico Aschieri - 2017 - Journal of Symbolic Logic 82 (2):672-708.details Download Export citation Bookmark

1