Document Open Access Logo

A Unifying Framework for Type Inhabitation

Authors Sandra Alves , Sabine Broda

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2018.5.pdf
  • Filesize: 489 kB
  • 16 pages

Document Identifiers

Author Details

Sandra Alves
  • DCC-Faculty of Science & CRACS, University of Porto, Portugal
Sabine Broda
  • DCC-Faculty of Science & CMUP, University of Porto, Portugal

Funding

  • Alves, Sandra: Partially funded by the ERDF through the COMPETE 2020 Programme within project POCI-01-0145-FEDER-006961, and by National Funds through the FCT as part of project UID/EEA/50014/2013.
  • Broda, Sabine: Partially funded by CMUP (UID/MAT/00144/2013), which is funded by FCT (Portugal) with national (MEC) and european structural funds through the programs FEDER, under the partnership agreement PT2020.

Cite As Get BibTex

Sandra Alves and Sabine Broda. A Unifying Framework for Type Inhabitation. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSCD.2018.5

Abstract

In this paper we define a framework to address different kinds of problems related to type inhabitation, such as type checking, the emptiness problem, generation of inhabitants and counting, in a uniform way. Our framework uses an alternative representation for types, called the pre-grammar of the type, on which different methods for these problems are based. Furthermore, we define a scheme for a decision algorithm that, for particular instantiations of the parameters, can be used to show different inhabitation related problems to be in PSPACE.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Lambda calculus
  • Theory of computation → Rewrite systems
Keywords
  • simple types
  • type inhabitation
  • rewriting
  • PSPACE

Metrics

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

References

  1. Sandra Alves and Sabine Broda. Inhabitation machines: determinism and principality. In %Ninth Workshop on Non-Classical Models of Automata and Applications, NCMA 2017, pages 57-70, 2017. Google Scholar
  2. Ch. Ben-Yelles. Type Assignment in the Lambda-Calculus: Syntax and Semantics. PhD thesis, University College of Swansea, September 1979. Google Scholar
  3. S. Broda and L. Damas. Counting a type’s (principal) inhabitants. Fundam. Inform., 45(1-2):33-51, 2001. Google Scholar
  4. S. Broda and L. Damas. On long normal inhabitants of a type. J. Log. and Comput., 15:353-390, June 2005. Google Scholar
  5. M.W. Bunder. Proof finding algorithms for implicational logics. Theoretical Computer Science, 232(1–2):165-186, 2000. Google Scholar
  6. Andrej Dudenhefner and Jakob Rehof. The complexity of principal inhabitation. In %2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, volume 84 of LIPIcs, pages 15:1-15:14, 2017. Google Scholar
  7. Silvia Ghilezan. Inhabitation in intersection and union type assignment systems. J. Log. Comput., 3(6):671-685, 1993. Google Scholar
  8. J.R. Hindley. Basic Simple Type Theory, volume 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1997. Google Scholar
  9. R. Hindley. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc, 146:29-60, December 1969. Google Scholar
  10. S. Hirokawa. Infiniteness of proof (α) is polynomial-space complete. Theor. Comput. Sci., 206(1-2):331-339, 1998. Google Scholar
  11. W.A. Howard. The formulas-as-types notion of construction. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479-490. Academic Press, 1980. Google Scholar
  12. Y. Komori and S. Hirokawa. The number of proofs for a BCK-formula. J. Symb. Log., 58(2):626-628, 1993. Google Scholar
  13. Aleksy Schubert, Wil Dekkers, and Hendrik Pieter Barendregt. Automata theoretic account of proof search. In CSL 2015, pages 128-143, 2015. Google Scholar
  14. R. Statman. Intuitionistic propositional logic is polynomial-space complete. Theor. Comput. Sci., 9:67-72, 1979. Google Scholar
  15. M. Takahashi, Y. Akama, and S. Hirokawa. Normal proofs and their grammar. Information and Computation, 125(2):144-153, 1996. Google Scholar
  16. P. Urzyczyn. Inhabitation in typed lambda-calculi (a syntactic approach). In TLCA'97, volume 1210 of LNCS, pages 373-389. Springer, 1997. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact