A visual introduction to tree calculus
Why is it useful? How does it work?
Tree calculus is a minimal, modular, Turing-complete and reflective calculus. The goal of this post is to convey this, quickly and intuitively. I strongly recommend reading Barry’s book, blog or recent paper to dig both more deeply and broadly!
One thing I love about tree calculus is that, while it is incredibly exciting to the theorist in me for pushing some technical boundaries, at the same time its specification is utterly compact and self-contained. That should make it very teachable. I tested this theory on my mom. After under 1h of me explaining and sketching things with pen and paper, she successfully rendered out the reductions of “not false → true” and “not true → false” and understood what’s going on. Whoa! Now, my mom is very smart, but she has never heard of λ-calculus, combinatory logic or term rewriting systems. And this still holds true now, because tree calculus can be explained — and used — without any Greek letters or parentheses. Because it’s all trees. Thanks for volunteering as my test subject, mom! ❤
Playing field and motivation
Before jumping into how tree calculus works, let’s talk about what kind of thing it is, and what it accomplishes. The real world is complicated, so computer scientists and software engineers alike love looking at things abstractly: Start from simple assumptions or standards and bootstrap complexity on top of it, layer by layer. The vast majority of people can swim in the top layers, producing powerful apps or science. Something like this:
Dig into the linked resources to learn exactly how and why, but the gist is: Tree calculus is minimal (note narrow, almost singularity-like “base” of the funnel), which makes it nice to reason about and trivial to run in any environment — including pen and paper. It can do more than λ-calculus natively (reflective, finite normal forms for recursive programs), which also reduces the distance between core calculus and high-level applications. Our website hosts a number of fully self-contained, interactive demos that aim to convey that.
Enough context, let’s get started!
Tree Calculus
Think of programs and values as unlabeled binary trees. Every node is either a leaf, stem (has one child) or fork (has two children).
Programs act on values. Tree calculus provides the rules for how a tree (program) applied to a tree (argument value) reduce into a new tree (result value). Programs are a kind of value, so programs can consume and produce programs as well.
Representing Data
If all values are unlabeled binary trees, we need to decide on ways to represent them. The reduction rules of tree calculus prescribe how to represent a certain program as a tree, but the choice is ours when it comes to representing “inert” data like numbers, lists, etc. How about:
Running Programs
In his 2021 book, Barry proposes a set of just three rules that describe how to reduce trees. In 2024, I suggested an alternative set of rules that seems to make some things more straightforward. This post and our website uses those latter rules, which we call triage calculus.
To visualize the rules that describe how a tree applied to a tree reduces to another tree, it is convenient to explicitly represent this “applied to” step as another kind of node. Let’s draw a hollow node:
Note that programs/values continue to only have one kind of node. The above is how we represent expressions that only become values upon reduction. Now here are the reduction rules:
It is left as an exercise for the reader to apply these rules to reduce “not true” (see previous picture) and “not false” with pen and paper.
Constructing Programs
From here, it is an engineering challenge to come up with the trees for increasingly useful and complex programs. For instance, here is a program that computes the size (number of nodes) of its argument. So applied to the “not” program from earlier, it returns 8. Applied to itself, it returns 180.
Our website hosts various more advanced demos, such as a program optimizer or programs that emit trees as programs in other languages. The trees constructed in these demos may be too large to render reasonably — but they are all just trees! The compiler that compiles the pseudo-language used by the interactive playground is a tree of size ~200k.
Conclusion
Hopefully this visual introduction conveyed an intuition about the motivation and workings of tree calculus. And hopefully you’re excited enough to follow all the links for a deep dive! Let’s revisit the attributes I promised in the very first sentence of this post:
- Minimal: Programs are trees, few reduction rules bootstrap everything.
- Modular: Programs can be composed into larger programs.
- Turing-complete: Tree calculus can model λ-calculus via rules 1 and 2.
- Reflective: Rules 3 allow reflecting on programs, e.g. to optimize them.
Appendix: An alternative way to think of expressions and reduction
This post visualized application explicitly, as a hollow node. I think this makes the distinction between reducible expression and value maximally clear. However, there is an alternative way to represent and think of reducible expressions, namely as non-binary trees. Starting with a binary tree that represents a program, we can attach arguments to it as new, right-most child trees. Then the reduction rules are about turning non-binary trees into binary trees:
Note that rules 0a-b become unnecesarry as they also just attach the argument to the program as a right-most child. Caution: In rule 3c (analogous for rule 3b and rule 2), what does it mean for “y” to be an arbitrary subtree, but also have children “u” and “v”? Again, the way to read this is that “u” and “v” attach as additional right-most children to “y”. That’s the way application is implicitly encoded here, compared to the explicit hollow node. Despite not needing rules 0a-b, I felt like this is a bit confusing. But let me know if you have a different impression!
Appendix: Implementation
If you are a software engineer, you’re probably thinking about implementing this in your favorite language or platform. Please don’t hesitate to reach out if you created something cool, I’m happy to link to it!
Check out the website for reference implementations. You will find the OCaml version implementing the rules exactly as visualized in this post, with function “apply” taking the role of the hollow node. The JavaScript version takes the alternative perspective introduced above: The reduction rules are implemented as mutating trees until they are binary. More mutation instead of allocation makes the garbage collector happy.
Appendix: Notation
Pictures don’t scale well to trees of massive size. Talking about them precisely benefits from some kind of notation or even pseudo-language. Barry fittingly chose Δ to denote tree nodes. The “not” program from earlier would be written as “Δ (Δ (Δ Δ) (Δ Δ Δ)) Δ”, with applications written just like is standard in λ-calculus or combinatory logic (left-associative). Check out Barry’s recent paper or our website for a formal specification and reduction rules using this notation.
For readability and brevity, it makes sense to then assign names to trees. For instance:
// If we define
not = Δ (Δ (Δ Δ) (Δ Δ Δ)) Δ
false = Δ
true = Δ Δ
// then we can say that
not true --> false
not false --> trueThe interactive playground on the website allows assigning names to trees just like this and provides additional syntactic sugar for convenience.
