Equivalence, and Property Internalization and Preservation for Equational Programs

An equational theory \(\mathcal {E}=(\varSigma , E \cup B)\) is an equational program if its equations E, oriented as rewrite rules \(\vec{E}\) , are ground convergent modulo axioms B. Its properties are the inductive theorems of the initial algebra \(\mathbb {T}_{\varSigma /E \cup B}\) defined by \((\varSigma , E \cup 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 \(\mathcal {E}=(\varSigma , E \cup B)\) and \(\mathcal {E}'=(\varSigma , E' \cup B')\) are equivalent iff they define the same computable functions on the same algebraic data types. Succinct conditions to verify \(\mathcal {E}\) and \(\mathcal {E}'\) equivalent are given. A useful internalization method to extend an equational program \(\mathcal {E}\) into an equivalent one by adding new rewrite rules or structural axioms that are inductive theorems of \(\mathcal {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.