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

81–90 of 101 posts

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

#81

Post by lisper »

medo-bear wrote: post #59
lisper wrote: post #44

Earlier quoted context omitted.

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

"You live in a finite universe" is not the same as "the universe is finite". You live in a light cone, and unless you are immortal that light cone comprises a finite amount of space-time.

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

#82

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

A quote operator that doesn't work on arbitrary lambda terms is not correct. It doesn't meet the definition of quoting.

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

#83

Post by kazinator »

anderskaseorg wrote: post #80
kazinator wrote: post #74

Earlier quoted context omitted.

> The situation with Lisp is exactly the same. No it isn't, because the Lisp code is already understood to have an encoding. So we don't have to play any Gödel-numbering-like games to get the code to be able to talk about code. That battery is included. > gives us a more convenient syntax for the latter, in the form of the quote macro The ' in (cons 'lambda ...) is an instance of quote! You must write (cons (intern "…

Yes, I was clear above that I know ' means quote. My experiment is to compare Lisp to a restriction of Lisp where quote only works on symbols. This restriction doesn’t make it any harder to write a self-interpreter. > If we have quote, we can make the additional step in the documentation that all code has the representation produced by quote, even when quote is not being used. When lambda is seen in code, that is act…

If we don't have quote for expressions but only for symbols, we can still write the interpreter function, and give it a test case by writing an expression which calculates the code that we want to interpret. Even without quote the language has given us a representation of the syntax that we can rely on.

We have it as a given that (list 'lambda (list 'x) 'x) produces (lambda (x) x).

We do not have such a thing in lambda calculus. We could create an extended lambda calculus which has it.

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

#84

Post by anderskaseorg »

kazinator wrote: post #83
anderskaseorg wrote: post #80

Earlier quoted context omitted.

Yes, I was clear above that I know ' means quote. My experiment is to compare Lisp to a restriction of Lisp where quote only works on symbols. This restriction doesn’t make it any harder to write a self-interpreter. > If we have quote, we can make the additional step in the documentation that all code has the representation produced by quote, even when quote is not being used. When lambda is seen in code, that is act…

If we don't have quote for expressions but only for symbols, we can still write the interpreter function, and give it a test case by writing an expression which calculates the code that we want to interpret. Even without quote the language has given us a representation of the syntax that we can rely on. We have it as a given that (list 'lambda (list 'x) 'x) produces (lambda (x) x). We do not have such a thing in lamb…

The sense in which the Lisp code (list 'lambda (list 'x) x) evaluates to the data representation of (lambda (x) x) is exactly the same as the sense in which the lambda calculus code λa. λb. λc. c (λx. λa. λb. λc. a x) evaluates to the data representation of λx. x.

What makes Lisp special is that this particular correspondence is made visible to the programmer via quote and other macros. Again, very cool, but not fundamental to this particular discussion.

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

#85

Post by kazinator »

woodrush wrote: post #79
kazinator wrote: post #78

Earlier quoted context omitted.

A LC interpreter (whether in LC or anything else) has to process the actual syntax with the lambdas and symbols (or integer literals, in the case of De Bruin). If it is necessary to translate that representation to something else, the interpreter must do that itself. You can take a LC expression and write some other LC expression which encodes it; but if that is done outside of LC in some meta-language, then that has…

The basic tools required for implementing a LC interpreter in LC is demonstrated in LambdaLisp. Although LambdaLisp implements Lisp, the same tools can be used to implement a LC interpreter in LC. The largest concern in question here may be how I/O is done. I/O can be done by viewing a lambda term as a function that takes a string as an input and outputs a string. Here, a "string" can be expressed as a "list" of "cha…

Statements like "IO can be done [in lambda calculus] by ..." really mean "lambda calculus doesn't have IO but can be extended by ...".

Here's what it means to have an LC in LC interpreter. Firstly pick what LC means. Choose a representation for it. Exactly one. Show that this is lambda calculus with no extensions. Then show how an embedded expression of this can be interpreted.

For instance supposed we have a lambda calculus which is based on a three letters M I and U. Spaces are insignificant.

Say that MUIMUIMMU is a valid expression. Then a self-interpreting situation might look like this:

  IMUMIUMM...MUI MUIMUIMMU UMI
The to-be-interpreted expression appears embedded. I set it off with spaces for clarity. It is not translated into any different representation. The surrounding material represents the interpreter. There needn't be an epilogue piece after the embedded expression. Important: no part of this interpreter depends on the embedded expression. We can swap in arbitrary other expressions without changing the interpreter; will correctly interpret those expressions.

I am skeptical that this is possible with standard, unextended lambda calculus, whether regular or de Bruin.

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

#86

Post by quickthrower2 »

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…

Yeah I made huge assumptions!

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

#87

Post by kazinator »

kazinator wrote: post #85
woodrush wrote: post #79

Earlier quoted context omitted.

The basic tools required for implementing a LC interpreter in LC is demonstrated in LambdaLisp. Although LambdaLisp implements Lisp, the same tools can be used to implement a LC interpreter in LC. The largest concern in question here may be how I/O is done. I/O can be done by viewing a lambda term as a function that takes a string as an input and outputs a string. Here, a "string" can be expressed as a "list" of "cha…

Statements like "IO can be done [in lambda calculus] by ..." really mean "lambda calculus doesn't have IO but can be extended by ...". Here's what it means to have an LC in LC interpreter. Firstly pick what LC means. Choose a representation for it. Exactly one. Show that this is lambda calculus with no extensions. Then show how an embedded expression of this can be interpreted. For instance supposed we have a lambda…

Under these rules, an identity function can serve as an interpreter. This is valid. Empty text (nothing wrapped around the input case) is also an instance of interpretation. The question is, can it be achieved without just throwing the expression into the path of the host evaluator in these kinds of ways.

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

#88

Post by medo-bear »

lisper wrote: post #81
medo-bear wrote: post #59

Earlier quoted context omitted.

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

"You live in a finite universe" is not the same as "the universe is finite". You live in a light cone, and unless you are immortal that light cone comprises a finite amount of space-time.

> "You live in a finite universe" is not the same as "the universe is finite".

it is if the word 'universe' designates the same thing. otherwise what you want to say is "your experience of the universe is finite"

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

#89

Post by lisper »

medo-bear wrote: post #88
lisper wrote: post #81

Earlier quoted context omitted.

"You live in a finite universe" is not the same as "the universe is finite". You live in a light cone, and unless you are immortal that light cone comprises a finite amount of space-time.

> "You live in a finite universe" is not the same as "the universe is finite". it is if the word 'universe' designates the same thing. otherwise what you want to say is "your experience of the universe is finite"

OK, whatever. The point is you cannot possibly access unlimited parallelism.

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

#90

Post by tromp »

lisper wrote: post #69
tromp wrote: post #51

Earlier quoted context omitted.

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…

> People can actually write useful programs in Lisp.

I find programming in Haskell much more pleasant. Using car/cdr feels rather primitive compared to pattern matching.

> Lisp matters because it is a local maximum on the ratio of real-world utility to the size of the formalism.

I feel that role is better served by Haskell, which is basically typed lambda calculus with syntactic sugar on top.

Ben Lynn's awesome work [1] shows how minimal a Haskell implementation can be...

[1] https://crypto.stanford.edu/~blynn/compiler/

Post reply on HN