Matching and equational simplification

Although this section and the next are quite technical, and it may be possible to skip them in a first reading, they introduce the concepts of matching and equational simplification that are essential to understand how Maude works. Therefore, we advise the reader to come back to them as needed to gain a better understanding of those concepts.

Recall from Section 4.3 that a functional module defines an equational theory $(\Sigma,E\cup A)$ in membership equational logic, with $A$ the equations specified as equational attributes in operators (see Section 4.4.1), and $E$ the (possibly conditional) equations and memberships specified as statements.

Ground terms in the signature $\Sigma$ form a $\Sigma$-algebra denoted $T_{\Sigma}$. Similarly, equivalence classes of terms modulo $E\cup A$ define the $\Sigma$-algebra denoted $T_{\Sigma/E \cup A}$, which is the initial model for the theory $(\Sigma,E\cup A)$ specified by the module [60].

Given a set $X$ of variables, we can add them to the signature $\Sigma$ as new constants, and get in this way a term algebra $T_{\Sigma}(X)$ where now the terms may have variables in $X$.

Given a set $X$ of variables, each having a given kind, a (ground) substitution is a kind-preserving function $\sigma : X \longrightarrow T_{\Sigma}$. Such substitutions may be used to represent assignments of terms in $T_{\Sigma}$ to the variables in $X$, and also assignments of elements in $T_{\Sigma/E \cup A}$ to such variables by $\sigma$ picking up a representative of the corresponding $E\cup A$-equivalence class. For example, a very natural choice is to assign to each $x$ in $X$ a term $\sigma(x)$ which is in canonical form according to $E\cup A$. Furthermore, under the preregularity, Church-Rosser, and termination assumptions (more on this below) this canonical form will have a least sort. Therefore, we may allow each variable $x$ in $X$ to have either a kind or a sort assigned to it, and can call the substitution $\sigma$ well-sorted relative to $E\cup A$ if the least sort of $\sigma(x)$ is smaller or equal to that of $x$. By substituting terms for variables (as indicated by $\sigma$) in the usual way, a substitution $\sigma : X \longrightarrow T_{\Sigma}$ is extended to a homomorphic function on terms $\sigma : T_{\Sigma}(X) \longrightarrow T_{\Sigma}$ that we denote with the same name.

Given a term $t \in T_{\Sigma}(X)$, corresponding to the lefthand side of an oriented equation, and a subject ground term $u \in T_{\Sigma}$, we say that $t$ matches^4.13 $u$ if there is a substitution $\sigma$ such that $\sigma(t) \equiv u$, that is, $\sigma(t)$ and $u$ are syntactically equal terms.

For an oriented $\Sigma$-equation $l = r$ to be used in equational simplification, it is required that all variables in the righthand side $r$ also appear among the variables of the lefthand side $l$. In the case of a conditional equation $l = r \; \textit{if} \; cond$, this requirement is relaxed, so that more variables can appear in the condition $cond$, provided that they are introduced by matching equations according to the admissibility requirements in Section 4.6; then the variables in the righthand side $r$ must be among those in the lefthand side $l$ or in the condition $cond$. Under this assumption, given a theory $(\Sigma, E)$ a term $t$ rewrites to a term $t'$ using such an equation if there is a subterm $t\vert _{p}$ of $t$ at a given position^4.14$p$ of $t$ such that $l$ matches $t\vert _{p}$ via a well-sorted substitution^4.15 $\sigma$ and $t'$ is obtained from $t$ by replacing the subterm $t\vert _{p} \equiv \sigma(l)$ with the term $\sigma(r)$. In addition, if the equation has a condition $cond$, the substitution $\sigma$ must make the condition provably true according to the equations and memberships in $E$, which are assumed to be Church-Rosser and terminating and are used also from left to right to try to simplify the condition. Note that, in general, the variables instantiated by $\sigma$ must contain both those in the lefthand side, and those in the condition (which are incrementally matched using the matching equations).

We denote this step of equational simplification by $t \rightarrow_E t'$, where the possible equations for rewriting are chosen in the set $E$. The reflexive and transitive closure of the relation $\rightarrow_E$ is denoted $\rightarrow^\ast_E$.

In many texts, equational simplification is also called (equational) rewriting but, since in Maude we have two very different types of rewriting, rewriting with equations in functional modules, and rewriting with rules in system modules, each with a completely different semantics, to avoid confusion we favor the terminology of equational simplification for the process of rewriting with equations.

A set of equations $E$ is confluent when any two rewritings of a term can always be unified by further rewriting: if $t \rightarrow^\ast_E t_1$ and $t \rightarrow^\ast_E t_2$, then there exists a term $t'$ such that $t_1 \rightarrow^\ast_E t'$ and $t_2 \rightarrow^\ast_E t'$. This is summarized in Figure 4.1.

Figure 4.1: Confluence diagram

A set of equations $E$ is terminating when there is no infinite sequence of rewriting steps

$$t_0 \rightarrow_E t_1 \rightarrow_E t_2 \rightarrow_E \ldots$$

If $E$ is both confluent and terminating, a term $t$ can be reduced to a unique canonical form $t \!\downarrow_E$, that is, to a unique term that can no longer be rewritten. Therefore, in order to check semantic equality of two terms $t=t'$ (that is, that they belong to the same equivalence class), it is enough to check that their respective canonical forms are equal, $t \!\downarrow_E \; = t' \!\downarrow_E$, but, since canonical forms cannot be rewritten anymore, the last equality is just syntactic coincidence: $t \!\downarrow_E \; \equiv t' \!\downarrow_E$.

In membership equational theories a third important property is sort decreasingness. Intuitively, this means that, assuming $E$ is confluent and terminating, the canonical form $t \!\downarrow_E$ of a term $t$ by the equations $E$ should have the least sort possible among the sorts of all the terms equivalent to it by the equations $E$; and it should be possible to compute this least sort from the canonical form itself, using only the operator declarations and the memberships. By a Church-Rosser and terminating theory $(\Sigma, E)$ we precisely mean one that is confluent, terminating, and sort-decreasing. For a more detailed treatment of these properties, we refer the reader to the paper [7].

Since Maude functional modules have an initial algebra semantics, we are primarily interested in ground terms. Therefore, we can relax the above Church-Rosser and termination requirements by requiring that they just hold for ground terms, without losing the desired coincidence between the mathematical and operational semantics. In this way, we obtain notions of ground Church-Rosser, terminating, confluent, etc. specifications. In practice, some perfectly reasonable Maude functional modules are ground confluent, but fail to be confluent. This however is not a problem, since ground confluence (together with ground termination) is just what is needed to ensure uniqueness of canonical forms. Indeed, under the ground Church-Rosser and termination assumptions, it is easy to prove that we have the desired isomorphism

$$T_{\Sigma/E} \cong \mathit{Can}_{\Sigma/E}$$

ensuring the coincidence between the mathematical semantics of $(\Sigma, E)$ provided by the initial algebra $T_{\Sigma/E}$, and its operational semantics by equational simplification provided by the algebra $\mathit{Can}_{\Sigma/E}$ of canonical forms.

Equational specifications $(\Sigma, E)$ in Maude functional modules (and in the equational part of system modules), are assumed to be ground Church-Rosser and terminating up to the context-sensitive strategy specified by the evaluation strategies declared for the operators in $\Sigma$ (see Section 4.4.7). More precisely, we can view the information about operator evaluation strategies as a function $\mu$ that assigns to each operator $f \in \Sigma$ with $n$ argument sorts a string of numbers indicating the argument positions to be evaluated and ended with a $0$ (that is, the information given in the operator's strat attribute, or, if no such information is given, the string $1 \ldots n 0$). This then defines a more restricted rewrite relation $\rightarrow_{E}^{\mu}$ where we can only rewrite in subterms in positions that can be evaluated according to $\mu$. If the relation $\rightarrow_{E}^{\mu}$ is (ground) confluent, we call the specification (ground) $\mu$-confluent; similarly, if $\rightarrow_{E}^{\mu}$ is (ground) terminating, we call it (ground) $\mu$-terminating. We define the concepts of (ground) $\mu$-sort-decreasing and (ground) $\mu$-Church-Rosser in the same way. When we talk about the specification being ``ground Church-Rosser and terminating up to the context-sensitive strategy specified by the evaluation strategies,'' we exactly mean that it is ground $\mu$-Church-Rosser and ground $\mu$-terminating. Of course, when no such strategies are declared, this specializes to the usual notions of ground Church-Rosser and ground terminating. Under the ground $\mu$-Church-Rosser and ground $\mu$-terminating assumptions, the $\mu$-canonical forms define a canonical term algebra $Can_{\Sigma/E}^{\mu}$ (see [45]), which provides a perfect mathematical model for the module's operational semantics, since its elements are the values that the user gets when evaluating expressions in such a module. The question then arises: how is this model related to the module's mathematical semantics? In general, the quotient map $t \mapsto [t]_{E}$ sending each $\mu$-canonical form to its $E$-equivalence class is a surjective homomorphism

$$q: Can_{\Sigma/E}^{\mu} \longrightarrow T_{\Sigma/E},$$

but not necessarily an isomorphism. If $q$ fails to be an isomorphism, this means that $\mu$-rewriting is a sound deductive method for proving $E$-equalities, but it is incomplete. Therefore we call the specification $\mu$-semantically complete iff $q$ is an isomorphism. $\mu$-semantic completeness therefore expresses the complete agreement between the mathematical and operational semantics of the module. Specifications where evaluation strategies are used mainly for efficiency and/or termination purposes, that is, those where the execution becomes more efficient by avoiding wasteful computation in unnecessary parts of the term and/or that would not terminate without the strategy restrictions are typically $\mu$-semantically complete. Instead, specifications such as the sieve of Eratosthenes in Section 4.4.7, where the main intent is to compute with infinite data structures in a lazy way, are typically $\mu$-semantically incomplete. Not all is lost in this second case: we still have a good mathematical model associated to our specification, namely, $Can_{\Sigma/E}^{\mu}$, but this is a more concrete model than $T_{\Sigma/E}$, that is, one in which fewer elements are identified.

What are the appropriate notions when we have a theory of the form $(\Sigma,E\cup A)$? Then matching must be defined modulo the equational axioms $A$, and all the above concepts, including those for $\mu$-rewriting, must be generalized to equational simplification, confluence, and termination modulo $A$. We discuss this in more detail in Section 4.8 below. See also [45] for a detailed treatment of $\mu$-rewriting and $\mu$-semantic completeness modulo axioms $A$.

As already mentioned, the operational semantics of functional modules is equational simplification, that is, equational rewriting of terms until a canonical form is obtained in the sense explained above. Notice that the system does not check the ground confluence and termination properties: they are left to the user's responsibility. However, in some cases it is possible to check these properties with Maude's Church-Rosser checker and termination tools [17,30,29]. Similar checkings are also possible for functional modules with evaluation strategies; for example, the Maude's MTT termination tool can check $\mu$-termination (also called context-sensitive termination [51]). Moreover, although the relations between the standard Church-Rosser property and the $\mu$-Church-Rosser property are somewhat subtle [50,52], the work in [45] shows how one can use standard tools in conjunction with Maude's Sufficient Completeness Checker [46] to check both the $\mu$-Church-Rosser property and $\mu$-semantic completeness. See Section 9.4 for some examples of the use of these formal tools.