Counting a type's (principal) inhabitants (Q2708317)

This paper is concerned with questions of counting inhabitants posed on page 127 of the book ``Basic simple type theory'' [Cambridge Univ. Press, Cambridge (1997; Zbl 0906.03012)] by \textit{J. R. Hindley}. These questions are the following: NEWLINENEWLINENEWLINE-- How many inhabitants in \(\beta\)-normal forms receive a given type as principal type? NEWLINENEWLINENEWLINE-- How many inhabitants receive a given type as principal type? NEWLINENEWLINENEWLINE-- How many inhabitants in \(\beta\)-normal forms of \(\lambda I\) receive a given type and how many have it as principal type? NEWLINENEWLINENEWLINEFor each case, the authors present an algorithm which decides in a finite number of steps whether the cardinality of the corresponding set of inhabitants is finite or infinite and computes this number in the finite case and lists all relevant terms in both cases. These algorithms follow the idea of Ben Yelles' counting algorithm which counts (and lists) the set of inhabitants in \(\beta\)-normal form that receive a given type. NEWLINENEWLINENEWLINEAlthough the paper is well-written and self-contained, I recommend the reader to first have a look at Hindley's clear account of Ben Yelles's algorithm.