<p>As explained by Damiano Mazza <a href="https://mathoverflow.net/questions/296312/do-you-know-important-theorems-that-remain-unknown/296879#296879">here on MathOverflow</a> (see also <a href="https://cstheory.stackexchange.com/questions/27824/can-typed-lambda-calculi-express-all-algorithms-below-a-given-complexity/27863#27863">this TCS.SE question</a>), for a very natural choice of encodings of input strings and output booleans, one gets exactly the regular languages! This is in fact a theorem in Hillebrand and Kanellakis's paper &quot;On the expressive power…&quot; that you mention (though your link seems dead).</p>
<p>By changing the input/output representation, one can get different things. For instance, the following paper shows that, when a certain input encoding inspired by relational databases is used, the simply typed λ-calculus can express exactly the elementary recursive predicates:
<a href="https://www.sciencedirect.com/science/article/pii/S0890540196900553" rel="nofollow noreferrer">https://www.sciencedirect.com/science/article/pii/S0890540196900553</a></p>
<p>In fact this <em>implies</em> Statman's result that convertibility is non-elementary: if it were, it would be decidable in time bounded by a tower of exponentials of fixed height, but the fact that all elementary recursive functions are representable makes this impossible. So Statman's theorem hints at an expressibility property, but not in the way you're saying; to the contrary, morally, reasonable encodings cannot yield anything beyond elementary recursive.</p>
<p>More precisely, let the <em>order</em> of a type be defined as the nesting depth of → to the left (<span class="math-container">$ord(o) = 0$</span> and <span class="math-container">$ord(A \to B) = max(ord(A)+1, ord(B))$</span>) and the <em>level</em> 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 <em>not</em> 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.</p>
<p>(*) see for instance <a href="https://www.beckmann.pro/PaperFiles/lambda.pdf" rel="nofollow noreferrer">https://www.beckmann.pro/PaperFiles/lambda.pdf</a> or <a href="https://www.kurims.kyoto-u.ac.jp/%7Eterui/nbi8.pdf" rel="nofollow noreferrer">https://www.kurims.kyoto-u.ac.jp/~terui/nbi8.pdf</a></p>
<p>(Let me mention that I've tried to clarify some of these points concerning the expressive power of STLC in the introduction to <a href="https://nguyentito.eu/thesis.pdf" rel="nofollow noreferrer">my PhD thesis</a> (sections 1.1.6, 1.3.5 and 1.3.6) though in retrospect I suspect the attempt is a failure…)</p>

CC BY-SA 4.0
2022-11-02T23:13:41.683Z
2022-11-03T13:08:32.657Z
2022-11-03T13:08:32.657Z
Lê Thành Dũng 'Tito' Nguyễn
<p>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 <strong>extended polynomials</strong>.</p>

<p>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.</p>

<p>However we should be more permissive and provide only an output restriction: a boolean type ( $Bool = \tau \rightarrow \tau \rightarrow \tau $).
Under this convention, <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.4048">Statman's theorem</a> 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.</p>

<p>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.</p>

<p>I've found many articles, in particular "<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.8845">On the expressive power of simply typed and let-polymorphic lambda calculi</a>" but I'm not able to understand if it is what I'm looking for.</p>

CC BY-SA 3.0
2012-07-28T19:52:10.717Z
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.
Huck Bennett
CC BY-SA 3.0
2012-07-29T03:51:15.440Z
@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.
Anthony
CC BY-SA 3.0
2012-07-29T07:03:30.767Z
@Anthony: My mistake. I didn't realize that Church encodings were used except in the untyped lambda calculus.
Huck Bennett
CC BY-SA 3.0
2012-07-29T11:45:51.447Z
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.
Tsuyoshi Ito
CC BY-SA 3.0
2012-07-29T15:06:45.663Z
@TsuyoshiIto: Sorry, you have reason. But in the article I linked on "Statman's theorem", Mairson shows that simply typed lambda-calculus can be used to simulate an arbitrary turing machine for nonelementary time.
Mycol
CC BY-SA 3.0
2015-10-05T19:08:12.580Z
Looking forward for this answer in 2015, any luck yet?
MaiaVictor
CC BY-SA 4.0
2021-03-28T08:12:24.350Z
I have not formally verified this but the inductive proof of strong normalizability of STLC as given in [Normalization without Reducibility](https://www.sciencedirect.com/science/article/pii/S0168007200000300) might be relevant.

The induction seems to be on the triple (length of typing derivation, depth of term, length of term) = (l,d,t). The length of a term can at most square when you do a substitution, the depth is at most the length. I think it follows that the length of the normal form can then be at most around 2^2^2^... (length l). Does this constitute a bound for the question?
Suhail Sherif
<lo.logic><lambda-calculus><upper-bounds>
What's the expressive power of Simply Typed Lambda calculus?
Mycol
# What's the expressive power of Simply Typed Lambda calculus?

(Asked by: username_0 on 2012-07-28)

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](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.4048) 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](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.8845)" but I'm not able to understand if it is what I'm looking for.

**Tags:** lo.logic, lambda-calculus, upper-bounds
> **Comments:**
> **username_1**: 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.  
> **username_2**: @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.  
> **username_1**: @Anthony: My mistake. I didn't realize that Church encodings were used except in the untyped lambda calculus.  
> **username_3**: 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.  
> **username_0**: @TsuyoshiIto: Sorry, you have reason. But in the article I linked on "Statman's theorem", Mairson shows that simply typed lambda-calculus can be used to simulate an arbitrary turing machine for nonelementary time.  
> **username_4**: Looking forward for this answer in 2015, any luck yet?  
> **username_5**: I have not formally verified this but the inductive proof of strong normalizability of STLC as given in [Normalization without Reducibility](https://www.sciencedirect.com/science/article/pii/S0168007200000300) might be relevant.  The induction seems to be on the triple (length of typing derivation, depth of term, length of term) = (l,d,t). The length of a term can at most square when you do a substitution, the depth is at most the length. I think it follows that the length of the normal form can then be at most around 2^2^2^... (length l). Does this constitute a bound for the question?  

---

## 1 answers

### Answer by username_6 on 2022-11-02. Score: 10

As explained by Damiano Mazza [here on MathOverflow](https://mathoverflow.net/questions/296312/do-you-know-important-theorems-that-remain-unknown/296879#296879) (see also [this TCS.SE question](https://cstheory.stackexchange.com/questions/27824/can-typed-lambda-calculi-express-all-algorithms-below-a-given-complexity/27863#27863)), for a very natural choice of encodings of input strings and output booleans, one gets exactly the regular languages! This is in fact a theorem in Hillebrand and Kanellakis's paper "On the expressive power…" that you mention (though your link seems dead).

By changing the input/output representation, one can get different things. For instance, the following paper shows that, when a certain input encoding inspired by relational databases is used, the simply typed λ-calculus can express exactly the elementary recursive predicates:
<https://www.sciencedirect.com/science/article/pii/S0890540196900553>

In fact this *implies* Statman's result that convertibility is non-elementary: if it were, it would be decidable in time bounded by a tower of exponentials of fixed height, but the fact that all elementary recursive functions are representable makes this impossible. So Statman's theorem hints at an expressibility property, but not in the way you're saying; to the contrary, morally, reasonable encodings cannot yield anything beyond elementary recursive.

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.

(\*) see for instance <https://www.beckmann.pro/PaperFiles/lambda.pdf> or [https://www.kurims.kyoto-u.ac.jp/~terui/nbi8.pdf](https://www.kurims.kyoto-u.ac.jp/%7Eterui/nbi8.pdf)

(Let me mention that I've tried to clarify some of these points concerning the expressive power of STLC in the introduction to [my PhD thesis](https://nguyentito.eu/thesis.pdf) (sections 1.1.6, 1.3.5 and 1.3.6) though in retrospect I suspect the attempt is a failure…)


---

