> 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.
This link below gives a better description of it, along with the definitions of the reduction rules. (which I got from further down in this thread)
But what I believe was meant by the above was: "delta E1 E1" creates a new "reduction tree" (my own made up term) with E1 being the left child of this new root node, and E2 being the right child of this new root node - and which then begins applying the reduction on this newly constructed tree.
https://olydis.medium.com/a-visual-introduction-to-tree-calc...
Overall the concept seems pretty interesting - and it's nice to see someone come up with something both novel in the space and at the same time seemly "applicable".