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

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

woodrush.github.io

Post reply on HN
Print view View original

51–60 of 101 posts

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

#51

Post by tromp »

lisper wrote: post #10
somewhereoutth wrote: post #9

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…

Lambda Calculus is computationally foundational. Lisp carries a lot of non-foundational baggage, some of which (like number primitives) makes it far more efficient for running on actual hardware.

> As such, Lisp's identification of CONS/CAR/CDR/COND as a sufficient set of primitives for a universal Turing machine

You don't need any of those for universality. They are trivially expressible in Lambda Calculus. LAMBDA is really the only necessary primitive.

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

#52

Post by tromp »

armchairhacker wrote: post #21
somewhereoutth wrote: post #9

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

Lisp is more expressive: I can write any program in LC but I'd much rather use Lisp. Similarly someone could write C or JavaScript or Swift or Haskell in LC. Although I'd argue Lisp is a bit better as it's one of the first languages, one of the first to involve functional concepts like code-as-data, and itself is based on really simple concepts like LC.

Haskell is more expressive. I can write any program in LISP but I'd much rather use Haskell. Btw, Haskell is much closer in spirit to LC than LISP is.

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

#53

Post by tromp »

kazinator wrote: post #22
somewhereoutth wrote: post #9

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

Lisp gives you a programming language in which you don't have to write a cryptic 42 page one-liner to have an implementation of lambda calculus. Lisp gives you a way to talk about lambda calculus, in a way that executes. For instance, papers about lambda calculus may talk about "beta reduction" and things of that nature. Those concepts are not in lambda calculus; they are about lambda calculus. In lambda calculus exa…

> Lisp gives you a programming language in which you don't have to write a cryptic 42 page one-liner to have an implementation of lambda calculus.

You totally misunderstood what the 42 pages are. They are not an implementation of LC, but an implementation of LISP in LC.

> Lisp gives you a way to talk about lambda calculus, in a way that executes.

LC gives you that too; it allows you to encode lambda terms as bitstrings, which can be represented as lambda terms themselves.

> But lambda calculus doesn't explain what x is

In the binary encoding, x is a de-Bruijn index: a natural number indicating the nesting level of the binding lambda.

> Lisp closes the circle

So does Binary Lambda Calculus.

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

#54

Post by kazinator »

tromp wrote: post #47
kazinator wrote: post #24

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…

> LC has a great disadvantage: it's difficult to write a LC interpreter in LC. It's not; here it is quoted from [1]: (λ 1 1) (λ λ λ 1 (λ λ λ λ 3 (λ 5 (3 (λ 2 (3 (λ λ 3 (λ 1 2 3))) (4 (λ 4 (λ 3 1 (2 1)))))) (1 (2 (λ 1 2)) (λ 4 (λ 4 (λ 2 (1 4))) 5)))) (3 3) 2) (λ 1 ((λ 1 1) (λ 1 1))) > LC does not know what a LC expression is. Again, it's trivial to encode LC terms as bitstrings [1], which are trivially decoded back in…

> BLC requires translating bitstrings into lambda terms, to which the machine (itself a lambda term) can be readily applied.

I.e. a man behind the curtain is required to complete the "interpreter".

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

#55

Post by kazinator »

tromp wrote: post #49
kazinator wrote: post #37

Earlier quoted context omitted.

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…

You're claiming that LC cannot implement a quoting operator. Which is quite wrong. What you misunderstand is that a LC quote would not work on arbitrary lambda terms. A Mogensen quote operator would take a Mogensen encoding, and output a Mogensen encoding of that Mogensen encoding. Or a BLC quote operator would take a bitstring like 0010 which encodes the identity function λ 1, and output the blc encoding of the nil-…

> would take a Mogensen encoding

obtained where?

> output a Mogensen encoding of that Mogensen encoding

That's not what a quote operator does; it does precisely nothing, yielding the argument formula without evaluating it. No encoding-of-encoding. Just the encoding.

> output the blc encoding of the nil-terminated list of 4 booleans that represents that bitstring

Where/how does that become λ 1 again?

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

#56

Post by kazinator »

tromp wrote: post #53
kazinator wrote: post #22

Earlier quoted context omitted.

Lisp gives you a programming language in which you don't have to write a cryptic 42 page one-liner to have an implementation of lambda calculus. Lisp gives you a way to talk about lambda calculus, in a way that executes. For instance, papers about lambda calculus may talk about "beta reduction" and things of that nature. Those concepts are not in lambda calculus; they are about lambda calculus. In lambda calculus exa…

> Lisp gives you a programming language in which you don't have to write a cryptic 42 page one-liner to have an implementation of lambda calculus. You totally misunderstood what the 42 pages are. They are not an implementation of LC, but an implementation of LISP in LC. > Lisp gives you a way to talk about lambda calculus, in a way that executes. LC gives you that too; it allows you to encode lambda terms as bitstrin…

> You totally misunderstood what the 42 pages are.

There is a deliberate reversal of roles in my sentence that may not be obvious at a glance.

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

#57

Post by kazinator »

lisper wrote: post #46
kazinator wrote: post #24

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…

> it's difficult to write a LC interpreter in LC. Why? It's pretty easy to write Lisp in LC (a simple Lisp, not the feature-full version described in TFA) and it's pretty easy to write an LC interpreter in Lisp. I'll bet that an LC interpreter in LC could be done in only a few hundred lambda terms.

Good point; a minimal Lisp needed for processing LC doesn't require the 42 page formula. That has features like mutable global variables.

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

#58

Post by anderskaseorg »

kazinator wrote: post #37
anderskaseorg wrote: post #32

Earlier quoted context omitted.

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…

The situation with Lisp is exactly the same. To run a Lisp self-interpreter, we don’t pass it a Lisp function:

    (interpret (lambda (x) x))
but rather an encoded version of that Lisp function’s code:

    (interpret (cons 'lambda (cons (cons 'x nil) (cons 'x nil)))
Of course, Lisp gives us a more convenient syntax for the latter, in the form of the quote macro:

    (interpret (quote (lambda (x) x)))

    (interpret '(lambda (x) x))
But the quote macro is not a function; it’s just syntax. If it were a function, you’d expect this to be equivalent:

    (interpret
      (let ((f (lambda (x) x)))
        (quote f)))
which of course it is not.

Although the quote macro is an important part of what makes Lisp Lisp, it’s not a fundamental part of what makes Lisp a programming language. We could write any Lisp program without it (assuming we were still given a way to build a primitive 'symbol).

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

#59

Post by medo-bear »

lisper wrote: post #44
kazinator wrote: post #27

Earlier quoted context omitted.

The complexity topic from which we have P = NP is not actually about time, but number of steps. Of course that matters physically because if you only have a machine that performs one step at a time (or a somewhat better one that performs N steps at a time, for some fixed N), then the number of steps does translate to amount of time. If you have access to unlimited parallelism, then, for instance, some recursive algor…

> Of course that matters physically because if you only have a machine that performs one step at a time (or a somewhat better one that performs N steps at a time, for some fixed N), then the number of steps does translate to amount of time. It's much more fundamental than that. If you have any finite machine then the amount of time it takes to perform N steps will be proportional to N for sufficiently large N. > If y…

> Sorry to be the one to break this to you but you live in a finite universe

i don't think cosmologists make that claim in such a strong way. its mainly worded something along the lines of, "given our current understanding, its most likely to be finite"

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

#60

Post by tromp »

tromp wrote: 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…

> Writing in continuation-passing style also helps the lambda calculus interpreter to prevent re-evaluating the same term multiple times. This is very, very important and critical when writing programs for the 521-byte binary lambda calculus interpreters Blc, tromp and uni, since it seems that they lack a memoization feature, although they readily have a garbage collection feature.

Note that Melvin Zhang added a memoization feature (call-by-need evaluation with result sharing) in his refactoring [1] of my BLC interepreter.

[1] https://github.com/melvinzhang/binary-lambda-calculus

Post reply on HN