Admissible functional modules

The nonexec attribute allows us to include arbitrary equations or memberships, conditional or not, in a functional module and likewise in a functional theory (see Section 6.3.1). Any such statement is then disregarded for purposes of execution by the Maude engine: it can only be used in a controlled way at the metalevel. But what about all the other statements? That is, what requirements should be imposed on executable equations and memberships so that they can be given an operational interpretation and can be executed by the Maude engine?

The intuitive idea is that we want to use such equations as simplification rules from left to right to reach a single final result or canonical form. For this purpose, the executable equations and memberships (that is, all statements not having the nonexec attribute) should be Church-Rosser and terminating (modulo the equational attributes declared in the module) in the sense explained in Section 4.7 below. This guarantees that, given a term $t$, all chains of equational simplification using those equations and memberships end in a unique canonical form (again, modulo the equational attributes). Furthermore, under the preregularity assumption (see Section 3.8), such a canonical form has the smallest sort possible in the subsort ordering.

The traditional requirement in this context is that, given a conditional equation^4.12 the set of variables appearing in $t$ contains those appearing in both $t'$ and in the conditions $C_{i}$. In Maude, this requirement is relaxed to support matching equations in conditions (see Section 4.3) which can introduce new variables not present in $t$. Specifically, all executable conditional equations in a Maude functional module M have to satisfy the following admissibility requirements, ensuring that all the extra variables will become instantiated by matching:

1. 
   
   $$\displaystyle{\mathit{vars}(t') \subseteq \mathit{vars}(t) \cup \bigcup_{j=1}^{n} \mathit{vars}(C_j).}$$
   
   

2. If $C_i$ is an equation $u_i = u'_i$ or a membership $u_i : s$, then
   
   $$\mathit{vars}(C_i) \subseteq \mathit{vars}(t) \cup \bigcup_{j=1}^{i-1} \mathit{vars}(C_j).$$
   
   

3. If $C_i$ is a matching equation $u_i:= u'_i$, then $u_i$ is an M-pattern and
   
   $$\mathit{vars}(u'_i) \subseteq \mathit{vars}(t) \cup \bigcup_{j=1}^{i-1} \mathit{vars}(C_j).$$
   
   

In a similar way, all executable conditional memberships must satisfy conditions 2-3 above.

In summary, therefore, we expect all executable equations and memberships in a functional module (and also in a system module) to be Church-Rosser and terminating (see Section 4.7 below, and [7, Section 10.1]) and to satisfy the above admissibility requirements.