Is there a typed lambda calculus which is consistent and Turing complete?

Question

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)?

Answer 1

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.

Answer 2

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.