[paulddraper]

> In classic lambda calculus, everything is a lambda term

OO says everything is an object. Even though Java has non-object primitives, we're still gonna classify Java as OO.

> Lambda calculus does not have any evaluation rules.

> The lambda terms in lambda calculus are not inspectable objects, but more just a sequence of symbols.

It's not clear to me why this makes Lisp not in the family of Lambda implementations.

> In the original Lisp, there was a stack of variable bindings instead, leading to something that is now known as dynamic scoping.

That's true. Every modern Lisp (Scheme, Clojure, Racket) has lexical scoping. And Common LISP uses lexical by default.

> Later, many of these ideas were backported to Lisp during the standardization of Common Lisp.

Again this contributes to the notion that LISP/Schema/Lambda Calculus were "discovered", not that Lambda calculus has an explicit pedigree.

[kmill]

Unlike lambda calculus, OO is not a specific mathematical formalism but rather a methodology and ontology for organizing a program. Lambda calculus, defined by Alonzo Church, is a kind of 'arithmetic' of abstract function manipulation devoid of semantics. It has some strong theoretical footing as, in modern language, reflexive objects in a category.

> It's not clear to me why this makes Lisp not in the family of Lambda implementations.

To be clear, I started my comment by writing "if it is a realization, then it is one with [the following differences]." Lambda calculus was such a good idea that pretty much anything with function abstractions can be described by some variation of it. It's the dynamic scoping that causes the main issues here, though, and suggests lambda calculus was not a significant motivation in the definition of McCarthy's Lisp. Yet, he was still aware of it enough to call the abstraction operator "lambda."

>> Later, many of these ideas were backported to Lisp during the standardization of Common Lisp.

> Again this contributes to the notion that LISP/Schema/Lambda Calculus were "discovered", not that Lambda calculus has an explicit pedigree.

I don't see how that follows. Sussman was a math undergrad and PhD and was well aware of developments in logic, and he influenced Steele, who created the quite-influential Scheme and went on be one of the main people on the standardization committee for Common Lisp. This isn't even mentioning all the work people have done in PL research with typed lambda calculi (going back to corrections to Church's attempt to use lambda calculus as a foundation for mathematics), which has influenced the designs of many type systems in modern programming languages.

[ProfHewitt]

Object orientation derived from Simula-67 which was lexically scoped and preceded Sch3me by many years.

[DonHopkins]

So Lisp 1, Lisp 2, Sch3me?

[ProfHewitt]

Sorry for the typo, HN on Android didn't enable me to fix it :-(

[DonHopkins]

Are you really who you profess to be, or are you only acting?

[pron]

> this contributes to the notion that LISP/Schema/Lambda Calculus were "discovered", not that Lambda calculus has an explicit pedigree.

That notion is wrong (at least with a very high likelihood), and it's usually stated by people who fetishize the lambda calculus but know little of its long evolution. It's just your ordinary case (of hubris) where people aesthetically drawn to something describe it as inevitable or even a law of nature. And I know it's wrong in part because of the following quote:

> We do not attach any character of uniqueness or absolute truth to any particular system of logic. The entities of formal logic are abstractions, invented because of their use in describing and systematizing facts of experience or observation, and their properties, determined in rough outline by this intended use, depend for their exact character on the arbitrary choice of the inventor.

This quote is by the American logician Alonzo Church (1903-1995) in his 1932 paper, A Set of Postulates for the Foundation of Logic, and it appears as an introduction to the invention Church first described in that paper: the (untyped) lambda calculus [1].

The simpler explanation, which has the added benefit of also being true, or at least supported by plentiful evidence, is that the lambda calculus was invented as a step in a long line of research, tradition and aesthetics, and so others exposed to it could have (and did) invent similar things.

If you're interested in the real history of the evolution of formal logic and computation (and algebra) you can find the above quote, and many others, in a 300-page anthology of (mostly) primary sources that I composed about a year and a half ago [2]. They describe the meticulous, intentional invention of various formalisms over the centuries, as well as aesthetic concerns that have led some to prefer one formalism over another.

[1]: Actually, in that paper, what would become the lambda calculus is presented as the proof calculus for a logic that was later proven unsound. The calculus itself was then extracted and used in Church's more famous 1936 paper, An Unsolvable Problem of Elementary Number Theory in an almost-successful attempt to describe the essence of computation. That feat was finally achieved by Turing a few months later.

[2]: https://pron.github.io/computation-logic-algebra

[burakemir]

Thanks for this comment and the anthology. Indeed the whole question is a bit odd and one ought not to glorify calculi but study them.

Lambda calculus originated from research in formal logic, which is about manipulating symbols according to precise rules that would capture reasoning. It is a compelling way to combine variable binding, equality and substitution into a model of "function calls" - even if the purpose was to formalize arithmetic computation and reasoning.

At some level, reasoning is what programming is about as well! The notation and rules may change, but ultimately we want to make the machines do things and at some level, we need abstraction mechanisms. Recursive procedures are such a mechanism and it can be expressed as a lambda term that involves a fixed-point combinator, or machine code.

It is easy to model and understand many things using lambda calculus or functional programming techniques, depending on whether the interest is theoretical/formal or practical.

To quote Peter Landin (heavily influenced by McCarthy and LISP and author of 'The next 700 programming languages'):

> A possible first step in the research program is 1700 doctoral theses called "A Correspondence between x and Church's λ-notation."

Maybe people think this was different in the late 1950s?

Let's read McCarthy's paper 'Recursive Functions of Symbolic Expressions and their computation by machine Part I' where he explicitly cites Church and introduces lambda notation.

I would consider that paper part of the phenomenon that is LISP, would that not settle the question? Lambda calculus gives little guidance in terms of implementation, but I think it does not diminish LISP in any way that it should be "based" on lambda calculus.

And I do not find the linked article adds any value, but I am very glad to read the HN discussion to find gems like the above (even if I should rather have slept for the past few hours).

[DonHopkins]

So Lambda isn't the Ultimate Law of Nature, but Lambda isn't the Ultimate Scam either.

https://softwareengineering.stackexchange.com/questions/1076...

[carlehewitt]

BTW, the Church/Turing theory of computation is not universal for digital computation as explained in the following article:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3418003

[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.

[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.

[ProfHewitt]

The lambda calculus and Turing machines are both adequate for Church/Turing computability. However, neither are adequate for all digital computation.

[kmill]

Wow, that is an impressive survey --- thanks for putting that together!

[sideeffffect]

Ron presented this at Curry On 2018

Ron Pressler - Finite of Sense and Infinite of Thought: A History of Computation, Logic and Algebra

https://www.youtube.com/watch?v=2oNmR0q1uA0