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.