Publica
Hier finden Sie wissenschaftliche Publikationen aus den FraunhoferInstituten. The Complexity of Principal Inhabitation
 Miller, D.: 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 : 3rd  9th September 2017, Oxford, UK Saarbrücken/Wadern: Dagstuhl Publ., 2017 (Leibniz International Proceedings in Informatics. LIPIcs 84) ISBN: 9783959770477 Art. 15, 14 pp. 
 International Conference on Formal Structures for Computation and Deduction (FSCD) <2, 2017, Oxford> 

 English 
 Conference Paper, Electronic Publication 
 Fraunhofer ISST () 
Abstract
It is shown that in the simply typed lambdacalculus the following decision problem of principal inhabitation is Pspacecomplete: Given a simple type tau, is there a lambdaterm N in betanormal form such that tau is the principal type of N? While a BenYelles 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.