License: 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: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/10050/
Go to the corresponding LIPIcs Volume Portal

Dudenhefner, Andrej ; Rehof, Jakob

Lower End of the Linial-Post Spectrum

pdf-format:
LIPIcs-TYPES-2017-2.pdf (0.5 MB)

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
Collection: 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
Issue Date: 2018
Date of publication: 08.01.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI