This is a naïve and, therefore, possibly malformed question, so apologies in advance!

My view is that a Turing Machine can be seen as the computational basis for procedural/imperative programming languages. Similarly, the lambda calculus is the foundation for functional programming languages.

I have recently learnt that the Church-Turing Thesis also shows mutual equivalence with a third model of computation: general recursive functions. Are there any programming languages that use this as their model of computation? If not, is there a technical reason why; i.e., besides "No one's tried yet"?

  • 1
    $\begingroup$ I would say that Turing machines or universal register machines are a basis of processor PLs (Assembly PLs). They do not have functions. $\mu$-recursive functions are a basis of imperative PLs. They do not have higher-order functions. $\endgroup$ – beroal Jul 30 '18 at 19:16
  • 1
    $\begingroup$ I would also recommend looking into first-order logic and Prolog. $\endgroup$ – beroal Jul 30 '18 at 19:18
  • 1
    $\begingroup$ Prior to C++11's constexpr you could (/had to) use 'templates' to have computations done at compile time by the compiler. The restrictions on templates do not allow loops, but you can use recursion to emulate any loop, so that you end up with a Turing-complete (meta-programming) facility as part of the C++ language standard, see e.g. stackoverflow.com/questions/189172/c-templates-turing-complete $\endgroup$ – JimmyB Aug 1 '18 at 9:40
  • 1
    $\begingroup$ See also en.wikipedia.org/wiki/Template_metaprogramming $\endgroup$ – JimmyB Aug 1 '18 at 9:49

Direct answer to the question: yes, there are esoteric and highly impractical PLs based on $\mu$-recursive functions (think Whitespace), but no practical programming language is based on $\mu$-recursive functions due to valid reasons.

General recursive (i.e., $\mu$-recursive) functions are significantly less expressive than lambda calculi. Thus, they make a poor foundation for programming languages. You are also not correct that the TM is the basis of imperative PLs: in reality, good imperative programming languages are much closer to $\lambda$-calculus than they are to Turing machines.

In terms of computability, $\mu$-recursive functions, Turing machine, and the untyped $\lambda$-calculus are all equivalent. However, the untyped LC has good properties that none of the other two have. It is very simple (only 3 syntactic forms and 2 computational rules), is highly compositional, and can express programming constructs relatively easily. Moreover, equipped with a simple type system (e.g., System $F\omega$ extended with $\mathsf{fix}$), the $\lambda$-calculus can be extremely expressive in that it can express many complex programming constructs easily, correctly and compositionally. You can also extend the $\lambda$-calculus easily to include constructs that are not lambdas. None of the other computational models mentioned above give you those nice properties.

The Turing machine is neither compositional nor universal (you need to have a TM for each problem). There are no concepts of "functions", "variables" or "composition". It is also not exactly true that TMs are the basis of imperative PLs - FWIW, imperative PLs are much, much closer to lambda calculi with control operators than to Turing machines. See Peter J. Landin's "A Correspondence Between ALGOL 60 and Church's Lambda-Notation" for a detailed explanation. If you have programmed in Brainf**k (which actually implements a rather simple Turing machine), you will know that Turing machines are not a good idea for programming.

$\mu$-recursive functions are similar to TMs in this respect. They are compositional, but not nearly as compositional as the LC. You also just can't encode useful programming constructs in $\mu$-recursive functions. Moreover, the $\mu$-recursive functions only compute over $\mathbb{N}$, and to compute over anything else you'd need to encode your data into natural numbers using some sort of Gödel numbering, which is painful.

So, it is not a coincidence that most programming languages are somehow based off the $\lambda$-calculus! The $\lambda$-calculus has good properties: expressiveness, compositionality and extensibility, that other systems lack. However, Turing machines are good for studying computational complexity, and $\mu$-recursive functions are good for studying the logical notion of computability. They both have outstanding properties that the $\lambda$-calculus lacks, but in the field of programming $\lambda$-calculus clearly wins.

In fact, there are many, many more Turing complete systems out there, but they lack any outstanding property whatsoever. Conway's Game of Life, LaTeX macros, and even (some claim) DNA are all Turing complete, but no one programs (i.e. do serious programming) with Conway or studies computational complexity using LaTeX macros. They simply lack good properties. Turing complete per se is nearly meaningless when it comes to programming.

Also, many non-Turing complete computational systems are very useful when it comes to programming. Regular expressions and yacc are not Turing complete, but they are extremely powerful in solving a certain class of problems. Coq is also not Turing complete, but it is incredibly powerful (it's actually considered much more expressive than its Turing complete cousin, OCaml). When it comes to programming, Turing completeness is not the key, as many (close to) useless systems are uninterestingly Turing complete. You're not going to claim that Brainf**k or Whitespace are more powerful programming languages than Coq, are you? An expressive foundation is the key to powerful programming languages, and that's why modern programming languages are almost always based on the $\lambda$-calculus.

  • 7
    $\begingroup$ "no one programs with Conway"... some do Build a working game of Tetris in Conway's Game of Life... also indeed it is as practical as whitespace :) $\endgroup$ – Alexei Levenkov Jul 31 '18 at 3:45
  • $\begingroup$ One way to see this is that a $\lambda$-calculus function that simulates Turing machines would probably be much shorter than a Turing machine that simulates the $\lambda$-calculus (not that I've seen either). $\endgroup$ – Noncontextual Spelling Jul 31 '18 at 6:28
  • $\begingroup$ @AlexeiLevenkov That is utterly untrue. Whitespace is essentially a (simple) imperative language, albeit with a strange syntax. It has facilities for arithmetic, basic control flow, stack and heap manipulation, and I/O. The QFT project, on the other hand, required designing a compiler from a very simple language down to a RISC assembly created for a CPU built within a Wireworld-like cellular automaton emulated using OTCA Metapixels. $\endgroup$ – Noncontextual Spelling Jul 31 '18 at 23:35
  • $\begingroup$ @AlexeiLevenkov The ultimate Cogol → CGoL compiler required the work of many people over four years, while there exists a project called HaPyLi, compiling a far more complex language to Whitespace, that was written by one person in their free time. $\endgroup$ – Noncontextual Spelling Jul 31 '18 at 23:39

Typing µ-recursive function programming language in Google led me to this GitHub repo, so the answer to your question is:

Yes, and it's called myopia

It's written in Haskell, by the way.

  • $\begingroup$ I'd add: but no practical programming language is based on $\mu$-recursive functions. It seems that myopia is a distant cousin of Brainf**k and is quite hopelessly distant from practical programming. $\endgroup$ – xuq01 Jul 31 '18 at 17:19
  • 2
    $\begingroup$ Of course. I just assumed that OP wants to find such a language to study the theory or something, not to actually conquer the world with it ;-) $\endgroup$ – Kapol Jul 31 '18 at 17:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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