Document Open Access Logo

Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic

Authors José Espírito Santo , Ralph Matthes , Luís Pinto

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2020.4.pdf
  • Filesize: 0.85 MB
  • 24 pages

Document Identifiers

Author Details

José Espírito Santo
  • Centre of Mathematics, University of Minho, Braga, Portugal
Ralph Matthes
  • CNRS, Institut de Recherche en Informatique de Toulouse (IRIT), France
Luís Pinto
  • Centre of Mathematics, University of Minho, Braga, Portugal

Funding

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.

Acknowledgements

We would like to thank for the careful and thoughtful review by an anonymous referee.

Cite AsGet BibTex

José Espírito Santo, Ralph Matthes, and Luís Pinto. Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.TYPES.2020.4

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Proof theory
Keywords
  • Inhabitation problems
  • Coinduction
  • Lambda-calculus
  • Polarized logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. 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. Google Scholar
  2. Roy Dyckhoff and Stéphane Lengrand. Call-by-value lambda-calculus and LJQ. J. Log. Comput., 17(6):1109-1134, 2007. Google Scholar
  3. 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. Google Scholar
  4. 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.
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. 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.
  8. 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.
  9. Mauro Ferrari and Camillo Fiorentini. Goal-oriented proof-search in natural deduction for intuitionistic propositional logic. J. Autom. Reasoning, 62(1):127-167, 2019. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. 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. Google Scholar
  13. Jörg Hudelmaier. An o(n log n)-space decision procedure for intuitionistic propositional logic. J. Log. Comput., 3(1):63-75, 1993. Google Scholar
  14. Paul Blain Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. High. Order Symb. Comput., 19(4):377-414, 2006. Google Scholar
  15. Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logic. Theor. Comput. Sci., 410:4747-4768, 2009. Google Scholar
  16. 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. Google Scholar
  17. Robert J. Simmons. Structural focalization. ACM Trans. Comput. Log., 15(3):21:1-21:33, 2014. Google Scholar
  18. 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. Google Scholar
  19. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact