21 ms·
Tree Calculus
- __MatrixMan__ 2y agoI 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 2y agoStraight up dude. Can we get an explanation for the rest of us?
- quantadev 2y ago[flagged]
- hollerith 2y agoAlthough it might turn out to be a waste of everyone's time, it is quite sincere (not a hoax).
- ryandv 2y agoIt's a sign of the times here when people decry computer science constructs they can't understand as hoaxes.
- quantadev 2y agoWell, "hoax" may indeed not be the best word, because it implies intent. I've known of another highly intelligent software developer that invented similar symbology, but was suffering from a mental disorder which made him believe his work was useful even though it's only uses were 'self-referential'. Highly intelligent people, including software developers, are not immune from such disorders.
- ryandv 2y agoThe author has been publishing math and compsci papers since the 80s [0] with another on the way [1]. Maybe stick to TypeScript? [0] https://scholar.google.com/citations?user=eWreFm4AAAAJ&hl=en https://scholar.google.com/citations?user=eWreFm4AAAAJ&hl=en [1] https://popl25.sigplan.org/details/pepm-2025-papers/5/Typed-Program-Analysis-Without-Encodings https://popl25.sigplan.org/details/pepm-2025-papers/5/Typed-...
- quantadev 2y agoOk, thanks. I'll avoid the Turning Tarpits. https://en.wikipedia.org/wiki/Turing_tarpit https://en.wikipedia.org/wiki/Turing_tarpit
- mrkeen 2y agoIs the Y combinator a hoax? λf. (λx. f (x x))(λx. f (x x))
- quantadev 2y agoY Combinator is the simple syntax for representing the concept of passing a function to itself, so it's useful, for symbolic manipulation. However the "Tree Calculus", just from those 5 little rules, is supposedly able to do all kinds of magic. I'm not buying it. It's nothing but musings and examples of binary trees, and how you can convert various data structures to binary trees.
- hollerith 2y agoIf 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.
- toxik 2y agoDo you know what a Y combinator is?
- hollerith 2y agoYes. And I needed to know to follow some of the code ("constructions"?) in the OP.
- lolinder 2y agoBy the measuring stick of "anything that gratifies one's intellectual curiosity," I'd say this submission has been a roaring success for a lot of people. The nice thing about HN is that if something on the front page doesn't gratify your personal curiosity there are 29 more things that might.
- AnimalMuppet 2y agoAnd if the other 29 don't scratch your itch either, then there's a "More" link...
- lolinder 2y agoIt'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__ 2y 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.
- lolinder 2y agoYou know, it's entirely possible that it isn't a language and I just assumed that into existence. It's a very confusing landing page. Edit: no, it's definitely a language of some sort: > The syntax and semantics of Tree Calculus are minimal and self-contained, relying on no platform-specific concepts or abstractions. As a result, it is trivial to write interpreters on any platform or in any programming language (demo). ... > The ability to bootstrap the full power of Tree Calculus anywhere makes it an excellent configuration as code language in a heterogeneous system. Developers could write Tree Calculus programs that generate, say, JSON, and use an interpreter ...
- olydis 2y agoThanks for the feedback! Tree Calculus is a calculus/logic, see Specification page or the book by Barry Jay (linked on that page) for way way better and detailed verbose explanations. It only defines what I chose to call "t" on the website, Barry uses "Δ" in his book and papers. So without anything else, we'd have to talk about programs in terms of "(t t) t ..." or binary trees, which gets unwieldy quickly. The first natural step, for practical purposes, is to allow definitions "foo = ...", then some syntactic sugar for lists, functions, etc. Ooops and now we have a "language". If you open the "Playground" page there's a summary of what exactly is TC and what is syntactic sugar (and really nothing more!) on top of it. I like to think that the line is so blurry precisely because TC needs nothing but a bit of syntactic sugar to feel like a usable PL haha.
- almostgotcaught 2y agopeople 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).
- bertylicious 2y agoI'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.
- almostgotcaught 2y ago> have never seen a programming language that allowed me to de/serialize functions. You can pickle functions in python? You can trivially serialize any lisp function (I'm not a lisp fan). Plenty of programming languages with both macros and first class function objects (those that can be passed around and thus have data representations). > Let alone calculate the inverse of a function Note it says "try to compute the inverse" because actually computing inverses is equivalent to the halting problem. "If it seems to good to be true it probably is" could be adapted here to "If it seems too magical to be true, it's probably just cherry-picked".
- ryandv 2y ago> You can pickle functions in python? You can trivially serialize any lisp function (I'm not a lisp fan). The point of the tree calculus appears to be that it doesn't require the intermediate step of "pickling" or, as the author calls it, "quoting" the program to produce a data structure or other representation of the program [0]: Previous accounts of self-interpretation had to work with programs that were not normal forms, that were unstable. Stability was imposed by first quoting the program to produce a data structure, by putting on some make-up. In tree calculus, the programs are already data structures, so that no pre-processing is required; both of the self-evaluators above act on the program and its input directly. In short, tree calculus supports honest reflection without make-up. It sounds similar to the notion of homoiconicity as in Lisp, but probably more precisely or even strongly stated. > Plenty of programming languages with both macros and first class function objects (those that can be passed around and thus have data representations). A language may have first class function objects, but its actual structure may be opaque and not open to reflection or manipulation (beyond of course just munging the source code as plaintext). You can maybe create a function literal, pass the function around and to higher-order functions, but you can't inspect or modify its internal structure, or decide program equality (based on either exact structure, or one program reducing to another according to the reduction rules of the calculus). Lastly the tree calculus would also appear to differ from the lambda calculus in that programs are stable and won't reduce infinitely, instead converging on some normal form of irreducible terms. [1] [0] https://github.com/barry-jay-personal/tree-calculus/blob/master/tree_book.pdf https://github.com/barry-jay-personal/tree-calculus/blob/mas... [1] https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs.2019.02.016 https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
- theogravity 2y agoThanks for writing what I was afraid to post.
- tkgally 2y agoA 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.”
- rtxgucci 2y ago[dead]
- justinpombrio 2y agoQuick 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 2y ago
- ryandv 2y agoIt'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 https://en.wikipedia.org/wiki/SKI_combinator_calculus [1] https://github.com/barry-jay-personal/tree-calculus/blob/master/tree_book.pdf https://github.com/barry-jay-personal/tree-calculus/blob/mas... [2] https://treecalcul.us/specification/ https://treecalcul.us/specification/ [3] https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs.2019.02.016 https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
- cjfd 2y 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?
- ryandv 2y agoIt would appear that programs in even SKI calculus and other combinatory logics can reduce to base combinators in finitely many steps, but when those combinators are applied to arguments, then the possibility of non-termination arises [0]: Combinatory logic [9,12] is very close to λ-calculus, and widely considered to be equivalent to it [8], but there are important differences. In particular, by modifying the usual account of recursion, i.e. by modifying the usual account of fixpoint functions, it is possible to ensure that all programs are represented by stable combinators, i.e. combinators that are irreducible or in normal form. Only when applied to arguments does non-termination become possible. That is, we may define a program to be a combinator in normal form. As such it is both an executable, since applications of it will trigger evaluation, and also a syntax tree, i.e. a binary tree of applications, with leaves labelled by the primitive combinators, say S and K. [0] https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs.2019.02.016 https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
- Skeime 2y agoI 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 2y agoGreat extra detail - thanks
- mojomark 2y agoSorry, I don't understand what I just saw.
- e-dant 2y agoFeels like clojure from afar
- revskill 2y agoThis is simpler to undrestand than clojure.
- ks2048 2y agoI'm not sure that's true since most of the top-level comments here are saying they don't understand it.
- maxbond 2y agoThere's some kind of problem with the presentation which is causing people not to engage with it. It's no more complex a concept than, say, Lisp; everyone here has learned more complex programming topics than this. But people are not really processing the information presented, eg, there's confusion about whether or not a page with code examples is describing a programming language. I think the presentation is effective but intimidating? There's something about it that causes people to tune out? But if you actually pay it some attention, it's pretty clear. I'm a bit baffled, the presentation looks good to me, and I know these commenters aren't dumb, so I just don't understand what went wrong here.
- adastra22 2y agoThe text on the website linked to is entirely vacant and content-free. It doesn’t actually describe what the language is or how it works.
- maxbond 2y agoThere's a lot of precise, technical language, including a specification - that seems very contentful and specific to me. The code examples seem very straightforward and compelling to me. > # Setup: Simple function on strings > f = λa λb concat ["Hello ",a," ",b,"!"] > f "Jane" "Doe" Hello Jane Doe! This requires some familiarity with languages like Lisp or Forth to follow, but otherwise it's very straightforward. > # What else can we do with a function? > g = f "Admiral" > # Try to invert it: > invert g "Hello Admiral Alice!" Alice That's a really concise and impressive demo to me! I've never seen a language that can invert functions!
- Vampiero 2y agoOn 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.
- bertylicious 2y agoThis depends a lot on what an eval step actually is. Could you give us an example or a reference to compare it to?
- oersted 2y agoBut 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.
- Vampiero 2y agoDamn, that's true. I keep coming back to this thread hoping for more insight because the idea is very pretty.
- adastra22 2y agoCan 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.
- casey2 2y agoLisp 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.
- adastra22 2y agoLambda 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 2y 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_correct_to_say_that_lisp_is_based_on/ https://www.reddit.com/r/lisp/comments/e467tk/is_it_more_cor...
- psychoslave 2y agoIf 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.
- maxbond 2y agoReminds me of Modal. https://wiki.xxiivv.com/site/modal https://wiki.xxiivv.com/site/modal https://wryl.tech/projects/modal.html https://wryl.tech/projects/modal.html
- quantadev 2y ago[flagged]
- Lerc 2y agoThis doesn't seem any more esoteric than lambda calculus. In fact I'm not entirely sure that it isn't a notational variant of lambda calculus. It will take some more investigation than a quick glance to see what truly distinguishes it.
- quantadev 2y ago[flagged]
- keybored 2y agohttps://en.wikipedia.org/wiki/Fixed-point_combinator#Y_combinator_in_lambda_calculus https://en.wikipedia.org/wiki/Fixed-point_combinator#Y_combi...
- chewxy 2y agoBarry Jay's got an upcoming paper at PEPM regarding typed tree calculus. Good read too.
- agnishom 2y agoI googled that, and I found that it is a sister conference of POPL: https://popl25.sigplan.org/details/pepm-2025-papers/5/Typed-Program-Analysis-Without-Encodings https://popl25.sigplan.org/details/pepm-2025-papers/5/Typed-... I was inclined to think that Barry Jay is some kind of crackpot
- justosophy 2y agoSee the Coq proofs in https://github.com/barry-jay-personal/tree-calculus/ https://github.com/barry-jay-personal/tree-calculus/ for the pre-typed tree content as well.
- agnishom 2y agoIt's a good thing there are Coq proofs. However, I would still like to see the paper though. A paper is supposed to be more than just a syntactic theory. Typically there is some motivation included as well.
- vincentpants 2y agoSo wait. How is this not a lisp? And consider that a compliment, we need more lisp in our lives.
- justincredible 2y ago[dead]
- ryandv 2y agoImmediately 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 https://en.wikipedia.org/wiki/SKI_combinator_calculus [1] https://treecalcul.us/live/?example=demo-turing-intensional https://treecalcul.us/live/?example=demo-turing-intensional
- gatane 2y agoYour example reminds me of Binary Lambda Calculus [0]: [0] https://tromp.github.io/cl/Binary_lambda_calculus.html https://tromp.github.io/cl/Binary_lambda_calculus.html
- casey2 2y agoThe 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.
- sitkack 2y agoAn Architecture for Combinator Graph Reduction (TIGRE) https://users.ece.cmu.edu/~koopman/tigre/index.html https://users.ece.cmu.edu/~koopman/tigre/index.html
- xigoi 2y agoThe 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.
- gatane 2y agoThis 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 2y agoOof. 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.
- Jtsummers 2y agoStream fusion is a fancier version of the concept of loop fusion: https://en.wikipedia.org/wiki/Loop_fission_and_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.
- cyberax 2y agoReminds me of Refal, which is somewhat surprisingly Turing-complete.
- LudwigNagasena 2y agoSo it’s based on a universal combinator like Iota?
- Jtsummers 2y agoYes. And the author is Johannes Bader who wrote about that one as well: https://lambada.pages.dev https://lambada.pages.dev https://johannes-bader.com https://johannes-bader.com
- tromp 2y agoNo, 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)
- blahedo 2y agoJust 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 2y agoThank 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.
- olydis 2y agoCorrect! 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 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!
- deleted 2y ago[deleted]
- Trung0246 2y agoInteresting, 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 https://en.wikipedia.org/wiki/Fixed-point_combinator
- october8140 2y agoThis code is so easy to read.
- idle_zealot 2y agoYeah, 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 2y agoNo kidding.. I didn't think parenthesis hell could get worse than Lisp
- galaxyLogic 2y agoSo 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?
- ryandv 2y agoPresumably you could implement Church numerals [0] or something similar in the tree calculus. [0] https://en.wikipedia.org/wiki/Church_encoding https://en.wikipedia.org/wiki/Church_encoding
- blahedo 2y agoTimur Latypoff's page (elsewhere in this thread but also: https://latypoff.com/tree-calculus-visualized/ 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.
- galaxyLogic 2y agoCool, so Church Encoding of numbers is not needed after all. Seems much more simple to do as you describe, numbers are lists of bits. And that is how it is in computer memory too. But, I thought the nodes of the tree in Tree Calculus were supposed to be "unlabeled". How can they then be booleans? Ah, a short read through the link you provided explaines it simply. Thanks.
- quchen 2y agoThe specification talks about numbers, strings, lists. The playground has concrete, runnable (bash, JS) examples.
- agnishom 2y agoThe homepage says "Democratizing Functions" and "Democratizing Metatheory". Whatever that means, I have a strong feeling that this is an abuse of the word "democraztizing"
- falcor84 2y agoThis 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 https://www.britannica.com/dictionary/democratize
- skrebbel 2y agoYeah 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")
- falcor84 2y agoI get your point, but would disagree that being able to apply a function is the same as understanding functions. As with most other things in CS&math, I would argue that you only start to "really understand" functions when you get proficient with higher-order functions, which is what this is about.
- skrebbel 2y agoI never suggested "really understand", I talked about democratization which is used here to mean "to make available to all people". To remind, I'm solely writing all this in support of the comment that "democratizing" is the wrong choice of word here. Sidenote, you can't possibly claim that this site helps anyone understand anything about functions they didn't yet, right? I mean, it's cool, but it's not really easy to understand or anything.
- visarga 2y agoThis 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.
- deleted 2y ago[deleted]
- mrkeen 2y 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/ https://treecalcul.us/specification/ it shows 5 lines of small-step semantics. If you threw these away, could you recover them from the syntax?
- visarga 2y agosyntax becomes semantics after sufficient iterative updates in the environment
- october8140 2y agoIs everyone upvoting this just pretending to understand what it is?
- hoseja 2y agoWe ARE on YCombinator here, after all. And there are lambdas there. Good enough?
- deleted 2y ago[deleted]
- mykowebhn 2y agoNot I, but I upvoted you for telling it how it is.
- mykowebhn 2y agoDarnit, I upvoted. Guilty
- bjackman 2y agoIt's democratisating metatheory! What's not to understand?
- RossBencina 2y agoI upvoted in the hope someone would explain it to me.
- magicalhippo 2y agoThis is one of those articles which I hoped would generate an interesting discussion, and hence I upvoted it on that basis.
- desperate 2y agoSame. Pretty much upvoted because I didn't understand but wanted to, and thought other people might be able to provide more insight.
- golol 2y agoLambda calculus consists pretty much just of function compositions, which in principle have a tree structure. Is this just lambda calculus in a dress?
- tromp 2y agoClose, but not quite; it's combinatory logic plus introspection in a tree dress.
- ranma_42 2y agoThe 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 2y agoAgreed, 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 2y agoI'm too dumb for this
- ethernot 2y agoI've got a mathematics degree and I can't work it out either if that's any consolation.
- GistNoesis 2y agoI 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/ 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.
- justosophy 2y agoTree 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/master/tree_book.pdf https://github.com/barry-jay-personal/tree-calculus/blob/mas...
- al-king 2y agoOh cool, his Bondi Language / Pattern Calculus was the first thing I thought of seeing this, so I guess I wasn't too far wrong.
- olydis 2y agoNote 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 https://news.ycombinator.com/item?id=42375914
- sulam 2y agoEnglish 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.)
- deleted 2y ago[deleted]
- nlitened 2y agoAs I understand, he uses both "intention" and "intension". "Intention" as a desire to do something, and "intensional" as opposite of "extensional": https://www.collinsdictionary.com/dictionary/english/intensional https://www.collinsdictionary.com/dictionary/english/intensi...
- p4bl0 2y agoOn 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 2y agoThis 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.
- nlitened 2y agoHere are some pictures I made for myself trying to "feel" the logic of Tree Calculus's reduction rules: https://latypoff.com/tree-calculus-visualized/ https://latypoff.com/tree-calculus-visualized/ — might be handy for other people who are visual thinkers.
- olydis 2y agoSuper cool! I think a (potentially animated) version of this would be an excellent addition for the website's "Specification" page :)
- alan-crowe 2y agoThat 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.
- nlitened 2y agoThank you for your kind words and also for noticing the mistake — fixed.
- rep_lodsb 2y agoReminds 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.
- olydis 2y agoHi all, author of the website here (I'm https://johannes-bader.com/ 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/blob/main/typed_program_analysis.pdf 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/ https://lambada.pages.dev/). In that work I started noticing that the Iota combinator (https://en.wikipedia.org/wiki/Iota_and_Jot 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 2y agoWould 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.
- wslh 2y agoI'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/ https://treecalcul.us/specification/
- mrkeen 2y 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 2y agoI 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.
- js8 2y agoAFAIK 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 https://github.com/tromp/AIT/blob/master/Bases.lhs
- olydis 2y agoSuper 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 https://treecalcul.us/live/?example=demo-fusion which demos a little stream fusion optimizer, entirely from scratch, including small test.
- js8 2y agoOh, OK! I think it would be interesting to know to which universal combinator (or lambda expression) is the 't' related to.
- chriswarbo 2y agoReduction rules (1) and (2) correspond to those of K and S, respectively. Reduction rule (3) corresponds to the elimination form for a Scott-encoding of a datatype like `X = Leaf | Stem X | Fork X X`. The cases of rule (3) are essentially parsing the argument into one of these three forms, and dispatching on the result.
- ahmadkhan786 2y ago[flagged]
- jcmontx 2y agothis looks like OCaml/F# to me
- spencerchubb 2y agothe ability to invert a function sounds crazy to me. I never imagined that was possible
- scotty79 2y agoRight, 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 2y agoI couldn't imagine trying to type the lambda character that much.
- yayr 2y agoCan 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
- GistNoesis 2y agoHere is a visualization I made of the tree calculus rules as a pattern matching on binary trees https://github.com/unrealwill/tree-calculus-visualizer https://github.com/unrealwill/tree-calculus-visualizer
- barryjay 2y agoIt’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 2y agoI'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 2y agoI'm not Barry Jay, but I found it here: https://github.com/barry-jay-personal/typed_tree_calculus/blob/main/typed_program_analysis.pdf https://github.com/barry-jay-personal/typed_tree_calculus/bl...
- cemerick 2y agoA working link to the book is: https://github.com/barry-jay-personal/tree-calculus/blob/master/tree_book.pdf https://github.com/barry-jay-personal/tree-calculus/blob/mas... (look for the download button on the right)
- Iwan-Zotow 2y agoIsn't it 1 to 1 to iota language/combinator ?
- nextaccountic 2y agoIs 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 2y agoIn 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 2y agoAnd 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.