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.