Seemingly impossible programs

In case this one went under the radar, at POPL'12, Martín Escardó gave a tutorial on seemingly impossible functional programs:

Programming language semantics is typically applied to
prove compiler correctness and allow (manual or automatic) program
verification. Certain kinds of semantics can also be applied to
discover programs that one wouldn't have otherwise thought of. This is
the case, in particular, for semantics that incorporate topological
ingredients (limits, continuity, openness, compactness). For example,
it turns out that some function types (X -> Y) with X infinite (but
compact) do have decidable equality, contradicting perhaps popular
belief, but certainly not (higher-type) computability theory. More
generally, one can often check infinitely many cases in finite time.

I will show you such programs, run them fast in surprising instances,
and introduce the theory behind their derivation and working. In
particular, I will study a single (very high type) program that (i)
optimally plays sequential games of unbounded length, (ii) implements
the Tychonoff Theorem from topology (and builds finite-time search
functions for infinite sets), (iii) realizes the double-negation shift
from proof theory (and allows us to extract programs from classical
proofs that use the axiom of countable choice). There will be several
examples in the languages Haskell and Agda.

A shorter version (coded in Haskell) appears in Andrej Bauer's blog.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Paper writing algorithm

I'm curious to know whether anyone has applied his algorithm for finding theorems in computability theory (slide 26):

1. Go the library.
2. Pick a book on topology.
3. Pick a theorem.
4. Apply the dictionary.
5. Get a theorem in computation.

Anyone other than Scott &

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

Very nice!

Very nice!

Haskell "countable" package

I coded this up in Haskell and published it on Hackage as countable. The class of searchable types is called "Searchable", and Escardó's method is used to construct "instance (Countable c, Searchable s) => Searchable (c -> s)". It's a bit slow, though.

It's a bit slow, though.One

It's a bit slow, though.

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

dogs playing chess

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

Actually impossible functional programs

Of course, there are actually impossible functional programs in the sense that there are programs which cannot be implemented in the nondeterministic lambda calculus.

For example see the following:
A program that cannot be implemented in the nondeterministic lambda calculus

re actually impossible functional programs

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 computations cannot be expressed as functional programs

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

re Some computations cannot...

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.

ActorScript has a meta-circular definition

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

alas, no

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.

Nondeterministic lambda calculus is same as NDTM

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.

sorry, but no

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.

Unlike Actors, a NDTM can't implement unbounded nondeterminism

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

re: nondeterministic Turing Machine cannot implement

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.

Lambda calculus is not performant versus Actors

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

argument by repetition

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.

argument by reason

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

Some people see the world

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.

re crankiness

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

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

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.

where's the libel?

Nobody here has made any libelous comments about your behavior.

Libel

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

Problem with form

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.

Unicode is the future of programming languages

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

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.

Proving theorems is a difficult and rigorous business

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

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?

Actor Model Semantics

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.

also re actors

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 article on the Actor Model

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

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

re Please help

Sorry, already asked and answered.

Increasing understanding

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

Practicallly impossible functional programs

For important practical applications, functional programs (i.e. what can be implemented in the parallel lambda calculus) can be exponentially slower than concurrency.

See the following article:
Programming language for systems that are exponentially faster than the parallel lambda calculus