Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus
woodrush.github.io
Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus
1–10 of 101 posts
Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus
#2This is one of the most mind-blowing things I have ever seen. Words fail me, so I'll appropriate some of the author's:
"Lisp has been described by Alan Kay as the Maxwell’s equations of software. In the same sense, I believe that lambda calculus is the particle physics of computation. LambdaLisp may therefore be a gigantic electromagnetic Lagrangian that connects the realm of human-friendly programming to the origins of the notion of computation itself."
BTW, if you have no idea what is going on here, eight years ago I took a whack at writing a gentle introduction to this same sort of thing, but done in a more half-assed way, and with a much less ambitious scope:
Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus
#3> Here is a PDF showing its entire lambda term, which is 42 pages long:
Elsewhere, Douglas Adams smiles.
Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus
#4Maybe I am stupid but what's the point in reimplementing lisp in lambda? Just to prove how beautiful simple lambda calculus is? The lambda functionality is allready in lisp. And lisp is beautiful simple!
() is nothing and (is something) What does the implementation show more beautiful than that?
Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus
#5> Here is a PDF showing its entire lambda term, which is 42 pages long: Elsewhere, Douglas Adams smiles.
This
Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus
#6This is undoubtedly cool, but I'd be really impressed if it wasn't stupidly slow. (I'm not saying it is stupidly slow, because I haven't had a chance to run it, just that I'd be impressed if it wasn't.)
Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus
#7As author of the Binary Lambda Calculus (BLC), I find this quite fascinating.
It implements LISP in 163,654 bits of BLC.
For comparison, minimal esoteric languages like BLC itself can be implemented in 232 bits of BLC, and Brainfuck in 893 bits.
I'm still reading the document, but one thing that caught my eye is the List encoding with cons and nil, which is claimed to be a Mogensen-Scott one.
Rather, cons \x\y\c. c x y is the Scott encoding of infinite lists that have no nil terminator (also known as streams) and thus only one constructor, while nil is the Scott encoding in nil-terminated lists with 2 constructors.
Thus the given encoding is some non-standard hybrid of streams and lists that helps BLC achieve its conciseness. In Wikipedia [1] it's described as
> Alternatively, with NIL := FALSE, the construct l (λh.λt.λz.deal_with_head_h_and_tail_t) (deal_with_nil) obviates the need for an explicit NULL test
Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus
#8Maybe I am stupid but what's the point in reimplementing lisp in lambda? Just to prove how beautiful simple lambda calculus is? The lambda functionality is allready in lisp. And lisp is beautiful simple! () is nothing and (is something) What does the implementation show more beautiful than that?
Binary Lambda Calculus is indeed beautifully simple [1].
LISP is rather complex by comparison, but then it's full-fledged non-esoteric programming language.
Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus
#9Lambda calculus is mathematically foundational in a way that Lisp of course isn't.
The question is what does Lisp give us as an interpretation of those foundations? Or does it admit issues that might be unhelpful? (Are macros a good thing?)
Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus
#10Lambda calculus is mathematically foundational in a way that Lisp of course isn't. The question is what does Lisp give us as an interpretation of those foundations? Or does it admit issues that might be unhelpful? (Are macros a good thing?)
Let's not sell Lisp short here. LC might be mathematically foundational, but I think it's fair to say that Lisp is computationally foundational. Mathematics and computation are related, of course, but they are not identical. Computation is the study of mechanical processes for doing math. As such, Lisp's identification of CONS/CAR/CDR/COND as a sufficient set of primitives for a universal Turing machine is important because it's obvious (or at least it was obvious by 1958) how those primitives can be implemented as a mechanical process. Implementing LAMBDA in all its generality is far less obvious, which is why it took 20 years of further research to go from Lisp 1 to Scheme.