Can one get Turing-completeness without nontermination? As I'm reading the movfuscator paper by Stephen Dolan, I encounter this claim:


  In order to have Turing-completeness, we must allow for nontermination.


This seems like a reasonable statement. But I'm also aware of this work by Wouter Swierstra which aims to prove quite the opposite (as I see it): that one can simulate a Turing-complete machine in a total language such as Agda.

From a purely theoretic point of view: I'm somewhat confused. Total languages permit only total functions, and total functions always terminate. Yet there exists a total interpreter of a Turing-complete language. Can somebody help reconcile this confusion?

Is nontermination necessary for Turing-completeness? Is this a valid question at all?
Many total languages, including Agda and Coq, allow you to define coinductive data types. These model infinite objects, like infinite lists.

Obviously, a function producing an infinite list cannot terminate. However, it must, in a total language, be productive. This means that any finite prefix of the produced infinite list can be computed in finite time. Coq and Agda have productivity checkers to ensure this, like they have termination checkers for functions which consume inductive data types.

Using these coinductive data types, you can model infinite executions. In the example you linked, 'running' a brainfuck program produces a trace, which is a potentially-infinite list of machine states.

Whether this is enough to declare the language 'Turing-complete' is, I guess, a question for philosophers. Agda only ever allows you to inspect a finite prefix of the generated trace, so you can't 'run' a program for an infinite amount of time. Then again, no physical machine can run a program for an infinite amount of time. And in practice, you can just disable Agda's termination checker for the one function that prints out your potentially-infinite trace.