<p>An answer to a question Damiano raised in his excellent answer:</p>

<blockquote>
  <p>I am much more ignorant regarding the calculi obtained by just enabling dependent types (essentially Martin-Löf type theory without equality and natural numbers), higher order types or both. In these calculi, types are powerful but terms can't access this power, so I don't know what you get. </p>
</blockquote>

<p>Adding dependent types does not change the consistency strength of the theory. Simple dependent types have the same consistency strength as the simply-typed lambda, and the calculus of constructions has the same consistency strength as System F$_\omega$. </p>

<p>In fact, pure Martin-Löf type theory ($\lambda{P}$ in the lambda-cube) cannot prove that 0=1 implies false. To do this, you need at least one universe -- and universes <em>gigantically</em> increase the strength of the theory. The calculus of inductive constructions (roughly speaking, $\lambda{P}\omega$ plus inductive types plus countably many universes) is equal in consistency strength to ZFC with countably many inaccessible cardinals. </p>

<p>I do not know what the strength of the impredicative calculus of constructions is, if you add inductive types and large eliminations.</p>

CC BY-SA 3.0
2014-12-17T22:28:39.390Z
Thanks @Neel!  I guess that now we have the full picture.
Damiano Mazza
CC BY-SA 3.0
2014-12-17T09:27:01.170Z
2014-12-17T09:27:01.170Z
Neel Krishnaswami
<p>I'll try to complement Damiano's excellent answer.</p>

<p>In general a typed $\lambda$-calculus can be used as a <a href="http://en.wikipedia.org/wiki/Realizability" rel="nofollow noreferrer">language of realizers</a> for a certain logic. In particular system $F$ is a language of realizers for <em>2nd order Heyting arithmetic</em> $\mathrm{HA}_2$. The informal theorem can be stated as follows</p>

<blockquote>
  <p>If the terms of a typed calculus $\cal{T}$ are the realizers for a logic $\cal{L}$, then the <em>definable functions</em> in $\cal{T}$ represent <strong>exactly</strong> the <em>provably total</em> functional relations in $\cal{L}$.</p>
</blockquote>

<p>The details are more murky of course, and $\cal{L}$ has to contain at least arithmetic, but the application of this idea gives</p>

<ul>
<li><p>The definable functions in system $F$ are the provably total functions in $\mathrm{HA}_2$ (this includes the Ackermann function, and much, much faster growing functions)</p></li>
<li><p>The definable functions in system $T$ are the provably total functions in $\mathrm{PA}$ (peano arithmetic). This also includes the Ackermann function (but includes much less than system $F$)!</p></li>
</ul>

<p>There are some typed $\lambda$-calculi that <em>exactly</em> capture $\mathrm{PTIME}$ computations. These usually involve <em><a href="http://en.wikipedia.org/wiki/Linear_logic" rel="nofollow noreferrer">linear type systems</a></em> to control duplication. One such example is given by <a href="http://www.sciencedirect.com/science/article/pii/S0890540108001119" rel="nofollow noreferrer">Baillot and Terui</a>.</p>

<p>In general this is a large avenue of research, so I'll just refer to one of my <a href="https://cstheory.stackexchange.com/questions/12585/to-what-extent-can-an-algorithm-predict-the-time-complexity-an-arbitrary-input-p/12592#12592">previous answers</a>.</p>

CC BY-SA 3.0
2014-12-17T05:02:20.350Z
Cf. Stephen Cook and Alasdair Urquhart's "[Functional interpretations of feasibly constructive arithmetic](http://dx.doi.org/10.1016/0168-0072(93)90044-E)", 1993, for a complexity theoretic variant.
Kaveh
CC BY-SA 3.0
2014-12-16T19:53:58.843Z
2014-12-16T19:53:58.843Z
2017-04-13T12:32:28.053Z
cody
<p>Two complements to Damiano's answer:</p>
<ul>
<li>in the simply typed λ-calculus, the expressible functions depend very much on the input and output representations, and for instance there is a way to make all elementary recursive predicates (and only them) definable as I explain in <a href="https://cstheory.stackexchange.com/questions/12156/whats-the-expressive-power-of-simply-typed-lambda-calculus/52102#52102">this other TCS.SE answer</a>;</li>
<li>since the question talks about typed λ-calculi in general, it is the perfect opportunity for a shameless self-advertisement: Pradic and I have found a variant of the characterization of regular languages that Damiano mentions, where we capture <em>star-free</em> languages using a <em>non-commutative</em> (i.e. <em>planar</em> or <em>ordered</em>) <em>affine</em> λ-calculus: <a href="https://cs-web.swan.ac.uk/%7Epierrepradic/aperiodic.pdf" rel="noreferrer">https://cs-web.swan.ac.uk/~pierrepradic/aperiodic.pdf</a></li>
</ul>

CC BY-SA 4.0
2022-11-02T23:21:57.223Z
2022-11-02T23:21:57.223Z
Lê Thành Dũng 'Tito' Nguyễn
<p>I will give a partial answer, I hope others will fill in the blanks.</p>

<p>In typed $\lambda$-calculi, one may give a type to usual representations of data ($\mathsf{Nat}$ for Church (unary) integers, $\mathsf{Str}$ for binary strings, $\mathsf{Bool}$ for Booleans) and wonder what is the complexity of the functions/problems representable/decidable by typed terms.  I know a precise asnwer only in some cases, and in the simply typed case it depends on the convention used when defining "representable/decidable".  Anyhow, I don't know of any case in which there is a doubly exponential upper bound.</p>

<p>First, a brief recap on the Lambda Cube.  Its 8 calculi are obtained by enabling or disabling the following 3 kinds of dependencies on top of the simply typed $\lambda$-calculus (STLC):</p>

<ul>
<li><strong>polymorphism</strong>: terms may depend on types;</li>
<li><strong>dependent types</strong>: types may depend on terms;</li>
<li><strong>higher order</strong>: types may depend on types.</li>
</ul>

<p>(The dependency of terms on terms is always there).</p>

<p>Adding polymorphism yields System F.  Here, you can type the Church integers with $\mathsf{Nat}:=\forall X.(X\rightarrow X)\rightarrow X\rightarrow X$, and similarly for binary strings and Booleans. Girard proved that System F terms of type $\mathsf{Nat}\rightarrow\mathsf{Nat}$ represent exactly the numerical functions whose totality is provable in second order Peano arithmetic. That's pretty much everyday mathematics (albeit without any form of choice), so the class is huge, the Ackermann function is a sort of tiny microbe in it, let alone the function $2^{2^n}$. I don't know of any "natural" numerical function which cannot be represented in System F. Examples usually are built by diagonalization, or encoding the consistency of second order PA, or other self-referential tricks (like deciding $\beta$-equality within System F itself).  Of course in System F you can convert between unary integers $\mathsf{Nat}$ and their binary representation $\mathsf{Str}$, and then test for instance whether the first bit is 1, so the class of decidable problems (by terms of type $\mathsf{Str}\rightarrow\mathsf{Bool}$) is equally huge.</p>

<p>The other 3 calculi of the Lambda Cube which include polymorphism are therefore at least as expressive as System F.  These include System F$_\omega$ (polymorphism + higher order), which can express exactly the provably total functions in higher order PA, and the Calculus of Constructions (CoC), which is the most expressive calculus of the Cube (all dependencies are enabled).  I don't know a characterization of the expressiveness of the CoC in terms of arithmetical theories or set theories, but it must be pretty frightening :-)</p>

<p>I am much more ignorant regarding the calculi obtained by just enabling dependent types (essentially Martin-Löf type theory without equality and natural numbers), higher order types or both. In these calculi, types are powerful but terms can't access this power, so I don't know what you get.  Computationally, I don't think you get much more expressiveness than with simple types, but I may be mistaken.</p>

<p>So we are left with the STLC. As far as I know, this is the only calculus of the Cube with interesting (i.e., not monstrously big) complexity upper bounds. There is an <a href="https://cstheory.stackexchange.com/questions/12156/whats-the-expressive-power-of-simply-typed-lambda-calculus">unanswered question about this</a> on TCS.SE, and in fact the situation is a bit subtle.</p>

<p>First, if you fix an atom $X$ and define $\mathsf{Nat}:=(X\rightarrow X)\rightarrow X\rightarrow X$, there is <a href="http://epub.ub.uni-muenchen.de/4273/" rel="noreferrer">Schwichtenberg's result</a> (I know there's an english translation of that paper somewhere on the web but I can't find it now) which tells you that the functions of type $\mathsf{Nat}\rightarrow\mathsf{Nat}$ are exactly the extended polynomials (with if-then-else). If you allow some "slack", i.e. you allow the parameter $X$ to be instantiated at will and consider terms of type $\mathsf{Nat}[A]\rightarrow\mathsf{Nat}$ with $A$ arbitrary, much more can be represented. For example, any tower of exponentials (so you may go well beyond doubly exponential) as well as the predecessor function, but still no subtraction (if you consider binary functions and try to type them with $\mathsf{Nat}[A]\rightarrow\mathsf{Nat}[A']\rightarrow\mathsf{Nat}$). So the class of numerical functions representable in the STLC is a bit weird, it is a strict subset of the elementary functions but does not correspond to anything well known.</p>

<p>In apparent contradiction with the above, there's <a href="http://www.cs.brandeis.edu/~mairson/Papers/statman.ps.gz" rel="noreferrer">this paper</a> by Mairson which shows how to encode the transition function of an <em>arbitrary</em> Turing machine $M$, from which you obtain a term of type $\mathsf{Nat}[A]\rightarrow\mathsf{Bool}$ (for some type $A$ depending on $M$) which, given a Church integer $n$ as input, simulates the execution of $M$ starting from a fixed initial configuration for a number of steps of the form
$$2^{2^{\vdots^{2^n}}},$$
with the height of the tower fixed. This <strong>does not</strong> show that every elementary problem is decidable by the STLC, because in the STLC there is no way of converting a binary string (of type $\mathsf{Str}$) representing the input of $M$ to the type used for representing the configurations of $M$ in Mairson's encoding. So the encoding is somehow "non-uniform": you can simulate elementarily-long executions from a fixed input, using a distinct term for each input, but there is no term that handles arbitrary inputs.</p>

<p>In fact, the STLC is extremely weak in what it can decide "uniformly".  Let us call $\mathcal C_{ST}$ the class of languages decidable by simply typed terms of type $\mathsf{Str}[A]\rightarrow\mathsf{Bool}$ for some $A$ (like above, you allow arbitrary "slack" in the typing). As far as I know, a precise characterization of $\mathcal C_{ST}$ is missing. However, we do know that $\mathcal C_{ST}\subsetneq\mathrm{LINTIME}$ (deterministic linear time). Both the containment and the fact that it is strict may be shown by very neat semantic arguments (using the standard denotational semantics of the STLC in the category of finite sets). The former was shown recently by <a href="http://www.kurims.kyoto-u.ac.jp/~terui/nbi8.pdf" rel="noreferrer">Terui</a>. The latter is essentially a reformulation of old results of Statman. An example of problem in $\mathrm{LINTIME}\setminus\mathcal C_{ST}$ is MAJORITY (given a binary string, tell whether it contains strictly more 1s than 0s).</p>

<hr>

<p><strong>(Much) Later add-on:</strong> I just found out that the class I call $\mathcal C_{ST}$ above actually <em>does</em> have a precise characterization, which is moreover extremely simple.  In <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.23.8845&amp;rep=rep1&amp;type=pdf" rel="noreferrer">this beautiful 1996 paper</a>, Hillebrand and Kanellakis prove, among other things, that</p>

<blockquote>
  <p><strong>Theorem.</strong> $\mathcal C_{ST}=\mathsf{REG}$ (the regular languages on $\{0,1\}$).</p>
</blockquote>

<p>(This is Theorem 3.4 in their paper).</p>

<p>I find this doubly surprising: I am surprised by the result itself (it never occurred to me that $\mathcal C_{ST}$ could correspond to something so "neat") and by how little known it is. It is also amusing that Terui's proof of the $\mathrm{LINTIME}$ upper bound uses the same methods employed by Hillebrand and Kanellakis (interpreting the simply-typed $\lambda$-calculus in the category of finite sets). In other words, Terui (and myself) could have easily re-discovered this result were it not for the fact that we were somehow happy with $\mathcal C_{ST}$ being a "weird" class :-)</p>

<p>(Incidentally, I shared my surprise in <a href="https://mathoverflow.net/a/296879/45027">this answer</a> to a MO question about "unknown theorems").</p>

CC BY-SA 3.0
2015-10-05T19:17:09.443Z
Finished reading the answer only to see that name yet again. I think you've already taught me more than my own professors. Internet is a beautiful thing. Thanks.
MaiaVictor
CC BY-SA 3.0
2017-03-08T15:32:27.160Z
@Damiano Mazza. Liked your answer, but the notion of "uniformity" is not so trivial, isn't it?
Andrea Asperti
CC BY-SA 3.0
2017-03-09T11:58:15.433Z
Hi @Andrea, thank you.  "Uniformity" here is just the fact that you decide a language using a single program working for all possible inputs, as opposed to deciding a language by means of an infinite family of programs, each working only on inputs of a fixed length (or, worse, one program for each input, as in Mairson's paper).  Uniformity is the norm in the $\lambda$-calculus ($\lambda$-terms are far too powerful to be used for non-uniform approaches, unless one considers restrictions such as linearity/affinity) so in a sense it is "trivial". But perhaps I am not understanding your comment...
Damiano Mazza
CC BY-SA 3.0
2014-12-16T16:43:54.757Z
2018-04-03T11:25:05.003Z
2018-04-03T11:25:05.003Z
Damiano Mazza
<p>I know that the complexity of most varieties of typed lambda calculi without the Y combinator primitive is bounded, i.e. only functions of bounded complexity can be expressed, with the bound becoming larger as the expressiveness of the type system grows. I recall that, e.g., the Calculus of Constructions can express at most doubly exponential complexity.</p>

<p>My question concerns whether the typed lambda calculi can express <strong>all</strong> algorithms below a certain complexity bound, or only some? E.g. are there any exponential-time algorithms not expressible by any formalism in the Lambda Cube? What is the "shape" of the complexity space which is completely covered by different vertices of the Cube?</p>

CC BY-SA 3.0
2014-12-14T04:33:20.853Z
I think the answer is yes: we can express the bounded-time universal Turing machine.
Kaveh
CC BY-SA 3.0
2014-12-14T20:49:18.620Z
Are you sure about the doubly exponential upper bound?  If I remember correctly, the CoC is the most expressive "corner" of the Lambda Cube, which means it includes System F (i.e. the polymorphic $\lambda$-calculus), which goes **way** beyond doubly exponential...  Anyway, the answer is definitely yes, see for example my answer [here](http://cstheory.stackexchange.com/questions/25423/can-affine-lambda-calculus-solve-every-problem-in-p?rq=1).  I can post a more detailed answer if you want.
Damiano Mazza
CC BY-SA 3.0
2014-12-14T20:57:37.107Z
Sorry, I misread your question, you're not asking about *some* typed $\lambda$-calculi but specifically about the typed $\lambda$-calculi of the Lambda Cube.  I'm afraid there is no interesting complexity there, they are all far too expressive, although I know the precise answer only for System F and System F$_\omega$.
Damiano Mazza
CC BY-SA 3.0
2014-12-15T17:01:29.167Z
The Ackermann function can be expressed in the calculus of constructions, so it can't be right that that one is just doubly exponential.
Andrej Bauer
CC BY-SA 3.0
2014-12-15T21:32:04.867Z
I think I read about that bound in the Coq'Art book but I am very likely mistaken. Thanks!
jkff
<cc.complexity-theory><complexity-classes><lambda-calculus><typed-lambda-calculus>
Can typed lambda calculi express *all* algorithms below a given complexity?
jkff
# Can typed lambda calculi express *all* algorithms below a given complexity?

(Asked by: username_0 on 2014-12-14)

I know that the complexity of most varieties of typed lambda calculi without the Y combinator primitive is bounded, i.e. only functions of bounded complexity can be expressed, with the bound becoming larger as the expressiveness of the type system grows. I recall that, e.g., the Calculus of Constructions can express at most doubly exponential complexity.

My question concerns whether the typed lambda calculi can express **all** algorithms below a certain complexity bound, or only some? E.g. are there any exponential-time algorithms not expressible by any formalism in the Lambda Cube? What is the "shape" of the complexity space which is completely covered by different vertices of the Cube?

**Tags:** cc.complexity-theory, complexity-classes, lambda-calculus, typed-lambda-calculus
> **Comments:**
> **username_1**: I think the answer is yes: we can express the bounded-time universal Turing machine.  
> **username_2**: Are you sure about the doubly exponential upper bound?  If I remember correctly, the CoC is the most expressive "corner" of the Lambda Cube, which means it includes System F (i.e. the polymorphic $\lambda$-calculus), which goes **way** beyond doubly exponential...  Anyway, the answer is definitely yes, see for example my answer [here](http://cstheory.stackexchange.com/questions/25423/can-affine-lambda-calculus-solve-every-problem-in-p?rq=1).  I can post a more detailed answer if you want.  
> **username_2**: Sorry, I misread your question, you're not asking about *some* typed $\lambda$-calculi but specifically about the typed $\lambda$-calculi of the Lambda Cube.  I'm afraid there is no interesting complexity there, they are all far too expressive, although I know the precise answer only for System F and System F$_\omega$.  
> **username_3**: The Ackermann function can be expressed in the calculus of constructions, so it can't be right that that one is just doubly exponential.  
> **username_0**: I think I read about that bound in the Coq'Art book but I am very likely mistaken. Thanks!  

---

## 4 answers

### Answer by username_2 on 2014-12-16. Score: 22 | Accepted answer

I will give a partial answer, I hope others will fill in the blanks.

In typed $\lambda$-calculi, one may give a type to usual representations of data ($\mathsf{Nat}$ for Church (unary) integers, $\mathsf{Str}$ for binary strings, $\mathsf{Bool}$ for Booleans) and wonder what is the complexity of the functions/problems representable/decidable by typed terms. I know a precise asnwer only in some cases, and in the simply typed case it depends on the convention used when defining "representable/decidable". Anyhow, I don't know of any case in which there is a doubly exponential upper bound.

First, a brief recap on the Lambda Cube. Its 8 calculi are obtained by enabling or disabling the following 3 kinds of dependencies on top of the simply typed $\lambda$-calculus (STLC):

* **polymorphism**: terms may depend on types;
* **dependent types**: types may depend on terms;
* **higher order**: types may depend on types.

(The dependency of terms on terms is always there).

Adding polymorphism yields System F. Here, you can type the Church integers with $\mathsf{Nat}:=\forall X.(X\rightarrow X)\rightarrow X\rightarrow X$, and similarly for binary strings and Booleans. Girard proved that System F terms of type $\mathsf{Nat}\rightarrow\mathsf{Nat}$ represent exactly the numerical functions whose totality is provable in second order Peano arithmetic. That's pretty much everyday mathematics (albeit without any form of choice), so the class is huge, the Ackermann function is a sort of tiny microbe in it, let alone the function $2^{2^n}$. I don't know of any "natural" numerical function which cannot be represented in System F. Examples usually are built by diagonalization, or encoding the consistency of second order PA, or other self-referential tricks (like deciding $\beta$-equality within System F itself). Of course in System F you can convert between unary integers $\mathsf{Nat}$ and their binary representation $\mathsf{Str}$, and then test for instance whether the first bit is 1, so the class of decidable problems (by terms of type $\mathsf{Str}\rightarrow\mathsf{Bool}$) is equally huge.

The other 3 calculi of the Lambda Cube which include polymorphism are therefore at least as expressive as System F. These include System F$\_\omega$ (polymorphism + higher order), which can express exactly the provably total functions in higher order PA, and the Calculus of Constructions (CoC), which is the most expressive calculus of the Cube (all dependencies are enabled). I don't know a characterization of the expressiveness of the CoC in terms of arithmetical theories or set theories, but it must be pretty frightening :-)

I am much more ignorant regarding the calculi obtained by just enabling dependent types (essentially Martin-Löf type theory without equality and natural numbers), higher order types or both. In these calculi, types are powerful but terms can't access this power, so I don't know what you get. Computationally, I don't think you get much more expressiveness than with simple types, but I may be mistaken.

So we are left with the STLC. As far as I know, this is the only calculus of the Cube with interesting (i.e., not monstrously big) complexity upper bounds. There is an [unanswered question about this](https://cstheory.stackexchange.com/questions/12156/whats-the-expressive-power-of-simply-typed-lambda-calculus) on TCS.SE, and in fact the situation is a bit subtle.

First, if you fix an atom $X$ and define $\mathsf{Nat}:=(X\rightarrow X)\rightarrow X\rightarrow X$, there is [Schwichtenberg's result](http://epub.ub.uni-muenchen.de/4273/) (I know there's an english translation of that paper somewhere on the web but I can't find it now) which tells you that the functions of type $\mathsf{Nat}\rightarrow\mathsf{Nat}$ are exactly the extended polynomials (with if-then-else). If you allow some "slack", i.e. you allow the parameter $X$ to be instantiated at will and consider terms of type $\mathsf{Nat}[A]\rightarrow\mathsf{Nat}$ with $A$ arbitrary, much more can be represented. For example, any tower of exponentials (so you may go well beyond doubly exponential) as well as the predecessor function, but still no subtraction (if you consider binary functions and try to type them with $\mathsf{Nat}[A]\rightarrow\mathsf{Nat}[A']\rightarrow\mathsf{Nat}$). So the class of numerical functions representable in the STLC is a bit weird, it is a strict subset of the elementary functions but does not correspond to anything well known.

In apparent contradiction with the above, there's [this paper](http://www.cs.brandeis.edu/~mairson/Papers/statman.ps.gz) by Mairson which shows how to encode the transition function of an *arbitrary* Turing machine $M$, from which you obtain a term of type $\mathsf{Nat}[A]\rightarrow\mathsf{Bool}$ (for some type $A$ depending on $M$) which, given a Church integer $n$ as input, simulates the execution of $M$ starting from a fixed initial configuration for a number of steps of the form
$$2^{2^{\vdots^{2^n}}},$$
with the height of the tower fixed. This **does not** show that every elementary problem is decidable by the STLC, because in the STLC there is no way of converting a binary string (of type $\mathsf{Str}$) representing the input of $M$ to the type used for representing the configurations of $M$ in Mairson's encoding. So the encoding is somehow "non-uniform": you can simulate elementarily-long executions from a fixed input, using a distinct term for each input, but there is no term that handles arbitrary inputs.

In fact, the STLC is extremely weak in what it can decide "uniformly". Let us call $\mathcal C\_{ST}$ the class of languages decidable by simply typed terms of type $\mathsf{Str}[A]\rightarrow\mathsf{Bool}$ for some $A$ (like above, you allow arbitrary "slack" in the typing). As far as I know, a precise characterization of $\mathcal C\_{ST}$ is missing. However, we do know that $\mathcal C\_{ST}\subsetneq\mathrm{LINTIME}$ (deterministic linear time). Both the containment and the fact that it is strict may be shown by very neat semantic arguments (using the standard denotational semantics of the STLC in the category of finite sets). The former was shown recently by [Terui](http://www.kurims.kyoto-u.ac.jp/~terui/nbi8.pdf). The latter is essentially a reformulation of old results of Statman. An example of problem in $\mathrm{LINTIME}\setminus\mathcal C\_{ST}$ is MAJORITY (given a binary string, tell whether it contains strictly more 1s than 0s).

---

**(Much) Later add-on:** I just found out that the class I call $\mathcal C\_{ST}$ above actually *does* have a precise characterization, which is moreover extremely simple. In [this beautiful 1996 paper](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.23.8845&rep=rep1&type=pdf), Hillebrand and Kanellakis prove, among other things, that

> **Theorem.** $\mathcal C\_{ST}=\mathsf{REG}$ (the regular languages on $\{0,1\}$).

(This is Theorem 3.4 in their paper).

I find this doubly surprising: I am surprised by the result itself (it never occurred to me that $\mathcal C\_{ST}$ could correspond to something so "neat") and by how little known it is. It is also amusing that Terui's proof of the $\mathrm{LINTIME}$ upper bound uses the same methods employed by Hillebrand and Kanellakis (interpreting the simply-typed $\lambda$-calculus in the category of finite sets). In other words, Terui (and myself) could have easily re-discovered this result were it not for the fact that we were somehow happy with $\mathcal C\_{ST}$ being a "weird" class :-)

(Incidentally, I shared my surprise in [this answer](https://mathoverflow.net/a/296879/45027) to a MO question about "unknown theorems").

> **Comments:**
> **username_7**: Finished reading the answer only to see that name yet again. I think you've already taught me more than my own professors. Internet is a beautiful thing. Thanks.  
> **username_8**: @Damiano Mazza. Liked your answer, but the notion of "uniformity" is not so trivial, isn't it?  
> **username_2**: Hi @Andrea, thank you.  "Uniformity" here is just the fact that you decide a language using a single program working for all possible inputs, as opposed to deciding a language by means of an infinite family of programs, each working only on inputs of a fixed length (or, worse, one program for each input, as in Mairson's paper).  Uniformity is the norm in the $\lambda$-calculus ($\lambda$-terms are far too powerful to be used for non-uniform approaches, unless one considers restrictions such as linearity/affinity) so in a sense it is "trivial". But perhaps I am not understanding your comment...  

---

### Answer by username_4 on 2014-12-17. Score: 13

An answer to a question Damiano raised in his excellent answer:

> I am much more ignorant regarding the calculi obtained by just enabling dependent types (essentially Martin-Löf type theory without equality and natural numbers), higher order types or both. In these calculi, types are powerful but terms can't access this power, so I don't know what you get.

Adding dependent types does not change the consistency strength of the theory. Simple dependent types have the same consistency strength as the simply-typed lambda, and the calculus of constructions has the same consistency strength as System F$\_\omega$.

In fact, pure Martin-Löf type theory ($\lambda{P}$ in the lambda-cube) cannot prove that 0=1 implies false. To do this, you need at least one universe -- and universes *gigantically* increase the strength of the theory. The calculus of inductive constructions (roughly speaking, $\lambda{P}\omega$ plus inductive types plus countably many universes) is equal in consistency strength to ZFC with countably many inaccessible cardinals.

I do not know what the strength of the impredicative calculus of constructions is, if you add inductive types and large eliminations.

> **Comments:**
> **username_2**: Thanks @Neel!  I guess that now we have the full picture.  

---

### Answer by username_5 on 2014-12-16. Score: 9

I'll try to complement Damiano's excellent answer.

In general a typed $\lambda$-calculus can be used as a [language of realizers](http://en.wikipedia.org/wiki/Realizability) for a certain logic. In particular system $F$ is a language of realizers for *2nd order Heyting arithmetic* $\mathrm{HA}\_2$. The informal theorem can be stated as follows

> If the terms of a typed calculus $\cal{T}$ are the realizers for a logic $\cal{L}$, then the *definable functions* in $\cal{T}$ represent **exactly** the *provably total* functional relations in $\cal{L}$.

The details are more murky of course, and $\cal{L}$ has to contain at least arithmetic, but the application of this idea gives

* The definable functions in system $F$ are the provably total functions in $\mathrm{HA}\_2$ (this includes the Ackermann function, and much, much faster growing functions)
* The definable functions in system $T$ are the provably total functions in $\mathrm{PA}$ (peano arithmetic). This also includes the Ackermann function (but includes much less than system $F$)!

There are some typed $\lambda$-calculi that *exactly* capture $\mathrm{PTIME}$ computations. These usually involve *[linear type systems](http://en.wikipedia.org/wiki/Linear_logic)* to control duplication. One such example is given by [Baillot and Terui](http://www.sciencedirect.com/science/article/pii/S0890540108001119).

In general this is a large avenue of research, so I'll just refer to one of my [previous answers](https://cstheory.stackexchange.com/questions/12585/to-what-extent-can-an-algorithm-predict-the-time-complexity-an-arbitrary-input-p/12592#12592).

> **Comments:**
> **username_1**: Cf. Stephen Cook and Alasdair Urquhart's "[Functional interpretations of feasibly constructive arithmetic](http://dx.doi.org/10.1016/0168-0072(93)90044-E)", 1993, for a complexity theoretic variant.  

---

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

Two complements to Damiano's answer:

* in the simply typed λ-calculus, the expressible functions depend very much on the input and output representations, and for instance there is a way to make all elementary recursive predicates (and only them) definable as I explain in [this other TCS.SE answer](https://cstheory.stackexchange.com/questions/12156/whats-the-expressive-power-of-simply-typed-lambda-calculus/52102#52102);
* since the question talks about typed λ-calculi in general, it is the perfect opportunity for a shameless self-advertisement: Pradic and I have found a variant of the characterization of regular languages that Damiano mentions, where we capture *star-free* languages using a *non-commutative* (i.e. *planar* or *ordered*) *affine* λ-calculus: [https://cs-web.swan.ac.uk/~pierrepradic/aperiodic.pdf](https://cs-web.swan.ac.uk/%7Epierrepradic/aperiodic.pdf)


---

