Counting a type's (pringipal) inhabitants
Sabine Broda and Luís Damas
FI (to appear)
We present a Counting Algorithm that computes the number of lambda
terms in beta normal form that have a given type tau 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 tau. Furthermore, we show that one can use similar algorithms with adequate limits to count normal and principal inhabitants in the lambda-I-calculus.