Counting a Type's (Principal) Inhabitants

Issue title: Typed Lambda Calculi and Applications (TLCA'99)

Article type: Research Article

Authors: Broda, Sabine | Damas, Luís

Abstract: We present a Counting Algorithm that computes the number of λ-terms in β-normal form that have a given type τ as a principal type and produces a list of these terms. The design of the algorithm follows the lines of Ben-Yelles' algorithm for counting normal (not necessarily principal) inhabitants of a type τ. Furthermore, we show that one can use similar algorithms with adequate limits to count normal and principal normal inhabitants in the λI-calculus.

Keywords:

Journal: Fundamenta Informaticae, vol. 45, no. 1-2, pp. 33-51, 2001