Tree Calculus

by tosh • 4 months ago

115 35 4 months ago

timcobb• 3 months ago

I'm not used to math things being promoted like this (not to suggest that's a bad thing at all!). Can someone offer some context please.

seanhunter• 3 months ago

This isn't a math thing[1], it's a theoretical computing model (ie instead of a Turing machine or lambda calculus, you can use this instead) that you might study as part of studying computation theory or other bits of theoretical computer science.

[1] or not pure maths anyway. It's applied maths like all computer science.

froh• 3 months ago

is theoretical computer science (turing machines and automata theory, lambda calculus, complexity theory, computability, devidability, etc) pure maths? or applied maths indeed?

tree calculus is theoretical computer science for sure.

and that, computer science, in its beginnings at least, until the 1950s or so, was a field of mathematics, like algebra, or analysis or logic. all of which have pure maths parts and applied maths parts, don't they?

long story short, I don't think theoretical computer science is "applied maths", it to the contrary can be deep in pure maths land.

phlakaton2• 3 months ago

I think it might be a bad thing. I'm no stranger to math or computer science, but even after staring at the front page for a minute I was ready to dismiss this as the ravings of a lunatic.

It's like they had the idea of marketing this like a software project, not realizing that most front pages of software projects are utter bunk as well. It introduces terminology and syntax with no motivation or explanation.

Even once trying to get into "Quick Start" and "Specification" I was still mystified as to what it is or why I should want to play with it, or care. I had to go to the link mentioned upthread to get any sense of what this was or how it worked.

I think it's just badly written.

That being said, what seems to be proposed is a structure and calculus that are an alternative to lambda-calculus. The structures, as you can probably guess from the picture, are binary trees, ostensibly unlabeled except that there is significance to the ordering of the children. The calculus appears to be rules about how trees can be "reduced", and there is where the analogy to lambda calculus comes in.

Hopefully someone who actually knows this stuff can see whether I managed to get all that right – because I promise you, none of that understanding came from the website.

wordToDaBird• 3 months ago

Get good, IDK where you’re from but we don’t generally spoon feed here.

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

If you don’t understand what it does, it’s not for you. But if you don’t understand what it does, get good.

TLDR; what happens when a very small piece of js can be run in the browser or any environment and offer a meta programming layer, that is stupid simple, but also useful because it offers Turing completeness with reflection? Also, it’s site explains what it does, but you have to center on what it is doing. “Minimal” 20 lines of rust is the entire calculus. If you don’t know what Turing complete means get out. Similarly with reflective. Modular, look at the demos.

You flunked out of putting in an effort before spouting your mouth do try and actually be useful before you respond, there are those of us actually paying attention.

henearkr• 3 months ago

That makes me think of the Inca's quipus.

macintux2• 3 months ago

Extensive discussion (202 comments) about 15 months ago: https://news.ycombinator.com/item?id=42373437

eitally• 3 months ago

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

macintux2• 3 months ago

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

bawolff3• 3 months ago

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

robot-wrangler2• 3 months ago

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

BoiledCabbage3• 3 months ago

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...

afc• 3 months ago

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

tripplyons• 3 months ago

The reduction rules seem kind of arbitrary to me. At that point why don't you just use combinators instead of defining a set of 5 ways their operator can be used?

olydis• 3 months ago

A good point! From the “visual introduction” post mentioned elsewhere: Rules 1 and 2 seem arbitrary […], but behave analogous to the K and S operators of combinatory logic, which is sufficient to bootstrap λ-calculus. Rules 3a-c “triage” what happens next based on whether the argument tree is a leaf, stem or fork. This allows writing reflective programs.

See Barry’s post https://github.com/barry-jay-personal/blog/blob/main/2024-12... for more discussion.

gavinray• 3 months ago

This seems really up Stephen Wolframs alley.

He's really into the graphical representation of Turing machines and multiway Turing machines.

tombert• 3 months ago

Tangential, but I read his New Kind of Science book. It's an interesting book, but I found the first chapter to be pretty amusing.

The first chapter is so completely self-aggrandizing about how this book will change your life and the world and the entirety of science and mathematics and you should feel lucky for reading it.

The cellular automata stuff is pretty cool, but I don't feel like it lived up to the hype of the first chapter.

gram-hours• 3 months ago

Tree calculus is minimal, Turing-complete, reflective, modular

Ok. But what is it?

rhsjie294nd• 3 months ago

A lambda calculus variant Quite niche, so people who read about it know what a calculus is

steego3• 3 months ago

You can think of a calculus as a mathematical system one can use to define the essential computational basis for how a programming language or a runtime works mathematically.

Lambda calculus is often the foundation for functional programming languages, but lambda calculus is also a mathematical system you can calculate things with pencil and paper.

What makes lambda calculus interesting is it’s a relatively simple mathematical system where EVERYTHING is defined as a function. I’m serious. Imagine a programming language where you don’t have numbers, bools, if statements, while loops, gotos, etc.

You only have functions. All functions accept one argument (a function) and they always return functions.

Tree calculus is like lambda calculus, but it takes the idea a bit further. Not only can tree calculus do all this stuff where you create functions from other functions, tree calculus is fundamentally capable of reflecting on itself in a way that allows it to easily understand and transform its own interpreter.

In other words, if you base a programming language on tree calculus, your programming language or interpreter will allow you to create programs that can reflect on and transform other programs just like it was any other piece of data.

It’s pretty remarkable, especially when you find out how simple a core tree calculus based language can be implemented.

pgt3• 3 months ago

The inversion is really cool, e.g.

f = λa λb concat ["Hello ",a," ",b,"!"] f "Jane" "Doe" Hello Jane Doe!

then,

g = f "Admiral" invert g "Hello Admiral Alice!" Alice

pgt3• 3 months ago

@dang, pleaaase can we get proper markdown formatting on HN? I tried adding two spaces after each line, but I don't want paragraphs between code

lupire• 3 months ago

4 spaces indent

The inversion is really cool, e.g.

    > f = λa λb concat ["Hello ", a, " ", b, "!"] 
    > f "Jane" "Doe" 
    Hello Jane Doe!

then,

    > g = f "Admiral" 
    > invert g "Hello Admiral Alice!" 
    Alice

est• 3 months ago

wow this is amazing. There's an old Chinese proverb, 道生一，一生二，二生三，三生万物

The Tao giveth △ (false)

△ gives △ △ (true)

△(△, △) giveth rise to all things computable

(just kidding, I am totally lost to this)

layer8• 3 months ago

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.

BoiledCabbage3• 3 months ago

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".

BoiledCabbage3• 3 months ago

I'm actually going to reply to myself with my understanding of what's written here as the more I've looked at it, the cooler I think it is.

I happened to read this link [1], so that's what I'm basing it off of. Also note, I don't know this at all so I may be flat our wrong, but hopefully this gives someone a good intuition. I would recommend glancing at the image at the top of that link (https://olydis.medium.com/a-visual-introduction-to-tree-calc...) for reference to follow along with my interpretation.

To me it overall seems like similar to a lisp, but focused on binary trees. There are rules 0a, 0b, 1, 2, 3a, 3b, 3c. And the concept is actually pretty simple. Rules 0 are construction rules. Rules 1 & 2 are combinators. And rule 3 is pattern matching which allows for reflection / acting on the shape of code (according to the docs).

First I think of there are 3 main constructions (and via analogy I'll use lisp terms even though this clearly is not lisp and will not directly translate, but I think that will make communication easier rather than using unfamiliar terms).

Being a binary tree there are 3 main basic shapes. There is nil/false/empty that is represented by a single node. There is a "boxed expression" (a single root node with a left child) and there is a "paired expression" (a root node with left and right children). (in the diagram on the link w,x,y,z ... represent "unknown" expressions or maybe arguments if you want to think of them that way). '@' is used as the "apply" operator, but I'm going to call it "cons" even though it is not the "cons" from lisp.

Here is my view:

Construction Rules:

0a - If I cons false/nil with an unknown expression what do I get? i.e. what is "(cons 'nil z)", where z is an unknown expression? The answer is '(z) (or equivalently (z . 'nil)) What I'll call a boxed expression.

0b - If I cons a "boxed expression" with an unknown expression what do I get? What is "(cons (y . 'nil) 'nil) z)"? Answer: a boxed pair: (y . z).

1 - [Note this rule does double duty and starts a new pattern that's kinda cool]. So continuing the pattern, if I cons a boxed pair with an unknown expression (cons (x . y) z) what do I get? Well it depends on the shape of the boxed pair. Specifically what is the shape of x? If it's 'nil then apply rule 1. (cons ('nil . y) z) results in y.

Detour, it turns out (looking from the the perspective of the y and z, and 'cons' being a operator/combinator that this just happens to also be the 'K' combinator.

2 - So in this same boxed pair from above (cons (x . y) z), we said apply rule 1 if x is 'nil. But we've had consistent pattern (nil, boxed expr, paired expr) here so let's follow it now on the shape of x. So if x isn't 'nil, but is instead a boxed expression (x . 'nil) then use rule 2. Or to be explicit: (cons ((x . 'nil) . y) z) reduces to (cons (cons x z) (cons y z)). Here it is helpful to think of cons as "apply" as they define it and not my made-up 'cons', because then it's easy to see that this is the S combinator. Ie (apply (apply x z) (apply y z)).

3 - Ok so we have one stage left of our pattern for (cons (x . y) z). We said if x is 'nil you get rule 1. If x is a boxed expression, you get rule 2. And so if x is a paired expression, what do you get? Well you get a flavor of rule 3. Which flavor of rule 3? Well it depends on the shape of z. And if you've been following there are 3 choices for the shape of z. The same 3: nil, boxed expression and paired expression. You'll also note that this is the only time we have transformations depend on anything in z (the second argument to cons). Up until now z has always been a blackbox and had no affect on our rules -- the first arg to cons always decided what we did. If you think of z as the data argument to cons and the first arg to cons being the code, this is allowing the code we execute to structurally depend on the data/argument. Ie this is your functional pattern matching behavior. Again, thinking of 'cons' as 'apply' here helps.

So let's walk through them, but where we left off we said in (cons (x . y) z), x could be nil and we get rule 1. x could be a boxed expression and we get rule 2. And if x is a paired expression we get rule 3. So a paired expression replacing the unknown x above looks like (cons ((w . x) . y) z).

[A note you can skip: To be consistent with the image in the link I've reused the letter 'x', but the x in (cons ((w . x) . y) z) is not the x in (cons (x . y) z). The 'x' in (cons (x . y) z) is equivalent to (w . x) in the (cons ((w . x) . y) z). Think hygienic syntax replacement for my own convenience. You can also ignore this whole bracketed aside if it didn't make sense.]

Continuing rule 3, a paired expression replacing the unknown x above looks like (cons ((w . x) . y) z). Whether you apply rule 3a, 3b or 3c depends on the shape of the "argument" z. If z is nil (or a base case like 0), you get the fixed expression 'w'. If z is a boxed expression (u . 'nil), you get (cons x u), and if it's a paired expression (u . v) you get (cons (cons y u) v). Ignoring the details, it will conditionally apply the "code" w, x or y to the argument z, depending on the shape of z. In my view that is essentially equivalent to functional programming style pattern matching - they describe it as reflection.

Overall it's a pretty cool system. 3 "basic shapes". A few basic construction rules, 2 combinators and a case for pattern matching. In my view they have an operator that combines cons and apply in an elegant way, and can do pattern matching on it. It seems to really get to the essence of a lot of ideas in the space and very concisely without many assumptions or overhead. And note, while I specified, nil and cons and others, this all when serialized is represented by a single symbol with open and close parens for grouping. It's all just valueless binary trees.

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

steego3• 3 months ago

For people wondering what this is and whether to take this seriously, I’ll try to provide some context:

Tree Calculus is a novel alternative to lambda calculus as a minimal model of computation. Unlike most minimal systems, tree calculus is fundamentally capable of being fully reflective.

If you were ever interested in creating a programming language that could fully reflect and enhance itself with libraries, this is one of a very few number of known minimal system you can use as a starting point. Think of it as a lambda calculus with macros built into the underlying calculus, not something bolted on afterward based on a partially implemented meta-theory.

If you’re into formal proofs, you can find Rocq proofs of his work in his repo.

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

If you’re interested in how something like tree calculus can express a type system, here’s a recent ACM paper:

https://dl.acm.org/doi/pdf/10.1145/3704253.3706138

Personal context, Barry Jay is a respected academic and researcher who’s collaborated with people like Simon Peyton Jones and Eugenio Moggi. His PhD advisor was Joachim Lambek (from the Curry-Howard-Lambek correspondence). He’s not a random professor with a neat toy, Barry’s been working with many of the best minds on the foundations of computation long before most of us knew category theory existed. He’s been formalizing and defining pattern matching, higher-ordered patterns and has been searching/separating what is truly essential from what is not essential for decades.

Seriously, look at his research history on Google Scholar.

I think it will take the rest of us a while to understand and unpack the insight he’s already imbued into such a small and simple calculus.

barryjay• 3 months ago

Tree calculus is more expressive, can define more functions, than lambda calculus or traditional combinatory logic. This theorem is so startling, so outrageous, that mere proof, even a formal proof, is not enough to get the message across. This is no one’s fault. To help, I am currently writing a series of conversations, where the characters come at these ideas from many points of view, letting it all hang out. It doesn’t help that the current formal proof of the theorem is indirect. So here is a challenge for you all. Find a direct proof that the node operator of tree calculus is not definable in traditional combinatory logic. That is, no SK-combinator satisfies the equations of tree calculus. Conversely, trying to find such a combinator may give you a better feel for intensionality.

Tree Calculus

Related Stories