TY - GEN
T1 - Order-sorted equality enrichments modulo axioms
AU - Gutiérrez, Raúl
AU - Meseguer, José
AU - Rocha, Camilo
N1 - Funding Information:
This work has been supported in part by NSF Grant CCF 09-05584, the “Programa de Apoyo a la Investigación y Desarrollo” (PAID-02-11) of the Universitat Politècnica de València, the EU (FEDER), the spanish MICINN/MINECO under Grant TIN2010-21062-C02 and by the Generalitat Valenciana, ref. PROMETEO/2011/052.
PY - 2012
Y1 - 2012
N2 - Built-in equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications with initial algebra semantics beyond the pale of theorem proving tools based, for example, on explicit or inductionless induction techniques, and of other formal tools for checking key properties such as confluence, termination, and sufficient completeness. Such specifications would instead be amenable to formal analysis if an equationally-defined equality predicate enriching the algebraic data types were to be added to them. Furthermore, having an equationally-defined equality predicate is very useful in its own right, particularly in inductive theorem proving. Is it possible to effectively define a theory transformation ε → ε ≃ that extends an algebraic specification ε to a specification ε ≃ having an equationally-defined equality predicate? This paper answers this question in the affirmative for a broad class of order-sorted conditional specifications ε that are sort-decreasing, ground confluent, and operationally terminating modulo axioms B and have a subsignature of constructors. The axioms B can consist of associativity, or commutativity, or associativity-commutativity axioms, so that the constructors are free modulo B. We prove that the transformation ε → ε ≃ preserves all the just-mentioned properties of ε. The transformation has been automated in Maude using reflection and is used in several Maude formal tools.
AB - Built-in equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications with initial algebra semantics beyond the pale of theorem proving tools based, for example, on explicit or inductionless induction techniques, and of other formal tools for checking key properties such as confluence, termination, and sufficient completeness. Such specifications would instead be amenable to formal analysis if an equationally-defined equality predicate enriching the algebraic data types were to be added to them. Furthermore, having an equationally-defined equality predicate is very useful in its own right, particularly in inductive theorem proving. Is it possible to effectively define a theory transformation ε → ε ≃ that extends an algebraic specification ε to a specification ε ≃ having an equationally-defined equality predicate? This paper answers this question in the affirmative for a broad class of order-sorted conditional specifications ε that are sort-decreasing, ground confluent, and operationally terminating modulo axioms B and have a subsignature of constructors. The axioms B can consist of associativity, or commutativity, or associativity-commutativity axioms, so that the constructors are free modulo B. We prove that the transformation ε → ε ≃ preserves all the just-mentioned properties of ε. The transformation has been automated in Maude using reflection and is used in several Maude formal tools.
UR - http://www.scopus.com/inward/record.url?scp=84868330084&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84868330084&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-34005-5_9
DO - 10.1007/978-3-642-34005-5_9
M3 - Conference contribution
AN - SCOPUS:84868330084
SN - 9783642340048
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 162
EP - 181
BT - Rewriting Logic and Its Applications - 9th International Workshop, WRLA 2012, Held as a Satellite Event of ETAPS, Revised Selected Papers
T2 - 9th International Workshop on Rewriting Logic and Its Applications, WRLA 2012, Held as a Satellite Event of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012
Y2 - 24 March 2012 through 25 March 2012
ER -