4 ms·

> 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

> 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.
- dreamcompiler 6y ago
  That's not enough. You also have to constrain what the mapped function is doing. For example, it could create one or more brand new arrays or for that matter perform any infinite computation without mutating the original array. Proving that the mapped function does not do any of that requires that it not be Turing Complete.
jlouis 6y ago
You make sure all operations on lists and arrays terminate. For instance by requiring the user to annotate where progress is being made on the bounded array.
lokedhs 6y ago
You can have a condition that you need to be able to prove that some variable is strictly decreasing on each iteration. Then you ensure that the loop exits once the variable reaches zero or less. ATS has this kind of proof built into the language, so that the type system helps you prove that a loop will always exit, and if it can't, it's a compile error. It's not entirely clear how useful this is in practice. While you may be able to prove that a loop always exits, it can prove nothing about how long it will take before it does. A loop never terminating, and one that terminates some time after the Milky Way has merged with Andromeda is pretty much equivalent from a practical standpoint.
- chriswarbo 6y ago
  From a computational perspective you're right, but for languages which allow formal verification (like ATS) there is a big difference between infinite loops and long-running loops. In particular, if we only care whether something exists then we can accept a long-running computation as proof without having to run it, whilst an infinite loop may be false. For example, a function which takes a list, an index and a proof that the index occurs in the list: we can look up the index safely, without having to care about the actual contents of the proof (the language ensures it's valid). On the other hand, we can write an infinite loop which claims to prove anything we like, but never actually has to cough up anything. For example: ProofOfRiemannConjecture myProof { while (true) {} }

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.

dreamcompiler 6y ago
That's not enough. You also have to constrain what the mapped function is doing. For example, it could create one or more brand new arrays or for that matter perform any infinite computation without mutating the original array. Proving that the mapped function does not do any of that requires that it not be Turing Complete.

jlouis 6y ago

You make sure all operations on lists and arrays terminate. For instance by requiring the user to annotate where progress is being made on the bounded array.

lokedhs 6y ago

You can have a condition that you need to be able to prove that some variable is strictly decreasing on each iteration. Then you ensure that the loop exits once the variable reaches zero or less. ATS has this kind of proof built into the language, so that the type system helps you prove that a loop will always exit, and if it can't, it's a compile error. It's not entirely clear how useful this is in practice. While you may be able to prove that a loop always exits, it can prove nothing about how long it will take before it does. A loop never terminating, and one that terminates some time after the Milky Way has merged with Andromeda is pretty much equivalent from a practical standpoint.

chriswarbo 6y ago
From a computational perspective you're right, but for languages which allow formal verification (like ATS) there is a big difference between infinite loops and long-running loops. In particular, if we only care whether something exists then we can accept a long-running computation as proof without having to run it, whilst an infinite loop may be false. For example, a function which takes a list, an index and a proof that the index occurs in the list: we can look up the index safely, without having to care about the actual contents of the proof (the language ensures it's valid). On the other hand, we can write an infinite loop which claims to prove anything we like, but never actually has to cough up anything. For example: ProofOfRiemannConjecture myProof { while (true) {} }