TY - JOUR

T1 - Order-sorted equality enrichments modulo axioms

AU - Gutiérrez, Raúl

AU - Meseguer, José

AU - Rocha, Camilo

N1 - Publisher Copyright:
© 2014 Elsevier B.V. All rights reserved.
Copyright:
Copyright 2015 Elsevier B.V., All rights reserved.

PY - 2015/3/1

Y1 - 2015/3/1

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 EE∼ that extends an algebraic specification E to a specification E∼ having an equationally-defined equality predicate? This paper answers this question in the affirmative for a broad class of order-sorted conditional specifications E 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 EE∼ preserves all the just-mentioned properties of E. The transformation has been automated in Maude using reflection and is used as a component in many 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 EE∼ that extends an algebraic specification E to a specification E∼ having an equationally-defined equality predicate? This paper answers this question in the affirmative for a broad class of order-sorted conditional specifications E 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 EE∼ preserves all the just-mentioned properties of E. The transformation has been automated in Maude using reflection and is used as a component in many Maude formal tools.

KW - Algebraic specifications

KW - Equality predicate

KW - Initial algebra semantics

KW - Maude

KW - Order-sorted equational logic modulo axioms

UR - http://www.scopus.com/inward/record.url?scp=84919875540&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84919875540&partnerID=8YFLogxK

U2 - 10.1016/j.scico.2014.07.003

DO - 10.1016/j.scico.2014.07.003

M3 - Article

AN - SCOPUS:84919875540

VL - 99

SP - 235

EP - 261

JO - Science of Computer Programming

JF - Science of Computer Programming

SN - 0167-6423

ER -