Conditional Narrowing Modulo in Rewriting Logic and Maude

Abstract

This work studies the relationship between verifiable and computable answers for reachability problems in rewrite theories with an underlying membership equational logic. These problems have the form

$$\begin{aligned} (\exists \bar{x})s(\bar{x})\rightarrow ^* t(\bar{x}) \end{aligned}$$

with $\bar{x}$ some variables, or a conjunction of several of these subgoals. A calculus that solves this kind of problems has been developed and proved correct. Given a reachability problem in a rewrite theory, this calculus can compute any normalized answer that can be checked by rewriting, or a more general one. Special care has been taken in the calculus to keep membership information attached to each term, using this information whenever possible.

Research supported by MINECO Spanish project StrongSoft (TIN2012–39391–C04–04) and Comunidad de Madrid program PROMETIDOS (S2009/TIC-1465).

1 Introduction

Rewriting logic is a computational logic that has been around for more than twenty years [Mes90], whose semantics [BM06] has a precise mathematical meaning allowing mathematical reasoning for property proving, providing a more flexible framework for the specification of concurrent systems. It turned out that it can express both concurrent computation and logical deduction, allowing its application in many areas such as automated deduction, software and hardware specification and verification, security, etc. One important property of rewriting logic is reflection [CM96]. Intuitively, reflection means representing a logic’s metalevel at the object level, allowing the definition of strategies that guide rule application in an object-level theory.

Reachability problems have the form

$$\begin{aligned} (\exists \bar{x})s(\bar{x})\rightarrow ^* t(\bar{x}) \end{aligned}$$

with $\bar{x}$ some variables, or a conjunction of several of these subgoals. They can be solved by model checking methods for finite state spaces. A technique known as narrowing [Fay78] that was first proposed as a method for solving equational goals (unification), has been extended to cover also reachability goals [MT07], leaving equational goals as a special case of reachability goals. In recent years the idea of variants of a term has been applied to narrowing. A strategy for order-sorted unconditional rewrite theories known as folding variant narrowing [ESM12], which computes a complete set of variants of any term, has been developed by Escobar, Sasse and Meseguer, allowing unification modulo a set of equations and axioms. The strategy terminates on any input term on those systems enjoying the finite variant property, and it is optimally terminating. It is being used for cryptographic protocol analysis [MT07], with tools like Maude-NPA [EMM05], termination algorithms modulo axioms [DLM+08], and algorithms for checking confluence and coherence of rewrite theories modulo axioms, such as the Church-Rosser (CRC) and the Coherence (ChC) Checkers for Maude [DM12].

This work explores narrowing for membership conditional rewrite theories, going beyond the scope of folding variant narrowing which works on order-sorted unconditional rewrite theories. A calculus that computes answers to reachability problems in membership conditional rewrite theories has been developed and proved correct with respect to idempotent normalized answers.

The work is structured as follows: in Sect. 2 all needed definitions and properties for rewriting and narrowing are introduced. Section 3 introduces the first part of the narrowing calculus, the one that deals with equational unification. Section 4 introduces the part of the calculus dealing with reachability and its proof of correctness. Section 5 shows the calculus at work. In Sect. 6, related work, conclusions and current lines of investigation for this work are presented. An extended version of this paper, with all the missing proofs, can be found at http://maude.sip.ucm.es/cnarrowing/, together with a previous version of this work with transformation rules and a prototype.

2 Preliminaries

We assume familiarity with rewriting logic [BM06]. There are several language implementations of rewriting logic, including Maude [CDE+07]. Rewriting logic is parameterized by an underlying equational logic. In Maude’s case this logic is membership equational logic [Mes97].

2.1 Tower of Hanoi Example

Throughout this paper the Tower of Hanoi puzzle will be used as a motivating example to explain the definitions in a less abstract way. We have Rods a, b and c, and Disks 1, 2, 3 and 4 which can slide onto any Rod. We call a Rod with zero or more stacked Disks (written juxtaposed) a Tower. If smaller Disks are always stacked on top of bigger Disks we have a ValidTower (abbreviated VT). A set of valid towers (written separated by commas) is a State (abbreviated St). A move between a Pair of towers (written separated by a $-$ symbol) is defined by the rules: 1) only one Disk may be moved at a time, 2) each move consists of taking the upper Disk from one Tower and placing it on top of another Tower, and 3) Disk $X$ may be placed on top of Disk $Y$ only if $X$ is smaller than $Y$ (written $X<Y=\mathtt {t}$, where t is the true Boolean value). The goal of the puzzle is to reach a desired State from a given initial State.

2.2 Membership Equational Logic

A membership equational logic (Mel) signature [BM06] is a triple $\varSigma =(K,\varOmega ,S)$, with $K$ a set of kinds, $\varOmega =\lbrace \varSigma _{w;k}\rbrace _{(w;k)\in K^{*}\mathsf {x}K}$ a many-kinded algebraic signature, and $S=\lbrace S_{k}\rbrace _{k\in K}$ a $K$-kinded family of disjoint sets of sorts. For simplicity, we only allow overloading of operators whenever the result belongs in the same kind. The kind of a sort $s$ is denoted by $[s]$. The sets $T_{\varSigma ,s}$, $T_{\varSigma }(X)_{s}$, $T_{\varSigma ,k}$ and $T_{\varSigma }(X)_{k}$ denote, respectively, the set of ground $\varSigma$-terms with sort $s$, the set of $\varSigma$-terms with sort $s$ over the set $X$ of sorted variables, the set of ground $\varSigma$-terms with kind $k$ and the set of $\varSigma$-terms with kind $k$ over the set $X$ of sorted variables. We write $T_{\varSigma }$, $T_{\varSigma }(X)$ for the corresponding term algebras. $Var (t) \subseteq X$ denotes the set of variables in $t\in T_{\varSigma }(X)$.

In the Tower of Hanoi puzzle, $\varSigma = (K,\varOmega ,S)$ is:

• $K = \lbrace \mathtt {TS}, \mathtt {P}, \mathtt {D}, \mathtt {B}\rbrace ,$

• $\varOmega = \lbrace \cdot _{\mathtt {D}\ \mathtt {TS};\mathtt {TS}},\, ,_{\mathtt {TS}\ \mathtt {TS};\mathtt {TS}},\ -_{\mathtt {TS}\ \mathtt {TS};\mathtt {P}},\,\mathtt{move }_{\mathtt {P};\mathtt {P}},\,<_{\mathtt {D}\ \mathtt {D};\mathtt {B}}\rbrace ,$

• $S = \lbrace S_{\mathtt {TS}},S_{\mathtt {P}},S_\mathtt {D},S_\mathtt {B}\rbrace$, where

  $S_{\mathtt {TS}} = \lbrace \mathtt {Rod},\mathtt {VT},\mathtt {Tower},\mathtt {St}\rbrace$, $S_\mathtt {P} = \lbrace \mathtt {Pair}\rbrace$, $S_\mathtt {D} = \lbrace \mathtt {Disk}\rbrace$, $S_\mathtt {B} = \lbrace \mathtt {Boolean}\rbrace$.

Finally, $\lbrace \mathtt {a},\mathtt {b},\mathtt {c}\rbrace$, $\lbrace \mathtt {1},\mathtt {2},\mathtt {3},\mathtt {4}\rbrace$, and $\lbrace \mathtt {t}\rbrace$ are the atoms with sort Rod, Disk, and Boolean respectively.

Positions in a term $t$: we represent the root of $t$ as $\epsilon$ and the other positions as strings of nonzero natural numbers in the usual way, considering $t$ as a tree. The set of positions of a term is written $Pos (t)$. $t|_{p}$ is the subtree below position $p$. $t[u]_{p}$ is the replacement in $t$ of the subterm at position $p$ with term $u$.

A substitution $\sigma :Y\rightarrow T_{\varSigma }(X)$ is a function from a finite set of sorted variables $Y\subseteq X$ to $T_{\varSigma }(X)$ such that $\sigma (y)$ has the same or lower sort as that of the variable $y\in Y$ ($s_1\le s_2$, formally defined in the next paragraph). Substitutions are written as $\sigma {=}\lbrace x_{1}{\mapsto } t_{1},{\ldots },x_{n}{\mapsto } t_{n}\rbrace$ where $Dom (\sigma ){=}\lbrace x_{1},{\ldots },x_{n}\rbrace$ and $Ran (\sigma ){=}\bigcup ^n_{i{=}1} Var (t_i)$. The identity substitution is $id$. The restriction of $\sigma$ to a set of variables $V$ is $\sigma |_{V}$. Composition of two substitutions is denoted by $\sigma \sigma '$. For substitutions $\sigma$ and $\sigma '$ where $Dom (\sigma ){\cap } Dom (\sigma '){=}\emptyset$, we denote their union by $\sigma \cup \sigma '$.

A Mel theory [BM06] is a pair $(\varSigma ,\mathcal {E})$, where $\varSigma$ is a Mel signature and $\mathcal {E}$ is a finite set of Mel sentences, either conditional equations or conditional memberships of the forms:

$$\begin{aligned} (\forall X)\ t{=}t'\ \mathtt {if}\ \bigwedge \limits _{i}A_i,\quad (\forall X)\ t{:}s\ \mathtt {if}\ \bigwedge \limits _{i}A_i \end{aligned}$$

for $t,t'\in T_{\varSigma }(X)_{k}$ and $s\in S_{k}$, the latter stating that $t$ is a term of sort $s$, provided the condition holds, and each $A_i$ can be of the form $t{=}t'$, $t{:}s$, or $t{:=}t'$ (a matching equation). Matching equations are treated as ordinary equations, but they impose a limitation in the syntax of admissible Mel theories, as we will see. We also admit unconditional sentences in $\mathcal {E}$. Order-sorted (sugared) notation $s_{1}\le s_{2}$ can be used instead of $(\forall x{:}[s_1])\ x{:}s_{2}\ \mathtt {if}\ x{:}s_{1}$. An operator declaration $f:s_{1}\times \cdots \times s_{n}\rightarrow s$ corresponds to declaring $f$ at the kind level and giving the membership axiom $(\forall x_{1}{:}[s_{1}],\ldots ,x_{n}{:}[s_{n}])\ f(x_{1},\ldots ,x_{n}){:}s\ \mathtt {if}\ \bigwedge _{1\le i\le n}x_{i}{:}s_{i}$. Given a Mel sentence $\phi$, we denote by $\mathcal {E}\vdash \phi$ that $\phi$ can be deduced from $\mathcal {E}$ using the rules in Fig. 1, where $=$ can be either $=$ or $:=$ as explained before [BM12]. The rules of Fig. 1 specify a sound and complete calculus. A Mel theory $(\varSigma ,\mathcal {E})$ has an initial algebra, denoted by $T_{\varSigma /\mathcal {E}}$, whose elements are the equivalence classes $[t]_{\mathcal {E}}\subseteq T_{\varSigma }$ of ground terms identified by the equations in $\mathcal {E}$.

Fig. 1.

Deduction rules for membership equational logic.

The Mel theory for the Tower of Hanoi puzzle consists of $\varSigma =(K,\varOmega ,S)$ and the following set $\mathcal {E}$ of Mel sentences where we omit the universal quantifiers:

A single Disk stacked on a Rod is always a ValidTower. For multiple Disks, we compare them recursively. The operator move distinguishes between two cases: if one Tower is empty, i.e. a Rod, then we can stack any Disk on it; else the sizes of the top Disks on each Tower must be compared ($\mathtt{< }$) and we can stack the smaller one on top of the other.

2.3 Rewriting Logic

A rewrite theory $\mathcal {R}=(\varSigma ,\mathcal {E},R)$ consists of a Mel theory $(\varSigma ,\mathcal {E})$ together with a finite set $R$ of conditional rewrite rules each of which has the form

$$\begin{aligned} (\forall X)\ l\rightarrow r\ \mathtt {if}\ \bigwedge _{i}p_{i}{=}q_{i}\wedge \bigwedge _{j}w_{j}{:}s_{j}\wedge \bigwedge _{k} l_{k}\rightarrow r_{k}, \end{aligned}$$

where $l,r$ are $\varSigma$-terms of the same kind and $=$ can be either $=$ or $:=$. Rewrite rules can also be unconditional.

Such a rewrite rule specifies a one-step transition from a state $t[l\theta ]_{p}$ to the state $t[r\theta ]_{p}$, denoted by $t[l\theta ]_{p}\rightarrow ^{1}_{R}t[r\theta ]_{p}$, provided the condition holds. The subterm $t|_{p}$ is called a redex.

In the example, $R$ has as only element the conditional rewrite rule: $D,E\rightarrow F,G\ if\ D:\mathtt {Tower}\wedge E:\mathtt {Tower}\wedge F-G:=\mathtt{move }(D-E)\wedge F:\mathtt {Tower}\wedge G:\mathtt {Tower}$.

$F$ and $G$ are new variables on the right side of the rule. They are instantiated by matching on the conditional part of the rule.

The inference rules in Fig. 2 for rewrite theories can infer all possible computations in the system specified by $\mathcal {R}$ [BM12]. We can reach a state $v$ from a state $u$ if we can prove $\mathcal {R}\vdash u\rightarrow v$.

Fig. 2.

Deduction rules for rewrite theories.

The relation $\rightarrow ^{1}_{R/\mathcal {E}}$ on $T_{\varSigma }(X)$ is $=_{\mathcal {E}}{\circ }\rightarrow ^{1}_{R}{\circ }=_{\mathcal {E}}$. $\rightarrow ^{1}_{R/\mathcal {E}}$ on $T_{\varSigma }(X)$ induces a relation $\rightarrow ^{1}_{R/\mathcal {E}}$ on $T_{\varSigma /\mathcal {E}}(X)$, the equivalence relation modulo $\mathcal {E}$, by $[t]_{\mathcal {E}}\rightarrow ^{1}_{R/\mathcal {E}}[t']_{\mathcal {E}}$ iff $t\rightarrow ^{1}_{R/\mathcal {E}}t'$. The transitive (resp. transitive and reflexive) closure of $\rightarrow ^{1}_{R/\mathcal {E}}$ is denoted $\rightarrow ^{+}_{R/\mathcal {E}}$ (resp. $\rightarrow ^{*}_{R/\mathcal {E}}$). We say that a term $t$ is $\rightarrow _{R/\mathcal {E}}$-irreducible (or just $R/\mathcal {E}$-irreducible) if there is no term $t'$ such that $t\rightarrow ^{1}_{R/\mathcal {E}} t'$.

A rewrite rule $l\rightarrow r\ \mathtt {if}\ cond$, is sort-decreasing if for each substitution $\sigma$, we have that for any sort $s$ if $l\sigma \in T_{\varSigma }(X)_{s}$ and $( cond )\sigma$ is verified implies $r\sigma \in T_{\varSigma }(X)_{s}$. A $\varSigma$-equation $t=t'$ is regular if $Var (t)= Var (t')$. It is sort-preserving if for each substitution $\sigma$, we have $t\sigma \in T_{\sigma }(X)_{s}$ implies $t'\sigma \in T_{\sigma }(X)_{s}$ and vice versa.

A substitution is called $\mathcal {E}$-normalized (or normalized) if $x\sigma$ is $\mathcal {E}$-irreducible for all $x\in V$.

The relation $\rightarrow ^{1}_{R/\mathcal {E}}$ is terminating if there are no infinite rewriting sequences. The relation $\rightarrow ^{1}_{R/\mathcal {E}}$ is operationally terminating if there are no infinite well-formed proof trees. The relation $\rightarrow ^{1}_{R/\mathcal {E}}$ is confluent if whenever $t{\rightarrow ^{*}_{R/\mathcal {E}}}t'$ and $t{\rightarrow ^{*}_{R/\mathcal {E}}}t''$, there exists a term $t'''$ such that $t'{\rightarrow ^{*}_{R/\mathcal {E}}}t'''$ and $t''{\rightarrow ^{*}_{R/\mathcal {E}}}t'''$. In a confluent, terminating, sort-decreasing, and operationally terminating membership rewrite theory, for each term $t\in T_{\varSigma }(X)$, there is a unique (up to $\mathcal {E}$-equivalence) $R/\mathcal {E}$-irreducible term $t'$ obtained by rewriting to canonical form, denoted by $t\rightarrow ^{!}_{R/\mathcal {E}}t'$, or $t\downarrow _{R/\mathcal {E}}$ when $t'$ is not relevant, which we call $can _{R/\mathcal {E}}(t)$.

2.4 Executable Rewrite Theories

For a rewrite theory $\mathcal {R}=(\varSigma ,\mathcal {E},R)$, whether a one step rewrite $t\rightarrow ^{1}_{R/\mathcal {E}}t'$ holds is undecidable in general. We impose additional conditions, similar to those required for functional and system modules in Maude, under which we can decide if $t\rightarrow ^{1}_{R/\mathcal {E}}t'$ holds. We decompose $\mathcal {E}$ into a disjoint union $E\cup A$, with $A$ a set of equational axioms (such as associativity, and/or commutativity, and/or identity). We define the relation $\rightarrow ^{1}_{E,A}$ on $T_{\varSigma }(X)$ as follows: $t\rightarrow ^{1}_{E,A}t'$ if there is a position $\omega \in Pos (t)$, an equation $l=r\ \mathtt {if}\ cond \in E$, and a substitution $\sigma$ such that $t|_{\omega }=_{A}l\sigma$ ($A$-matching), $( cond )\sigma$ is satisfied, and $t'=t[r\sigma ]_{\omega }$. The relation $\rightarrow ^{1}_{R,A}$ is similarly defined. We define $\rightarrow ^{1}_{R\cup E,A}$ as $\rightarrow ^{1}_{R,A}\cup \rightarrow ^{1}_{E,A}$. A rewrite theory $\mathcal {R}=(\varSigma ,E\cup A,R)$ is executable if each kind $k$ in $\varSigma$ is nonempty, $E$, $A$, and $R$ are finite and the following conditions hold:

• 1. $E$ and $R$ are operationally terminating and admissible [CDE+07]. Then we have a deterministic 3-CTRS [Ohl02]. Any new variable in the conditions will be instantiated by matching. New variables are distinguished in Maude by using a ${:=}$ symbol instead of $=$ in the condition. They appear on the left terms of these matching equations. Conditions in deterministic 3-CTRS’s must be solved in left to right order.

• 2. Equality modulo $A$ is decidable and there exists a finite matching algorithm modulo $A$ producing a finite number of A-matching substitutions, or failing otherwise.

• 3. The equations in $E$ are sort-decreasing, and terminating and confluent modulo A when we consider them as oriented rules, where $\rightarrow ^1_{E/A}$ is defined in the same way as we did for $\rightarrow ^{1}_{R/\mathcal {E}}$.

• 4. $\rightarrow _{E,A}$ is coherent with $A$, i.e., $\forall t_1,t_2,t_3$ we have $t_1\rightarrow ^+_{E,A}t_2$ and $t_1=_A t_3$ implies $\exists t_4,t_5$ such that $t_2\rightarrow ^*_{E,A}t_4, t_3\rightarrow ^+_{E,A}t_5$ and $t_4=_A t_5$ [MT07].

  $$\begin{array}{ccccc} t_1 \;\; &{} \rightarrow ^+_{E,A} &{} t_2 &{} \rightarrow ^*_{E,A} \; \; &{} t_4 \\ \parallel _{A} &{} &{} &{} &{} \parallel _{A} \\ t_3 &{} &{} \longrightarrow ^+_{E,A} &{}&{} t_5 \end{array} $$

• 5. $\rightarrow _{R,A}$ is $\mathcal {E}$ -consistent with $A$, i.e., $\forall t_1,t_2,t_3$ we have $t_1\rightarrow _{R,A}t_2$ and $t_1=_A t_3$ implies $\exists t_4$ such that $t_3\rightarrow _{R,A}t_4$ and $t_2=_\mathcal {E}t_4$. Also $\rightarrow _{R,A}$ is $\mathcal {E}$ -consistent with $\rightarrow _{E,A}$, i.e., $\forall t_1,t_2,t_3$ we have $t_1\rightarrow _{R,A}t_2$ and $t_1\rightarrow ^*_{E,A} t_3$ implies $\exists t_4,t_5$ such that $t_3\rightarrow ^*_{E,A}t_4$ and $t_4\rightarrow _{R,A}t_5$ and $t_2=_{\mathcal {E}}t_5$. In both cases the $\rightarrow _{R,A}$ rewriting steps from $t_3$ and $t_4$ must be performed with the same rule that was applied to $t_1$ [MT07].

  

Technically, what coherence means is that the weaker relation $\rightarrow ^{1}_{E,A}$ becomes semantically equivalent to the stronger relation $\rightarrow ^{1}_{E/A}$, so we can decide $t\rightarrow ^{1}_{R/\mathcal {E}}t'$ by finding $t''$ such that $can _{E,A}(t)\rightarrow ^{1}_{R}t''$ and $can _{E,A}(t')=_A can _{E,A}(t'')$, which is decidable, since the number of rules is finite and $A$-matching is decidable and finite.

Under these conditions we can implement $\rightarrow _{R/\mathcal {E}}$ on terms using $\rightarrow _{R\cup E,A}$ [MT07]. This lemma links $\rightarrow _{R/\mathcal {E}}$ with $\rightarrow _{E,A}$ and $\rightarrow _{R,A}$. Patrick Viry gave a proof for unsorted unconditional rewrite theories [Vir94], which can easily be lifted to our membership conditional case.

Lemma 1

Let $\mathcal {R}=(\varSigma ,\mathcal {E},R)$ be an executable rewrite theory, that is, it has all the properties specified in Sect. 2.4. Then $t_1\rightarrow _{R/\mathcal {E}}t_2$ if and only if $t_1\rightarrow ^*_{E,A}\rightarrow _{R,A}t_3$ for some $t_3=_{\mathcal {E}}t_2$.

The rewrite theory for the Tower of Hanoi puzzle is executable if we decompose $\mathcal {E}$ in the following way: the set $A$ has as elements the associative equation and the commutative equations in $\mathcal {E}$; the set $E$ has as elements the rest of equations and all memberships in $\mathcal {E}$, and we add to $R$ the following rule needed for $\mathcal {E}$-consistency:

2.5 Unification

Given a rewrite theory $\mathcal {R}=(\varSigma ,\mathcal {E},R)$, a $\varSigma$-equation is an expression of the form $t=t'$ where $t,t'\in T_{\varSigma }(X)_{s}$ for an appropriate $s$. The $\mathcal {E}$-subsumption preorder $\ll _{\mathcal {E}}$ on $T_{\varSigma }(X)_{s}$ is defined by $t\ll _{\mathcal {E}}t'$ if there is a substitution $\sigma$ such that $t=_{\mathcal {E}}t'\sigma$. For substitutions $\sigma ,\rho$ and a set of variables $V$ we define $\sigma |_{V}\ll _{\mathcal {E}}\rho |_{V}$ if there is a substitution $\eta$ such that $\sigma |_{V}=_{\mathcal {E}}(\rho \eta )|_{V}$. Then we say that $\rho$ is more general than $\sigma$ with respect to $V$. When $V$ is not specified, we assume that $V= Dom (\sigma )= Dom (\rho )$ and we say that $\rho$ is more general than $\sigma$.

A system of equations $F$ is a conjunction of the form $t_{1}=t'_{1}\wedge \ldots \wedge t_{n}=t'_{n}$ where for $1\le i\le n$, $t_{i}=t'_{i}$ is a $\varSigma$-equation. We define $Var (F)=\bigcup _{i} Var (t_{i})\cup Var (t'_{i})$. An $\mathcal {E}$-unifier for $F$ is a substitution $\sigma$ such that $t_{i}\sigma =_{\mathcal {E}}t'_{i}\sigma$ for $1\le i\le n$. For $V= Var (F)\subseteq W$, a set of substitutions $CSU ^W_{\mathcal {E}}(F)$ is said to be a complete set of unifiers modulo $\mathcal {E}$ of $F$ away from $W$ if

• each $\sigma \in CSU ^W_{\mathcal {E}}(F)$ is an $\mathcal {E}$-unifier of $F$;

• for any $\mathcal {E}$-unifier $\rho$ of $F$ there is a $\sigma \in CSU ^W_{\mathcal {E}}(F)$ such that $\rho |_{V}\ll _{\mathcal {E}}\sigma |_{V}$;

• for all $\sigma \in CSU ^W_{\mathcal {E}}(F)$, $Dom (\sigma )\subseteq V$ and $Ran (\sigma )\cap W=\emptyset$.

An $\mathcal {E}$-unification algorithm is complete if for any given system of equations it generates a complete set of $\mathcal {E}$-unifiers, which may not be finite. A unification algorithm is said to be finite and complete if it terminates after generating a finite and complete set of solutions.

2.6 Reachability Goals

Given a rewrite theory $\mathcal {R}=(\varSigma ,\mathcal {E},R)$, a reachability goal $G$ is a conjunction of the form $t_{1}\rightarrow ^{*}t'_{1}\wedge \ldots \wedge t_{n}\rightarrow ^{*}t'_{n}$ where for $1\le i\le n$, $t_{i},t'_{i}\in T_{\varSigma }(X)_{s_{i}}$ for appropriate $s_{i}$. We define $Var (G)=\bigcup _{i} Var (t_{i})\cup Var (t'_{i})$. A substitution $\sigma$ is a solution of $G$ if $t_{i}\sigma \rightarrow ^{*}_{R/\mathcal {E}}t'_{i}\sigma$ for $1\le i\le n$. We define $\mathrm {E}(G)$ to be the system of equations $t_{1}=t'_{1}\wedge \ldots \wedge t_{n}=t'_{n}$. We say $\sigma$ is a trivial solution of $G$ if it is an $\mathcal {E}$-unifier for $\mathrm {E}(G)$. We say $G$ is trivial if the identity substitution $id$ is a trivial solution of $G$.

For goals $G:t_{1}\rightarrow ^{*}t_{2}\wedge \ldots \wedge t_{2n-1}\rightarrow ^{*}t_{2n}$ and $G':t'_{1}\rightarrow ^{*}t'_{2}\wedge \ldots \wedge t'_{2n-1}\rightarrow ^{*}t'_{2n}$ we say $G=_{\mathcal {E}}G'$ if $t_{i}=_{\mathcal {E}}t'_{i}$ for $1\le i\le 2n$. We say $G\rightarrow _{R}G'$ if there is an odd $i$ such that $t_{i}\rightarrow _{R}t'_{i}$ and for all $j\ne i$ we have $t_{j}=t'_{j}$. That is, $G$ and $G'$ differ only in one subgoal ($t_i\rightarrow t_{i{+}1}$ vs $t'_i\rightarrow t_{i{+}1}$), but $t_i\rightarrow t'_{i}$, so when we rewrite $t_i$ in $G$ to $t'_i$ we get $G'$. The relation $\rightarrow _{R/\mathcal {E}}$ over goals is defined as $=_{\mathcal {E}}\circ \rightarrow _{R}\circ =_{\mathcal {E}}$.

2.7 Narrowing

Let $t$ be a $\varSigma$-term and $W$ be a set of variables such that $Var (t)\subseteq W$. The $R,A$-narrowing relation on $T_{\varSigma }(X)$ is defined as follows: $t\rightsquigarrow _{p,\sigma ,R,A}t'$ if there is a non-variable position $p\in \textit{Pos}_{\varSigma }(t)$, a rule $l\rightarrow r\ \mathtt {if}\ cond$ in $R$, properly renamed, such that $Var (l)\cap W=\emptyset$, and a unifier $\sigma \in CSU ^{W'}_{A}(t|_{p}=l)$ for $W'=W\cup Var (l)$, such that $t'=(t[r]_{p})\sigma$ and $( cond )\sigma$ holds. Similarly $E,A$-narrowing and $R\cup E,A$-narrowing relations are defined.

2.8 Associated Rewrite Theory

Any executable Mel theory $(\varSigma ,E\cup A )$ has a corresponding rewrite theory $\mathcal {R}_E=(\varSigma ', A ,R_E)$ associated to it [DLM+08]: we add a fresh new kind $Truth$ with a constant $tt$ to $\varSigma$, and for each kind $k\in K$ an operator $eq :\ k\ k\rightarrow Truth$. $\top$ represents a conjunction of any number of $tt$’s. There are rules $eq (x{:}k,x{:}k)\rightarrow tt$ for each kind $k\in K$. For each conditional equation or membership in $E$ the set $R_E$ has a conditional rule or membership of the form

$$\begin{aligned} t\rightarrow t'\ if \ A_1^\bullet \wedge \ldots \wedge A_n^\bullet \quad \quad t{:}s\ if \ A_1^\bullet \wedge \ldots \wedge A_n^\bullet \end{aligned}$$

where if $A_i$ is a membership then $A_i^\bullet {=}A_i$, if $A_i\equiv t_i{:=}t'_i$ then $A_i^\bullet$ is $t'_i{\rightarrow }t_i$, and if $A_i\equiv t{=}t'$ then $A_i^\bullet$ is $eq (t,t'){\rightarrow } tt$.

Fig. 3.

Inference rules for membership rewriting.

Systems of equations in $(\varSigma ,E\cup A )$ with form $G\equiv \bigwedge ^m_{i=1}(s_{i}=t_{i})$ become reachability goals in $\mathcal {R}_E$ of the form $\bigwedge ^m_{i=1} eq (s_{i},t_{i})\rightarrow tt$. A substitution $\sigma$ is a solution of $G$ if there are derivations for $\bigwedge ^m_{i=1}(s_{i}\sigma =t_{i}\sigma )$, or $\bigwedge ^m_{i=1} eq (s_{i}\sigma ,t_{i}\sigma )$ rewrites to $\top$.

The inference rules for membership rewriting in $\mathcal {R}_E$ are the ones in Fig. 3, adapted from [DLM+08, Fig. 4, p. 12], where the rules are defined for context-sensitive membership rewriting.

3 Conditional Narrowing Modulo Unification

Narrowing allows us to assign values to variables in such a way that a reachability goal holds. We implement narrowing using a calculus that has the following properties:

• 1. If $\sigma$ is an $R/\mathcal {E}$-normalized idempotent solution for a reachability goal $G$, the calculus can compute a more general answer $\sigma \ll _\mathcal {E}\sigma '$ for $G$.

• 2. If the calculus computes an answer $\sigma$ for $G$, then $\sigma$ is a solution for $G$.

That is, we want to compute a complete set of answers for $G$, a set that includes a generalization of any possible solution for $G$, with respect to $R/\mathcal {E}$-normalized substitutions.

We are going to split this task into two subtasks: first we will solve the part of the calculus that deals with unification; second, we will solve the part that deals with reachability.

3.1 Calculus Rules for Unification

We assume we are working with an executable rewrite theory named $M$. We refer to the set of equations and memberships in $M$ as $E$, to the set of rules as $R$ and to the set of axioms as $A$. We also assume that we have an $A$-unification algorithm that returns a $CSU$ for any pair of terms.

A unification equation is a term $s{:}S=t{:}T$, which is a shorthand for the system of equations $s=t\wedge s=X_S\wedge t=Y_T$ (we will also write $s=t$, $s{:}S$, $t{:}T$). This means that we intend to unify $s$ and $t$, with resulting sorts $S$ and $T$ respectively. A unification goal is a sequence (understood as conjunction) of unification equations.

Admissible goals, or simply goals, are any sequence of $s{:}S{=}t{:}T$, $s{:}S{:=}t{:}T$, $s{:}S{\rightarrow }t{:}T$, $s{:}S{\rightarrow ^1}t{:}T$ and $t{:}T$. Any condition in an equation, of the form $s{=}t$ or $s{:=}t$ is turned into an admissible goal by adding inferred sorts to it. If any term $s$ is a variable or a constant, we use the sort of $s$ as inferred sort. If the term is of the form $f(\bar{s})$, we use the kind of any membership for $f$.

Our calculus is defined by the following set of inference rules derived from those in Fig. 3. The first two rules, $[u]$ and $[x]$, transform equational problems into rewriting problems modulo axioms, rule $[u]$ playing the part of the added rules $eq (x{:}k,x{:}k)\rightarrow tt$ in the associated rewrite theory; rule $[n]$ describes one step of unification narrowing where the conditions on the applied rule are turned into subgoals and the instantiated right side of the rule ($r\theta$) is required to have a sort which is a common subsort of $S$ and $T$; rule $[t]$ allows us to apply several unification narrowing steps; rule $[i]$ decomposes a term allowing rule $[n]$ to be applied to any subterm of it; rule $[r]$ allows instantiation of variables on unificable terms; rule $[m1]$ solves the membership problem for variables, and rules $[s]$ and $[m2]$ for the rest of terms, using the membership conditions in $E$:

• $[u]$ unification

  $$\begin{aligned} \frac{s{:}S=t{:}T,G'}{s{:}S'\rightarrow X_{S'}{:}S', t{:}S'\rightarrow X_{S'}{:}S',G'} \end{aligned}$$
  $$\begin{aligned} \text {where } X_{S'} \text { fresh variable, } S'\le S,S'\le T. \end{aligned}$$

• $[x]$ matching

  $$\begin{aligned} \frac{s{:}S := t{:}T,G'}{t{:}S'\rightarrow s{:}S',G'} \end{aligned}$$
  $$\begin{aligned} \text {where } S'\le S,S'\le T. \end{aligned}$$

• $[n]$ narrowing

  $$\begin{aligned} \frac{s{:}S \rightarrow ^1 X{:}T,G'}{((c,)X{:}S',G')\rho \theta } \end{aligned}$$
  $$\begin{array}{c} \text {where } s \text { is not a variable, } (c)eq \ l{=}r\ ( if \ c)\in E \text { has fresh variables,}\\ S'\le S,S'\le T,\, \theta \in CSU_A (s=l),\,\rho {=}\lbrace X\mapsto r\rbrace .\end{array}$$

• $[t]$ transitivity

  $$\begin{aligned} \frac{s{:}S \rightarrow t{:}T,G'}{s{:}S'\rightarrow ^1 X_{S'}{:}S',X_{S'}{:}S'\rightarrow t{:}S',G'} \end{aligned}$$
  $$\begin{aligned} \text {where } X_{S'} \text { fresh variable, } S'\le S,S'\le T. \end{aligned}$$

• $[i]$ imitation

  $$\begin{aligned} \frac{f(\bar{s}{:}\bar{S}){:}S\rightarrow ^1 X{:}T,G'}{G'\theta ,s_i{:}S_i\rightarrow ^1 X'_{S_i}{:}S_i, X\theta {:}S',G''\theta } \end{aligned}$$
  $$\begin{array}{c}\text {with } X {\notin } Var (s),\theta =\lbrace X\mapsto f((s_1,{\ldots },s_{i-1},X'_{S_i}{:}S_i,s_{i+1},{\ldots },s_n))\rbrace ,\\ X'_{S_i} \text { fresh variable, } S'\le S,S'\le T. \end{array}$$

• $[r]$ removal of equations

  $$\begin{aligned} \frac{s{:}S \rightarrow t{:}T,G'}{(G',s{:}S',G')\theta } \end{aligned}$$
  $$\begin{aligned} \text {with } \theta \in CSU_A (s=t),\, S'\le S, S'\le T \end{aligned}$$

• $[s]$ subject reduction

  $$\begin{aligned} \frac{s{:}S,G'}{s{:}[S]\rightarrow ^1 X_S{:}{S},G'} \end{aligned}$$
  $$\begin{aligned} X_S \text { fresh variable.} \end{aligned}$$

• $[m1]$ membership

  $$\begin{aligned} \frac{X_S{:}T,G'}{(G')\theta } \end{aligned}$$
  $$\begin{aligned} \text {where }\theta =\lbrace X_S\mapsto X'_{S'}\rbrace \text { with } X'_{S'} \text { fresh variable and } S'\le S,S'\le T. \end{aligned}$$

• $[m2]$ membership

  $$\begin{aligned} \frac{s{:}S,G'}{((c,)\,G')\theta } \end{aligned}$$
  $$\begin{array}{c} \text {where } (c)mb\,\, t{:}T\,(if\,c) \text { is a fresh variant, with } T \le S, \text { of a (conditional)}\\ \text {membership in } E, \text { and } \theta \in CSU_A (s=t). \end{array}$$

From a unification equation $u$ a derivation is made applying rules of the calculus. If the derivation ends in the empty goal, denoted by $\square$, then the composition of the substitutions used on each derivation step, restricted to those variables appearing in $u$, is a computed answer for $u$.

Theorem 1

The calculus for unification is sound and weakly complete.

That is, given a unification goal $G$, if $G\rightsquigarrow ^*_\sigma \square$ then $G\sigma$ can be derived, so $\sigma$ is a solution for $G$ in $\rightarrow _{E/A}$, and if $\rho$ is an $E/A$-normalized idempotent answer of $G$ ($G\rho \rightarrow ^*_{E/A}\top )$, then there is $\rho '$ idempotent, with $\rho \ll _A \rho '$, such that $G\rightsquigarrow _{\rho '}\square$.

Proof

We prove correctness of the calculus with respect to $E/A$-normalized idempotent substitutions for the executable Mel theory $(\varSigma ,E\cup A )$ and the corresponding rewrite theory $\mathcal {R}_E=(\varSigma ', A ,R_E)$ associated to it.

• 1. Soundness: by structural induction on the calculus rule for unification applied.

• 2. Completeness: by induction on the length of inferences in $\mathcal {R}=(\varSigma ', A ,R_E)$, looking at the last inference rule used.

4 Reachability by Conditional Narrowing

Conditional narrowing relies on conditional unification. As we have used the symbol $\rightarrow$ in the calculus rules for unification, we will use a different symbol $\Rightarrow$ in the calculus rules for reachability. Our goal, given a reachability problem $\bigwedge _i s_{i}{:}S_i\Rightarrow t_{i}{:}T_i$, is to find a solution $\sigma$ (ground or not) such that $\bigwedge _i s_{i}\sigma {:}S_i\Rightarrow _{R/\mathcal {E}} t_{i}\sigma {:}T_i$. For executable rewrite theories this is equivalent to $\bigwedge _i s_{i}\sigma {:}S_i\Rightarrow _{R\cup E,A}\bigwedge _i t_{i}\sigma {:}T_i$. These new calculus rules deal with the $\rightsquigarrow _{R,A}$ part. Narrowing, we call it replacement here, takes place only at position $\epsilon$ of terms, thanks to new transitivity and imitation calculus rules.

Reachability goals are any sequence (understood as conjunction) of subgoals of the form $s{:}S\Rightarrow t{:}T$. Admissible goals, or simply goals, are now extended to be any sequence of $s{:}S{\Rightarrow } t{:}T$, $s{:}S{\Rightarrow ^1} t{:}T$, $s{:}S{=}t{:}T$, $s{:}S{\rightarrow }t{:}T$, $s{:}S{\rightarrow ^1}t{:}T$, $s{:}S{:=}t{:}T$ and $t{:}T$. If the calculus derives the empty goal from a reachability goal $G$ with a substitution $\sigma$, then $\sigma$ is a computed answer for $G$.

As for unification, any reachability subgoal in our calculus of the form of $s{:}S\Rightarrow ^{(1)} t{:}T$ is equivalent to the admissible goal $s\Rightarrow ^{(1)} t$, $s{:}S$, $t{:}T$.

4.1 Calculus Rules for Reachability

Reachability by conditional narrowing is achieved using the calculus rules presented in Sect. 3, extended with the following calculus rules, based on the deduction rules for rewrite theories in Fig. 2. Rule $[X]$ solves reachability problems by unification; rule $[R]$ applies one step of reachability narrowing; rule $[T]$ enables reachability narrowing modulo and multiple steps of reachability narrowing. It is a direct consequence of Lemma 1; rule $[I]$ allows us to imitate narrowing at non root term positions, replacing the rewriting rule for congruence, that can now be achieved by transitivity and imitation. Recall that narrowing steps for reachability ($\Rightarrow ^1$), which are generated by rule $[T]$, impose no sort within the given kind on the right side of the step:

• $[X]$ reflexivity

  $$\begin{aligned} \frac{s{:}S \Rightarrow t{:}T,G'}{s{:}S=t{:}T,G'} \end{aligned}$$

• $[R]$ replacement

  $$\begin{aligned} \frac{s{:}S \Rightarrow ^1 X_{[S]}{:}[S],G'}{(s{:}S,(c,),G')\rho \theta } \end{aligned}$$
  $$ \begin{array}{c} \text {where } s \text { is not a variable, } (c)rl \ l\Rightarrow r\ (if\ c) \text { is a fresh variant of a} \\ \text {(conditional)} \text {rule in } R, \, \rho =\lbrace X_{[S]}\mapsto r\rbrace ,\,\theta \in CSU_A (s=l).\end{array} $$

• $[T]$ transitivity

  $$\begin{aligned} \frac{s{:}S \Rightarrow t{:}T,G'}{s{:}S\rightarrow X'_S{:}S,X'_S{:}S\Rightarrow ^1 X''_{[S]}{:}[S],X''_{[S]}{:}[S]\Rightarrow t{:}T,G'} \end{aligned}$$
  $$\begin{aligned} \text {where } X'_S \text { and } X''_{[S]} \text { are fresh variables.} \end{aligned}$$

• $[I]$ imitation

  $$\begin{aligned} \frac{f(\bar{s}{:}\bar{S}){:}S \Rightarrow ^1 X_{[S]}{:}[S],G'}{s_i{:}S_i\Rightarrow ^1 X'_{S_i}{:}S_i,f(\bar{s}{:}\bar{S}){:}S,G'\theta } \end{aligned}$$

$$\begin{aligned} \begin{array}{c}\text {where } X_{[S]} {\notin } Var (s),\theta =\lbrace X_{[S]}\mapsto f((s_1,{\ldots },X'_{S_i}{:}S_i,{\ldots },s_n))\rbrace , \,X'_{S_i} \text { fresh variable.}\end{array} \end{aligned}$$

From a reachability goal $r$ a derivation is made applying rules of the calculus. Each application of the reflexivity rule generates a unification equation. These unification equations as well as any generated membership goals must be solved using the calculus rules for unification. If the derivation ends with an empty goal, written $\square$, then the composition of the substitutions used on each derivation step, restricted to those variables appearing in $r$, is a computed answer for $r$.

Theorem 2

The calculus for reachability is sound and weakly complete.

That is, given a reachability goal $G$, if $G\rightsquigarrow ^*_\sigma \square$ then $G\sigma$ can be derived, so $\sigma$ is a solution for $G$ in $\rightarrow _{R/\mathcal {E}}$, and if $\theta$ is an $R/\mathcal {E}$-normalized idempotent answer for a reachability problem $G$ in $\rightarrow _{R/\mathcal {E}}$, then there is $\sigma$ idempotent, with $\theta \ll _\mathcal {E}\sigma$, such that $G\rightsquigarrow ^*_{\sigma }\square$.

Proof

We prove correctness of the calculus for reachability with respect to $R/\mathcal {E}$-normalized (equivalently $R\cup E,A$) idempotent substitutions for the executable rewrite theory $\mathcal {R}=(\varSigma ,\mathcal {E},R)$ in $\rightarrow _{R/\mathcal {E}}$.

• 1. Soundness: By structural induction on the calculus rule for reachability applied.

• 2. Completeness: We prove that for $R/\mathcal {E}$-normalized idempotent answers $\Rightarrow ^1$ solves $\rightarrow ^1_{R,A}$ reachability problems and $\Rightarrow$ solves $\rightarrow ^*_{R/\mathcal {E}}$ reachability problems, according to [MT07, Theorem 3] and Lemma 1. Then it follows that if $\theta$ is an $R/\mathcal {E}$-normalized idempotent answer for a reachability problem $G$ in $\rightarrow _{R/\mathcal {E}}$, then there is $\sigma$ idempotent, with $\theta \ll _\mathcal {E}\sigma$, such that $G\rightsquigarrow ^*_{\sigma }\square$. Inferred sorts are treated as in the proof of completeness of the calculus for unification (see extended version). We don’t show the inferred sorts here.

  • (a) We prove that if $s\rho \rightarrow ^1_{R,A}t$ then $s\Rightarrow ^1 t'\rightsquigarrow ^*_\sigma \square$, with $\rho {\ll _{\mathcal {E}}}\sigma$ and $t{\ll _{\mathcal {E}}}t'$. By definition there is a position $p$ in $s\rho$, a rule $l{\rightarrow }r \ if\ c \in R$ and a matching $\theta$ such that $s\rho |_p{=}l\theta$, $c\theta$ can be derived and $t\equiv (s\rho )[r\theta ]_p$. By the same reasoning we used for the completeness of the calculus for unification, $p$ must be a nonvariable position in $s$. Otherwise $\rho$ would not be $R/\mathcal {E}$-normalized. From $s\Rightarrow ^1 X$, by imitation we can reach position $p$, turning our reachability problem into $s|_p\Rightarrow ^1 X^p$ with $\eta {=}\lbrace X\mapsto s[X^p]_p\rbrace$. Applying replacement, as $s\rho |_p{=}l\theta$, there is $\sigma (\equiv \rho '\cup \theta ')\in CSU_A (s\rho |_p{=}l)$, with $\rho \ll _{\mathcal {E}}\rho '$, $\theta \ll _{\mathcal {E}}\theta '$ and $t'\equiv X\eta \sigma \equiv (s\rho ')[r\theta ']_p$.

    It is important to remember, again, that ACU-coherence completion allows $A$-unification of the left term of the ACU-coherence completed version of the rule, $l$, with the whole $s\rho |_p$ whenever the original left term $l$ can be $A$-unified with some subterm of a recombination of $s\rho |_p$.

  • (b) We prove that if $s\rho \rightarrow ^*_{R/\mathcal {E}}t\rho$, $\rho$ is a solution, then $s\Rightarrow t\rightsquigarrow ^*_\sigma \square$, with $\rho \ll _{\mathcal {E}}\sigma$. We distinguish two cases:

    • Reflexive case: $s\rho =_{\mathcal {E}}t\rho$. Then $s{\Rightarrow }t\rightsquigarrow _{[X]}s{=}t\rightsquigarrow ^*_\sigma \square$, with $\rho \ll _{\mathcal {E}}\sigma$ by correctness of the calculus for unification.

    • Rest of the cases: According to [MT07, Lemmas 7 and 8] and the Lemma in Sect. 2.4 it suffices to show that $(\rightsquigarrow ^*_{E,A}\rightsquigarrow _{R,A})^+=_\mathcal {E}$ is implemented by $\Rightarrow$. This is done in the transitivity rule

      $$\begin{aligned} \frac{s{:}S \Rightarrow t{:}T,G'}{s{:}S\rightarrow X'_S{:}S,X'_S{:}S\Rightarrow ^1 X''_{[S]}{:}[S],X''_{[S]}{:}[S]\Rightarrow t{:}T,G'} \end{aligned}$$

      $s{:}S\rightarrow X'_S$ implements $\rightsquigarrow ^*_{E,A}$ as proved in the calculus for unification. $X'_S{:}S\Rightarrow ^1 X''_{[S]}{:}[S]$ implements $\rightsquigarrow _{R,A}$ as proved in the previous point. $X''_{[S]}{:}[S]\Rightarrow t{:}T$ allows iteration (the $^+$ part) through several uses of the transitivity rule ending with the $=_\mathcal {E}$ part through the use of the reflexivity rule, which is the only rule that enables us to exit the loop generated by the transitivity rule.

      Finally, correct typing is ensured because $s{:}S$ and $t{:}T$ are included as conditions.

5 Example

As an example of our calculus we use the specification of the Tower of Hanoi puzzle in Sect. 2 and the reachability problem

$$\begin{aligned} (3T^0_T,b,c){:}S\Rightarrow (a,b,T^1_T){:}S \end{aligned}$$

where from a State composed of one Tower with Disk $3$ on top of it and two Towers with Rods $b$ and $c$ alone respectively we want to reach a State composed of two Towers with Rods $a$ and $b$ alone respectively and another Tower. The subindex of each variable means its type (sort or kind) and we write $D, R, V, T, P, S$ instead of Disk, Rod, ValidT, Tower, Pair, State for readability.:

• 1. $\underline{(3T^0_T,b,c){:}S\Rightarrow (a,b,T^1_T){:}S}\rightsquigarrow _{[T]}$

  Transitivity decomposes reachability into several rewriting narrowing steps.

• 2. $\underline{(3T^0_T,b,c){:}S\rightarrow X^1_S{:}S}, X^1_S{:}S\Rightarrow ^1 X^2_{[S]}{:}[S], X^2_{[S]}{:}[S]\Rightarrow (a,b,T^1_T){:}S$

  $\rightsquigarrow _{[r],\lbrace T^0_T\mapsto a, X^1_S\mapsto (3a,b,c)\rbrace }$ $T^0_T$ is instantiated through rule $[r]$.

• 3. $\underline{(3a,b,c){:}S}, (3a,b,c){:}S\Rightarrow ^1 X^2_{[S]}{:}[S], X^2_{[S]}{:}[S]\Rightarrow (a,b,T^1_T){:}S$

  We focus on the first subgoal.

• 4. $\underline{(3a,b,c){:}S}\rightsquigarrow _{[m2], S^1_{[S]},S^2_{[S]}: S \ if\ S^1_{[S]}{:}S\bigwedge S^2_{[S]}{:}S, \lbrace S^1_{[S]}\mapsto (3a,b),S^2_{[S]}\mapsto c\rbrace }$

• 5. $\underline{c{:}S},(3a,b){:}S\rightsquigarrow \ldots$

• 6. $\underline{3a{:}S}\rightsquigarrow _{[m2], X_{[D]}R_{[R]}: V \ if\ X_{[D]}{:}D\bigwedge R_{[R]}{:}R,\lbrace X_{[D]}\mapsto 3,R_{[R]}\mapsto a\rbrace }$. OK because $V\le S$.

• 7. $\underline{3{:}D,a{:}R}$ $\rightsquigarrow \ldots$ similar to previous steps. First subgoal finished.

• 8. $\underline{(3a,b,c){:}S\Rightarrow ^1 X^2_{[S]}{:}[S]}, X^2_{[S]}{:}[S]\Rightarrow (a,b,T^1_T){:}S$. We focus on the first subgoal.

• 9. $\underline{(3a,b,c){:}S\Rightarrow ^1 X^2_{[S]}{:}[S]}\rightsquigarrow _{[R],D_{[T]},E_{[T]},X_{[S]}\rightarrow F_{[T]},G_{[T]},X_{[S]}\ if }$

  $_{D_{[T]}{:}T\wedge E_{[T]}{:}T\wedge X_{[S]}{:}S\wedge F_{[T]}{:}T\wedge G_{[T]}{:}T\wedge F_{[T]}-G_{[T]}:=\textit{move}(D_{[T]}-E_{[T]}),}$

  $_{\theta =\lbrace D_{[T]}\mapsto 3a,E_{[T]}\mapsto c,X_{[S]}\mapsto b\rbrace ,\rho =\lbrace X^2_{[S]}{:}[S]\mapsto F_{[T]},G_{[T]},X_{[S]}\rbrace }$ Narrowing step.

• 10. $\underline{(3a,b,c){:}S,3a{:}T, c{:}T,b{:}S}, (F_{[T]}-G_{[T]}){:}[P]:=\textit{move}(3a-c){:}[P]$ $\rightsquigarrow \ldots$

• 11. $\underline{F_{[T]}-G_{[T]}{:}[P]:=\textit{move}(3a-c){:}[P]}\rightsquigarrow _{[x]}$

• 12. $\underline{\textit{move}(3a-c)}{:}[P]\rightarrow F_{[T]}-G_{[T]}{:}[P]\rightsquigarrow _{[t]}$

  Transitivity decomposes unification into several unification narrowing steps.

• 13. $\underline{\textit{move}(3a-c)}{:}[P]\rightarrow ^1 Y_{[P]}{:}[P],Y_{[P]}{:}[P]\rightarrow F_{[T]}-G_{[T]}{:}[P]\rightsquigarrow _{[n],}$

  $_{ move (X_{[D]}T_{[T]}-R_{[R]})=T_{[T]}-X_{[D]}R_{[R]}\, if \, X_{[D]}{:}D\bigwedge T_{[T]}{:}T\bigwedge R_{[R]}{:}R,}$

  $_{\theta =\lbrace X_{[D]}\mapsto 3,T_{[T]}\mapsto a,R_{[R]}\mapsto c\rbrace ,\rho =\lbrace Y_{[P]}\mapsto T_{[T]}-X_{[D]}R_{[R]}\rbrace }$

  Unification narrowing step. $Y_{[P]}$ is instantiated to a ground term.

• 14. $\underline{a-3c{:}[P],3{:}[D],a{:}[T],c{:}[R]},a-3c{:}[P]\rightarrow F_{[T]}-G_{[T]}{:}[P]$ $\rightsquigarrow \ldots$

• 15. $\underline{a-3c{:}[P]\rightarrow F_{[T]}-G_{[T]}{:}[P]}$ $\rightsquigarrow _{[r],\theta _1=\lbrace F_{[T]}\mapsto a,G_{[T]}\mapsto 3c\rbrace }$ Removal of equations.

• 16. $\underline{a-3c{:}[P]}\rightsquigarrow \ldots$ We omit this and go back to the second subgoal on step 8.

• 17. $\underline{(a,3c,b):[S]\Rightarrow (a,b,T^1_T){:}S}$ $\rightsquigarrow _{[X]}\ldots$

• 18. $\underline{(a,3c,b):S\rightarrow X_S{:}S},(a,b,T^1_T){:}S\rightarrow X_S{:}S$ $\rightsquigarrow _{[r],\lbrace X_S\mapsto (a,3c,b)\rbrace }$

• 19. $\underline{(a,3c,b):S},(a,b,T^1_T){:}S\rightarrow (a,3c,b){:}S$ $\rightsquigarrow \ldots$

• 20. $\underline{(a,b,T^1_T){:}S\rightarrow (a,3c,b){:}S}$ $\rightsquigarrow _{[r],\lbrace T^1_T\mapsto 3c\rbrace }$ $T^1_T$ is instantiated through rule $[r]$.

• 21. $\underline{(a,b,3c):S}$ $\rightsquigarrow \ldots \square$

From the substitutions in steps 2 and 20 the answer $\lbrace T^1_T\mapsto 3c,T^0_T\mapsto a\rbrace$ is computed. The calculus has found the solution $(3a,b,c){:}S\Rightarrow (a,b,3c){:}S$ which is an instance of the given reachability problem $(3T^0_T,b,c){:}S\Rightarrow (a,b,T^1_T){:}S$.

6 Related Work, Conclusions and Future Work

A classic reference in equational conditional narrowing modulo is the work of Bockmayr [Boc93]. The topic is addressed here for Church-Rosser equational CTRS with empty axioms, but non terminating axioms (like ACU) are not allowed. Non conditional narrowing modulo order-sorted equational logics is covered by Meseguer and Thati [MT07], the reference for recent development in this area, which is actively being used for cryptographic protocol analysis. This work is partially based on the work of Viry [Vir94] where $R/\mathcal {E}$ rewriting is defined in terms of $R,A$ and $E,A$ for unsorted rewrite theories. Another topic addressed by the present work, membership equational logic, is defined by Meseguer [Mes97]. An equivalent rewrite system for Mel theories is presented by Durán, Lucas et al. [DLM+08], allowing unification by rewriting. Strategies, which also play a main role in narrowing, have been studied by Antoy, Echahed and Hanus [AEH94]. Their needed narrowing strategy, for inductively sequential rewrite systems, generates only narrowing steps leading to a computed answer. The use of this lazy narrowing strategy has been explained by Alpuente, Lucas and Escobar [ALE99] inside the programming language Curry. Recently Escobar, Sasse, and Meseguer [ESM12] have developed the concepts of variant and folding variant, a narrowing strategy for order-sorted unconditional rewrite theories that terminates on those theories having the finite variant property. As an extension to rewrite theories Bruni and Meseguer [BM06] have defined generalized rewrite theories that support context-sensitive rewriting, thus allowing rewrites only on certain positions of terms.

In this work we have developed a narrowing calculus for unification in membership equational logic and a narrowing calculus for reachability in rewrite theories with an underlying membership equational logic. The main features in these calculi are that they make use of membership information whenever possible, reducing the state space, and also that they only allow steps leading to a different state, no mutual cancelling steps are allowed. The calculi have been proved correct. This work is part of a bigger effort where we attempt to explore the possibilities of performing conditional narrowing with constraint solvers. A transformation for rules and goals that will make both calculi strongly complete is under study. Strong completeness of reachability for topmost rewrite theories, Russian dolls configurations and linear theories are also under study. Finally, decidability of the calculus for unification in the case of operationally terminating Mel theories with a finitary and complete $A$-unification algorithm [LM09], using the required strategy for deterministic 3-CTRS’s of solving subgoals from left to right, is being studied.

Our current line of investigation also intends to study the extension of the calculi to handle constraints and their connection with external constraint solvers for domains such as finite domains, integers, Boolean values, etc., that could greatly improve the performance of any implementation. We also plan on the extension of the calculi, adding support for generalized rewrite theories. Better strategies that may help reducing the state space will also be studied. All the improvements will have new sets of transformation rules that will allow their implementation on Maude.