2 Preliminaries

Let $\Sigma$ be a signature that includes typed operators (also called function symbols) of the form $f\colon s_1\ldots s_m\to s$ , where $s_i$ , for $i=1,\ldots n$ , and s are sorts in a poset $(S,<)$ that models subsort relations (e.g., $s < s'$ means that sort s is a subsort of s’). The connected components of ${(S, <)}$ are the equivalence classes corresponding to the least equivalence relation $\equiv_{<}$ containing ${<}$ . As usual in RWL (Alpuente et al. Reference Alpuente, Escobar, Espert and Meseguer2014b), we assume kind-complete ^{Footnote 6} signatures such that: each connected component in the poset $(S,<)$ has a top sort (also called kind), and, for each ${s}\in{S}$ , we denote by $[{s}]$ the top sort in the connected component of s (i.e., if s and s’ are sorts in the same connected component, then $[{s}]=[{s'}]$ ); and (ii) for each operator declaration $f: {s}_1 \times \ldots \times {s}_n \rightarrow {s}$ in $\Sigma$ , there is also a declaration $f: [{s}_1] \times \ldots \times [{s}_n] \rightarrow [{s}]$ in $\Sigma$ . Binary operators in $\Sigma$ may have an axiom declaration attached that specifies any combinations of algebraic laws such as associativity (A), commutativity (C), identity (U), left identity ( $U_l$ ), and right identity ( $U_r$ ). We use strings over the alphabet $\{A,C,U,U_l,U_r\}$ to indicate the combinations of axioms satisfied by an operator f. By ax(f), we denote the set of algebraic axioms for the operator f.

We consider an S-sorted family $\mathcal{X} = \{\mathcal{X}_s\}_{s \in S}$ of disjoint variable sets. ${{\cal T}^{}_{{\Sigma,{{s}}}}({\mathcal{X}})}_{}^{}$ and $\mathcal{T}_{{\Sigma},s}$ are the sets of terms and ground terms of sort s, respectively. By $\mathcal{T}_{{\Sigma}}(\mathcal{X})=\bigcup_{s\in S} {{\cal T}^{}_{{\Sigma,{s}}}({\mathcal{X}})}_{}^{}$ , we denote the usual non-ground term algebra built over $\Sigma$ and the variables in $\mathcal{X}$ . By $\mathcal{T}_{\Sigma}=\bigcup_{s\in S} \mathcal{T}_{{\Sigma},s}$ , we denote the ground term algebra over $\Sigma$ . By notation $x:s$ , we denote a variable x with sort s. The set of variables that appear in a term t is denoted by Var(t).

We assume pre-regularity of the signature $\Sigma$ : for each operator declaration $f\colon s_1\ldots s_m\to s$ , and for the set $S_f$ containing all sorts s’ that appear in operator declarations of the form : $f\colon s'_1\ldots s'_m\to s'$ in $\Sigma$ such that $s_i < s'_i$ for $1 \leq i \leq m$ , then the set $S_f$ has a least sort. Given a term $t\in\mathcal{T}_{{\Sigma}}(\mathcal{X})$ , ls(t) denotes the least sort of t in the poset $(S,<)$ . An expression $\overline{t_n}$ denotes a finite sequence of terms $t_1\ldots t_n$ , $n\geq 0$ . A position w in a term t is represented by a sequence of natural numbers that addresses a subterm of t ( $\Lambda$ denotes the empty sequence, i.e., the root position). Given a term t, we let Pos(t) denote the set of positions of t. We denote the usual prefix preorder over positions by $\leq$ . By $t_{|w}$ , we denote the subterm of t at position w. By root(t), we denote the operator of t at position $\Lambda$ .

A substitution $\sigma$ is a sorted mapping from a finite subset of $\mathcal{X}$ to ${{\cal T}^{}_{{\Sigma}}({\mathcal{X}})}_{}^{}$ . Substitutions are written as $\sigma=\{X_1 \mapsto t_1,\ldots,X_n \mapsto t_n\}$ . The identity substitution is denoted by id. Substitutions are homomorphically extended to ${{\cal T}^{}_{{\Sigma}}({\mathcal{X}})}_{}^{}$ . The application of a substitution $\sigma$ to a term t is denoted by $t\sigma$ . The restriction of $\sigma$ to a set of variables $V \subset \mathcal{X}$ is denoted ${\sigma}_{|{V}}$ . Composition of two substitutions is denoted by $\sigma\sigma'$ so that $t(\sigma\sigma')=(t\sigma)\sigma'$ .

A $\Sigma$ -equation (or simply equation, where $\Sigma$ is clear from the context) is an unoriented pair $\lambda = \rho$ , where $\lambda,\rho \in {{\cal T}^{}_{{\Sigma,{s}}}({\mathcal{X}})}_{}^{}$ for some sort ${s}\in{S}$ , where ${{\cal T}^{}_{{\Sigma,{s}}}({\mathcal{X}})}_{}^{}$ is the set of terms of sort s built over $\Sigma$ and $\mathcal{X}$ . An equational theory $\mathcal{E}$ is a pair $(\Sigma,E\uplus B)$ that consists of a signature $\Sigma$ , a set E of $\Sigma$ -equations, and a set B of algebraic axioms (e.g., associativity, commutativity, and/or identity) that are expressed by means of equations for some binary operators in $\Sigma$ . The equational theory $\mathcal{E}$ induces a congruence relation $=_{ {\mathcal{E}}}$ on ${{\cal T}^{}_{{\Sigma}}({\mathcal{X}})}_{}^{}$ .

A term t is more general than (or at least as general as) t’ modulo $\mathcal{E}$ , denoted by $t \leq_{\mathcal{E}} t'$ , if there is a substitution $\gamma$ such that $t' =_\mathcal{E} t\gamma$ . We also define $t \simeq_{\mathcal{E}} t'$ iff $t \leq_{\mathcal{E}} t'$ and $t' \leq_{\mathcal{E}} t$ . By abuse of notation, we write $\leq_B$ and $\simeq_B$ when B is an axiom set.

A substitution $\theta$ is more general than (or at least as general as) $\sigma$ modulo $\mathcal{E}$ , denoted by $\theta \leq_{\mathcal{E}} \sigma$ , if there is a substitution $\gamma$ such that $\sigma =_\mathcal{E} \theta\gamma$ , i.e., for all $x \in \mathcal{X}, x\sigma =_{\mathcal{E}} x\theta\gamma$ . Also, $\theta \leq_{\mathcal{E}} \sigma \ [V]$ iff there is a substitution $\gamma$ such that, for all $x \in V, ~x\sigma =_{\mathcal{E}} x\theta\gamma$ .

An $\mathcal{E}$ -unifier for a $\Sigma$ -equation $t = t'$ is a substitution $\sigma$ such that $t\sigma =_\mathcal{E} t'\sigma$ .

We consider three different kinds of expressions that may appear in a conditional rewrite theory: (1) an equational condition, which is is any (ordinary ^{Footnote 7} ) equation $t=t'$ , with $t, t' \in {{\cal T}^{}_{{\Sigma,{s}}}({\mathcal{X}})}_{}^{}$ for some sort ${s}\in{S}$ ; (2) a matching condition, which is a pair $t:=t'$ , with $t, t' \in {{\cal T}^{}_{{\Sigma,{s}}}({\mathcal{X}})}_{}^{}$ for some sort ${s}\in{S}$ ; and (3) a rewrite expression, which is a pair $t \Rightarrow t'$ , with $t, t' \in {{\cal T}^{}_{{\Sigma,{s}}}({\mathcal{X}})}_{}^{}$ for some sort ${s}\in{S}$ . A conditional rule is an expression of the form $\lambda \Rightarrow \rho\ \mathit{if}\ C$ , where $\lambda,\sigma\in{{\cal T}^{}_{{\Sigma,{s}}}({\mathcal{X}})}_{}^{}$ for some sort ${s}\in{S}$ , and C is a (possibly empty, with identity symbol $\mathit{nil}$ ) sequence $c_1 \wedge\ldots \wedge c_n$ , where each $c_i$ is an equational condition, a matching condition, or a rewrite expression. Conditions are evaluated ^{Footnote 8} from left to right, and therefore the order in which they appear, although mathematically inessential, is operationally important. When the condition C is empty, we simply write $\lambda \Rightarrow \rho$ . A rewrite theory is a triple $\mathcal{R} = (\Sigma,E\uplus B,R)$ , where $(\Sigma,E\uplus B)$ is an equational theory and R is a set of rewrite rules. A rewrite theory $(\Sigma,E\uplus B,R)$ is called topmost if there is a sort State such that: (i) for each rewrite rule $\lambda \Rightarrow \rho\ \mathit{if}\ C$ , $\lambda$ and $\rho$ are of sort State; and (ii) for each $f\colon [s_1]\ldots [s_n]\to s \in \Sigma$ and $i\in\{1,\ldots,n\}$ , $[s_i] \neq$ $\mathit{State}$ . ^{Footnote 9}

In a rewrite theory $\mathcal{R}=(\Sigma,E\uplus B, R)$ , computations evolve by rewriting states using the equational rewriting relation $\rightarrow_{R,\mathcal{E}}$ , which applies the rewrite rules in R to states modulo the equational theory $\mathcal{E}=(\Sigma, E\uplus B)$ (Meseguer Reference Meseguer1992a). The Maude interpreter implements equational rewriting $\rightarrow_{R,\mathcal{E}}$ by means of two simple relations, namely $\rightarrow_{\vec{E},B}$ and $\rightarrow_{R,B}$ . These allow rules and (oriented) equations to be intermixed in the rewriting process by simply using both an algorithm of matching modulo B. The relation $\rightarrow_{\vec{E},B}$ uses $\vec{E}$ (the explicitly oriented version of the equations in E) for term simplification. Thus, for any term t, by repeatedly applying the equations as simplification rules, we eventually reach a term $t\!\downarrow_{\vec{E},B}$ to which no further equations can be applied. The term $t\!\downarrow_{\vec{E},B}$ is called canonical form (also called irreducible or normal form) of t w.r.t. $\vec{E}$ modulo B. On the other hand, the relation $\rightarrow_{R,B}$ implements rewriting with the rules of R, which might be nonterminating and nonconfluent, whereas $\mathcal{E}$ is required to be convergent (i,.e., $\rightarrow_{\vec{E},B}$ is terminating and confluent modulo B) and B-coherent (a kind of non-interference between E and B) in order to guarantee the existence and unicity (modulo B) of a canonical form w.r.t. $\vec{E}$ for any term. Also, the set R of rules must be coherent w.r.t. $\mathcal{E}$ , ensuring that any rewrite step with $\rightarrow_{R,B}$ can always be postponed in favor of deterministically rewriting with $\rightarrow_{\vec{E},B}$ .

Formally, for a set of rules P (with P being either R or $\vec{E}$ ), the rewriting relation $\rightarrow_{P,B}$ in P modulo B is defined as follows. Given a rewrite rule $r=(\lambda\Rightarrow\rho \mathit{\:if\:} C)\in P$ , a substitution $\sigma$ , a term t, and a position w of t, $t \stackrel{r,\sigma,w}{\rightarrow}_{\!\!P,B} t'$ iff $\lambda\sigma =_B t_{|w}$ , $t'=t[\rho\sigma]_w$ , and C holds (the specific evaluation strategy for rule conditions of Maude can be found in (Clavel et al. Reference Clavel, Durán, Eker, Lincoln, Martí-Oliet, Meseguer and Talcott2007)). When no confusion arises, we simply write $t \rightarrow_{P,B} t'$ instead of $t \stackrel{r,\sigma,w}{\rightarrow}_{\!\!P,B} t'$ .

Under these conditions, a $(R,E\uplus B)$ -rewrite step $\rightarrow_{R,E\uplus B}$ on a term t in the rewrite theory $\mathcal{R}=(\Sigma,E\uplus B,R)$ can be implemented by applying the following rewrite strategy: (i) reduce t w.r.t. $\rightarrow_{\vec{E},B}$ to the canonical form $t\!\downarrow_{\vec{E},B}$ ; and (ii) rewrite $t\!\downarrow_{\vec{E},B}$ w.r.t. $\rightarrow_{R,B}$ . This strategy is still complete in the sense that, rewriting of congruence classes induced by $=_\mathcal{E}$ , with $\mathcal{E}=(\Sigma,E\uplus B)$ , can be mimicked by $(R,E\uplus B)$ -rewrite steps.

A rewrite sequence $t \rightarrow_{R,\mathcal{E}}^{*} t'$ in the rewrite theory $\mathcal{R}=(\Sigma,E\uplus B,R)$ is then deployed as the (possibly infinite) rewrite sequence (with $t_{0}=t$ and $t_n\!\!\downarrow_{\vec{E},B}= t'$ )

\begin{equation*}t_0\rightarrow_{\vec{E},B}^*t_0\!\!\downarrow_{\vec{E},B}\: \rightarrow_{R,B} t_1\rightarrow_{\vec{E},B}^*t_1\!\!\downarrow_{\vec{E},B}\rightarrow_{R,B}\ldots \rightarrow_{R,B} t_n\!\!\downarrow_{\vec{E},B} \end{equation*}

that interleaves $\rightarrow_{\vec{E},B}$ rewrite steps and $\rightarrow_{R,B}$ rewrite steps following the strategy mentioned above. Note that, after each rewrite step using $\rightarrow_{R,B}$ , generally the resulting term $t_{i}$ , $i=1,\ldots, n$ , is not in canonical form and is thus normalized before the subsequent rewrite step using $\rightarrow_{R,B}$ is performed. Also, in the precise strategy adopted by Maude, the last term of a finite computation is finally normalized before the result is delivered.

2.1 Concurrent object-oriented specifications: a communication protocol model with Caesar ciphering

Rewrite theories provide a natural computation model for concurrent object-oriented systems (Meseguer Reference Meseguer1992a). Indeed, Maude fully supports the object-oriented programming paradigm by means of pre-defined data structures that identify the main building blocks of this paradigm such as classes, objects, and messages (Clavel et al. Reference Clavel, Durán, Eker, Escobar, Lincoln, Martí-Oliet, Meseguer, Rubio and Talcott2020). The essential facts about concurrent object-oriented configurations are all formalized in the CONFIGURATION module, which provides special notation and avoids boilerplate class declarations. More specifically, the sorts Oid and Cid respectively define object and class identifiers, while the sort Msg represents messages (which are typically used to model object communication). It is worth noting that class names are just sorts. Therefore, class inheritance is directly supported by RWL order-sorted type structure. A subclass declaration is thus an expression of the form subsort C < C’ where C and C’ are two sorts representing object classes. Multiple inheritance is also supported, allowing a class C to be defined as a subsort of many several sorts (each of which represent a different class).

The PE framework that we define in this work is able to deal with objects that are represented as terms of the following form:

\begin{equation*}{< O\ :\ C\ |\ a_{1}\ :\ v_{1},~...~,~a_{n}\ :\ v_{n} >}\end{equation*}

where O is a term of sort Oid, C is a term of sort Cid, and $a_{1}\ :\ v_{1},\ldots, a_{n}\ :\ v_{n}$ is a list of attributes of sort Attribute, each consisting of an identifier $a_{i}$ followed by its respective value $v_{i}$ .

The concurrent state of an object-oriented system is a multiset (of sort Configuration) of objects and messages that are built using the empty syntax (juxtaposition) ACU operator _ _ : Configuration Configuration $\to$ Configuration whose identity is none. Thus, an object-oriented configuration will be either none (empty configuration) or $Ob_1\ \dots\ Ob_k\ Mes_1\ \ldots\ Mes_n$ , where $Ob_1$ , …, $Ob_k$ are objects, and $Mes_1$ ,…, $Mes_n$ are messages.

Transitions between object-oriented configurations are specified by means of rewrite rules of the form

\begin{equation*}Ob_1\ \dots\ Ob_k\ Mes_1\ \ldots\ Mes_n \Rightarrow Ob'_1\ \dots\ Ob'_j\ Ob_{k+1}\ \dots\ Ob_{m}\ Mes'_1\ \ldots\ Mes'_p\ if\ Cond .\end{equation*}

where $Ob'_1\ \dots\ Ob'_j$ are updated versions of $Ob_1\ \dots\ Ob_j$ for $j\leq k$ , $Ob_{k+1}\ \dots\ Ob_{m}$ are newly created objects, $Mes'_1\ \ldots\ Mes'_p$ are new messages, and Cond is a rule condition.

An important special case are rules with a single object and at most one message on the left-hand side. These rules directly model asynchronous distributed interactions. Rules involving multiple objects are called synchronous and are used to model higher-level communication abstractions.

Example 1 Let us consider a rewrite theory $\mathcal{R}=(\Sigma,E\uplus B,R)$ that encodes an object-oriented ^{Footnote 10} specification for a client-server communication protocol in an asynchronous medium where messages can arrive out-of-order. The theory signature $\Sigma$ includes several operators and sorts that model the protocol entities. The constant operators Cli and Serv (of respective sorts Client and Server) are used to specify two classes that respectively identify clients and servers. Both sorts inherit the class behavior of the built-in abstract class Cid via the subsort relations Client < Cid and Server < Cid.

Data exchanged between clients and servers is encoded as non-empty, associative sequences ${\tt s_1\ldots s_n}$ , where, for the sake of simplicity, each $\tt s_i$ is a term of sort Symbol in the alphabet {a,b,c}. We assume that Symbol is a subsort of Data; hence, any symbol is also a (one-symbol) data sequence.

Clients are represented as objects of the form

\begin{equation*}\tt<\ C\ :\ Cli\ |\ server\ :\ S\ ,\ data\ :\ M\ ,\ key\ :\ K\ ,\ status\ :\ V >\end{equation*}

where C is an object identifier for a client of the class Cli, S is the server object that C wants to communicate with, M is a piece of data representing a client request, K is a natural number (specified in Peano’s notation) that determines an encryption/decryption key for messages, and V is a constant value that models the client status. Initially, the status is set to the empty value mt, and it changes to success whenever a server acknowledges message reception.

Servers are simple objects of the form

\begin{equation*}\tt <\ S\ :\ Serv\ |\ key\ :\ K\ >\end{equation*}

where S is an object identifier for a server, and K is an encryption/decryption key.

Network packets are naturally modeled by object messages that can be exchanged between servers and clients. More specifically a network packet is a pair of the form Host <- CNT of sort Msg, where Host is a client or server recipient, and CNT specifies the packet content. Specifically, CNT is a term {H,M}, with H being the sender’s name and M being a data item that represents either a client request or a server response, expressed as a list of symbols in the alphabet {a,b,c}.

System states are represented by object-oriented configurations which may include clients, servers, and network packets.

The protocol dynamics is specified by the term rewriting system R in $\mathcal{R}$ of Figure 1. It consists of three rules, where clients and servers agree on a shared key $\tt K$ .

Fig. 1.

Rewrite rules for the client-server communication protocol.

More specifically, the rule $\tt req$ allows a client C to initiate a transmission request with a server S by sending the data item M that is encrypted by function enc(M,s(K)) using a positive client’s key s(K). Note that this rule is conditional and is enabled if and only if the key s(K) is less than the constant len, which represents the cardinality of the chosen alphabet of symbols. Furthermore, to initiate a client request, we require the satisfaction of the property enc(M,s(K)) = enc(enc(M,K),s(0)), which enforces an additive property on the enc function.

The rule reply lets the server $\tt S$ consume a client request packet S <- {C,M} by first decrypting the incoming data item M with the server key and then sending a response packet back to C that includes the decrypted request data. The rule rec successfully completes the data transmission between C and S whenever the server response packet C <- {S,M} includes a data item M that is equal to the initial client request message. In this case, the status of the client is changed from mt to success. Note that the transmission succeeds when the client and server use the same key K, as this guarantees that the client plain message M is equal to dec(enc(M,K),K) as required by the rec rule.

Encryption and decryption functionality is implemented by two functions (namely, enc(M,K) and dec(M,K)) that are specified by the equational theory $\mathcal{E}$ in $\mathcal{R}$ . The equational theory $\mathcal{E}$ implements a Caesar cipher with key K, which is a simple substitution ciphering where each symbol in the plaintext data item M is replaced by the symbol that appears K positions later in the alphabet (handled as the list a,b,c). The cipher is circular, i.e., it works modulo the cardinality of the alphabet. For instance, enc(a b,s(0)) delivers (b c), and dec(a b,s(0)) yields (c a). The equational theory $\mathcal{E}$ includes the equations ^{Footnote 11} in Figure 1.

3 A glimpse into narrowing-based symbolic computation in Maude

Similarly to rewriting modulo an equational theory $\mathcal{E}$ , where syntactic pattern-matching is replaced with matching modulo $\mathcal{E}$ (or $\mathcal{E}$ -matching), in narrowing modulo an equational theory, syntactic unification is replaced by equational unification (or $\mathcal{E}$ -unification).

Given a rewrite theory $\mathcal{R}=(\Sigma,E\uplus B, R)$ , with $\mathcal{E}=(\Sigma,E\uplus B)$ , the conditional narrowing ^{Footnote 12} relation $\leadsto_{R,\mathcal{E}}$ on ${{\cal T}^{}_{{\Sigma}}({\mathcal{X}})}_{}^{}$ is defined by $t \leadsto_{\sigma,p,R,\mathcal{E}} t'$ (or simply $t \leadsto_{R,\mathcal{E}} t'$ ) if and only if there is a non-variable position $p \in \mathit{Pos}_{\Sigma}({t})$ , a (renamed apart) rule $\lambda \Rightarrow \rho\ \mathit{if}\ C$ in R, and an $\mathcal{E}$ -unifier of ${t}_{|p}$ and $\lambda$ such that $t' = {t}[{\rho}]_{p}\sigma$ and condition $C\sigma$ holds (Aguirre et al. Reference Aguirre, Martí-Oliet, Palomino and Pita2014). Furthermore, we write $t \leadsto_{\sigma,p,r,\mathcal{E}} t'$ , when we want to highlight the rewrite rule r that has been used in the narrowing step. A term t is called $(R,\mathcal{E})$ -strongly irreducible (also called a rigid normal form (Alpuente et al. Reference Alpuente, Escobar and Iborra2009a)) iff there is no term u such that $t \leadsto_{\sigma,p,R,\mathcal{E}} u$ for any position p, which amounts to say that no subterm of t unifies modulo B with the left-hand side of any equation of E.

Narrowing derivations correspond to sequences $t_0~ \leadsto_{{{\sigma_{0},p_0,r_{0},B}}} {~t_1} ~ \leadsto_{{{\sigma_{1},p_1,r_{1},B}}} \ldots \leadsto_{{{\sigma_{n},p_{n-1},r_{n-1},B}}}~ t_n$ . The composition $\sigma_0 \sigma_1\ldots \sigma_{n-1}$ of all the unifiers along a narrowing sequence leading to $t_n$ (restricted to the variables of $t_0$ ) is called computed substitution.

The search space of all narrowing derivations for a term t in $\mathcal{R}=(\Sigma,E\uplus B, R)$ is represented as a tree-like structure called $(R,E\uplus B)$ -narrowing tree (or simply narrowing tree).

3.1 Two-level narrowing in Maude

A rewrite theory $\mathcal{R}=(\Sigma,E\uplus B, R)$ can be symbolically executed in Maude by using narrowing at two levels: (i) narrowing with oriented equations $\vec{E}$ (i.e., rewrite rules obtained by explicitly orienting the equations in E) modulo the axioms B; and (ii) narrowing with the (typically non-confluent and non-terminating) rules of R modulo $\mathcal{E}=(\Sigma,E\uplus B)$ .

Narrowing with $\vec{E}$ modulo B .

This form of narrowing is typically used for $\mathcal{E}$ -unification and it is implemented in Maude via the folding variant narrowing (or simply fV-narrowing) strategy of (Escobar et al. Reference Escobar, Sasse and Meseguer2012). fV-narrowing is centered around the notion of equational variant of a term. Given ${\cal E} = (\Sigma, E \uplus B)$ , the set of all pairs $(t',\sigma)$ , where t’ is $(t\sigma)\!\!\downarrow_{\vec{E},B}$ , i.e., the canonical form of $t\sigma$ for a substitution $\sigma$ , is called the set of equational variants (or simply variants) of a term t (Escobar et al. Reference Escobar, Sasse and Meseguer2012). Intuitively, the variants of t are the “irreducible patterns” to which t can be symbolically evaluated by applying $\vec{E}$ modulo B. A variant $(t,\sigma)$ is more general than a variant $(t',\sigma')$ w.r.t. an equational theory $\mathcal{E}$ (in symbols, $(t,\sigma)\leq_\mathcal{E} (t',\sigma')$ ) iff there exists a substitution $\gamma$ such that $t\gamma =_\mathcal{E} t'$ and $\sigma\gamma =_\mathcal{E} \sigma'$ .

An equational theory $\mathcal{E}$ has the finite variant property (FVP) (or $\mathcal{E}$ is called a finite variant theory) iff there is a finite, complete, and minimal set of most general equational variants for each term. It is generally undecidable whether an equational theory has the FVP (Bouchard et al. Reference Bouchard, Gero, Lynch and Narendran2013); a semi-decision procedure is given in (Meseguer Reference Meseguer2015) that works well in practice. The FVP can be semi-decided by checking whether there is a finite number of most general variants for all flat terms $f(X_1,\ldots,X_n)$ for any n-ary operator f in the theory and pairwise-distinct variables $X_1,\ldots,X_n$ (of the corresponding sort). For instance, the specification of the exclusive-or operator on natural numbers given by $E= \{N\oplus N = 0, N\oplus 0 = N \}$ , with $\oplus$ being commutative, is a finite variant theory, since the (flat) term $N\oplus M$ has four most general variants: $(N\oplus M, \{\})$ , $(M, \{N \mapsto 0\})$ , $(N, \{M \mapsto 0\})$ , and $(0, \{N \mapsto M\})$ . Instead, the specification of the auxiliary function d in Figure 1 does not satisfy the FVP, since the term d(X,Y) has an infinite number of most general variants ( ${\tt X}, \{{\tt Y} \mapsto 0\}$ ), (unshift(X), $\{{\tt Y} \mapsto {\tt s(0)}\}$ ), $\ldots$ , ( ${\tt unshift}^k{\tt (X)}$ , $\{{\tt Y} \mapsto {\tt s}^k{\tt (0)}\}$ ). Therefore, the equational theory of Example 1 does not have the FVP either.

The main idea of folding variant narrowing is to “fold” ^{Footnote 13} the $(\vec{E},B)$ -narrowing tree by subsumption modulo B. That is, folding variant narrowing shrinks the search space and avoids computing any variant that is a substitution instance modulo B of a more general variant.

A fV-narrowing derivation is a sequence $t_0~ \leadsto_{{{\sigma_{0},p_0,\vec{e}_{0},B}}} ~t_1 ~ \leadsto_{{{\sigma_{1},p_1,\vec{e}_{1},B}}}^{} \ldots \leadsto_{{{\sigma_{n},p_{n-1},\vec{e}_{n-1},B}}}~ t_n,$ where $ t \leadsto_{{{\sigma,p,\vec{e},B}}}~ t'$ (or simply $ t \leadsto_{{{\sigma}}}~ t'$ when no confusion can arise) denotes a transition (modulo the axioms B) from term t to t’ via the variant equation e (i.e., an oriented equation $\vec{e}$ that is enabled to be used for fV-narrowing thanks to the attribute variant) using the B-unifier $\sigma$ . Assuming that the initial term t is normalized, each step $ t \leadsto_{{{\sigma,p,\vec{e},B}}}~ t'$ (or folding variant narrowing step) is followed by the simplification of the term into its normal form by using all equations in the theory, which may include not only the variant equations in the theory but also (non-variant) equations (e.g., built-in equations in Maude). In order for finite variant narrowing to be effectively applicable the equational theory $\mathcal{E}=(\Sigma,E\uplus B)$ must be convergent, B-coherent, finite variant, and B-unification must be decidable.

Narrowing with R modulo $\mathcal{E}$ .

It is mainly used for solving reachability goals (Meseguer and Thati Reference Meseguer and Thati2007) and logical model checking (Escobar and Meseguer Reference Escobar and Meseguer2007).

Given a non-ground term t, t represents an abstract characterization of the (possibly) infinite set of all of the concurrent states $[\![t]\!]$ (i.e., all the ground substitution instances of t, or, more precisely, the $\mathcal{E}$ -equivalence classes associated to such ground instances) within $\mathcal{R}$ . In this scenario, each narrowing derivation $\mathcal{D}$ subsumes all of the rewrite computations that are “instances” of $\mathcal{D}$ modulo $\mathcal{E}$ (Clavel et al. Reference Clavel, Durán, Eker, Escobar, Lincoln, Martí-Oliet, Meseguer, Rubio and Talcott2020). Therefore, an exhaustive exploration of the $(R,E\uplus B)$ -narrowing tree of t allows one to prove existential reachability goals of the form

(2) \begin{equation}(\exists X)\; t \longrightarrow^{*} t'\end{equation}

with t and t’ being two (possibly) non-ground terms —called the input term and target term, respectively— and X being the set of variables appearing in both t and t’.

A solution for the reachability goal (2) in a rewrite theory $\mathcal{R}=(\Sigma,E\uplus B,R)$ , with $\mathcal{E}=(\Sigma, E\uplus B)$ , is a substitution $\sigma$ such that $t\sigma\rightarrow_{R,\mathcal{E}}^* t'\sigma$ ; thus, any computed substitution $\theta$ of a narrowing derivation $t\leadsto_{R,\mathcal{E}}^*t'$ is a solution for the reachability goal (2) since $t\theta\rightarrow_{R,\mathcal{E}}^* t'\theta$ .

In practice, solving a reachability goal $(\exists X)\; t \longrightarrow^{*} t'$ means searching for a symbolic solution within the $(R,E\uplus B)$ -narrowing tree that originates from t in a hopefully complete way (so that, for any existing solution, a more general answer modulo $\mathcal{E}$ will be found). Completeness of narrowing with R modulo $\mathcal{E}$ holds for topmost rewrite theories, provided that a finitary and complete $\mathcal{E}$ -unification algorithm exists ^{Footnote 14} .

We note that only rewrite rules with the narrowing attribute are used by $\leadsto_{R,\mathcal{E}}$ , while any rule without this attribute is only considered for rewriting modulo $\mathcal{E}$ . By $\mathit{att(r)}$ we denote the attributes ^{Footnote 15} associated with the rewrite rule r. For instance, in Example 1, rec and reply rules can be used by $\leadsto_{R,\mathcal{E}}$ , while req only supports rewriting modulo $\mathcal{E}$ , since ${\tt narrowing}\not\in \mathit{att({\tt req})}$ .

Unfortunately, not all the rewrite theories are topmost or admit finitary and complete $\mathcal{E}$ -unification. For instance, object-oriented specifications of Section 2.1 are typically non-topmost, since their rewrite rules might apply to inner state positions, thereby implementing local state changes. This fact may compromise the effectiveness of narrowing-based symbolic reachability, because existing solutions of a given reachability goal may be missed due to incompleteness of $\leadsto_{R,\mathcal{E}}$ . Let us see an example.

Example 2 Consider a simpler version of the client-server protocol given in Example 1, where the shared key K is set to a fixed value (for simplicity, s(0)) and messages consist of just one symbol. In this setting, we can greatly simplify the equational theory of Figure 1 into an equational theory $\mathcal{E}$ that only contains the encryption and decryption equations:

Note that $\mathcal{E}$ -unification can be performed by fV-narrowing, since $\mathcal{E}$ has the FVP (in contrast to the equational theory of Example 1, which did not have the FVP) and fV-narrowing executability conditions are met (in particular, $\mathcal{E}$ is convergent and B-unification is trivially decidable since $B=\emptyset$ ).

The protocol dynamics is implemented by the rewrite rules reply, rec, and req that are specified in Example 1. Such rules are clearly not topmost since they may be applied to (strict) fragments of an object-oriented configuration.

Now, consider the reachability goal G

\begin{align*}\exists {\tt S:Symbol}&\\&\mbox{ < Cli-A : Cli | server : Srv-A , data : S , key : s(0) , status : mt >}\\&\mbox{ < Srv-A : Serv | key : s(0) > (Srv-A <- \{ Cli-A , c \} )}\\& \longrightarrow^*\\&\mbox{ < Cli-A : Cli | server : Srv-A , data : S , key : s(0) , status : success > }\\&\mbox{ < Srv-A : Serv | key : s(0) > }\end{align*}

The goal admits the solution ${\tt \{S\mapsto b\}}$ and proves that the handshake between client Cli-A and server Srv-A succeeds when Cli-A sends the encrypted message c to Srv-A if the original unencrpyted data Q is equal to b.

Nonetheless, since completeness of the narrowing relation $\leadsto_{R,\mathcal{E}}$ is not ensured for rewrite theories that are not topmost, the solution ${\tt \{S\mapsto b\}}$ for G cannot be found. Indeed, executing G by means of the vu-narrow built-in Maude command, which implements narrowing-based reachability search in Maude, produces the following output:

3.2 Relaxing the topmost requirement for object-oriented specifications

Object-oriented specifications, albeit not topmost, fall into the more general category of topmost modulo Ax rewrite theories, for which the topmost property can be easily recovered by means of an automatic program transformation. Topmost modulo Ax rewrite theories are rewrite theories where Ax consists of any of the combinations of axioms ACU, $ACU_l$ , $ACU_r$ , AC, AU, $AU_l$ , $AU_r$ , or A for a given binary symbol $\otimes : \mathit{Config} \: \mathit{Config} \rightarrow \mathit{Config}$ of the signature. The operator $\otimes$ is used to build system configurations that obey the structural axioms of $\otimes$ given by Ax.

Definition 1 (topmost modulo rewrite theory) Let $\mathcal{R}=(\Sigma,E\uplus B,R)$ be a rewrite theory with a finite poset of sorts ${(S, <)}$ . Let $\mathit{Config}$ be a top sort in S, and let $\otimes : \mathit{Config}\:\mathit{Config}\to\mathit{Config} \in \Sigma$ be a binary operator that obeys a combination of associativity, commutativity, and/or identity axioms $Ax\in\{ACU, ACU_l, ACU_r, AC, AU, AU_l, AU_r, A\}$ .

The theory $\mathcal{R}$ is said to be topmost modulo Ax if

1. 1. for each rule $(\lambda\Rightarrow\rho\mbox{ if } C)$ in R, $\lambda$ and $\rho$ are terms of sort Config and C does not contain terms of sort ${s}$ such that its top sort $[{s}] =\mathit{Config}$ ;

2. 2. $\otimes$ is the only operator in $\Sigma$ whose arguments include a sort ${s}$ such that its top sort $[{s}] =\mathit{Config}$ .

The rewrite rules in R are also said to be topmost modulo Ax.

Example 3 The rewrite theory in Example 1 is topmost modulo ACU. To show this, it suffices to interpret the juxtaposition ACU operator _ _ : Configuration Configuration $\to$ Configuration, which is used to build object-oriented configurations, as the operator $\otimes : \mathit{Config}\:\mathit{Config}\to\mathit{Config}$ of Definition 1.

We are able to convert topmost modulo Ax rewrite theories into topmost theories automatically by means of the following solution-preserving theory transformation.

Definition 2 (topmost extension of $\mathcal{R}$ ) Let $\mathcal{R}=(\Sigma,E\uplus B,R)$ be a topmost modulo Ax rewrite theory and $Ax\in B$ . Let X, $X_1$ , and $X_2$ be variables of sort Config not occurring in either R or E. We define the topmost rewrite theory $\hat{\mathcal{R}}=(\hat{\Sigma},E\uplus B,\hat{R})$ where $\hat{\Sigma}$ extends $\Sigma$ by adding a new top sort State, and a new operator $\{\_ \} \colon \mathit{Config}\to\mathit{State}$ ; and $\hat{R}$ is obtained by transforming R according to Ax as follows. For each $(\lambda \Rightarrow \rho\ \mathit{if}\: C )\in R$

We call $\hat{\mathcal{R}}$ the topmost extension of $\mathcal{R}$ .

The topmost extension of a rewrite theory $\mathcal{R}$ preserves the rewriting semantics of $\mathcal{R}$ , as shown in the following proposition.

Proposition 3.1 (correctness and completeness of the topmost extension) Let $\mathcal{R}=(\Sigma,E\uplus B,R)$ , with $\mathcal{E}=(\Sigma, E\uplus B)$ , be a topmost modulo Ax theory and let $\hat{\mathcal{R}}$ be the topmost extension of $\mathcal{R}$ . For any terms $t_i$ and $t_f$ of sort $\mathit{Config}$ , $t_i\rightarrow_{R,\mathcal{E}}^{*}t_f$ iff $\{t_i\}\rightarrow_{\hat{R},\mathcal{E}}^{*}\{t_f\}$ .

The above proposition implies that the set of solutions of a reachability goal $G=(\exists X)\; t\longrightarrow^* t'$ in $\mathcal{R}$ is the same as the set of solutions of $\hat{G}=(\exists X)\; \{t\}\longrightarrow^* \{t'\}$ in the topmost extension $\hat{\mathcal{R}}$ of $\mathcal{R}$ . Thus, to find a complete set of solutions in $\mathcal{R}$ for G, we can just find a complete set of solutions for $\hat{G}$ in $\hat{\mathcal{R}}$ . Furthermore, as $\hat{\mathcal{R}}$ is topmost, narrowing with $\hat{R}$ modulo $\mathcal{E}$ is complete and can thus be effectively used to search for all solutions of G even if they could not be computed in Maude by narrowing in $\mathcal{R}$ .

Theorem 3.1 (strong completeness of the topmost extension) Let $\mathcal{R}=(\Sigma,E\uplus B,R)$ be a topmost modulo Ax rewrite theory, with $Ax\in B$ , and let $\mathcal{E}=(\Sigma,E\uplus B)$ be a convergent, finite variant equational theory where B-unification is decidable. Let $\hat{\mathcal{R}}=(\hat{\Sigma},E\uplus B,\hat{R})$ be the topmost extension of $\mathcal{R}$ and let $G=(\exists X)\; t \longrightarrow^{*} t'$ be a reachability goal in $\mathcal{R}$ . If $\sigma$ is a solution for G in $\mathcal{R}$ , then there exists a term t” such that $\{t\}\leadsto_{\hat{R},\mathcal{E}}^* \{t''\}$ with computed substitution $\theta$ and $\sigma=_\mathcal{E}\theta\eta$ , where $\eta$ is an $\mathcal{E}$ -unifier of t” and t’.

Example 4 Consider the rewrite theory $\mathcal{R}$ for the simplified client-server protocol and the reachability goal G of Example 2. Let EXT be a variable that we use as a placeholder for arbitrary object-oriented configurations to generate an ACU topmost extension $\hat{\mathcal{R}}$ of ${\mathcal{R}}$ . The topmost extension $\hat{\mathcal{R}}$ includes the three rewrite rules of Figure 4.

Fig. 2.

Equations of the equational theory encoding the Caesar cipher.

Fig. 3.

Topmost extension of the simplified client-server protocol of Example 2.

Fig. 4.

Definition of the $\mathit{sCond}$ function.

In contrast to Example 2, here the solution ${\tt \{S\mapsto b\}}$ for G can be automatically obtained in Maude by searching the solution for $\hat{G}$ in $\hat{\mathcal{R}}$ via narrowing. This is because $\hat{\mathcal{R}}$ is topmost and hence $\mathcal{E}$ -unification is decidable. In fact, executing $\hat{G}$ in $\hat{\mathcal{R}}$ via the vu-narrow command

produces

It is worth noting that the program transformation in Definition 2 is not only able to transform a topmost modulo Ax rewrite theory $\mathcal{R}$ into a semantically equivalent topmost rewrite theory, but it also ensures coherence of the rewrite rules of $\hat{\mathcal{R}}$ w.r.t. Ax for free. Indeed, the transformation algorithm of Definition 2 extends to object-oriented specifications the Maude (explicit) coherence completion algorithm that automatically produces coherent rewrite theories w.r.t. any given combination of ACU axioms (Clavel et al. Reference Clavel, Durán, Eker, Escobar, Lincoln, Martí-Oliet, Meseguer, Rubio and Talcott2020).

In the following section, we show that our PE algorithm can deal with finite variant theories as well as theories that do not satisfy the FVP, and it is powerful enough to transform them into specialized theories that, in many cases, do satisfy the FVP, thus enabling the use of both levels of narrowing on the theory. In Section 5, we show how the communication protocol of Example 1 can be automatically transformed into a specialized theory that meets the FVP and in which reachability goals of the form $(\exists X) ~t \longrightarrow^* t'$ can be symbolically solved by means of narrowing after having applied the topmost extension described above.

4 Specializing rewrite theories with $\tt{{Presto}}$

In this section, we present the specialization procedure ${ NPER}^{\mathcal{U}}$ , which allows a rewrite theory $\mathcal{R}=(\Sigma,E\uplus B, R)$ to be optimized by specializing the underlying equational theory $\mathcal{E}=(\Sigma,E\uplus B)$ with respect to the calls in the rewrite rules of R. The ${ NPER}^{\mathcal{U}}$ procedure extends the equational, NPE algorithm ${ EqNPE}^{\mathcal{U}}$ of Alpuente et al. (Reference Alpuente, Cuenca-Ortega, Escobar and Meseguer2020b), which applies to equational theories and is parametric w.r.t. an unfolding operator $\mathcal{U}$ that is used to construct finite narrowing trees for a given expression.

4.1 Partial evaluation of equational theories

Given $\mathcal{E}=(\Sigma, E \uplus B)$ , we consider a natural partition of the signature as $\Sigma = \mathcal{D} \uplus \mathcal{C}$ , where $\mathcal{C}$ are the constructor symbols, which are used to define the (irreducible) values of the theory, and $\mathcal{D}$ are the defined symbols, which are evaluated away by equational rewriting. Given a set Q of calls (henceforth called specialized calls), the main goal of ${ EqNPE}^{\mathcal{U}}$ is to derive a new equational theory $\mathcal{E}'$ that computes the same substitutions (and values) as $\mathcal{E}$ for any input term t that is a recursive instance (modulo B) of the terms in Q (i.e., t is an instance of some term in Q and, recursively, every non-variable subterm of t that is rooted by a defined symbol is an instance of some term in Q). The algorithm follows the classic control strategy of logic specializers (Martens and Gallagher Reference Martens and Gallagher1995), with two separate components: (1) local control (managed by the unfolding operator), which avoids infinite evaluations and is responsible for the construction of the residual rules for each specialized call; (2) global control or control of polyvariance (managed by an abstraction operator), which avoids infinite iterations of the PE algorithm and decides which specialized functions appear in the transformed theory. Abstraction guarantees that only finitely many expressions are evaluated, thus ensuring global termination.

The transformation of Alpuente et al. (Reference Alpuente, Cuenca-Ortega, Escobar and Meseguer2020b), is done by iterating two steps:

1. 1. Symbolic execution (Unfolding). A finite, possibly partial folding variant narrowing tree for each input term t of Q is generated. This is done by using the unfolding operator $\mathcal{U}(Q,\vec{\mathcal{E})}$ that determines when and how to stop the derivations in the narrowing tree.

2. 2. Search for regularities (Abstraction). In order to ensure that all calls that may occur at runtime are covered by the specialization, it must be guaranteed that every (sub-)term in any leaf of the tree is equationally closed w.r.t. Q. Equational closedness ^{Footnote 16} extends the classical PD closedness (Lloyd and Shepherdson Reference Lloyd and Shepherdson1991) by: (1) considering B-equivalence of terms; and (2) recursing over the term structure (in order to handle nested function calls). To properly add the non-closed (sub-)terms to the set of already partially evaluated calls, an abstraction operator ${\mathcal{A}}$ is applied that yields a new set of terms which may need further evaluation.

Steps (1) and (2) are iterated as long as new terms are generated until a fixpoint is reached, and the augmented, final set Q’ of specialized calls is yielded. Note that the algorithm does not explicitly compute a partially evaluated equational theory. It does so implicitly; the desired partially evaluated equations E are generated as the set of resultants $t\sigma = t'$ associated with the derivations in the narrowing tree from the root $t\in Q'$ to the leaf t’ with computed substitution $\sigma$ , such that the closedness condition modulo B w.r.t. Q’ is satisfied for all function calls that appear in the right-hand sides of the equations in E’. We assume the existence of a function GenTheory $(Q',(\Sigma, E \uplus B))$ that delivers the partially evaluated equational theory $\mathcal{E}'=(\Sigma,E'\uplus B)$ that is uniquely determined by Q’ and the original equational theory $\mathcal{E}=(\Sigma, E \uplus B)$ . Formally,

\begin{align*}{\rm { G{\small EN}T{\small HEORY}}}(Q',\mathcal{E}) = (\Sigma,\{t\sigma = t'\,\mid\, & t\in Q', t'\in\mathcal{U}(Q',\vec{\mathcal{E}}),\: t \mbox{ fV-narrows to } t' \\&\mbox{with computed substitution } \sigma\} \uplus B).\end{align*}

4.2 The ${ NPER}^{\mathcal{U}}$ scheme for the specialization of rewrite theories

The specialization of the rewrite theory $\mathcal{R}=(\Sigma,E\uplus B,R)$ is achieved by partially evaluating the hosted equational theory $\mathcal{E}=(\Sigma,E\uplus B)$ w.r.t. the rules of R, which is done by using the PE procedure ${ EqNPE}^{\mathcal{U}}$ of Section 4.1. By providing suitable unfolding (and abstraction) operators, different instances of the specialization scheme can be defined.

Before going into the details, let us summarize the advantages of the final, specialized rewrite theory $\mathcal{R}_{\sf sp}=(\Sigma_{\sf sp},E_{\sf sp}\uplus B_{\sf sp},R_{\sf sp})$ over the original $\mathcal{R}=(\Sigma,E\uplus B,R)$ :

1. 1. The transformed rewrite theory $\mathcal{R}_{\sf sp}$ generally performs more efficiently than $\mathcal{R}$ for two reasons. On the one hand, the partially evaluated equational theory $\mathcal{E}_{\sf sp}=(\Sigma_{\sf sp},E_{\sf sp}\uplus B_{\sf sp})$ has been optimized to fulfill the needs of the host rewrite rules of R (that have been correspondingly transformed into $R_{\sf sp}$ ). On the other hand, the specialization process may remove unnecessary equational axioms and rule conditions, thereby significantly speeding up the rewriting and narrowing computations in the specialized theory at the level of both equations and rules.

2. 2. The specialization may cut down an infinite folding variant narrowing space to a finite one. Actually, the transformed equational theory $\mathcal{E}_{\sf sp}$ may have the FVP while the original one may not, so that symbolic analysis based on narrowing with $R_{\sf sp}$ modulo $\mathcal{E}_{\sf sp}$ is enabled, whereas narrowing with R modulo $\mathcal{E}$ is not.

The ${ NPER}^{\mathcal{U}}$ procedure is outlined in Algorithm 1 and it consists of two phases.

Phase 1 (Partial Evaluation). It applies the ${ EqNPE}^{\mathcal{U}}$ algorithm to specialize the equational theory $\mathcal{E}=(\Sigma, E \uplus B)$ w.r.t. a set Q of specialized calls that consists of all of the maximal function calls that appear in the $(\vec{E},B)$ -normalized version R’ of the conditional rewrite rules of R, where $C\!\downarrow_{\vec{E},B}$ denotes $c_1\!\downarrow_{\vec{E},B}\wedge\ldots\wedge c_n\!\downarrow_{\vec{E},B}$ for any rule condition $C=c_1\wedge\ldots\wedge c_n$ . Given $\Sigma = (\mathcal{D} \uplus \mathcal{C})$ , a maximal function call in a term t is any outermost subterm of t that is rooted by a defined function symbol of E. By mcalls(R), we denote the set of all maximal calls in both the right-hand sides and the conditions of the rules of R. This phase produces the new set of specialized calls Q’ from which the PE $\mathcal{E}'=(\Sigma', E' \uplus B')$ of $\mathcal{E}$ w.r.t. Q is unambigously derived by GenTheory( $Q',(\Sigma,E\uplus B)$ ).

Phase 2 (Compression). It consists of a refactoring transformation that computes a new, simplified rewrite theory $\mathcal{R}_{\sf sp}=(\Sigma_{\sf sp},E_{\sf sp}\uplus B_{\sf sp},R_{\sf sp})$ by taking as input the $({\vec{E},B})$ -normalized rewrite theory $\mathcal{R}'=(\Sigma,E\uplus B,R')$ , the computed partially evaluated theory $\mathcal{E}'=(\Sigma', E' \uplus B')$ , and the final set of specialized calls Q’ from which $\mathcal{E}'$ derives.

The compression phase consists of two subphases: renaming and rule condition simplification. The renaming (sub-)phase aims at yielding a much more compact equational theory $\mathcal{E}_{ren}=(\Sigma_{ren}, E_{ren} \uplus B_{ren})$ where unused symbols and unnecessary repetitions of variables are removed and equations of $E_{ren}$ are simplified by recursively renaming all expressions that are Q’-closed modulo B by using an independent renaming function that is derived from the set of specialized calls Q’. Formally, an independent renaming $\delta$ for a set of terms T and a signature $\Sigma$ is a mapping from terms to terms, which is defined as follows. For each t of sort s in T with $root(t)=f$ , $\delta(t)={f_{t}(\overline{x_{n}:s_{n}})}$ , where $\overline{x_{n}}$ are the distinct variables in t in the order of their first occurrence and $f_{t}\colon \overline{s_n}\to s$ is a new function symbol that does not occur in $\Sigma$ or T and is different from the root symbol of any other $\delta(t')$ , with $t'\in T$ and $~t'\neq t$ . Abusing notation, we let $\delta(T)$ denote the set $\{\delta(t)\mid t\in T\}$ for a given set of terms T.

Example 5 Consider the rewrite theory in Example 1 together with the set of specialized calls

\begin{equation*}Q= \{\tt dec(enc(M:Data,s(s(0)))), enc(enc(M,K1:Nat),K2:Nat)\}\end{equation*}

An independent renaming $\delta$ for Q is given by

\begin{align*}\delta =\{&{\tt dec(enc(M:Data,s(s(0)))) \mapsto f0(M:Data),} \\ &{\tt enc(enc(M:Data,K1:Nat),K2:Nat) \mapsto f1(M:Data,K1:Nat,K2:Nat)}\}\end{align*}

where f0: Data -> Data and f1: Data Nat Nat -> Data are new function symbols.

Renaming is performed by the Rename function given in Algorithm 2.

Essentially, the Rename function recursively computes (by means of the function ${ RN}_{\delta}$ ) a new equation set $E_{ren}$ by replacing each call in E’ by a call to the corresponding renamed function according to $\delta$ . Furthermore, a new rewrite rule set $R_{ren}$ is also produced by consistently applying ${ RN}_{\delta}$ to the conditional rewrite rules of R’. Formally, each conditional rewrite rule $\lambda \Rightarrow \rho ~\mathit{if}~ C$ in R’ is transformed into the rewrite rule ${ RN}_{\delta}(\lambda)\Rightarrow { RN}_{\delta}(\rho) ~\mathit{if}~ { RN}_{\delta}(C)$ , in which every maximal function call t in the rule is recursively renamed according to the independent renaming $\delta$ . The renaming algorithm also computes the specialized signature $\Sigma_{ren}$ and restricts the set B’ to those axioms obeyed by the function symbols in $\Sigma'\cap\Sigma_{ren}$ , delivering the rewrite theory $(\Sigma_{ren}, E_{ren}\uplus B_{ren},R_{ren})$ .

Note that, while the independent renaming suffices to rename the left-hand sides of the equations in E’ (since they are mere instances of the specialized calls), the right-hand sides are renamed by means of the auxiliary function ${ RN}_{\delta}$ , which recursively replaces each call in the given expression by a call to the corresponding renamed function (according to $\delta$ ).

The simplification subphase is undertaken by the Simplify procedure of Algorithm 3 that further refines the rewrite theory $\mathcal{R}_{ren}$ . Indeed, the PE process may produce specialized rewrite rules that include conditions that can be safely removed without changing the original program semantics. This transformation is implemented by function $\mathit{SimpConds}(\mathcal{R})$ and may have a huge impact on program efficiency since Maude executes unconditional rules much faster than conditional rules because the evaluation of rule conditions is notoriously speculative in Maude. This is because, besides the fact that many equational matchers for the rule conditions may exist, solving rewriting conditions requires non-deterministic search (Serbanuta and Rosu Reference Serbanuta and Rosu2006; Clavel et al. Reference Clavel, Durán, Eker, Escobar, Lincoln, Martí-Oliet, Meseguer, Rubio and Talcott2020). The rule simplification function $\mathit{SimpConds}(\mathcal{R})$ is left generic in Algorithm 3 and can be specialized for different kinds of rewrite theories.

After simplifying rule conditions, there might exist spurious equations $l=r$ in $E_{ren}$ such that root(l) does not occur in either the simplified rewrite rules of R’ or in $(E_{ren}\setminus \{l=r\})$ . Hence, Simplify removes such equations, and the theory signature is cleaned up by deleting any operators (and their corresponding axioms) that do not occur in the transformed equations and rules.

A concrete implementation $\mathit{SimpConds}^*(\mathcal{R})$ of the generic rule simplication function $\mathit{SimpConds}(\mathcal{R})$ of Algorithm 3 that works for the theories that are considered in this article is given in the following definition:

Definition 3 (Rule Condition Simplification) Let $\mathcal{R} = (\Sigma,E\uplus B,R)$ be a rewrite theory with an equational theory $\mathcal{E}=(\Sigma,E\uplus B)$ . Then, $\mathit{SimpConds}^*(\mathcal{R})$ is given by the set

\begin{align*} \bigcup_{\lambda \Rightarrow \rho \;\mathit{if} \;C \;\in \;R} \{\lambda \Rightarrow \rho \;\mathit{if}\ \mathit{sCond}_{\mathcal{E}}(\lambda,\rho,C,\mathit{nil}) \mid &~ \mbox{no condition in } C \mbox{ is } ~\mathit{false}\} \end{align*}

where the definition of the auxiliary function $\mathit{sCond}_{\mathcal{E}}(\lambda,\rho,C,\sharp C)$ is given in Figure 4.

Roughly speaking, for any conditional rule $\lambda \Rightarrow \rho ~\mathit{if}~ C$ in R such that none of the conditions in C is false, ^{Footnote 17} the auxiliary function $\mathit{sCond}_{\mathcal{E}}$ gets rid of

(Case 2) those maximal subsequences ^{Footnote 18} C’ of C such that all of its elements are tautological expressions of the form $t=t$ , $t':=t'$ , or $t''\Rightarrow t''$ (so that t and t’ unify with the empty substitution by using fV-narrowing). Note that this optimization cannot be done by standard Maude Boolean simplification, which does not apply to non-ground, rule condition expressions; or C’ consists of n equations of the form $t_{i} = t'_{i}$ , with $t_{i} \neq t'_{i}$ , such that there exists an $\mathcal{E}$ -unifier $\theta$ for all of the equations in the sequence. To safely perform this optimization two extra conditions must hold: (i) $\mathcal{E}$ must have the FVP to make $\mathcal{E}$ -unification decidable; (ii) the variables occurring in C’ must not occur in the rest of the rule to be simplified. The constraint on the variables in C’ is required to preserve the narrowing semantics since we must ensure that removing the equationally satisfiable sequence C’ does not affect the overall computation.

(Case 3) those equations (resp. matching equations $t_1 := t_2$ and rewrite expressions $t_2 \Rightarrow t_1$ ) such that $t_1$ and $t_2$ are B-unifiable (resp. $t_2$ is an instance of $t_1$ modulo B), and the variables in $t_1$ and $t_2$ do not occur in the rest of the rule. those equations $t _{1}= t_{2}$ , with $t_{1} \neq t_{2}$ , such that the set of (most general) constructor variants (i.e., equational variants that only include constructor symbols and variables (Meseguer Reference Meseguer2020)) of $t_{1}$ and $t_{2}$ are the same (in symbols, $CV_{\mathcal{E}}(t_1) = CV_{\mathcal{E}}(t_2)$ ), which implies that $t _{1}$ and $t_{2}$ compute the very same set of constructor values and answers. However, since variables in $t _{1}= t_{2}$ are not required to be apart from the variables in the rest of the rule, this simplification only applies when the rule to be simplified is not enabled for narrowing but only for rewriting. Otherwise, removing the condition $t _{1}= t_{2}$ might not preserve the overall computed answers. Furthermore, to ensure that constructor variant sets are computable, two extra conditions on $\mathcal{E}$ are required (Meseguer Reference Meseguer2020): (i) $\mathcal{E}$ must have the FVP and (ii) $\mathcal{E}$ must be sufficiently complete modulo axioms (i.e., it specifies total functions). We say that equational theories satisfying (i) and (ii) have the constructor finite variant property ^{Footnote 19} (CFVP).

Note that Cases 1 and 4 of the $\mathit{sCond}_{\mathcal{E}}$ function are simply used to incrementally process the rule condition to be simplified, yet they do not remove any expression.

The renaming subphase of the compression transformation can be seen as a qualified extension to the RWL setting of the classical renaming ^{Footnote 20} that is applied in the PE of logic programs and implemented in well-known PD tools such as Logen and ECCE (Leuschel et al. Reference Leuschel, Elphick, Varea, Craig and Fontaine2006), which greatly lessens the program structure. The rule condition simplification transformation is novel and further contributes to lighten the specialized rewrite theory. Although more aggressive rule simplification is possible, our transformation is relatively straightforward and inexpensive. Actually, neither it propagates answers from the removed expressions to the rest of the rule, nor does it require replicating rules due to several equational unifiers.

Let us illustrate the rule condition simplification given by $\mathit{SimpConds}^*(\mathcal{R})$ by means of two examples.

Example 6 Let $\mathcal{E}=(\Sigma,E\uplus B)$ be the equational theory of Figure 1 modeling the Caesar cypher, and let $\mathcal{R}$ be a rewrite theory $(\Sigma,E\uplus B,\{r\})$ , where r is a conditional rewrite rule whose condition C is ${\tt enc(a,s(K:Nat)) = enc(b,K:Nat)}$ . By applying the PE algorithm ${ NPER}^{\mathcal{U}}$ to $\mathcal{R}$ , first the rule condition C is normalized in $\vec{E}$ (modulo B) into

\begin{equation*} {\tt toSym(e(s(0),K)) = toSym(e(s(0),K)). }\end{equation*}

After partially evaluating the equational theory, the rule condition is transformed into a trivial equation f(K:Nat) = f(K:Nat), with independent renaming

\begin{equation*}{\tt toSym(e(s(0), K:Nat)) \mapsto f(K:Nat)}\end{equation*}

for the call toSym(e(s(0), K:Nat)). Then, the trivial equation f(K:Nat) = f(K:Nat) is removed (via Case 2.a of the sCond function), thereby delivering an unconditional version of r as final outcome.

Example 7 Let $\mathcal{E}=(\Sigma,E\uplus B)$ be the equational theory of Figure 1 modeling the Caesar cypher, and let $\mathcal{R}$ be a rewrite theory $(\Sigma,E\uplus B,\{r\})$ , where r is a conditional rewrite rule whose condition C is ${\tt enc(S:Symbol,s(0)) = enc(enc(S:Symbol,0),s(0))}$ . We note that this condition does not generally hold for every symbol S in an arbitrary encryption function, but it certainly does when considering the implementation of the enc function defined by the equational theory of Example 1. We also assume that the variable S only appears in the condition C of the rule r. By specializing in $\tt{{Presto}}$ the two (already normalized) maximal function calls in rule r, enc(S:Symbol,s(0)) and enc(enc(S:Symbol,0),s(0)), we get an equational theory $\mathcal{E}_{ren}$ containing the following equations

where f0 and f1 are two new operators that are introduced to rename the initial calls enc(S:Symbol,s(0)) and enc(enc(S:Symbol,0),s(0)), and actually denote the very same encryption function.

Furthermore, the condition C is renamed as

\begin{equation*}{\tt f1(S:Symbol) = f0(S:Symbol).}\end{equation*}

Since $\mathcal{E}_{ren}$ has the FVP, equational unification of $\tt f1(S:Symbol)$ and $\tt f0(S:Symbol)$ is decidable and delivers three unifiers, namely, $\tt \{S \mapsto a\}$ , $\tt \{S \mapsto b\}$ and $\tt \{S \mapsto c\}$ . Hence, the condition f1(S:Symbol) = f0(S:Symbol) can be safely removed from the specialized version of r (via Case 2.b of the $\mathit{sCond}_{\mathcal{E}}$ function), since variable $\tt S$ does not appear elsewhere in the rule.

An example of condition simplification that exploits Case 3.b of the $\mathit{sCond}_{\mathcal{E}}$ function is shown in Example 10.

Given the rewrite theory $\mathcal{R}=(\Sigma,E\uplus B,R)$ and its specialization ${\mathcal{R}_{\sf sp}}=$ NPER $^{\mathcal{U}}\!\!(\mathcal{R})$ , all of the executability conditions that are satisfied by $\mathcal{R}$ are also satisfied by ${\mathcal{R}_{\sf sp}}=(\Sigma_{\sf sp},E_{\sf sp}\uplus B_{\sf sp},R_{\sf sp})$ , including the fact that $R_{\sf sp}$ is coherent w.r.t. $E_{\sf sp}$ modulo $B_{\sf sp}$ . This is proved in Theorem 1 of Alpuente et al. (Reference Alpuente, Ballis, Escobar and Sapiña2022) for the case of unconditional rewrite theories such that the left-hand sides of the rules in R are $(\vec{E},B)$ -strongly irreducible, and straightforwardly extends to conditional rewrite theories since 1) the conditional version of ${ NPER}^{\mathcal{U}}$ only augments the initial set Q of specialized calls with the maximal calls in the rule conditions, while the core equational PE algorithm is kept untouched; and 2) only conditions that do not modify any semantic property are removed by the rule condition simplification that is performed by the compression phase.

Similarly, the strong semantic correspondence between both narrowing and rewriting computations in $\mathcal{R}$ and $\mathcal{R}_{\sf sp}$ was proved in Theorem 2 of Alpuente et al. (Reference Alpuente, Ballis, Escobar and Sapiña2022) for unconditional rewrite theories and immediately extends to the conditional case for the same reasons and under the above-mentioned strong irreducibility requirement.

5 Instantiating the specialization scheme for rewrite theories

In the following, we outline two instances of the ${ NPER}^\mathcal{U}$ scheme that are obtained by choosing two distinct implementations of the unfolding operator $\mathcal{U}$ . More precisely, we present the unfolding operators $\mathcal{U}_{\mathit{FVP}}$ and $\mathcal{U}_{\mathit{\overline{FVP}}}$ that allow $\mathcal{R}$ to be specialized when $\mathcal{E}$ is (respectively, is not) a finite variant theory. Both operators have been implemented in $\tt{{Presto}}$ .

With regard to global control, $\tt{{Presto}}$ implements the same abstraction operator for both scheme instantiations. This abstraction operator is described in Alpuente et al. (Reference Alpuente, Cuenca-Ortega, Escobar and Meseguer2020c) and relies on the equational least general generalization algorithm of Alpuente et al. (Reference Alpuente, Escobar, Meseguer and Sapiña2021b) that improves our original calculus in Alpuente et al. (Reference Alpuente, Escobar, Espert and Meseguer2014b) by providing a finitary, minimal, and complete set of order-sorted generalizers modulo any combinations of associativity and/or commutativity and/or identity axioms for any unification problem. This property holds even when the theory contains function symbols with an arbitrary number n of distinct identity elements, $e_{1}, \ldots, e_{n}$ , provided their respective least sorts are incomparable at the kind level. In symbols, $[ls(e_{i})] \neq [ls(e_{j})]$ for any $i\neq j$ , with $i,j \in 1,\ldots, n$ . Theories that satisfy this property are called $U-\mathit{tolerant}$ theories. Note that the traditional one-unit condition that was implicitly assumed in Alpuente et al. (Reference Alpuente, Escobar, Espert and Meseguer2014b) implies U-tolerance.

where the ctor declarations specify that all of these operators are data constructors. Note that, since Nat < List and Nat < MSet, 0 is both a list of length one and a singleton multiset, but the list 0 ; s(0) ; s(s(0)) and the multiset 0, s(0), s(s(0)) have incomparable least sorts List and MSet. Moreover these are also the least sorts of nil and null, respectively. Therefore, this theory is not U-tolerant, since $[ls({\tt nil})] = [ls({\tt null})] = {\tt Top}$ .

Automated ways to achieve U-tolerance in a semantics-preserving manner are discussed in Alpuente et al. (Reference Alpuente, Escobar, Meseguer and Sapiña2021b).

Case 1: $\mathcal{E}$ is not a finite variant theory.

When $\mathcal{E}$ is not a finite variant theory, the fV-narrowing strategy may lead to the creation of an infinite fV-narrowing tree for some specialized calls in Q. In this case, an equational order-sorted extension $\breve{\trianglelefteq}_B$ (Alpuente et al. Reference Alpuente, Cuenca-Ortega, Escobar and Meseguer2020b) of the classical homeomorphic embedding relation ^{Footnote 21} $\trianglelefteq$ is used to detect the risk of non-termination. Roughly speaking, a homeomorphic embedding relation is a structural preorder under which a term t is greater than or equal to another term t’ (i.e., t embeds t’), written as $t \trianglerighteq t'$ , if t’ can be obtained from t by deleting some parts, e.g., $s(s(X+Y)\ast(s(X)+Y))$ embeds $s(Y\ast(X+Y))$ ). Embedding gets much less intuitive when dealing with axioms. For example, let us write natural numbers in classical decimal notation and the addition operator ${\tt +}$ for natural numbers in prefix notation. Due to associativity and commutativity of symbol ${\tt +}$ , there can be many equivalent terms such as $+(+(1,2),+(3,0))$ and $+(+(1,+(3,2)), 0)$ , all of which are internally represented in Maude by the flattened term $+(0,1,2,3)$ . Actually, flattened terms like $+(1,0,2,3)$ can be further simplified into a single canonical representative $+(0,1,2,3)$ , hence $+(1,2) \breve{\trianglelefteq}_B +(0,1,2,3)$ and also $+(2,1) \breve{\trianglelefteq}_B +(0,1,2,3)$ . In contrast, if $+$ was associative (and not commutative), then $+(2,1) \not\!\!\!\breve{\trianglelefteq}_B +(1,0, 3, 2)$ . A more detailed description that takes into account the extra complexity given by sorts and subsorts can be found in Alpuente et al. (Reference Alpuente, Cuenca-Ortega, Escobar and Meseguer2020c).

When iteratively computing a sequence $t_1, t_2, \ldots,t_n$ , finiteness of the sequence can be guaranteed by using the well-quasi order relation $\breve{\trianglelefteq}_B$ (Alpuente et al. Reference Alpuente, Cuenca-Ortega, Escobar and Meseguer2020c) as a whistle (Leuschel Reference Leuschel1998): whenever a new expression $t_{n+1}$ is to be added to the sequence, we first check whether $t_{n+1}$ embeds any of the expressions already in the sequence. If that is the case, we say that the homeomorphic embedding test $\breve{\trianglelefteq}_B$ whistles, i.e., it has detected (potential) non-termination and the computation has to be stopped. Otherwise, $t_{n+1}$ can be safely added to the sequence and the computation can proceed.

The operator $\mathcal{U}_{\mathit{\overline{FVP}}}$ implements such an embedding check to guarantee the termination of the unfolding phase. Specifically, the generation of a fV-narrowing tree fragment is stopped when each fV-narrowing derivation (i.e., each branch of the fV-narrowing tree) is stopped because a term is reached that is either unnarrowable or it embeds (w.r.t. $\breve{\trianglelefteq}_B$ ) a previously narrowed term in the same derivation.

Let $\mathcal{R}=(\Sigma,E\uplus B,R)$ be such a rewrite theory, where $\mathcal{E}=(\Sigma,E\uplus B)$ is the equational theory of $\mathcal{R}$ . In $\mathcal{E}$ , the fV-narrowing trees associated with encryption and decryption functionality may be infinite since $\mathcal{E}$ does not have the FVP, as shown in Section 3. For instance, terms of the form ${\tt (t_1\ \ldots\ t_n\ enc(M',s(0)))}$ derive from ${\tt enc(M,k1)}$ by fV-narrowing, where $\tt enc(M',s(0))$ can be further narrowed to unravel an unlimited sequence of identical terms modulo renaming. Nonetheless, equational homeomorphic embedding detects this non-terminating behavior since $\tt enc(M',s(0))$ embeds $\tt enc(M,s(0))$ .

By using the unfolding operator $\mathcal{U}_{\overline{FVP}}$ , the first phase of the ${ NPER}^{\mathcal{U}_{\overline{FVP}}}(\mathcal{R})$ algorithm first normalizes the rewrite rules in R. The normalization process produces a new set of rules R’ where the reply and rec rules are left unchanged, while the req rule is simplified into

because of the normalization of the equational condition (s(0) < len) = true and the instantiation of the condition enc(M,s(0)) = enc(enc(M,0),s(0)) to the specific case where K is equal to s(0).

Subsequently, the specialization algorithm computes the initial set

\begin{equation*}{\tt Q=\{enc(M,s(0)),dec(M,s(0)),enc(enc(M,0),s(0))\}}\end{equation*}

of the (normalized) maximal function calls in R’, where M is a variable of sort Data, and the equational theory $\mathcal{E}$ is partially evaluated by ${ EqNPE}^{\mathcal{U}_{\overline{FVP}}}$ w.r.t. Q. During the PE process, $\mathcal{U}_{\overline{FVP}}$ only unravels finite fragments of the fV-narrowing trees that are rooted by the specialized calls, and the final set Q’ of specialized calls is

\begin{align*}\!\{&{\tt dec(X:Data, s(0))}, {\tt enc(X:Data, s(0))}, {\tt enc(enc(X:Data, 0), s(0))},\\ &\!\!\!{\tt toSym([toNat(Y:Symbol) < s(s(0)),s(toNat(Y:Symbol)),0])},{\tt toSym(toNat(Y:Symbol)\!)},\\&\!\!\!{\tt toSym(unshift(toNat(Y:Symbol)))}\}.\end{align*}

The resulting PE $\mathcal{E}'$ of $\mathcal{E}$ , which is generated from Q’, is given in Figure 9. The second phase (compression) renames $\mathcal{E}'$ into the equational theory $\mathcal{E}_{ren}$ of Figure 9 by computing the following renaming for the specialized calls:

\begin{equation*}\begin{array}{l}{\tt dec(X:Data, s(0))} \mapsto {\tt f0(X:Data)} \\{\tt enc(X:Data, s(0))} \mapsto {\tt f1(X:Data)}\\{\tt enc(enc(X:Data, 0), s(0))} \mapsto {\tt f2(X:Data)}\\{\tt toSym([toNat(Y:Symbol) < s(s(0)),s(toNat(Y:Symbol)),0])}\mapsto {\tt f3(Y:Symbol)}\\{\tt toSym(toNat(Y:Symbol))} \mapsto {\tt f4(Y:Symbol)}\\{\tt toSym(unshift(toNat(Y:Symbol)))} \mapsto {\tt f5(Y:Symbol)}\end{array}\end{equation*}

Fig. 5.

${ NPER}^{\mathcal{U}_{\overline{FVP}}}$ Phase 1: Partial evaluation of $\mathcal{E}$ w.r.t. Q output by $\tt{{Presto}}$ .

Fig. 6.

${ NPER}^{\mathcal{U}_{\overline{FVP}}}$ Phase 2: Renamed theory $\mathcal{E}_{ren}$ output by $\tt{{Presto}}$ .

Fig. 7.

${ NPER}^{\mathcal{U}_{\overline{FVP}}}$ Phase 2: Specialized rewrite rules output by $\tt{{Presto}}$ .

Fig. 8.

Equations of the specialized equational theory for one-symbol messages and key s(0).

Fig. 9.

Loading specifications and selecting the unfolding strategy in $\tt{{Presto}}$ .

which eliminates complex nested calls and redundant arguments in $\mathcal{E}_{ren}$ computations.

It is worth noting that the resulting specialization $\mathcal{E}_{ren}$ provides a highly optimized version of $\mathcal{E}$ for the arbitrarily fixed key s(0), where both functional and structural compression are achieved. Specifically, data structures in $\mathcal{E}$ for natural numbers and their associated operations for message encryption and decryption are totally removed from $\mathcal{E}_{ren}$ . Also, code reuse is automatically achieved in $\mathcal{E}_{ren}$ . Indeed, the obtained specialization reuses the renamed specialized call f3(X:Data) in the specialization of both enc(X:Data,s(0)) (given by eq f1(S:Symbol M:Data) = f3(S:Symbol) f1(M:Data) [variant]) and enc(enc(X:Data,0),s(0)) (given by eq f2(S:Symbol M:Data) = f3(f4(S:Symbol)) f2(M:Data) [variant]).

Note that the _+_ operator, together with its associative and commutative axioms, disappears from $\mathcal{E}_{ren}$ , thereby avoiding expensive matching operations modulo axioms. This transformation power cannot be achieved by existing functional, logic, or functional-logic partial evaluators for a language that implements native matching modulo axioms. Decryption (resp., encryption) in $\mathcal{E}_{ren}$ is now the direct mapping f0 (resp., f1) that associates messages to their corresponding decrypted (resp. encrypted) counterparts, avoiding a huge amount of computation in the profuse domain of natural numbers. The computed renaming is also applied to $\mathcal{R}$ by respectively replacing, into the rewrite rules of $\mathcal{R}$ , the maximal function calls dec(M,s(s(0))), enc(M,s(s(0))), and enc(enc(M,0),s(0)) with f0(M), f1(M), and f2(M), respectively. This allows the renamed rewrite rules to be able to access the new specialized encryption and decryption functionality provided by $\mathcal{E}_{ren}$ . Finally, condition simplification is run, thereby removing the trivial condition true = true from the renamed version of the req rule and delivering the set of specialized rules of Figure 9 as outcome. Note that condition simplification is not able to remove condition f1(M) = f2(M) from the specialized rewrite rule req-sp since the partially evaluated equational theory $\mathcal{E}_{ren}$ does not have the FVP and thus the Simplify Algorithm can only remove trivial rule conditions.

Example 9 shows that a great degree of simplification can be achieved by the specialization technique of $\tt{{Presto}}$ for theories that do not have the FVP. Furthermore, in many cases, the algorithm ${ NPER}^{\mathcal{U}_{\overline{FVP}}}$ is also able to transform an equational theory that does not meet the FVP into a specialized one that does. This typically happens when the function calls to be specialized can only be unfolded a finite number of times. Let us see an example.

Example 10 Consider a slight variant of the protocol theory of Example 9 in which messages consist of one single symbol instead of arbitrarily long sequences of symbols. This variant can be obtained by simply modifying the sort of the messages from Data to Symbol in the protocol rewrite rules. In this scenario, the set of (normalized) maximal function calls becomes

\begin{equation*}\tt Q=\{enc(M,s(0))\downarrow_{\mathit{\vec{E},B}}, dec(M,s(0))\downarrow_{\mathit{\vec{E},B}}, enc(enc(M,0),s(0))\downarrow_{\mathit{\vec{E},B}}\}\end{equation*}

where M is a variable of sort Symbol. The rewrite theory can be automatically specialized by $\tt{{Presto}}$ for this use case by using ${ NPER}^{\mathcal{U}_{\overline{FVP}}}$ . The intermediate, partially evaluated equational theory $\mathcal{E}_{ren}$ is shown in Figure 8.

The obtained specialization gets rid of the associative data structure that is needed to build messages of arbitrary size since only one-symbol messages are allowed in the specialized program. Also, note that $\mathcal{E}_{ren}$ clearly meets the FVP because it specifies three non-recursive functions (namely, f0, f1, f2), which all work over the finite domain {a,b,c}. Additionally, $\mathcal{E}_{ren}$ is sufficiently complete (indeed, f1, f2, and f3 are total functions that respectively implement the behavior of the calls dec(M,s(0)), enc(M,s(0)), and enc(enc(M,0),s(0)) for each $\tt M\in\{a,b,c\}$ ). Therefore $\mathcal{E}_{\sf ren}$ also has the CFVP, which means that the Simplify algorithm can fully apply its simplification strategy to the (renamed) specialized conditional rule for protocol request

This rule is completely deconditionalized by removing both the trivial condition true = true (as in Example 9) and the condition f1(M) = f2(M). The latter condition is removed by applying Case 3.b of the $\mathit{sCond}_{\mathcal{E}}$ function since the req-ren rule has not the narrowing label and f1(M) and f2(M) have the same (most general) constructor variants in $\mathcal{E}_{ren}$ :

\begin{equation*}CV_{\mathcal{E}_{ren}}({\tt f1(M)}) = {\tt \{(\{M\mapsto a\},b),(\{M\mapsto b\},c),(\{M\mapsto c\},a)\}} = CV_{\mathcal{E}_{ren}}({\tt f2(M)}).\end{equation*}

Finally, note that the satisfaction of the FVP allows narrowing-based reachability problems in the specialized rewrite theory $\mathcal{R}_{\sf sp}$ to be effectively solved in the topmost extension of $\mathcal{R}_{\sf sp}$ , which can be automatically computed by the program transformation of Section 3.2. Therefore, reachability goals such as the one of Example 4 can be solved in the topmost extension of the specialized rewrite theory obtained in Example 10.

Case 2: $\mathcal{E}$ is a finite variant theory.

When $\mathcal{E}$ is a finite variant theory, fV-narrowing trees are always finite objects that can be effectively constructed in finite time. Therefore, it is possible to construct the complete fV-narrowing tree for any possible specialized call. The unfolding operator $\mathcal{U}_{\mathit{FVP}}$ develops such a complete fV-narrowing tree for a given input term in $\mathcal{E}$ .

The advantage of using $\mathcal{U}_{\mathit{FVP}}$ instead of $\mathcal{U}_{\mathit{\overline{FVP}}}$ is twofold. First, $\mathcal{U}_{\mathit{FVP}}$ disregards any embedding check, which can be extremely time-consuming when $\mathcal{E}$ includes several operators that obey complex modular combinations of algebraic axioms ^{Footnote 22} . Second, $\mathcal{U}_{\mathit{FVP}}$ exhaustively explores the whole fV-narrowing tree of a term, while $\mathcal{U}_{\mathit{\overline{FVP}}}$ does not. This leads to a lower degree of specialization when $\mathcal{U}_{\mathit{\overline{FVP}}}$ is applied to a finite variant theory, as shown in the following (pathological) example.

The equational theory specifies the encoding for natural numbers in Presburger’s style ^{Footnote 23} and uses this encoding to define the function mkEven(X,Y) that makes X even (if X is odd) by “moving” one unit from Y to X. Otherwise, if X is even, X is left unchanged. The PE of the given theory w.r.t. the call mkEven(X,Y) yields different outcomes that depend on the chosen unfolding operator. On the one hand, by using $\mathcal{U}_{\mathit{\overline{FVP}}}$ , the output is the very same input theory, thus no “real” specialization is achieved. On the other hand, the unfolding operator $\mathcal{U}_{\mathit{FVP}}$ produces the specialized definition of mkEven given by

where the second equation is generated by fully exploring the fV-narrowing derivation

\begin{equation*}{\tt mkEven(Z,W)}\leadsto_{\tt\{Z\mapsto X + X + 1,W\mapsto 1 + Y\}} {\tt mkEven(1\ +\ 1\ +\ X\ +\ X, Y)} \leadsto_{\tt \{Y\mapsto 0\}} {\tt 1\ +\ 1\ +\ X\ +\ X}\end{equation*}

where $t \leadsto_{{{\sigma}}}{} t$ denotes a fV-narrowing step from t to t’ with substitution $\sigma$ . In contrast, $\mathcal{U}_{\mathit{\overline{FVP}}}$ stops the sequence at mkEven(1 + 1 + X + X, Y) since mkEven(1 + 1 + X + X, Y) embeds mkEven(Z,W) and hence yields a specialized equation that is equal (modulo associativity and commutativity of +) to the original equation mkEven(X + X + 1,1 + Y) = mkEven(X + X + 1 + 1,Y).

6 The $\tt{{Presto}}$ system

$\tt{{Presto}}$ is a program specializer for Maude programs whose core engine consists of approximately 1800 lines of Maude. The system is available, together with a quick start guide and a number of examples at http://safe-tools.dsic.upv.es/presto. The $\tt{{Presto}}$ distribution package also contains $\tt{{Presto}}$ source code for local installation, which is updated to the latest Maude release.

Similarly to Victoria, the earlier PE tool for equational theories (Alpuente et al. Reference Alpuente, Cuenca-Ortega, Escobar and Meseguer2020b), $\tt{{Presto}}$ follows the on-line approach to PE that makes control decisions about specialization on the fly. This offers better opportunities for powerful automated strategies than off-line PE (Jones et al. Reference Jones, Gomard and Sestoft1993), where decisions are made before specialization by using abstract data descriptions that are represented as program annotations. Compared to Victoria, the whole $\tt{{Presto}}$ implementation is totally new code that is cleaner and much simpler, including the equational least general generalization component of the system that is based on the improved least general generalization algorithm of Alpuente et al. (Reference Alpuente, Escobar, Meseguer and Sapiña2021b). Also, $\tt{{Presto}}$ can deal with Maude system modules (i.e., rewrite theories) and multi-module Maude specifications that cannot be managed by Victoria, which only handles equational theories encoded by single Maude functional modules.

$\tt{{Presto}}$ can be accessed via a user-friendly web interface that has been developed by using CSS, HTML5, and JavaScript technologies in addition to a command-line interface. This enables users to specialize Maude rewrite theories using a web browser, without the need for a local installation. The Maude core component is connected to the client web user interface through 10 RESTful Web Services that are implemented by using the JAX-RS API for developing Java RESTful Web Services (around 500 lines of Java source code). Since $\tt{{Presto}}$ is a fully automatic online specializer, its usage is simple and accessible for inexperienced users. With regard to the security of the system, in order to prevent the execution of unsafe code submitted by users, every call to a Maude function is first checked against a blocklist of unsafe functions so that the process is aborted if there is a call that belongs to the blocklist and a warning message is triggered. We consider unsafe functions to be all of those Maude system-level commands that may remotely control the system-level activities in the server hosting Presto. Also, spawned processes are automatically killed when a time limit is exceeded.

$\tt{{Presto}}$ comes with a set of preloaded Maude specifications that includes all of the examples shown in this paper. Preloaded examples can be selected from a pull-down menu, or new specifications can be written from scratch using a dedicated text area. Another pull-down menu allows the user to select the unfolding operator (either ${\mathcal{U}_{\mathit{\overline{FVP}}}}$ or ${\mathcal{U}_{\mathit{FVP}}}$ ) to automatically optimize the input rewrite theory by specializing its underlying guest equational theory and hardcoding the obtained specialized functions into the rewrite rules. $\tt{{Presto}}$ also supports the PE of equational theories w.r.t. a given set of user-defined calls by using either ${\mathcal{U}_{\mathit{\overline{FVP}}}}$ or ${\mathcal{U}_{\mathit{FVP}}}$ .

Figure 9 shows a screenshot of the $\tt{{Presto}}$ interface where the object-oriented client-server communication protocol of Example 9 has been selected among the preloaded examples and the ${\mathcal{U}_{\mathit{\overline{FVP}}}}$ operator has been chosen for the specialization of the rewrite theory under consideration (the Partial evaluation of rewrite theories (no-FVP/embedding) option in the pull-down menu).

Finally, $\tt{{Presto}}$ includes the following useful additional features.

Specialization views. Two possible views of the resulting specialization are delivered, with or without the compression phase enabled. The user can switch back and forth between the two representations by respectively selecting the Specialized and Specialized with Compression tabs. Figures 10 and 11 respectively show the specialization of the client-server communication protocol before and after the compression phase. Furthermore, by accessing the Renaming tab, it is possible to explicitly inspect the renaming computed by the compression phase and see how nested calls are dramatically compacted by using the corresponding fresh function symbols.

Fig. 10.

Specialized client-server communication protocol before the compression phase.

Inspection mode. By activating the inspect tab, $\tt{{Presto}}$ shows detailed information of the specialization process that can be particularly useful for a user who wants to experiment with different specializations for analysis and verification purposes. Specifically, for each iteration i of the ${\sf EqNPE}^{\mathcal{U}}$ algorithm (invoked in Line 4 of Algorithm 1), $\tt{{Presto}}$ shows all of the leaves (term variants) in the deployed fV-narrowing trees for the calls that were specialized at the iteration i, together with their corresponding computed substitution (i.e., the substitution component of a term variant). Also, thanks to the interconnection with the narrowing stepper Narval (Alpuente et al. Reference Alpuente, Ballis, Escobar and Sapiña2019b), each fV-narrowing tree computed at iteration i can be graphically visualized and interactively navigated. This is automatically done by simply selecting the desired tree root term to be expanded from the displayed list of calls that were specialized at any iteration (including the last one). This can be done by simply clicking the hyperlink associated with the desired call. By doing this, the user can perform a fine-grained and stepwise inspection of all narrowing steps, computation of equational unifiers, and interactive exploration of different representations of Maude’s narrowing and rewriting search spaces (tree-based or graph-based, source-level or meta-level). For instance, Figure 12 shows that, at iteration 1, a fV-narrowing tree was expanded whose root term is the specialized call dec(M:Data,s(0)) (Line 47). The root can be narrowed to the leaf a (Line 48) with the computed substitution {M $\mapsto$ b} (Line 49), which allows the resultant equation dec(b,s(0)) = a to be generated (Line 50). Furthermore, Figure 13 shows (a fragment of) the fV-narrowing tree for the specialized call dec(M:Data,s(0)) of Line 47 that has been generated by the ${\sf Narval}$ system. ^{Footnote 24}

Fig. 11.

Specialized client-server communication protocol after the compression phase.

Fig. 12.

Inspecting the specialization process.

Topmost extension transformation. The topmost extension transformation of Section 3.2 has been fully implemented in $\tt{{Presto}}$ . Since the topmost property is not required to perform the PE, it can be applied either ex-ante to the original input program (and it is preserved by the specialization) or ex-post to the specialized program. The transformation enables narrowing-based search reachability for all topmost modulo Ax programs, and particularly for object-oriented specifications. Reachability goals can be solved in $\tt{{Presto}}$ through the connection to the Narval system (Alpuente et al. Reference Alpuente, Ballis, Escobar and Sapiña2019b), which provides a graphical environment for symbolic analysis in Maude. This feature is illustrated in the system quick start guide.

FVP and Strong irreducibility checkers. $\tt{{Presto}}$ includes a FVP checker for equational theories that is based on the checking procedure described in Meseguer (Reference Meseguer2015). All of the theories that satisfy the FVP can be specialized by using the unfolding operator $\mathcal{U}_{\mathit{FVP}}$ instead of the typically costlier operator $\mathcal{U}_{\overline{\mathit{FVP}}}$ . As discussed in Section 3, the checker implements a semi-decidable procedure that terminates when the FVP holds for the equational theory under examination. If the FVP does not hold, the user has to manually stop the checking process or wait for the time-out; otherwise, the process would produce an infinite number of most general variants for some terms. For instance, consider the Client-Server Communication Protocol with FVP that is available in the $\tt{{Presto}}$ preloaded examples. This Maude specification is a slight mutation of the client-server communication protocol of Example 9 that models the Caesar cypher by using a finite variant equational theory. By clicking the Check FVP button, the checking process starts and, in this case, the check succeeds since the flat terms associated with the program operators have only a finite number of most general variants, as illustrated in Figure 14. Hence, the specification could be safely specialized by using the $\mathcal{U}_{\mathit{FVP}}$ unfolding operator without the risk of jeopardizing termination.

Fig. 13.

Fragment of the fV-narrowing tree for dec(M:Data,s(0)).

Fig. 14.

FVP checking of the Client-Server Communication Protocol with FVP.

Moreover, $\tt{{Presto}}$ implements an efficient checker for the $(\vec{E},B)$ -strong irreducibility of the left-hand side of the rewrite rules of the input program. As discussed at the end of Section 4.2, strong irreducibility is an essential requirement for the completeness of the specialization algorithm. Figure 15 illustrates the outcome of the strong irreducibility check for a variant of the Client-Server Communication Protocol with FVP that includes the rewrite rule

Fig. 15.

Strong irreducibility failure for a variant of the Client-Server Communication Protocol with FVP.

Note that the check fails due to the narrowable subterm enc(Q:Message, K:Nat) occurring in the left-hand side of the considered rule.

Iterative specialization. $\tt{{Presto}}$ can be automatically re-applied to any generated specialization in an iterative manner. After completing a given specialization for a rewrite theory, the user can perform a further specialization process to re-specialize the given outcome by using a distinct unfolding operator. This is achieved by simply pressing the Specialize button again, which is directly displayed after the specialization and avoids the need to reload the initial web input form to manually enter the intermediate program to be re-specialized. As shown in Alpuente et al. (Reference Alpuente, Ballis, Escobar, Meseguer, Sapiña, Gallagher, Giacobazzi and López-Garca2021a), this feature is particularly useful in the case when a given input rewrite theory $\mathcal{R}$ must be specialized using $\mathcal{U}_{\overline{\mathit{FVP}}}$ , since its equational theory does not satisfy the FVP, while the resulting specialization $\mathcal{R}'$ hosts an equational theory that does satisfy the FVP so that $\mathcal{R}'$ can be further specialized by using the $\mathcal{U}_{\mathit{FVP}}$ operator. For a detailed session with $\tt{{Presto}}$ that illustrates this feature, we refer to the $\tt{{Presto}}$ quick start guide.

Total evaluation. This feature provides a slightly modified version of the unfolding operator $\mathcal{U}_{\mathit{FVP}}$ that implements the total evaluation transformation of Meseguer (Reference Meseguer2020) for sufficiently complete equational theories that have the FVP. By means of a suitable sort downgrading, which is described in Meseguer (Reference Meseguer2020), function calls always generate values and cannot be stuck in an intermediate, partial result. In this scenario, unfolding can safely rule out variants that are not constructor terms. This means that all of the specialized calls get totally evaluated and the maximum compression is achieved, thereby dramatically reducing the search space for the construction of the specialized theories as shown in Alpuente et al. (Reference Alpuente, Ballis, Escobar, Meseguer, Sapiña, Gallagher, Giacobazzi and López-Garca2021a).

For instance, the specialized rewrite theory Client-Server Communication Protocol with FVP can be totally evaluated into the extremely compact rewrite theory of Figure 16, which does not include any equation. Actually, all calls to the encryption and decryption functions have been totally evaluated, and their values have been hard-coded into their place in the specialized rewrite rules.

Fig. 16.

Total evaluation of the Client-Server Communication Protocol with FVP.

7 Experimental evaluation of $\tt{{Presto}}$

Table 1 contains the experiments that we have performed with $\tt{{Presto}}$ using an Intel Xeon E5-1660 3.3GHz CPU with 64 GB RAM running Maude v3.0 and considering the average of ten executions for each test. These experiments, together with the source code of all of the examples are also publicly available at $\tt{{Presto}}$ ’s website.

Table 1.

Experimental results for the specialization of rewrite theories with $\tt{{Presto}}$ .

We have considered the following benchmark programs: Cond-Cli-Srv-OO, the conditional, object-oriented, client-server communication protocol of Example 9; Cli-Srv, a re-encoding of Cond-Cli-Srv-OO that does not use either Maude built-in object-oriented features or conditional rules; Cli-Srv-Mod, a variant of Cli-Srv where we introduce an extra function (i.e., the mod function that computes the remainder of the integer division) in the underlying equational theory that is commonly used in protocol specification and makes the key generation heavier; Cli-Srv-FVP, a variant of Cli-Srv for one-symbol messages whose equational theory meets the FVP and differs from the one in Example 10 in using Presburger’s encoding for natural numbers; Diffie-Hellman, the well-known network protocol for safely sharing keys between two nodes over an untrusted channel; Cond-Diffie-Hellman-OO, a conditional, object-oriented specification of the Diffie-Hellman protocol; Handshake-KMP, an unconditional rewrite theory that specifies a simple handshake protocol in which a client sends an arbitrary long and noisy message M to a server. The handshake succeeds if the server can recognize a secret handshake sequence P inside the client message M by matching P against M via the well-known KMP string matching algorithm; and Cond-Handshake-KMP-OO, a conditional, object-oriented version of Handshake-KMP.

As for the experiments with Cli-Srv, Cli-Srv-Mod and Cond-Cli-Srv-OO, we considered input messages of three different sizes: from twenty-five thousand symbols to one million symbols. This cannot be done for Cli-Srv-FVP since it encodes one-symbol messages, and, hence, we cannot use this parameter for benchmarking purposes. Similarly, Handshake-KMP and Cond-Handshake-KMP-OO consider fixed-size messages of 350 symbols, while Diffie-Hellman and Cond-Diffie-Hellman-OO are specialized w.r.t. fixed-size keys (modeled as natural numbers obtained though exponentiation). For these experiments, we use as benchmark parameter the number of client requests sent over a time-bounded period of time. We considered one, five, and ten millions requests. The column Size in Table 1 indicates either the message length parameter or the number of client requests according to the benchmark program considered.

For each experiment, we executed the original specification $\mathcal{R}$ and the specialized one $\mathcal{R}'$ on the very same input states, and we recorded the following data: the execution times (in ms) $T_\mathcal{R}$ and $T_\mathcal{R}'$ , the total number of rewrites $\#Rews_{\mathcal{R}}$ and $\#Rews_{\mathcal{R}'}$ , the percentage of reduction in terms of number of rewrites, and the specialization speedup computed as the ratio $T_{\mathcal{R}} / T_{\mathcal{R}'}$ .

Our figures show that the specialized rewrite theories achieve a significant improvement in execution time when compared to the original theory, with an average speedup for these benchmarks of $59.24$ . Particularly remarkable is the performance improvement of the Cond-Handshake-KMP-OO which reaches two orders of magnitude for the case when the specialized maximal calls within the rewrite theory partially instantiate the input pattern and input message. Such an impressive performance is largely due to the compression phase of the specialization algorithm that, in this case, completely deconditionalizes the rewrite rules, thereby yielding as outcome a faster, unconditional rewrite theory. This does not happen for Cond-Cli-Srv-OO which exhibits a smaller speedup. For this benchmark, complete deconditionalization cannot be achieved as shown in Example 9, hence some heavy conditional computations are kept in the specialized program as well.

We note that none of these specializations could be performed by using our earlier partial evaluator Victoria, which cannot handle rewrite theories but only equational theories. Thus, the specialization of rewrite theories supported by $\tt{{Presto}}$ could not be achieved in Victoria unless a complex hack is introduced not only at the level of the theory signature but also by providing a suitable program infrastructure that simulates rewrite rule nondeterminism through deterministic, equational evaluation.

We do not benchmark the specialization times since they are almost negligible (for most cases $<$ 100 ms). Nonetheless, we compared the performance of the unfolding operators $\mathcal{U}_{\mathit{FVP}}$ and $\mathcal{U}_{\overline{FVP}}$ , when both can be applied in the specialization process (i.e., when the rewrite theory to be specialized includes a finite variant equational theory). The most significant difference appears in the Cli-Srv-FVP theory, where ${ NPER}^{\mathcal{U}_{\mathit{FVP}}}$ is 56% faster (on average) than ${ NPER}^{\mathcal{U}_{\overline{FVP}}}$ . This figure is expected and favors the use of $\mathcal{U}_{\mathit{FVP}}$ whenever it is possible since it avoids any overhead caused by homeomorphic embedding checks performed by $\mathcal{U}_{\overline{FVP}}$ . Finally, we benchmarked the symbolic execution of long-winded reachability goals in rewrite theories that include a finite variant equational theory such as the pathological theory of Example 11. The achieved improvement is also striking, with an average speedup of $16.46$ .

Let us finally discuss how Presto compares in practice with existing on-line specialization systems with related transformation power. A narrowing-based partial evaluator for the lazy functional logic language Curry is described in Hanus and Peemöller (2014) and Peemöller (2017) whose implementation can be seen as an instance of the generic narrowing-based PE framework of Alpuente et al. (Reference Alpuente, Falaschi and Vidal1998b). This system improves a former prototype in Albert et al. (Reference Albert, Hanus and Vidal2002) by taking into account (mutually recursive) let expressions and non-deterministic operations, while the PE system of Albert et al. (Reference Albert, Hanus and Vidal2002) was restricted to confluent programs. Obviously, the protocol benchmarks in this paper cannot be directly specialized by using Curry’s partial evaluator since neither evaluation modulo algebraic axioms nor concurrency are supported by Curry’s partial evaluator; this would require artificially rewriting the program code so that any comparison would be meaningless. In the opposite direction, $\tt{{Presto}}$ cannot manage the specialization of higher-order functions that is achieved by Hanus and Peemöller (Reference Hanus and Peemöller2014) since RWL is not a higher-order logic. Furthermore, our partial evaluator cannot deal with many other important Curry features such as monadic I/O or encapsulated search. In order to provide some evidence of how $\tt{{Presto}}$ performs on classical specialization examples, we reproduced the standard kmp-match test ^{Footnote 25} (i.e., without using any algebraic axioms), and we benchmarked the speed and specialization that is achieved by $\tt{{Presto}}$ on this program. This example is particularly interesting because it is a kind of transformation that neither (conventional) PE nor deforestation can perform automatically while CPD ^{Footnote 26} of logic programs and positive supercompilation of functional programs can pass the test (Alpuente et al. Reference Alpuente, Falaschi and Vidal1998a; Jørgensen et al. 1996). The speedup achieved by $\tt{{Presto}}$ on this test for an input list with 500,000 elements is 58, which is comparable to the speedup of the last release of Victoria (actually, the KMP specialized programs that are generated by $\tt{{Presto}}$ and Victoria are essentially the same and they both yield an optimal specialized string matcher). Curry’s partial evaluator also produces an optimal KMP specialization and the achieved speedup for input lists of 500,000 elements is $12.22$ , which is obtained by using an unlimited unfolding strategy that, however, may risk nontermination (Peemöller Reference Peemæller2017). The corresponding specialization time of Curry’s partial evaluator reported in Peemöller (Reference Peemæller2017) is $1.61$ seconds.

We compared the specialization times achieved by $\tt{{Presto}}$ in comparison to Victoria as follows. In order to reduce the noise on the small time for a single specialization, we benchmarked the total specialization time for a loop consisting of 1000 specializations of the KMP program, and then we divided the accumulated specialization time by 1000. The resulting specialization times of Victoria and $\tt{{Presto}}$ are $6.6$ ms and $5.6$ ms, respectively, which shows that $\tt{{Presto}}$ outperforms Victoria with a performance improvement of 15%. This is noteworthy since the implementation of $\tt{{Presto}}$ is considerably more ambitious, and it provides much greater coverage compared to the simpler approach of Victoria.