For significantly more detail, discussion, examples and illustrations, read Reflective Programs in Tree Calculus by Barry Jay.

Definition: Tree calculus expressions $E$ have abstract syntax $E::=\mathrm{△}|EE$.

A note on notation: Parentheses are used to clarify structure, e.g. to distinguish $\mathrm{△}(\mathrm{△}\mathrm{△})$ from $(\mathrm{△}\mathrm{△})\mathrm{△}$. To reduce the number of parentheses required in practice, we assume that the binary operator $EE$ is left associative. For instance, $\mathrm{△}(\mathrm{△}\mathrm{△})\mathrm{△}\mathrm{△}$ means $((\mathrm{△}(\mathrm{△}\mathrm{△}))\mathrm{△})\mathrm{△}$. This convention is standard in combinatory logic and was already used by Moses Schönfinkel.

Expressions are reduced according to the following small-step semantics:

$$\begin{array}{rlrlrlrlrlrl}& \mathrm{△}& & \mathrm{△}& & a& & b& & ⟶a& & (1)\\ & \mathrm{△}& (& \mathrm{△}a)& & b& & c& & ⟶ac(bc)& & (2)\\ & \mathrm{△}& (& \mathrm{△}ab)& & c& & \mathrm{△}& & ⟶a& & (3a)\\ & \mathrm{△}& (& \mathrm{△}ab)& & c& (& \mathrm{△}u)& & ⟶bu& & (3b)\\ & \mathrm{△}& (& \mathrm{△}ab)& & c& (& \mathrm{△}uv)& & ⟶cuv& & (3c)\end{array}$$

Note: We call these particular reduction rules triage calculus. Johannes Bader suggested these as an alternative to the original rules, see Barry’s blog post for more context.

Conventions:

• We call irreducible expressions values or programs.
• We can think of expressions as unlabeled trees, generated by interpreting every subexpression $(\mathrm{△}arg\dots arg)$ as a node with $arg\dots arg$ as child trees.
  • We call expression $\mathrm{△}$ leaf.
  • We call expressions $\mathrm{△}a$ stem of $a$.
  • We call expressions $\mathrm{△}ab$ fork of $a$ and $b$.

Tip: Check out Timur Latypoff’s visualization of these rules and conventions. Thanks Timur!

Consequences:

• Values are binary trees, i.e. only consist of leafs, stems and forks. As long as there is a subexpression $(\mathrm{△}abc)$, one of the reduction rules apply.
• Tree Calculus is Turing complete: Reduction rules $1$ and $2$ are analogous to K and S operators of combinatory logic.
• Tree Calculus is intensional: Rules $3a\text{-}c$ allow reflecting on values by distinguishing leafs, stems and forks.
• Tree Calculus is confluent: The five reduction rules are non-overlapping and only allow observing values, not reducible expressions.

Example reduction: Negating booleans

If we define $\mathtt{\text{false}}=\mathrm{△}$, $\mathtt{\text{true}}=\mathrm{△}\mathrm{△}$ and $\mathtt{\text{not}}=\mathrm{△}(\mathrm{△}(\mathrm{△}\mathrm{△})(\mathrm{△}\mathrm{△}\mathrm{△}))\mathrm{△}$ then

$$\mathtt{\text{not}}\mathtt{\text{false}}\stackrel{\text{def}}{=}\mathrm{△}(\mathrm{△}(\mathrm{△}\mathrm{△})(\mathrm{△}\mathrm{△}\mathrm{△}))\mathrm{△}\mathrm{△}\stackrel{\text{3a}}{⟶}\mathrm{△}\mathrm{△}\stackrel{\text{def}}{=}\mathtt{\text{true}}$$

and

$$\mathtt{\text{not}}\mathtt{\text{true}}\stackrel{\text{def}}{=}\mathrm{△}(\mathrm{△}(\mathrm{△}\mathrm{△})(\mathrm{△}\mathrm{△}\mathrm{△}))\mathrm{△}(\mathrm{△}\mathrm{△})\stackrel{\text{3b}}{⟶}\mathrm{△}\mathrm{△}\mathrm{△}\mathrm{△}\stackrel{\text{1}}{⟶}\mathrm{△}\stackrel{\text{def}}{=}\mathtt{\text{false}}$$

The tree representation of $\mathtt{\text{not}}$ is