A context-free grammar representation for normal inhabitants of types in TA-lambda

Sabine Broda and Luís Damas

EPIA'01

Abstract

In~\cite{TAH96} it was shown that it is possible to describe the set of
normal inhabitants of a given type $\tau$, in the standard simple type
system, using an
infinitary extension of the
concept of context-free grammar, which allows for an infinite number of
non-terminal symbols as well as production rules. The set of normal
inhabitants of $\tau$ corresponds then to the set of terms generated
by this, possibly infinitary, grammar plus all terms obtained from
those by $\eta$-reduction.
In this paper we show
that the set of normal inhabitants of a type $\tau$ can in fact be described
using a standard (finite) context-free grammar,
and more interestingly
that normal inhabitants of types with the same structure are
described by identical context-free grammars, up to renaming of symbols.