Reading the technical papers around Tree Calculus, I now see this claim a little more clearly. It's based around Tree Calculus rejecting eta-equivalence.
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
This is sound and, if we apply it before beta-reduction, ensures that both forms will also reduce in the same way (and hence have the same normal forms, if they exist). Note that Python has a single evaluation strategy, which will not reduce an expression like `lambda f: lambda x: f(x)` to `lambda f: f`; hence it doesn't implement eta-reduction.
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.
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.
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:
This is sound and, if we apply it before beta-reduction, ensures that both forms will also reduce in the same way (and hence have the same normal forms, if they exist). Note that Python has a single evaluation strategy, which will not reduce an expression like `lambda f: lambda x: f(x)` to `lambda f: f`; hence it doesn't implement eta-reduction.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.