Document Open Access Logo

Lower End of the Linial-Post Spectrum

Authors Andrej Dudenhefner, Jakob Rehof

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2017.2.pdf
  • Filesize: 0.53 MB
  • 15 pages

Document Identifiers

Author Details

Andrej Dudenhefner
  • Technical University of Dortmund, Dortmund, Germany
Jakob Rehof
  • Technical University of Dortmund, Dortmund, Germany

Cite As Get BibTex

Andrej Dudenhefner and Jakob Rehof. Lower End of the Linial-Post Spectrum. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 2:1-2:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.TYPES.2017.2

Abstract

We show that recognizing axiomatizations of the Hilbert-style calculus containing only the axiom a -> (b -> a) is undecidable (a reduction from the Post correspondence problem is formalized in the Lean theorem prover). Interestingly, the problem remains undecidable considering only axioms which, when seen as simple types, are principal for some lambda-terms in beta-normal form. This problem is closely related to type-based composition synthesis, i.e. finding a composition of given building blocks (typed terms) satisfying a desired specification (goal type). 
Contrary to the above result, axiomatizations of the Hilbert-style calculus containing only the axiom a -> (b -> b) are recognizable in linear time.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • combinatory logic
  • lambda calculus
  • type theory
  • simple types
  • inhabitation
  • principal type

Metrics

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

References

  1. H. P. Barendregt. The Lambda Calculus. Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, 2nd Edition. Elsevier Science Publishers, 1984. URL: http://dx.doi.org/10.2307/2274112.
  2. H. P. Barendregt, W. Dekkers, and R. Statman. Lambda Calculus with Types. Perspectives in Logic, Cambridge University Press, 2013. Google Scholar
  3. Marcin Benke, Aleksy Schubert, and Daria Walukiewicz-Chrzaszcz. Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic. In FSCD 2016, volume 52 of LIPIcs, pages 12:1-12:16, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.12.
  4. Grigoriy V. Bokov. Completeness problem in the propositional calculus. Intelligent Systems, 13(1-4):165-182, 2009. Google Scholar
  5. Grigoriy V. Bokov. Undecidability of the problem of recognizing axiomatizations for propositional calculi with implication. Logic Journal of the IGPL, 23(2):341-353, 2015. URL: http://dx.doi.org/10.1093/jigpal/jzu047.
  6. Grigoriy V. Bokov. Undecidable problems for propositional calculi with implication. Logic Journal of the IGPL, 24(5):792-806, 2016. URL: http://dx.doi.org/10.1093/jigpal/jzw013.
  7. Sabine Broda and Luís Damas. On Long Normal Inhabitants of a Type. J. Log. Comput., 15(3):353-390, 2005. URL: http://dx.doi.org/10.1093/logcom/exi016.
  8. Boris Düdder, Moritz Martens, Jakob Rehof, and Paweł Urzyczyn. Bounded Combinatory Logic. In CSL 2012, Proceedings of Computer Science Logic, volume 16 of LIPIcs, pages 243-258. Schloss Dagstuhl, 2012. Google Scholar
  9. Andrej Dudenhefner and Jakob Rehof. The Complexity of Principal Inhabitation. In FSCD 2017, pages 15:1-15:14, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2017.15.
  10. J. R. Hindley. Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, vol. 42, Cambridge University Press, 2008. Google Scholar
  11. J. R. Hindley and J. P. Seldin. Lambda-calculus and Combinators, an Introduction. Cambridge University Press, 2008. Google Scholar
  12. AV Kuznecov and E Mendelson. Undecidability of the general problems of completeness, decidability and equivalence for propositional calculi. The Journal of Symbolic Logic, 1972. Google Scholar
  13. Samuel Linial and Emil L. Post. Recursive Unsolvability of the Deducibility, Tarski’s Completeness and Independence of Axioms Problems of Propositional Calculus. Bulletin of the American Mathematical Society, 55:50, 1949. Google Scholar
  14. Emil L. Post. A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society, 52(4):264-268, 1946. Google Scholar
  15. Jakob Rehof. Towards Combinatory Logic Synthesis. In BEAT'13, 1st International Workshop on Behavioural Types. ACM, 2013. Google Scholar
  16. W. E. Singletary. Many-one Degrees Associated with Partial Propositional Calculi. Notre Dame Journal of Formal Logic, XV(2):335-343, 1974. Google Scholar
  17. M.H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006. Google Scholar
  18. R. Statman. Intuitionistic Propositional Logic Is Polynomial-space Complete. Theoretical Computer Science, 9:67-72, 1979. Google Scholar
  19. Mary Katherine Yntema. A detailed argument for the Post-Linial theorems. Notre Dame Journal of Formal Logic, 5(1):37-50, 1964. URL: http://dx.doi.org/10.1305/ndjfl/1093957737.
  20. Evgeny Zolin. Undecidability of the Problem of Recognizing Axiomatizations of Superintuitionistic Propositional Calculi. Studia Logica, 102(5):1021-1039, 2014. URL: http://dx.doi.org/10.1007/s11225-013-9520-5.
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 About DROPS Imprint Privacy Contact