###
Technical Report: DCC-2001-1

###
Generating Normal Inhabitants of Types with a Common Structure

###
Sabine Broda and Luís Damas

DCC-FC & LIACC, Universidade do Porto

R. do Campo Alegre 823, 4150-180 Porto, Portugal

Phone: 351 22 6078830, Fax: 351 22 6003654

E-mail: {sbb,luis}@ncc.up.pt}
Junho 2000

##
Abstract

In 1996 Takahashi et al. showed 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
the sets of normal inhabitants of all types with a same structure are
described by context-free grammars which share one unique underlying
structure. The definition of a common scheme for these grammars, which
depends uniquely on the given type structure, is based on an
alternative representation for types, introduced in 2000
(BrodaDamas-Wollic-2000), which gives us a better insight on the
nature of a type's structure and its relation to the structure of the
set of its normal inhabitants.