fix(AC): Abstract AC arguments that contain other AC symbols

[bclement-ocp]

This patch implements a variation of the abstraction mechanism described in the AC(X) paper. This should hopefully ensure that we can't create substitution cycles due to improper term ordering.

Note that the issue is related to comparing distinct AC symbols: when the AC symbols are identical, the AC theory uses a multiset ordering on its argument, which prevent substitution cycles. But when the AC symbols are different, only the symbols are compared, not the arguments, and so we must rely on the abstraction mechanism to prevent cycles.

This is a do-over of #974 that should be closer in spirit to the implementation of the paper and without the associated regressions (based upon a manual inspection; will re-run the benchmarks).

Fixes #964

[bclement-ocp]

without the associated regressions

Confirmed: this patch is +3-0 on AE-format.

[bclement-ocp]

@Gbury @Halbaroth ping (PR rebased onto next)

[bclement-ocp]

@Gbury ping

[Halbaroth]

I will review this PR this afternoon :) Thanks for your patience!

[Halbaroth]

Nit: we should use DOI as much as possible to have permanent link:
https://doi.org/10.2168/LMCS-8(3:16)2012

[bclement-ocp]

I generally don't use DOI links because, in my experience, they more often than not point to sources that are not open access — and they typically point to some sort of publisher page rather than to the actual article, introducing friction. I'd argue arXiv (and institutional archives such as HAL) links are about as permanent as DOIs.

That said, the paper title should definitely be there; I will update the comment with the paper title and DOI for completeness (but keep the arXiv link as it is more convenient for the reader).

[Halbaroth]

I agree that arXiv links should be stable and adding the title of the article should sufficient to retrieve the article in future.

[Halbaroth]

If I understand well, in the paper we first define a set of terms T and equations s = t with s, t \in T and we consider a subset of equations (named abstracted equations (technically it's not a subset as we introduce abstract variables from a fresh set K)) on which the multiset order should ensure the termination of the AC(X) procedure.

In the implementation, we never produce the superset of equations because the terms (named semantic values in the implementation) are abstracted by construction?

[bclement-ocp]

I think it is something like that, yes — in the paper we first build the equations and then perform term abstraction until all equations are in "abstracted form" (note that being abstracted is a condition on the equation, not on the term). But in the implementation we abstract terms when building semantic values, and so we must make sure that all possible equations between arbitrary semantic values are in abstracted form.

In particular, this implies (definition of T_AC) that AC symbols that appear at any depth inside the arguments of another AC symbol must be abstracted, which is what this PR enforces.

There might be additional properties that we need to enforce to ensure completeness; for instance, it is still possible to build equalities between uninterpreted/AC terms which should not be allowed as per the paper (one at least must be abstracted as per Definition 6.1). I think that this turns out OK because comparison between AC semantic values/terms starts by comparing the head symbol, and everything behaves as if the term with smallest head symbol was always abstracted in a consistent way — but I have done no proof and could easily be wrong.

[Halbaroth]

I guess this is the only important line in this PR :)

Let's u and v two distinct AC symbols (for sake of simplicity, say that u and v are binary integer operators).
Consider the expressions A := u(v(x, y), z) and B := u(v(x, y) + t, z).

In the previous implementation, we abstracted the subterm v(x, y) in the former case but we don't in the latter one.

In the new implementation, we'll abstract both of them because v(x, y) is now a leaf of an argument of u and u is distinct of v.

If we replace the operator + by a non-ac uninterpreted symbol, we don't abstract the subterm v(x, y), right? For instance we don't abstract v(x, y) in the term u(h(v(x, y), t), z) where h is a non-ac uninterpreted operator.

I guess the notation Σ_∅ in 𝒯_∅ in the paper denotes the interpreted symbols?

We don't need to abstract uninterpreted symbols here because, by definition they are already abstracted, so there is no relation between h(x, y) and h(y, x) that can induce an infinity path in the reduction algorithm?

[bclement-ocp]

Yes exactly — uninterpreted terms do not take part in this process because with semantic values we never look inside uninterpreted terms to see that they actually contain AC symbols. Instead, if we merge AC terms, say we have h(v(x, v(y, z))) and h(v(v(x, y), z)), the AC theory will normalize v(x, v(y, z)) and v(v(x, y), z) (as semantic values) to the same representative, it will be picked up by CC(X) to prove equality of the two h terms. But we never actually look inside or indeed rewrite inside uninterpreted terms.