LIPIcs.FSCD.2023.32.pdf
- Filesize: 0.59 MB
- 16 pages
Document
Diller-Nahm Bar Recursion
Author
-
Part of:
Volume:
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 4.0 International license
- Publication date: 2023-06-28
Cite AsGet BibTex
Valentin Blot. Diller-Nahm Bar Recursion. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 32:1-32:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.32
https://doi.org/10.4230/LIPIcs.FSCD.2023.32
Abstract
We present a generalization of Spector’s bar recursion to the Diller-Nahm variant of Gödel’s Dialectica interpretation. This generalized bar recursion collects witnesses of universal formulas in sets of approximation sequences to provide an interpretation to the double-negation shift principle. The interpretation is presented in a fully computational way, implementing sets via lists. We also present a demand-driven version of this extended bar recursion manipulating partial sequences rather than initial segments. We explain why in a Diller-Nahm context there seems to be several versions of this demand-driven bar recursion, but no canonical one.
Subject Classification
ACM Subject Classification
- Theory of computation → Proof theory
Keywords
- Dialectica
- Bar recursion
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Stefano Berardi, Marc Bezem, and Thierry Coquand. On the Computational Content of the Axiom of Choice. Journal of Symbolic Logic, 63(2):600-622, 1998.
-
Justus Diller and Werner Nahm. Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen. Archiv für mathematische Logik und Grundlagenforschung, 16:49-66, 1974.
-
Martín Escardó and Paulo Oliva. The herbrand functional interpretation of the double negation shift. Journal of Symbolic Logic, 82(2):590-607, 2017.
-
Harvey Friedman. Classically and intuitionistically provably recursive functions. In Gert Müller and Dana Scott, editors, Higher Set Theory, volume 669 of Lecture Notes in Mathematics, pages 21-27. Springer, 1978.
-
Kurt Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12(3-4):280-287, 1958.
-
Stephen Cole Kleene. On the Interpretation of Intuitionistic Number Theory. Journal of Symbolic Logic, 10(4):109-124, 1945.
-
Georg Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In Constructivity in mathematics: Proceedings of the colloquium held at Amsterdam, 1957, Studies in Logic and the Foundations of Mathematics, pages 101-128. North-Holland Publishing Company, 1959.
-
Paulo Oliva and Thomas Powell. Bar recursion over finite partial functions. Annals of Pure and Applied Logic, 168(5):887-921, 2017.
-
Pierre-Marie Pédrot. A functional functional interpretation. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 77:1-77:10. ACM, 2014.
-
Pierre-Marie Pédrot. A Materialist Dialectica. (Une Dialectica matérialiste). PhD thesis, Paris Diderot University, France, 2015.
-
Clifford Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In Recursive Function Theory: Proceedings of Symposia in Pure Mathematics, volume 5, pages 1-27. American Mathematical Society, 1962.