21
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ I think the answer is yes: we can express the bounded-time universal Turing machine. $\endgroup$ – Kaveh Dec 14 '14 at 4:33
  • 3
    $\begingroup$ 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. I can post a more detailed answer if you want. $\endgroup$ – Damiano Mazza Dec 14 '14 at 20:49
  • 1
    $\begingroup$ 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$. $\endgroup$ – Damiano Mazza Dec 14 '14 at 20:57
  • 4
    $\begingroup$ The Ackermann function can be expressed in the calculus of constructions, so it can't be right that that one is just doubly exponential. $\endgroup$ – Andrej Bauer Dec 15 '14 at 17:01
  • $\begingroup$ I think I read about that bound in the Coq'Art book but I am very likely mistaken. Thanks! $\endgroup$ – jkff Dec 15 '14 at 21:32
19
$\begingroup$

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 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 (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 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. 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, 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 to a MO question about "unknown theorems").

$\endgroup$
  • 3
    $\begingroup$ 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. $\endgroup$ – MaiaVictor Oct 5 '15 at 19:17
  • $\begingroup$ @Damiano Mazza. Liked your answer, but the notion of "uniformity" is not so trivial, isn't it? $\endgroup$ – Andrea Asperti Mar 8 '17 at 15:32
  • $\begingroup$ 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... $\endgroup$ – Damiano Mazza Mar 9 '17 at 11:58
12
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks @Neel! I guess that now we have the full picture. $\endgroup$ – Damiano Mazza Dec 17 '14 at 22:28
7
$\begingroup$

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

In general a typed $\lambda$-calculus can be used as a language of realizers 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 to control duplication. One such example is given by Baillot and Terui.

In general this is a large avenue of research, so I'll just refer to one of my previous answers.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.