4 ms·

So I might have made this a bit confusing too by conflating the two things in my original post. The real thing is that there are a lot of undecidable programs

So I might have made this a bit confusing too by conflating the two things in my original post. The real thing is that there are a lot of undecidable programs that don't require Turing completeness. And a lot of those useful programs are undecidable, an example of a really simple undecidable program: 10 PRINT "Enter your name" 20 INPUT NAME$ 30 PRINT "Hello ", NAME$ 40 IF NAME$ <> "Ralph" THEN 41 GOTO 10 42 END IF 50 PRINT "Goodby Ralph" That program, because it might loop indefinitely isn't decidable and isn't possible to describe with Viper by design. This kind of program is pretty analogous to basically every program that communicates with the network, user, or some other external system.

dragonwriter 9y ago
> This kind of program is pretty analogous to basically every program that communicates with the network, user, or some other external system. Not really; it's quite possible, and often desirable, to do that without potentially infinite loops.
- sillysaurus3 9y ago
  How?
- swsieber 9y ago
  Exactly - you want timeouts, exponential backoff, etc. You want to know what happens if a network failure happens - you don't want to retry ad nauseam.
  - sillysaurus3 9y ago
    Some of the most reliable programs are those without exponential backoff and which retry infinitely in network failure situations. `ping` is one example.
    - swsieber 9y ago
      And yet I'd be completely fine with a ping that was capped to running for no more than a week. YMMV though. And more to the point, you don't want a program that goes on forever in a setup like ethereum. I guess your rebuttal was called for since the initial point was a little hyperbolic.
- simcop2387 9y ago
  So how do you do that for the server side of things? Only accept a certain number of connections before you have to completely shut down and restart the server? How do you do the restart without the infinite loop somewhere?
Shorel 9y ago
The old good O-Machine.
mycall 9y ago
I miss line numbers
Risord 9y ago
So how non-turing completeness work with infinite streams? Many practical applications (like this) are working with possibly infinite stream of user inputs / requests etc. If we can guarantee that our server, browser or game application just stops eventually we know that something is wrong. However we like to guarantee that our application won't work infinitely with single request / input / time tick. So does this say that we want avoid using turing complete language mostly but turing complete part need to be handled somewhere maybe outside of our code? Something like how Haskell works with side effects. What you think?
- dismantlethesun 9y ago
  It won't. It will instead operate over the first googol items and then require a restart.
- tom_mellior 9y ago
  Coq is not Turing complete but has support for coinductive data types (= infinite streams) and (co-)recursion over them. Simplifying a lot, it has a syntactic "guard condition" that says that you must produce some result before you're allowed to make a recursive call. For example, you can map over an infinite stream because a map produces a result for each element of the input stream. Unlike Haskell, you cannot write a fold over an infinite stream because you would need to look at all elements before producing a result. So if you can structure your system as a transformation from an infinite stream of requests to an infinite stream of responses, you're fine in Coq even though it is not Turing complete. The intuition is that, just like in Haskell, you don't actually end up doing an infinite computation if only a finite part of the final result is ever requested.
  - pron 9y ago
    If you have support for coinductive data types then you are Turing complete. Proof: you can simulate a Turing machine. However, Coq's term language is not Turing complete, meaning that every syntactic element in Coq evaluates to a terminating computation.
- lmm 9y ago
colanderman 9y ago
"Undecidability" doesn't apply to interactive systems. Inputs must be finite: https://en.wikipedia.org/wiki/Undecidable_problem https://en.wikipedia.org/wiki/Undecidable_problem In your example, the input (an infinite stream of strings not equal to "Ralph") is not finite. Instead, think of an interactive system as a finite state machine. The question to ask then is, do any of my state transitions require a Turing-complete language to express? In 99.999% of all software ever written the answer is "no". Inability to prove termination is almost certainly a software bug or flaw in the design. The theoretical exceptions are exotic algorithms for which termination is not provable; the practical exceptions are probabilistic algorithms for which termination is not in fact guaranteed (e.g. a naïve hash table implementation). The difference is important. A state machine, even one that represents a non-terminating system over infinite input (e.g. a web server), still can be reasoned about. This is exactly the domain of tools like TLA+, which can answer questions such as, "is my system guaranteed to always eventually take action X given input Y?" and "is my system guaranteed to never terminate?" But to be able to answer such questions, it's a prerequisite that the transitions between states do in fact terminate.
- E6300 9y ago
  It's not a given that the input is infinite. If the used types in "Rob" then goes away forever, the program will neither terminate nor process an infinite number of non-"Ralph" strings. It will sit just sit there waiting (possibly in a loop, possibly not) for a hardware interrupt that will never arrive.
  - PKop 9y ago
    Isn't this a question of upper-bound on input? Not specific examples that are less than the upper bound..
  - colanderman 9y ago
    For decidability to apply, the input needs to be known a priori in its entirety. Decidability is a mathematical statement about natural numbers (or any other countably infinite set); it has absolutely nothing to do with "paused" input or any notion of "interactivity". The type of behavior you're concerned with does on the other hand fall squarely in the realm of temporal logics (e.g. TLA+), which do concern themselves with interactivity and indeterminate pauses. For example, the statement "so long as the user eventually inputs the string 'Ralph', the algorithm eventually terminates" is decidable for any finite state machine. In other words, if you limit your interactivity logic to that expressible by a finite state machine with decidably halting transitions, congratulations, you are writing decidably halting programs, even though they don't "halt" in the temporal sense. It's always possible to tell whether they will halt for a given input by completely analyzing the state space.

dragonwriter 9y ago

> This kind of program is pretty analogous to basically every program that communicates with the network, user, or some other external system. Not really; it's quite possible, and often desirable, to do that without potentially infinite loops.

sillysaurus3 9y ago
How?
swsieber 9y ago
Exactly - you want timeouts, exponential backoff, etc. You want to know what happens if a network failure happens - you don't want to retry ad nauseam.
- sillysaurus3 9y ago
  Some of the most reliable programs are those without exponential backoff and which retry infinitely in network failure situations. `ping` is one example.
  - swsieber 9y ago
    And yet I'd be completely fine with a ping that was capped to running for no more than a week. YMMV though. And more to the point, you don't want a program that goes on forever in a setup like ethereum. I guess your rebuttal was called for since the initial point was a little hyperbolic.
simcop2387 9y ago
So how do you do that for the server side of things? Only accept a certain number of connections before you have to completely shut down and restart the server? How do you do the restart without the infinite loop somewhere?

Shorel 9y ago

The old good O-Machine.

mycall 9y ago

I miss line numbers

Risord 9y ago

So how non-turing completeness work with infinite streams? Many practical applications (like this) are working with possibly infinite stream of user inputs / requests etc. If we can guarantee that our server, browser or game application just stops eventually we know that something is wrong. However we like to guarantee that our application won't work infinitely with single request / input / time tick. So does this say that we want avoid using turing complete language mostly but turing complete part need to be handled somewhere maybe outside of our code? Something like how Haskell works with side effects. What you think?

dismantlethesun 9y ago
It won't. It will instead operate over the first googol items and then require a restart.
tom_mellior 9y ago
Coq is not Turing complete but has support for coinductive data types (= infinite streams) and (co-)recursion over them. Simplifying a lot, it has a syntactic "guard condition" that says that you must produce some result before you're allowed to make a recursive call. For example, you can map over an infinite stream because a map produces a result for each element of the input stream. Unlike Haskell, you cannot write a fold over an infinite stream because you would need to look at all elements before producing a result. So if you can structure your system as a transformation from an infinite stream of requests to an infinite stream of responses, you're fine in Coq even though it is not Turing complete. The intuition is that, just like in Haskell, you don't actually end up doing an infinite computation if only a finite part of the final result is ever requested.
- pron 9y ago
  If you have support for coinductive data types then you are Turing complete. Proof: you can simulate a Turing machine. However, Coq's term language is not Turing complete, meaning that every syntactic element in Coq evaluates to a terminating computation.
lmm 9y ago

colanderman 9y ago

"Undecidability" doesn't apply to interactive systems. Inputs must be finite: https://en.wikipedia.org/wiki/Undecidable_problem https://en.wikipedia.org/wiki/Undecidable_problem In your example, the input (an infinite stream of strings not equal to "Ralph") is not finite. Instead, think of an interactive system as a finite state machine. The question to ask then is, do any of my state transitions require a Turing-complete language to express? In 99.999% of all software ever written the answer is "no". Inability to prove termination is almost certainly a software bug or flaw in the design. The theoretical exceptions are exotic algorithms for which termination is not provable; the practical exceptions are probabilistic algorithms for which termination is not in fact guaranteed (e.g. a naïve hash table implementation). The difference is important. A state machine, even one that represents a non-terminating system over infinite input (e.g. a web server), still can be reasoned about. This is exactly the domain of tools like TLA+, which can answer questions such as, "is my system guaranteed to always eventually take action X given input Y?" and "is my system guaranteed to never terminate?" But to be able to answer such questions, it's a prerequisite that the transitions between states do in fact terminate.

E6300 9y ago
It's not a given that the input is infinite. If the used types in "Rob" then goes away forever, the program will neither terminate nor process an infinite number of non-"Ralph" strings. It will sit just sit there waiting (possibly in a loop, possibly not) for a hardware interrupt that will never arrive.
- PKop 9y ago
  Isn't this a question of upper-bound on input? Not specific examples that are less than the upper bound..
- colanderman 9y ago
  For decidability to apply, the input needs to be known a priori in its entirety. Decidability is a mathematical statement about natural numbers (or any other countably infinite set); it has absolutely nothing to do with "paused" input or any notion of "interactivity". The type of behavior you're concerned with does on the other hand fall squarely in the realm of temporal logics (e.g. TLA+), which do concern themselves with interactivity and indeterminate pauses. For example, the statement "so long as the user eventually inputs the string 'Ralph', the algorithm eventually terminates" is decidable for any finite state machine. In other words, if you limit your interactivity logic to that expressible by a finite state machine with decidably halting transitions, congratulations, you are writing decidably halting programs, even though they don't "halt" in the temporal sense. It's always possible to tell whether they will halt for a given input by completely analyzing the state space.