Just spent a bunch of time with this and had a couple insights that might help (particularly if you have some familiarity with the lambda calculus or formal semantics and are trying to get a foothold on this):
- I had to go down to the OCaml implementation to work out what the small-step semantics were saying, in part because I couldn't see what the underlying tree structure was. In each of the four-element reductions in the definition, put parentheses around the first three to see what is applying to what. Also I think the right-hand sides are under-parenthesised. So:
(t (t) a) b -> a (1)
(t (t a) b) c -> (a c) (b c) (2)
(t (t a b) c) t -> a (3a)
(t (t a b) c) (t u) -> b u (3b)
(t (t a b) c) (t u v) -> (c u) v (3c)
Relatedly, the table is missing some cases because (I think) the authors see them as "obviously" falling out from the associativity of the written syntax, but I think it's helpful to add:
t a -> (t a) (0a)
(t a) b -> (t a b) (0b)
Now you can look at an expression with the syntax E E and more cleanly apply these semantic reductions to them.
- So wtf is all this doing? In the same way that working out the lambda calculus is frequently about bundling a lambda to "choose" between two options, this tree calculus is built to "choose" between three options based on whether it's presented with a node that is a leaf, a "stem" (one child), or a "fork" (two children). This is the core of rules 3a, 3b, 3c. If the "function" being applied is a fork whose left child is a fork, we think of the left-left grandchild as A, the left-right grandchild as B, and the right child as C; and if applied to a leaf, we use A, if applied to a stem we apply B to the stem's sole child, and if applied to a fork we apply C to the fork's two children. That three-way "choosing" is going to be how the system builds up the rest of the things you can do with it.
Thank you, this should have been on the front page.
That makes this a fun calculus, I guess, but isn't necessarily any more amenable to inversion (hard), serialisation (easy), or compilation (easy-ish) that something like SKI or lambda calculus already is.
Correct! The huge value add of TC is that it is also intensional, which SKI or LC are not. This is a property one is not commonly confronted with (which is a shame), but means that all the things you say (and more) can be defined right in TC. The crucial thing to see is that, while I can surely write a (say) program analysis for C in C, the analysis will have to work on a quoted version of programs! For instance a string, or AST. In TC, thanks to being intensional, you can do this directly. Concretely, say you had a function "add", in one line you can call "add 123 234", in the next line you can all "type_check add yadayada" to check its type. Or to serialize it. Or to compile it into x86.
To be very clear, there are other calculi and even programming languages that are intensional, TC is not first. But it is the most compact formulation, having just one combinator. And IMO the most practical, as I try to prove with the various demos on the website. E.g. I'd recommend looking at https://treecalcul.us/live/?example=demo-fusion which demos stream fusion. All demos are 100% self contained, in line 1 nothing but "t" is defined, and in less than 200 lines we have both a working program optimization and a little demo of it!
- I had to go down to the OCaml implementation to work out what the small-step semantics were saying, in part because I couldn't see what the underlying tree structure was. In each of the four-element reductions in the definition, put parentheses around the first three to see what is applying to what. Also I think the right-hand sides are under-parenthesised. So:
Relatedly, the table is missing some cases because (I think) the authors see them as "obviously" falling out from the associativity of the written syntax, but I think it's helpful to add: Now you can look at an expression with the syntax E E and more cleanly apply these semantic reductions to them.- So wtf is all this doing? In the same way that working out the lambda calculus is frequently about bundling a lambda to "choose" between two options, this tree calculus is built to "choose" between three options based on whether it's presented with a node that is a leaf, a "stem" (one child), or a "fork" (two children). This is the core of rules 3a, 3b, 3c. If the "function" being applied is a fork whose left child is a fork, we think of the left-left grandchild as A, the left-right grandchild as B, and the right child as C; and if applied to a leaf, we use A, if applied to a stem we apply B to the stem's sole child, and if applied to a fork we apply C to the fork's two children. That three-way "choosing" is going to be how the system builds up the rest of the things you can do with it.