Logical Methods in Computer Science
Vol. 13(4:16)2017, pp. 1–54
www.lmcs-online.org

Submitted May 31, 2016
Published Nov. 28, 2017

FAITHFUL (META-)ENCODINGS OF PROGRAMMABLE STRATEGIES
INTO TERM REWRITING SYSTEMS ∗
HORATIU CIRSTEA, SERGUEÏ LENGLET, AND PIERRE-ETIENNE MOREAU
Université de Lorraine, CNRS, LORIA, UMR 7503, F-54506 Vandœuvre-lès-Nancy, France
e-mail address: {firstname.lastname@loria.fr}

Abstract. Rewriting is a formalism widely used in computer science and mathematical
logic. When using rewriting as a programming or modeling paradigm, the rewrite rules
describe the transformations one wants to operate and rewriting strategies are used to
control their application. The operational semantics of these strategies are generally
accepted and approaches for analyzing the termination of specific strategies have been
studied. We propose in this paper a generic encoding of classic control and traversal
strategies used in rewrite based languages such as Maude, Stratego and Tom into a plain
term rewriting system. The encoding is proven sound and complete and, as a direct
consequence, established termination methods used for term rewriting systems can be
applied to analyze the termination of strategy controlled term rewriting systems. We show
that the encoding of strategies into term rewriting systems can be easily adapted to handle
many-sorted signatures and we use a meta-level representation of terms to reduce the size
of the encodings. The corresponding implementation in Tom generates term rewriting
systems compatible with the syntax of termination tools such as AProVE and TTT2, tools
which turned out to be very effective in (dis)proving the termination of the generated term
rewriting systems. The approach can also be seen as a generic strategy compiler which can
be integrated into languages providing pattern matching primitives; experiments in Tom
show that applying our encoding leads to performances comparable to the native Tom
strategies.

1. Introduction
Term rewriting is a very powerful tool used in theoretical studies as well as for practical
implementations. It is used, for example, in order to describe the meaning of programming
languages [30, 35], and also to describe by inference rules a logic [19], a theorem prover [25],
or a constraint solver [24]. Besides its use for specifying and implementing such formalisms,
it is also used as an underlying computation mechanism in systems like Mathematica [42],
Maude [9], or Tom [31, 4], where rewrite rules are objects of the language: they can be
defined by the user and manipulated by other constructs.
Rewrite rules, the core concept in term rewriting, consist of a pattern that describes a
schematic situation and the transformation that should be applied in that particular case.
Key words and phrases: Programmable strategies, termination, term rewriting systems.
This is an extension of “A faithful encoding of programmable strategies into term rewriting systems”
presented at RTA 2015.
∗

l

LOGICAL METHODS
IN COMPUTER SCIENCE

c
DOI:10.23638/LMCS-13(4:16)2017

CC

H. Cirstea, S. Lenglet, and P.-E. Moreau
Creative Commons

2

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

For example, the following set of rewrite rules specify how to transform a Boolean expression
into its corresponding disjunctive normal form (DNF):
and(or(x, y), z) _ or(and(x, z), and(y, z))
and(z, or(x, y)) _ or(and(z, x), and(z, y))

The left-hand side of each rule, i.e. its pattern, expresses a potentially infinite number of
expressions on which the rule can be applied; these expressions are obtained by instantiating
the variables x, y, z with arbitrary Boolean expressions. The application of the rewrite
rule is decided using a (matching) algorithm which only depends on the pattern and on
the term it is applied on, and not on the context in which it is applied. Given a term,
a rewrite rule can be thus potentially applied on any of its sub-terms. The expression
and(or(P, Q), and(or(P, Q), R)) where P, Q, R are atoms (constants) of the language, is transformed either into or(and(P, and(or(P, Q), R)), and(Q, and(or(P, Q), R))), if we applied the first
rule on the whole term, or into and(or(P, Q), or(and(P, R), and(Q, R))) if we apply it on the
and sub-term. The latter term can be further reduced in two different ways depending on
whether we apply the first or the second rule. Such sets of rewrite rules, called term rewriting
systems (TRS), are thus very convenient for describing schematically the transformations
one wants to operate.
In many situations, the application of a set of rewrite rules to a term eventually leads
to the same final result independently on the way the rules are applied, and in such cases
we say that the rewrite rules are confluent and terminating. This is for example the case
for the above two rules. When using rewriting as a programming or modeling paradigm, it
is nevertheless common to consider TRS that are non-confluent or non-terminating. For
example, if we want to compute not only DNF but also conjunctive normal forms the
following two rules could be added to the previous TRS:
or(and(x, y), z) _ and(or(x, z), or(y, z))
or(z, and(x, y)) _ and(or(z, x), or(z, y))

The resulting TRS is clearly non-terminating since we can have an infinite number of rule
applications: or(and(P, Q), R) rewrites into and(or(P, R), or(Q, R)), which in turn rewrites
into or(and(P, or(Q, R)), and(R, or(Q, R))), and we can go on like this forever. The problem
clearly comes here from the interference between the two sets of rules and there are several
solutions to tackle this problem [40].
In a programming context, we can imagine that these rules are separated in different
modules; this solves the termination problem but we could end up with a multitude of small
modules if the problem occurs for several sets of rules. Another more general solution is
functionalization [40] which consists in introducing some new function symbols and use them
to implicitly guide the application of the rewrite rules modified accordingly. If we use now
the symbol at to represent atoms, we can compute the DNF of a Boolean expression e by
applying the following TRS on DNF(e):
DNF(at(x)) _ at(x)
DNF(and(x, y)) _ DNFr(and(DNF(x), DNF(y)))
DNF(or(x, y)) _ or(DNF(x), DNF(y))
DNFr(and(or(x, y), z)) _ or(DNF(and(x, z)), DNF(and(y, z)))
DNFr(and(z, or(x, y))) _ or(DNF(and(z, x)), DNF(and(z, y)))
DNFr(and(at(x), at(y))) _ and(at(x), at(y))

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

3

The rules for DNF simulate the innermost normalization strategy by recursively traversing
terms while the rules for DNFr are used to encode the distribution. However, for each new
transformation, like, e.g., computing the conjunctive normal forms, new symbols should
be introduced and new rules for these symbols should be defined. Moreover, if we extend
our grammar of Boolean expressions with new symbols, like for example negation not and
implication imp, then new rewrite rules should be added for traversing the corresponding
terms or for defining the base cases. Thus, this approach not only leads to a TRS with
considerably more rules than the original one, but they are also more difficult to understand
and to reuse.
The functionalization approach encodes an order on the application of rules and gives an
explicit specification on how to traverse symbols. Rewriting strategies allow one to specify
which rules should be applied and where in the term without having to write explicitly in
the rewrite rules how to perform this control. Rule-based languages like Elan [6], Maude,
Stratego [39], or Tom provide elementary rewriting strategies and allow the programmer
to define its own strategies thanks to a specific strategy language. These user-defined
strategies are usually called programmable strategies [40]. All these languages thus clearly
distinguish between what we want to transform (the data structures), how to transform
them (the rewrite rules), and how to control the application of these transformations (the
programmable strategies).
Rewriting strategies may or may not change the semantics of the TRS they are controlling.
If the TRS is terminating and confluent, imposing a reduction strategy would always lead to
the same result, but the number of alternative reductions to get to this result is possibly
smaller than for the uncontrolled TRS. Imposing an order on the (application of) the rules
may reduce the number of alternative reductions even further. For example, if we extend the
TRS computing the DNF with some simplification rules for Boolean expressions, we could give
a higher priority to the application of some specific rules like, e.g. and(x, false) _ false,
to obtain shorter reductions. When the underlying TRS is non-confluent or non-terminating,
the rewriting strategy could change its original semantics. The TRS consisting of the first
four rules in this section is non-terminating, but when controlled by a strategy which applies
in an innermost way only the first two rules, the termination is retrieved. Rewriting strategies
can be also used to specify some default rules which are applied only when the others are
not applicable. For example, if we replace the last rule in the TRS defining DNF with the
more general rule DNFr(and(x, y)) _ and(x, y) the TRS would become non-confluent, but
we can recover confluence by using a strategy which prioritizes the application of the other,
meaningful rules, and gives the lowest priority to the last one.
Similarly to plain TRS (i.e. TRS without strategy), it is interesting to guarantee that a
strategy-controlled TRS enjoys properties such as confluence and termination. Confluence
holds as long as the rewrite rules are deterministic (i.e. the corresponding matching
algorithm exhibits at most one solution) and all strategy operators are deterministic (or
a deterministic implementation is provided). Confluence is clearly lost when considering
non-deterministic strategies. Termination is more delicate and the normalization under
some specific strategy is usually guaranteed by imposing (sufficient) conditions on the
rewrite rules on which the strategy is applied. Such conditions have been proposed for
the innermost [2, 15, 38, 20], outermost [10, 37, 20, 34], context-sensitive [16, 1, 20], or
lazy [17] reduction strategies. Termination under programmable strategies has been studied
for Elan [13] and Stratego [26, 28]. In [13], the authors give sufficient conditions for the
termination of certain programmable strategies relying only on the rewrite rules involved

4

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

in the strategy. Since the proposed criterion is applicable only to a specific subclass
of programmable strategies and relies on a coarse-grained description of strategies, the
approach cannot be used to prove termination for many terminating strategies. In [26, 28],
the termination of some traversal strategies (such as top-down, bottom-up, innermost) is
proven, assuming the rewrite rules are measure decreasing for a notion of measure that
combines the depth and the number of occurrences of a specific constructor in a term.
Contributions. In this paper we describe a general approach consisting in translating
programmable strategies into plain TRS. The interest of this encoding that we show sound
and complete is twofold. First, termination analysis techniques [2, 22, 18] and corresponding
tools like AProVE [14] and TTT2 [27] that have been successfully used for checking the
termination of plain TRS can be used to verify termination in presence of rewriting strategies.
Confluence can be analyzed in a similar way. Second, the translation can be seen as a generic
strategy compiler and thus can be used as a portable implementation of strategies which
could be easily integrated in any language accepting a term representation for the objects it
manipulates and providing rewrite rules or at least pattern matching primitives.
This translation was introduced in [8]. We propose here two additional translations
which are intended to improve the efficiency and expressiveness of the approach. The number
of rewrite rules in the original encoding strongly depends on the considered signature;
we introduce a meta-level representation of terms allowing to abstract over the signature
leading thus to encodings whose number of rules is independent of the signature. We also
consider many-sorted signatures and we show how the original translation handling only
mono-sorted signatures can be adapted to generate well-sorted encodings executable in
languages offering this feature. In summary, given a strategy S, we present an unsorted
translation, a many-sorted one, as well as one working at meta-level, and we show that they
produce faithful, i.e. sound and complete, encodings of the original strategy.
The translations have been implemented in Tom and generate TRS which could be fed
into TTT2/AProVE for termination analysis or executed efficiently by Tom.
The paper is organized as follows. The next section introduces the notions of rewriting
system and rewriting strategy. Section 3 presents the translation of rewriting strategies into
rewriting systems (introduced in [8]), and in Sections 4 and 5, we describe the translations for
meta-level terms and sorted terms, respectively. In Section 6, we give some implementation
details and present experimental results. In the appendix, we provide detailed proofs of the
properties stated in the paper and, in particular, of the simulation theorem from [8].
2. Strategic rewriting
This section briefly recalls some basic notions of rewriting used in this paper; see [3, 36]
for more details on first order terms and term rewriting systems, and [41, 5] for details on
rewriting strategies and their implementation in rewrite based languages.
2.1. Term rewriting systems. A signature Σ consists of a finite set F of symbols together
with a function ar which associates to any symbol f its arity. We write F n for the subset of
symbols of arity n, and F + for the symbols of arity n > 0. Symbols in F 0 are called constants.
Given a countable set X of variable symbols, the set of first-order terms T (F, X ) is the
smallest set containing X and such that f (t1 , . . . , tn ) is in T (F, X ) whenever f ∈ F n and
ti ∈ T (F, X ) for i ∈ [1, n]. We write Var (t) for the set of variables occuring in t ∈ T (F, X ).

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

5

If Var (t) is empty, t is called a ground term; T (F) denotes the set of all ground terms.
A linear term is a term where every variable occurs at most once. A substitution σ is a
mapping from X to T (F, X ) which is the identity except over a finite set of variables (its
domain). A substitution extends as expected to a mapping from T (F, X ) to T (F, X ).
A position of a term t is a finite sequence of positive integers describing the path from
the root of t to the root of the sub-term at that position. We write ε for the empty sequence,
which represents the root of t, Pos(t) for the set of positions of t, and t|ω for the sub-term
of t at position ω ∈ Pos(t). Finally, t [s]ω is the term t with the sub-term at position ω
replaced by s.
A rewrite rule (over Σ) is a pair (l, r) ∈ T (F, X ) × T (F, X ) (also denoted l _ r) such
that Var (r) ⊆ Var (l) and a TRS is a set of rewrite rules R inducing a rewriting relation
over T (F), denoted by −→R and such that t −→R t0 iff there exist l _ r ∈ R, ω ∈ Pos(t),
and a substitution σ such that t|ω = σ(l) and t0 = t [σ(r)]ω . In this case, t|ω is a redex, l
matches t|ω , and σ is the solution of the corresponding matching problem. The reflexive
and transitive closure of −→R is denoted by −→
→R . In what follows, we generally use the
0
0
notation R • t −→
→ t to denote t −→
→R t . A TRS R is terminating if there exists no infinite
rewriting sequence t1 −→R t2 −→R . . . −→R tn −→R . . .
2.2. Rewriting strategies. Rewriting strategies allow one to specify how rules should
be applied. Classical strategies like innermost or outermost are considered often when
implementing or reasoning about strategy controlled rewriting, but it could be useful to
have more fine-grained strategies to control the application of rewrite rules. For example,
we sometimes need to apply a set of rules only once, without retrying to apply the rules on
the obtained result as with an innermost strategy. Consider a rule var(x) _ fresh(var(x)),
whose purpose is to indicate that every variable in the abstract syntax tree of a program
should be replaced by a corresponding fresh variable; to mark all the concerned variables it
is sufficient to apply the rule once on the corresponding leaves of the tree, and it is needless
to try the rule on upper positions in the tree or on the newly generated fresh variable. We
could then combine this strategy with another one in charge of handling these fresh variables.
Taking the same terminology as the one proposed by Elan and Stratego, a rewrite
rule is considered to be an elementary strategy, and a strategy is an expression built over a
strategy language.
The strategy language we consider in this paper consists of the main operators used
in Tom, Elan, and Stratego. Let Σ be a signature and XS be a set of strategy variables,
ranged over by X. In what follows, we use uppercase for strategy variables and lowercase
for term variables. We define the strategy language over Σ as follows:
S ::= Identity | Fail | l _ r | S; S | S ←
+ S | One(S) | All (S) | µX . S | X

where l _ r is any rewrite rule over Σ. We call the term to which the strategy is applied
the subject.
The recursion operator µX . S binds X in S; a strategy variable is said to be free if
it is not bound. We write FVarX (S) for the set of free variables of S. As usual, we work
modulo α-conversion and we adopt Barendregt’s “hygiene-convention”, i.e. free and bound
variables have different names.
Informally, the Identity strategy can be applied to any term without changing it, and
thus Identity always succeeds. Conversely, the strategy Fail always fails when applied to a
term. As mentioned above, a rewrite rule is an elementary strategy which is (successfully or

6

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

not) applied at the root position of its subject. By combining these elementary strategies,
more complex strategies can be built: we can apply sequentially two strategies, make a choice
between the application of two strategies, apply a strategy to one or to all the immediate
sub-terms of the subject, and apply recursively a strategy.
The application of a strategy to a subject may diverge because recursion, fail because
of the strategy Fail has been used or because a rewrite rule cannot be applied, or return a
(unique) result. We use the symbol Fail to signal failure, and we let u range over terms
and Fail. We implement recursion using a context Γ which maps variables to strategies;
its syntax is defined as Γ ::= | Γ; X : S. When writing a context X1 : S1 ; . . . ; Xn : Sn , we
omit the empty context , and we assume that the variables (Xi )1≤i≤n are pairwise distinct.
We write DomX (Γ) for the domain of Γ, defined as DomX ( ) = ∅, and DomX (Γ; X : S) =
DomX (Γ) ∪ {X}. We define the evaluation judgment Γ ` S ◦ t =⇒ u inductively by the
rules of Figure 1; it means that the application of the strategy S to the subject t produces
the result u under the context Γ (the context may be omitted if empty). The semantics
being defined inductively and in a big-step style, there is no derivation for Γ ` S ◦ t if the
application of S to t diverges (e.g. if S = µX . X). There is also no derivation if a free
variable X of S is applied to a term and X ∈
/ DomX (Γ).
We distinguish between three kinds of operators in the strategy language:
• elementary strategies consisting of Identity, Fail , and rewrite rules, which are the basic
building blocks for strategies;
• control combinators consisting of choice S1 ←
+ S2 , sequence S1 ; S2 , and recursion µX . S,
that compose strategies but are still applied at the root position of the subject;
• traversal combinators One(S) and All (S) that modify the current application position.
We stress that a rewrite rule taken as an elementary strategy is not applied at every possible
position of a subject, but only at the root position, as we can see with the following example.
Example 2.1. Let Σ be the signature corresponding to Peano natural numbers such that
F 0 = {Z}, F 1 = {S}, and F 2 = {+}, and consider the rewrite rule +(Z, x) _ x. Then, we
have ` +(Z, x) _ x ◦ +(Z, S(Z)) =⇒ S(Z), but ` +(Z, x) _ x ◦ S(+(Z, Z)) =⇒ Fail, because
the rule cannot be applied at the root position in the second case. Similarly, only the redex
at the root position is reduced in ` +(Z, x) _ x ◦ +(Z, +(Z, S(Z))) =⇒ +(Z, S(Z)).

Control combinators are also applied at the root position. The (left-)choice S1 ←
+ S2 tries
to apply S1 and considers S2 only if S1 fails. Using this operator, we can then define a strategy
Try(S) which tries to apply S and applies the identity if S fails: Try(S) = S ←
+ Identity.
Given a set of rules R1 , . . . , Rn , the strategy R1 ←
+ (· · · ←
+ Rn ) can be used to express an
order on the rules, mirroring how pattern matching is done in most functional programming
languages. The sequential application S1 ; S2 succeeds if S1 succeeds on the subject and S2
succeeds on the subsequent term; it fails if one of the two strategy applications fails. We
consider these two operators to be right-associative, so that S1 ←
+ (S2 ←
+ S3 ) is written
S1 ←
+ S2 ←
+ S3 and S1 ; (S2 ; S3 ) is written S1 ; S2 ; S3 .
Example 2.2. We can apply sequentially twice the rewrite rule +(Z, x) _ x using the
strategy +(Z, x) _ x; +(Z, x) _ x. As we have seen in Example 2.1, the rule +(Z, x) _ x
applied once to +(Z, +(Z, S(Z))) gives +(Z, S(Z)), and since the rule can then be applied again
at the root position, we eventually obtain S(Z) as a final result:
(r1 )

(r1 )

` +(Z, x) _ x ◦ +(Z, +(Z, S(Z))) =⇒ +(Z, S(Z))
` +(Z, x) _ x ◦ +(Z, S(Z)) =⇒ S(Z)
(seq1 )
` +(Z, x) _ x; +(Z, x) _ x ◦ +(Z, +(Z, S(Z))) =⇒ S(Z)

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

7

Elementary strategies

Γ ` Identity ◦ t =⇒ t

(id)

Γ ` Fail ◦ t =⇒ Fail

(fail)

∃σ, σ(l ) = t
(r1 )
Γ ` l _ r ◦ t =⇒ σ(r )

@σ, σ(l ) = t
(r2 )
Γ ` l _ r ◦ t =⇒ Fail
Control combinators
Γ ` S1 ◦ t =⇒ t0
(choice1 )
Γ ` (S1 ←
+ S2 ) ◦ t =⇒ t0

Γ ` S1 ◦ t =⇒ Fail
Γ ` S2 ◦ t =⇒ u
(choice2 )
Γ ` (S1 ←
+ S2 ) ◦ t =⇒ u

Γ ` S1 ◦ t =⇒ t0
Γ ` S2 ◦ t0 =⇒ u
(seq1 )
Γ ` (S1 ; S2 ) ◦ t =⇒ u
Γ; X : S ` S ◦ t =⇒ u
(mu)
Γ ` µX . S ◦ t =⇒ u

Γ ` S1 ◦ t =⇒ Fail
(seq2 )
Γ ` (S1 ; S2 ) ◦ t =⇒ Fail
Γ; X : S ` S ◦ t =⇒ u
(muvar)
Γ; X : S ` X ◦ t =⇒ u

Traversal combinators
∃i ∈ [1, n], (Γ ` S ◦ ti =⇒ t0i ∧ ∀j ∈ [1, i − 1], Γ ` S ◦ tj =⇒ Fail)
(one1 )
Γ ` One(S) ◦ f (t1 , . . . , tn ) =⇒ f (t1 , . . . , ti−1 , t0i , ti+1 , . . . , tn )
∀i ∈ [1, n], Γ ` S ◦ ti =⇒ Fail
(one2 )
Γ ` One(S) ◦ f (t1 , . . . , tn ) =⇒ Fail
∀i ∈ [1,n], Γ ` S ◦ ti =⇒ t0i
(all1 )
Γ ` All (S) ◦ f (t1 , . . . , tn ) =⇒ f (t01 , . . . , t0n )
∃i ∈ [1,n], Γ ` S ◦ ti =⇒ Fail
(all2 )
Γ ` All (S) ◦ f (t1 , . . . , tn ) =⇒ Fail
Figure 1: Strategy semantics; t and its indexed and primed versions denote terms (which
cannot be Fail), whereas u denotes a result which is either a well-formed term, or Fail.
However, the application of the same strategy on the term +(Z, S(+(Z, Z))) fails because the
first application produces S(+(Z, Z)), on which we cannot apply the rule again:
(r1 )

(r2 )

` +(Z, x) _ x ◦ +(Z, S(+(Z, Z))) =⇒ S(+(Z, Z))
` +(Z, x) _ x ◦ S(+(Z, Z)) =⇒ Fail
(seq2 )
` +(Z, x) _ x; +(Z, x) _ x ◦ +(Z, S(+(Z, Z))) =⇒ Fail
We can avoid failure using the strategy Try(+(Z, x) _ x; +(Z, x) _ x) which represents in
fact the strategy (+(Z, x) _ x; +(Z, x) _ x) ←
+ Identity. If we denote T the above derivation

8

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

tree, we obtain the following evaluation when applying the T ry strategy:
(id)

` Identity ◦ +(Z, S(+(Z, Z))) =⇒ +(Z, S(+(Z, Z)))
T
(choice2 )
` Try(+(Z, x) _ x; +(Z, x) _ x) ◦ +(Z, S(+(Z, Z))) =⇒ +(Z, S(+(Z, Z)))

Note that the resulting term is the initial subject, not the intermediate term S(+(Z, Z))
responsible for the failure. To obtain this intermediate term, we should have applied
Try(+(Z, x) _ x); Try(+(Z, x) _ x) to the subject.
The application of a recursive strategy µX . S to a subject t applies S to t in a context
where X is mapped to S (rule mu). During this evaluation, the strategy variable X may
be applied to a term t0 , triggering the application of S to t0 (rule muvar), allowing thus
recursion. For the recursion to stop, the evaluation of S should not involve X anymore at
some point, otherwise the application of µX.S to t diverges. For example, the strategy µX.X
always diverges when applied to any subject, and we cannot derive any evaluation judgment
for it. A more interesting example of recursive strategy is Repeat(S) = µX . Try(S; X)
which applies a strategy S as much as possible at the root position of the subject. The
last successful result of the application of S is the overall result of Repeat(S). Note that
applying a Repeat strategy either diverges or evaluates to a term (and not to Fail).

Example 2.3. To see how recursion works, let us build the derivation tree for the application of the strategy Repeat(+(Z, x) _ x) = µX . Try(+(Z, x) _ x; X) to the term
t = +(Z, +(Z, S(Z))). To evaluate this application we necessarily start by applying the
rule (mu), which adds to the context the mapping of X to Try(+(Z, x) _ x; X) and triggers
the evaluation of this latter strategy. Thus, supposing the derivation tree can be eventually
built then, it has the shape
..
.
X : Try(+(Z, x) _ x; X) ` Try(+(Z, x) _ x; X) ◦ +(Z, +(Z, S(Z))) =⇒ u
(mu)
` µX . Try(+(Z, x) _ x; X) ◦ +(Z, +(Z, S(Z))) =⇒ u

The subsequent evaluations in this derivation tree are performed w.r.t. this context
Γpz = X : Try(+(Z, x) _ x; X). In order to apply the strategy Try(+(Z, x) _ x; X) =
+(Z, x) _ x; X ←
+ Identity to t, we have to decide between the two choice rules; in both
cases, we have to apply the strategy +(Z, x) _ x; X, and subsequently the rewrite rule
+(Z, x) _ x, to t. This rewrite rule succeeds when applied at the root position of t, and thus
the derivation tree has the form:
T1
(r1 )
(muvar)
Γpz ` +(Z, x) _ x ◦ +(Z, +(Z, S(Z))) =⇒ +(Z, S(Z))
Γpz ` X ◦ +(Z, S(Z)) =⇒ u
(seq1 )
Γpz ` +(Z, x) _ x; X ◦ +(Z, +(Z, S(Z))) =⇒ u
(choice1 )
Γpz ` Try(+(Z, x) _ x; X) ◦ +(Z, +(Z, S(Z))) =⇒ u
(mu)
` µX . Try(+(Z, x) _ x; X) ◦ +(Z, +(Z, S(Z))) =⇒ u

with T1 the derivation tree for the judgment Γpz ` Try(+(Z, x) _ x; X) ◦ +(Z, S(Z)) =⇒ u
obtained by instantiating the variable X with the corresponding strategy from the context.
We can apply the same reasoning as above, and since the rewrite rule +(Z, x) _ x also

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

9

succeeds on the new term +(Z, S(Z)), the derivation tree T1 has the following shape:
Γpz

T2
(muvar)
` +(Z, x) _ x ◦ +(Z, S(Z)) =⇒ S(Z)
Γpz ` X ◦ S(Z) =⇒ u
(seq1 )
Γpz ` +(Z, x) _ x; X ◦ +(Z, S(Z)) =⇒ u
(choice1 )
Γpz ` Try(+(Z, x) _ x; X) ◦ +(Z, S(Z)) =⇒ u
(r1 )

with T2 the derivation tree for the judgment Γpz ` Try(+(Z, x) _ x; X) ◦ S(Z) =⇒ u obtained,
as before, by instantiating accordingly the variable X. The rewrite rule +(Z, x) _ x fails
when applied to the term S(Z) and the derivation tree T2 is therefore as follows:
(r2 )

Γpz ` +(Z, x) _ x ◦ S(Z) =⇒ Fail
(seq2 )
(id)
Γpz ` +(Z, x) _ x; X ◦ S(Z) =⇒ Fail
Γpz ` Identity ◦ S(Z) =⇒ S(Z)
(choice2 )
Γpz ` Try(+(Z, x) _ x; X) ◦ S(Z) =⇒ S(Z)

This completes the derivation tree, and we can thus conclude that the result of applying the
strategy Repeat(+(Z, x) _ x) to the term +(Z, +(Z, S(Z))) is u = S(Z).

So far, the strategies are applied only at the root position; we use traversal combinators
to move to other positions. The strategy One(S) tries to apply S to a sub-term of the
subject, starting from the leftmost one (rule one1 ). If S fails on all the sub-terms, then
One(S) also fails (rule one2 ). In contrast, All (S) applies S to all the sub-terms of the
subject (rule all1 ) and fails if S fails on one of them (rule all2 ). Note that One(S) always
fails when applied to a constant while All (S) always succeeds in this case.
Example 2.4. In ` One(+(Z, x) _ x) ◦ +(+(Z, Z), +(Z, S(Z))) =⇒ +(Z, +(Z, S(Z))), only the
first sub-term is reduced, while in ` All (+(Z, x) _ x) ◦ +(+(Z, Z), +(Z, S(Z))) =⇒ +(Z, S(Z)),
they are both reduced. These operators give access only to the immediate sub-term: we
have ` One(+(Z, x) _ x) ◦ S(S(+(Z, Z))) =⇒ Fail, and similarly with All .
Combined with recursion, traversal combinators can be used to have access to any
position of a term. In fact, most of the classic reduction strategies can be defined using
recursion and traversal operators:
OnceBottomUp(S)
BottomUp(S)
OnceTopDown(S)
TopDown(S)

=
=
=
=

µX . One(X) ←
+S
µX . All (X); S
µX . S ←
+ One(X)
µX . S; All (X)

OnceBottomUp (denoted obu in the following) tries to apply a strategy S once, starting
from the leftmost-innermost leaves. BottomUp behaves almost like obu except that S is
applied to all nodes, starting from the leaves. OnceTopDown and TopDown are similar,
except they start from the root position. The strategy which applies S as many times as
possible, starting from the leaves can be either defined naively as Repeat(OnceBottomUp(S))
or using a more efficient approach [41]: Innermost(S) = µX . All (X); Try(S; X).
Example 2.5. We use OnceTopDown, OnceBottomUp, and Innermost, when applying S =
+(Z, x) _ x ←
+ +(S(x), y) _ S(+(x, y)) to t = +(+(Z, Z), +(S(Z), Z)). With OnceTopDown(S),
we start at the root position of t and since there is no redex at this position, we recursively try to apply S to one of its children: we can apply it on the first child and obtain
+(Z, +(S(Z), Z)). If we apply OnceTopDown(S) on this latter term we obtain +(S(Z), Z). With

10

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

OnceBottomUp(S), we start from the leaves, and we obtain the same term +(Z, +(S(Z), Z))
as before but if we apply OnceBottomUp(S) once again on this term we obtain now
+(Z, S(+(Z, Z))). Innermost(S) also starts from the leaves but makes a recursive call after each application of S, so we obtain ` Innermost(S) ◦ t =⇒ S(Z).
Both BottomUp(S) and TopDown(S) fail on t but we have ` BottomUp(Try(S)) ◦ t =⇒
S(+(Z, Z)) and ` TopDown(Try(S)) ◦ t =⇒ +(Z, S(Z)).
Remark 2.6. The semantics of One is deterministic, as it looks for the leftmost sub-term
that can be successfully transformed; a non-deterministic behavior can easily be obtained
by removing the second condition in the premises of the inference rule one1 . Similarly, we
can adopt a non-deterministic semantics for S1 ←
+ S2 , where either S1 or S2 is tried first,
by removing the first judgment in the premises of the inference rule choice2 . We focus
here on the encoding of the deterministic semantics but we also explain in the next section
(Remark 3.4) how our encoding can be adapted to handle the non-deterministic versions of
One and choice.
Given this semantics, we can define a notion of termination for strategies.
Definition 2.7. Let S, Γ such that FVarX (S) ⊆ DomX (Γ). The strategy S is terminating
under Γ if for all t ∈ T (F), there exists u such that Γ ` S ◦ t =⇒ u.
The condition on the variables of S and Γ ensures that if there is no derivation for Γ ` S ◦ t,
this is not because a free variable of S does not occur in the domain of Γ. If FVarX (S) = ∅,
then Γ does not play a role in the derivation, and we simply say that S is terminating as a
shorthand for S is terminating under any context. Note that we allow terminating strategies
to fail, as u can be Fail. A terminating strategy may contain non-terminating rewrite
rules: the strategy Z _ +(Z, Z) is terminating because the rule is applied once at the root
position (and either succeeds or fails). However, Innermost(Z _ +(Z, Z)) is not terminating.
A terminating strategy may also contain a non-terminating strategy: Identity ←
+ µX . X is
terminating because the diverging part µX . X is never applied.
3. Encoding rewriting strategies with rewrite rules
We translate a strategy into a faithful TRS, in the sense that a strategy applied to a term
produces a result iff the TRS also rewrites the encoded term into the encoded result.
3.1. Strategy translation. The evaluation of the application of a strategy S on a term t
consists in selecting and applying the corresponding sub-strategies of S to t when the head
operator of S is a control combinator (e.g. selecting S1 in S1 ←
+ S2 in the inference rule
choice1 ), in applying S on the corresponding sub-terms of t when the head operator of S is a
traversal combinator (e.g. applying S on the sub-term ti of f (t1 , . . . , tn ) in the inference rule
one1 ), and eventually in applying elementary strategies. The translation function presented
in Figure 2 associates to each strategy a set of rewrite rules which encodes exactly this
behaviour and preserves the original evaluation: T(S) • ϕS (t) −→
→ t0 whenever ` S ◦ t =⇒ t0
(the exact relationship between a strategy and its encoding is formally stated in Section 3.2).
Since the application of the rewrite rules of the encoding cannot be explicitly controlled,
the first issue is to ensure that only the rules of the appropriate (sub-)strategy can be applied
to the current subject, and that an encoded strategy is applied to the right sub-term(s)
in the case of traversal combinators. The other difficulties concern the representations of

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

11

contexts Γ, as well as of (matching and strategy) failures, since these notions are not explicit
in plain term rewriting. To deal with the first problem, we introduce some symbols ϕ used
to implicitly control the application of the rewrite rules encoding a strategy. The set T(S)
thus contains rules whose left-hand sides are headed by a symbol ϕS and which encode the
behaviour of the strategy S by using, in the right-hand sides, the symbols ϕ corresponding
to the sub-strategies of S and potentially some auxiliary symbols. All these symbols are
supposed to be freshly generated and uniquely identified, i.e. there will be only one ϕS
symbol for each encoded (sub-)strategy S and each auxiliary ϕ symbol can be identified
by the strategy it has been generated for. For example, in the encoding T(S1 ; S2 ), the
symbol ϕ; is just an abbreviation for ϕS; 1 ;S2 , i.e. the specific ϕ; used for the encoding of the
strategy S1 ; S2 .
In addition to these ϕ symbols, we also use a particular symbol ⊥ of arity 1 which
encodes failure and whose argument is used, as explained later on in this section, to keep
track of the term on which the strategy failed. For example, the fact that the strategy
Fail applied to t results in Fail corresponds in our encoding to the reduction of ϕFail (t)
w.r.t. T(Fail ) into ⊥(t). This additional information attached to a failure is particularly
helpful when encoding strategies where a sub-strategy is tried successively on different terms,
namely for the choice and for One.
Apart from the application of Fail , strategy failures only come from matching failures.
We have to be careful in encoding these failures since we should conclude that a matching
failure occurred only if the terms involved are built over the initial signature and contain no
generated symbols. For this we use the so-called anti-terms 1 of the form !t with t ∈ T (F, X )
or !⊥(x) with x ∈ X . An anti-term !t represents all the ground terms in T (F) which
do not match t and the anti-pattern !⊥(x) denotes all the ground terms t ∈ T (F) of the
original signature; the way the finite representation of these terms is generated is explained
in Section 6. For example, if we consider the signature from Example 2.1, !+(Z, x) denotes
exactly the terms matched by Z, S(x1 ), +(S(x1 ), x2 ), or +(+(x1 , x2 ), x3 ). We should emphasize
that in this encoding, the semantics of !t is considered w.r.t. the terms in T (F). For example,
!c for some constant c does not include ⊥(c) or terms of the form ϕ(t1 , . . . , tn ), because ⊥
and ϕ symbols do not belong to the original signature.
To keep the presentation of the translation compact and intuitive, we express it using
rule schemas involving anti-terms and a special aliasing symbol “@”: each rule in Figure 2
involving these notations represent in fact a set of rewrite rules. Anti-terms in the left-hand
sides of rules can be aliased with @ by variables which can be then conveniently used in
the right-hand sides of the corresponding rules. The rewrite rule l _ r with l, r such that
l|ω = x @ !u and r|ω0 = x, for some u ∈ T (F, X ) ∪ {⊥(x) | x ∈ X } and positions ω, ω 0 is
thus just an alias for the set of rewrite rules l [u1 ]ω _ r [u1 ]ω0 , . . . , l [un ]ω _ r [un ]ω0 , where
u1 , . . . , un are the terms represented by !u. Moreover, the variable symbol “ ” can be used
in the left-hand side of a rule to indicate a variable that does not appear in the right-hand
side.
For example, the rule schema ϕ(y @ !+(Z, )) _ ⊥(y) denotes the set of rewrite rules
consisting of ϕ(Z) _ ⊥(Z), ϕ(S(y1 )) _ ⊥(S(y1 )), ϕ(+(S(y1 ), y2 )) _ ⊥(+(S(y1 ), y2 )), and
ϕ(+(+(y1 , y2 ), y3 )) _ ⊥(+(+(y1 , y2 ), y3 )).
1We restrict here to a limited form of anti-terms; we refer to [7] for the complete semantics of anti-terms.

12

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

T(Identity) = { ϕIdentity (x @ !⊥( )) _ x,

(E1)

T(Fail ) = { ϕFail (x @ !⊥( )) _ ⊥(x),

(E2)

T(l _ r) = { ϕl_r (l) _ r,
ϕl_r (x @ !l) _ ⊥(x),

(E3)

ϕIdentity (⊥(x)) _ ⊥(x) }
ϕFail (⊥(x)) _ ⊥(x) }

ϕl_r (⊥(x)) _ ⊥(x) }

T(S1 ; S2 ) = T(S1 ) ∪ T(S2 )
S
{ ϕS1 ;S2 (x @ !⊥( )) _ ϕ; (ϕS2 (ϕS1 (x)), x), ϕS1 ;S2 (⊥(x)) _ ⊥(x),
ϕ; (x @ !⊥( ), ) _ x, ϕ; (⊥( ), x) _ ⊥(x) }

(E4)

T(S1 ←
+ S2 ) = T(S1 ) ∪ T(S2 )
S
{ ϕS1 ←
ϕS1 ←
+ (ϕS1 (x)),
+S2 (x @ !⊥( )) _ ϕ←
+S2 (⊥(x)) _ ⊥(x),
ϕ←
ϕ←
+ (⊥(x)) _ ϕS2 (x),
+ (x @ !⊥( )) _ x }

(E5)

(E6)

T(µX . S) = T(S)
S
{ ϕµX.S (x @ !⊥( )) _ ϕS (x), ϕµX.S (⊥(x)) _ ⊥(x),
ϕX (x @ !⊥( )) _ ϕS (x), ϕX (⊥(x)) _ ⊥(x) }
T(X) = ∅

(E7)
(E8)

T(All (S)) = T(S)
S
{ ϕAll(S) (⊥(x)) _ ⊥(x) }
S
{ ϕAll(S) (c) _ c }
c∈F
S0
{ ϕAll(S) (f (x1 , . . . , xn )) _ ϕf (ϕS (x1 ), . . . , ϕS (xn ), f (x1 , . . . , xn )),
f ∈F +

(E9)

ϕf (x1 @ !⊥( ), . . . , xn @ !⊥( ), ) _ f (x1 , . . . , xn ),
ϕf (⊥( ), , . . . , , x) _ ⊥(x),
..
.
ϕf ( , . . . , , ⊥( ), x) _ ⊥(x) }

T(One(S)) = T(S)
S
{ ϕOne(S) (⊥(x)) _ ⊥(x) }
S
{ ϕOne(S) (c) _ ⊥(c) }
c∈F
S0
{ ϕOne(S) (f (x1 , . . . , xn )) _ ϕf1 (ϕS (x1 ), x2 , . . . , xn ) }
f ∈F +
S
S
{ ϕfi (⊥(x1 ), . . . , ⊥(xi−1 ), xi @ !⊥( ), xi+1 , . . . , xn ) _ f (x1 , . . . , xn )}
+
f ∈F
S 1≤i≤ar(f
S )
{ ϕfi (⊥(x1 ), . . . , ⊥(xi ), xi+1 , . . . , xn ) _
f ∈F + 1≤i<ar(f )
ϕfi+1 (⊥(x1 ), . . . , ⊥(xi ), ϕS (xi+1 ), xi+2 , . . . , xn ) }
S
{ ϕfn (⊥(x1 ), . . . , ⊥(xn )) _ ⊥(f (x1 , . . . , xn )) }
f ∈F +

(E10)
(E11)

B(Γ; X : S) = B(Γ) ∪ T(S)
S
{ ϕX (x @ !⊥( )) _ ϕS (x),
B( ) = ∅

ϕX (⊥(x)) _ ⊥(x) }

Figure 2: Strategy translation.

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

13

The translation of the Identity strategy (E1) consists of a rule whose left-hand side
matches any term in the signature2 (contextualized by the corresponding ϕ symbol) and
whose right-hand side is the initial term, and of a rule encoding strict propagation of failure.
This latter rule guarantees a faithful encoding of the strategy guided evaluation and is in
fact present, in different forms, in the translations of all the strategy operators.
Example 3.1. If we consider the signature in Example 2.1, the following encoding is
obtained for the Identity strategy:
T(Identity) = { ϕIdentity (Z) _ Z,
ϕIdentity (S(y1 )) _ S(y1 ),
ϕIdentity (+(y1 , y2 )) _ +(y1 , y2 ),
ϕIdentity (⊥(x)) _ ⊥(x) }

Similarly, the translation of the Fail strategy (E2) contains a failure propagation rule, and
a rule whose left-hand side matches any term and whose right-hand side is a failure keeping
track of this term. A rewrite rule (which is an elementary strategy applicable at the root of
the subject) is translated (E3) by two rules encoding the behaviour in case of respectively a
matching success or a failure, together with a rule for failure propagation.
Example 3.2. The strategy Spz = +(Z, x) _ x is encoded by the following rules:
T(Spz ) = { ϕpz (+(Z, x)) _ x,
ϕpz (y @ !+(Z, x)) _ ⊥(y),
ϕpz (⊥(x)) _ ⊥(x) }
which lead, when the anti-terms are expanded w.r.t. to the signature, to the TRS:
T(Spz ) = { ϕpz (+(Z, x)) _ x,
ϕpz (Z) _ ⊥(Z),
ϕpz (S(y1 )) _ ⊥(S(y1 )),
ϕpz (+(S(y1 ), y2 )) _ ⊥(+(S(y1 ), y2 )),
ϕpz (+(+(y1 , y2 ), y3 )) _ ⊥(+(+(y1 , y2 ), y3 )),
ϕpz (⊥(x)) _ ⊥(x) }
The term ϕpz (+(Z, S(Z))) reduces w.r.t. this latter TRS to S(Z) and ϕpz (Z) reduces to ⊥(Z).
The translation of the sequential application of two strategies (E4) includes the translation of the respective strategies and some specific rules. A term ϕS1 ;S2 (t) is reduced by
the first rule into a term ϕ; (ϕS2 (ϕS1 (t)), t), which guarantees that the rules of the encoding
of S1 are applied before the ones of S2 . Indeed, a term of the form ϕ(t) can be reduced only
if t ∈ T (F) or t = ⊥( ) and thus, the rules for ϕS2 can be applied to a term ϕS2 (ϕS1 ( ))
only after ϕS1 ( ) is reduced to a term in T (F) (or failure). The original subject t is kept
during the evaluation (of ϕ; ), so that ⊥(t) can be returned if the evaluation of S1 or S2 fails
(i.e. produces a ⊥) at some point. If ϕS2 (ϕS1 (t)) evaluates to a term t0 ∈ T (F), then the
evaluation of ϕS1 ;S2 (t) succeeds, and t0 is the final result.
In a similar manner, the translation for the choice operator (E5) uses a first rule which
triggers the application of the rules for S1 . If we start with a term ϕS1 ←
+S2 (t) we first obtain
ϕ←
+ (ϕS1 (t)) and this latter term can be further reduced only after the reduction of ϕS1 (t) to
a term in the signature or to a failure. Recording the origin of the failure and propagating
it together with its origin is crucial here. The eventual failure for the reduction of ϕS1 (t)
can be thus detected and the original subject, i.e. the term t, can be retrieved and used to
trigger the rules for S2 on ϕS2 (t).
2The rule is in fact expanded into n rewrite rules with n the number of symbols in F.

14

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

The translation for a strategy µX . S (E6) triggers the application of the rules for S at
first, and then each time the symbol ϕX is encountered. As in all the other cases, failure is
strictly propagated. There is no rewrite rule for the translation of a strategy variable (E7)
but we should note that the corresponding ϕX symbol is used when the sub-strategy X is
reached during the translation of the strategy S (in µX . S).
Example 3.3. The strategy Srpz = µX . (+(Z, x) _ x ; X) ←
+ Identity which applies repeatedly (as long as possible) the rewrite rule from Example 3.2 is encoded by:
T(Srpz ) = { ϕrpz (x @ !⊥( )) _ ϕtpz (x),
∪ { ϕX (x @ !⊥( )) _ ϕtpz (x),
∪ { ϕtpz (x @ !⊥( )) _ ϕ←
+ (ϕpzX (x)),
ϕ←
+ (x @ !⊥( )) _ x,
∪ { ϕpzX (x @ !⊥( )) _ ϕ; (ϕX (ϕpz (x)), x),
ϕ; (x @ !⊥( ), ) _ x,
∪ T(Spz ) ∪ T(Identity)

ϕrpz (⊥(x)) _ ⊥(x) }
ϕX (⊥(x)) _ ⊥(x) }
ϕtpz (⊥(x)) _ ⊥(x),
ϕ←
+ (⊥(x)) _ ϕIdentity (x) }
ϕpzX (⊥(x)) _ ⊥(x),
ϕ; (⊥( ), x) _ ⊥(x) }

For presentation purposes, we separated the TRS in subsets of rules corresponding to the
translation of each operator occurring in the initial strategy. Note that the symbol ϕX used
in the rules for the inner sequence can be reduced with the rules generated to handle the
recursion operator. The term ϕrpz (+(Z, +(Z, S(Z)))) reduces w.r.t. the TRS to S(Z).
The rules encoding the traversal operators follow the same principle – the rules corresponding to the translation of the argument strategy S are applied, depending on the
traversal operator, to one or all the sub-terms of the subject. For the All operator (E8), if
the application of S to all the sub-terms succeeds (produces terms in T (F)), then the final
result is built using the results of each evaluation. If the evaluation of one of the sub-terms
produces a ⊥, a failure with the original subject as origin is returned as a result. Special
rules encode the fact that All applied to a constant always succeeds; the same behaviour
could have been obtained by instantiating the rules for non-constants with n = 0, but we
preferred an explicit approach for uniformity and efficiency reasons. The strict propagation
of failure together with its origin is essential in the case of the One operator (E9) since it
allows for a more economic encoding approach than the duplication of the original subject
used for the All operator. If the evaluation for one sub-term results in a failure, then the
evaluation of the strategy S is triggered on the next one and if S fails on all sub-terms, the
final result can be directly built using the origin of these failures which represent nothing
else than the original arguments. Note that the failure in case of constants is necessarily
encoded by specific rules.
Finally, each binding X : S of a context (E10) is translated by two rules, including the
one that propagates failure. The other rule operates as in the recursive case (E6): applying
the strategy variable X to a subject t leads to the application of the rules encoding S to t.
Remark 3.4. It is possible to adapt our encoding to a non-deterministic version of S1 ←
+ S2
and One(S) (cf Remark 2.6). For the choice combinator, the encoding becomes
Tnd (S1 ←
+ S2 ) = Tnd (S1 ) ∪ Tnd (S2 )
S
{ ϕS1 ←
ϕS1 ←
+ (ϕS1 (x), ϕS2 (x)),
+S2 (x @ !⊥( )) _ ϕ←
+S2 (⊥(x)) _ ⊥(x),
ϕ←
ϕ←
+ ( , x @ !⊥( )) _ x,
+ (x @ !⊥( ), ) _ x,
ϕ←
(⊥(x),
⊥(x))
_
⊥(x)
}
+

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

15

In this modified encoding, the subject t is duplicated so that the rules of Tnd (S1 ) can
be applied to ϕS1 (t) and those of Tnd (S2 ) to ϕS2 (t). If either copy rewrites into a term
t0 in T (F), then it can be selected as the final result by the rule ϕ←
+ (x @ !⊥( ), ) _ x
or its symmetric. If both of them could be eventually rewritten into the terms t01 , t02 in
T (F), the final result is either t01 or t02 depending on whether ϕ←
+ (x @ !⊥( ), ) _ x or
ϕ←
+ ( , x @ !⊥( )) _ x is applied first in the corresponding reduction.This non-deterministic
choice reflects the non-deterministic nature of the encoded strategy.
The encoding for the non-deterministic One follows the same idea.
S
S
Tnd (One(S)) = Tnd (S) { ϕOne(S) (⊥(x)) _ ⊥(x) }
{ ϕOne(S) (c) _ ⊥(c) }
0
c∈F
S
{ ϕOne(S) (f (x1 , . . . , xn )) _ ϕf (ϕS (x1 ), . . . , ϕS (xn ), f (x1 , . . . , xn )),
f ∈F +

ϕf (⊥( ), . . . , ⊥( ), x) _ ⊥(x),
ϕf (y @ !⊥( ), , . . . , , f (x1 , . . . , xn )) _ f (y, x2 , . . . , xn ),
..
.
ϕf ( , . . . , , y @ !⊥( ), f (x1 , . . . , xn )) _ f (x1 , . . . , xn−1 , y) }

The obtained encoding is similar to the one for All : the rules corresponding to the translation
S are triggered on all the sub-terms of the subject. We remember the original subject so it
can be returned as origin of an eventual failure, or to construct the final result with one of
the last n rules. Again, if the encoding of S succeeds on several sub-terms, different results
can be obtained depending on which of the last n rules is being applied.
3.2. Properties of the translation. The goal of the translation is twofold: use wellestablished methods and tools for plain TRS in order to prove properties of strategy
controlled rewrite rules, and offer a generic compiler for user defined strategies. For both
items, it is crucial to have a sound and complete translation, and this turns out to be true
in our case.
Theorem 3.5 (Simulation). Given a term t ∈ T (F), a strategy S and a context Γ such
that FVarX (S) ⊆ DomX (Γ),
(1) Γ ` S ◦ t =⇒ t0 iff T(S) ∪ B(Γ) • ϕS (t) −→
→ t0 , t0 ∈ T (F)
(2) Γ ` S ◦ t =⇒ Fail iff T(S) ∪ B(Γ) • ϕS (t) −→
→ ⊥(t)
Sketch. The completeness is shown by induction on the height of the derivation tree and
the soundness by induction on the length of the reduction. The base cases consisting of
the strategies with a constant length reduction – Identity, Fail , and the rewrite rule – are
straightforward to prove since, in particular, the translation of a rule explicitly encodes
matching success and failure. Induction is applied for all the other cases and the corresponding
proofs rely on some auxiliary properties.
First, the failure is strictly propagated: if B(Γ) ∪ T(S) • ϕS (⊥(t)) −→
→ u, then u = ⊥(t).
This is essential, in particular, for the sequence case where a failure of the first strategy
should be strictly propagated as the final result of the overall sequential strategy.
Second, terms in T (F) are in normal form w.r.t. the translation of any strategy and
terms of the form ϕS (t) are head-rigid w.r.t. strategies other than S, i.e., they can be
reduced at the head position only by the rules in T(S) and only if t is a term in the signature.
More precisely, if for a strategy S 0 and a context Γ, B(Γ) ∪ T(S 0 ) • ϕS (t) −→
→ u then t ∈ T (F)

16

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

and T(S) ⊆ B(Γ) ∪ T(S 0 ) (or S = X and X ∈ DomX (Γ)). This guarantees that the steps
in the strategy derivation are encoded accurately by the evaluations w.r.t. the rules in the
translation.
Finally, the origin of the failure is preserved in the sense that if for a t ∈ T (F), ϕS (t)
reduces to a failure, then the reduct is necessarily ⊥(t). This is crucial in particular for the
choice strategy: if the (translation of the) first strategy fails, then the (translation of the)
second one should be applied on the initial subject.
The main goal is to prove the termination of some strategy guided system by proving
the property for the plain TRS obtained by the translation. As a direct consequence of
Theorem 3.5, we obtain that the termination of the TRS encoding a strategy implies the
termination of the strategy.
Corollary 3.6 (Termination). Given a strategy S and a context Γ such that FVarX (S) ⊆
DomX (Γ), S terminates under Γ if T(S) ∪ B(Γ) is terminating.
Because of the modular encoding of strategies, the non-termination of the TRS does not
necessarily imply the non-termination of the original strategy, and could instead indicate
just the non-termination of one of its sub-strategies. Given the shape of the rewrite rules
in the encoding, an eventual non-terminating reduction could be always reduced to a nonterminating reduction of a term of the form ϕS (t) with ϕS encoding the behaviour of a substrategy S and t ∈ T (F). For example, the terminating strategies Fail ; µX . (Identity; X),
Identity ←
+ µX . (Identity; X), and a _ a; µX . (b _ b; X) use some non-terminating substrategies whose encodings are also non-terminating.
Note that even if the non-termination of the encoding reflects the non-termination
of the strategy, the counterexample exhibited (by an automatic tool) could concern only
a sub-strategy. For example, the strategy All (µX . (Identity; X)) is non-terminating because of its sub-strategy µX . (Identity; X) and an automatic tool would usually provide a
counterexample for (the encoding of) this latter strategy.
Another direct consequence of Theorem 3.5 is that the confluence of the strategy is
implied by the confluence of the corresponding encoding TRS.
Corollary 3.7 (Confluence). Given a strategy S and a context Γ such that FVarX (S) ⊆
DomX (Γ), if T(S) ∪ B(Γ) is confluent then, for any evaluation judgments Γ ` S ◦ t =⇒ u
and Γ ` S ◦ t =⇒ u0 we have u = u0 .
Moreover, the encoding of a deterministic strategy always leads to a confluent TRS:
Lemma 3.8. Given a strategy S and a context Γ such that FVarX (S) ⊆ DomX (Γ), the
TRS T(S) ∪ B(Γ) is confluent.
Sketch. We split T(S) ∪ B(Γ) into two TRS and show that they are both linear, confluent
and orthogonal to each other, i.e. there is no overlap between a rule from one and a rule
from the other. As a consequence, we have the confluence of T(S) ∪ B(Γ) [32].
4. Meta-encoding rewriting strategies with rewrite rules
The strategy translation of Section 3 generates a potentially large number of rewrite rules
essentially because of the way All and One are encoded, and this may impact the efficiency
of the corresponding implementation or prevent an automatic tool from deciding termination.

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

17

We propose in this section a meta-encoding of terms which allows for a more economic
encoding of strategies into rewrite rules.
4.1. Meta-level representation
of terms. The non-failure !⊥( ) has been encoded so
S
far by the set of terms f ∈F {f (x1 , . . . , xn )}, with ar(f ) = n, and thus all rule schemas
in Figure 2 using this construction are expanded into a number of rules proportional to
the number of symbols in the signature. The size of the encodings for All and One in the
translation depends also on the signature F, as the number of rules generated grows with
the number of symbols and with their arities. To avoid this potential explosion, we represent
terms in T (F) using a meta-level application and lists: roughly, we write f (t1 , . . . , tn ) as
appl(f, args), where args is the list of the meta-encoded arguments, and a constant c is
represented as appl(c, nil).
Formally, given a signature F, we define a meta-signature Fappl = {appl, ::, nil} ∪ {_f ^ |
f ∈ F} so that appl and :: are of arity 2, and nil and _f ^ are of arity 0 for all f ∈ F.
The symbols :: and nil are the usual building blocks for lists, and we use :: as a rightassociative infix operator, so that x1 :: (x2 :: nil) is written x1 :: x2 :: nil. Given a
term t ∈ T (F, X ), we define its meta-level encoding _t^ ∈ T (Fappl , X ) as _f (t1 , . . . , tn )^ =
appl(_f ^, _t1 ^ :: . . . :: _tn ^ :: nil), _c^ = appl(_c^, nil) if c ∈ F 0 , and _x^ = x if x ∈ X .
4.2. Strategy meta-encoding. Given the above meta-encoding of terms, we define a
translation TM of rewriting strategies on terms in T (F) into plain rewrite rules on terms
built from Fappl extended with a set of generated ϕ symbols, with the symbols ⊥, ⊥list
encoding failure, and with the symbols for lists manipulation presented in Figure 4. The
translations of the elementary strategies and of the control combinators are almost the same
as in Section 3, so we present in Figure 3 only the strategies whose encoding differs the most
from Figure 2, and we give the complete translation in Appendix 9 (Figure 6).
First, note that meta-encoded terms are of the form appl( , ), so instead of using
x @ !⊥( ) (as in the rule schemas in Figure 2) to filter all the ground terms of the original
signature, we directly use x @ appl( , ). As explained in the previous section, the rule
schemas relying on x @ !⊥( ) are expanded into a set of rewrite rules whose cardinality
depends on the original signature. By using the term x @ appl( , ) instead of this anti-term,
each set of rules represented by a rule schema in the original encoding is replaced by only one
rewrite rule in the meta-encoding. Consequently, the number of rules in the meta-encoding
can be significantly smaller than in the previous encoding.
We should point out that the meta-encoding of a rewrite rule (ME3) uses _!l^ and
not !_l^, meaning that we meta-encode the terms of T (F) that do not match l, instead of
considering all the terms of T (Fappl ) that do not match _l^. Indeed, Fappl is more expressive
than F since we can write terms appl(_f ^, args) where the size of args differs from the arity
of f in F. Such ill-formed terms are matched by !_l^, but not by _!l^; however, they do not
have to be considered since they are never produced during the evaluation of a meta-encoded
term w.r.t. a strategy meta-encoding (see Lemma 4.3). As a result, we generate as many
rules to represent this anti-pattern with the meta-encoding as with the original encoding.
Example 4.1. If we consider the signature in Example 2.1, the meta-encoding of the strategy
Spz = +(Z, x) _ x contains the same rules as in the regular encoding in Example 3.2, except

18

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

(ME3)
(ME8)

TM (l _ r) = { ϕl_r (_l^) _ _r^, ϕl_r (x @ _!l^) _ ⊥(x),
ϕl_r (⊥(x)) _ ⊥(x) }

TM (All (S)) = TM (S) ∪ L
S
{ ϕAll(S) (⊥(x)) _ ⊥(x),
ϕAll(S) (appl(f, args)) _ propag(appl(f, ϕlist
All(S) (args))),
list
0
ϕAll(S) (h :: q) _ ϕAll(S) (ϕS (h), q, h :: nil, nil),
ϕlist
All(S) (nil) _ nil,
0
ϕAll(S) (⊥( ), todo, r tried, ) _ ⊥list (rconcat(r tried, todo)),
ϕ0All(S) (x @ appl( , ), nil, , r done) _ rev(x :: r done),
ϕ0All(S) (x @ appl( , ), h :: q, r tried, r done) _
ϕ0All(S) (ϕS (h), q, h :: r tried, x :: r done) }

(ME9) TM (One(S)) = TM (S) ∪ L
S
{ ϕOne(S) (⊥(x)) _ ⊥(x),
ϕOne(S) (appl(f, args)) _ propag(appl(f, ϕlist
One(S) (args))),
list
0
ϕOne(S) (h :: q) _ ϕOne(S) (ϕS (h), q, h :: nil),
ϕlist
One(S) (nil) _ ⊥list (nil),
ϕ0One(S) (⊥( ), nil, r tried) _ ⊥list (rev(r tried)),
ϕ0One(S) (⊥( ), h :: q, r tried) _ ϕ0One(S) (ϕS (h), q, h :: r tried),
ϕ0One(S) (x @ appl( , ), todo, :: r tried) _
rconcat(r tried, x :: todo) }
Figure 3: Strategy translation for meta-encoded terms; L is defined in Figure 4.
that we replace the terms of the original signature by their meta-level encodings:3
TM (Spz ) = { ϕpz (appl(+, appl(Z, nil) :: x :: nil)) _ x,
ϕpz (appl(Z, nil)) _ ⊥(appl(Z, nil)),
ϕpz (appl(S, y1 :: nil)) _ ⊥(appl(S, y1 :: nil)),
ϕpz (appl(+, appl(S, y1 :: nil) :: y2 :: nil)) _
⊥(appl(+, appl(S, y1 :: nil) :: y2 :: nil)),
ϕpz (appl(+, appl(+, y1 :: y2 :: nil) :: y3 :: nil)) _
⊥(appl(+, appl(+, y1 :: y2 :: nil) :: y3 :: nil)),
ϕpz (⊥(x)) _ ⊥(x) }

The following meta-encoding is obtained for the Identity strategy:

TM (Identity) = { ϕIdentity (appl(y1 , y2 )) _ appl(y1 , y2 ), ϕIdentity (⊥(x)) _ ⊥(x) }
3For readability reasons we write in what follows appl(f, . . .) instead of appl(_f ^, . . .) for all f ∈ F .

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

L = { append(nil, x)
append(h :: q, x)
rev(nil)
rev(h :: q)
rconcat(nil, x)
rconcat(h :: q, x)
propag(appl(f, ⊥list (args)))
propag(appl(f, h :: q))
propag(appl(f, nil))

_
_
_
_
_
_
_
_
_

19

x :: nil,
h :: append(q, x),
nil,
append(rev(q), h),
x,
rconcat(q, h :: x),
⊥(appl(f, args)),
appl(f, h :: q),
appl(f, nil) }

Figure 4: Auxiliary symbols and rewrite rules for lists manipulation.
and the strategy Srpz = µX . (+(Z, x) _ x ; X) ←
+ Identity from Example 3.3 is encoded by:
TM (Srpz ) = { ϕrpz (x @ appl( , )) _ ϕtpz (x),
∪ { ϕX (x @ appl( , )) _ ϕtpz (x),
∪ { ϕtpz (x @ appl( , )) _ ϕ←
+ (ϕpzX (x)),
,
))
_
x,
ϕ←
(x
@
appl(
+
∪ { ϕpzX (x @ appl( , )) _ ϕ; (ϕX (ϕpz (x)), x),
ϕ; (x @ appl( , ), ) _ x,
∪ TM (Spz ) ∪ TM (Identity)

ϕrpz (⊥(x)) _ ⊥(x) }
ϕX (⊥(x)) _ ⊥(x) }
ϕtpz (⊥(x)) _ ⊥(x),
ϕ←
+ (⊥(x)) _ ϕIdentity (x) }
ϕpzX (⊥(x)) _ ⊥(x),
ϕ; (⊥( ), x) _ ⊥(x) }

In contrast with the translations of the previous section, only the encoding of the strategy Spz
depends on the considered signature, all the other rules in the encoding would be the same
independently of the signature.
The meta-level representation of the terms has a more important impact on the way
All (S) and One(S) are translated. When applying (the encoding of) one of these strategies
to a term appl(f, args) we want to apply S to each of the elements of the list args to check
if S succeeds or not on these arguments. To do so, we have to manipulate explicitly lists of
arguments and we introduce thus some extra symbols and the corresponding rewrite rules to
handle them: append(list, x) adds the element x at the end of list, rev(list) computes the
reverse of list, rconcat(list1 , list2 ) concatenates the reverse of list1 with list2 , and propag
propagates the failure or the success of the application of a strategy on the arguments of a
meta-level term to the whole term. The rewrite rules for these symbols are given in Figure 4.
Given a subject appl(f, args), the encoding of All (S) first checks whether the list
args is empty or not with the rules for the symbol ϕlist
All(S) . If it is empty, then All (S) has
been applied to a (meta-)constant appl(f, nil), and the result should be the term itself,
which is the case because ϕlist
All(S) (nil) _ nil and propag(appl(f, nil)) _ appl(f, nil).
If args = t1 :: t2 :: . . . :: tn :: nil, we go through the list of arguments, using terms of
the form ϕ0All(S) (x, todo, r tried, r done), where x is the element being reduced, initialized
successively with ϕS (ti ) for 1 ≤ i ≤ n, todo is a list containing the terms ti+1 . . . tn remaining
to reduce, r tried is a list containing the terms ti . . . t1 already reduced, and r done is the
list containing the reducts t0i . . . t01 of the terms in r tried. If ϕS (ti ) reduces to ⊥(ti ), then we
abort the whole process by producing first ⊥list (rconcat(r tried, todo)), which reduces to
⊥list (args), and then propagating failure with propag to generate the term ⊥(appl(f, args)).
If reducing ϕS (ti ) produces a meta-term t0i , then we store this result in r done and proceed
with the next term in todo. If there are no terms left to be evaluated in todo, we build

20

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

the final result using the last result t0n and the previously reduced arguments t0n−1 . . . t01 to
obtain appl(f, t01 :: . . . :: t0n :: nil).
Example 4.2. The meta-encoding of the strategy Sall = All (+(Z, x) _ x) consists of:
TM (Sall ) = { ϕall (⊥(x)) _ ⊥(x),
ϕall (appl(f, args)) _ propag(appl(f, ϕlist
all (args))),
list
0
ϕall (h :: q) _ ϕall (ϕpz (h), q, h :: nil, nil),
ϕlist
all (nil) _ nil,
ϕ0all (⊥( ), td, rt, ) _ ⊥list (rconcat(rt, td)),
ϕ0all (appl(f, args), nil, , rd) _ rev(appl(f, args) :: rd),
ϕ0all (appl(f, args), h :: q, rt, rd) _
ϕ0all (ϕpz (h), q, h :: rt, appl(f, args) :: rd) }
∪ TM (Spz ) ∪ L

The translation T(All (+(Z, x) _ x)) would contain much more rules and their number
depends on the considered signature. We can see in Example 5.4 the impact of the signature
on the size of the encoding using the original terms instead of their meta-level representation.
The encoding of One(S) follows the same principles. If args = t1 :: t2 :: . . . ::
tn :: nil, then we explore the list with ϕ0One(S) (x, todo, r tried), where x is initialized
successively with ϕS (ti ) until the encoding of S succeeds on one of these terms. The
list todo contains what is left to try (i.e. ti+1 :: . . . :: tn :: nil), and r tried contains ti :: ti−1 :: . . . :: t1 :: nil. If x becomes a meta-term t0i , then we rewrite it into
rconcat(ti−1 :: . . . :: t1 :: nil, t0i :: ti+1 :: . . . :: tn :: nil) which then reduces to the required
result. If S fails on ti (i.e. x becomes ⊥(ti )) and todo is not empty, then we consider
the next term by reducing to ϕ0One(S) (ϕS (ti+1 ), todo, ti+1 :: r tried). Otherwise, we reduce
to ⊥list (rev(r tried)), which produces ⊥list (args), and the rules for propag then generate
⊥(appl(f, args)), as wished.
4.3. Properties of the meta-encoding. We state now the correctness of the metaencoding by first establishing the correspondence between TM and the translation of
Section 3. The next lemma also shows that applying the strategy meta-encoding to a
meta-encoded term results in a meta-encoded term, as expected. We extend _ · ^ to ⊥ by
defining _⊥(t)^ = ⊥(_t^).
Lemma 4.3. Given a term t ∈ T (F), a strategy S and a context Γ such that FVarX (S) ⊆
DomX (Γ),
(1) if T(S) ∪ B(Γ) • ϕS (t) −→
→ u with u ∈ T (F) or u = ⊥(t), then TM (S) ∪ BM (Γ) •
ϕS (_t^) −→
→ _u^;
(2) if TM (S) ∪ BM (Γ) • ϕS (_t^) −→
→ t00 and t00 ∈ T (Fappl ), then there exists t0 such that
_t0 ^ = t00 and T(S) ∪ B(Γ) • ϕS (t) −→
→ t0 .
(3) if TM (S) ∪ BM (Γ) • ϕS (_t^) −→
→ ⊥(t00 ) and t00 ∈ T (Fappl ), then t00 = _t^ and T(S) ∪
B(Γ) • ϕS (t) −→
→ ⊥(t).
Sketch. The proof is by induction on S. The correspondence is direct for the reduction
steps which do not involve All or One. In these two cases, we relate how TM (All (S)) or
TM (One(S)) behaves on appl(_f ^, _t1 ^ :: . . . :: _tn ^ :: nil) depending on how TM (S) behaves

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

21

on each of the _ti ^. For example, we show that TM (S) ∪ BM (Γ) • ϕS (_ti ^) −→
→ _t0i ^ with
0
_ti ^ 6= ⊥(_ti ^) for all i iff
TM (All (S)) ∪ BM (Γ) • ϕ0All(S) (ϕS (_t1 ^), _t2 ^ :: . . . :: _tn ^ :: nil, _t1 ^ :: nil, nil)
−→
→ _t01 ^ :: . . . :: _t0n ^ :: nil
From there the induction hypothesis tells us that TM (S) ∪ BM (Γ) • ϕS (_ti ^) −→
→ _t0i ^ iff
T(S) ∪ B(Γ) • ϕS (ti ) −→
→ t0i , and then we can show that T(S) ∪ B(Γ) • ϕS (ti ) −→
→ t0i iff
0
0
T(All (S)) ∪ B(Γ) • f (t1 , . . . , tn ) −→
→ f (t1 , . . . , tn ) to conclude. In total, we have four different
cases (depending on whether the applications of All (S) or One(S) succeed or not), which
are treated similarly.
Combined with Theorem 3.5 this result allows us to deduce the correspondence between
the strategy application and TM .
Theorem 4.4 (Simulation). Given a term t ∈ T (F), a strategy S and a context Γ such
that FVarX (S) ⊆ DomX (Γ),
(1) Γ ` S ◦ t =⇒ t0 iff TM (S) ∪ BM (Γ) • ϕS (_t^) −→
→ _t0 ^, t0 ∈ T (F)
(2) Γ ` S ◦ t =⇒ Fail iff TM (S) ∪ BM (Γ) • ϕS (_t^) −→
→ ⊥(_t^)
Proof. By Lemma 4.3 and Theorem 3.5.

5. Encoding rewriting strategies with typed rewrite rules
Many programming languages use type systems to classify values and expressions into
types, to define how those types can be manipulated and how they interact. In logic [29],
many-sorted signatures are used similarly to partition the universe into disjoint subsets, one
for every sort, and a many-sorted logic naturally leads to a type theory [23]. Indeed, sorts of
many-sorted signatures are also known as algebraic data-types in programming languages.
When using many-sorted signatures the strategy translations should guarantee that all
the generated terms and rewrite rules respect the corresponding construction constraints.
Traversal strategies propagate the application of a given strategy to (sub-)terms of potentially
different sorts and consequently the strategies we consider here are intrinsically polymorphic.
This polymorphic nature should be clearly retrieved in the encoding and thus, the sorts of
the symbols generated during the translation should cope with this constraint. To support
this behaviour we consider many-sorted signatures with potentially overloaded symbols and
we show that the proposed translations can be adapted easily to work even when overloaded
symbols are not supported by the targeted language.
We consider in what follows sort preserving rewrite rules and consequently sort preserving
strategies. We propose a translation generating sort preserving TRS which are, as before,
faithful encodings of the corresponding strategies.
5.1. Many-sorted signatures and term rewriting systems. A many-sorted signature
Σ = (S, F), or simply Σ, consists of a set of sorts S and a set of symbols F. A symbol f
with domain w = s1 × . . . ×sn ∈ S ∗ and co-domain s is written f : w 7→ s; n is its arity and
w 7→ s its profile. Symbols can be overloaded, i.e. a symbol f can have profiles w 7→ s and
w0 7→ s0 with w 6= w0 .

22

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

We write Fs for the subset of symbols of codomain s. Variables are also sorted and x : s
means that variable x has sort s. We sometimes annotate the name of a variable by its sort
and use, for example, xs to implicitly
indicate a variable of sort s. The set Xs denotes a set
S
of variables of sort s and X = s∈S Xs is the set of sorted variables.
The set of terms of sort s, denoted Ts (F, X ) is the smallest set containing Xs and such
that f (t1 , . . . , tn ) is in Ts (F, X ) whenever f : s1 × . . . ×sn 7→ s and ti ∈ Tsi (F, X ) for i ∈ [1, n].
We write t : s when the S
term t is of sort s, i.e. when t ∈ Ts (F, X ). The set of sorted terms is
defined as TS (F, X ) = s∈S Ts (F, X ). Sorted substitutions are defined as mappings σ from
sorted variables to sorted terms such that if x : s then σ(x) ∈ Ts (F, X ). Note that for any
such sorted substitution σ, t : s iff σ(t) : s.
A sorted rewrite rule is a rewrite rule l _ r with l, r : s and a sorted TRS is a set of
sorted rewrite rules inducing a corresponding rewriting relation over sorted terms. Given
two sorted terms l, t : s, we say that l matches t if there exists a sorted substitution σ such
that t = σ(l); in this case we say that t is a sorted instance of l.
5.2. Typed encoding of rewriting strategies. Given a strategy built over a many-sorted
signature, the translation defined in Section 3 can still be used to generate a faithful encoding
in the sense of Theorem 3.5. Since any term in TS (F) is also a term in T (F), the termination
of the (unsorted) TRS encoding the strategy guarantees the termination of the sorted
strategy. Nevertheless, we can use the extra information provided by sorts to refine this
translation and remove the generated rewrite rules that are useless, because they cannot be
applied to sorted terms. More importantly, this translation cannot be used as a strategy
compiler if the target language is many-sorted and accepts only sorted terms and rewrite
rules.
The presence of ill-sorted terms in the encoding generated by the translation in Figure 2
is essentially due to the unsorted semantics we have considered so far for anti-terms. In an
unsorted world, the anti-term !t represents all the terms which do not match t, and !⊥(x)
denotes all the ground terms in T (F). We adapt these notions to a many-sorted setting as
s
follows: given a term t of sort s, we write ! t for the terms of sort s which do not match t,
s
and given a sort s we write ! ⊥(x) to denote all the ground sorted terms in Ts (F). Note
S
s
that s∈S {! ⊥(x)} denotes all the ground sorted terms TS (F) of the original signature.
Example 5.1. Consider the many-sorted signature (S, F) where S = {Nat, Bool} and
F = FNat ∪ FBool with FNat = {Z : 7→ Nat, S : Nat 7→ Nat, + : Nat×Nat 7→ Nat}, FBool =
{true : 7→ Bool, false : 7→ Bool, odd : Nat 7→ Bool, even : Nat 7→ Bool}. The anti-term
!Nat+(Z, x) denotes exactly the sorted terms in TNat (F) matched by Z, S(x1 ), +(S(x1 ), x2 )
or +(+(x1 , x2 ), x3 ). In particular, it does not denote the (ill-sorted) term +(true, Z). The
Bool
anti-term ! +(Z, x) denotes the sorted terms in TBool (F) matched by true, false, odd(x1 )
or even(x1 ).
Bool
The anti-term ! ⊥(x) denotes all sorted instances of true, false, odd(x1 ) and
Nat
even(x1 ) while ! ⊥(x) denotes all sorted instances of Z, S(x1 ) and +(x1 , x2 ). The union of
all these instances represent indeed all the sorted terms in t ∈ TS (F).
We now adapt the unsorted translation defined in Section 3 to accommodate manysorted signatures. Given a sorted signature (S, F), we define the signature (S, F) where
the sorts are unchanged, and F is extended with the generated ϕ symbols and ⊥. Unlike
in the unsorted case, we have to specify their profile: the symbols ⊥ and ϕIdentity , ϕFail ,

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

23

ϕl_r , ϕS1 ;S2 , ϕS1 ←
+ , ϕµX.S , ϕX , ϕAll(S) , ϕOne(S) have sort s 7→ s for all s ∈ S, and
+S2 , ϕ←
ϕ; : s×s 7→ s for all s ∈ S. These symbols are overloaded, since they have as many profiles as
there are sorts in S. In contrast, the profiles of the generated symbols of the form ϕf and
ϕfi depend on the profile of f : if f : s1 × . . . ×sn 7→ s ∈ Fs+ then ϕf : s1 × . . . ×sn ×s 7→ s and
ϕfi : s1 × . . . ×sn 7→ s.
The translation TS (S) transforms the strategy S into a set of sorted rewrite rules;
since its definition is the same as for the unsorted case (Figure 2), except for extra sort
annotations on variables and !, we give the rules only in Appendix 10 (Figure 7). Even
though the definitions of T and TS are almost the same, taking sorts into account could have
an important impact on the number of rules generated in the resulting encoding. Sorts may
introduce duplication: since ⊥ has now a profile, for every rule of S
the form ϕ(⊥(x)) _ ⊥(x)
generated in the unsorted case, we generate now the set of rules s∈S {ϕ(⊥(xs )) _ ⊥(xs )}.
In contrast, expanding !⊥( ) in the unsorted case produces as many rules as considering
S
S
s
as s∈S Fs . As detailed
s∈S {! ⊥(x)} in the sorted case, assuming F has as many elements
S
in Section 6.4, !⊥( ) is expanded into the set of terms f ∈F {f (x1 , . . . , xar(f ) )}, while
S
S
S
s
s∈S {! ⊥(x)} becomes the generally smaller set
s∈S
f ∈Fs {f (x1 , . . . , xn )}.
Example 5.2. If we consider the many-sorted signature in Example 5.1, we obtain the
following encoding for the Identity strategy when expanding the rule schemas in Figure 7:
TS (Identity) = { ϕIdentity (Z) _ Z
ϕIdentity (S(y1 )) _ S(y1 ),
ϕIdentity (+(y1 , y2 )) _ +(y1 , y2 ),
ϕIdentity (⊥(x)) _ ⊥(x),

ϕIdentity (true) _ true,
ϕIdentity (false) _ false,
ϕIdentity (odd(y1 )) _ odd(y1 ),
ϕIdentity (even(y1 )) _ even(y1 ),
ϕIdentity (⊥(z)) _ ⊥(z) }
To improve readability, we do not annotate variables but instead use an environment mapping
variables to sorts: here, we have x, y1 , y2 : Nat and z : Bool. Besides, the signature is enriched
in this case with the symbols { ⊥ : Nat 7→ Nat, ϕIdentity : Nat 7→ Nat, ⊥ : Bool 7→ Bool,
ϕIdentity : Bool 7→ Bool }.
For this signature, the unsorted encoding would contain the same rewrite rules modulo
syntactic equivalence, i.e. the rules in T(Identity) are those in TS (Identity) with the rules
ϕIdentity (⊥(x)) _ ⊥(x) and ϕIdentity (⊥(z)) _ ⊥(z) collapsed into only one rule.
The unsorted and sorted encodings differ more on how they handle rewrite rules and
traversal combinators. As explained before, the anti-pattern ϕl_r (x@ !l) _ ⊥(x) is expanded
differently between the unsorted and sorted cases: we consider only the terms of the same
sort as l in the sorted translation, thus reducing the number of generated rules compared to
the unsorted case.
Example 5.3. Let Spz = +(Z, x) _ x, S = {Nat, Bool}, and F = FNat ∪ FBool with
FBool = {odd : Nat 7→ Bool, even : Nat 7→ Bool, true 7→ Bool, false 7→ Bool}. Then
TS (Spz ) = { ϕpz (+(Z, x)) _ x,
ϕpz (Z) _ ⊥(Z),
ϕpz (S(y1 )) _ ⊥(S(y1 )),
ϕpz (+(S(y1 ), y2 )) _ ⊥(+(S(y1 ), y2 )),
ϕpz (+(+(y1 , y2 ), y3 )) _ ⊥(+(+(y1 , y2 ), y3 )),
ϕpz (⊥(x)) _ ⊥(x),

ϕpz (true) _ ⊥(true),
ϕpz (false) _ ⊥(false),
ϕpz (odd(y1 )) _ ⊥(odd(y1 )),
ϕpz (even(y1 )) _ ⊥(even(y1 )),
ϕpz (⊥(z)) _ ⊥(z) }

24

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

so that x, y1 , y2 , y3 : Nat, z : Bool, and the signature is extended with { ⊥ : Nat 7→ Nat,
ϕpz : Nat 7→ Nat, ⊥ : Bool 7→ Bool, ϕpz : Bool 7→ Bool }.
The unsorted translation T(Spz ) contains the rules in TS (Spz ) as well as the rules
{ ϕpz (+(odd(y1 ), y2 )) _ ⊥(+(odd(y1 ), y2 )),
ϕpz (+(true, y2 )) _ ⊥(+(true, y2 )),
ϕpz (+(even(y1 ), y2 )) _ ⊥(+(even(y1 ), y2 )), ϕpz (+(false, y2 )) _ ⊥(+(false, y2 )) }

which operate on ill-sorted terms w.r.t. the sorted signature we consider here.

For the encodings of All and One, we can also exploit the profiles of the symbols and
generate less rules to filter the ground terms of the original many-sorted signature. Given
s1
f : s1 × . . . ×sn 7→ s, encoding produces now schemas of the form ϕf (x1 @ ! ⊥( ), . . . , xn @
si
si+1
i−1
!sn⊥( ), ys ) _ f (x1 , . . . , xn ) and ϕfi (⊥(xs11 ), . . . , ⊥(xsi−1
), xi @ ! ⊥( ), xi+1
, . . . , xsnn ) _
f (xs11 , . . . , xsnn ) for respectively All and One and thus generates significantly less rules than
in the unsorted case where we used the exhaustive !⊥( ).
The encodings of the other operators (sequence, choice, . . . ) also filter terms using
s
x @ ! ⊥( ), but for all s ∈ S and not for a given s, so the number of generated rules for these
constructs is the same as in the unsorted case.
Example 5.4. If we consider theSmany-sorted signature in Example 5.1, we obtain
TS (All (+(Z, x) _ x)) = TS (Spz )
{
ϕAll (⊥(x)) _ ⊥(x),
ϕAll (+(x1 , x2 )) _ ϕ+ (ϕpz (x1 ), ϕpz (x2 ), +(x1 , x2 )), ϕ+ (Z, +(x1 , x2 ), x) _ +(Z, +(x1 , x2 )),
ϕ+ (Z, S(x1 ), x) _ +(Z, S(x1 )),
ϕ+ (⊥(x1 ), x2 , x) _ ⊥(x),
ϕ+ (Z, Z, x) _ +(Z, Z),
ϕ+ (x1 , ⊥(x2 ), x) _ ⊥(x),
ϕ+ (+(x1 , x2 ), +(y1 , y2 ), x) _ +(+(x1 , x2 ), +(y1 , y2 )), ϕAll (S(x1 )) _ ϕS (ϕpz (x1 ), S(x1 )),
ϕS (⊥(x1 ), x) _ ⊥(x),
ϕ+ (+(x1 , x2 ), S(y1 ), x) _ +(+(x1 , x2 ), S(y1 )),
ϕS (+(x1 , x2 ), x) _ S(+(x1 , x2 )),
ϕ+ (+(x1 , x2 ), Z, x) _ +(+(x1 , x2 ), Z),
ϕ+ (S(x1 ), +(y1 , y2 ), x) _ +(S(x1 ), +(y1 , y2 )),
ϕS (S(x1 ), x) _ S(S(x1 )),
ϕ+ (S(x1 ), S(y1 ), x) _ +(S(x1 ), S(y1 )),
ϕS (Z, x) _ S(Z),
ϕAll (Z) _ Z,
ϕ+ (S(x1 ), Z, x) _ +(S(x1 ), Z),
ϕAll (⊥(z)) _ ⊥(z),
ϕodd (⊥(x1 ), z) _ ⊥(z),
ϕAll (even(x1 )) _ ϕeven (ϕpz (x1 ), even(x1 )),
ϕeven (⊥(x1 ), z) _ ⊥(z),
ϕodd (+(x1 , x2 ), z) _ odd(+(x1 , x2 )),
ϕeven (+(x1 , x2 ), z) _ even(+(x1 , x2 )),
ϕodd (S(x1 ), z) _ odd(S(x1 )),
ϕeven (S(x1 ), z) _ even(S(x1 )),
ϕodd (Z, z) _ odd(Z),
ϕeven (Z, z) _ even(Z),
ϕAll (false) _ false,
ϕAll (odd(x1 )) _ ϕodd (ϕpz (x1 ), odd(x1 )),
ϕAll (true) _ true }

so that x, x1 , x2 , y1 , y2 : Nat, z : Bool, and we extend the original signature with

{ ϕAll : Nat 7→ Nat, ϕAll : Bool 7→ Bool, ⊥ : Nat 7→ Nat, ⊥ : Bool 7→ Bool,
ϕpz : Nat 7→ Nat, ϕpz : Bool 7→ Bool, ϕ+ : Nat×Nat×Nat 7→ Nat, ϕS : Nat×Nat 7→ Nat,
ϕeven : Nat×Bool 7→ Bool, ϕodd : Nat×Bool 7→ Bool }.
The unsorted translation T(All (+(Z, x) _ x)) would contain not only the above rules but
also a significant number of rules which would be ill-sorted w.r.t. the many-sorted signature
considered here.

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

25

We show in Section 5.3 that although the sorted translation generates less rules (modulo
syntactic equivalence) than the unsorted translation, we still obtain a faithful encoding for
sorted terms.
Remark 5.5. We suppose in this section that the targeted language supports overloaded
symbols, but if it is not the case, like, e.g. in Tom, the sorted translation can be easily
adapted to fit this constraint: instead of overloading the generated symbols, we add one
symbol for each sort.
S For example, the original signature would be extended in this case
with the symbol(s) s∈S {⊥s : s 7→ s}. We then use the symbol of the appropriate sort in the
rules of Figure 7, depending of the sort of its argument(s). For example, the translation of a
rewrite rule l _ r with l : sl becomes:
[
s
l
TS (l _ r) = { ϕsl_r
(l) _ r }
{ ϕsl_r (x @ ! l) _ ⊥s (x), ϕsl_r (⊥s (xs )) _ ⊥s (xs ) }
s∈S

5.3. Properties of the many-sorted encoding. It is easy to see that for each of the
generated rewrite rules, for any sort assignment for the variables such that the left-hand side
is well-sorted, the right-hand side is also well-sorted and has the same sort as the left-hand
side. Starting from this observation we can show that the reduction of a sorted term w.r.t.
a strategy encoding is sort preserving:
Lemma 5.6 (Subject reduction). Consider a many-sorted signature (S, F), a strategy S, a
context Γ such that FVarX (S) ⊆ DomX (Γ), and the term rewriting system R=TS (S)∪BS (Γ)
built over the extended signature (S, F). Given a term t ∈ Ts (F) for some sort s ∈ S, if
t −→R t0 then t0 ∈ Ts (F).
Sketch. By induction on the structure of the strategy S (and the context Γ) and by case
analysis on the rewrite rule applied in the reduction. For each case we consider reductions
at the top position since the replacement of a sub-term by another one of the same sort is
obviously sort preserving.
As we have seen in the previous section, the rewrite rules generated by the sorted
translation are the ones generated by the unsorted encoding that are well-sorted w.r.t. the
considered many-sorted signature. Since an ill-sorted rewrite rule cannot be applied on
a sorted term, the reduction of a such a sorted term is the same if we use the sorted or
unsorted encoding.
Lemma 5.7 (Equivalent reductions). Consider a many-sorted signature (S, F), a strategy S,
a context Γ such that FVarX (S) ⊆ DomX (Γ), and the term rewriting systems R=T(S)∪B(Γ)
and RS =TS (S) ∪ BS (Γ) built over the extended signature (S, F). Given a term t ∈ TS (F),
t −→RS t0 iff t −→R t0 .
Sketch. Every rewrite rule in RS is also included in R and thus, if t −→RS t0 then t −→R t0 .
For the other direction we proceed by induction on the structure of the strategy S (and the
context Γ) and by case analysis on the rewrite rule applied in the reduction.
The interesting cases concern the rule schemas using anti-patterns in the encodings of a
rewrite rule, All , and One. For the first one, we remark that if a rewrite rule corresponding
s
to the rule schema ϕl_r (x @ ! l) _ ⊥(x) from the unsorted translation is applied to a sorted
term then, there exists an identical rewrite rule corresponding to the similar rule schema
from the sorted translation which can be applied. For the other two cases, we proceed

26

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

similarly and use the fact that if a rewrite rule corresponding to one of the rule schemas
relying on a !⊥( ) is applied, then the same rewrite rule is also exhibited by the similar rule
s
schema using the corresponding pattern ! ⊥( ) from the sorted translation.
The one-step reduction of a sorted term is thus exactly the same when using the sorted
or unsorted encodings and since the latter is also sort preserving we can conclude that the
sorted translation produces faithful strategy encodings.
Theorem 5.8 (Simulation). Given a a many-sorted signature (S, F), a strategy S, two
terms t, t0 ∈ TS (F), and a context Γ such that FVarX (S) ⊆ DomX (Γ),
(1) Γ ` S ◦ t =⇒ t0 iff TS (S) ∪ BS (Γ) • ϕS (t) −→
→ t0 ,
(2) Γ ` S ◦ t =⇒ Fail iff TS (S) ∪ BS (Γ) • ϕS (t) −→
→ ⊥(t)
Proof. Follows immediately from Lemma 5.6, Lemma 5.7 and Theorem 3.5.
The sorted translation can be consequently used as a strategy compiler for many-sorted
languages and, as explained above, it can be used for languages allowing symbol overloading
or not. If we collapse all syntactically equivalent rules in a sorted encoding we obtain less
rules than in the corresponding unsorted encoding but we can still feed it into (usually
unsorted) termination tools to verify the termination of the corresponding strategy for sorted
terms.
6. Implementation and experimental results
The strategy translations presented in the previous sections have been implemented in a
tool called StrategyAnalyser4, written in Tom, a language that extends Java with high
level constructs for pattern matching, rewrite rules and strategies (i.e. the tool itself is
written using rules and strategies!). Given a set of rewrite rules guided by a strategy, the
tool generates a plain TRS in AProVE/TTT2 syntax5 or Tom syntax (restricted to rewrite
rules only).
The tool can be configured to generate TRS at meta-level or not, in a many-sorted
context or not, to use the alias notation or not, and to use the notion of anti-term or not.
An encoding using anti-terms and aliasing can be directly used in a Tom program but for
languages and tools which do not offer such primitives, aliases and anti-terms have to be
expanded into plain rewrite rules. We explain first how this expansion is realized and we
illustrate then our approach on several representative examples.
6.1. Expansion of anti-terms. The rules given in Figure 2 can generate two kinds of rules
which contain anti-terms. The first family is of the form ϕ(. . . , yi @ !⊥( ), . . .) _ u with
yi ∈ X , and with potentially several occurrences of !⊥( ). These rules can be easily expanded
into a family of rules ϕ(. . . , yi @ f (x1 , . . . , xn ), . . .) _ u with such a rule for all f ∈ F, and
with x1 , . . . , xn ∈ X and n = ar(f ). This expansion is performed recursively to eliminate all
the instances of !⊥( ). The other rules containing anti-terms come from the translation of
rewrite rules (E3) and have in the unsorted case the form ϕ(y @ !f (t1 , . . . , tn )) _ ⊥(y), with
f ∈ F n and t1 , . . . , tn ∈ T (F, X ). If the term f (t1 , . . . , tn ) is linear, then the tool generates
two families of rules:
4http://github.com/rewriting/tom/tree/master/applications/strategyAnalyzer
5

http://aprove.informatik.rwth-aachen.de/

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

27

• ϕ(g(x1 , . . . , xm )) _ ⊥(g(x1 , . . . , xm )) for all g ∈ F, g 6= f , x1 , . . . , xm ∈ X , m = ar(g),
• ϕ(f (x1 , . . . , xi−1 , xi @ !ti , xi+1 , . . . , xn )) _ ⊥(f (x1 , . . . , xn )) for all i ∈ [1, n] and ti 6∈ X ,
with the second family of rules recursively expanded, using the same algorithm, until there
is no anti-term left.
This expansion mechanism is more difficult when we want to find a convenient (finite)
encoding for non-linear anti-terms, and in this case the expansion should be done, in fact,
w.r.t. the entire translation of a rewrite rule. Given the rules ϕ(l) _ r and ϕ(y @ !l) _ ⊥(y)
with l ∈ T (F, X ) a non-linear term, we consider the linearized version of l, denoted l0 , with
all the variables xi ∈ Var (l) appearing more than once (mi times, with mi > 1) renamed
into zi1 , . . . , zimi −1 (the first occurrence of xi is not renamed). Then, these two rules can be
translated into:
• ϕ(y @ !l0 ) _ ⊥(y)
• ϕ(l0 ) _ ϕ0 (l0 , x1 = z11 ∧ · · · ∧ x1 = z1m1 −1 ∧ · · · ∧ xn = zn1 ∧ · · · ∧ xn = znmn −1 )
• ϕ0 (l0 , tt) _ r
• ϕ0 (l0 , ff) _ ⊥(l0 )
with the first rule containing now the linear anti-term !l0 expanded as previously. The rules
generated for equality and conjunction are as expected.
The expansion goes in the same way in the many-sorted case,
S but using only symbols of
the appropriate sort; a sort B, an overloaded equality symbol s∈S {= : s×s 7→ B} together
with the symbols {tt : 7→ B, ff : 7→ B, ∧ : B×B 7→ B} are added to the extended signature.
The rules generated for equality are then restricted to those whose left-hand side and
right-handS
side have
sort. Given a many-sorted signature (S, F), this set of rules
S the same
s1
consists of s∈S f ∈Fsn { f (x1 , . . . , xsnn ) = f (y1s1 , . . . , ynsn ) _ xs11 = y1s1 ∧. . .∧xsnn = ynsn ∧tt }
S
S
S
s1
s1
sn
sm
s∈S
f ∈Fsn g6=f ∈Fsn { f (x1 , . . . , xn ) = g(y1 , . . . , ym ) _ ff }. For the translation TM in
Section 4, the expansion is performed as in the unsorted case, except that the expansion
process generates meta-level representations directly.
6.2. Examples. The first example we consider in what follows comes from an optimizer
for multi-core architectures [11], a project where abstract syntax trees are manipulated and
transformations are expressed using rewrite rules and strategies, and consists of two rewrite
rules identified as patterns occurring often in various forms in the project. First, the rewrite
rule g(f (x)) _ f (g(x)) corresponds to the search for an operator g (which can have more than
one parameter in the general case) which is pushed down under another operator f (again, this
operator may have more than one parameter). This rule is important since the corresponding
m
z
}|
{
(innermost) reduction of a term of the form tgf = g(f (· · · (f (g(f (· · · (f (g(f (· · · (f (g(a))) · · · ),
| {z } | {z } | {z }
n

n

n

with, for example, n = 10 and m = 18 occurrences of g, involves O(n2 m2 ) computations
and could be a performance bottleneck.
Second, the rewrite rule h(x) _ g(h(x)) corresponds to wrapping some parts of a
program by some special constructs, like try/catch for example, and it is interesting since
its uncontrolled application is obviously non-terminating.
At present, strategy definitions given as input to StrategyAnalyser are written in a
simple functional style.

28

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

Example 6.1. The syntax allowing the definition of the above rewrite rules and possible
corresponding strategies could be defined as follows:
abstract syntax
T = a() | b()
strategies
gfx()
=
hx()
=
obu(t)
=
bu(t)
=
repeat(s)
=
mainStrat() =

| f(T) | g(T) | h(T)
[ g(f(x)) -> f(g(x)) ]
[ h(x) -> g(h(x)) ]
mu x.(one(x) <+ t)
mu x.(all(x) ; (t <+ Identity))
mu y.((s ; y) <+ Identity)
repeat(obu(gfx()))

#
#
#
#

obu stands for OnceBottomUp
bu stands for BottomUp
naive definition of innermost
strategy to compile

As a second example, we consider a strategy involving rewrite rules which are either non
left-linear or non right-linear and which are non-terminating if their application is not guided
by a strategy.
Example 6.2. We consider the following rewrite rules which implement the distributivity
and factorization of symbolic expressions composed of + and * and their application under a
specific strategy:
abstract syntax
T = Plus(T,T) | Mult(T,T) | Val(V)
V = a() | b()
strategies
dist()
= [ Mult(x,Plus(y,z)) -> Plus(Mult(x,y),Mult(x,z)) ]
fact()
= [ Plus(Mult(x,y),Mult(x,z)) -> Mult(x,Plus(y,z)) ]
innermost(s) = mu x.(all(x) ; ((s ; x) <+ Identity))
mainStrat() = innermost(dist()) ; innermost(fact())

As a third example, we consider a larger program inspired by the Tom compiler
itself, where the signature is composed of seven sorts and contains a significant number of
constructors.
Example 6.3. We consider two rewrite rules. The purpose of the first one, compile, is
to identify Match constructs and to replace them by instructions of the form If, Assign,
WhileDo, . . . , which implement the matching algorithm. In the Tom compiler, these
instructions are transformed by the backend into executable code written in Java or C for
instance. The second rule identifies occurrences of variables and produces a term which
contains both the new variable and the initial one (this rule represents the first stage of a
refactoring process).
abstract syntax # refactor example
CodeList = NilCode() | ConsCode(Code,CodeList)
Code = Match(TermList) | Assign(Name,Exp) | If(Exp,Code,Code) | WhileDo(Exp,Code)
| Nop() | ...
Exp = Or(Exp,Exp) | And(Exp,Exp) | IsFsym(Name,Term) | EqualTerm(Term,Term)
| TrueTL() | FalseTL() | ...
TermList = ConsTerm(Term,TermList) | NilTerm()
Term = VarTerm(Name) | ApplTerm(Name,TermList) | RenamedTerm(Term,Term)
Nat = Z() | S(Nat)
Name = Name(Nat)
strategies
compile() = [ Match(l) -> <...Code...> ]

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

29

rename() = [ VarTerm(Name(n)) -> RenamedTerm(VarTerm(Name(S(n))), VarTerm(Name(n))) ]
td(s) = mu x.((s <+ Identity) ; all(x))
# td stands for TopDown
tdstoponsucces(s) = mu x.(s <+ all(x))
mainStrat() = tdt(compile()) ; tdstoponsucces(rename())

The right-hand side of the rule rename contains the left-hand side of the rule and thus a
top-down strategy on this rule would not be terminating. Furthermore, it would rename
the second argument of RenamedTerm that we want to keep unchanged. The strategy we
consider (tdstoponsucces) is interesting because it searches for a VarName constructor in a
top-down way, but performs the replacement only once and does not continue the search
into sub-terms when a transformation is performed. Intuitively, this strategy is terminating,
and we will see that termination tools are able to prove it.
We also consider a relatively large example containing 4 sorts, 13 constructors, and 20
rules.
Example 6.4. The following represents the implementation of red-black-trees based on [33],
but expressed using rules and strategies.
abstract syntax # rbTree example
Tree = E() | T(Color,Tree,Nat,Tree) | balance(Tree) | ins(Nat,Tree)
| insAux(Nat,Tree,Cmp)
Color = R() | B()
Nat = Z() | S(Nat)
Cmp = lt() | gt() | eq0() | cmp(Nat,Nat)
strategies
b1() = [ balance(T(B(),T(R(),T(R(),a1,a2,a3),x,b),y,T(R(),c,z,d))) ->
T(R(),T(B(),T(R(),a1,a2,a3),x,b),y,T(B(),c,z,d)) ]
b2() = [ balance(T(B(),T(R(),a,x,T(R(),b1,b2,b3)),y,T(R(),c,z,d))) ->
T(R(),T(B(),a,x,T(R(),b1,b2,b3)),y,T(B(),c,z,d)) ]
... # rules b3()...b8()
b9() = [ balance(t) -> t ] # no balancing necessary
... # rules i1()...i5() and c1()...c4()
mainStrat() = repeat(obu(b1() <+ b2() <+ b3() <+ ...))

The complexity here comes also from the presence of a constructor T of arity 4, whose
negation (!T (. . .)) generates a large list of patterns to capture the cases where the rule cannot
be applied. The anti-term !balance(T (B(), T (R(), T (R(), a1, a2, a3), x, b), y, T (R(), c, z, d)))
is expanded into 108 patterns.
6.3. Generation of TRS for termination analysis. When run with the flag -aprove,
the StrategyAnalyser tool generates a TRS in AProVE/TTT2 syntax which can be
analyzed by any tool accepting this syntax. In this case, aliases and anti-terms are always
completely expanded leading generally to a significant number of plain rewrite rules.
The tool can be configured to generate many-sorted TRS or to generate the meta-level
representation of the TRS. The number of generated rules for a strategy could thus vary a
lot. In Table 1, we give for each example the number of generated rules in the (U)nsorted
case, in the many-(S)orted case, and in the (M)eta-level case. The last column indicates
whether the termination of the generated TRS has been proven or disproven by AProVE.
In practice, AProVE is able to handle relatively big sets of rules and, for example,
the termination of the strategy repeat(obu(gfx)), which is translated into 91 rules, is proven

30

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

Name

Strategy

U

S

repeat(dist)
repeat(fact)
repeat(dist ; fact)
td(dist)
obu(fact)
repeat(obu(fact))
factorize
simplify
innermost(dist)
innermost(fact)
repeat(td(dist))
bu(hx)
td(hx)
repeat(obu(gfx))
innermost(gfx)
propagate
bu(propagate)
bu(propagate2)
refactor
rbTree

µX . ((dist ; X) ←
+ Identity)
49
57
µX . ((fact ; X) ←
+ Identity)
84
78
µX . (((dist ; fact) ; X) ←
+ Identity)
110
107
µX . ((dist ←
+ Identity) ; All (X))
97
68
µX . (One(X) ←
+ fact)
102
83
µX . ((obu(fact) ; X) ←
+ Identity)
138
125
µX . (All (X) ; ((fact ; All (X)) ←
+ Identity))
162
124
td(dist) ; factorize
272
206
µX . (All (X) ; ((dist ; X) ←
+ Identity))
127
103
µX . (All (X) ; ((fact ; X) ←
+ Identity))
162
124
µX . ((td(dist) ; X) ←
+ Identity)
133
110
µX . (All (X) ; (hx ←
+ Identity))
51
51
µX . ((hx ←
+ Identity) ; All (X))
51
51
µX . ((obu(gfx) ; X) ←
+ Identity)
91
91
µX . (All (X) ; ((gfx ; X) ←
+ Identity))
85
85
µX . (gfx ; (All (X) ←
+ Identity))
73
73
µX . (All (X) ; (propagate ←
+ Identity))
127
127
– bu(propagate)with f, g, h of arity 2 –
991
378
td(compile) ; tdStopOnSuccess(rename)
63065 2350
µX . ((obu(b1 ←
+ b2 ←
+ · · · ) ; X) ←
+ Identity) 1956 1449

M
25
60
77
35
70
82
80
110
45
80
47
31
31
47
45
41
58
66
145
1260

AProVE

∅

3
3
7
3
3
3
3
3
3
3
7
3
7
3
3
3
3
3
3 3
∅

Table 1: Termination analysis: the columns U, S, and M indicate the number of plain rewrite
rules generated for the strategy, respectively in the (U)nsorted case, many-(S)orted
case, and (M)eta-level case. The column AProVE indicates (for the U, S and M
cases) whether the termination of the rules has been proven (3) or disproven (7)
by AProVE; ∅ is used when AProVE gives no information. A unique symbol in
the row indicates that the results are the same for the three cases.
in approximately 10 s (using the web interface). Similarly, for the example bu(propagate2)
which corresponds to an extension of the example bu(propagate) where symbols f, g, and h
become binary and the rule gfx is replaced by g(f (x, y), z) _ f (g(x, z), y), we generate 991
rules and the proof can be done in less then 80 s. For this example, when considering the
378 many-sorted rules, the proof can be done in less than 15 s and in the meta-level case,
consisting of 66 rules, the proof can be done in approximately 12 s. The size of the (left-hand
and right-hand sides of the) rules seems to be an important factor since the termination for
the rbTree example consisting of roughly 1000 rules cannot be (dis)proven while the 2350
rules of the many-sorted encoding of refactor can be handled in 160 s.
The termination of some strategies like, for example, repeat(obu(gfx)) might look pretty
easy to show for an expert, but termination is less obvious for more complex strategies like,
for example, bu(propagate), which is a specialized version of repeat(obu(gfx)), or rbu(fact),
which is a variant of bu(fact).
The approach was effective not only in proving termination of some strategies, but also
in disproving it when necessary. Once again this might look obvious for some strategies like,
for example, td(hx), which involves a non-terminating rewrite rule, but it is less clear for
strategies combining terminating rewrite rules or strategies like, e.g., repeat(dist;fact).

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

31

6.4. Generation of executable TRS. When run with the flag -tom, the StrategyAnalyser tool generates a TRS in Tom syntax which can be subsequently compiled into
Java code and executed.
By default, Tom executes a plain TRS with a built-in leftmost-innermost strategy
encoded using function calls. But Tom can also execute a rule controlled by a user-defined
strategy. In that case, the user-defined strategy is encoded into Java objects and is evaluated
using a library written in Java. This library provides several implementations where the
notion of failure can be encoded by a Java exception or by a special value to provide an
exception-free implementation.
Name

TRS Meta TRS Tom Tom*

repeat(dist)
<5
repeat(fact)
<5
obu(fact)
<5
repeat(obu(fact)) 190
innermost(dist)
332
innermost(fact)
310
bu(hx)
<5
repeat(obu(gfx)) 400
innermost(gfx)
553
propagate
<5
bu(propagate)
49
refactor
rbTree
1480

<5
<5
<5
323
347
472
<5
780
433
<5
108
570
2200

<5
13
<5
2460
650
308
<5
6300
4180
<5
46
220
2070

<5
<5
<5
120
230
149
<5
414
365
<5
42
115
840

Table 2: Benchmarks: the column TRS indicates the execution time in milliseconds for
the generated TRS compiled using Tom (i.e. using a built-in leftmost-innermost
strategy), the column Meta TRS indicates the execution time for a meta-level TRS
compiled using Tom, the column Tom indicates the execution time of the same
strategy written directly in Tom, using Java exception-based implementation, and
the column Tom* indicates the execution time of the Tom Java exception-free
implementation.
It is interesting to see how the varying number of generated rules for a strategy impacts
the efficiency of the execution of such a system. If we execute a Tom+Java program
corresponding to the repeat(obu(gfx)) strategy with a classic built-in implementation where
strategy failure is implemented by a Java exception, the normalization of the term tgf takes
6.3 s6 (Table 2, column Tom). With an alternative built-in implementation which uses a
special value and does not throw Java exceptions, the computation time decreases to 0.41 s
(Table 2, column Tom*). The strategy repeat(obu(gfx)) is translated into an executable
TRS containing 91 Tom plain rewrite rules and the normalization takes in this case 0.4 s!
When generating a meta-level TRS, the number of rules decrease to 47, but the normalization
takes 0.78 s. When implementing the innermost(gfx) strategy natively in Tom Java, using
a built-in implementation with a special encoding of failure, the normalization takes 0.36 s.
The same strategy is translated into an executable TRS which contains 85 plain rewrite
6on a MacPro 3GHz

32

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

rules in the unsorted case and 45 rules in the meta-level case. The first TRS normalizes the
term tgf in 0.55 s, whereas it takes 0.43 s to the meta-level TRS to normalize the term. This
example is interesting because it shows that the meta-level approach allows to considerably
reduce the number of rules, and thus the size of the generated code, without slowing down
the execution time. The performances are confirmed for the large examples; the 63065 rules
generated for refactor with the plain encoding could not be compiled with Tom.
We observe that, although the number of generated rules could be significant, the
execution times of the resulting plain TRS are comparable to those obtained with the
native implementation of Tom strategies. This might look somewhat surprising but can be
explained when we take a closer look to the way rewriting rules and strategies are generally
implemented:
• the implementation of a TRS can be done in an efficient way since the complexity of
syntactic pattern matching depends only on the size of the term to reduce and, thanks to
many-to-one matching algorithms [21, 12], the number of rules has almost no impact.
• in Tom, each native strategy constructor is implemented by a Java class with a visit
method which implements (i.e. interprets) the semantics of the corresponding operator.
The evaluation of a strategy S on a term t is implemented thus by a call S.visit(t) and
an exception (VisitFailure) is thrown when the application of a strategy fails.
In the generated TRS, the memory allocation involved in the construction of terms headed
by the ⊥ symbol encoding failure appears to be more efficient than the costly Java exception
handling. This is reflected by better performances of the plain TRS implementation compared
to the exception-based native implementation (especially when the strategy involves a lot of
failures). We obtain performances with the generated TRS comparable to an exception-free
native implementation of strategies (as we can see with the columns TRS and Tom* in
Table 2), because efficient normalization techniques can be used for the plain TRS, since its
rewrite rules are not controlled by a programmable strategy.
7. Conclusions and further work
We have proposed a translation of programmable strategies into plain rewrite rules that we
have proven sound and complete; Figure 5 summarizes the obtained results. Well-established
termination methods can be thus used to (dis)prove the termination of the obtained TRS
and we can deduce, as a direct consequence, the property for the corresponding strategy.
Alternatively, the translation can be used as a strategy compiler for languages which do not
implement natively such primitives.
The translation has been also adapted to cope with many-sorted signatures, and although
the size of the obtained encodings could be smaller than in the unsorted case, it still depends
strongly on the underlying signature. We have proposed a meta-level representation of the
terms and a corresponding translation which produces encodings whose size depends to a
lesser extent on the signature and are significantly smaller than the ones obtained with the
(un)sorted translation.
The translation has been implemented in Tom and can generate, for the moment, plain
TRS using either a Tom or an AProVE/TTT2 syntax. We have experimented with classic
strategies and AProVE and TTT2 have been able to (dis)prove the termination even
when the number of generated rules was significant. The performances for the generated
executable TRS are comparable to the ones of the Tom built-in (exception-free) strategies.

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

33

t −→
→T(S) u
<D KS Zb

Sect. 3
[8]

Lemma 4.3

Lemma 5.7



` S19 ◦ t =⇒em u
|

qy

Sect. 4

Sect. 5

_t^ −→
→TM (S) _u^

%-

"

t : s −→
→TS (S) u : s

Figure 5: Relationships between the different encodings of this paper
The framework can be of course improved. When termination is disproven and a
counterexample can be exhibited, it is interesting to reproduce the corresponding infinite
reductions in terms of strategy derivations. Since the TRS reductions corresponding to
distinct (sub-)strategy derivations are not interleaved, we think that, when the infinite
reduction starts with a term headed by the symbol encoding the strategy, the back-translation
of the counterexample provided by the termination tools can be automatized. When the
counterexample concerns another symbol than the one encoding the strategy we could try to
rebuild a complete infinite reduction by a backward application of the rules in the encoding
until an appropriate term (headed by the symbol encoding the strategy) is found; although
such an approach wouldn’t work in all the cases it could give valuable warnings concerning
the design of the strategy under investigation.
As far as the executable TRS is concerned, we intend to develop new backends allowing
the integration of programmable strategies in other languages than Tom.
Acknowledgments. We would like to thank the anonymous referees for their valuable
comments and suggestions that led to a substantial improvement of the paper.
References
[1] Beatriz Alarcón, Raúl Gutiérrez, and Salvador Lucas. Context-sensitive dependency pairs. Information
and Computation, 208(8):922–968, 2010.
[2] Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theoretical
Computer Science, 236(12):133 – 178, 2000.
[3] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
[4] Emilie Balland, Paul Brauner, Radu Kopetz, Pierre-Etienne Moreau, and Antoine Reilles. Tom: Piggybacking rewriting on java. In RTA ’07, volume 4533 of LNCS, pages 36–47. Springer-Verlag, 2007.
[5] Emilie Balland, Pierre-Etienne Moreau, and Antoine Reilles. Effective strategic programming for Java
developers. Software: Practice and Experience, 44(2):129–162, 2012.
[6] Peter Borovanský, Claude Kirchner, Hélène Kirchner, Pierre-Etienne Moreau, and Christophe Ringeissen.
An overview of ELAN. In WRLA ’98, volume 15. ENTCS, 1998.
[7] Horatiu Cirstea, Claude Kirchner, Radu Kopetz, and Pierre-Etienne Moreau. Anti-patterns for rule-based
languages. Journal of Symbolic Computation, 45(5):523 – 550, 2010. Symbolic Computation in Software
Science.

34

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

[8] Horatiu Cirstea, Sergueı̈ Lenglet, and Pierre-Etienne Moreau. A faithful encoding of programmable
strategies into term rewriting systems. In RTA ’15, volume 36 of LIPIcs, pages 74–88. Schloss Dagstuhl Leibniz-Zentrum fuer Informatik, 2015.
[9] Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martı́-Oliet, José Meseguer, and
Carolyn Talcott. The Maude 2.0 System. In RTA ’03, volume 2706 of LNCS, pages 76–87. Springer-Verlag,
2003.
[10] Jörg Endrullis and Dimitri Hendriks. From outermost to context-sensitive rewriting. In RTA ’09, volume
5595 of LNCS, pages 305–319. Springer, 2009.
[11] Yuki Tomofumi et al. Alphaz: A system for design space exploration in the polyhedral model. Technical
Report CS-12-101, Colorado State University, 2012.
[12] Fabrice Le Fessant and Luc Maranget. Optimizing pattern matching. In ICFP ’01, pages 26–37. ACM
Press, 2001.
[13] Olivier Fissore, Isabelle Gnaedig, and Hélène Kirchner. Simplification and termination of strategies in
rule-based languages. In PPDP ’03, pages 124–135. ACM, 2003.
[14] Carsten Fuhs, Jürgen Giesl, Michael Parting, Peter Schneider-Kamp, and Stephan Swiderski. Proving
termination by dependency pairs and inductive theorem proving. Journal of Automated Reasoning,
47(2):133–160, 2011.
[15] Jürgen Giesl and Aart Middeldorp. Innermost termination of context-sensitive rewriting. In DLT ’02,
volume 2450 of LNCS, pages 231–244. Springer, 2002.
[16] Jürgen Giesl and Aart Middeldorp. Transformation techniques for context-sensitive rewrite systems.
Journal of Functional Programming, 14(4):379–427, 2004.
[17] Jürgen Giesl, Matthias Raffelsieper, Peter Schneider-Kamp, Stephan Swiderski, and René Thiemann.
Automated termination proofs for haskell by term rewriting. ACM Transactions on Programming
Languages and Systems, 33(2):7, 2011.
[18] Jürgen Giesl, René Thiemann, and Stephan Falke. Mechanizing and improving dependency pairs. Journal
of Automated Reasoning, 37:2006, 2006.
[19] Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in
Theoretical Computer Science. Cambridge University Press, 1989.
[20] Isabelle Gnaedig and Hélène Kirchner. Termination of rewriting under strategies. ACM Transactions on
Computational Logic, 10(2), 2009.
[21] Albert Gräf. Left-to-right tree pattern matching. In RTA ’91, volume 488 of LNCS, pages 323–334.
Springer-Verlag, April 1991.
[22] Nao Hirokawa and Aart Middeldorp. Automating the dependency pair method. Information and
Computation, 199(12):172 – 199, 2005.
[23] B. Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of
Mathematics. North Holland, Amsterdam, 1999.
[24] Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: a rule-based survey
of unification. In Computational Logic. Essays in honor of Alan Robinson, chapter 8, pages 257–321.
The MIT press, 1991.
[25] Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations.
SIAM Journal of Computing, 15(4):1155–1194, 1986.
[26] Markus Kaiser and Ralf Lämmel. An Isabelle/HOL-based model of stratego-like traversal strategies. In
PPDP ’09, pages 93–104. ACM, 2009.
[27] Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. Tyrolean Termination Tool 2.
In RTA ’09, volume 5595 of LNCS, pages 295–304. Springer-Verlag, 2009.
[28] Ralf Lämmel, Simon J. Thompson, and Markus Kaiser. Programming errors in traversal programs over
structured data. Science of Computer Programing, 78(10):1770–1808, 2013.
[29] Marı́a Manzano. Many-sorted logic and its applications. chapter Introduction to Many-sorted Logic,
pages 3–86. John Wiley & Sons, Inc., New York, NY, USA, 1993.
[30] José Meseguer and Christiano Braga. Modular rewriting semantics of programming languages. In
Algebraic Methodology and Software Technology, volume 3116 of LNCS, pages 364–378. Springer Berlin
Heidelberg, 2004.
[31] Pierre-Etienne Moreau, Christophe Ringeissen, and Marian Vittek. A Pattern Matching Compiler for
Multiple Target Languages. In CC ’03, volume 2622 of LNCS, pages 61–76. Springer-Verlag, 2003.
[32] Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer-Verlag, 2002.

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

35

[33] Chris Okasaki. Red-black trees in a functional setting. Journal of Functional Programming, 9(4):471–477,
1999.
[34] Matthias Raffelsieper and Hans Zantema. A transformational approach to prove outermost termination
automatically. ENTCS, 237:3–21, 2009.
[35] Grigore Rosu and Traian-Florin Serbanuta. An overview of the K semantic framework. Journal of Logic
and Algebraic Programming, 79(6):397–434, 2010.
[36] Terese. Term Rewriting Systems. Cambridge University Press, 2003. M. Bezem, J. W. Klop and R. de
Vrijer, eds.
[37] René Thiemann. From outermost termination to innermost termination. In SOFSEM ’09, volume 5404
of LNCS, pages 533–545. Springer, 2009.
[38] René Thiemann and Aart Middeldorp. Innermost termination of rewrite systems by labeling. ENTCS,
204:3–19, 2008.
[39] Eelco Visser. Stratego: A language for program transformation based on rewriting strategies. System
description of Stratego 0.5. In RTA ’01, volume 2051 of LNCS, pages 357–361. Springer-Verlag, 2001.
[40] Eelco Visser. A survey of strategies in rule-based program transformation systems. Journal of Symbolic
Computation, 40(1):831 – 873, 2005.
[41] Eelco Visser, Zine-el-Abidine Benaissa, and Andrew Tolmach. Building program optimizers with rewriting
strategies. In ICFP ’98, pages 13–26. ACM Press, 1998.
[42] Stephen Wolfram. The Mathematica Book. Wolfram Media, Incorporated, 5 edition, 2003.

36

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

8. Proofs for the Regular Translation
Lemma 8.1 (Propagation lemma). Let t ∈ T (F), S, and Γ such that FVarX (S) ⊆
DomX (Γ). We have B(Γ) ∪ T(S) • ϕS (⊥(t)) −→
→ ⊥(t), and if B(Γ) ∪ T(S) • ϕS (⊥(t)) −→
→ u,
then u = ⊥(t).
Proof. For all S 6= X, the only rule in B(Γ) ∪ T(S) that can rewrite ϕS (⊥(t)) is ϕS (⊥(t)) _
⊥(t). For S = X, because X ∈ DomX (Γ), B(Γ) contains the rule ϕX (⊥(t)) _ ⊥(t), and it
is also the only rule that can rewrite ϕX (⊥(t)).
Lemma 8.2 (Rigid). Given a term t ∈ T (F), a strategy S, and a context Γ, the term t
is in normal form w.r.t. B(Γ) ∪ T(S). If B(Γ) ∪ T(S 0 ) • ϕS (t) −→
→ u, then S = X and
X ∈ DomX (Γ), or T(S) ⊆ B(Γ) ∪ T(S 0 ).
Proof. A term t ∈ T (F) does not contain any ϕ symbols, and all the rules in B(Γ) ∪ T(S)
assumes a ϕ symbol at the root, hence the first result holds.
Because of this result, if B(Γ) ∪ T(S 0 ) • ϕS (t) −→
→ u, then B(Γ) ∪ T(S 0 ) contains a rule
of the form ϕS ( ) _ . . .. If S 6= X, then it is possible only if Γ or S 0 contains S, and then it
is easy to prove that T(S) ⊆ B(Γ) ∪ T(S 0 ).
If S = X, then only the translation of contexts or recursive strategies generate rules
than can rewrite a term of the form ϕX (t). But according to the Barendregt convention, any
recursive strategy in Γ or S 0 will be of the form µY.S 00 , with Y 6= X. The only remaining
possibility is B(Γ) • ϕX (t) −→
→ u, which is possible only if Γ binds X.
Lemma 8.3. If B(Γ) ∪ T(S) • ϕS (t) −→
→ u, then t ∈ T (F) or t = ⊥( ).
Proof. Immediate by definition of the translation.
Lemma 8.4 (Initial term as failure). Given a term t ∈ T (F), if B(Γ)∪T(S)•ϕS (t) −→
→ ⊥(t0 )
then t = t0 .
Proof. By induction on the length of the reduction B(Γ) ∪ T(S) • ϕ(t) −→
→ ⊥(t0 ).
If S = Identity, it is not possible to obtain ⊥(t0 ) from ϕIdentity (t), because t ∈ T (F).
If S = Fail , then because t ∈ T (F), the only rule that can be applied to ϕFail (t) is
ϕFail (x @ !⊥( )) _ ⊥(x), and we obtain ⊥(t), as wished.
If S = l _ r, then the only rule that can be applied to ϕl_r (t) (with t ∈ T (F)) to
produce ⊥(t0 ) is ϕl_r (x @ !l) _ ⊥(x), and we obtain ⊥(t), as required.
Suppose S = S1 ; S2 . Because T(S1 ) and T(S2 ) cannot reduce ϕS1 ;S2 (t) (by Lemma 8.2),
the first rule to be applied is ϕS1 ;S2 (x @ !⊥( )) _ ϕ; (ϕS2 (ϕS1 (x)), x), and we obtain
ϕ; (ϕS2 (ϕS1 (t)), t). By Lemma 8.3, B(Γ)∪T(S2 ) cannot reduce ϕS2 (ϕS1 (t)), and by Lemma 8.2,
only T(S1 ) (or B(Γ) is S1 = X) can reduce ϕS1 (t). We have several possibilities. If
B(Γ) ∪ T(S1 ) • ϕS1 (t) −→
→ ⊥(u), then by induction, u = t, and by Lemma 8.1, B(Γ) ∪
T(S2 ) • ϕ; (ϕS2 (⊥(t)), t) −→
→ ϕ; (⊥(t), t). The only rule that can be applied to the latter term is ϕ; (⊥( ), x) _ ⊥(x), and we obtain ⊥(t), as wished. Otherwise, we have
B(Γ) ∪ T(S1 ) • ϕS1 (t) −→
→ u. Because we obtain ⊥(t0 ) as a result, necessarily the rule
ϕ; (⊥( ), x) _ ⊥(x) has been applied, which means that B(Γ) ∪ T(S2 ) • ϕS2 (u) −→
→ ⊥(t00 ) for
some t00 . By induction, t00 = u, and consequently, B(Γ) ∪ T(S2 ) • ϕ; (ϕS2 (u), t) −→
→ ϕ; (⊥(u), t).
We then have {ϕ; (⊥( ), x) _ ⊥(x)} • ϕ; (⊥(u), t) −→
→ ⊥(t), as required.
Suppose S = S1 ←
+ S2 . Because T(S1 ) and T(S2 ) cannot reduce ϕS1 ←
+S2 (t) (by
Lemma 8.2), the first rule to be applied is ϕS1 ←
+ (ϕS1 (x)), and we
+S2 (x @ !⊥( )) _ ϕ←
obtain ϕ←
+ (ϕS1 (t)). By Lemma 8.2, only T(S1 ) (or B(Γ) is S1 = X) can reduce ϕS1 (t). We

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

37

have two possibilities. If B(Γ) ∪ T(S1 ) • ϕS1 (t) −→
→ ⊥(u), then by induction u = t, and
then {ϕ←
(⊥(x))
_
ϕ
(x)}
•
ϕ
(⊥(t))
−→
→
ϕ
(t).
By Lemma 8.2, only T(S2 ) (or B(Γ) is
+
←
+
S2
S2
S2 = X) can reduce ϕS2 (t), therefore we have B(Γ) ∪ T(S2 ) • ϕS2 (t) −→
→ ⊥(t0 ). By induction,
we have t = t0 , and the result holds. Otherwise, we have B(Γ) ∪ T(S1 ) • ϕS1 (t) −→
→ u with
u ∈ T (F). But then, the only rule that can be applied to ϕ←
+ (u) is ϕ←
+ (x @ !⊥( )) _ x,
and we obtain u ∈ T (F) as a result of the reduction of ϕS1 ←
+S2 (t), which is in contradiction
with the original hypothesis.
Suppose S = µX.S 0 . Because T(S 0 ) cannot reduce ϕµX.S 0 (t) (by Lemma 8.2), the first
rule to be applied is ϕµX.S 0 (Y @ !⊥( )) _ ϕS 0 (Y ), and we obtain ϕS 0 (t). We therefore have
B(Γ) ∪ T(µX.S 0 ) • ϕS 0 (t) −→
→ ⊥(t0 ) with less steps than the original reduction. Besides,
0
0
only T(S ) (or B(Γ) if S = X) can reduce ϕS 0 (t) (Lemma 8.2), therefore we have in fact
B(Γ) ∪ T(S 0 ) • ϕS 0 (t) −→
→ ⊥(t0 ). By induction, t0 = t, and the result holds.
Suppose S = X. By Lemma 8.2, only B(Γ) can reduce ϕX (t), and assuming X : S 0
belongs to Γ, the only rule that can be applied is ϕX (Y @ !⊥( )) _ ϕS 0 (Y ), which generates
ϕS 0 (t). Only T(S 0 ) (or B(Γ) if S 0 = Z) can reduce ϕS 0 (t) (Lemma 8.2), therefore we have
B(Γ) ∪ T(S 0 ) • ϕS 0 (t) −→
→ ⊥(t0 ) with less steps than the original reduction. By induction,
0
t = t, and the result holds.
Suppose S = All (S 0 ). If t is a constant c, then we cannot obtain ⊥(t0 ). Suppose
t = f (t1 , . . . , tn ). Because T(S 0 ) cannot reduce ϕAll(S 0 ) (t) (by Lemma 8.2), the first rule to
be applied is ϕAll(S) (f (x1 , . . . , xn )) _ ϕf (ϕS 0 (x1 ), . . . , ϕS 0 (xn ), f (x1 , . . . , xn )) to generate
ϕf (ϕS 0 (t1 ), . . . , ϕS 0 (tn ), f (t1 , . . . , tn )). Note that according to Lemma 8.2, the rules in
B(Γ)∪T(All (S 0 )) cannot rewrite f (t1 , . . . , tn ) in ϕf (ϕS 0 (t1 ), . . . , ϕS 0 (tn ), f (t1 , . . . , tn )). From
this term, the only possibility to obtain ⊥(t0 ) is to apply one of the rules of the form
ϕf ( , . . . ⊥( ), . . . , , z) _ ⊥(z), which generates f (t1 , . . . , tn ), as wished.
Suppose S = One(S 0 ). If t is a constant c, then the only rule that can be applied is ϕOne(S 0 ) (c) _ ⊥(c), hence the result holds. Suppose t = f (t1 , . . . , tn ). Because T(S 0 ) cannot reduce ϕOne(S 0 ) (t) (by Lemma 8.2), the first rule to be applied is
ϕOne(S 0 ) (f (x1 , . . . , xn )) _ ϕf1 (ϕS 0 (x1 ), x2 , . . . , xn ), which generates ϕf1 (ϕS 0 (t1 ), t2 , . . . , tn ).
Only T(S 0 ) (or B(Γ) if S 0 = X) can reduce ϕS 0 (t1 ). Suppose B(Γ) ∪ T(S 0 ) • ϕS 0 (t1 ) −→
→u
with u ∈ T (F). Then we can only apply the rule ϕf1 (x1 @ !⊥( ), x2 , . . . , xn ) _ f (x1 , . . . , xn )
to ϕf1 (u, t2 , . . . , tn ), and we obtain f (u, t2 , . . . , tn ), in contradiction with the initial hypothesis. Therefore, B(Γ) ∪ T(S 0 ) • ϕS 0 (t1 ) −→
→ ⊥(t01 ), in less steps than the original
0
reduction. By induction, t1 = t1 . We can only apply the rule ϕf1 (⊥(x1 ), x2 , . . . , xn ) _
ϕf2 (⊥(x1 ), ϕS (x2 ), . . . , xn ) to ϕf1 (⊥(t1 ), t2 , . . . , tn ), and we obtain ϕf2 (⊥(t1 ), ϕS 0 (t2 ), . . . , tn ).
With the same reasoning, we have B(Γ) ∪ T(S 0 ) • ϕS 0 (ti ) −→
→ ⊥(ti ) for all i, and we therefore
have B(Γ) ∪ T(One(S 0 )) • ϕS 0 (ϕf1 (ϕS 0 (t1 ), t2 , . . . , tn )) −→
→ ϕfn (⊥(t1 ), . . . , ⊥(tn )). We can
apply only the rule ϕfn (⊥(x1 ), . . . , ⊥(xn )) _ ⊥(f (x1 , . . . , xn )) to the latter term, and we
obtain ⊥(f (t1 , . . . tn )), as required.
Theorem 3.5 (Simulation). Given a term t ∈ T (F), a strategy S and a context Γ such
that FVarX (S) ⊆ DomX (Γ),
(1) Γ ` S ◦ t =⇒ t0 iff T(S) ∪ B(Γ) • ϕS (t) −→
→ t0 , t0 ∈ T (F)
(2) Γ ` S ◦ t =⇒ Fail iff T(S) ∪ B(Γ) • ϕS (t) −→
→ ⊥(t)
Proof. By induction on the height of derivation tree and respectively of on the length of the
reduction.
S := Identity | Fail | l _ r | S1 ; S2 | S1 ←
+ S2 | One(s) | All (s) | µX.S 0

38

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

Base case: S := Identity | Fail | l _ r
(1) S := Identity
Independently of Γ, for all t ∈ T (F) we have
Γ ` Identity ◦ t =⇒ t
and
→t
{ϕIdentity (x @ !⊥( )) _ x } ∪ B(Γ) • ϕIdentity (t) −→

(2) S := Fail
Independently of Γ, for all t ∈ T (F) we have

Γ ` Fail ◦ t =⇒ Fail
and
{ϕFail (x @ !⊥( )) _ ⊥(x) } ∪ B(Γ) • ϕFail (t) −→
→ ⊥(t)

(3) S := l _ r
(a) S ⇒ T(S) ∪ B(Γ)
If Γ ` l _ r ◦ t =⇒ u then ∃σ, σ(l ) = t and σ(r ) = u. Then, σ(ϕl_r (l )) = ϕl_r (t)
and thus ϕl_r (l) _ r • ϕl_r (t) −→
→ u.
If Γ ` l _ r ◦ t =⇒ Fail then 6 ∃σ, σ(l ) = t and thus 6 ∃σ, σ(ϕl_r (l )) = ϕl_r (t).
The rewrite rule ϕl_r (l) _ r cannot be applied to ϕl_r (t) at the head position.
Since ϕl_r is a fresh symbol (6 ∃p s.t. t(p) = ϕl_r ) the rule cannot be applied to
another position of ϕl_r (t). Since 6 ∃σ, σ(ϕl_r (l )) = ϕl_r (t) then ϕl_r (t) is in the
semantics of ϕl_r (!l) and thus the rule ϕl_r (x @ !l) _ ⊥(x) can be applied and
the result is ⊥(t).
(b) T(S) ∪ B(Γ) ⇒ S
If the rule ϕl_r (l) _ r is used then, since ϕl_r does not occur in t, it can be
only applied at the head position of ϕl_r (t) and thus ∃σ, σ(ϕl_r (l )) = ϕl_r (t) and
σ(r ) = u. Since u contains no ϕl_r (the codomain of σ contains no ϕl_r because
it does not occur in t) and the only rules in B(Γ) concerning ϕl_r could be at most
the same as those in T(l _ r) then u is in normal form w.r.t. T(l _ r) ∪ B(Γ). We
have then that ∃σ, σ(l ) = t and thus l _ r ◦ t =⇒ u. Since ϕl_r is a fresh symbol
then there is no other way to apply the rewrite rule ϕl_r (l) _ r to ϕl_r (t).
If the rule ϕl_r (x @ !l) _ ⊥(x) is applied then it is applied at the top position
(ϕl_r fresh) and ∃σ = {t/x}, σ(ϕl_r (x @ !l)) = ϕl_r (t) and 6 ∃µ, µ(l ) = ϕl_r (t).
Consequently, Γ ` l _ r ◦ t =⇒ Fail. We have ϕl_r (x @ !l) _ ⊥(x) • t −→
→ ⊥(t),
and because ϕ symbols do not occur in t, then ⊥(t) is in normal form w.r.t.
T(l _ r) ∪ B(Γ). Because ⊥ is a fresh symbol then 6 ∃σ, σ(⊥(x)) = t and the rule
ϕl_r (⊥(x)) _ ⊥(x) cannot be applied to ϕl_r (t).
Induction: S := S1 ; S2 | S1 ←
+ S2 | One(S 0 ) | All (S 0 ) | µX.S 0
(1) S := S1 ; S2
(a) S ⇒ T(S)
Since Γ ` S1 ; S2 ◦ t =⇒ u then Γ ` S1 ◦ t =⇒ v and Γ ` S2 ◦ v =⇒ u with a shorter
derivation tree. By induction, B(Γ) ∪ T(S1 ) • ϕS1 (t) −→
→ v and B(Γ) ∪ T(S2 ) •
ϕS2 (v) −→
→ u. We have ϕS1 ;S2 (x @ !⊥( )) _ ϕ; (ϕS2 (ϕS1 (x)), x) • ϕS1 ;S2 (t) −→
→
ϕ; (ϕS2 (ϕS1 (t)), t). By the induction hypothesis, B(Γ)∪T(S1 )•ϕ; (ϕS2 (ϕS1 (t)), t) −→
→
ϕ; (ϕS2 (v), t) and B(Γ)∪T(S2 )•ϕ; (ϕS2 (v), t) −→
→ ϕ; (u, t). Finally, ϕ; (x@!⊥( ), ) _
x • ϕ; (u, t) −→
→ u.

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

39

If Γ ` S1 ; S2 ◦ t =⇒ Fail then Γ ` S1 ◦ t =⇒ Fail, or Γ ` S1 ◦ t =⇒ v and
Γ ` S2 ◦ v =⇒ Fail. For the first case, by induction, B(Γ) ∪ T(S1 ) • ϕS1 (t) −→
→ ⊥(t).
We have ϕS1 ;S2 (x @ !⊥( )) _ ϕ; (ϕS2 (ϕS1 (x)), x) • ϕS1 ;S2 (t) −→
→ ϕ; (ϕS2 (ϕS1 (t)), t)
and, by induction, B(Γ) ∪ T(S1 ) • ϕ; (ϕS2 (ϕS1 (t)), t) −→
→ ϕ; (ϕS2 (⊥(t)), t). By
Lemma 8.1, B(Γ) ∪ T(S2 ) • ϕ; (ϕS2 (⊥(t)), t) −→
→ ϕ; (⊥(t), t) and ϕ; (⊥( ), x) _
⊥(x) • ϕ; (⊥(t), t) −→
→ ⊥(t). For the second case, by induction, B(Γ) ∪ T(S1 ) •
ϕS1 (t) −→
→ v and B(Γ) ∪ T(S2 ) • ϕS2 (v) −→
→ ⊥(v). We have, ϕS1 ;S2 (x @ !⊥( )) _
ϕ; (ϕS2 (ϕS1 (x)), x) • ϕS1 ;S2 (t) −→
→ ϕ; (ϕS2 (ϕS1 (t)), t). By induction, B(Γ) ∪ T(S1 ) •
→ ϕ; (⊥(v), t).
ϕ; (ϕS2 (ϕS1 (t)), t) −→
→ ϕ; (ϕS2 (v), t) and B(Γ) ∪ T(S2 ) • ϕ; (ϕS2 (v), t) −→
Finally, ϕ; (⊥( ), x) _ ⊥(x) • ϕ; (⊥(v), t) −→
→ ⊥(t).
(b) T(S) ⇒ S
If B(Γ) ∪ T(S1 ; S2 ) • ϕS1 ;S2 (t) −→
→ u, since t ∈ T (F) contains no ϕ symbols, the
first reduction is necessarily ϕS1 ;S2 (x @ !⊥( )) _ ϕ; (ϕS2 (ϕS1 (x)), x) • ϕS1 ;S2 (t) −→
→ ϕ; (ϕS2 (ϕS1 (t)), t). According to Lemma 8.2, ϕS1 (t) can only be reduced by
B(Γ)∪T(S1 ), which gives B(Γ)∪T(S1 )•ϕ; (ϕS2 (ϕS1 (t)), t) −→
→ ϕ; (ϕS2 (v), t) for some
v. If we had B(Γ) ∪ T(S1 ) • ϕS1 (t) −→
→ ⊥(t), the ⊥ would have been propagated (by
Lemma 8.1) and the final result would have been ⊥(t) which contradicts the initial
hypothesis. By induction (the latter reduction needs less steps than the initial one),
Γ ` S1 ◦t =⇒ v. Next, the only possible reduction is B(Γ)∪T(S2 )•ϕ; (ϕS2 (v), t) −→
→
ϕ; (u, t) and then ϕ; (x@ !⊥( ), ) _ x•ϕ; (u, t) −→
→ u. By induction, Γ ` S2 ◦v =⇒ u
and since Γ ` S1 ◦ t =⇒ v we can conclude that Γ ` S1 ; S2 ◦ t =⇒ u.
If B(Γ)∪T(S1 ; S2 )•ϕS1 ;S2 (t) −→
→ ⊥(t), since ϕS1 ;S2 (t) is in normal form w.r.t. B(Γ)∪
T(S1 ) and B(Γ) ∪ T(S2 ) (according to Lemma 8.2), the first reduction is necessarily
ϕS1 ;S2 (x @ !⊥( )) _ ϕ; (ϕS2 (ϕS1 (x)), x) • ϕS1 ;S2 (t) −→
→ ϕ; (ϕS2 (ϕS1 (t)), t). The only
way to obtain ⊥(t) as a result is to have a reduction B(Γ)∪T(S1 ; S2 )•ϕS2 (ϕS1 (t)) −→
→
⊥(v). Thus, either B(Γ)∪T(S1 ; S2 )•ϕS1 (t) −→
→ v 0 and B(Γ)∪T(S1 ; S2 )•ϕS2 (v 0 ) −→
→
⊥(v) or B(Γ)∪T(S1 ; S2 )•ϕS1 (t) −→
→ ⊥(v) and B(Γ)∪T(S1 ; S2 )•ϕS2 (⊥(v)) −→
→ ⊥(v)
(by Lemma 8.1). In the first case, we have B(Γ)∪T(S1 )•ϕS1 (t) −→
→ v 0 since only the
rules in B(Γ)∪T(S1 ) can reduce ϕS1 (t) and, by induction, Γ ` S1 ◦t =⇒ v 0 . Similarly,
B(Γ) ∪ T(S2 ) • ϕS2 (v 0 ) −→
→ ⊥(v) and, by Lemma 8.4, v 0 = v. Thus, by induction,
0
Γ ` S2 ◦ v =⇒ Fail. Consequently, Γ ` S1 ; S2 ◦ t =⇒ Fail. For the second case,
as previously, we have that B(Γ) ∪ T(S1 ) • ϕS1 (t) −→
→ ⊥(v) and, by Lemma 8.4,
v = t. By induction, Γ ` S1 ◦ t =⇒ Fail and consequently, Γ ` S1 ; S2 ◦ t =⇒ Fail.
(2) S := µX.S 0
(a) S ⇒ T(S)
Since Γ ` µX.S 0 ◦t =⇒ u then Γ; X : S 0 ` S 0 ◦t =⇒ u with the latter having a shorter
derivation tree and thus, by induction, B(Γ; X : S 0 ) ∪ T(S 0 ) • ϕS 0 (t) −→
→ u. The
only possible reduction of ϕµX.S 0 (t) w.r.t. B(Γ) ∪ T(µX.S 0 ) is obtained by applying
ϕµX.S 0 (Y @ !⊥( )) _ ϕS 0 (Y ) which results in the term ϕS 0 (t). Since, by induction,
B(Γ; X : S 0 ) ∪ T(S 0 ) • ϕS 0 (t) −→
→ u and since B(Γ; X : S 0 ) ∪ T(S 0 ) ⊆ B(Γ) ∪ T(µX.S 0 )
we eventually have B(Γ) ∪ T(µX.S 0 ) • ϕµX.S 0 (t) −→
→ u.
If Γ ` µX.S 0 ◦ t =⇒ Fail then Γ; X : S 0 ` S 0 ◦ t =⇒ Fail. Using the same reasoning
as for the successful case we obtain B(Γ) ∪ T(µX.S 0 ) • ϕµX.S 0 (t) −→
→ ⊥(t).
(b) T(S) ⇒ S
If B(Γ) ∪ T(µX.S 0 ) • ϕµX.S 0 (t) −→
→ u since t ∈ T (F) contains no ϕ symbols and B(Γ)
contains no rules potentially rewriting ϕµX.S 0 (t), the first reduction is necessarily

40

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

→ ϕS 0 (t) and thus B(Γ) ∪ T(µX.S 0 ) •
ϕµX.S 0 (Y @ !⊥( )) _ ϕS 0 (Y ) • ϕµX.S 0 (t) −→
ϕS 0 (t) −→
→ u in strictly less steps than the original reduction. We also have
that B(Γ; X : S 0 ) ∪ T(S 0 ) = B(Γ) ∪ T(µX.S 0 ) \ {ϕµX.S 0 (⊥(Y )) _ ⊥(Y ), ϕµX.S 0 (Y @
!⊥( )) _ ϕS 0 (Y )} and since ϕS 0 (t) and all its reducts w.r.t. B(Γ) ∪ T(µX.S 0 )
contain no ϕµX.S 0 then B(Γ; X : S 0 ) ∪ T(S 0 ) • ϕS 0 (t) −→
→ u (in strictly less steps
than the original reduction). By induction, Γ; X : S 0 ` S 0 ◦ t =⇒ u and thus
Γ ` µX.S 0 ◦ t =⇒ u.
If B(Γ) ∪ T(µX.S 0 ) • ϕµX.S 0 (t) −→
→ ⊥(t) the first reduction is still ϕµX.S 0 (Y @
0
0
!⊥( )) _ ϕS (Y )•ϕµX.S (t) −→
→ ϕS 0 (t) and thus B(Γ)∪T(µX.S 0 )•ϕS 0 (t) −→
→ ⊥(u)
in strictly less steps than the original reduction. With the same arguments as before
we obtain Γ; X : S 0 ` S 0 ◦ t =⇒ Fail and thus Γ ` µX.S 0 ◦ t =⇒ Fail.
(3) S := X
(a) S ⇒ T(S)
Since Γ; X : S 0 ` X ◦ t =⇒ u then Γ; X : S 0 ` S 0 ◦ t =⇒ u with the latter having a
shorter derivation tree and thus, by induction, B(Γ; X : S 0 ) ∪ T(S 0 ) • ϕS 0 (t) −→
→ u.
Since we supposed all bound variables (by a µ operator or a context assignment) to
have different names, the only rewrite rules in B(Γ; X : S 0 ) involving ϕX are the ones
generated by the context assignment: ϕX (⊥(Y )) _ ⊥(Y ) and ϕX (Y @ !⊥( )) _
ϕS 0 (Y ). Consequently, the only possible reduction of ϕX (t) w.r.t. B(Γ; X : S 0 ) is
obtained by applying the latter rule which results in the term ϕS 0 (t). It is easy to
check that B(Γ; X : S 0 )∪T(S 0 ) = B(Γ; X : S 0 ). Consequently B(Γ; X : S 0 )•ϕS 0 (t) −→
→ u and thus B(Γ; X : S 0 ) • ϕX (t) −→
→ u. If Γ; X : S 0 ` X ◦ t =⇒ Fail then
0
0
Γ; X : S ` S ◦ t =⇒ Fail. Using the same reasoning as for the successful case we
obtain B(Γ; X : S 0 ) • ϕX (t) −→
→ ⊥(t).
(b) T(S) ⇒ S
If B(Γ; X : S 0 ) • ϕX (t) −→
→ u since t ∈ T (F) contains no ϕ symbols and since, as
explained before the only rewrite rules in B(Γ; X : S 0 ) involving ϕX are the ones
generated by the context assignment, the first reduction is necessarily ϕX (Y @
!⊥( )) _ ϕS 0 (Y ) • ϕX (t) −→
→ ϕS 0 (t) and thus B(Γ; X : S 0 ) • ϕS 0 (t) −→
→ u in strictly
less steps than the original reduction. We have B(Γ; X : S 0 ) ∪ T(S 0 ) = B(Γ; X : S 0 )
and thus B(Γ; X : S 0 ) ∪ T(S 0 ) • ϕS 0 (t) −→
→ u (in strictly less steps than the original
reduction). By induction, Γ; X : S 0 ` S 0 ◦ t =⇒ u and thus Γ; X : S 0 ` X ◦ t =⇒ u.
If B(Γ; X : S 0 ) • ϕX (t) −→
→ ⊥(t) the first reduction is still ϕX (Y @ !⊥( )) _
ϕS 0 (Y ) • ϕX (t) −→
→ ϕS 0 (t) and thus B(Γ; X : S 0 ) • ϕS 0 (t) −→
→ ⊥(u) in strictly less
steps than the original reduction. With the same arguments as before we obtain
Γ; X : S 0 ` S 0 ◦ t =⇒ Fail and thus Γ; X : S 0 ` X ◦ t =⇒ Fail.
(4) S := S1 ←
+ S2
(a) S ⇒ T(S)
If S1 ←
+ S2 ◦ t =⇒ u then S1 ◦ t =⇒ u or, S1 ◦ t =⇒ Fail and S2 ◦ t =⇒ r. In the first
case, by induction, B(Γ) ∪ T(S1 ) • ϕS1 (t) −→
→ v. We have, ϕS1 ←
+S2 (x @ !⊥( )) _
ϕ←
→ ϕ←
→
+ (ϕS1 (x)) • ϕS1 ←
+ (ϕS1 (t)) and B(Γ) ∪ Tϕ1 (S1 ) • ϕ←
+ (ϕS1 (t)) −→
+S2 (t) −→
ϕ←
(u).
Finally,
ϕ
(x
@
!
⊥(
))
_
x
•
ϕ
(u)
−→
→
u.
For
the
second
case,
by
←
+
←
+
+
induction, B(Γ) ∪ T(S1 ) • ϕS1 (t) −→
→ ⊥(t) and B(Γ) ∪ T(S2 ) • ϕS2 (t) −→
→ u. We
have, as before, ϕS1 ←
→ ϕ←
+ (ϕS1 (x)) • ϕS1 ←
+ (ϕS1 (t))
+S2 (x @ !⊥( )) _ ϕ←
+S2 (t) −→
and B(Γ) ∪ T(S1 ) • ϕ←
(ϕ
(t))
−→
→
ϕ
(⊥(u)).
Then,
ϕ
(⊥(x))
_
ϕS2 (x) •
+ S1
←
+
←
+
ϕ←
(⊥(u))
−→
→
ϕ
(u)
and
finally,
B(Γ)
∪
T(S
)
•
ϕ
(t)
−→
→
u.
+
2
2
S2

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

41

If S1 ←
+ S2 ◦ t =⇒ Fail then S1 ◦ t =⇒ Fail and S2 ◦ t =⇒ Fail. By induction,
B(Γ) ∪ T(S1 ) • ϕS1 (t) −→
→ ⊥(t) and B(Γ) ∪ T(S2 ) • ϕS2 (t) −→
→ ⊥(t). We have,
ϕS1 ←
→ ϕ←
+ (ϕS1 (x)) • ϕS1 ←
+ (ϕS1 (t)) and B(Γ) ∪ T(S1 ) •
+S2 (x @ !⊥( )) _ ϕ←
+S2 (t) −→
ϕ←
→ ϕ←
→ ϕS2 (u)
+ (ϕS1 (t)) −→
+ (⊥(u)). Then, ϕ←
+ (⊥(x)) _ ϕS2 (x) • ϕ←
+ (⊥(u)) −→
and finally, B(Γ) ∪ T(S2 ) • ϕ2 (t) −→
→ ⊥(u).
(b) T(S) ⇒ S
If B(Γ) ∪ T(S1 ←
+ S2 ) • ϕS1 ←
→ u, since t ∈ T (F) contains no ϕ symbols, the
+S2 (t) −→
→
first reduction is necessarily ϕS1 ←
+ (ϕS1 (x)) • ϕS1 ←
+S2 (x @ !⊥( )) _ ϕ←
+S2 (t) −→
ϕ←
(ϕ
(t)).
No
rule
can
be
applied
at
the
top
position
until
ϕ
(t)
is
reduced
to
a
+ S1
S1
term in T (F) or to a term of the form ⊥( ). In the former case, we can only have
B(Γ) ∪ T(S1 ) • ϕS1 (t) −→
→ u in less steps than the original reduction, so by induction,
S1 ◦ t =⇒ u. Consequently, S1 ←
+ S2 ◦ t =⇒ u. In the latter case, we necessarily have
(Lemma 8.4) B(Γ) ∪ T(S1 ) • ϕS1 (t) −→
→ ⊥(t) and B(Γ) ∪ T(S1 ) • ϕ←
→
+ (ϕS1 (t)) −→
Then
we
have
ϕ
(⊥(x))
_
ϕ
(x)
•
ϕ
(⊥(t))
−→
→
ϕ
(t),
which
can
ϕ←
(⊥(t)).
←
+
←
+
+
S2
S2
only be reduced as B(Γ) ∪ T(S2 ) • ϕS2 (t) −→
→ u. By induction, S1 ◦ t =⇒ Fail and
S2 ◦ t =⇒ u and consequently, S1 ←
+ S2 ◦ t =⇒ u.
If B(Γ) ∪ T(S1 ←
+ S2 ) • ϕS1 ←
(t)
−→
→ ⊥(t), since ϕS1 ←
+S2
+S2 (t) is in normal form
w.r.t. B(Γ) ∪ T(S1 ) and B(Γ) ∪ T(S2 ) (Lemma 8.2), the first reduction is necessarily
ϕS1 ←
→ ϕ←
+ (ϕS1 (x)) • ϕS1 ←
+ (ϕS1 (t)). No rule can be
+S2 (x @ !⊥( )) _ ϕ←
+S2 (t) −→
applied at the top position until ϕS1 (t) is reduced to a term in T (F) or to a term of
the form ⊥( ). If it is a term in T (F) then the rule ϕ←
+ (x@!⊥( )) _ x is the only one
that can be applied and the final result is not ⊥(t). Thus, B(Γ) ∪ T(S1 ) • ϕS1 (t) −→
→
⊥(t) (in less steps than the original reduction) and B(Γ) ∪ T(S1 ) • ϕ←
+ (ϕS1 (t)) −→
→ ϕ←
+ (⊥(x)) _ ϕS2 (x) • ϕ←
+ (⊥(t)) −→
+ (⊥(t)). The only possible reduction is ϕ←
→ ϕS2 (t) and then B(Γ) ∪ T(S2 ) • ϕS2 (t) −→
→ ⊥(t) in less steps than the original
reduction. By induction, S1 ◦ t =⇒ Fail and S2 ◦ t =⇒ Fail and consequently,
S1 ←
+ S2 ◦ t =⇒ Fail.
(5) S := All (S 0 )
(a) S ⇒ T(S)
If All (S 0 ) ◦ t =⇒ u with t = f (t1 , . . . , tn ) then ∀i ∈ [1,n], S 0 ◦ ti =⇒ ui and
u = f (u1 , . . . , un ). Then, by induction, B(Γ) ∪ T(S 0 ) • ϕS 0 (ti ) −→
→ ui . When we
apply the rules corresponding to the encoding of All we obtain
ϕAll(S 0 ) (f (x1 , . . . , xn )) _ ϕf (ϕS 0 (x1 ), . . . , ϕS 0 (xn ), f (x1 , . . . , xn ))

•ϕAll(S 0 ) (f (t1 , . . . , tn )) −→
→ ϕf (ϕS 0 (t1 ), . . . , ϕS 0 (tn ), f (t1 , . . . , tn ))

and no other rule can be applied at the top position for this latter term. By
the induction hypothesis we have ϕf (ϕS 0 (t1 ), . . . , ϕS 0 (tn ), f (t1 , . . . , tn ))
ϕf (u1 , . . . , un , f (t1 , . . . , tn )) and subsequently

B(Γ)∪T(S 0 )∗

−→
→

ϕf (x1 @ !⊥( ), . . . , xn @ !⊥( ), ) _ f (x1 , . . . , xn )

•ϕf (u1 , . . . , un , f (t1 , . . . , tn )) −→
→ f (u1 , . . . , un )

All (S 0 )

If
◦ t =⇒ Fail with t = f (t1 , . . . , tn ) then ∃i ∈ [1,n], S 0 ◦ ti =⇒ Fail. By
induction, B(Γ) ∪ T(S 0 ) • ϕS 0 (ti ) −→
→ ⊥(ti ). As before, when we apply the rules

42

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

corresponding to the encoding of All we obtain
ϕAll(S 0 ) (f (x1 , . . . , xn )) _ ϕf (ϕS 0 (x1 ), . . . , ϕS 0 (xn ), f (x1 , . . . , xn ))

•ϕAll(S 0 ) (f (t1 , . . . , tn )) −→
→ ϕf (ϕS 0 (t1 ), . . . , ϕS 0 (tn ), f (t1 , . . . , tn ))

and using induction
ϕf (ϕS 0 (t1 ), . . . , ϕS 0 (ti ), . . . ,ϕS 0 (tn ), f (t1 , . . . , tn ))
B(Γ)∪T(S 0 )

−→
→

ϕf (u1 , . . . , ⊥(ti ), . . . , un , f (t1 , . . . , tn )) .

We have then
ϕf (⊥( ), . . . , , z) _ ⊥(z)

•ϕf (u1 , . . . , ⊥(ti ), . . . , un , f (t1 , . . . , tn )) −→
→ ⊥(f (t1 , . . . , tn ))

as required.
If t is a constant c then All (S 0 )◦c =⇒ c. We have ϕAll(S 0 ) (c) _ ϕc (c)•ϕAll(S 0 ) (c) −→
→ c.
→ ϕc (c) and ϕc ( ) _ c • ϕc (c) −→
(b) T(S) ⇒ S
We consider t = f (t1 , . . . , tn ) and handle the case of a constant later on. If
B(Γ) ∪ T(All (S 0 )) • ϕAll(S 0 ) (t) −→
→ u, since t ∈ T (F) contains no ϕ symbols,
we have first ϕAll(S 0 ) (f (x1 , . . . , xn )) _ ϕf (ϕS 0 (x1 ), . . . , ϕS 0 (xn ), f (x1 , . . . , xn )) •
ϕAll(S 0 ) (f (t1 , . . . , tn )) −→
→ ϕf (ϕS 0 (t1 ), . . . , ϕS 0 (tn ), f (t1 , . . . , tn )). No rule can be
applied at the top position until the ϕS 0 (ti ) are reduced to terms in T (F) or at
least one of them is reduced to a term of the form ⊥( ). The former case holds
only if B(Γ) ∪ T(S 0 ) • ϕS 0 (ti ) −→
→ ui (in less steps than the original reduction) and
ϕf (ϕS 0 (t1 ), . . . , ϕS 0 (tn ), f (t1 , . . . , tn ))

B(Γ)∪T(S 0 )∗

−→
→

ϕf (u1 , . . . , un , f (t1 , . . . , tn )).

This term can be further reduced only by the rule ϕf (x1 @!⊥( ), . . . , xn @!⊥( ), ) _
f (x1 , . . . , xn ) to f (u1 , . . . , un ) = u. By induction, S 0 ◦ ti =⇒ ui . Consequently,
All (S 0 ) ◦ t =⇒ u. In the latter case, we necessarily have (Lemmas 8.4) B(Γ) ∪ T(S 0 ) •
ϕS 0 (ti ) −→
→ ⊥(ti ) for some i, and then
ϕf (. . . , ⊥( ), . . . , , z) _ ⊥(z)

•ϕf (ϕS 0 (t1 ), . . . , ⊥(ti ), . . . , ϕS 0 (tn ), f (t1 , . . . , tn )) −→
→ ⊥(f (t1 , . . . , tn ))

We obtain a term not in T (F), hence a contradiction with the original hypothesis.
If B(Γ) ∪ T(All (S 0 )) • ϕAll(S 0 ) (t) −→
→ ⊥(t), since ϕAll(S 0 ) (t) is in normal form w.r.t.
B(Γ) ∪ T(S 0 ) (Lemma 8.2), the first reduction can only be, as before,
ϕAll(S 0 ) (f (x1 , . . . , xn )) _ ϕf (ϕS 0 (x1 ), . . . , ϕS 0 (xn ), f (x1 , . . . , xn ))

•ϕAll(S 0 ) (f (t1 , . . . , tn )) −→
→ ϕf (ϕS 0 (t1 ), . . . , ϕS 0 (tn ), f (t1 , . . . , tn ))

and no rule can be applied at the top position until the ϕS 0 (ti ) are reduced to terms in
T (F) or at least one of them is reduced to a term of the form ⊥( ). We already handled the former case just before. As we have seen, for the latter case we have B(Γ) ∪
T(S 0 )•ϕS 0 (ti ) −→
→ ⊥(ti ) for some i in less steps than the original reduction, and eventually ϕf (. . . , ⊥( ), . . . , , z) _ ⊥(z) • ϕf (ϕS 0 (t1 ), . . . , ϕS 0 (tn ), f (t1 , . . . , tn )) −→
→
⊥(f (t1 , . . . , tn )). By induction, S 0 ◦ ti =⇒ Fail and thus All (S 0 ) ◦ f (t1 , . . . , tn ) =⇒
Fail.

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

43

If t is a constant c then ϕAll(S 0 ) (c) _ ϕc (c) • ϕAll(S 0 ) (c) −→
→ ϕc (c) and ϕc ( ) _
c • ϕc (c) −→
→ c. On the other hand we have All (S 0 ) ◦ c =⇒ c which confirms the
property.
(6) S := One(S 0 )
(a) S ⇒ T(S)
If One(S 0 ) ◦ t =⇒ u with t = f (t1 , . . . , tn ) then ∃i ∈ [1,n], S ◦ ti =⇒ ui and
u = f (t1 , . . . , ui . . . , tn ). Then, by induction, B(Γ) ∪ T(S 0 ) • ϕS 0 (ti ) −→
→ ui . The
encoding implements a leftmost behaviour for One, i.e. it supposes that ∀j <
i, S 0 ◦ tj =⇒ Fail and if we suppose that this assumption holds in our case then,
by induction, B(Γ) ∪ T(S 0 ) • ϕS 0 (tj ) −→
→ ⊥(tj ) for all j < i. When we apply the
rules corresponding to the encoding of One we obtain ϕOne(S 0 ) (f (x1 , . . . , xn )) _
ϕf1 (ϕS 0 (x1 ), x2 , . . . , xn ) • ϕOne(S 0 ) (f (t1 , . . . , tn )) −→
→ ϕf1 (ϕS 0 (t1 ), t2 , . . . , tn ). and
no other rule can be applied at the top position for this latter term until ϕS 0 (t1 ) is
reduced to a term in T (F) or to a term of the form ⊥( ). We have
ϕf1 (ϕS 0 (t1 ), . . . , tn )

B(Γ)∪T(S 0 )

−→
→

ϕf1 (⊥(t1 ), . . . , tn )

and then
ϕf1 (⊥(x1 ), x2 , . . . , xn ) _ ϕf2 (⊥(x1 ), ϕS 0 (x2 ), . . . , xn )

•ϕf1 (⊥(t1 ), . . . , tn ) −→
→ ϕf2 (⊥(t1 ), ϕS 0 (t2 ) . . . , tn ) .

Repeating the reasoning for all j < i, we eventually get
ϕf1 (ϕS 0 (t1 ), . . . , tn )

B(Γ)∪T(S 0 )∗

−→
→

ϕfi (⊥(t1 ), . . . , ⊥(ti−1 ), ui . . . , tn )

and then
ϕfi (⊥(x1 ), . . . , ⊥(xi−1 ), xi @ !⊥( ), xi+1 , . . . , xn ) _ f (x1 , . . . , xn )

→ ϕfi (t1 , . . . , ui , . . . , tn )
•ϕfi (⊥(t1 ), . . . , ⊥(ti−1 ), ui . . . , tn ) −→

as required.
If One(S 0 ) ◦ t =⇒ Fail with t = f (t1 , . . . , tn ) then ∀i ∈ [1,n], S 0 ◦ ti =⇒ Fail.
By induction, B(Γ) ∪ T(S 0 ) • ϕS 0 (ti ) −→
→ ⊥(ti ). As before, applying the rules
corresponding to the encoding of One gives ϕOne(S 0 ) (f (x1 , . . . , xn ))
ϕfn (⊥(t1 ), . . . , ⊥(tn )) and then

B(Γ)∪T(S 0 )∗

−→
→

ϕfn (⊥(x1 ), . . . , ⊥(xn )) _ ⊥(f (x1 , . . . , xn ))

•ϕfn (⊥(t1 ), . . . , ⊥(tn )) −→
→ ⊥(f (t1 , . . . , tn ))

as wished.
If t is a constant c then One(S 0 ) ◦ c =⇒ Fail, and we have ϕOne(S 0 ) (c) _ ⊥(c) •
ϕ(One(S 0 )) (c) −→
→ ⊥(c) as well.
(b) T(S) ⇒ S
If B(Γ) ∪ T(One(S 0 )) • ϕOne(S 0 ) (t) −→
→ u, then t = f (t1 , . . . , tn ), because if t is a
constant c then we would necessarily have ϕOne(S 0 ) (c) _ ⊥(c)•ϕOne(S 0 ) (c) −→
→ ⊥(c),
which contradicts the hypothesis. Because t ∈ T (F) contains no ϕ symbols, the
first reduction is necessarily
ϕOne(S 0 ) (f (x1 , . . . , xn )) _ ϕf1 (ϕS 0 (x1 ), x2 , . . . , xn )
•ϕOne(S 0 ) (f (t1 , . . . , tn )) −→
→ ϕf1 (ϕS 0 (t1 ), t2 , . . . , tn ) .

44

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

No rule can be applied at the top position until the ϕS 0 (t1 ) is reduced to a
term in T (F) or to a term of the form ⊥( ). In the former case, we have
B(Γ) ∪ T(S 0 ) • ϕS 0 (t1 ) −→
→ u1 in less steps than the original reduction, and also
B(Γ)∪T(S 0 )

ϕf1 (ϕS 0 (t1 ), . . . , tn )
−→
→
ϕf1 (u1 , . . . , tn ) which can be further reduced only
by the rule ϕf1 (x1 @ !⊥( ), x2 , . . . , xn ) _ f (x1 , . . . , xn ) to f (u1 , . . . , tn ) = u. By
induction, S 0 ◦ t1 =⇒ u1 , and consequently, One(S 0 ) ◦ t =⇒ u. In the latter
case, we necessarily have (Lemma 8.4) B(Γ) ∪ T(S 0 ) • ϕS 0 (t1 ) −→
→ ⊥(t1 ) and
B(Γ)∪T(S 0 )

ϕf1 (ϕS 0 (t1 ), . . . , tn ) −→
→ ϕf1 (⊥(t1 ), . . . , tn ) which can be further reduced only
by ϕf1 (⊥(x1 ), x2 , . . . , xn ) _ ϕf2 (⊥(x1 ), ϕS 0 (x2 ), . . . , xn ) to f (⊥(t1 ), ϕS 0 (t2 ), . . . , tn ).
Once again, no rule can be applied at the top position until the ϕS 0 (t2 ) is reduced
to a term in T (F), in which case we conclude as before, or to a term of the form
⊥( ), in which case we continue the same way and we eventually get a term of the
form ϕfi (⊥(t1 ), . . . , ⊥(ti−1 ), ui , ti+1 , . . . , tn ), then reduced by
ϕfi (⊥(x1 ), . . . , ⊥(xi−1 ), xi @ !⊥( ), xi+1 , . . . , xn ) _ f (x1 , . . . , xn )

to f (t1 , . . . , ui , ti+1 , . . . , tn ) = u. In this case we have, by induction, S 0 ◦ tj =⇒ ⊥(tj )
for all j < i and S 0 ◦ ti =⇒ ui , and thus, One(S 0 ) ◦ t =⇒ u. Note that we can
always get an ui ∈ T (F) at some point since otherwise we would eventually obtain
the term ϕfn (⊥(t1 ), . . . , ⊥(tn )) which can be reduce only to ⊥(f (t1 , . . . , tn )) which
is not a term in T (F) and thus contradicts the original hypothesis.
If B(Γ) ∪ T(One(S 0 )) • ϕOne(S 0 ) (t) −→
→ ⊥(t) and t is not a constant, because
ϕOne(S 0 ) (t) is in normal form w.r.t. B(Γ) ∪ T(S 0 ) (Lemma 8.2), the first reduction
can only be
ϕOne(S 0 ) (f (x1 , . . . , xn )) _ ϕf1 (ϕS 0 (x1 ), x2 , . . . , xn )

•ϕOne(S 0 ) (f (t1 , . . . , tn )) −→
→ ϕf1 (ϕS 0 (t1 ), t2 , . . . , tn )

and no rule can be applied at the top position until the ϕS 0 (t1 ) is reduced to a term
in T (F) or to a term of the form ⊥( ). As we have seen just before, the former case
leads to a term in T (F) which does not correspond to our hypothesis. We have
also already handled the second case but we supposed that at some point we have
B(Γ) ∪ T(S 0 ) • ϕS 0 (ti ) −→
→ ui which would lead to an eventual reduction to a term in
T (F) which, once again, does not correspond to our hypothesis. The only remaining
possibility is B(Γ) ∪ T(S 0 ) • ϕS 0 (ti ) −→
→ ⊥( ) for all i ≤ n and thus, by Lemma 8.4,
B(Γ) ∪ T(S 0 ) • ϕS 0 (ti ) −→
→ ⊥(ti ) (in less steps than the original reduction) for
all i ≤ n. In this case, we obtain ϕfn (⊥(x1 ), . . . , ⊥(xn )) _ ⊥(f (x1 , . . . , xn )) •
ϕfn (⊥(t1 ), . . . , ⊥(tn )) −→
→ ⊥(f (t1 , . . . , tn )). By induction, S 0 ◦ ti =⇒ Fail and thus
0
One(S ) ◦ f (t1 , . . . , tn ) =⇒ Fail.
If t is a constant c then ϕOne(S 0 ) (c) _ ⊥(c) • ϕOne(S 0 ) (c) −→
→ ⊥(c). We also have
0
One(S ) ◦ c =⇒ Fail.
Lemma 3.8. Given a strategy S and a context Γ such that FVarX (S) ⊆ DomX (Γ), the
TRS T(S) ∪ B(Γ) is confluent.
Proof. We consider two subsets of T(S) ∪ B(Γ): a set T1 consisting of the rewrite rules
in T(S) ∪ B(Γ) obtained by expanding the rule schemas of the form ϕl_r (x @ !l) _ ⊥(x)
and a set T2 consisting of the remaining rules in T(S) ∪ B(Γ). Keeping in mind that all ϕ
symbols are freshly generated we can easily notice that T2 is orthogonal and thus confluent.

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

45

T1 is linear but not orthogonal because of possible critical pairs between rules generated
for a rewrite rule l _ r by ϕl_r (x @ !l) _ ⊥(x); there are no critical pairs between the
rules generated for different rewrite rules because of the different ϕ head symbol in the
left-hand sides of the corresponding rules. All these critical pairs are trivially joinable
and since T1 is also obviously terminating then it is also confluent. Since T1 and T2 are
orthogonal to each other, i.e. there is no overlap between a rule from T1 and one from T2 ,
then T1 ∪ T2 = T(S) ∪ B(Γ) is confluent [32].
9. Proofs for the Meta-Encoding
Lemma 9.1. Given terms t1 . . . tn ∈ T (F), S, and Γ such that FVarX (S) ⊆ DomX (Γ),
TM (S) ∪ BM (Γ) • ϕS (_ti ^) −→
→ _t0i ^ with _t0i ^ 6= ⊥(_ti ^) for all i iff
TM (All (S)) ∪ BM (Γ)
. •ϕ0All(S) (ϕS (_t1 ^), _t2 ^ :: . . . :: _tn ^ :: nil, _t1 ^ :: nil, nil) −→
→ _t01 ^ :: . . . :: _t0n ^ :: nil
Proof. Because TM (All (S)) contains TM (S), and by definition of TM (All (S)), TM (S) ∪
BM (Γ) • ϕS 0 (_ti ^) −→
→ _t0i ^ with _t0i ^ 6= ⊥(_ti ^) for all i iff
ϕ0All(S) (ϕS (_ti ^), _ti+1 ^ :: . . . :: _tn ^ :: nil, _ti ^ :: . . . _t1 ^ :: nil, _t0i−1 ^ :: . . . :: _t01 ^ :: nil)
−→
→TM (All(S))∪BM (Γ)
ϕ0All(S) (ϕS (_ti+1 ^), _ti+2 ^

:: . . . :: _tn ^ :: nil, _ti+1 ^ :: . . . _t1 ^ :: nil, _t0i ^ :: . . . :: _t01 ^ :: nil)

for all i. As a result, we deduce
ϕ0All(S) (ϕS (_t1 ^), _t2 ^ :: . . . :: _tn ^ :: nil, _t1 ^ :: nil, nil)
−→
→TM (All(S))∪BM (Γ) ϕ0All(S) (ϕS (_tn ^), nil, _tn ^ :: . . . _t1 ^ :: nil, _t0n−1 ^ :: . . . :: _t01 ^ :: nil)
−→
→TM (All(S))∪BM (Γ) ϕ0All(S) (_t0n ^, nil, _tn ^ :: . . . _t1 ^ :: nil, _t0n−1 ^ :: . . . :: _t01 ^ :: nil)
−→
→TM (All(S))∪BM (Γ) rev(_t0n ^ :: _t0n−1 ^ :: . . . :: _t01 ^ :: nil)
−→
→TM (All(S))∪BM (Γ) _t01 ^ :: . . . :: _t0n ^ :: nil
as wished.
Lemma 9.2. Given terms t1 . . . tn ∈ T (F), S, and Γ such that FVarX (S) ⊆ DomX (Γ),
TM (S) ∪ BM (Γ) • ϕS (_tj ^) −→
→ _t0j ^ with _t0j ^ 6= ⊥(_tj ^) for all j < i0 and TM (S) ∪ BM (Γ) •
ϕS (_ti0 ^) −→
→ ⊥(_ti0 ^) iff
TM (All (S)) ∪ BM (Γ)
. •ϕ0All(S) (ϕS (_t1 ^), _t2 ^ :: . . . :: _tn ^ :: nil, _t1 ^ :: nil, nil) −→
→ ⊥list (_t1 ^ :: . . . :: _tn ^ :: nil)
Proof. As in the proof of Lemma 9.1, TM (S) ∪ BM (Γ) • ϕS (_tj ^) −→
→ _t0j ^ with _t0j ^ =
6 ⊥(_tj ^)
for all j < i0 iff
ϕ0All(S) (ϕS (_t1 ^), _t2 ^ :: . . . :: _tn ^ :: nil, _t1 ^ :: nil, nil)
−→
→TM (All(S))∪BM (Γ)
ϕ0All(S) (ϕS (_ti0 ^), _ti0 +1 ^ :: . . . :: _tn ^ :: nil, _ti0 ^ :: . . . _t1 ^ :: nil, _t0i0 −1 ^ :: . . . :: _t01 ^ :: nil)

46

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

(ME1)
(ME2)
(ME3)
(ME4)

(ME5)

(ME6)

(ME7)

TM (Identity) = { ϕIdentity (x @ appl( , )) _ x,

TM (Fail ) = { ϕFail (x @ appl( , )) _ ⊥(x),

ϕIdentity (⊥(x)) _ ⊥(x) }
ϕFail (⊥(x)) _ ⊥(x) }

TM (l _ r) = { ϕl_r (_l^) _ _r^, ϕl_r (x @ _!l^) _ ⊥(x),
ϕl_r (⊥(x)) _ ⊥(x) }

TM (S1 ; S2 ) = TM (S1 ) ∪ TM (S2 )
S
{ ϕS1 ;S2 (x @ appl( , )) _ ϕ; (ϕS2 (ϕS1 (x)), x),
ϕS1 ;S2 (⊥(x)) _ ⊥(x),
ϕ; (x @ appl( , ), ) _ x, ϕ; (⊥( ), x) _ ⊥(x) }

TM (S1 ←
+ S2 ) = TM (S1 ) ∪ TM (S2 )
S
{ ϕS1 ←
+ (ϕS1 (x)),
+S2 (x @ appl( , )) _ ϕ←
ϕS1 ←
+S2 (⊥(x)) _ ⊥(x),
ϕ←
ϕ←
+ (x @ appl( , )) _ x }
+ (⊥(x)) _ ϕS2 (x),

TM (µX . S) = TM (S)
S
{ ϕµX.S (x @ appl( , )) _ ϕS (x), ϕµX.S (⊥(x)) _ ⊥(x),
ϕX (x @ appl( , )) _ ϕS (x), ϕX (⊥(x)) _ ⊥(x) }
TM (X) = ∅

(ME8)

TM (All (S)) = TM (S) ∪ L
S
{ ϕAll(S) (⊥(x)) _ ⊥(x),
ϕAll(S) (appl(f, args)) _ propag(appl(f, ϕlist
All(S) (args))),
list
0
ϕAll(S) (h :: q) _ ϕAll(S) (ϕS (h), q, h :: nil, nil),
ϕlist
All(S) (nil) _ nil,
ϕ0All(S) (⊥( ), todo, r tried, ) _ ⊥list (rconcat(r tried, todo)),
ϕ0All(S) (x @ appl( , ), nil, , r done) _ rev(x :: r done),
ϕ0All(S) (x @ appl( , ), h :: q, r tried, r done) _
ϕ0All(S) (ϕS (h), q, h :: r tried, x :: r done) }

(ME9)

TM (One(S)) = TM (S) ∪ L
S
{ ϕOne(S) (⊥(x)) _ ⊥(x),
ϕOne(S) (appl(f, args)) _ propag(appl(f, ϕlist
One(S) (args))),
list
0
ϕOne(S) (h :: q) _ ϕOne(S) (ϕS (h), q, h :: nil),
ϕlist
One(S) (nil) _ ⊥list (nil),
ϕ0One(S) (⊥( ), nil, r tried) _ ⊥list (rev(r tried)),
ϕ0One(S) (⊥( ), h :: q, r tried) _ ϕ0One(S) (ϕS (h), q, h :: r tried),
ϕ0One(S) (x @ appl( , ), todo, :: r tried) _
rconcat(r tried, x :: todo) }

(ME10)

BM (Γ; X : S) = BM (Γ) ∪ TM (S)
S
{ ϕX (x @ appl( , )) _ ϕS (x),

(ME11)

BM ( ) = ∅

ϕX (⊥(x)) _ ⊥(x) }

Figure 6: Strategy translation for meta-encoded terms; L is defined in Figure 4.

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

47

This latter term can only reduce to
ϕ0All(S) (⊥_ti0 ^, _ti0 +1 ^ :: . . . :: _tn ^ :: nil, _ti0 ^ :: . . . _t1 ^ :: nil, _t0i0 −1 ^ :: . . . :: _t01 ^ :: nil)
which in turn reduces to ⊥list (rconcat(_ti0 ^ :: . . . _t1 ^ :: nil, _ti0 +1 ^ :: . . . :: _tn ^ :: nil)), and
then to ⊥list (_t1 ^ :: . . . :: _tn ^ :: nil), as wished.
Lemma 9.3. Given terms t1 . . . tn ∈ T (F), S, and Γ such that FVarX (S) ⊆ DomX (Γ),
TM (S) ∪ BM (Γ) • ϕS (_ti ^) −→
→ ⊥(_ti ^) for all i iff
TM (One(S)) ∪ BM (Γ)
. •ϕ0All(S) (ϕS (_t1 ^), _t2 ^ :: . . . :: _tn ^ :: nil, _t1 ^ :: nil) −→
→ ⊥list (_t1 ^ :: . . . :: _tn ^ :: nil)
Proof. Because TM (One(S)) contains TM (S), and by definition of TM (One(S)), TM (S) ∪
BM (Γ) • ϕS 0 (_ti ^) −→
→ ⊥(_ti ^) for all i iff
ϕ0One(S) (ϕS (_ti ^), _ti+1 ^ :: . . . :: _tn ^ :: nil, _ti ^ :: . . . _t1 ^ :: nil)
−→
→TM (One(S))∪BM (Γ) ϕ0One(S) (ϕS (_ti+1 ^), _ti+2 ^ :: . . . :: _tn ^ :: nil, _ti+1 ^ :: . . . _t1 ^ :: nil)
for all i. As a result, we deduce
ϕ0One(S) (ϕS (_t1 ^), _t2 ^ :: . . . :: _tn ^ :: nil, _t1 ^ :: nil)
−→
→TM (One(S))∪BM (Γ) ϕ0One(S) (ϕS (_tn ^), nil, _tn ^ :: . . . _t1 ^ :: nil)
−→
→TM (One(S))∪BM (Γ) ϕ0One(S) (⊥(_tn ^), nil, _tn ^ :: . . . _t1 ^ :: nil)
−→
→TM (One(S))∪BM (Γ) ⊥list (rev(_tn ^ :: . . . :: _t1 ^ :: nil))
−→
→TM (One(S))∪BM (Γ) ⊥list (_t1 ^ :: . . . :: _tn ^ :: nil)
as wished.
Lemma 9.4. Given terms t1 . . . tn ∈ T (F), S, and Γ such that FVarX (S) ⊆ DomX (Γ),
TM (S) ∪ BM (Γ) • ϕS (_tj ^) −→
→ ⊥(_tj ^) for all j < i0 and TM (S) ∪ BM (Γ) • ϕS (_ti0 ^) −→
→ _t0i0 ^
with _t0i0 ^ 6= ⊥(_ti0 ^) iff
TM (One(S)) ∪ BM (Γ)
. •ϕ0One(S) (ϕS (_t1 ^), _t2 ^ :: . . . :: _tn ^ :: nil, _t1 ^ :: nil) −→
→ _t1 ^ :: . . . :: _t0i0 ^ :: . . . :: _tn ^ :: nil
→ ⊥(_tj ^) for all j < i0 iff
Proof. As in the proof of Lemma 9.3, TM (S) ∪ BM (Γ) • ϕS (_tj ^) −→
ϕ0One(S) (ϕS (_t1 ^), _t2 ^ :: . . . :: _tn ^ :: nil, _t1 ^ :: nil)
−→
→TM (One(S))∪BM (Γ) ϕ0One(S) (ϕS (_ti0 ^), _ti0 +1 ^ :: . . . :: _tn ^ :: nil, _ti0 ^ :: . . . _t1 ^ :: nil)
This latter term can only reduce to
ϕ0One(S) (_t0i0 ^, _ti0 +1 ^ :: . . . :: _tn ^ :: nil, _ti0 ^ :: . . . _t1 ^ :: nil)
which in turn reduces to rconcat(_ti0 − 1^ :: . . . _t1 ^ :: nil, _t0i0 ^ :: _ti0 +1 ^ :: . . . :: _tn ^ :: nil),
and then to _t1 ^ :: . . . :: _t0i0 ^ :: . . . :: _tn ^ :: nil, as wished.

48

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

Lemma 4.3. Given a term t ∈ T (F), a strategy S and a context Γ such that FVarX (S) ⊆
DomX (Γ),
(1) if T(S) ∪ B(Γ) • ϕS (t) −→
→ u with u ∈ T (F) or u = ⊥(t), then TM (S) ∪ BM (Γ) •
ϕS (_t^) −→
→ _u^;
(2) if TM (S) ∪ BM (Γ) • ϕS (_t^) −→
→ t00 and t00 ∈ T (Fappl ), then there exists t0 such that
_t0 ^ = t00 and T(S) ∪ B(Γ) • ϕS (t) −→
→ t0 .
→ ⊥(t00 ) and t00 ∈ T (Fappl ), then t00 = _t^ and T(S) ∪
(3) if TM (S) ∪ BM (Γ) • ϕS (_t^) −→
B(Γ) • ϕS (t) −→
→ ⊥(t).
Proof. The proof is by induction on S. Most cases are straightforward, as the meta-encoding
is the same as the encoding in these cases. We only detail the ones with significant changes.
In what follows, we write RM for TM (S) ∪ BM (Γ).
(1) S = All (S 0 ).
(a) T(S) ⇒ TM (S).
Suppose t is a constant c; then T(S) ∪ B(Γ) • ϕS (c) −→
→ c. With the meta-encoding,
we have
ϕAll(S 0 ) (appl(c, nil)) −→
→RM propag(appl(c, ϕlist
S (nil)))
−→
→RM propag(appl(c, nil))
−→
→RM appl(c, nil) = _c^
The result therefore holds.
We now suppose that t = f (t1 , . . . , tn ). First, we assume t0 6= ⊥(t). By the definition
of T(S), it is possible iff the rule
ϕAll(S 0 ) (f (x1 , . . . , xn )) _ ϕf (ϕS 0 (x1 ), . . . , ϕS 0 (xn ), f (x1 , . . . , xn ))

has been applied, meaning that T(S 0 ) ∪ B(Γ) • ϕS 0 (ti ) −→
→ t0i with t0i 6= ⊥(ti ) for
0
all i. By induction, we have TM (S ) ∪ BM (Γ) • ϕS 0 (_ti ^) −→
→ _t0i ^, and _t0i ^ =
6 ⊥(_ti ^).
As a result, we have
ϕAll(S 0 ) (appl(f, _t1 ^ :: . . . :: _tn ^ :: nil))
−→
→RM propag(appl(f, ϕlist
S (_t1 ^ :: . . . :: _tn ^ :: nil)))
−→
→RM propag(appl(f, ϕ0S (ϕS 0 (_t1 ^), _t2 ^ :: . . . :: _tn ^, _t1 ^ :: nil, nil)))
By Lemma 9.1, we have
propag(appl(f, ϕ0S (ϕS 0 (_t1 ^), _t2 ^ :: . . . :: _tn ^, _t1 ^ :: nil, nil)))
−→
→RM propag(appl(f, _t01 ^ :: . . . :: _t0n ^))
−→
→RM appl(f, _t01 ^ :: . . . :: _t0n ^) = _t0 ^
Assume now t0 = ⊥(t). By the definition of T(S), it is possible iff there exists i
such that T(S 0 ) ∪ B(Γ) • ϕS 0 (ti ) −→
→ ⊥(ti ). Let i0 be the smallest of such i; then
for all j < i0 , we have T(S 0 ) ∪ B(Γ) • ϕS 0 (tj ) −→
→ t0j with t0j =
6 ⊥(tj ). By induction,
we have TM (S 0 ) ∪ BM (Γ) • ϕS 0 (_tj ^) −→
→ _t0j ^ with _t0j ^ 6= ⊥(_tj ^) for j < i0 , and

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

49

→ ⊥(_ti0 ^). Using Lemma 9.2, we have
TM (S 0 ) ∪ BM (Γ) • ϕS 0 (_ti0 ^) −→
ϕAll(S 0 ) (appl(f, _t1 ^ :: . . . :: _tn ^ :: nil))
−→
→RM propag(appl(f, ϕ0S (ϕS 0 (_t1 ^), _t2 ^ :: . . . :: _tn ^, _t1 ^ :: nil, nil)))
−→
→RM propag(appl(f, ⊥list (_t1 ^ :: . . . :: _tn ^ :: nil)))
−→
→RM ⊥(appl(f, _t1 ^ :: . . . :: _tn ^ :: nil)) = _⊥(t)^
(b) T(S) ⇒ TM (S)
If t is a constant c, then it is easy to check that t00 = _c^. Suppose t = f (t1 , . . . , tn ).
First, we assume t00 ∈ T (Fappl ). It is possible only if the rule
ϕ0All(S 0 ) (x @ appl( , ), nil, , r done) _ rev(x :: r done)

has been applied. It is possible only if rewriting ϕS 0 (_ti ^) produces a term t00i of
the form appl( , ) for all i, so that t00 = appl(_f ^, t001 :: t002 :: . . . :: t00n :: nil). Only
the rules of TM (S 0 ) may apply to ϕS 0 (_ti ^), so we have in fact TM (S 0 ) ∪ BM (Γ) •
ϕS 0 (_ti ^) −→
→ t00i with t00i ∈ T (Fappl ). By induction, there exists t0i such that
0
00
_ti ^ = ti and T(S 0 ) ∪ B(Γ) • ϕS 0 (ti ) −→
→ t0i for all i. From that, we can deduce that
T(All (S 0 )) ∪ B(Γ) • ϕAll(S 0 ) (f (t1 , . . . , tn )) −→
→ f (t01 , . . . , t0n ), as wished.
00
00
Now assume we obtain ⊥(t ) with t ∈ T (Fappl ). Then the rule
ϕ0All(S 0 ) (⊥( ), todo, r tried, ) _ ⊥list (rconcat(r tried, todo))

has been applied, meaning that there exists i such that TM (All (S 0 )) ∪ BM (Γ) •
ϕS 0 (_ti ^) −→
→ ⊥(t00i ) for some t00i . Only the rules of TM (S 0 ) may apply to ϕS 0 (_ti ^),
so we have in fact TM (S 0 ) ∪ BM (Γ) • ϕS 0 (_ti ^) −→
→ ⊥(t00i ). By induction, t00i = _ti ^
0
and T(S ) ∪ B(Γ) • ϕS 0 (ti ) −→
→ ⊥(ti ). From there, we can show that T(All (S 0 )) ∪
B(Γ) • ϕAll(S 0 ) (f (t1 , . . . , tn )) −→
→ ⊥(f (t1 , . . . , tn )), as wished.
0
(2) S = One(S ).
(a) T(S) ⇒ TM (S).
Suppose t is a constant c; then T(S) ∪ B(Γ) • ϕS (c) −→
→ ⊥(c). With the metaencoding, we have
ϕOne(S 0 ) (appl(c, nil)) −→
→RM propag(appl(c, ϕlist
S (nil)))
−→
→RM propag(appl(c, ⊥list (nil)))
−→
→RM ⊥(appl(c, nil)) = _⊥(c)^
The result therefore holds.
We now suppose that t = f (t1 , . . . , tn ). First, we assume t0 = ⊥(t). By the definition
of T(S), it is possible if T(S 0 ) ∪ B(Γ) • ϕS 0 (ti ) −→
→ ⊥(ti ) for all i. By induction, we
have TM (S 0 ) ∪ BM (Γ) • ϕS 0 (_ti ^) −→
→ _⊥(ti )^, which in turn implies
ϕOne(S 0 ) (appl(f, _t1 ^ :: . . . :: _tn ^ :: nil))
−→
→RM propag(appl(f, ϕlist
S (_t1 ^ :: . . . :: _tn ^ :: nil)))
−→
→RM propag(appl(f, ϕ0S (ϕS 0 (_t1 ^), _t2 ^ :: . . . :: _tn ^, _t1 ^ :: nil)))

50

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

By Lemma 9.3, we have
propag(appl(f, ϕ0S (ϕS 0 (_t1 ^), _t2 ^ :: . . . :: _tn ^, _t1 ^ :: nil)))
−→
→RM propag(appl(f, ⊥list (_t1 ^ :: . . . :: _tn ^)))
−→
→RM ⊥(appl(f, _t1 ^ :: . . . :: _tn ^)) = _⊥(t)^
Assume now t0 6= ⊥(t). By the definition of T(S), it is possible if there exists i0 such
that T(S 0 ) ∪ B(Γ) • ϕS 0 (ti ) −→
→ t0i0 with t0i0 6= ⊥(ti0 ), and for all j < i0 , we have
0
T(S ) ∪ B(Γ) • ϕS 0 (tj ) −→
→ ⊥(tj ). By induction, it means that TM (S 0 ) ∪ BM (Γ) •
ϕS 0 (_tj ^) −→
→ ⊥(_tj ^) and TM (S 0 ) ∪ BM (Γ) • ϕS 0 (_ti0 ^) −→
→ t0i0 with _t0i0 ^ =
6 ⊥(_ti0 ^).
Using Lemma 9.4, we have
ϕOne(S 0 ) (appl(f, _t1 ^ :: . . . :: _tn ^ :: nil))
−→
→RM propag(appl(f, ϕ0S (ϕS 0 (_t1 ^), _t2 ^ :: . . . :: _tn ^, _t1 ^ :: nil)))
−→
→RM propag(appl(f, _t1 ^ :: . . . :: _t0i0 ^ :: . . . :: _tn ^ :: nil))
−→
→RM appl(f, _t1 ^ :: . . . :: _t0i0 ^ :: . . . :: _tn ^ :: nil) = _t0 ^
(b) T(S) ⇒ TM (S)
If t is a constant c, then it is easy to check that the meta-encoding fails with ⊥(_c^).
Suppose t = f (t1 , . . . , tn ). First, we assume we obtain ⊥(t00 ) with t00 ∈ T (Fappl ).
Then the rule
ϕ0One(S 0 ) (⊥( ), nil, r tried) _ ⊥list (rev(r tried))

has been applied, meaning that for all i, we have TM (One(S 0 ))∪BM (Γ)•ϕS 0 (_ti ^) −→
→ ⊥(t00i ) for some t00i . Only the rules of TM (S 0 ) may apply to ϕS 0 (_ti ^), so
we have in fact TM (S 0 ) ∪ BM (Γ) • ϕS 0 (_ti ^) −→
→ ⊥(t00i ) for all i. By induction,
00
0
ti = _ti ^ and T(S ) ∪ B(Γ) • ϕS 0 (ti ) −→
→ ⊥(ti ). From there, we can show that
T(One(S 0 )) ∪ B(Γ) • ϕOne(S 0 ) (f (t1 , . . . , tn )) −→
→ ⊥(f (t1 , . . . , tn )), as wished.
00
Now we assume t ∈ T (Fappl ). It is possible only if the rule
ϕ0One(S 0 ) (x @ appl( , ), todo, :: r tried) _ rconcat(r tried, x :: todo)

has been applied. It is possible only if there exists i such that ϕS 0 (_ti ^) produces a
term t00i of the form appl( , ), and for all j < i, we obtain ⊥(t00j ). As a result, we
have t00 = appl(_f ^, _t1 ^ :: _t2 ^ :: . . . :: t00i :: . . . :: _tn ^ :: nil). Only the rules of TM (S 0 )
may apply to ϕS 0 (_ti ^), so we have in fact TM (S 0 ) ∪ BM (Γ) • ϕS 0 (_ti ^) −→
→ t00i
00
0
00
with ti ∈ T (Fappl ) and TM (S ) ∪ BM (Γ) • ϕS 0 (_tj ^) −→
→ ⊥(tj ) for all j < i. By
0
0
00
0
induction, there exists ti such that _ti ^ = ti and T(S ) ∪ B(Γ) • ϕS 0 (ti ) −→
→ t0i , and
00
0
also tj = ⊥(_tj ^), T(S ) ∪ B(Γ) • ϕS 0 (tj ) −→
→ ⊥(tj ) for all j < i. From that, we can
deduce that T(One(S 0 )) ∪ B(Γ) • ϕOne(S 0 ) (f (t1 , . . . , tn )) −→
→ f (t1 , . . . , t0i , . . . , t0n ), as
wished.

10. Properties of the many-sorted encoding
Lemma 5.6 (Subject reduction). Consider a many-sorted signature (S, F), a strategy S, a
context Γ such that FVarX (S) ⊆ DomX (Γ), and the term rewriting system R=TS (S)∪BS (Γ)
built over the extended signature (S, F). Given a term t ∈ Ts (F) for some sort s ∈ S, if
t −→R t0 then t0 ∈ Ts (F).

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

(SE1)
(SE2)

TS (Identity) =
TS (Fail ) =

S
s∈S
S
s∈S

(SE3)

s

{ ϕIdentity (x @ ! ⊥( )) _ x,
s

{ ϕFail (x @ ! ⊥( )) _ ⊥(x),

TS (l _ r) = { ϕl_r (l) _ r }
S
s
{ ϕl_r (x @ ! l) _ ⊥(x),
s∈S

(SE4)

ϕS1 ;S2 (⊥(xs )) _ ⊥(xs ),
s
ϕ; (x @ ! ⊥( ), y s ) _ x, ϕ; (⊥(y s ), xs ) _ ⊥(xs ) }

TS (S1 ←
+ S2 ) = TS (S1 ) ∪ TS (S2 )
S
s
{ ϕS1 ←
+ (ϕS1 (x)),
+S2 (x @ ! ⊥( )) _ ϕ←
s
s
ϕ←
+ (⊥(x )) _ ϕS2 (x ),

TS (X) = ∅

TS (One(S)) =
S
{
s∈S
S
{
f ∈F +
S
S
{
S

S

f ∈F + 1≤i<n

S
f ∈F +

ϕX (⊥(xs )) _ ⊥(xs ) }

TS (S)
S
ϕOne(S) (⊥(xs )) _ ⊥(xs ) }
{ϕOne(S) (c) _ ⊥(c) }
c∈F 0

ϕOne(S) (f (xs11 , . . . , xsnn )) _ ϕf1 (ϕS (xs11 ), xs22 , . . . , xsnn ) }
s

si

s

i+1
i−1
, . . . , xsnn ) _
ϕfi (⊥(xs11 ), . . . , ⊥(xi−1
), xi @ ! ⊥( ), xi+1
f (xs11 , . . . , xsnn ) }
si+1
{ ϕfi (⊥(xs11 ), . . . , ⊥(xsi i ), xi+1
, . . . , xsnn ) _
si+1
si+2
ϕfi+1 (⊥(xs11 ), . . . , ⊥(xsi i ), ϕS (xi+1
), xi+2
, . . . , xsnn ) }
{ ϕfn (⊥(xs11 ), . . . , ⊥(xsnn )) _ ⊥(f (xs11 , . . . , xsnn )) }

BS (Γ; X : S) = BS (Γ) ∪ TS (S)
S
s
{ ϕX (x @ ! ⊥( )) _ ϕS (x),
s∈S

(SE11)

ϕµX.S (⊥(xs )) _ ⊥(xs ),

TS (All (S)) = TS (S)
S
S
{ ϕAll(S) (⊥(xs )) _ ⊥(xs ) }
{ϕAll(S) (c) _ c }
0
s∈S
c∈F
S
{ ϕAll(S) (f (xs11 , . . . , xsnn )) _
f ∈F +
ϕf (ϕS (xs11 ), . . . , ϕS (xsnn ), f (xs11 , . . . , xsnn )),
s1
sn
ϕf (x1 @ ! ⊥( ), . . . , xn @ ! ⊥( ), y s ) _ f (x1 , . . . , xn ),
ϕf (⊥(xs11 ), xs22 , . . . , xsnn , xs ) _ ⊥(xs ),
..
.
ϕf (xs11 , xs22 , . . . , ⊥(xsnn ), xs ) _ ⊥(xs ) }

f ∈F + 1≤i≤n

(SE10)

s

ϕX (x @ ! ⊥( )) _ ϕS (x),

(SE7)

(SE9)

s

s
s
ϕS1 ←
+S2 (⊥(x )) _ ⊥(x ),

ϕ←
+ (x @ ! ⊥( )) _ x }

TS (µX . S) = TS (S)
S
s
{ ϕµX.S (x @ ! ⊥( )) _ ϕS (x),
s∈S

(SE8)

ϕFail (⊥(xs )) _ ⊥(xs ) }

ϕl_r (⊥(xs )) _ ⊥(xs ) }

s∈S

(SE6)

ϕIdentity (⊥(xs )) _ ⊥(xs ) }

TS (S1 ; S2 ) = TS (S1 ) ∪ TS (S2 )
S
s
{ ϕS1 ;S2 (x @ ! ⊥( )) _ ϕ; (ϕS2 (ϕS1 (x)), x),
s∈S

(SE5)

51

BS ( ) = ∅

ϕX (⊥(xs )) _ ⊥(xs ) }

Figure 7: Sorted strategy translation. We consider that f : s1 × . . . ×sn 7→ s ∈ Fs+ . The
original signature is enriched with ⊥, ϕIdentity , ϕFail , ϕl_r , ϕS1 ;S2 , ϕ; , ϕS1 ←
+ , ϕµX.S ,
+S2 , ϕ←
ϕX , ϕAll(S) , ϕOne(S) : s 7→ s, and ϕf : s1 × . . . ×sn ×s 7→ s, and ϕfi+1 : s1 × . . . ×sn 7→ s.

52

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

Proof. By induction on the structure of the strategy S (and the context Γ) and by cases
on the rewrite rule applied in the reduction. We have that t −→R t0 iff there exist a
rule l _ r ∈ R, ω ∈ Pos(t), and a well-sorted substitution σ such that t|ω = σ(l) and
t0 = t [σ(r)]ω ; we write t −→l_r t0 to explicit the applied rule. We first show by cases on the
rewrite rule applied in the reduction that the property holds for ω = ε. It is then easy to
conclude by observing that for any term t [u]ω : s with u : s0 we also have t [u0 ]ω : s whenever
u0 : s0 .
Base case: the applied rewrite rule is one the rules in TS (Identity), TS (Identity) or TS (l _ r).
(1) t −→ρ t0 with ρ ∈ TS (Identity)
s
(a) ρ corresponds to a rule schema of the form ϕIdentity (x @ ! ⊥( )) _ x. In this case
s
t = ϕIdentity (u) with u : s and there exist v ∈ ! ⊥( ) and σ s.t. σ(v) = u. Then
t0 = u and thus t0 : s.
(b) ρ is a rule of the form ϕIdentity (⊥(xs )) _ ⊥(xs ). In this case t = ϕIdentity (⊥(u))
with u : s and there exists σ s.t. σ(xs ) = u. We have thus t0 = ⊥(u) and t0 : s.
(2) t −→ρ t0 with ρ ∈ TS (Fail )
s
(a) ρ corresponds to a rule schema of the form ϕFail (x @ ! ⊥( )) _ ⊥(x). In this
s
case t = ϕFail (u) with u : s and there exist v ∈ ! ⊥( ) and σ s.t. σ(v) = u. Then
t0 = ⊥(u) and t0 : s.
(b) ρ is a rule of the form ϕFail (⊥(xs )) _ ⊥(xs ). Similar to case 1b.
(3) t −→ρ t0 with ρ ∈ TS (l _ r)
(a) ρ is a rule of the form ϕl_r (l) _ r. In this case t = ϕl_r (u) and u : s. Then l, r : s
and there exists σ s.t. σ(l) = u. Then t0 = σ(r) and t0 : s.
s
(b) ρ corresponds to a rule schema of the form ϕl_r (x @ ! l) _ ⊥(x). In this case
s
t = ϕl_r (u) with u : s and there exist v ∈ ! l, v : s and σ s.t. σ(v) = u. Then
t0 = ⊥(u) and thus t0 : s.
(c) ρ is a rule of the form ϕl_r (⊥(xs )) _ ⊥(xs ). Similar to case 1b.
Induction case: the applied rewrite rule is one the rules in the encoding of a strategy other
than Identity, Fail or rewrite rule.
(4) t −→ρ t0 with ρ ∈ TS (S1 ; S2 )
s
(a) ρ corresponds to a rule schema of the form ϕS1 ;S2 (x @ ! ⊥( )) _ ϕ; (ϕS2 (ϕS1 (x)), x).
s
In this case t = ϕS1 ;S2 (u) with u : s and there exist v ∈ ! ⊥( ) and σ s.t. σ(v) = u.
Then t0 = ϕ; (ϕS2 (ϕS1 (u)), u) and since ϕS2 , ϕS1 : s 7→ s and ϕ; : s, s 7→ s we have
t0 : s.
s
(b) ρ corresponds to a rule schema of the form ϕ; (x @ ! ⊥( ), y s ) _ x. In this case
t = ϕ; (u0 , u00 ) with u0 , u00 : s. Then t0 = u0 and thus t0 : s using the same reasoning
as in case 1a.
(c) ρ is a rule of the form ϕS1 ;S2 (⊥(xs )) _ ⊥(xs ). Similar to case 1b.
(d) ρ is a rule of the form or ϕ; (⊥(y s ), xs ) _ ⊥(xs ). In this case t = ϕ; (⊥(u0 ), u00 ) with
u0 , u00 : s. Then t0 = ⊥(u00 ) and thus t0 : s using the same reasoning as in case 1a.
(e) ρ is one of the rules in TS (S1 ) ∪ TS (S2 ). Apply th induction hypothesis.
+ S2 ). Each of the possible cases is similar to one of the cases
(5) t −→ρ t0 with ρ ∈ TS (S1 ←
for 4.
(6) t −→ρ t0 with ρ ∈ TS (µX . S). Each of the possible cases is similar to one of the cases
for 4.

(META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS

53

(7) t −→ρ t0 with ρ ∈ TS (All (S))
(a) ρ is a rule of the form ϕAll(S) (⊥(xs )) _ ⊥(xs ). Similar to case 1b.
(b) ρ is a rule of the form ϕAll(S) (c) _ c. In this case t = ϕAll(S) (c) with c : s and t0 = c
and t0 : s.
(c) ρ has the form ϕAll(S) (f (xs11 , . . . , xsnn )) _ ϕf (ϕS (xs11 ), . . . , ϕS (xsnn ), f (xs11 , . . . , xsnn )).
In this case t = ϕAll(S) (f (u1 , . . . , un )) with u1 : s1 , . . . , un : sn if f : s1 × . . . ×sn 7→ s.
Since ϕS : s0 7→ s0 for any s0 ∈ S and ϕf : s1 × . . . ×sn ×s 7→ s we have t0 : s.
s1
sn
(d) ρ corresponds to a rule schema of the form ϕf (x1 @ ! ⊥( ), . . . , xn @ ! ⊥( ), y s ) _
f (x1 , . . . , xn ). In this case t = ϕf (u1 , . . . , un , u) with u1 : s1 , . . . , un : sn , u : s if
si
f : s1 × . . . ×sn 7→ s and for all i = 1 . . . n there exist vi ∈ ! ⊥( ) and σ s.t. σ(vi ) = ui .
Then t0 = f (u1 , . . . , un ) and thus t0 : s.
(e) ρ is a rule of the form or ϕf (xs11 , . . . , ⊥(xsi i ), . . . , xsnn , xs ) _ ⊥(xs ). In this case
t = ϕf (u1 , . . . , ⊥(ui ), . . . , un , u) with u1 : s1 , . . . , un : sn , u : s if f : s1 × . . . ×sn 7→ s.
Then t0 = ⊥(u) and thus t0 : s.
(f) ρ is one of the rules in TS (S). Apply th induction hypothesis.
(8) t −→ρ t0 with ρ ∈ TS (One(S)). Each of the possible cases is similar to one of the cases
for 7.
(9) t −→ρ t0 with ρ ∈ BS (Γ; X : S). Each of the possible cases is similar to one of the cases
for 6, for example.
Lemma 5.7 (Equivalent reductions). Consider a many-sorted signature (S, F), a strategy S,
a context Γ such that FVarX (S) ⊆ DomX (Γ), and the term rewriting systems R=T(S)∪B(Γ)
and RS =TS (S) ∪ BS (Γ) built over the extended signature (S, F). Given a term t ∈ TS (F),
t −→RS t0 iff t −→R t0 .
Proof. Every rewrite rule in RS is also included in R and thus, if t −→RS t0 then t −→R t0 .
For the other direction we proceed by induction on the structure of the strategy S (and
the context Γ) and by cases on the rewrite rule applied in the reduction. For simplicity,
we consider reduction at the top position but as shown in the proof of Lemma 5.6 this
generalises immediately for any application position. We consider in what follows that
t ∈ Ts (F) for some s ∈ S.
Base case: the applied rewrite rule is one the rules in T(Identity), T(Identity) or T(l _ r).
(1) t −→ρ t0 with ρ ∈ T(Identity)
(a) ρ is one of the rules corresponding to the rule schema ϕIdentity (x @ !⊥( )) _ x and
thus of the form ϕIdentity (f (x1 , . . . , xn )) _ f (x1 , . . . , xn ) with f ∈ F. In this case
t = ϕIdentity (f (t1 , . . . , tn )) and thus f ∈ Fs . This rule also corresponds to the rule
s
schema ϕIdentity (x @ ! ⊥( )) _ x from the sorted translation and thus t −→RS t0 .
(b) ρ is the rule ϕIdentity (⊥(x)) _ ⊥(x). The rule ϕIdentity (⊥(xs )) _ ⊥(xs ) from the
sorted translation applies also to t which has necessarily the form ϕIdentity (⊥(u))
with u : s and thus t −→RS t0 .
(2) t −→ρ t0 with ρ ∈ T(Fail ). We proceed similarly as for the case 1.
(3) t −→ρ t0 with ρ ∈ T(l _ r)
(a) ρ is one of the rules corresponding to the rule schema ϕl_r (x @ !l) _ ⊥(x) and
thus of the form ϕl_r (f (u1 , . . . , un )) _ ⊥(f (u1 , . . . , un )) with f ∈ F. In this case
t = ϕl_r (f (t1 , . . . , tn )) and thus f ∈ Fs . Consequently, the rule ρ corresponds

54

H. CIRSTEA, S. LENGLET, AND P.-E. MOREAU

s

also to the rule schema ϕl_r (x @ ! l) _ ⊥(x) from the sorted translation and thus
t −→RS t0 .
(b) ρ is the rule ϕl_r (l) _ r. Since the rule is also present in the sorted translation
then t −→RS t0 .
(c) ρ is the rule ϕl_r (⊥(x)) _ ⊥(x). Similar to the case 1b.
Induction case: the applied rewrite rule is one the rules in the encoding of a strategy other
than Identity, Fail or rewrite rule. When the applied rule is not in T(All (S)) or T(One(S))
we can conclude either by induction or similarly to one of the above cases.
(4) t −→ρ t0 with ρ ∈ T(All (S)). Once again we can proceed either by induction or similarly
to one of the above cases except for one case:
(a) ρ corresponds to a rule schema ϕf (x1 @ !⊥( ), . . . , xn @ !⊥( ), ) _ f (x1 , . . . , xn )
and thus is a rewrite rule of the form ϕf (f1 (x11 , . . . , x1m ), . . . , fn (xn1 , . . . , xnp ), x) _
f (f1 (x11 , . . . , x1m ), . . . , fn (xn1 , . . . , xnp )) with f1 , . . . , fn , f ∈ F. Since the rewrite rule
can be applied to the well-sorted term t then f1 ∈ Fs1 , . . . , fn ∈ Fsn , f ∈ Fs
and consequently, this rewrite rule also corresponds to the rule schema ϕf (x1 @
!s1⊥( ), . . . , xn @ !sn⊥( ), ys ) _ f (x1 , . . . , xn ) from the sorted translation. Thus
t −→RS t0 .
(5) t −→ρ t0 with ρ ∈ TS (One(S)). Similar to the cases for 4.
Theorem 5.8 (Simulation). Given a a many-sorted signature (S, F), a strategy S, two
terms t, t0 ∈ TS (F), and a context Γ such that FVarX (S) ⊆ DomX (Γ),
(1) Γ ` S ◦ t =⇒ t0 iff TS (S) ∪ BS (Γ) • ϕS (t) −→
→ t0 ,
(2) Γ ` S ◦ t =⇒ Fail iff TS (S) ∪ BS (Γ) • ϕS (t) −→
→ ⊥(t)
Proof. Follows immediately from Lemma 5.7 and Theorem 3.5.

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view
a copy of this license, visit http://creativecommons.org/licenses/by-nd/4.0/ or send a
letter to Creative Commons, PO Box 1866, Mountain View, CA 9404, USA

