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?)
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 basically a rewrite engine, so I'm not sure it would be so hard to implement? Probably some plastic bags, in two colours, paper scraps, and a marker pen would do it? (Edit - one colour bag would need 2 ordered compartments - or if you really have lots of spare time you could build it all with just plain bags and some set theory) However as you say perhaps Lisp is a better abstraction over the Turing tape (yuck).
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
> 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.
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 what that is, but they are not executable.
In Lisp we can say, okay, lambda calculus can be represented sort of like this:
(lambda (x) x)
Lisp has the programmatic vocabulary to talk about lambda calculus formally, in a way that is executable.
I don't suspect there is a significantly easier way for LC to interpret LC than to use the 42 page expression to create a Lisp, and then write the interpreter in that lisp.
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 examples you have terms like \x x and whatnot. But lambda calculus doesn't explain what x is; x is an identifier and that is part of the description of lambda calculus, and not in lambda calculus.
Lisp has the batteries included for describing languages, such as lambda calculus. It has an answer for what is x: it's a symbol, available as a data type. It has an answer for what is "beta reduction"; it's a function you can write, and execute on some piece of lambda calculus.
Lisp closes the circle; the stuff you talk about in a paper can become code, and code which is not far from what the paper talks about.
The beauty and generality of LC is that x doesn't need an explanation, it is just a placeholder, yet that is enough to define interesting (perhaps all) things.
Lisp is an abstraction, that per article can be built upon the deeper abstraction of LC - question is, what does it give us in terms of expressiveness and understanding?
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.
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.
I'd suggest that code-as-data is in fact not a functional concept, and indeed may not necessarily be as helpful as we might like to think.
Lisp strayed from the path somewhat when it embarked on runtime enclosure (if my understanding is correct), and anyway it was never going to be as elegant as a true rewrite system.
"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:
it's the theoretical basis for ML and Haskell.
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
That's hardly a fair comparison. LambdaLisp includes a ton of features that BLC and BF do not.
I was unaware of the nil-test-free method for Scott-encoded lists. It's true that it would remove a lot of bits from LambdaLisp's implementation. I'll also be using this for future projects. I was also unaware of Melvin Zhang's interpreter. I suspect that result sharing would improve the execution speed. I'll try to add that in one of the supported interpreters in the repository. Thank you very much for thoroughly reading my post and pointing these facts out. It has deepened my understanding and interest for binary lambda calculus.
I also want to say that Lazy K is one of my all-time favorite languages, as I mentioned in the post. It was about 10 years ago when I first found out about Lazy K - at that time I wrote a blog post about a language I made that directly transpiles to Lazy K (written in Japanese). Although at that time I couldn't fully grasp the language, I'm happy that now I could write large programs for Lazy K. I was thrilled to find that the Lazy K language proposal was now published on your website.
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)
list
(\head \tail \_ . result2)
result1
Note that Melvin Zhang added a memoization feature (call-by-need evaluation with result sharing) in his refactoring [1] of my BLC interepreter.
Elsewhere, Douglas Adams smiles.
() is nothing and (is something) What does the implementation show more beautiful than that?
Page 33:
>(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((...
Yeah that seems about right.