6
$\begingroup$

I myself have fallen prey to this misconception, i.e., that being dependently typed as in Agda, Coq, etc., implies not being Turing complete, which can be (whether now or previously) found at quite a few locations on the internet such as:

Various SE sites, such as:

Wikipedia (e.g., the Agda page), and elsewhere, such as:

Is this perhaps a problem with 'common understanding' regarding what it means to be Turing complete?

$\endgroup$
7
  • 1
    $\begingroup$ @MevenLennon-Bertrand why DTT seems to have become somehow associated with not being Turing complete (in many places outsiders such as myself stumble across). $\endgroup$ Commented May 28 at 11:02
  • 3
    $\begingroup$ My question is why is this such a contentious topic? I was genuinely surprised when someone accused me of spouting propaganda for saying that pure Lean wasn't Turing complete (your first link above). I felt in that particular case it was helpful as a pedagogical aid in my answer to explain the three types of languages in Lean. (Also, as a computability theorist by training, it was correct in that narrow interpretation.) Of course, you can program in any language with primitive recursion if you have the right interpretation. (A big enough for loop is a while loop in practice...) $\endgroup$
    – Jason Rute
    Commented May 28 at 23:46
  • 1
    $\begingroup$ The problem is that this is often implied to be some barrier to the programs that can be written in languages like Agda when that is just not the case. Like saying, "Haskell can't do I/O," because technically the I/O capabilities are an embedded language, not every expression. That is a misleading technicality unless further clarified. Similarly, the fact that, say, $ℕ → ℕ$ in Agda does not contain all Turing computable functions means little about your ultimate ability to write and execute Turing equivalent programs using Agda. $\endgroup$
    – Dan Doel
    Commented May 29 at 3:05
  • 2
    $\begingroup$ I think this is now more of a sociology and scientific communication problem than a proof assistants problem. $\endgroup$
    – Trebor
    Commented May 30 at 9:52
  • 1
    $\begingroup$ This has nothing to do with sociology and everything with insufficient knowledge of computability theory. There is no misconception here, dependent type theories that are total and have a computable normalization procedure are Turing-incomplete. This is a theorem (see my answer), not an opinion. Now, what the implication are for practical usability of dependent type theories that are total, that's an entirely different matter. $\endgroup$ Commented May 30 at 15:55

2 Answers 2

8
$\begingroup$

[Supplemental: I rewrote the answer so that any shred of vagueness is gone, as it was evoking religuous zeal, and I would prefer to stick to math. Everything is explained in terms of a widely accepted and general idea of models of computation, namely (typed) realizability theory. There are of course other ways of modeling computation, and anyone else is welcome to present a coherent mathematically mature alternative picture in their own answer.]

We work with typed partial combinatory algebras as models of computation. These include a host of examples, ranging from Turing machines, Turing machines with oracles, $\lambda$-calculi of various kinds, programming languages, topological models based on Scott domains, topological models based on the Baire space, etc. My notes on realizability cover all the material needed to understand the following definitions and theorems. I shall refer to theorems and definitions therein.

I shall call typed partial combinatory algebras (tpca)"models of computation". We shall also assume that all tpcas under consideration have numerals (Definition 2.6.3 of the notes.)

Kleene's first algbra $\mathbb{K}_1$ is the untyped pca whose elements are natural numbers and application is defined by $m \bullet n = \phi_m(n)$, where $\phi$ is a standard enumeration of partial computable maps.

Definition 1: A model of computation $\mathbb{A}$ is computable if it can be simulated by Turing machines, i.e., there exists a decidable simulation $\mathbb{A} \to \mathbb{K}_1$.

(See Definition 2.8.8 for definition of decidable simulation.)

From definition 1 it follows that any total function $\mathbb{N} \to \mathbb{N}$ realized (Definition 2.8.16) in a computable model is Turing computable.

Definition 2: A model of computation $\mathbb{A}$ is Turing-complete if there exists a decidable simulation $\mathbb{K}_1 \to \mathbb{A}$.

(Note: An alternative definition of Turing completeness of a tpca is given in the notes as 2.8.16. I will leave it as an exercise to think about what happens with the alternative definition.)

Martin-Löf type theory (MLTT) is a model of computation $\mathbb{M}$ whose types are the closed types of MLTT, and the elements of a type $T$ are the closed terms of type $T$, quotiented by definitional equality. (This is a standard way of turning a $\lambda$-calculus into a tpca, see John Longley's PhD for variations, such as using open terms.)

We have the following:

Theorem 3: Suppose $\mathbb{A}$ is a computable total typed combinatory algebra, with a decidable simulation $\gamma : \mathbb{A} \to \mathbb{K}_1$, such that the set $\{n \in \mathbb{N} \mid \exists \mathtt{t} \in |\mathbb{A}_{\mathtt{nat} \to \mathtt{nat}}| .\, \gamma(\mathtt{t}, n)\}$ is computably enumerable. Then $\mathbb{A}$ it is not Turing complete.

Proof. It may help to think of $\{n \in \mathbb{N} \mid \exists \mathtt{t} \in |\mathbb{A}_{\mathtt{nat} \to \mathtt{nat}}| .\, \gamma(\mathtt{t}, n)\}$ as the set of Gödel codes of elements of $\mathbb{A}$ of type $\mathtt{nat} \to \mathtt{nat}$.

Let $e : \mathbb{N} \to \{n \in \mathbb{N} \mid \exists \mathtt{t} \in |\mathbb{A}_{\mathtt{nat} \to \mathtt{nat}}| .\, \gamma(\mathtt{t}, n)\}$ be a computable enumeration. It suffices to find a Turing-computable total map $f : \mathbb{N} \to \mathbb{N}$ which is not realized by $\mathbb{A}$. Such a map $f$ is obtained by diagonalization against $e$: given $n \in \mathbb{N}$, there is $\mathtt{t} \in |\mathbb{A}_{\mathtt{nat} \to \mathtt{nat}}|$ such that $e(n) = \mathtt{t}$, and $f$ can compute (using $\gamma$) $k \in \mathbb{N}$ such that $\mathtt{t}\,\overline{n} + 1 = \overline{k}$. If $f$ were realized by some $\mathtt{f} \in |\mathbb{A}_{\mathtt{nat} \to \mathtt{nat}}|$, it would follow that $\mathtt{f} \, m = \mathtt{f} \, m + 1$ for some $m \in \mathbb{N}$ such that $\gamma(\mathtt{f}, e(m))$. $\Box$

Corollary 4: MLTT qua typed combinatory algebra $\mathbb{M}$ is not Turing complete.

Proof. Obviously, $\mathbb{M}$ is a total tpca. We may define a decidable simuation $\gamma : \mathbb{M} \to \mathbb{K}_1$ by setting $\gamma(\mathtt{t})$ to be the Gödel code of $\mathtt{t}$. The set featuring in the statement of Theorem 3 is computably enumerable because it is decidable whether a given number $n$ encodes a closed term of type $\mathtt{nat} \to \mathtt{nat}$ in MLTT. $\Box$

Remark: Corollary 4 applies to many variations of MLTT, such as MLTT with coinductive types, inductive types, etc, so long as it is decidable whether a given number encodes a closed term of type $\mathtt{nat} \to \mathtt{nat}$.

In type theory we often model computation by a monad, such as the delay monad (or Agda's $\mathtt{IO}$ monad suggested by Guillaume Allais). The basic idea is that the computable partial maps $\mathbb{N} \rightharpoonup \mathbb{N}$ are represented as closed terms of type $\mathtt{nat} \to \mathtt{Delay} \; \mathtt{nat}$, where $\mathtt{Delay}$ is a monad defined in an otherwise total type theory.

This sort of approach essentially corresponds to representing partial computable maps via the Kleene normal form theorem. The so-called "fuel" of the delay monad corresponds to Kleene's use the minimization operator in the normal form theorem.

Can we reintrpret a type theory with such a delay monad as a typed partial combinatory algebra? It seems so, although someone would have to check the details. The idea is to define the function type $\mathtt{t} \to \mathtt{u}$ of the corresponding tpca to be the type $\mathtt{t} \mathtt{Delay} \; \mathtt{u}$ of the type theory, and use the monadic bind to set up the tpca application operation. This should give a Turing-complete model of computation.

However, this is not at all useful to gauge the computational power of a type theory, because we can play the exact same trick with System T already (define $\mathtt{Delay} \; \mathtt{t} = \mathtt{nat} \to \mathtt{t}$ and use the input as fuel).

$\endgroup$
6
  • 1
    $\begingroup$ I challenge you to make Definition 2 precise by defining "model of computation" in enough generality that it includes Turing machines, lambda calculi, cellular automata, and other examples you can think of. Without such a definition Theorem 5 is neither provable nor refutable. I'd love to know one such general definition that doesn't have the fault that for any total programming language (MLTT, or even just STLC), there are at least two ways to formalize it as such a "model of computation" such that one is Turing-complete and the other is not. $\endgroup$
    – Li-yao Xia
    Commented May 30 at 16:02
  • $\begingroup$ @Li-yaoXia: I have rephrased my answer to a purely mathematical one. I invite anyone else who to give an alternative, similarly comprehensive mathematical account if they wish to do so. I am happy to answer further mathematical questiond and give clarifications, but I will not participate in a religuous war. (I also removed comments that were designed to trigger you, apologies for that.) $\endgroup$ Commented May 30 at 17:50
  • $\begingroup$ Is this a typed pca: consider STLC with Nat, a unary type constructor M, with return, bind, and a fix : (M a -> M a) -> M a. A pca type t denotes the STLC type [t], where the denotation is defined by [Nat] = M Nat, [t -> u] = M ([t] -> [u]), [t * u] = M ([t] * [u]). The set A(t) is the set of STLC terms of type [t]. One may object that this is no longer "STLC" because non-termination is possible via fix, or that this encoding of STLC as a pca is somehow not natural. I rather think that formal non-Turing-completeness claims very partially capture expressiveness. $\endgroup$
    – Li-yao Xia
    Commented May 30 at 17:54
  • $\begingroup$ My home-grown definition of model of computation is: a set of programs $P$ and an evaluation function $e : P \to (\mathbb{N} \rightharpoonup \mathbb{N})$. A pair $(P, e)$ is Turing-complete if $e$'s image includes the general recursive functions. It's intentionally broad, useless for theory. "What a language can express" is inherently a fuzzy notion, and that definition leaves room for that fuzziness. There may be more than one way to view a concrete language (e.g., STLC) as such a pair $(P,e)$: Turing-(in)completeness claims can only be made about specific encodings/usages of a language. $\endgroup$
    – Li-yao Xia
    Commented May 30 at 18:34
  • 1
    $\begingroup$ Be reassured that I was not offended in any way by your jabs. I make outrageous claims to provoke experts into giving me history lessons. $\endgroup$
    – Li-yao Xia
    Commented May 30 at 18:55
6
$\begingroup$

Is this perhaps a problem with 'common understanding' regarding what it means to be Turing complete?

Indeed it is: a pop-science understanding of dependent types has led to this myth being deeply ingrained after years of unfettered propagation. Turing completeness is about being able to write and run certain programs but some people insist it's about the types being given to these programs (not the ability to write them) which is silly because the notion predates typed languages...

It is true that MLTT without coinduction mandates that "functions always terminate" like a poster on the dev.to thread you linked says. But with coinduction you can happily write programs that are only required to demonstrably make progress on a regular basis. Waiting for a user-interrupt in the form of a Ctrl-C is a form of making progress and so you can absolutely write a program that will go on forever & attempt to run an arbitrary Turing machine / normalise an untyped lambda term.

It's not a hard problem to decide: the people claiming they're not Turing complete only have their strong belief to back their claims, the people claiming they are Turing complete actually show you programs that are supposedly impossible to write. Here, have an interpreter for the untyped lambda calculus in Agda.

$\endgroup$
8
  • 3
    $\begingroup$ I've always found this kind of debate utterly sterile. "MLTT is Turing-complete" is basically a rephrasing of Kleene's normal form theorem. $\endgroup$ Commented May 28 at 16:36
  • 8
    $\begingroup$ In particular, there is a technical definition of "Turing-complete" in extensions of System T, and by any means MLTT is not Turing-complete by this definition. So, to piss both sides: the people claiming MLTT is not Turing complete are technically right but are completely missing the point, while the people claiming MLTT is Turing complete are provably wrong but actually making an unrelated claim that boils down to "nobody gives rightfully a shit about Turing-completeness as long as your language has primitive recursion". $\endgroup$ Commented May 28 at 16:51
  • 1
    $\begingroup$ My point is that a stepper alone is proof of "Turing expressiveness" (and formal definitions of "Turing-completeness" that don't allow it are wrong). Here's another take: you don't need coinduction; you can use the fuel monad (Nat -> Maybe _) instead of the delay monad. $\endgroup$
    – Li-yao Xia
    Commented May 28 at 20:36
  • 2
    $\begingroup$ @Pierre-MariePédrot I think your comments would make a good answer. $\endgroup$
    – Jason Rute
    Commented May 28 at 23:37
  • 2
    $\begingroup$ I saved PMP from having to write a long diatribe. $\endgroup$ Commented May 30 at 7:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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