This thread is perhaps phrased confusingly. If I understand correctly, the claim is only that any program (including recursive ones) can be expressed in a finite normal form, which may of course diverge when "run" (applied to an argument). The same is true for basically every language though, e.g. consider the following Python:
omega = lambda x: x(x)
omega(omega)(42)
The expression `omega(omega)` diverges, but only because we've applied it to an argument. The function `omega` itself is in an irreducible normal form, namely `lambda x: x(x)`.
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)
The function `adjust` is not in a normal form, since it depends on the value of `increase` (when truthy, `adjust` will increment; when falsy it'll decrement). Yet most programmers would probably avoid that, in favour of this:
adjust = lambda x: x + 1 if increase else x - 1
Both implementations of `adjust` will behave the same, but the second is in a normal form.
I'm rusty but doesn't the increase depend differently, the second adjust lets you decide to assign a value for the variable increase much later, whereas the first adjust fixes the value of increase at the point of evaluating that very assignment statement. There's a name for this, dynamic scoping or something.
Yes, my argument relies on immutability of all values (including `increase`). Also, under lazy evaluation we can call `adjust2` immediately, since we know it's a `lambda`; yet attempting to call `adjust1` will force evaluation of `increase`; not good if `increase = provable(collatz_conjecture)`!
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.
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:
The function `adjust` is not in a normal form, since it depends on the value of `increase` (when truthy, `adjust` will increment; when falsy it'll decrement). Yet most programmers would probably avoid that, in favour of this: Both implementations of `adjust` will behave the same, but the second is in a normal form.