Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2017.2
URN: urn:nbn:de:0030-drops-100503
URL: https://drops.dagstuhl.de/opus/volltexte/2018/10050/
Dudenhefner, Andrej ; Rehof, Jakob
Lower End of the Linial-Post Spectrum
| pdf-format: |
|
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.
BibTeX - Entry
@InProceedings{dudenhefner_et_al:LIPIcs:2018:10050,
author = {Andrej Dudenhefner and Jakob Rehof},
title = {{Lower End of the Linial-Post Spectrum}},
booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
pages = {2:1--2:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-071-2},
ISSN = {1868-8969},
year = {2018},
volume = {104},
editor = {Andreas Abel and Fredrik Nordvall Forsberg and Ambrus Kaposi},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/10050},
URN = {urn:nbn:de:0030-drops-100503},
doi = {10.4230/LIPIcs.TYPES.2017.2},
annote = {Keywords: combinatory logic, lambda calculus, type theory, simple types, inhabitation, principal type}
}
| Keywords: | combinatory logic, lambda calculus, type theory, simple types, inhabitation, principal type | |
| Seminar: | 23rd International Conference on Types for Proofs and Programs (TYPES 2017) | |
| Issue date: | 2018 | |
| Date of publication: | 08.01.2019 |
