Lambda the Ultimate

Anyone other than Scott & Strachey? The References section of, eg PRG-05, ought to provide a few more names...

It's a bit slow, though.

One is reminded of the saying, "The difficult we do immediately, the impossible takes a little longer"...

it isn't how well, it is that it works AT ALL. :-)

If language A contains programs that can not be expressed in language B then why not just exhibit an interpreter for A that can not be implemented in B? Should someone counter with translation of the interpreter into B then you lose. Any proof that such translation is impossible should be in its clearest form in reference to that interpreter.

Some ActorScript programs implement computations that cannot be expressed in the nondeterministic lambda calculus. Consequently, it is not possible to write an interpreter for ActorScript in the nondeterministic lambda calculus.

See the following:
ActorScript

Well, that paper repeats your assertion without adding argument or support. It doesn't exhibit an interpreter for actorscript that can not be implemented in "the parallel lambda calculus".

So, hmm. I think you are repeating a false result. It is not true that there are programs in ActorScript that can not be expressed in lambda terms.

Unfortunately, you missed the proof by Gordon Plotkin in the following referenced article that the nondeterministic lambda calculus cannot implement the ActorScript program in the article:

Actor Model

So, hmm, it is indeed the case that there ActorScript programs that cannot be expressed in the nondeterministic lambda calculus.

Also, you missed the meta-circular definition of ActorScript in the article at:

ActorScript

If you're referring to the quote from Plotkin on page 39, that isn't about a limit on nondeterministic computational power if it uses global state, it's about a limit on nondeterministic computational power if there isn't any infinite path in the nondeterminism.

The nondeterministic lambda calculus has the same computational power as nondeterministic Turing Machines.

Consequently, Plotkin's proof about the limitation of the computational power of nondeterministic Turing Machines also applies to the nondeterministic lambda calculus.

The passage you quote from Plotkin is not about any limitation on the power of nondeterministic Turing machines. Having misunderstood what Plotkin was talking about, you've based your reasoning on a false premise. I'm sorry, but it's just that simple. Another way of putting what Plotkin says there is, if a nondeterministic Turing machine can only branch in a finite number of ways at any given point in a computation, and if it has an infinite number of possible outputs, then there can't be any finite bound on how many steps it'll take.

Plotkin's proof show that a nondeterministic Turing Machine cannot implement unbounded nondeterminism. However, as explained in the following article,
Actors can implemenent unbounded nondeterminism.

Actors implement unbounded nondeterminism

It is very clear that lambda terms can simulate actor systems perfectly well. The distinction between simulation and direct implementation is a practical distinction, not a fundamental one.

It is very clear that the lambda calculus is not performant versus Actors:
* There are some Actor computations that cannot be implemented at all in the nondeterministic lambda calculus
* For many important applications, Actors are exponentially faster than the parallel lambda calculus.

It is fundamentally important to understand both of the above.

Please see the following article:
Actor Model

I searched your linked paper for "exponent" and found five references. Every single one was a repetition of your assertion. I don't see any argument at all that would defend this assertion. Was the same-fringe example on page 45 supposed to be such an argument? We can easily compute a stream from a tree and compare streams to get the same performance properties there.

And your argument regarding unbounded non-determinism seems incomplete and weak, too. Your alleged proof is an example on page 40. We could certainly implement a non-deterministic machine that, in each step, chooses between incrementing a number or halting and returning the number. This has the same observable behavior as your actors system that, in each iterative step, receives either a go message or a stop message. You seem to be relying on an unspecified implementation of your 'fairness' property to claim that the Actors version will certainly stop, whereas we cannot guarantee the the non-deterministic machine will halt. The unspecified nature of your fairness rule allows a lot of hand-wavy magic.

There isn't even a guarantee that an implementation of your actors model will exhibit any non-determinism. For example, we could most easily implement fairness by sticking available messages in a queue, in which case your counting example would always return 1. Clearly, we can lose unbounded non-determinism with some implementations of fairness. Will we always lose unbounded non-determinism the moment we implement fairness? If not, how can you prove this? If so, it seems that Actors model has some mathematical artifacts and isn't as close to reflecting physical reality as you've claimed it to be.

In any case, I've seen you repeat your assertions here at least twice a year for as long as I've been reading LtU, never once clearly acknowledging the counterpoints, never yielding an inch in your position. My impression is not positive. Please change my impression. Address the substance of arguments by John Shutt, Thomas Lord, and others instead of repeating your assertions using slightly different words or assuming disagreement is misunderstanding.

... has proven ineffective. Maybe we should try adding nofollow to linked references.

Some people see the world different and we lack common ground for productive arguments. Gabriel's essay is useful in this context.

Towards the end:

Bracha & Cook and Cannon are perfectly capable of understanding everything about each others' material set-ups and conceptual frameworks, but they don't want to, because they are in the mangle of their own practices—to use Pickering's terminology.

I cringe when accusations of crankiness are thrown around, justisfied or not, because I'm deathly aware that they will be thrown at me eventually.

I cringe when accusations of crankiness are thrown around, justisfied or not, because I'm deathly aware that they will be thrown at me eventually.

Amen. Anyway there's no shame in it and even when Hewitt is a little bit out of lunch munching on a swiss cheese sandwich (a) there's something interesting to it; (b) i mean it when I say that i think the actor model is under-rated, that the physicality of it Hewitt keeps pointing at is really key to what is missed in it ... just these late formulations are not quite right.

Most ideas have one person who drives them forward. Even when they move a bit beyond that stage, it's still hard for the idea to make major progress without a chief advocate. I remember years ago a former professor of mine opining that a programming language we were discussing would never really take off because of the personality of its creator. Here mathematical competence is an obstacle as well. I'm not sanguine about the near future of actors.

Libels probably won't limit the future of Actors.

The book is being favorably reviewed and there is good uptake from industry. So libelous comments from the side lines about the competence of researchers in the field will probably not have much effect.

Nobody here has made any libelous comments about your behavior.

Libel including insinuating that I am not a competent mathematician, etc.

There is still a problem with form. I am unable to productively read any conversation which has degraded into ActorScript(TM) babbling. I think it is a shame that the beautiful topic created by Ohad on the realization of topological results by programming ends up this way.

Future programming languages will use Unicode.

Just as mathematics is not restricted to ASCII, future programming languages will also not be restricted. (Of course, there must be chords for use on a keyboard to type Unicode into an IDE.)

You can do a lot with unicode given just a smart text editor. Why not render a greater than followed by an equal as ≥? See http://research.microsoft.com/en-us/projects/liveprogramming/typography.aspx.

David,

Proving theorems is a difficult and rigorous business, particularly for something as sophisticated as the Actor Model.

Your bringing up the same-fringe program is just a red herring concerning concurrency because the same-fringe discussion in the article is about co-routines using lists and postponed evaluation instead of the kludges using yield in Java, C#, etc.

Unfortunately, the rest of your post is sufficiently unfocused that it is difficult to know how clarify.

Also, it doesn't help your case to make a lot of unfounded personal attacks. For example, I don't assume that disagreement is misunderstanding. Your challenge is to say something that is sufficiently focused and precise that it rises to the level of a disagreement.

You might try another post that is more focused and rigorous.

Regards,
Carl

PS. Questions, comments, and suggestions on the articles in the book are always most welcome. But please try to keep them focused and precise.

On exactly which page of your linked paper is a valid defense of your "exponentially faster" assertion?

On exactly which page is your proof that implementations of fairness are compatible with unbounded non-determinism?

Thanks David, this is much more focused and precise!

* The published version of the article has that Actor implementations of Direct Logic can be exponentially faster than implementations in the parallel lambda calculus.

* The term "fairness" never appears in the published version of the article. However, there is a great deal of discussion about the semantics of message passing.

I am also of the opinion that the actor model is underrated and merits further development, by the way. I am arguing only against particular arguments you've offered, not against the overall conceptual framework. The physicality of actors is pretty profound, I think.

Please help improve the following article on the Actor Model:
Actor Model

Which particular arguments do you find confusing in the above article?

Sorry, already asked and answered.

Thomas,

We need increased understanding of the following:
* That the lambda calculus does not implement unbounded nondeterminism
* The meta-circular definition of ActorScript
* That it is impossible to write an interpreter for ActorScript in the lambda calculus

I would be pleased to respond to further questions.

Regards,
Carl