TY - GEN
T1 - Equivalence, and Property Internalization and Preservation for Equational Programs
AU - Meseguer, José
N1 - I thank the reviewers for their excellent comments and suggestions. Work partially supported under NRL contract N0017323C2002.
PY - 2024
Y1 - 2024
N2 - An equational theory E=(Σ,E∪B) is an equational program if its equations E, oriented as rewrite rules E→, are ground convergent modulo axioms B. Its properties are the inductive theorems of the initial algebra TΣ/E∪B defined by (Σ,E∪B). Since programs are structured in module hierarchies, checkable syntactic conditions are given to preserve program properties up and/or down such hierarchies. Two equational programs E=(Σ,E∪B) and E′=(Σ,E′∪B′) are equivalent iff they define the same computable functions on the same algebraic data types. Succinct conditions to verify E and E′ equivalent are given. A useful internalization method to extend an equational program E into an equivalent one by adding new rewrite rules or structural axioms that are inductive theorems of E is also given. This method can make proofs of program properties simpler and shorter, and offers a new way to prove equational theories ground convergent.
AB - An equational theory E=(Σ,E∪B) is an equational program if its equations E, oriented as rewrite rules E→, are ground convergent modulo axioms B. Its properties are the inductive theorems of the initial algebra TΣ/E∪B defined by (Σ,E∪B). Since programs are structured in module hierarchies, checkable syntactic conditions are given to preserve program properties up and/or down such hierarchies. Two equational programs E=(Σ,E∪B) and E′=(Σ,E′∪B′) are equivalent iff they define the same computable functions on the same algebraic data types. Succinct conditions to verify E and E′ equivalent are given. A useful internalization method to extend an equational program E into an equivalent one by adding new rewrite rules or structural axioms that are inductive theorems of E is also given. This method can make proofs of program properties simpler and shorter, and offers a new way to prove equational theories ground convergent.
UR - http://www.scopus.com/inward/record.url?scp=85201127952&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85201127952&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-65941-6_4
DO - 10.1007/978-3-031-65941-6_4
M3 - Conference contribution
AN - SCOPUS:85201127952
SN - 9783031659409
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 62
EP - 83
BT - Rewriting Logic and Its Applications - 15th International Workshop, WRLA 2024, Revised Selected Papers
A2 - Ogata, Kazuhiro
A2 - Martí-Oliet, Narciso
PB - Springer
T2 - 15th International Workshop on Rewriting Logic and Its Applications, WRLA 2024
Y2 - 6 April 2024 through 7 April 2024
ER -