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

61–70 of 138 posts

Re: Lisp is not based on the Lambda Calculus

#61

Post by Mathnerd314 »

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.

It's valid Haskell 98 with a type constructor: http://r6.ca/blog/20060919T084800Z.html. But in GHC I think the first code snippet without NOINLINE still crashes, it's a perma-bug: https://downloads.haskell.org/~ghc/latest/docs/html/users_gu...

Some type systems do support equi-recursive types without the type constructor, e.g. Whiley (http://whiley.org/2013/04/21/iso-recursive-versus-equi-recur...). Maybe there you could implement Y without a type signature and have the recursive type inferred.

The main problem is speed. Using the Y combinator is going to mess up whatever code flow analysis the compiler has, unless it's using some cutting edge optimization research that I haven't been able to find.

Re: Lisp is not based on the Lambda Calculus

#62

Post by pron »

paulddraper wrote: post #53
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…

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

Re: Lisp is not based on the Lambda Calculus

#63

Post by tempguy9999 »

carapace wrote: post #46
didibus wrote: post #37

Can we extend from this another misconception then? That functional programming stems from the Lambda Calculus? When in reality, it might come from Lisp, which does not come from Lambda Calculus, thus making Lisp the root of the tree for the origin of functional programming?

We know "the root of the tree for the origin of functional programming": John Backus's Turing Award lecture "Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs" https://amturing.acm.org/award_winners/backus_0703524.cfm It's not obvious but the "ACM Turing Award Lecture" link is the PDF.

I dunno. I thought the foundations were laid in mathematics considerably pre computer. eg. from wiki's page on haskell curry:

"

The focus of Curry's work were attempts to show that combinatory logic could provide a foundation for mathematics. (edit: accidentally stripped the part here mentioned that was in 1933 ie. very pre-computer) [...]. The paradox, developed by Rosser and Stephen Kleene, had proved the inconsistency of a number of related formal systems, including one proposed by Alonzo Church (a system which had the lambda calculus as a consistent subsystem) and Curry's own system. [...]

By working in the area of Combinatory Logic for his entire career, Curry essentially became the founder and biggest name in the field. Combinatory logic is the foundation for one style of functional programming language. The power and scope of combinatory logic are quite similar to that of the lambda calculus of Church, and the latter formalism has tended to predominate in recent decades.

"

And I think there's more but it's hardly my field. Prolog is grown out of predicate calculus which has its roots in propositional calculus, which goes back to the ancient greeks.

The mathematical foundations of things can be surprisingly old. I saw a 3D wireframe of a goblet with perspective, and that was from the 1500's. It could have been done on a 1980's home computer by appearance.

Re: Lisp is not based on the Lambda Calculus

#64

Post by aap_ »

btilly wrote: post #38
vilhelm_s wrote: post #33

Earlier quoted context omitted.

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.

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

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.

Re: Lisp is not based on the Lambda Calculus

#65

Post by empath75 »

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.

From what I understand, he purposefully took ideas from it, but because he did not feel like he understood it fully, he didn’t try to make a full implementation of it.

Re: Lisp is not based on the Lambda Calculus

#66

Post by empath75 »

tempguy9999 wrote: post #58

This is not relevant directly to the subject but perhaps someone in formal langs can help me. I'm interested in optimisation of (necessarily) pure functional langs. Starting with deforesting (the elimination of intermediate structures) eg. map(f, map(g, list(1, 2, 3))) can be optimised trivially by a human to map(f.g, list(1, 2, 3)) (where f.g is functional composition) but I want to do this automatically, and the fi…

The compiler will generally do that sort of optimization.

Re: Lisp is not based on the Lambda Calculus

#67

Post by carapace »

tempguy9999 wrote: post #63
carapace wrote: post #46

Earlier quoted context omitted.

We know "the root of the tree for the origin of functional programming": John Backus's Turing Award lecture "Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs" https://amturing.acm.org/award_winners/backus_0703524.cfm It's not obvious but the "ACM Turing Award Lecture" link is the PDF.

I dunno. I thought the foundations were laid in mathematics considerably pre computer. eg. from wiki's page on haskell curry: " The focus of Curry's work were attempts to show that combinatory logic could provide a foundation for mathematics. (edit: accidentally stripped the part here mentioned that was in 1933 ie. very pre-computer) [...]. The paradox, developed by Rosser and Stephen Kleene, had proved the inconsist…

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

Re: Lisp is not based on the Lambda Calculus

#68

Post by tempguy9999 »

empath75 wrote: post #66
tempguy9999 wrote: post #58

This is not relevant directly to the subject but perhaps someone in formal langs can help me. I'm interested in optimisation of (necessarily) pure functional langs. Starting with deforesting (the elimination of intermediate structures) eg. map(f, map(g, list(1, 2, 3))) can be optimised trivially by a human to map(f.g, list(1, 2, 3)) (where f.g is functional composition) but I want to do this automatically, and the fi…

The compiler will generally do that sort of optimization.

Lord, that's an unhelpful comment. Some compilers do not do that eg. scala, and the cost is high hence my request.

Re: Lisp is not based on the Lambda Calculus

#69

Post by kmill »

paulddraper wrote: post #53
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…

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

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.

Re: Lisp is not based on the Lambda Calculus

#70

Post by bontaq »

dualogy wrote: post #7
tudelo wrote: post #6

Earlier quoted context omitted.

What "three primary functions" are you referring to?

Probably means the 3 irreducable primitives in LC: applications, abstractions, and "variables" (ie. attribute identifiers)

These three? https://en.wikipedia.org/wiki/SKI_combinator_calculus
Post reply on HN