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

61–70 of 101 posts

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

#61

Post by bidirectional »

kazinator wrote: post #54
tromp wrote: post #47

Earlier quoted context omitted.

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

Can you explain at a high level what you think a valid LC-in-LC interpreter looks like then? Because it's very hard to understand what your objection is to the examples in this thread.

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

#62

Post by tromp »

kazinator wrote: post #55
tromp wrote: post #49

Earlier quoted context omitted.

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?

> That's not what a quote operator does; it does precisely nothing,

This is what gives Lisp murky semantics; you need something (quote) to do nothing, while having nothing (no quote) does something (evaluate).

Lisp lacks referential transparency, even without the use of variables. An evaluated term can be evaluated again, yielding something different.

> Where/how does that become λ 1 again?

By decoding it, which is what mostly what the LC self-interpreter does, as detailed on pages 6,7 of [1].

[1] https://tromp.github.io/cl/LC.pdf

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

#63

Post by wrbs »

quickthrower2 wrote: post #31
sudosysgen wrote: post #26

Earlier quoted context omitted.

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

There's nothing about the lambda calculus which forces you to use the church encoding of natural numbers.

You could also come up with an encoding based on booleans as bits:

  {true} = \t f. t
  {false} = \t f. f
then bytes:

  {0b00001111} = \f. f [false] [false] [false] [false] [true] [true] [true] [true]
which you could merge up into larger integers just like real computers.

or for one less based on the 8-bits and to keep the infinite range you could just represent integers as lists of binary numbers:

  {[]} = \c n. n
  {x::y} = \c n. c x y

  {0} = []
  {1} = [true]
  {2} = [false, true] (i.e. reversed 0b10)
  {3} = [true, true]
  {4} = [false, false, true]
which you could imagine using to implement a way more efficient shift-and-add multiply, O(log M * log N)

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

#64

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…

> The pattern \lambda a. \lambda b. \lambda w. \lambda x. \lambda y. yλa.λb.λw.λx.λy.y is noticable in many places in lambdalisp.pdf, since isnil is used a lot of times in LambdaLisp.

Sadly, this heavy use of the isnil operator derived in section [1] adds a lot of unnecessary verbosity, since instead of writing

    isnil list
      result1
      (let { head = car list, tail = cdr list} in result2)
one can simply write

    list
      (\head \tail \_ . result2)
      result1
[1] https://woodrush.github.io/blog/lambdalisp.html#deriving-isn...

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

#65

Post by tromp »

wrbs wrote: post #63
quickthrower2 wrote: post #31

Earlier quoted context omitted.

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

There's nothing about the lambda calculus which forces you to use the church encoding of natural numbers. You could also come up with an encoding based on booleans as bits: {true} = \t f. t {false} = \t f. f then bytes: {0b00001111} = \f. f [false] [false] [false] [false] [true] [true] [true] [true] which you could merge up into larger integers just like real computers. or for one less based on the 8-bits and to keep…

> {[]} = \c n. n

> {x::y} = \c n. c x y

Note that Binary Lambda Calculus uses the simpler {x::y} = \c. c x y, which allows you to operate on a list l with

    l (\head \tail \dummy. non_null_case) null_case

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

#66

Post by keithalewis »

lisper wrote: post #39
keithalewis wrote: post #35

Earlier quoted context omitted.

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.

You missed the substantive portion of the post.

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

#67

Post by haskellandchill »

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

Then what is System F?

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

#68

Post by haskellandchill »

tromp wrote: post #48
lisper wrote: post #46

Earlier quoted context omitted.

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

> an LC interpreter in LC could be done in only a few hundred lambda terms. Make that a few dozen...

lisper and kazinator need to put down the keyboard and spare some time for reflection. thanks tromp for your tireless efforts at education. big fan of your work!

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

#69

Post by lisper »

tromp wrote: post #51
lisper wrote: 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…

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

Yes, that is why I said sufficient and not necessary. The reason CONS/CAR/CDR/COND matter is not because they are necessary. That they are not necessary was known long before 1958. The reason they matter is that they are a better impedance match to human cognition than LC. People can actually write useful programs in Lisp. Very few people can write useful code in LC. Lisp matters because it is a local maximum on the ratio of real-world utility to the size of the formalism.

[UPDATE] One idea I've been kicking around for a long time but have not yet acted on is to explore using abstract associative maps as a primitive and see how far that gets you. I suspect this would be a significant win in terms of comprehensibility of code. The foundational axiom would be something like:

((amap k1 v2 k2 v2 ... kn vn ...) kn) == vn

So IF, for example, can be written as (amap true [then] false [else]), CONS is (amap car [left] cdr [right]), etc.

Or something like that.

Oh, yeah, Lisp also introduced symbols as first-class entities. That's a big win.

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

#70

Post by lisper »

pmcjones wrote: post #34
lisper wrote: 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…

> 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

Thanks for that link! TIL.
Post reply on HN