Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic
The approach to proof search dubbed "coinductive proof search", and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to LJP, a focused sequent-calculus presentation of polarized intuitionistic logic, including an array of positive and negative connectives. As before, this includes developing a coinductive description of the search space generated by a sequent, an equivalent inductive syntax describing the same space, and decision procedures for inhabitation problems in the form of predicates defined by recursion on the inductive syntax. We prove the decidability of existence of focused inhabitants, and of finiteness of the number of focused inhabitants for polarized intuitionistic logic, by means of such recursive procedures. Moreover, the polarized logic can be used as a platform from which proof search for other logics is understood. We illustrate the technique with LJT, a focused sequent calculus for full intuitionistic propositional logic (including disjunction). For that, we have to work out the "negative translation" of LJT into LJP (that sees all intuitionistic types as negative types), and verify that the translation gives a faithful representation of proof search in LJT as proof search in the polarized logic. We therefore inherit decidability of both problems studied for LJP and thus get new proofs of these results for LJT.
Inhabitation problems
Coinduction
Lambda-calculus
Polarized logic
Theory of computation~Type theory
Theory of computation~Proof theory
4:1-4:24
Regular Paper
The first and the last authors were partially financed by Portuguese Funds through FCT (Fundação para a Ciência e a Tecnologia) within the Projects UIDB/00013/2020 and UIDP/00013/ 2020. All authors got financial support by the COST action CA15123 EUTYPES.
We would like to thank for the careful and thoughtful review by an anonymous referee.
José
Espírito Santo
José Espírito Santo
Centre of Mathematics, University of Minho, Braga, Portugal
https://orcid.org/0000-0002-6348-5653
Ralph
Matthes
Ralph Matthes
CNRS, Institut de Recherche en Informatique de Toulouse (IRIT), France
https://orcid.org/0000-0002-7299-2411
Luís
Pinto
Luís Pinto
Centre of Mathematics, University of Minho, Braga, Portugal
https://orcid.org/0000-0003-1338-2688
10.4230/LIPIcs.TYPES.2020.4
Pierre-Louis Curien and Guillaume Munch-Maccagnoni. The duality of computation under focus. In Cristian S. Calude and Vladimiro Sassone, editors, Proceedings of Theoretical Computer Science - 6th IFIP TC 1/WG 2.2 International Conference, TCS 2010, Brisbane, Australia, September 20-23, 2010, volume 323 of IFIP Advances in Information and Communication Technology, pages 165-181. Springer, 2010.
Roy Dyckhoff and Stéphane Lengrand. Call-by-value lambda-calculus and LJQ. J. Log. Comput., 17(6):1109-1134, 2007.
Roy Dyckhoff and Luís Pinto. A permutation-free sequent calculus for intuitionistic logic. Technical report, St Andrews University Computer Science Research Report CS/96, August 1996.
José Espírito Santo. The polarized λ-calculus. In Vivek Nigam and Mário Florido, editors, 11th Workshop on Logical and Semantic Frameworks with Applications, LSFA 2016, Porto, Portugal, January 1, 2016, volume 332 of Electronic Notes in Theoretical Computer Science, pages 149-168. Elsevier, 2016. URL: https://doi.org/10.1016/j.entcs.2017.04.010.
https://doi.org/10.1016/j.entcs.2017.04.010
José Espírito Santo, Ralph Matthes, and Luís Pinto. A coinductive approach to proof search. In David Baelde and Arnaud Carayol, editors, Proceedings Workshop on Fixed Points in Computer Science, FICS 2013, Turino, Italy, September 1st, 2013, volume 126 of EPTCS, pages 28-43, 2013.
José Espírito Santo, Ralph Matthes, and Luís Pinto. Decidability of several concepts of finiteness for simple types. Fundam. Inform., 170(1-3):111-138, 2019.
José Espírito Santo, Ralph Matthes, and Luís Pinto. A coinductive approach to proof search through typed lambda-calculi. CoRR, abs/1602.04382v3, 2020. URL: http://arxiv.org/abs/1602.04382v3.
http://arxiv.org/abs/1602.04382v3
José Espírito Santo, Ralph Matthes, and Luís Pinto. Inhabitation in simply-typed lambda-calculus through a lambda-calculus for proof search. Mathematical Structures in Computer Science, 29:1092-1124, 2019. Also found at HAL through https://hal.archives-ouvertes.fr/hal-02360678v1. URL: https://doi.org/10.1017/S0960129518000099.
https://doi.org/10.1017/S0960129518000099
Mauro Ferrari and Camillo Fiorentini. Goal-oriented proof-search in natural deduction for intuitionistic propositional logic. J. Autom. Reasoning, 62(1):127-167, 2019.
Hugo Herbelin. A λ-calculus structure isomorphic to a Gentzen-style sequent calculus structure. In L. Pacholski and J. Tiuryn, editors, Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 61-75. Springer-Verlag, 1995.
Hugo Herbelin. Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de λ-termes et comme calcul de stratégies gagnantes. Ph.D. thesis, University Paris 7, 1995.
Jacob Howe. Proof Search Issues in Some Non-Classical Logics. Ph.D. thesis, University of St.Andrews, available as University of St.Andrews Research Report CS/99/1, 1998.
Jörg Hudelmaier. An o(n log n)-space decision procedure for intuitionistic propositional logic. J. Log. Comput., 3(1):63-75, 1993.
Paul Blain Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. High. Order Symb. Comput., 19(4):377-414, 2006.
Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logic. Theor. Comput. Sci., 410:4747-4768, 2009.
Gabriel Scherer and Didier Rémy. Which simple types have a unique inhabitant? In Kathleen Fisher and John H. Reppy, editors, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015, pages 243-255. ACM, 2015.
Robert J. Simmons. Structural focalization. ACM Trans. Comput. Log., 15(3):21:1-21:33, 2014.
J. B. Wells and Boris Yakobowski. Graph-based proof counting and enumeration with applications for program fragment synthesis. In Logic Based Program Synthesis and Transformation, 14th International Symposium, LOPSTR 2004, Verona, Italy, August 26-28, 2004, Revised Selected Papers, volume 3573 of LNCS, pages 262-277. Springer, 2004.
Noam Zeilberger. Focusing and higher-order abstract syntax. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 359-369. ACM, 2008.
José Espírito Santo, Ralph Matthes, and Luís Pinto
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode