Unification and combination of a class of traversal strategies made with pattern matching and fixed-points
Walid Belkhir, Nicolas Ratier, Duy Duc Nguyen, Michel, Lenczner

TL;DR
This paper introduces a formal framework for combining traversal strategies and context insertions in term transformations, demonstrating their algebraic properties and correctness, with applications in deriving asymptotic PDE models.
Contribution
It defines unification and combination operations for traversal strategies, proving their algebraic properties and correctness, advancing formal methods in term transformation techniques.
Findings
Unification and combination operations are associative and congruent.
These operations have neutral elements, forming algebraic structures.
Operations are proven correct for complex term transformations.
Abstract
Motivated by an ongoing project on computer aided derivation of asymptotic models governed by partial differential equations, we introduce a class of term transformations that consists of traversal strategies and insertion of contexts. We define unification and combination operations on this class which amount to merging transformations in order to obtain more complex ones. We show that the unification and combination operations enjoy nice algebraic properties like associativity, congruence and the existence of neutral elements. The main part of this paper is devoted to proving that the unification and combination operations are correct.
| in | ||||||
|---|---|---|---|---|---|---|
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsPolynomial and algebraic computation · Numerical methods for differential equations · Matrix Theory and Algorithms
Unification and combination of a class of traversal strategies made with pattern matching and fixed-points111This work was supported by LABEX ACTION ANR-11-LABX-0001-01 and
by the European Territorial Cooperation Programme INTERREG IV project OSCAR.
Walid Belkhir
Nicolas Ratier
Duy Duc Nguyen
Michel Lenczner
FEMTO-ST Institute, Time and Frequency Department, Univ. Bourgogne Franche-Comté (UBFC), ENSMM, CNRS, 15B avenue des Montboucons, 25030 Besançon cedex, France
Abstract
Motivated by an ongoing project on computer aided derivation of asymptotic models governed by partial differential equations, we introduce a class of term transformations that consists of traversal strategies and insertion of contexts. We define unification and combination operations on this class which amount to merging transformations in order to obtain more complex ones. We show that the unification and combination operations enjoy nice algebraic properties like associativity, congruence and the existence of neutral elements. The main part of this paper is devoted to proving that the unification and combination operations are correct.
keywords:
Traversal strategies , unification , combination , fixed-point , -calculus
1 Introduction
The general context of this article is the incremental design of complex models using a notion of extension. The models we are considering are described by abstract terms and subjected to symbolic transformations. The latter are assumed to rely on two fundamental operations: the operation of extension that transforms a reference object to a more complex one by enriching it, and the operation of combination that merges several extensions to produce a new one that incorporates all the characteristics and effects of those used for its generation. This process is guided by the semantics of the objects in question, namely the way the extensions operate.
We briefly recall the background of this work. Our motivation originates in an undergoing project for the modeling and simulation of complex systems in micro or nano-technologies, e.g. [1, 2, 3]. The systems under consideration are governed by Partial Differential Equations (PDEs) and are too complex to be simulated by straightforward numerical methods, unless at the time-scale of design engineering. In addition, asymptotic methods for PDEs have been an active domain of mathematics for more than seventy years whose main goal is to derive “simpler” PDEs from those which have small parameters in their geometry or their equations. These methods are called singular perturbation methods in physics.
They are developed in all fields where PDEs are used for modeling ranging from physics, biology, finance etc, see for instance the review paper [4].
The use of asymptotic methods for modeling and simulation leads to reduced computation times while retaining the essence of the models. Nevertheless, they suffer from a major drawback which limits their diffusion in the community of engineers which is that their derivation is done on a case by case basis. In other words, for each new problem, the entire process of deriving the model must be redone from scratch even if the new problem has many functionalities in common with one or more problems already modeled. It follows that despite the immense number of existing models, relatively few of them are used in general simulation software.
Our group has adopted an alternative approach by developing a software package called MEMSALab (for MEMS Array Lab) [5] whose function is to build asymptotic models by successive extensions which intend to take into account different characteristics such as scalar or vector forms of solutions, various a priori estimates on the solutions and the sources, thinness or periodicity of geometries, several nested substructures, etc.
Our approach takes advantage of the modularity and the algebraic nature of asymptotic methods by following the approach presented in [6]. It is also based on the so-called combination of extensions [3] method that we are now sketching.
-
First, remember that the construction of an asymptotic model operates on a PDE comprising small parameters. The construction of an asymptotic model consists in passing to the limit to zero on the small parameters which requires several proof steps leading to a new PDE. The latter can be implemented in generic simulation software. Among all pairs of input PDEs and proofs of asymptotic models, the simplest one is chosen, which is the pair of reference PDE and reference proof, from which the others can be constructed by successive complexifications. Technically, a proof is implemented by a rewriting strategy, that is to say by a series of transformations made up of rewriting rules accompanied by strategies which specify the way in which the rewriting rules are applied to PDEs.
-
Second, the reference proof is complexified, we say that it is extended, in several ways to take into account new functionalities giving new proofs. This is done by applying an extension to the reference proof in so far as an extension is another kind of rewriting strategies. This results in an extended proof. Then, applying an extended proof to a complexified PDE yields a new asymptotic model.
-
Finally, to cover several new elementary functionalities, we merge several elementary extensions by an operation of combination. The extension resulting from a combination can itself be applied to the reference proof. It follows a new proof which applied to a complex PDE produces an asymptotic model benefiting from all the characteristics.
To illustrate the concept of combination of extensions, consider the input PDE of reference and the proof of reference both containing the term , an extension that adds an index on the variable of derivation and a second extension which adds an index on the derived function . The application of each of these two extensions to the reference term yields the terms and , respectively. The combination of these two extensions would be another extension that, when applied to the reference term, yields .
In summary, there are three levels for PDEs, proofs and extensions. A proof can be applied to a PDE, an extension to a proof, and extensions can be combined to produce new extensions. Therefore, combining extensions related to several elementary features allows for building, in an incremental way, new proofs and therefore new asymptotic models.
Although the concepts of extension and combination were introduced for the first time in [1], in that earlier work the combination of extensions was done by composition, not allowing for conflicts between extensions. A conflict between two extensions arises when they modify the same part of a proof and when the application of one of them creates new possibilities for the application of the other one. In that restricted framework, the combination of non conflicting extensions simply amounts to their composition. The complete principle of the extension-combination method was introduced in [3] where a user language was defined for specifying proofs and extensions as rewriting strategies. We also have defined the combination on a small class of extensions. However, the question of the correctness of the combination formulas was left open.
When defining a new class of strategies with an operation of combination, there are many difficulties to overcome. A careful attention must be payed to the choice of the constructors out of which these strategies are built up. There are two extreme ways to proceed. One way is to build the strategies by means of the most rudimentary constructors, as in [7]. This makes the strategies hard to use in practice due to their huge size. But the advantage of such rudimentary constructors is to allow one to understand the mechanisms behind the combination operation and to define it correctly. Even more, to proceed in this way was inevitable and justifies our work [7].
The other extreme way is to rather design high level strategy constructors which are easy to use in practice. But this makes it hard to understand the mechanisms behind the combination operation since a high level constructor hides several rudimentary constructors. For instance, given a rule , the translation of the high level strategy into rudimentary constructors requires three rudimentary constructors since can be written as , where “” stands for the fixed-point or the recursion constructor, “” stands for the left-choice constructor, and “” is the one-step constructor that accesses to all the children of a term if viewed as a tree. In this case, one has to define the combination of two high level constructors in just one step which is usually difficult or even impossible. Furthermore, this raises the question of the closure of such class of strategies under combination since, for instance, the combination of two s is not an . In earlier attempts, we figured out that the combination of extensions based on high-level strategies such as BottomUp or TopDown or OuterMost can not be expressed with high-level strategies, making such a class not closed under combination. We thus understood that more rudimentary strategy constructors were needed.
In [7] we followed the first way and introduced the large class of context embedding strategies, or CE-strategies for short, that involves elementary and, more importantly, an explicit handling of failures which are produced when an application of an extension fails.
We proved the correctness of the combination operation for a fragment of the class of CE-strategies. The drawback of working with this class is that the definition of the traversal navigation strategies such as OuterMost yields a CE-strategy whose size depends on the signature. Even worse, the size of the resulting combined CE-strategy can be exponential with respect to the size of the two input CE-strategies. In this paper we overcome these difficulties by pursing a third way which is in between the two extreme ways exposed above. We introduce another class of strategies, called the -strategies, which is built up using both high level and rudimentary constructors inspired by the propositional modal -calculus [8, 9] rather than strategy languages as in [10]. The -calculus-like approach involves natural and rudimentary strategy constructors, especially the jumping to a position and the recursion with the fixed-point operator. This makes tractable the question of language closure for combinations. Moreover, the procedure of combination of -strategies together with their verification is also much simplified. Although this new class of -strategies is less expressive that the class of CE-strategies of [7], the new class remains powerful enough to be used in practice and its closure is harder to achieve since it incorporates high level and rudimentary constructors, this makes this paper more complete than [7], since the CE-strategies of [7] can not be used in practice because of their huge size. Besides, we define a unification and combination operations for the class of -strategies. Roughly speaking, the unification of two -strategies amounts to construct a -strategy that captures the effect of both insofar as they are compatible, where the compatibility of two -strategies depends on each input term and is related to their successful application. The incompatible effects are covered by the combination. This class enjoys similar algebraic properties as CE-strategies with respect to unification and combination, like associativity, congruence and the existence of a neutral and an absorbing element. The main result of this paper shows that the unification and combination operations of -strategies are correct with respect to a correctness criterion that we shall devise and that is guided by the semantics of -strategies, Subsection 5.1.
We notice that the size of the resulting combined -strategy is polynomial with respect of the size of the two input -strategies. The -strategies are reasonably easy to use in practice and they have been implemented and used in MEMSALab software in the previous years within a user specification language of mathematical expressions, proofs and extensions and their combination for asymptotic models where the first applications targeted micro and nanotechnology [1, 2, 3].
The concept of extension, sometimes called refinement in the literature, is developed in different contexts such as the parallel and concurrent systems, for example in [11, 12, 13] 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 that consists of the merging of structures or algorithms motivated mainly by the incremental design of complex systems by integration of simple and heterogeneous subsystems. For instance, the works in combination of logics [14, 15], algorithms and verification methods [16], decision procedures [17], the composition and synthesis for service-oriented and agent-oriented computing [18, 19] in which the synchronous and asynchronous product of automata and transition systems are a form of combination, and the unification of grammars in linguistics [20, 21, 22, 23, 24]. However, the integration of the two concepts of extension and combination seems to have not been addressed in the literature.
Organization of the paper.
The paper is organized as follows.
Section 2 is devoted to a review of the useful concepts of rewriting theory, and to definitions and notations.
In Section 3 we introduce the position-based -strategies and their combination.
In Section 4 we introduce the larger class of -strategies together with their semantics.
In Section 5 we give the unification procedure.
In Section 6 we state the results of this paper without proof, namely the correctness of the unification and combination and their algebraic properties.
In Section 7 we expose a detailed outline of the proof of the main result, that is, the correctness of the unification of -strategies.
In Section 8 we construct a mapping that is needed in the formulation of the correctness criterion of the unification and combination of -strategies.
In Section 9 we prove the correctness of the unification of the fixed-point free fragment of -strategies, that is, the -strategies without the fixed-point constructor.
In Sections 10, 11 and 12 we develop the notions and tools as well as the intermediary results required in the proof of the main result. This is the technical core of the paper.
In Section 13 we sum up the results of the previous three sections and prove the correctness of the unification and combination for the full class of -strategies, from which we prove the important algebraic properties of the unification and combination.
In Section 14 we give a summary, few concluding remarks and we announce future work.
To improve the readability of the paper, some proofs are given in the Appendix.
Contents
-
5.1 A correctness criterion for the extension of the unification and combination to -strategies
-
6.1 Correctness of the unification and combination procedures
-
8 From -strategies to position-based -strategies: the definition of the mapping
-
9 Proof of the correctness of the unification of -strategies: the fixed-point free setting
-
10 Properties of the unification reduction system and of -strategies
-
10.1 Measures of -strategies: the star height and the depth of -strategies
-
10.2 Termination and confluence of the unification reduction system
-
10.3 Iteration mapping and (generalized) unfolding of -strategies
-
11.1 The equivalence between the unification of several unfoldings of two -strategies
-
11.4 Relating the structure of the unification of two -strategies with that of their unfolding
-
12 The equivalence between the unification of two -strategies and that of their unfoldings
-
12.3 The unification of two -strategies is equivalent to the unification of their unfolding
-
13.2 The algebraic properties of the unification and combination
2 Preliminaries: terms, substitution, notations, rewriting
We introduce preliminary definitions and notations.
Terms, contexts
Let be a set of symbols called function symbols. The arity of a symbol in is and is denoted . Elements of arity zero are called constants and often denoted by the letters etc. The set of constants is always assumed to be not empty. Given a denumerable set of variable symbols, the set of terms is the smallest set containing and such that is in whenever and for . Let be an extra variable, the set of contexts, denoted simply by , is made with terms with symbols in which always includes exactly one occurence of . Evidently, and are two disjoint sets. For a term and a context , we shall write for the term that results from the replacement of by in . We shall write simply (resp. ) instead of (resp. ). We denote by the set of variables occurring in . We shall write to mean the arity of of the symbol at the root of .
Positions, prefix-order, substitution
Let be a term in . The position is called the root position of , and the function or variable symbol at this position is called the root symbol of . A position in a tree is a sequence of integers, i.e., an element in . In particular we shall write for , such positions are called unitary positions. Given two positions and , the concatenation of and , denoted by , is the position . We notice that in the examples, when we write, for instance, the position , we mean the concatenation of and , and not the twelfth position.
The set of positions of the term , denoted by , is a set of positions of positive integers such that, if is a variable or is a constant, then . If then .
The prefix order defined as iff there exists such that , is a partial order on positions. If then we obtain the strict order . We write iff and are incomparable with respect to . The binary relations and 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 we denote by the subterm of at position , that is, , and . For a term , we shall denote by the depth of , defined by , if is a variable or a constant, and , for . For any position we denote by the term obtained by replacing the subterm of at position by : and .
A substitution is a mapping such that for only finitely many ’s. The finite set of variables that does not map to themselves is called the domain of : . If then we write as: .
A substitution uniquely extends to an endomorphism defined by: for all , for all , and for . In what follows we do not distinguish between a substitution and its extension.
For two terms , we say that matches , written , iff there exists a substitution , such that . It turns out that if such a substitution exists, then it is unique. A substitution is subsumed by a substitution iff matches for any term .
A most general unifier of the two terms and is a substitution such that and, for any other substitution satisfying , we have that is subsumed by . The most general unifier is unique up to a variable renaming.
The composition of functions will be denoted by “”. The set of all subsets of a set will be denoted by . For a finite set , we write for the number of elements of . For a finite set of integers, the maximum (resp. minimum) of will be denoted by (resp. ).
Lexicographic ordering
A lexicographic ordering, denoted by ””, on the Cartesian product (-times), where , is inductively defined for any and in such that iff either , and in this case . Or , and in this case either i.) or ii.) and .
3 Position-based -strategies and their combination
The operation of combining -strategies requires an abstract operation of merging contexts, a concrete example of which will be provided. The algebraic properties of the combination will be presented in the general case.
Definition 1** (Merging of contexts)**
Any associative binary operation
[TABLE]
is called merging of contexts.
Example 2** (Merging of contexts by composition)**
We give an example of the operation of merging of contexts, denoted by ”\mathbin{\vbox{\hbox{{\bullet}}}}”, as follows:
[TABLE]
where is the position of in . This kind of merging has been introduced in [25] and implemented in MEMSALab software. For instance, the merging of the two contexts and , used for inserting indices to mathematical variables or functions, is given by
[TABLE]
where and are terms.
To define the position-based -strategies, we introduce two particular position-based strategies as follows. Firstly, for a position and a context , we define the jump strategy that, when applied to a term , it inserts at the position of . Secondly, we define the failing strategy that fails when applied to any term. Their precise semantics are given in Definition 5 of the semantics of position-based -strategies.
Definition 3** (Position-based -strategies)**
Let be positions in and be contexts in with . A position-based -strategy is either the failing strategy or the ordered conjunction
[TABLE]
*The set of position-based -strategies is denoted by . *
Notice that the order of positions in matters. We impose that the position-based -strategies follow some constraints regarding the positions of insertions to avoid conflicts: the order of context insertions must go up from the leaves to the root. Formally,
Definition 4** (Well-founded position-based -strategy)**
Let positions in and be contexts in with . A position-based -strategy
[TABLE]
is well-founded iff
- i.)
every position occurs at most once in , i.e. for all , and 2. ii.)
lower positions appear earlier in , i.e. if , for all .
Moreover, the position-based -strategy is well-founded.
In all what follows we work only with the set of well-founded position-based -strategies, still denoted by . For two position-based -strategies and , we shall abuse of notation and write to mean that they are equal up to a permutation of their parallel positions. For a position , we let
[TABLE]
We next define the semantics of a position-based -strategy as a function in , with the idea that if the application of a position-based -strategy to a term fails, the result is . Besides, we adopt a stronger version of failure, that is, fails when each of fails. To formalize this notion of failure we need to introduce an intermediary function
[TABLE]
that stands for the fail as identity. It is defined for any function in and any term by
[TABLE]
The semantics of position-based -strategies follows.
Definition 5** (Semantics of position-based -strategies)**
The semantics of a position-based -strategy is a function in inductively defined by:
[TABLE]
Two -strategies and are said to be semantically equivalent, if and only if , for any term .
Notice that two position-based -strategies are semantically equivalent iff they are equal up to a renaming of parallel positions.
Example 6
We illustrate with an example of position-based -strategies with their application to a term in MEMSALab. Consider the two contexts and . Applying the position-based -strategy to the term gives the transformation of a space variable defined on a domain to its coordinate . The procedure is given by
[TABLE]
Let \tau=\tau_{1}\mathbin{\vbox{\hbox{{\bullet}}}}\tau_{2}, where ”\mathbin{\vbox{\hbox{{\bullet}}}}” stands for the operation of merging of contexts by composition as defined in Example 1. The application of the position-based -strategy to the term gives
[TABLE]
Example 7
We illustrate an application of a position-based -strategy on the derivative of a function represented by the term , where is the derived function, is the the mathematical variable and the derivation operator with respect to . Let and be contexts. The application of the position-based -strategy to yields the term . Since the positions and are parallel, this -strategy is well-founded and its application to yields
[TABLE]
The tree structures of , , and are depicted in Figure 1.
The unification of two position-based -strategies amounts to sort and merge their positions, and to merge their contexts if they are inserted at the same position. To simplify the following Definition 8, when unifying position-based -strategies and in the general case (2), we can assume without loss of generality that each of them contains an insertion at the root position , because otherwise one can add to each of them the identity insertion that leaves unchanged any term to which it is applied.
Definition 8** (Unification of position-based -strategies)**
The unification of two position-based -strategies is the binary operation defined as
-
-
(a)
** 2. (b)
** 2. 2.
If and , for two partially ordered sets and of positions, then
[TABLE]
where
[TABLE]
Notice that since one can reorder the positions of , then the unification of two well-founded position-bases -strategies can be turned into an equivalent well-founded one, i.e. into a unique (up to a permutation of parallel positions) well-founded position-based -strategy.
Example 9
Consider position-based -strategies
[TABLE]
and the sets of their positions are and , respectively. Hence and . The unification of and is
[TABLE]
For practical reasons, we need to introduce the combination of two position-based -strategies in the same way as their unification apart that the combination of a position-based -strategy with the failure is the identity.
Definition 10** (Combination of two position-based -strategies)**
*The combination of two position-based -strategies is a binary operation defined for any and in by *
[TABLE]
The algebraic properties of the unification and the combination of position-based -strategies are stated in the following Propositions 11 and 12, respectively.
Proposition 11
The set of position-based -strategies together with the unification operation enjoy the following properties.
The neutral element of the unification is , 2. 2.
The absorbing element of the unification is , 3. 3.
The unification is associative, i.e. . 4. 4.
The unification of position-based -strategies is (non-)commutative if and only if the operation ”\mathbin{\vbox{\hbox{{\bullet}}}}” of merging of contexts is (non-)commutative. 5. 5.
The unification is idempotent if and only if the operation of merging of the contexts is idempotent, that is, for any iff \tau\mathbin{\vbox{\hbox{{\bullet}}}}\tau=\tau for any contexts in .
Proposition 12
The set of position-based -strategies together with the unification and combination operations enjoy the following properties.
The neutral element of the combination is . 2. 2.
The combination is associative, i.e. . 3. 3.
The combination of position-based -strategies is (non-)commutative if and only if the operation of merging of the contexts ”\mathbin{\vbox{\hbox{{\bullet}}}}” is (non-)commutative. 4. 4.
The combination is idempotent iff the operation ”\mathbin{\vbox{\hbox{{\bullet}}}}*” of merging of contexts is idempotent. *
The proof of these propositions does not provide any difficulties since the properties of associativity, (non)-commutativity, and idempotence of the unification and combination are inherited from their counterpart properties of the merging of contexts.
4 The class of -strategies
As far as the unification is concerned, designing a class of strategies faces the following challenging issues: 1.) finding the right class of extensions that is closed by combination: a less expressive class would not be closed under combination nor useful in practice, while very expressive extensions are impossible to combine, 2.) finding the right basic constructors of the extensions: very rudimentary constructors would make the size of the extensions very huge and non-practical, while more general constructors are very hard to combine, 3.) combining the ”while” loops, or iterations, is the most difficult part and requires a special care, 4.) proving the correctness of the combination by taking into account the semantics of the extensions.
We introduced the position-based -strategies to clarify the ideas behind contexts, their insertion as well as their combination. However, position-based -strategies are not satisfactory for practical applications, since the positions are generally not flexible, not accessible and cannot be used on a regular basis in applications. So, we enrich this framework by supplementing position-based -strategies with navigation strategies to form a class of -strategies which is closed under combination.
Syntax and semantics of -strategies
A -strategy is composed of two parts: a navigation of the input term without changing it, and an insertion of contexts at certain positions. The navigation part is built up using the left-choice constructor (), a conditional constructor “”, a pattern-matching “” with a pattern , the constructor that applies to all the children of the input term, the jump constructor to a position as well as a conjunction of such jumps, and the fixed-point constructor (“”) allowing the recursion in the definition of strategies. The resulting class is called the class of -strategies, which stands for traversal strategies with fixed-points.
In what follows we assume that there is an enumerable set of fixed-point variables denoted by . Fixed-point variables in will be denoted by
Definition 13** (Grammar of -strategies)**
The class of -strategies is defined by the following grammar:
[TABLE]
where is a fixed-point variable in , and is a context in , and is a term in , and are unitary positions in . The set of -strategies will be denoted by . The subset of fixed-point free -strategies will be denoted by .
Notations
We shall write ”” instead of \mathtt{\mathbf{If}}\,{S_{1}}\,\mathtt{\mathbf{Then}}\,{\big{(}\mathtt{\mathbf{If}}\,{S_{2}}\,\mathtt{\mathbf{Then}}\,{S}\big{)}}. If a set of positions is empty, then the -strategy is just the failure .
We notice that extending the class of -strategies by allowing the position of the jump constructor to range over arbitrary positions in instead of unitary positions in does not increase the expressiveness of the strategy language. This can be achieved by turning each -strategies , where is a position in into , with and each is a unitary position in .
The design of the class of -strategies is inspired by the -calculus formalism [8] 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 ( and ) of the propositional modal -calculus. And the fixed-point constructor is much finer than the iterate operator of e.g. [10]. Besides, we incorporate the left-choice strategy constructor and a pattern matching operation.
An occurence of a fixed-point variable is bound in a -strategy if it is under the scope of a ””. Otherwise, it is said free. The set of bound variables of will be denoted by . A -strategy is closed if all its fixed-point variables are bound. We shall sometimes write to emphasize that the fixed-point variable is free in .
Example 14
We informally illustrate the semantics of -strategies through an example. Consider the -strategy defined by and its iteration , where is a term and is a context. When applied to a term , the -strategy checks first whether matches with . If it is the case, then the context is inserted at the root of and stops, yielding the term . Otherwise, the -strategy jumps to the position of , i.e. the left-most child of , and reiterates the procedure by applying to this child. If it reaches the left-most leaf of with which does not match, then the -strategy fails on . For instance, the application of to the term gives , while it fails on .
Remark 15
Notice that a -strategy is composed of two parts: i.) a navigation part that consists of the navigation strategies that browse the input term without changing it. These strategies are the pattern matching, the left-choice, the iteration, the jump, the conjunction, the , and the “”. And, ii.) an insertion part that modifies the input term and consists of an insertion of contexts.
Definition 16** (Unfolding)**
*For any -strategy , and , we define the unfolding of which replaces the fixed-point operator on by -iterations as follows *
[TABLE]
Example 17** (Unfolding)**
For a pattern and a context , let
[TABLE]
be a -strategy. We give examples of the replacement of the fixed-point operator of by -iterations, for , as follow:
[TABLE]
The formal definition of the semantics of -strategies follows.
Definition 18** (Semantics of -strategies)**
*The semantics of a closed -strategy is the function , which is defined inductively as follows. *
[TABLE]
We shall refer to as the application of to .
Notice that when the application of or of fails, it does not return the input term untouched (i.e. it does not behave as the identity), but fails as well. The reason is that we want a fine semantics that distinguishes between the identity that operates successfully and returns the input term (e.g. ), and the failure that indicates that the -strategy was not applied, which may launch other -strategies. Notice also that fails if and only if each fails, and not just one of them fails. This is important because we want to make the semantics of compatible with that of in terms of failure, that is why we expressed the latter in terms of the former, and the only reason for that is to be able to unify with , see Section 5, and remaining in the same framework of -strategies. Otherwise, a richer semantics in terms of handling the failure requires the framework [7] in which the failures are handled explicitly in the formalism, making it impractical.
The general definition of the semantics of the fixed-point constructor requires an unnecessary machinery involving Knaster-Tarski fixed-point theorem [26] and complete lattices. However, due to the particular nature of -strategies, we gave an adhoc definition of the fixed-point -strategy by , which is the same as that given by the least-fixed point. The justification of the iteration of at most times, the depth of , is that the navigation part of a -strategy does not change the input term , see Remark 15 and Example 19. Therefore, either the -strategy progresses on the term and will reach the leaves of after at most iterations, or does not progress and in this case it fails after any iteration. Examples of -strategies that do not progress are and for a term . Technically, we show in Corollary 70 that, for every term , the -strategy is a fixed-point of in the sense that . Notice that any -strategy of the form , in which occures twice, can be turned into the equivalent -strategy in which occurs once. This equivalence can be proved by induction on , and more generaly it holds for any -calculus [8].
Example 19** (Semantics of -strategies)**
We give two examples of -strategies and their semantics. Let be contexts in , and let and be terms in , where are constants, and is a rewriting variable.
Consider the -strategy
[TABLE]
The -strategy checks whether the constant matches with an input term , if it does then is inserted at the root of (i.e. ) yielding , otherwise it jumps to the position of and iterates the same operation. We next illustrate the application of to . Since the depth of is , we need to compute , as we did for a similar -strategy in Example 17, thus we get:
[TABLE]
Hence the application of to yields
[TABLE] 2. 2.
Consider the -strategy
[TABLE]
The -strategy expects a term of the form , then it inserts on its first child (i.e. ), and inserts on its second child (i.e. ), then jumps to the third child (i.e. ) and iterates the same operation. Hence the application of to the term , which has depth , yields
[TABLE]
hence
[TABLE]
Summing up, we get
[TABLE]
In the following example we show how to encode the two standard traversal strategies and in our formalism using the fixed-point constructor.
Example 20
In what follows we assume that is a -strategy. We recall that, when applied to a term , the -strategy tries to apply to the maximum of the sub-terms of starting from the root of , it stops when it is successfully applied. And when applied to a term , the -strategy tries to apply to the maximum of the sub-terms of starting from the leaves of , it stops when it is successfully applied. Hence,
[TABLE]
Definition 21
Let be -strategies and an integer. We shall write
- i)
* iff . In this case, and are called equivalent.* 2. ii)
* iff for any term of depth . In this case, and are called -equivalent.*
Notice that ”” is an equivalence relation and that and are equivalent iff they are -equivalent for any .
5 Unification and combination of -strategies
The problem now is to extend the operations of unification and combination of position-based -strategies (i.e. Definitions 8 and 10) to the larger class of -strategies. These two extensions must fulfill a correctness criterion that will be devised in Subsection 5.1. The subsequent subsections are devoted to the definition of the extension of unification (Definition 34) and the extension of the combination (Definition 35). Then we give an example of unification of -strategies and comment it.
5.1 A correctness criterion for the extension of the unification and combination to -strategies
Since there are many ways to define an extension of the unification operation from position-based -strategies (i.e. the class ) to -strategies (i.e. the class ), one needs a criterion that both guides the elaboration of a definition and ensures its correctness. Such a criterion should impose a compatibility between the unification operation upon and its extension to the larger class , in the sense that the former operation should stand as the basis for the latter.
For this purpose, out of a term in and a -strategy in , we shall construct a unique (up to a permutation of parallel positions) position-based -strategy in . That is, we shall define a mapping
[TABLE]
that associates to any term in and any closed -strategy in , a position-based -strategy in , denoted simply by , such that the semantic equivalence is preserved in the following sense:
[TABLE]
Since the mapping takes into account the semantics, then the correctness criterion is nothing but the compatibility between the unification upon and its extension to , i.e. for any term , the following two operations yield the same result:
- i.)
the unification of two -strategies in , followed by the mapping of the result to by , and 2. ii.)
the mapping of each of these two -strategies to by , followed by the unification of the resulting position-based -strategies.
This natural correctness criterion will be formalized in Definition 22 for both the unification and combination. However, to simplify the exposition we shall not define the mapping here but in Definition 46 of Section 8, since the statement of the main results does not require this definition. Furthermore, we shall show in Lemma 48 of Section 8 that the thus defined preserves the semantic equivalence in the sense of Eq.(1).
Definition 22** (Correctness criterion for the extension of and )**
An extension of the unification is correct, if and only if, for every term and for every -strategies and in , we have that
[TABLE]
Similarly, an extension of the combination is correct, if and only if, for every term and for every -strategies and in , we have that
[TABLE]
That is, the following diagrams commute.
[TABLE]
5.2 Sub--strategies, memory and pre--strategies
Since the unification of -strategies will be defined by induction, we need to define the notion of the set of sub--strategies of a given -strategy. With a slight modification allowing to be in the set of such sub--strategies of , we also define the set of augmented sub--strategies.
Definition 23** (Sub--strategies of a -strategy)**
Given a -strategy , we inductively define the finite set of sub--strategies of , denoted by , as well as the finite set of augmented sub--strategies of , denoted by , which are similar apart for the fixed-point -strategies:
[TABLE]
A -strategy is said to be a sub--strategy of if is in .
Similarly, the set of all fixed-point sub--strategies of , denoted by , as well as the set of all augmented fixed-point sub--strategies of , denoted by , are defined similarly apart for the fixed-point -strategies:
[TABLE]
Clearly, and and . Notice that if is fixed-point free, then and . Indeed, the set of augmented sub--strategies is finite and this can be easily shown by induction on . We illustrate the Definition 23 with the following example.
Example 24** (Of , , and )**
For a given pattern and a context , let
[TABLE]
be a -strategy. Hence the sets , , and are easily computed as follows:
[TABLE]
and
[TABLE]
In the Example 24 above we have that , but this is not true in general as shown in the following remark.
Remark 25
The inclusion is strict in general, that is, there is a -strategy such that . This is achieved by taking a -strategy of the form:
[TABLE]
and noticing that the -strategy is neither in nor in , but in and in .
The unification of two -strategies will be given by means of a reduction system that requires storing a piece of information, called memory, related to the input -strategies. Roughly speaking, a memory is a set of triples where the first and the second element of each triple is a fixed-point sub--strategy or an augmented -strategy, and the third element is a fixed-point variable. The idea behind the memory is that the unification of a fixed-point -strategy with a -strategy amounts to the unification of with , or more precisely, the unification of with produces a -strategy , where is a fresh-fixed point variable and is the unification of with . To ensure that this process terminates we need to store the triple in the memory so that is produced whenever is unified again with .
The formal definition of the memory follows.
Definition 26** (Memory)**
Given an enumerable set of fixed-point variables, as well as two -strategies and , we define the set of all memories related to and with respect to , denoted by or simply by , as the following set of sets of triples:
[TABLE]
More generally, the set of all memories, denoted by , is defined by
[TABLE]
*An element in or in is called a memory. *
An example of a memory related to two -strategies follows.
Example 27** (Memory)**
For given patterns and contexts , let
[TABLE]
be -strategies. From Example 24 above we have that
[TABLE]
Given , we give an example of a memory related to and and , i.e. \mathcal{M}\in\mathfrak{M}_{\mathcal{Z}}\big{(}\mu X.S(X),\mu X^{\prime}.S^{\prime}(X^{\prime})\big{)}.
[TABLE]
From now on we let to be an enumerable set of fixed-point variables. Since the unification reduction system will handle two -strategies together with a memory, this new object is called a Pre--strategy and defined next.
Definition 28** (Pre--strategies)**
The class of pre--strategies is defined by the following grammar:
[TABLE]
where are -strategies in , is a memory in , is a fixed-point variable in , is a term in and are unitary positions in . The set of pre--strategies will be denoted by .
Like in the modal -calculus, it is easier and convenient to work with -strategies that make progress when applied to a term. Making progress is guaranteed by a syntactic requirement, called monotonicity, that imposes that in each fixed-point sub--strategy there is at least a position jump or a from the root of to .
Definition 29** (Monotonicity of -strategies)**
A -strategy is monotonic if for any , there exist -strategies and each of which is a sub--strategy of such that is either of the form where , or of the form .
For instance, the -strategy \mu X.\big{(}(u;@\varepsilon.\tau)\[email protected]\big{)} (resp. \mu X.\big{(}(u;@\varepsilon.\tau)\oplus\mathtt{Most}(X)\big{)}) is monotonic since there the jump ”” (resp. ””) between and . While \mu X.\big{(}(u;@\varepsilon.\tau)\oplus X\big{)} is not monotonic.
We generalize next the condition of well-foundedness from position-based -strategies to -strategies.
Definition 30** (Well-founded -strategies.)**
A -strategy is well-founded iff every position-based -strategy that is a sub--strategy of is well-founded in the sense of Definition 4.
5.3 The procedure of unification of -strategies
From now on we shall abuse of language and refer to the extension of the unification operation from position-based -strategies to -strategies, as simply the unification of -strategies. Before giving the procedure of unification of -strategies, we need the following assumptions on the structure of -strategies.
Assumptions 31
Throughout this paper, each -strategy is well-founded, monotonic, closed, and in which each fixed-point variable appears once, and each of their sub--strategies which is of the form or , is preceded by a pattern-matching, i.e. and .
These assumptions do not exclude interesting cases, since either they exclude cases which do not make sense (e.g. a -strategy with free fixed-point variables, or not well-founded), or they make the -strategies easier to handle in the proofs without missing interesting cases, for instance, imposing that each fixed-point variable appears once is not a restriction since each -strategy can be turned into a -strategy with such a property by applying the following simplification operations which preserve the semantic equivalence (i.e. a -strategy is semantically equivalent to its simplification).
Simplifications 32
The simplification operations of -strategies consists of:
- (i)
renaming identical bound variables, for instance can be turned into , this is known in the literature as the -conversion, and 2. (ii)
renaming identical occurrences of variables if they are bound to the same fixed-point operator, for instance if is a -strategy in which appears twice, then we can turn into the equivalent -strategy , and 3. (iii)
removing useless contractors, i.e. turning into when does not appear in .
We define next the procedure of unification of -strategies by means of a reduction system that operates on pre--strategies, in which the pattern related to the position in -strategy will be denoted by , or simply by when is known.
Definition 33
We define the reduction system operating on pre--strategies and consisting of the following reduction rules with a decreasing order of priority.
-
-
(a)
** 2. (b)
** 2. 2.
\langle{@\varepsilon.{\tau},@\varepsilon.{\tau}^{\prime},\mathcal{M}}\rangle\;\;\rightarrow\;\;@\varepsilon.({\tau}\mathbin{\vbox{\hbox{{\bullet}}}}{\tau}^{\prime}).* * 3. 3.
- (a)
** 2. (b)
** 4. 4.
- (a)
. 2. (b)
*If and then *
[TABLE]
where
[TABLE] 5. 5.
- (a)
** 2. (b)
** 6. 6.
- (a)
. 2. (b)
. 7. 7.
- (a)
\langle{\mathtt{Most}(S),\mathtt{Most}(S^{\prime}),\mathcal{M}}\rangle\;\;\rightarrow\;\;\mathtt{\mathbf{If}}{\big{(}\mathtt{Most}(S)\&\mathtt{Most}(S^{\prime})\big{)}}\mathtt{\mathbf{Then}}\,\mathtt{Most}\big{(}\langle{S,S^{\prime},\mathcal{M}}\rangle\oplus S\oplus S^{\prime}\big{)}. 2. (b)
** 3. (c)
** 8. 8.
- (a)
[TABLE] 2. (b)
[TABLE]
Explanation of the rules
Notice that, by construction, for any tuple produced by the unification reduction system , the memory is redundancy free, that is, if and are in , then . We comment on the key points in Definition 33.
Pattern matching:
If we omit the memory in the rule 3a for sake of simplicity, then the unification of with is naturally , where is the unification of with , since we want that the pattern proceeds the merging of and .
:
For the unification of two s (i.e. rule 7a), we first recall the semantics of this constructor. When a -strategy is applied to term , the -strategy is applied to each of its children. In particular, fails on if and only if fails on each of ’s children. Otherwise, when succeeds on , then behaves as the identity on the children of on which it fails, see Definition 18. While unifying two -strategies and we need to distinguish two cases. (i) If one of these -strategies fails, then the result should fail. This is achieved by the condition \mathtt{\mathbf{If}}{\big{(}\mathtt{Most}(S)\&\mathtt{Most}(S^{\prime})\big{)}} in the resulting -strategy. (ii) If both of them do not fail when applied to a term the we need to consider whether each of them fails or not on each child of . In order to explain the \mathtt{Most}\big{(}\langle{S,S^{\prime},\mathcal{M}}\rangle\oplus S\oplus S^{\prime}\big{)} part in the resulting unified -strategy, let be a child of , and consider the four cases:
- (ii.1)
if both of and succeeds on , then we need to consider their unification. This explains the part. 2. (ii.2)
If both of them fails on , then their unification should fail on as well. But this holds since fails as well. 3. (ii.3)
If succeeds on while fails on it, then the resulting unified -strategy should apply to . But this is achieved by which is equal to since fails on . 4. (ii.4)
If fails on while succeeds on it, then this case is symmetric to the previous one.
The unification of with a conjunction of position jumps requires that we encode into a conjunction of position jumps as well.
Fixed-points:
The idea behind the unification of with (i.e. rule 8a) is to unfold to and then to unify with . Indeed this process is terminating thanks to the use of memory since we memorized that we passed through the unification of with and we generated a fresh fixed-point variable , this is done by adding the tuple to the memory. Thanks to the memory, the next time we face the unification of with , we shall produce .
We shall show in Subsection 10.2 that the unification system is terminating and confluent. This allows us to define the unification operation in terms of the normal form with respect to . The normal form of will be denoted by . The definition of the unification and combination of -strategies follow. We emphasize that throughout this paper, as far as we are dealing with the unification and combination, we assume that the two sets of the fixed-point variables of the two input -strategies are disjoint.
Definition 34** (Unification of -strategies)**
*The unification of -strategies is the binary operation
, defined for any and in by*
[TABLE]
Notice that the unification of two -strategies yields a -strategy that captures the effect of both insofar as they are compatible, where the compatibility of two -strategies depends on each input term and is related to their successful application. That is, if and can be applied successfully to a term , then the application of their unification on succeeds as well and reproduces the effect that and being applied simultaneously. However, the incompatible effects are covered by the combination in the sense that if fails on a term , then or fails, and the combination returns the non-failing one, if any. This justifies the following definition of the combination.
Definition 35** (Combination of -strategies)**
*The combination of -strategies is the binary operation
, defined for any and in by*
[TABLE]
Example 36** (Unification of -strategies)**
We give an example of the unification of two fixed-point -strategies. For given patterns and contexts , let
[TABLE]
*be -strategies. We compute the unification which is the normal form of the tuple
by applying the reduction rules of given in Definition 33. Let*
[TABLE]
Summing up, the unification of and is:
[TABLE]
Notice that the fixed-point variable does not appear in the resulting -strategy and therefore ”” can be removed. The application of the resulting -strategy to a term features four cases.
- i.)
Either both and match with , and in this case the context {\tau}^{\prime}\mathbin{\vbox{\hbox{{\bullet}}}}{\tau} is inserted at the root of . 2. ii.)
Or only matches with , and in this case is inserted at the position of provided the -strategy is applied successfully at the position of . 3. iii.)
Or only matches with , and in this case is inserted at the position of provided the -strategy is applied successfully at the position of . 4. iv.)
Or both and are applied at the position of .
The unification of two -strategies in which each fixed-point variable appears once may yields a -strategy in which a variable appears many times or does not appear at all, e.g. the in the Example 36. An attention will be payed to this issue since this assumption on the occurrences of fixed-point variables is not preserved by unification. However, other assumptions listed in Assumptions 31 are preserved. Namely, it is easy to show that the unification of two well-founded -strategies is a well-founded one. And we shall show later that the unification of two monotonic -strategies is a monotonic one as well.
6 Statement of the results
In this section we state the main results of this paper, that is, the correctness of the procedure of unification and combination stated in Subsection 6.1, and the algebraic properties of the unification and combination of -strategies stated in Subsection 6.2. The proofs of these results can be found in Section 13.
6.1 Correctness of the unification and combination procedures
Theorem 37** (Correctness of the unification)**
The unification of -strategies is correct. That is, for every term and for every -strategies and in , we have that
[TABLE]
Theorem 38** (Correctness of the combination)**
The combination of -strategies is correct. That is, for every term and for every -strategies and in , we have that
[TABLE]
6.2 Algebraic properties of the unification and combination
The existence of the neutral elements and the associativity property of the unification and combination are obvious for the sub-class of position-based -strategies but they are far from being so for the larger class of -strategies, and it is crucial and useful to have them. Namely, a user of -strategies needs know the algebraic properties of the structure he handles. For instance, he needs combine many -strategies, and thus needs to know if this combination is associative and/or commutative. Besides, the properties of the neutral and absorbing elements allow one to simplify -strategies.
We notice that the neutral elements and the associativity property of the unification and combination must be understood at the semantic level and not at the syntactic level since there are -strategies which are syntactically different but semantically equivalent. For instance, the -strategies and and , where are variables, are all equivalent. More generally, the algebraic properties of the unification and combination will be formulated in terms of equivalence classes of -strategies (with respect to the semantic equivalence relation) rather than syntactic -strategies.
Technically speaking, since the semantic equiavalence ”” (Definition 21) is an equivalence relation, we shall use the standard notation for the equivalence class of the -strategy , i.e. , and the notation for the quotient set of by ””, i.e. . Moreover, the unification and combination of the equivalence classes of -strategies in can be defined in a natural way as:
[TABLE]
We notice that these two operations are well defined since they are a congruence by Theorems 41 and 42. The algebraic properties of the unification of -strategies follow. In fact, the unification of -strategies inherits the properties of associativity, (non-)commutativity and idempotence from the position-based -strategies and the merging of contexts.
Theorem 39
The quotient set of -strategies together with the unification operation enjoy the following properties.
The neutral element of the unification upon is . 2. 2.
The absorbing element of the unification is . 3. 3.
The unification of -strategies is associative, i.e. , for any . 4. 4.
The unification of -strategies is (non-)commutative if and only if the operation of merging of contexts ”\mathbin{\vbox{\hbox{{\bullet}}}}” is (non-) commutative. 5. 5.
The unification of -strategies is idempotent if and only if the operation of merging of contexts is idempotent, that is, for any iff \tau\mathbin{\vbox{\hbox{{\bullet}}}}\tau=\tau for any context in .
The algebraic properties of the combination of -strategies follow. In fact, the combination of -strategies inherits the properties of associativity, (non-)commutativity and idempotence from the position-based -strategies and the merging of contexts.
Theorem 40
The quotient set of -strategies together with the combination operation enjoy the following properties.
The neutral element of the combination upon is . 2. 2.
The combination of -strategies is associative, i.e. , for any . 3. 3.
The combination of -strategies is (non-)commutative if and only if the operation of merging of contexts \mathbin{\vbox{\hbox{{\bullet}}}} is (non-) commutative. 4. 4.
*The combination of -strategies is idempotent if and only if the operation of merging of contexts is idempotent. *
Since the mapping preserves the semantic equivalence in the sense of Eq.(1), then induces a mapping in a natural way by , for any term in and -strategy in . It turned out that, for any term , the mapping is a morphism from the structure to since for any -strategies and in , on the one hand,
[TABLE]
and on the other hand, it follows from Theorems 37 and 38 that
[TABLE]
The congruence and non-degeneracy of the unification and combination are stated in the two following theorems, respectively.
Theorem 41** (Congruence and non-degeneracy of the unification)**
The following holds.
The unification of -strategies is a congruence, that is, for any -strategies in , we have that:
[TABLE] 2. 2.
The unification is non-degenerate, that is, for any -strategies and in , we have that
[TABLE]
Theorem 42** (Congruence and non-degeneracy of the combination)**
The following hold.
The combination of -strategies is a congruence, that is, for any -strategies in , we have that:
[TABLE] 2. 2.
The combination is non-degenerate, that is, for any -strategies and in , we have that
[TABLE]
7 Outline of the proof of the main result
The most lengthy and difficult result to prove is Theorem 37 on the correctness of the unification of -strategies. The remaining theorems are more or less a consequence of this theorem. In this section we give a relatively detailed outline of the proof of Theorem 37 without the technical machinery which will be developed in the next sections. We shall proceed in four steps:
Step 1.
We first show that the unification of -strategies is correct in the particular setting, where the -strategies are fixed-point free. More precisely, we shall show that the mapping permutes with the unification (in the sense of Theorem 37) within this particular setting. The proof is relatively easy and will be exposed in Section 9.
Step 2.
Then we reduce the general setting to the fixed-point free setting by replacing the fixed-point operators by iterations whose number depends on the input term, Sections 10, 11 and 12. That is, we replace in the input -strategies each fixed-point -strategy with the unfolding whose length is an arbitrary fixed integer . Clearly, the unfolding of a -strategy is a fixed-point free one. The key idea is to show that the unification of two -strategies is -equivalent to the unification of their unfoldings. To accomplish this, we compare the structure of the resulting two -strategies and show that they have a similar structure (Lemma 87). We illustrate this idea of similarity of structures in a particular case through a simple example, then we discuss the more general case. For the simple example, let and be three fixed-point free -strategies where does not contain neither a left choice nor an . Consider, on the one hand, the unification of with , and on the other hand, the unification of the unfolding of with the unfolding of . Notice that the unfolding of is equal to since is fixed-point free. The structure of the -strategy is depicted on the left of Figure 2, while that of the -strategy is on the right. That is, the unification yields a -strategy of the form , whereas the unification yields a (fixed-point) free -strategy of the form .
The general case in which we unify and where both of them contain many fixed-point operators can be obtained by generalizing the simple example. The general structure of the -strategy is depicted on the left of Figure 3, while that of the -strategy that results from the unification of an unfolding of with an unfolding of is on the right. The general structure of the -strategy on the left is of the form , while that on the right, is . Besides, each -strategy on the left is either a fixed-point variable or a fixed-point -strategy that results from the unification of two -strategies where one of them is a fixed-point. Assume that is the normal form of , where is a fixed-point -strategy that is a sub--strategy of , while is a sub--strategy of . The main point is that each is the result of the unification of an unfolding of with an unfolding of . Furthermore, the more we go deeper into the right tree, i.e. increases, the more the size of iterations in the unfoldings decreases. The formalization of the notion of similarity between the unification of two -strategies and that of their unfoldings will be done in Subsection 11.3. Proving the existence of such similarity between the unification and the unification of unfoldings, as well as developing the properties of this similarity, namely the decrease of the size of iterations in the unfoldings, will be done in Section 11.4.
Step 3.
The third step of the proof consists of proving that the unification of two -strategies is equivalent to that of their unfoldings by using the notion of similarity discussed before. More precisely, we shall show that, for any , the unification of two -strategies is -equivalent to the -unfolding of them, where -unfolding amounts to replace each fixed-point operator with an iteration of size . This will be proved in Section 12, Proposition 105. We outline next the general idea of this proof in a simple setting in which the unification yields a -strategy . Thanks to the notion of similarity, we know that the unification of the -unfolding of with the -unfolding of is of the form , where is the result of the unification of an -unfolding of with a -unfolding of , where the -unfolding (resp. -unfolding) replaces each fixed-point operator in (resp. in ) with certain number of iterations that can be computed. To show that is -equivalent to it suffices to show that is a fixed-point of , i.e. that is -equivalent to . To achieve this it is enough to show that is -equivalent to provided that there is at least jumps between the root of and , where is a constant that depends on and . This raises two technical problems. (i) Since is the unification of the -unfolding of with the -unfolding of , and since is the unification of the -unfolding of with the -unfolding of , how to relate in general the unification of two unfoldings with the unification of two other unfoldings of the same -strategies? We shall address this problem in Section 11.1 and show that the two resulting -strategies are equivalent up to a constant that depends on the four unfoldings. And (ii) how to compute a lower bound on the number of such jumps? This question will be addressed in Subsections 12.1 and 12.2. These results will be summed up in Subsection 12.3 to show the main result of this third step (i.e. Proposition 105).
Step 4.
Since an unfolding of a -strategy is a fixed-point free one, we shall rely on Proposition 105 together with the correctness of the unification and combination for the fixed-point free setting outlined in Step 1, to prove the correctness of the unification and combination in the general setting. The proof turns to be relatively straightforward and will be exposed in Subsection 13.1.
8 From -strategies to position-based -strategies: the definition of the mapping
In this section we define the mapping announced in Section 5, then state and prove its properties. Before doing this, we need to define the tree depth of a -strategy that corresponds to the usual notion of depth of such a -strategy after removing all the back-edges. We warn the reader that we shall use the same notation used for the depth of terms introduced in the preliminaries section 2.
Definition 43** (Tree depth of a -strategy)**
The tree depth of a -strategy is the depth of its underlying tree after we have ignored the fixed-point constructors of this -strategy. That is, it is the function defined inductively as follows:
[TABLE]
It is useful to normalize -strategies which are almost position-based -strategies, i.e. they involve position jumps and conjunctions, by concatenation of their nested positions and by removing the failures. For instance, turning into , and turning into . The definition of the normalization follows.
Definition 44** (Normalization)**
The normalization is the function that turns any -strategy built up with just position jumps and conjunctions to a position-based -strategy as follows for any set of positions :
[TABLE]
Example 45** (Normalization)**
Let , and be contexts in . Let be the following -strategy:
[TABLE]
Then its normalization yields:
[TABLE]
Guided by the semantics of -strategies, we next define the mapping .
Definition 46** (The mapping )**
*We define the mapping *
[TABLE]
that associates to any term in and any closed -strategy in a position-based -strategy in by
. 2. 2.
. 3. 3.
** 4. 4.
\Psi_{t}(\mu X.S(X))=\Psi_{t}\big{(}\mu^{\delta(t)}X.S(X)\big{)}. 5. 5.
** 6. 6.
\Psi_{t}\big{(}\mathtt{\mathbf{If}}\,{S^{\prime}}\,\mathtt{\mathbf{Then}}\,{S}\big{)}=\begin{cases}\Psi_{t}(S)&\textrm{if }\Psi_{t}(S^{\prime})\neq\mathfrak{f},\\ \mathfrak{f}&\textrm{otherwise}.\end{cases}** 7. 7.
\Psi_{t}\big{(}\bigwedge_{i=1,n}@p_{i}.S_{i}\big{)}=\theta\big{(}\bigwedge_{i=1,n}@p_{i}.\Psi_{t_{|p_{i}}}(S_{i})\big{)}. 8. 8.
\Psi_{t}(\mathtt{Most}(S))=\Psi_{t}\big{(}\bigwedge_{i=1,ar(t)}@i.S\big{)}.
Example 47
If we consider the two -strategies and defined in Example 19 by
[TABLE]
together with the two terms and , then
[TABLE]
Lemma 48
The mapping preserves the semantic equivalence in the sense that, for any term in and any -strategy in , we have that
[TABLE]
The proof of this Lemma does not provide any difficulties since the definition of is close to the definition of the semantics of -strategies. The previous Lemma can be restated in terms of explicit properties as follows.
Lemma 49
The mapping satisfies the following properties for any terms , and for any closed -strategies , where is built using only jumps and failures, and for any position-based -strategy :
-
-
(a)
. 2. (b)
. 2. 2.
. 3. 3.
. 4. 4.
- (a)
. 2. (b)
. 3. (c)
* if .* 4. (d)
. 5. 5.
- (a)
\Psi_{t}(S\wedge R)=\Psi_{t}\big{(}S\wedge R^{\prime}\big{)}* if , whenever are a conjunction of jumps.* 2. (b)
* if , whenever are a conjunction of jumps.*
It turns out that the mapping (Definition 46) preserves the semantics of -strategies in the following sense.
Lemma 50
The mapping enjoys the following properties.
- i.)
For any position-based -strategies in , we have that iff for any term . 2. ii.)
For any -strategies in , we have that iff for any term . 3. iii.)
For any -strategies in , we have that iff for any term of depth .
Proof. We only prove Item ii.), the other items follow immediately from the definition of . On the one hand, from the definition of we have that
[TABLE]
However, it follows from Lemma 48 that
[TABLE]
Therefore,
[TABLE]
Since, both and are position-based -strategies, it follows from Item i.) of this Lemma that .
We show in the following lemma that the mapping can be pushed over the -strategy constructors.
Lemma 51
The mapping satisfies the following properties for any closed -strategies and any position-based -strategy and any terms :
-
-
(a)
\Psi_{t}\big{(}u;\big{(}\Psi_{t}(S)\curlywedge E\big{)}\big{)}=\Psi_{t}(u;S)\curlywedge E. 2. (b)
\Psi_{t}\big{(}u;\big{(}E\curlywedge\Psi_{t}(S)\big{)}\big{)}=\Psi_{t}\big{(}E\curlywedge\Psi_{t}(u;S)\big{)}. 2. 2.
- (a)
\Psi_{t}\big{(}(\Psi_{t}(S)\oplus\Psi_{t}(S^{\prime}))\curlywedge E\big{)}=\Psi_{t}(S\oplus S^{\prime})\curlywedge E. 2. (b)
E\curlywedge\Psi_{t}\big{(}\Psi_{t}(S)\oplus\Psi_{t}(S^{\prime})\big{)}=E\curlywedge\Psi_{t}(S\oplus S^{\prime}). 3. 3.
- (a)
\Psi_{t}\big{(}\mathtt{\mathbf{If}}\,{S^{\prime}}\,\mathtt{\mathbf{Then}}\,{(\Psi_{t}(S)\curlywedge E)}\big{)}=\Psi_{t}\big{(}\mathtt{\mathbf{If}}\,{S^{\prime}}\,\mathtt{\mathbf{Then}}\,{\Psi_{t}(S)}\big{)}\curlywedge E. 2. (b)
\Psi_{t}\big{(}\mathtt{\mathbf{If}}\,{S^{\prime}}\,\mathtt{\mathbf{Then}}\,{(E\curlywedge\Psi_{t}(S))}\big{)}=E\curlywedge\Psi_{t}(\mathtt{\mathbf{If}}\,{S^{\prime}}\,\mathtt{\mathbf{Then}}\,{\Psi_{t}(S)}).
Proof. We only prove the cases 1a and 2a and 3a since the proof of the cases 1b and 2b and 3b is similar.
-
-
(a)
We distinguish two cases depending on whether matches with or not. If matches with then the left-hand side of the equation is
[TABLE]
and the right-hand side of the equation is by the Definition of , which is equal to the left-hand side. If does not match with then, the left-hand side of the equation is by the definition of ; and the right-hand side is . 2. 2.
- (a)
We distinguish two cases depending on whether or not. If then the left-hand side of the equation is
[TABLE]
and the right-hand side of the equation is by the definition of , which is equal to the left-hand side. If , then left-hand side of the equation is \Psi_{t}\big{(}(\Psi_{t}(S)\oplus\Psi_{t}(S^{\prime}))\curlywedge E\big{)}=\Psi_{t}\big{(}\Psi_{t}(S)\curlywedge E\big{)} by the definition of on the left-choice, which is equal to , since is position-based. For the right-hand side, we have by the definition of , thus we get the desired result. 3. 3.
We distinguish two cases depending on whether or not. If then the left-hand side of the equation is \Psi_{t}\big{(}\mathtt{\mathbf{If}}\,{S^{\prime}}\,\mathtt{\mathbf{Then}}\,{(\Psi_{t}(S)\curlywedge E)}\big{)}=\mathfrak{f} by the definition of , and the right-hand side is \Psi_{t}\big{(}\mathtt{\mathbf{If}}\,{S^{\prime}}\,\mathtt{\mathbf{Then}}\,{\Psi_{t}(S)}\big{)}\curlywedge E=\mathfrak{f}\curlywedge E=\mathfrak{f}. If then left-hand side of the equation is
\Psi_{t}\big{(}\mathtt{\mathbf{If}}\,{S^{\prime}}\,\mathtt{\mathbf{Then}}\,{(\Psi_{t}(S)\curlywedge E)}\big{)}=\Psi_{t}(\Psi_{t}(S)\curlywedge E) which is equal to since is a position-based -strategy, by the Item 1a of Lemma 49. And the right-hand side is \Psi_{t}\big{(}\mathtt{\mathbf{If}}\,{S^{\prime}}\,\mathtt{\mathbf{Then}}\,{\Psi_{t}(S)}\big{)}\curlywedge E=\Psi_{t}(\Psi_{t}(S))\curlywedge E which is equal to by the same item.
9 Proof of the correctness of the unification of -strategies: the fixed-point free setting
In this section we prove the correctness of the unification procedure in the case where the two input -strategies are fixed-point free (Proposition 55). This is an important step since we shall reduce in the next three sections 10, 11, 12 the general setting into the fixed-point free one.
We notice that, in the fixed-point free setting, the memory involved in the unification system remains empty and does not play any role since the only rules that modify the contexts are the fixed-point ones. Obviously, such rules are not applied since the input -strategies are fixed-point free. Besides, in this setting, the proof of the termination and the confluence of is trivial. Indeed, terminates since each rule transforms a left-hand side -strategy into its immediate sub--strategies.
We need a simple set theoretic fact.
Fact 52
Let be sets. Then, .
Since the definition of the mapping involves the normalization of positions (function in Item 7 of Definition 46), we need to show that this normalization does not disturb the unification in the following sense.
Lemma 53
Let and be two -strategies where each and is either the failure or the insertion , for a context in . Then,
[TABLE]
Proof. Assume that
[TABLE]
where for any , and for any , and and . Therefore,
[TABLE]
Consider the -strategy :
[TABLE]
By computing the -strategies and involved in the right-hand side and the left-hand side of Eq.(2) respectively, we get:
[TABLE]
where is the -strategy
[TABLE]
Hence to prove Eq.(2) we need to show that . It follows that can be written as
[TABLE]
Notation 54
Throughout this paper the set of fixed-point free -strategies will be denoted by .
Now we are ready to show the main result of this section, that is, that the unification of fixed-point free -strategies is correct.
Proposition 55
For every term and for every fixed-point free -strategies and in , we have that
[TABLE]
Or, equivalently, the following diagram commutes.
[TABLE]
Proof. The proof is by structural induction on and , which amounts to consider the depth of , and the depth of .
Base case. If then or , and or . In this case the proof is trivial since and .
Induction step. We assume that the claim holds for some and and we shall show it for any and such that either i.) is an immediate sub--strategy of and , or ii.) is an immediate sub--strategy of and , or iii.) is an immediate sub--strategy of , and is an immediate sub--strategy of .
- 1.
If and is arbitrary then
[TABLE] 2. 2.
If and is arbitrary then
[TABLE] 3. 3.
If and is arbitrary then
[TABLE] 4. 4.
If and then let
[TABLE]
The left-hand side of Eq.(3) can be written as
[TABLE] 5. 5.
If and then assume that is neither a constant nor a rewriting variable, i.e. , the case when being trivial since both sides of the equation are equal to . In this case we rewrite as and we apply Item 4 of this proof. Let
[TABLE]
and notice that and . Hence
[TABLE]
10 Properties of the unification reduction system and of -strategies
This section, together with the next two sections 11 and 12, are devoted to developing the ingredients required in the proof of the main result of this paper regarding the correctness of the unification of -strategies in the general setting, in which the -strategies contain fixed-point operators. In this section we introduce definitions and show preliminary results which will be used in the next two sections. In Subsection 10.1 we define some measures on the structure of -strategies, namely the number of nested fixed-point operators of a -strategy and its size. In Subsection 10.2 we show the termination and the confluence of the unification reduction system. Un Subsection 10.3 we introduce the operation of unfolding which turns all fixed-point operators of a -strategy into iterations of arbitrary fixed size. In Subsection 10.4 we show some useful properties related to -strategies, namely the semantic equivalence of two -strategies when applied to terms of a certain depth, as well as a condition under which a -strategy is equivalent to a fixed-point one. In Subsection 10.5 we show a key Lemma, called composition lemma, that expresses the unification of two -strategies in terms of their sub--strategies.
10.1 Measures of -strategies: the star height and the depth of -strategies
Taking into account that the structure of a -strategy is no longer a tree but a tree with back-edges that may contain 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 fixed-point constructor , and the distance from the root of the tree to the leaves. Many proofs will be done by induction on this measure.
We adapt the definition of the star height [27, 28] that measures the depth of Kleen operator in regular languages to -strategies in order to capture the number of the nested fixed-point constructor.
Definition 56** (Star height of a -strategy)**
*The star height of a -strategy is the function
defined inductively as follows:*
[TABLE]
Example 57** (Star height)**
If and are fixed-point free -strategies with distinct free fixed-point variables, then
[TABLE]
We compute the star height of the -strategies and and \mu X.\big{(}S(X)\oplus\mu Y.R(Y)\big{)}. Since the two fixed-point operators in are not nested, we have that:
[TABLE]
However, since the two fixed-point operators in are nested, we have that:
[TABLE]
And similarly, the two fixed-point operators in \mu X.\big{(}S(X)\oplus\mu Y.R(Y)\big{)} are nested, thus we get:
[TABLE]
We combine the star height and the tree depth, defined in Definition 43, to obtain the desired measure that takes into account both the number of the nested fixed-point constructors and the size of a -strategy.
Definition 58** (Depth of a -strategy)**
*The depth of a -strategy is the function
defined by*
[TABLE]
Notice that if a -strategy is fixed-point free, i.e. it does not contain the fixed-point constructor , then its depth , for some .
The following fact shows that the depth of a fixed-point -strategy is strictly greater than the depth of its unfolding.
Fact 59
Let be a -strategy where is free in . Then for any integer we have
[TABLE]
Proof. The case when is trivial since . We show next that for any . It follows from the definition of the star height that \mathbf{h}(\mu^{n}X.S(X))=\mathbf{h}\big{(}S(S(\ldots(S(\mathfrak{f}))))\big{)}=\mathtt{max}\{\mathbf{h}(S(X)),\mathbf{h}(S(\mathfrak{f}))\}=\mathbf{h}(S(\mathfrak{f}))=\mathbf{h}(S(X)). On the other hand, by the definition of the star height . And it follows from the lexicographic order that .
We next define the number of jumps (i.e. -strategies which are position jumps of the form or s) that lie between the root of a -strategy to a free fixed-point variable. The idea is that by meeting jumps, the -strategy makes progress. In particular, if at least one jump lies between any fixed-point constructor and the occurrence of in a -strategy , then is monotonic. Besides, we can compare the semantics of two -strategies and thanks to number of jumps between the root of and .
Definition 60
Let be a -strategy where the fixed-point variable is free and appears once. The number of jumps between the root of and , denoted by , is inductively defined as follows:
[TABLE]
Example 61
Let be patterns in , and let be a fixed-point free -strategy. Let be the following -strategy:
[TABLE]
There are three jumps between the root of and , which are and and . That is,
[TABLE]
Notice that if is monotonic, then for every sub--strategy of , we have that .
10.2 Termination and confluence of the unification reduction system
To show the termination of the reduction system we need to define a measure on the tuples that strictly decreases with each derivation rule. Notice that all the reduction rules strictly decrease the size of one or both of the left-hand side -strategies except the fixed-point rules (8a) and (8b) which can replace with that is larger than . However, these fixed-point rules increase the size of the memory because the right-hand side memory is augmented with . Since the size of any memory related to two fixed -strategies is bounded, to ensure the termination of , we need to define a measure that couples the difference between such bound and the size of the memory with the size of the -strategies.
Definition 62
Let and be -strategies, and let be a memory in . We pose
[TABLE]
and define the measure .
Proposition 63
The unification reduction system enjoys the following properties.
The reduction system is terminating and confluent. 2. 2.
The normal form of a pre--strategy with respect to is a -strategy in (i.e. the normal form does not contain tuples).
Proof.
The termination is guaranteed by the fact that each reduction rule strictly decreases the measure
with respect to the lexicographic order. The confluence is guaranteed by the priority order imposed on the reduction rules. 2. 2.
Each rule either advances in the -strategy of the tuple of the left-hand side part of this rule, or reduces the left-hand side part into a -strategy.
We show next in Lemma 64 a useful property of the unification of monotonic -strategies: if the same fixed-point -strategy appears twice in a derivation with respect to the unification reduction system , then this derivation produces a jump. Indeed this is a direct consequence of monotonicity.
Lemma 64
Let , and be -strategies. Let be a pre--strategy. Let be memories. If there is a series of derivations of one of the following forms:
[TABLE]
in , then there is at least one jump between the root of and . That is,
[TABLE]
Proof. We only consider the first derivation since the other ones can be obtained by the same arguments. Recall that is monotonic by the general Assumption 31, that is, between and there is a position jump or . This implies that, there exist -strategies and , a memory , a tuple , and a series of derivations
[TABLE]
in where is either of the form or . This implies that one of the rules (4a), (4b), (7a), (7b), (7c) is applied in the derivation from to . Each of which produces a position jump or .
An immediate consequence of the previous Lemma 64 is the following Corollary.
Corollary 65
The unification of two monotonic -strategies is a monotonic -strategy.
10.3 Iteration mapping and (generalized) unfolding of -strategies
We next generalize the notion of unfolding of -strategies to allow the replacement of each fixed-point constructor of a -strategy by an iteration of arbitrary fixed size. The resulting -strategy is obviousely fixed-point free.
Definition 66** (Iteration mapping, unfolding of a -strategy)**
Let be a -strategy with bound fixed-point variables and let be a mapping, called hereafter iteration mapping. The unfolding of with respect to , denoted by , consists of replacing each fixed-point constructor by a certain number of iterations given by . It is inductively defined as follows:
[TABLE]
For two iteration mappings and defined on the same domain, we shall write to mean that for any in the domain. We shall write also to mean that and there exists in the domain such that .
Notice that, for a -strategy and an iteration mapping , if is fixed-point free then .
Example 67** (Unfolding of a -strategy)**
Let and be fixed-point free -strategies. Let
[TABLE]
be a -strategy. Consider the iteration mapping defined by :
[TABLE]
Then the unfolding of the -strategy with respect to is defined as follows:
[TABLE]
Further computations involve the replacement of each fixed-point operator by an iteration, given in Definition 16, as follow. Let be the -strategy:
[TABLE]
hence,
[TABLE]
10.4 Properties of -strategies and their fixed-points
We give fundamental properties of -strategies regarding their semantics and fixed-points. Namely the properties related, on the one hand, to the composition of -strategies in the sense of a -strategy being a sub--strategy of another one (Lemma 68), and on the other hand, a sufficient condition under which a -strategy is equivalent to a fixed-point one (i.e. Corollary 70). Finally, we study the equivalence between a -strategy and its unfolding (Lemma 71).
Lemma 68
Let , and be -strategies where the fixed-point variable appears once in , and let .
If and then . 2. 2.
If and then . 3. 3.
For any fixed-point free -strategy , and -strategies with , we have that
[TABLE]
Proof. The proof of the two first items can be easily done by a straightforward induction on and does not provide any difficulties. The proof of the third item can be easily done by a straightforward induction on since it is a generalization of the first item.
Notice that Eq.(4) holds as well if we omit the condition , i.e.
[TABLE]
because
[TABLE]
Indeed, Eq.(4) is more refined than Eq.(5) but we shall sometimes use the latter one.
From Item 2 of Lemma 68 it follows that one has to keep in mind that the notion of -equivalence between -strategies can be equivalently restated as follows: two -strategies are -equivalent if they give the same result when applied to any term of depth and not just of depth as initially defined in Definition 21.
Corollary 69
Let and be -strategies. For any term of depth and any positive integer , if we denote by the -times iteration -strategy , then we have that
[TABLE]
The following Corollary is a crucial one. It guarantees that to show that two -strategies and are -equivalent, it is enough to show that is a fixed-point of in the sense that and are -equivalent.
Corollary 70
Let and be -strategies. For any , we have that
[TABLE]
Proof. Let be a term of depth . If then clearly . On the other hand, it follows from the second equality of Eq.(6) of Corollary 69 that . Hence . But holds by Definition 18 of the semantics of -strategies.
We show in the following Lemma 71 that a -strategy is -equivalent to its unfolding, where is the minimal number of iterations in the unfolding. To achieve this, we need a technical property (i.e. Eq.(8)) that will be used later on in other proofs.
Lemma 71
Let be a -strategy with (bound) fixed-point variables and let be an iteration mapping.
- (i)
If is a fixed-point -strategy, say with , then there exists a fixed-point free -strategy with , and -strategies such that for any ,
[TABLE]
*where is the iteration mapping defined on by and for . * 2. (ii)
If , then .
Remark 72
Let be a -strategy with (bound) fixed-point variables and let be iteration mappings where . Let , and . Then it follows from Item (ii) of Lemma 71 that since and . Besides, it follows from the proof of this item that and can be written as
[TABLE]
10.5 The composition Lemma
In the following key Lemma 73 we shall formulate how the unification of two given -strategies behaves with respect to their sub--strategies. This Lemma is very useful and will be heavily used throughout this paper, namely when it comes to make a structural induction on the given -strategies. More precisely, we shall show, under some assumptions, that the unification of a -strategy with a -strategy yields a -strategy where each is either the unification of some with a sub--strategy of , or the unification of some sub--strategy of with a .
counter:composition:unif:lemma
Lemma 73** (Composition Lemma)**
Let and be -strategies. Assume that there are fixed-point free -strategies and , where and , and -strategies where , and -strategies where , such that and can be written as:
[TABLE]
Then, there is a fixed-point free -strategy and -strategies , where , such that
[TABLE]
where for any , there is an alternative between the two following choices.
- (a)
There are , a -strategy that is a sub--strategy of with , and a set of -strategies such that
[TABLE] 2. (b)
There are , a -strategy that is a sub--strategy of with , and a set of -strategies such that
[TABLE]
11 Unification and unfolding
In this section we show two independent results which will a crucial ingredient for the next section 12 in which the main theorems will be proved. The first result, shown in Subsection 11.1, establishes a semantic equivalence between the unification of unfoldings of two -strategies, say , and the unification of other unfoldings of the same -strategies, say . The second result, shown in Subsection 11.4, relates the structure of the unification of two -strategies, say , with that of their unfoldings, say , according to a relation of similarity that will be formalized in Subsection 11.3. In Subsection 11.2 we introduce some notions, namely the underlying structure of the set of fixed-point sub--strategies of a given -strategy. In Subsection 11.3 we introduce two relations of similarity, a strong and a weak one, between a -strategy and a fixed-point free one.
11.1 The equivalence between the unification of several unfoldings of two -strategies
The purpose of this section is to relate two kinds of fixed-point free -strategies: the -strategy that results from the unification of an unfolding of two -strategies, and the -strategy that results from the unification of a different unfolding of the same two -strategies. The purpose is to show that these two resulting -strategies are equivalent for any term of a certain depth that depends on the unfoldings. Given four iteration mappings where and (resp. and ) are defined on the same domain, we shall devise a measure between two the pairs and , called codistance and denoted by D^{\star}\big{(}(\mathbf{s},\mathbf{r}),(\mathbf{s}^{\prime},\mathbf{r}^{\prime})\big{)}, and show that the -strategies and are equivalent for any term of depth at most D^{\star}\big{(}(\mathbf{s},\mathbf{r}),(\mathbf{s}^{\prime},\mathbf{r}^{\prime})\big{)}. The definition of this measure will be given in Definition 74. We shall compare in Lemma 76 the fixed-point free -strategy with the (fixed-point free) -strategy , namely when and , by showing that -strategy and -strategy have the same structure except that the former -strategy is deeper than the latter. The equivalence is the main result of this section and will be proved in Corollary 77.
To illustrate the idea and justify the name of the codistance between two pairs of iteration mappings, we first consider the codistance between two iteration mapping with the same domain. Let , and be iteration mappings and assume
[TABLE]
It is clear that for any -strategy with bound variables that the (fixed-point free) -strategies and are equivalent for any of depth at most . This number corresponds to the minimal such that , for . For the same reason, and are equivalent for any term of depth at most . Obviously, is equivalent with itself for any term, and this will be taken into account in the definition of codistance 74 by saying that the codistance between an iteration mapping and itself is infinity. Besides, the more two iterations mappings are far from each others, the less is their codistance, which justifies the name of codistance. This idea of codistance between two iteration mappings can be adapted as well to measure the codistance between two pairs of iteration mappings as follows.
Definition 74** (Codistance between pairs of iteration mappings)**
Let and be iteration mappings such that and . We define the codistance between and by:
[TABLE]
We define the codistance between the pairs and by:
[TABLE]
Example 75
We only give an example of the codistance since the computation of is straightforward. If we consider the iteration mappings defined above by Eqs.(11),(12),(13) respectively, then
[TABLE]
In the following Lemma 76 (which makes use of Lemma 71) and Corollary 77 we use the following definitions: let and be -strategies with bound fixed-point variables and , respectively. Let and be iteration mappings where and .
Lemma 76
There exist fixed-point free -strategies , where each is a free fixed-point variable and , such that and can be written as
[TABLE]
The following Corollary 77 follows from Lemma 76, it confirms that the definition of codistance between two pairs of iteration mappings is the right one since it provides an upper bound for the depth of terms on which the -strategies and are equivalent. It is easy to construct examples where this bound is reached.
Corollary 77
We have that
[TABLE]
Proof. It follows from Lemma 76 that there exist fixed-point free -strategies , where each is a fixed-point variable and , such that and can be written as
[TABLE]
From Item (3) of Lemma 68, if follows that to prove Eq.(14) it suffices to show that
[TABLE]
Assume that with . Assume that there exists such that
. Let be the fixed-point -strategy related to . From the monotonicity property it follows that the shortest path in terms of number of jumps from the root of to some , say with , unfolded times giving arise to at least positions. If then in this first case we have by the definition of that and we are done. If then in this case and we pick another such that \min\big{\{}{\mathbf{s}_{2}(X_{j})\;\;|\;\;j\in\{{1,\ldots,s}\}\setminus\{{v}\}}\big{\}}=\mathbf{s}_{2}(X_{v^{\prime}}). If such does not exist then this means that for any thus and are equivalent in the strong sense. Otherwise, we reiterate the same reasoning of the first case with instead of .
11.2 Fixed-point tree and fixed-point sequence
This Subsection is first devoted to the definitions of two notions related to the tree-like structure underlying the set of all fixed-point sub--strategies of a given -strategy, Definition 78. Roughly speaking, if we look at all fixed-point sub--strategies of a given -strategy, they form a tree in the sense that there is an arrow from a fixed-point -strategy to a fixed-point -strategy if is a sub--strategy of together with further conditions.
Definition 78** (Fixed-point tree and fixed-point sequence of a -strategy)**
Let be a strategy in which each fixed-point variable appears once.
- i)
The fixed-point tree of , denoted by or simply , is the pair , where is a binary relation over defined as follows: iff is a sub--strategy of with , and there is no -strategy in such that , , is a sub--strategy of , and is a sub--strategy of . 2. ii)
A sequence in the tree , where , is a set of -strategies where each is in such that either or and in this case , for . Such a sequence will be denoted by . 3. iii)
A sequence in is left-maximal (resp. right-maximal) if there is no such that (resp. ) and (resp. ). A sequence is maximal if it is both left-maximal and right-maximal. In such case is called a root, while is called a leaf. 4. iv)
A fixed-point tree is connected if it has just one root.
Notice that if a fixed-point tree is not connected then it is composed of many fixed-point sub-trees each of which is connected.
Example 79
Let and be fixed-point free -strategies. Consider the -strategy
[TABLE]
The set of fixed-point sub--strategies is
[TABLE]
and the fixed-point tree comes with the two maximal sequences
[TABLE]
Indeed, is the root of while and are leaves. However if we take then the tree is no longer connected since it has two roots: and .
11.3 The relations of -simulation and -quasi-simulation
In Section 7 we informally outlined the proof of the main result of this paper. Namely, we described how to relate the structure of the -strategy that results from the unification of two -strategies to the structure of the (fixed-point free) -strategy that results from the unification of their related unfolding, and we illustrated the idea in Figure 2 for a simple case, and in Figure 3 for the general case. Now we formalize this idea that relates a -strategy in to a fixed-point free one in in terms of -simulation defined next.
Definition 80** (-simulation)**
For any -strategy in and any fixed-point free -strategy in , a -simulation is a binary relation between the sets of augmented sub--strategies of and of sub--strategies of , i.e.
[TABLE]
inductively defined from that fulfills the inference rules of Table 1.
Notice that if there is a -simulation between two -strategies, then it is unique, i.e. if and , for two -simulations and , then .
Example 81
Let be a fixed-point free -strategy. Then, for any , there is a -simulation between and , since is nothing but the -times iteration .
The following claims are not hard to prove.
Remark 82
For any -strategy with bound fixed-variables with , any iteration mapping , and any -strategy , the following holds.
There is a -simulation between and . 2. 2.
If there is a -simulation between and , then there is a -simulation between and for any fixed-point free -strategy . That is, the following diagram commutes.
[TABLE] 3. 3.
If there is a -simulation between and and if results from by Simplifications (32), denoted hereby , that transform a -strategy into an equivalent -strategy in which each fixed-point variable occurs once, then there is a -simulation between and as well. That is, the following diagram commutes.
[TABLE]
We next define a weaker relation of -simulation by relaxing the constraint imposed by the fixed-point rule that unravels into . The motivation is that in the upcoming proofs, rather than proving the existence of a -simulation, it is much easier and less cumbersome to proceed in two steps by firstly constructing the weaker relation and then strengthening it by deducing its properties.
Definition 83** (-quasi-simulation)**
For any -strategy in and any fixed-point free -strategy in , a -quasi-simulation is a binary relation between sub--strategies of and of , i.e.
[TABLE]
inductively defined from that fulfills the inference rules of Table 2 which are the same as the inference rules of Table 1 apart for the fixed-point rule which is replaced by new two rules.
Notice that -quasi-simulation is strictly weaker than the -simulation in the sense that if there is a -simulation between and then there is a -quasi-simulation between and as well, while the opposite does not hold in general. This is due to the fact that the -simulation imposes that and must correspond to the ”same” -strategy in , while the -quasi-simulation does not impose that. For instance, there is a -quasi-simulation between and whatever maybe since , while it is not the case that there is in general a -simulation between and unless further constraints are imposed on . Hence Remark 82 holds for -quasi-simulations as well.
A -quasi-simulation between and induces two mappings, the first one that maps each fixed-point -strategy of to a sub--strategy of , and the second one that maps each bound variable of to a sub--strategy of as well.
Definition 84
*For any -quasi-simulation relation between and , with and , define the mappings *
[TABLE]
as:
, for any , being the unique such that , and
- 2.
, for any , being where is the (unique) fixed-point -strategy related to .
Besides, the mapping extends uniquely to an endomorphism defined for any -strategy by:
[TABLE]
Notice that it follows from Definition 80 that any -simulation from to is not defined for the bound fixed-point variables of since any fixed-point sub--strategy of is unravelled to and hence is never reached.
Example 85** (The mappings and )**
Let and be fixed-point free -strategies. Then there is a -simulation and a -quasi-simulation between and and we have that:
[TABLE]
And therefore,
[TABLE]
Remark 86
Notice that if is a fixed-point free -strategy in which are free fixed-point variables, and if are -strategies where each of is either fixed-point -strategy or a fixed-point variable, then it follows from Definition 84 together with Definition 83 of -quasi-simulations that
[TABLE]
11.4 Relating the structure of the unification of two -strategies with that of their unfolding
The purpose of this section is to relate the structure of the unification of two -strategies with that of their unfolding as illustrated in Section 7 in Figure 2 for a simple case, and in Figure 3 for the general case. More precisely, we show in the following Lemma 87 that the unification commutes with the unfolding in the following sense: there is a -quasi-simulation between the -strategy that results from the unification of two -strategies and the fixed-point free -strategy that results from the unification of their related unfolding.
We illustrate with a simple unification example how this -quasi-simulation is constructed, and thus how the two structures in Figure 2 are obtained. Let and be fixed-point -strategies, and consider, on one hand, the unification of with , and on the other hand, the unification of the unfolding of with the unfolding of , which is , since is fixed-point free. We explain how these two unifications are related. During the unification process that starts from on one side, and from , where , on the other, we distinguish many cases.
- (I)
As far as we have on one side, and on the other, where (resp. ) is a sub--strategy of (resp. ), the constructed -strategy is the same on both sides, it is in Figure 2. 2. (II)
If the derivation reaches a fixed-point -strategy, that is, it reaches on the left side, and on the right one, where is a sub--strategy of , then the left derivation produces and continues from , while the right one continues from . This goes back to case (I), in which we take , and in which the left derivation will produce , while the right one will produce . During the generation of two cases can happen:
- (a)
If the left derivation reaches , then the right derivation reaches . The left derivation continues and produces the fixed-point generated at the end of case (II), while the right derivation produces the -strategy depicted on the right of Figure 2. 2. (b)
If the left derivation reaches with , then the right derivation reaches . Thus the left derivation produces the fixed-point -strategy
and continues from (see left of Figure 2), while the right derivation continues from , see right of Figure 2. This goes back to case (I).
In the following Lemma 87 we construct a -quasi-simulation between the unification of any two -strategies and the unification of their any unfolding.
Lemma 87
Let and be -strategies with bound fixed-point variables and . Let be a memory with respect to and . Let and be iteration mappings. There is a -quasi-simulation between and . In particular, the following diagram commutes.
[TABLE]
It turned out that the -quasi-simulation of 87 is actually a -simulation, but we can not prove it now in this section, because it requires the further developments of the next section 12, and there we shall be ready to prove it in Corollary 98.
Now we can state and prove in Lemma 88 useful properties of the -quasi-simulation constructed in the proof of the previous Lemma 87. Roughly speaking, we need to distinguish in the resulting -strategy between two kinds of fixed-point -strategies:
- (i.)
a fixed-point -strategy , where is fresh, that is generated by the fixed-point rules (8a) and (8b) of the unification reduction system given in Definition 33, and 2. (ii.)
a fixed-point -strategy that is a sub--strategy of or .
In the first case, the fixed-point -strategy is related by the -quasi-simulation to the unification of an iteration (over a fixed-point -strategy) with a -strategy, or symmetrically, to the unification of a -strategy with an iteration (over a fixed-point -strategy). However, in the second case, the fixed-point -strategy is related by the -quasi-simulation to its unfolding. Formally,
Lemma 88
Let and be -strategies with bound fixed-point variables and . Let and be iteration mappings. The -quasi-simulation between and constructed in the proof of Lemma 87 has the following property.
For any sub--strategy in that is either a fixed-point or a bound variable, i.e.
[TABLE]
there exist -strategies and , iteration mappings and and a memory such that one of the four following case holds:
- (a)
[TABLE]
and in this case and . 2. (b)
[TABLE]
and in this case and . 3. (c)
[TABLE]
with and . 4. (d)
[TABLE]
with and .
Proof. Item (a) follows immediately from the case (3) of the proof of Lemma 87 since any fixed-point -strategy and any fixed-point variable in the resulting -strategy results from the unification of a fixed-point -strategy with an arbitrary -strategy such that and is related by the -quasi-simulation to a unification of two -strategies where the left one is an iteration over a fixed-point -strategy (i.e. ).
Item (b) follows from the symmetric case of case (3) of the proof of Lemma 87 which we omitted and in which any fixed-point -strategy and any fixed-point variable in the resulting -strategy results from the unification of an arbitrary -strategy with a fixed-point -strategy such that and would be related by the -quasi-simulation to a unification of two -strategies where the right one is an iteration over a fixed-point -strategy.
Items (c) and (d) follow from the case (3) of the proof of Lemma (87) together with the explicit computations made in the composition Lemma 73, with properties (9) and (10), in which we take one of the or one of the as fixed-point -strategy, and by taking one of the as a fixed-point -strategy that is either or , for some and some .
In the following example we illustrate the cases (a) and (c) of Lemma 88, we omit the cases (b) and (d) since they are respectively symmetrical to the two former ones.
Example 89
Let be -strategies such that are fixed-point free, and are fixed-point -strategies of the form
[TABLE]
where is a sub--strategy of which is a sub--strategy of . Consider the following iteration mappings in which :
[TABLE]
Since are fixed-point free, then they are equal to their unfoldings. We next consider the two unifications and that result respectively from the following two derivations, in which we omit the explicit expression of the -strategies and of , where and are memories:
[TABLE]
If we assume, for the sake of simplicity, that the normal form of in the derivation (16) produces just one fixed-point -strategy, then the set of fixed-point sub--strategies of is:
[TABLE]
Recall that, from Definition 34 of unification, we have
[TABLE]
Therefore, the cases (a) and (c) of Lemma 88 are as follows:
[TABLE]
We recall that a -strategy that results from a unification may contain useless fixed-point constructor of the form where does not appear in , or it may contain a fixed-point variable that appears many times. We noticed in Item 3 of Remark 82 that Simplifications (32) preserve the relation of -simulation and therefore the -quasi-simulation. Hence we can assume from now on that the -strategies that result from the unification follow Assumptions 31. It is simpler for later development, to lift the properties of the relation -quasi-simulation of Lemma 88 to its induced mapping . This will be done in Lemma 90 together with a simple and useful property on the image by of fixed-points -strategies in . Roughly speaking, this property states that if and are fixed-point -strategies in where is an immediate sub--strategy of , then the number of iterations over a certain fixed-point -strategy decreases by one from to .
Lemma 90
Let and be -strategies with bound fixed-point variables and . Let and be iteration mappings. Let be the mapping induced by the -quasi-simulation between and constructed in the proof of Lemma 87. The mapping enjoys the following properties.
For any fixed-point -strategy in , there exist -strategies and , mappings and , and a memory such that one of the four following cases holds.
- (a)
\mathbf{T}=\mathtt{\mathcal{NF}}\big{(}\langle{\mu X^{\prime}.S^{\prime}(X),R^{\prime},\mathcal{M}^{\prime}}\rangle\big{)}* and \phi_{\mu}(\mathbf{T})=\big{(}\rho_{\mathbf{s}^{\prime}}({\mu X^{\prime}.S^{\prime}(X^{\prime})})\curlywedge\rho_{\mathbf{r}^{\prime}}({R^{\prime}})\big{)}.* 2. (b)
\mathbf{T}=\mathtt{\mathcal{NF}}\big{(}\langle{R^{\prime},\mu X^{\prime}.S^{\prime}(X^{\prime}),\mathcal{M}^{\prime}}\rangle\big{)}* and \phi_{\mu}(\mathbf{T})=\big{(}\rho_{\mathbf{r}^{\prime}}({R^{\prime}})\curlywedge\rho_{\mathbf{s}^{\prime}}({\mu X^{\prime}.S^{\prime}(X^{\prime})})\big{)}.* 3. (c)
, with and , and . 4. (d)
, with and , and . 2. 2.
For any fixed-point sequence
[TABLE]
in with and for any , there are iteration mappings and , such that one of the following two cases holds:
- (a)
There is a -strategy with , and a -strategy such that
[TABLE]
and for and for any and any , we have that
[TABLE] 2. (b)
There is a -strategy , and a -strategy with , such that
[TABLE]
and for and for any and any , we have that
[TABLE]
Example 91
We consider the two unifications and of Example 89, as well as their related derivations (16) and (17).
The cases (1a) and (1c) of Lemma 90 correspond to the following equalities:
[TABLE] 2. 2.
Notice that from the derivation (16) of Example 89, we have that is a (fixed-point) sub--strategy of , which is a (fixed-point) sub--strategy of . Thus we have the fixed-point sequence
[TABLE]
in . Recall that the iteration mappings , and were defined in Example 89 as:
[TABLE]
Therefore, Eq.(18) of the case (2a) of Lemma 90 expresses in terms of , as well as in terms of as follows:
[TABLE]
where .
12 The equivalence between the unification of two -strategies and that of their unfoldings
This is the most technical section in which we develop the last ingredient required in the proof of the main result of this paper. The purpose of this section is to show that the unification of two -strategies is equivalent to the unification of their unfolding for any term of depth at most a certain bound that depends on the two unfoldings, i.e. Proposition 105. More precisely, we shall prove that for any two iteration mappings and with , the -strategies and are equivalent for any term of depth at most , where (resp. ) are the bound variables of (resp. ).
To achieve this we need, on the one hand, the main result of Subsection 11.4 that ensures the existence of a -quasi-simulation between and (Lemma 87), together with the properties of this relation (Lemma 90). Indeed such results guarantee that and have almost the same structure and should be equivalent. However, on the other hand, the structure of differs from that of when it comes to certain sub--strategies. Therefore, to complete the proof we need to show that any such sub--strategy of is equivalent to its related sub--strategy of with respect to any term of a certain depth that depends on the position of such distinct sub--strategy in , or equivalently in .
To illustrate the idea, we consider the simplest case where such that is fixed-point free. Let . Therefore, thanks to the -quasi-simulation and its properties, we know that , where , for iteration mappings and . Hence to show that is -equivalent to , it suffices to show that is a fixed-point of , i.e. that . But since , we need to show that is -equivalent to . To achieve this, it suffices to show that is -equivalent to for some provided that the number of jumps between the root of and is at least . That is, and are -equivalent where depends on the iteration mappings , , and . It turns out that in this simple case, is nothing but the codistance , and is a lower bound for the number of jumps between the root of and .
However, for the general case where contains many nested fixed-point -strategies, say
[TABLE]
which yields the fixed-point sequence , many difficulties arise. Namely, the codistance is no longer an exact lower bound to the number of jumps, say between the root of and , where . However the same technique remains: to prove that it is enough to show that , for some , provided that the number of jumps from the root of to is at least . Besides, the same principle remains: the more we go deeper in the sequence , the more the iterations in the related -strategies of (i.e. that result in and have the form for ) decrease, and the more we get more jumps from the root of to .
Having said that, we need to supplement the codistance with further measures that will be introduced in Subsection 12.1 together with their properties. In Subsection 12.2 we shall show that these measures provide enough information to compute an adequate lower bound for the number of jumps. More precisely, these measures will allow us to extract a subsequence from the fixed-point sequence , called the derivative sequence, with the property that there is at least one jump between any two successive -strategies in this Subsequence. Summing up these results we shall show in Subsection 12.3 that the unification of two -strategies, say , is -equivalent to the unification of their unfolding, i.e. say , where the iteration mappings and associate to each fixed-point variable the constant . We shall make use of the main result of Subsection 11.1 that allows to compare the equivalence of the unification of an unfolding of two -strategies with the unification of another unfolding of the same two -strategies.
12.1 Measures and codistance on fixed-point tree
We define next the number of occurences of a -strategy in a sequence of tuples.
Definition 92
Let and be -strategies. Let be a sequence of tuples
[TABLE]
with , and for . Let be a fixed-point sub--strategy of . We shall denote by the number of occurrences of in the sequence , that is
[TABLE]
For a -strategy that is a fixed-point sub--strategy of , the definition of is similar to by taking instead of in Eq.(20).
We shall use the following notations throughout this Subsection and the next Subsection 12.2 as well. Let (resp. ) be a -strategy with fixed-point variables (resp. ). Let and let and be iteration mappings with . Let be the mapping induced by the -quasi-simulation between and . Let be the fixed-point tree of . Recall that is not necessarily connected, i.e. it may be composed of many connected sub-trees and thus it may have many roots.
In the following Definition 94 we define three measures, one to count the maximal number of repetitions of -strategies in a sequence of tuples, a second one that is minus the previous measure, and the third one that transfers the codistance from to the related -strategies that belong to the fixed-point tree .
Notations 93** (For Definition 94)**
In the following Definition 94 we let to be a left-maximal sequence
[TABLE]
in (i.e. being a root of ) with . According to Items (1a) and (1b) of Lemma 90, we know that for any , one of the following two cases holds.
- (i)
\mathbf{T}_{i}\in\widetilde{\Phi}(S\curlywedge R)\setminus\big{(}\widetilde{\Phi}(S)\cup\widetilde{\Phi}(R)\big{)}* and hence it can be written as and in this case \mathbf{T}_{i^{\prime}}\in\widetilde{\Phi}(S\curlywedge R)\setminus\big{(}\widetilde{\Phi}(S)\cup\widetilde{\Phi}(R)\big{)} for .* 2. (ii)
* and in this case and or .*
This yields the finite sequence of tuples
[TABLE]
that either ends with a tuple or a fixed-point -strategy or a fixed-point -strategy . Besides, the mapping associates to the sequence the sequence
[TABLE]
in which is
[TABLE]
that ends with the -strategy or or , for iteration mappings and .
Definition 94** (Measures on -strategies of fixed-point tree)**
We define three measures.
We define , for , as the maximal number of occurrences of -strategies that appear in the series of tuples in starting from the tuple related to and ending with the tuple related to . That is, if \mathbf{T}_{j}\in\widetilde{\Phi}(S\curlywedge R)\setminus\big{(}\widetilde{\Phi}(S)\cup\widetilde{\Phi}(R)\big{)}, then
[TABLE]
If , then
[TABLE] 2. 2.
For , define
[TABLE] 3. 3.
For , we define the codistance between and as follows.
If \mathbf{T}_{i}\in\widetilde{\Phi}(S\curlywedge R)\setminus\big{(}\widetilde{\Phi}(S)\cup\widetilde{\Phi}(R)\big{)}, then
[TABLE]
If , then
[TABLE]
When the sequence is known and if there is no ambiguity we shall simplify the notations by omitting and simply writing , and instead of , and . These three measures are illustrated with the following example.
Example 95
Let be fixed-point -strategies, where for , such that is a sub--strategy of which is a sub--strategy of . Let be fixed-point free -strategies, and let be memories with .
Firstly, we consider the unification . We do not make explicit the derivation that starts from because it has been detailed in the similar and simpler Example 89, see Eq.(16). We assume that the unification gives rise to the following sequence of tuples, in which occurs times, occurs times and occurs once:
[TABLE]
This yields the following (fixed-point) left-maximal sequence, denoted by :
[TABLE]
in , where each is the normal form of the related triplet (i.e. , etc).
Secondly, we consider the unification of an unfolding of with an unfolding of . Recall that , as well as the other , are fixed-fixed point free, and therefore they are equal to their unfolding. Hence, we define the following iteration mappings in which :
[TABLE]
and we consider the unification , which is related to the unification via the mapping as follows:
[TABLE]
The measures and and , related to the (fixed-point) sequence , are given in Table 3, in which the second row shows the -strategy among that appears in ; and the third row shows the iteration mapping involved in .
In Lemma 96 we shall establish a useful relation between and .
Lemma 96
For any left-maximal sequence
[TABLE]
in with , and for any and where ,
*If for , there are -strategies and , and iteration mappings *
* and such that*
[TABLE]
then
[TABLE] 2. 2.
If there is a -strategy and an iteration mapping such that
[TABLE]
then
[TABLE]
From Lemma 76 we get the following corollary that establishes, in addition to another property, the semantic equivalence between and for a fixed-point variable of a -strategy that appears in the fixed-point tree . Roughly speaking, this corollary will be useful to prove that is a fixed-point of as explained at the beginning of Subsection 12.3, and used in the proof of Lemma 103.
Corollary 97
Let be a sequence
[TABLE]
in with and .
If then
[TABLE] 2. 2.
If (i.e. ) then
[TABLE]
Proof.
Since then it follows from Items (1a) and (1b) of Lemma 90 that there are -strategies and , and iteration mappings and such that
[TABLE]
where and . Thus, by Eq. (24) of Definition 94 of , we have . Hence the claim follows from Corollary 77 that states that
[TABLE] 2. 2.
Assume that is a sub--strategy of , the case when it is a sub--strategy of is similar. From Items (1c) of Lemma 90 if follows that there is an iteration mapping such that
[TABLE]
Let . We know from Item (ii) Lemma 71 that
[TABLE]
Hence it follows from From Item (2) of Lemma 68 that to show Eq.(30) it suffices to show
[TABLE]
But this was proved in Lemma 96, see Eq. (28).
Although the following corollary will not be used in any further proofs, it is worth mentioning it.
Corollary 98
The -quasi-simulation that results between the unification of two -strategies, say , and that of their unfolding, say , (i.e. constructed in the proof of Lemma 87) is actually a -simulation.
Proof. This follows immediately from Corollary 97. That is, on the one hand for any -strategy in that is not a sub--strategy of nor , we have that each of (i.e. ) and corresponds to the unification of two unfoldings of the same two -strategies. And on the other hand, for any -strategy in that is a sub--strategy of or , there is a -simulation between and any unfolding of it.
12.2 Derived tree and a lower bound for the number of jumps
The Eq.(27) of Lemma 96 allows one to distinguish between elements of whose and are equal, and those whose and are different by . The latter elements form the derived tree of . The name ”derived” tree is justified by the fact that we want to focus on the elements of on which changes and increases by .
Definition 99** (Derived tree of )**
Recall that . We define the derived tree of , denoted by , as the pair where is defined by
[TABLE]
Example 100** (Derived tree )**
We consider Example 95, and we assume that the fixed-point tree of contains just the sequence , defined in Eq. (26). By examining the last two rows of Table 3 that respectively exhibit and , we notice that the equality holds for . Hence it follows that the derived tree is composed of . Besides, in , we have .
The following remark provides useful observations that can be illustrated by the Table 3 of the Example 95.
Remark 101
Notice that, for any maximal sequence in , the following statements follow from Eq.(27) of Lemma 96 and from Definition 99.
Any (fixed-point) -strategy which is in but not in has the property . 2. 2.
Since by Items (1a) and (1b) of Lemma 90 we know that each of and can be incremented by at most from a -strategy to its immediate sub--strategy in , then if is in and is in such that , then and hence . 3. 3.
Similarly, if are in , and is in such that , then and , for any . 4. 4.
In particular, if and are in such that , then and .
Thanks to Lemma 96 and Remark 101, we show in the following Lemma 102 a crucial property of the derived tree that was behind its introduction: if two -strategies and are in with , then the number of jumps between the root of and is at least one.
Lemma 102
Let
[TABLE]
be a sequence in . Define to be the (unique) -strategy satisfying
[TABLE]
We have that
[TABLE]
12.3 The unification of two -strategies is equivalent to the unification of their unfolding
We arrive at the key lemma that will allows us to show that unification of two -strategies is -equivalent to the unification of their unfolding. We already explained at the beginning of this Section 12 that, in the particular setting where is composed of just one -strategy, say , the purpose is to show that is a fixed-point of , where is the unification of the unfolding of two -strategies. That is, we want to show that is -equivalent to .
However, if we consider the general setting in which the fixed-point -strategies in can be nested, namely if we have a sequence in , then a fixed-point variable may appear in any -strategy for . Therefore, we need a general and inductive way to formulate and then to show that certain fixed-point free -strategies (which are in the -strategy that results from the unification of the unfolding of with the unfolding of ) are a fixed-point of , respectively, in the sense that is -equivalent to , for , where is an appropriate constant. This general and inductive way of formulating such requirements is achieved thanks to the mappings and by just imposing that \phi_{\mu}\big{(}\mu Z_{i}.T_{i}(Z_{i})\big{)} and must be -equivalent. In particular, \phi_{\mu}\big{(}\mu Z_{i}.T_{i}(Z_{i})\big{)} corresponds to , while corresponds to since, roughly speaking, corresponds to T_{i}\big{(}\widehat{\phi}_{\nu}^{\mu}(Z_{i})\big{)} which is .
Lemma 103
Let (resp. ) be a -strategy with bound fixed-point variables (resp. ), and let . Let and be iteration mappings with , for and . Let be the fixed-point tree of rooted at . Let be a right maximal sub-tree of rooted at yielding the unique sequence :
[TABLE]
in and let
[TABLE]
Then for any , and any maximal sequence
[TABLE]
*in where , either *
- (i)
Z_{i}\in{\mathcal{B}ound({S\curlywedge R})}\setminus\big{(}{\mathcal{B}ound({S})}\cup{\mathcal{B}ound({R})}\big{)}* and in this case we have that*
[TABLE] 2. (ii)
or and , and in this case we have that
[TABLE]
Proof. The proof is by a double induction. The outer one is a structural induction on the tree .
Outer base case .
In this case consider a maximal sequence
[TABLE]
in with . Indeed, since then
[TABLE]
We make an inner structural induction on .
Inner base case: .
Since is not necessarily connected, it may contain many maximal sequences, but each one of them is composed of just one fixed-point -strategy. Hence, consider a maximal sequence
[TABLE]
in . And we need to show that
[TABLE]
If then Eq (36) follows from Eq.(30) of Corollary 97.
If Z_{m}\in{\mathcal{B}ound({S\curlywedge R})}\setminus\big{(}{\mathcal{B}ound({S})}\cup{\mathcal{B}ound({R})}\big{)} then notice that is fixed point-free but may contain free fixed-point variables besides . Therefore there exists a fixed point-free -strategy with and such that . Hence we need to show that
[TABLE]
On the one hand, it follows from Remark 86 that the left-hand side of Eq. (37) can be written as
[TABLE]
On the other hand, by the Definition 84 of , the right-hand side of Eq. (37) can be written as
[TABLE]
Thus we need to show that
[TABLE]
From Eq.(29) of Corollary 97 we have that
[TABLE]
But we know from Eq.(34) above that as well as for . Thus Eq.(38) holds by Item (2) of Lemma 68.
Inner induction step. Assume that Eq.(32) holds for a fixed-point sub-tree of , and we shall prove it for the (unique) fixed-point sub-tree (of ) that contains such that is an immediate sub-tree of . Assume that is rooted at .
Consider such tree and a maximal sequence
[TABLE]
in . We recall that we have
[TABLE]
The -strategy can be written in terms of its immediate fixed-point sub--strategies and fixed-point variables in the sense that there exist and and
- i.)
a fixed-point free -strategy in which each fixed-point variable is free, and 2. ii.)
-strategies where each is either a fixed-point -strategy in , and 3. iii.)
fixed-point variables where ,
such that can be written as
[TABLE]
Hence, we need to show that
[TABLE]
On the one hand, it follows from Remark 86 that the left-hand side of Eq.(40) can be written as
[TABLE]
On the one hand, by Definition 84 of , the right-hand side of Eq.(40) can be written as
[TABLE]
Therefore showing Eq.(40) amounts to show that
[TABLE]
We recall that from Eq.(39), we have for as well as for . Therefore from Item 2 of Lemma 68 it follows that to show Eq.(41) it is enough to show that for any
[TABLE]
and that for any ,
[TABLE]
To achieve this, consider the two cases.
- 1.
For Eq.(42) assume that is of the form . We distinguish two cases depending on whether \mathbf{Z}^{j}\in{\mathcal{B}ound({S\curlywedge R})}\setminus\big{(}{\mathcal{B}ound({S})}\cup{\mathcal{B}ound({R})}\big{)} or . For the first case we have the sequence
[TABLE]
in . Let be the maximal sub-tree of which is rooted at . Since is an immediate sub-tree of , then Eq. (42) follows from the inner induction hypothesis. However, for the second case where we have the sequence
[TABLE]
in . That is, in this case we remind that the fixed-point -strategy is either a sub--strategy of or of . Hence, we have . It follows from the base case, i.e. Eq.(33) that
[TABLE]
- 2.
For Eq.(43), it follows from Eq.(29) of Corollary 97.
Outer induction step. Assume that Eq.(32) holds for a fixed-point sub-tree of , we shall prove it for the (unique) fixed-point sub-tree (of ) that contains such that is an immediate sub-tree of . Let be a root of , and let be a root of . Consider such tree and a maximal sequence
[TABLE]
in . Assume that the maximal sequence in that lays between the root of and the root of is non-empty, the case where it is empty can be handled similarly. Let the following be such a sequence:
[TABLE]
where . In this case, by Definition 99 of the derived tree we have
[TABLE]
On the one hand, from the outer induction hypothesis we have that
[TABLE]
On the other hand, as far as Eq.(45) holds, using the same kind of induction made in the inner base case, we can easily show that, for , we have
[TABLE]
Since is a sub--strategy of then there is a -strategy such that can be written as
[TABLE]
Since by Eq.(44) we know that \mathbf{D^{\star}}\big{(}\mu\hat{Z}_{\hat{i}-1}.\hat{T}_{\hat{i}-1}(\hat{Z}_{\hat{i}-1})\big{)}=\mathbf{D^{\star}}\big{(}\mu Z_{p}.T_{p}(Z_{p})\big{)}+1, then it follow from Item 1 of Lemma 68 that to show Eq.(32), it suffices to show that
[TABLE]
but this was proved in Lemma 102, see Eq.(31).
In the following Corollary we show that the unification of two -strategies is equivalent to that of their unfolding in the particular setting in which one of these two -strategies is a fixed-point one.
Corollary 104
Let (resp. ) be a -strategy with bound fixed-point variables (resp. ) and let . Let and be iteration mappings with for and . If either or is a fixed-point -strategy then
[TABLE]
Or, the following two diagrams commute where stands of the set of fixed-point -strategies.
[TABLE]
Proof. Let
[TABLE]
and assume that for some -strategy . The key idea of the proof is to show that is a fixed-point of in the sense that . To achieve this we take in Eq.(32) of Lemma 103, and we get
[TABLE]
But since \mathbf{D^{\star}}\big{(}\mu Z_{1}.T_{1}(Z_{1})\big{)}=n by the Eq.(24) of Definition 94 of , we get
[TABLE]
On the one hand, by Definition 84 of together with Lemma 90 on the properties of , it follows that the left-hand side of Eq.(49) can be written as:
[TABLE]
On the other hand, the right-hand side of Eq.(49) can be written as:
[TABLE]
Summing up, and relying on Eq.(49), we get
[TABLE]
It follows from Corollary 70 that
[TABLE]
But since, by definition, we have that and , then we get the desired result, i.e. Eq.(48).
We generalize Corollary 104 by relaxing the assumption on the input -strategies and letting them to be arbitrary instead of being fixed-point ones. We thus arrive at the main result of this Subsection.
Proposition 105
Let (resp. ) be a -strategy with bound fixed-point variables (resp. ) and let . Let and be iteration mappings with for and . Then,
[TABLE]
which is illustrated by the commutative diagram below.
[TABLE]
Proof. There are fixed-point free -strategies and , where and , as well as fixed-point -strategies and such that and can be written as:
[TABLE]
On the one hand, it follows from the composition Lemma 73 that there is a fixed-point free -strategy and -strategies , where , such that can be written as
[TABLE]
where for any , one of the following cases holds.
There is and a -strategy that is a sub--strategy of such that
[TABLE] 2. 2.
There is and a -strategy that is a sub--strategy of such that
[TABLE]
We only discuss the first case since the second one is similar. On the other hand, since there is a -quasi-simulation between and (i.e. Lemma 87) to together with the properties of the induced mapping (Item (1) of Lemma 90) it follows that can be written as
[TABLE]
such that for any , we have
[TABLE]
If then it follows from Item (ii) of Lemma 71 that since for any in . Otherwise, if then it follows from Corollary 104 that . Therefore,
[TABLE]
Hence,
[TABLE]
Thus the desired result follows.
13 Proof of the main results
In this section we prove the main results of this paper stated in Section 6. The correctness of the unification and combination operations for arbitrary -strategies will be proved in Subsection 13.1. The algebraic properties of the unification and combination follow immediately from the correctness result, and will be proved in Subsection 13.2.
13.1 The correctness of the unification and combination
Now we are ready to prove the first main theorem of this paper regarding the correctness of the unification of -strategies, Theorem 37. Its proof relies mainly on Proposition 105 and on the correctness of the unification for the fixed-point free fragment of -strategies stated and proved in Proposition 55.
Theorem 37** (Correctness of the unification)**
For every term and for every -strategies and in , we have that
[TABLE]
Proof.
Let be the depth of . Assume that (resp. ) are the (bound) fixed-point variables of (resp. ) and let and be iteration mappings with , for and . The proof follows from the commutativity of the following diagram.
[TABLE]
Indeed, it follows from Proposition 105, Proposition 55, Item (ii) of Lemma 71 + Item (iii) of Lemma 49, and Item (iii) of Lemma 49, respectively, that the following diagrams commute.
[TABLE]
We restate these arguments in the language of equations rather than the language of diagrams. Let
[TABLE]
We have that
[TABLE]
On the other hand,
[TABLE]
Therefore
[TABLE]
We can now state and prove the second main theorem of this paper on the correctness of the combination of -strategies. In fact, the correctness of the combination follows from the correctness of the unification that we stated and proved in Theorem 37 above.
Theorem 38** (Correctness of the combination)**
For every term and for every -strategies and in , we have that
[TABLE]
Proof.
[TABLE]
13.2 The algebraic properties of the unification and combination
Thanks to Theorems 37 and 38, and using mapping (Definition 46), we can transfer all the algebraic properties of the combination and unification of position-based -strategies (stated in Propositions 11 and 12) to -strategies.
Theorem 39
The quotient set of -strategies together with the unification operation enjoy the following properties.
The neutral element of the unification upon is . 2. 2.
The absorbing element of the unification is . 3. 3.
The unification of -strategies is associative, i.e. , for any . 4. 4.
The unification of -strategies is (non-)commutative if and only if the operation of merging of contexts ”\mathbin{\vbox{\hbox{{\bullet}}}}” is (non-)commutative. 5. 5.
The unification of -strategies is idempotent if and only if the operation of merging of contexts is idempotent, that is, for any iff \tau\mathbin{\vbox{\hbox{{\bullet}}}}\tau=\tau for any contexts in .
Proof. We only prove the associativity property. To prove the associativity of the unification for -strategies we rely on the associativity of the unification of position-based -strategies (Proposition 11) together with the property of the function (Theorems 37). Let and be -strategies in . To prove we shall prove , i.e.
[TABLE]
It follows from Item iii.) of Lemma 49 that it suffices to prove that, for any term , we have that
[TABLE]
But this follows from an easy computation:
[TABLE]
The algebraic properties of the combination of -strategies follow. They inherit the properties of associativity, (non-)commutativity and idempotence from the position-based -strategies and the merging of contexts.
Theorem 40
The quotient set of -strategies together with the combination operation enjoy the following properties.
The neutral element of the combination upon is . 2. 2.
The combination of -strategies is associative, i.e. , for any . 3. 3.
The combination of -strategies is (non-)commutative if and only if the operation of merging of contexts \mathbin{\vbox{\hbox{{\bullet}}}} is (non-)commutative. 4. 4.
The combination of -strategies is idempotent if and only if the operation of merging of contexts is idempotent, that is, for any iff \tau\mathbin{\vbox{\hbox{{\bullet}}}}\tau=\tau for any contexts in .
Proof. Very similar to the proof of Theorem 39.
The congruence and non-degeneracy of the unification and combination are stated in the two following theorems, respectively.
Theorem 41** (Congruence and non-degeneracy of the unification)**
The following holds.
The unification of -strategies is a congruence, that is, for any -strategies in , we have that:
[TABLE] 2. 2.
The unification is non-degenerate, that is, for any -strategies and in , we have that
[TABLE]
Proof. We only prove the first Item. On the one hand, if follows from Theorem 38 that
[TABLE]
On the other hand, since , it follows from Item iii.) of Lemma 49 that
[TABLE]
Hence we get
[TABLE]
Again, from Item iii.) of Lemma 49, we get
[TABLE]
The proof of the remaining claims is similar.
Theorem 42** (Congruence and non-degeneracy of the combination)**
The following holds.
The combination of -strategies is a congruence, that is, for any -strategies in , we have that:
[TABLE] 2. 2.
The combination is non-degenerate, that is, for any -strategies and in , we have that
[TABLE]
Proof. Similar to the proof of Theorem 41.
14 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 introduced a class of rewriting strategies on which the operations of unification and combination were defined and proved correct. The design of this class is inspired by the -calculus formalism [8] together with practical needs emerging from asymptotic model derivation.
The -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. Besides, the ideas and techniques behind the unification and combination of the navigation part, namely the unification of fixed-point -strategies or recursion, are generic and could be used in several applications beyond rewriting strategies as far as they incorporate recursion. Although the -strategies can be viewed as a finite algebraic representation of infinite trees [29, 30], our technique of unification and combination involving -terms and their unfolding is new. 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 they are expressed as -terms in the same way we expressed the -strategies. It follows that a rewriting language that transforms algebraic infinite trees and incorporates the least and greatest fixed-point operators could be elaborated.
We implemented the unification procedure within a user specification language of mathematical expressions, proofs and extensions and their combination for asymptotic models. We noticed that the size of the resulting -strategies is big, and the good news is that they contain many redundant and inaccessible parts in the same way a graph or a transition system contains equivalent sub-parts, and a program contains inaccessible code. This raises the question of the minimization or reduction of -strategies which remains open. We managed recently to design an algorithm that decides whether two -strategies are semantically equivalent by looking at their structure. This is known as the word problem in other fields, e.g. in universal algebras [31, 32]. Proving the correctness of this algorithm is under way. This semantic equivalence algorithm will probably be useful for the minimization of -strategies since one can factorize the equivalent sub-parts. This technique is similar to the techniques of reduction of Petri nets and transition systems and event structures by the bisimulation equivalence relation [33, 34, 35, 36], and to the reduction of graphs by internal isomorphisms, or automorphism [37, 38].
Since the class of -strategies can be viewed as -calculus in the sense that it supplements elementary strategies with the fixed-point operator, one can pose the hierarchy problem for it. The hierarchy problem asks whether, for any , there exists a -strategy with bound fixed-point variables, such that no -strategy with less than bound fixed-point variables is equivalent to it. The hierarchy problem was posed for many -calculi [39, 40] and it might help in reducing the size of the -strategies, namely in minimizing the number of bound fixed-point variables.
Appendix: proofs of Lemmas
A Proofs for Section 9
Fact 52
Let be sets. Then, .
Proof.
[TABLE]
B Proofs for Section 10
Lemma 71
Let be a -strategy with (bound) fixed-point variables and let be an iteration mapping.
- (i)
If if a fixed-point -strategy, say with , then there exists a fixed-point free -strategy with , and -strategies such that for any ,
[TABLE]
where is the iteration mapping defined on by and for . 2. (ii)
If , then .
Proof. For Item (i), indeed can be written in terms of its immediate fixed-point sub--strategies where appears free in one of them since appears once in . That is, there exists a fixed-point free -strategy with , and (fixed-point) -strategies such that can be written as . To show Eq.(51) we rely on the fact that is fixed-point free and on Definition 66 of unfolding together with a simple structural induction on . The computations are straightforward and we don’t make them. To show Eq.(52), let be the iteration mapping defined on as the restriction of on . Since is fixed-point free, then by the definition 66 of unfolding and making use of Eq.(51) we get
[TABLE]
To show the Item (ii) we next generalize the idea that a -strategy could be written as where the number of jumps between its root and is at least , as well as the fact that could be written as . Technically, we rely on Eq.(5) and we shall show that there exist -strategies and a fixed-point free -strategy and an unravelling of , such that and can be written as
[TABLE]
such that
[TABLE]
We make a double induction: the outer one being on with the lexicographic order, and the inner one being on the number of nested fixed-point sub--strategies of , i.e. on the star height of . The outer base case when holds trivially since in this case the set of terms of depth [math] is empty. For the outer induction step, we assume that the claim holds for and we shall prove it for any with where there is such that and for any . We make an inner induction on . The inner base case holds trivially since in this case is fixed-point free because the unfolding of is . For the inner induction step we assume that the claim holds for a -strategy and we shall prove it for any with . We only discuss the case when if a fixed-point -strategy, say , since the case when is of the form , for a fixed-point free -strategy and a fixed-point -strategies with , does not provide difficulties since it is easily reducible to the case under discussion, because \rho_{\mathbf{s}}\big{(}{\tilde{S}(\xi_{1},\ldots,\xi_{k})}\big{)}=\tilde{S}\big{(}\rho_{\mathbf{s}}({\xi_{1}}),\ldots,\rho_{\mathbf{s}}({\xi_{k}})\big{)} . We rely on the fact that can be written as , for fixed-point -strategies in , being a fixed-point free -strategy. From Eq.(51) above we have that \rho_{\mathbf{s}}({S})=\rho_{\mathbf{s}}({\mu X.S^{\prime}(X)})=\tilde{S}\Big{(}\rho_{\mathbf{s}}({S_{1}}),\ldots,\rho_{\mathbf{s}}({S_{m-1}}),\rho_{\mathbf{s}^{\prime}}\big{(}{S_{m}(\mu X.S^{\prime}(X))}\big{)}\Big{)}, where is the iteration mapping defined on by and for .
Therefore, we have that
[TABLE]
On the one hand, then it follows from inner induction hypothesis that the claims (53), (54) and (55) hold for with respect to for , since . On the other hand, since and for any , then it follows from the outer induction hypothesis that there is a fixed-point free -strategy and -strategies such that
[TABLE]
such that
[TABLE]
where . If , then we are done since in this case . Otherwise, if then . But since is monotonic then . That is, there is at least one jump between the root of and . This jump is either between the root of and , i.e. \Pi_{X^{m}}\big{(}\tilde{S}(S_{1},\ldots,S_{m-1},X^{m})\big{)}\geq 1 and in this case we are done; or between the root of and , i.e. \Pi_{X}\big{(}S_{m}(X)\big{)}\geq 1 and in this case we can assume without loss of generality that is an immediate sub--strategy of , say , and thus we get the desired result since \Pi_{X^{m}}\big{(}T(X^{1},\ldots,X^{m})\big{)}\leq 1+\Pi_{Y^{k}}\big{(}T(X^{1},\ldots,S_{m}(Y^{k}))\big{)}.
Lemma 73** (Composition Lemma)**
Let and be -strategies. Assume that there are fixed-point free -strategies and , where and , and -strategies where , and -strategies where , such that and can be written as:
[TABLE]
Then, there is a fixed-point free -strategy and -strategies , where , such that
[TABLE]
where for any , there is an alternative between the two following choices.
- (a)
There are , a -strategy that is a sub--strategy of with , and a set of -strategies such that
[TABLE] 2. (b)
There are , a -strategy that is a sub--strategy of with , and a set of -strategies such that
[TABLE]
Proof. The proof is by structural induction on the fixed-point free -strategies and . The base case is when and and . In this case we have and . The result is obvious since . For the induction step assume that the claim holds for some -strategies and , and we shall show it for any and such that either (i) is an immediate sub--strategy of and , or (ii) and is an immediate sub--strategy of , or (iii) (resp. ) is an immediate sub--strategy of (resp. ). The proof is not hard and involves straightforward computations. We only elucidate the case when is a pattern-matching and is arbitrary, and the case when both and are -strategies. The remaining cases fall into one of these two.
If and is arbitrary, then in this case
[TABLE]
From the induction hypothesis it follows that there is a fixed-point free -strategy and -strategies with the right properties (59) and (60) such that . By letting we get the desired result.
If and , then
[TABLE]
On the one hand, it follows from the induction hypothesis that there is a fixed-point free -strategy and -strategies with the right properties (59) and (60) such that . One the other hand, let the fixed-point free -strategy with free variables defined as follows:
[TABLE]
Let be the -strategies defined by
[TABLE]
Therefore, can be written as
[TABLE]
which satisfies the properties (59) and (60).
C Proofs for Section 11
Lemma 76
There exist fixed-point free -strategies , where each is a free fixed-point variable and , such that and can be written as
[TABLE]
Proof. The proof is by induction on \Gamma(S,R,\mathbf{s}_{1},\mathbf{s}_{2},\mathbf{r}_{1},\mathbf{r}_{2})\stackrel{{\scriptstyle def}}{{=}}\big{(}\delta(\rho_{\mathbf{s}_{1}}({S})),\delta(\rho_{\mathbf{s}_{2}}({S})),\delta(\rho_{\mathbf{r}_{1}}({R})),\delta(\rho_{\mathbf{r}_{2}}({R}))\big{)}. The base case is when , i.e. and are either or . This case is trivial. For the induction step, assume that the claim holds for -strategies and iteration mappings , and we shall prove it for any -strategies and iteration mappings where , or , or . We only discuss the cases when (and hence since ) and (and hence since ), because the cases when or (but not both) are just a particular case of the general case that follows, and can be handled similarly using the composition Lemma 73. We distinguish two cases depending on and .
First case. If neither nor is a fixed-point -strategy, then there exist fixed-point free -strategies and and -strategies and , where each (resp. ) is an immediate sub--strategy of (resp. ), i.e. (resp. ), such that and can be written as:
[TABLE]
Hence,
[TABLE]
It follows from the composition Lemma 73 that there exist a fixed-point free -strategy , and -strategies and such that
[TABLE]
where the Item (a) or (b) holds. We only discuss the first possibility (since the second is symmetric) according to which, for any there is , and a -strategy that is a sub--strategy of with , and a set of -strategies such that
[TABLE]
If and hence , then the claim follows from Remark 72. Otherwise, the claim follows from the induction hypothesis.
Second case. If if a fixed-point -strategy, say , then we distinguish two cases. If then the claim holds trivially since in this case . If and therefore since , then it follows from Eq.(52) of Lemma 71, that there exists a fixed-point free -strategy and -strategies , where , such that and can be written as
[TABLE]
where and for , for . Thus the reasoning is very similar to the one made in the first case, more precisely it is done by taking Eq.(61) in which we replace by \rho_{\mathbf{s}^{\prime}_{v}}\big{(}{S_{k}(\mu X.\tilde{S}(X))}\big{)}, for . Thus the induction hypothesis can be applied as well.
Lemma 87
Let and be -strategies with bound fixed-point variables and . Let be a memory with respect to and . Let and be iteration mappings. There is a -quasi-simulation between and . In particular, the following diagram commutes.
[TABLE]
Proof. We make of use of Lemma 73. The proof is by structural induction on and , according to which the -simulation will be inductively constructed. The base case holds trivially. For the induction step we assume that the claim holds for -strategies and and we shall prove for any -strategies and such that either (i) is an immediate sub--strategy of and and , or (ii) is an immediate sub--strategy of and and , or (iii) (resp. ) is an immediate sub--strategy of (resp. ). We distinguish three cases depending on and :
If and are fixed-point free, then this case is trivial since and . 2. 2.
If and are of the form and for fixed-point free -strategies and , i.e. or or or or and similarly for , then the result follows immediately from Lemma 73 since in these cases \rho_{\mathbf{s}}({S^{\prime}(S_{1},\ldots,S_{k})})=S^{\prime}\big{(}\rho_{\mathbf{s}}({S_{1}}),\ldots,\rho_{\mathbf{s}}({S_{k}})\big{)} and \rho_{\mathbf{r}}({R^{\prime}(R_{1},\ldots,R_{l})})=R^{\prime}\big{(}\rho_{\mathbf{r}}({R_{1}}),\ldots,\rho_{\mathbf{r}}({R_{l}})\big{)}, since the induction hypothesis can be applied on each and , for and . 3. 3.
If is fixed-point , with , then is replaced by in the unification, and thus we reduce this case to the case 2 above as follows:
[TABLE]
where and , and
[TABLE]
If then this case is trivial since there is by definition a -quasi-simulation between any fixed-point -strategy and , as well as between any fixed-point variable and . If and then there is by definition a -quasi-simulation between and \mathtt{\mathcal{NF}}\big{(}\langle{\rho_{\mathbf{s}}({\mu X.S^{\prime}(X)})\big{)},\rho_{\mathbf{r}}({R}),\emptyset}\rangle\big{)}. If and then it follows from Eq. (52) of Lemma 71 that there exist a fixed-point free -strategy and -strategies , with , such that can be written as . On the one hand, . On the other hand,
[TABLE]
where and for . This brings us back to the case 2 above in which the induction hypothesis can be applied on each , for and for \rho_{\mathbf{s}^{\prime}}\big{(}{S_{m}(\mu X.S^{\prime}(X))}\big{)}.
Lemma 90
Let and be -strategies with bound fixed-point variables and . Let and be iteration mappings. Let be the mapping induced by the -quasi-simulation between and constructed in the proof of Lemma 87. The mapping enjoys the following properties.
For any fixed-point -strategy in , there exist -strategies and , mappings and , and a memory such that one of the four following cases holds.
- (a)
\mathbf{T}=\mathtt{\mathcal{NF}}\big{(}\langle{\mu X^{\prime}.S^{\prime}(X),R^{\prime},\mathcal{M}^{\prime}}\rangle\big{)}* and \phi_{\mu}(\mathbf{T})=\big{(}\rho_{\mathbf{s}^{\prime}}({\mu X^{\prime}.S^{\prime}(X^{\prime})})\curlywedge\rho_{\mathbf{r}^{\prime}}({R^{\prime}})\big{)}.* 2. (b)
\mathbf{T}=\mathtt{\mathcal{NF}}\big{(}\langle{R^{\prime},\mu X^{\prime}.S^{\prime}(X^{\prime}),\mathcal{M}^{\prime}}\rangle\big{)}* and \phi_{\mu}(\mathbf{T})=\big{(}\rho_{\mathbf{r}^{\prime}}({R^{\prime}})\curlywedge\rho_{\mathbf{s}^{\prime}}({\mu X^{\prime}.S^{\prime}(X^{\prime})})\big{)}.* 3. (c)
, with and , and . 4. (d)
, with and , and . 2. 2.
For any fixed-point sequence
[TABLE]
in with and for any , there are iteration mappings and , such that one of the following two cases holds:
- (a)
There is a -strategy with , and a -strategy such that
[TABLE]
and for and for any and any , we have that
[TABLE] 2. (b)
There is a -strategy , and a -strategy with , such that
[TABLE]
and for and for any and any , we have that
[TABLE]
Proof.
For Item 1, we just replaced the -quasi-simulation relation of Lemma 88 by its induced mapping . 2. 2.
For Item 2, we consider a fixed-point -strategy in with , and we shall see that Eq.(64) and Eq.(65) hold for any -strategy in such that
[TABLE]
For this purpose, assume that
[TABLE]
since the case when
[TABLE]
can be handled similarly. It follows from Eq.(52) of Lemma 71 that there is a -strategy such that can be written as
[TABLE]
On the other hand, notice that there is a fixed-point free -strategy (resp. ) with (resp. ), and fixed-point -strategies (resp. ) each one is in (resp. ), such that (resp. ) can be written as
[TABLE]
It follows from the composition Lemma 73 that there is a fixed-point free -strategy such that
[TABLE]
such that for any , one the following two cases holds.
- (a)
There is , and a -strategy that is a sub--strategy of with , and a set such that
[TABLE]
But since , , and the iteration mappings and satisfy Eq.(68), then we get Eq.(64). 2. (b)
There is , and a -strategy that is a sub--strategy of with , and a set such that
[TABLE]
But since and the we have , and the iteration mappings and satisfy Eq.(68), then we get Eq.(64).
In summary, we assumed that satisfies Eq.(66) and we get Eq.(64). However if we assume that satisfies Eq.(67) then we get Eq.(65) by similar arguments.
D Proofs for Section 12
Before proving Lemma 96, we want to get a certain fixed-point -strategy from each of the sequence . More precisely, notice that for any , one of the following situations holds.
- i.)
If , then either is a fixed-point -strategy regardless of that could be a fixed-point -strategy as well, or is a fixed-point -strategy and is not. In the first case we want to get , and in the second we want to get . 2. ii.)
Otherwise, if is a fixed-point sub--strategy of or , then we want to get .
The formal definition follows.
Definition 91
For any , we define
[TABLE]
We need the following simple Fact.
Fact 92
For any finite sets ,
- (i)
if and if then . 2. (ii)
Therefore, to show that , it suffices to show that and .
Lemma 96
For any left-maximal sequence
[TABLE]
in with , and for any and where ,
*If for , there are -strategies and , and iteration mappings *
* and such that*
[TABLE]
then
[TABLE] 2. 2.
If there is a -strategy and an iteration mapping such that
[TABLE]
then
[TABLE]
Proof.
Since , showing Eq.(69) amounts to show
[TABLE]
Since and , then for there exist positive numbers where , and for , there exist positive numbers where , such that the iteration mappings can be written as
[TABLE]
On the one hand, from the Definition 74 of and , we get
[TABLE]
Similarly
[TABLE]
Let
[TABLE]
Hence
[TABLE]
On the other hand, since , for , then consider the sequence of tuples
[TABLE]
and recall the definition of from Eq.(21) of Definition 94:
[TABLE]
We distinguish three cases depending on the iteration mappings .
- (a)
If then , and and hence . In this case
and , and hence . Therefore, in this case showing Eq.(71) amounts to show that
[TABLE]
- (b)
If then , and and hence . With similar reasoning, in this case we need to show that
[TABLE]
- (c)
If and then and . In this case showing Eq.(71) amounts to show
[TABLE]
That is,
[TABLE]
It follows from Item (ii) of Fact 92 that to show Eq.(71) it suffices to show that
[TABLE]
Summing up these three cases, to show Eq.(71) it suffices to assume that and to show
[TABLE]
Let be a fixed-point -strategy. Indeed, appears times in and let be the greatest such that . Since is by definition a fixed-point -strategy, then it can be written as , for some and for some -strategy . To show Eq.(72), is suffices to show that either
- (i)
and in this case , or 2. (ii)
and in this case .
The proof is by induction on . For the base case , we claim that is a fixed-point -strategy because otherwise which contradicts the assumption . Hence let . Recall that for . In this case it follows from Eq.(64) of Item 2 of Lemma 90 that and that for any . That is, , and for any .
- (i)
If , i.e. , then . 2. (ii)
If , i.e. , then in this case .
For the induction step assume that the claim holds for and let us prove it for .
- (1)
If , then by the induction hypothesis . Besides, from Eq.(64) of Item 2 of Lemma 90 we have that .
- (i)
If , i.e. , then in this case we have . 2. (ii)
If , i.e. , then in this case we have . 2. (2)
If , then by the induction hypothesis . Besides, from Eq.(64) of Item 2 of Lemma 90 we have that .
- (i)
If , i.e. , then in this case we have . 2. (ii)
If , i.e. and , then in this case we have . 2. 2.
To show Eq.(70), assume that , the case where is similar. Let
[TABLE]
Recall from Eq.(25) of Definition 94 of that
[TABLE]
We want to show that . If then , hence the claim trivially holds. If then \mathbf{D^{\star}}(\mathbf{T}_{m})=\min\big{\{}\mathbf{D^{\star}}(\mathbf{T}_{m-1}),d^{\star}(\mathbf{s}_{1},\mathbf{s}_{m})\big{\}} and in this case we distinguish two cases depending on . If then , and , thus . Therefore, . If then in this case , which is obviously greater or equal to \min\big{\{}\mathbf{D^{\star}}(\mathbf{T}_{m-1}),d^{\star}(\mathbf{s}_{1},\mathbf{s}_{m})\big{\}}.
Lemma 102
Let
[TABLE]
be a sequence in . Define to be the (unique) -strategy satisfying
[TABLE]
We have that
[TABLE]
Proof. The idea of the proof is to show that either (i) both and result from the unification of the same -strategy with another -strategy, i.e. and in this case we know from Lemma 64 that there is at least one jump between the root of and . Or, (ii) and result from the unification of different -strategies, i.e. . In this case there must be a -strategy that lies in between and such that . Hence there is at least one jump between the root of and , and therefore there is at least one jump between the root of and . We need the two following claims, where Claim 103 is used to prove Claim 104 which will be used to prove this Lemma.
Claim 103
Consider a sequence : in where is the root of , with . For any , if there are two -strategies such that then is not in .
Proof. Assume that there are only two -strategies and such that . The case where there are more than two can be handled similarly. Indeed, there is a -strategy in on which the number of occurences of (resp. or ) has reached the maximum while that of (resp. ) did not. More precisely, there is such that either or . Assume that the first case holds since the second case can be handled similarly. Recall that since . Towards a contradiction: assume that is in . If then by Item (4) of Remark 101 we have , which is a contradiction. If is not in then by Item (3) of Remark 101 we have , which is a contradiction. This ends the proof of Claim 103.
Claim 104
Let and be two -strategies in where . If then the sequence in that lies between and is not empty, and there exists a -strategy in this sequence such that .
Proof. Assume that and . Let (resp. ) be the sequence in from the root of to (resp. to ). By Item (4) of Remark 101 we have . However, either there is at least one -strategy, say , in in the sequence between and such that , or . But this second possibility is not possible, since otherwise, by Claim 103 we would have had that is not in which contradicts the assumption of the current claim. This ends the proof of Claim 104.
To prove Lemma 102 we distinguish two cases depending whether the sequence in that lies between and is empty or not. Let be such sequence. If is empty, then if follows from Claim 104 that . This means that during the unification process, the same -strategy which is a sub--strategy of or appeared twice, which implies that there is a position jump between and . Or more formally, it follows from Lemma 64 that . Otherwise, if the sequence is not empty then from Claim 104 it follows that there is a -strategy in such that . Since is a sub--strategy of , then there is a unique -strategy such that . Thus by using the same Lemma 64 we deduce that . But since is a sub--strategy of , then is a sub--strategy of and hence as well. This ends the proof of Lemma 102.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] B. Yang, W. Belkhir, M. Lenczner, Computer-aided derivation of multi-scale models: A rewriting framework, International Journal for Multiscale Computational Engineering. 12 (2) (2014) 91–114.
- 2[2] W. Belkhir, A. Giorgetti, M. Lenczner, A symbolic transformation language and its application to a multiscale method, Journal of Symbolic Computation 65 (2014) 49–78.
- 3[3] W. Belkhir, N. Ratier, D. D. Nguyen, B. Yang, M. Lenczner, F. Zamkotsian, H. Cirstea, Towards an automatic tool for multi-scale model derivation illustrated with a micro-mirror array , in: SYNASC 2015, IEEE Computer Society, 2015, pp. 47–54. URL https://hal.inria.fr/hal-01243204
- 4[4] N. Charalambakis, Homogenization techniques and micromechanics. A survey and perspectives, Applied Mechanics Reviews 63 (3) (2010) 030803.
- 5[5] B. Yang, W. Belkhir, M. Lenczner, A. Giorgetti, R. Dhara, Computer–aided multiscale model derivation for MEMS arrays. , EUROSIM 2011, IEEE Computer Society, 6 pages. (2011). URL https://members.femto-st.fr/sites/femto-st.fr.michel-lenczner/files/content/conferences/Eurosim E 2011-Yan Bel.pdf
- 6[6] M. Lenczner, R. C. Smith, A two-scale model for an array of AFM’s cantilever in the static case, Mathematical and Computer Modelling 46 (5-6) (2007) 776–805.
- 7[7] W. Belkhir, N. Ratier, D. D. Nguyen, M. Lenczner, Unification and combination of iterative insertion strategies with rudimentary traversals and failure , Co RR abs/1904.10901 (2019). ar Xiv:1904.10901 . URL http://arxiv.org/abs/1904.10901
- 8[8] A. Arnold, D. Niwiński, Rudiments of μ 𝜇 \mu -calculus, Studies in logic and the foundations of mathematics, London, Amsterdam, 2001.
