Tree calculus, visualized

10 Dec, 2024

Here are some drawings I made for myself to better understand how rewriting rules work in Tree Calculus, inspired by this helpful comment on HN.

NOTE: According to this comment, the author of Tree Calculus is Prof. Barry Jay, here's a link to his Tree Book.

Tree calculus works with binary trees, I draw them as black nodes and lines connecting them, with the root on top, and children below. Node with no children is called a Leaf, and I draw it as a black circle. Node with a single child is called a Stem, I draw it as a black triangle. Node with two children is called a Fork, I draw it as a black square. These binary trees can be arbitrarily deep.

There's a single operation that can be applied between two trees, denoted by this dashed arrow. I think of it as a "combine the left tree with the right tree", but in Tree Calculus it is essentially "apply a function that is the left tree to a single argument that is the right tree".

I use colorful shapes as "variables", they stand for "any kind of tree, we don't care what".

Here are the "reduction rules"

Rule (0a)

Rule (0b)

Rule (1)

Rule (2)

Rule (3a)

Rule (3b)

Rule (3c)

Encodings

Here is how the Tree Calculus's author encodes booleans (bits) and lists.

He encodes integers as lists of booleans — arbitrarily long lists of binary bits, starting from least significant. He encodes strings as lists of integers, each integer representing a Unicode code point.