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.FSCD.2017.15
URN: urn:nbn:de:0030-drops-77359
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7735/
Go to the corresponding LIPIcs Volume Portal

Dudenhefner, Andrej ; Rehof, Jakob

The Complexity of Principal Inhabitation

pdf-format:
LIPIcs-FSCD-2017-15.pdf (0.6 MB)

Abstract

It is shown that in the simply typed lambda-calculus the following decision problem of principal inhabitation is Pspace-complete: Given a simple type tau, is there a lambda-term N in beta-normal form such that tau is the principal type of N?

While a Ben-Yelles style algorithm was presented by Broda and Damas in 1999 to count normal principal inhabitants (thereby answering a question posed by Hindley), it does not induce a polynomial space upper bound for principal inhabitation. Further, the standard construction of the polynomial space lower bound for simple type inhabitation does not carry over immediately.

We present a polynomial space bounded decision procedure based on a characterization of principal inhabitation using path derivation systems over subformulae of the input type, which does not require candidate inhabitants to be constructed explicitly. The lower bound is shown by reducing a restriction of simple type inhabitation to principal inhabitation.

BibTeX - Entry

@InProceedings{dudenhefner_et_al:LIPIcs:2017:7735,
  author =	{Andrej Dudenhefner and Jakob Rehof},
  title =	{{The Complexity of Principal Inhabitation}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{15:1--15:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Dale Miller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7735},
  URN =		{urn:nbn:de:0030-drops-77359},
  doi =		{10.4230/LIPIcs.FSCD.2017.15},
  annote =	{Keywords: Lambda Calculus, Type Theory, Simple Types, Inhabitation, Principal Type, Complexity}
}

Keywords: Lambda Calculus, Type Theory, Simple Types, Inhabitation, Principal Type, Complexity
Collection: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Issue Date: 2017
Date of publication: 30.08.2017

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