20
$\begingroup$

What are the limitations of total functional programming? It is not Turing-complete, but still supports a large subset of the possible programs. Are there important constructs that you could write in a Turing-complete language, but not in a total functional language?

And is it correct to say that programs written in total functional languages can be completely statically analysed, while static analysis in Turing-complete languages is limited by things like the halting problem? With that I do not mean that in total functional languages everything can be staticaly determined, because some things are only known at runtime, but I mean that in theory, programs written in an ideal total functional programming language, can be analysed so that everything that could in theory be determined statically can be determined statically. Or are there still undecidable problems inherit in total functional languages that make static analysis incomplete? Some problems will always be undecidable, no matter in which language they are written, but I am interested in such problems that are inherit to the language, like the halting problem in Turing-complete languages.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
17
$\begingroup$

It depends on the total functional language.

This answer sounds like a cop-out, but nothing more specific can be said. After all, consider whatever important decidable program that you're interested in. Write a program in your favorite Turing-complete language to solve it. Since the problem is decidable, your program will halt on all inputs.

(Arguably, a non-decidable problem could have interesting programs, but not such that people can use, because they'll never be able to wait long enough to know the answer.)

Now, define a new language such that it has only one valid input program: the program that you just wrote, with the same semantics as it had before. It's certainly total, since all inputs to all programs written in it (of which there's only one) always terminate.

This cheap trick is actually useful: the language Coq, for example, is a total functional language in that no program typechecks unless there is a proof that it terminates. (If you were to waive that requirement, it would be Turing-complete, so the only obstacle is finding a proof of termination.)

I'm not sure what you mean by "everything that could in theory be determined statically can be determined statically"; it sounds tautologically true. Nonetheless, total languages aren't inherently easy to analyze; you know that nothing diverges, which is a useful fact, but the relationship between input and output is still complex. (In particular, there are still infinitely many possible inputs, so you can't exhaustively try them all, even in theory.)

Improve this answer
$\endgroup$
5
  • $\begingroup$ Thanks for your answer. So being total helps somewhat, but it remains a very difficult problem. What I meant with "everything that could in theory be determined statically can be determined statically" was that would it be possible, extremely difficult or not, to analyse all the relationships between input and output, if you were to have enough resources to do so. Or are the fundamental reasons why this is limited? Like Rice's theorm proofs that this is the case for partial functions. Or am I misunderstanding Rice's theorem? $\endgroup$
    – Matthijs Steen
    Oct 31, 2012 at 10:23
  • $\begingroup$ I think it may depend on what you mean by "relationship". In particular, if you just mean "input A goes to output B", this is trivially determinable in a total functional language; just run the program. But you're probably interested in analyses that say something about an infinite class of inputs. $\endgroup$
    – Paul Stansifer
    Oct 31, 2012 at 12:29
  • $\begingroup$ (oops; hit enter accidentally) ...but this opens up another silly trick, because I can ask undecidable questions about the identity function if I want to: "For some X, is (identity X) a Turing Machine that halts?" Sure, that doesn't seem to be about identity, but how do you define "about"? $\endgroup$
    – Paul Stansifer
    Oct 31, 2012 at 12:35
  • $\begingroup$ Yes, I want to know whether it holds for all the possible input values of some definition, not for individual inputs. So if I understand you correctly, you mean that there will always be some undecidable questions, no matter what type of programming language used? Although some of this undecidable questions might be circumvented by preventing the problem from occuring in the first place, like total functional languages for the Halting Problem? Because wouldn't your question about the identity function be decidable in a total functional language? $\endgroup$
    – Matthijs Steen
    Oct 31, 2012 at 15:41
  • $\begingroup$ Yes; a modified version of the problem, in which "Turing Machine" is replaced by "Breaks Down After Its Warranty Expires Turing Machine" is trivially solvable. It's sort of troublesome for these purposes that the halting problem is the go-to example of an undecidable problem when examining programs is chock-full of undecidability. $\endgroup$
    – Paul Stansifer
    Nov 3, 2012 at 0:47
16
$\begingroup$

What are the limitations of total functional programming? It is not Turing-complete, but still supports a large subset of the possible programs. Are there important constructs that you could write in a Turing-complete language, but not in a total functional language?

Assuming your functional language $L$ lets you encode arithmetic operations, there is one program that you can count on not being expressible if it is total: namely, an interpreter for $L$, written in $L$.

  1. The proof of this fact is essentially Goedel's incompleteness theorem, viewed through the lens of the Curry-Howard correspondence. Recall that a consistency proof is a proof that false is not derivable.in a logical system. Since CH says proofs are programs, a consistency proof is hence a proof that there are no closed programs of the empty type. (Note that non-termination gives you an easy way to inhabit all types, since the looping program can be given any type you like, since it will never evaluate to a value.) So in a total functional language, a self-interpreter for $L$ gives a proof in $L$ that every program in $L$ terminates, and hence proves that $L$ is consistent. This is just what Goedel's theorem rules out, assuming you can do arithmetic. So we know that we can't write self-interpreters in total functional languages.

  2. The flip side of this, though, is that the limits on the expressive power of total languages are essentially the limits on the expressive power of mathematics itself. For example, the functions definable in Coq (a proof assistant) are those that can be proved to be computable using ZFC, with countably many inaccessible cardinals. So essentially any function that you could prove total to the satisfaction of a working mathematician is definable in Coq.

  3. The flip side of the flip side is that mathematics is hard! So there's no easy sense in which total languages are "completely analyzable" -- even if you know that a function terminates, you may still have to do a lot of creative work to prove that it has a property that you want. For example, just knowing that a function from lists to lists is total, doesn't get you very far in proving that it is a sorting function....

Improve this answer
$\endgroup$
4
  • $\begingroup$ Thanks for your answer. I have read the post about this problem at the Lambda the Ultimate weblog, but some people in the comments state that although it is not possible to have it's own evaluator as a regular explicitly constructible term, it would be possible to create a working self-evaluator with some tricks. So I wonder, are there problems that cannot be solved (or approximated) in a total functional language with some tricks of detours? $\endgroup$
    – Matthijs Steen
    Oct 31, 2012 at 9:55
  • $\begingroup$ I would say that self-evaluation does not count as a problem, because it varies depending on the language. The problem "evaluate a program in language X" is the same problem, regardless of whether you try to solve it in language X or Y. In particular, if language X is a total functional language, the problem is solvable in some total functional language, using the same silly trick I used before. $\endgroup$
    – Paul Stansifer
    Oct 31, 2012 at 12:11
  • $\begingroup$ Neel, it seems like it should be considerably easier than that to prove that a total language cannot support its own interpreter. Am I misunderstanding you? By a simple diagonalization, any language with a function with no fixed points cannot support its own interpreter (whether it supports arithmetic or not). The argument is elaborated by Conor McBride here: mail.haskell.org/pipermail/haskell-cafe/2003-May/004343.html $\endgroup$
    – Tom Ellis
    Mar 7, 2015 at 20:19
  • $\begingroup$ @TomEllis: My argument is essentially the same as Conor's. In fact, his post already makes this observation (with Conor's characteristic wit) when he calls it "the Epimenides/Cantor/Russell/Quine/Godel/Turing argument." $\endgroup$
    – Neel Krishnaswami
    Mar 8, 2015 at 13:35

Your Answer

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

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