On the structure of normal lambda terms having a certain type

Sabine Broda and Luís Damas

Wollic 2000


Abstract

We define an alternative representation for types in the simply typed lambda-calculus or equivalently for formulas in the implicational fragment of intuitionist propositional logic, which gives us a better insight on the nature of a types structure and its relation to the structure of the set of its normal inhabitants. Based on this representation of a type phi we define the notion of a valid proof tree. Any such a valid proof tree represents a finite set of normal inhabitants of phi and every normal inhabitant corresponds to exactly one valid proof tree, constructable with the primitive parts in the formula tree of phi. Precise algorithms are given to establish this relation. Finally, we give a simple characterisation of the proof trees that represent principal normal inhabitants of a type phi.