LIPIcs.FSCD.2017.15.pdf
- Filesize: 0.55 MB
- 14 pages
Document
The Complexity of Principal Inhabitation
Authors
-
Part of:
Volume:
2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2017-08-30
Cite AsGet BibTex
Andrej Dudenhefner and Jakob Rehof. The Complexity of Principal Inhabitation. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.FSCD.2017.15
https://doi.org/10.4230/LIPIcs.FSCD.2017.15
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.
Keywords
- Lambda Calculus
- Type Theory
- Simple Types
- Inhabitation
- Principal Type
- Complexity
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
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.
- 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.
- 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.
- 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.
-
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.
- 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.
- 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.