Document Open Access Logo

On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction

Author Andreas Abel

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2020.1.pdf
  • Filesize: 0.85 MB
  • 21 pages

Document Identifiers

Author Details

Andreas Abel
  • Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden
  • Gothenburg University, Göteborg, Sweden

Funding

This work has been supported by grant no. 2019-04216 Modal Dependent Type Theory of the Swedish Research Council (Vetenskapsrådet).

Acknowledgements

Thanks to Herman Geuvers for explaining me truth-table natural deduction during a 2018 visit to Nijmegen for the purpose of Henning Basold’s PhD ceremony. Thanks to Ralph Matthes, Herman Geuvers and Tonny Hurkens for some email discussions on the topics of this article. I am also grateful for the feedback of the reviewer that led to a substantial clarification of the proof using orthogonality.

Cite AsGet BibTex

Andreas Abel. On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.TYPES.2020.1

Abstract

Intuitionistic truth table natural deduction (ITTND) by Geuvers and Hurkens (2017), which is inherently non-confluent, has been shown strongly normalizing (SN) using continuation-passing-style translations to parallel lambda calculus by Geuvers, van der Giessen, and Hurkens (2019). We investigate the applicability of standard model-theoretic proof techniques and show (1) SN of detour reduction (β) using Girard’s reducibility candidates, and (2) SN of detour and permutation reduction (βπ) using biorthogonals. In the appendix, we adapt Tait’s method of saturated sets to β, clarifying the original proof of 2017, and extend it to βπ.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • Natural deduction
  • Permutative conversion
  • Reducibility
  • Strong normalization
  • Truth table

Metrics

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

Supplementary Materials

References

  1. Andreas Abel. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, Ludwig-Maximilians-Universität München, 2006. Google Scholar
  2. Agda developers. Agda 2.6.1 documentation, 2020. URL: http://agda.readthedocs.io/en/v2.6.1/.
  3. Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In Jörg Flum and Mario Rodríguez-Artalejo, editors, Computer Science Logic, 13th Int. Wksh., CSL '99, 8th Annual Conf. of the EACSL, volume 1683 of Lect. Notes in Comput. Sci., pages 453-468. Springer, 1999. URL: https://doi.org/10.1007/3-540-48168-0_32.
  4. Franco Barbanera and Stefano Berardi. A symmetric lambda calculus for classical program extraction. Inf. Comput., 125(2):103-117, 1996. URL: https://doi.org/10.1006/inco.1996.0025.
  5. Nick Benton, Chung-Kil Hur, Andrew Kennedy, and Conor McBride. Strongly typed term representations in Coq. J. of Autom. Reasoning, 49(2):141-159, 2012. URL: https://doi.org/10.1007/s10817-011-9219-0.
  6. Garrett Birkhoff. Lattice Theory. Amer. Math. Soc., Providence, RI, USA, 3rd edition, 1967. Google Scholar
  7. Coq developers. The Coq proof assistant, version 8.12.0, 2019. URL: https://doi.org/10.5281/zenodo.2554024.
  8. Vincent Danos and Jean-Louis Krivine. Disjunctive tautologies as synchronisation schemes. In Peter Clote and Helmut Schwichtenberg, editors, Computer Science Logic, 14th Int. Wksh., CSL 2000, 9th Annual Conf. of the EACSL, volume 1862 of Lect. Notes in Comput. Sci., pages 292-301. Springer, 2000. URL: https://doi.org/10.1007/3-540-44622-2_19.
  9. René David. Normalization without reducibility. Ann. Pure Appl. Logic, 107(1-3):121-130, 2001. URL: https://doi.org/10.1016/S0168-0072(00)00030-0.
  10. René David and Karim Nour. Arithmetical proofs of strong normalization results for the symmetric lambda-mu-calculus. In Pawel Urzyczyn, editor, Proc. of the 7th Int. Conf. on Typed Lambda Calculi and Applications, TLCA 2005, volume 3461 of Lect. Notes in Comput. Sci., pages 162-178. Springer, 2005. URL: https://doi.org/10.1007/11417170_13.
  11. N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 75(5):381-392, 1972. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  12. Gerhard Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176-210, 405-431, 1935. URL: http://gdz.sub.uni-goettingen.de/.
  13. Herman Geuvers and Tonny Hurkens. Deriving natural deduction rules from truth tables. In Sujata Ghosh and Sanjiva Prasad, editors, Proc. of the 7th Indian Conference on Logic and Its Applications, volume 10119 of Lect. Notes in Comput. Sci., pages 123-138. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54069-5_10.
  14. Herman Geuvers and Tonny Hurkens. Proof terms for generalized natural deduction. In Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi, editors, 23rd Int. Conf. on Types for Proofs and Programs, TYPES 2017, volume 104 of Leibniz Int. Proc. in Informatics, pages 3:1-3:39. Schloss Dagstuhl, 2017. URL: https://doi.org/10.4230/LIPIcs.TYPES.2017.3.
  15. Herman Geuvers and Tonny Hurkens. Addendum to "Proof terms for generalized natural deduction", 2020. URL: http://www.cs.ru.nl/~herman/PUBS/addendum_to_TYPES.pdf.
  16. Herman Geuvers, Iris van der Giessen, and Tonny Hurkens. Strong normalization for truth table natural deduction. Fundam. Inform., 170(1-3):139-176, 2019. URL: https://doi.org/10.3233/FI-2019-1858.
  17. Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur. Thèse de Doctorat d'État, Université de Paris VII, 1972. Google Scholar
  18. Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. Math. Struct. in Comput. Sci., 11(3):301-506, 2001. URL: https://doi.org/10.1017/S096012950100336X.
  19. Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoret. Comput. Sci. Cambridge University Press, 1989. Google Scholar
  20. Felix Joachimski and Ralph Matthes. Standardization and confluence for a lambda calculus with generalized applications. In Leo Bachmair, editor, Rewriting Techniques and Applications, RTA 2000, Norwich, UK, volume 1833 of Lect. Notes in Comput. Sci., pages 141-155. Springer, 2000. URL: https://doi.org/10.1007/10721975_10.
  21. Felix Joachimski and Ralph Matthes. Short proofs of normalization for the simply-typed lambda-calculus, permutative conversions and Gödel’s T. Archive of Mathematical Logic, 42(1):59-87, 2003. URL: https://doi.org/10.1007/s00153-002-0156-9.
  22. Sam Lindley and Ian Stark. Reducibility and ⊤⊤-lifting for computation types. In Pawel Urzyczyn, editor, Proc. of the 7th Int. Conf. on Typed Lambda Calculi and Applications, TLCA 2005, volume 3461 of Lect. Notes in Comput. Sci., pages 262-277. Springer, 2005. URL: https://doi.org/10.1007/11417170_20.
  23. Zhaohui Luo. ECC: An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990. URL: https://www.cs.rhul.ac.uk/home/zhaohui/ECS-LFCS-90-118.pdf.
  24. Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Google Scholar
  25. Ralph Matthes. Characterizing strongly normalizing terms of a calculus with generalized applications via intersection types. In José D. P. Rolim, Andrei Z. Broder, Andrea Corradini, Roberto Gorrieri, Reiko Heckel, Juraj Hromkovic, Ugo Vaccaro, and J. B. Wells, editors, Intersect. Types and Related Sys. (ITRS 2000), ICALP Satellite Wksh., pages 339-354. Carleton Scientific, Waterloo, ON, Canada, 2000. Google Scholar
  26. Ralph Matthes. Non-strictly positive fixed-points for classical natural deduction. Ann. Pure Appl. Logic, 133(1-3):205-230, 2005. URL: https://doi.org/10.1016/j.apal.2004.10.009.
  27. Michel Parigot. Proofs of strong normalization for second order classical natural deduction. J. Symb. Logic, 62(4):1461-1479, 1997. URL: https://doi.org/10.2307/2275652.
  28. Michel Parigot. Strong normalization of second order symmetric λ-calculus. In Sanjiv Kapoor and Sanjiva Prasad, editors, FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science, volume 1974 of Lect. Notes in Comput. Sci., pages 442-453. Springer, 2000. URL: https://doi.org/10.1007/3-540-44450-5_36.
  29. Andrew M. Pitts. Parametric polymorphism and operational equivalence. Math. Struct. in Comput. Sci., 10(3):321-359, 2000. URL: http://journals.cambridge.org/action/displayAbstract?aid=44651.
  30. William W. Tait. Intensional interpretations of functionals of finite type I. J. Symb. Logic, 32(2):198-212, 1967. URL: https://doi.org/10.2307/2271658.
  31. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285-309, 1955. Google Scholar
  32. Jérôme Vouillon and Paul-André Melliès. Semantic types: A fresh look at the ideal model for types. In Neil D. Jones and Xavier Leroy, editors, Proc. of the 31st ACM Symp. on Principles of Programming Languages, POPL 2004, pages 52-63. ACM Press, 2004. URL: https://doi.org/10.1145/964001.964006.
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