6 ms·

The Turing-Completeness Problem

87 points by pimterry 6y ago

Athas 6y ago
While I'm always down with research into applied restricted languages, I'm not sure this is the path to mainstream parallel programming. It's one thing to identify that parallel execution is safe, and it's quite another to exploit that parallelism efficiently. E.g. in a pure functional language, you can automatically extract an enormous amount of parallelism, but doing so eagerly and naively will lead to a very slow program, as the communication and synchronisation overheads will dwarf any performance benefits of parallel execution. In practice, it appears that programmers don't find it problematic to explicitly indicate when things should run in parallel, and the main task of the language is to impose restrictions to avoid accidental sharing and race conditions. Rust is probably the most hyped example of such a language, but it's by no means the first or only one. Also, the elephant in the room is that in many common cases, the programming model is such that you get massive parallelism almost for free - e.g. when writing server-side web programs, where parallelism inside of one request may not matter (and often the database will take care of it when it does), because you have thousands of concurrent requests anyway.
jonathanstrange 6y ago
I don't see the connection between the Halting Problem and automatic parallelization. The Halting Problem itself plays no noteworthy role in practical algorithm verification anyway because in practice halting is not proved for any input program, but rather for only some very specific inputs. Theoretically speaking, parallel computation makes proving that a computation halts sometimes unnecessary. For example, a parallel OR boolean comparison may succeed, while the corresponding sequential comparison would lead to an infinite loop. Is there another connection? Isn't the problem with parallel computation rather that there is no unique description of it? AFAIK, e.g. derivations of the untyped lambda calculus describe any kind of sequential computation, just like a Turing Machine would do. In contrast, the pi calculus does not offer this uniqueness. Or is there such a description for any parallel computation? Anyway, maybe someone else can explain the connection between the Halting Problem and parallel computation, if there is one, because it's not clear to me from the article.
- ivanbakel 6y ago
  The actual Halting-ness of the program (or subsections of the program) seems to be a nice bonus of the language's actual goal: accurate worst-case estimation of running time for all computations. That then feeds into the automatic parallelisation, because it helps the compiler to decide how to parallelise different computations against each other based on their estimated running times. The fact that the language is not Turing-complete is a necessary consequence of being able to accurately determine a worst-case execution time for some code.
Gehinnn 6y ago
> So how do we make this barely not Turing complete? We make a list/array type a first class citizen in the VM itself and then we only add operations that know the bounds that they are to operate on based on that list or some other condition that cannot be directly mutated by the user's own code. I don't understand this paragraph. If they do have do-while loops, how do they prevent turing completeness?
- shoeffner 6y ago
  If I got it correctly, they do not have do-while, it was only shown as an example operation. Instead, they only use "for each", i.e., bounded loops directly on the data structures list/array.
  - ISV_Damocles 6y ago
    That's mostly correct. :) We used `do-while` to demonstrate that we could replicate the behaviors of a normal assembly language within the dependency graph representation. However, we do have a restricted version of `do-while` implemented as described in the Sequential Algorithms RFC[1]. We want to push people into writing parallelizable code by having the default constructs and data types encouraging that, but we know certain algorithms are only possible in a sequential form, and some of them (like the Newton-Raphson method) are not predictable in the number of sequences to run so we have an escape hatch in the language that lets you do the classic iterative programming, but all of them wrapped in a maximum iteration counter so we'll still be able to assign a maximum expected runtime to them (and be sure they halt, perhaps with an error). [1]: https://github.com/alantech/alan/blob/main/rfcs/007%20-%20Sequential%20Algorithms%20RFC.md https://github.com/alantech/alan/blob/main/rfcs/007%20-%20Se...
- benjaminjosephw 6y ago
  I think this is saying that arrays are immutable at runtime and the bounds of the array are checked on compile. By doing this, loops can be checked before execution to prevent infinite loops and so constrain that as a Turing Machine construct. I think the underlying good idea here is that Turing Completeness is maybe overrated. You could argue that most good programming languages are good because of what they don't let you do - constraints around how state is mutated is core to Object-oriented and functional programming. Adding some more constraints to ensure complete and reliable static analysis sounds like an excellent idea to me.
codeulike 6y ago
I always took the Turing 'Halting problem' as a sortof proxy for the general unknowableness of complex programs. As in, 'halting' could have been substitued with 'somewhere in the program variable x gets set to 5' and you could still construct a program in which it would be impossible to prove whether or not x gets set to 5. And of course the proof of the Halting problem relies on the possibility of crafting programs that are deliberately hard to parse - something that may or may not happen in practice. And so for me it all boils down to 'complexity is complex'. Which is kindof obvious to anyone thats wokred on large programs but might not be so intuitively obvious in some other fields. And so thats why there's always bugs. However hard you try, there is so much complexity in a large bit of software that you can't ever squash them all. And parallel processing adds another layer of complexity for sure. But I dont see how worrying about the Halting Problem helps deal with that any better than some of the language constructs we've already seen.
- mtklein 6y ago
  Yep! That general version of the halting problem is Rice's Theorem, and that's exactly the thinking that proves it, by showing that if we did have an algorithm to determine any given non-trivial property of a program, we'd be able to use that algorithm to solve the halting problem. As for parallel processing, it can be fun to think about how things would work if you had a CPU with infinite cores. Any time your program wants to explore two or more options, you always have cores to explore those options in parallel. This sort of thinking is the root of the "non-deterministic" 'N' in "NP"... with infinite cores you can solve NP problems (including NP-complete ones) in polynomial time.
  - Gehinnn 6y ago
    With infinitely many cores that are all connected to the same bus while each core has a unique id, you actually can solve the halting problem. You can basically brute force infinitely many inputs at once.
    - mtklein 6y ago
      I'm not sure that that's true. Some of the tricky cases for the halting problem boil down to the spiritual equivalent of trying to determine whether "this sentence is false" is true or false. It's not; it's neither. No infinite number of cores can help you there.
deleted 6y ago
[deleted]
Laakeri 6y ago
>Further, it has been exacerbated by recent computing mechanisms, such as multithreading, NUMA, GPGPU, and distributed computing, which have moved away from the "single tape" Turing Machine model of computation that most programming languages are founded upon. Stopped reading here. No programming language with arrays resembles single tape Turing machines. The correct model would be random-access machine (RAM).
- deleted 6y ago
  [deleted]
- jvanderbot 6y ago
  That's unfortunate, because they weren't talking about the physical execution, they were referring to the determinism, decideability, and serial-sequential nature of program execution.
- MauranKilom 6y ago
  I am curious in which way programming languages with arrays are not equivalent to a Turing Machine model. It's not clear to me what you mean with "resembles" and why that would be the same thing as "founded upon".
  - Laakeri 6y ago
    All Turing-complete programming languages/models of computation can simulate each other with polynomial overhead. What I think is weird is that the article specifically mentions that programming languages are built on single tape Turing machines (as opposed to Turing machines in general, or random access machines), because single tape Turing machines are highly impractical and programming them would feel completely different than programming with any real programming language. For example as basic operation as array access takes a linear number of operations in the size of the array in the single tape model.
sabas123 6y ago
This article appeals to so many results in complexity theory but can anybody tell me if they are valid? I did pass a basic course in theory of computation but can't verify these myself.
jejones3141 6y ago
Of course, there are some programs that are intended to run potentially forever, e.g. servers. Does Alan have some way to allow a non-terminating top level while constraining all the pieces underneath?
- deleted 6y ago
  [deleted]
- ISV_Damocles 6y ago
  Yes, we didn't want to make this article too long or confusing, but we have a static, compile-time-defined event system[1] to allow for applications that wait for external inputs to start executing again. Each event handler is guaranteed to halt even if the application continues to run. [1]: https://alan-lang.org/alan_overview.html#a-static-event-system https://alan-lang.org/alan_overview.html#a-static-event-syst...
jvanderbot 6y ago
Could some of these compiler-friendly loops be done in traditional languages by specifying that the data structure or array bounds are not modified during the execution of the statements inside the loop? Could for-each be leveraged to be a for-each-constant?
cjg 6y ago
We give up on automated program analysis far too easily - even for "Turing complete" languages. To be truly Turing complete requires infinite memory. That clearly doesn't hold for any current programming language. Mathematical proofs are only applicable where their assumptions are valid. So why would we believe that the where memory isn't infinite (everywhere in practice) that Turing's halting analysis is applicable? Sure, automated program analysis might not be easy, but that doesn't mean we should just give up. Indeed I have a simple algorithm (although relatively inefficient) to solve the halting problem where memory size is fixed and finite: enumerate every state until either a state is repeated or the program halts. This completes in O(2^N) time where N is the size of the memory. But I'm sure someone clever will come up with a more efficient algorithm than that. I already have several ideas that this margin is too small to contain. For me the tricky bits are where a loop terminates if and only if Goldbach's conjecture is true (or similar) - but perhaps a compiler could require an "unsafe" block for such code (in the vein of Rust).
- Strilanc 6y ago
  The halting problem proof will work fine on finite sizes, I think. Failing due to an infinite loop will just be replaced by going out of memory. The main caveat would be if the solver fills memory then the diagonalized solver (which is slightly larger) won't fit on the machine.
  - Conlectus 6y ago
    For finite sized memory, the problem can be solved by recording every system state (registers, memory values etc.) and seeing if the same state is ever reached twice. If so, the program will never terminate, and vice versa.
    - Strilanc 6y ago
      For clarification: I was imagining the the solver machine had the same number of resources as the problem machine (e.g. same length of tape, same number of states). I of course agree that there is a Turing machine that decides the computability of LBAs. When I said the problem still existed I meant you'd need e.g. larger and larger LBAs to solve the LBA problem up to a given size and that an LBA of tape size K with M states could not solve the halting problem for all LBAs of that size.
problem-halting 6y ago
also see Blockstack's Clarity language (https://docs.blockstack.org/references/language-overview https://docs.blockstack.org/references/language-overview) for another example of a non-Turing-complete language. Clarity bans loops altogether, which is theoretically exactly the same as only allowing "bounded loops", since any bounded loop can be written as, well, not a loop. :)

87 points by pimterry 6y ago

While I'm always down with research into applied restricted languages, I'm not sure this is the path to mainstream parallel programming. It's one thing to identify that parallel execution is safe, and it's quite another to exploit that parallelism efficiently. E.g. in a pure functional language, you can automatically extract an enormous amount of parallelism, but doing so eagerly and naively will lead to a very slow program, as the communication and synchronisation overheads will dwarf any performance benefits of parallel execution. In practice, it appears that programmers don't find it problematic to explicitly indicate when things should run in parallel, and the main task of the language is to impose restrictions to avoid accidental sharing and race conditions. Rust is probably the most hyped example of such a language, but it's by no means the first or only one. Also, the elephant in the room is that in many common cases, the programming model is such that you get massive parallelism almost for free - e.g. when writing server-side web programs, where parallelism inside of one request may not matter (and often the database will take care of it when it does), because you have thousands of concurrent requests anyway.

jonathanstrange 6y ago

I don't see the connection between the Halting Problem and automatic parallelization. The Halting Problem itself plays no noteworthy role in practical algorithm verification anyway because in practice halting is not proved for any input program, but rather for only some very specific inputs. Theoretically speaking, parallel computation makes proving that a computation halts sometimes unnecessary. For example, a parallel OR boolean comparison may succeed, while the corresponding sequential comparison would lead to an infinite loop. Is there another connection? Isn't the problem with parallel computation rather that there is no unique description of it? AFAIK, e.g. derivations of the untyped lambda calculus describe any kind of sequential computation, just like a Turing Machine would do. In contrast, the pi calculus does not offer this uniqueness. Or is there such a description for any parallel computation? Anyway, maybe someone else can explain the connection between the Halting Problem and parallel computation, if there is one, because it's not clear to me from the article.

ivanbakel 6y ago
The actual Halting-ness of the program (or subsections of the program) seems to be a nice bonus of the language's actual goal: accurate worst-case estimation of running time for all computations. That then feeds into the automatic parallelisation, because it helps the compiler to decide how to parallelise different computations against each other based on their estimated running times. The fact that the language is not Turing-complete is a necessary consequence of being able to accurately determine a worst-case execution time for some code.

Gehinnn 6y ago

> So how do we make this barely not Turing complete? We make a list/array type a first class citizen in the VM itself and then we only add operations that know the bounds that they are to operate on based on that list or some other condition that cannot be directly mutated by the user's own code. I don't understand this paragraph. If they do have do-while loops, how do they prevent turing completeness?

shoeffner 6y ago
If I got it correctly, they do not have do-while, it was only shown as an example operation. Instead, they only use "for each", i.e., bounded loops directly on the data structures list/array.
- ISV_Damocles 6y ago
  That's mostly correct. :) We used `do-while` to demonstrate that we could replicate the behaviors of a normal assembly language within the dependency graph representation. However, we do have a restricted version of `do-while` implemented as described in the Sequential Algorithms RFC[1]. We want to push people into writing parallelizable code by having the default constructs and data types encouraging that, but we know certain algorithms are only possible in a sequential form, and some of them (like the Newton-Raphson method) are not predictable in the number of sequences to run so we have an escape hatch in the language that lets you do the classic iterative programming, but all of them wrapped in a maximum iteration counter so we'll still be able to assign a maximum expected runtime to them (and be sure they halt, perhaps with an error). [1]: https://github.com/alantech/alan/blob/main/rfcs/007%20-%20Sequential%20Algorithms%20RFC.md https://github.com/alantech/alan/blob/main/rfcs/007%20-%20Se...
benjaminjosephw 6y ago
I think this is saying that arrays are immutable at runtime and the bounds of the array are checked on compile. By doing this, loops can be checked before execution to prevent infinite loops and so constrain that as a Turing Machine construct. I think the underlying good idea here is that Turing Completeness is maybe overrated. You could argue that most good programming languages are good because of what they don't let you do - constraints around how state is mutated is core to Object-oriented and functional programming. Adding some more constraints to ensure complete and reliable static analysis sounds like an excellent idea to me.

codeulike 6y ago

I always took the Turing 'Halting problem' as a sortof proxy for the general unknowableness of complex programs. As in, 'halting' could have been substitued with 'somewhere in the program variable x gets set to 5' and you could still construct a program in which it would be impossible to prove whether or not x gets set to 5. And of course the proof of the Halting problem relies on the possibility of crafting programs that are deliberately hard to parse - something that may or may not happen in practice. And so for me it all boils down to 'complexity is complex'. Which is kindof obvious to anyone thats wokred on large programs but might not be so intuitively obvious in some other fields. And so thats why there's always bugs. However hard you try, there is so much complexity in a large bit of software that you can't ever squash them all. And parallel processing adds another layer of complexity for sure. But I dont see how worrying about the Halting Problem helps deal with that any better than some of the language constructs we've already seen.

mtklein 6y ago
Yep! That general version of the halting problem is Rice's Theorem, and that's exactly the thinking that proves it, by showing that if we did have an algorithm to determine any given non-trivial property of a program, we'd be able to use that algorithm to solve the halting problem. As for parallel processing, it can be fun to think about how things would work if you had a CPU with infinite cores. Any time your program wants to explore two or more options, you always have cores to explore those options in parallel. This sort of thinking is the root of the "non-deterministic" 'N' in "NP"... with infinite cores you can solve NP problems (including NP-complete ones) in polynomial time.
- Gehinnn 6y ago
  With infinitely many cores that are all connected to the same bus while each core has a unique id, you actually can solve the halting problem. You can basically brute force infinitely many inputs at once.
  - mtklein 6y ago
    I'm not sure that that's true. Some of the tricky cases for the halting problem boil down to the spiritual equivalent of trying to determine whether "this sentence is false" is true or false. It's not; it's neither. No infinite number of cores can help you there.

deleted 6y ago

[deleted]

Laakeri 6y ago

>Further, it has been exacerbated by recent computing mechanisms, such as multithreading, NUMA, GPGPU, and distributed computing, which have moved away from the "single tape" Turing Machine model of computation that most programming languages are founded upon. Stopped reading here. No programming language with arrays resembles single tape Turing machines. The correct model would be random-access machine (RAM).

deleted 6y ago
[deleted]
jvanderbot 6y ago
That's unfortunate, because they weren't talking about the physical execution, they were referring to the determinism, decideability, and serial-sequential nature of program execution.
MauranKilom 6y ago
I am curious in which way programming languages with arrays are not equivalent to a Turing Machine model. It's not clear to me what you mean with "resembles" and why that would be the same thing as "founded upon".
- Laakeri 6y ago
  All Turing-complete programming languages/models of computation can simulate each other with polynomial overhead. What I think is weird is that the article specifically mentions that programming languages are built on single tape Turing machines (as opposed to Turing machines in general, or random access machines), because single tape Turing machines are highly impractical and programming them would feel completely different than programming with any real programming language. For example as basic operation as array access takes a linear number of operations in the size of the array in the single tape model.

sabas123 6y ago

This article appeals to so many results in complexity theory but can anybody tell me if they are valid? I did pass a basic course in theory of computation but can't verify these myself.

jejones3141 6y ago

Of course, there are some programs that are intended to run potentially forever, e.g. servers. Does Alan have some way to allow a non-terminating top level while constraining all the pieces underneath?

deleted 6y ago
[deleted]
ISV_Damocles 6y ago
Yes, we didn't want to make this article too long or confusing, but we have a static, compile-time-defined event system[1] to allow for applications that wait for external inputs to start executing again. Each event handler is guaranteed to halt even if the application continues to run. [1]: https://alan-lang.org/alan_overview.html#a-static-event-system https://alan-lang.org/alan_overview.html#a-static-event-syst...

jvanderbot 6y ago

Could some of these compiler-friendly loops be done in traditional languages by specifying that the data structure or array bounds are not modified during the execution of the statements inside the loop? Could for-each be leveraged to be a for-each-constant?

cjg 6y ago

We give up on automated program analysis far too easily - even for "Turing complete" languages. To be truly Turing complete requires infinite memory. That clearly doesn't hold for any current programming language. Mathematical proofs are only applicable where their assumptions are valid. So why would we believe that the where memory isn't infinite (everywhere in practice) that Turing's halting analysis is applicable? Sure, automated program analysis might not be easy, but that doesn't mean we should just give up. Indeed I have a simple algorithm (although relatively inefficient) to solve the halting problem where memory size is fixed and finite: enumerate every state until either a state is repeated or the program halts. This completes in O(2^N) time where N is the size of the memory. But I'm sure someone clever will come up with a more efficient algorithm than that. I already have several ideas that this margin is too small to contain. For me the tricky bits are where a loop terminates if and only if Goldbach's conjecture is true (or similar) - but perhaps a compiler could require an "unsafe" block for such code (in the vein of Rust).

Strilanc 6y ago
The halting problem proof will work fine on finite sizes, I think. Failing due to an infinite loop will just be replaced by going out of memory. The main caveat would be if the solver fills memory then the diagonalized solver (which is slightly larger) won't fit on the machine.
- Conlectus 6y ago
  For finite sized memory, the problem can be solved by recording every system state (registers, memory values etc.) and seeing if the same state is ever reached twice. If so, the program will never terminate, and vice versa.
  - Strilanc 6y ago
    For clarification: I was imagining the the solver machine had the same number of resources as the problem machine (e.g. same length of tape, same number of states). I of course agree that there is a Turing machine that decides the computability of LBAs. When I said the problem still existed I meant you'd need e.g. larger and larger LBAs to solve the LBA problem up to a given size and that an LBA of tape size K with M states could not solve the halting problem for all LBAs of that size.

problem-halting 6y ago

also see Blockstack's Clarity language (https://docs.blockstack.org/references/language-overview https://docs.blockstack.org/references/language-overview) for another example of a non-Turing-complete language. Clarity bans loops altogether, which is theoretically exactly the same as only allowing "bounded loops", since any bounded loop can be written as, well, not a loop. :)