Potential nontermination for flat operators

[HarrisonGrodin]

The clash between flattening rules and flat pattern matching causes nontermination with some flat operators. For example:

f(f(a, f(b, c), d), f(e, f(g, h)))

This exists regardless of whether the flat operator is explicitly given in the rule (e.g. current master) or if the operator is variable (e.g. #52).

[willow-ahrens]

Pardon my slight digression, but this seems like the right issue on which to ask a design question. Why are the orderless and flat properties implemented in the match function? It seems that most of the same functionality could be implemented with rules?

Lets assume that flatness is implemented with a flattening rule, and orderlessness is implemented with an ordering rule. If one wanted to match the terms A and B structurally without orderless and flat properties, they could call match(A, B). If one wanted to take into account orderless and flat, they would add those rewrite rules to TRS and call match(A, B, TRS) which would call match(normalize(A, TRS), normalize(B, TRS)). One doesn't technically need Context to implement Orderless and Flat properties, right?

Edit: Okay I see now how Orderless properties make it easier to implement EvalRules, for instance. It would be possible to implement without a context, but one would need to make special eval rules for orderless functions, etc. https://github.com/HarrisonGrodin/Rewrite.jl/blob/03af1708d18f17efbc6e604b58c4d4943930607b/src/rule.jl#L98-L104

[HarrisonGrodin]

TL;DR: variables are hard.

---

Unfortunately, orderless matching is fairly necessary, even for pattern-based rules; the underlying reason is that there's no logical ordering for variables. Consider the following (albeit somewhat contrived) example:

rs = @term RULES [
    x + 0 + 5 => x + 5
]

a = @term(sin(1) + 0 + 5)
b = @term(0 + 3 + 5)

I would argue that no sensible ordering would remove the need for orderless matching. In general, it seems reasonable that constants should be ordered by magnitude. It seems that we should keep a as-is to ensure the rule matches. However, for b to match the rule, the 3 would also have to be at the beginning. (Similar arguments can be made for any positioning of the x in the input pattern of the rule.)

It does seem like a significant speedup for orderless matching could be achieved under the knowledge that terms are automatically ordered, though, simply moving variables through the term without modifying the relative order of the rest of the arguments. (I've opened #55 for this purpose.)

---

Flat matching is "less required" from a theoretical point of view, since rules can be initially rewritten to prefer left- or right-associativity (see Completion.jl). However, from a practical perspective, it's an extremely useful feature to have, especially since Rewrite follows the Julian precedent of treating associative/flat operations as if they have variable arity.

Let f be a flat (but not orderless) function:

rs = @term RULES [
    f(x, x) => x^2
]

@syms a b
normalize(@term(f(a, b, a, b)), rs)
# @term(f(a, b)^2)

Here, Rewrite is able to leverage flat matching to interpret f(a, b, a, b) as f(f(a, b), f(a, b)) when attempting to match the given rule, since variables in flat expressions are allowed to "slurp" multiple subterms.

---

Dealing with the properties themselves by writing rules is typically the best approach. In addition to OrderRule, we have:
https://github.com/HarrisonGrodin/Rewrite.jl/blob/03af1708d18f17efbc6e604b58c4d4943930607b/src/rules.jl#L65-L66
However, when dealing with the consequences of these properties, handling special cases through matching seems like the only viable solution.

[willow-ahrens]

Thanks for the detailed response! This has been very helpful, and I have a renewed respect for the Context type.

[MasonProtter]

I think I recently found a simple instance of this:

t = @term 1 + x + y - x
normalize(t)

seems to not terminate.