# What's the expressive power of Simply Typed Lambda calculus?

The standard approach to simply typed lambda calculus considers computations over Church numerals. If input and outputs are Church numerals always typed as $Int$, where $Int = (\tau \rightarrow \tau) \rightarrow \tau \rightarrow \tau$, a result of Schwichtenberg showed that expressible functions are the extended polynomials.

If inputs are Church numerals given more complex types than $Int$, exponentiation and predecessor can be expressed (however Statman showed that equality, ordering and subtraction are not expressibile for any typing of church numerals.

However we should be more permissive and provide only an output restriction: a boolean type ( $Bool = \tau \rightarrow \tau \rightarrow \tau$). Under this convention, Statman's theorem that "deciding equivalence of normal forms of two simply typed lambda-terms is not elementary recursive" can be seen as an expressibility result (right?): we can express nonelementary functions.

Pushing to the limit, where we can arrive? Of course (by strong normalization) we can express only total functions. But I'm asking if there is a precise upper bound to simply typed lambda calculus expressive power.

I've found many articles, in particular "On the expressive power of simply typed and let-polymorphic lambda calculi" but I'm not able to understand if it is what I'm looking for.

• A base type is never equal to a function type (a mistake appearing twice in this question). I think you're trying to say that the final output of a function type is a particular base type, which is different. Jul 28, 2012 at 19:52
• @HuckBennett: That is false. The encoding for the type of Church numerals in the simply typed lambda calculus is (A -> A) -> A -> A where the numerals are defined as usual. Likewise the type of the booleans is indeed A -> A -> A where true = \x . \y . x and false = \x . \y . y. Jul 29, 2012 at 3:51
• @Anthony: My mistake. I didn't realize that Church encodings were used except in the untyped lambda calculus. Jul 29, 2012 at 7:03
• Why does “deciding equivalence of normal forms of two simply typed lambda-terms is not elementary recursive” imply that you can express nonelementary functions? I do not think that there is any guarantee that equivalence can be expressed. Jul 29, 2012 at 11:45
• Looking forward for this answer in 2015, any luck yet? Oct 5, 2015 at 19:08

More precisely, let the order of a type be defined as the nesting depth of → to the left ($$ord(o) = 0$$ and $$ord(A \to B) = max(ord(A)+1, ord(B))$$) and the level of a term be the greatest order of the type of one of its subterms. Then for terms of level at most k, normalization is in O(k)-EXPTIME (*). So if you consider input/output encodings such that the order of terms may depend on the function being represented, but not on the input, then all the functions you can represent are elementary recursive (i.e. in the union of the k-EXPTIME classes over all k). This condition seems to be satisfied by practically all typable encoding schemes that one could naturally come up with.