[vga805]

The post quotes McCarthy:

"one of the myths concerning LISP that people think up or invent for themselves becomes apparent, and that is that LISP is somehow a realization of the lambda calculus, or that was the intention. The truth is that I didn't understand the lambda calculus, really" - John McCarthy

So there are a two issues here, 1) whether or not it was McCarthy's intention to realize the Lambda Calculus in LISP, and 2) whether or not LISP is such a realization. Or at least some kind of close realization.

The answer to 1 is clearly no. This doesn't imply an answer to 2 one way or another.

If 2 isn't true, what explains the widespread belief? Is it really just that he, McCarthy, borrowed some notation?

[vilhelm_s]

Modern lisps do realize the lambda calculus, but this was not immediate. In particular, in order to exactly match the lambda-calculus beta-reduction rule, you need to use lexical rather than dynamic scope, which did not really become popular until Scheme in the 1970s.

[btilly]

Did not become popular, or did not become implemented?

My understanding is that lexical scope was first implemented in Algol and Pascal, and then was first implemented with true garbage collection in Scheme. (Thereby leading to the restriction in Algol and Pascal that closures existed, but they could only be passed into functions, and never returned from them. That way the variables being closed over could live on the stack.)

But I'd love to learn that I'm wrong and that these things came before that.

[vilhelm_s]

Oh, I think you're right, Scheme was at least the first lexically scoped Lisp.

Wikipedia says

> The concept of closures was developed in the 1960s for the mechanical evaluation of expressions in the λ-calculus and was first fully implemented in 1970 as a language feature in the PAL programming language to support lexically scoped first-class functions.

> PAL, the Pedagogic Algorithmic Language, is a programming language developed at the Massachusetts Institute of Technology in around 1967 to help teach programming language semantics and design. It is a "direct descendant" of ISWIM and owes much of its philosophy to Christopher Strachey.

[aap_]

LISP 1.5 as described in the manual implements lexical scope, at least in the interpreter. I haven't studied the compiler too closely, I think there dynamic scope is more prevalent, but as far as I know it has lexical scope as well.

[vilhelm_s]

Where do you see that?

Looking at the "Universal LISP function" on page 13 in [0], the case for apply/LAMBDA just extends the current environment a with the arguments of the lambda, but it doesn't unpack a closure to get the environment the lambda function was defined in, so it implements the dynamic version. (Unlike, e.g., the interpreter in SICP [1].)

[0] http://www.softwarepreservation.org/projects/LISP/book/LISP%... [1] https://mitpress.mit.edu/sites/default/files/sicp/full-text/...

[aap_]

The one on page 13 is not what LISP 1.5 does, that's more of an earlier purer idea. I meant the one on page 70 where FUNCTION packs a fucking together with its environment into a FUNARG closure, which when applied unpacks the environment it was created with.

[vilhelm_s]

Interesting! So yeah, the LISP 1.5. interpreter already seems to do this.

Googling a bit, it seems that McCarthy mentions this in "History of Lisp" [0], as a change from LISP 1 to LISP 1.5:

> In modern terminology, lexical scoping was wanted, and dynamic scoping was obtained. I must confess that I regarded this difficulty as just a bug and expressed confidence that Steve Russell would soon fix it. He did fix it but by inventing the so-called FUNARG device that took the lexical environment along with the functional argument. Similar difficulties later showed up in Algol 60, and Russell's turned out to be one of the more comprehensive solutions to the problem. While it worked well in the interpreter, comprehensiveness and speed seem to be opposed in compiled code, and this led to a succession of compromises. Unfortunately, time did not permit writing an appendix giving the history of the problem, and the interested reader is referred to (Moses 1970) as a place to start. (David Park tells me that Patrick Fischer also had a hand in developing the FUNARG device).

So I guess closures had been invented at least by 1962 (when the LISP 1.5 manual was published), but were not widely used because of performance considerations?

[0] http://www-formal.stanford.edu/jmc/history/lisp/node4.html

[paulddraper]

Now, all the Lisps (Racket, Clojure) are lexically scoped.

Common LISP is lexically scoped, though it does still have opt-in dynamic scoping ("special variables").

[bathyspheric]

Emacs Lisp is still dynamically scoped, no?

[Jtsummers]

https://www.gnu.org/software/emacs/manual/html_node/elisp/Us...

Since Emacs 24.1 (had to look up the version), it's been possible to enable lexical scope for a file or buffer. The default is still dynamic scope, and dynamic scope can be achieved even after enabling lexical scope with certain conditions.

[Impl0x]

I believe so, yes.

[jasonhansel]

Question: if lexical scopes are in the language's data structures, but can't be explicitly created or made visible in the language's syntax, is it still homoiconic?

[seanhunter]

If you look up a definition of lexical scope, you'll typically see something like this (from https://en.wikipedia.org/wiki/Scope_(computer_science)#Lexic... but others are similar).

"With lexical scope, a name always refers to its (more or less) local lexical environment. This is a property of the program text..."

So as local lexical environment isa property of the program text, lexical scope is explicit in the language's syntax.

[fourthark]

Aren't lexical scopes visible in the language's syntax?

[_emacsomancer_]

> So there are a two issues here, 1) whether or not it was McCarthy's intention to realize the Lambda Calculus in LISP, and 2) whether or not LISP is such a realization. Or at least some kind of close realization.

This would fit in with Graham's suggestion that McCarthy more "discovered" Lisp than "invented" it.

[kmill]

If it was a realization of a lambda calculus, then it is one with (a) primitives, (b) strict evaluation, (c) quoted lambda terms, and (d) "dynamic" bindings.

(a) In classic lambda calculus, everything is a lambda term. McCarthy's Lisp has primitives like lists and numbers. However, it is known that lambda calculus is powerful enough to encode these things as lambda terms (for example,

  null = (lambda (n c) (n))
  (cons a b) = (lambda (n c) (c a b))

gives a way to encode lists. The car function would be something like

  (car a) = (lambda (lst)
              (lst (lambda () (error "car: not cons"))
                   (lambda (a b) a)))

This would not work in the original Lisp because of binding issues: the definition of cons requires the specific a and b bindings be remembered by the returned lambda.)

(b) Lambda calculus does not have any evaluation rules. Rather, it is like algebra where you can try to normalize an expression if you wish, but the point is that some lambda terms are equivalent to others based on some simple rules that model abstract properties of function compositions. Lambda-calculus-based programming languages choose some evaluation rule, but there is no guarantee of convergence: there might be two programs that lambda calculus says are formally equivalent, but one might terminate while the other might not. Depending on how you're feeling, you might say that no PL for a computer can ever realize the lambda calculus, but more pragmatically we can say most languages use lambda calculus with a strict evaluation strategy.

(c) The lambda terms in lambda calculus are not inspectable objects, but more just a sequence of symbols. Perhaps one of the innovations of McCarthy is that lambda terms can be represented using lists, and the evaluator can be written as a list processor (much better than Godel numbering!). In any case, the fact that terms have the ability to evaluate representations of terms within the context of the eval makes things a little different. It's also not too hard to construct a lambda evaluator in the lambda calculus[1], but you don't have the "level collapse" of Lisp.

(d) In lambda calculus, one way to model function application is that you immediately substitute in arguments wherever that parameter is used in the function body. Shadowing is dealt with using a convention in PL known as lexical scoping, and an efficient implementation uses a linked list of environments. In the original Lisp, there was a stack of variable bindings instead, leading to something that is now known as dynamic scoping, which gives different results from the immediate substitution model. Pretty much everything fun you can do with the lambda calculus depends on having lexical scoping.

All this said, the widespread belief about Lisp being the lambda calculus probably comes from Scheme, which was intentionally lambda calculus with a strict evaluation model. Steele and Sussman were learning about actors for AI research, and I think it was Sussman (a former logician) who suggested that their planning language Schemer (truncated to Scheme) ought to have real lambdas. At some point, they realized actors and lambdas (with mutable environments) had the exact same implementation. This led to "Scheme: An Interpreter for Extended Lambda Calculus" (1975) and the "Lambda the ultimate something" papers. Later, many of these ideas were backported to Lisp during the standardization of Common Lisp.

[1] https://math.berkeley.edu/~kmill/blog/blog_2018_5_31_univers...

[carlehewitt]

Schemer (later renamed Scheme) was invented to scheme against Actors reprising Conniver, which was invented to connive against Planner.

See the following for the current state of the art including the latest Actor approach to Eval, which is more modular and concurrent than the Eval in Lisp and Scheme:

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

The above article explains exactly how Actors are much more powerful than lambdas with mutable environments.

[DonHopkins]

How wonderful to hear directly from the Master himself! Brilliant!!! Thank you! ;)

https://www.youtube.com/watch?v=dmZSkWBJwBU

https://www.youtube.com/watch?v=AtnBumt82_Y

[Cybiote]

Adding a little to your wonderful post, another possibility for why the conflation of the original lisp as based on the lambda calculus is that its notation was heavily inspired by the lambda calculus, even though it was more properly a refinement of the μ-recursive functions (of form f:(N,N,...N) -> N) over the natural numbers.

While a lot of people are trying to defend the lambda calculus as a basis, I think this actually undersells the significance of LISP. Apart from Lisp the language family and its implementations, there is Lisp, (arguably) the first practically realizable mathematical model of computation. That is, it stands on its own as a model for computation†, continuing along a long line of which I think Grassmann's 1861 work on arithmetic and induction is a good starting point.

Turing Machines are intuitive and the lambda calculus is subtle and expressive, but Lisp's contribution was to place partial recursive function on a more intuitive/realizable basis in terms of simple building blocks of partial functions, predicates, conditional expressions and symbolic expressions (ordered pairs/lists of atomic symbols). Lambdas come in as a notation for functions with a modification to facilitate recursive definitions.

†Making Greenspun's Tenth Rule trivially true.

[btilly]

Thank you.

This is probably the most informative comment that I've read on HN in the last couple of months.

[eries]

Agreed

[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 :-(

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

[ProfHewitt]

There are simple nondetermintic procedures that can be implemented by digital circuits using arbiters that cannot be implemented by a nondeterminustic Turing Machine.

[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

[danielszm]

This is excellent. Thank you!

John McCarthy said that he never had the intention to realize the lambda calculus, but he followed that statement with the corollary that had someone "started out with that intention, he might have ended with something like LISP." Peter Landin was a pioneer in that regard. See "The Mechanical Evaluation of Expressions", published in 1964, and the SECD virtual machine. Machine interpreters like SECD and CEK may come close to a "realization" of the lambda calculus. Their design is directly inspired by its semantics. You don't necessarily end up with something like LISP, but you can, see Lispkit and LispMe.

[dwohnitmok]

For (b) isn't this the appeal of normal-order evaluation (or its related sibling lazy evaluation)? If there is a terminating reduction sequence lazy evaluation will find it, whereas eager evaluation will fail to find it.

Moreover the lambda calculus is confluent, so if you find the terminating reduction sequence, you're guaranteed all other terminating sequences end up with the same result.

So as long as your PL uses normal-form evaluation or lazy evaluation you can entirely realize any equivalences in the lambda calculus.

[kazinator]

and (e) mutation: `setq`, `rplacd`, ...

[carlehewitt]

'Setq' and 'rplacd' also do not provide the power of Actors.

See the following:

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

[illvm]

Could it be that, at least some, university teach programming languages with the idea that Lisp has this feature? My PL course at Northeastern had SHLAC (Scheme Has Lambda Calculus) where we started with an identity function and built up from there.

[vga805]

That seems likely. But then, I would think LISP does realize the lambda calculus in some sense. It naturally lends itself to this sort of exercise and it's really successful.

[agumonkey]

both fair points but I'd like to know if he mentioned why on earth did he pick lambda. lambda expressions/closures turned out to be a very peculiar and important path.