[Add/Refactor] New module family `Relation.Binary.Rewriting` — Abstract Rewriting Systems

[DrPolonsky]

Summary

We have formalized a substantial body of results about binary relations under the Abstract Rewriting Systems (ARS) rubric and would like to contribute this to the standard library. The existing library covers closure operators and a proof of Newman's Lemma (Relation.Binary.Construct.Closure.ReflexiveTransitive, Relation.Binary.Properties.Setoid), but there is no systematic treatment of ARS properties or their logical interdependencies. We believe this material would be a natural fit under a new Relation.Binary.Rewriting namespace.

This issue is a contribution request: we want to know whether such a contribution would be welcome, and if so, what conventions and structural requirements we should meet before submitting a PR.

Contributors

• Dr. Andrew Polonsky (Appalachian State University), @DrPolonsky
• Sam Arkle, @Sam-Arkle

Existing Codebase

https://github.com/DrPolonsky/FPLA — the relevant modules are under ARS/.

Proposed Content

1. ARS Property Definitions (Rewriting.Properties)

A systematic catalogue of local and global ARS properties, all parametric over {A : Set} (R : Rel A _):

• Confluence family: WCR, CR, diamond property (◆), subcommutativity, commutativity of two relations
• Normalization family: NF, WN, SN (= Acc R), MF (minimal/recurrent form), WM
• NF uniqueness family: NP, MP, UN (and conversion-based variants NP₌, UN₌)
• Sequence-based: RP, BP, CP (recurrence/boundedness/cofinality properties for reduction sequences)
• Completeness: isComplete (= CR ∧ SN), isSemicomplete (= UN₌ ∧ WN)

2. Property Hierarchy (Rewriting.Hierarchy)

Elementary implications and equivalences between the above properties, not tied to specific reference results. Examples: NF ↔ MF ∧ SN, NF ⊆ MF ⊆ MP ⊆ NP ⊆ UN, upward/downward closure of WN, SN, MF, UN under reduction.

3. TeReSe Chapter 1 (Rewriting.TeReSe.Propositions, .Implications, .Theorems, .NewmansLemma)

A formalization of Chapter 1 of TeReSe (Terese 2003), with classical and decidability hypotheses carefully identified and eliminated where possible:

• Prop. 1.1.9–1.1.11: Reformulations of confluence notions; the ◆-sandwich theorem
• Implications: The standard hierarchy diagram (CR→UN, SN→SM, WN→WM, etc.)
• Thm. 1.2.2: CR ↔ WN ∧ UN
• Thm. 1.2.3: WN ∧ WCR ∧ RP⁻ → SN (constructive hypotheses analyzed in detail)
• Newman's Lemma: Classical formulation (SN ∧ WCR → CR); a generalized constructive variant via recurrent elements (see §4 below)

4. Recurrent Elements (Rewriting.Recurrent)

An extension of the standard ARS ontology with the concept of strongly minimal (SM) elements — an inductive generalization of MF — together with:

• SM ⊆ SMseq and double-negation lifts SM⁻, SMseq⁻
• A constructive local Newman's Lemma: WCR ∧ SM x → CR x (no SN hypothesis)

5. Well-Foundedness Analysis (Rewriting.WellFounded — placement TBD)

A detailed constructive analysis of SN and related notions:

• Equivalences between Acc, WFseq (no infinite decreasing sequences), WFmin (minimal element property), under varying classical/decidability assumptions
• WN ∧ isSM → isSN; WN ∧ WCR ∧ RP⁻ → SN (the classical proof, requiring accessibilityIsCoreductive and dec(SN))

Here is a figure from our preprint:

We are unsure where this material belongs: it overlaps with Induction.WellFounded but is specifically about rewriting rather than general well-foundedness.

Questions for Maintainers

1. Is this contribution welcome in principle? We are aware there is no existing lambda calculus or rewriting theory in the standard library; we want to confirm ARS is considered foundational rather than domain-specific before investing in full refactoring.

2. Proposed namespace: We suggest Relation.Binary.Rewriting.*. Does this fit the existing organizational scheme, or would another location (e.g., under Induction.*) be more appropriate?

3. Well-foundedness placement: Should the SN analysis live under Induction.WellFounded or under the new Rewriting.* namespace?

4. Universe polymorphism: Our current codebase is fixed at Set₀. We plan to lift to {a ℓ : Level} {A : Set a} (R : Rel A ℓ) before submitting. Are there other universe-polymorphism conventions we should follow?

5. Prior art: Are we missing any existing ASL modules that already cover some of this material?

References

• Terese (2003). Term Rewriting Systems. Cambridge University Press. Chapter 1.

[jwaldmann]

Nice. I will read, and possibly use, this. You mention "our preprint", where is it?

I am working on something related, but it has ARS only as far as it's needed for some methods of termination (cf. Chapter 6 of Terese) of string rewriting. It's nowhere as polished as yours seems to be. Perhaps we can merge this somehow sometime https://git.imn.htwk-leipzig.de/waldmann/cetera/-/blob/main/core/Cetera/ARS.agda?ref_type=heads

"welcome in principle?" that's for maintainers to decide. My opinion as a mere user/observer: ARS certainly is a fundamental concept, and Terese is the standard reference. So, everything that's directly from Terese, could go into stdlib. But your work has some extras, you mention "notions of wellfoundedness", how stable are these? What choices did you make? (I guess you discuss that in the paper.)

stdlib is monolithic: both the result and the process, everything goes through one repo, one issue tracker, one release management. A distributed development/release of libraries (cf. hackage.haskell.org, archive of formal proofs?) might be preferable, at least in theory - in practice I think that currently, Agda does not have the tools and infra. This makes working with extra libraries somewhat inconvenient (manually wget, tar, edit config file) .

See also . https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/How.20standard.20is.20stdlib.3F

[DrPolonsky]

Thank you very much for the feedback!
We just put the preprint on arxiv, I'll follow-up as soon as it goes live.
The Cetera project looks really nice. I can certainly see potential for merging some of the overlap we have, and would be glad to help do this/discuss this further.
Do you have TRS termination as part of the scope of your project? Because formalizing TRSs is something on our radar, and we have not found any significant formalization of TRSs in Agda thus far...
Thanks also for the discussion about the current state of agda-stdlib.

[DrPolonsky]

Here is the preprint about our development:
https://arxiv.org/abs/2603.10936

[jwaldmann]

Thanks for linking the paper.

TRS formalisation: not planned for my project. I don't have the ressources. The goal is to formalize "sparse tiling" (FSCD 2019), which is SRS only. Alas, that paper uses "local termination" (LMCS 2010) which is for TRS. So - formalize a different (SRS-only) proof, or write a postulate and wait until some TRS formalization pops up elsewhere. (In other words: please do!)

This may be the kind of discussion that is very interesting to have (for a subset of the community) but not here (stdlib issue tracker)?

So, coming back to your work on ARS: as I said, I'd welcome it very much, and it will be useful for any (step-wise) model of computation (not just TRS, SRS).

I think some ARS results from Geser: Relative Termination https://homepage.cs.uiowa.edu/~astump/papers/geser_dissertation.pdf would be good to have, also Bachmair Dershowitz CADE 86 on Commutation. (Some are in Terese already.) I would prefer constructive proofs (where possible). I have not checked in detail. Example: https://git.imn.htwk-leipzig.de/waldmann/cetera/-/blob/main/core/Cetera/RFC.agda?ref_type=heads#L250 Of course, these can be added to stdlib later, after we see what we need in a TRS/SRS formalisation.

[JacquesCarette]

I am, in principle, very much in favour of doing this. I would think some material could well belong in Relation.Binary.Rewriting.*. and other in Induction.WellFounded. Yes, you will definitely first have to make things as universe polymorphic as possible.

Assuming that other agda-stdlib maintainers agree, the hardest part will be to 'stage' the review and inclusion of this material. Suggestion: you fork a version of FPLA for this purpose. Reason: we (the maintainers) will likely ask you to make a bunch of changes, which you should propagate through all of FPLA to make sure our suggestions 'scale' properly. [This is the biggest danger of local suggestions!]

[DrPolonsky]

@JacquesCarette — Thanks for the feedback! We will do as you suggested, forking FPLA and revising it to comply with ASL guidelines on universes, decidability, etc.

@jwaldmann — These are great suggestions, I agree that the ARS results on relative termination and commutation would naturally belong here. We could look into adding those once the current codebase is ported.

We will start refactoring now. Will follow up once we are done.