Invariant Density and Bounded Derivability in Finite Equational Presentations
Fuente:
Zenodo
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Recurso digital |
| Pubblicazione: |
Zenodo
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866901504994050048 |
|---|---|
| author | Tonnel, David Gérard |
| author_facet | Tonnel, David Gérard |
| contents | <p>This paper introduces invariant density, a syntactic measure for finite equational presentations based on bounded derivability.</p> <p>The framework is explicitly bounded, decidable, and terminating for fixed parameters, but intentionally incomplete. It formalizes invariant sets, proves monotonicity properties, and shows how redundancy elimination increases invariant density without loss of bounded invariants.</p> <p>A reference implementation realizing the definitions and algorithms is archived separately on Zenodo and publicly available. <a href="https://doi.org/10.5281/zenodo.18441678">10.5281/zenodo.18441678</a></p> <blockquote> <p>An appendix documenting a reference implementation snapshot is included for reproducibility.</p> <p>This work is part of a broader suite developing invariant density across syntactic, formal, and semantic contexts. The present paper focuses on bounded derivability in finite equational presentations. Complementary works in the suite address geometric formulations, general syntactic frameworks, algebraic semantics, and proof assistant realizations (including Coq), each archived separately on Zenodo:</p> <p><a href="https://doi.org/10.5281/zenodo.18265909" target="_new" rel="noopener">https://doi.org/10.5281/zenodo.18265909</a> (geometric formulation)<br><a href="https://doi.org/10.5281/zenodo.18301563" target="_new" rel="noopener">https://doi.org/10.5281/zenodo.18301563</a> (syntactic framework)<br><a href="https://doi.org/10.5281/zenodo.18301522" target="_new" rel="noopener">https://doi.org/10.5281/zenodo.18301522</a> (algebraic semantics)<br><a href="https://doi.org/10.5281/zenodo.18301480" target="_new" rel="noopener">https://doi.org/10.5281/zenodo.18301480</a> (proof assistants)</p> </blockquote> <p> </p> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_18405714 |
| institution | Zenodo |
| language | |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | Invariant Density and Bounded Derivability in Finite Equational Presentations Tonnel, David Gérard equational logic equational presentations bounded derivability invariant density rewrite systems syntactic invariants algebraic redundancy computational logic <p>This paper introduces invariant density, a syntactic measure for finite equational presentations based on bounded derivability.</p> <p>The framework is explicitly bounded, decidable, and terminating for fixed parameters, but intentionally incomplete. It formalizes invariant sets, proves monotonicity properties, and shows how redundancy elimination increases invariant density without loss of bounded invariants.</p> <p>A reference implementation realizing the definitions and algorithms is archived separately on Zenodo and publicly available. <a href="https://doi.org/10.5281/zenodo.18441678">10.5281/zenodo.18441678</a></p> <blockquote> <p>An appendix documenting a reference implementation snapshot is included for reproducibility.</p> <p>This work is part of a broader suite developing invariant density across syntactic, formal, and semantic contexts. The present paper focuses on bounded derivability in finite equational presentations. Complementary works in the suite address geometric formulations, general syntactic frameworks, algebraic semantics, and proof assistant realizations (including Coq), each archived separately on Zenodo:</p> <p><a href="https://doi.org/10.5281/zenodo.18265909" target="_new" rel="noopener">https://doi.org/10.5281/zenodo.18265909</a> (geometric formulation)<br><a href="https://doi.org/10.5281/zenodo.18301563" target="_new" rel="noopener">https://doi.org/10.5281/zenodo.18301563</a> (syntactic framework)<br><a href="https://doi.org/10.5281/zenodo.18301522" target="_new" rel="noopener">https://doi.org/10.5281/zenodo.18301522</a> (algebraic semantics)<br><a href="https://doi.org/10.5281/zenodo.18301480" target="_new" rel="noopener">https://doi.org/10.5281/zenodo.18301480</a> (proof assistants)</p> </blockquote> <p> </p> |
| title | Invariant Density and Bounded Derivability in Finite Equational Presentations |
| topic | equational logic equational presentations bounded derivability invariant density rewrite systems syntactic invariants algebraic redundancy computational logic |
| url | https://doi.org/10.5281/zenodo.18405714 |