[eitally]

Much better intro article about tree calculus here, vs the actual site: https://olydis.medium.com/a-visual-introduction-to-tree-calc...

[macintux]

Another resource I found in HN discussions: https://latypoff.com/tree-calculus-visualized/

[afc]

This is indeed much better. I couldn't really follow the original, but this one made it click. Pretty cool!

[bawolff]

I feel like neither of these just give actual formal definitions, which would be much clearer.

[robot-wrangler]

https://github.com/barry-jay-personal/tree-calculus/blob/mas...

[bawolff]

Surely there is a middle ground between a book length treatment and whatever the linked page was that fails to give a definition or motivation.

[steego]

This introduction to this paper explains the motivation:

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.

[robot-wrangler]

My friend this ain't memes or celebrity news, it's theoretical computer science. You'll get out of it roughly what you're ready to put into it. If you're short on time, the grammar is like 5 characters and the proof of the halting problem isn't much bigger. If you don't already know why that is interesting though you really might have to read a bit to find out

[bawolff]

That's my complaint, this page is essentially a meme.

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

[BoiledCabbage]

I believe this to be correct, where code and data are arguments consisting of binary trees constructed from pairs or can be 'nil:

    (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
         )))

https://olydis.medium.com/a-visual-introduction-to-tree-calc...