Confluence: Does the Evaluation Strategy Matter?

In our open-source announcement in May, we briefly mentioned a new capability of AProVE: the automated analysis of confluence. Since then, AProVE has taken part in the Confluence Competition (CoCo) 2026 in Lisbon, where it finished third in the TRS category, in only its second year of participation. Time to take a closer look: What is confluence, why does a termination tool care about it, and how does AProVE prove (and disprove) it?

What is Confluence?

A term rewrite system (TRS) computes by repeatedly replacing parts of a term according to its rules. In contrast to most programming languages, a TRS does not fix an evaluation strategy: often, several rules can be applied at several positions of a term, and every choice is allowed. Consider the following TRS for addition in Peano arithmetic, where 0 represents zero and s(x) represents the successor x + 1:

plus(0, y)    -> y
plus(s(x), y) -> s(plus(x, y))
plus(x, 0)    -> x
plus(x, s(y)) -> s(plus(x, y))

Here, the recursion may be on either argument. The left part of the figure above shows that the term plus(s(0), s(0)) (i.e., 1 + 1) can be evaluated in two different ways, but both computations result in s(s(0)) (i.e., 2). A TRS is confluent if this always works: whenever a term can be rewritten to two different terms, then these two terms can be rewritten into a common term again. Every term t then has at most one result of all possible computations starting in t. In other words, in a confluent TRS the result of a computation does not depend on the choices made along the way.

Now consider the predecessor function on natural numbers. Since there are no negative numbers, we define the predecessor of 0 to be 0. In addition, we add a rule that simplifies terms of the form (x − 1) + 1 to x:

pred(0)    -> 0
pred(s(x)) -> x
s(pred(x)) -> x

Each rule makes sense on its own, but together they lead to problems. The term s(pred(0)) (i.e., (0 − 1) + 1) can be evaluated in two different ways, as depicted on the right of the figure above. If we first apply the simplification rule at the top, we obtain 0. If we first evaluate the inner subterm pred(0), we obtain s(0) (i.e., 1). These are two different results that can never be joined again, so this TRS is not confluent: here, the evaluation strategy does matter.

Why Does a Termination Tool Care?

Termination and confluence are closely related, and the connection works in both directions:

• Confluence Helps Termination: If all overlaps between the rules of a TRS occur at the root (an overlay system) and the TRS is locally confluent (i.e., every two terms reachable from the same term in a single step can be joined), then termination coincides with innermost termination, where arguments are always evaluated first. Innermost termination is substantially easier to prove, and AProVE’s termination analysis exploits this whenever possible.
• Termination Helps Confluence: For terminating TRSs, confluence is decidable. The reason is that one only has to consider the finitely many situations where two rules overlap, like s(pred(0)) above: since every computation terminates, we can evaluate both results of each overlap to their normal forms, and the TRS is confluent if and only if these normal forms coincide in every case. Hence, AProVE’s powerful termination analysis is a natural foundation for proving confluence.

AProVE at CoCo

The Confluence Competition is the confluence counterpart of the termination competition: every year, confluence tools are run on problems from the ARI database and have to answer YES (confluent) or NO (not confluent) within a fixed time limit. The tool with the most correct answers wins.

• CoCo 2025 (Leipzig): In its first participation, AProVE correctly answered 42 of the 100 competition problems (21 YES, 21 NO) and finished sixth out of seven tools.
• CoCo 2026 (Lisbon, as part of FLoC 2026): With the new techniques, AProVE correctly answered 46 of the 100 competition problems (26 YES, 20 NO) and finished third, behind CSI and Hakusan.

The full results are available for 2026 and 2025.

New in the CoCo 2026 Version

For this year’s competition, we added several new techniques, many of them based on polynomial interpretations, which AProVE already uses heavily for termination proofs:

• Decreasing diagrams (van Oostrom) automated via polynomial interpretations (Aoto), which can prove confluence of non-terminating TRSs.
• Redundant rules (Nagele, Felgenhauer, and Middeldorp): adding or removing rules that can be simulated by other rules can simplify the confluence analysis considerably.
• Disproving confluence via interpretations (Aoto): polynomial interpretations cannot only be used to prove but also to disprove confluence.

These techniques are not yet part of any official release, but they will be released by the end of 2026. All details and references can be found in our system description for CoCo 2026.

Try It Yourself

The confluence analysis is part of the open-source release and can be used via the command line. Simply write your TRS in the ARI format, e.g., the pred example from above:

(format TRS)
(fun 0 0)
(fun s 1)
(fun pred 1)
(rule (pred 0) 0)
(rule (pred (s x)) x)
(rule (s (pred x)) x)

and select the goal confluence:

java -ea -jar aprove.jar -m wst --goal confluence pred.ari

AProVE answers NO and reports a term with two different normal forms:

The TRS is not confluent:
The following term leads to following normal forms:
s(pred(0))
->* 0
->* s(0)

— The AProVE Team