Live data from Hacker News

Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus

woodrush.github.io

31–40 of 101 posts

Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus

#31

Earlier quoted context omitted.

It has to be slow. Multiplication will be O(N^2)!

Multiplication is generally done in O(n^2) of the number of bits so I'm not sure what you mean to say. Do you mean O(n^2) of the size of the operands?

In Lambda calculus, numbers are encoded using 0 and successor. So 3 = S(S(S(0)))

Adding these would be O(N+M) where N and M are the numbers, not the number of bits.

Multiplying is O(N*M) where again it is the numbers.

1000*1000 would require a million operations at least. It takes a million operations just to store/read the number million!

See: https://en.wikipedia.org/wiki/Church_encoding

Unless this HN submitted implementation doesn't use church encoding. In which case I am wrong.

Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus

#32
post #10

Earlier quoted context omitted.

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…

LC is only computationally foundational; it describes recursive functions. It's just another universal turing machine. LC has a great disadvantage: it's difficult to write a LC interpreter in LC. This project shows exactly what that means. To write an LC interpreter, you need a data structure for representing expressions. You need a symbolic data type. LC does not know what a LC expression is. Papers about LC know wh…

There is. Using the Mogensen–Scott encoding, a self-interpreter can be written in lambda calculus as

(λf.ff)(λf.λt.t(λx.x)(λm.λn.ffm(ffn))(λm.λv.ff(mv))),

which is a direct translation of the equivalent Haskell code

    data Term t = Var t | App (Term t) (Term t) | Abs (t -> Term t)
    newtype Function = Function {apply :: Function -> Function}

    interpret :: Term Function -> Function
    interpret (Var x) = x
    interpret (App m n) = apply (interpret m) (interpret n)
    interpret (Abs m) = Function (\v -> interpret (m v))
https://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encodin...

Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus

#33
post #2

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

Delightful, thank you

Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus

#34
post #10

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

> which is why it took 20 years of further research to go from Lisp 1 to Scheme.

Actually it only took Peter Landin a few years. For example see:

P. J. Landin, The Mechanical Evaluation of Expressions, The Computer Journal, Volume 6, Issue 4, January 1964, Pages 308–320, https://doi.org/10.1093/comjnl/6.4.308

Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus

#35
post #11
post #7

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

> 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. That's hardly a fair comparison. LambdaLisp includes a ton of features that BLC and BF do not.

Slap yourself and reread the rest of the post.

Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus

#36
post #10

Earlier quoted context omitted.

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…

I'd say that all foundations are mathematical (at least for 'concrete' stuff, and more besides). If lisp was foundationaly interesting presumably mathematicians would have given it more study? (perhaps they did?) I would disagree that computation is process for doing math - it is math in its own right, specifically that for operating over a discrete state space (urgh help needed to tighten this statement up) LC is ba…

Lisp is called the dyck language or the catalan numbers depending on what kind of mathematician you are talking to.

Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus

#37

Earlier quoted context omitted.

LC is only computationally foundational; it describes recursive functions. It's just another universal turing machine. LC has a great disadvantage: it's difficult to write a LC interpreter in LC. This project shows exactly what that means. To write an LC interpreter, you need a data structure for representing expressions. You need a symbolic data type. LC does not know what a LC expression is. Papers about LC know wh…

There is. Using the Mogensen–Scott encoding, a self-interpreter can be written in lambda calculus as (λf.ff)(λf.λt.t(λx.x)(λm.λn.ffm(ffn))(λm.λv.ff(mv))), which is a direct translation of the equivalent Haskell code data Term t = Var t | App (Term t) (Term t) | Abs (t -> Term t) newtype Function = Function {apply :: Function -> Function} interpret :: Term Function -> Function interpret (Var x) = x interpret (App m n)…

I don't see what in the interpreter converts the lambda calculus into the Morgensen-Scott encoding.

The Wikipedia page describes a "mse" function that is in some meta-language which is not lambda calculus. So first wee need a Lambda Calculus based interpreter for the meta-language, which can run this "mse" function.

It looks like mse[x] is supposed to match a variable term, and mse[M N] matches a function application and so on. There are no such concepts and representations in lambda calculus, not to mention shape matching on them.

The meta language might as well just be a paragraph of English: instructions on how to hand-compile the lambda calculus into a bunch of thunks which the interpreter can just invoke in certain ways to bring about the evaluation.

Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus

#39
post #11

Earlier quoted context omitted.

> 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. That's hardly a fair comparison. LambdaLisp includes a ton of features that BLC and BF do not.

Slap yourself and reread the rest of the post.

Sorry, I’m going to need you to give me a little more of a clue what you are talking about.

Re: Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus

#40
post #18

Earlier quoted context omitted.

I think I meant computation in the mathematical sense. In other words that 'computation' is a mathematical object worthy of study in its own right. Per analog and quantum, indeed, and they are also mathematics. I think that is my point - (very nearly) everything proceeds from mathematics, there is no other foundation.

What can I say? You are mistaken. Computation is as much about physics as it is about math. It is the study of what can actually be done in this universe with real hardware (including human brains). If you doubt this, read the opening paragraph of this paper: https://www.scottaaronson.com/papers/pnp.pdf The only reason that P=NP? matters at all (let alone why it is a foundational question) is because the theory of co…

Opening paragraphs of the linked paper:

> In 1900, David Hilbert challenged mathematicians to design a “purely mechanical procedure” to determine the truth or falsehood of any mathematical statement. That goal turned out to be impossible. But the question — does such a procedure exist, and why or why not? — helped launch two related revolutions that shaped the twentieth century: one in science and philosophy, as the results of G ̈odel, Church, Turing, and Post made the limits of reasoning itself a subject of mathematical analysis; and the other in technology, as the electronic computer achieved, not all of Hilbert’s dream, but enough of it to change the daily experience of most people on earth.

> Although there’s no “purely mechanical procedure” to determine if a mathematical statement S is true or false, there is a mechanical procedure to determine if S has a proof of some bounded length n: simply enumerate over all proofs of length at most n, and check if any of them prove S. This method, however, takes exponential time. The P ?= NP problem asks whether there’s a fast algorithm to find such a proof (or to report that no proof of length at most n exists), for a suitable meaning of the word “fast.” One can think of P ?= NP as a modern refinement of Hilbert’s 1900 question. The problem was explicitly posed in the early 1970s in the works of Cook and Levin, though versions were stated earlier—including by G ̈odel in 1956, and as we see above, by John Nash in 1955.

> Think of a large jigsaw puzzle with (say) 101000 possible ways of arranging the pieces, or an encrypted message with a similarly huge number of possible decrypts, or an airline with astronomically many ways of scheduling its flights, or a neural network with millions of weights that can be set independently. All of these examples share two key features:

> (1) a finite but exponentially-large space of possible solutions; and

> (2) a fast, mechanical way to check whether any claimed solution is “valid.”

Post reply on HN