Maude Specifications as Equational Generalized Term Rewriting Systems: Functional Modules

Abstract

Generalized Term Rewriting Systems (GTRSs) extend Conditional Term Rewriting Systems by considering replacement restrictions on selected arguments of function symbols and conditional rules whose conditional part may include not only a mix of the usual (reachability, joinability,...) conditions, but also atoms defined by a set of Horn clauses. Conditional equations can also be included as particular Horn clauses in GTRSs. However, in order to give them an appropriate treatment as specifications of \emph{equational theories} which can be used to define rewriting modulo computations, we have recently introduced Equational GTRSs (EGTRSs). This paper shows that EGTRSs can often be used to simulate computations described by Maude functional modules. In this way, existing confluence and termination results (modulo) for \gtrs{s} and EGTRSs can be used to prove computational properties of Maude programs.