Much better intro article about tree calculus here, vs the actual site: https://olydis.medium.com/a-visual-introduction-to-tree-calc...
https://dl.acm.org/doi/pdf/10.1145/3704253.3706138
Tree Calculus is an alternative to lambda calculus that is capable of doing meta-theory without having to construct or bolt on something else entirely.
If lambda calculus provides a theoretical foundation for a language like Lisp. Tree calculus provides a theoretical foundation for a Lisp with a macro system that is fundamentally part of the core calculus.
You don’t have to write parsers and other stuff to do meta programming. It’s fundamentally built in and the paper I posted above explores how to construct type systems as a library, not as something that is outside of the runtime environment.
Here’s what’s really cool about it too: Just like lambda calculus, you can evaluate tree calculus with pencil and paper.
It’s very slick.
And yes, i know enough about computer science to know that making an axinomic system with a short grammar that has a proof that the halting problem is undecidable, isn't particularly note worthy by itself. I highly doubt the reason people are interested in this is just code golfing a proof of the undecidability of the halting problem
(define apply
(lambda (code data)
(match (code . data)
[('nil . z) (z . 'nil)] ; rule 0a - construct stem
[((y . 'nil) . z) (y . z)] ; rule 0b - construct fork
[('nil . y) . z) y] ; rule 1 - K combinator
[(((x . 'nil) . y) . z) (apply (apply x z) (apply y z))] ; rule 2 - S Combinator
[(((w . x) . y) . 'nil) w] ; rule 3a - pattern match case of data is leaf
[(((w . x) . y) . (u . 'nil)) (apply x u)] ; rule 3b - pattern match case of data is stem
[(((w . x) . y) . (u . v)) (apply (apply y u) v)] ; rule 3c - pattern match case of data is fork
)))