8 ms·

Weakening Cycles So That Turing Can Halt

96 points by Kinrany 6y ago

ausbah 6y ago
wow brilliant article! I always love the connections to be made between theory and computer system! are there any good reads that cover topics like in detail?
- munificent 6y ago
  You'd like "Gödel, Escher, Bach: An Eternal Golden Braid", mentioned in the article.
mpoteat 6y ago
This was a very enjoyable read... twice. A metaphorical fugue on Turing, Godel, type theory and the generalization of this fundamental paradox that is Lawvere's proof. And, how it may relate to the more practical problems of memory management! I've been reading Permutation City recently. There has to be a way to shoe horn the fundamental problem of consciousness in here somewhere.
- throwaway6734 6y ago
  Permutation City is fantastic!
ajkjk 6y ago
Oh, wow, this is a very stimulating comparison. My summary is that all of these are structurally the same: * programs with recursion that either halts or not -- is there a partial order on states of a recursive algorithm such that some state is eventually terminal? * threads with resource dependencies that either deadlock or not -- is there a partial order on resource acquisition so that eventually some operation is unblocked? * garbage collection of memory references -- is there a partial order on resource ownership such that some element is eventually unowned? * Russell's paradox -- presumably something like: is there a partial order on the definitions of some sets such that all of the definitions can be resolved? * Godel's Incompleteness theorem and Liar's paradox, etc -- presumably something like: is there a partial order on statements that allows their truth values to be resolved? In every case it seems like the solution is some form of diagonal argument. I really like the version I just found in this paper[1]: if Y is a set and there's a function a(Y): Y that doesn't have a fixed point, then for any function f(T, T): Y there's a function g(T): Y that can't be written as g(s) = f(s,t) for all t. Namely, set g(t) = a(f(t,t)); clearly f(s,s) = g(s) = a(f(s,s)) != f(s,s). For the Liar Paradox ("this sentence is false") and Godel ("this statement cannot be proved in G") the set Y is (True/Proven, False/Disproven) and the function a() just takes False <-> True and so has no fixed point. The function f(s, t) tries to assign a truth value to a statement 's' and also to the _claim_ made by 's'. The function g(s) tries to assign a truth value to 's' alone, but for 'this sentence is false' the definition is g(s) = a(f(s,s)), and the definition of f(s,s) = g(s), so g(s) = a(g(s)) and there's no solution -- just like a recursive function that says f(x) = !f(x) never terminates! The connection to partial orders is: there must be a partial order on the possible states of the system such that there isn't an infinite loop. The states can be the truth values of statements, the input to a function, the states of a Turing machine's tape, the state of the condition a thread is waiting on, or the state of whether an object has been freed. Etc. Of course I have never really thought through this before and I'm making it up as I go, but this is grand and delightful to sort-of hand-wavingly understand. [1]: https://arxiv.org/pdf/math/0305282.pdf https://arxiv.org/pdf/math/0305282.pdf
- jondgoodwin 6y ago
  It is indeed grand and delightful. I am glad you enjoyed the post so much. It was every bit as much fun for me to grok and then and share with others.
ivanbakel 6y ago
>This is important because ... Pony can still experience deadlocks. By carefully modeling each dining philosopher and fork using distinct actors that synchronize by sending messages to each other, it becomes clear that at some point the philosopher actors just end up silently waiting on messages that will never arrive. I'm interested by this rather offhand comment. Pony makes rather strong claims about being deadlock free - and what the author describes is not a deadlock, any more than hitting the end of `main()` represents a deadlock because your sequential program doesn't progress any further. Are there examples of Pony programs which actually "deadlock" - that is, fail to continue executing in some way while there is still some unfinished work to be done (and not just because they choose not to progress)?
- ubadair 6y ago
  > not just because they choose not to progress To a computer, what's the difference? Instructions are instructions.
  - lonelappde 6y ago
    AIUI, Pony programs don't have a blocking wait. They terminate if they are idle.
    - jondgoodwin 6y ago
      AIUI actors are regularly idle. However, you are right that Pony offers a clever mechanism not offered by Erlang, which allows an actor to effectively despawn itself. I believe how it does this is to notice when no other actor has a reference to it. If no other actor has a reference to it, no one cannot send it any messages. If it has no messages in its queue and it is idle (not currently dispatched on a message), we know it will never again receive any messages, and therefore it is safe to free itself because it will never again have work to do.
- jondgoodwin 6y ago
  Author here. You are 100% correct that Pony makes a strong claim about being deadlock-free: "It’s deadlock free. This one is easy, because Pony has no locks at all! So they definitely don’t deadlock, because they don’t exist." (from the first page of the tutorial). Sylvan Clebsch is a really smart guy and Pony is a stunning piece of engineering based on rigorous analysis. He would surely know. So far as I can determine, this part of the claim is true: it makes no use of locks, not in the runtime and none are surfaced to the Pony programmer. The only synchronization mechanism that Pony makes use of is the MPSC queues that make possible message passing between actors. Each actor has its own queue, and it is only "active" when it has messages on its queue that need to serviced. The work-stealing scheduler will give every actor with messages an opportunity to process at least one message. When it does so, it never blocks and (hopefully) finishes with no requirement to return a result to any other actor (although it may be pass messages to other actors if it wishes). Now consider Wikipedia's definition of a deadlock: "a deadlock is a state in which each member of a group is waiting for another member, including itself, to take action, such as sending a message or more commonly releasing a lock". Notice that deadlocks can occur not only because of locks (which Pony does not have), but also because of waiting on another actor to send a message. The wiki article lists four conditions for a deadlock, which (it turns out) can also occur in a message-passing architecture. How would Pony trigger this sort of deadlock? Consider implementing the dining philosophers problem in Pony by having the main actor spawn five fork actors (with on-table state) and then five philosopher actors, telling each the fork actor to their left and the fork actor to their right. The philosopher actors all wake up hungry, so they reach for their left fork first, by sending it an acquire message and then effectively suspend. If the left fork A is in on-table state, it changes its state to indicate it has been acquired by a specific philosopher and sends a message back to the philosopher to say it has been acquired. That reactivates the philospher to now send an acquire message to the right fork B. But maybe by this point in time another philosopher has already acquired that right fork B as its left fork! So it sends a message back to the requesting philosopher to say it is not currently available to be acquired, try again later. If you walk through this implications of this carefully, you will see that although every philosopher is getting activated by messages regularly, at a certain point in time it is possible that meaningful forward progress can cease for at least one philosopher. At least some philosophers will starve, because they become deadlocked in not being able to get two forks needed to eat, because they are effectively contending over access to shared resources. The situation is semantically equivalent to when we use locks for forks instead. And if we apply Dijkstra's partial order to how the philosopher actors acquire their forks in an actor-based message passing architecture, the deadlock risk vanishes and all the philosophers have a reasonable chance, eventually, to eat and therefore guarantee eventual forward progress. Does this explanation of an example satisfy your question?
garganzol 6y ago
The article uses an intuitive approach trying to find a way to crack the halting problem. But the truth is that halting dilemma is real and despite any attempt to "unwind" or "simplify" the control and data flows, there is a real barrier. It is in the math. My favorite example: finding an odd perfect number. Euler stated: "Whether (...) there are any odd perfect numbers is a most difficult question". More recently, Carl Pomerance has presented a heuristic argument suggesting that indeed no odd perfect number should exist. [1] Does it exist? Definitely. Somewhere in 10^300 range. What is the exact value? Nobody knows. You can write a program that finds an odd perfect number: def odd_perfect_number(): n = 1 while True: if sum(filter(lambda x: n % x == 0, xrange(1, n))) == n: return "OK! I FIND IT!" n += 2 Will this program ever complete? Maybe. However nobody can say for sure. Avoiding recursion or some kind of groups won't give you any favor. This is the halting problem in all of its glory. [1] https://en.wikipedia.org/wiki/Perfect_number https://en.wikipedia.org/wiki/Perfect_number
- cortesoft 6y ago
  If it definitely exists, don't we then know that this program will definitely halt?
  - garganzol 6y ago
    Only from algebraic and philosophical standpoints. This knowledge is not 100% precise unless a specific number is found.
    - groby_b 6y ago
      Nobody cares about the halting problem from a specific standpoint. If it's algebraically guaranteed to halt, it halts. When it halts is entirely meaningless for purposes of the halting problem. But the thing is, it isn't algebraically guaranteed either - we still don't know if an odd perfect number exists. (I'm not sure where the "Definitely. Somewhere in 10^300 range." is coming from. There's nothing definite about the existence, only constraints that need to be satisfied if it exists)
Sophistifunk 6y ago
The liar "paradox" is only one if you're operating with the assumption all statements are falsifiable and valid, which I've never been shown to be a good ground truth.
- andrewflnr 6y ago
  That's pretty much the same idea underlying intuitionistic logic, IIUC
musicale 6y ago
Paradoxical self-reference cycles seem to give rise to the halting problem, the incompleteness theorem, the liar paradox, and Russell's paradox (among other paradoxes and self-contradictions) so breaking those cycles seems like a practical idea. However, in practice there really isn't a noticeable difference between a program that never completes and one that takes 100 years to complete. Both programs will almost certainly be halted (or at least paused indefinitely) by some external means. If a program takes too long to produce its desired output, then it simply isn't a useful piece of software.
- saagarjha 6y ago
  Well, that depends. A program that takes 100 years to complete (say factoring a large number) can be optimized to not take 100 years, and it is worth looking for algorithmic advances that would make that possible. A program that can proven to never halt (a soundness detector that checks programs for behavioral violations) can never be perfect and must rely on heuristics or be known to fail on certain input.
  - whatshisface 6y ago
    In fact, 100 years to 1/10th of a year is a mere constant factor, that could be arrived at in some cases by buying a lot of GPUs.
    - musicale 6y ago
      If it doesn't take 100 years to complete, then it doesn't take 100 years to complete. But it is a sort of good point that a 100 year runtime in 2020 might turn into a 10 year runtime in 2030, making it only a 20 year runtime overall. For some jobs, a 20 year runtime might be acceptable, but probably those jobs are rare. In general if a program takes so long to complete that its output is no longer useful, that limits its practicality and utility.
  - musicale 6y ago
    If it doesn't take 100 years to complete, it doesn't take 100 years to complete.
TheNewAndy 6y ago
I feel like this is circling around total functional programming. I found this to be an accessible paper on this: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.364&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106... The language it uses enforces that all recursive steps "simplify" the input, and gives a simple definition of "simplify". Note that the language is not (nor does it try to be) Turing complete - intuitively you could imagine that there might be some level of expressiveness which is not enough to get to halting problem like levels of complexity, but enough to get "real world" complexity.
- jondgoodwin 6y ago
  Total functional programming indeed is another example of a valid approach to weakening cycles and thereby guaranteeing termination. Although it works for that, it is too restrictive for my taste. I am looking for less restrictive forms of weakening that allow creation of a broader range of algorithms (including "imperative") that we can still guarantee will terminate.
  - lmm 6y ago
    > Although it works for that, it is too restrictive for my taste. I am looking for less restrictive forms of weakening that allow creation of a broader range of algorithms (including "imperative") that we can still guarantee will terminate. How is it weak? Surely it's equivalent to any other approach: given a function and any form of termination guarantee for that function, you can encode that guarantee as a phantom type and then you have an expression of that function in a total functional language.
    - remexre 6y ago
      I mean, how long does it take to convince yourself a function will halt vs how long does it take to use implement it with well-founded recursion, with comparable readability? Not that it's not possible, it's just more of a pain.
yters 6y ago
Check out Kolmogorov complexity and the law of independence conservation.
- andrewflnr 6y ago
  Link for "the law of independence conservation"? Google results look mostly unrelated (except for one page trying to use it to prove AI is impossible).
  - yters 6y ago
    See: https://www.sciencedirect.com/science/article/pii/S0019995884800601 https://www.sciencedirect.com/science/article/pii/S001999588... look at section 1.2 it is the non growth theorem for algorithmic information, but also deals with randomness Levin proves randomness + computation is not expected to increase algorithmic mutual information. In other words there is no randomness loophole in Godël's theorem.
SteveJS 6y ago
Seems like the results in this blog post would be of interest. https://www.scottaaronson.com/blog/?p=2741 https://www.scottaaronson.com/blog/?p=2741 Not so much in avoiding the halting problem while allowing complexity, but instead using it and actual runnable Turing machines to create ridiculously cool cases of unprovable truths. For example a running Turing machine that only halts if it contradicts set theory.
Xophmeister 6y ago
I've noticed a related phenomenon in day-to-day life, especially regarding deadlocking. There are occasions when two parties will deadlock; the classic one is when two people walk towards each other, directly in line, and come to a point where they want to pass without colliding. It happens -- often with comic effect -- when the two parties sidestep at perceptibly the same point and in the same direction, again and again, deadlocking themselves. However, something kicks in after two-or-three failed attempts to resolve the deadlock. I've noticed similar things at traffic junctions; roundabouts and single-lane roads, especially. Personally, I sometimes do this when I go to open a door that is often, but not always, locked: my hand will reach for the latch, then go for the handle, then back and forth semi-automatically, until my higher thinking kicks in and I realise I've just got to make a decision! In these cases, I feel as though the cycles aren't weakened, but instead there's some kind of executive function -- that's normally asleep, because it's presumably expensive to run -- which oversees to break the impasse, when needed.
- chris_st 6y ago
  In the "two people walking towards each other" case, I've battled that my whole life. I typically stare right at the other person, anxiously waiting for them to pick a direction so I can go the other way. My wife pointed out to me that just by picking a side, and then looking in that direction as the other person comes towards you, that they (possibly unconsciously) go the other way, and conflict avoided! Mind blown. And it works.
  - Xophmeister 6y ago
    Another solution I've heard for this problem is to not look the other person in the eye and just look passed/through them without faltering. IIRC, this comes across as an assertion of dominance and the other party will submit and move aside. I don't actually know if this works :P Also, I assume there's a hilarious edge case where two super-assertive people just walk into each other.
    - heavenlyblue 6y ago
jondubois 6y ago
It reminds me of something I had posted to a math/engineering forum some time ago but my answer was taken down because I didn't use proper mathematical terminology and I had ended the comment with a question mark asking for feedback. My idea was that what if the halting detection function sometimes intentionally lied about whether or not the program halts (E.g. just returned a random true/false 1% the time instead of actually doing the analysis work) then because Turing's proof is recursive (and relies on the occurrence of an infinite recursive deadlock condition), eventually, at a certain random depth in the recursion, the halting detection function would break out of the recursion when it hits that random error case. So the intentional % error added to the halting detection function would prevent hitting the infinite recursion case on which Turing's proof relies. The downside of this approach would be that my hypothetical halting detection function would return incorrect results a certain percentage of the time when applied to other algorithms; but this problem can be offset by running it multiple times against the same input. The accuracy of such a function could approach 100% as you run it more often but never quite reach 100%.
- Drakim 6y ago
  I'm not so sure I understand, because if you do have some code that a turning machine would throw for an infinite loop, wouldn't your 1% trick be the only escape the first time, second time, third time and forth time you tried to run the halting analyzer? Thus you wouldn't get closer and closer to 100% accuracy, but rather, you'd get the randomness response every single attempt
  - jondubois 6y ago
    Given that the analyzer function 'H' needs to work with any algorithm 'F'. We could separate 'F' into two distinct subsets of functions (the union of which fully spans the set of all possible F): 1. 'F1' which represents any possible function which does not invoke the H(F1) function internally. 2. 'F2' which represents any possible function which invokes the H(F2) function internally. Turing's proof relies entirely on the existence of 'F2' functions and the fact that these kinds of functions always lead to a an infinite loop deadlock condition. Turing's proof relies on these 'F2' functions as a counter example to prove why H cannot exist. Turing's proof does not apply for functions of the 'F1' kind. So my thinking is that assuming that there existed a probabilistic analyzer function `H` which worked with 'F1' functions and which could be modified to also work with 'F2' functions (I.e. by adding a probabilistic error % as I suggested), then that would invalidate Turing's counter-example. It would not give any answers about the halting problem itself though; just move the problem back to a state of uncertainty. My idea aims to prove that if you have an 'H' which works for 'F1' then it can be easily modified to also work for 'F2' if you're prepared to accept an error probability each time you run the function. A key part of my argument is that any F2 function can use an error % as an escape hatch to protect itself from infinite recursion and thus gives those functions the ability to decide their own output. For these kinds of F2 functions, whatever output H(F2) returns becomes self-fulfilling after the recursion has finished unwinding and so it does not matter if H(F2) is true or false.
chriswarbo 6y ago
I really like the "delay" datatype as a way to implement general recursion (i.e. Turing-completeness) in a non-general/non-Turing-complete system like Coq or Agda. We can think of 'Delay<T>' as being a bit like 'List<T>'. If we follow Lisp's encoding, there are two forms of list: the empty list 'Nil', which doesn't "contain" anything; and the pair 'Cons(x, y)' which contains a value 'x' (the "head" or "car" of the list) and another list 'y' (the "tail" or "cdr", which might be 'Nil'). 'Delay' is the other way around: it is either 'Now(x)', which contains the value 'x', or it is 'Later(y)' which contains another delay 'y' (which might be a 'Now'). We can imagine 'Delay<T>' a bit like a list containing a single 'T' value at the end, preceded by an arbitrary amount of NULL elements. I've gone into a bit more depth on such constructions (AKA "initial algebras") in a blog post http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html This gets interesting if our language allows co-termination (like Agda, Coq, Haskell, etc.). This is where we're allowed to recurse 'inside' our return value. For example, the following function doesn't terminate, since it will always call itself recursively; yet it does co-terminate, since the recursion is happening "inside" the 'Cons'. We don't know what the full result will be, but at every stage we definitely know what the next part will be (a 'Cons' list). We can reach any finite "depth" of the result within a finite amount of time. This is also known as being "productive": function countUpFrom(x) { return new Cons(x, countUpFrom(x+1)); } The following function doesn't co-terminate (whether it always terminates is currently unknown), since (in the non-1 case) we don't 'narrow down' the return value before recursing. As far as we know, this could keep "passing the buck" forever, and we'd never get any closer to knowing what any part of the result looks like: function collatz(x) { return (x == 1)? 1 : collatz(even(x)? x / 2 : 3 * x + 1); } Implementing co-termination requires that the "contents" of a datastructure are calculated on-demand rather than straight away (AKA 'lazily'). We can actually do this in any language with first-class functions by creating (and subsequently forcing) "thunks", although it gets quite verbose, e.g. function countUpFrom(x) { return new Cons(x, function() { return countUpFrom(x+1); }); } I wrote a blog post which uses this to generate Fibonacci numbers in PHP: http://chriswarbo.net/blog/2014-07-23-fib.html http://chriswarbo.net/blog/2014-07-23-fib.html We can use co-termination to implement a Turing machine, or any other generally-recursive system, by simply making a list of each "step": function turingMachineList(tm) { return Cons(tm, halted(tm)? Nil : turingMachineList(step(tm))); } This will produce a list of each machine state, which might stop (if the machine reaches a halted state) or go on forever. Likewise we can implement a list of Collatz values: function collatzList(x) { return Cons(x, (x == 1)? Nil : collatzList(even(x)? x / 2 : x * 3 + 1)); } If we only care about the "result" then we can use 'Delay' instead of 'List': function turingMachineDelay(tm) { return halted(tm)? Now(tm) : Later(turingMachineDelay(step(tm))); } function collatDelay(x) { return (x == 1)? Now(1) : Later(collatzList(even(x)? x / 2 : x * 3 + 1)); } These will return a value like 'Later(Later(Later(...)))' which will either keep nesting forever, or (if the calculation has an answer) will eventually contain 'Now(answer)'. 'Delay' is nice since we can write programs in pretty much the same way as normal. The only changes are mechanical and obvious: - If a recursive call isn't "inside" the return value, we wrap it in 'Later(...)' so it is; and wrap any corresponding base-cases in 'Now(...)'. - If we need to perform some calculation on the result of a 'Delay' (i.e. the value in its 'Now'), we can't do so directly, since there might not be a result (it could be 'Later(Later(...))' forever); and even if there is, we don't know how many 'Later' wrappers to dig through. Instead, we use these values indirectly, by mapping our calculation over the 'Delay' value. This isn't hard: it's exactly the same as mapping over the elements of a list, or over an optional value, etc. Here's what 'map' looks like for 'Delay': function mapDelay(f, x) { return case x { Now(y): Now(f(y)); Later(y): Later(mapDelay(f, y)); }; } We can run such programs in two ways: - We can remove (up to) some finite number of 'Later' wrappers, which is equivalent to running with a timeout. We can always do this inside the total (terminating/co-terminating) language. We might still end up with a 'Later(...)', unless we can prove that the computation will always finish before our timeout (i.e. if we have a termination proof). - We can use an external program (in a Turing-complete language) as a clock to 'tick' through each step; essentially playing the role of OS or VM (similar to using a trampoline for recursion, in languages which don't eliminate tail-calls). In this sense, 'Delay' is like a language-enforced version of cooperative multitasking, since we must always eventually yield, at which point the OS can pick another delayed value to tick. The ticks are also a convenient place for the user to interrupt/cancel a program. Of course, knowing that the next tick will be occur within a finite time doesn't guarantee that it will be happen before the heat-death of the universe! Note that we can also use co-termination to build datatypes which have no base-case, and hence every value must be infinite. This would be pretty useless for 'Delay' (since there is only one infinite value, namely 'Later(Later(...))' forever). The always-infinite equivalent of lists are called "streams", and are defined as having a 'Cons' form but no 'Nil' form. From the OS/VM perspective above, this lets us write programs which are guaranteed to run forever (e.g. servers which never crash), although they may run out of memory, and responses might take a while (bounded by the busy beaver number for the server's code size + the request size). The classic example is to represent input as an infinite stream, e.g. 'Stream<HTTPRequest>', have a function for constructing a response 'respond : HTTPRequest -> HTTPResponse', and construct a server via 'streamMap(respond, input) : Stream<HTTPResponse>'. If we want a stateful server we can include the new state with our reponse and have the server plumb it through: respond : (State, HTTPRequest) -> (State, HTTPResponse) server : (State, Stream<HTTPRequest>) -> Stream<HTTPResponse> function server(currentState, stream) { return case stream { StreamCons(request, rest): case respond(currentState, request) { (nextState, response): StreamCons(response, server(nextState, rest)); }; }; }

96 points by Kinrany 6y ago

wow brilliant article! I always love the connections to be made between theory and computer system! are there any good reads that cover topics like in detail?

munificent 6y ago
You'd like "Gödel, Escher, Bach: An Eternal Golden Braid", mentioned in the article.

mpoteat 6y ago

This was a very enjoyable read... twice. A metaphorical fugue on Turing, Godel, type theory and the generalization of this fundamental paradox that is Lawvere's proof. And, how it may relate to the more practical problems of memory management! I've been reading Permutation City recently. There has to be a way to shoe horn the fundamental problem of consciousness in here somewhere.

throwaway6734 6y ago
Permutation City is fantastic!

ajkjk 6y ago

Oh, wow, this is a very stimulating comparison. My summary is that all of these are structurally the same: * programs with recursion that either halts or not -- is there a partial order on states of a recursive algorithm such that some state is eventually terminal? * threads with resource dependencies that either deadlock or not -- is there a partial order on resource acquisition so that eventually some operation is unblocked? * garbage collection of memory references -- is there a partial order on resource ownership such that some element is eventually unowned? * Russell's paradox -- presumably something like: is there a partial order on the definitions of some sets such that all of the definitions can be resolved? * Godel's Incompleteness theorem and Liar's paradox, etc -- presumably something like: is there a partial order on statements that allows their truth values to be resolved? In every case it seems like the solution is some form of diagonal argument. I really like the version I just found in this paper[1]: if Y is a set and there's a function a(Y): Y that doesn't have a fixed point, then for any function f(T, T): Y there's a function g(T): Y that can't be written as g(s) = f(s,t) for all t. Namely, set g(t) = a(f(t,t)); clearly f(s,s) = g(s) = a(f(s,s)) != f(s,s). For the Liar Paradox ("this sentence is false") and Godel ("this statement cannot be proved in G") the set Y is (True/Proven, False/Disproven) and the function a() just takes False <-> True and so has no fixed point. The function f(s, t) tries to assign a truth value to a statement 's' and also to the _claim_ made by 's'. The function g(s) tries to assign a truth value to 's' alone, but for 'this sentence is false' the definition is g(s) = a(f(s,s)), and the definition of f(s,s) = g(s), so g(s) = a(g(s)) and there's no solution -- just like a recursive function that says f(x) = !f(x) never terminates! The connection to partial orders is: there must be a partial order on the possible states of the system such that there isn't an infinite loop. The states can be the truth values of statements, the input to a function, the states of a Turing machine's tape, the state of the condition a thread is waiting on, or the state of whether an object has been freed. Etc. Of course I have never really thought through this before and I'm making it up as I go, but this is grand and delightful to sort-of hand-wavingly understand. [1]: https://arxiv.org/pdf/math/0305282.pdf https://arxiv.org/pdf/math/0305282.pdf

jondgoodwin 6y ago
It is indeed grand and delightful. I am glad you enjoyed the post so much. It was every bit as much fun for me to grok and then and share with others.

ivanbakel 6y ago

>This is important because ... Pony can still experience deadlocks. By carefully modeling each dining philosopher and fork using distinct actors that synchronize by sending messages to each other, it becomes clear that at some point the philosopher actors just end up silently waiting on messages that will never arrive. I'm interested by this rather offhand comment. Pony makes rather strong claims about being deadlock free - and what the author describes is not a deadlock, any more than hitting the end of `main()` represents a deadlock because your sequential program doesn't progress any further. Are there examples of Pony programs which actually "deadlock" - that is, fail to continue executing in some way while there is still some unfinished work to be done (and not just because they choose not to progress)?

ubadair 6y ago
> not just because they choose not to progress To a computer, what's the difference? Instructions are instructions.
- lonelappde 6y ago
  AIUI, Pony programs don't have a blocking wait. They terminate if they are idle.
  - jondgoodwin 6y ago
    AIUI actors are regularly idle. However, you are right that Pony offers a clever mechanism not offered by Erlang, which allows an actor to effectively despawn itself. I believe how it does this is to notice when no other actor has a reference to it. If no other actor has a reference to it, no one cannot send it any messages. If it has no messages in its queue and it is idle (not currently dispatched on a message), we know it will never again receive any messages, and therefore it is safe to free itself because it will never again have work to do.
jondgoodwin 6y ago
Author here. You are 100% correct that Pony makes a strong claim about being deadlock-free: "It’s deadlock free. This one is easy, because Pony has no locks at all! So they definitely don’t deadlock, because they don’t exist." (from the first page of the tutorial). Sylvan Clebsch is a really smart guy and Pony is a stunning piece of engineering based on rigorous analysis. He would surely know. So far as I can determine, this part of the claim is true: it makes no use of locks, not in the runtime and none are surfaced to the Pony programmer. The only synchronization mechanism that Pony makes use of is the MPSC queues that make possible message passing between actors. Each actor has its own queue, and it is only "active" when it has messages on its queue that need to serviced. The work-stealing scheduler will give every actor with messages an opportunity to process at least one message. When it does so, it never blocks and (hopefully) finishes with no requirement to return a result to any other actor (although it may be pass messages to other actors if it wishes). Now consider Wikipedia's definition of a deadlock: "a deadlock is a state in which each member of a group is waiting for another member, including itself, to take action, such as sending a message or more commonly releasing a lock". Notice that deadlocks can occur not only because of locks (which Pony does not have), but also because of waiting on another actor to send a message. The wiki article lists four conditions for a deadlock, which (it turns out) can also occur in a message-passing architecture. How would Pony trigger this sort of deadlock? Consider implementing the dining philosophers problem in Pony by having the main actor spawn five fork actors (with on-table state) and then five philosopher actors, telling each the fork actor to their left and the fork actor to their right. The philosopher actors all wake up hungry, so they reach for their left fork first, by sending it an acquire message and then effectively suspend. If the left fork A is in on-table state, it changes its state to indicate it has been acquired by a specific philosopher and sends a message back to the philosopher to say it has been acquired. That reactivates the philospher to now send an acquire message to the right fork B. But maybe by this point in time another philosopher has already acquired that right fork B as its left fork! So it sends a message back to the requesting philosopher to say it is not currently available to be acquired, try again later. If you walk through this implications of this carefully, you will see that although every philosopher is getting activated by messages regularly, at a certain point in time it is possible that meaningful forward progress can cease for at least one philosopher. At least some philosophers will starve, because they become deadlocked in not being able to get two forks needed to eat, because they are effectively contending over access to shared resources. The situation is semantically equivalent to when we use locks for forks instead. And if we apply Dijkstra's partial order to how the philosopher actors acquire their forks in an actor-based message passing architecture, the deadlock risk vanishes and all the philosophers have a reasonable chance, eventually, to eat and therefore guarantee eventual forward progress. Does this explanation of an example satisfy your question?

garganzol 6y ago

The article uses an intuitive approach trying to find a way to crack the halting problem. But the truth is that halting dilemma is real and despite any attempt to "unwind" or "simplify" the control and data flows, there is a real barrier. It is in the math. My favorite example: finding an odd perfect number. Euler stated: "Whether (...) there are any odd perfect numbers is a most difficult question". More recently, Carl Pomerance has presented a heuristic argument suggesting that indeed no odd perfect number should exist. [1] Does it exist? Definitely. Somewhere in 10^300 range. What is the exact value? Nobody knows. You can write a program that finds an odd perfect number: def odd_perfect_number(): n = 1 while True: if sum(filter(lambda x: n % x == 0, xrange(1, n))) == n: return "OK! I FIND IT!" n += 2 Will this program ever complete? Maybe. However nobody can say for sure. Avoiding recursion or some kind of groups won't give you any favor. This is the halting problem in all of its glory. [1] https://en.wikipedia.org/wiki/Perfect_number https://en.wikipedia.org/wiki/Perfect_number

cortesoft 6y ago
If it definitely exists, don't we then know that this program will definitely halt?
- garganzol 6y ago
  Only from algebraic and philosophical standpoints. This knowledge is not 100% precise unless a specific number is found.
  - groby_b 6y ago
    Nobody cares about the halting problem from a specific standpoint. If it's algebraically guaranteed to halt, it halts. When it halts is entirely meaningless for purposes of the halting problem. But the thing is, it isn't algebraically guaranteed either - we still don't know if an odd perfect number exists. (I'm not sure where the "Definitely. Somewhere in 10^300 range." is coming from. There's nothing definite about the existence, only constraints that need to be satisfied if it exists)

Sophistifunk 6y ago

The liar "paradox" is only one if you're operating with the assumption all statements are falsifiable and valid, which I've never been shown to be a good ground truth.

andrewflnr 6y ago
That's pretty much the same idea underlying intuitionistic logic, IIUC

musicale 6y ago

Paradoxical self-reference cycles seem to give rise to the halting problem, the incompleteness theorem, the liar paradox, and Russell's paradox (among other paradoxes and self-contradictions) so breaking those cycles seems like a practical idea. However, in practice there really isn't a noticeable difference between a program that never completes and one that takes 100 years to complete. Both programs will almost certainly be halted (or at least paused indefinitely) by some external means. If a program takes too long to produce its desired output, then it simply isn't a useful piece of software.

saagarjha 6y ago
Well, that depends. A program that takes 100 years to complete (say factoring a large number) can be optimized to not take 100 years, and it is worth looking for algorithmic advances that would make that possible. A program that can proven to never halt (a soundness detector that checks programs for behavioral violations) can never be perfect and must rely on heuristics or be known to fail on certain input.
- whatshisface 6y ago
  In fact, 100 years to 1/10th of a year is a mere constant factor, that could be arrived at in some cases by buying a lot of GPUs.
  - musicale 6y ago
    If it doesn't take 100 years to complete, then it doesn't take 100 years to complete. But it is a sort of good point that a 100 year runtime in 2020 might turn into a 10 year runtime in 2030, making it only a 20 year runtime overall. For some jobs, a 20 year runtime might be acceptable, but probably those jobs are rare. In general if a program takes so long to complete that its output is no longer useful, that limits its practicality and utility.
- musicale 6y ago
  If it doesn't take 100 years to complete, it doesn't take 100 years to complete.

TheNewAndy 6y ago

I feel like this is circling around total functional programming. I found this to be an accessible paper on this: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.364&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106... The language it uses enforces that all recursive steps "simplify" the input, and gives a simple definition of "simplify". Note that the language is not (nor does it try to be) Turing complete - intuitively you could imagine that there might be some level of expressiveness which is not enough to get to halting problem like levels of complexity, but enough to get "real world" complexity.

jondgoodwin 6y ago
Total functional programming indeed is another example of a valid approach to weakening cycles and thereby guaranteeing termination. Although it works for that, it is too restrictive for my taste. I am looking for less restrictive forms of weakening that allow creation of a broader range of algorithms (including "imperative") that we can still guarantee will terminate.
- lmm 6y ago
  > Although it works for that, it is too restrictive for my taste. I am looking for less restrictive forms of weakening that allow creation of a broader range of algorithms (including "imperative") that we can still guarantee will terminate. How is it weak? Surely it's equivalent to any other approach: given a function and any form of termination guarantee for that function, you can encode that guarantee as a phantom type and then you have an expression of that function in a total functional language.
  - remexre 6y ago
    I mean, how long does it take to convince yourself a function will halt vs how long does it take to use implement it with well-founded recursion, with comparable readability? Not that it's not possible, it's just more of a pain.

yters 6y ago

Check out Kolmogorov complexity and the law of independence conservation.

andrewflnr 6y ago
Link for "the law of independence conservation"? Google results look mostly unrelated (except for one page trying to use it to prove AI is impossible).
- yters 6y ago
  See: https://www.sciencedirect.com/science/article/pii/S0019995884800601 https://www.sciencedirect.com/science/article/pii/S001999588... look at section 1.2 it is the non growth theorem for algorithmic information, but also deals with randomness Levin proves randomness + computation is not expected to increase algorithmic mutual information. In other words there is no randomness loophole in Godël's theorem.

SteveJS 6y ago

Seems like the results in this blog post would be of interest. https://www.scottaaronson.com/blog/?p=2741 https://www.scottaaronson.com/blog/?p=2741 Not so much in avoiding the halting problem while allowing complexity, but instead using it and actual runnable Turing machines to create ridiculously cool cases of unprovable truths. For example a running Turing machine that only halts if it contradicts set theory.

Xophmeister 6y ago

I've noticed a related phenomenon in day-to-day life, especially regarding deadlocking. There are occasions when two parties will deadlock; the classic one is when two people walk towards each other, directly in line, and come to a point where they want to pass without colliding. It happens -- often with comic effect -- when the two parties sidestep at perceptibly the same point and in the same direction, again and again, deadlocking themselves. However, something kicks in after two-or-three failed attempts to resolve the deadlock. I've noticed similar things at traffic junctions; roundabouts and single-lane roads, especially. Personally, I sometimes do this when I go to open a door that is often, but not always, locked: my hand will reach for the latch, then go for the handle, then back and forth semi-automatically, until my higher thinking kicks in and I realise I've just got to make a decision! In these cases, I feel as though the cycles aren't weakened, but instead there's some kind of executive function -- that's normally asleep, because it's presumably expensive to run -- which oversees to break the impasse, when needed.

chris_st 6y ago
In the "two people walking towards each other" case, I've battled that my whole life. I typically stare right at the other person, anxiously waiting for them to pick a direction so I can go the other way. My wife pointed out to me that just by picking a side, and then looking in that direction as the other person comes towards you, that they (possibly unconsciously) go the other way, and conflict avoided! Mind blown. And it works.
- Xophmeister 6y ago
  Another solution I've heard for this problem is to not look the other person in the eye and just look passed/through them without faltering. IIRC, this comes across as an assertion of dominance and the other party will submit and move aside. I don't actually know if this works :P Also, I assume there's a hilarious edge case where two super-assertive people just walk into each other.
  - heavenlyblue 6y ago

jondubois 6y ago

It reminds me of something I had posted to a math/engineering forum some time ago but my answer was taken down because I didn't use proper mathematical terminology and I had ended the comment with a question mark asking for feedback. My idea was that what if the halting detection function sometimes intentionally lied about whether or not the program halts (E.g. just returned a random true/false 1% the time instead of actually doing the analysis work) then because Turing's proof is recursive (and relies on the occurrence of an infinite recursive deadlock condition), eventually, at a certain random depth in the recursion, the halting detection function would break out of the recursion when it hits that random error case. So the intentional % error added to the halting detection function would prevent hitting the infinite recursion case on which Turing's proof relies. The downside of this approach would be that my hypothetical halting detection function would return incorrect results a certain percentage of the time when applied to other algorithms; but this problem can be offset by running it multiple times against the same input. The accuracy of such a function could approach 100% as you run it more often but never quite reach 100%.

Drakim 6y ago
I'm not so sure I understand, because if you do have some code that a turning machine would throw for an infinite loop, wouldn't your 1% trick be the only escape the first time, second time, third time and forth time you tried to run the halting analyzer? Thus you wouldn't get closer and closer to 100% accuracy, but rather, you'd get the randomness response every single attempt
- jondubois 6y ago
  Given that the analyzer function 'H' needs to work with any algorithm 'F'. We could separate 'F' into two distinct subsets of functions (the union of which fully spans the set of all possible F): 1. 'F1' which represents any possible function which does not invoke the H(F1) function internally. 2. 'F2' which represents any possible function which invokes the H(F2) function internally. Turing's proof relies entirely on the existence of 'F2' functions and the fact that these kinds of functions always lead to a an infinite loop deadlock condition. Turing's proof relies on these 'F2' functions as a counter example to prove why H cannot exist. Turing's proof does not apply for functions of the 'F1' kind. So my thinking is that assuming that there existed a probabilistic analyzer function `H` which worked with 'F1' functions and which could be modified to also work with 'F2' functions (I.e. by adding a probabilistic error % as I suggested), then that would invalidate Turing's counter-example. It would not give any answers about the halting problem itself though; just move the problem back to a state of uncertainty. My idea aims to prove that if you have an 'H' which works for 'F1' then it can be easily modified to also work for 'F2' if you're prepared to accept an error probability each time you run the function. A key part of my argument is that any F2 function can use an error % as an escape hatch to protect itself from infinite recursion and thus gives those functions the ability to decide their own output. For these kinds of F2 functions, whatever output H(F2) returns becomes self-fulfilling after the recursion has finished unwinding and so it does not matter if H(F2) is true or false.

chriswarbo 6y ago

I really like the "delay" datatype as a way to implement general recursion (i.e. Turing-completeness) in a non-general/non-Turing-complete system like Coq or Agda. We can think of 'Delay<T>' as being a bit like 'List<T>'. If we follow Lisp's encoding, there are two forms of list: the empty list 'Nil', which doesn't "contain" anything; and the pair 'Cons(x, y)' which contains a value 'x' (the "head" or "car" of the list) and another list 'y' (the "tail" or "cdr", which might be 'Nil'). 'Delay' is the other way around: it is either 'Now(x)', which contains the value 'x', or it is 'Later(y)' which contains another delay 'y' (which might be a 'Now'). We can imagine 'Delay<T>' a bit like a list containing a single 'T' value at the end, preceded by an arbitrary amount of NULL elements. I've gone into a bit more depth on such constructions (AKA "initial algebras") in a blog post http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html This gets interesting if our language allows co-termination (like Agda, Coq, Haskell, etc.). This is where we're allowed to recurse 'inside' our return value. For example, the following function doesn't terminate, since it will always call itself recursively; yet it does co-terminate, since the recursion is happening "inside" the 'Cons'. We don't know what the full result will be, but at every stage we definitely know what the next part will be (a 'Cons' list). We can reach any finite "depth" of the result within a finite amount of time. This is also known as being "productive": function countUpFrom(x) { return new Cons(x, countUpFrom(x+1)); } The following function doesn't co-terminate (whether it always terminates is currently unknown), since (in the non-1 case) we don't 'narrow down' the return value before recursing. As far as we know, this could keep "passing the buck" forever, and we'd never get any closer to knowing what any part of the result looks like: function collatz(x) { return (x == 1)? 1 : collatz(even(x)? x / 2 : 3 * x + 1); } Implementing co-termination requires that the "contents" of a datastructure are calculated on-demand rather than straight away (AKA 'lazily'). We can actually do this in any language with first-class functions by creating (and subsequently forcing) "thunks", although it gets quite verbose, e.g. function countUpFrom(x) { return new Cons(x, function() { return countUpFrom(x+1); }); } I wrote a blog post which uses this to generate Fibonacci numbers in PHP: http://chriswarbo.net/blog/2014-07-23-fib.html http://chriswarbo.net/blog/2014-07-23-fib.html We can use co-termination to implement a Turing machine, or any other generally-recursive system, by simply making a list of each "step": function turingMachineList(tm) { return Cons(tm, halted(tm)? Nil : turingMachineList(step(tm))); } This will produce a list of each machine state, which might stop (if the machine reaches a halted state) or go on forever. Likewise we can implement a list of Collatz values: function collatzList(x) { return Cons(x, (x == 1)? Nil : collatzList(even(x)? x / 2 : x * 3 + 1)); } If we only care about the "result" then we can use 'Delay' instead of 'List': function turingMachineDelay(tm) { return halted(tm)? Now(tm) : Later(turingMachineDelay(step(tm))); } function collatDelay(x) { return (x == 1)? Now(1) : Later(collatzList(even(x)? x / 2 : x * 3 + 1)); } These will return a value like 'Later(Later(Later(...)))' which will either keep nesting forever, or (if the calculation has an answer) will eventually contain 'Now(answer)'. 'Delay' is nice since we can write programs in pretty much the same way as normal. The only changes are mechanical and obvious: - If a recursive call isn't "inside" the return value, we wrap it in 'Later(...)' so it is; and wrap any corresponding base-cases in 'Now(...)'. - If we need to perform some calculation on the result of a 'Delay' (i.e. the value in its 'Now'), we can't do so directly, since there might not be a result (it could be 'Later(Later(...))' forever); and even if there is, we don't know how many 'Later' wrappers to dig through. Instead, we use these values indirectly, by mapping our calculation over the 'Delay' value. This isn't hard: it's exactly the same as mapping over the elements of a list, or over an optional value, etc. Here's what 'map' looks like for 'Delay': function mapDelay(f, x) { return case x { Now(y): Now(f(y)); Later(y): Later(mapDelay(f, y)); }; } We can run such programs in two ways: - We can remove (up to) some finite number of 'Later' wrappers, which is equivalent to running with a timeout. We can always do this inside the total (terminating/co-terminating) language. We might still end up with a 'Later(...)', unless we can prove that the computation will always finish before our timeout (i.e. if we have a termination proof). - We can use an external program (in a Turing-complete language) as a clock to 'tick' through each step; essentially playing the role of OS or VM (similar to using a trampoline for recursion, in languages which don't eliminate tail-calls). In this sense, 'Delay' is like a language-enforced version of cooperative multitasking, since we must always eventually yield, at which point the OS can pick another delayed value to tick. The ticks are also a convenient place for the user to interrupt/cancel a program. Of course, knowing that the next tick will be occur within a finite time doesn't guarantee that it will be happen before the heat-death of the universe! Note that we can also use co-termination to build datatypes which have no base-case, and hence every value must be infinite. This would be pretty useless for 'Delay' (since there is only one infinite value, namely 'Later(Later(...))' forever). The always-infinite equivalent of lists are called "streams", and are defined as having a 'Cons' form but no 'Nil' form. From the OS/VM perspective above, this lets us write programs which are guaranteed to run forever (e.g. servers which never crash), although they may run out of memory, and responses might take a while (bounded by the busy beaver number for the server's code size + the request size). The classic example is to represent input as an infinite stream, e.g. 'Stream<HTTPRequest>', have a function for constructing a response 'respond : HTTPRequest -> HTTPResponse', and construct a server via 'streamMap(respond, input) : Stream<HTTPResponse>'. If we want a stateful server we can include the new state with our reponse and have the server plumb it through: respond : (State, HTTPRequest) -> (State, HTTPResponse) server : (State, Stream<HTTPRequest>) -> Stream<HTTPResponse> function server(currentState, stream) { return case stream { StreamCons(request, rest): case respond(currentState, request) { (nextState, response): StreamCons(response, server(nextState, rest)); }; }; }