The Complexity of Principal Inhabitation
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.
Lambda Calculus
Type Theory
Simple Types
Inhabitation
Principal Type
Complexity
15:1-15:14
Regular Paper
Andrej
Dudenhefner
Andrej Dudenhefner
Jakob
Rehof
Jakob Rehof
10.4230/LIPIcs.FSCD.2017.15
H. P. Barendregt, W. Dekkers, and R. Statman. Lambda Calculus with Types. Perspectives in Logic, Cambridge University Press, 2013.
C.-B. Ben-Yelles. Type-assignment in the lambda-calculus; syntax and semantics. PhD thesis, Mathematics Dept., University of Wales Swansea, UK, 1979.
Jan Bessai, Andrej Dudenhefner, Boris Düdder, Moritz Martens, and Jakob Rehof. Combinatory Logic Synthesizer. In Leveraging Applications of Formal Methods, Verification and Validation, 6th International Symposium ISoLA 2014, Corfu, Greece, October 8-11, 2014, pages 26-40, 2014. URL: http://dx.doi.org/10.1007/978-3-662-45234-9_3.
http://dx.doi.org/10.1007/978-3-662-45234-9_3
Sabine Broda and Luís Damas. Counting a Type’s Principal Inhabitants. In TLCA'99, pages 69-82, 1999. URL: http://dx.doi.org/10.1007/3-540-48959-2_7.
http://dx.doi.org/10.1007/3-540-48959-2_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.
http://dx.doi.org/10.1093/logcom/exi016
Boris Düdder, Moritz Martens, and Jakob Rehof. Staged Composition Synthesis. In ESOP 2014, Proceedings, pages 67-86, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54833-8_5.
http://dx.doi.org/10.1007/978-3-642-54833-8_5
Andrej Dudenhefner and Jakob Rehof. Typability in Bounded Dimension. In LICS 2017, Proceedings of the 32nd ACM/IEEE Symposium on Logic in Computer Science, Reykjavik, Iceland, June, 2017.
J. Roger Hindley. Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, vol. 42, Cambridge University Press, 2008.
Jakob Rehof. Towards Combinatory Logic Synthesis. In BEAT 2013, 1st International Workshop on Behavioural Types. ACM, 2013.
Sylvain Schmitz. Implicational relevance logic is 2-exptime-complete. J. Symb. Log., 81(2):641-661, 2016. URL: http://dx.doi.org/10.1017/jsl.2015.7.
http://dx.doi.org/10.1017/jsl.2015.7
Richard Statman. Intuitionistic Propositional Logic is Polynomial-space Complete. Theoretical Computer Science, 9:67-72, 1979. URL: http://dx.doi.org/10.1016/0304-3975(79)90006-9.
http://dx.doi.org/10.1016/0304-3975(79)90006-9
P. Urzyczyn. Inhabitation in Typed Lambda-Calculi (A Syntactic Approach). In TLCA'97, Typed Lambda Calculi and Applications, Proceedings, volume 1210 of LNCS, pages 373-389. Springer, 1997. URL: http://dx.doi.org/10.1007/3-540-62688-3-47.
http://dx.doi.org/10.1007/3-540-62688-3-47
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode