Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Lisp is not based on the Lambda Calculus

danielsz.github.io

Post reply on HN
Print view View original

81–90 of 138 posts

Re: Lisp is not based on the Lambda Calculus

#81

Post by carlehewitt »

kazinator wrote: post #41
kmill wrote: post #34

Earlier quoted context omitted.

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…

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

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

See the following:

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

Re: Lisp is not based on the Lambda Calculus

#82

Post by carlehewitt »

pron wrote: post #62
paulddraper wrote: post #53

Earlier quoted context omitted.

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

> 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…

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

Re: Lisp is not based on the Lambda Calculus

#83

Post by carlehewitt »

mrkeen wrote: post #50
bjourne wrote: post #42

Afaik, Haskell is a realization of the (typed!) lambda calculus. Lisps aren't because they don't do lazy evaluation. The LC beta reduction of (\a. a) (\c. d) (\e. f) is (\c. d) (\e. f) but most lisps will reduce it to (\a. a) d. This might seem like a minor detail but means general recursion using the y combinator isn't actually implementable in lisps (I could be wrong though).

> general recursion using the y combinator isn't actually implementable in lisps I think the 'typed' bit is key. You can't implement Y in plain old Haskell because it would need to recurse infinitely during type-checking.

There is a strongly-typed definition of Y here:

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

Re: Lisp is not based on the Lambda Calculus

#84

Post by carlehewitt »

klawed wrote: post #28
danharaj wrote: post #4

It is difficult to believe that McCarthy did not understand he was beating the same horse along with Church, Curry, Schoenfinkel, et al.

Don't forget Gödel!

In his famous 1936 article, Turing correctly noted that proof of the computational undecidabilty of halting problem does not involve the same fixed point as the one used by Gödel.

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

Re: Lisp is not based on the Lambda Calculus

#85

Post by juliangamble »

There are some common themes here. Let's get some precise terminology so we can all talk about the same thing.

Some questions to ponder:

Is Lisp a term re-writing system? https://news.ycombinator.com/item?id=9554335

Is lambda calculus a term rewriting system? https://cstheory.stackexchange.com/questions/36090/how-is-la...

Is the Mathematica language a term-rewriting system? https://mathematica.stackexchange.com/questions/119933/why-d...

And to round it all up: Is Lisp an evaluation system and Lambda calculus an evaluation system? [I'll leave this one to the reader]

Re: Lisp is not based on the Lambda Calculus

#86

Post by pron »

carlehewitt wrote: post #82
pron wrote: post #62

Earlier quoted context omitted.

> 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…

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

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!

Re: Lisp is not based on the Lambda Calculus

#88

Post by dwohnitmok »

kmill wrote: post #34
vga805 wrote: post #3

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 LIS…

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…

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.

Re: Lisp is not based on the Lambda Calculus

#89

Post by carapace »

tempguy9999 wrote: post #74
carapace wrote: post #67

Earlier quoted context omitted.

You reminded me of one of my favorite jokes: "Computer Science could be called the post-Turing decline in the study of formal systems." (I dunno who said it. Maybe Dijkstra.)

That is funny. But you could also restate that as "computer science could be called the post-turing mass commercialisation of formal systems" cos AFAIK being a pure mathematician was never a path to wealth. Come to think of it, still isn't so here's one in return Q. What's the difference between a mathematician and a large pizza? A. A large pizza can feed a family of four.

Not in every case...

https://en.wikipedia.org/wiki/James_Harris_Simons

Re: Lisp is not based on the Lambda Calculus

#90

Post by burakemir »

pron wrote: post #62
paulddraper wrote: post #53

Earlier quoted context omitted.

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

> 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…

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

Post reply on HN