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 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:
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 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
> 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.
Thank you for taking a look, and many thanks for your constructive comments. I found the BLC language and interpreter to be elegant and that was what brought me here.
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.
> 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)
> 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.
Yes but isn't it beautiful? But seriously, instead of seeing lots of brackets, see the whole as a texture, a texture that has some importance (per Lisp advocates). See it in context with other textures, indeed all possible textures.
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 because it's obvious (or at least it was obvious by 1958) how those primitives can be implemented as a mechanical process. Implementing LAMBDA in all its generality is far less obvious, which is why it took 20 years of further research to go from Lisp 1 to Scheme.
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 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).
> I would disagree that computation is process for doing math
Sorry, but you are mistaken. This is not a matter of opinion, it is a matter of historical fact. There is a reason that the title of McCarthy's original Lisp paper ends with "and Their Computation by Machine." The opening paragraph of Turing's 1936 paper ends with the sentence, "According to my definition, a number is computable if its decimal can be written down by a machine."
> specifically that for operating over a discrete state space.
Sorry, but you are mistaken about that too. Analog computers and quantum computers are computers but they do not operate over discrete state spaces. They are, however, machines.
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:
The only reason that P=NP? matters at all (let alone why it is a foundational question) is because the theory of computation concerns itself with what can be done with actual physical hardware in actual physical time.
> Per analog and quantum, indeed, and they are also mathematics.
No, they aren't. Analog computers are machines. Quantum computers are machines (or at least they will be if we ever actually manage to build one). We can describe the behavior of these machines mathematically, but that is not why they matter. They matter because we can actually build them.
> 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.”
I agree that much of the motivation comes from real world imperatives, but, for example, P=NP is of deep mathematical interest in its own right, and if/when mathematicians solve it, they will move on and let us sort out the details.
We can actually build stuff (beyond some somewhat blessed prototypes) often only when we've understood the mathematics behind it - edit: or is that the other way around??
I'm not sure that any rigorous discipline can consider itself outside or unbound by mathematics.
> P=NP is of deep mathematical interest in its own right
Sure. Computation and math are closely related, but they are not identical. Physics is described almost exclusively by differential equations, but differential equations and physics are nonetheless two distinct fields of study.
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 algorithms that completely process a tree structure can drop from linear time to logarithmic.
> 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 you have access to unlimited parallelism...
And if you had some magic pixie dust...
Sorry to be the one to break this to you but you live in a finite universe.
For sufficiently large N, all computation that isn't O(1) takes infinite time.
Complexity analysis goes out to infinity, but the way we use it as a tool is to inform us about what happens with our practical, finite inputs.
We know that something requires a non-polynomial number of steps, it quickly becomes untractable for small inputs. (So if we code that in a practical program, we need some justification that either the inputs won't occur, or we actively guard against them.)
Whether the entire universe is actually finite is not known, and not really relevant because that subset of it which is available to us as resources is vastly tiny.
The universe is vast, and vastly parallel: things are happening all over it at once, with more objects than have ever been crammed into any of our computing machines.
> 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.
> 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
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.
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.
Most mainstream Lisp dialects have some sort of structural pattern matching. Common Lisp has destructuring-bind, which is enough for avoiding car/cdr. Plus a number of advanced pattern matching libraries that are not just for matching lists.
> I find programming in Haskell much more pleasant.
Sure, but that misses the point. Some people like Java. Some like Perl. Some like C++. But, none of these languages come close to Lisp's ratio of utility vs size. So the fact that some people gravitate towards Haskell means nothing in and of itself. (Also, and I mean this with the utmost respect, your brain doesn't work like most people's brains.)
> Ben Lynn's awesome work [1] shows how minimal a Haskell implementation can be...
I'm not sure what you are referring to here. There are two links on that page. One is to an entry in the obfuscated C contest and the other is to Duet. The former is impressively small but, well, it is an entry in the obfuscated C contest and so it's pretty obfuscated. Duet is not obfuscated, but it doesn't seem to me to be particularly minimal. A minimal Lisp compiler can be both readable and an order of magnitude smaller.
> Using car/cdr feels rather primitive compared to pattern matching.
But adding pattern matching to Lisp is an elementary exercise and can be done at the user level. (And surely you knew that too.)
> Haskell, which is basically typed lambda calculus with syntactic sugar on top
Yes, but Haskell's syntactic sugar is significant for two reasons. First, it's not optional. You can put all sorts of fancy syntax on top of Lisp too, but you don't have to, and empirically, most Lisp programmers try this once early in their careers and come to realize that it is a bad idea, that working directly in the AST is weird at first but that it is actually much more productive in the long run. In Haskell there is no AST exposed to the user so this is not an option. There is one syntax and you're stuck with it. And second, Haskell's syntax not well designed IMHO. I am not a particularly skilled coder, but I have worked in a lot of different languages and I find Haskell borderline impenetrable.
BTW, this is a tangent, but I feel the need to say this since you brought up pattern matching: IMHO, if you are using pattern matching in real-world code, you are doing something wrong. Pattern-matching is a way to impose some discipline on punning cons cells to hold structured data, but punning cons cells is a fundamental mistake. If you have structured data, that data should be contained in structures, not cons cells.
(The only exception to this rule is a macro expander, where you have no choice but to deal with cons cells because that is what is handed to you by the reader. But if you are writing a lot of macro expanders then that too is an indication that you are doing something wrong.)
I agree with everything you wrote, except: adding pattern matching that hits even the lower rungs of good quality is sweating bullets. (So good thing users of Lisps don't have to.)
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 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)
and so on. That's a nested list. It contains symbols. We can use an assoc list to associate symbols with the terms that are their values. And so on ...
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.
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))
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.
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).
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 "lambda") ...) to remove quote. Oops, now you're using a different kind of quote: a string literal quote. If you remove that, you will have character literals to otherwise build the symbol name.
I agree that quote is not essential: take out quote and you can still do useful symbolic processing. Just doing interactive testing and writing unit tests will be inconvenient, mainly.
The requirement for quote has a different effect. 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 actually the same thing that (quote lambda) produces or that (intern "lambda") produces.
The above is almost inescapable if user-defined macros are supported. When code is read, it is not determined at read time what is a macro and what isn't. Therefore it is not known what parts of the form may need to be passed to a user-defined expander function without having been evaluated (and thus in the quote representation). The whole thing is in the quoted encoding, so that quote doesn't have to do anything other than pass through its interior.
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 actually the same thing that (quote lambda) produces or that (intern "lambda") produces.
I’m not sure what you’re suggesting here. Certainly the number (+ 2 2) must be distinguishable from the list '(+ 2 2). Even lambda expressions must be distinguishable from their quoted encodings, because otherwise lexical scoping breaks. If you make (lambda () x) equivalent to '(lambda () x), then this breaks:
match is nothing but a macro; application code could supply an equivalent, depending only on what is publicly documented.
Syntactically, the variable terms in (@x @y) are in the same category. Yet x is interpreted by the pattern matcher as a bound variable, whose value matches the corresponding object; whereas y is interpreted as a free variable to be lexically bound to the corresponding object.
You just need a macro system with environment parameters, and a defined API into them.
With help from the macro system, we could write an interpreter such that (let ((a 1) (b 2)) (interpret '(list a b))) will yield (1 2). interpret can't be a function; it has to be a macro which analyzes the argument for variables and creates a bridge between those variables and the surrounding lexicals at the point where interpret finds itself. The interpret macro transforms the code somehow and then hands it to an interpreter function.
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.
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.
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-terminated list of 4 booleans that represents that bitstring:
> 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
> An evaluated term can be evaluated again, yielding something different.
Yes, and a Mogensen-Scott encoding can be Mogensen-Scott-encoded again, requiring two rounds of decoding, and so on.
Multiple rounds of encoding and evaluation seem inescapable of you have the entanglement of homoiconicity.
The quote operator in Lisp is designed exactly right.
In mathematics there are literals like the number 3 or the set {}. These objects stand for themselves and are not understood as requiring any calculation: they just are.
Symbols like x do not stand for themselves. If you want to talk about x literally as the symbol object, it is inescapable that there is some quoting operator to indicate that the usual semantics of x denoting something else do not apply. (Oxford's A Dictionary of Computer Science has a definition of literal which acknowledges this very issue.)
Literals being constants, it means that when they are concretely implemented in a computer, in the best possible way, they do nothing other than trivially reproduce a canned value that already exists before the program starts.
What's so special about "literals"? They must be symbols in the sense that they can be evaluated. The fact that you've defined them so that they evaluate to something indistinguishable from the unevaluated form is neat, but it doesn't seem to me fundamental. We could have a lisp where you aren't allowed to evaluate a raw number, it would just be a little more awkward.
Again, it's trivial to encode LC terms as bitstrings [1], which are trivially decoded back into lambda terms. That is exactly what the above lambda expression does. Alternatively, you can encode LC terms with Mogensen's encoding, but that one doesn't give you a textual representation like a bitstring.
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.
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 to be counted as part of the interpreter's implementation, which means that it's not in LC any more.
Based on that, I think it's not actually possible without extensions to LC.
You need to be able to read the syntax with the lambda symbols and names (or integer constants in the case of De Bruin), so I/O is needed. Or else, if that is unacceptable, you need to be able to embed the representation of the code as a quoted literal.
Without I/O or quoting, you have no way to express the test cases.
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 "characters", where lists can be encoded using the Scott encoding, and characters can be encoded as a list of bits, and "bits" can be encoded as 0=\x.\y.x, 1=\x.\y.y. This I/O strategy is used in LambdaLisp as well, and is explained in my post in [1].
How Lisp terms are encoded as lambda terms in LambaLisp is explained in [2].
To implement a LC interpreter instead of a Lisp interpreter in LC, it then remains to somehow encode and quote a lambda calculus term into a lambda calculus term. The function described by tromp's reply in this thread, called the Universal Machine, does this - it does so by using an encoding called the binary lambda calculus (BLC) notation for encoding lambda terms into lambda terms. In this notation, an arbitrary lambda term in the usual plaintext notation such as \x.\y.\z.(x y z) can be encoded into a bitstream. The converse is also always possible. The Universal Machine uses the BLC notation for expressing lambda terms, with the same 0/1 bit encoding and list encoding mentioned earlier, and outputs a bitstream (encoded as lambda terms) representing the evaluation result. The BLC notation is described in my post in [3].
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.
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.
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.
Yeah, I should have realized that. In fact, I had seen your BLC interpreter some time ago but for some reason it didn't come to mind as I was writing that. I must be getting old.
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!
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 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.
Beta reduction is in fact the essence of LC - without it all you'd have is a nice tree.
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?
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.
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.
Maybe I am stupid but what's the point in reimplementing lisp in lambda? Just to prove how beautiful simple lambda calculus is? The lambda functionality is allready in lisp. And lisp is beautiful simple!
() is nothing and (is something)
What does the implementation show more beautiful than that?
Binary Lambda Calculus is indeed beautifully simple [1].
LISP is rather complex by comparison, but then it's full-fledged non-esoteric programming language.
This is undoubtedly cool, but I'd be really impressed if it wasn't stupidly slow. (I'm not saying it is stupidly slow, because I haven't had a chance to run it, just that I'd be impressed if it wasn't.)
Thanks for your feedback, I forgot to mention the execution speed in the post. The number guessing game example (44 lines long) in the Usage section actually runs with an instantaneous response time on the terminal. I added some remarks on the execution speed.
I haven't tried it either, but I would not bet my life savings on it being slow. I tried something similar to this a few years ago (see my top-level comment for a pointer) and was amazed at how fast it turned out to be.
Ah but this is where it becomes interesting! Because we can then guage how much work this abstraction is doing for us - and indeed whether or not it might stray from the 'one true path' (whatever that might be)
"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:
https://flownet.com/ron/lambda-calculus.html