Although my evaluator detects the two most common types of infinite loop, at sizes of 6 and above there are too many undetected ones to evaluate by hand. However, when you’re confirming the non‐termination of a function, you can perform simplifications on its subexpressions which wouldn’t be valid in other contexts, and this lets you perform drastic pruning.
In the general case, we can simplify expression e to expression d if they are equivalent functions, meaning they evaluate to the same values (here including “∞”) when given the same inputs. But if d is part of a function which doesn’t terminate, we only need for e’s and d’s outputs to match when e terminates — the function is non‐terminating, so substitutions which match behaviors except to introduce new ways to not terminate won’t go and make it terminate instead.
To prove that, let’s say f is a function which doesn’t terminate, and it has d as a subexpression, and that e(x₁, ..., xₖ) = d(x₁, ..., xₖ) whenever e terminates, and g is obtained by substituting e in place of d within f. We need to show that g doesn’t terminate. Since f doesn’t terminate, it could either:
In case (1) we could have substituted anything in for d and g would still get stuck. In case (2), every time e is called in the evaluation of g, it either returns the same value d did in the evaluation of f or it enters an infinite loop. If the latter, then g doesn’t terminate. If the former, g will behave identically to f because e returned the same value d did, and so g will call e again. At this point e will once again either enter an infinite loop or return the same value d did. So e either right here prevents g from terminating, or e faithfully matches d again and g calls it again. So unless e enters an infinite loop, thereby preventing g from terminating, g calls it infinitely, and hence doesn’t terminate. In case (3), each time e is called it similarly has an opportunity to enter an infinite loop, which would ensure g doesn’t terminate. If it doesn’t loop, then that can’t be a time when d entered an infinite loop, and it must return the same value d does, ensuring g’s evaluation matches f ’s, and so when g doesn’t get caught in an infinite loop from e, it must get caught in the same infinite loop f does.
So we can consider the cases where e “returns” ∞ to be wild cards when matching against d’s. With this license to do this special form of sloppy matching, let’s look at some pruning we can do. You can’t simplify single‐operator expressions, so let’s start with the expressions with size=2 (of any arity). They fall into these four classes:
Class (2) is an infinite loop and classes (1) and (4) are equivalent to Z. The behavior of class (3) depends on i. When i=1, it’s equivalent to Z. Otherwise it returns 0 if the i−1ᵗʰ argument is 0 and ∞ otherwise.
Interestingly, every size=2 expression will evaluate down to either 0 or ∞. That means that every time a non‐terminating function has a Z in it, we can prune every function which has that Z replaced with any size=2 expression.
For size=3 and up, the behavior is more diverse. I had my generator make all the GRF’s with size 3 or 4 and arity 1‒3, and I found simplifications for 89 of them. These are listed in this table.
These simplifications pruned down the GRF’s requiring manual validation drastically. I wouldn’t consider size 7’s validation doable without it.