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...
> 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
(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.)
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....
How is that possible if the reduction rules define a Turing complete language?
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.
omega = lambda x: x(x)
omega(omega)(42)
On the other hand, consider the function call with argument `42`: in that case, the function is `omega(omega)`, which is not in a normal form, and in fact diverges. In a system like SK, and presumably this tree calculus, we can form a similar expression, where the "function part" (i.e. left sub-tree) diverges with no normal form. That's unavoidable, due to the halting problem.
I think the claim is that we never need to write such expressions, since there's always an alternative which behaves the same but whose "function part" has a normal form.
As a (slightly) more practical example, consider some code like:
adjust = (lambda x: x + 1) if increase else (lambda x: x - 1)
adjust = lambda x: x + 1 if increase else x - 1
Test:
increase = True
adjust1 = (lambda x: x + 1) if increase else (lambda x: x - 1)
adjust2 = lambda x: x + 1 if increase else x - 1
print(adjust1(42))
print(adjust2(42))
increase = False
print(adjust1(42))
print(adjust2(42))In Lambda Calculus, eta-equivalence says that `λf. λx. f x` is equivalent to `λf. f`, i.e. a function which passes its argument straight into `f` and returns the result unmodified, is indistinguishable from the function `f` itself. Those two functions could beta-reduce in a different order, depending on the evaluation strategy we use; but such distinctions are unobservable from within Lambda Calculus itself. In fact, we can make a rule, called eta-reduction, which transforms one into the other:
λx. F x --> F
In SK combinatory logic, eta-reduction is also sound; e.g. if 'xyz' reduces to 'yz' then 'xy' is equivalent to 'y'. This is obvious with a combinator like I = SKK, since Iy reduces to y via the ordinary S and K rules, so Iyz reduces yz in the same way, and the above implication is trivial. However, there are other combinators which don't reduce reduce all the way until they get another argument, i.e. a combinator W where Wy does not reduce to y, but Wyz does reduce to yz (the Tree Calculus papers give examples, referred to as "wait" combinators). It's fine to use an eta-equivalence rule like "if xyz ~= yz then xy ~= y" for reasoning about SK programs, but to actually reduce real expressions we may need a whole bunch of rules, to cover the most common "wait" combinators. The reason this is sound is that the only ways an SK expression can "use" an argument it's applied to is either (a) discard it, (b) apply some other other expression to it (potentially copying it a few times), or (c) apply it to some other expression. Cases (a) and (b) do not depend on the particular value of the expression, and the behaviour of (c) respects eta-equivalence.
(Side note, I recently implemented SK in egglog, and wrote a search procedure for finding eta-equivalent expressions and setting them equal http://www.chriswarbo.net/blog/2024-05-10-sk_logic_in_egglog... )
Tree Calculus can also use a given expression in another way: it can branch on the structure. That doesn't respect eta-equivalence, and hence Tree Calculus can use this to distinguish between two combinators P and Q even if Px == Qx for all x.
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.
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?
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.
Note that the first two rules of this Tree Calculus are precisely those of K and S.
Wrong. I = S K M where M can be anything:
I x = S K M x = K x (M x) = x
> essentially an obfuscated mix of S and K
Most alternatives are tuples of S and K like λz. z S K or λz. z K S K. But the arguably shortest one is indeed a proper mix:
A = λx λy λz. x z (y (λ. z)) = λx λy λz. x z (y (K z))You're absolutely right.
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 ...
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.
I love the idea of having a website like this to introduce people to one of the less popular calculi, and the playground is a great touch. It might be helpful to have an introductory paragraph that explains exactly what the tree calculus is, starting from what a "calculus" is—your target audience seems to be people who aren't otherwise going to go out of their way to read Barry's papers, which means you can't assume as much background as you currently do. As a reference, I'm a casual PL nerd who actually has read academic papers related to some of the less well-known calculi with an eye towards implementing them, so I'm on the more informed end of the spectrum of your target audience.
Have you considered making this site open source? No pressure if not, but if so I'd be happy to contribute to polishing up the landing page. I'm very interested in learning more about this anyway, and I'm more than willing to help!
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.)
“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.”
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).
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".
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.
But there's a reason for that. Functions make a good basis for programming languages. It's not the only good basis! Concatenative combinators make a good basis too: see Factor and Joy.
If you take the lambda calculus and add numbers and a few operations on them, it's easy to program in it. Likewise for the concatenative calculus. But not so for NAND gates or SK combinators. You certainly can do anything you want with them, but doing so feels more like solving a logic puzzle than programming. I am likewise skeptical about the tree calculus.
Turing machine includes write over some place, thus it models a calculating man with infinite paper, infinite pencil and infinite eraser. Lambda calculus models calculating man with infinite paper and infinite pencil. Lambda calculus has very substantial advantage here.
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?
These choices will affect what the functions that operate on data look like, concretely.
It'd be great if you could add some beginner-friendly introduction to your website. :)
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)
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).
⍝ Convert Fahrenheit to Celsius
f_to_c ← (÷∘1.8)∘(-∘32)
f_to_c 68
20
(f_to_c ⍣ ¯1) 20
68
More interesting are logic languages such as Prolog. If you stick to the core logical features, you get the inverse of a function for free:
?- append([1,2,3], [4,5,6], X).
X = [1, 2, 3, 4, 5, 6].
?- append(X, [4,5,6], [1,2,3,4,5,6]).
X = [1, 2, 3].
?- append(X, Y, [1,2,3,4]).
X = [], Y = [1, 2, 3, 4] ;
X = [1], Y = [2, 3, 4] ;
X = [1, 2], Y = [3, 4] ;
X = [1, 2, 3], Y = [4] ;
X = [1, 2, 3, 4], Y = [].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".
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.
> 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/mas...
[1] https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
What he implemented IS quotation, despite his objections.
Reflective programs are programs that can act on themselves to query their own struc-
ture. The querying is important: that the identity function can be applied to itself does
not make it reflective. A simple example is the size function defined in Chapter 5.
When applied to itself, the result is (the tree of) the number 508 [...] Self-evaluation
in a calculus provides good evidence for the ability to perform program analysis and
optimisation within the calculus itself. Traditionally, self-interpreters were allowed to
act on the syntax tree of a program, i.e. its quotation. [...] When quotation lies
outside of the formal calculus then interpretation is separated from computation proper,
so that some sort of staging is required.
size = \x (y $ \self \x compose succ $ triage id self (\x \y compose (self x) (self y)) x) x 0
[1] https://treecalcul.us/live/?example=demo-program-optimizatio...
At its current state of development, it might be more appropriate for the blog "Lambda the Ultimate" than HN.
Maybe stick to TypeScript?
[0] https://scholar.google.com/citations?user=eWreFm4AAAAJ&hl=en
[1] https://popl25.sigplan.org/details/pepm-2025-papers/5/Typed-...
λf. (λx. f (x x))(λx. f (x x))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.
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")
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.
Here is a (slightly provocative) thought: We developers were promised "first class functions" with functional programming languages. And it's true, you can pass them around like any other value! Cool. But first: What about inspecting those values? I can "look inside of" a number or string or array any day. But functions, I can only call. Huh, so an intensional view (not that anyone thinks that out loud) for all kinds of values, except functions. Yes sure, many languages do allow you do dig into functions. But it is all not the same as or as powerful as supporting it right down at the logic level! TC is also not first to do that. But IMO the most compact and practical calculus/language to do so, yet. Second, a practical example: We had "first class functions" for decades now. But where is our main stream config language (JSON etc) that has first class support for them? Of course the answer is: Because it remains tricky. In industry I've seen all sorts of work arounds, usually involving strings that get compiled/interpreted on the fly. Which usually means some amount of scary security, and no static guarantees whatsoever. With TC, a parser/runtime for arbitrary (but pure) functions is a few dozens lines of code. And thanks to being intensional, one can imagine type checking those functions at the time of loading the config, not only when executing! Concrete demo/blog post for exactly this is in the works.
So anyways, I do belive this enables truly fundamental shifts, hence "democratizing".
$ pil +
: (de blepis (x y) (+ x y]
-> blepis
: (car 'blepis)
-> ((x y) (+ x y))Unlike school, were you are thought to reproduce them apply them, fire and forget them.
Just because something is available, doesn't mean its democratic. Even in a democracy.
I do not know what it would even mean to democratize functions. Functions just are. Can you democratize the number 5?
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.
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.
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.
I don’t mean that as a criticism or midwit dismissal. Just want to understand.
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.
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...
Nit picky point: quote/eval is an integral part of Lisp, not a later addon.
It's fine other people have different tastes really. I'm just sad that homoiconicity is mostly trapped within lisp dialects.
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)))))))
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))))));
Why would it be readable?
The next one would be () = t, to finally get a language consisting solely of parentheses.
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));
- 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)
t a -> (t a) (0a)
(t a) b -> (t a b) (0b)
- 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.
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.
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!
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 (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)
Should be "t (t (t t) (t t t)) t (t t)".
('signatures', in case you were wondering)
I was inclined to think that Barry Jay is some kind of crackpot
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
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.
Theoretically profound but ultimately needing to be somewhat removed from its application to be of much practical use.
Thanks for the inspiration!
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?
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?
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.
The playground has concrete, runnable (bash, JS) examples.
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.
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.
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.
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
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."
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.
(t (t) a) b -> a (1)
(t (t a) b) c -> (a c) (b c) (2)But this criticism is valid for most of the website. Nothing is really clear.
It's certainly not a practical way to write programs.
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.
At a high level and skipping details, suppose you want to do something like this:
(filter predicate (map f sequence))
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.
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.
The heading of the entire page is "the essence of computation" but I'm not shown why the code examples (which at a cursory glance look like a run-of-the-mill FP language) warrant that claim.
Then we read that there is "one operator", but that's clearly not visible from the examples. You have to read the comments in the playground to understand that things like definitions, lambdas, lists, etc. are syntactic sugar added on top of TC (which is fine, but it's just not transparent initially). In general, the distinction between TC (a formal calculus) and the programming language implemented here based on TC is not made clear enough.
The code examples themselves are fine (and there's some interesting things in there), but I stumbled over the "try to invert function" example. While the example itself is reasonably clear, it's not at all clear what that would mean in the general case - you clearly can't invert all functions (especially not non-injective ones). That should definitely be explained better.
At the top of https://treecalcul.us/specification/ you have 5 rules. Your (valid) program will match one of the left-hand-sides. To execute your program, turn whichever LHS your program is into its corresponding RHS. Keep doing that until you can't, and you'll be left with your final answer.
It also provides 2 reference interpreters (OCaml and JS) on the same page. Each interpreter is just a single recursive function 'apply' (which does what I described in the above paragraph). Note the 'match a with' section in the OCaml version. That's essentially the 5 rules from the top translated to OCaml. (I'm not sure why they're slightly different but there's probably a good reason).
The JS interpreter is harder to read ("length"? "push"? "pop"? these aren't in the spec above). My guess is that a machine-friendly translation was needed so that JS wouldn't die from recursing too deeply.
I clicked on 'runjs.app' link, looked at the examples at the bottom, and added my own.
apply(_not, apply(_not, _true));
[ [] ]
const _true = [[]];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!
> # What else can we do with a function?
> g = f "Admiral"
> # Try to invert it:
> invert g "Hello Admiral
Alice!"
Alice
prolog
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
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.
Could you link typed_program_analysis.pdf? I can’t seem to find it.