Under consideration for publication in Theory and Practice of Logic Programming

1

arXiv:1209.2617v2 [cs.PL] 10 Oct 2012

Rewriting and narrowing for constructor
systems with call-time choice semantics∗
FRANCISCO J. LÓPEZ-FRAGUAS, ENRIQUE MARTIN-MARTIN,
JUAN RODRÍGUEZ-HORTALÁ and JAIME SÁNCHEZ-HERNÁNDEZ
Departamento de Sistemas Informáticos y Computación
Universidad Complutense de Madrid, Spain
(e-mail: fraguas@sip.ucm.es, emartinm@fdi.ucm.es,
juan.rodriguez.hortala@gmail.com, jaime@sip.ucm.es)
submitted 30 November 2010; revised 14 November 2011; accepted 4 July 2012

Abstract
Non-confluent and non-terminating constructor-based term rewriting systems are useful
for the purpose of specification and programming. In particular, existing functional logic
languages use such kind of rewrite systems to define possibly non-strict non-deterministic
functions. The semantics adopted for non-determinism is call-time choice, whose combination with non-strictness is a non trivial issue, addressed years ago from a semantic
point of view with the Constructor-based Rewriting Logic (CRWL), a well-known semantic framework commonly accepted as suitable semantic basis of modern functional logic
languages. A drawback of CRWL is that it does not come with a proper notion of one-step
reduction, which would be very useful to understand and reason about how computations
proceed. In this paper we develop thoroughly the theory for the first order version of letrewriting, a simple reduction notion close to that of classical term rewriting, but extended
with a let-binding construction to adequately express the combination of call-time choice
with non-strict semantics. Let-rewriting can be seen as a particular textual presentation
of term graph rewriting. We investigate the properties of let-rewriting, most remarkably
their equivalence with respect to a conservative extension of the CRWL-semantics coping with let-bindings, and we show by some case studies that having two interchangeable
formal views (reduction/semantics) of the same language is a powerful reasoning tool.
After that, we provide a notion of let-narrowing which is adequate for call-time choice
as proved by soundness and completeness results of let-narrowing with respect to letrewriting. Moreover, we relate those let-rewriting and let-narrowing relations (and hence
CRWL) with ordinary term rewriting and narrowing, providing in particular soundness
and completeness of let-rewriting with respect to term rewriting for a class of programs
which are deterministic in a semantic sense.
To appear in Theory and Practice of Logic Programming (TPLP).
KEYWORDS: term rewriting systems, constructor-based rewriting logic, narrowing, nondeterminism, call-time choice semantics, sharing, local bindings

∗ This work has been partially supported by the Spanish projects FAST-STAMP (TIN2008-06622C03-01/TIN), PROMETIDOS-CM (S2009TIC-1465) and GPD-UCM (UCM-BSCH-GR58/ 08910502).

2

López-Fraguas et al.
coin → 0
coin → 1

repeat(X) → X : repeat(X)
heads(X : Y : Ys) → (X, Y )

Fig. 1. A non-terminating and non-confluent program
1 Introduction
Term rewriting systems (TRS, (Baader and Nipkow 1998)) are a well-known and
useful formalism from the point of view of specification and programming. The
theory of TRS underlies many of the proposals made in the last decades for socalled functional logic programming, attempting to integrate into a single language
the main features of both functional and logic programming —see (DeGroot and
Lindstrom 1986; Hanus 1994; Hanus 2007) for surveys corresponding to different
historical stages of the development of functional logic languages—. Typically, functional logic programs are modeled by some kind of TRS to define functions, and
logic programming capabilities are achieved by using some kind of narrowing as
operational mechanism. Narrowing, a notion coming from the field of automated
theorem proving, generalizes rewriting by using unification instead of matching in
reduction steps. Up to 14 different variants of narrowing were identified in (Hanus
1994) as being used in different proposals for the integration of functional and logic
programming.
Modern functional logic languages like Curry (Hanus et al. 1995; Hanus (ed.)
2006) or Toy (López-Fraguas and Sánchez-Hernández 1999; Caballero and Sánchez
2006) consider that programs are constructor-based term rewrite systems, possibly non-terminating and non-confluent, thus defining possibly non-strict nondeterministic functions. For instance, in the program of Figure 1, non-confluence
comes from the two rules of coin and non-termination is due to the rule for repeat.
For non-determinism, those systems adopt call-time choice semantics (Hussmann 1993; González-Moreno et al. 1999), also called sometimes singular semantics
(Søndergaard and Sestoft 1992). Loosely speaking, call-time choice means to pick
a value for each argument of a function application before applying it. Call-time
choice is easier to understand and implement in combination with strict semantics
and eager evaluation in terminating systems as in (Hussmann 1993), but can be
made also compatible —via partial values and sharing— with non-strictness and
laziness in the presence of non-termination.
In the example of Figure 1 the expression heads(repeat(coin)) can take, under
call-time choice, the values (0, 0) and (1, 1), but not (0, 1) or (1, 0). The example
illustrates also a key point here: ordinary term rewriting (called run-time choice in
(Hussmann 1993)) is an unsound procedure for call-time choice semantics, since a
possible term rewriting derivation is:
heads(repeat(coin)) → heads(coin : repeat(coin)) →
heads(0 : repeat(coin)) → heads(0 : coin : repeat(coin)) →
heads(0 : 1 : repeat(coin)) → (0, 1)
In operational terms, call-time choice requires to share the value of all copies of
a given subexpression created during reduction (all the occurrences of coin, in

Theory and Practice of Logic Programming

3

the reduction above). In contrast, with ordinary term rewriting all copies evolve
independently.
It is commonly accepted (see e.g. (Hanus 2007)) that call-time choice semantics
combined with non-strict semantics is adequately formally expressed by the CRWL
framework1 (González-Moreno et al. 1996; González-Moreno et al. 1999), whose
main component is a proof calculus that determines the semantics of programs
and expressions. The flexibility and usefulness of CRWL is evidenced by the large
set of extensions that have been devised for it, to cope with relevant aspects of
declarative programming: higher order functions, types, constraints, constructive
failure, . . . ; see (Rodrı́guez-Artalejo 2001) for a survey on the CRWL approach.
However, a drawback of the CRWL-framework is its lack of a proper one-step reduction mechanism that could play a role similar to term rewriting with respect
to equational logic. Certainly CRWL includes operational procedures in the form
of goal-solving calculi (González-Moreno et al. 1999; Vado-Vı́rseda 2003) to solve
so-called joinability conditions, but they are too complex to be seen as a basic way
to explain or understand how a reduction can proceed in the presence of non-strict
non-deterministic functions with call-time choice semantics.
On the other hand, other works have been more influential on the operational
side of the field, specially those based on the notion of needed narrowing (Antoy
et al. 1994; Antoy et al. 2000), a variant of narrowing that organizes the evaluation
of arguments in function calls in an adequate way (optimal, for some classes of programs). Needed narrowing became the ‘official’ operational procedure of functional
logic languages, and has also been subject of several variations and improvements
(see (Hanus 2007; Escobar et al. 2005)).
These two coexisting branches of research (one based on CRWL, and the other
based on classical term rewriting, mostly via needed narrowing) have remained
disconnected for many years from the technical point of view, despite the fact that
they both refer to what intuitively is the same programming language paradigm.
A major problem to establish the connection was that the theory underlying
needed narrowing is classical term rewriting, which, as we saw above, is not valid
for non-determinism with call-time choice semantics. This was not a flaw in the
conception of needed narrowing, as it emerged in a time when non-deterministic
functions had not yet started to play a distinctive role in the functional logic programming paradigm. The problem is overcome in practice by adding a sharing
mechanism to the implementation of narrowing, using for instance standard Prolog
programming techniques (Cheong and Fribourg 1993; Loogen et al. 1993; Antoy
and Hanus 2000). But this is merely an implementation patch that cannot be used
as a precise and sound technical basis for the application of results and techniques
from the semantic side to the operational side and vice versa. Other works, specially
(Echahed and Janodet 1998; Albert et al. 2005) have addressed in a more formal
way the issue of sharing in functional logic programming, but they are not good

1

CRWL stands for Constructor Based ReWriting Logic.

4

López-Fraguas et al.

starting points to establish a relationship with the CRWL world (see ‘Related work’
below).
In (López-Fraguas et al. 2007b) we aimed at establishing a bridge, by looking for
a new variant of term rewriting tailored to call-time choice as realized by CRWL,
trying to fulfil the following requirements:
• it should be based on a notion of rewrite step useful to follow how a computation proceeds step by step.
• it should be simple enough to be easily understandable for non-expert potential users. (e.g., students or novice programmers) of functional logic languages
adopting call-time choice.
• it should be provably equivalent to CRWL, as a well-established technical
formulation of call-time choice.
• it should serve as a basis of subsequent notion of narrowing and evaluation
strategies.
That was realized in (López-Fraguas et al. 2007b) by means of let-rewriting,
a simple modification of term rewriting using local bindings in the form of letexpressions to express sharing. Let-rewriting will be fully presented in Section 4,
but its main intuitions can be summarized as follows:
(i) do not rewrite a function call if any of its arguments is evaluable (i.e., still
contains other function calls), even if there is a matching rule;
(ii) instead, extract those evaluable arguments to outer let-bindings of the form
let X = e in e0 ;
(iii) if after some reduction steps the definiens e of the let-binding becomes a
constructor term t —a value— then the binding X/t can be made effective in
the body e0 . In this way, the values obtained for e in the reduction are shared,
and therefore call-time choice is respected.
Consider, for instance, the program example of Figure 1 and the expression
heads(repeat(coin))
for which we previously performed an ordinary term rewriting reduction ending in
(0, 1). Now we are going to apply liberally the previous intuitive hints as a first
illustration of let-rewriting. Note first that no rewrite step using a program rule
can be done with the whole expression heads(repeat(coin)), since in this case there
is no matching rule. But we can extract the argument repeat(coin) to a let-binding,
obtaining:
let X = repeat(coin) in heads(X)
Now we cannot rewrite repeat(coin), even though the program rule for repeat matches
it, because coin is evaluable. Again, we can create a let-binding for coin, that will
be used to share the value selected for coin, if at any later step in the reduction
coin is indeed reduced:
let Y = coin in let X = repeat(Y ) in heads(X)

Theory and Practice of Logic Programming

5

At this point there is no problem with rewriting repeat(Y), which gives:
let Y = coin in let X = Y : repeat(Y ) in heads(X)
Rewriting repeat(Y) again, we have:
let Y = coin in let X = Y : Y : repeat(Y ) in heads(X)
Reducing repeat(Y) indefinitely leads to non-termination, but, at the same time, its
presence inhibits the application of the binding for X. What we can do is creating
a new let-binding for the remaining repeat(Y), which results in:
let Y = coin in let Z = repeat(Y ) in let X = Y : Y : Z in heads(X)
Now, the binding for X can be performed, obtaining:
let Y = coin in let Z = repeat(Y ) in heads(Y : Y : Z)
At this point, we can use the rule for heads to evaluate heads(Y : Y : Z), because
nothing evaluable remains in its argument Y : Y : Z, arriving at:
let Y = coin in let Z = repeat(Y ) in (Y, Y )
We proceed now by reducing coin, for instance, to 0 (reducing it to 1 is also possible):
let Y = 0 in let Z = repeat(Y ) in (Y, Y )
Performing the binding for Y leads to:
let Z = repeat(0) in (0, 0)
Since Z does not occur in (0, 0), its binding is junk that could be deleted (there will
be a rule for that in the definition of let-rewriting), and the reduction is finished
yielding the value
(0, 0)
It is apparent that (1, 1) is another possible result, but not (0, 1) nor (1, 0), a
behavior coherent with call-time choice.
In this example we have tried to proceed in a more or less natural ‘lazy’ way.
However, the previous intuitive precepts —and its complete and precise realization
in Section 4— do not assume any particular strategy for organizing reductions,
but only determine which are the ‘legal movements’ in call-time choice respectful
reductions. Strategies have been left aside in the paper, not only for simplicity, but
also to keep them independent of the basic rules for term rewriting with sharing
(see however Section 6.2).
Let-rewriting was later on extended to cope with narrowing (López-Fraguas et al.
2009c) and higher order features (López-Fraguas et al. 2008).
This paper is a substantially revised and completed presentation of the theory of
first order let-rewriting and let-narrowing proposed in (López-Fraguas et al. 2007b;
López-Fraguas et al. 2009c); some contents have been also taken from (LópezFraguas et al. 2008). Here, we unify technically those papers and develop a deeper
investigation of the properties of let-rewriting and related semantics issues.

6

López-Fraguas et al.

Related work Our let-rewriting and let-narrowing relations are not the only
nor the first formal operational procedures tuned up to accomplish with the calltime choice semantics of functional logic languages. We have already mentioned the
goal-solving calculi associated to the CRWL-framework and its variants (GonzálezMoreno et al. 1999; González-Moreno et al. 1997; Vado-Vı́rseda 2003).
A natural option to express different levels of sharing in rewriting is given by the
theory of term graph rewriting (Barendregt et al. 1987; Plump 2001). In (Echahed and Janodet 1997; Echahed and Janodet 1998), the theory of needed rewriting
and narrowing was extended to the framework of so-called admissible graph rewriting systems, aiming at formally modeling the operational behavior of functional
logic programs. Originally, those works considered orthogonal systems, and extra
variables were not allowed. These restrictions were dropped in (Antoy et al. 2007)
(however, a formal treatment of the extension is missing).
As a matter of fact, our let-rewriting relation can be understood as a particular
textual adaptation and presentation of term graph rewriting in which a shared
node is made explicit in the syntax by giving it a name in a let-binding. The
achievements of Echahed’s works are somehow incomparable to ours, even if both
are attempts to formalize sharing in constructor based systems. They focus and
succeed on adapting known optimal strategies to the graph rewriting and narrowing
setting; they also take profit of the fine-grained descriptions permitted by graphs
to manage aspects of data structures like cycles or pointers. However, they do not
try to establish a technical relationship with other formulations of call-time choice.
In contrast, proving equivalence of our operational formalisms wrt. the CRWL
semantic framework has been a main motivation of our work, but we do not deal
with the issue of strategies, except for a short informal discussion at the end of the
paper.
It is our thought that proving equivalence with respect to CRWL of term graph
rewriting as given in (Echahed and Janodet 1997) would have been a task much
harder than the route we follow here. We see a reason for it. The basic pieces that
term rewriting and CRWL work with are purely syntactic: terms, substitutions,
etc. Graph rewriting recast these notions in terms of graphs, homomorphisms, etc.
In contrast, let-rewriting and let-narrowing keep the same set of basic pieces of
term rewriting and CRWL. In this way, the formalisms are relatively close and
moving from one to another becomes technically more natural and comfortable.
This applies also to some further developments of our setting that we have made
so far, like the extension to higher order features given in (López-Fraguas et al.
2008), the combination of semantics proposed in (López-Fraguas et al. 2009a), or
the application of let-rewriting as underlying formal notion of reduction for type
systems in functional logic languages (López-Fraguas et al. 2010b; López-Fraguas
et al. 2010a).
Another proposal that can be seen as reformulation of graph rewriting was given
in (Albert et al. 2005), inspired in Launchbury’s natural semantics (Launchbury
1993) for lazy evaluation in functional programming. It presents two operational
(natural and small-step) semantics for functional logic programs supporting sharing

Theory and Practice of Logic Programming

7

and residuation (a specific feature of Curry). These semantics use a flat representation of programs coming from an implicit program transformation encoding the
demand analysis used by needed narrowing, and some kind of heaps to express
bindings for variables. As in our case, let-expressions are used to express sharing.
The approach is useful as a technical basis for implementation and program manipulation purposes; but we think that the approach is too low-level and close to
a particular operational strategy to be a completely satisfactory choice as basic
abstract reduction mechanism for call-time choice. In (López-Fraguas et al. 2007a)
we established a technical relation of CRWL with the operational procedures of
(Albert et al. 2005). But this turned out to be a really hard task, even if it was
done only for a restricted class of programs and expressions.
Our work focuses on term rewriting systems as basic formalism, as happens with
the majority of papers about the foundations of functional logic programming, in
particular the CRWL-series. The idea of reformulating graph rewriting in a syntactic style by expressing sharing through let-bindings has been applied also to other
contexts, most remarkably to λ-calculus considered as a basis of functional programming (Ariola and Arvind 1995; Ariola et al. 1995; Ariola and Felleisen 1997; Maraist
et al. 1998). In a different direction, but still in relation with λ-calculus, other papers (Kutzner and Schmidt-Schauß 1998; Schmidt-Schauß and Machkasova 2008)
have extended it with some kind of non-deterministic choice, an idea that comes
back to McCarthy’s amb (McCarthy 1963). As a final note, we should mention that
our initial ideas about let-rewriting were somehow inspired by (López-Fraguas and
Sánchez-Hernández 2001; Sánchez-Hernández 2004) where indexed unions of set
expressions —a construction generalizing the idea of let-expressions —were used to
express sharing in an extension of CRWL to deal with constructive failure.
The rest of the paper is organized as follows. Section 2 presents some preliminaries about term rewriting and the CRWL framework; although with them the
paper becomes almost self-contained, some familiarity with the basic notions of
TRS certainly help to read the paper. Section 3 contains a first discussion about
failed or partial solutions to the problem of expressing non-strict call-time choice
by a simple notion of rewriting. Section 4 is the central part of the paper. First,
it introduces local bindings in the syntax to express sharing, defines let-rewriting
as an adequate notion of rewriting for them and proves some intrinsic properties
of let-rewriting. After that, in Section 4.2, we extend the CRWL-logic to a new
CRWLlet -logic able to deal with lets in programs and expressions, and we investigate in depth the properties of the induced semantics, mostly through the notion
of hypersemantics. Finally, in Section 4.3 we prove results of soundness and completeness of let-rewriting with respect to CRWLlet , which have as corollary the
equivalence of both, and hence the equivalence of let-rewriting and CRWL for programs and expressions not containing lets, as the original CRWL ones are. Section
5 aims at showing the power of having reduction and semantics as equivalent interchangeable tools for reasoning, including a remarkable case study. In Section 6 we
generalize the notion of let-rewriting to that of let-narrowing and give soundness
and completeness results of the latter with respect to the former. At the end of
the section we give some hints on how computations can be organized according

8

López-Fraguas et al.

to known narrowing strategies. Section 7 addresses the relationship between letrewriting and classical term rewriting, proving in particular their equivalence for
semantically deterministic programs. Finally, Section 8 analyzes our contribution
and suggests further work. For the sake of readability, most of the (fully detailed)
proofs have been moved to Appendix A.
2 Preliminaries
2.1 Constructor based term rewriting systems
We assume a fixed first order signature Σ = CS ∪ F S, where CS and F S are two
disjoint sets of constructor and defined function symbols respectively, each of them
with an associated arity. We write CS n and F S n for the set of constructor and
function symbols of arity n respectively, and Σn for CS n ∪ F S n . As usual notations
we write c, d, . . . for constructors, f, g, . . . for functions and X, Y, . . . for variables
taken from a denumerable set V. The notation o stands for tuples of any kind of
syntactic objects.
The set Exp of expressions is defined as Exp 3 e ::= X | h(e1 , . . . , en ), where X ∈
V, h ∈ Σn and e1 , . . . , en ∈ Exp. The set CT erm of constructed terms (or c-terms)
has the same definition of Exp, but with h restricted to CS n (so CT erm Exp).
The intended meaning is that Exp stands for evaluable expressions, i.e., expressions
that can contain (user-defined) function symbols, while CT erm stands for data
terms representing values. We will write e, e0 , . . . for expressions and t, s, p, t0 , . . . for
c-terms. The set of variables occurring in an expression e will be denoted as var(e).
Contexts (with one hole) are defined by Cntxt 3 C ::= [ ] | h(e1 , . . . , C, . . . , en ),
where h ∈ Σn . The application of a context C to an expression e, written as C[e], is
defined inductively as follows:
[ ][e]
h(e1 , . . . , C, . . . , en )[e]

= e
= h(e1 , . . . , C[e], . . . , en )

Substitutions are finite mappings σ : V −→ Exp which extend naturally to σ :
Exp −→ Exp. We write eσ for the application of the substitution σ to e. The
domain and variable range of a substitution σ are defined as dom(σ) = {X ∈ V |
S
Xσ 6= X} and vran(σ) = X∈dom(σ) var(Xσ). By [X1 /e1 , . . . , Xn /en ] we denote
the substitution σ such that Y σ = ei if Y ≡ Xi for some Xi ∈ {X1 , . . . , Xn }, and
Y σ = Y otherwise. Given a set of variables D, the notation σ|D represents the
substitution σ restricted to D and σ|\D is a shortcut for σ|(V\D) . A c-substitution
is a substitution θ such that Xθ ∈ CT erm for all X ∈ dom(θ). We write Subst and
CSubst for the sets of substitutions and c-substitutions respectively.
A term rewriting system is any set of rewrite rules of the form l → r where
l, r ∈ Exp and l 6∈ V. A constructor based rewrite rule or program rule has the
form f (p1 , . . . , pn ) → r where f ∈ F S n , r ∈ Exp and (p1 , . . . , pn ) is a linear tuple
of c-terms, where linear means that no variable occurs twice in the tuple. Notice
that we allow r to have extra variables (i.e., variables not occurring in the lefthand side). To be precise, we say that X is an extra variable in the rule l → r iff
X ∈ var(r) \ var(l), and by vExtra(R) we denote the set of extra variables in a

Theory and Practice of Logic Programming

9

rule R. Then a constructor system or program P is any set of program rules, i.e., a
term rewriting system composed only of program rules.
Given a program P, its associated rewrite relation →P is defined as C[lσ] →P
C[rσ] for any context C, rule l → r ∈ P and σ ∈ Subst. There, the subexpression lσ
is called the redex used in that rewriting step. Notice that σ can instantiate extra
variables to any expression. For any binary relation R we write R∗ for the reflexive
and transitive closure of R, and Rn for the composition of R with itself n times.
∗
We write e1 →P e2 for a term rewriting derivation or reduction from e1 to e2 , and
n
e1 →P e2 for a n-step reduction. e2 is a normal form wrt. →P , written as ↓P e2 ,
if there is not any e3 such that e2 →P e3 ; and e2 is a normal form for e1 wrt.
∗
→P , written as e1 ↓P e2 , iff e1 →P e2 and e2 is a normal form. When presenting
derivations, we will sometimes underline the redex used at each rewriting step. In
the following, we will usually omit the reference to P when writing e1 →P e2 , or
denote it by P ` e1 → e2 .
A program P is confluent if for any e, e1 , e2 ∈ Exp such that e →∗P e1 , e →∗P e2
there exists e3 ∈ Exp such that both e1 →∗P e3 and e2 →∗P e3 .
2.2 The CRWL framework
We present here a simplified version of the CRWL framework (González-Moreno
et al. 1996; González-Moreno et al. 1999). The original CRWL logic considered also
the possible presence of joinability constraints as conditions in rules in order to
give a better treatment of strict equality as a built-in, a subject orthogonal to the
aims of this work. Furthermore, it is possible to replace conditions by the use of
an if then function, as has been technically proved in (Sánchez-Hernández 2004)
for CRWL and in (Antoy 2005) for term rewriting. Therefore, we consider only
unconditional program rules.
In order to deal with non-strictness at the semantic level, we enlarge Σ with a
new constant (i.e., a 0-ary constructor symbol) ⊥ that stands for the undefined
value. The sets Exp⊥ , CT erm⊥ , Subst⊥ , CSubst⊥ of partial expressions, etc., are
defined naturally. Notice that ⊥ does not appear in programs. Partial expressions
are ordered by the approximation ordering v defined as the least partial ordering
satisfying ⊥v e and e v e0 ⇒ C[e] v C[e0 ] for all e, e0 ∈ Exp⊥ , C ∈ Cntxt. This
partial ordering can be extended to substitutions: given θ, σ ∈ Subst⊥ we say θ v σ
if Xθ v Xσ for all X ∈ V.
The semantics of a program P is determined in CRWL by means of a proof
calculus able to derive reduction statements of the form e _ t, with e ∈ Exp⊥ and
t ∈ CT erm⊥ , meaning informally that t is (or approximates to) a possible value of
e, obtained by evaluating e using P under call-time choice.
The CRWL-proof calculus is presented in Figure 2. Rule (B) allows any expression to be undefined or not evaluated (non-strict semantics). Rule (OR) expresses
that to evaluate a function call we must choose a compatible program rule, perform
parameter passing (by means of a c-substitution θ) and then reduce the right-hand
side. The use of c-substitutions in (OR) is essential to express call-time choice; notice also that by the effect of θ in (OR), extra variables in the right-hand side of a

10

López-Fraguas et al.
(B)

(RR)

e_⊥

X∈V

X_X

(DC)

e1 _ t1 . . . en _ tn
c(e1 , . . . , en ) _ c(t1 , . . . , tn )

(OR)

e1 _ p1 θ . . . en _ pn θ rθ _ t
f (e1 , . . . , en ) _ t

c ∈ CS n
(f (p1 , . . . , pn ) → r) ∈ P
θ ∈ CSubst⊥

Fig. 2. Rules of CRWL

DC
0_0
OR
coin _ 0

0_0

DC

0_0

DC

0_0

DC

repeat(0) _⊥

0 : repeat(0) _ 0 :⊥

repeat(0) _ 0 :⊥

0 : repeat(0) _ 0 : 0 :⊥

repeat(coin) _ 0 : 0 :⊥

DC

OR

heads(repeat(coin)) _ (0, 0)

B
DC

OR
DC
DC
0_0
0_0
DC
(0, 0) _ (0, 0)
OR

Fig. 3. A CRWL-derivation for heads(repeat(coin)) _ (0, 0)
rule can be replaced by any partial c-term, but not by any expression as in ordinary
term rewriting →P . We write P `CRWL e _ t to express that e _ t is derivable in
the CRWL-calculus using the program P, but in many occasions we will omit the
mention to P, writing simply e _ t.
Definition 1 (CRWL-denotation)
Given a program P, the CRWL-denotation of an expression e ∈ Exp⊥ is defined as
[[e]]P
CRWL = {t ∈ CT erm⊥ | P `CRWL e _ t}
We will usually omit the subscript CRWL and/or the superscript P when implied
by the context.
As an example, Figure 3 shows a CRWL-derivation or CRWL-proof for the statement heads(repeat(coin)) _ (0, 0), using the program of Figure 1. Observe that in
the derivation there is only one reduction statement for coin (namely coin _ 0),
and the obtained value 0 is then shared in the whole derivation, as corresponds to
call-time choice.
In alternative derivations, coin could be reduced to 1 (or to ⊥). It is easy to check
that:
[[heads(repeat(coin))]] = {(0, 0), (1, 1), (⊥, 0), (0, ⊥), (⊥, 1), (1, ⊥), (⊥, ⊥), ⊥}
Note that (1, 0), (0, 1) 6∈ [[heads(repeat(coin))]].
We stress the fact that the CRWL-calculus is not an operational mechanism for
executing programs, but a way of describing the logic of programs. In particular,
the rule (B) is a semantic artifact to reflect in a CRWL-proof of a statement e _ t
the fact that, for obtaining t as value of e, one does not need to know the value of a

Theory and Practice of Logic Programming

11

certain subexpression e0 (to which the rule (B) is applied). But the calculus comes
with no indication of when to apply (B) in a successful proof. At the operational
level, the CRWL framework is accompanied with various lazy narrowing-based goalsolving calculi (González-Moreno et al. 1999; Vado-Vı́rseda 2003) not considered in
this paper.
One of the most important properties of CRWL is its compositionality, a property
very close to the DET-additivity property for algebraic specifications of (Hussmann
1993) or the referential transparency property of (Sondergaard and Sestoft 1990).
Compositionality shows that the CRWL-denotation of any expression placed in a
context only depends on the CRWL-denotation of that expression. This implies
that the semantics of a whole expression depends only on the semantics of its
constituents, as shown by the next result, which is an adaptation of a similar one
proved for the higher order case in (López-Fraguas et al. 2008).
Theorem 1 (Compositionality of CRWL)
For any C ∈ Cntxt, e, e0 ∈ Exp⊥
[[C[e]]] =

[

[[C[t]]]

t∈[[e]]

As a consequence: [[e]] = [[e0 ]] ⇔ ∀C ∈ Cntxt.[[C[e]]] = [[C[e0 ]]]
According to this result we can express for example
S
S
[[heads(repeat(coin))]] = t∈[[coin]] s∈[[repeat(t)]] [[heads(s)]]
The right hand side has an intuitive reading that reflects call-time choice: get a
value t of coin, then get a value s of repeat(t) and then get a value of heads(s).
In Theorem 2 we give an alternative formulation to the compositionality property.
Although it is essentially equivalent to Theorem 1, it is a somehow more abstract
statement, based on the notion of denotation of a context introduced in Definition
2. Our main reason for developing such alternative is to give good insights for the
compositionality results of the extension of CRWL to be presented in Section 4.3.
We will use sometimes Den as an alias for P(CT erm⊥ ), i.e, for the kind of objects
that are CRWL-denotations of expressions2 . We define the denotation of a context
C as a denotation transformer that reflects call-time choice.
Definition 2 (Denotation of a context)
Given C ∈ Cntxt, its denotation is a function [[C]] : Den → Den defined as
[
[[C]]δ =
[[C[t]]], ∀δ ∈ Den
t∈δ

With this notion, compositionality can be trivially re-stated as follows:
2

Den is indeed a superset of the set of actual denotations, which are particular elements of
P(CT erm⊥ ), namely cones —see (González-Moreno et al. 1999)—. But this is not relevant to
the use we make of Den.

12

López-Fraguas et al.

Theorem 2 (Compositionality of CRWL, version 2 )
For any C ∈ Cntxt and e, e0 ∈ Exp⊥
[[C[e]]] = [[C]][[e]]
0

As a consequence: [[e]] = [[e ]] ⇔ ∀C ∈ Cntxt.[[C[e]]] = [[C[e0 ]]]
The formulation of compositionality given by Theorem 2 makes even more apparent than Theorem 1 the fact that the syntactic decomposition of an expression e
in the form C[e0 ] has a direct semantic counterpart, in the sense that the semantics
of e is determined by the semantics of its syntactic constituents C and e0 . However,
Theorems 1 and 2 are indeed of the same strength, since each of them can be easily
proved from the other.
3 CRWL and rewriting: a first discussion
Before presenting let-rewriting we find interesting to discuss a couple of (in principle) shorter solutions to the problem of expressing non-strict call-time choice semantics by means of a simple one-step reduction relation. A first question is whether
a new relation is needed at all: maybe call-time choice can be expressed by ordinary
term rewriting via a suitable program transformation. The next result shows that
in a certain technical sense this is not possible: due to different closedness under
substitution and compositionality properties of call-time choice and term rewriting,
none of them can be naturally simulated by each other.
Proposition 1
There is a program P for which the following two conditions hold:
i) no term rewriting system (constructor based or not) P 0 verifies
P `CRW L e _ t iff P 0 ` e →∗ t , for all e ∈ Exp, t ∈ CT erm

ii) no program P 0 verifies

P ` e →∗ t iff P 0 `CRW L e _ t , for all e ∈ Exp, t ∈ CT erm
Proof
The following simple program P suffices:
f (X) → c(X, X)

coin → 0

coin → 1

i) We reason by contradiction. Assume there is a term rewriting system P 0
such that: P `CRWL e _ t ⇔ e →∗P 0 t, for all e, t. Since P `CRWL f (X) _
c(X, X), we must have f (X) →∗P 0 c(X, X). Now, since →∗P 0 is closed under substitutions (Baader and Nipkow 1998), we have f (coin) →∗P 0 c(coin, coin), and
thereforef (coin) →∗P 0 c(coin, coin) →∗P 0 c(0, 1). But it is easy to see that P `CRWL
f (coin) _ c(0, 1) does not hold.
ii) Assume now there is a program P 0 such that: P ` e →∗ t ⇔ P 0 `CRW L e _ t,
for all e, t. Since P ` f (coin) →∗ c(0, 1), we have P 0 `CRW L f (coin) _ c(0, 1). By
compositionality of call-time choice (Theorem 1), there must exist a possibly partial

Theory and Practice of Logic Programming
(Brw )
(ORrw )

C[e]
C[f (t1 θ, . . . , tn θ)]




C[⊥]
C[rθ]

13

∀C ∈ Cntxt, e ∈ Exp⊥
∀C ∈ Cntxt, f (t1 , . . . , tn ) → r ∈ P,
θ ∈ CSubst⊥

Fig. 4. A one-step reduction relation for non-strict call-time choice
t ∈ CT erm⊥ such that P 0 `CRW L coin _ t and P 0 `CRW L f (t) _ c(0, 1). Now we
distinguish cases on the value of t:
(a) If t ≡⊥, then monotonicity of CRW L-derivability —see (González-Moreno et al.
1999) or Proposition 3 below— proves that P 0 `CRW L f (s) _ c(0, 1) for any
s ∈ CT erm⊥ , in particular P 0 `CRW L f (0) _ c(0, 1). Then, by the assumption on
P 0 , it should be P ` f (0) →∗ c(0, 1), but this is not true.
(b) If t ≡ 0, then P 0 ` f (0) _ c(0, 1) as before. The cases t ≡ 1, t ≡ Y or t ≡ d(s) for
a constructor d different from 0, 1 lead to similar contradictions.

Notice that Proposition 1 does not make any assumption about signatures: in
any of i) or ii), no extension of the signature can lead to a simulating P 0 . This does
not contradict Turing completeness of term rewriting systems. Turing completeness arguments typically rely on encodings not preserving the structure of data,
something not contemplated in Proposition 1.
In a second trial, requiring minimal changes over ordinary term rewriting, we
impose that the substitution θ in a rewriting step must be a c-substitution, as in
the rule (OR) of CRWL. This is done in the one-step rule (ORrw ) in Figure 4.
According to it, the step heads(repeat(coin)) → heads(coin : repeat(coin)) in the
introductory example of Figure 1 would not be legal anymore. However, (ORrw )
corresponds essentially to innermost evaluation, and is not enough to deal with
non-strictness, as the following example shows:
Example 1
Consider the rules f (X) → 0 and loop → loop. With a non-strict semantics f (loop)
should be reducible to 0. But (ORrw ) does not allow the step f (loop) → 0; only
f (loop) → f (loop) → . . . is a valid (ORrw )-reduction, thus leaving f (loop) semantically undefined, as would correspond to a strict semantics.
At this point, the rule (B) of CRWL is a help, since it allows to discard the
evaluation of any (sub)-expression by reducing it to ⊥. The result of this discussion
is the one-step reduction relation  given in Figure 4.
This relation satisfies our initial goals to a partial extent, as it is not difficult to
prove the following equivalence result.
Theorem 3
Let P be a CRWL-program, e ∈ Exp⊥ and t ∈ CT erm⊥ . Then:
P `CRWL e _ t iff e ∗P t

14

López-Fraguas et al.

This result has an interesting reading: non-strict call-time choice can be achieved
via innermost evaluation if at any step one has the possibility of reducing a subexpression to ⊥ (then, we could speak also of call-by-partial value). For instance, a
-rewrite sequence with the example of Figure 1 would be:
heads(repeat(coin))  heads(repeat(0)) 
heads(0 : repeat(0))  heads(0 : 0 : repeat(0)) 
heads(0 : 0 :⊥)  (0, 0)
This gives useful intuitions about non-strict call-time choice and can actually
serve for a very easy implementation of it, but has a major drawback: in general,
reduction of a subexpression e requires a don’t know guessing between (Brw ) and
(ORrw ), because at the moment of reducing e it is not known whether its value
will be needed or not later on in the computation. Instead of reducing to ⊥, letrewriting will create a let-binding let U=e in . . . , which does not imply any guessing
and keeps e for its eventual future use.

4 Rewriting with local bindings
Inspired by (Ariola and Arvind 1995; Ariola et al. 1995; Ariola and Felleisen 1997;
Maraist et al. 1998; Plump 1998; Sánchez-Hernández 2004), let-rewriting extends
the syntax of expressions by adding local bindings to express sharing and call-time
choice. Formally the syntax for let-expressions is:
LExp 3 e ::= X | h(e1 , . . . , en ) | let X = e1 in e2
where X ∈ V, h ∈ Σn , and e1 , e2 , . . . , en ∈ LExp. The intended behaviour of
let X = e1 in e2 is that the expression e1 will be reduced only once (at most) and
then its corresponding value will be shared within e2 . For let X = e1 in e2 we call
e1 the definiens of X, and e2 the body of the let-expression.
The sets F V (e) of free and BV (e) bound variables of e ∈ LExp are defined as:
F V (X) = {X}
S
F V (h(e)) = ei ∈e F V (ei )
F V (let X = e1 in e2 ) = F V (e1 ) ∪ (F V (e2 )\{X})
BV (X) = ∅
S
BV (h(e)) = ei ∈e BV (ei )
BV (let X = e1 in e2 ) = BV (e1 ) ∪ BV (e2 ) ∪ {X}
Notice that with the given definition of F V (let X = e1 in e2 ) there are not recursive let-bindings in the language since the possible occurrences of X in e1 are not
considered bound and therefore refer to a ‘different’ X. For example, the expression let X = f (X) in g(X) can be equivalently written as let Y = f (X) in g(Y ).
This is similar to what is done in (Maraist et al. 1998; Ariola et al. 1995; Ariola
and Felleisen 1997), but not in (Albert et al. 2005; Launchbury 1993). Recursive
lets have their own interest but there is not a general consensus in the functional
logic community about their meaning in presence of non-determinism. We remark

Theory and Practice of Logic Programming

15

also that the let-bindings introduced by let-rewriting derivations to be presented
in Section 4.1 are not recursive. Therefore, recursive lets are not considered in this
work.
We will use the notation let X = a in e as a shortcut for let X1 = a1 in . . . in let
Xn = an in e. The notion of one-hole context is also extended to the new syntax:
C ::= [ ] | let X = C in e | let X = e in C | h(. . . , C, . . .)
By default, we will use contexts with lets from now on.
Free variables of contexts are defined as for expressions, so that F V (C) = F V (C[h]),
for any h ∈ Σ0 . However, the set BV (C) of variables bound by a context is defined
quite differently because it consists only of those let-bound variables visible from
the hole of C. Formally:
BV ([ ]) = ∅
BV (h(. . . , C, . . .)) = BV (C)
BV (let X = e in C) = {X} ∪ BV (C)
BV (let X = C in e) = BV (C)
As a noticeable difference with respect to (López-Fraguas et al. 2007b), from
now on we will allow to use lets in any program, so our program rules have the
shape f (p1 , . . . , pn ) → r, for f ∈ F S n , (p1 , . . . , pn ) a linear tuple of c-terms, and
r ∈ LExp. Notice, however, that the notion of c-term does not change: c-terms do
not contain function symbols nor lets, although they can contain bound variables
when put in an appropriate context as happens for example with the subexpression
(X, X) in the expression let X = coin in (X, X).
As usual with syntactical binding constructs, we assume a variable convention
according to which bound variables can be consistently renamed as to ensure that
the same variable symbol does not occur free and bound within an expression.
Moreover, to keep simple the management of substitutions, we assume that whenever θ is applied to an expression e ∈ LExp, the necessary renamings are done in
e to ensure BV (e) ∩ (dom(θ) ∪ vran(θ)) = ∅. With all these conditions the rules
defining application of substitutions are simple while avoiding variable capture:
Xθ = θ(X), for X ∈ V
h(e1 , . . . , en )θ = h(e1 θ, . . . , en θ), for h ∈ Σn
(let X = e1 in e2 )θ = let X = e1 θ in e2 θ
The following example illustrates the use of these conventions.
(let X = c(X) in let Y = z in d(X, Y ))[X/c(Y )]
= (let U = c(X) in let V = z in d(U, V ))[X/c(Y )]
= let U = c(c(Y )) in let V = z in d(U, V )
The following substitution lemma will be often a useful technical tool:
Lemma 1 (Substitution lemma for let-expressions)
Let e, e0 ∈ LExp⊥ , θ ∈ Subst⊥ and X ∈ V such that X 6∈ dom(θ) ∪ vran(θ). Then:
(e[X/e0 ])θ ≡ eθ[X/e0 θ]

16

López-Fraguas et al.

(Fapp) f (p1 , . . . , pn )θ →l rθ,

if (f (p1 , . . . , pn ) → r) ∈ P, θ ∈ CSubst

l

(LetIn) h(. . . , e, . . .) → let X = e in h(. . . , X, . . .),
if h ∈ Σ, e ≡ f (e0 ) with f ∈ F S or e ≡ let Y = e0 in e00 , and X is a fresh variable
(Bind) let X = t in e →l e[X/t],
l

(Elim) let X = e1 in e2 → e2 ,

if t ∈ CT erm
if X 6∈ F V (e2 )

(Flat) let X = (let Y = e1 in e2 ) in e3 →l let Y = e1 in (let X = e2 in e3 )
if Y 6∈ F V (e3 )
(Contx) C[e] →l C[e0 ],
if C =
6 [ ], e →l e0 using any of the previous rules, and in case e →l e0 is a (Fapp)
step using (f (p) → r) ∈ P and θ ∈ CSubst, then vran(θ|\var(p) ) ∩ BV (C) = ∅.

Fig. 5. Rules of the let-rewriting relation →l
4.1 The let-rewriting relation
Let-expressions can be reduced step by step by means of the let-rewriting relation
→l , shown in Figure 5. Rule (Contx) allows us to use any subexpression as redex
in the derivation. (Fapp) performs a rewriting step in the proper sense, using a
program rule. Note that only c-substitutions are allowed, to avoid copying of unevaluated expressions which would destroy sharing and call-time choice. To prevent
that the restriction of (Fapp) to total c-substitutions results in a strict semantics,
we also provide the rule (LetIn) that suspends the evaluation of a subexpression
by introducing a let-binding. If its value is needed later on, its evaluation can be
performed by some (Contx) steps and the result propagated by (Bind). This latter
rule is safe wrt. call-time choice because it only propagates c-terms, that is, either
completely defined values (without any bound variable) or partially computed values with some suspension (bound variable) on it, which will be safely managed by
the calculus. On the other hand, if the bound variable disappears from the body of
the let-binding during evaluation, rule (Elim) can be used for garbage collection.
This rule is useful to ensure that normal forms corresponding to values are c-terms.
Finally, (Flat) is needed for flattening nested lets; otherwise some reductions could
become wrongly blocked or forced to diverge. Consider for example the program
{loop → loop, g(s(X)) → 1} and the expression g(s(loop)), which can be reduced
to let X = (let Y = loop in s(Y )) in g(X) by applying (LetIn) twice. Then, without (Flat) we could only perform reduction steps on loop, thus diverging; by using
(Flat), we can obtain let Y = loop in let X = s(Y ) in g(X), which can be finally
reduced to 1 by applying (Bind), (Fapp) and (Elim). The condition Y 6∈ F V (e3 )
in (Flat) could be dropped by the variable convention, but we have included it to
keep the rules independent of the convention. Quite different is the case of (Elim),
where the condition X 6∈ F V (e2 ) is indeed necessary.
Note that, in contrast to CRWL or the relation  in Section 3, let-rewriting
does not need to use the semantic value ⊥, which does not appear in programs nor
in computations.
Example 2
Consider the program of Figure 1. We can perform the following let-rewriting deriva-

Theory and Practice of Logic Programming

17

tion for the expression heads(repeat(coin)), where in each step the corresponding
redex has been underlined for the sake of readability.
heads(repeat(coin))
→l let X = repeat(coin) in heads(X)
→l let X = (let Y = coin in repeat(Y )) in heads(X)
→l let Y = coin in let X = repeat(Y ) in heads(X)
→l let Y = coin in let X = Y : repeat(Y ) in heads(X)
→l let Y = coin in let X = (let Z = repeat(Y ) in Y : Z) in heads(X)
→l let Y = coin in let Z = repeat(Y ) in let X = Y : Z in heads(X)
→l let Y = coin in let Z = repeat(Y ) in heads(Y : Z)
→l let Y = coin in let Z = Y : repeat(Y ) in heads(Y : Z)
→l let Y = coin in let Z = (let U = repeat(Y ) in Y : U ) in heads(Y : Z)
→l let Y = coin in let U = repeat(Y ) in let Z = Y : U in heads(Y : Z)
→l let Y = coin in let U = repeat(Y ) in heads(Y : Y : U )
→l let Y = coin in let U = repeat(Y ) in (Y, Y )
→l let Y = coin in (Y, Y )
→l let Y = 0 in (Y, Y )
→l (0, 0)

(LetIn)
(LetIn)
(F lat)
(F app)
(LetIn)
(F lat)
(Bind)
(F app)
(LetIn)
(F lat)
(Bind)
(F app)
(Elim)
(F app)
(Bind)

Note that there is not a unique →l -reduction leading to (0, 0). The definition of
→l , like traditional term rewriting, does not prescribe any particular strategy. The
definition of on-demand evaluation strategies for let-rewriting is out of the scope of
this paper, and is only informally discussed in Section 6.2.
We study now some properties of let-rewriting that have intrinsic interest and
will be useful when establishing a relation to CRWL in next sections.
The same example used in Proposition 1 to show that CRWL is not closed under
general substitutions shows also that the same applies to let-rewriting. However,
let-rewriting is closed under c-substitutions, as expected in a semantics for call-time
choice.
Lemma 2 (Closedness under CSubst of let-rewriting)
n
n
For any e, e0 ∈ LExp, θ ∈ CSubst we have that e →l e0 implies eθ →l e0 θ.
Another interesting matter is the question of what happens in let-rewriting
derivations in which the rule (Fapp) is not used—and as a consequence, the program
is ignored.
Definition 3 (The →lnf relation)
The relation →lnf is defined by the rules of Figure 5 except (Fapp). As a consequence, for any program →lnf ⊆ →l .
We can think about any let-expression e as an expression from Exp in which
some additional sharing information has been encoded using the let-construction.
When we avoid the use of the rule (Fapp) in derivations, we do not make progress in
the evaluation of the implicit let-less expression corresponding to e, but we change
the sharing-enriched representation of that expression in the let-rewriting syntax.
Following terminology from term graph rewriting —as in fact a let-expression is a
textual representation of a term graph— all the rules of let-rewriting except (Fapp)

18

López-Fraguas et al.

move between two isomorphic term graphs (Plump 2001; Plump 1998). The →lnf
relation will be used to reason about these kind of derivations.
The first interesting property of →lnf is that it is a terminating relation.
Proposition 2 (Termination of →lnf )
For any program P, the relation →lnf is terminating. As a consequence, every
e ∈ LExp has at least one →lnf -normal form e0 (written as e ↓lnf e0 ).
However, for nontrivial signatures the relation →lnf is not confluent (hence the
relation →l is not confluent either).
Example 3
∗
Consider a signature such that f, g ∈ F S 0 , c ∈ CS 2 and f 6≡ g. Then c(f, g) →lnf
∗
let X = f in let Y = g in c(X, Y ) and c(f, g) →lnf let Y = g in let X =
f in c(X, Y ), but these expressions do not have a common reduct.
The lack of confluence of let-rewriting is alleviated by a strong semantic property
of →lnf which, combined with the adequacy to CRWL of let-rewriting that we will
see below, may be used as a substitute for confluence in some situations. These
questions will be treated in detail in Section 4.3.1.
The next result characterizes →lnf -normal forms. What we do in →lnf derivations
is exposing the computed part of e —its outer constructor part— concentrating it
in the body of the resulting let, that is, the part which is not a function application
whose evaluation is pending. This is why we call it ‘Peeling lemma’.
Lemma 3 (Peeling lemma)
For any e, e0 ∈ LExp, if e ↓lnf e0 then e0 has the shape e0 ≡ let X = f (t) in e00 such
that e00 ∈ V or e00 ≡ h(t0 ) with h ∈ Σ, f ⊆ F S and t, t0 ⊆ CT erm.
Moreover if e ≡ h(e1 , . . . , en ) with h ∈ Σ, then
∗

e ≡ h(e1 , . . . , en ) →lnf let X = f (t) in h(t1 , . . . , tn ) ≡ e0
under the conditions above, and verifying also that ti ≡ ei whenever ei ∈ CT erm.
The next property of →l and →lnf uses the notion of shell |e| of an expression
e, that is the partial c-term corresponding to the outer constructor part of e. More
precisely:
Definition 4 (Shell of a let-expression)
|X|
|c(e1 , . . . , en )|
|f (e1 , . . . , en )|
|let X = e1 in e2 |

=
=
=
=

X
c(|e1 |, . . . , |en |)
⊥
|e2 |[X/|e1 |]

for X ∈ V
for c ∈ CS
for f ∈ F S

Notice that in the case of a let-rooted expression, the information contained in the
binding is taken into account for building up the shell of the whole expression: for
instance |c(let X = 2 in s(X))| = c(s(2)).
During a computation, the evolution of shells reflects the progress towards a
value. The next result shows that shells never decrease. Moreover, only (Fapp) may

Theory and Practice of Logic Programming

19

change shells. As discussed above, ‘peeling’ steps (i.e. →lnf - steps) just modify the
representation of the implicit term graph corresponding to a let-expression; thus,
they preserve the shell.
Lemma 4 (Growing of shells)
∗
i) e →l e0 implies |e| v |e0 |, for any e, e0 ∈ LExp
∗
ii) e →lnf e0 implies |e| ≡ |e0 |, for any e, e0 ∈ LExp
4.2 The CRWLlet logic
In this section we extend the CRWL logic to deal with let-expressions, obtaining
an enlarged framework that will be useful as a bridge to establish the connection
between CRWL and let-rewriting.
As in the CRWL framework, we consider partial let-expressions e ∈ LExp⊥ ,
defined in the natural way. The approximation order v is also extended to LExp⊥
but now using the notion of context for let-expressions, which in particular implies
that let X = e1 in e2 v let X = e01 in e02 iff e1 v e01 and e2 v e02 . The CRWLlet
logic results of adding the following rule (Let) to the CRWL logic of Section 2.2:
(Let)

e1 _ t1

e2 [X/t1 ] _ t

let X = e1 in e2 _ t
We write P `CRWLlet e _ t if e _ t is derivable in the CRWLlet -calculus using
the program P. In many occasions, we will omit P.
Definition 5 (CRWLlet -denotation)
Given a program P, the CRWLlet -denotation of e ∈ LExp⊥ is defined as:
[[e]]P
CRWLlet = {t ∈ CT erm⊥ | P `CRWLlet e _ t}
We will omit the sub(super)-scripts when they are clear by the context.
There is an obvious relation between CRWL and CRWLlet for programs and
expressions without lets:
Theorem 4 (CRWL vs. CRWLlet )
For any program P without lets, and any e ∈ Exp⊥ :
P
[[e]]P
CRWL = [[e]]CRWLlet

This result allows us to skip the mention to CRWL or CRWLlet when referring
to the denotation [[e]] of an expression: if some let-binding occurs in e —or in the
program wrt. which the denotation is considered— then [[e]] can be interpreted only
as [[e]]CRWLlet ; otherwise, both denotations coincide.
The CRWLlet logic inherits from CRWL a number of useful properties.
Lemma 5
For any program e ∈ LExp⊥ , t, t0 ∈ CT erm⊥ :
i) t _ t0 iff t0 v t.
ii) |e| ∈ [[e]].

20

López-Fraguas et al.

iii) [[e]] ⊆ (|e|↑)↓, where for a given E ⊆ LExp⊥ its upward closure is E↑= {e0 ∈
LExp⊥ | ∃e ∈ E. e v e0 }, its downward closure is E↓= {e0 ∈ LExp⊥ | ∃e ∈
E. e0 v e}, and those operators are overloaded for let-expressions as e↑= {e}↑
and e↓= {e}↓.
The first part of the previous result shows that c-terms can only be reduced to
smaller c-terms. The other parts express that the shell of an expression represents
‘stable’ information contained in the expression in a similar way to Lemma 4, as
the shell is in the denotation by ii), and everything in the denotation comes from
refining it by iii).
The following results are adaptations to CRWLlet of properties known for CRWL
(González-Moreno et al. 1999; Vado-Vı́rseda 2002). The first one states that if we
can compute a value for an expression then from greater expressions we can reach
smaller values. The second one says that CRWLlet -derivability is closed for partial
c-substitutions.
Proposition 3 (Polarity of CRWLlet )
For any e, e0 ∈ LExp⊥ , t, t0 ∈ CT erm⊥ , if e v e0 and t0 v t then e _ t implies
e0 _ t0 with a proof of the same size or smaller—where the size of a CRWLlet -proof
is measured as the number of rules of the calculus used in the proof.
Proposition 4 (Closedness under c-substitutions of CRWLlet )
For any e ∈ LExp⊥ , t ∈ CT erm⊥ , θ ∈ CSubst⊥ , t ∈ [[e]] implies tθ ∈ [[eθ]].
Compositionality is a more delicate issue. Theorem 1 does not hold for CRWLlet ,
as shown by the following example: consider the program {f (0) → 1}, the expression
e ≡ f (X) and the context C ≡ let X = 0 in []. C[e] can produce the value 1.
However, f (X) can only be reduced to ⊥, and C[⊥] cannot reach the value 1. The
point in that example is that the subexpression e needs some information from the
context to produce a value that is then used by the context to compute the value
for the whole expression C[e]. This information may only be the definientia of some
variables of e that get bound when put in C; with this idea in mind we can state
the following weak compositionality result for CRWLlet .
Theorem 5 (Weak Compositionality of CRWLlet )
For any C ∈ Cntxt, e ∈ LExp⊥
[
[[C[e]]] =
[[C[t]]]
if BV (C) ∩ F V (e) = ∅
t∈[[e]]

As a consequence, [[let X = e1 in e2 ]] =

S

t1 ∈[[e1 ]] [[e2 [X/t1 ]]].

In spite of not being a fully general compositionality result, Theorem 5 can be
used to prove new properties of CRWLlet , like the following monotonicity property
related to substitutions, that will be used later on. It is formulated for the partial order v over LSubst⊥ (defined naturally as it happened for Susbt⊥ ) and the
preorder E over LSubst⊥ , defined by σ E σ 0 iff ∀X ∈ V, [[σ(X)]] ⊆ [[σ 0 (X)]].

Theory and Practice of Logic Programming

21

Proposition 5 (Monotonicity for substitutions of CRWLlet )
If σ v σ 0 or σ E σ 0 then [[eσ]] ⊆ [[eσ 0 ]], for any e ∈ LExp⊥ and σ, σ 0 ∈ LSubst⊥ .
The limitations of Theorem 5 make us yearn for another semantic notion for letexpressions with a better compositional behaviour. We have already seen that the
problem with CRWLlet is the possible loss of definientia when extracting an expression from its context. But in fact what bound variables need is access to the
values of their corresponding definientia, as it is done in the rule (Let) where the
value of the definiens is transmited to the body of the let-binding by applying a
c-substitution replacing the bound variable by that value. With these ideas in mind
we define the stronger notion of hyperdenotation (sometimes we say hypersemantics), which gives a more active role to variables in expressions: in contrast to the
denotation of an expression e, which is a set of c-terms, its hyperdenotation [[[e]]] is
a function mapping c-substitutions to denotations, i.e., to sets of c-terms.
Definition 6 (Hyperdenotation)
The hyperdenotation of an expression e ∈ LExp⊥ under a program P is a function
[[[e]]]P : CSubst⊥ → Den defined by [[[e]]]P θ = [[eθ]]P .
As usual, in most cases we will omit the mention to P. We will use sometimes
HD as an alias for CSubst⊥ → Den, i.e, for the kind of objects that are hyperdenotations of expressions.
The notion of hyperdenotation is strictly more powerful than the notion of
CRWLlet denotation. Equality of hyperdenotations implies equality of denotations
—because if [[[e]]] = [[[e0 ]]] then [[e]] = [[e]] = [[[e]]] = [[[e0 ]]] = [[e0 ]] = [[e0 ]]— but the
opposite does not hold: consider the program {f (0) → 1} and the expressions f (X)
and ⊥; they have the same denotation (the set {⊥}) but different hyperdenotations, as [[[⊥]]][X/0] 63 1 ∈ [[[f (X)]]][X/0]. Hypersemantics are useful to characterize
the meaning of expressions present in a context in which some of its variables may
get bound, like in the body of a let-binding or in the right hand side of a program
rule. Therefore are useful to reason about expressions put in arbitrary contexts, in
which let-bindings may freely appear.
Most remarkably, hyperdenotations allow to recover strong compositionality results for let-expressions similar to Theorems 1 and 2. We find it more intuitive to
start the analog to the latter. Semantics of contexts were defined as denotation
transformers (Definition 2). Analogously, the hypersemantics [[[C]]] of a context C is
a hyperdenotation transformer defined as follows:
Definition 7 (Hypersemantics of a context)
Given C ∈ Cntxt, its hyperdenotation is a function [[[C]]] : HD → HD defined by
induction over the structure of C as follows:
• [[[[]]]]ϕθ = ϕθ
S
• [[[h(e1 , . . . , C, . . . , en )]]]ϕθ =
[[h(e1 θ, . . . , t, . . . , en θ)]]
St∈[[[C]]]ϕθ
• [[[let X = C in e]]]ϕθ =
[[let X = t in eθ]]
t∈[[[C]]]ϕθ
S
• [[[let X = e in C]]]ϕθ =
[[[C]]]ϕ(θ[X/t])
t∈[[[e]]]θ

22

López-Fraguas et al.

With this notion, our first version of strong compositionality for hypersemantics
looks like Theorem 2.
Theorem 6 (Compositionality of hypersemantics)
For all C ∈ Cntxt, e ∈ LExp⊥
[[[C[e]]]] = [[[C]]][[[e]]]
As a consequence: [[[e]]] = [[[e0 ]]] ⇔ ∀C ∈ Cntxt.[[[C[e]]]] = [[[C[e0 ]]]].
This result implies that in any context we can replace any subexpression by another one having the same hypersemantics (and therefore also the same semantics)
without changing the hypersemantics (hence the semantics) of the global expression.
In Theorems 2 and 6 the role of call-time choice is hidden in the definition of semantics and hypersemantics of a context, respectively. To obtain a version of strong
compositionalty of hypersemantics closer to Theorem 1 and 5, we need some more
notions and notations about hyperdenotations or, more generally, about functions
in HD. Since they are set-valued functions, many usual set operations and relations can be lifted naturally in a pointwise manner to HD. The precise definitions
become indeed clearer if we give them for general sets, abstracting away the details
about HD. We introduce also some notions about decomposing set-valued functions that will be useful for hyperdenotations. We use freely λ-notation to write
down a function in the mathematical sense; we may write λx ∈ A to indicate its
domain A, if it not clear by the context.
Definition 8 (Operations and relations for set-valued functions)
Let A, B be two sets, F the set of functions A → P(B), and f, g ∈ F. Then:
i) The hyperunion of f, g is defined as f d g = λx ∈ A.f (x) ∪ g(x).
ii) More generally, the hyperunion of a family I ⊆ F, written indistinctly as
d I or d f , is defined as
f ∈I

d

I≡

d

f ∈I

f =def λx ∈ A.

[

f (x)

f ∈I

Notice that f d g = d {f, g}.
iii) We say that f is hyperincluded in g, written f b g, iff ∀x ∈ A.f (x) ⊆ g(x).
iv) A decomposition of f is any I ⊆ F such that d I = f .
v) The elemental decomposition of f is the following set of functions of F:

{b} if x = a
∆f = {λx ∈ A.
| a ∈ A, b ∈ f (a)}
∅ otherwise

{b} if x = a
Or, using the abbreviation λ̂a.{b} as a shorthand for λx.
,
∅ otherwise
∆f = {λ̂a.{b} | a ∈ A, b ∈ f (a)}

Theory and Practice of Logic Programming

23

Decompositions are used to split set-valued functions into smaller pieces; elemental
decompositions do it with minimal ones. For instance, if f : {a, b} → P({0, 1, 2}) is
given by f (a) = {0, 2} and f (b) = {1, 2}, then ∆f = {λ̂a.{0}, λ̂a.{2}, λ̂b.{1}, λ̂b.{2}}.
Hyperinclusion and hyperunion share many properties of standard set inclusion
and union. Some of them are collected in the next result, that refer also to decompositions:
Proposition 6
Consider two sets A, B, and let F be the set of functions A → P(B). Then:
i) b is indeed a partial order on F, and ∆f is indeed a decomposition of f ∈ F,
i.e., d (∆f ) = f .
ii) Monotonicity of hyperunion wrt. inclusion: for any I1 , I2 ⊆ F
I1 ⊆ I2 implies

d

I1 b d I2

iii) Distribution of unions: for any I1 , I2 ⊆ F

d

(I1 ∪ I2 ) = (d I1 ) d (d I2 )

iv) Monotonicity of decomposition wrt. hyperinclusion: for any f1 , f2 ∈ F
f1 b f2 implies ∆f1 ⊆ ∆f2
We will apply all these notions, notations and properties to the case when A ≡
CSubst⊥ and B ≡ CT erm⊥ (i.e. P(B) ≡ Den and therefore F ≡ HD). Therefore,
we can speak of the hyperunion of two hyperdenotations, or of a family of them,
we can elementarily decompose a hyperdenotation, etc.
Proposition 7 (Distributivity under context of hypersemantics unions)
[[[C]]](d H) =

d

[[[C]]]ϕ

ϕ∈H

With this result we can easily prove our desired new version of a strong compositionality result for hypersemantics, with a style closer to the formulations of
Theorems 1 and 5. This new form of compositionality will be used in Section 5.1 for
building a straightforward proof of the adequacy of a transformation that otherwise
becomes highly involved by using other techniques.
Theorem 7 (Compositionality of hypersemantics, version 2 )
For any C ∈ Cntxt, e ∈ LExp⊥ :
[[[C[e]]]] =

d

[[[C]]]ϕ, for any decomposition H of [[[e]]]

ϕ∈H

In particular: [[[C[e]]]] =

d

ϕ ∈ ∆[[[e]]]
0

[[[C]]]ϕ.

As a consequence: [[[e]]] = [[[e ]]] ⇔ ∀C ∈ Cntxt.[[[C[e]]]] = [[[C[e0 ]]]].

24

López-Fraguas et al.

Proof
[[[C[e]]]] = [[[C]]][[[e]]]
= [[[C]]](d H)
= d [[[C]]]ϕ

by compositionality v.1 (Theorem 6)
by definition of decomposition (Def. 8 iv)
by distributivity (Proposition 7)

ϕ∈H

As happened with Theorems 1 and 2 with respect to denotations, Theorems
6 and 7 are different aspects of the same property, which shows that the hypersemantics of a whole let-expression depends only on the hypersemantics of its
constituents; it also allows us to interchange in a context any pair of expressions
with the same hypersemantics. This is reflected on the fact that we have attached
[[[e]]] = [[[e0 ]]] ⇔ ∀C ∈ Cntxt.[[[C[e]]]] = [[[C[e0 ]]]] as a trivial consequence both in Theorem 6 and Theorem 7. Moreover, Theorem 6 can also be proved by a combination
of Theorem 7 and Propositions 6 i) and 7, in a similar way to the proof for Theorem
7 above.
[[[C[e]]]] =

d

[[[C]]]ϕ

by compositionality v.2 (Theorem 7)

ϕ∈H

= [[[C]]](d (∆[[[e]]]))
= [[[C]]][[[e]]]

by distributivity (Proposition 7)
because ∆[[[e]]] decomposes e (Proposition 6 i))

Therefore Theorems 6 and 7 are results with the same strength, two sides of the
same coin that will be useful tools for reasoning with hypersemantics.
To conclude, we present the following monotonicity property under contexts of
hypersemantics, which will be useful in the next section.
Lemma 6 (Monotonicity under contexts of hypersemantics)
For any C ∈ Cntxt, ϕ1 , ϕ2 ∈ HD:
ϕ1 b ϕ2 implies that [[[C]]]ϕ1 b [[[C]]]ϕ2
Proof
Assume ϕ1 b ϕ2 . Then:
[[[C]]]ϕ1 = [[[C]]](d (∆ϕ1 ))
= [[[C]]](d {λ̂µ.{t} | µ ∈ CSubst⊥ , t ∈ ϕ1 µ})
b [[[C]]](d {λ̂µ.{t} | µ ∈ CSubst⊥ , t ∈ ϕ2 µ})
= [[[C]]](d (∆ϕ2 ))
= [[[C]]]ϕ2

by
by
by
by
by

Proposition 6 i)
definition of ∆
Proposition 6 ii)
definition of ∆
Proposition 6 i)

We have now the tools needed to tackle the task of formally relating CRWL and
let-rewriting.
4.3 Equivalence of let-rewriting to CRWL and CRWLlet
In this section we prove soundness and completeness results of let-rewriting with
respect to CRWLlet and CRWL.

Theory and Practice of Logic Programming

25

4.3.1 Soundness
Concerning soundness we want to prove that →l -steps do not create new CRWLsemantic values. More precisely:
Theorem 8 (Soundness of let-rewriting)
∗
For all e, e0 ∈ LExp, if e →l e0 then [[e0 ]] ⊆ [[e]].
Notice that because of non-determinism ⊆ cannot be replaced by = in this theorem. For example, with the program P = {coin → 0, coin → 1} we can perform
the step coin →l 0, for which [[0]] = {0, ⊥}, [[coin]] = {0, 1, ⊥}.
It is interesting to explain why a direct reasoning with denotations fails to prove
Theorem 8.
A proof could proceed straightforwardly by a case distinction on the rules for
→l to prove the soundness of a single →l step. The problem is that the case for
a (Contx) step would need the following monotonicity property under context of
CRWLlet denotations:
[[e]] ⊆ [[e0 ]] implies [[C[e]]] ⊆ [[C[e0 ]]]
Unfortunately, the property is false, for the same reasons that already explained
the weakness of Theorem 5: the possible capture of variables when switching from
e to C[e].
Counterexample 1
Consider the program P = {f (0) → 1}. We have [[f (X)]] = {⊥} ⊆ {⊥, 0} = [[0]],
but when these expressions are placed within the context let X = 0 in [ ] we obtain
[[let X = 0 in f (X)]] = {⊥, 1} 6⊆ {⊥, 0} = [[let X = 0 in 0]].
The good thing is that we can overcome these problems by using hypersemantics. Theorem 8 will be indeed an easy corollary of the following generalization to
hypersemantics.
Theorem 9 (Hyper-Soundness of let-rewriting)
∗
For all e, e0 ∈ LExp, if e →l e0 then [[[e0 ]]] b [[[e]]].
And, in order to prove this generalized theorem, we also devise a generalization of
the faulty monotonicity property of CRWLlet denotations above mentioned. That
generalization is an easy consequence of the compositionality and monotonicity
under contexts of hypersemantics.
Lemma 7
For all e, e0 ∈ LExp⊥ and C ∈ Cntxt, if [[[e]]] b [[[e0 ]]] then [[[C[e]]]] b [[[C[e0 ]]]].
Proof
[[[C[e]]]] = [[[C]]][[[e]]]
b [[[C]]][[[e0 ]]]
= [[[C[e0 ]]]]

by Theorem 6
by Lemma 6, as [[[e]]] b [[[e0 ]]]
by Theorem 6

26

López-Fraguas et al.

With the help of Lemma 7, we can now prove Theorem 9 by a simple case distinction on the rules for →l and a trivial induction on the length of the derivation.
Now, Theorem 8 follows as an easy consequence.
Proof for Theorem 8
∗
Assume e →l e0 . By Theorem 9 we have [[[e0 ]]] b [[[e]]], and therefore [[e0 θ]] ⊆ [[eθ]] for
every θ ∈ CSubst⊥ . Choosing θ =  (the empty substitution) we obtain [[e0 ]] ⊆ [[e]]
as desired.
The moral then is that when reasoning about the semantics of expressions and
programs with lets it is usually better to lift the problem to the hypersemantic world,
and then particularize to semantics the obtained result. This is done, for instance,
in the following result:
Proposition 8 (The →lnf relation preserves hyperdenotation)
∗
For all e, e0 ∈ LExp, if e →lnf e0 then [[[e]]] = [[[e0 ]]]—and therefore [[e]] = [[e0 ]].
This result mirrors semantically the fact that →lnf performs transitions between
let-expressions corresponding to the same implicit term graph. Proposition 8 in
some sense lessens the importance of the lack of confluence for the →lnf relation
seen in Section 4.1. Preservation of hyperdenotation may be used in some situations
as a substitute for confluence, specially taking into account that let-rewriting and
CRWLlet enjoy a really strong equivalence, as it is shown in this section.
Finally, we combine the previous results in order to get our main result concerning
the soundness of let-rewriting with respect to the CRWLlet calculus:
Theorem 10 (Soundness of let-rewriting)
For any program P and e ∈ LExp we have:
∗

i) e →l e0 implies P `CRWLlet e _ |e0 |, for any e0 ∈ LExp.
∗
ii) e →l t implies P `CRWLlet e _ t, for any t ∈ CT erm.
Furthermore, if neither P nor e have lets then we also have:
∗

iii) e →l e0 implies P `CRWL e _ |e0 |, for any e0 ∈ LExp.
∗
iv) e →l t implies P `CRWL e _ t, for any t ∈ CT erm.

i)
ii)
iii)
iv)

Proof
∗
Assume e →l e0 . Then, by Theorem 8 we have [[e0 ]]CRWLlet ⊆ [[e]]CRWLlet . Since
|e0 | ∈ [[e0 ]]CRWLlet by Lemma 5, we get |e0 | ∈ [[e]]CRWLlet , which means e _ |e0 |.
Trivial by (i), since |t| = t for any t ∈ CT erm.
Just combining i) and Theorem 4.
Just combining ii) and Theorem 4.

Theory and Practice of Logic Programming

27

4.3.2 Completeness
Now we look for the reverse implication of Theorem 10, that is, the completeness
of let-rewriting as its ability to compute, for any given expression, any value that
can been computed by the CRWL-calculi. With the aid of the Peeling Lemma 3 we
can prove the following strong completeness result for let-rewriting, which still has
a certain technical nature.
Lemma 8 (Completeness lemma for let-rewriting)
For any e ∈ LExp and t ∈ CT erm⊥ such that t 6≡⊥,
∗

e _ t implies e →l let X = a in t0

for some t0 ∈ CT erm and a ⊆ LExp such that t v |let X = a in t0 | and |ai | =⊥
for every ai ∈ a. As a consequence, t v t0 [X/ ⊥].
Note the condition t 6≡⊥ is essential for this lemma to be true, as we can see by
taking P = {loop → loop} and e ≡ loop: while loop _⊥, the only LExp reachable
from loop is loop itself.
Our main result concerning completeness of let-rewriting follows easily from
Lemma 8. It shows that any c-term computed by CRWL or CRWLlet for an expression can be refined by a let-rewriting derivation; moreover, if the c-term is total,
then it can be exactly reached by let-rewriting.
Theorem 11 (Completeness of let-rewriting)
For any program P, e ∈ LExp, and t ∈ CT erm⊥ we have:
∗

i) P `CRWLlet e _ t implies e →l e0 for some e0 ∈ LExp such that t v |e0 |
∗
ii) Besides, if t ∈ CT erm then P `CRWLlet e _ t implies e →l t

Furthermore, if neither P nor e have lets then we also have
∗

iii) P `CRWL e _ t implies e →l e0 for some e0 ∈ LExp such that t v |e0 |
∗
iv) Besides, if t ∈ CT erm then P `CRWL e _ t implies e →l t
Proof
0
Regarding part i), if t ≡⊥ then we are done with e →l e as ∀e, ⊥v |e|. On the
∗
other hand, if t 6≡⊥ then by Lemma 8 we have e →l let X = a in t0 such that
t v |let X = a in t0 |.
To prove part ii), assume P `CRWLlet e _ t. Then, by Lemma 8, we get
∗
e →l let X = a in t0 such that t v |let X = a in t| ≡ t0 [X/⊥], for some t0 ∈
CT erm, a ⊆ LExp. As t ∈ CT erm then t is maximal wrt. v, so t v t0 [X/⊥] implies
t0 [X/⊥] ≡ t, but then t0 [X/⊥] ∈ CT erm so it must happen that F V (t0 ) ∩ X = ∅
∗
and therefore t0 ≡ t0 [X/⊥] ≡ t. But then let X = a in t0 →l t0 ≡ t by zero or more
∗
∗
∗
steps of (Elim), so e →l let X = a in t0 →l t, that is e →l t.
Finally, parts ii) and iv) follow from ii), iii) and Theorem 4.
As an immediate corollary of this completeness result and soundness (Theorem
10), we obtain the following result relating let-rewriting to CRWL and CRWLlet
for total c-terms, which gives a clean and easy way to understand the formulation
of the adequacy of let-rewriting.

28

López-Fraguas et al.

Corollary 1 (Equivalence of CRWLlet and let-rewriting for total values)
For any program P, e ∈ LExp, and t ∈ CT erm we have
∗

P `CRWLlet e _ t iff e →l t.
Besides if neither P nor e have lets then we also have
∗

P `CRWL e _ t iff e →l t.
As final consequence of Theorems 10 and 11 we obtain another strong equivalence result for both formalisms, this time expressed in terms of semantics and
hypersemantics.
Theorem 12 (Equivalence of CRWLlet and let-rewriting)
For any program P and e ∈ LExp:
∗

i) [[e]] = {|e0 | | e →l e0 }↓
∗
ii) [[[e]]] = λθ ∈ CSubst⊥ .({|e0 | | e →l e0 }↓)
where ↓ is the downward closure operator defined in Lemma 5.
Proof
∗
i) We prove both inclusions. Regarding [[e]] ⊆ {|e0 | | e →l e0 }↓, assume t ∈ [[e]]. By
∗
Theorem 11 there must exist some e0 ∈ LExp such that e →l e0 and t v |e0 |,
∗
therefore |e0 | ∈ {|e0 | | e →l e0 }. But this, combined with t v |e0 |, results in
∗
t ∈ {|e0 | | e →l e0 }↓.
∗
Regarding the other inclusion, consider some t ∈ {|e0 | | e →l e0 }↓. By definition of
∗
the ↓ operator, there must exist some e0 ∈ LExp such that t v |e0 | and e →l e0 .
But that implies |e0 | ∈ [[e]], by Theorem 10, which combined with t v |e0 | and the
polarity property (Proposition 3) gives us that t ∈ [[e]].
ii) Trivial by applying the previous item and the definition of hypersemantics of an
expression.

5 Semantic reasoning
Having equivalent notions of semantics and reduction allows to reason interchangeably at the rewriting and semantic levels. In this section we show the power of such
technique in different situations. We start with a concrete example, adapted from
(López-Fraguas et al. 2009b), where semantic reasoning leads easily to conclusions
non-trivially achievable when thinking directly in operational terms.
Example 4
Imagine a program using constructors a, b ∈ CS 0 , c ∈ CS 1 , d ∈ CS 2 and defining a
function f ∈ F S 1 for which we know that f (a) can be let-rewritten to c(a) and c(b)
but no other c-terms. Consider also an expression e having f (a) as subexpression,
i.e., e has the shape C[f (a)]. We are interested now in the following question: can
we safely replace in e the subexpression f (a) by any other ground expression e0

Theory and Practice of Logic Programming

29

let-reducible to the same set of values3 ? By safely we mean not changing the values
reachable from e.
The question is less trivial than it could appear. For instance, if reductions were
made with term rewriting instead of let-rewriting —i.e., considering run-time instead of call-time choice— the answer is negative (López-Fraguas et al. 2009b). To
see that, consider the program
f (a) → c(a) g → a
f (a) → c(b) g → b

h(c(X)) → d(X, X)

and the expressions e ≡ h(f (a)) and e0 ≡ c(g). All this is compatible with the
assumptions of our problem. However, e is reducible by term rewriting only to
d(a, a) and d(b, b), while replacing f (a) by e0 in e gives h(c(g)), which is reducible
by term rewriting to two additional values, d(a, b) and d(b, a); thus, the replacement
of f (a) by e0 has been unsafe.
However, the answer to our question is affirmative in general for let-rewriting, as
it is very easily proved by a semantic reasoning using compositionality of CRWLlet :
the assumption on f (a) and e0 means that they have the same denotation [[f (a)]] =
[[e0 ]] = {c(a), c(b)} ↓ and, since they are ground, the same hyperdenotation [[[f (a)]]] =
[[[e0 ]]] = λθ.{c(a), c(b)} ↓. By compositionality of hypersemantics, C[f (a)] and C[e0 ]
have the same (hyper)denotation, too. By equivalence of CRWLlet and let-rewriting
this implies that both expressions reach the same value by let-rewriting.
Despite its simplicity, the example raises naturally interesting questions about
replaceability, for which semantic methods could be simpler than direct reasonings
about reduction sequences. This is connected to the full abstraction problem that
we have investigated for run-time and call-time choice in (López-Fraguas et al.
2009b; López-Fraguas and Rodrı́guez-Hortalá 2010).
Semantic methods can be also used to prove the correctness of new operational
rules not directly provided by our set of let-rewriting rules. Such rules can be useful
for different purposes: to make computations simpler, for program transformations,
to obtain new properties of the framework, . . . Consider for instance the following
generalization of the (LetIn) rule in Figure 5:
(CLetIn) C[e] →l let X = e in C[X],

if BV (C) ∩ F V (e) = ∅ and X is fresh

This rule allows to create let-bindings in more situations and to put them in outer
positions than the original (LetIn) rule. If we have not considered it in the definition of let-rewriting is because it would destroy the strong termination property of
Proposition 2, as it is easy to see. However, this rule may shorten derivations. For
instance, the derivation in Example 2 could be shortened to:

3

More precisely, to the same set of shells in the sense of Theorem 12 part i).

30

López-Fraguas et al.

heads(repeat(coin))
→l let C = coin in heads(repeat(C))
→l let C = coin in heads(C : repeat(C))
→l let C = coin in heads(C : C : repeat(C))
→l let C = coin in let X = repeat(C) in heads(C : C : X)
→l let C = coin in let X = repeat(C) in (C, C)
→l let C = coin in (C, C)
→l let C = 0 in (C, C)
→l (0, 0)

(CLetIn)
(F app)
(F app)
(CLetIn)
(F app)
(Elim)
(F app)
(Bind)

Reasoning the correctness of (CLetIn) rule is not difficult by means of semantic
methods. We only need to prove that the rule preserves hypersemantics.
Lemma 9
If BV (C) ∩ F V (e) = ∅ and X is fresh, then [[[C[e]]]] = [[[let X = e in C[X]]]].
Proof
Assume an arbitrary θ ∈ CSubst⊥ :
[[[let X = e in C[X]]]]θ = [[(let X = e in C[X])θ]]
= [[let X = eθ in Cθ[X]]]
S
=
[[(Cθ[X])[X/t]]]
t∈[[eθ]]
S
=
[[Cθ[t]]]

as X is fresh
by Theorem 5
as X is fresh

t∈[[eθ]]

= [[Cθ[eθ]]]
= [[(C[e])θ]] = [[[C[e]]]]θ

by Theorem 5

The rule (CLetIn) is indeed used in some of the proofs in the online appendix,
together with another derived rule:
(Dist) C[let X = e1 in e2 ] →l let X = e1 in C[e2 ],
if BV (C) ∩ F V (e1 ) = ∅ and X 6∈ F V (C)
which also preserves hypersemantics:
Lemma 10
If BV (C) ∩ F V (e1 ) = ∅ and X 6∈ F V (C) then [[[C[let X = e1 in e2 ]]]] = [[[let X =
e1 in C[e2 ]]]].
These ideas can be made more general. Consider the equivalence relation e1 
e2 iff [[[e1 ]]] = [[[e2 ]]]. This relation is especially relevant because e1  e2 iff ∀C ∈
Cntxt.[[[C[e]]]] = [[[C[e0 ]]]], by Theorem 6. We can contemplate  as an abstract,
although non-effective, reduction relation, of which the relations →lnf of Section 4
and the rules (CLetIn) and (Dist) are particular subrelations. It is trivial to check
that, by construction, the combined relation →l ∪  is sound and complete wrt.
CRWLlet . We can use that relation to reason about the meaning or equivalence
of let-expressions and programs. We could also employ it in the definition of ondemand evaluation strategies for let-rewriting. As any subrelation of →l ∪  is

Theory and Practice of Logic Programming

31

sound wrt. CRWLlet , an approach to strategies for let-rewriting could consist in
defining a suitable operationally effective subrelation of →l ∪  and then proving
its completeness and optimality (if it is the case).

5.1 A case study: correctness of bubbling
We develop here another nice application of the ‘semantic route’, where let-rewriting
provides a good level of abstraction to formulate a new operational rule —bubbling—
while the semantic point of view is appropriate for proving its correctness.
Bubbling, proposed in (Antoy et al. 2007), is an operational rule devised to
improve the efficiency of functional logic computations. Its correctness was formally
studied in (Antoy et al. 2006) in the framework of a variant (Echahed and Janodet
1998) of term graph rewriting. The idea of bubbling is to concentrate all nondeterminism of a system into a choice operation ? defined by the rules X ? Y → X
and X ? Y → Y , and to lift applications of ? out of their surrounding context, as
illustrated by the following graph transformation taken from (Antoy et al. 2006):

As it is shown in (Antoy et al. 2007), bubbling can be implemented in such a way
that many functional logic programs become more efficient, but we will not deal
with these issues here.
Due to the technical particularities of term graph rewriting, not only the proof of
correctness, but even the definition of bubbling in (Antoy et al. 2007; Antoy et al.
2006) are involved and need subtle care concerning the appropriate contexts over
which choices can be bubbled. In contrast, bubbling can be expressed within our
framework in a remarkably easy and abstract way as a new rewriting rule:
(Bub)

C[e1 ?e2 ] →bub C[e1 ]?C[e2 ], for e1 , e2 ∈ LExp

With this rule, the bubbling step corresponding to the graph transformation of
the example above is:
let X = true ? f alse in c(not(X), not(X)) →bub
let X = true in c(not(X), not(X)) ? let X = f alse in c(not(X), not(X))
Notice that the effect of this bubbling step is not a shortening of any existing letrewriting derivation; bubbling is indeed a genuine new rule, the correctness of which
must be therefore subject of proof. Call-time choice is essential, since bubbling is
not correct with respect to ordinary term rewriting, i.e., run-time choice.
Counterexample 2 (Incorrectness of bubbling for run-time choice)
Consider a function pair defined by the rule pair(X) → c(X, X) and the expression

32

López-Fraguas et al.

pair(0 ? 1) for c ∈ CS 2 and 0, 1 ∈ CS 0 . Under term rewriting/run-time choice the
derivation
pair(0 ? 1) → c(0 ? 1, 0 ? 1) → c(0, 0 ? 1) → c(0, 1)
is valid. But if we performed the bubbling step
pair(0 ? 1) →bub pair(0) ? pair(1)
then the c-term c(0, 1) would not be reachable anymore by term rewriting from
pair(0) ? pair(1).
Formulating and proving the correctness of bubbling for call-time choice becomes
easy by using semantics. As we did before, we simply prove that bubbling steps
preserve hypersemantics. We need first a basic property of the (hyper)semantics of
binary choice ?. Its proof stems almost immediately from the rules for ? and the
definition of CRWL-(hyper)denotation.
Proposition 9 ((Hyper)semantic properties of ?)
For any e1 , e2 ∈ LExp⊥
i) [[e1 ? e2 ]] = [[e1 ]] ∪ [[e2 ]]
ii) [[[e1 ? e2 ]]] = [[[e1 ]]] d [[[e2 ]]]
Combining this property with some of the powerful hypersemantic results from
Section 4.2 leads to an appealing proof of the correctness of bubbling.
Theorem 13 (Correctness of bubbling for call-time choice)
If e →bub e0 then [[[e]]] = [[[e0 ]]], for any e, e0 ∈ LExp.
Proof
If e →bub e0 then e = C[e1 ? e2 ] and e0 = C[e1 ] ? C[e2 ], for some e1 , e2 . Then:
[[[C[e1 ? e2 ]]]] = [[[C]]][[[e1 ? e2 ]]] by Theorem 6
= [[[C]]]([[[e1 ]]] d [[[e2 ]]])
by Proposition 9 ii)
= [[[C]]][[[e1 ]]] d [[[C]]][[[e2 ]]]
by Proposition 7
= [[[C[e1 ]]]] d [[[C[e2 ]]]]
by Theorem 6
= [[[C[e1 ] ? C[e2 ]]]]
by Proposition 9 ii)

This property was proved also for the HO case in (López-Fraguas et al. 2008).
But the proof given here is much more elegant thanks to the new semantic tools
developed in Section 4.2.
6 Let-narrowing
It is well known that there are situations in functional logic computations where
rewriting is not enough and must be lifted to some kind of narrowing, because
the expression being reduced contains variables for which different bindings might
produce different evaluation results. This might happen either because variables are

Theory and Practice of Logic Programming

33

already present in the initial expression to reduce, or due to the presence of extra
variables in the program rules. In the latter case let-rewriting certainly works, but
not in an effective way, since the parameter passing substitution in the rule (Fapp)
of Figure 5 (page 16) ‘magically’ guesses the appropriate values for those extra
variables (see Example 6 below). Some works (Antoy and Hanus 2006; Dios-Castro
and López-Fraguas 2007; Braßel and Huch 2007) have proved that guessing can
be replaced by a systematic non-deterministic generation of all (ground) possible
values. However, this does not cover all aspects of narrowing, which is able to
produce non-ground answers, while generator functions are not. In this section we
present let-narrowing, a natural lifting of let-rewriting devised to effectively deal
with free and extra variables.
Using the notation of contexts, the standard definition of narrowing as a lifting
of term rewriting in ordinary TRS’s is the following: C[f (t)] θ Cθ[rθ], if θ is a
mgu of f (t) and f (s), where f (s) → r is a fresh variant of a rule of the TRS. The
requirement that the binding substitution θ is a mgu can be relaxed to accomplish
with certain narrowing strategies like needed narrowing (Antoy et al. 2000), which
use unifiers but not necessarily most general ones.
This definition of narrowing cannot be directly translated as it is to the case of letrewriting, for two reasons. First, binding substitutions must be c-substitutions, as
for the case of let-rewriting. Second, let-bound variables should not be narrowed, but
their values should be rather obtained by evaluation of their binding expressions.
The following example illustrates some of the points above.
Example 5
Consider the following program over Peano natural numbers:
0+Y →Y
s(X) + Y → s(X + Y )
0 == 0 → true
0 == s(Y ) → f alse
coin → 0

even(X) → if (Y +Y == X) then true
if true then Y → Y
s(X) == s(Y ) → X == Y
s(X) == 0 → f alse
coin → s(0)

Notice the extra variable Y in the rule for even. The evaluation of even(coin) by
let-rewriting could start as follows:
even(coin) →l let X = coin in even(X)
→l let X = coin in if (Y + Y == X) then true
∗
→l let X = coin in let U = Y + Y in let V = (U == X) in if V then true
∗
→l let U = Y + Y in let V = (U == 0) in if V then true
Now, because all function applications involve variables, the evaluation cannot continue merely by rewriting, and therefore narrowing is required instead. We should
not perform standard narrowing steps that bind already let-bound variables; otherwise, the syntax of let-expressions can be lost. For instance, narrowing at if V
then true generates the binding [V /true] that, if applied naively to the surrounding
context, results in the syntactically illegal expression:
let U=Y+Y in let true=(U==0) in true

34

López-Fraguas et al.

(X) e

l



e0

if e →l e0 using X∈ {LetIn, Bind, Elim, F lat} in Figure 5 (page 16).

(Narr) f (t) l θ rθ, for any fresh variant (f (p) → r) ∈ P and θ ∈ CSubst such that
f (t)θ ≡ f (p)θ.
l
0
(Contx) C[e]
6 [], if e l θ e0 by any of the previous rules, and if
θ Cθ[e ], for C =
the step is (Narr) using (f (p) → r) ∈ P, then:
(i) dom(θ) ∩ BV (C) = ∅
(ii) vRan(θ|\var(p) ) ∩ BV (C) = ∅

Fig. 6. Rules of the let-narrowing relation

l

What is harmless is to perform narrowing at Y + Y (Y is a free variable). This
gives the substitution [Y /0] and the result 0 for the subexpression Y + Y . Placing
it in its surrounding context, the derivation continues as follows:
let U = 0 in let V = (U == 0) in if V then true
→l let V = (0 == 0) in if V then true
→l let V = true in if V then true
→l if true then true →l true
The previous example shows that let-narrowing must protect bound variables
against substitutions, which is the key observation for defining narrowing in presence of let-bindings.
The one-step let-narrowing relation e l θ e0 (assuming a given program P) is
defined in Figure 6.
• The rule (X) collects (Elim), (Bind), (Flat), (LetIn) of →l , that remain the
l
same in
, except for the decoration with the empty substitution .
• The rule (Narr) performs a narrowing step in a proper sense. To avoid unnecessary loss of generality or applicability of our approach, we do not impose
θ to be a mgu. For the sake of readability, we will sometimes decorate (Narr)
steps with θ|F V (f (t)) instead of θ, i.e., with the projection over the variables
in the narrowed expression.
• The rule (Contx) indicates how to use the previous rules in inner positions.
The condition C =
6 [ ] simply avoids trivial overlappings of (Contx) with the
previous rules. The rest of the conditions are set to ensure that the combination of (Contx) with (Narr) makes a proper treatment of bound variables:
— (i) expresses the protection of bound variables against narrowing justified in Example 5.
— (ii) is a rather technical condition needed to prevent undesired situations
when the narrowing step has used a program rule with extra variables
and a unifier θ which is not a mgu. Concretely, the condition states that
the bindings created by θ for the extra variables in the program rule do
not introduce variables that are bound by the surrounding context C.
To see the problems that can arise without (ii), consider for instance
the program rules f → Y and loop → loop and the expression let X =
loop in f . A legal reduction for this expression, respecting condition (ii)

Theory and Practice of Logic Programming

35

could be the following:
let X = loop in f

l



let X = loop in Z

by applying (Narr) to f with θ =  taking the fresh variant rule f →
Z, and using (Contx) for the whole expression. However, if we drop
condition (ii) we could perform a similar derivation using the same fresh
variant of the rule for f , but now using the substitution θ = [Z/X]:
let X = loop in f

l



let X = loop in X

which is certainly not intended because the free variable Z in the previous derivation appears now as a bound variable, i.e., we get an undesired
capture of variables.
We remark that if the substitution θ in (Narr) is chosen to be a standard
mgu4 of f (t) and f (p) (which is always possible) then the condition (ii)
is always fulfilled.
l
The one-step relation
θ is extended in the natural way to the multiple-steps
∗
narrowing relation lθ , which is defined as the least relation verifying:

e
We write e

ln
θ

l∗


e

e

l

θ 1 e1

l

θ2

. . . en

l

θn e

0

l∗
θ1 ...θn

⇒ e

e0

e0 for a n-steps narrowing sequence.

Example 6
Example 5 essentially contains already a narrowing derivation. For the sake of
clarity, we repeat it here making explicit the rule of let-narrowing used at each step
(maybe in combination with (Contx), which is not written). Besides, if the step
uses (Narr), the narrowed expression is underlined.
even(coin) l 
let X = coin in even(X) l 
3
let X = coin in if Y + Y == X then true l
let X = coin in let U = Y + Y in
let V = (U == X) in if V then true l 
let X = 0 in let U = Y + Y in
let V = (U == X) in if V then true l 
let U = Y +Y in let V = (U == 0) in if V then true
let U = 0 in let V = (U == 0) in if V then true l 
let V = (0 == 0) in if V then true l 
let V = true in if V then true l 
if true then true l 
true

(LetIn)
(N arr)
(LetIn2 , F lat)
(N arr)

l

[Y/0]

(Bind)
(N arr)
(Bind)
(N arr)
(Bind)
(N arr)

Notice that all (Narr) steps in the derivation except one have  as narrowing
substitution (because of the projection over the variables of the narrowed expression), so they are really rewriting steps. An additional remark that could help to
4

By standard mgu of t, s we mean an idempotent mgu θ with dom(θ) ∪ ran(θ) ⊆ var(t) ∪ var(s).

36

López-Fraguas et al.

further explain the relationship between the let-narrowing relation l and the letrewriting relation →l is the following: since we have even(coin) l θ true for some
θ, but even(coin) is ground, Theorem 14 in next section ensures that there must
∗
be also a successful let-rewriting derivation even(coin) →l true. This derivation
could have the form:
even(coin) →l
let X = coin in even(X) →l
let X = coin in if (0 + 0 == X) then true →l
. . . . . . . . . →l true

(LetIn)
(F app)

The indicated (Fapp)-step in this let-rewriting derivation has used the substitution [Y /0], thus anticipating and ‘magically guessing’ the correct value of the
extra variable Y of the rule of even. In contrast, in the let-narrowing derivation the
binding for Y is not done while reducing even(X) but in a later (Narr)-step over
Y + Y . This corresponds closely to the behavior of narrowing-based systems like
Toy or Curry.

6.1 Soundness and completeness of the let-narrowing relation

l

In this section we show the adequacy of let-narrowing wrt. let-rewriting. From now
on we assume a fixed program P.
As usual with narrowing relations, soundness results are not difficult to formulate
l
and prove. The following soundness result for
states that we can mimic any
l
l
derivation with → by applying over the starting expression the substitution
computed by the original let-narrowing derivation.
Theorem 14 (Soundness of the let-narrowing relation
0

For any e, e ∈ LExp, e

l∗
θ

l

)

l∗ 0

0

e implies eθ → e .

Completeness is more complicated to prove. The key result is a generalization
to let-rewriting of Hullot’s lifting lemma (Hullot 1980) for classical term rewriting
and narrowing. It states that any rewrite sequence for a particular instance of an
expression can be generalized by a narrowing derivation.
Lemma 11 (Lifting lemma for the let-rewriting relation →l )
∗

Let e, e0 ∈ LExp such that eθ →l e0 for some θ ∈ CSubst, and let W, B ⊆ V with
dom(θ) ∪ F V (e) ⊆ W, BV (e) ⊆ B and (dom(θ) ∪ vran(θ)) ∩ B = ∅, and for each
∗
(Fapp) step of eθ →l e0 using a rule R ∈ P and a substitution γ ∈ CSubst then
∗
vran(γ|vExtra(R) ) ∩ B = ∅. Then there exist a derivation e l σ e00 and θ0 ∈ CSubst
such that:
(i) e00 θ0 = e0

(ii) σθ0 = θ[W]

(iii) (dom(θ0 ) ∪ vran(θ0 )) ∩ B = ∅

Besides, the let-narrowing derivation can be chosen to use mgu’s at each (Narr)
step. Graphically:

Theory and Practice of Logic Programming
e

l∗
σ

e00
θ0

θ
eθ

37

l

∗

e0

With the aid of this lemma we are now ready to state and prove the following
l
strong completeness result for
.
l
Theorem 15 (Completeness of the let-narrowing relation
)
0
l∗ 0
Let e, e ∈ LExp and θ ∈ CSubst. If eθ → e , then there exist a let-narrowing
∗
derivation e l σ e00 and θ0 ∈ CSubst such that e00 θ0 ≡ e0 and σθ0 = θ[F V (e)].

Proof
∗
Applying Lemma 11 to eθ|F V (e) →l e0 with W = F V (e) and B = BV (e), as
eθ|F V (e) ≡ eθ and the additional conditions over B hold by the variable convention.
Finally, by combining Theorems 14 and 15, we obtain a strong adequacy theorem
for let-narrowing with respect to let-rewriting.
Theorem 16 (Adequacy of the let-narrowing relation
Let e, e1 ∈ LExp and θ ∈ CSubst, then:

l

wrt. →l )
∗

∗

eθ →l e1 ⇔

there exist a let-narrowing derivation e lσ e2 and
some θ0 ∈ CSubst such that σθ0 = θ[F V (e)], e2 θ0 ≡ e1

Proof
∗
∗
(⇒) Assume eθ →l e1 . As eθ|F V (e) ≡ eθ then trivially eθ|F V (e) →l e1 . We can
∗
l
apply Lemma 11 taking W = F V (e) to get e
σ e2 such that there exists
0
0
0
θ ∈ CSubst with σθ = θ|F V (e) [W] and e2 θ ≡ e1 . But as W = F V (e) then
σθ0 = θ|F V (e) [W] implies σθ0 = θ[F V (e)].
We remark that the lifting lemma ensures that the narrowing derivation can be
chosen to use mgu’s at each (Narr) step.
l∗
0
(⇐) Assume e
σ e2 and θ under the conditions above. Then by Theorem
l∗
14 we have eσ → e2 . As →l is closed under c-substitutions (Lemma 2) then
∗
∗
eσθ0 →l e2 θ0 . But as σθ0 = θ[F V (e)], then eθ ≡ eσθ0 →l e2 θ0 ≡ e1 .

6.2 Organizing computations
Deliberately, in this paper we have kept the definitions of let-rewriting and narrowing apart from any particular computation strategy. In this section we explain
rather informally how the ideas of some known strategies for functional logic programming (Antoy 2005) can be adapted also to our formal setting. For the sake
of brevity we focus only on let-narrowing computations. As a running example,
consider the program

38

López-Fraguas et al.
leq(0, Y ) → true
leq(s(X), 0) → f alse
leq(s(X), s(Y )) → leq(X, Y )

f (0) → 0

and the initial expression leq(X, f (Y )) to be let-narrowed using it.
As a first remark, when designing a strategy one can freely use ‘peeling’ steps in a
don’t care manner using the relation →lnf (Definition 3), since it is terminating and
(hyper-)semantics-preserving. In our case one step suffices: leq(X, f (Y )) l  let U =
f (Y ) in leq(X, U ). After a peeling (multi-)step, a (Narr) step must be done. Where?
Certainly, the body leq(. . .) must be narrowed at some point. One don’t know possibility is narrowing at leq(X, U ) using the first rule for leq that does not bind U :
let U = f (Y ) in leq(X, U ) l [X/0] let U = f (Y ) in true. A new peeling step leads
to a first final result true, with computed substitution [X/0].
The second and third rules for leq could lead to more results. Those rules have
non-variable patterns as second arguments, and then the bound variable U in
leq(X, U ) inhibits a direct (Narr) step in that position. Typically it is said that
U is demanded by those leq rules. Therefore, we narrow f (Y ) to get values for U ,
and then we ‘peel’:
let U = f (Y ) in leq(X, U )

l

[Y /0] let

U = 0 in leq(X, U )

l

 leq(X, 0)

(1)

The computation proceeds now by two don’t know choices using the rules for leq,
leading to two more solutions (true, [Y /0, X/0]) and (f alse, [Y /0, X/s(Z)]).
This implicitly applied strategy can be seen as a translation to let-narrowing
of lazy narrowing (Moreno-Navarro and Rodrı́guez-Artalejo 1992; Alpuente et al.
2003). As a known drawback of lazy narrowing, notice that the second solution
(true, [Y /0, X/0]) is redundant, since it is less general than the first one (true, [X/0]).
Redundancy is explained because we have narrowed the expression f (Y ) whose evaluation was demanded only by some of the rules for the outer function application
leq(X, f (Y )), but after that we have used the rules not demanding the evaluation
(the first rule for leq). This problem is tackled successfully by needed narrowing
(Antoy et al. 2000) which takes into account, when narrowing an inner expression,
what are the rules for an outer function application demanding such evaluation. A
needed narrowing step ‘anticipates’ the substitution that will perform these rules
when they are to be applied. The ideas of needed narrowing can be adapted to our
setting. In our example, we get the following derivation instead of (1):
let U = f (Y ) in leq(X, U )
leq(s(Z), 0) l  f alse

l

[X/s(Z),Y /0] let

U = 0 in leq(s(Z), U )

l



(1’)

The first step does not use a mgu. This a typical feature of needed narrowing, and
is also allowed by let-narrowing steps. Needed narrowing steps rely on definitional
trees that structure demandness information from the rules of a given function. This
information can be embedded also into a program transformation. There are simple
transformations for which the transformed program, under a lazy narrowing regime
using mgu’s, obtains the same solutions than the original program (Zartmann 1997),
although it is not guaranteed that the number of steps is also preserved. In our
example, the definition of leq can be transformed as follows:

Theory and Practice of Logic Programming
leq(0, Y ) → true
leq(s(X), Y ) → leqS(X, Y )

39

leqS(X, 0) → f alse
leqS(X, s(Y )) → leq(X, Y )

As happened with (1’), the derivation
let U = f (Y ) in leq(X, U )
let U = 0 in leqS(Z, U )

l
l

[X/s(Z)] let

 leqS(Z, 0)

U = f (Y ) in leqS(Z, U )
l
 f alse

l

[Y /0]

gets rid of redundant solutions.
To which extent do our results guarantee the adequateness of the adaptation
to let-narrowing of these strategies or others that could be defined? Certainly any
strategy is sound for call-time choice semantics, because unrestricted l is already
sound (Theorem 14). This will be true also if the strategy uses derived rules in
the sense of Section 5. With respect to completeness, we know that the space
of let-narrowing derivations is complete wrt. let-rewriting (Theorem 15). But this
does not imply the completeness of the strategy, which in general will determine
a smaller narrowing space. Therefore completeness of the strategy must be proved
independently. Such a proof may use semantic methods (i.e., prove completeness
wrt. CRWL-semantics) or operational methods (i.e., prove completeness wrt. →l derivations). We will not go deeper into the issue of strategies.
7 Let-rewriting versus classical term rewriting
In this section we examine the relationship between let-rewriting and ordinary term
rewriting, with the focus put in the set of c-terms reachable by rewriting with each
of these relations. As term rewriting is not able to handle expressions with letbindings, during this section we assume that all considered programs do not have
let-bindings in the right-hand side of its rules.
We will first prove in Section 7.1 that let-rewriting is sound with respect to
term rewriting, in the sense that any c-term that can be reached by a let-rewriting
derivation from a given expression can also be reached by a term rewriting derivation starting from the same expression. As we know, completeness does not hold
in general because run-time choice computes more values than call-time choice for
arbitrary programs. However, we will be able to prove completeness of let-rewriting
wrt. term rewriting for the class of deterministic programs, a notion close to confluence that will be defined in Section 7.2. Finally, we will conclude in Section 7.3 with
a comparison between let-narrowing and narrowing, that will follow easily from the
results in previous subsections and the adequacy of let-narrowing to let-rewriting.
Thanks to the strong equivalence between CRWL and let-rewriting we can choose
the most appropriate point of view for each of the two goals (soundness and completeness): we will use let-rewriting for proving soundness, and CRWL for defining
the property of determinism and proving that, under determinism, completeness of
let-rewriting wrt. term rewriting also holds.
7.1 Soundness of let-rewriting wrt. classical term rewriting
In order to relate let-rewriting to term rewriting, we first need to find a way for
term rewriting to cope with let-bindings, which are not supported by its syntax,

40

López-Fraguas et al.

that is only able to handle expressions from Exp. Therefore, we define the following
syntactic transformation from LExp into Exp that takes care of removing the let
constructions, thus losing the sharing information they provide.
Definition 9 (Let-binding elimination transformation)
Given e ∈ LExp we define its transformation into a let-free expression eb ∈ Exp as:
b =def X
X
h(e1\
, . . . , en ) =def h(eb1 , . . . , ec
n)
let X \
= e1 in e2 =def eb2 [X/eb1 ]
Note that eb ≡ e for any e ∈ Exp.
We will need also the following auxiliary lemma showing the interaction between
term rewriting derivations and substitution application.
Lemma 12 (Copy lemma)
For all e, e1 , e2 ∈ Exp, X ∈ V:
i) e1 → e2 implies e[X/e1 ] →∗ e[X/e2 ].
ii) e1 →∗ e2 implies e[X/e1 ] →∗ e[X/e2 ].
Note how in i), each of the different copies of e1 introduced in e by the substitution
has to be reduced to e2 in a different term rewriting step in order to reach the
expression e[X/e2 ].
Using this lemma we can get a first soundness result stating that the result of
one let-rewriting step can also be obtained in zero or more steps of ordinary rewriting, after erasing the sharing information by means of the let-binding elimination
transformation.
Lemma 13 (One-Step Soundness of let-rewriting wrt. term rewriting)
For all e, e0 ∈ LExp we have that e →l e0 implies eb →∗ eb0 .
The remaining soundness results follow easily from this lemma. The first one
shows how we can mimic let-rewriting with term rewriting through the let-binding
elimination transformation. But then, as eb ≡ e for any e ∈ Exp, we conclude that
for let-free expressions let-rewriting is a subrelation of term rewriting.
Theorem 17 (Soundness of let-rewriting wrt. term rewriting)
∗
For any e, e0 ∈ LExp we have that e →l e0 implies eb →∗ eb0 . As a consequence, if
∗
∗
e, e0 ∈ Exp then e →l e0 implies e →∗ e0 , i.e., (→l ∩ (Exp × Exp)) ⊆ →∗ .
Proof
The first part follows from an immediate induction on the length of the let-derivation,
using Lemma 13 for the inductive step. The rest is obvious taking into account that
e ≡ eb and e0 ≡ eb0 when e, e0 ∈ Exp.
To conclude this part, we can combine this last result with the equivalence of
CRWL and let-rewriting, thus getting the following soundness result for CRWL
with respect to term rewriting.

Theory and Practice of Logic Programming

41

Theorem 18 (Soundness of CRWL wrt. term rewriting)
For any e ∈ Exp, t ∈ CT erm⊥ , if e _ t then there exists e0 ∈ Exp such that
e →∗ e0 and t v |e0 |.

Proof
∗
Assume e _ t. By Theorem 11, there exists e00 ∈ LExp such that e →l e00 and
t v |e00 |. Then, by Theorem 17, we have eb →∗ eb00 . As e ∈ Exp, we have e ≡ eb and
we can choose e0 ≡ eb00 ∈ Exp so we get e →∗ e0 . It is easy to check that |e00 | = |eb00 |
and then we have t v |e00 | = |eb00 | = |e0 |.

7.2 Completeness of CRWL wrt. classical term rewriting
We prove here the completeness of the CRWL framework wrt. term rewriting for
the class of CRWL-deterministic programs, which are defined as follows.
Definition 10 (CRWL-deterministic program)
A program P is CRWL-deterministic iff for any expression e ∈ Exp⊥ its denotation
[[e]]P is a directed set. In other words, iff for all e ∈ Exp⊥ and t1 , t2 ∈ [[e]]P , there
exists t3 ∈ [[e]]P with t1 v t3 and t2 v t3 .
Thanks to the equivalence of CRWL and let-rewriting, it is easy to characterize
CRWL-determinism also in terms of let-rewriting derivations.
Lemma 14
A program P is CRWL-deterministic iff for any e ∈ Exp, e0 , e00 ∈ LExp with
∗
∗
∗
P ` e →l e0 and P ` e →l e00 there exists e000 ∈ LExp such that P ` e →l e000
and |e000 | w |e0 |, |e000 | w |e00 |.

Proof
For the left to right implication, assume a CRWL-deterministic program P and
∗
∗
e ∈ Exp, e0 , e00 ∈ LExp with e →l e0 and e →l e00 . By part iii) of Theorem 10
we have |e0 |, |e00 | ∈ [[e]] and then by Definition 10 there exists t ∈ [[e]] such that
|e0 |, |e00 | v t. Now, by part iii) of Theorem 11 there exists e000 ∈ LExp such that
∗
e →l e000 and t v |e000 |, so we have |e0 |, |e00 | v t v |e000 | as expected.
Regarding the converse implication, assume e ∈ Exp with t1 , t2 ∈ [[e]]. By part
∗
∗
iii) of Theorem 11 there exist e0 , e00 ∈ LExp such that e →l e0 , e →l e00 and
∗
t1 v |e0 |, t2 v |e00 |. Then by hypothesis there exists e000 ∈ LExp such that e →l e000
and |e0 |, |e00 | v |e000 |. Now, by part iii) of Theorem 10 we have |e000 | ∈ [[e]] and this
|e000 | is the t3 of Definition 10 we are looking for, i.e., t3 ∈ [[e]] and t1 , t2 v t3 .
CRWL-determinism is intuitively close to confluence of term rewriting, but these
two properties are not equivalent, as shown by the following example of a CRWLdeterministic but not confluent program.

42

López-Fraguas et al.

Example 7
Consider the program P given by the rules
f →a

f → loop

loop → loop

where a is a constructor. It is clear that →P is not confluent (f can be reduced
to a and loop, which cannot be joined into a common reduct), but it is CRWLdeterministic, since [[f ]]P = {⊥, a}, [[loop]]P = {⊥} and [[a]]P = {⊥, a}, which are
all directed sets.
We conjecture that the reverse implication is true, i.e., that confluence of term
rewriting implies CRWL-determinism. Nevertheless, a precise proof for this fact
seems surprisingly complicated and we have not yet completed it.
A key ingredient in our completeness proof is the notion of CRWL-denotation of
a substitution, which is the set of c-substitutions whose range can be obtained by
CRWL-reduction over the range of the starting expression.
Definition 11 (CRWL-denotation for a substitution)
Given a program P, the CRWL-denotation of a σ ∈ Subst⊥ is defined as:
[[σ]]P
CRWL = {θ ∈ CSubst⊥ | ∀X ∈ V, P `CRWL σ(X) _ θ(X)}
We will usually omit the subscript CRWL and/or the superscript P when implied
by the context.
Any substitution θ in the denotation of some substitution σ contains less information than σ, because it only holds in its range a finite part of the possibly infinite
denotation of the expressions in the range of σ. We formalize this property in the
following result.
Proposition 10
For all σ ∈ Subst⊥ , θ ∈ [[σ]], we have that θ E σ.
Besides, we will use the notion of deterministic substitution, which is a substitution with only deterministic expressions in its range.
Definition 12 (Deterministic substitution)
The set DSubst⊥ of deterministic substitutions for a given program P is defined as
DSubst⊥ = {σ ∈ Subst⊥ | ∀X ∈ dom(σ).[[σ(X)]] is a directed set}
Then CSubst⊥ ⊆ DSubst⊥ , and under any program ∀σ ∈ Subst⊥ .[[σ]] ⊆ CSubst⊥ ⊆
DSubst⊥ . Note that the determinism of substitutions depends on the program,
which gives meaning to the functions in its range. Obviously if a program is deterministic then Subst⊥ = DSubst⊥ .
A good thing about deterministic substitutions is that their denotation is always
a directed set.

Theory and Practice of Logic Programming

43

Proposition 11
For all σ ∈ DSusbt⊥ , [[σ]] is a directed set.
But the fundamental property of deterministic substitutions is that, for any
CRWL-statement starting from an instance of an expression that has been constructed using a deterministic substitution, there is another CRWL-statement to
the same value from another instance of the same expression that now has been
built using a c-substitution taken from the denotation of the starting substitution.
This property is a direct consequence of Proposition 11.
Lemma 15
For all σ ∈ DSusbt⊥ , e ∈ Exp⊥ , t ∈ CT erm⊥ ,
if eσ _ t then ∃θ ∈ [[σ]] such that eθ _ t
Proof (sketch)
We proceed by a case distinction over e. If e ≡ X ∈ dom(σ) then we have eσ ≡
σ(X) _ t, and we can define

if Y ≡ X
 t
θ(Y ) =
⊥ if Y ∈ dom(σ) \ {X}

Y
otherwise
Then it is easy to check that θ ∈ [[σ]] and besides eθ ≡ θ(X) ≡ t _ t by Lemma 5,
so we are done. If e ≡ X ∈ V \dom(σ) then we have eσ ≡ σ(X) ≡ X _ t, and given
Y = dom(σ) it is easy to check that [Y / ⊥] ∈ [[σ]], and besides e[Y / ⊥] ≡ X _ t by
hypothesis.
Finally if e 6∈ V we proceed by induction on the structure of the proof for eσ _ t.
The interesting cases are those for (DC) and (OR) where we use that σ ∈ DSusbt⊥ ,
so by Proposition 11 its denotation is directed. Then there must exist some θ ∈
[[σ]] which is greater than each of the θi obtained by induction hypothesis over
the premises of the starting CRWL-proof for eσ _ t. Using the monotonicity of
Proposition 5 we can prove eθ _ t, which also holds for CRWL, by Theorem 4 (see
Appendix A, page 88 for details).
Now we are finally ready to prove our first completeness result of CRWL wrt.
term rewriting, for deterministic programs.
Lemma 16 (Completeness lemma for CRWL wrt. term rewriting)
Let P be a CRWL-deterministic program, and e, e0 ∈ Exp. Then:
e →∗ e0 implies [[e0 ]] ⊆ [[e]]
Proof
We can just prove this result for e → e0 , then its extension for an arbitrary number
of term rewriting steps holds by a simple induction on the length of the term
rewriting derivation, using transitivity of ⊆.
Assume e → e0 , then the step must be of the shape e ≡ C[f (p)σ] → C[rσ] ≡ e0 for
some program rule (f (p) → r) ∈ P, σ ∈ Subst. First, let us focus on the case for

44

López-Fraguas et al.

C = [ ], and then assume some t ∈ CT erm⊥ such that P `CRWL e0 ≡ rσ _ t. As P
is deterministic then σ ∈ DSubst⊥ , therefore by Lemma 15 there must exist some
θ ∈ [[σ]] such that P `CRWL rθ _ t. But then we can use θ to build the following
CRWL-proof.
. . . pi θ _ pi θ . . . rθ _ t
OR
f (p)θ _ t

where for each pi ∈ p we have P `CRWL pi θ _ pi θ by Lemma 5, as pi ∈ CT erm
because P is a constructor system, and so pi θ ∈ CT erm⊥ , as θ ∈ [[σ]] ⊆ CSubst⊥ .
But we also have θ E σ by Proposition 10, therefore by applying the monotonicity
for substitutions from Proposition 5 —which also holds for CRWL, by Theorem
4— we get P `CRWL e ≡ f (p)σ _ t. Hence [[e0 ]] = [[rσ]] ⊆ [[f (p)σ]] = [[e]].
Finally, we can generalize this result to arbitrary contexts by using the compositionality of CRWL from Theorem 1. Given a term rewriting step e ≡ C[f (p)σ] →
C[rσ] ≡ e0 then by the proof for C = [ ] we get [[rσ]] ⊆ [[f (p)σ]], but then
[[e0 ]] = [[C[rσ]]]
S
=
[[C[t]]]
t∈[[rσ]]
S
[[C[t]]]
⊆

by Theorem 1
as [[rσ]] ⊆ [[f (p)σ]]

t∈[[f (p)σ]]

= [[C[f (p)σ]]] = [[e]]

by Theorem 1

The previous lemma, together with the equivalence of CRWL and let-rewriting
given by Theorem 12 and Theorem 4, allows us to obtain a strong relationships between term rewriting, let-rewriting and CRWL, for the class of CRWL-deterministic
programs.
Theorem 19
Let P be a CRWL-deterministic program, and e, e0 ∈ Exp, t ∈ CT erm. Then:
∗

a) e →∗ e0 implies e →l e00 for some e00 ∈ LExp with |e00 | w |e0 |.
∗
b) e →∗ t iff e →l t iff P `CRWL e _ t.
∗

Notice that in part a) we cannot ensure e →∗ e0 implies e →l e0 , because term
rewriting can reach some intermediate expressions not reachable by let-rewriting.
For instance, given the deterministic program with the rules g → a and f (x) →
∗
c(x, x), we have f (g) →∗ c(g, a), but f (g) 6→l c(g, a). Still, parts a) is a strong completeness results for let-rewriting wrt. term rewriting for deterministic programs,
since it says that the outer constructed part obtained in a rewriting derivation can
be also obtained or even refined in a let-rewriting derivation. Combined with Theorem 17, part a) expresses a kind of equivalence between let-rewriting and term
rewriting, valid for general derivations, even non-terminating ones. For derivations
reaching a constructor term (not further reducible), part b) gives an even stronger
equivalence result.

Theory and Practice of Logic Programming

45

7.3 Let-narrowing versus narrowing for deterministic systems
Joining the results of the previous section with the adequacy of let-narrowing to
let-rewriting, we can easily establish some relationships between let-narrowing and
ordinary term rewriting/narrowing, summarized in the following result.
Theorem 20
For any program P, e ∈ Exp, θ ∈ CSubst and t ∈ CT erm:
∗

a) If e lθ t then eθ →∗ t.
b) If in addition P is CRWL-deterministic, then:
b1 ) If eθ →∗ t then ∃t0 ∈ CT erm, σ, θ0 ∈ CSubst such that e
and σθ0 = θ[var(e)].
b2 ) If e ∗θ t, the same conclusion of (b1 ) holds.

l∗
σ

t0 , t0 θ0 ≡ t

l
Part a) expresses soundness of
wrt. term rewriting, and part b) is a coml
pleteness result for
wrt. term rewriting/narrowing, for the class of deterministic
programs.

Proof
Part a) follows from soundness of let-narrowing wrt. let-rewriting (Theorem 14)
and soundness of let-rewriting wrt. term rewriting of Theorem 19.
For part b1 ), for let-narrowing, assume eθ →∗ t. By the completeness of letrewriting wrt. term rewriting for deterministic programs (Theorem 19), we have
∗
eθ →l t, and then by the completeness of let-narrowing wrt. let-rewriting (Theorem
∗
15), there exists a narrowing derivation e lσ t0 with t0 θ0 = t and σθ0 = θ[F V (e)].
But notice that for e ∈ Exp, the sets F V (e) and var(e) coincide, and the proof is
finished.
Finally, b2 ) follows simply from soundness of (ordinary) narrowing wrt. term
rewriting and b1 ).

8 Conclusions
This paper contains a thorough presentation of the theory of first order let-rewriting
and let-narrowing for constructor-based term rewriting systems. These two relations
are simple notions of one-step reduction that express sharing as it is required by
the call-time choice semantics of non-determinism adopted in the functional logic
programming paradigm. In a broad sense, let-rewriting and let-narrowing can be
seen as particular syntactical presentations of term graph rewriting and narrowing.
However, keeping our formalisms very close to the syntax and basic notions of
term rewriting systems (terms, substitutions, syntactic unification,. . . ) has been an
essential aid in establishing strong equivalence results with respect to the CRWLframework —a well-established realization of call-time choice semantics—, which
was one of the main aims of the paper.
Along the way of proving such equivalence we have developed powerful semantic tools that are interesting in themselves. Most remarkably, the CRWLlet -logic, a

46

López-Fraguas et al.

conservative extension of CRWL that deals with let-bindings, and the notion of hypersemantics of expressions and contexts, for which we prove deep compositionality
results not easily achievable by thinking directly in terms of reduction sequences.
We have shown in several places the methodological power of having provably
equivalent reduction-based and logic-based semantics. In some occasions, we have
used the properties of the CRWL-semantics to investigate interesting aspects of
reductions, as replaceability conditions or derived operational rules, like bubbling.
In others, we have followed the converse way. For instance, by transforming letrewriting reductions into ordinary term rewriting reductions, we easily concluded
that let-rewriting (call-time choice) provides less computed values than term rewriting (run-time choice). By using again semantic methods, we proved the opposite
inclusion for deterministic programs, obtaining for such programs an equivalence
result of let-rewriting and term rewriting.
In our opinion, the different pieces of this work can be used separately for different purposes. The CRWLlet -logic provides a denotational semantics reflecting
call-time choice for programs making use of local bindings. The let-rewriting and
let-narrowing relations provide clear and abstract descriptions of how computations
respecting call-time choice can proceed. They can be useful to explain basic operational aspects of functional logic languages to students or novice programmers, for
instance. They have been used also as underlying formalisms to investigate other
aspects of functional logic programming that need a clear notion of reduction; for
instance, when proving essential properties of type systems, like subject reduction or
progress. In addition, all the pieces are interconnected by strong theoretical results,
which may be useful depending on the pursued goal.
Just like classical term rewriting and narrowing, the let-rewriting and narrowing
relations define too broad computation spaces as to be adopted directly as concrete operational procedures of a programming language. To that purpose, they
should be accompanied by a strategy that selects only certain computations. In
this paper we have only given an example-driven discussion of strategies. We are
quite confident that some known on-demand evaluation strategies, like lazy, needed
or natural rewriting/narrowing, can be adapted to our formal setting. In (Riesco
and Rodrı́guez-Hortalá 2010; Sánchez-Hernández 2011) we work out in more detail
two concrete on-demand strategies for slight variants of let-rewriting and narrowing
formalisms.
A subject of future work that might be of interest to the functional logic community is that of completing the comparison of different formalisms proposed in the
field to capture call-time choice semantics: CRWL, admissible term graph rewriting/narrowing, natural semantics à la Launchbury, and let-rewriting/narrowing.
Proving their equivalence would greatly enrich the set of tools available to the
functional logic programming theoretician, since any known or future result obtained for one of the approaches could be applied to the rest on a sound technical
basis.

Theory and Practice of Logic Programming

47

References
Albert, E., Hanus, M., Huch, F., Oliver, J., and Vidal, G. 2005. Operational semantics for declarative multi-paradigm languages. Journal of Symbolic Computation 40, 1,
795–829.
Alpuente, M., Falaschi, M., Iranzo, P. J., and Vidal, G. 2003. Uniform lazy narrowing. Journal of Logig and Computation 13, 2, 287–312.
Antoy, S. 2005. Evaluation strategies for functional logic programming. Journal of
Symbolic Computation 40, 1, 875–903.
Antoy, S., Brown, D., and Chiang, S. 2006. On the correctness of bubbling. In 17th
International Conference on Rewriting Techniques and Applications (RTA’06). Springer
LNCS 4098, 35–49.
Antoy, S., Brown, D., and Chiang, S. 2007. Lazy context cloning for non-deterministic
graph rewriting. Electronic Notes in Theoretical Computer Science 176, 1, 3–23.
Antoy, S., Echahed, R., and Hanus, M. 1994. A needed narrowing strategy. In
21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
(POPL’94). ACM, 268–279.
Antoy, S., Echahed, R., and Hanus, M. 2000. A needed narrowing strategy. Journal
of the ACM 47, 4, 776–822.
Antoy, S. and Hanus, M. 2000. Compiling multi-paradigm declarative programs into
prolog. In 3rd International Workshop on Frontiers of Combining Systems (FroCoS’00).
Springer LNCS 1794, 171–185.
Antoy, S. and Hanus, M. 2006. Overlapping rules and logic variables in functional
logic programs. In 22nd International Conference on Logic Programming (ICLP’06).
Springer LNCS 4079, 87–101.
Ariola, Z. M. and Arvind. 1995. Properties of a first-order functional language with
sharing. Theoretical Computer Science 146, 1&2, 69–108.
Ariola, Z. M. and Felleisen, M. 1997. The call-by-need lambda calculus. Journal of
Functional Programming 7, 3, 265–301.
Ariola, Z. M., Felleisen, M., Maraist, J., Odersky, M., and Wadler, P. 1995.
The call-by-need lambda calculus. In 22nd ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (POPL’95). ACM, 233–246.
Baader, F. and Nipkow, T. 1998. Term Rewriting and All That. Cambridge University
Press.
Barendregt, H. P., Eekelen, M. C. J. D., Glauert, J. R. W., Kennaway, J. R.,
Plasmeijer, M. J., and Sleep, M. R. 1987. Term Graph Rewriting. In 1st Parallel
Architectures and Languages Europe (PARLE’87), Volume II. Springer LNCS 259, 141–
158.
Braßel, B. and Huch, F. 2007. On a tighter integration of functional and logic programming. In 5th Asian Symposium on Programming Languages and Systems (APLAS’07).
Springer LNCS 4807, 122–138.
Caballero, R. and Sánchez, J., Eds. 2006. TOY: A multiparadigm declarative language, version 2.2.3. Technical report, Universidad Complutense de Madrid.
Cheong, P. and Fribourg, L. 1993. Implementation of narrowing: The Prolog-based
approach. In Logic programming languages: constraints, functions, and objects. MIT
Press, 1–20.
DeGroot, D. and Lindstrom, G. e. 1986. Logic Programming, Functions, Relations,
and Equations. Prentice Hall.
Dios-Castro, J. and López-Fraguas, F. J. 2007. Extra variables can be eliminated
from functional logic programs. Electronic Notes in Theoretical Computer Science
188 188, 3–19.

48

López-Fraguas et al.

Echahed, R. and Janodet, J.-C. 1997. On constructor-based graph rewriting systems.
Research Report 985-I, IMAG.
Echahed, R. and Janodet, J.-C. 1998. Admissible graph rewriting and narrowing. In
Joint International Conference and Symposium on Logic Programming (JICSLP’96).
MIT Press, 325 – 340.
Escobar, S., Meseguer, J., and Thati, P. 2005. Natural narrowing for general term
rewriting systems. In 16th International Conference on Rewriting Techniques and Applications (RTA’05). Springer LNCS 3467, 279–293.
González-Moreno, J. C., Hortalá-González, T., López-Fraguas, F. J., and
Rodrı́guez-Artalejo, M. 1996. A rewriting logic for declarative programming. In
6th European Symposium on Programming (ESOP’96). Springer LNCS 1058, 156–172.
González-Moreno, J. C., Hortalá-González, T., López-Fraguas, F. J., and
Rodrı́guez-Artalejo, M. 1999. An approach to declarative programming based on a
rewriting logic. Journal of Logic Programming 40, 1, 47–87.
González-Moreno, J. C., Hortalá-González, T., and Rodrı́guez-Artalejo, M.
1997. A higher order rewriting logic for functional logic programming. In 14th International Conference on Logic Programming (ICLP’97). MIT Press, 153–167.
Hanus, M. 1994. The integration of functions into logic programming: From theory to
practice. Journal of Logic Programming 19&20, 583–628.
Hanus, M. 2007. Multi-paradigm declarative languages. In 23rd International Conference
on Logic Programming (ICLP’07). Springer LNCS 4670, 45–75.
Hanus, M., Kuchen, H., and Moreno-Navarro, J. J. 1995. Curry: A truly functional
logic language. In Workshop on Visions for the Future of Logic Programming (ILPS’95).
95–107.
Hanus, M., Ed. 2006. Curry: An integrated functional logic language (version 0.8.2).
Available at http://www.informatik.uni-kiel.de/~curry/report.html.
Hullot, J. 1980. Canonical forms and unification. In 5th Conference on Automated
Deduction (CADE’80). Springer LNCS 87, 318–334.
Hussmann, H. 1993. Non-Determinism in Algebraic Specifications and Algebraic Programs. Birkhäuser Verlag.
Kutzner, A. and Schmidt-Schauß, M. 1998. A non-deterministic call-by-need lambda
calculus. In 3th ACM SIGPLAN International Conference on Functional Programming
(ICFP’98). ACM SIGPLAN Notices 34(1), 324–335.
Launchbury, J. 1993. A natural semantics for lazy evaluation. In 20th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL’93). ACM, 144–
154.
Loogen, R., López-Fraguas, F. J., and Rodrı́guez-Artalejo, M. 1993. A demand
driven computation strategy for lazy narrowing. In 5th International Symposium on
Programming Language Implementation and Logic Programming (PLILP’93). Springer
LNCS 714, 184–200.
López-Fraguas, F. J., Martin-Martin, E., and Rodrı́guez-Hortalá, J. 2010a. Liberal typing for functional logic programs. In 8th Asian Symposium on Programming
Languages and Systems (APLAS’10). Springer LNCS 6461, 80–96.
López-Fraguas, F. J., Martin-Martin, E., and Rodrı́guez-Hortalá, J. 2010b. New
results on type systems for functional logic programming. In 18th International Workshop on Functional and (Constraint) Logic Programming (WFLP’09), Revised Selected
Papers. Springer LNCS 5979, 128–144.
López-Fraguas, F. J. and Rodrı́guez-Hortalá, J. 2010. The full abstraction problem
for higher order functional-logic programs. CoRR, arXiv:1002:1833.

Theory and Practice of Logic Programming

49

López-Fraguas, F. J., Rodrı́guez-Hortalá, J., and Sánchez-Hernández, J. 2007a.
Equivalence of two formal semantics for functional logic programs. Electronic Notes in
Theoretical Computer Science 188 188, 117–142.
López-Fraguas, F. J., Rodrı́guez-Hortalá, J., and Sánchez-Hernández, J. 2007b.
A simple rewrite notion for call-time choice semantics. In 9th International Conference
on Principles and Practice of Declarative Programming (PPDP’07). ACM, 197–208.
López-Fraguas, F. J., Rodrı́guez-Hortalá, J., and Sánchez-Hernández, J. 2008.
Rewriting and call-time choice: the HO case. In 9th International Symposium on Functional and Logic Programming (FLOPS’08). Springer LNCS 4989, 147–162.
López-Fraguas, F. J., Rodrı́guez-Hortalá, J., and Sánchez-Hernández, J. 2009a.
A flexible framework for programming with non-deterministic functions. In 2009 ACM
SIGPLAN Symposium on Partial Evaluation and Program Manipulation (PEPM’09).
ACM, 91–100.
López-Fraguas, F. J., Rodrı́guez-Hortalá, J., and Sánchez-Hernández, J. 2009b.
A fully abstract semantics for constructor based term rewriting systems. In 20th International Conference on Rewriting Techniques and Applications (RTA’09). Springer
LNCS 5595, 320–334.
López-Fraguas, F. J., Rodrı́guez-Hortalá, J., and Sánchez-Hernández, J. 2009c.
Narrowing for First Order Functional Logic Programs with Call-Time Choice Semantics. In 17th International Conference on Applications of Declarative Programming and
Knowledge Management (INAP’07) and 21st Workshop on (Constraint) Logic Programming (WLP’07), Revised Selected Papers. Springer LNAI 5437, 206–222.
López-Fraguas, F. J. and Sánchez-Hernández, J. 1999. T OY: A multiparadigm
declarative system. In 10th International Conference on Rewriting Techniques and Applications (RTA’99). Springer LNCS 1631, 244–247.
López-Fraguas, F. J. and Sánchez-Hernández, J. 2001. Functional logic programming with failure: A set-oriented view. In 8th International Conference on Logic for
Programming and Automated Reasoning (LPAR’01). Springer LNAI 2250, 455–469.
Maraist, J., Odersky, M., and Wadler, P. 1998. The call-by-need lambda calculus.
Journal of Functional Programming 8, 3, 275–317.
McCarthy, J. 1963. A Basis for a Mathematical Theory of Computation. In Computer
Programming and Formal Systems. North-Holland, 33–70.
Moreno-Navarro, J. J. and Rodrı́guez-Artalejo, M. 1992. Logic programming with
functions and predicates: The language Babel. Journal of Logic Programming 12, 189–
223.
Plump, D. 1998. Term graph rewriting. Report CSI-R9822, Computing Science Institute,
University of Nijmegen.
Plump, D. 2001. Essentials of term graph rewriting. Electronic Notes Theoretical Computer Science 51, 277–289.
Riesco, A. and Rodrı́guez-Hortalá, J. 2010. Programming with singular and plural
non-deterministic functions. In 2010 ACM SIGPLAN Workshop on Partial Evaluation
and Program Manipulation (PEPM’10). ACM, 83–92.
Rodrı́guez-Artalejo, M. 2001. Functional and constraint logic programming. In Revised
Lectures of the International Summer School CCL’99. Springer LNCS 2002, 202–270.
Sánchez-Hernández, J. 2004. Una aproximación al fallo constructivo en programación
declarativa multiparadigma. Ph.D. thesis, Departamento Sistemas Informáticos y Programación, Universidad Complutense de Madrid.
Sánchez-Hernández, J. 2011. Reduction strategies for rewriting with call-time choice.
In 11th Jornadas sobre Programación y Lenguajes (PROLE’11).

50

López-Fraguas et al.

Schmidt-Schauß, M. and Machkasova, E. 2008. A finite simulation method in a nondeterministic call-by-need lambda-calculus with letrec, constructors, and case. In 19th
International Conference on Rewriting Techniques and Applications (RTA’08). Springer
LNCS 5117, 321–335.
Sondergaard, H. and Sestoft, P. 1990. Referential transparency, definiteness and
unfoldability. Acta Informatica 27, 6, 505–517.
Søndergaard, H. and Sestoft, P. 1992. Non-determinism in functional languages.
The Computer Journal 35, 5, 514–523.
Vado-Vı́rseda, R. d. 2002. Estrategias de estrechamiento perezoso. Trabajo de Investigación de Tercer Ciclo, Dpto. de Sistemas Informáticos y Programación, Universidad
Complutense de Madrid.
Vado-Vı́rseda, R. d. 2003. A demand-driven narrowing calculus with overlapping definitional trees. In 5th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP’03). ACM, 213–227.
Zartmann, F. 1997. Denotational abstract interpretation of functional logic programs.
In 4th International Symposium on Static Analysis (SAS’97). Springer LNCS 1302,
141–159.

Appendix A Detailed proofs for the results
In the proofs we will use the usual notation for positions, subexpressions and
repacements from (Baader and Nipkow 1998). The set of positions of an expression
e ∈ Exp is a set O(e) of strings of positive integers defined as:
• If e ≡ X ∈ V, then O(e) = , where  is the empty string.
• If e ≡ h(e1 , . . . , en ) with h ∈ Σ, then
O(e) = {} ∪

n
[

{ip | p ∈ O(ei )}

i=1

The subexpression of e at position p ∈ O(e), denoted e|p , is defined as:
e|
h(e1 , . . . , en )|ip

=
=

e
ei |p

For a position p ∈ O(e), we define the replacement of the subexpression of e at
position p by e0 —denoted e[e0 ]p — as follows:
e[e0 ]
h(e1 , . . . , en )[e0 ]ip

= e0
= h(e1 , . . . , ei [e0 ]p , . . . , en )

When performing proofs by induction we will usually use IH to refer to the
induction hypothesis of the current induction. We will use an asterisk to denote the
use of a let-rewriting rule one or more times, as in (Flat*). We will also use the
following auxiliary results.
A.1 Lemmas
The following lemmas are used in the proofs for the results in the article. Most of
them are straightforwardly proved by induction, so we only detail the proof in the
interesting cases.

Theory and Practice of Logic Programming

51

Lemma 17
∀t ∈ CT erm⊥ . |t| = t.
Lemma 18
∀t ∈ CT erm⊥ . P `CRWLlet t _ t.
Lemma 19
Given θ, θ0 ∈ LSubst⊥ , e ∈ LExp⊥ , if θ v θ0 then eθ v eθ0 .
Lemma 20
Given θ ∈ LSubst⊥ , e, e0 ∈ LExp⊥ , if e v e0 then eθ v e0 θ.
Lemma 21
For every e, e0 ∈ LExp⊥ , C ∈ Cntxt, if |e| v |e0 | then |C[e]| v |C[e0 ]|.
Proof
We proceed by induction on the structure of C. The base case is straightforward
because of the hypothesis. For the Inductive Step we have:
• C ≡ h(. . . , C 0 , . . .). Directly by IH.
• C ≡ let X = C 0 in e1 , so C[e] ≡ let X = C 0 [e] in e1 . Then:
|C[e]| = |let X = C 0 [e] in e1 | = |e1 |[X/|C 0 [e]|]
vIH (∗) |e1 |[X/|C 0 [e0 ]|] = |let X = C 0 [e0 ] in e1 | = |C[e0 ]|
(∗) By IH we have |C 0 [e]| v |C 0 [e0 ]|, therefore [X/|C 0 [e]|] v [X/|C 0 [e0 ]|]. Finally, by
Lemma 19, |e1 |[X/|C 0 [e]|] v |e1 |[X/|C 0 [e0 ]|].
• C ≡ let X = e1 in C 0 . Similar to the previous case but using Lemma 20 to obtain
|C 0 [e]| [X/|e1 |] v |C 0 [e0 ]|[X/|e1 |] from the IH |C 0 [e]| v |C 0 [e0 ]|.

Lemma 22
If |e| = |e0 | then |C[e]| = |C[e0 ]|
Proof
Since v is a partial order, we know by reflexivity that |e| v |e0 | and |e0 | v |e|. Then
by Lemma 21 we have |C[e]| v |C[e0 ]| and |C[e0 ]| v |C[e]|. Finally, by antisymmetry
of the partial order v we have that |C[e]| = |C[e0 ]|.
Lemma 23
For all e1 , e2 ∈ LExp, X ∈ V, |e1 [X/e2 ]| ≡ |e1 |[X/|e2 |]

52

López-Fraguas et al.

Proof
By induction on the structure of e1 . The most interesting case is when e1 ≡ let Y =
s1 in s2 . By the variable convention Y 6∈ dom([X/e2 ]) and Y 6∈ vran([X/e2 ]), so:
|e1 [X/e2 ]| ≡ |let Y = s1 [X/e2 ] in s2 [X/e2 ]|
≡ |s2 [X/e2 ]|[Y /|s1 [X/e2 ]|]
≡IH |s2 |[X/|e2 |][Y /(|s1 |[X/|e2 |])]
≡ |s2 |[Y /|s1 |][X/|e2 |]
≡ |let Y = s1 in s2 |[X/|e2 |] ≡ |e1 |[X/|e2 |]

(*)

(*) Using Lemma 1 with the matching [e/|s2 |, θ/[X/|e2 |], X/Y, e0 /|s1 |].
Lemma 24
Given θ ∈ LSubst⊥ , e, e0 ∈ LExp⊥ , if e v e0 then eθ v e0 θ.
Lemma 25
For every σ ∈ LSubst⊥ , C ∈ Cntxt and e ∈ LExp⊥ such that (dom(σ) ∪ vran(σ)) ∩
BV (C) = ∅ we have that (C[e])σ ≡ Cσ[eσ].
Proof
By induction on the structure of C. The most interesting cases are those concerning
let-expressions:
• C ≡ let X = C 0 in e1 : therefore C[e] ≡ let X = C 0 [e] in e1 . Then
(∗)

(C[e])σ ≡ let X = (C 0 [e])σ in e1 σ ≡IH let X = C 0 σ[eσ] in e1 σ
≡ (let X = (C 0 [])σ in e1 σ)[eσ] ≡(∗∗) ((let X = C 0 [] in e1 )σ)[eσ] ≡ Cσ[eσ]
(∗): by definition BV (let X = C 0 in e) = BV (C 0 ), so (dom(σ)∪vran(σ))∩BV (C) =
∅ = (dom(σ) ∪ vran(σ)) ∩ BV (C 0 ).
(∗∗): we can apply the last step because by hypothesis we can assure that we do
not need any renaming to apply (let X = C 0 [] in e1 )σ.
• C ≡ let X = e1 in C 0 : therefore C[e] ≡ let X = e1 in C 0 [e]. Then
(C[e])σ ≡ let X = e1 σ in (C 0 [e])σ ≡IH let X = e1 σ in C 0 σ[eσ]
≡ (let X = e1 σ in (C 0 [])σ)[eσ] ≡(∗) ((let X = e1 in C 0 [])σ)[eσ] ≡ Cσ[eσ]
(∗): we can apply the last step because by hypothesis we can assure that we do not
need any renaming to apply (let X = e1 in C 0 [])σ.

Lemma 26
For any e ∈ Exp⊥ , t ∈ CT erm⊥ and program P, if P ` e _ t then there is a
derivation for P ` e _ t in which every free variable used belongs to F V (e _ t).
Proof
A simple extension of the proof in (Dios-Castro and López-Fraguas 2007).

Theory and Practice of Logic Programming

53

Lemma 27
For every CRWLlet derivation e _ t there exists e0 ∈ LExp⊥ which is syntactically
equivalent to e module α-conversion, and a CRW Llet derivation for e0 _ t such
that if B is the set of bound variables used in e0 _ t and E is the set of free variables
used in the instantiation of extra variables in e0 _ t then B ∩ (E ∪ var(t)) = ∅.
Proof
By Lemma 26, if F is the set of free variables used in e0 _ t, then F ⊆ F V (e0 _ t),
in fact F = F V (e0 _ t), as F V (e0 ) and F V (t) are used in the top derivation of the
derivation tree for e0 _ t. As by definition E ∪ var(t) ⊆ F, if we prove B ∩ F = ∅
then B ∩ (E ∪ var(t)) = ∅ is a trivial consequence. To prove that we will prove that
for every a ∈ LExp⊥ used in the derivation for e0 _ t we have BV (a) ∩ F V (a) = ∅.
We can build e0 using α-conversion to ensure that BV (e0 )∩F V (e0 ) = ∅. This can be
easily maintained as an invariant during the derivation, as the new let-bindings that
appear during the derivation are those introduced in the instances of the rule used
during the OR steps, and be can ensure by α-conversion that BV (a) ∩ F V (a) = ∅
for these instances too, as α-conversion leaves the hypersemantics untouched.

A.2 Proofs for Section 2.2
Theorem 1 (Compositionality of CRWL)
For any C ∈ Cntxt, e, e0 ∈ Exp⊥
[[C[e]]] =

[

[[C[t]]]

t∈[[e]]

As a consequence: [[e]] = [[e0 ]] ⇔ ∀C ∈ Cntxt.[[C[e]]] = [[C[e0 ]]]
Proof
We prove that C[e] _ t ⇔ ∃s ∈ CT erm⊥ such that e _ s and C[s] _ t.
⇒) Induction on the size of the proof for C[e] _ t.
Base case The base case only allows the proofs C[e] _ ⊥ using (B), C[e] ≡ X _
X using (RR) and C[e] ≡ c _ c with c ∈ CS using (DC), that are clear. When
C = [ ] the proof is trivial with s = t and using Lemma 18.
Inductive step Direct application of the IH.

⇐) By induction on the size of the proof for C[s] _ t
Base case The base case only allows the proofs C[s] _ ⊥, C[s] ≡ X _ X and
C[s] ≡ c _ c with c ∈ CS, that are clear. When C = [ ] we have that ∃s ∈ CT erm⊥
such that e _ s and s _ t. Since s _ t by Lemma 5 we have t v s, and using
Proposition 3 e _ t —as e v e because v is a partial order.
Inductive step Direct application of the IH.

54

López-Fraguas et al.
A.3 Proofs for Section 3

Theorem 3
Let P be a CRWL-program, e ∈ Exp⊥ and t ∈ CT erm⊥ . Then:
P `CRWL e _ t iff e ∗P t
Proof
It is easy to see that ∗ coincides with the relation defined by the BRC-proof
calculus of (González-Moreno et al. 1999), that is, P `BRC e _ e0 ↔ e ∗ e0 .
But in that paper it is proved that BRC-derivability and CRWL-derivability (called
there GORC-derivability) are equivalent.
A.4 Proofs for Section 4
Lemma 1 (Substitution lemma for let-expressions)
Let e, e0 ∈ LExp⊥ , θ ∈ Subst⊥ and X ∈ V such that X 6∈ dom(θ) ∪ vran(θ). Then:
(e[X/e0 ])θ ≡ eθ[X/e0 θ]
Proof
By induction over the structure of e. The most interesting cases are the base cases:
• e ≡ X: Then (e[X/e0 ])θ ≡ (X[X/e0 ])θ ≡ e0 θ ≡ X[X/e0 θ]
≡X6∈dom(θ) Xθ[X/e0 θ] ≡ eθ[X/e0 θ]
• e ≡ Y 6≡ X: Then (e[X/e0 t])θ ≡ (Y [X/e0 ])θ ≡ Y θ
≡X6∈ran(θ) Y θ[X/e0 θ] ≡ eθ[X/e0 θ]

A.5 Proofs for Section 4.1
Lemma 2 (Closedness under CSubst of let-rewriting)
n
n
For any e, e0 ∈ LExp, θ ∈ CSubst we have that e →l e0 implies eθ →l e0 θ.
Proof
We prove that e →l e0 implies eθ →l e0 θ by a case distinction over the rule of the
let-rewriting calculus applied:
(Fapp) Assume f (t1 , . . . , tn ) →l r, using (f (p1 , . . . , pn ) → e) ∈ P and σ ∈ CSubst
such that ∀i.pi σ = ti and eσ = r. But since σθ ∈ CSubst and ∀i.pi σθ = ti θ then
we can perform a (Fapp) step f (t1 , . . . , tn )θ ≡ f (t1 θ, . . . , tn θ) →l eσθ ≡ rθ.
(LetIn) Easily since X 6∈ dom(θ) because X is fresh.
(Bind) Assume let X = t in e →l e[X/t] and some θ ∈ CSubst. Then t ∈ CT erm
by the conditions of (Bind), hence tθ ∈ CT erm too and we can perform a (Bind)
step (let X = t in e)θ ≡ let X = tθ in eθ →l eθ[X/tθ]. Besides X 6∈ (dom(θ) ∪
vran(θ)) by the variable convention, and so eθ[X/tθ] ≡ e[X/t]θ by Lemma 1, so
are done.

Theory and Practice of Logic Programming

55

(Elim) Easily as X 6∈ F V (e2 θ) because X 6∈ vran(θ) by the variable convention.
(Flat) Similar to the previous case since Y 6∈ F V (e3 θ).
0
(Contx) Assume C[e] →l C[e0 ] because e →l e0 by one of the previous rules, and
some θ ∈ CSubst. Then we have already proved that eθ →l e0 θ. Besides by the
variable convention we have BV (C) ∩ (dom(θ) ∪ vran(θ)) = ∅, hence by Lemma
25 (C[e])θ ≡ Cθ[eθ]. Furthermore, if e →l e0 was a (Fapp) step using σ ∈ CSubst
to build the instance of the program rule (f (p)σ → rσ), then vran(σ|\var(p) ) ∩
BV (C) = ∅ by the conditions of (Contx), and therefore vran((σθ)|\var(p) ) ∩
BV (C) = ∅. But as σθ is the substitution used in the (Fapp) step eθ →l e0 θ,
then Cθ[eθ] →l Cθ[e0 θ] by (Contx). On the other hand, if e →l e0 was not a (Fapp)
step then Cθ[eθ] →l Cθ[e0 θ] too, and finally we can apply Lemma 25 again to get
Cθ[e0 θ] ≡ (C[e0 ])θ.
n

The proof for e →l e0 proceeds straightforwardly by induction on the length n
of the derivation.
Proposition 2 (Termination of →lnf )
Under any program we have that →lnf is terminating.
Proof
We define for any e ∈ LExp the size (k1 , k2 , k3 ), where
k1 ≡ number of subexpressions in e to which (LetIn) is applicable.
k2 ≡ number of lets in e.
k3 ≡ sum of the levels of nesting of all let-subexpressions in e.
Sizes are lexicographically ordered. We prove now that application of (LetIn),
(Bind), (Elim), (Flat) in any context (hence, also the application of (Contxt))
decreases the size, what proves termination of →lnf . The effect of each rule in the
size is summarized as follows (in each case, we stop at the decreasing component):
(LetIn):
(Bind):
(Elim):
(Flat):

(<, , )
(=, <, )
(≤, <, )
(=, =, <)

Lemma 3 (Peeling lemma)
For any e, e0 ∈ LExp if e ↓lnf e0 —i.e, e0 is a →lnf normal form for e— then e0
has the shape e0 ≡ let X = f (t) in e00 such that e00 ∈ V or e00 ≡ h(t0 ) with h ∈ Σ,
f ⊆ F S and t, t0 ⊆ CT erm.
Moreover if e ≡ h(e1 , . . . , en ) with h ∈ Σ, then
∗

e ≡ h(e1 , . . . , en ) →lnf let X = f (t) in h(t1 , . . . , tn ) ≡ e0
under the conditions above, and verifying also that ti ≡ ei whenever ei ∈ CT erm.
Proof
We prove it by contraposition: if an expression e does not have that shape, e is not
a →lnf normal form. We define the set of expressions which are not cterms as:

56

López-Fraguas et al.
nt ::=

c(. . . , nt, . . .)
| f (e)
| let X = e1 in e2
We also define the set of expressions which do not have the presented shape
recursively as:
ne ::= h(. . . , nt, . . .)
| let X = f (t) in ne
| let X = f (. . . , nt, . . .) in e
| let X = c(e) in e
| let X = (let Y = e0 in e00 ) in e
We prove by induction on the structure of an expression ne that it is always
possible to perform a →lnf step:
Base case:
• ne ≡ h(. . . , nt, . . .): there are various cases depending on nt:
— at some depth the non-cterm will contain a subexpression c0 (. . . , nt0 , . . .)
where nt0 is a function application f (e) or a let-rooted expression let X =
e1 in e2 . Therefore we can apply the rule (Contx) with (LetIn) in that position.
— f (e): we can apply the rule (LetIn) and perform the step
h(. . . , f (e), . . .) →lnf let X = f (e) in h(. . . , X, . . .)
— let X = e1 in e2 : the same as the previous case.
• let X = f (. . . , nt, . . .) in e: we can perform a (Contx) with (LetIn) step in f (. . . , nt, . . .)
as in the previous h(. . . , nt, . . .) case.
• let X = c(e) in e: if e are cterms t, then c(t) is a cterm and we can perform a
(Bind) step let X = c(t) in e →lnf e[X/c(t)]. If e contains any expression ne then
we can perform a (Contx) with (LetIn) step as in the previous h(. . . , nt, . . .) case.
• let X = (let Y = e0 in e00 ) in e: by the variable convention we can assume that
Y ∈
/ F V (e), so we can perform a (Flat) step let X = (let Y = e0 in e00 ) in e →lnf
let Y = e0 in let X = e00 in e.
Inductive step:
• let X = f (t) in ne: by IH we have that ne →lnf ne0 , so by the rule (Contx) we can
perform a step let X = f (t) in ne →lnf let X = f (t) in ne0 .
Notice that if the original expression has the shape h(e1 , . . . , en ) the arguments
ei which are cterms remain unchanged in the same position. The reason is that no
rule can affect them: the only rule applicable at the top is (LetIn), and it can not
place them in a let binding outside h(. . .); besides cterms do not match with the
left-hand side of any rule, so they can not be rewritten by any rule.
Lemma 4 (Growing of shells)
Under any program P and for any e, e0 ∈ LExp
∗

i) e →l e0 implies |e| v |e0 |
∗
ii) e →lnf e0 implies |e| ≡ |e0 |

Theory and Practice of Logic Programming

57

Proof for Lemma 4
We prove the lemma for one step (e →l e0 and e →lnf e0 ) by a case distinction over
the rule of the let-rewriting calculus applied:
(Fapp) The step is f (t1 , . . . , tn ) →l r, and |f (t1 , . . . , tn )| =⊥v |r|.
(LetIn) The equality |h(e1 , . . . , e, . . . , en )| = |let X = e in h(e1 , . . . , X, . . . , en )|
follows easily by a case distinction on h.
(Bind) The step is let X = t in e →l e[X/t], so |let X = t in e| = |e|[X/|t|] =
|e[X/t]| by Lemma 23.
(Elim) The step is let X = e1 in e2 →l e2 with X ∈
/ F V (e2 ). Then |let X =
e1 in e2 | = |e2 |[X/|e1 |] = |e2 |. Since the variables in the shell of an expression
is a subset of the variables in the original expression, we can conclude that if
X∈
/ F V (e2 ) then X ∈
/ F V (|e2 |).
(Flat) The step is let X = (let Y = e1 in e2 ) in e3 →l let Y = e1 in (let X =
e2 in e3 ) with Y ∈
/ F V (e3 ). By the variable convention we can assume that
X∈
/ F V (let Y = e1 in e2 ) —in particular X ∈
/ F V (e1 ). Then:
|let Y = e1 in (let X = e2 in e3 )|
= |let X = e2 in e3 |[Y /|e1 |]
= (|e3 |[X/|e2 |])[Y /|e1 |]
Notice that X ∈
/ dom([Y /|e1 |]) and X ∈
/ vran([Y /|e1 |]) = F V (|e1 |) because
X∈
/ F V (e1 ) and F V (|e1 |) ⊆ F V (e1 ). Therefore we can use Lemma 1:
(|e3 |[X/|e2 |])[Y /|e1 |]
= (|e3 |[Y /|e1 |])[X/(|e2 |[Y /|e1 |])]
By Lemma 1
= |e3 |[X/(|e2 |[Y /|e1 |])]
Y ∈
/ F V (e3 ), so Y ∈
/ F V (|e3 |)
= |e3 |[X/|let Y = e1 in e2 |]
= |let X = (let Y = e1 in e2 ) in e3 |
(Contx) The step is C[e] →l C[e0 ] with e →l e0 using any of the previous rules. Then
we have |e| v |e0 |, and by Lemma 21 C[e] v C[e0 ]. If the step is C[e] →lnf C[e0 ]
then rule (Fapp) has not been used in the reduction e →lnf e0 and by the previous
rules we have |e| = |e0 |. In that case by Lemma 22 we have C[e] = C[e0 ].
∗

∗

The extension of this result to →l and →lnf is a trivial induction over the number
of steps of the derivation.
A.6 Proofs for Section 4.2
Theorem 4 (CRWL vs. CRWLlet )
For any program P without lets, and any e ∈ Exp⊥ :
P
[[e]]P
CRWL = [[e]]CRWLlet

Proof
As any calculus rule from CRWL is also a rule from CRWLlet , then any CRWL-proof
is also a CRWLlet -proof, therefore [[e]]CRWL ⊆ [[e]]CRWLlet . For the other inclusion,
assume no let-binding is present in the program and let e ∈ Exp. Then, for any

58

López-Fraguas et al.

t ∈ CT erm⊥ , as the rules of CRWLlet do not introduce any let-binding and the rule
(Let) is only used for let-rooted expressions, the CRWLlet -proof P `CRWLlet e _ t
will be also a CRWL-proof for P `CRWLlet e _ t, hence [[e]]CRWLlet ⊆ [[e]]CRWL too.
The following Lemma is used to prove point iii) of Lemma 5. Notice that this
Lemma uses the notions of hyperdenotation ([[[ ]]]) and hyperinclusion (b) presented
in the final part of Section 4.2.
Lemma 28
Under any program P and for any e ∈ LExp⊥ we have that [[[e]]] b λθ.(|eθ|↑)↓.
Proof
We will use the following equivalent characterization of (e↑)↓:
(e↑)↓= {e1 ∈ LExp⊥ | ∃e2 ∈ LExp⊥ . e v e2 ∧ e1 v e2 }
note that {e2 ∈ LExp⊥ | e v e2 } is precisely the set e↑. Besides note that:
[[[e]]] b λθ.(|eθ|↑)↓
⇔ ∀θ ∈ CSubst⊥ . [[eθ]] ⊆ (|eθ|↑)↓
⇔ ∀θ ∈ CSubst⊥ , t ∈ CT erm⊥ . eθ _ t
⇒ t ∈ (|eθ|↑)↓
⇔ ∀θ ∈ CSubst⊥ , t ∈ CT erm⊥ . eθ _ t
⇒ ∃t0 ∈ CT erm⊥ . |eθ| v t0 ∧ t v t0
where t0 ∈ CT erm⊥ is implied by |eθ| v t0 . To prove this last formulation first
consider the case when t ≡⊥. Then we are done with t0 ≡ |eθ| because then |eθ| v
|eθ| ≡ t0 and t ≡⊥v |eθ| ≡ t0 .
For the other case we proceed by induction on the structure of e. Regarding the
base cases:
• If e ≡⊥ then t ≡⊥ and we are in the previous case.
• If e ≡ X ∈ V then eθ ≡ θ(X) _ t, and as θ ∈ CSubst⊥ then θ(X) ∈ CT erm⊥
which implies t v θ(X) by Lemma 5. But then we can take t0 ≡ θ(X) for which
t v θ(X) ≡ t0 and |eθ| ≡ |θ(X)| ≡ θ(X) —by Lemma 17 since θ(X) ∈ CT erm⊥ —,
and θ(X) v θ(X) ≡ t0 .
• If e ≡ c ∈ DC then either t ≡⊥ and we are in the previous case, or t ≡ c. But then
we can take t0 ≡ c for which |eθ| ≡ c v c ≡ t0 , and t ≡ c v c ≡ t0 .
• If e ≡ f ∈ F S then |eθ| ≡ |f | ≡⊥, and so |eθ| ↑= CT erm⊥ and (|eθ| ↑) ↓=
CT erm⊥ ⊇ [[eθ]], so we are done.
Concerning the inductive steps:
• If e ≡ f (e1 , . . . , en ) for f ∈ F S then |eθ| ≡⊥ and we proceed like in the case for
e ≡ f.
• If e ≡ c(e1 , . . . , en ) for c ∈ DC then either t ≡⊥ and we are in the previous case,
or t ≡ c(t1 , . . . , tn ) such that ∀i. ei θ _ ti . But then by IH we get ∀i. ∃t0i . |ei θ| v
t0i ∧ ti v t0i , so we can take t0 ≡ c(t01 , . . . , t0n ) for which |eθ| ≡ c(|e1 θ|, . . . , |en θ|) v
c(t01 , . . . , t0n ) ≡ t0 and t ≡ c(t1 , . . . , tn ) v c(t01 , . . . , t0n ) ≡ t0 .

Theory and Practice of Logic Programming

59

• If e ≡ let X = e1 in e2 then either t ≡⊥ and we are in the previous case, or we
have the following proof:
e1 θ _ t1 e2 θ[X/t1 ] _ t
Let
eθ ≡ let X = e1 θ in e2 θ _ t

Then by IH over e1 we get that ∃t01 . |e1 θ| v t01 ∧ t1 v t01 . Hence [X/t1 ] v [X/t01 ] so
by Proposition 5 we have that e2 θ[X/t1 ] _ t implies e2 θ[X/t01 ] _ t. But then we
can apply the IH over e2 with θ[X/t01 ] to get some t0 ∈ CT erm⊥ such that t v t0
and |e2 θ[X/t01 ]| v t0 , which implies:
t0 w |e2 θ[X/t01 ]|
≡ |e2 θ|[X/|t01 |]
by Lemma 23
≡ |e2 θ|[X/t01 ]
by Lemma 17 as t01 ∈ CT erm⊥
w |e2 θ|[X/|e1 θ|]
as |e1 θ| v t01
≡ |let X = e1 θ in e2 θ| ≡ |eθ|

Lemma 5
For any program e ∈ LExp⊥ , t, t0 ∈ CT erm⊥ :
1. t _ t0 iff t0 v t.
2. |e| ∈ [[e]].
3. [[e]] ⊆ (|e|↑)↓, where for a given E ⊆ LExp⊥ its upward closure is E↑= {e0 ∈
LExp⊥ | ∃e ∈ E. e v e0 }, its downward closure is E↓= {e0 ∈ LExp⊥ | ∃e ∈
E. e0 v e}, and those operators are overloaded for let-expressions as e↑= {e}↑
and e↓= {e}↓.
Proof
1. Easily by induction on the structure of t.
2. Straightforward by induction on the structure of e. In the case of let expressions,
the proof uses |e| ∈ CT erm⊥ and Proposition 4 in order to apply the CRWLlet rule
(Let).
3. By Lemma 28 we have that [[[e]]] b λθ.(|eθ|↑)↓. By definition of hyperinclusion —
Definition 8— we know that [[[e]]] ⊆ (λθ.(|eθ|↑)↓), so [[[e]]] = [[e]] ≡ [[e]] ⊆ (|e|↑)↓≡
(|e|↑)↓= (λθ.(|eθ|↑)↓).
Proposition 3 (Polarity of CRWLlet )
For any program e, e0 ∈ LExp⊥ , t, t0 ∈ CT erm⊥ , if e v e0 and t0 v t then e _ t
implies e0 _ t0 with a proof of the same size or smaller—where the size of a
CRWLlet -proof is measured as the number of rules of the calculus used in the
proof.
Proof
By induction on the size of the CRWL-derivation. All the cases are straightforward
except the (Let) rule:

60

López-Fraguas et al.

(Let) We have the derivation:
e1 _ t1 e2 [X/t1 ] _ t
(Let)
e ≡ let X = e1 in e2 _ t

Since e v e0 then e0 ≡ let X = e01 in e02 with e1 v e01 and e2 v e02 . As e1 v e01
and t1 v t1 —because v is reflexive— then by IH we have e01 _ t1 . We know
that e2 v e02 so by Lemma 24 we have e2 [X/t1 ] v e02 [X/t1 ] and by IH P `CRWLlet
e02 [X/t1 ] _ t0 such that t0 v t. Therefore:
e01 _ t1 e02 [X/t1 ] _ t0
(Let)
e0 ≡ let X = e01 in e02 _ t0

Proposition 4 (Closedness under c-substitutions)
For any e ∈ LExp⊥ , t ∈ CT erm⊥ , θ ∈ CSubst⊥ , t ∈ [[e]] implies tθ ∈ [[eθ]].
Proof
By induction on the size of the CRWLlet -proof. All the cases are straightforward
except the (Let) rule:
(Let) In this case the expression is e ≡ let X = e1 in e2 so we have a derivation
e1 _ t1 e2 [X/t1 ] _ t
(Let)
let X = e1 in e2 _ t
By IH we have that e1 θ _ t1 θ and (e2 [X/t1 ])θ _ tθ. By the variable convention
we assume that X ∈
/ dom(θ) ∪ vran(θ), so by Lemma 1 e2 [X/t1 ]θ ≡ e2 θ[X/t1 θ]
and e2 θ[X/t1 θ] _ tθ. Then we can construct the proof:
e1 θ _ t1 θ e2 θ[X/t1 θ] _ tθ
(Let)
let X = e1 θ in e2 θ _ tθ

Theorem 5 (Weak Compositionality of CRWLlet )
For any C ∈ Cntxt, e ∈ LExp⊥
[
[[C[e]]] =
[[C[t]]]
if BV (C) ∩ F V (e) = ∅
t∈[[e]]

As a consequence, [[let X = e1 in e2 ]] =

S

t1 ∈[[e1 ]] [[e2 [X/t1 ]]].

Proof
We prove that C[e] _ t ⇔ ∃s ∈ CT erm⊥ such that e _ s and C[s] _ t.
⇒) By induction on the size of the proof for C[e] _ t. The proof proceeds in a
similar way to the proof for Theorem 1, page 53, so we only have to prove the (Let)
case:
(Let) There are two cases depending on the context C (since C 6= [ ]):
• C ≡ let X = C 0 in e2 ) Straightforward.

Theory and Practice of Logic Programming

61

• C ≡ let X = e1 in C 0 ) The proof is
e1 _ t1 C 0 [e][X/t1 ] _ t
(Let)
C[e] ≡ let X = e1 in C 0 [e] _ t
We assume that X ∈
/ var(t1 ) by the variable convention, since X is bound in
C and we can rename it freely. Moreover, we assume also that X ∈
/ BV (C 0 )
because X is bound in C, so we could rename the bound occurrences in
C 0 . Therefore (dom([X/t1 ] ∪ vran([X/t1 ])) ∩ BV (C 0 ) = ∅ and C 0 [e][X/t1 ] ≡
(C 0 [X/t1 ])[e[X/t1 ]] by Lemma 25. Since BV (C) ∩ F V (e) = ∅ by the premise
and X ∈ BV (C) then X ∈
/ F V (e), so (C 0 [X/t1 ])[e[X/t1 ]] ≡ C 0 [X/t1 ][e].
Then by IH ∃s ∈ CT erm⊥ such that e _ s and C 0 [X/t1 ][s] _ t. Therefore
we can build:
e1 _ t1 C 0 [s][X/t1 ] ≡(∗) C 0 [X/t1 ][s] _ t
(Let)
C[s] ≡ let X = e1 in C 0 [s] _ t
(*) Using Lemma 25 as above and the assumption that X ∈
/ var(s) by the
variable convention, since X is bound in C and we can rename it freely.

⇐) By induction on the size of the proof for C[s] _ t. As before, the proof proceeds
in a similar way to the proof for Theorem 1, page 53, so we only have to prove the
(Let) case:
(Let) If we use (Let) then there are two cases depending on the context C (since
C 6= [ ]):
• C = let X = C 0 in e2 ) Straighforward.
• C = let X = e1 in C 0 ) then we have e _ s and
e1 _ t1 C 0 [s][X/t1 ] _ t
(Let)
C[s] ≡ let X = e1 in C 0 [s] _ t
By the same reasoning as in the second case of the (Let) rule of the ⇒)
part of this theorem, C 0 [s][X/t1 ] ≡ C 0 [X/t1 ][s]. Then by IH C 0 [X/t1 ][e] _ t.
Again by the same reasoning we have C 0 [e][X/t1 ] ≡ C 0 [X/t1 ][e], so we can
build the proof:
e1 _ t1 C 0 [e][X/t1 ] ≡ C 0 [X/t1 ][e] _ t
(Let)
C[e] ≡ let X = e1 in C 0 [e] _ t

This ends the proof of the main part of the theorem. With respect to the con-

62

López-Fraguas et al.

sequence [[let X = e1 in e2 ]]CRWLlet =

S

t1 ∈[[e1 ]]CRWLlet [[e2 [X/t1 ]]]CRWLlet

[[let X = e1 in e2 ]]CRWLlet
= [[(let X = [ ] in e2 )[e1 ]]]CRWLlet
S
=
[[let X = t1 in e2 ]]CRWLlet
t1 ∈[[e1 ]]CRWLlet
S
=
[[e2 [X/t1 ]]]CRWLlet

we have:

by Theorem 5
by Proposition 8

t1 ∈[[e1 ]]CRWLlet

In the last step we replace let X = t1 in e2 by e2 [X/t1 ] which is a (Bind) step of
→lnf , so by Proposition 8 it preserves the denotation.
For Proposition 5, in this Appendix we prove a generalization of the statement
appearing in Section 4.2 (page 21). However, it is easy to check that Proposition 5
in Section 4.2 follows easily from points 2 and 3 here.
Proposition 5 (Monotonicity for substitutions of CRWLlet )
For any program e ∈ LExp⊥ , t ∈ CT erm⊥ , σ, σ 0 ∈ LSubst⊥
1. If ∀X ∈ V, s ∈ CT erm⊥ given σ(X) _ s with size K we also have σ 0 (X) _ s
with size K 0 ≤ K, then eσ _ t with size L implies eσ 0 _ t with size L0 ≤ L.
2. If σ v σ 0 then eσ _ t implies eσ 0 _ t with a proof of the same size or smaller.
3. If σ E σ 0 then [[eσ]] ⊆ [[eσ 0 ]].
Proof
1. If e ≡ X ∈ V, assume Xσ _ t, then Xσ 0 _ t with a proof of the same size or
smaller, by hypothesis. Otherwise we proceed by induction on the structure of the
proof eσ _ t.
Base cases
(B) Then t ≡⊥ and eσ 0 _⊥ with a proof of size 1 just applying rule (B).
(RR) Then e ∈ V and we are in the previous case.
(DC) Then e ≡ c ∈ CS 0 , as e 6∈ V, hence eσ ≡ c ≡ eσ 0 and every proof for
eσ _ t is a proof for eσ 0 _ t.

Inductive steps

(DC) Then e ≡ c(e1 , . . . , en ), as e 6∈ V, and we have:
e1 σ _ t1 . . . e n σ _ tn
(DC)
eσ ≡ c(e1 σ, . . . , en σ) _ c(t1 , . . . , tn ) ≡ t

By IH or the proof of the other cases ∀i ∈ {1, . . . , n} we have ei σ 0 _ ti
with a proof of the same size or smaller, so we can built a proof for eσ 0 ≡
c(e1 σ 0 , . . . , en σ 0 ) _ c(t1 , . . . , tn ) ≡ t using (DC), with a size equal or smaller
than the size of the starting proof.
(OR) Similar to the previous case.
(Let) Then e ≡ let X = e1 in e2 , as e 6∈ V, and we have:
e1 σ _ t1 e2 σ[X/t1 ] _ t
(Let)
let X = e1 σ in e2 σ _ t
By IH we have e1 σ _ t1 . By the variable convention we assume that X ∈
/

Theory and Practice of Logic Programming

63

dom(σ) ∪ vran(σ) and X ∈
/ dom(σ 0 ) ∪ vran(σ 0 ). Then it is easy to check
that ∀Y ∈ V, s, t ∈ CT erm⊥ , given Y (σ[X/t]) _ s with size K we also have
Y (σ 0 [X/t]) _ s with size K 0 ≤ K. Then by IH we have e2 σ 0 [X/t1 ] _ t.
Therefore we can construct a proof with a size equal or smaller than the starting
one:
e1 σ 0 _ t1 e2 σ 0 [X/t1 ] _ t
(Let)
let X = e1 σ 0 in e2 σ 0 _ t
2. By induction on the size of the CRWLlet -proof. The cases for classical CRWL appear
in (Vado-Vı́rseda 2002), so we only have to prove the case for the (Let) rule:
(Let) In this case the expression is e ≡ let X = e1 in e2 so we have a proof
e1 σ _ t1 e2 σ[X/t1 ] _ t
(Let)
let X = e1 σ in e2 σ _ t
By IH we have that e1 σ _ t1 . By the variable convention we can assume that
BV (e) ∩ (dom(σ) ∪ vran(σ)) = ∅ and BV (e) ∩ (dom(σ 0 ) ∪ vran(σ 0 )) = ∅. With
the previous properties it is easy to see that σ[X/t1 ] v σ 0 [X/t1 ], so by IH
e2 σ 0 [X/t1 ] _ t. Therefore we can build the proof:
e1 σ 0 _ t1 e2 σ 0 [X/t1 ] _ t
(Let)
let X = e1 σ 0 in e2 σ 0 _ t

3. By induction on the structure of e:
e ≡ X ∈ V - In this case [[Xσ]]CRWLlet ⊆ [[Xσ 0 ]]CRWLlet because by the hypothesis
σ E σ0 .
e ≡ h(e1 , . . . , en ) - Applying Theorem 5 with C ≡ h([ ], e2 σ, . . . , en σ) we have
S
[[h(e1 σ, . . . , en σ)]]CRWLlet = [[C[e1 σ]]]CRWLlet =
[[C[t]]]CRWLlet because
t∈[[e1 σ]]CRWLlet

BV (C) = ∅. On the other hand, by Theorem 5 we also know that
[[h(e1 σ 0 , e2 σ, . . . , en σ)]]CRWLlet

= [[C[e1 σ 0 ]]]CRWLlet
S
=
[[C[t]]]CRWLlet
t∈[[e1 σ 0 ]]CRWLlet

Since by IH we have [[e1 σ]]CRWLlet ⊆ [[e1 σ 0 ]]CRWLlet it is easy to check that
[
[
[[C[t]]]CRWLlet ⊆
[[C[t]]]CRWLlet
t∈[[e1 σ]]CRWLlet

t∈[[e1 σ 0 ]]CRWLlet

so [[h(e1 σ, e2 σ, . . . , en σ)]]CRWLlet ⊆ [[h(e1 σ 0 , e2 σ, . . . , en σ)]]CRWLlet . Using the same
reasoning in the rest of subexpressions ei σ we can prove:
[[h(e1 σ 0 , e2 σ, . . . , en σ)]]CRWLlet ⊆ [[h(e1 σ 0 , e2 σ 0 , e3 σ . . . , en σ)]]CRWLlet
[[h(e1 σ 0 , e2 σ 0 , e3 σ . . . , en σ)]]CRWLlet ⊆ [[h(. . . , e3 σ 0 , e4 σ . . . , en σ)]]CRWLlet
...
[[. . . , en−1 σ 0 , en σ)]]CRWLlet ⊆ [[h(e1 σ 0 , . . . , en σ 0 )]]CRWLlet
Then by transitivity of ⊆ we have:
[[h(e1 , . . . , en )σ]]CRWLlet ≡ [[h(e1 σ, . . . , en σ)]]CRWLlet ⊆
[[h(e1 σ 0 , . . . , en σ 0 )]]CRWLlet ≡ [[h(e1 , . . . , en )σ 0 ]]CRWLlet .

64

López-Fraguas et al.

e ≡ let X = e1 in e2 - As Theorem 5 states, [[let X = e1 σ in e2 σ]]CRWLlet =

S
t1 ∈[[e1 σ]]CRWLlet

By the Induction Hypothesis we have that [[e1 σ]]CRWLlet ⊆ [[e1 σ 0 ]]CRWLlet . Due to
the variable convention we assume that X ∈
/ dom(σ)∪vran(σ) and X ∈
/ dom(σ 0 )∪
0
0
vran(σ ), so it is easy to check that σ[X/t]Eσ [X/t] for any t ∈ CT erm. Then by
the Induction Hypothesis we know that [[e2 σ[X/t]]]CRWLlet ⊆ [[e2 σ 0 [X/t]]]CRWLlet .
Therefore
S
[[(let X = e1 in e2 )σ]]CRWLlet =
[[e2 σ[X/t1 ]]]CRWLlet
t1 ∈[[e1 σ]]CRWLlet
S
⊆
[[e2 σ 0 [X/t1 ]]]CRWLlet
=
=

t1 ∈[[e1 σ 0 ]]CRWLlet
[[let X = e1 σ 0

in e2 σ 0 ]]CRWLlet
[[(let X = e1 in e2 )σ 0 ]]CRWLlet

Theorem 6 (Compositionality of hypersemantics)
For all C ∈ Cntxt, e ∈ LExp⊥
[[[C[e]]]] = [[[C]]][[[e]]]
As a consequence: [[[e]]] = [[[e0 ]]] ⇔ ∀C ∈ Cntxt.[[[C[e]]]] = [[[C[e0 ]]]].
Proof
By induction over the structure of contexts. The base case is C = [], so [[[C[e]]]] =
[[[e]]] = [[[[]]]][[[e]]] = [[[C]]][[[e]]], as [[[[]]]] is the identity function by definition. Regarding
the inductive step:
• C = h(e1 , . . . , C 0 , . . . , en ): Then
S
[[[C]]][[[e]]] = λθ.
[[h(e1 θ, . . . , t, . . . , en θ)]]
0
S t∈[[[C ]]][[[e]]]θ
= λθ.
[[h(e1 θ, . . . , t, . . . , en θ)]]
t∈[[[C 0 [e]]]]θ
S
= λθ.
[[h(e1 θ, . . . , t, . . . , en θ)]]

by IH
by definition

t∈[[(C 0 [e])θ]]

= λθ.[[h(e1 θ, . . . , (C 0 [e])θ, . . . , en θ)]]
= λθ.[[(C[e])θ]] = [[[C[e]]]]

by Lemma 5

• C = let X = C 0 in s: Then
S
[[[C]]][[[e]]] = λθ.
[[let X = t in sθ]]
t∈[[[C 0 ]]][[[e]]]θ
S
= λθ.
[[sθ[X/t]]]
t∈[[[C 0 ]]][[[e]]]θ
S
= λθ.
[[sθ[X/t]]]
t∈[[[C 0 [e]]]]θ
S
= λθ.
[[sθ[X/t]]]

by definition
by rule (Bind)(∗)
by IH
by definition

t∈[[(C 0 [e])θ]]

= λθ.[[let X = (C 0 [e])θ in sθ]]
= [[[C[e]]]]

by Lemma 5

(*): by Proposition 8 [[let X = t in sθ]] = [[sθ[X/t]]] since let X = t in sθ →lnf
sθ[X/t].

[[e2 σ[X/t1 ]]]CRWLlet .

Theory and Practice of Logic Programming

65

• C = let X = s in C 0 : Then
S
[[[C]]][[[e]]] = λθ.
[[[C 0 ]]][[[e]]](θ[X/t])
t∈[[[s]]]θ
S
= λθ.
[[[C 0 [e]]]](θ[X/t])
t∈[[[s]]]θ
S
= λθ.
[[(C 0 [e])(θ[X/t])]]
t∈[[[s]]]θ
S
= λθ.
[[(C 0 [e])(θ[X/t])]]
t∈[[sθ]]
S
= λθ.
[[((C 0 [e])θ)[X/t]]]

by IH
by definition
by definition

t∈[[sθ]]

= λθ.[[let X = sθ in (C 0 [e])θ]]
= [[[C[e]]]]

by Lemma 5

Proposition 6
Consider two sets A, B, and let F be the set of functions A → P(B). Then:
i) b is indeed a partial order on F, and ∆f is indeed a decomposition of f ∈ F,
i.e., d (∆f ) = f .
ii) Monotonicity of hyperunion wrt. inclusion: for any I1 , I2 ⊆ F
I1 ⊆ I2 implies

d

I1 b d I2

iii) Distribution of unions: for any I1 , I2 ⊆ F

d

(I1 ∪ I2 ) = (d I1 ) d (d I2 )

iv) Monotonicity of decomposition wrt. hyperinclusion: for any f1 , f2 ∈ F
f1 b f2 implies ∆f1 ⊆ ∆f2
Proof
i) The binary relation b is a partial order on F because:
• It is reflexive, as for any function f and any x ∈ A we have that f (x) = f (x),
and thus f (x) ⊆ f (x), therefore f b f .
• It is transitive because given some functions f1 , f2 , f3 such that f1 b f2 and
f2 b f3 , then for any x ∈ A we have f1 (x) ⊆ f2 (x) ⊆ f3 (x) by definition of
b, hence f1 b f3 .
• It is antisymmetric wrt. extensional function equality, because for any pair of
hypersemantics f1 , f2 such that f1 b f2 and f2 b f1 and any x ∈ A we have
that f1 (x) ⊆ f2 (x) and f2 (x) ⊆ f1 (x) by definition of b, hence f1 (x) = f2 (x)
by antisymmetry of ⊆ and f1 = f2 .
In order to prove that ∆f is indeed a decomposition of f ∈ F we first perform a
little massaging by using the definitions of d and ∆.
S S
d (∆f ) = d {λ̂a.{b} | a ∈ A, b ∈ f (a)} = λx ∈ A.
(λ̂a.{b})x
a∈A b∈f (a)

66

López-Fraguas et al.

Now we will use the fact that b is a partial order, and therefore it is antisymmetric,
so mutual inclusion by b implies equality.
• f b d (∆f ): Given arbitraries a ∈ A, b ∈ f (a) then
S S
(d (∆f ))a =
(λ̂x.{y})a
x∈A y∈f (x)
S
⊇
(λ̂a.{y})a
as a ∈ A
y∈f (a)
S
=
{y} 3 b
as b ∈ f (a)
y∈f (a)

•

d
b∈

(∆f ) b f : Given arbitraries a ∈ A, b ∈ (d (∆f ))a then we have that
S S
(λ̂x.{y})a, therefore ∃x ∈ A, y ∈ f (x) such that b ∈ (λ̂x.{y})a.
x∈A y∈f (x)

But then a ≡ x —otherwise (λ̂x.{y})a = ∅— and y ≡ b —because b ∈
(λ̂x.{y})a = {y}—, and so y ∈ f (x) implies b ∈ f (a).
ii) Given an arbitrary a ∈ A then
S
(d I1 )a =
f (a)
f ∈I1
S
⊆
f (a)

by definition of
as I1 ⊆ I2

f ∈I2

= (d I2 )a

d

by definition of

d

iii)

d

S
(I1 ∪ I2 ) = λa.
f (a)
f ∈(I1 ∪I2 )
S
S
= λa.
f (a) ∪
f (a)
f ∈I1

f ∈I2

= λa.(d I1 )a ∪ (d I2 )a
= (d I1 ) d (d I2 )

by definition of

d

by definition of d
by definition of d

iv) Suppose an arbitrary λ̂a.{b} ∈ ∆f1 with a ∈ A and b ∈ f1 (a) by definition. Since
f1 b f2 then f1 (a) ⊆ f2 (a). Therefore b ∈ f2 (a) and λ̂a.{b} ∈ ∆f2 .

Proposition 7 (Distributivity under context of hypersemantics union)
[[[C]]](d H) =

d

[[[C]]]ϕ

ϕ∈H

Proof
We proceed by induction on the structure of C. Regarding the base case, then C = []
and so:
[[[C]]](d H) = d H by definition of [[[C]]]
= d ϕ
ϕ∈H

=

d

[[[C]]]ϕ

by definition of [[[C]]]

ϕ∈H

For the inductive step we have several possibilities.

Theory and Practice of Logic Programming
• C ≡ h(e1 , . . . , C 0 , . . . , en ): then
S
[[[C]]](d H) = λθ.

d

t∈[[[C 0 ]]](

S

= λθ.

[[h(e1 θ, . . . , t, . . . , en θ)]]
[[h(e1 θ, . . . , t, . . . , en θ)]]

dS{[[[C ]]]ϕ | ϕ∈H})θ)

t∈(

S

by IH

0

[[h(e1 θ, . . . , t, . . . , en θ)]]

by definition of

[[[C 0 ]]]ϕθ)

Sϕ∈H S

= λθ.

by definition of [[[C]]]

H)θ

t∈((

= λθ.

67

d

[[h(e1 θ, . . . , t, . . . , en θ)]]

ϕ∈H t∈[[[C 0 ]]]ϕθ

S

= λθ.

[[[C]]]ϕθ

by definition of [[[C]]]

ϕ∈H

d

=

[[[C]]]ϕ

by definition of

ϕ∈H

d

• C ≡ let X = C 0 in e: then
[[[C]]](d H) = λθ.

S

d

t∈[[[C 0 ]]](

S

= λθ.

[[let X = t in eθ]]
[[let X = t in eθ]]

t∈((

dS{[[[C ]]]ϕ | ϕ∈H})θ)

t∈(

S

= λθ.

by IH

0

[[let X = t in eθ]]

by definition of

[[[C 0 ]]]ϕθ)

Sϕ∈H S

= λθ.

by definition of [[[C]]]

H)θ

d

[[let X = t in eθ]]

ϕ∈H t∈[[[C 0 ]]]ϕθ

S

= λθ.

[[[C]]]ϕθ

by definition of [[[C]]]

ϕ∈H

=

d

[[[C]]]ϕ

by definition of

ϕ∈H

• C ≡ let X = e in C 0 : then
S
[[[C 0 ]]](d H)(θ[X/t])
[[[C]]](d H) = λθ.
t∈[[[e]]]θ
S
= λθ.
(d {[[[C 0 ]]]ϕ | ϕ ∈ H})(θ[X/t])
t∈[[[e]]]θ
S S
= λθ.
[[[C 0 ]]]ϕ(θ[X/t])
t∈[[[e]]]θ ϕ∈H
S S
= λθ.
[[[C 0 ]]]ϕ(θ[X/t])
ϕ∈H t∈[[[e]]]θ
S
= λθ.
[[[C]]]ϕθ

d

by definition of [[[C]]]
by IH
by definition of

d

as H is independent from t
by definition of [[[C]]]

ϕ∈H

=

d

[[[C]]]ϕ

by definition of

ϕ∈H

d

A.7 Proofs for Section 4.3
Theorem 9 (Hyper-Soundness of let-rewriting)
∗
For all e, e0 ∈ LExp, if e →l e0 then [[[e0 ]]] b [[[e]]].
Proof
We first prove the theorem for a single step of →l . We proceed assumming some

68

López-Fraguas et al.

θ ∈ CSubst⊥ such that e0 θ _ t and then proving eθ _ t. The case where t ≡⊥
holds trivially using the rule B, so we will prove the rest by a case distinction on
the rule of the let-rewriting calculus applied:
(Fapp) Assume f (t1 , . . . , tn ) →l r with (f (p1 , . . . , pn ) → e) ∈ P, σ ∈ CSubst, such
that ∀i.pi σ ≡ ti and eσ ≡ r, and θ ∈ CSubts⊥ such that rθ _ t. Then as
σθ ∈ CSubts⊥ , ∀i.pi σθ ≡ ti θ and eσθ ≡ rθ we can use the (OR) rule to build the
following proof:
Lemma 18
t1 θ _ t1 θ

Lemma 18
...
tn θ _ tn θ
f (t1 θ, . . . , tn θ) _ t

rθ _ t

(OR)

(LetIn) Assume h(. . . , e, . . .) →l let X = e in h(. . . , X, . . .) by (LetIn) and θ ∈
CSubts⊥ such that (let X = e in h(. . . , X, . . .))θ _ t. This proof must be of the
shape of:
eθ _ t1
h(d1 θ, . . . , Xθ, . . . , dn θ)[X/t1 ] _ t
(Let)
let X = eθ in h(d1 θ, . . . , Xθ, . . . , dn θ) _ t

for some d1 , . . . , dn ∈ LExp, t1 ∈ CT erm⊥ . Besides X 6∈ (dom(θ) ∪ vran(θ)) by
the variable convention5 , hence Xθ ≡ X and so h(d1 θ, . . . , Xθ, . . . , dn θ)[X/t1 ] ≡
h(d1 θ, . . . , t1 , . . . , dn θ), as X is fresh by the conditions in (LetIn) and so it does
not appear in any di . Now we have two possibilities:
a) h ≡ c ∈ DC : Then h(d1 θ, . . . , t1 , . . . , dn θ) _ t must proved by (DC):
d1 θ _ s1 . . . t1 _ t01 . . . dn θ _ sn
c(d1 θ, . . . , t1 , . . . , dn θ) _ c(s1 , . . . , t01 , . . . , sn ) ≡ t

(DC)

for some s1 , . . . , sn , t01 ∈ CT erm⊥ . Then t1 _ t01 implies t01 v t1 by Lemma
5, hence eθ _ t1 implies eθ _ t01 by Proposition 3, and we can build the
following proof:
d1 θ _ s1 . . . eθ _ t01 . . . dn θ _ sn
h(. . . , e, . . .)θ ≡ c(d1 θ, . . . , eθ, . . . , dn θ) _ c(s1 , . . . , t01 , . . . , sn ) ≡ t
b) h ≡ f ∈ F S : Then h(d1 θ, . . . , t1 , . . . , dn θ) _ t must be proved by (OR):
d1 θ _ s1 σ

. . . t1 _ t01 σ . . . dn θ _ sn σ
f (d1 θ, . . . , t1 , . . . , dn θ) _ t

rσ _ t

(OR)

for some s1 σ, . . . , sn σ, t01 σ ∈ CT erm⊥ , (f (s1 , . . . , t01 , . . . sn ) → r) ∈ P, σ ∈
CSubst⊥ . Then we can prove eθ _ t01 σ like in the previous case, to build
the following proof:
d1 θ _ s1 σ . . . eθ _ t01 σ . . . dn θ _ sn σ rσ _ t
(OR)
h(. . . , e, . . .)θ ≡ f (d1 θ, . . . , eθ, . . . , dn θ) _ t
5

Actually, to prove this theorem properly, we cannot restrict the substitution to fulfill these
restrictions, so in fact we rename the bound variables in an α-conversion fashion and use the
equivalence e[X/e0 ] ≡ e[X/Y ][Y /e0 ] (with Y the new bound variable), to use the hypothesis.
This will be done implicitly when needed during the remaining of the proof.

Theory and Practice of Logic Programming

69

(Bind) Assume let X = t1 in e →l e[X/t1 ] by (Bind) and θ ∈ CSubst⊥ such that
(e[X/t1 ])θ _ t. Then X 6∈ (dom(θ) ∪ vran(θ)) by the variable convention, so we
can apply Lemma 1 (Substitution lemma) to get eθ[X/t1 θ] ≡ (e[X/t1 ])θ. Besides
t1 ∈ CT erm and θ ∈ CSubst⊥ by hypothesis, hence t1 θ ∈ CT erm⊥ and we can
build the following proof:
Lemma 18
t1 θ _ t1 θ
eθ[X/t1 θ] ≡ (e[X/t1 ])θ _ t
(Let)
let X = t1 θ in eθ _ t

(Elim) Assume let X = e1 in e2 →l e2 by (Elim) and θ ∈ CSubts⊥ such that
e2 θ _ t. Then X 6∈ vran(θ) by the variable convention and X 6∈ F V (e2 ) by the
condition of (Elim), hence e2 θ[X/ ⊥] ≡ e2 θ and we can build the following proof:
(B)
e1 θ _⊥
e2 θ[X/ ⊥] ≡ e2 θ _ t
(Let)
let X = e1 θ in e2 θ _ t

(Flat) Assume let X = (let Y = e1 in e2 ) in e3 →l let Y = e1 in (let X = e2 in e3 )
by (Flat) and θ ∈ CSubts⊥ such that (let Y = e1 in (let X = e2 in e3 ))θ _ t.
This proof must be must be of the shape of:
e2 θ[Y /t1 ] _ t2 e3 θ[Y /t1 ][X/t2 ] _ t
(Let)
(let X = e2 θ in e3 θ)[Y /t1 ] _ t
e1 θ _ t1
(Let)
let Y = e1 θ in (let X = e2 θ in e3 θ) _ t

for some t1 , t2 ∈ CT erm⊥ . Besides Y 6∈ vran(θ) by the variable convention and
Y 6∈ F V (e3 ) by the condition of (Flat), hence e3 θ[Y /t1 ] ≡ e3 θ and we can build
the following proof:
Hypothesis
Hypothesis
e1 θ _ t1
e2 θ[Y /t1 ] _ t2
(Let)
let Y = e1 θ in e2 θ _ t2
e3 θ[X/t2 ] ≡ e3 θ[Y /t1 ][X/t2 ] _ t
(Let)
let X = (let Y = e1 θ in e2 θ) in e3 θ _ t

(Contx) By the proof of the other cases, [[[e0 ]]] b [[[e]]], but then [[[C[e0 ]]]] b [[[C[e]]]] by
Lemma 7, and we are done.
The proof for several steps is a trivial induction on the length of the derivation
∗
e →l e0 .
Proposition 8 (The →lnf relation preserves hyperdenotation)
∗
For all e, e0 ∈ LExp, if e →lnf e0 then [[[e]]] = [[[e0 ]]]—and therefore [[e]] = [[e0 ]].
Proof
We first prove the lemma for one step of →lnf by case distinction over the rule
applied to reduce e to e0 . By Theorem 9 we already have that ∀e, e0 ∈ LExp if
e →lnf e0 then [[[e0 ]]] b [[[e]]], so all that is left is proving that [[[e]]] b [[[e0 ]]] also, and
finally applying the transitivity of b, as it is a partial order by Lemma 6-i. We
proceed assumming some θ ∈ CSubst⊥ such that eθ _ t and then proving e0 θ _ t.
The case where t ≡⊥ holds trivially using the rule (B), so we will prove the other
by a case distinction on the rule of the let calculus applied:

70

López-Fraguas et al.

(LetIn) Assume h(d1 , . . . , e, . . . , dn ) →l let X = e in h(d1 , . . . , X, . . . , dn ) by the
(LetIn) rule and θ ∈ CSubts⊥ such that
h(d1 , . . . , e, . . . , dn )θ ≡ h(d1 θ, . . . , eθ, . . . , dn θ) _ t
Then by the compositionality of Theorem 5 we have that ∃t1 ∈ [[eθ]] such that
h(d1 θ, . . . , t1 , . . . , dn θ) _ t. Besides X is fresh and X 6∈ (dom(θ) ∪ vran(θ)) by
the variable convention, hence
(let X = e in h(d1 , . . . , X, . . . , dn ))θ ≡ let X = eθ in h(d1 θ, . . . , X, . . . , dn θ)
and
h(d1 θ, . . . , X, . . . , dn θ)[X/t1 ] ≡ h(d1 θ, . . . , t1 , . . . , dn θ)
and so we can do:
hypothesis
hypothesis
eθ _ t1
h(d1 θ, . . . , X, . . . , dn θ)[X/t1 ] ≡ h(d1 θ, . . . , t1 , . . . , dn θ) _ t
(Let)
(let X = e in h(d1 , . . . , X, . . . , dn ))θ ≡ let X = eθ in h(d1 θ, . . . , X, . . . , dn θ) _ t
(Bind) Assume let X = t1 in e →l e[X/t1 ] by (Bind) and θ ∈ CSubst⊥ such that (let X =
t1 in e)θ ≡ let X = t1 θ in eθ _ t. Then it must be with a proof of the following shape:
t1 θ _ t01 eθ[X/t01 ] _ t
(Let)
let X = t1 θ in eθ _ t

But θ ∈ CSubst⊥ and t1 ∈ CT erm implies t1 θ ∈ CT erm⊥ , and so t1 θ _ t01 implies t01 v
t1 θ by Lemma 5-1. Hence [X/t01 ] v [X/t1 θ] and so eθ[X/t01 ] _ t implies eθ[X/t1 θ] _ t
by the monoticity of Proposition 5. Besides X 6∈ (dom(θ) ∪ vran(θ)) by the variable
convention, and so we can apply Lemma 1 (substitution lemma) to get (e[X/t1 ])θ ≡
eθ[X/t1 θ], so we are done.
(Elim) Assume let X = e1 in e2 →l e2 by (Elim) and θ ∈ CSubts⊥ such that (let X =
e1 in e2 )θ ≡ let X = e1 θ in e2 θ _ t. Then it must be with a proof of the following
shape:
e1 θ _ t1 e2 θ[X/t1 ] _ t
(Let)
let X = e1 θ in e2 θ _ t
Then X 6∈ vran(θ) by the variable convention and X 6∈ F V (e2 ) by the condition of
(Elim), hence e2 θ ≡ e2 θ[X/t1 ] _ t, so we are done.
(Flat) Straightforward since e3 θ[Y /t1 ] ≡ e3 θ because Y 6∈ vran(θ) by the variable convention and Y 6∈ F V (e3 ) by the condition of (Flat).
(Contx) By the proof of the other cases, [[[e]]] b [[[e0 ]]], but then [[[C[e]]]] b [[[C[e0 ]]]] by Lemma
7, and we are done.

The following lemmas —Lemmas 29, 30, 31 and 32— will be used to prove Lemma
8.
Lemma 29
Let linear e, e1 ∈ Exp such that eθ v e1 for θ ∈ Subst⊥ . Then ∃θ0 ∈ Subst such
that eθ0 ≡ e1 and θ v θ0 .

Theory and Practice of Logic Programming

71

Proof
By induction on the structure of e. For the base case (e ≡ X ∈ V) we define a
function rep⊥ : Exp⊥ → Exp → Exp rep⊥ (e, e0 ) that replaces the occurrences of
⊥ in e by the expression e0 . We define this function recursively on the structure of
e:
• rep⊥ (⊥, e0 ) = e0
• rep⊥ (Z, e0 ) = Z
• rep⊥ (h(e1 , . . . , en ), e0 ) = h(rep⊥ (e1 , e0 ), . . . , rep⊥ (en , e0 ))
It is easy to check that rep⊥ (e, e0 ) = e00 implies e v e00 . Then we define θ0 ∈ Subst
as:

e1
if X ≡ Y
θ0 (Y ) =
rep⊥ (θ(Y ), Y ) if Y ∈ dom(θ) r {X}
Trivially eθ0 ≡ Xθ0 ≡ e1 and θ v θ0 because eθ v e1 by the premise and θ(Y ) v
rep⊥ (θ(Y ), Y ).
Regarding the inductive step —e ≡ h(e1 , . . . , en )— we know that
eθ ≡ h(e1 θ, . . . , en θ) v e1 ≡ h(e01 , . . . , e0n )
so ei θ v e0i . Then by IH ∃θi0 ∈ Subst such
θ0 as:
 0
θ1 (Y )



0

 θ2 (Y )
0
θ (Y ) =
...



θ0 (Y )

 n
rep⊥ (θ(Y ), Y )

that ei θi0 ≡ e0i and θ v θi0 . Then we define
if Y ∈ var(e1 )
if Y ∈ var(e2 )
if Y ∈ var(en )
if Y ∈ dom(θ) r var(e)

The substitution θ0 is well defined because e is linear. Then eθ0 ≡ h(e1 θ0 , . . . , en θ0 ) ≡
h(e1 θ10 , . . . , en θn0 ) = h(e01 , . . . , e0n ) ≡ e1 and θ v θ0 by IH and the fact that θ(Y ) v
rep⊥ (θ(Y ), Y ).
Lemma 30
For any e ∈ LExp⊥ , F V (|e|) ⊆ F V (e).
Proof
Straightforward by induction on the structure of e.
Lemma 31
Given e ∈ LExp, θ ∈ LSubst⊥ , |eθ| = |e|θ̂ where θ̂ is defined as X θ̂ = |Xθ|
Proof
By induction on the structure of e. We have two base cases:
• e ≡ X ∈ V. Then |eθ| ≡ |Xθ| = X θ̂ = |X|θ ≡ |e|θ̂.
• e ≡ f (e1 , . . . , en ). Then |eθ| ≡ |f (e1 , . . . , en )θ| = |f (e1 θ, . . . , en θ)| =⊥=⊥ θ̂ =
|f (e1 , . . . , en )|θ̂ ≡ |e|θ̂.
Regarding the inductive step we have:

72

López-Fraguas et al.

• e ≡ c(e1 , . . . , en ). Straightforward.
• e ≡ let X = e1 in e2 . Then |eθ| = |(let X = e1 in e2 )θ| = |let X = e1 θ in e2 θ| =
|e2 θ|[X/|e1 θ|]. By IH we have that |e1 θ| = |e1 |θ̂ and |e2 θ| = |e2 |θ̂, so |e2 θ|[X/|e1 θ|] =
|e2 θ| = (|e2 |θ̂)[X/|e1 |θ̂]. By the variable convention we can assume that X ∈
/
dom(θ) ∪ vran(θ), and since dom(θ̂) = dom(θ) and vran(θ̂) ⊆ vran(θ) —using
Lemma 30— we can use Lemma 1 and obtain (|e2 |θ̂)[X/|e1 |θ̂] = (|e2 |[X/|e1 |])θ̂.
Finally, (|e2 |[X/|e1 |])θ̂ = |let X = e1 in e2 |θ̂ = |e|θ̂.

Lemma 32
Given e ∈ LExp, θ ∈ LSubst⊥ , if |e| =⊥ then |eθ| =⊥.
Proof
By induction on the structure of e. Notice that e cannot be a variable X or an
applied constructor symbol c(e1 , . . . , en ) because in those cases |e| 6=⊥. The base
case e ≡ f (e1 , . . . , en ) is straightforward. Regarding the inductive step we have
e ≡ let X = e1 in e2 such that |let X = e1 in e2 | = |e2 |[X/|e1 |] =⊥. Then
|eθ| = |(letX = e1 in e2 )θ| = |let X = e1 θ in e2 θ| = |e2 θ|[X/|e1 θ|]. By Lemma
23 |e2 θ|[X/|e1 θ|] = |(e2 θ)[X/e1 θ]|, and since X ∈
/ dom(θ) ∪ vran(θ) by the variable convention then we can apply Lemma 1 and |(e2 θ)[X/e1 θ]| = |(e2 [X/e1 ])θ|.
Finally by Lemma 31 |(e2 [X/e1 ])θ| = |e2 [X/e1 ]|θ̂, and by Lemma 23 |e2 [X/e1 ]|θ̂ =
(|e2 |[X/|e1 |])θ̂ =⊥ θ̂ =⊥.
Lemma 8 (Completeness lemma for let-rewriting)
For all e ∈ LExp and t ∈ CT erm⊥ such that t 6≡⊥,
∗

e _ t implies e →l let X = a in t0

for some t0 ∈ CT erm and a ⊆ LExp in such a way that t v |let X = a in t0 | and
|ai | =⊥ for every ai ∈ a. As a consequence, t v t0 [X/ ⊥].
Proof
By induction on the size s of the CRWLlet -proof, that we measure as the number
of CRWLlet rules applied. Concerning the base cases:
(B) This contradicts the hypothesis because then t ≡⊥, so we are done. In the
rest of the proof we will assume that t 6≡⊥ because otherwise we would be in this
case.
0
(RR) Then we have X _ X. But then X →l X and X v X ≡ |X|, so we are
done with X = ∅.
0
(DC) Then we have c _ c. But then c →l c and c v c ≡ |c|, so we are done with
X = ∅.
Now we treat the inductive step:
(DC) Then we have e ≡ c(e1 , . . . , en ) and the CRWLlet -proof has the shape:
e1 _ t1 , . . . , en _ tn
(DC)
c(e1 , . . . , en ) _ c(t1 , . . . , tn )

Theory and Practice of Logic Programming

73

In the general case some ti will be equal to ⊥ and some others will be different. For
the sake of simplicity we consider the case when n = 2 with t1 = ⊥ and t2 6≡ ⊥,
the proof can be easily extended to the general case. Then we have c(e1 , e2 ) _
∗
c(⊥, t2 ), so by IH over the second argument we get e2 →l let X2 = a2 in t02 with
t02 ∈ CT erm, |a2i | =⊥ for every a2i ∈ a2 and |let X2 = a2 in t02 | = t02 [X2 / ⊥] w t2 .
So:
∗
c(e1 , e2 ) →l c(e1 , let X2 = a2 in t02 )
by IH
→l let Y = (let X2 = a2 in t02 ) in c(e1 , Y ) by (LetIn)
∗
→l let X2 = a2 in let Y = t02 in c(e1 , Y )
by (Flat*)
l
0
→ let X2 = a2 in c(e1 , t2 )
by (Bind)
Then there are several possible cases:
a) e1 ≡ f1 (e1 ): Then let X2 = a2 in c(f1 (e1 ), t02 ) →l let X2 = a2 in let Z =
f1 (e1 ) in c(Z, t02 ), by (LetIn). So we are done as |a2i | =⊥ for every a2i
by the IH, |f1 (e1 )| =⊥ and |let X2 = a2 in let Z = f1 (e1 ) in c(Z, t02 )| =
c(Z, t02 )[X2 / ⊥, Z/ ⊥] w c(⊥, t2 ) because t02 [X2 / ⊥] w t2 by the IH, and Z
is fresh and so it does not appear in t02
b) e1 ≡ t01 ∈ CT erm: Then we are done as |a2i | =⊥ for every a2i ∈ a2 by
the IH, and |let X2 = a2 in c(t01 , t02 )| = c(t01 , t02 )[X2 / ⊥] w c(⊥, t2 ), because
t02 [X2 / ⊥] w t2 by the IH
c) e1 ≡ c1 (e1 ) 6∈ CT erm with c1 ∈ CS: Then by Lemma 3 we have the
∗
derivation c1 (e1 ) →l let X1 = f1 (t01 ) in c1 (t1 ). But then:
let X2 = a2 in c(c1 (e1 ), t02 )
∗

→l let X2 = a2 in c(let X1 = f1 (t01 ) in c1 (t1 ), t02 )

Lemma 3

→ let X2 = a2 in let Y = (let X1 =
in c1 (t1 )) in c(Y, t02 )
∗
→l let X2 = a2 in let X1 = f1 (t01 ) in let Y = c1 (t1 ) in c(Y, t02 )
→l let X2 = a2 in let X1 = f1 (t01 ) in c(c1 (t1 ), t02 )

by (LetIn)

f1 (t01 )

l

by (Flat*)
by (Bind)

In the last step notice that Y is fresh and it cannot appear in t02 . Then
we are done as |fi (t0i )| =⊥, |a2i | =⊥ for every a2i ∈ a2 by the IH, and
|let X2 = a2 in let X1 = f1 (t01 ) in c(c1 (t1 ), t02 )| = c(c1 (t1 ), t02 )[X1 / ⊥][X2 / ⊥]
w c(⊥, t2 ) because t02 [X2 / ⊥] w t2 by the IH, and no variable in X1 appears
in t02 by α-conversion, as those are bound variables which were present in
c1 (e1 ) or that appeared after applying Lemma 3 to it, and this expression
was placed in a position parallel to the position of t02 .
∗
d) e1 ≡ let X = e11 in e12 : Then by Lemma 3 let X = e11 in e12 →l
let X1 = f1 (t01 ) in e00 where e00 ∈ V or e00 ≡ h1 (t1 ). Then:
let X2 = a2 in c(let X = e11 in e12 , t02 )
∗

→l let X2 = a2 in c(let X1 = f1 (t01 ) in e00 , t02 )

by Lemma 3

→l let X2 = a2 in let Y = (let X1 = f1 (t01 ) in e00 ) in c(Y, t02 )
→

l∗

let X2 = a2 in let X1 =

f1 (t01 )

00

in let Y = e in

Then we have two possibilities depending on e00 :

c(Y, t02 )

by (LetIn)
by (Flat∗ )

74

López-Fraguas et al.
i) e00 ≡ Z ∈ V: Then we can do:
let X2 = a2 in let X1 = f1 (t01 ) in let Y = Z in c(Y, t02 )
→l let X2 = a2 in let X1 = f1 (t01 ) in c(Z, t02 )

by (Bind)

Then we are done as |f1 (t01 )| =⊥, |a2i | =⊥ for every a2i ∈ a2 by IH, and
|let X2 = a2 in let X1 = f1 (t01 ) in c(Z, t02 )| = c(Z, t02 )[X1 / ⊥][X2 / ⊥] w
c(⊥, t2 ), as t02 [X2 / ⊥] w t2 by IH, and no variable in X1 appears in t02
by α-conversion, like in the case c).
ii) e00 ≡ h1 (t1 ): there are two possible cases:
A) h1 = f1 ∈ F S: We are done as |f1 (t01 )| =⊥, |a2i | =⊥ for every a2i ∈
a2 by IH, |f1 (t1 )| =⊥, and |let X2 = a2 in let X1 = f1 (t01 ) in let Y =
f1 (t1 ) in c(Y, t02 )| = c(Y, t02 )[Y / ⊥][X1 /⊥][X2 /⊥] w c(⊥, t2 ), as by IH
t02 [X2 /⊥] w t2 , Y is fresh and so it does not appear in t02 , and no
variable in X1 appears in t02 as in the case i).
B) h1 = c1 ∈ DC: Then we can do a (Bind) step:
let X2 = a2 in let X1 = f1 (t01 ) in let Y = c1 (t1 ) in c(Y, t02 )
→l let X2 = a2 in let X1 = a1 in c(c1 (t1 ), t02 )
Then we are done as |f1 (t01 )| =⊥, |a2i | =⊥ for every a2i ∈ a2 by IH,
and
|let X2 = a2 in let X1 = f1 (t01 ) in c(c1 (t1 ), t02 )|
= c(c1 (t1 ), t02 )[X1 / ⊥][X2 / ⊥]
w c(⊥, t2 )
as t02 [X2 / ⊥] w t2 by IH, and no variable in X1 appears in t02 , as we
saw in i).
(OR) If f has no arguments (n = 0) then we have:
rθ _ t (OR)
f _t

with (f _ r) ∈ P and θ ∈ CSubst⊥ . Let us define θ0 ∈ CSubst as the substitution which is equal to θ except that every ⊥ introduced by θ is replaced
with some constructor symbol or variable. Then θ v θ0 , so by Proposition 5 we
have rθ0 _ t with a proof of the same size. But then applying the IH to this
∗
proof we get rθ0 →l let X = a in t0 under the conditions of the lemma. Hence
∗
f →l rθ0 →l let X = a in t0 applying (Fapp) in the first step, and we are done.
If n > 0, we will proceed as in the case for (DC), doing a preliminary version for
f (e1 , e2 ) _ t which can be easily extended for the general case. Then we have:
e1 _⊥ e2 _ t2 rθ _ t
(OR)
f (e1 , e2 ) _ t

such that t2 6≡⊥, and with (f (p1 , p2 ) → r) ∈ P, θ ∈ CSubst⊥ , such that

Theory and Practice of Logic Programming

75
∗

p1 θ =⊥ and p2 θ = t2 . Then applying the IH to e2 _ t2 we get that e2 →l
let X2 = a2 in t02 such that |a2i | =⊥ for every a2i and |let X2 = a2 in t02 | =
t02 [X2 / ⊥] w t2 . Then we can do:
∗

f (e1 , e2 ) →l f (e1 , let X2 = a2 in t02 )
→l let Y = (let X2 = a2 in t02 ) in f (e1 , Y )
∗
→l let X2 = a2 in let Y = t02 in f (e1 , Y )
→l let X2 = a2 in f (e1 , t02 )

by
by
by
by

IH
(LetIn)
(Flat*)
(Bind)

Then applying Lemma 3 we get
∗

f (e1 , t02 ) →l let X1 = f1 (t0 ) in f (t01 , t02 )
Now as t02 [X2 / ⊥] w t2 then (t01 , t02 ) w (⊥, t2 ), so by Lemma 29 there must exist
θ0 ∈ CSubst such that θ v θ0 and (p1 , p2 )θ0 ≡ (t01 , t02 ). Then by Proposition 5, as
rθ _ t then rθ0 _ t with a proof of the same size. As θ0 ∈ CSubst and e ∈ LExp
(because it is part of the program) then rθ0 ∈ LExp and we can apply the IH
∗
to that proof getting that rθ0 →l let X = a in t0 such that |ai | =⊥ for every ai
and |let X = a in t0 | = t0 [X/ ⊥] w t. Then we can do:
let X2 = a2 in f (e1 , t02 )
∗
→l let X2 = a2 in let X1 = f1 (t0 ) in f (t01 , t02 )
≡ let X2 = a2 in let X1 = f1 (t0 ) in f (p1 , p2 )θ0
→l let X2 = a2 in let X1 = f1 (t0 ) in rθ0
∗
→l let X2 = a2 in let X1 = f1 (t0 ) in let X = a in t0

by Lemma 3
by (Fapp)
by 2nd IH

Then |a2i | =⊥ for every a2i ∈ a2 by IH, |f1 (t0 )| =⊥ and |ai | =⊥ for every ai by
IH. Besides the variables in X1 ∪X2 either belong to BV (e1 )∪BV (e2 ) or are fresh,
hence none of them may appear in t (by Lemma 27 over f (e1 , e2 ) _ t or by freshness). So t0 [X/ ⊥] w t implies that ∀p ∈ O(t0 ) such that t0 |p = Y for some Y ∈
X1 ∪ X2 then t|p =⊥. But then |let X2 = a2 in let X1 = a1 in let X = a in t0 | ≡
t0 [X/ ⊥][X1 / ⊥][X2 / ⊥] w t.
(Let) Then e ≡ let X = e1 in e2 and we have a proof of the following shape:
e1 _ t1 e2 [X/t1 ] _ t
(Let)
let X = e1 in e2 _ t
Then we have two possibilities:
a) t1 ≡⊥: Then e2 [X/t1 ] ≡ e2 [X/ ⊥] v e2 . Hence, as e2 [X/t1 ] _ t and
[X/t1 ] v , by Proposition 5 we get e2  ≡ e2 _ t with a proof of the
∗
same size or smaller, and so by IH we get e2 →l let X = a in t0 , with
t0 ∈ CT erm, |ai | ≡⊥ for every ai and |let X = a in t0 | ≡ t0 [X/ ⊥] w t, and
we can do:
∗

let X = e1 in e2 →l let X = e1 in let X = a in t0
Besides X 6∈ var(t) by Lemma 27 over let X = e1 in e2 _ t, and then
t0 [X/ ⊥] w t implies ∀p ∈ O(t0 ) such that t0 |p ≡ X then t|p ≡⊥, and we
have several possible cases:

76

López-Fraguas et al.
i) e1 = f1 (e1 ): Then we are donde because |a| ≡ ⊥ by IH, |f1 (e1 )| ≡⊥ and
|let X = f1 (e1 ) in let X = a in t0 | ≡ t0 [X/ ⊥][X/ ⊥] w t, as t0 [X/ ⊥] w t
and ∀p ∈ O(t0 ) such that t0 |p ≡ X then t|p ≡⊥, as we saw above.
ii) e1 = t01 ∈ CT erm: But then
let X = t01 in let X = a in t0 →l let X = a[X/t01 ] in t0 [X/t01 ]

by (Bind)

and we are done because |a| ≡ ⊥ by IH, and so |a[X/t01 ]| ≡ ⊥ by
Lemma 32. Besides, as in i), t0 [X/ ⊥] w t combined with the fact
that ∀p ∈ O(t0 ) such that t0 |p ≡ X we have t|p ≡⊥, implies that
|let X = a[X/t01 ] in t0 [X/t01 ]| ≡ t0 [X/t01 ][X/ ⊥] w t.
iii) e1 = c1 (e1 ) 6∈ CT erm with c1 ∈ CS: Then by Lemma 3 we have
∗
c1 (e1 ) →l let X1 = f1 (t1 ) in c1 (t1 ), hence
let X = c1 (e1 ) in let X = a in t0
∗
→l let X = (let X1 = f1 (t1 ) in c1 (t1 )) in let X = a in t0
∗
→l let X1 = f1 (t1 ) in let X = c1 (t1 ) in let X = a in t0
→l let X1 = f1 (t1 ) in let X = a[X/c1 (t1 )] in t0 [X/c1 (t1 )]

by Lemma 3
by (Flat∗ )
by (Bind)

As by IH |a| ≡ ⊥ then |a[X/c1 (t1 )]| ≡ ⊥ by Lemma 32. At this
point we have to check that |let X1 = a1 in let X = a[X/c1 (t1 )] in
t0 [X/c1 (t1 )]| ≡ t0 [X/c1 (t1 )][X/ ⊥][X1 / ⊥] w t. The variables in X1 either belong to BV (c1 (e1 )) or are fresh, hence by α-conversion none of
them may appear in t0 , because in let X = c1 (e1 ) in let X = a in t0
the expression t0 has no access to the variables bound in c1 (e1 ). Hence
t0 [X/c1 (t1 )][X/ ⊥][X1 / ⊥] ≡ t0 [X/t00 ][X/ ⊥], for some t00 ∈ CT erm⊥ .
But then, as in ii), t0 [X/ ⊥] w t combined with the fact that ∀p ∈ O(t0 )
such that t0 |p ≡ X we have t|p ≡⊥, implies that t0 [X/t00 ][X/ ⊥] w t.
∗
iv) e1 ≡ let Y = e11 in e12 : Then by Lemma 3 we have let Y = e11 in e12 →l
let X1 = f1 (t1 ) in h1 (t1 ), and so
let X = (let Y = e11 in e12 ) in let X = a in t0
∗
→l let X = (let X1 = f1 (t1 ) in h1 (t1 )) in let X = a in t0 by Lemma 3
∗
→l let X1 = f1 (t1 ) in let X = h1 (t1 ) in let X = a in t0 by (Flat∗ )
Then either h ∈ CS and we are like in iii) before the final (Bind) step, or
h ∈ F S and |h1 (t1 )| =⊥ and |a| = ⊥ (by IH), and |let X1 = a1 in let X =
h1 (t1 ) in let X = a in t0 | ≡ t0 [X/ ⊥][X/ ⊥][X1 / ⊥] ≡ t0 [X/ ⊥][X/ ⊥]
because X1 ∩var(t0 ) = ∅, as we saw in iii). But then, as in ii), t0 [X/ ⊥] w
t combined with the fact that ∀p ∈ O(t0 ) such that t0 |p ≡ X we have
t|p ≡⊥, implies that t0 [X/ ⊥][X/ ⊥] w t.
∗

b) t1 6≡⊥: Then by IH we get e1 →l let X1 = a1 in t01 , with t01 ∈ CT erm,
|a1i | ≡⊥ for every a1i and |let X1 = a1 in t01 | ≡ t01 [X1 / ⊥] w t1 . Hence t1 v
t01 and so e2 [X/t1 ] v e2 [X/t01 ], but then e2 [X/t1 ] _ t implies e2 [X/t01 ] _ t
with a proof of the same size or smaller, by Proposition 3. Therefore we
∗
may apply the IH to that proof to get e2 [X/t01 ] →l let X = a in t0 , with
t0 ∈ CT erm, |ai | ≡⊥ for every ai and |let X = a in t0 | ≡ t0 [X/ ⊥] w t. But

Theory and Practice of Logic Programming

77

then we can do:
∗

let X = e1 in e2 →l let X = (let X1 = a1 in t01 ) in e2
∗
→l let X1 = a1 in let X = t01 in e2
→l let X1 = a1 in e2 [X/t01 ]
∗
→l let X1 = a1 in let X = a in t0

by
by
by
by

IH
(Flat∗ )
(Bind)
IH

Then by the IH’s we have |a| = ⊥ and |a1 | = ⊥. Besides the variables in X1
either belong to BV (e1 ) or are fresh, hence none of them may appear in t
(by Lemma 27 over let X = e1 in e2 _ t or by freshness). So t0 [X/ ⊥] w t
implies that ∀p ∈ O(t0 ) such that t0 |p = Y for some Y ∈ X1 then t|p =⊥.
But then |let X1 = a1 in let X = a in t0 | ≡ t0 [X/ ⊥][X1 / ⊥] w t.

A.8 Proofs for Section 5
Lemma 10
If BV (C) ∩ F V (e1 ) = ∅ and X 6∈ F V (C) then [[[C[let X = e1 in e2 ]]]] = [[[let X =
e1 in C[e2 ]]]]
Proof
One step of the rule (Dist) can be replaced by two steps (CLetIn) + (Bind):
C[let X = e1 in e2 ] →l let U = e1 in C[let X = U in e2 ] →l let U = e1 in C[e2 [X/U ]]
followed by a renaming of U by X in the last expression. Then the lemma follows from preservation of hypersemantics by (CLetIn) and (Bind) (Lemma 9 and
Proposition 8).
Proposition 9 ((Hyper)semantic properties of ?)
For any e1 , e2 ∈ LExp⊥
i) [[e1 ? e2 ]] = [[e1 ]] ∪ [[e2 ]]
ii) [[[e1 ? e2 ]]] = [[[e1 ]]] d [[[e2 ]]]
Proof
i) Direct from definition of ? and the CRWL-proof calculus.
ii)
[[[e1 ? e2 ]]] = λθ.[[(e1 ? e2 )θ]]
= λθ.[[e1 θ ? e2 θ]]
= λθ.([[e1 θ]] ∪ [[e2 θ]])
= λθ.([[[e1 ]]]θ ∪ [[[e2 ]]]θ)
= [[[e1 ]]] d [[[e2 ]]]

by definition of [[[ ]]]
by i)
by definition of [[[ ]]]
by definition of d

A.9 Proofs for Section 6
Theorem 14 (Soundness of the let-narrowing relation
∗
∗
For any e, e0 ∈ LExp, e lθ e0 implies eθ →l e0 .

l

)

78

López-Fraguas et al.

Proof
First we prove the soundness of narrowing for one step, proceeding by a case distinction over the rule used in e l θ e0 . The cases of (Elim), (Bind), (Flat) and
(LetIn) are trivial, since narrowing and rewriting coincide for these rules.
(Narr) Then we have f (t) l θ rθ for (f (p) → r) ∈ P fresh, θ ∈ CSubst such that
f (t)θ ≡ f (p)θ. But then (f (p) → r)θ ≡ f (p)θ → rθ ≡ f (t)θ → rθ, so we can do
eθ ≡ f (t)θ →l rθ ≡ e0 by (Fapp).
(Contxt) Then we have C[e] l θ Cθ[e0 ] because e
tion over the rule applied in e l θ e0 :

l

θe

0

. Let us do a case distinc-

a) e l θ e0 ≡ f (t) l θ rθ by (Narr), for (f (p) → r) ∈ P fresh, so f (t)θ →l rθ
by (Fapp). Then (C[e])θ ≡ (C[e])θ|\var(p) , because the variables in var(p)
are fresh as (f (p) → r) is. But then, as dom(θ)∩BV (C) = ∅ and vRan(θ|\var(p) )∩
BV (C) = ∅ by the conditions in (Contx), and dom(θ) ∩ BV (C) = ∅ implies
dom(θ|\var(p) )∩BV (C) = ∅, we can apply Lemma 25 getting (C[e])θ|\var(p) ≡
Cθ|\var(p) [eθ|\var(p) ] ≡ Cθ|\var(p) [f (t)θ|\var(p) ] ≡ Cθ[f (t)θ], because the
variables in var(p) are fresh. Besides vran(θ|\var(p) ) ∩ BV (C) = ∅, so
we can apply (Contx) combined with an inner (Fapp) to do (C[e])θ ≡
Cθ[f (t)θ] →l Cθ[rθ] ≡ Cθ[e0 ].
b) In case a different rule was applied in e l θ e0 then θ = . By the proof
of the other cases we have eθ ≡ e →l e0 , so (C[e])θ ≡ C[e] →l C[e0 ] ≡ Cθ[e0 ]
(remember θ = ).
Now we prove the lemma for any number of steps →l , proceeding by induction
n
0
over the length n of e lθ e0 . The case e l e ≡ e0 is straightforward because
0
n−1
e →l e ≡ e0 . For n > 0 we have the derivation e lσ e00 lγ
e0 with θ = γ ◦ σ. By
the proof for one step eσ →l e00 , and by the closeness under CSubst of let-rewriting
∗
∗
(Lemma 2) eσγ →l e00 γ. By IH e00 γ →l e0 , so we can link eθ ≡ eσγ →l e00 γ →l e0 .
Lemma 11 (Lifting lemma for the let-rewriting relation →l )
∗
Let e, e0 ∈ LExp such that eθ →l e0 for some θ ∈ CSubst, and let W, B ⊆ V with
dom(θ) ∪ F V (e) ⊆ W, BV (e) ⊆ B and (dom(θ) ∪ vran(θ)) ∩ B = ∅, and for each
∗
(Fapp) step of eθ →l e0 using a rule R ∈ P and a substitution γ ∈ CSubst then
∗
vran(γ|vExtra(R) ) ∩ B = ∅. Then there exist a derivation e l σ e00 and θ0 ∈ CSubst
such that:
(i) e00 θ0 = e0

(ii) σθ0 = θ[W]

(iii) (dom(θ0 ) ∪ vran(θ0 )) ∩ B = ∅

Besides, the let-narrowing derivation can be chosen to use mgu’s at each (Narr)
step.
Proof
Let us do a case distinction over the rule applied in eθ →l e0 :

Theory and Practice of Logic Programming

79

(Fapp) e ≡ f (t), so:
e ≡ f (t)

l
σ

rσ

≡ e00

θ0

θ
f (t)θ

rγ
l

≡ e0

With an (Fapp) step eθ ≡ f (t)θ →l rγ with (f (p) → r) ∈ P, γ ∈ CSubst, such
that f (t)θ ≡ f (p)γ and f (p) → r is a fresh variant. We can assume that dom(γ) ⊆
F V (f (p) → r) without loss of generality. But then dom(θ) ∩ dom(γ) = ∅, and
so θ ] γ is correctly defined, and it is a unifier of f (t) and f (p). So, there must
exist σ = mgu(f (t), f (p)), which we can use to perform a (Narr) step, because
σ ∈ CSubst and f (t)σ ≡ f (p)σ.
e ≡ f (t)

l

σ

rσ ≡ e00

As this unifier is an mgu then dom(σ) ⊆ F V (f (t)) ∪ F V (f (p)), vran(σ) ⊆
F V (f (t)) ∪ F V (f (p)) and σ . (θ ] γ), so there must exist θ10 ∈ CSubst such that
σθ10 = θ ]γ. Besides we can define θ00 = θ|\(dom(θ10 )∪F V (f (t))) and then we can take
θ0 = θ00 ]θ10 which is correctly defined as obviously dom(θ00 )∩dom(θ10 ) = ∅. Besides
dom(θ00 ) ∩ (F V (f (t)) ∪ F V (f (p)) = ∅, as if Y ∈ F V (f (t)) then Y 6∈ dom(θ00 ) by
definition; and if Y ∈ F V (f (p)) then Y 6∈ dom(θ) as p belong to the fresh variant,
and so Y ∈
/ dom(θ00 ). Then the conditions in Lemma 11 hold:
• Condition i) e00 θ0 ≡ e0 : As e00 θ0 ≡ rσθ0 ≡ rσθ10 because given Y ∈ F V (rσ),
if Y ∈ F V (r) then it belongs to the fresh variant and so Y ∈
/ dom(θ) ⊇
dom(θ00 ); and if Y ∈ vran(σ) ⊆ F V (f (t)) ∪ F V (f (p)) then Y ∈
/ dom(θ00 )
0
0
because dom(θ0 ) ∩ (F V (f (t)) ∪ F V (f (p))) = ∅. But rσθ1 ≡ r(θ ] γ) ≡ rγ ≡
e0 , because σθ10 = θ ] γ and r is part of the fresh variant.
• Condition ii) σθ0 = θ[W]: Given Y ∈ W, if Y ∈ F V (f (t)) then Y ∈
/ dom(γ)
and so Y θ ≡ Y (θ ] γ) ≡ Y σθ10 , as σθ10 = θ ] γ. But Y σθ10 ≡ Y σθ0 because
given Z ∈ var(Y σ), if Z ≡ Y then as Y ∈ F V (f (t)) then Z ≡ Y ∈
/ dom(θ00 )
0
0
by definition of θ0 ; if Z ∈ vran(σ) then Z 6∈ dom(θ0 ), as we saw before.
On the other hand, (W \ F V (f (t))) ∩ (F V (f (t)) ∪ F V (f (p))) = (W \
F V (f (t)) ∩ F V (f (t))) ∪ (W \ F V (f (t)) ∩ F V (f (p))) = ∅ ∪ ∅ = ∅, because
F V (f (p)) are part of the fresh variant. So, if Y ∈ W \ F V (f (t)), then
Y 6∈ dom(σ) ⊆ F V (f (t)) ∪ F V (f (p)). Now if Y ∈ dom(θ00 ) then Y θ ≡
Y θ00 (by definition of θ00 ), Y θ00 ≡ Y θ0 (as Y ∈ dom(θ00 )), Y θ0 ≡ Y σθ0 (as
Y 6∈ dom(σ)). If Y ∈ dom(θ10 ), Y θ ≡ Y (θ ] γ) (as Y ∈ W \ F V (f (t))
implies it does not appear in the fresh instance), Y (θ ] γ) ≡ Y σθ10 (as
σθ10 = θ ] γ), Y σθ10 ≡ Y θ10 (as Y 6∈ dom(σ)), Y θ10 ≡ Y θ0 (as Y ∈ dom(θ10 ))
and Y θ0 ≡ Y σθ0 (as Y 6∈ dom(σ)). And if Y 6∈ (dom(θ00 ) ∪ dom(θ10 )) then
Y 6∈ dom(θ0 ), and as Y 6∈ dom(σ) and Y θ ≡ Y (θ ]γ), then Y θ ≡ Y (θ ]γ) ≡
Y σθ10 ≡ Y ≡ Y σθ0 .

80

López-Fraguas et al.
• Condition iii.1) dom(θ0 ) ∩ B = ∅. Remember θ0 = θ00 ] θ10 :
— dom(θ00 ) ∩ B = ∅: Given Y ∈ dom(θ00 ) then Y ∈ dom(θ) by definition of
θ00 , and so Y 6∈ B, because dom(θ) ∩ B = ∅ by hypothesis.
— dom(θ10 ) ∩ B = ∅: As σ is an mgu and σ . θ ] γ, then dom(σ) ⊆
dom(θ ] γ). Given Z ∈ B then Z 6∈ dom(θ), as dom(θ) ∩ B = ∅ by
hypothesis, and Z ∈
/ dom(γ) ⊆ F V (f (p) → r) which are fresh, so
Z 6∈ dom(σ). But then, as σθ10 = θ ] γ, Z ≡ Z(θ ] γ) ≡ Zσθ10 ≡ Zθ10 , so
Z 6∈ dom(θ10 ).
• Condition iii.2) vran(θ0 ) ∩ B = ∅. Remember θ0 = θ00 ] θ10 :
— vran(θ00 )∩B = ∅: Given Y ∈ dom(θ00 ) then Y θ00 ≡ Y θ by definition of θ00 .
As vran(θ) ∩ B = ∅ by hypothesis then it must happen var(Y θ) ∩ B = ∅,
so var(Y θ00 ) ∩ B = ∅.
— vran(θ10 ) ∩ B = ∅: As σθ10 = θ ] γ then we can assume dom(θ10 ) ⊆
vran(σ) ∪ (dom(θ ] γ) \ dom(σ)).
– Let X ∈ dom(θ10 ) ∩ vran(σ) be such that Xθ10 ≡ r[Z] with Z ∈ B.
We will see that this Z ∈ B can appear in Xθ10 without leading to contradiction. The intuition is, as vran(θ) ∩ B = ∅ and
vran(γ|vExtra(R) ) ∩ B = ∅, then every Z ∈ B must come from an appearance in e of the same variable, transmitted to e0 by the matching
substitution γ, and so transmitted to e00 by σ.
As X ∈ vran(σ) then there must exist Y ∈ dom(σ) such that Y 7−→σ
0
r1 [X]p 7−→θ1 r2 [s[Z]]p . But as σθ10 = θ ] γ then Y 7−→θ]γ r2 [s[Z]]p .
Then, Z ∈ vran(θ]γ), but Z ∈ B, vran(θ)∩B = ∅, vran(γ|vExtra(R) )∩
B = ∅, dom(γ) ⊆ F V (f (p) → s), so it must happen Z ∈ vran(γ|F V (p) ),
and as a consequence Y ∈ F V (p). Let o ∈ O(f (p)) (set of positions
in f (p)) be such that f (p)|o ≡ Y , then:
· ((f (t))σ)|o ≡ ((f (p))σ)|o ≡ ((f (p))|o )σ ≡ Y σ ≡ r1 [X]p .
· As f (t) 6∈ dom(γ), which are the fresh variables of the variant
of the program rule, ((f (t))θ)|o ≡ ((f (t))(θ ] γ))|o ≡ ((f (p))(θ ]
γ))|o ≡ ((f (p))|o )(θ ] γ) ≡ Y (θ ] γ) ≡ r2 [s[Z]]p
So, as X ∈ dom(θ10 ) then X 6∈ B and Z ∈ B has been introduced by
θ, but this is impossible as vran(θ) ∩ B = ∅.
– Let Y ∈ dom(θ) \ dom(σ) be. Then Y θ ≡ Y (θ ] γ) (as Y ∈ dom(θ),
Y (θ ] γ) ≡ Y σθ10 (as σθ10 = θ ] γ), Y σθ10 ≡ Y θ10 (as Y 6∈ dom(σ).
But then no variable in B can appear in Y θ10 ≡ Y θ as (dom(θ) ∪
vran(θ)) ∩ B = ∅.
– Let Y ∈ dom(γ) \ dom(σ) be. Then Y γ ≡ Y (θ ] γ) ≡ Y σθ10 ≡ Y θ10 ,
reasoning like in the previous case. As dom(γ) ⊆ F V (f (p) → s) it
can happen:
· Y 6∈ F V (f (p)): Then no variable in B can appear in Y γ because
vran(γ|vExtra(R) ) ∩ B = ∅ by the hypothesis.

Theory and Practice of Logic Programming

81

· Y ∈ F V (f (p)): Let Z ∈ B appearing in Y γ, then Z appears in
f (t), so it must happen Y ∈ dom(σ) because otherwise σ could
not be a unifier of f (t) and f (p). But this is a contradiction so
this case is impossible.
(LetIn) In this case eθ ≡ h(e1 θ, . . . , eθ, . . . , en θ) and e ≡ h(e1 , . . . , e, . . . , en ). Then
the let-rewriting step is
eθ ≡ h(e1 θ, . . . , eθ, . . . , en θ) →l let X = eθ in h(e1 θ, . . . , X, . . . , en θ) ≡ e0
with h ∈ Σ, eθ ≡ f (e0 ) —f ∈ F S— or eθ ≡ let Y = e01 in e02 , and X is a
fresh variable. Notice that eθ is a let-rooted expression or a f (e0 ) iff e is a letrooted expression or a function application, as θ ∈ CT erm. Then we can apply
a let-narrowing step:
e ≡ h(e1 , . . . , e, . . . , en )

l

σ

let X = e in h(e1 , . . . , X, . . . , en ) ≡ e00

with σ ≡  and θ0 ≡ θ. Then the conditions in Lemma 11 hold:
i) e00 θ0 ≡ (let X = e in h(e1 , . . . , X, . . . , en ))θ ≡
let X = eθ in h(e1 θ, . . . , Xθ, . . . , en θ) ≡
let X = eθ in h(e1 θ, . . . , X, . . . , en θ) ≡ e0 , since X is fresh an it cannot
appear in dom(θ0 ).
ii) σθ0 ≡ θ ≡ θ = θ[W].
iii) (dom(θ0 ) ∪ vran(θ0 )) ∩ B = (dom(θ) ∪ vran(θ)) ∩ B = ∅ by hypothesis.
(Bind) In this case eθ ≡ let X = tθ in e2 θ and e ≡ let X = t in e2 . Then
the let-rewriting step is let X = tθ in e2 θ →l e2 θ[X/tθ] with tθ ∈ CT erm. As
θ ∈ CT erm, if tθ ∈ CT erm then t ∈ CT erm, so we can apply a let-narrowing
step:
e ≡ let X = t in e2

l

σ

e2 [X/t] ≡ e00

with σ ≡  and θ0 ≡ θ. Then the conditions in Lemma 11 hold:
i) e00 θ0 ≡ e2 [X/t]θ. By the variable convention we can assume that X ∈
/
0
dom(θ) ∪ vran(θ), so by Lemma 1 e2 [X/t]θ ≡ e2 θ[X/tθ] ≡ e .
ii) and iii) As before.
(Elim) We have eθ ≡ let X = e1 θ in e2 θ, so e ≡ let X = e1 in e2 . Then the
let-rewriting step is eθ ≡ let X = e1 θ in e2 θ →l e2 θ with X ∈
/ F V (e2 θ). By the
variable convention (dom(θ) ∪ vran(θ)) ∩ BV (e) = ∅, so as X ∈ BV (e) then
X ∈
/ dom(θ) ∪ vran(θ). Then X ∈
/ F V (e2 θ) implies X ∈
/ F V (e2 ) and we can
apply a let-narrowing step:
e ≡ let X = e1 in e2

l

σ

e2 ≡ e00

with σ ≡  and θ0 ≡ θ. Then the conditions in Lemma 11 hold trivially.
(Flat) In this case eθ ≡ let X = (let Y = e1 θ in e2 θ) in e3 θ and e ≡ let X =
(let Y = e1 in e2 ) in e3 . The let-rewriting step is eθ ≡ let X = (let Y =
e1 θ in e2 θ) in e3 θ →l let Y = e1 θ in let X = e2 θ in e3 θ ≡ e0 with Y ∈
/ F V (e3 θ).

82

López-Fraguas et al.
By a similar reasoning as in the (Elim) case we conclude that Y ∈
/ dom(θ) ∪
vran(θ), so Y ∈
/ F V (e3 ). Then we can apply a let-narrowing step:
e ≡ let X = (let Y = e1 in e2 ) in e3

l

σ

let Y = e1 in let X = e2 in e3 ≡ e00

with σ ≡  and θ0 ≡ θ. Then the conditions in Lemma 11 hold trivially.
(Contx) Then we have e ≡ C[s]. By the variable convention (dom(θ) ∪ vran(θ)) ∩
BV (e) = ∅, so by lemma 25 eθ ≡ (C[s])θ ≡ Cθ[sθ], and the step was
eθ ≡ Cθ[sθ] →l Cθ[s0 ] ≡ e0 , because sθ →l s0
Then we know that the lemma holds for sθ →l s0 , by the proof of the other cases,
so taking W 0 = W ∪ F V (s) and B 0 = B (as BV (s) ⊆ BV (C[s])) we can do
s l σ2 s00 for some θ20 under the conditions stipulated. Now we can put this step
into (Contx) to do:
e ≡ C[s]

l

00
σ2 Cσ2 [s ]

≡ e00 taking σ = σ2 and θ0 = θ20

because if s l σ2 s00 was a (Narr) step which lifts a (Fapp) step that uses the fresh
variant (f (p) → r) ∈ P and adjusts with γ ∈ CSubst, then:
• dom(σ2 ) ∩ BV (C) = ∅: As σ2 = mgu(s, f (p)) then dom(σ2 ) ⊆ F V (s) ∪
F V (f (p)). As σ2 . θ ] γ and it is an mgu then dom(σ2 ) ⊆ dom(θ ] γ).
If X ∈ F V (s) ∩ dom(σ2 ) then X 6∈ dom(γ) ⊆ F V (f (p) → r), so it must
happen X ∈ dom(θ); but then X 6∈ BV (C) because dom(θ) ∩ BV (C) = ∅
by the variable convention.
Otherwise it could happen X ∈ F V (f (p)) ∩ dom(σ2 ), then X appears in
the fresh variant and so it cannot appear in C.
• vran(σ2 |\var(p) ) ∩ BV (C) = ∅: As dom(σ2 ) ⊆ F V (s) ∪ F V (f (p)) then we
have vran(σ2 |\var(p) ) = vran(σ2 |F V (s) ). But as σ2 = mgu(s, f (p)) then
vran(σ|F V (s) ) ⊆ F V (f (p)), which are part of the fresh variant, so every
variable in vran(σ2 |\var(p) ) is fresh and so cannot appear in C.
Then the conditions in Lemma 11 hold:
ii) σθ0 = θ[W]: Because W ⊆ W 0 , and σ2 θ20 = θ[W 0 ], by the proof of the other
cases.
i) e00 θ0 ≡ e0 : As BV (Cσ2 ) = BV (C), by the variable convention, BV (C) ⊆
BV (e) ⊆ BV (B), by the hypothesis, and (dom(θ20 ) ∪ vran(θ20 )) ∩ B = ∅,
by the proof of the other cases, then (dom(θ20 ) ∪ vran(θ20 )) ∩ BV (Cσ2 ) = ∅.
But then:
e00 θ0 ≡ (Cσ2 [s00 ])θ20 ≡ Cσ2 θ20 [s00 θ20 ] ≡ e0
| {z } |{z}
Cθ

s00 θ20

0

s0

Because we have
≡ s , by the proof of the other cases, and because
F V (C) ⊆ F V (e) ⊆ W and σ2 θ20 = θ[W], as we saw in the previous case
(remember σ = σ2 and θ0 = θ20 ).
iii) (dom(θ0 ) ∪ vran(θ0 )) ∩ B = ∅: Because θ0 = θ20 and the proof of the other
cases.

Theory and Practice of Logic Programming

83

The proof for any number of steps proceeds by induction over the number n of
n
steps of the derivation eθ →l e0 . The base case where n = 0 is straightforward, as
0
0
then we have eθ →l eθ ≡ e0 so we can do e l  e ≡ e00 , so σ =  and taking θ0 = θ
∗
the lemma holds. In the inductive step we have eθ →l e1 →l e0 , and we will try to
build the following diagram:
e

l
σ1

l∗
σ2

e002

l

e1

≡ e00

θ20 = θ0

θ1

θ
eθ

e001

∗
l

e0

By the previous proof for one step we have e l σ1 e001 and θ10 ∈ CSubst under the
conditions stipulated. In order to this with the IH we define the sets B1 = B∪BV (e1 )
and W1 = (W \ dom(σ1 )) ∪ vran(σ1 ) ∪ vE, where vE is the set of extra variables
in the fresh variant f (p) → s used in e l σ1 e001 , if it was a (Narr) step; or empty
otherwise. We also define θ1 = θ10 |W1 . Then:
• F V (e001 ) ∪ dom(θ1 ) ⊆ W1 : We have dom(θ1 ) ⊆ W1 by definition of θ1 . On the other
hand we have F V (e001 ) ⊆ W1 because given X ∈ F V (e001 ) we have two possibilities:
a) X ∈ F V (e)): then X ∈
/ dom(σ1 ) since otherwise it disappears in the step
e l σ1 e00 . As dom(θ) ∪ F V (e) ⊆ W then X ∈ W \ dom(σ1 ), so X ∈ W1 .
b) X ∈
/ F V (e)) : then there are two possibilities:
i) X has been inserted by σ1 , so X ∈ vran(σ1 ) and X ∈ W1 .
ii) X has been inserted as an extra variable in a (Narr) step. Since the narrowing substitution is a mgu then σ1 cannot affect X, so X ∈ W1 because
X ∈ vE.
• e001 θ1 ≡ e1 : Because as we have seen, F V (e001 ) ⊆ W1 , and so e001 θ1 ≡ e001 θ10 |W1 ≡
e001 θ10 ≡ e1 , by the proof for one step.
• BV (e001 ) ⊆ B1 : As θ10 ∈ CSubst, e001 θ10 ≡ e1 and no CSubst can introduce any binding
then BV (e1 ) = BV (e001 ). But B1 = B ∪ BV (e1 ), so BV (e001 ) = BV (e1 ) ⊆ B1 .
• (dom(θ1 ) ∪ vran(θ1 )) ∩ B1 = ∅: As θ10 ∈ CSubst, e001 θ10 ≡ e1 and no CSubst can
introduce any binding then BV (e1 ) = BV (e001 ). Then it can happen:
a) BV (e001 ) ⊆ BV (e): Then B = B1 , as BV (e1 ) = BV (e001 ) ⊆ BV (e) ⊆ B by
hypothesis. Then, as (dom(θ10 ) ∪ vran(θ10 )) ∩ B = ∅ by the proof for one step,
then (dom(θ10 ) ∪ vran(θ10 )) ∩ B1 = ∅, and so (dom(θ1 ) ∪ vran(θ1 )) ∩ B1 = ∅,
because θ1 = θ10 |W1 and so its domain and variable range is smaller than the
domain of θ10 .
b) BV (e001 ) ⊃ BV (e): Then e l σ1 e001 must have been a (LetIn) step and so σ = 
and θ10 = θ. As the new bounded variable Z is fresh wrt. θ then it is also fresh
for θ10 = θ, and so B1 = B ∪ {Z} has no intersection with dom(θ10 ) ∪ vran(θ10 )
nor with dom(θ1 ) ∪ vran(θ1 ), which is smaller.

84

López-Fraguas et al.

• σ1 θ1 = θ[W]: It is enough to see that σ1 θ1 = σ1 θ10 [W], because we have σ1 θ10 = θ[W]
by the proof for one step, and this is true because given X ∈ W:
a) If X ∈ dom(σ1 ) then F V (Xσ1 ) ⊆ vran(σ1 ) ⊆ W1 , so as θ1 = θ10 |W1 then
Xσ1 θ1 ≡ Xσ1 θ10 |W1 ≡ Xσ1 θ10 .
b) If X ∈ W \ dom(σ1 ) then X ∈ W1 by definition, and so Xσ1 θ1 ≡ Xθ1 (as
X 6∈ dom(σ1 )), Xθ1 ≡ Xθ10 |W1 ≡ Xθ10 (as X ∈ W1 ), and Xθ10 ≡ Xσθ10 (as
X 6∈ dom(σ1 )).
∗

So we have e001 θ1 ≡ e1 and e1 →l e0 , but then we can apply the induction
∗
hypothesis to e001 θ1 →l e0 using W1 and B1 , which fulfill the hypothesis of the
∗
lemma, as we have seen. Then we get e001 l σ2 e002 and θ20 ∈ CSubst under the
conditions stipulated. But then we have:
e

l

00
σ1 e1

l∗
σ2

e002 taking e00 ≡ e002 , σ = σ1 σ2 and θ0 = θ20

for which we can prove the conditions in Lemma 11:
i) e00 θ0 ≡ e0 : As e00 θ0 ≡ e002 θ20 ≡ e0 by IH.
ii) σθ0 = θ[W]: That is, σ1 σ2 θ20 = θ[W]. As we have σ1 θ1 = θ[W], as we saw before,
all that is left is proving σ1 σ2 θ20 = σ1 θ1 [W], which happens because given X ∈ W:
a) If X ∈ dom(σ1 ) then F V (Xσ1 ) ⊆ vran(σ1 ) ⊆ W1 , so as σ2 θ20 = θ1 [W1 ] by
IH, then (Xσ1 )σ2 θ20 ≡ (Xσ1 )θ1 .
b) If X ∈ W \ dom(σ1 ) then X ∈ W1 by definition, and so, as σ2 θ20 = θ1 [W1 ] by
IH, then Xσ1 σ2 θ20 ≡ Xσ2 θ20 (as X 6∈ dom(σ1 )), Xσ2 θ20 ≡ Xθ1 (as X ∈ W1 ),
Xθ1 ≡ Xσ1 θ1 (as X 6∈ dom(σ1 )).
iii) (dom(θ0 ) ∪ vran(θ0 )) ∩ B = ∅: That is (dom(θ20 ) ∪ vran(θ20 )) ∩ B = ∅, which happens
as (dom(θ20 ) ∪ vran(θ20 )) ∩ B1 = ∅ by IH and B ⊆ B1 .

A.10 Proofs for Section 7
The let-binding elimination transformation b satisfies the following interesting
properties, which illustrate that its definition is sound.
Lemma 33
For all e, e0 ∈ LExp, C ∈ Cntxt, X ∈ V we have:
i) |b
e| ≡ |e|.
ii) If e ∈ Exp then eb ≡ e.
iii) F V (b
e) ⊆ F V (e)
\
iv) e[X/e0 ] = eb[X/b
e0 ].

Theory and Practice of Logic Programming

85

Proof
i–iii) Easily by induction on the structure of e.
iv) A trivial induction on the structure of e, using Lemma 1 for the case when e has
the shape e ≡ let X = e1 in e2 .
Lemma 12 (Copy lemma)
For all e, e1 , e2 ∈ Exp, X ∈ V:
i) e1 → e2 implies e[X/e1 ] →∗ e[X/e2 ].
ii) e1 →∗ e2 implies e[X/e1 ] →∗ e[X/e2 ].
Proof
To prove i) we proceed by induction on the structure of e. Concerning the base
cases:
• If e ≡ X then e[X/e1 ] ≡ e1 → e2 ≡ e[X/e2 ], by hypothesis.
• If e ≡ Y ∈ V \ {X} then e[X/e1 ] ≡ Y →0 Y ≡ e[X/e2 ].
• Otherwise e ≡ h for some h ∈ Σ, so e[X/e1 ] ≡ h →0 h ≡ e[X/e2 ]
Regarding the inductive step, then e ≡ h(e01 , . . . , e0n ) and so
e[X/e1 ] ≡ h(e01 [X/e1 ], . . . , e0n [X/e1 ])
→∗ h(e01 [X/e2 ], . . . , e0n [X/e2 ])
≡ e[X/e2 ]

by IH, n times

The proof for ii) follows the same structure.
Lemma 13 (One-Step Soundness of let-rewriting wrt. term rewriting)
For all e, e0 ∈ LExp we have that e →l e0 implies eb →∗ eb0 .
Proof
We proceed by a case distinction over the rule of let-rewriting used in the step
e →l e0 .
(Fapp) Then we have:
e ≡ f (p)θ →l rθ ≡ e0 for some (f (p) → r) ∈ P, θ ∈ CSubst
b ≡ rθ, by Lemma 33
But then f (p)θ, rθ ∈ Exp, therefore f\
(p)θ ≡ f (p)θ and rθ
b ≡ eb0 , by a term rewriting
ii), and so we can link eb ≡ f\
(p)θ ≡ f (p)θ → rθ ≡ rθ
step.
(LetIn) Then we have:
e ≡ h(e1 , . . . , ek , . . . , en ) →l let X = ek in h(e1 , . . . , X, . . . , en ) ≡ e0
where X is a fresh variable (among other conditions). But then
eb0 ≡ h(e1 , . . \
. , X, . . . , en )[X/ebk ] ≡ h(eb1 , . . . , X, . . . , ec
n )[X/ebk ]
≡ h(eb1 , . . . , ebk , . . . , ec
n)
≡ h(e1 , . . \
. , ek , . . . , en ) ≡ eb
Therefore eb →0 eb ≡ eb0 .

as X is fresh

86

López-Fraguas et al.

(Bind) Then we have:
e ≡ let X = t in e1 →l e1 [X/t] ≡ e0 with t ∈ CT erm
b0
But then eb ≡ eb1 [X/b
t] ≡ e\
b →0 eb ≡ eb0 .
1 [X/t] ≡ e , by Lemma 33 iv), hence e
(Elim) Then we have:
e ≡ let X = e1 in e2 →l e2 ≡ e0 with X 6∈ F V (e2 )
But then
eb ≡ eb2 [X/eb1 ]
≡ e2\
[X/e1 ]
≡ eb2 ≡ eb0

by Lemma 33 iv)
as X 6∈ F V (e2 )

Therefore eb →0 eb ≡ eb0 .
(Flat) Then we have:
e ≡ let X = (let Y = e1 in e2 ) in e3 →l let Y = e1 in (let X = e2 in e3 ) ≡ e0
where Y ∈
/ F V (e3 ). But then
eb ≡ eb3 [X/let Y \
= e1 in e2 ] ≡ eb3 [X/(eb2 [Y /eb1 ])]
≡ eb3 [X/eb2 ][Y /eb1 ]
Y ∈
/ F V (eb3 ) by Lemma 33 iii)
0
b
\
≡ (let X = e2 in e3 )[Y /eb1 ] ≡ e
Therefore eb →0 eb ≡ eb0 .
(Contx) Then we have:
e ≡ C[e1 ] →l C[e2 ] ≡ e0
with e1 →l e2 by some of the previous rules, therefore eb1 →∗ eb2 by the proof of
∗ [
[
the previous cases. We will prove that eb1 →∗ eb2 implies C[e
1 ] → C[e2 ], thus
∗ b0
getting eb → e as a trivial consequence.
We proceed by induction on the structure of C. Regarding the base case then
∗
[
[
C ≡ [] and so C[e
1 ] ≡ eb1 → eb2 ≡ C[e2 ] by hypothesis. For the inductive step:
0 [e ] →∗ C
0 [e ], and so
\
\
• If C ≡ let X = C 0 in a then by IH we get C
1
2
0 [e ]]
[
\
C[e
a[X/C
1] ≡ b
1
0 [e ]] by IH and Lemma 12
\
→∗ b
a[X/C
2
[
≡ C[e
2]

Notice that it is precisely because of this case that we cannot say that e →l e0
0 [e ] made by
\
implies eb →∗ eb0 in zero or one steps, because the copies of C
1
0
\
the substitution [X/C [e1 ]] may force the zero or one steps derivation from
0 [e ] to be repeated several times in derivation b
0 [e ]] →∗ b
0 [e ]].
\
\
\
C
a[X/C
a[X/C
1
2
1
This is typical situation when mimicking term graph rewriting derivations
by term rewriting.
0
0 [e ][X/b
[
\
\
[
• If C ≡ let X = a in C 0 then C[e
a] →∗ C
a] ≡ C[e
1 ] ≡ C [e1 ][X/b
2
2 ], by
IH combined with closedness under substitutions of term rewriting.

Theory and Practice of Logic Programming

87

0
[
\
• Otherwise C ≡ h(a1 , . . . , C 0 , . . . , an ) and then C[e
c
1 ] ≡ h(ab1 , . . . , C [e1 ], . . . , a
n)
∗
0
\
[
→ h(ab1 , . . . , C [e2 ], . . . , ac
n ) ≡ C[e2 ] by IH.

Proposition 10
For all σ ∈ Subst⊥ , θ ∈ [[σ]], we have that θ E σ.
Proof
Given some X ∈ V, we have two possibilities. If X ∈ dom(θ) then taking any
t ∈ CT erm⊥ such that P `CRWL θ(X) _ t, by Lemma 5 we have t v θ(X),
because θ ∈ [[σ]] ⊆ CSubst⊥ . But θ ∈ [[σ]] implies P `CRWL σ(X) _ θ(X), therefore
P `CRWL σ(X) _ t by the polarity from Proposition 3, which holds for CRWL
too. Hence [[θ(X)]] ⊆ [[σ(X)]].
On the other hand, if X 6∈ dom(θ) then for any t ∈ CT erm⊥ such that P `CRWL
θ(X) ≡ X _ t we have that t ≡⊥ or t ≡ X. If t ≡⊥ then P `CRWL σ(X) _ t
by rule (B). Otherwise θ ∈ [[σ]] implies P `CRWL σ(X) _ θ(X) ≡ X ≡ t. Hence
[[θ(X)]] ⊆ [[σ(X)]].
Proposition 11
For all σ ∈ DSusbt⊥ , [[σ]] is a directed set.
Proof
For any preorder ≤, any directed set D wrt. it and any elements e1 , e2 ∈ D by
e1 tD e2 we denote the element e3 ∈ D such that e1 ≤ e3 and e2 ≤ e3 that must
exist because D is directed.
Now, given any σ ∈ DSubst⊥ we have that ∀X ∈ V, [[σ(X)]] is a directed set,
because if X ∈ dom(σ) then we can apply the definition of DSubst⊥ and otherwise
[[X]] = {X, ⊥}, which is directed. Now given θ1 , θ2 ∈ [[σ]] we can define θ3 ∈ CSubst⊥
as θ3 (X) = θ1 (X) tσ(X) θ2 (X), which fulfills:
1. θi v θ3 for i ∈ {1, 2}, because for any X ∈ V we have that [[σ(X)]] is directed
(as we saw above) and θi (X) ∈ [[σ(X)]] (because θ1 , θ2 ∈ [[σ]]), therefore θi (X) v
θ1 (X) tσ(X) θ2 (X) = θ3 (X) by definition.
2. θ3 ∈ [[σ]], because ∀X ∈ V, θ3 (X) = θ1 (X) tσ(X) θ2 (X) ∈ [[σ(X)]] by definition.

We will use the following lemma about non-triviality of substitution denotations
as an auxiliary result for proving Lemma 15.
Lemma 34
For all σ ∈ Subst⊥ we have that [[σ]] 6= ∅ and given X = dom(σ) then [X/ ⊥] ∈ [[σ]].
Proof
It is enough to prove that if X = dom(σ) then [X/ ⊥] ∈ [[σ]]. First of all [X/ ⊥] ∈
CSubst⊥ by definition. Now consider some Y ∈ V.
i) If Y ∈ X then σ(Y ) _⊥≡ Y [X/ ⊥], by rule (B).
ii) Otherwise Y 6∈ X = dom(σ), hence σ(Y ) ≡ Y _ Y ≡ Y [X/ ⊥], by rule (RR).

88

López-Fraguas et al.

Lemma 15
For all σ ∈ DSusbt⊥ , e ∈ Exp⊥ , t ∈ CT erm⊥ ,
if eσ _ t then ∃θ ∈ [[σ]] such that eθ _ t
Proof
We proceed by a case distinction over e:
• If e ≡ X ∈ dom(σ) : Then eσ ≡ σ(X) _ t, so we can define:

if Y ≡ X
 t
θ(Y ) =
⊥ if Y ∈ dom(σ) \ {X}

Y
otherwise
Then θ ∈ [[σ]] because obviously θ ∈ CSusbt⊥ , and given Z ∈ V.
a) If Z ≡ X then σ(Z) ≡ σ(X) _ t ≡ θ(Z) by hypothesis.
b) If Z ∈ (dom(σ) \ {X}) then σ(Z) _⊥≡ θ(Z) by rule (B).
c) Otherwise Z 6∈ dom(σ) and then σ(Z) ≡ Z _ Z ≡ θ(Z) by rule (RR).
But then eθ ≡ θ(X) ≡ t _ t by Lemma 5—which also holds for CRWL, because
CRWL and CRWLlet coincide for c-terms— , as t ∈ CT erm⊥ .
• If e ≡ X 6∈ dom(σ) : Then given Y = dom(σ) we have [Y / ⊥] ∈ [[σ]] by Lemma 34,
so we can take θ = {[Y / ⊥]} for which [[eσ]] = [[Xσ]] = [[X]] = [[X[Y / ⊥]]] = [[Xθ]].
• If e 6∈ V then we proceed by induction over the structure of eσ _ t:
Base cases
(B) Then t ≡⊥, so given Y = dom(σ) we can take θ = {[Y / ⊥]} for which
eθ _⊥ by rule (B).
(RR) Then e ∈ V and we are in the previous case.
(DC) Similar to the case for e ≡ X 6∈ dom(σ).
Inductive steps
(DC) Then e ≡ c(e1 , . . . , en ), as e 6∈ V, and we have:
e1 σ _ t1 . . . e n σ _ tn
DC
eσ ≡ c(e1 σ, . . . , en σ) _ c(t1 , . . . , tn ) ≡ t
Then by IH or the proof of the other cases we have that ∀i ∈ {1, . . . , n}. ∃θi ∈
[[σ]] such that ei θi _ ti . But as σ ∈ DSusbt⊥ then [[σ]] is directed by Lemma
11, therefore there must exist some θ ∈ [[σ]] such that ∀i ∈ {1, . . . , n}.θi v θ,
and so by Proposition 5 —which also holds for CRWL, by Theorem 4— we
have ∀i ∈ {1, . . . , n}.ei θ _ ti , so we can build the following proof:
e1 θ _ t1 . . . en θ _ tn
DC
eθ ≡ c(e1 θ, . . . , en θ) _ c(t1 , . . . , tn ) ≡ t

(OR) Very similar to the proof of the previous case. We also have e ≡ f (e1 , . . . , en )
(as e 6∈ V) and given a proof for eσ ≡ f (e1 , . . . , en )σ _ t, so we can apply the
IH or the proof of the other cases to every ei σ _ pi µ to get some θi ∈ [[σ]]

Theory and Practice of Logic Programming

89

such that ei θi _ pi µ. Then we can use Lemma 11 and Proposition 5 to use
the obtained θ to compute the same values for the arguments of f , thus using
the same substitution µ ∈ CSubst⊥ for parameter passing in (OR).

Theorem 19
Let P be a CRWL-deterministic program, and e, e0 ∈ Exp, t ∈ CT erm. Then:
∗

a) e →∗ e0 implies e →l e00 for some e00 ∈ LExp with |e00 | w |e0 |.
∗
b) e →∗ t iff e →l t iff P `CRWL e _ t.
Proof
a) Assume e →∗ e0 . By Lemma 16, [[e0 ]] ⊆ [[e]] and by Lemma 5 we have |e0 | ∈ [[e0 ]], then
∗
|e0 | ∈ [[e]]. Therefore, by Theorem 12 there exists e00 ∈ LExp such that e →l e00
with |e00 | w |e0 |.
∗
∗
b) The parts e →l t iff P `CRWL e _ t, and e →l t implies e →∗ t have been already
proved for arbitrary programs in Theorems 12 and 17 respectively. What remains
∗
to be proved is that e →∗ t implies e →l t (or the equivalent P `CRWL e _ t).
Assume e →∗ t. Then [[t]] ⊆ [[e]] by Lemma 16. Now, by Lemma 5 t ∈ [[t]], and
therefore t ∈ [[e]], which exactly means that P `CRWL e _ t.

