2
$\begingroup$

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?

Improve this question
$\endgroup$
1
  • $\begingroup$ It may be there is another function that always terminates, another "mov" function that may just terminate always, on all inputs, just that the one that you may have under consideration may not terminate.So, in a sense, Turing completeness is enforced by some "mov" function that terminates on all inputs, given a proper definition of "mov". Besides, Turing Ccompleteness guarantees an answer - non termination does not guarantee an answer. $\endgroup$
    – user3483902
    Commented Jan 28, 2019 at 18:46

1 Answer 1

Reset to default
2
$\begingroup$

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.

Improve this answer
$\endgroup$
0

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.