previous | top | next

A surprising observation


A certain class of lambda-terms is "the same shape as" their types. Specifically, the class of lambda-terms is BCI-terms in normal form. If you know the definition of beta-reduction, it is easy to see that the set of BCI-terms is closed under beta-reduction.