  Godel's theory T can be understood as a theory of the simply-typed lambda
calculus that is extended to include the constant 0, the successor function S,
and the operator R_tau for primitive recursion on objects of type tau. It is
known that the functions from non-negative integers to non-negative integers
that can be defined in this theory are exactly the <epsilon_0-recursive
functions of non-negative integers. As an extension of this result, we show
that when the domain and codomain are restricted to pure closed normal forms,
the functionals of arbitrary type that are definable in T can be encoded as
<epsilon_0-recursive functions.
