Lambda the Ultimate

...that the Haskell code for the lambda calculus interpreter is a lot longer than Penrose's, but the compiled code is significantly smaller. :-)

(Just so used to throwing away constants in the big-O notation.)

I'm guessing that the proposition is that a UTM can be constructed from the pattern of 14 bits (00010011011111), but would those 14 bits constitute an actual Turing Machine in and of themselves?

Thought an email I received from John Tromp might be of interest:

Those cellular automata are universal only in a very roundabout sense, requiring you to first express your computation as a cyclic tag system, and then providing the CA with a specific infinitely long pattern (of which those 14 bits repeated form the background) as initial state, then running it long enough for certain conditions to arise, and then extracting the answer again from the current pattern.

My machines are universal in a much more useful, direct, sense: they process binary streams, parsing a program from it, that they run on the remainder of the stream. Furthermore, these programs are quite compact, which is of course what I needed for my application to Kolmogorov Complexity.

Hmm... If by apples and orange you mean both are roughly spherical fruits of similar size, then I guess I agree ;-)

John Tromp's examples are universal only in a very roundabout sense, requiring you to first express your computation in the lambda calculus (or combinatory logic), encode that program in binary, and then having an interpreter with a an infinitely long stack space to hold intermediate results...

then having an interpreter with a an infinitely long stack space to hold intermediate results...

...encode that program in binary...

...

My argument above was a little different than John's response in that I don't consider a single cell of Rule 110 to be a Turing Machine. Rather, a TM can be constructed from a grid of interacting cells. Drawing an analogy, a single human brain cell is likely not considered to be a TM, but get enough of them together and you eventually end up with something that is Turing complete. So the measure of Rule 110 should not be that a TM can be constructed with a single 14 bit cell, but rather we'd like to know what is the smallest grid which can be constructed that achieves this level of computing? I suspect that the minimum number of cells required to achieve Turing completeness would dwarf the LC and CL implementations - but that's pure conjecture on my part. Something along the lines of the way a TM was constructed in the Game of Life.

And I suppose I should have made it more obvious from my reference in the original post that Occam's Razor is not really a decisive form of logic - being more a technique of persuasion. What is simple is a matter of circumstance and judgement. And since we measure all these forms of analysis in terms of Turing Completeness, the means by which we actually compare the relative merits of each has to be based on the insight they give us, the kinds of problems we are attempting to solve, and the constraints we are given.

But that's not nearly as much fun as saying "mine's smaller". :-)

And I suppose I should have made it more obvious from my reference in the original post that Occam's Razor is not really a decisive form of logic - being more a technique of persuasion. What is simple is a matter of circumstance and judgement.

Occam's razor is not about "simplicity", but about the axioms of logical arguments; it actually is a valid logical principle.

Occam's Razor is fine when applied to variations of a single system. For example, the SK-Combinator logic is considered to be more fundamental than SKI because I can be derived from S and K.

However, using Occam's Razor to compare two disparate competing systems is more tenuous. In the current instance, is Combinator Logic more fundamental than Lambda Calculus (or Turing Machines or Cellular Automata)? And how do we compare the axioms between the systems? I'm not sure that sheer quantity of axioms (or even more arbitrarily, the number of bits) represents a fair cop.

I'd say that Combinator Logic's more fundamental in that it doesn't need variables. I think there's a way we can go in (E)DSL design with the knowledge that variables aren't "fundamental" - that they're effectively a UI issue. Not least in EDSLs by handing off binding to the host language!

I'd say that Combinator Logic's more fundamental in that it doesn't need variables

And I would say the opposite for the same reason. Variable binding ( a separate concept from the mere labelling of the variable) is the fundamental concept of computation.

Bringing that concept explicitly into the model by means of labelling, however, is much clearer than trying to hide it as a "UI issue", or throwing explicit variables aside because they present some descriptive problems for the theory.

(We really haven't given enough time to the pointed vs. point-free holy war here on LtU; consider this my pro forma entry. ;-) )

So would you go to the other extreme and suggest A-normal form as more fundamental than the conventional lambda calculus?

o would you go to the other extreme and suggest A-normal form as more fundamental than the conventional lambda calculus?

Definitely not. A-normal form is more generally conceived as a convenience for compilers, not for humans. (Though, there may be exceptions to this...)

My position here is based on the goal of making key theoretical concepts visible and central for a person trying to understand computation by means of the model.

Maybe it's just me, but though I think combinatory logic is cool, for real purposes, I find LC much easier to reason about, thanks to the explicit labelling of bindings.

ANF's just the extreme form though - almost everything gets labelled, including all those temporaries that only get used once. The only values that go unbound are constants. IME it's often actually easier to explain that to people first and then release the restrictions to get plain LC back, even if LC is simpler syntactically.

One way of looking at it is that ANF requires you to bind results as well as parameters - something that in an unsugared LC you can't actually do.

One way of looking at it is that ANF requires you to bind results as well as parameters - something that in an unsugared LC you can't actually do.

By "can't actually do", do you just mean that unsugared LC has no 'let'? Otherwise, (λ x. M) E  seems like a pretty good candidate for binding results in unsugared LC, i.e. binding the result of E to x in M.

From this perspective, in an unsugared LC with CBV evaluation (for simplicity in talking about "results"), results are "required" to be bound because the only thing you can do with a result is apply a function to it, thereby binding it.

It seems to me that ANF only becomes meaningful when you're dealing with languages that have more complex built-in data types (e.g. tuples) and/or functions that take multiple arguments, so that the idea of intermediate values comes into play. ANF requires you to bind intermediate values. [Edit: whereas in an unsugared LC, there aren't any intermediate values.]

Sure, I'm discussing in the terms already given - though for pedagogical purposes I don't think using the unsugared version (except to show the desugaring) is exactly helpful in showing results being bound.

Exposing the notion of intermediate values is perhaps entirely the point here. I'm reminded of the result about the lambda calculus not offering any opportunities for parallelism against an imperative language that strangely disappears when you add things that take multiple parameters.

Variable binding may be how _you_ think about computation, but that doesn't make it fundamental. The fact that combinators do everything lambdas can completely proves that. Either one is fundamental, and combinators lack a complex feature lambdas have while still preserving the same functionality.
But this doesn't prove anything about a "pointed vs. point-free holy war"; combinators may be more fundamental, but that doesn't mean all your code should use nothing but combinators. There's SO MUCH else to do with one's life aside from figuring out combinators or primitive lambdas :-).

There's SO MUCH else to do with one's life aside from figuring out combinators or primitive lambdas :-).

As if. Name one thing that's more important! ;-)

Contemplating the nature of the curse from which all recursion originated?

Somewhat reminiscent of the discussion on which is more fundamental: Lists or Sets. The answer is the somewhat unsatisfying: it depends on what you want to do.

Since we're focused on PLs and this is not "Tape the Ultimate", we are allowed to root for the home team. :-)

Some points about the tools you mention. Because these are analytic systems order and steps are ignored sence order is irrelevant to the outcome. But there are reasons to consider states even in an analytic situation. You need state in any information theory context, like the one in the paper. Also I would argue that you need information in dealing with the world outside any analytic component.