The Complexity of Principal Inhabitation

Authors Andrej Dudenhefner, Jakob Rehof

Thumbnail PDF


  • Filesize: 0.55 MB
  • 14 pages

Document Identifiers

Author Details

Andrej Dudenhefner
Jakob Rehof

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)


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


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. H. P. Barendregt, W. Dekkers, and R. Statman. Lambda Calculus with Types. Perspectives in Logic, Cambridge University Press, 2013. Google Scholar
  2. C.-B. Ben-Yelles. Type-assignment in the lambda-calculus; syntax and semantics. PhD thesis, Mathematics Dept., University of Wales Swansea, UK, 1979. Google Scholar
  3. 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:
  4. Sabine Broda and Luís Damas. Counting a Type’s Principal Inhabitants. In TLCA'99, pages 69-82, 1999. URL:
  5. Sabine Broda and Luís Damas. On long normal inhabitants of a type. J. Log. Comput., 15(3):353-390, 2005. URL:
  6. Boris Düdder, Moritz Martens, and Jakob Rehof. Staged Composition Synthesis. In ESOP 2014, Proceedings, pages 67-86, 2014. URL:
  7. 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. Google Scholar
  8. J. Roger Hindley. Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, vol. 42, Cambridge University Press, 2008. Google Scholar
  9. Jakob Rehof. Towards Combinatory Logic Synthesis. In BEAT 2013, 1st International Workshop on Behavioural Types. ACM, 2013. Google Scholar
  10. Sylvain Schmitz. Implicational relevance logic is 2-exptime-complete. J. Symb. Log., 81(2):641-661, 2016. URL:
  11. Richard Statman. Intuitionistic Propositional Logic is Polynomial-space Complete. Theoretical Computer Science, 9:67-72, 1979. URL:
  12. 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:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail