Unification and combination of iterative insertion strategies with rudimentary traversals and failure

TL;DR

This paper presents a new, general framework for combining navigation strategies and context insertions in term extensions, with properties like associativity and idempotency, aimed at aiding multiscale PDE modeling.

Contribution

It introduces a novel, algebraic combination operation for term extensions that is associative, neutral, and idempotent, independent of specific application semantics.

Findings

The combination operation is associative and admits a neutral element.

The class of extensions is closed under the combination operation.

The framework is applicable to multiscale PDE model derivation.

Abstract

We introduce a new class of extensions of terms that consists in navigation strategies and insertion of contexts. We introduce an operation of combination on this class which is associative, admits a neutral element and so that each extension is idempotent. The class of extension is also shown to be closed by combination, with a constructive proof. This new framework is general and independent of any application semantics. However it has been introduced for the kernel of a software tool which aims at aiding derivation of multiscale partial differential equation models.

Equations

$$[[\varnothing ]](t)$$

$$[[E]](\mathbb{F})$$

$$[[@p.\mathbf{\tau }]](t)$$

$$[[[@p_1.{\mathbf{\tau }}_1,\dots ,@p_n.{\mathbf{\tau }}_n]]](t)$$

$$\mathtt{eval}({\mathbf{\tau }}_1\cdot \dots \cdot {\mathbf{\tau }}_i\cdot {\mathbf{\tau }}_{i+1}\cdot \dots$$

$$\mathtt{eval}({\mathbf{\tau }}_1\cdot \dots \cdot {\mathbf{\tau }}_i\cdot {\mathbf{\tau }}_{i+2}\cdot \dots \cdot {\mathbf{\tau }}_n),$$

$$\mathtt{eval}\left(\left({\tau }_1,\dots ,{\tau }_m\right)\right)=\{\begin{array}{ll}{\tau }_1,& \text{ if }n=1\\ {\tau }_1[\mathtt{eval}\left(\left({\tau }_2,\dots ,{\tau }_m\right)\right)],& \text{ if }n\ge 2.\end{array}$$

$$E⋏E^{\prime }=\{\begin{array}{ll}{E}^{\prime \prime }& \text{ if }E\ne \varnothing \text{ and }{E}^{\prime }\ne \varnothing \\ \varnothing & \text{ if }E=\varnothing \text{ or }{E}^{\prime }=\varnothing \end{array}$$

$${\mathbf{\tau }}_k^{\prime \prime }={\mathbf{\tau }}_i\text{ if }{p}_k^{\prime \prime }=p_i\in P$$

$$E⋎E^{\prime }=\{\begin{array}{ll}E⋏E^{\prime }& \text{ if }E\ne \varnothing \text{ and }{E}^{\prime }\ne \varnothing \\ E& \text{ if }E\ne \varnothing \text{ and }{E}^{\prime }=\varnothing \\ E^{\prime }& \text{ if }E=\varnothing \text{ and }{E}^{\prime }\ne \varnothing \\ \varnothing & \text{ if }E=\varnothing \text{ and }{E}^{\prime }=\varnothing \end{array}$$

$$\mathcal{B}::=\mathtt{True}|\mathtt{False}|\hat{p}|\mathcal{B}\wedge \mathcal{B}|\mathcal{B}\vee \mathcal{B}$$

$$\mathcal{S}::=$$

$$\text{displaystyle@p}.\mathcal{S}|@p.\mathbf{\tau }|⟨[@p_1.{\mathcal{S}}_1\dots ,@p_n.{\mathcal{S}}_n]|\varphi ⟩$$

$$(\eta (f))(t)=\{\begin{array}{ll}f(t)& \text{ if }f(t)\ne \mathbb{F}\\ t& \text{ otherwise}.\end{array}\text{vspace}-0.4cm$$

$$[[\varnothing ]](t)$$

$$[[(u,s^{\prime })]](t)$$

$$[[@p.\mathbf{\tau }]](t)$$

$$[[S_1\oplus S_2]](t)$$

$$[[\mu X.S(X)]](t)$$

$$[[@p.S]](t)$$

$$[[⟨\underset{i=1,n}{⨆}@p_i.S_i|\varphi ⟩]](t)\stackrel{def}{=}$$

$$\displaystyle\;\;\begin{cases}\big{(}\eta([\![@p_{n}.S_{n}]\!])\circ\cdots\circ\eta([\![@p_{1}.S_{1}]\!])\big{)}(t)&\textrm{if }\mathcal{V}_{\mathfrak{f}}({S},{t})\models\phi,\\ \mathbb{F}&\textrm{otherwise},\end{cases}$$

$$\text{ where }S=[@p_1.S_1,\cdots ,@p_n.S_n],\text{ and }$$

$$\mathcal{V}(S,t)({\hat{p}}_i)=\mathtt{False}\text{ iff }[[@p_i.S_i]](t)=\mathbb{F}$$

$$\mathtt{OneLeft}(S)=$$

$$\displaystyle\mu X.\big{(}S\oplus\bigoplus_{\begin{subarray}{c}f\in\mathcal{F},\\ ar(f)=n\end{subarray}}\big{(}f(x_{1},\cdots,x_{n}),\bigoplus_{i=1,n}\big{\langle}{[@i.X]}\,|\,{\bigvee_{i=1,n}\widehat{i}\,}\big{\rangle}\big{)}\big{)},$$

$$\displaystyle\mathtt{TopDown}(S)=\mu X.\big{(}$$

$$\displaystyle S\oplus\bigoplus_{\begin{subarray}{c}f\in\mathcal{F},\\ ar(f)=n\end{subarray}}\big{(}f(x_{1},\cdots,x_{n}),\big{\langle}{[@1.X,\cdots,@i.X]}\,|\,{\bigvee_{i=1,n}\widehat{i}\,}\big{\rangle}\big{)}\big{)}.$$

$$\Psi (\varnothing ,t)$$

$$\Psi (@p.\mathbf{\tau },t)$$

$$\Psi ((u,\mathbf{\tau }),t)$$

$$\Psi ((u,S),t)$$

$$\Psi (⟨\underset{i\in [n]}{⨆}@p_i.{\mathbf{\tau }}_i|\varphi ⟩,t)$$

$$\Psi (@p.S,t)$$

$$\Psi (S\oplus S^{\prime },t)$$

$$\Psi (\mu X.S(X),t)$$

$$\displaystyle\Psi\big{(}\big{\langle}{S}\,|\,{\phi}\big{\rangle},t\big{)}$$

$$\varnothing ⋏S$$

$$S⋏\varnothing$$

$$\text{displaystyle@i}.\mathbf{\tau }\text{curlywedge@i}.{\mathbf{\tau }}^{\prime }$$

$$\text{displaystyle@i}.\mathbf{\tau }\text{curlywedge@j}.{\mathbf{\tau }}^{\prime }$$

$$\text{displaystyle@i}.\mathbf{\tau }\text{curlywedge@i}.S$$

$$\text{displaystyle@i}.\mathbf{\tau }\text{curlywedge@j}.S$$

$$(u,\mathbf{\tau })\text{curlywedge@i}.{\mathbf{\tau }}^{\prime }$$

Full text

Keywords. Rewriting strategies, adding contexts, unification, combination, fixed-point.

I Introduction

This article presents a new computation framework based on reusability for the development of complex models described by trees. This method is based on two operations. The operation of extension transforms a reference model in a more complex model by adding or embedding sub-trees, and the combination assembles several extensions to produce one that has all the characteristics of those used for its generation. At this stage, the process is purely operative and does not include any aspect of model semantics. The concepts of combination of two extensions is well illustrated with the term $\partial_{x}v(x)$ that plays the role of the reference model, with an extension that adds an index $j$ on the variable $x$ of derivation, and with an extension that adds an index $i$ on the derivated function $v$. Applying these two extensions to the reference term yields the terms $\partial_{x}v_{i}(x)$ and $\partial_{x_{j}}v(x)$. The combination of these two extensions applied to the reference term might yield $\partial_{x_{j}}v_{i}(x)$.

The concept of extension, also called refinement, is developed in different contexts, for example in [GR01] the refinement is done by replacement of components with more complex components. Combination principles are present in different areas of application, they involve different techniques but follow the same key idea. For instance, the works in combination of logics [GS03, Ben13], algorithms, verification methods [BK15], and decision procedures [MZ02] share a common principle of incremental design of complex systems by integration of simple and heterogeneous subsystems.

The integration of the two concepts of extension and combination seems to have not been addressed in the literature. To make it simple to operate and effective, we have adopted the simplest possible principles. Reformulating the above description in terms of trees, an extension applied to a reference tree is an operation of context insertion at different positions. We call it a position based strategy for Context Embedding or shortly a position-based CE-strategy. A combination of several extensions therefore consists of all of their contexts and insertion positions. Obviously if two contexts have to be inserted at the same place they are first assembled one above the other before insertion excepted if they are identical. In the latter case, the context is inserted one time only so that the extensions are idempotent for the operation of combination. With this definition, the combination of two position-based CE-strategies is another one so that this set of extensions is closed by combination. Note that unlike these kind of extensions, extensions comprising substitutions cannot be combined. The principle of CE-strategy has been developed for a software tool that does automatic derivation of multiscale models based on partial differential equation and that uses asymptotic methods. The first target applications are in micro and nanotechnology [YBL14, BGL14, BRN*+*15].

The drawback of the principle of extensions at positions is its lack of robustness with respect to changes in the reference tree. Indeed, any of its change requires another determination of the insertion positions. To add flexibility and robustness, the strategy of insertion at some positions is completed by strategies of navigation in trees using pattern matching. This leads to the broader concept of extensions called strategy for Context Embedding or CE-strategy for shortness. These class of extensions can be expressed with a language of high-level strategies [CKLW03, Ter03]. To perform the combination of two CE-strategies in view of its application to a particular reference tree, we starts by detecting the positions of the context insertion of the CE-strategies when they are applied to the tree. This allows to build the equivalent CE-strategies based on positions and then to achieve the combination without further difficulty.

It is natural to ask whether the step of replacement of strategies by positions can be avoided, i.e. if it is possible to determine formulas of combination for CE-strategies that are expressed as high-level strategies. Of course, the combination formulas should be theoretically validated by comparison to the principle of combination based on positions. Thus, combinations formulas may be set as definitions, but their correctness has be proved. To this end, a preliminary step is to establish calculation formulas of positions associated with any CE-strategies applied to any reference tree.

In our work, we found that the combination of extensions based on high-level strategies such as BottomUp or TopDown can not be expressed with high-level strategies. We thus understood that more rudimentary** **strategies are needed, especially operators of jumping and iteration with fixed point issued from mu-calculus [AN01]. From this standpoint, we asked the question of finding a class of CE-strategies which is closed by the operation of combination. Moreover, we consider as highly desirable that a number of nice algebraic properties as associativity of the combination of CE-strategies based on positions or their idempotence are still true for all CE-strategies.

All these theoretical questions have been addressed with success, and the results are presented in this article. An application is implemented in the context of our work on the generation of multiscale models but with an intermediate-level and yet a closed fragment of CE-strategies. A user language allows the expression of an input reference partial differential equation (PDE) and of a reference proof that transforms this PDE into another one. The reference proof corresponds to what is called the reference model in the paper. The user language allows also the statement of CE-strategies and combinations. An OCaml program generates the reference tree and allows to apply the extensions. The combinations of extensions are then computed and applied to the reference model. Transforming CE-strategies into position-based CE-strategies is used to test the validity of the program. Nevertheless, the implementation aspects are not presented here for the obvious reason of lack of space.

The paper is organized as follows. After a review in Section II of the useful concepts of rewriting theory, the position-based CE-strategies and their combination are introduced in Section III. The broad class of CE-strategies is introduced in Section IV. The formulas for calculation of positions of a CE-strategies and a given reference tree are also set forth. Finally the combination formulas and the important algebraic properties of combination are in Section V. The proofs are given in the appendix.

II Preliminaries

We introduce preliminary definitions and notations, introduced for instance in the reference book [Ter03].

Terms, contexts. Let ${\mathcal{F}}=\cup_{n\geq 0}{\mathcal{F}}_{n}$ be a set of symbols called function symbols. The arity of a symbol $f$ in ${\mathcal{F}}_{n}$ is $n$ and is denoted $\mathit{ar}(f)$. Elements of arity zero are called constants and often denoted by the letters $a,b,c,$ etc. The set ${\mathcal{F}}_{0}$ of constants is always assumed to be not empty. Given a denumerable set ${\mathcal{X}}$ of variable symbols, the set of terms $\mathcal{T}\left(\mathcal{F},\mathcal{X}\right)$, is the smallest set containing ${\mathcal{X}}$ and such that $f(t_{1},\ldots,t_{n})$ is in $\mathcal{T}\left(\mathcal{F},\mathcal{X}\right)$ whenever $ar(f)=n$ and $t_{i}\in\mathcal{T}\left(\mathcal{F},\mathcal{X}\right)$ for $i\in[1..n]$. Let the constant $\square\not\in{\mathcal{F}}$, the set $\mathcal{T}_{\square}(\mathcal{F},\mathcal{X})$ of ”contexts”, denoted simply by $\mathcal{T}_{\square}$, is made with terms with symbols in $\mathcal{F}\cup\mathcal{X}\cup\{\square\}$ which includes exactly one occurence of $\square$. Evidently, $\mathcal{T}_{\square}(\mathcal{F},\mathcal{X})$ and $\mathcal{T}(\mathcal{F},\mathcal{X})$ are two disjoint sets. We shall write simply $\mathcal{T}$ (resp. $\mathcal{T}_{\square}$) instead of $\mathcal{T}\left(\mathcal{F},\mathcal{X}\right)$ (resp. $\mathcal{T}_{\square}(\mathcal{F},\mathcal{X})$). We denote by $\mathcal{V}ar\left({t}\right)$ the set of variables occurring in $t$.

Positions, prefix-order. Let $t$ be a term in $\mathcal{T}\left(\mathcal{F},\mathcal{X}\right)$. A position in a tree is a finite sequence of integers in $\mathbb{N}^{\star}_{\epsilon}=\{{\epsilon}\}\cup\mathbb{N}\cup(\mathbb{N}\times\mathbb{N})\cup\cdots$. In particular we shall write $\mathbb{N}_{\epsilon}$ for $\{{\epsilon}\}\cup\mathbb{N}$. Given two positions $p=p_{1}p_{2}\ldots p_{n}$ and $q=q_{1}q_{2}\ldots q_{m}$, the concatenation of $p$ and $q$, denoted by $p\cdot q$ or simply $pq$, is the position $p_{1}p_{2}\ldots p_{n}q_{1}q_{2}\ldots q_{m}$. The set of positions of the term $t$, denoted by $\mathcal{P}os\left(t\right)$, is a set of positions of positive integers such that, if $t\in\mathcal{X}$ is a variable or $t\in\mathcal{F}_{0}$ is a constant, then $\mathcal{P}os\left(t\right)=\left\{\epsilon\right\}$. If $t=f\left(t_{1},...,t_{n}\right)$ then $\mathcal{P}os\left(t\right)=\left\{\epsilon\right\}\cup\bigcup_{i=1,n}\left\{ip\mid p\in\mathcal{P}os\left(t_{i}\right)\right\}$. The position $\epsilon$ is called the root position of term $t,$ and the function or variable symbol at this position is called root symbol of $t$.

The prefix order defined as $p\leq q$ iff there exists $p^{\prime}$ such that $pp^{\prime}=q$, is a partial order on positions. If $p^{\prime}\neq\epsilon$ then we obtain the strict order $p<q$. We write $\left(p\parallel q\right)$ iff $p$ and $q$ are incomparable with respect to $\leq$. The binary relations $\sqsubset$ and $\sqsubseteq$ defined by p\sqsubset q\quad\text{ iff }\quad\big{(}p<q\text{ or }p\parallel q\big{)} and p\sqsubseteq q\quad\text{ iff }\quad\big{(}p\leq q\text{ or }p\parallel q\big{)}, are total relations on positions. For any $p\in\mathcal{P}os(t)$ we denote by $t_{|p}$ the subterm of $t$ at position $p$, that is, $t_{|{\epsilon}}=t$, and $f(t_{1},...,t_{n})_{|iq}=(t_{i})_{|q}$. For a term $t$, we shall denote by $\delta(t)$ the depth of $t$, defined by $\delta(t_{0})=0$, if $t_{0}\in\mathcal{X}\cup\mathcal{F}^{0}$ is a variable or a constant, and $\delta(f(t_{1},\ldots,t_{n}))=1+max(\delta(t_{i}))$, for $i=1,\ldots,n$. For any position $p\in\mathcal{P}os\left(t\right)$ we denote by $t\left[s\right]_{p}$ the term obtained by replacing the subterm of $t$ at position $p$ by $s$: $t[s]_{\epsilon}=s$ and $f(t_{1},...,t_{n})[s]_{iq}=f(t_{1},...,t_{i}[s]_{q},...,t_{n})$.

Substitutions, terms matching and unification. A substitution is a mapping $\sigma:\mathcal{X}\rightarrow\mathcal{T}(\mathcal{F},\mathcal{X})$ such that $\sigma(x)\neq x$ for only finitely many $x$s. The finite set of variables that $\sigma$ does not map to themselves is called the domain of $\sigma$: ${\mathsf{Dom}}(\sigma)\overset{def}{=}\left\{x\in\mathcal{X}\;\;|\;\;\sigma(x)\neq x\right\}$. If ${\mathsf{Dom}}(\sigma)=\left\{x_{1},...,x_{n}\right\}$ then we write $\sigma$ as: $\sigma=\left\{x_{1}\mapsto\sigma\left(x_{1}\right),...,x_{n}\mapsto\sigma\left(x_{n}\right)\right\}$. A substitution $\sigma:\mathcal{X}\rightarrow{\mathcal{T}(\mathcal{F},\mathcal{X})}$ uniquely extends to an endomorphism $\widehat{\sigma}:\mathcal{T}(\mathcal{F},\mathcal{X})\rightarrow\mathcal{T}(\mathcal{F},\mathcal{X})$ defined by: $\widehat{\sigma}(x)=\sigma(x)$ for all $x\in{\mathsf{Dom}}(\sigma)$, and $\widehat{\sigma}(x)=x$ for all $x\not\in{\mathsf{Dom}}(\sigma)$, and $\widehat{\sigma}(f(t_{1},\ldots,t_{n}))=f(\widehat{\sigma}(t_{1}),\ldots,\widehat{\sigma}(t_{n}))$ for $f\in\mathcal{F}$. In what follows we do not distinguish between a substitution and its extension.

For two terms $t,t^{\prime}\in\mathcal{T}$, we say that $t$ matches $t^{\prime}$, written $t\ll t^{\prime}$, iff there exists a substitution $\sigma$, such that $\sigma(t)=t^{\prime}$. It turns out that if such a substitution exists, then it is unique. The most general unifier of the two terms $u$ and $u^{\prime}$ is a substitution $\gamma$ such that $\gamma(u)=\gamma(u^{\prime})$ and, for any other substitution $\gamma^{\prime}$ satisfying $\gamma^{\prime}(u)=\gamma^{\prime}(u^{\prime})$, we have that $\gamma^{\prime}$ is subsumed by $\gamma$. Besides, we shall write $u\wedge u^{\prime}$ to denote the term $\gamma(u)$. The composition of functions will be denoted by “$\circ$”. For a set $A$, the set of all functions from $A$ to $A$ will be denoted by $\mathfrak{F}(A)$. If $l_{1}$ and $l_{2}$ are lists, then we denote by $l_{1}\sqcup l_{2}$ (resp. $l_{1}\sqcap l_{2}$) their concatenation (resp. intersection). Sometimes we shall write $\sqcup_{i=1,n}e_{i}$ to denote the list $[e_{1},\ldots,e_{n}]$. For any $n\in\mathbb{N}$ we simply denote by $[n]$ the interval $[1,\ldots,n]$.

III Position-Based CE-strategies and their combination

In this section we introduce position-based CE-strategies. The definition of combination of position-based CE-strategies is given by means of their unification. Finally, the algebraic properties of the unification and combination are stated in Proposition 7, namely the associativity and the idempotence which are important in the applications. We first explain the ideas through an example.

III.1 Example of combination of two position-based CE-strategies

We illustrate the idea and the interest of position-based CE-strategies through the simple example, presented in [BRN*+*15], of an extension of a mathematical expression encountered in an extension of a proof. The context $\tau=\mathtt{list}(\square,j)$ depicted in Figure 1 captures the idea that the extension transforms a one-dimensional space coordinate variable $x$ to an indexed multi-dimensional space coordinate variable $x_{j}$. Similarly, the context $\tau^{\prime}=\mathtt{list}(\square,i)$ depicted in Figure 1 captures the idea that the extension transforms a function $v(x)$ to $v_{i}(x)$.

Figure 2 shows the combination of these two position-based CE-strategies and their application to the term $t=\partial_{x}v(x)$. We mean by combination of two CE-strategies, a CE-strategy that behaves as if we have merged these two CE-strategies. The combination is clearly different from the sequential composition.

III.2 Position-Based CE-strategies and their semantics

We formally define the class of position-based CE-strategies and their semantics. The semantics of a CE-strategy is a function on terms and takes into account the failure of the application position-based CE-strategy.

Definition 1** (Position-Based CE-strategies)**

An position-based CE-strategy is either the failing strategy $\varnothing$ or the list $[@p_{1}.\boldsymbol{\tau}_{1},\ldots,@p_{n}.\boldsymbol{\tau}_{n}]$, where $n\geq 1$, each $p_{i}$ is a positions and each $\boldsymbol{\tau}_{i}$ is a tuple of contexts in $\mathcal{T}_{{}_{\square}}^{\star}$.

We impose constraints on the positions of insertions to avoid conflicts: the order of context insertions goes from the leaves to the root.

Definition 2** (Well-founded position-based CE-strategy)**

An position-based CE-strategy $E=[@p_{1}.\boldsymbol{\tau}_{1},...,@p_{n}.\boldsymbol{\tau}_{n}]$ is well-founded iff

1. i.)

a position occurs at most one time in $E$, i.e. $p_{i}\neq p_{j}$ for all $i\neq j$, and 2. ii.)

insertions at lower positions occur earlier in $E$, i.e. $i<j$ iff $p_{i}\sqsubset p_{j}$, for all $i,j\in[n]$.

In particular, the empty position-based CE-strategy $\varnothing$ is well-founded.

In all what follows we work only with the set of well-founded position-based CE-strategies, denoted by $\mathcal{E}$. For two position-based CE-strategies $E^{\prime}$ and $E^{\prime}$, we shall write $E=E^{\prime}$ to mean that they are equal up to a permutation of their parallel positions. For a position $p$, we let $p.[@p_{1}.\boldsymbol{\tau}_{1},\ldots,@p_{n}.\boldsymbol{\tau}_{n}]=[@pp_{1}.\boldsymbol{\tau}_{1},\ldots,@pp_{n}.\boldsymbol{\tau}_{n}]$. We next define the semantics of position-based CE-strategies as a function in $\mathfrak{F}(\mathcal{T}\cup\{{\mathbb{F}}\})$, with the idea that if the application of an position-based CE-strategy to a term fails, the result is $\mathbb{F}$.

Definition 3** (Semantics of position-based CE-strategies)**

*The semantics of an position-based CE-strategy $E$ is a function $[\![E]\!]$ in $\mathfrak{F}(\mathcal{T}\cup\{{\mathbb{F}}\})$ inductively defined by: *

[TABLE]

III.3 Unification and combination of position-based CE-strategies

To ensure the idempotence of the combination of position-based CE-strategies, we need to pay attention to the combination of contexts when they are inserted at the same position. More precisely, while combining contexts, which are assumed to be inserted at the same position, we form a tuple of such contexts. This tuple will be evaluated during the application of an position-based CE-strategy to a term.

Definition 4** (Combination and evaluation of contexts)**

For any $\tau,\tau^{\prime}\in\mathcal{T}_{\square}$, we define the combination of two contexts by ${\tau}[{\tau}^{\prime}]=\tau[\tau^{\prime}]_{\mathcal{P}os\left(\tau,\square\right)}$, where ${\mathcal{P}os\left(\tau,\square\right)}$ is the position of $\square$ in $\tau$. For any two finite tuples of contexts $\boldsymbol{\tau}=(\tau_{1},\ldots,\tau_{n})$ and $\boldsymbol{\tau^{\prime}}=(\tau_{1}^{\prime},\ldots,\tau_{m}^{\prime})$ in $\mathcal{T}_{\square}^{\star}=\mathcal{T}_{\square}\cup(\mathcal{T}_{\square}\times\mathcal{T}_{\square})\cup\cdots$, we define the concatenation operation ”$\cdot$” by $\boldsymbol{\tau}\cdot\boldsymbol{\tau^{\prime}}=(\tau_{1},\ldots,\tau_{n},\tau_{1}^{\prime},\ldots,\tau_{m}^{\prime})$. The evaluation of a tuple of contexts $\boldsymbol{\tau}=\boldsymbol{\tau}_{1}\cdot\ldots\cdot\boldsymbol{\tau}_{n}$, denoted as $\mathtt{eval}(\boldsymbol{\tau})$, is inductively defined by:

1. i.)

if $\boldsymbol{\tau}_{i}=\boldsymbol{\tau}_{i+1}$, for some $i\in[1,\ldots,n]$, then

[TABLE] 2. ii.)

otherwise,

[TABLE]

The unification of two position-based CE-strategies amounts to sort and merge their positions, and to combine their contexts if they are inserted at the same position.

Definition 5** (Unification of two position-based CE-strategies)**

The unification of two position-based CE-strategies is the binary operation $\curlywedge:\mathcal{E}\times\mathcal{E}\longrightarrow\mathcal{E}$ defined as

[TABLE]

where the first case $E=[@p_{1}.\boldsymbol{\tau}_{1},\ldots,@p_{n}.\boldsymbol{\tau}_{n}]$, $E^{\prime}=[@p_{1}^{\prime}.\boldsymbol{\tau}_{1}^{\prime},\ldots,@p_{m}^{\prime}.\boldsymbol{\tau}_{m}^{\prime}]$ and $E^{\prime\prime}=[@p_{1}^{\prime\prime}.\boldsymbol{\tau}_{1}^{\prime\prime},\ldots,@p_{r}^{\prime\prime}.\boldsymbol{\tau}_{r}^{\prime\prime}]$ with sets of positions $P$, $P^{\prime}$ and $P^{\prime\prime}=P\cup P^{\prime}$ and the contexts $\boldsymbol{\tau}_{k}^{\prime\prime}$ defined as follows. For a position $p_{k}^{\prime\prime}\in P^{\prime\prime}\setminus P\cap P^{\prime}$,

[TABLE]

Otherwise, $p_{k}^{\prime\prime}=p_{i}=p_{j}^{\prime}\in P\cap P^{\prime}$ for some $i,j$ and $\boldsymbol{\tau}_{k}^{\prime\prime}=\boldsymbol{\tau}_{j}^{\prime}\cdot\boldsymbol{\tau}_{i}$. Besides, the other of the positions in $P^{\prime\prime}$ is chosen so that $E^{\prime\prime}$ is well-founded.

The combination of two position-based CE-strategies is similar to their unification apart that we relax the constraint on the failure.

Definition 6** (Combination of two position-based CE-strategies)**

The combination of two position-based CE-strategies is a binary operation $\curlyvee:\mathcal{E}\times\mathcal{E}\longrightarrow\mathcal{E}$ defined for any $E$ and $E^{\prime}$ in $\mathcal{E}$ by

[TABLE]

Proposition 7

The following hold.

The set $\mathcal{E}$ of position-based CE-strategies together with the unification and combination operations enjoys the following properties.

1. (a)

The neutral element of the unification and combination is $@\epsilon.\square$. 2. (b)

Every position-based CE-strategy $E$ is idempotent for the unification and combination, i.e. $E\curlywedge E=E$ and $E\curlyvee E=E$. 3. (c)

The unification and combination are associative. 2. 2.

The unification and combination of position-based CE-strategies is non commutative.

The idempotence follows from the equality $\mathtt{eval}(\boldsymbol{\tau}\cdot\boldsymbol{\tau})=\mathtt{eval}(\boldsymbol{\tau})$, the associativity follows from the equality $\mathtt{eval}((\boldsymbol{\tau_{1}}\cdot\boldsymbol{\tau}_{2})\cdot\boldsymbol{\tau}_{3})=\mathtt{eval}(\boldsymbol{\tau_{1}}\cdot(\boldsymbol{\tau}_{2}\cdot\boldsymbol{\tau}_{3}))$, and the non-commutativity is a consequence of $\mathtt{eval}(\boldsymbol{\tau}_{1}\cdot\boldsymbol{\tau}_{2})\neq\mathtt{eval}(\boldsymbol{\tau}_{2}\cdot\boldsymbol{\tau}_{1})$ in general, for any tuples of contexts $\boldsymbol{\tau},\boldsymbol{\tau}_{1},\boldsymbol{\tau}_{2}$ and $\boldsymbol{\tau}_{3}$.

IV The class of context-embedding strategies (CE-strategies)

In this section we enrich the framework of position-based CE-strategies introduced in Section III by introducing navigation strategies to form a class of CE-strategies. The $\rho$-calculus strategy constructors of [CKLW03] or the standard traversal strategies of [Ter03] yield a class of strategies which is not closed under combination. The design of the class of CE-strategies is inspired by the $\mu$-calculus formalism [AN01] since we need very rudimentary strategy constructors. In particular the jumping into the immediate positions of the term tree is morally similar to the diamond and box modalities ($\langle\cdot\rangle$ and $[\cdot]$) of the propositionsal modal $\mu$-calculus. And the fixed-point constructor is much finer than the iterate operator of e.g. [CKLW03]. Besides, we incorporate the left-choice strategy constructor and a restricted form of the composition.

IV.1 Specification of failure by Boolean formulas

The first enrichment of the position-based CE-strategies is to specify and handle the failure.

Assume that we applied the position-based CE-strategy $E=[@p_{1}.\boldsymbol{\tau}_{1},\ldots,@p_{n}.\boldsymbol{\tau}_{n}]$ to a term, and assume that one of the $@p_{i}.\boldsymbol{\tau}_{i}$ fails. In this case the whole position-based CE-strategy $E$ fails. We shall relax this strong failure specification by allowing one to explicitly specify whether the application of a strategy to a term fails depending on the failure of the application of its sub-strategies. In this subsection we propose to specify the failure by means of Boolean formulas that we next introduce. For this purpose, to each position $p$ in $\mathbb{N}^{\star}_{\epsilon}$, we associate a Boolean position-variable denoted by $\widehat{p}$. The idea is that when we apply a CE-strategy, say $@p.\boldsymbol{\tau}$, to a term, then we get $\widehat{p}:=\mathtt{True}$ if this application succeeds, and $\widehat{p}:=\mathtt{False}$ if it fails. For instance, assume that we want that the application of the position-based CE-strategy $[@p_{1}.\boldsymbol{\tau}_{1},@p_{2}.\boldsymbol{\tau}_{2}]$ succeeds if the application of $@p_{1}.\boldsymbol{\tau}_{1}$ succeeds or the application of $@p_{2}.\boldsymbol{\tau}_{2}$ succeeds. This is specified by the Boolean formula $\widehat{p}_{1}\lor\widehat{p}_{2}$.

In what follows, the set of Boolean position-variables is denoted by $\widehat{\mathbb{N}}^{\star}_{\epsilon}$.

Definition 8** (Boolean formulas over $\widehat{\mathbb{N}}^{\star}_{\epsilon}$)**

*The set of Boolean formulas over $\widehat{\mathbb{N}}^{\star}_{\epsilon}$, denoted by $\mathscr{B}ool(\widehat{\mathbb{N}}^{\star}_{\epsilon})$, is defined by the grammar: *

[TABLE]

where $\widehat{p}\in\widehat{\mathbb{N}}^{\star}_{\epsilon}$. The set of position-variables of $\phi\in\mathscr{B}ool(\widehat{\mathbb{N}}^{\star}_{\epsilon})$ will be denoted by $\mathcal{V}ar\left({\phi}\right)$. A valuation is a mapping $\nu:\widehat{\mathbb{N}}^{\star}_{\epsilon}\longrightarrow\{{\mathtt{True},\mathtt{False}}\}$. We write $\nu\models\phi$ to mean that $\nu(\phi)$ holds.

IV.2 Syntax and semantics of CE-strategies

Besides the specification of failure, the second enrichment of the position-based CE-strategies is the introduction of navigation strategies. Namely, we shall introduce the left-choice strategy constructor ($\oplus$), a restricted form of the composition (“;”), and the fixed-point constructor (“$\mu$”) allowing the recursion in the definition of strategies. In what follows we assume that there is a denumerable set of fixed-point variables denoted by $\mathcal{Z}$. Fixed-point variables in $\mathcal{Z}$ will be denoted by $X,Y,Z,\ldots$

Definition 9** (CE-strategies)**

The class of CE-strategies is defined by the following grammar:

[TABLE]

where $X$ is a fixed-point variable in $\mathcal{Z}$, and $u$ is a term in $\mathcal{T}$, and $\boldsymbol{\tau}$ is a tuple of contexts in $\mathcal{T}_{\square}^{\star}$ and $p,p_{1},\ldots,p_{n}$ are positions in ${\cal P}os$, and $\phi$ is a Boolean formula in $\mathscr{B}ool(\widehat{\mathbb{N}}^{\star}_{\epsilon})$ with $\mathcal{V}ar\left({\phi}\right)=\{{\widehat{p}_{1},\ldots,\widehat{p}_{n}}\}\setminus\{{\epsilon}\}$. The set of CE-strategies will be denoted by $\mathcal{C}$.

The strategy $@p.S$ means to jump to the position $p$ and to apply $S$ there. The strategy $\langle{[@p_{1}.S_{1}\ldots,@p_{n}.S_{n}]}\,|\,{\phi}\rangle$ consists in applying each of $@p_{i}.S_{i}$, which yields a valuation that sends the position-variable $\widehat{p}_{i}$ to $\mathtt{False}$ iff the application of $@p_{i}.S_{i}$ fails, then evaluating the Boolean formula $\phi$. If this evaluation is false then the whole strategy $\langle{[@p_{1}.S_{1}\ldots,@p_{n}.S_{n}]}\,|\,{\phi}\rangle$ fails, otherwise, every sub-strategy $@p_{i}.S_{i}$ that failed behaves like the identity, i.e. it does nothing, while the other non-failing sub-strategies $@p_{j}.S_{j}$ are applied. For example, if we apply the CE-strategy $S=\langle{[@p_{1}.S_{1},@p_{2}.S_{2}]}\,|\,{\widehat{p}_{1}\lor\widehat{p}_{2}}\rangle$ to a term $t$, and $@p_{1}.S_{1}$ fails while $@p_{2}.S_{2}$ does not, we get an evaluation $\nu$ with $\nu(\widehat{p}_{1})=\mathtt{False}$ and $\nu(\widehat{p}_{1})=\mathtt{True}$. Since $\nu\models\widehat{p}_{1}\lor\widehat{p}_{2}$, then the result of the application of $S$ to $t$ is precisely the result of the application of $@p_{2}.S_{2}$ to $t$, making $@p_{1}.S_{1}$ behaving like the identity.

It’s worth mentioning that the aim of incorporation of the Boolean formulas in CE-strategies is to make it expressive enough so we can write the standard traversal strategies (see Example 12). The fragment of CE-strategies without Boolean formulas remains closed under unification and combination.

We shall sometimes write $\mu X.S(X)$ instead of $\mu X.S$ to emphasize that the fixed-point variable $X$ is free in $S$.

To define the semantics of CE-strategies we need to introduce an intermediary function $\eta:\mathfrak{F}(\mathcal{T}\cup\{{\mathbb{F}}\})\rightarrow\mathcal{T}\cup\{{\mathbb{F}}\}\rightarrow\mathcal{T}\cup\{{\mathbb{F}}\}$, that stands for the fail as identity. It is defined for any function $f$ in $\mathfrak{F}(\mathcal{T}\cup\{{\mathbb{F}}\})$ and any term $t\in\mathcal{T}\cup\{{\mathbb{F}}\}$ by

[TABLE]

Beside, let $S^{i+1}(S^{\prime})\stackrel{{\scriptstyle def}}{{=}}S^{i}(S(S^{\prime}))$, for all any CE-strategies $S(X)$ and $S^{\prime}$ in $\mathcal{C}$. A CE-strategy strategy is closed if all its fixed-point variables are bound.

Definition 10** (Semantics of CE-strategies)**

The semantics of a closed CE-strategy $S$ is a function $[\![S]\!]$ in $\mathfrak{F}(\mathcal{T}\cup\mathbb{F})$, which is defined inductively as follows.

[TABLE]

[TABLE]

For any CE-strategies $S,S^{\prime}$ in $\mathcal{C}$, we shall write $S\equiv S^{\prime}$ iff $[\![S]\!]=[\![S^{\prime}]\!]$. To simplify the presentation, we shall write $(u,S)$ instead of $(u\rightarrow u);S$ and we shall write $(u,\boldsymbol{\tau})$ instead of $u\rightarrow u[\boldsymbol{\tau}]$.

Example 11

Let $\mathcal{F}=\{{f,a}\}$ be a set of two functional symbols where $ar(f)=1$ and $ar(a)=0$. The CE-strategy S=\mu.X\big{(}(f(a),\boldsymbol{\tau})\oplus(@1.X)\big{)}, when applied to a term $t$, matches the pattern $f(a)$ with the term $t$ at the root. If it is the case, then it inserts $\boldsymbol{\tau}$ at the root position of $t$. Otherwise, it jumps to the position $1$ of $t$ and restarts again. Obviously, if it reaches a leaf of $t$ then it fails since the position $1$ does not exist.

Example 12

We show how to encode some standard traversal strategies in our formalism using the fixed-point constructor. In what follows we assume that $S$ is a CE-strategy. We recall that, when applied to a term $t$, the CE-strategy $\mathtt{OneLeft}(S)$ tries to apply $S$ to the subterm of $t$ (if any) which is the closest to the root and on the far-left. The CE-strategy $\mathtt{TopDown}(S)$ tries to apply $S$ to the maximum of the sub-terms of $t$ starting from the root of $t$, it stops when it is successfully applied. Hence,

[TABLE]

We generalize next the condition of well-foundedness from position-based CE-strategies to CE-strategies. Before that, it is helpful to view a CE-strategy as a tree with back-edges. A tree with back-edges is an oriented tree with possible edges going from a node to at most one of its ancestors in the tree. For instance, the tree-like structure of the CE-strategy $S(X)=(f(x),\boldsymbol{\tau})\oplus(@1.X)$, where the fixed-point variable $X$ is free, is depicted on the left of Figure 3. While the tree with- back-edge related to $\mu X.S(X)$ is depicted on the right.

Definition 13** (Well-founded CE-strategies.)**

A CE-strategy $S$ is well-founded iff

1. i.)

Every cycle in $S$ passes through a position111This constraint is similar to the one imposed on the modal $\mu$-calculus formulas in which each cycle has to pass through a modality [AN01].. 2. ii.)

All its sub-strategies of the form $\langle{[@p_{1}.{S}_{1},\ldots,@p_{n}.{S}_{n},@q_{1}.\boldsymbol{\tau}_{1},\ldots,@q_{m},\boldsymbol{\tau}_{m}]}\,|\,{\phi}\rangle$, where $n+m\geq 1$ and $p_{i},q_{j}$ are positions and $\boldsymbol{\tau}_{i}$ are tuples of contexts in ${T}_{\square}^{\star}$ and ${S}_{i}$ are CE-strategies, are subject to the following conditions:

1. (a)

$q_{i}\sqsubset q_{j}$, for all $i<j$, where $i,j\in[m]$, and 2. (b)

$p_{i}\parallel p_{j}$, for all $i\neq j$, where $i,j\in[n]$, and 3. (c)

$q_{j}\sqsubset p_{i}$, for all $j\in[m]$ and $i\in[n]$.

For instance the CE-strategy $\mu X.((f(x),\boldsymbol{\tau})\oplus X)$ is not well-founded because the cycle that corresponds to the regeneration of the variable $X$ does not cross a position. while the CE-strategy $\mu X.((f(x),\boldsymbol{\tau})\oplus(@1.X))$ is well-founded. In all what follows we assume that the CE-strategies are well-founded. Notice that any CE-strategy is terminating. This is a direct consequence of Item (i) of the well-foundedness of CE-strategies, that is, every cycle in a well-founded CE-strategy passes through a position delimiter.

The set of Boolean formulas (resp. positions) of an CE-strategy $S$, will be denoted by $\Phi(S)$ (resp. ${\cal P}os(S)$). It is defined in a straightforward way.

IV.3 Canonical form of CE-strategies

Instead of the direct combination of CE-strategies, we shall first simplify the CE-strategies by turning each CE-strategy into an equivalent CE-strategy in the canonical form. A CE-strategy is in the canonical form if each of its Boolean formulas is a conjunction of position-variables, where each position-variable is in $\widehat{\mathbb{N}}_{\epsilon}$ instead of $\widehat{\mathbb{N}}^{\star}_{\epsilon}$. The advantage of the use of canonical CE-strategies is that their combination is much simpler.

Definition 14** (Canonical form of CE-strategies)**

An CE-strategy strategy $S$ is in the canonical form iff any Boolean formula $\phi$ in $\Phi(S)$ is of the form $\phi=\bigwedge_{i}\widehat{p}_{i}$, where $\widehat{p}_{i}\in\widehat{\mathbb{N}}_{\epsilon}$. The set of CE-strategies in the canonical form is denoted by $\mathcal{C}^{o}$.

It follows that if a CE-strategy $S$ is in the canonical form, then we have ${\cal P}os(S)\subset\mathbb{N}_{\epsilon}$.

Lemma 15

Any CE-strategy can be turned into an equivalent CE-strategy in the canonical form.

Proof. (Sketch) Firstly, we turn all the Boolean formulas of the CE-strategy into formulas in the disjunctive normal form. Then we express the disjunction in terms of the left-choice strategy. Secondly, we turn each position in $\mathbb{N}^{\star}_{\epsilon}$ into a secession of positions in $\mathbb{N}_{\epsilon}$ by relying on the fact that a CE-strategy $@(ip).S$ is equivalent to $@i.(@p.S)$, where $i\in\mathbb{N}_{\epsilon}$ and $p\in\mathbb{N}^{\star}_{\epsilon}$.

IV.4 From CE-strategies to position-based CE-strategies

Out of a CE-strategy and a term it is possible to construct an position-based CE-strategy. The main purpose of this mapping is to formulate a correctness criterion for the combination of CE-strategies in terms of position-based CE-strategies.

Definition 16

Define the function $\Psi:\mathcal{C}\times\mathcal{T}\longrightarrow\mathcal{E}$, that associates to each closed CE-strategy $S$ in $\mathcal{C}$ and a term $t$ in $\mathcal{T}$ an position-based CE-strategy $\Psi(S,t)$ in $\mathcal{E}$ by

[TABLE]

[TABLE]

If $S=\sqcup_{i\in[n]}@p_{i}.S_{i}$, then

[TABLE]

The application of the position-based CE-strategy $\Psi(S,t)$ to the term $t$ will be simply written as $\Psi(S,t)(t)$ instead of $[\![\Psi(S,t)]\!](t)$.

It turns out that the function $\Psi$ (Definition 16) preserves the semantics of CE-strategies in the following sense.

Lemma 17

For any CE-strategy $S$ in $\mathcal{C}$ and any term $t$ in $\mathcal{T}$, we have $[\![S]\!](t)=\Psi(S,t)(t)$.

The proof of this Lemma does not provide any difficulties since the definition of $\Psi$ is close to the definition of the semantics of CE-strategies.

Lemma 18

The function $\Psi$ enjoys the following properties.

1. i.)

For any position-based CE-strategies $E,E^{\prime}$ in $\mathcal{E}$, we have that $E=E^{\prime}$ iff $\Psi(E,t)=\Psi(E^{\prime},t)$ for any term $t$. 2. ii.)

For any CE-strategies $S,S^{\prime}$ in $\mathcal{C}$, we have that $S\equiv S^{\prime}$ iff $\Psi(S,t)=\Psi(S^{\prime},t)$ for any term $t$.

V Unification and combination of CE-strategies

We define the combination of CE-strategies (Definition 21) by means of their unification (Definition 19) together with an example. The first main result of this section is Theorem 24 that guarantees the correctness of the combination of CE-strategies. The correctness is given in terms of the position-based CE-strategies, it imposes that the mapping (via the homomorphism $\Psi$ of Definition 16) of the combination of two CE-strategies is equivalent to the combination of their respective mapping. Besides, Theorem 24 is a consequence of Theorem 23 which is more difficult and proves the same result but for the unification of CE-strategies instead of the combination. The second main result is the nice algebraic properties of the unification and combination of CE-strategies, stated in Proposition 25. In particular, the combination and unification are associative, which is an important property in the applications, and are a congruence

Instead of unifying/combining CE-strategies directly, we unify/combine their canonical forms. We omit the symmetric cases in the following definition which is given by an induction on the CE-strategies by exhibiting all the possible cases.

Definition 19** (Unification of canonical CE-strategies)**

The unification of CE-strategies in the canonical form is a binary operation $\curlywedge:\mathcal{C}^{o}\times\mathcal{C}^{o}\longrightarrow\mathcal{C}^{o}$ inductively defined as follows.

[TABLE]

[TABLE]

*For the rest, let $\mathcal{L}=\bigsqcup\limits_{i\in\mathcal{I}}@i.S_{i}$ and $\mathcal{L}^{\prime}=\bigsqcup\limits_{j\in\mathcal{J}}@j.S^{\prime}_{j}$.

Let $\mathcal{L}_{1}=\bigsqcup\limits_{i\in\mathcal{I}\cap\mathcal{J}}@i.(S_{i}\curlywedge S^{\prime}_{i})$ and $\mathcal{L}_{2}=\bigsqcup\limits_{i\in\mathcal{I}\setminus\mathcal{J}}@i.S_{i}$ and $\mathcal{L}_{3}=\bigsqcup\limits_{i\in\mathcal{J}\setminus\mathcal{I}}@i.S^{\prime}_{i}$. Define*

[TABLE]

For the fixed-point CE-strategies,

[TABLE]

Comments. We comment on the key points in Definition 19. The unification of $(u,S)$ with $(u^{\prime},S^{\prime})$ is naturally $(u\land u^{\prime},S\curlywedge S^{\prime})$ since we want to merge them. The idea behind the unification of $\mu X.S(X)$ with $\mu X^{\prime}.S^{\prime}(X^{\prime})$ is to unfold $\mu X.S(X)$ (resp. $\mu X^{\prime}.S^{\prime}(X^{\prime})$) to S(\varnothing)\oplus S\big{(}\mu X.S(X)\big{)} (resp. $S^{\prime}(\varnothing)\oplus S^{\prime}(\mu X^{\prime}.S^{\prime}(X^{\prime}))$) and to combine the resulting CE-strategy. This is achieved by firstly unifying $S(X)$ with $S^{\prime}(X^{\prime})$, where clearly the fixed-point variable $X$ (resp. $X^{\prime}$) is free in $S(X)$ (resp. $S^{\prime}(X^{\prime})$). The resulting CE-strategy $S^{\prime\prime}(X,X^{\prime},X\curlywedge X^{\prime})$ contains three free fixed-point variables. The key point is to view $X\curlywedge X^{\prime}$ as a fresh fixed-point variable, say $Z$, and to bind it to the full expression $S^{\prime\prime}(\mu X.S(X),\mu X^{\prime}.S^{\prime}(X^{\prime}),Z)$, meaning that $Z$ corresponds exactly to the CE-strategy that we are defining.

Example 20

Let $S(X)=(u,\boldsymbol{\tau})\oplus@1.X$ and $S^{\prime}(X^{\prime})=(u^{\prime},\boldsymbol{\tau}^{\prime})\oplus@1.X^{\prime}$, be two CE-strategies. We compute $\mu X.S(X)\curlywedge\mu X^{\prime}.S^{\prime}(X^{\prime})$. Firstly, the unification $(*)$ of $S(X)$ and $S^{\prime}(X^{\prime})$ yields:

[TABLE]

Hence, combination of $\mu X.S(X)$ and $\mu X^{\prime}.S^{\prime}(X^{\prime})$ is

[TABLE]

Definition 21** (Combination of canonical CE-strategies)**

The combination of CE-strategies in the canonical form is a binary operation $\curlyvee:\mathcal{C}^{o}\times\mathcal{C}^{o}\longrightarrow\mathcal{C}^{o}$, defined for any ${S}$ and ${S}^{\prime}$ in $\mathcal{C}^{o}$ by ${S}\curlyvee{S}^{\prime}\stackrel{{\scriptstyle def}}{{=}}({S}\curlywedge{S}^{\prime})\oplus{S}\oplus{S}^{\prime}$.

The unification and combination of CE-strategies can be defined in terms of their canonical form.

Definition 22** (Unification and combination of CE-strategies)**

Let $S,S^{\prime}$ be two CE-strategies in $\mathcal{C}$ and $\tilde{S},\tilde{S}^{\prime}\in\mathcal{C}^{o}$ their canonical form, respectively. The unification (resp. combination) of $S$ and $S^{\prime}$ is defined by $S\curlywedge S^{\prime}\stackrel{{\scriptstyle def}}{{=}}\tilde{S}\curlywedge\tilde{S}^{\prime}$ (resp. $S\curlyvee S^{\prime}\stackrel{{\scriptstyle def}}{{=}}\tilde{S}\curlyvee\tilde{S}^{\prime}$).

Now we are ready to state the main results of this paper: the unification (Theorem 23) and combination (Theorem 24) of CE-strategies are correct.

Theorem 23

For every term $t\in\mathcal{T}$ and for every CE-strategies $S$ and $S^{\prime}$ in the canonical form in $\mathcal{C}^{o}$, we have that

[TABLE]

Theorem 24

For every term $t\in\mathcal{T}$, for every CE-strategies $S$ and $S^{\prime}$ in the canonical form in $\mathcal{C}^{o}$, we have that

[TABLE]

Since each CE-strategy can be turned into an equivalent CE-strategy in the canonical form (Lemma 15) and since the image of two equivalent CE-strategies under the homomorphism $\Psi$ is identical (Item ii. of Lemma 18), then Theorems 23 and 24 hold for the class of CE-strategies as well.

Besides, thanks to the fact that the function $\Psi$ is an homomorphism (in the first argument), one can transfer all the properties of the combination and unification of position-based CE-strategies (stated in Proposition 7) to CE-strategies.

Proposition 25

The following hold.

The set $\mathcal{C}$ of CE-strategies together with the unification and combination operations enjoy the following properties.

1. (a)

The neutral element of the unification and combination is $@\epsilon.\square$. 2. (b)

Every CE-strategy $S$ is idempotent for the unification and combination, i.e. $S\curlywedge S=S$ and $S\curlyvee S=S$. 3. (c)

The unification and combination of CE-strategies are associative. 2. 2.

The unification and combination of CE-strategies is non commutative. 3. 3.

*For any CE-strategies $S$ and $S^{\prime}$ in $\mathcal{C}$, and for any term $t$ in $\mathcal{T}$, we have that

[TABLE] 4. 4.

The unification and combination of CE-strategies is a congruence, that is, for any CE-strategies $S_{1},S_{2},S$ in $\mathcal{C}$, we have that:

[TABLE]

VI Conclusion and future work

We addressed the problem of extension and combination of proofs encountered in the field of computer aided asymptotic model derivation. We identified a class of rewriting strategies of which the operations of unification and combination were defined and proved correct. The design of this class is inspired by the $\mu$-calculus formalism [AN01]. On the other hand we use of the fixed-point operator which is finer and more powerful than the repeat constructor used e.g. in [CKLW03].

The CE-strategies are indeed modular in the sense that they navigate in the tree without modifying it, then they insert contexts. This makes our formalism flexible since it allows one to modify and enrich the navigation part and/or the insertion part without disturbing the set-up.

Although the CE-strategies can be viewed as a finite algebraic representation of infinite trees [Cou83], our technique of the unification and combination involving $\mu$-terms and their unfolding is new. Therefore, we envision consequences of these results on the study of the syntactic (or modulo a theory) unification and the pattern-matching of infinite trees once the infinite trees are expressed as $\mu$-terms in the same way we expressed the CE-strategies. Thus, a rewriting language that transforms algebraic infinite trees can be elaborated.

Appendix A: detailed proofs for reviewers

VII Proofs for preliminary section II

If $\pi=\{{\widehat{p}_{1},\ldots,\widehat{p}_{n}}\}$ is a set of variable-positions, then we shall write $\bigwedge\pi$ (resp. $\bigvee\pi$) for the Boolean formula $\widehat{p}_{1}\land\ldots\land\widehat{p}_{n}$ (resp. $\widehat{p}_{1}\lor\ldots\lor\widehat{p}_{n}$). In particular, $\bigwedge\emptyset=\bigvee\emptyset=\mathtt{False}$.

Fact 26

Let $u,t$ be two terms and $\gamma,\gamma^{\prime}$ two substitutions. We have that, if $\gamma(u)\ll t$ and $\gamma$ is subsumed by $\gamma^{\prime}$, then $\gamma^{\prime}(u)\ll t$ as well.

Lemma 27

Let $u,u^{\prime},t$ be terms in $\mathcal{T}$. Then,

[TABLE]

Proof. For the direction $(\Rightarrow)$, let $\gamma$ be the most general unifier of $u$ and $u^{\prime}$, and $\alpha$ be a substitution such that $\alpha(u\land u^{\prime})=t$. This means that $\alpha(\gamma(u))=t$ and $\alpha(\gamma(u^{\prime}))=t$. That is, $\gamma(u)\ll t$ and $\gamma(u^{\prime})\ll t$.

For the direction $(\Leftarrow)$, let $\sigma$ and $\sigma^{\prime}$ be substitutions such that $\sigma(u)=t$ and $\sigma^{\prime}(u^{\prime})=t$. Consider the decomposition $\sigma=\sigma_{1}\uplus\sigma_{2}$ and $\sigma^{\prime}=\sigma^{\prime}_{1}\uplus\sigma^{\prime}_{2}$, where ${\mathsf{Dom}}(\sigma_{1})\cap{\mathsf{Dom}}(\sigma^{\prime}_{1})=\emptyset$ and ${\mathsf{Dom}}(\sigma_{2})={\mathsf{Dom}}(\sigma^{\prime}_{2})$. Since $\sigma(u)=\sigma^{\prime}(u^{\prime})$, it follows that $\sigma_{2}=\sigma^{\prime}_{2}$. But this means that $\sigma_{2}(u)=\sigma_{2}(u^{\prime})$, and $\sigma_{2}(u)\ll t$. In other words, $u$ and $u^{\prime}$ can be unified. Let $\gamma$ be the most general unifier of $u$ and $u^{\prime}$. But since $\sigma_{2}(u)\ll t$ and $\sigma_{2}$ is subsumed by $\gamma$, then it follows from Fact 26 that $\gamma(u)\ll t$.

VIII Proofs and formal definitions for section IV

VIII.1 Set of Boolean formulas and positions of a CE-strategy

Definition 28** (Set of Boolean formulas and positions of a CE-strategy)**

The set of Boolean formulas (resp. positions) of an CE-strategy $S$, denoted by $\Phi(S)$ (resp. ${\cal P}os(S)$), is inductively defined by

[TABLE]

VIII.2 Depth of CE-strategies

Taking into account that the structure of a CE-strategy is no longer a tree but a tree with back-edges that may contains cycles, we slightly modify the standard measure of the depth of trees in order to capture both the number of nested loops, caused by the nested application of the constructor $\mu$, and the distance from the root of the tree to the leaves. Many proofs will be done by induction with respect to this measure.

Definition 29** (Depth of a CE-strategy)**

The depth of an CE-strategy is function $\Delta:\mathcal{C}\longrightarrow\mathbb{N}\times\mathbb{N}$ defined inductively as follows.

[TABLE]

We shall denoted by $<,\leq$ and $>,\geq$ the related lexicographic orders on $\mathbb{N}\times\mathbb{N}$.

Notice that if a CE-strategy $S$ is iteration-free, i.e. it does not contain the constructor $\mu$, then its depth $\Delta(S)=(0,n)$, for some $n\in\mathbb{N}$.

VIII.3 Canonical form of CE-strategies

Lemma 30

(i.e. Lemma 15) Any CE-strategy can be turned into an equivalent CE-strategy in the canonical form.

Proof. Firstly, we turn all the Boolean formulas of the CE-strategy into formulas in the disjunctive normal form. Then we express the disjunction in terms of the left-choice strategy. (Lemmas 31 and 32). Thus we obtain an equivalent CE-strategy in which all the Boolean formulas are conjunctions of position-variables. Secondly, we turn each position in $\mathbb{N}^{\star}_{\epsilon}$ into a secession of positions in $\mathbb{N}_{\epsilon}$ (Lemma 33) by relying on the fact that the CE-strategy $@(ip).S$ is equivalent to $@i.(@p.S)$, where $i\in\mathbb{N}_{\epsilon}$ and $p\in\mathbb{N}^{\star}_{\epsilon}$.

Lemma 31

Let $p_{1},\ldots,p_{n}$ be parallel positions in $\mathbb{N}^{\star}_{\epsilon}$, and $S_{1},\ldots,S_{n}$ be CE-strategies, with $n\geq 1$. Let $\pi,\pi^{\prime}\subseteq\{{\widehat{p}_{1},\ldots,\widehat{p}_{n}}\}$ with $\pi\cup\pi^{\prime}=\{{\widehat{p}_{1},\ldots,\widehat{p}_{n}}\}$ and let $\phi=\bigwedge\pi$ and $\phi^{\prime}=\bigwedge\pi^{\prime}$ be Boolean formulas. Let $\mathcal{S}=[@p_{1}.S_{1},\ldots,@p_{n}.S_{n}]$. Then we have the equivalence

[TABLE]

Proof. Recall that

[TABLE]

We discuss four cases depending on whether $\mathcal{V}({\mathcal{S}},{t})\models\phi$ or $\mathcal{V}({\mathcal{S}},{t})\models\phi^{\prime}$.

If $\mathcal{V}({\mathcal{S}},{t})\models\phi$ and $\mathcal{V}({\mathcal{S}},{t})\models\phi^{\prime}$, then in this case

[TABLE]

Thus Eq. (31) holds. 2. 2.

If $\mathcal{V}({\mathcal{S}},{t})\models\phi$ and $\mathcal{V}({\mathcal{S}},{t})\not\models\phi^{\prime}$, then we must show that

[TABLE]

However, Eq. (2) follows from the fact that $\mathcal{V}({\mathcal{S}},{t})\models\phi$ and $\mathcal{V}({\mathcal{S}},{t})\not\models\phi^{\prime}$.

To prove Eq. (3), we let

[TABLE]

Hence, $\mathcal{V}({\mathcal{S}},{t})\models\phi\lor\phi^{\prime}$ if and only if $\mathcal{V}({\mathcal{S}_{|\pi\cup\wp^{\prime}}},{t})\models\phi\land{\phi^{\prime}}_{|\wp^{\prime}}$. Besides,

[TABLE]

and

[TABLE]

Summing up, Eq. (3) holds.

To prove Eq. (4), we notice that there exists $\widehat{p}\in\varrho^{\prime}$ such that $\mathcal{V}({S},{t})(\widehat{p})=\mathtt{False}$, and hence $\mathcal{V}({S_{\pi\cup\varrho^{\prime}}},{t})\not\models\phi^{\prime}_{|\varrho^{\prime}}$, making $[\![\langle{\mathcal{S}_{|\pi\cup\varrho^{\prime}}}\,|\,{\phi\land{\phi^{\prime}}_{|\varrho^{\prime}}}\rangle]\!](t)=\mathbb{F}$. Thus Eq. (31) holds. 3. 3.

If $\mathcal{V}({\mathcal{S}},{t})\not\models\phi$ and $\mathcal{V}({\mathcal{S}},{t})\models\phi^{\prime}$, then this case is similar to the case when $\mathcal{V}({\mathcal{S}},{t})\models\phi$ and $\mathcal{V}({\mathcal{S}},{t})\not\models\phi^{\prime}$ discussed above in Item 2. 4. 4.

If $\mathcal{V}({\mathcal{S}},{t})\not\models\phi$ and $\mathcal{V}({\mathcal{S}},{t})\not\models\phi^{\prime}$, then in this case

[TABLE]

making the Eq. (31) hold.

Lemma 32

Let $p_{1},\ldots,p_{n}$ be parallel positions in $\mathbb{N}^{\star}_{\epsilon}$, and $S_{1},\ldots,S_{n}$ be CE-strategies, with $n\geq 1$. Let $\pi=\{{\widehat{p}_{1},\ldots,\widehat{p}_{n}}\}$ and Let $\mathcal{S}=[@p_{1}.S_{1},\ldots,@p_{n}.S_{n}]$. Then we have the equivalence

[TABLE]

Proof. We recall that

[TABLE]

Out of the valuation $\mathcal{V}({\mathcal{S}},{t})$, we shall show that there exists a unique $\wp\subseteq\pi$ such that

[TABLE]

and that for all $\wp^{\prime}\subseteq\pi$ where $|\wp^{\prime}|\geq|\wp|$ and $\wp^{\prime}\neq\wp$, we have that

[TABLE]

For this purpose, we define $\wp$ by

[TABLE]

Therefore, $\mathcal{V}({\mathcal{S}},{t})\models\bigvee\pi$ iff $\mathcal{V}({\mathcal{S}_{|\wp}},{t})\models\bigwedge\wp$, and

[TABLE]

Hence Eq. (6) holds. And Eq. (7) follows from the fact that there exists $\widehat{q}\in\wp^{\prime}$ such that $\mathcal{V}({\mathcal{S}},{t})(\widehat{q})=\mathtt{False}$, thus $\mathcal{V}({\mathcal{S}_{|\wp^{\prime}}},{t})(\widehat{q})=\mathtt{False}$ and $\mathcal{V}({\mathcal{S}_{|\wp^{\prime}}},{t})\not\models\bigwedge\wp^{\prime}$.

Lemma 33

Each CE-strategy in which every Boolean formulas is a conjunction of position-variables in $\widehat{\mathbb{N}}^{\star}_{\epsilon}$, can be turned into an equivalent CE-strategy in which every Boolean formulas is a conjunction of position-variables in $\widehat{\mathbb{N}}_{\epsilon}$.

Proof. Let $S$ be CE-strategy strategy. The idea is simple. If there are no Boolean formulas in the CE-strategy, then we rely on the observation that the CE-strategy $@(ip).S^{\prime}$ is equivalent to $@i.(@p.S^{\prime})$ where $i\in\mathbb{N}_{\epsilon}$ and $p\in\mathbb{N}^{\star}_{\epsilon}$. Which means that we use the reduction rule

[TABLE]

to put the CE-strategy in the canonical form. We generalize the rule (8) to take into account the presence of Boolean formulas as follows. Let

[TABLE]

Then we define the reduction rule

[TABLE]

Since all the Boolean formulas are conjunctions of position-variables, then we have

[TABLE]

VIII.4 Properties of the function $\Psi$

Lemma 34** ($\Psi$ preserves the semantics, i.e. Lemma 17)**

For any CE-strategy $S$ in $\mathcal{C}$ and any term $t$ in $\mathcal{T}$,

[TABLE]

Proof. The proof is by induction on $\Delta(S)$, the depth of $S$.

Basic case: $\Delta(S)=(0,0)$.

We distinguish three cases depending on $S$.

1. 1.

If $S=\varnothing$, then this case is trivial. 2. 2.

If $S=@p.\boldsymbol{\tau}$. This case is trivial since $\Psi(S,t)\stackrel{{\scriptstyle def}}{{=}}S$. 3. 3.

If $S=(u,\boldsymbol{\tau})$. In this case

[TABLE]

and on the other hand,

[TABLE]

That is, $[\![S]\!](t)=\Psi(S,t)(t)$.

Induction case: $\Delta(S)>(0,0)$.

We distinguish three cases depending on $S$.

1. 1.

If $S$ is a left-choice of the form

[TABLE]

then,

[TABLE]

and

[TABLE]

Since $\Psi(S_{1},t)=\varnothing$ iff $\Psi(S_{1},t)(t)=\mathbb{F}$, we get

[TABLE]

From the induction hypothesis we have that $[\![S_{i}]\!](t)=\Psi(S_{i},t)(t)$ for $i=1,2$. Hence, $[\![S_{1}\oplus S_{2}]\!](t)=\Psi(S_{1}\oplus S_{2},t)(t)$. 2. 2.

If $S$ is of the form

[TABLE]

then let

[TABLE]

On the one hand

[TABLE]

On the other hand, let

[TABLE]

Thus

[TABLE]

It remains to show that, for any term $t$ in $\mathcal{T}$,

[TABLE]

But $f^{\prime}=[\![\mathcal{L}^{\prime}]\!]$, and thus it remains to show that

[TABLE]

However,

[TABLE]

From the induction hypothesis we have $[\![S_{i}]\!](t_{|p_{i}})=\Psi(S_{i},t_{|p_{i}})(t_{|p_{i}})$. Therefore, the Eq. (10) holds. 3. 3.

If $S$ is of the form $S=\mu X.S(X)$, then the claims follows from the fact that

[TABLE]

by applying the induction hypothesis, since

[TABLE]

because if \Delta\big{(}\bigoplus_{i=1,\delta(t)}S^{i}(\varnothing)\big{)}=(n,m), for some $n,m\in\mathbb{N}$, then \Delta\big{(}\mu X.S(X)\big{)}=(n+1,m^{\prime}), for some $m^{\prime}>m$.

This ends the proof of Lemma 17.

Lemma 35** (i.e. Lemma 18)**

The function $\Psi$ enjoys the following properties.

1. i.)

For any elementary CE-strategies $E,E^{\prime}$ in $\mathcal{E}$, we have that

[TABLE]

for any term $t$. 2. ii.)

For any CE-strategies $S,S^{\prime}$ in $\mathcal{C}$, we have that

[TABLE]

for any term $t$.

Proof. We only prove Item ii.), the other item follows immediately from the definition of $\Psi$. On the one hand, from the definition of $\equiv$ we have that

[TABLE]

However, it follows from Lemma 17 that

[TABLE]

Therefore,

[TABLE]

Since, both $\Psi(S,t)$ and $\Psi(S^{\prime},t)$ are elementary CE-strategies, it follows from Item i.) of this Lemma that $\Psi(S,t)=\Psi(S^{\prime},t)$.

IX Proofs for section V

IX.1 Correctness and Completeness of the unification and combination of CE-strategies.

Theorem 36** (i.e. Theorem 23)**

For every term $t\in\mathcal{T}$, for every CE-strategies $S$ and $S^{\prime}$ in the canonical form in $\mathcal{C}^{o}$, we have that

[TABLE]

Proof. The proof is by a double induction on $\Delta(S)$ and $\Delta(S^{\prime})$. We recall that if there are two symmetric cases, we only prove one of them. We make an induction on $\Delta(S)$.

Base case: $\Delta(S)=(0,0)$.

We make an induction on $\Delta(S^{\prime})$.

Base case: $\Delta(S^{\prime})=(0,0)$.

We distinguish three cases depending on the structure of $S$ and $S^{\prime}$.

1. 1.

The cases when $(S,S^{\prime})=(\varnothing,\varnothing)$ or $(S,S^{\prime})=(@i.\boldsymbol{\tau},@j.\boldsymbol{\tau}^{\prime})$ are trivial whether $i=j$ or not. 2. 2.

If (S,S^{\prime})=\big{(}@i.\boldsymbol{\tau},(u,\boldsymbol{\tau}^{\prime})\big{)}, where $i\in\mathbb{N}_{\epsilon}\setminus\{{\epsilon}\}$, then in this case

[TABLE]

On the other hand,

[TABLE]

Hence

[TABLE] 3. 3.

If $S=@\epsilon.\boldsymbol{\tau}$ and $S^{\prime}=(u,\boldsymbol{\tau}^{\prime})$, then this case is similar to the previous one except that the insertion of the tuples of the contexts $\boldsymbol{\tau}$ and $\boldsymbol{\tau}^{\prime}$ occurs at the root position instead of two different positions. We have that

[TABLE]

On the other hand,

[TABLE]

Hence

[TABLE]

Induction step: $\Delta(S^{\prime})>(0,0)$.

We distinguish six cases depending on the structure of $S$ and $S^{\prime}$.

1. 1.

If $S=(@i,\boldsymbol{\tau})$ and $S^{\prime}=(u^{\prime},R^{\prime})$, where $i\in\mathbb{N}_{\epsilon}$, then in this case

[TABLE]

Since $\Delta(R^{\prime})<\Delta(S^{\prime})$, it follows from the induction hypothesis that

[TABLE]

On the other hand,

[TABLE]

Hence the unification $\Psi(S,t)\curlywedge\Psi(S^{\prime},t)$ is defined by

[TABLE] 2. 2.

If $S=(@i,\boldsymbol{\tau})$ and $S^{\prime}=\langle{\bigsqcup_{j\in J}@j.S_{j}}\,|\,{\phi}\rangle$, where $i\in\mathbb{N}_{\epsilon}$, then we only discuss the case when $i\in J$, the case when $i\notin I$ is immediate. In this case, let

[TABLE]

and

[TABLE]

Since $\Delta(S_{i})<\Delta(S^{\prime},t)$, it follows from the induction hypothesis that

[TABLE]

On the other hand,

[TABLE]

and since $i\in J$, the unification of $\Psi(S,t)$ and $\Psi(S^{\prime},t)$ is

[TABLE]

Since $\phi$ is a conjunction of position-variables, and $i\in J$, which means $i\in{\cal V}ar(\mathcal{S})$, then

[TABLE]

That leads to $\Psi(S\curlywedge S^{\prime},t)=\Psi(S,t)\curlywedge\Psi(S^{\prime},t)$. 3. 3.

If $S=(@i.\boldsymbol{\tau})$ and $S^{\prime}=\mu Z.R(Z)$, where $i\in\mathbb{N}_{\epsilon}$, then in this case

[TABLE]

If we assume that \Delta\big{(}\bigoplus_{i=1,\delta(t)}R^{i}(\varnothing)\big{)}=(n,m), for some $n,m\in\mathbb{N}$, then \Delta\big{(}\mu Z.R(Z)\big{)}=(n+1,m^{\prime}), for some $m^{\prime}\in\mathbb{N}$. Meaning that \Delta\big{(}\bigoplus_{i=1,\delta(t)}R^{i}(\varnothing)\big{)}<\Delta\big{(}\mu Z.R(Z)\big{)}. Thus it follows from the induction hypothesis that

[TABLE]

On the hand,

[TABLE]

Hence,

[TABLE] 4. 4.

If $S=(u,\boldsymbol{\tau})$ and $S^{\prime}=(u^{\prime},R^{\prime})$, then in this case

[TABLE]

On the other hand,

[TABLE]

Since

[TABLE]

We get

[TABLE] 5. 5.

If $S=(u,\boldsymbol{\tau})$ and $S^{\prime}=\langle{\bigsqcup_{i\in I}@i.S^{\prime}_{i}}\,|\,{\phi^{\prime}}\rangle$, then we only prove the case when $I\subset\mathbb{N}_{\epsilon}\setminus\{{\epsilon}\}$, the case when $\epsilon\in I$ is similar. We have that

[TABLE] 6. 6.

If $S=(u,\boldsymbol{\tau})$ and $S^{\prime}=\mu Z.R(Z)$, then this case is similar to the case where $S=@i.\boldsymbol{\tau}$ discussed before.

Induction step: $\Delta(S)>(0,0)$.

We make an induction on $\Delta(S^{\prime})$.

Base case: $\Delta(S^{\prime})=(0,0)$.

This case is symmetric to the case where $\Delta(S)=(0,0)$ and $\Delta(S^{\prime})>(0,0)$ discussed before.

Induction step: $\Delta(S^{\prime})>(0,0)$.

We distinguish four cases.

1. 1.

If $S=(u,R)$ and $S^{\prime}=(u^{\prime},R^{\prime})$, then in this case

[TABLE]

Since

[TABLE]

and since $\Delta(R)<\Delta(S)$ and $\Delta(R^{\prime})<\Delta(S^{\prime})$, it follows from the induction hypothesis that

[TABLE]

On the other hand,

[TABLE]

Therefore $\Psi(S,t)\curlywedge\Psi(S^{\prime},t)=\Psi(S\curlywedge S^{\prime},t)$. 2. 2.

If $S$ and $S^{\prime}$ are lists of position delimiters of the form

[TABLE]

where $\mathcal{I},\mathcal{J}\subset\mathbb{N}_{\epsilon}$, then let

[TABLE]

On the one hand we have that

[TABLE]

Hence, the unification $\Psi(S,t)\curlywedge\Psi(S^{\prime},t)$ is defined by

[TABLE]

On the other hand, let

[TABLE]

and thus the combination $S\curlywedge S^{\prime}$ is defined by

[TABLE]

To simplify the presentation, let

[TABLE]

Thus $\Psi(S\curlywedge S^{\prime},t)$ can be written as

[TABLE] 3. 3.

\langle{\bigsqcup\limits_{i\in\mathcal{I}}@i.S_{i}}\,|\,{\phi}\rangle\curlywedge(u^{\prime},S^{\prime})=\big{(}u^{\prime},\langle{\bigsqcup\limits_{i\in\mathcal{I}}@i.S_{i}}\,|\,{\phi\curlywedge S^{\prime}}\rangle\big{)} 4. 4.

If $S=\mu X.S(X)$ and $S^{\prime}=\mu X^{\prime}.S^{\prime}(X^{\prime})$, then we have

[TABLE]

Let $t\in\mathcal{T}$ and let $n=\delta(t)$. To show that

[TABLE]

it is sufficient to show that

[TABLE]

We have that for all $i\geq 1$,

[TABLE]

hence,

[TABLE]

Hence,

[TABLE] 5. 5.

The cases of $(\mu X.S(X))\curlywedge S^{\prime}$ and $S\curlywedge\mu X^{\prime}.S^{\prime}(X^{\prime})$ are similar to the previous one. 6. 6.

If $S=S_{1}\oplus S_{2}$ then we recall that

[TABLE]

and

[TABLE]

Hence,

[TABLE]

Since $\Delta(S_{i})<\Delta(S)$, for $i=1,2$, it follows from the induction hypothesis that

[TABLE]

This ends the proof of Theorem 36.

Theorem 37** (i.e. Theorem 24)**

For every term $t\in\mathcal{T}$, for every CE-strategies $S$ and $S^{\prime}$ in the canonical form in $\mathcal{C}^{o}$, we have that

[TABLE]

Proof.

[TABLE]

Proposition 38** (i.e. Proposition 25)**

The following hold.

The set $\mathcal{C}$ of CE-strategies together with the unification and combination operations enjoy the following properties.

1. (a)

The neutral element of the unification and combination is $@\epsilon.\square$. 2. (b)

Every CE-strategy $S$ is idempotent for the unification and combination, i.e. $S\curlywedge S=S$ and $S\curlyvee S=S$. 3. (c)

The unification and combination of CE-strategies are associative. 2. 2.

The unification and combination of CE-strategies is non commutative. 3. 3.

For any CE-strategies $S$ and $S^{\prime}$ in $\mathcal{C}$, and for any term $t$ in $\mathcal{T}$, we have that

[TABLE] 4. 4.

The unification and combination of CE-strategies is a congruence, that is, for any CE-strategies $S_{1},S_{2},S$ in $\mathcal{C}$, we have that:

[TABLE]

Proof. We only prove the last Item. To prove the associativity of the both unification and combination for CE-strategies we rely on the associativity of the unification and combination of elementary CE-strategies (Proposition 7) together with the property of the function $\Psi$ (Theorems 23 and 24).

Let $S_{1},S_{2}$ and $S_{3}$ be CE-strategies in $\mathcal{C}$. It follows from Item iii.) of Lemma 18 that in order to prove that

[TABLE]

it suffices to prove that, for any term $t\in\mathcal{T}$, we have that

[TABLE]

But this follows from an easy computation:

[TABLE]

On the one hand, it follows from Theorem 24 that

[TABLE]

On the other hand, since $S_{1}\equiv S_{2}$, it follows from Item iii.) of Lemma 18 that

[TABLE]

Hence we get

[TABLE]

Again, from Item iii.) of Lemma 18, we get

[TABLE]

The proof of the remaining claims is similar.