3

Non-turing complete languages can solve every practical problem that a turing-complete language can. Also, they are much more analyzable than turing complete languages. The compiler can comprehend the program as a whole, predict/compute/cache every possible computation in advance, optimize it the most mathematically possible and even prove it has done so. It is like a super fusion between static typing and lazy evaluation in roids.

Yet nobody is trying to design a non-turing complete language like COQ that is practical and usable. Why?

MaiaVictor
  • 5,820
  • 7
  • 27
  • 45
  • 3
    I don't see how your first sentence is true. How, for instance, would you write a spell checker in a non-Turing complete language? – Gort the Robot Aug 10 '13 at 00:05
  • @StevenBurnap I'm stating that because it seems to be generally agreed by other programmers. As in, I have just asked it and that was the accepted answer, so I thought you would not complain of that. Funny. – MaiaVictor Aug 10 '13 at 00:26
  • 4
    @StevenBurnap: realistically tho, you can have a "non-turing-complete" language by taking, say, Python, and halting the program after 10^100 instructions if it hasn't halted already: the phrase "turing complete" doesn't actually mean much for edge cases like coq – amara Aug 10 '13 at 01:31
  • I have a dumb question: Is SQL turing-complete? – Joseph Quinsey Aug 10 '13 at 01:39
  • 1
    @sparkleshy By that token, though, nothing's truly Turing Complete because no hardware lasts forever (not to mention that no hardware has infinite memory.) – Gort the Robot Aug 10 '13 at 01:43
  • An answer (which I should have checked first): http://stackoverflow.com/q/900055/318716. It gives both _yes_ and _no_. – Joseph Quinsey Aug 10 '13 at 01:43
  • 1
    @JosephQuinsey But can SQL solve "every practical problem"? – Gort the Robot Aug 10 '13 at 01:44
  • @StevenBurnap: Perhaps SQL implicitly _defines_ the notion a 'practical problem'. So it can _express_ every such problem. But it can't _solve_ all of them. – Joseph Quinsey Aug 10 '13 at 01:51
  • See also http://programmers.stackexchange.com/q/172879/3605 – Joseph Quinsey Aug 10 '13 at 01:57
  • @JosephQuinsey: http://stackoverflow.com/a/7580013 – Robert Harvey Aug 10 '13 at 02:22
  • @StevenBurnap: this is true! – amara Aug 10 '13 at 02:44
  • 1
    Well I write compilers in Coq for research purposes which is a practical useful problem, it's do-able. But the amount of pain that you have to go through with languages like coq (dependently typed) will forever bar it from general acceptance IMHO – daniel gratzer Aug 10 '13 at 03:37
  • Turing completeness is like a shortcut, yes it removes a great deal of analyzability and other such, but above all else: It removes the requirement of halting which is a heavy burden for developers to carry in the general case. It would simply be too burdensome for too little benefit for a majority of developers to avoid halting in a majority of tasks. – Jimmy Hoffa Aug 10 '13 at 03:50
  • 1
    @JosephQuinsey SQL is Turing complete. See http://www.valuedlessons.com/2009/08/sql-is-now-turing-complete.html for more. But until they added more features, it wasn't. – btilly Aug 10 '13 at 06:21

2 Answers2

7

Non-turing complete languages can solve every practical problem that a turing-complete language can.

Wrong. You cannot, for example, even do something as simple as implement the game of Life in a non-Turing complete language. Why? Because the game of Life is Turing complete.

Once that hypothesis is seen to be false, the answer to the question is obvious.

btilly
  • 18,250
  • 1
  • 49
  • 75
  • 5
    but just like how computers actually have finite memory you should be able to implement game of life up to some limit – jk. Aug 10 '13 at 06:26
  • 4
    and its not clear that game of life is a practical problem at all. I can't think of any problem for which the game of life is a solution – jk. Aug 10 '13 at 06:27
  • 5
    @jk. The point is that if even something as simple as the game of life can't be done, what kind of useful programming abstractions would you have at your disposal? Easy things should be easy, not hard. – btilly Aug 11 '13 at 18:08
  • 1
    @btilly - Why is not possible to provide an arbitrary limit on the number of iterations? That would allow a proof termination and allow the game of life for an arbitrary number of iterations at least. – Davorak Sep 10 '13 at 18:58
  • 1
    Just because GameOfLife as a whole couldn't be implemented doesn't stop very large parts of it to be implementable in a non-Turing complete language. So maybe a language that forces non-Turing completeness wouldn't be very useful, but being able to restrict a function/procedure to be non-Turing complete could still be extremely useful (i.e. analog to how `const` in C++ which forbids certain operations or how `unsafe` in C# allows some unsafe operations). – Grumbel Oct 28 '13 at 09:29
5

One effort in this direction is the Hume family of languages, the last of which is Turing complete,

HW-Hume: a hardware description language — capable of describing both synchronous and asynchronous hardware circuits, with pattern matching on tuples of bits, but with no other data types or operations [27];

FSM-Hume: a hardware/software language — HW-Hume plus first-order functions, conditionals expressions and local definitions [26];

Template-Hume: a language for template-based programmimng — FSM-Hume plus predefined higher-order functions, polymorphism and inductive data structures, but no user-defined higher-order functions or recursive function definitions;

PR-Hume: a language with decidable termination — Template-Hume plus user-defined primitive recursive and higher-order functions, and inductive data structure definitions;

Full-Hume: a Turing-complete language — PR-Hume plus unrestricted recursion in both functions and data structures.

http://www.hume-lang.org/

ja.
  • 234
  • 1
  • 2