We present a Counting Algorithm that computes the number of l-terms in b-normal form that have a given type t 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 t. Furthermore, we show that one can use similar algorithms with adequate limits to count normal and principal normal inhabitants in the lI-calculus.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.