[pron]

That proof is like disproving the conservation of energy by pointing out that the water inside a kettle boils. Or speaking about the "Toaster-Enhanced Turing Machine" (https://www.scottaaronson.com/blog/?p=1121). It's easy to "disprove" Turing's thesis when you misstate it.

Turing's thesis talks about some system transforming an input to an output. Clearly, a TM could simulate the actor itself in your proof. If it is not able to simulate the entire actor-collaborator system, that's only because you may have given the collaborator (whatever it is that generates the messages) super-Turing powers. You assumed that there could be something that could issue a `stop` after an arbitrary number of `go`'s, but you haven't established that such a mechanism could actually exist, and that's where the super-Turing computation actually hides: in a collaborator whose existence you have not established. As you have not established the existence of the collaborator, you have not established the existence of your actor-collaborator system. I claim that a TM cannot simulate it simply because it cannot exist (not as you describe it, at least).

So here's another "proof": The actor machine takes two messages, Q and A(Bool), and it gets them alternately, always Q followed by A. Every time it gets a Q, it increments a counter (initialized to zero) by 1 to the value N, and emits a string corresponding to the Nth Turing machine. It then gets a message A containing a value telling it whether the Nth TM terminates on an empty tape, and in response it emits A's argument back. And here you have an actor machine that decides halting!

[ProfHewitt]

The article referenced presents a strongly-typed proof that the halting problem is compurationally undecidable. Nevertheless, Actors can perform computations impossible on a nondeterministic Turing Machine.

[pron]

If they can, you haven't shown that. The "computation" you present is not just the actor's behavior, but the behavior of a combined actor-collaborator system (the collaborator is whatever it is that sends the actor messages). This system presents "super-Turing" behavior iff the collaborator is super-Turing. You haven't shown such a collaborator, that can reliably emit a `stop` command after an arbitrary number of `go`s, can exist. It's always possible that the scientific consensus is wrong, but that requires proof, and the "proof" in the paper isn't one.

[ProfHewitt]

There is no "collaborator" in the Actor computation that Plotkin:s proof shows cannot be preformed by a nondeterministic Turing Machine.

[pron]

Yes, there is. The "computation" of the actor (really, actor-collaborator) relies on something that can reliably emit a `stop` after an arbitrary number of `go`s. Please show that something can actually do that, and I'll show you a TM that can do the same. It's easy to describe non-computable behaviors; the difficulty is demonstrating that there are actual physical systems that can carry them out.

[ProfHewitt]

The Actor (which cannot be implemented by a nondeterministic TM) sends the 'stop' message to itself. However, just as there can be an arbitrarily long amount of time between two steps of a computation, there can be a arbitrarily long amount of time for a message to be delivered.

[pron]

> The Actor (which cannot be implemented by a nondeterministic TM)

As you now describe it, it cannot be implemented (physically realized) at all. Or, conversely, any physically implementable refinement of it (which will not exhibit the entire range of behaviors) will be simulatable by a TM.

There are many abstract machines that cannot be implemented by TMs -- e.g. various oracle TMs. There is nothing special, surprising or new about that.

There are many formalisms that are more or less convenient abstractions for various kinds of systems. There is nothing special, surprising or new about that, either. In fact, some formalisms that can describe non-computable behaviors are commonly used to specify either software or hardware as they're convenient (like Lamport's TLA).

But you're making a claim about the Church-Turing thesis, which, as commonly interpreted today (as the physical Church-Turing thesis), is the claim that any mechanism that can be implemented by a physical mechanism can be simulated by a TM. Unless you show how to build a physical system that cannot be simulated by a TM, your claim is no refutation of the thesis; it has nothing to do with it. Your claim that arbiters in digital circuits cannot be simulated has not been established and is not recognized by scientific consensus.

> However, just as there can be an arbitrarily long amount of time between two steps of a computation, there can be a arbitrarily long amount of time for a message to be delivered.

This is a completely different use of "arbitrary". In TMs, the fact that an arbitrary amount of time can pass between steps means that any device, with any finite amount of time between steps, can produce the full range of TM behaviors. In your actor case, to get non-computable behavior, you need to show that the device can delay the message by every amount of time. You need to show that such a physical device can exist.

Put simply, it's one thing to propose a non-computable abstraction that's convenient to model some systems, and another thing altogether to claim that there are realizable physical systems that cannot be simulated by a Turing machine. The former is useful but mundane (in fact, all of classical analysis falls in this category); the latter has not been achieved to date.

[ProfHewitt]

There are simple nondetermintic procedures that can be implemented by digital circuits using arbiters that cannot be implemented by a nondeterminustic Turing Machine.

[pron]

That is a strong assertion that requires proof. The consensus view is that there aren't. For example, one could claim that a TM couldn't simulate a coin flip as it cannot simulate true randomness, but this assumes that the coin flip is "truly" random without establishing it (which would be hard because of pseudorandomness). Or, in the case of arbiters, you could claim that the arbiter behaves like the magical collaborator in the stop/go examples, converting two analog inputs to a binary decision that takes an arbitrarily long time, but this only introduces yet another magical collaborator capable of producing analog inputs that are equal to arbitrary precision.

This is a common problem when we appeal to continuous natural phenomena, as their common description is usually a convenient, but imprecise, abstraction. Goldreich addressed this in On the philosophical basis of computational theories [1]: "A computational model cannot be justified by merely asserting that it is consistent with some theory of natural phenomena ... The source of trouble is the implicit postulate that asserts that whatever is not forbidden explicitly by the relevant electrical theories, can actually be implemented"[2]

[1]: http://www.wisdom.weizmann.ac.il/~oded/VO/qc-fable.pdf

[2]: He adds "at no cost" because his focus is complexity, not computability

[pron]

P.S

Goldreich demonstrates the problem by showing that our abstractions of electrical circuits don't in themselves preclude circuits that violate computational complexity results or even decide halting, but that alone is insufficient to show that such circuits can actually be built.

There are certain formalisms that make this kind of error harder to spot: actor formalisms make it easy to hide impossible "computation" in a collaborator; some typed formalisms could hide computation in the syntax (which requires a lot or even infinite computation to decide).

[ProfHewitt]

A thesis in the referenced article is that the Actor model formalizes digital computation.