The reduction rules seem kind of arbitrary to me. At that point why don't you just use combinators instead of defining a set of 5 ways their operator can be used?
You can think of a calculus as a mathematical system one can use to define the essential computational basis for how a programming language or a runtime works mathematically.
Lambda calculus is often the foundation for functional programming languages, but lambda calculus is also a mathematical system you can calculate things with pencil and paper.
What makes lambda calculus interesting is it’s a relatively simple mathematical system where EVERYTHING is defined as a function. I’m serious. Imagine a programming language where you don’t have numbers, bools, if statements, while loops, gotos, etc.
You only have functions. All functions accept one argument (a function) and they always return functions.
Tree calculus is like lambda calculus, but it takes the idea a bit further. Not only can tree calculus do all this stuff where you create functions from other functions, tree calculus is fundamentally capable of reflecting on itself in a way that allows it to easily understand and transform its own interpreter.
In other words, if you base a programming language on tree calculus, your programming language or interpreter will allow you to create programs that can reflect on and transform other programs just like it was any other piece of data.
It’s pretty remarkable, especially when you find out how simple a core tree calculus based language can be implemented.
> the application of E1 to E2 attaches E2 to the root of E1 on the right.
It’s completely unclear to me what this means. The literal meaning is obviously wrong, because attaching a tree to a root that already has two child nodes would result in a ternary node, but apparently all trees in tree calculus are binary.
For people wondering what this is and whether to take this seriously, I’ll try to provide some context:
Tree Calculus is a novel alternative to lambda calculus as a minimal model of computation. Unlike most minimal systems, tree calculus is fundamentally capable of being fully reflective.
If you were ever interested in creating a programming language that could fully reflect and enhance itself with libraries, this is one of a very few number of known minimal system you can use as a starting point. Think of it as a lambda calculus with macros built into the underlying calculus, not something bolted on afterward based on a partially implemented meta-theory.
If you’re into formal proofs, you can find Rocq proofs of his work in his repo.
Personal context, Barry Jay is a respected academic and researcher who’s collaborated with people like Simon Peyton Jones and Eugenio Moggi. His PhD advisor was Joachim Lambek (from the Curry-Howard-Lambek correspondence). He’s not a random professor with a neat toy, Barry’s been working with many of the best minds on the foundations of computation long before most of us knew category theory existed. He’s been formalizing and defining pattern matching, higher-ordered patterns and has been searching/separating what is truly essential from what is not essential for decades.
Seriously, look at his research history on Google Scholar.
I think it will take the rest of us a while to understand and unpack the insight he’s already imbued into such a small and simple calculus.
Tree calculus is more expressive, can define more functions, than lambda calculus or traditional combinatory logic. This theorem is so startling, so outrageous, that mere proof, even a formal proof, is not enough to get the message across. This is no one’s fault. To help, I am currently writing a series of conversations, where the characters come at these ideas from many points of view, letting it all hang out. It doesn’t help that the current formal proof of the theorem is indirect. So here is a challenge for you all. Find a direct proof that the node operator of tree calculus is not definable in traditional
combinatory logic. That is, no SK-combinator satisfies the equations of tree calculus. Conversely, trying to find such a combinator may give you a better feel for intensionality.
14 comments
[ 1.7 ms ] story [ 85.4 ms ] threadHe's really into the graphical representation of Turing machines and multiway Turing machines.
Ok. But what is it?
Lambda calculus is often the foundation for functional programming languages, but lambda calculus is also a mathematical system you can calculate things with pencil and paper.
What makes lambda calculus interesting is it’s a relatively simple mathematical system where EVERYTHING is defined as a function. I’m serious. Imagine a programming language where you don’t have numbers, bools, if statements, while loops, gotos, etc.
You only have functions. All functions accept one argument (a function) and they always return functions.
Tree calculus is like lambda calculus, but it takes the idea a bit further. Not only can tree calculus do all this stuff where you create functions from other functions, tree calculus is fundamentally capable of reflecting on itself in a way that allows it to easily understand and transform its own interpreter.
In other words, if you base a programming language on tree calculus, your programming language or interpreter will allow you to create programs that can reflect on and transform other programs just like it was any other piece of data.
It’s pretty remarkable, especially when you find out how simple a core tree calculus based language can be implemented.
> f = λa λb concat ["Hello ",a," ",b,"!"] > f "Jane" "Doe" Hello Jane Doe!
then,
> g = f "Admiral" > invert g "Hello Admiral Alice!" Alice
The Tao giveth △ (false)
△ gives △ △ (true)
△(△, △) giveth rise to all things computable
(just kidding, I am totally lost to this)
It’s completely unclear to me what this means. The literal meaning is obviously wrong, because attaching a tree to a root that already has two child nodes would result in a ternary node, but apparently all trees in tree calculus are binary.
Tree Calculus is a novel alternative to lambda calculus as a minimal model of computation. Unlike most minimal systems, tree calculus is fundamentally capable of being fully reflective.
If you were ever interested in creating a programming language that could fully reflect and enhance itself with libraries, this is one of a very few number of known minimal system you can use as a starting point. Think of it as a lambda calculus with macros built into the underlying calculus, not something bolted on afterward based on a partially implemented meta-theory.
If you’re into formal proofs, you can find Rocq proofs of his work in his repo.
https://github.com/barry-jay-personal/tree-calculus
If you’re interested in how something like tree calculus can express a type system, here’s a recent ACM paper:
https://dl.acm.org/doi/pdf/10.1145/3704253.3706138
Personal context, Barry Jay is a respected academic and researcher who’s collaborated with people like Simon Peyton Jones and Eugenio Moggi. His PhD advisor was Joachim Lambek (from the Curry-Howard-Lambek correspondence). He’s not a random professor with a neat toy, Barry’s been working with many of the best minds on the foundations of computation long before most of us knew category theory existed. He’s been formalizing and defining pattern matching, higher-ordered patterns and has been searching/separating what is truly essential from what is not essential for decades.
Seriously, look at his research history on Google Scholar.
I think it will take the rest of us a while to understand and unpack the insight he’s already imbued into such a small and simple calculus.