ON THE CONFLUENCE OF REWRITE SYSTEMS
Description
Term rewriting is a very simple model of computation based on
equational logic. It can be directly used to write declarative programs
or to give formal semantics to conventional programming languages. To
obtain an executable specification from an equational theory, some
computational conditions must be satisfied, such as termination and
confluence.
Confluence is the property of reduction relations that
guarantees that whenever a term has two different reducts, both are
joinable. It is one of the most important properties of reduction
relations because it ensures that for all expressions there exists at
most one reducible reduct and that two divergent computations always
join in the future.
Outline
- Introduction to Confluence.
- Confluence on Term Rewriting Systems.
- Confluence on Conditional Term Rewriting Systems
- Confluence on Context-Sensitive Term Rewriting Systems.
- The Confluence Framework.
- Feasibility and The Feasibility Framework.
Bibliography
- [BN98] F. Baader, T. Nipkow: Term rewriting and all that. Cambridge University Press 1998, ISBN 978-0-521-45520-6, pp. I-XII, 1-301
- [DOS87] N. Dershowitz, M. Okada, G. Sivakumar: Confluence of Conditional Rewrite Systems. CTRS 1987: 31-44
- [GL20] R. Gutiérrez, S. Lucas. Automatically Proving and
Disproving Feasibility Conditions. IJCAR (2) 2020: 416-435
- [GLV21] R. Gutiérrez, S. Lucas, M. Vítores: Confluence of
Conditional Rewriting in Logic Form. FSTTCS 2021: 44:1-44:18
- [GVL22] R. Gutiérrez, M. Vítores, S. Lucas. Confluence
Framework: Proving Confluence with CONFident. LOPSTR 2022: 24-43
- [Hue77] G. P. Huet: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. FOCS 1977: 30-45
- [LMG22] S. Lucas, M. Vítores, R. Gutiérrez. Proving and
disproving confluence of context-sensitive rewriting. J. Log. Algebraic
Methods Program. 126: 100749 (2022)
- [Luc96] S. Lucas: Context-Sensitive Computations in Confluent Programs. PLILP 1996: 408-422
- [Ohl02] E. Ohlebusch: Advanced topics in term rewriting. Springer 2002, ISBN 978-0-387-95250-5, pp. I-XV, 1-414