Tree Calculus

by iamwil • 2 years ago

493 184 2 years ago

I think this is really cool. It's at least shaped like something really cool. But I need to have my hand held a little bit more than this page is set up for. Is there like a... for dummies version?

cat5e• 2 years ago

Straight up dude. Can we get an explanation for the rest of us?

hollerith2• 2 years ago

If it turns out to be broadly useful (to working programmers) I'm sure someone will write up a better explanation.

At its current state of development, it might be more appropriate for the blog "Lambda the Ultimate" than HN.

lolinder6• 2 years ago

It's a very funny way to structure the main landing page—it takes cues from trendy programming language and framework websites (single word headings that feel slightly buzzwordy, animated code samples, etc), but then the text body is in quite overwhelmingly dense and lengthy academic language, but then it doesn't actually provide enough details in the academic language to really understand what is going on.

I spent a while parsing the paragraphs in the hope of understanding what this is, only to discover that in spite of its verbosity the text on the landing page is no more informative than PL landing pages usually are—it tells you a lot about what the author thinks is great about the language while not actually explaining how any of it works. I guess I need to go to the specification for that?

__MatrixMan__3• 2 years ago

it tells you a lot about what the author thinks is great about the language

I did not get so far as to understand that it was a language. I thought maybe it was some kind of higher order function to be implemented in a language of your closing. Like a map/reduce sort of thing.

scrubs• 2 years ago

Agreed!

almostgotcaught2• 2 years ago

people are always so impressed by this kind of stuff but i'll never get why. doesn't your intuition already lead you to recognize what's going on? or do you recognize and are still impressed?

look if it walks like an expression tree, talks like an expression tree, and quacks like... something else... then it's basically an expression tree with extra sugar and spice. that doesn't mean the sugar and spice isn't fun, it means the basic idea is exactly what you think it is - expression trees (plus in this case enough semantics to define combinators).

bertylicious2• 2 years ago

I'm very much impressed with this. I have never seen a programming language that allowed me to de/serialize functions. Let alone calculate the inverse of a function. If you're saying one or more languages with these features already exist then I'm very interested in names, links or references.

theogravity• 2 years ago

Thanks for writing what I was afraid to post.

tkgally• 2 years ago

A defining sentence at the top of the page, something like “Tree Calculus is a [noun phrase] for [summary of purpose],” would be helpful. Wikipedia articles typically begin with such sentences:

“Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution.”

“In mathematics, matrix calculus is a specialized notation for doing multivariable calculus, especially over spaces of matrices.”

“The felicific calculus is an algorithm formulated by utilitarian philosopher Jeremy Bentham (1748–1832) for calculating the degree or amount of pleasure that a specific action is likely to induce.”

justinpombrio3• 2 years ago

Quick summary:

It's a programming language whose programs (and whose values) are unlabeled trees.

An unlabeled tree is a tree-shaped data structure whose nodes hold no data. The children of a node are ordered, though. The "Tree Calculus" defines a set of rules by which you can "evaluate" an unlabeled tree to get another unlabeled tree. If you apply these rules repeatedly, either you'll get into an infinite loop, or you'll get a tree that the rules say doesn't change anymore. The rules are designed so that the rules don't effect binary trees, so if you evaluate a binary tree you'll get the same tree back out and the computation is "done". These rules are written as a small-step semantics (a standard way to write down evaluation rules in PL) in the "specifications" page.

They claim that:

- The evaluation rules for trees are Turing Complete, meaning that you can express any computation, e.g. any JS program, using the Tree Calculus. More precisely, the claim is that there's a straightforward way to convert any (say) JS Program into a tree, and any tree into a JS value, and now you can use tree evaluation to run a JS program by doing (i) convert the JS program into a tree, (ii) evaluate the tree to get another tree, and finally (iii) convert the tree into a JS value, which is the correct output of the JS program. To prove this you wouldn't actually use JS as the language, you'd use something simpler that we already know is Turing complete like the lambda calculus, but it's the same idea. Though glancing at the page they might have actually done this for JS.

- The evaluation is asymptotically optimal, meaning that for any programming language P (like JS), there's a conversion f(prog) from programs in P to Tree Calculus trees and constants a and b such that running_time(f(prog)) <= a+b*running_time(prog). That is, you can run programs in any language using the Tree Calculus with ~constant overhead. This is true for all the programming languages you love, e.g. you could write a JS program that takes a Java program, compiles it to bytecode, and run that bytecode, and unless you did this reasonably badly the running time won't be worse than a factor of 1,000,000.

- A whole bunch of other stuff too. It's all plausible at first glance (i.e., I don't think they're making any of it up), but not obviously consequential.

What's it good for:

Some PL people might think it's cool. Conceivably useful to simplify some theory of computation proofs.

If you find this sort of thing interesting, though, I'd recommend learning the lambda calculus instead. The lambda calculus is simpler, more well known, and more useful (it's a model of functions, instead of some made up rules about trees).

junon• 2 years ago

Thank you for this, way more digestible.

So if it's just an unlabeled tree (nodes hold no data) then the only information is the child order / count, correct? So part of it is somehow mapping some high level information to combination of nodes and children, and back (after some manipulation), correct? Or am I misunderstanding everything?

lolinder6• 2 years ago

If you find this sort of thing interesting, though, I'd recommend learning the lambda calculus instead. The lambda calculus is simpler, more well known, and more useful (it's a model of functions, instead of some made up rules about trees).

I was with you all the way up until here.

The lambda calculus is only more useful because it's become the basis for a lot of existing programming languages. Its made up rules are no more fundamental than the made-up rules of any other calculus, tree calculus included. They just seem more fundamental because they form the basis of most functional programming today.

I'm also unconvinced that the lambda calculus itself is meaningfully simpler. It typically has three syntactic components and two reduction operations, compared to one syntactic component and five reduction operations—that gives the lambda calculus a very small edge in moving parts, but it's very small.

The only way in which I could agree with you is that learning the lambda calculus first is going to be easier because there's so much more material on it. But that's not because the fundamental properties of the lambda calculus, it's because Church came first.

ufo• 2 years ago

I'd recommend learning the lambda calculus instead

Not to mention, it'll be hard to understand what's going on here without some peevious experience with lambda calculus and combinators (SKI, etc)

chriswarbo7• 2 years ago

The lambda calculus is simpler, more well known, and more useful (it's a model of functions, instead of some made up rules about trees).

Lambda calculus is actually quite tricky; e.g. I've implemented it many times over the decades, both for fun and for serious applications, and have still never properly implemented capture-avoiding substitution (I've tried, but usually give up and reach for an existing implementation).

Also, notice that the tree calculus reduction rules are confluent, disjoint and branch on their left subtrees (similar to SK calculus). Hence they are also a "model of functions" like lambda calculus; or, alternatively, lambda calculus is also "some made up rules about [expression] trees".

ryandv6• 2 years ago

It's a stripped down model of computation like the SKI calculus [0] or its cousin the lambda calculus, which are formal systems with precise rules for mechanically evaluating or reducing expressions.

It differs from the SKI calculus in that it can reflect on its own program structure, especially in ways the SKI calculus cannot - deciding if two programs are equal, for instance [1]. Further, unlike the lambda calculus, reducing a program with the reduction rules given [2] eventually converges upon a stable "normal form" of the program, which is expressed in irreducible terms, instead of leading to possibly infinite chains of reduction [3]. This allows for reflection without needing to "quote" or serialize the program into a stable data structure or other representation to sidestep the possibility of infinite reduction. This is similar to the notion of homoiconicity as in Lisp.

[0] https://en.wikipedia.org/wiki/SKI_combinator_calculus

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

[2] https://treecalcul.us/specification/

[3] https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....

cjfd• 2 years ago

"reducing a program with the reduction rules given eventually converges upon a stable "normal form" of the program".

How is that possible if the reduction rules define a Turing complete language?

__MatrixMan__3• 2 years ago

Thanks for the links, I'll be reading up on these.

When I signed up for a computer science degree, I was hoping I'd learn this stuff (if not this calculus, than enough context to grapple with it at least). What I actually got was software engineering. Snore.

Skeime• 2 years ago

I will also try to give some explanation:

The specification says that the syntax of expressions in this thing is `E ::= t | E E`. This is a bit confusing, because it might lead you to believe that all expressions just look like `t t t t t t t`. In reality, you are supposed to keep the implied bracketing, so expressions really look like `(t t) (t ((t t) (t t)))` (note that at the top level and in each parenthesis, there always exactly two subexpressions). Essentially, the space character becomes a binary operator (similar to how we often write multiplication with no symbol).

The expressions are a bit heavy on parentheses, so we say that this binary operator is left associative. This means that an expression `a b c` should be interpreted as `(a b) c`, an expression `a b c d` should be interpreted as `((a b) c) d`, and so on. If you think about it, this means that you can always get rid of an opening parenthesis at the left edge of an expression, i.e. we can assume that an expression always start without one.

With this out of the way, we can now understand where the trees come from: As there is only one terminal symbol, `t`, after removing unnecessary parentheses, every expression will always start with `t`, which is followed by a number of other expressions. To draw this as a tree, draw a node representing the initial `t`, and a sub-tree for each of the follow-up expressions (by applying the same procedure to them).

In this view, the semantic rules at the top of the specification page now tell you how to "simplify" a tree whenever there is a node with three or more sub-trees, or alternatively, how to reduce an expression that is a `t` followed by three or more sub-expressions. (In the syntax view, you replace the `t` and the first three expressions following it by whats on the right of the arrow. In the tree view, you replace the node and its first three children by some other sub-tree, then you attach the remaining children to the root of the new sub-tree.)

Exuma• 2 years ago

Great extra detail - thanks

mojomark• 2 years ago

Sorry, I don't understand what I just saw.

e-dant• 2 years ago

Feels like clojure from afar

revskill• 2 years ago

This is simpler to undrestand than clojure.

ks2048• 2 years ago

I'm not sure that's true since most of the top-level comments here are saying they don't understand it.

Vampiero2• 2 years ago

On paper, it's really cool and I hope that more comes out of it. In practice, I'm not sure that taking 9k eval steps to turn a string lowercase is viable for anything.

bertylicious2• 2 years ago

This depends a lot on what an eval step actually is. Could you give us an example or a reference to compare it to?

oersted• 2 years ago

But you can make any arbitrary compiler within the language itself to reduce certain patterns to fast native instructions. It’s interesting as a universal Intermediate Representation.

Vampiero2• 2 years ago

Damn, that's true. I keep coming back to this thread hoping for more insight because the idea is very pretty.

adastra226• 2 years ago

Can someone explain how this is not Lisp with a different syntax? Or Forth?

I don’t mean that as a criticism or midwit dismissal. Just want to understand.

casey22• 2 years ago

Lisp is based on lambda calculus which has no tools to modify programs written in itself, this is apparently a useful feature, so there are many lisp-like languages with added macros as such there are many different implementations of these features. Even something as prevalent in lisp-likes as eval isn't part of lambda calculus, which only has abstraction application and variables (no env). If the notion of reflection is well defined and if tree calculus is reflective then it's definitely not just lisp (certainly not forth) with a different syntax

I'm no expert so take this post with a mountain of salt. Without confusing the issue: In practice it's just a slow lisp, in theory it's different from lambda calculus and can be used to implement that slow lisp-like in a simpler way.

adastra226• 2 years ago

Lambda abstraction (which is used by this “tree calculus”) is a form of quotation.

Nit picky point: quote/eval is an integral part of Lisp, not a later addon.

medo-bear• 2 years ago

Lisp is based on lambda calculus which has no tools to modify programs written in itself

Lisp is not based on lambda calculus and lisp can certainly modify programs written in itself

https://www.reddit.com/r/lisp/comments/e467tk/is_it_more_cor...

psychoslave• 2 years ago

If it doesn't have mandatory parentheses around and indentation sensitivity, that's already a huge plus for people with my taste.

It's fine other people have different tastes really. I'm just sad that homoiconicity is mostly trapped within lisp dialects.

maxbond4• 2 years ago

Reminds me of Modal.

https://wiki.xxiivv.com/site/modal

https://wryl.tech/projects/modal.html

chewxy• 2 years ago

Barry Jay's got an upcoming paper at PEPM regarding typed tree calculus. Good read too.

agnishom4• 2 years ago

I googled that, and I found that it is a sister conference of POPL: https://popl25.sigplan.org/details/pepm-2025-papers/5/Typed-...

I was inclined to think that Barry Jay is some kind of crackpot

justosophy2• 2 years ago

See the Coq proofs in https://github.com/barry-jay-personal/tree-calculus/ for the pre-typed tree content as well.

vincentpants• 2 years ago

So wait. How is this not a lisp? And consider that a compliment, we need more lisp in our lives.

ryandv6• 2 years ago

Immediately I'm reminded of the SKI calculus as an extremely minimal model for computation [0].

Edit: in fact, they even define the SKI combinators in their demonstration of Turing completeness, so I wonder how the tree calculus differs aside from being based on only a single combinator.

[0] https://en.wikipedia.org/wiki/SKI_combinator_calculus

[1] https://treecalcul.us/live/?example=demo-turing-intensional

gatane2• 2 years ago

Your example reminds me of Binary Lambda Calculus [0]:

[0] https://tromp.github.io/cl/Binary_lambda_calculus.html

casey22• 2 years ago

The point of tree calculus as I understand is that all programs are valid data structures, so they can be modified and analyzed during runtime with nothing but other programs.

adastra226• 2 years ago

That is also true of Lisp. And Forth. And a dozen other homoiconic languages.

sitkack• 2 years ago

An Architecture for Combinator Graph Reduction (TIGRE) https://users.ece.cmu.edu/~koopman/tigre/index.html

xigoi• 2 years ago

The difference seems to be that tree-calculus is intensional – you can distinguish different trees within the language even if they have the same computational value.

tromp5• 2 years ago

It's not based on a single combinator. It's based on the two standard basis combinators S and K, and a non-combinator that can inspect normalized terms to distinguish between degrees 0,1,and 2.

quchen2• 2 years ago

A combinator is just a term without free variables. All the rules can be put as combinators, it’s just that they don’t have common names like SKICB(…).

alan-crowe2• 2 years ago

As far as I understand it so far, the idea that the trees are "unlabeled" over simplifies.

The most common kind of binary tree is defined as

binary-tree = nil | node of binary-tree label binary-tree

for example

empty-tree

node nil Alice nil

node nil Bob (node nil Carol nil)

node (node nil David nil) Edward (node nil Fred nil)

node (node nil George nil) Harold nil

If we erase the labels, there remains an implicit label Alice = 00, Bob = 01, Carol = 00, David = 00, Edward = 11, Fred = 00, George = 00, Harold = 10 encoded by the pattern of empty trees.

The trees in the article seem to be doing it slightly differently, with implicit labels 0,1, or 2. Edward is erased, leaving an implicit 2 and the erasure of both Bob and Harold leaves an implicit 1 for both of them, removing the distinction between 01 and 10.

Edited to add: I'm up to page 27 (pdf reader says page 39 of 176) and some nodes have three children. 0, 1, or 2 children represent "values". "It follows that trees containing a node with three of more branches is a computation that is not a value, and so must be evaluated."

gatane2• 2 years ago

This is like a weird child between Lisp/Forth and Prolog (?). I do think it is neat tho, got me thinking on how you could implement it and parse it.

Thanks for the inspiration!

nixosbestos• 2 years ago

Oof. I thought I had a grip on my ADHD but these non-seekable, side-by-side demos are giving me whiplash.

EDIT: oh no, oh god, they are text, so maybe Asciinema, so, we're light-years ahead of a GIF/mp4, but also, please don't disable the seekbar, come on.

:/ Even worse, they don't scroll. They don't need to be animated at all. Come on frontend people, just stop. Please, just... stop.

EDIT2: I have zero idea what "stream fusion" is and the 4 inscrutable paragraphs of text don't explain it either. But maybe I'm just a dumb and don't know what that is.

Jtsummers3• 2 years ago

Stream fusion is a fancier version of the concept of loop fusion: https://en.wikipedia.org/wiki/Loop_fission_and_fusion

At a high level and skipping details, suppose you want to do something like this:

  (filter predicate (map f sequence))

Naively, this is two linear passes over the data. Fusion would allow you to combine these into one single linear pass.

This has particular uses when there are intermediate, temporary allocations that can be eliminated, it's not just about time performance.

Come on frontend people, just stop. Please, just... stop.

I suspect this is part of why you're getting downvoted. This site seems to be a bit of a gag in its presentation. It's over-the-top on purpose.

adastra226• 2 years ago

This is more typically called lazy evaluation.

doall• 2 years ago

Is that something like Transducers in Clojure?

cyberax• 2 years ago

Reminds me of Refal, which is somewhat surprisingly Turing-complete.

LudwigNagasena• 2 years ago

So it’s based on a universal combinator like Iota?

Jtsummers3• 2 years ago

Yes. And the author is Johannes Bader who wrote about that one as well:

https://lambada.pages.dev

https://johannes-bader.com

tromp5• 2 years ago

No, it's based on K and S, as is clear from the two rules

    (t (t) a)     b       -> a           (1)
    (t (t a) b)   c       -> (a c) (b c) (2)

blahedo2• 2 years ago

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.

tomsmeding• 2 years ago

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.

olydis10• 2 years ago

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!

Trung02462• 2 years ago

Interesting, I tried to convert Z combinator in SKI to this using the lambda calculus example then print out the tree. Untested:

    z = (t (t (t t (t (t (t (t (t t (t (t (t (t (t t)) (t t))) (t (t (t t)) (t t))))) (t (t (t t (t (t (t t (t (t (t t t)) t))) (t t)))) (t (t (t t (t (t (t (t (t t)) (t t)))))) (t t))))) (t t (t (t (t (t (t t))))))))) (t (t (t (t (t t (t (t (t (t (t t (t (t (t t (t (t (t t t)) t))) (t t)))) (t (t (t t t)) t))) (t t (t t))))) (t (t (t t (t (t (t (t (t t (t (t (t t (t (t (t t t)) t))) (t t)))) (t (t (t t t)) t))) (t t (t t))))) (t (t (t t (t (t (t t t)) t))) (t t))))) (t t (t (t (t (t (t t (t (t (t (t (t t)) (t t))) (t (t (t t)) (t t))))) (t (t (t t (t (t (t t (t (t (t t t)) t))) (t t)))) (t (t (t t (t (t (t (t (t t)) (t t)))))) (t t))))) (t t (t (t (t t (t (t (t (t (t t (t (t (t (t (t t (t (t (t t (t (t (t t t)) t))) (t t)))) (t (t (t t t)) t))) (t t (t t))))) (t (t (t t (t (t (t (t (t t (t (t (t t (t (t (t t t)) t))) (t t)))) (t (t (t t t)) t))) (t t (t t))))) (t (t (t t (t (t (t (t (t t)) (t t)))))) (t t)))))))) (t t)))))))

Original tested but unoptimized and also converted using tool:

    var K = a => b => a;
    var S = a => b => c => a(c)(b(c));
    var Z = S(K(S(S(K(S(S(K)(K))(S(K)(K))))(S(K(S(K(S))(K)))(S(K(S(S(K)(K))))(K))))(K(S(S(K))))))(S(S(K(S(S(K(S(K(S))(K)))(S))(K(K))))(S(K(S(S(K(S(K(S))(K)))(S))(K(K))))(S(K(S))(K))))(K(S(S(K(S(S(K)(K))(S(K)(K))))(S(K(S(K(S))(K)))(S(K(S(S(K)(K))))(K))))(K(S(K(S(S(K(S(S(K(S(K(S))(K)))(S))(K(K))))(S(K(S(S(K(S(K(S))(K)))(S))(K(K))))(S(K(S(S(K)(K))))(K))))))(K))))));

https://en.wikipedia.org/wiki/Fixed-point_combinator

october81402• 2 years ago

This code is so easy to read.

idle_zealot• 2 years ago

Yeah, I think I'm going to take the author's advice and use Tree Calculus to generate JSON config files. That way I won't need to use a bloated tool with a JSON parser just to output configuration.

ktm5j• 2 years ago

No kidding.. I didn't think parenthesis hell could get worse than Lisp

scotty792• 2 years ago

It's equivalent to binary machine code for a procesor with 5 opcodes.

Why would it be readable?

tromp5• 2 years ago

Z = \f. (\x. f (\v. x x v)) (\x. f (\v. x x v)) can be much simpler, namely S (S (K (S S (K (S (S K K) (S K K))))) K) (S (K (S S (K (S (S K K) (S K K))))) K)

Trung02462• 2 years ago

If you means that it would be like this:

    var Z = S(S(K(S(S)(K(S(S(K)(K))(S(K)(K))))))(K))(S(K(S(S)(K(S(S(K)(K))(S(K)(K))))))(K));

Unfortunately not works with the `count_fn` function from the wikipedia page :(, `too much recursion`.

galaxyLogic2• 2 years ago

So a given function would be reprsented by an unlabeled tree, and its result calculated by applying rules which transform the source-tree into a binary tree?

Then how do I "call" such a tree with some specific arguments? Do I have to create a new tree that represents both the function, and the arguments it is called with?

How do I represent numbers, and strings, and arrays?

ryandv6• 2 years ago

Presumably you could implement Church numerals [0] or something similar in the tree calculus.

[0] https://en.wikipedia.org/wiki/Church_encoding

blahedo2• 2 years ago

Timur Latypoff's page (elsewhere in this thread but also: https://latypoff.com/tree-calculus-visualized/ ) shows a graphical view of this; you get to lists first—easy because tree structure is native here—and then a (natural) number is just a list of booleans, of arbitrary length, least significant first. Very elegant.

quchen2• 2 years ago

The specification talks about numbers, strings, lists.

The playground has concrete, runnable (bash, JS) examples.

agnishom4• 2 years ago

The homepage says "Democratizing Functions" and "Democratizing Metatheory". Whatever that means, I have a strong feeling that this is an abuse of the word "democraztizing"

falcor842• 2 years ago

This usage is quite common; it's the second definition on Britannica: "to make (something) available to all people : to make it possible for all people to understand (something)"

https://www.britannica.com/dictionary/democratize

skrebbel2• 2 years ago

Yeah but functions are available to all people. I mean, it's an abstract mathematical concept. When you find a 30% discount sticker on an item in a store and compute in your head what the resulting price is going to be, you're arguably applying a function.

Also, to say that this makes functions available to all people, and to immediately follow that with text such as "The reduction rules act on trees of higher degree, until they are binary" suggests that well, actually, this is only for PL gurus, not all people (and that's totally fine IMO, just don't use the word "democratizing")

xpe2• 2 years ago

Yes, it is a fact the definition exists on Brittanica. This is a positive thing, not a normative value.

But we, together, also shape how words are used. Just because someone uses a word doesn’t mean we have to like it or accept the context. We certainly don’t have to blindly repeat it.

We all put this into practice. We choose to reinforce patterns we find useful. And ignore ones we don’t.

We don’t need to disempower ourselves by acting like we have no power over language.

As for me, I would rather democratize mean something meaningful. So when someone uses it for self-interested purposes, I try to call it out.

I’m not a stickler for no reason. It is because I care — the world is still only marginally and fleetingly democratic. I don’t want marketing speak to ooze into yet another domain. Instead, I want such efforts to cause eye-rolls and backpressure.

But, yes, I will grant the printing press “democratized” books. And the Internet “democratized” information. These kinds of societal breakthrough are worthy of the word. It also so happens that such broad empowerings mutually reinforce democracy.

agnishom4• 2 years ago

In this case, they are not really democratizing metatheory. Am I understanding metatheory any better now?

I do not know what it would even mean to democratize functions. Functions just are. Can you democratize the number 5?

xpe2• 2 years ago

I agree. See: “What democratize really means”

https://intage.us/articles/words/democratize/

Remember, language is shaped by culture, and you are part of that culture. You do not have to abdicate responsibility. You have options.

visarga2• 2 years ago

This is a good counterexample to "syntax is not sufficient for semantics". It is sufficient when there is no distinction between data and code. Code can reflect on itself as data. Like bootstrapped autocompilers, Godel's Arithmetization or neural nets. In all cases syntax is both data and behavior, it is deep, self reflective and self generative.

mrkeen3• 2 years ago

This is a good counterexample to "syntax is not sufficient for semantics"

Perhaps I'm misunderstanding. At the top of https://treecalcul.us/specification/ it shows 5 lines of small-step semantics. If you threw these away, could you recover them from the syntax?

visarga2• 2 years ago

syntax becomes semantics after sufficient iterative updates in the environment

october81402• 2 years ago

Is everyone upvoting this just pretending to understand what it is?

mykowebhn2• 2 years ago

Not I, but I upvoted you for telling it how it is.

mykowebhn2• 2 years ago

Darnit, I upvoted. Guilty

hoseja• 2 years ago

We ARE on YCombinator here, after all. And there are lambdas there. Good enough?

bjackman• 2 years ago

It's democratisating metatheory! What's not to understand?

RossBencina• 2 years ago

I upvoted in the hope someone would explain it to me.

jeltz• 2 years ago

I think so. To me it seems like yet another implementation of lambda calculus with a poorly made webpage which does not explain why it is interesting.

magicalhippo• 2 years ago

This is one of those articles which I hoped would generate an interesting discussion, and hence I upvoted it on that basis.

desperate• 2 years ago

Same. Pretty much upvoted because I didn't understand but wanted to, and thought other people might be able to provide more insight.

golol• 2 years ago

Lambda calculus consists pretty much just of function compositions, which in principle have a tree structure. Is this just lambda calculus in a dress?

tromp5• 2 years ago

Close, but not quite; it's combinatory logic plus introspection in a tree dress.

ranma_42• 2 years ago

The idea might be nice but the syntax is so easy to mess up for humans that in the spec itself the author gets the translation of `not true` wrong (maybe a copy-paste from `not false`?).

Should be "t (t (t t) (t t t)) t (t t)".

gilleain• 2 years ago

Agreed, as someone who spent far too long writing out tree-like expressions similar to this, it's very easy to get them wrong. Of course an editor with bracket-matching will _help_ but not to get the subtrees correct.

('signatures', in case you were wondering)

marsknight• 2 years ago

I'm too dumb for this

ethernot• 2 years ago

I've got a mathematics degree and I can't work it out either if that's any consolation.

GistNoesis2• 2 years ago

I think the main problem people encounter understanding this thing is just parsing the expression tree for the rules.

It isn't stated but all trees in question are binary trees.

Even though the expression tree syntax is really easy E := t | E E

The mental gymnastic needed to visualize that the string

not = t ( t (t t) (t t t)) t correspond to the only tree drawn in https://treecalcul.us/specification/

is quite overwhelming.

The left-associative notation to remove unneeded parenthesis makes it even harder.

It could be explained so much better if the author made the 10 pictures corresponding to the transformation rules of the trees. Eventually highlighting the subtrees a, b, c, in the corresponding color before after.

Brains are used to pattern matching images but not abstractly defined syntax unless you have been trained in grammar theory.

justosophy2• 2 years ago

Tree Calculus is awesome with implications beyond this website.

Shame the website doesn't attribute the creator and author Prof. Barry Jay. (Seems to be a pattern for them sadly, not sure why)

See Jay's book on GitHub for more https://github.com/barry-jay-personal/tree-calculus/blob/mas...

al-king• 2 years ago

Oh cool, his Bondi Language / Pattern Calculus was the first thing I thought of seeing this, so I guess I wasn't too far wrong.

olydis10• 2 years ago

Note that it refers to his book on the "Specification" page :)

Seems to be a pattern for them sadly, not sure why

Can you elaborate? Agreed I could (and will) attribute more explicitly on the website, but the intention is in no way to grab credit. I just posted this reply for more background on everything: https://news.ycombinator.com/item?id=42375914

sulam• 2 years ago

English is likely not your first language and it’s fairly obvious what you mean, but the word you’re using a lot is spelled “intention”. Not at all how it sounds, stupid English.

(It’s also likely that this minor error is spawned by the use of intension, a very uncommon word, in the description of Tree Calculus.)

p4bl0• 2 years ago

On the semantics page the reductions presented in the definition are not the same thing as the OCaml code does. Or if it is actually equivalent, it should be largely commented because it really is not obvious.

But this criticism is valid for most of the website. Nothing is really clear.

kevindamm• 2 years ago

This strikes me as a good idea in the same way that counting in unary is a good idea.

Theoretically profound but ultimately needing to be somewhat removed from its application to be of much practical use.

nlitened4• 2 years ago

Here are some pictures I made for myself trying to "feel" the logic of Tree Calculus's reduction rules: https://latypoff.com/tree-calculus-visualized/ — might be handy for other people who are visual thinkers.

olydis10• 2 years ago

Super cool! I think a (potentially animated) version of this would be an excellent addition for the website's "Specification" page :)

nlitened4• 2 years ago

Let me know if I can help. Or just feel free to take the pics as they are.

alan-crowe2• 2 years ago

That is very helpful. I particularly appreciate the carefully written text.

I think the second figure, captioned "Stem with a single leaf child" has a mistake, with the line down from the triangle descending to a square. But that square should be a circle.

nlitened4• 2 years ago

Thank you for your kind words and also for noticing the mistake — fixed.

rep_lodsb• 2 years ago

Reminds me of Wolfram Physics: it's just "nodes" that exist in relation to each other - and are in all other ways identical -, with some rules for manipulating them leading to all possible computations?

It's certainly not a practical way to write programs.

olydis10• 2 years ago

Hi all, author of the website here (I'm https://johannes-bader.com/). Wow, thanks for the reactions and many good suggestions! I thought I'd add a bit of context here.

As has correctly been pointed out, Tree Calculus was developed by Barry Jay! The "Specification" page links to his book. And a preview of his PEPM 2025 paper (hi chewxy!) can now be found here: https://github.com/barry-jay-personal/typed_tree_calculus/bl...

Compared to how long Barry has been professionally researching this, I entered the picture yesterday and joined the effort to help. Potential mistakes on the website are mine, not Barry's, but I do firmly believe in some of the "ambitious" wording there. Blog posts and more concrete demos or details to come!

Just for the curious, here is my angle in all this:

I happened to (hobbyist!) research tiny, yet practical, languages for over a decade (see e.g. https://lambada.pages.dev/). In that work I started noticing that the Iota combinator (https://en.wikipedia.org/wiki/Iota_and_Jot) is not a combinator in the most traditional sense: It is usually defined as behaving like "\x x S K", but like, how can we just refer to a lambda in the definition of a logic? One could write reduction rules such as "Iota Iota x -> x", but now Iota appears on the left hand side, in argument position! Doesn't that allow reflecting on arguments? Horror! I just started realizing that, while SK is perfectly Turing complete and sane, forcing down the number of combinators from 2 to 1 magically forces some amount of intensionality! Curious, isn't it?

And that's when I came across Barry's work and book! A calculus that embraces intensionality. So I reached out to see if I can help. How can I be most useful? Barry has been figuring out theory, professionally, before I could think. So I felt like helping spread the word, maybe to a less academic developer crowd, would be a more effective way to contribute. I spent my entire career building developer tools, so I have some ideas what could be useful and what might be necessary to convince various kinds of developers. That's how the website came to be, and it is very much a work in progress. We sync regularly, for instance Barry had excellent ideas for demos and I suggested slightly tweaked reduction rules at some point (not more powerful in theory, just more convenient in practice), see "triage calculus" in typed_program_analysis.pdf

SkidanovAlex• 2 years ago

Would help a lot if somewhere at the very top it explained what tree calculus is (may be extend the animation of the addition example to first show what the t is)

It took me a while on the website to understand what it was all about. As it is it looks more like a website for a functional programming language.

skavi• 2 years ago

Are the tweaked reduction rules what you have on this website? I might be misunderstanding, but rule 3 certainly looks different on your website than in Barry’s book.

Could you link typed_program_analysis.pdf? I can’t seem to find it.

wslh• 2 years ago

I'm genuinely curious while skimming Jay’s book, I couldn’t help but notice parallels with LISP-based approaches, which are also tree-structured. How does this differ from those?

Additionally, I have another question: where is this theory [potentially] applied, even if only in niche areas?

Finally, I think there is a glitch in [1] where define "false = t, true = t, etc" I think they meant false = f ? I was mesmerized by a tree representation of not though.

[1] https://treecalcul.us/specification/

mrkeen3• 2 years ago

Additionally, I have another question: where is this theory [potentially] applied, even if only in niche areas?

Intermediate languages - write an interpreter, a JIT, or a compiler for the tree calculus. Then write a high-level language that reduces to tree calculus.

keepamovin• 2 years ago

I like this idea. It's hard to think about ways that trees might combine or operate on other trees. This is fantastic to get into. Thank you for posting and the other commenters for sources.

js82• 2 years ago

AFAIK there are many variations (I think infinite, even) of "tree calculi". You can build one easily from combinatory logic by using only one universal combinator, which will be implied at the leafs of the tree.

John Tromp in his repo has some research pertaining to short universal lambda expressions (each can be expressed as combinators) of this type: https://github.com/tromp/AIT/blob/master/Bases.lhs

olydis10• 2 years ago

Super cool, thanks for the pointer! I'll note, though, that one of the main value adds of (this) TC is that it is also intensional.

See website for some elaboration and examples, I'd particularly recommend looking at https://treecalcul.us/live/?example=demo-fusion which demos a little stream fusion optimizer, entirely from scratch, including small test.

js82• 2 years ago

Oh, OK! I think it would be interesting to know to which universal combinator (or lambda expression) is the 't' related to.

jcmontx• 2 years ago

this looks like OCaml/F# to me

spencerchubb• 2 years ago

the ability to invert a function sounds crazy to me. I never imagined that was possible

scotty792• 2 years ago

Right, two questions, how do you do this infinite loops and how do you do side effects.

All it can do is take programs and return values.

I can see how this could be useful for configuration generation.

But for it to be a programming language you would have to make it produce "execution plant" to be executed on more classical virtual machine that can do system calls and decide what to do next depending on what it gets back.

stronglikedan• 2 years ago

I couldn't imagine trying to type the lambda character that much.

yayr• 2 years ago

Can someone explain to me what is so special here? It seems to be just a simple binary abstract syntax tree, which with varying syntax can represented by almost any programming language

GistNoesis2• 2 years ago

Here is a visualization I made of the tree calculus rules as a pattern matching on binary trees https://github.com/unrealwill/tree-calculus-visualizer

barryjay• 2 years ago

It’s great to see Johannes experimenting with tree calculus, and making explicit the possibilities which are merely implicit in my book GitHub.com/barry-jay-personal/tree-calculus/tree_book.pdf Now that (finally) there is a typed tree calculus I have started blogging (all at GitHub.com/barry-jay-personal)

GregarianChild• 2 years ago

I'm very interested in the "Typed Program Analysis Without Encodings" paper. But I can't seem to find it online. Where do you suggest I look for it?

FranchuFranchu• 2 years ago

I'm not Barry Jay, but I found it here: https://github.com/barry-jay-personal/typed_tree_calculus/bl...

cemerick• 2 years ago

A working link to the book is: https://github.com/barry-jay-personal/tree-calculus/blob/mas... (look for the download button on the right)

Iwan-Zotow• 2 years ago

Isn't it 1 to 1 to iota language/combinator ?

nextaccountic• 2 years ago

Is there any programming language whose implementation uses tree calculus underneath? (Akin to how most programming languages use some variation of lambda calculus for its AST)

ljouhet• 2 years ago

In Python:

    Leaf = []
    Stem = lambda x: [x]
    Fork = lambda a, b: [a, b]

    is_leaf = lambda x: len(x)==0
    is_stem = lambda x: len(x)==1
    is_fork = lambda x: len(x)==2

    def apply(a, b):
        """ From https://treecalcul.us/specification/ (OCaml) """
        if is_leaf(a): return Stem(b)
        if is_stem(a): return Fork(a[0], b)
        x, y = a       # a == Fork(x, y)
        if is_leaf(x): return y
        if is_stem(x): return apply(apply(x[0], b), apply(y, b))
        u, v = x       # x == Fork(u, v)
        if is_leaf(b): return u
        if is_stem(b): return apply(v, b[0])
        s, t = b       # b == Fork(s, t)
        return apply(apply(y, s), t)

    T = {}
    T["false"] = Leaf
    T["true"]  = Stem(Leaf)
    T["not"]   = Fork (Fork (T["true"], Fork (Leaf, T["false"])), Leaf)

    def show(tree):
        name = [k for k in T if T[k]==tree][0]
        print(name or tree)

    show(apply(T["not"], T["false"])) # true
    show(apply(T["not"], T["true"]))  # false

nemoniac• 2 years ago

And here it is in Racket or Scheme:

    (define (apply a b)
      (cond ((null? a) (list b))
            ((procedure? a) (cons (car a) b))
            ((null? (car a)) (cdr a))
            ((procedure? (car a)) (apply (apply (caar a) b) (apply (cdr a) b)))
            ((null? b) (caar a))
            ((procedure? b) (apply (cdar a) (car b)))
            (else (apply (apply (cdr a) (car b)) (cdr b)))))
    
    (define t-false null)
    (define t-true (list null))
    (define t-not (cons (cons (list null) (cons null null)) null))
    
    (apply t-not t-false)
    (apply t-not t-true)

Leaf is null, Stem is list and Fork is cons.

Tree Calculus

Related Stories