Request for elucidation

[cpressey]

Hello Wouter,

I hate to ask you to revisit a subject you're fed up with, but, would you be so kind as to add some words to the README explaining just what the confusion you tended to encounter was?

The way I understand the terms, "total" and "Turing-complete" are obviously different:

• A system is total iff it always produces a final result.
• A system is Turing-complete iff it can simulate any Turing machine.
• Some Turing machines run forever, never producing a final result.
• Therefore, a Turing-complete system cannot be total, and a total system cannot be Turing-complete.

So it is difficult for me to see how you could encounter so much confusion.

But definitions vary; and perhaps these have special definitions in the context of Agda that I'm not aware of?

Also, it seems the term "Turing-complete" in particular is subject of a certain amount of abuse. For example, Conway's Game of Life automaton per se can only simulate Turing machines that never halt. You'd have to add some kind of "halting predicate" to Life to make it Turing-complete. But that doesn't stop people from informally calling it Turing-complete.

Cheers, -Chris

[wouter-swierstra]

Hi @cpressey,

Thanks for your question!

I guess I'd argue with your definition of 'total' -- if you take it in the sense of Turner's "Total Functional Programming" (sometimes also called Strong Functional Programming) -- it should rule out non-termination. This is slightly different from 'every computation returns a final result'; if you take that definition, you would rule out things like webservers, operating systems, and so forth: programs that run forever, but always respond to user input within a finite amount of time. It's a much more subtle notion of totality.

Turner (and many others) argue that it's OK for a program to use 'productive coinduction' -- which roughly says you can describe infinite data structures (such as the trace of execution steps that a Turing machine makes), as long as you can always produce 'the next element' in finite time (which rules out loops that sit there and do nothing). Turner explains it much better than I can in his paper on Total Functional Programming. Does that answer your question?

[cpressey]

Thanks for the response - it does help me understand that you are using "total" in a way I'm not accustomed to.

I do think it's a bit unfortunate that "total" has been overloaded to have a second, expanded meaning, inside functional programming. Being more familiar with Büchi automata than codata, I would have called the property you describe something like "ω-liveness", myself. (And if a system allows me to write an operating system in it, I can't really bring myself to describe that system as "ruling out non-termination." I would have to add "between inputs" to that phrase.) But I suppose naming conflicts are inevitable across fields of study.

However, I still don't quite see how this concept can get confused with Turing-completeness very easily. An idealized tally counter, for example, is total by your definition: advancing the counter always completes, and always returns to a state where you can advance the counter again. But it is clearly not Turing-complete.

[cpressey]

Thanks for the link to the paper, btw. It's interesting reading.

Reflecting a bit, I now suspect the confusion might've been this (please correct me if I'm wrong):

With your definition of total, totality and Turing-completeness are orthogonal (or virtually so, at least, with maybe some minor qualifications about how one can "interact" with a Turing machine,) so you wrote this Brainfuck interpreter to demonstrate that one can write a functional program which is both total and Turing-complete.

If that is the case, then the confusion you encountered (I would guess) is almost certainly due to people taking the meaning of "total" as it is used in function theory and computability theory, as I was.

Because, with the original mathematical meaning of "total", if you had a function that is both total and Turing-complete, you would have a solution to the halting problem; therefore these two properties are exclusive (see the bullet points in my first comment.)

And I can see how people who use that definition would take great exception at the claim you've written such a program.

This is, again, why I dislike that the term "total" has been overloaded this way -- it leads to confusion. Perhaps I'll simply avoid using it in the future.

[wouter-swierstra]

Thanks for your comments.

I the general confusion that I encounter is that:

'total functions must terminate, and hence a total language cannot be Turing complete.'

This program shows how to embed a Turing complete language (Brainfuck) in a total language (Agda), contradicting the above statement. The crucial insight is that totality (in the presence of codata) does not mean 'terminating in finite time', but something more subtle. I agree that a lot of this has to do with confusion or misunderstanding about what exactly 'total' means.

[cpressey]

Yes. I discussed this with a few colleagues this afternoon, and I see what you're saying, now.

You have defined, in Agda, a function which maps Brainfuck programs to possibly-infinite execution traces.

This function is total because there is no Brainfuck program which it does not map to a possibly-infinite execution trace.

I think one of the sources of confusion is that "total" has acquired some extra connotations in computability theory (for better or worse.) For example, in one of Dexter Kozen's textbooks, he uses the term "total Turing machine" to mean a Turing machine which always halts.

I have some further thoughts on the subject of total functional programming, but they are beyond the scope of this issue. Suffice to say, thank you again for pointing me to Turner's paper.

To step back, the goal of this issue was to add a few words to the README for anyone who, like me, stumbles across this repository and would like more context to help them better understand why you wrote this.

To that end, I could open a pull request to add something to the README. I can certainly do that if you like -- it may be simplest to just add a link to this issue -- but I also wouldn't want to put words in your mouth. I'll leave this decision up to you.

Thank you for your time, -Chris

[wouter-swierstra]

No worries -- I'll update the README to make it slightly less cryptic.

Thanks again for the interesting discussion!