Abstract
Most research of algorithm extraction from classical proofs is based on double negation translation or its variants. From the viewpoint of Curry-Howard isomorphism, double negation translation corresponds to CPS translation. Unfortunately, CPS translation makes resulting programs very complex.
In this paper, we study a new translation for a semi-classical logic which is not based on double negation translation. Though it does not validate full classical logic, it translates Limit Computable Mathematics (LCM) into constructive mathematics.
Our translation is inspired by game semantics with backtracking rules. Using the translation, we can extract an algorithm from a proof of a proposition A in LCM. The extracted algorithm gives a recursive winning strategy for the first mover of the game defined from A, at least when A is implication-free.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Akama, Y., Berardi, S., Hayashi, S., Kohlenbach, U.: An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles. In: Proceedings of IEEE Symposium on Logic in Computer Science (LICS), pp. 192–201 (2004)
Kobayashi, S., Tatsuta, M.: Realizability Interpretation of Generalized Inductive Definitions. Theoretical Computer Science 131(1), 121–138 (1994)
Kobayashi, S.: Kyoukugen Keisan Kanou Suugaku no Geimu Imiron (English title: Game Semantics of Limit Computable Mathematics). In: Proceedings of the 24th JSSST Annual Symposia (2007)
Berardi, S.: An Semantic for Intuitionistic Arithmetic based on Tarski Games with retractable moves. In: Typed Lambda Calculi and Applications (TLCA) (2007)
Berardi, S.: Some intuitionistic equivalents of classical principles for degree 2 formulas. Ann. Pure Appl. Logic 139(1-3), 185–200 (2006)
Berardi, S., Coquand, T., Hayashi, S.: Games with 1-Backtracking. In: Proceedings of Games for Logic and Programming Languages (2005)
Berardi, S., Yamagata, Y.: A sequent calculus for 1-backtracking, Technical Report, Turin University, CL&C 2006. Submitted to the special issue of APAL for the congress (2006), http://www.di.unito.it/~stefano/Yamagata-Berardi-report.pdf
Coquand, T.: A Semantics of Evidence for Classical Arithmetic. Journal of Symbolic Logic 60, 325–337 (1995)
Friedman, H.: Classically and intuitionistically provably recursive functions. In: Scott, D.S., Muller, G.H. (eds.) Higher Set Theory. Lecture Notes in Mathematics, vol. 699, pp. 21–28. Springer, Heidelberg (1978)
Hayashi, S., Nakata, M.: Towards Limit Computable Mathematics, Proceedings of TYPES 2000, Lecture Notes in Computer Science 2277. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 125–144. Springer, Heidelberg (2002)
Hayashi, S.: Mathematics based on incremental learning—Excluded middle and inductive inference. Theoretical Computer Science 350, 125–139 (2006)
Hayashi, S.: Can Proofs be animated by games? Fundamenta Informaticae 77, 1–13 (2007)
Nakata, M., Hayashi, S.: A Limiting First Order Realizability Interpretation. Scientiae Mathematicae Japonicae 55(3), 567–580 (2002)
Toftdal, M.: A Calibration of Ineffective Theorems of Analysis in a Hierarchy of Semi-classical Logical Principles. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1188–1200. Springer, Heidelberg (2004)
Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics, vol. I, II, North-Holland, Amsterdam (1988)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kobayashi, S. (2008). A New Translation for Semi-classical Theories — Backtracking without CPS. In: Garrigue, J., Hermenegildo, M.V. (eds) Functional and Logic Programming. FLOPS 2008. Lecture Notes in Computer Science, vol 4989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78969-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-78969-7_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78968-0
Online ISBN: 978-3-540-78969-7
eBook Packages: Computer ScienceComputer Science (R0)