Weakening Cycles So That Turing Can Halt

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...

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.

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

>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)?

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.

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.

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

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.

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%.

Seems like the results in this blog post would be of interest.

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.

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.

Check out Kolmogorov complexity and the law of independence conservation.

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?

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

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

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));
        };
      };
    }