De Bruijn notation, and why it's useful(blueberrywren.dev) |
De Bruijn notation, and why it's useful(blueberrywren.dev) |
Unrelated, but what would be your advice/study plan for a human to reach near perfect game play in Connect 4, and how difficult would it be?
[1] https://www.waterstones.com/book/the-complete-book-of-connec...
Similarly, it seems like languages with de Bruijn indices are immune to LLMs, since they require an internal stack/graph of sorts and don't reduce only on a textual basis.
i think large chain of thought LLMs (e.g. o3) might be able to manage
Is this a viable idea?
It employs a similar idea. Track the set of in scope variables and use them to unique variables on collision.
(\ a . a a) (\ x . \ y . x y)
Variables are uniquely named at parse time, but after one beta step, you have two distinct instances each of x and y, albeit in different scopes, and after a second beta step, you have two distinct variables named y in the same scope.
I've heard of this problem, but I've never really gotten why the solution in lambda calculus is to rename variables in lower scopes with overlapping names so that everything has a globally unique name. The way that programming languages usually solve this is by keeping a stack of symbol tables for scopes, right? Why is that never presented as a possible solution?
Of course, De Bruijn notation seems to sidestep that completely, which is convenient. I guess I'm just commenting on lambda calculus implementations in general.
Does it though? It's about the same amount of work as in renaming potentially conflicting variables (and more work than renaming actually conflicting variables). AFAIK, the main argument for them (by B. C. Pierce in his TAPL?) is that if you botch up the implementation of de Bruijn indices/levels, it will blow up in your face almost immediately, while the conventional renaming schemes may have subtle undetected bugs for months.
As for renaming, if you're going to be looking at every binding anyway, changing most of them is no big deal (unless of course that entails doing many deep copies)
Whilst a classic lambda expression like `λx.y` has three parts: the argument name `x`, the body/result `y`, and the `λ_._` syntax to distinguish it from a variable or application; if we instead use de Bruijn indices, then we don't need a separate part for the argument: all we need is a body wrapped in some distinguishing syntax (like `λy` in the article).
In Plumb, that distinguishing syntax is square brackets, so the "lambda term" `λy` would be written `[y]`. This wouldn't be possible if we had to write argument names, but ends up having some nice consequences:
- We can write this as-is in many languages, and the result is a data structure (usually a list) which we can easily walk over with an interpreter function.
- Variables are numbers, which can also be written as-is in many languages, and result in data that an interpreter function can handle.
- The final piece of syntax is applications, which necessarily has two parts (the function and the input value). Classic Lambda Calculus uses juxtaposition, whilst Plumb uses an explicit binary operator: the comma `,`. Again, commas can be written as-is in many languages, and they interact nicely with square bracket notation, (host language) function application, and (in the case of Python and Haskell) tuple notation.
The nice thing about using de Bruijn indexen, rather than de Bruijn "levels" or some other approaches to anonymous bindings (like those mentioned at the end of TFA), is that functions defined this way have an "intrinsic meaning"; e.g. `λ0` (or `[0]` in Plumb) is always the identity function; `λλλ(2 0 1)` (or `[[[2 , 0 , 1]]]` in Plumb) is always boolean NOT; etc. This lets us mix and match snippets of Plumb code with snippets of host-language code, embed each inside the other, and sprinkle around calls to an interpreter function willy-nilly, without worrying that the meaning depends on where our code ends up (e.g. at which "level" it reaches an interpreter).
Scrolling comments, I see somone else nentions this as well. I feel like this is something that got stuck in academia hell but in practice could be solved in more oractical ways. I remember various papers on fresh naming and name calculi from the 00's but why? We have a parser and we have numbers.
The reason I bring this up is because I recall it being easy to introduce bugs into de Bruijn calculi and also adding symbolic debugging to real-world languages was annoying for reasons I have no memory of.
* Note I said name not variable. (\ x . x (\x . x)) Would be (\ x#0 . x#0 (\x#1 . x#1)) similar to de Bruijn indices but could differ in other situations.
" What happens in the evaluator when you have
(\ a . a a) (\ x . \ y . x y)
Variables are uniquely named at parse time, but after one beta step, you have two distinct instances each of x and y, albeit in different scopes, and after a second beta step, you have two distinct variables named y in the same scope. "
This doesn't come up in most mainstream languages, but Zig and Jai are getting people excited about comptime evaluation, and dependent types need comptime evaluation as well. Uniqueness is fine until you're doing higher-order evaluation in your compilation pipeline like this, which will be more and more desirable in the future, at least if the current trends are any indication.
-->
(\ x#3 . \ y#4 . x#3 y#4)(\ x#5 . \ y#6 . x#5 y#6)
Code: http://t3x.org/clc/code.html
If you know Scheme, you almost don't need the book.
The Idris implementation also has a list of names in scope as an argument to the type of a Term, which makes the compiler (also Idris) check if you're making a mistake with your de Bruijn indices. (I did not do this in mine, but I should have.)
Edit: Oh, I see you mention reusing computations, that may be a bit more subtle. I'll have to look at your repo to see what you mean by that.
[1]: https://github.com/idris-lang/Idris2 [2]: https://github.com/dunhamsteve/newt
That's a perfectly fine way to implement this-or-that language (and is hence why many/most programming languages do it). However, it's not a valid solution in lambda calculus, since lambda calculus only has variables, lambdas or applications; there's literally no way to write down "a stack of symbol tables", or whathaveyou (note that you can implement such a thing using lambda calculus, but that would be more like an interpreter for some other language; "running" that implementation would still require a way to beta-reduce the "host" language in a capture-avoiding way)
Bad pseudocode:
function stepincrementgenerator(step) -> function (num) -> num + step
addsix = stepincrementgenerator(6)
addsix(5)
11
Note that lambda calc was invented ("defined") before the invention of the digital computer.
A big part of the value in the lambda calculus is in its aggressive simplicity meaning that you can do a bunch of theoretical work with relatively few concepts.
The less concepts and moving parts, the less proving necessary. And then you can layer on things and prove that they can also fit into your calculus.
I think most LC work _isn't_ about implementing something based on LC so much as providing theoretical foundations for your work being sound. And in that model you are likely going to focus on theoretical ease.
The expression λf.λx.f(f(fx)) for example is in normal form. The number 3 and the string "3" do not exist in the formalism, but at least some of the time, λf.λx.x is used to represent 0, λf.λx.fx to represent 1, λf.λx.f(fx) to represent 2, λf.λx.f(f(fx)) to represent 3, etc.
Again, lambda calc precedes the digital computer.
(\ a . a a) (\ x . \y . y x) => \ y . y (\ x . \ y' . y' x)
which still exhibits the variable shadowing problem.
In a good language (where "good" means the type system lets you do as much as you want to do while still being sound) you should be able to find some type for omega. The question is whether you can find the right type for omega to let us do what we want for this example.
Try the simple thing first:
w := (\ a : * -> * . a a) : (* -> *) -> * // works because (* -> *) is a subtype of *
Here is a bad thing you shouldn't be able to do with omega:
w w : untypable // thankfully, because (* -> *) -> * is not a subtype of * -> *
And here is a perfectly safe thing to do, which is exactly our example:
f := (\ x : * . \ y : * -> T . y x) : * -> (* -> T) -> T
w f : *
Unhappily such a weak type makes it pretty unusable within larger terms... So alternatively, we can try harder to find a good type for omega
w := (\ a : * -> (* -> T) -> T . a a) : (* -> (* -> T) -> T) -> (* -> T) -> T
w f : (* -> T) -> T // better!
Something similar would happen with the Y combinator. In a good language, there ought to be many valid types you can find for `\ f . (\ x . f x x) (\ x . f x x)` but not any that would permit you to construct a diverging computation with it.
A more limited form of perfect play is knowing how to win when playing first. I cannot do that either, but I suspect that I might be able to get close if I were to study hard on it for a year, trying to minimize the size of the opening book I need to keep in my head. The leaves of that book will then resemble the positions where Allis' rules apply so that you can work out further play on the fly.