20
$\begingroup$

Is there a typed lambda calculus where the corresponding logic under the Curry-Howard correspondence is consistent, and where there are typeable lambda expressions for every computable function?

This is admittedly an imprecise question, lacking a precise definition of "typed lambda calculus." I'm basically wondering whether there are either (a) known examples of this, or (b) known impossibility proofs for something in this area.

Edit: @cody gives a precise version of this question in his answer below: is there a logical pure type system (LPTS) which is consistent and Turing complete (in a sense defined below)?

$\endgroup$
  • 2
    $\begingroup$ There is no recursively axiomatizable calculus (lambda or otherwise) whose provably total recursive functions are all recursive functions, so your calculus would have to involve non-terminating terms. $\endgroup$ – Emil Jeřábek Apr 26 '15 at 11:09
  • 2
    $\begingroup$ This answer has a theorem which says you can't have any sort of calculus that is both Turing-complete and total. $\endgroup$ – Andrej Bauer Apr 26 '15 at 15:57
  • 1
    $\begingroup$ It will likely answer your question once you make it sufficiently precise. I think Andrej’s proof is unnecessarily complicated (but it shows more): the point is simply that if there were an effectively described system where all recursive function were representable in such a way that you can syntactically certify that an expression is an honest representation of a recursive function (e.g., by checking that it is correctly typed in the system), then you would obtain a universal total recursive function, which is impossible. $\endgroup$ – Emil Jeřábek Apr 26 '15 at 20:10
  • 1
    $\begingroup$ Of course a classic answer to this kind of question could be: typed $\lambda$-calculus with intersection types, since it types every (and only those) terms which are strongly normalizing. It's more of a philosophical question to ask whether or not the calculus admits a "Curry-Howard interpretation" though. $\endgroup$ – cody Apr 26 '15 at 23:57
  • 2
    $\begingroup$ It's hard to be more precise here because the question is not precise. $\endgroup$ – Andrej Bauer Apr 28 '15 at 5:57
21
$\begingroup$

Alright I'll give a crack at it: In general for a given type system $T$, the following is true:

If all well-type terms in the calculus $T$ are normalizing, then $T$ is consistent when viewed as a logic.

The proof generally proceeds by assuming you have a term $\mathrm{absurd}$ of type $\mathrm{False}$, using subject reduction to get a normal form, and then proceeding by induction on the structure of such a term to get a contradiction.

It is natural to wonder if the converse holds, i.e.

For any type system $T$, if $T$ is logically consistent, then every well-typed term in $T$ is normalizing.

The problem with this is that there is no real most general notion of "type system", and even less agreement on the meaning of logical consistency for such systems. However, we can empirically verify that

For most known type systems which have a logical interpretation, the converse does indeed hold.

How does this tie into Turing Completeness? Well, for one, if type-checking is decidable, then Andrej's argument shows that one of the following must hold:

  1. The set of all well-typed programs is not Turing Complete.
  2. There is a non-terminating well typed program.

This tends to suggest that:

Type systems which have a logical interpretation and are consistent and are recursively enumerable are not Turing Complete.

Giving an actual theorem rather than a suggestion requires making the notion of type systems and logical interpretations mathematically precise.

Now two remarks come to mind:

  1. There is an undecidable type system, the intersection type system which has a logical interpretation and can represent every normalizing $\lambda$-term. As you remark, this isn't quite the same as being Turing Complete, as the type of a total function may need to be updated (refined, in fact) before applying it to the desired argument. The calculus is a "curry style" calculus and is equal to STLC + $$ \frac{\Gamma\vdash M:\tau\quad \Gamma\vdash M:\sigma}{\Gamma\vdash M:\tau\cap\sigma} $$ and $$\frac{\Gamma\vdash M:\tau\cap\sigma}{\Gamma\vdash M:\tau}\quad \frac{\Gamma\vdash M:\tau\cap\sigma}{\Gamma\vdash M:\sigma}$$ It is clear that the "interpretation" $\cap=\wedge$ leads to a consistent logical interpretation.

  2. There is a class of type systems, the Pure Type Systems, in which such a question might be made precise. In this framework however, the logical interpretation is less clear. One might be tempted to say: "a PTS is consistent if it has an uninhabited type". But this doesn't work, since types may live in different "universes", where some might be consistent and some not. Coquand and Herbelin define a notion of Logical Pure Type Systems, in which the question makes sense, and show

    Every inconsistent, non-dependent LPTS has a looping combinator (and so is Turing Complete)

    Which answers the question in one direction (inconsistent $\Rightarrow$ TC) in this case. As far as I know, the question for general LPTS is still open and quite difficult.


Edit: The converse of the Coquand-Herbelin result is not as easy as I thought! Here is what I came up with so far.

A Logical Pure Type System is a PTS with (at least) the sorts $\mathrm{Prop}$ and $\mathrm{Type}$, (at least) the axiom $\mathrm{Prop}:\mathrm{Type}$ and (at least) the rule $(\mathrm{Prop},\mathrm{Prop},\mathrm{Prop})$, with the further requirement that there are no sorts of type $\mathrm{Prop}$.

Now I'm going to assume a particular statement of Turing Completeness: fix an LPTS $L$ and let $\Gamma$ be the context

$$ \Gamma = \mathrm{nat}:\mathrm{Prop},\ 0:\mathrm{nat},\ S:\mathrm{nat}\rightarrow \mathrm{nat}$$

$L$ is Turing Complete iff for every total computable function $f:\mathbb{N}\rightarrow\mathbb{N}$ there is a term $t_f$ such that $$ \Gamma \vdash t_f : \mathrm{nat}\rightarrow \mathrm{nat}$$ and for every $n\in\mathbb{N}$ $$ t_f\ (S^n\ 0)\rightarrow^*_{\beta} S^{f(n)}\ 0$$

Now Andrej's diagonalization argument shows that there are non-terminating $t$ of type $\mathrm{nat}$.

Now it seems like we are half-way there! Given a non terminating term $\Gamma \vdash \mathrm{loop}:\mathrm{nat}$, we want to replace occurrences of $\mathrm{nat}$ by some generic type $A$ and get rid of $0$ and $S$ in $\Gamma$, and we will have our inconsistency ($A$ is inhabited in the context $A:\mathrm{Prop}$)!

Unfortunately this is where I get stuck, since it is easy to replace $S$ by the identity, but the $0$ is much harder to get rid of. Ideally we would like to use some Kleene recursion theorem, but I haven't figured this out yet.

$\endgroup$
  • $\begingroup$ OK, so first two clarifications about your remark (1). What do you mean when you say that this system of intersection types is not recursively enumerable? Certainly the set of theorems of the system is r.e., because you've given it as a straightforward sequent calculus. Also, the result I see proven in the paper you linked is that the terms typable in the system are exactly the strongly normalizing terms; but isn't that different from saying that it can type exactly the total computable functions? E.g., isn't $\lambda x. xx$ strongly normalizing, but not total? $\endgroup$ – Morgan Thomas Apr 30 '15 at 19:42
  • $\begingroup$ Now a question about your remark (2). It looks to me like the theorem you quote is not what we're interested in. It says that for every non-dependent LPTS, if it's inconsistent then it's Turing complete. But we'd like to know whether for every LPTS, if it's Turing complete then it's inconsistent. Am I misunderstanding something here? $\endgroup$ – Morgan Thomas Apr 30 '15 at 19:45
  • $\begingroup$ @MorganThomas: Ah, you are correct about the first point: what I meant to say is that the type system can not be decidable, that is, given $\Gamma, t, A$, the statement $\Gamma\vdash t:A$ is undecidable. I'll correct this in the post. $\endgroup$ – cody May 1 '15 at 14:31
  • $\begingroup$ The second point: you are also correct that one can have a non-total function that is well-typed (though one may not necessarily apply it to a given argument). I'll amend the answer. $\endgroup$ – cody May 1 '15 at 14:42
  • 1
    $\begingroup$ Third point. You are correct again! However the converse (in the special case of LPTS) is rather trivial. I'll outline the argument. $\endgroup$ – cody May 1 '15 at 14:56
11
+50
$\begingroup$

Here is an answer to a variant of @cody's precisification of my question. There is a consistent LPTS which is Turing complete in roughly @cody's sense, if we allow the introduction of additional axioms and $\beta$-reduction rules. Thus strictly speaking the system is not an LPTS; it is merely something much like one.

Consider the calculus of constructions (or your favorite member of the $\lambda$-cube). This is an LPTS, but we're going to add extra stuff which makes it not an LPTS. Choose constant symbols $\text{nat}, 0, S$, and add the axioms:

$$ \vdash \text{nat} : \ast $$ $$ \vdash 0 : \text{nat} $$ $$ \vdash S : \text{nat} \to \text{nat} $$

Index the Turing machine programs by natural numbers, and for each natural number $e$, choose a constant symbol $f_e$, add the axiom $f_e : \text{nat} \to \text{nat}$, and for all $e,x \in \mathbb{N}$, add the $\beta$-reduction rule

$$ f_e(x) \to_\beta \Phi_e(x), $$

where as usual $\Phi_e(x)$ is the output of the $e$th Turing machine program on $x$. If $\Phi_e(x)$ diverges then this rule doesn't do anything. Note that by adding these axioms and rules the system's theorems remain recursively enumerable, though its set of $\beta$-reduction rules is no longer decidable, but merely recursively enumerable. I believe we could easily keep the set of $\beta$-reduction rules decidable by spelling out explicitly the details of a model of computation in the syntax and rules of the system.

Now, this theory is clearly Turing complete in roughly @cody's sense, just by brute force; but the claim is that it's also consistent. Let's construct a model of it.

Let $U_1 \in U_2 \in U_3$ be three sets, such that:

  • $\emptyset, \mathbb{N}, 0, S \in U_1$ (where $S$ is the successor function).
  • Each set is transitive; if $a \in b \in U_i$, then $a \in U_i$.
  • Each set is closed under the formation of function spaces; i.e., if $A, B \in U_i$, then $B^A \in U_i$.
  • Each set is closed under the formation of dependent products; i.e., if $A \in U_i$ and $f : A \to U_i$, then $\prod_{a \in A} f(a) \in U_i$.

The existence of such sets follows, for example, from ZFC plus the axiom that every cardinal is bounded by an inaccessible cardinal; we can take each set $U_i$ to be a Grothendieck universe.

We define an "interpretation" to be a mapping $v$ from the set of variable names to elements of $U_2$. Given an interpretation $v$, we can define an interpretation $I_v$ of terms of the system in the evident way:

  • $I_v(x) = v(x)$, for $x$ a variable name.
  • $I_v(\ast) = U_1, I_v(\Box) = U_2$.
  • $I_v(\text{nat}) = \mathbb{N}, I_v(0) = 0, I_v(S) = S$.
  • $I_v(f_e) = \Phi_e$, i.e., the function $\mathbb{N} \to \mathbb{N}$ defined by the $e$th Turing program.
  • $I_v(AB) = I_v(A)(I_v(B))$, if $I_v(A)$ is a function with $I_v(B)$ in its domain, or $I_v(AB) = 0$ otherwise (just an arbitrary choice).
  • $I_v(\lambda x : A. B)$ is the function which maps an element $a \in I_v(A)$ to $I_{v[x:=a]}(B)$.
  • $I_v(\Pi x : A. B) = \prod_{a \in I_v(A)} I_{v[x:=a]}(B)$.

We have that for all terms $A$, $I_v(A) \in U_3$. Now we say that an interpretation $v$ satisfies $A : B$, written $v \models A : B$, if $I_v(A) \in I_v(B)$. We say that $\Gamma \models A : B$ if for all interpretations $v$, if $v \models x : C$ for all $(x : C) \in \Gamma$, then $v \models A : B$.

It is straightforward to check that if $\Gamma \vdash A : B$, then $\Gamma \models A : B$, so this is a model of the system. But, for any variables $x,y$, it is not the case that $y : \ast \models x : y$, because we can interpret $y$ by $\emptyset$, so the system is consistent.

Now, this is an answer to my original question, in the sense that this is something that it's reasonable to call a typed lambda calulus, which is consistent and Turing complete. However, it's not an answer to @cody's question, because this is not an LPTS, because of the addition of extra axioms and $\beta$-reduction rules. I imagine that the answer to @cody's question is much harder.

$\endgroup$
  • 2
    $\begingroup$ This is a nice answer, but I'm not sure you need to go through all those calisthenics to prove consistency: a term of type $A$ in the empty context can be "de-sugared" to a term in the CoC: I'll call the $f_e(x)\rightarrow \Phi_e(x)$ rules $\iota$-rules and keep $\beta$ for the usual ones. Perform all $\beta$-reductions (this terminates since you have only added constants), and replace every term of the form $f_e(x)$ by its reduct if it has one. The idea here is that the $\iota$-rules only operate on ground terms, so you can do all the $\beta$-reductions first to get them out of the way. $\endgroup$ – cody May 9 '15 at 21:40
  • $\begingroup$ I think you're right. This is not my field, so I'm a bit clumsy doing things. :-) I think your proof works, and one interesting consequence, if I'm right, is that this theory doesn't have very much consistency strength. It looks like a potentially very powerful theory, since it has types and natural numbers, which should let you interpret set theory; but apparently you can't, because you can prove it consistent without using powerful set theory! $\endgroup$ – Morgan Thomas May 10 '15 at 6:26

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.