Lambda the Ultimate

Andrew I think you misunderstood my argument back there.

"Fairness" is completely beside the point. Rather:

Suppose that you take an Actor model and give a theorem that itself or in its proof makes use of the Actor model's concept of "eventual message delivery".

In every case, mechanically, I can translate that into a theorem about NDTMs without needing to add any concept of "fairness" to the NDTM model. For every statement about Actor termination conditions, there is an analogous statement about the sets of NDTM conditions achievable in some finite number of steps. Any reasonable, fully traditional formalization of NDTMs and any reasonable, traditional formalization of Actors are equivalent theories. Neither formally tells you more about computation than the other. Each can be seen as a fairly natural model of the other. In my opinion, there is some confusion about foundation of math issues in Clinger's work that is interpreted as proving otherwise.

The actor model may have informal conceptual or notational advantages but sometimes stronger claims seem to be made about it that I don't think hold up.

Yes that sounds as though I've misunderstood. NDTM's are not really in my area so I have missed one of the important details. I had assumed that given a set of possible transitions from a state that the selection was entirely non-deterministic (i.e the same transition could be selected infinitely often if the machine loops through that state). What I was phrasing as "fairness" was simply a guarantee that at some point a different transition would be selected.

Would it be true to say you are using "terminates in a finite number of steps" as that guarantee - and then working backwards to say if the NDTM did terminate in a finite number of steps then it must have taken an alternate transition from that state?

I am somewhat confused as I thought that NDTMs and TMs were equivalent in power. Yet the busy beaver function is a bound for computation length on a TM, but by your description a NDTM could execute the same program used as an example in the Actor model and output an arbitrary sized integer. Does this come down to the definition of "machine that always terminates"?

What I was phrasing as "fairness" was simply a guarantee that at some point a different transition would be selected.

Given a traditionally defined non-deterministic turing machine we can trivially speak of the sets of all machine configurations (state, position, and tape contents) achievable after N steps. For machine M and non-negative integer N, call the corresponding set Configs(M, N).

For each M and N, a possibly empty subset of Configs(M, N) is the set Finals(M, N) which are all the configurations in Configs(M,N) in which the machine is in a final state.

Every actor theorem that supposedly can't be achieved for turing machines can be mechanically translated in a fairly natural way back into a theorem about Finals(M,N). Actor models of computation aren't somehow fundamentally "more powerful" than TM models. Claims otherwise just misunderstand how the formalized math of NDTMs works.

It is interesting that you say this:

I am somewhat confused as I thought that NDTMs and TMs were equivalent in power. Yet the busy beaver function is a bound for computation length on a TM, but by your description a NDTM could execute the same program used as an example in the Actor model and output an arbitrary sized integer. Does this come down to the definition of "machine that always terminates"?

What do you mean by "always"? What do you mean by "terminates"?

For a given actors' theorem, my proof is likely to reason about "always" by some kind of induction over global states achievable in discrete steps over time.

For NDTMs, same thing, probably with reference to Finals(M,N).

For the DTM model of the same theorem, same thing again although be aware that so-called halt states in the DTM state machine specification are not going to play the same role as the halt states in the NDTM state machine specification.

The three different models, all of exactly the same thing, are trivially interchangeable for any proofs about the computable. Sometimes one is a more convenient notation or intuition than the other, is all.

What do you mean by "always"? What do you mean by "terminates"?

Yes - this is the part that confuses me. If I use the definition of a machine at the top of the thread as an example then it's not clear to me that it always terminates. It is true that every state in Finals(M,N) would be a unique value of N in state 1, and also (by induction) that every natural number would occur in a configuration in Finals. But there is also one infinite trace that always selects state zero. So the machine given would generate an unbounded integer, but with the possibility of non-termination.

Would this machine (or some version of it as a NDTM) give rise to the claim that it always terminates yet can generate an integer of unbounded size? Or if the problem is with the way that I'm using "always terminates" then what kind of definition would normally be used in this context?

But there is also one infinite trace that always selects state zero. So the machine given would generate an unbounded integer, but with the possibility of non-termination.

It would be non-standard to introduce an axiom of transfinite induction in an NDTM formalism so I can't tell what you mean by "is also one infinite trace taht always selects state zero".

A related problem with the Actors model is that the axiom of finite time message delivery is non-constructive.

Ok, it makes sense now: the question can't be phrased over NDTMs because there is no such thing as an infinite trace. NDTMs are only defined over finite numbers of sets / finite sized set of configurations. I remember somebody mentioning this in the last thread although I didn't realise the significance.

I'm sorry to bother you with such trivialities, but slideshare is definitely not a comfortable way to browse documents. Is a pdf export available somewhere?