The Unfolding Semantics of Functional
Programs

arXiv:1708.08003v1 [] 26 Aug 2017

José M. Rey Poza and Julio Mariño
School of Computer Science,
Universidad Politécnica de Madrid
josem.rey@gmail.com, jmarino@fi.upm.es

Abstract. The idea of using unfolding as a way of computing a program
semantics has been applied successfully to logic programs and has shown
itself a powerful tool that provides concrete, implementable results, as its
outcome is actually source code. Thus, it can be used for characterizing
not-so-declarative constructs in mostly declarative languages, or for static
analysis. However, unfolding-based semantics has not yet been applied to
higher-order, lazy functional programs, perhaps because some functional
features absent in logic programs make the correspondence between execution and unfolding not as straightforward. This work presents an unfolding semantics for higher-order, lazy functional programs and proves
its adequacy with respect to a given operational semantics. Finally, we
introduce some applications of our semantics.
Keywords: Semantics, Unfolding, Functional Programming.

1

Introduction

The broad field of program semantics can be classified according to the different
meanings intended to be captured or the various techniques employed. Thus,
traditionally, the term denotational semantics is used when a high-level, implementation independent description of the behaviour of a program is pursued,
while operational semantics usually refers to descriptions intended to capture
more implementation-related properties of the execution of a program, which
can then be used to gather resource-aware information, or as a blueprint for
actual language implementations.
The inability of those denotational semantics to capture certain aspects of
logic programs (such as the computed answer semantics) and the introduction of
“impure” constructs in Prolog, led to a considerable amount of proposals for alternative semantics of logic programs during the 80’s and 90’s. One of the most
remarkable proposals is the so-called s-semantics approach [4] which explores
the possibility of using syntactic denotations for logic programs. In other words,
programs in a very restricted form are the building blocks of the denotation,
and program transformation (e.g. via unfolding) takes the role of interpretation transformers in traditional constructions. Being closer to the source code
facilitates the treatment of the less declarative aspects.

2
Prolog code / s-semantics unfolding

Functional code / Funct. unfolding

add (zero ,X,X).
add Zero x = x
add (suc (X),Y, suc (Z)):−add (X,Y,Z). add (Suc x) y = Suc (add x y)

S1 = {add(zero,X,X)}
S2 = {add(zero,X,X),
add(suc(zero),X2 ,suc(X2 ))}

I0 = ∅
I1 = {add Zero x = x}
I2 = {add Zero x = x,
add (Suc Zero) y = (Suc y) }

Fig. 1. Logic and functional versions of a simple program, and their unfoldings.

However, in spite of the fact that unfolding is a technique equally applicable
to functional programs, little attention has been paid to its use as a semantics tool. Investigating how unfolding can be applied to find the semantics of
functional programs is the goal of this paper.
1.1

Unfolding Semantics

The process of unfolding is conceptually simple: replace any function or predicate
invocation by its definition. In logic programming this amounts to unifying some
literal in the body of a rule with the head of some piece of knowledge that has
already been calculated, and placing the corresponding body instance where the
literal was.
The previous paragraph mentions two important concepts: the first is that
of piece of knowledge generated by unfolding program rules according to all
current pieces of knowledge. Every piece of knowledge (called a fact) is valid
source code. The set of facts may increase with every iteration. A set of facts is
called an interpretation. In addition, the second concept hinted in the paragraph
above is that of initial interpretation.
Unfolding in Logic Programming. As an example, the left half of Fig. 1
shows a predicate called add that adds two Peano Naturals. This part shows
the source code (upper side) together with the corresponding unfolding results
(lower side).
The general unfolding procedure can be easily followed in the example, where
the first two clause sets are generated (S1 and S2 ).
Unfolding in Functional Programming. Unfolding in functional programming (FP) follows the very same idea of unfolding in logic programming: any
function invocation is replaced by the right side of any rule whose head matches
the invocation.
Consider the right half of Fig. 1 as the functional version of the previous
example, written in our model language. Some differences and analogies between

3
Functional code
ite : Bool → a → a → a
ite True t e = t
ite False t e = e
filter :(a→Bool )→[a]→[a]
filter p [] = []
filter p (x:xs) =
ite (p x)
(x:( filter p xs ))
( filter p xs)

Unfolding
I0 = ∅
I1 = {ite(True,t,e) = t, ite(False,t,e) = e,
filter(b,Nil) = Nil}
I2 = {ite(True,t,e) = t, ite(False,t,e) = e,
filter(b,Nil) = Nil,
filter(b,Cons(c,Nil))|
snd(match(True,b@[c]))=Cons(c,Nil),
filter(b,Cons(c,Cons(d,e)))|
snd(match(True,b@[c]))=Cons(c,Bot),
filter(b,Cons(c,Nil))|
snd(match(False,b@[c])) = Nil
filter(b,Cons(c,Cons(d,e)))|
snd(match(False,b@[c]))=Bot}

Fig. 2. Functional program requiring higher-order applications.

both paradigms can be spotted: In FP, unfolding generates rules (equations) as
pieces of knowledge, instead of clauses which appeared in logic programming.
The starting seed is also different: bodyless rules are used in logic programming
while the empty set is used in functional programming.
Finally, observe that both unfoldings (logic and functional) produce valid
code and analogous results, being In equivalent to Sn . This fact provides a clue
into two of the main reasons to define an unfolding semantics: first they are
implementable as the procedure above shows and, second, they are also a clear
point between denotational and operational semantics in proving the equivalence
between a semantics of each type.
1.2

Extending Unfolding Semantics to Suit Functional Programs

Section 1.1 showed that the ideas of unfolding semantics in logic programming
can also be applied to FP. However, some features of FP (e.g. higher-order,
laziness) render the unmodified procedures invalid.
Consider the function filter in Fig. 2. It takes a list of values and returns
those values in the list that satisfy a predicate passed as its first argument.
Applying naı̈ve unfolding to filter is impossible since ite (short for if-thenelse) demands a boolean value but both p and x are unknown at unfold time
(i.e. before execution).
In order to overcome this limitation, we have developed a technique capable
of generating facts in the presence of incomplete information. In this case we
generate conditional facts (the last four facts in I2 ). The function match checks
whether a given term matches an expression that cannot be evaluated at unfolding time (here, (p x)). Observe that match must be ready to deal with infinite
values in its second argument.
Note that, in automatically-generated code, such as the unfolded code shown
in Fig. 2 and the figures to come, variables are most often renamed and that our
unfolding implementation uses tuples to represent curried expressions.

4

1.3

Related Work

One of the earliest usages of unfolding in connection to semantics is due to Scott
[9], who used it to find the denotation of recursive functions, even though the
word unfolding was not used at the time.
Concerning logic programming, our main inspiration source is s-semantics
[4], which defines an unfolding semantics for pure logic programs that is defined
as the set of literals that can be successfully derived by using the program given.
In addition, fold and unfold have been used in connection to many other
problems in the field of logic programming. For example [7] describes a method
to check whether a given logic program verifies a logic formula. It does this by
applying program transformations that include fold and unfold.
Partial evaluation of logic programs has also been tackled by means of unfolding but it usually generates huge data structures even for simple programs.
As in logic programming, fold/unfold transformations have been used extensively to improve the efficiency of functional programs [5], but not as a way of
constructing a program’s semantics.
Unfolding has also been applied to functional-logic programming [1]. However, that paper is not oriented towards finding the meaning of a program but
to unfold it partially to achieve some degree of partial evaluation. Besides, it is
restricted to first order, eager languages.
Paper Organization Section 2 presents preliminary concepts. Section 3 describes
the unfolding semantics itself, the core of our proposal. Section 4 presents the
formal meaning we want to assign to the core language that we will be using.
Section 5 points out some applications of unfolding semantics. Section 6 concludes.

2

Preliminaries

Notation Substitutions will be denoted by σ, ρ, µ. σ(e) or just σe will denote the
application of substitution σ to e. The empty substitution will be denoted by ǫ.
e ≡ e′ will denote that the expressions e and e′ have the same syntax tree.
Given a term t, a position within t is denoted by a dot-separated list of integers. t|o denotes the content of position o within t. Replacement of the content
at position o within a term t by some term t′ is denoted by t[t′ ]|o . The set of
positions within an expression e will be denoted by Pos(e).
k, d will be used to denote constructors while c will denote guards.
The auxiliary functions fst : a×b → a and snd : a×b → b extract the first and
second element of a tuple, respectively. Boolean conjunction and disjunction are
denoted by ∧ and ∨. mgu(f t1 . . . tn , f e1 . . . en ) (where the tj are terms and ei do
not have user-defined functions) denotes its most general unifier. The conditional
operator will denoted by ◮, which has type (◮) : Bool → a → a and is defined
as: (True ◮ a) = a, (False ◮ a) = ⊥s .
Regarding types, A →
p
B denotes a partial function from domain A to
domain B. The type of π-interpretations (sets of facts) is noted by Set (F ). F

5

is intended to denote the domain from which facts are drawn. The projection
of an interpretation I to predefined functions only is denoted as Ip . Lack of
information is represented by ⊥s in unfolding interpretations and by the wellknown symbol ⊥ when it is related to the minimum element of a Scott domain.
Lastly, HNF stands for head normal form. An expression is said to be in head
normal form if it is a variable or its root symbol is a constructor. Normal form
(NF) terms are those in HNF, and whose subterms are in NF.
2.1

Core Language. Abstract Program Syntax

The language1 that will be the base to develop this work is a functional language
with guarded rules. Guards (which are optional) are boolean expressions that
must be rewritten to True in order for the rule that contains it to be applicable.
Note that the language we are using is a purely functional language (meaning
that it uses pattern matching,higher-order features and referential transparency).
Let us consider a signature Σ = hVΣ , DC Σ , FS Σ , PF Σ i where V is the set
of variables, DC is the set of Data Constructors that holds at least ⊥s and a
tuple-building constructor, FS holds the user-defined functions and PF denotes
the set of predefined functions that holds at least a function match, a function
nunif and a function @ that applies an expression e to a list of expressions (that
is, e@[e1 , . . . , en ] represents (e e1 . . . en )). PF and FS are disjoint.
Some of the sets above depend on the program P under study, so they should
be denoted as, e.g., FS P but we will omit that subscript if it is clear from the
context. All these sets are indexed by arity. The domains for a program are:
(Variables)
V ::= x, y, z, w . . .
(Terms)
T ::= v | k t1 . . . tk
(Expressions)
E ::= t | f ′ e1 . . . ek
(Patterns)
Pat ::= f t1 . . . tk
(Rules)
Rule ::= l | g = r
(Programs)
P ::= Set (Rule)

v ∈ V, k ∈ DC , ti ∈ T
f ′ ∈ FS ∪ PF , t ∈ T, ei ∈ E
f ∈ FS , ti ∈ T
l ∈ Pat , g ∈ E, r ∈ E

Terms are built with variables and constructors only. Expressions comprise terms
and those constructs that include function symbols (predefined or not).
Note that the description corresponding to expressions (E) does not allow
for an expression to be applied to another expression but we still want our
language to be a higher order one. We manage higher order by means of partial
applications, written by using the predefined function @. Thus, un application
like e1 e2 (where e1 and e2 are arbitrary expressions) is represented in our setting
by e1 @[e1 ] (or by @(e1 ,[e2 ]) in prefix form).
To ensure that programs defined this way constitute a confluent rewriting
system, these restrictions will be imposed on rules [6]: linear rule patterns, no
free variables in rules (a free variable is one that appears in the rule body but
1

We assume the core language to be typed although we do not develop its typing
discipline here because of lack of space.

6

not in the guard or the pattern) and finally, no superposition among rules (i.e.
given a function application, at most a rule must be applicable).
The core language does not include local declarations (i.e. let, where) but
this does not remove any power from the language since local declarations can
be translated into aditional rules by means of lambda lifting.

3
3.1

Unfolding Semantics for the Core Language
Interpretations

Definition 1 (Fact and π-Interpretation). We will use the word fact to
denote any piece of proven knowledge that can be extracted from a program P
and which conforms to the following restrictions: (i) They have shape h | c = b,
(ii) b and c include no symbols belonging to FS , (iii) Predefined functions are
not allowed inside b or c unless the subexpression headed by a symbol in PF
cannot be evaluated further (e.g. x + 1 would be allowed in b or c but 1 + 1 would
not, 2 should be used instead) and (iv) The value of c can be made equal to True
(by giving appropriate values to its variables). The type of facts is denoted F .
Facts can be seen as rules with a restricted shape.
In addition, a π-interpretation is any set of valid facts that can be generated
by using the signature of a given program P . The concept of π-interpretation has
been adapted from the concept with the same name in s-semantics.
The reason for imposing these restrictions on facts is to have some kind of
canonical form for interpretations. Even with this restrictions, a program does
not have a unique interpretation, but we intend to be as close to a canonical
form for interpretations as possible.

3.2

Defining the Unfolding Operator

The process we are about to describe is represented in pictorial form in the
Appendix, Sect. A in order to help understand the process as a whole.
The unfolding operator relies on a number of auxiliary functions that are described next, together with the operator itself. A full example aimed at clarifying
how these functions work can be found in the Appendix (Example 3).

Evaluation of Predefined Functions The function eval (Fig. 3) is in charge
of finding a value for those expressions which do not contain any full application
of user-defined functions. Since predefined functions do not have rules, their
appearances cannot be rewritten, just evaluated. Only predefined functions are
evaluated; all the other expressions are left untouched. Note that eval requires
the interpretation in order to know how to evaluate predefined functions.

7
eval : Set (F) × E → E
eval (I, x)
eval (I, (k e1 . . . en ))
eval (I, (k e1 , . . . , en ))
eval(I, (p e1 . . . en ))

eval (I, (c1 ∧. . .∧ci−1 ∧
snd (match(p, e))∧
ci+1 ∧ . . . ∧ cn ◮ e′ ))
eval (I, (x e1 . . . em ))
eval (I, (p e1 . . . em ))
eval (I, (f e1 . . . em ))

=x
= (k e′1 . . . e′n )
= (k e1 . . . en )
= (Ip e′1 . . . e′n )

x∈V
(k ∈ DC , n ≥ 0, arity (k) = n, eval (I, ei ) = e′i )
(k ∈ DC , n ≥ 0, n < arity (k))
if (p e′1 , . . . , e′n ) can be evaluated to NF
without error. It is left untouched otherwise.
(eval (I, ei ) = e′i , p ∈ PF − {match }).

=

σ(c1 ∧ . . . ∧ ci−1 ∧ b ∧ ci+1 ∧ . . . ∧ cn ◮ e′ )

= (x e1 . . . em )
= (p e1 . . . em )
= (f e1 . . . em )

if match(p, e) = (σ, b).
(x ∈ V )
p ∈ PF o , m < o.
f ∈ FS n , m ≤ n

Fig. 3. Evaluation of predefined functions

Housekeeping the Fact Set Every time a step of unfolding takes place, new
facts might be added to the interpretation. These new facts may overlap with
some existing facts (that is, be applicable to the same expressions as the existing
ones). Although overlapping facts do not alter the meaning of the program, they
are redundant and removing them makes the interpretation smaller and more
efficient. The function clean removes those redundancies. We believe this cleaning
step is a novel contribution in the field of unfolding semantics for functional
languages (see [2], where a semantics for logic functional programs is presented
but where interpretations are not treated to remove any possible overlapping).
Given an interpretation, the function clean removes the overlapping pairs in
order to erase redundant facts. Before defining clean, some definitions are needed.
Definition 2 (Overlapping Facts). A fact h | c = b overlaps with some other
fact h′ | c′ = b′ if the following two conditions are met:
– There exists a substitution µ such that: h ≡ µ(h′ ) and
– The condition c ∧ µ(c′ ) is satisfiable2 .
Intuitively, two facts overlap if there is some expression that can be rewritten
by using any of the facts.
What clean does is to remove any overlapping between facts from the interpretation it receives as argument. It does this by conserving the most specific fact
of every overlapping fact set untouched while restricting the other facts of the
set so that the facts do not overlap any more. This restriction is accomplished
by adding new conditions to the fact’s guard.
In order to be able to state that a fact is more specific than some other, we
need an ordering:
2

Note that satisfiability is undecidable in general. This means that there might be
cases where clean is unable to remove overlapping facts.

8

Definition 3 (Term and Fact Ordering). Let us define t ⊑ t′ (t, t′ ∈ E),
(t, t′ ) linear or µ(t) = σ(t′ ) for some substitutions µ, σ:
–
–
–
–

⊥s ⊑ t t ∈ T
t ⊑ x t ∈ T, x ∈ V
t1 . . . tn ⊑ t′1 . . . t′n if and only if ti ⊑ t′i ∀i : 1..n
(k t1 . . . tn ) ⊑ (k t′1 . . . t′n ) if and only if ti ⊑ t′i ∀i : 1..n, k ∈ DC ∪ PF

Now, this ordering can be used to compare facts.
Given two overlapping facts F ≡ f t1 . . . tn | c = b and F ′ ≡ f t′1 . . . t′n | c′ =
′
b , it is said that F ′ is more specific than F if and only if at least one of the
following criteria is met:
– t′1 . . . t′n ❁ t1 . . . tn or
– If t′1 . . . t′n and t1 . . . tn are a variant of each other (i.e., they are the same
term with variables renamed), the fact that is more specific than the other is
the one with the most restrictive guard (a guard c′ is more restrictive than
another guard c if and only if c′ entails c but not viceversa).
– If two facts are such that their patterns are a variant of each other and their
guards entail each other, the fact that is more specific than the other is the
one with the greatest body according to ⊑.
Remember that facts’ bodies do not contain full applications of user-defined
functions, so ⊑ will never be used to compare full expressions. However, ⊑ may
be used to compare expressions with partical applications or with predefined
functions. In these cases, function symbols (both from FS or from PF ) must be
treated as constructors. Note that, in a program without overlapping rules, the
bodies of two overlapping facts are forced to be comparable by means of ⊑.
Definition 4 (Function clean).
Given a fact F belonging to an interpretation I, let us define the set SIF =
{Fi ≡ f ti1 . . . tin | ci = bi ∈ I such that F overlaps with Fi and Fi
is more specific than F (i : 1..m)}.
Considering the set SIF for every fact F ∈ I, we can define clean (whose type
is Set (F ) → Set (F )) as:
clean(I) = I − I ⊥ − I O ∪
[
[f t1 . . . tn | c ∧
F ′ ≡(f t1 ...tn |c=b)∈I O

^
∀Fi ∈SIF

(nunif ((t1 , . . . , tn ), (ti1 , . . . , tin )) ∨ not (ci )) = b]
′

(Fi ≡ f ti1 . . . tin |ci = bi )
(1)
where − stands for set subtraction and:
– I ⊥ = {l = ⊥s such that (l = ⊥s ) ∈ I}. clean removes all the facts that are
identically ⊥.

9
nunif : T × T → Bool
nunif (x, t) = nunif (t, x)
=
nunif (k, d)
=
nunif (k, k)
=
nunif ((p1 , p2 ), (p3 , p4 ))
=
nunif (k(. . .), k′ (. . .))
=
nunif (k(p1 , . . . , pn ), k(p′1 , . . . , p′n ))=

False
True
False
nunif (p1 , p3 ) ∨ nunif (p2 , p4 )
True
nunif (p1 , p′1 ) ∨ . . . ∨ nunif (pn , p′n )

t ∈ T, x ∈ V
k, d ∈ DC , k 6= d
k ∈ DC
Tuples
k 6= k′
k ∈ DC

Fig. 4. Lack of unification between patterns: function nunif

′

– I O = {F ′ ∈ I such that SIF 6= ∅}. All the facts F ′ in I which are overlapped
by some more specific fact are removed from I and replaced by the amended
′
fact shown above which does not overlap with any fact in SIF .
The function nunif (Fig. 4) denotes lack of unification between its arguments.
Under some conditions clean will not add new facts to the given interpretation. This will happen if the guards for the facts under the big ∪ in Eq. 1 are
unsatisfiable. If the program under analysis meets certain properties, this is sure
to happen. Two definitions are needed to define those properties:
Definition 5 (Complete Function Definition). A function definition for
function f written in the core language is said to be complete if and only if for
any well typed, full application f t1 . . . tn of f , where the ti are terms there is a
rule f p1 . . . pn |g = r that can be used to unfold that application (that is, there
exists a substitution σ such that σ(t1 , . . . , tn ) = (p1 , . . . , pn ) and σ(g) satisfiable).
Definition 6 (Productive Rule). A program rule is said to be productive if
at least one fact which is not equal to the unguarded bottom (⊥s ) is generated by
unfolding that rule at some interpretation Im (m finite).
clean will not add new facts if all the function definitions in the program are
complete and all the rules in the program are productive. The following Lemma
states this. Note that the conditions mentioned are sufficient but not necessary.
Lemma 1 (When Can clean Drop Facts). Let P be a program without
overlapping rules, whose function definitions are all complete and whose rules
are all productive. Then:
For every fact H ≡ f t1 . . . tn | c = b ∈ In which is a result of unfolding the
rule Λ ≡ f s1 . . . sn | g = r, there exist in In+1 some facts which are also the
result of unfolding Λ which cover all the invocations of f covered by H.
The proof for this Lemma can be found in the Appendix.
We will be using the simplified version of clean whenever the program under
analysis meets the criteria that have been just mentioned.
To finish this section, let us state a result that justifies why it is legal to use
clean to remove overlapping facts.

10
match : T × E → (V →
p E) × E
match(x, e)
= ({x ← e}, True)
match(t, ⊥s )
= ({}, False)
match(t, (f e1 . . . en )) = (σh′ , c′h ∧ b′h )
match(k, k)
= ({}, True)
match((k . . .), (k′ . . .))= ({}, False)
match((k t1 . . . tn ),
(k e1 . . . en ))
= (σ1 ◦ · · · ◦ σn ,
b1 ∧ . . . ∧ bn )
match(t, (f e1 . . . en )) = ({}, False)
match(t, x)
= ({x ← t}, True)

x∈V
t ∈ T, f ∈ FS ∪ PF , hnf ((f e1 . . . en )) =
c′h ◮ e′h . match(t, e′h ) = (σh′ , b′h ).
(k ∈ DC )
(k, k′ ∈ DC , k 6= k′ )

(ti ∈ T, k ∈ DC , match(ti , ei ) = (σi , bi ))
(f ∈ FS m ∪ PF m , m > n)
(t ∈ T, x ∈ V )

Fig. 5. Function match.
umatch : T × E → (V →
p E) × E
umatch(t, e) = (σ, True)
if there exists some unifying σ such that σ(t) ≡ e
.
umatch(t, e) = (σ, snd(match(t|o , e|o )) ∧ c)
if e and t do not unify because there is at least a position o such that e|o is headed
by a symbol of PF (including @) and t|o is not a variable. umatch(t, e[(t|o )]|o ) = (σ, c).
if e and t do not unify but this is not due to a predefined
umatch(t, e) = (ǫ, False)
function symbol in e.
Fig. 6. umatch: Generation of matching conditions.

Lemma 2 (Programs without Overlappings). The fixpoint interpretation
(namely, Iω = UP∞ (I⊥ ) where U is the unfolding operator that will be presented
later) of any program P without overlapping rules cannot have overlappings. I⊥
is the empty interpretation.
The proof for this Lemma can be found in the Appendix.
Lazy Matching of Facts and Rules The unfolding process rewrites userdefined function applications but predefined functions (including partial application) will be left unaltered by the unfolding steps since there are no rules for
them. This means that when a match is sought to perform an unfolding step, the
arguments to the user-defined functions may include predefined functions that
must be evaluated before it is known whether they match some pattern. Such
applications may also generate infinite values. Thus, we need a function match3
that lazily matches a pattern to an expression.
Recall Fig. 2. The unfolding operator generates facts containing match whenever it finds a subexpression headed by a symbol in PF that needs to be matched
against some rule pattern. These special facts can be thought as imposing assumptions on what the pattern must be like before proceeding.
3

Note that match is similar to operator =:<= proposed in [3].

11

Those assumptions are included inside the fact’s guard. Two functions are
needed in connection to those assumptions: umatch (Fig. 6) 4 generates them as
a conjunction of calls to match (Fig. 5) which performs the matches at runtime.
umatch and match must be distinguished: umatch fits facts’ heads into expressions for unfolding while match is not an unfolding function; it is a function
used to check (at runtime) whether certain conditions are met in evaluated expressions. umatch does not call match: umatch generates code that uses match.
The function hnf, used in the definition for match, receives an expression and
returns that expression evaluated to Head Normal Form. hnf has type E → E.
In the result of umatch, σ is a list of assignments assigning values to variables
inside the arguments Vpassed to umatch and the right part of the result is a
condition of the form i snd(match(pi , ei )) where the pi are patterns and the ei
are expressions without symbols of FS (they have been removed by unfolding).
The function match returns whether that matching was possible and a list
of assignments from variables to expressions. The rules of match are tested from
the first to the last, applying the first suitable one only.
Both lists of assignments (the ones returned by umatch or match) are not
exactly substitutions because variables can be assigned to full expressions (not
just terms) but they behave as such.
Two remarks must be made about match: (i) The first element of the pair
returned by match is never used inside the definitions given in this paper because
it is only used in order to bind variables at runtime (not at unfolding time).
Those bindings will occur when a guard containing calls to match is evaluated.
(ii) Therefore, match is not purely functional (i.e., it is not a side effect-free).
Example 1. (How umatch works.) Code that generates a situation like the one
described is the one in Fig. 7 left. Part of its unfolding appears in Fig. 7 right 5 .
When the rule for app first is unfolded, it is found that (f n) cannot be
unfolded any more but it still does not match (x:xs) (the pattern in first’s rule).
Therefore, the second rule for umatch imposes the assumption in the resulting
fact that (f n) must match (x:xs) if the rule for app first is to be applied. Note
that f@[n] (f applied to variable n) generates an infinite term in this case. This
is why match cannot be replaced by strict equality. Example 2 in the Appendix
(Sect. C) shows how unfolding behaves when infinite structures are generated.
Unfolding Operator Operator U (I) (short form for UP (I)) where I is a πinterpretation is defined as shown in Fig. 8.
Given a program P, its meaning is given by the least fixed point of UP or by
Iω (= UP∞ (I⊥ )) if the program has infinite semantics.
The auxiliary function unfold, that unfolds a rule using the facts in an interpretation, is defined in Fig. 9. The behaviour of unfold can be described as
4

5

Observe that a function like umatch is not needed in pure Prolog since every atom
is guaranteed to have a rule and lack of instantiation will cause a runtime error.
The variables in the unfolder’s output have been renamed to ease understanding.

12
a) Code that Needs Matching b) Unfolding of the Source Code
from n :: Int→[Int ]
∗ first(Cons (x,xs)) = x
from n n = n:( from n (n+1)) ∗ from n (n) =
Cons (n,Cons (n+1, Bot ))
first ::[ a]→a
∗ app first (f,n) |
first (x:xs) = x
snd ( match( Cons (x,xs),f@[n]))= x
app first :: (a→[b])→a→ b Note: Any code preceded by * in every line has
app first f n = first(f n) been generated by our Prolog-based unfolder. The
unfolder uses Prolog terms to represent functional
main :: Int→Int
applications. That is why the unfolder uses tuples
main n= app first from n n to represent curried applications.

Fig. 7. Lazy matching of terms and rules.
I0 = I0⊥ = ∅
⊤
Im+1 = U
S(Im ) = clean(Im+1 )
⊤
⊥
Im+1 = Λ∈Rules (unfold (Λ, Im ∪ Im
)) ∪ Im
⊥
s
s
⊤
Im+1 = {l = ⊥ such that (l = ⊥ ) ∈ Im+1
}
Fig. 8. Unfolding operator

follows: unfold receives a (partially) unfolded rule (a pseudofact) which is unfolded by means of recursive calls. When the input to unfold has no invocations
of user defined functions, it is just returned as it is (case 1). Otherwise, the
pseudofact is unfolded by considering all the facts and positions o which hold
an invocation of a user-defined function (Case 2a). Those positions occupied by
user-defined function calls which cannot be unfolded are replaced by ⊥s (case
2b). unfold returns all the possible facts obtained by executing this procedure.
When performing the unfolding of a program, unfold behaves much like the
rewriting process in a TRS (i.e., it tries all the possible pairs hposition o, facti).
To summarize, ⊥s and match are the two enhancements required to write valid
code for unfolding functional programs. If eager evaluation is used, these enhancements would not be necessary but naı̈ve unfolding would still fail to work.

4

Operational Semantics

The operational semantics that describes how ground expressions written in the
kernel language are evaluated is shown in Fig. 10. The semantics defines a small
step relationship denoted by ❀. The notation e ❀ e′ means that the expression e
can be rewritten to e′ . The reduction relation (p e1 . . . en ) ❀p t (p ∈ PF ) states
that p e1 . . . en can be rewritten to t by using the definition of the predefined
function p.
The unfolding and operational semantics are equivalent in the following sense
for any ground expression goal : goal ❀∗ e′ ↔ e′ ∈ ueval (I∞ , goal ) where ❀∗ is

13
unfold : Rule × Set (F) → Set(F)
unfold (l | g = r, Im ) =


{l | eval (Im , g) = eval (Im , r)} if g and r have no total apps. of user funcs.









{(h′′ | c′′ = b′′ ) such that (h′′ | c′′ = b′′ ) ∈





unfold (σ(l) | eval (Im , σ(ghbj iko ∧ cj ∧ c′m )) = eval (Im , σ(rhbj iko )), Im )





∀o ∈ Pos(r) ∪ Pos(g), r|o (resp. g|o ) = f e1 . . . en , f ∈ FS n



 ∀(f t . . . t | c = b ) ∈ I such that
1
n
j
j
m
′
′
′
′

umatch((t
,
.
.
.
,
t
),
(e
,
1
n

1 . . . , en )) = (σ, cm ) and cm satisfiable




∪





unfold (l | eval (Im , gh⊥s iko ) = eval (Im , rh⊥s iko ), Im )





∀o ∈ Pos(r) ∪ Pos(g), r|o (resp. g|o ) = f e1 . . . en , f ∈ FS n




 ∄(f t1 . . . tn | cj = bj ) ∈ Im such that



umatch((t1 , . . . , tn ), (e′1 , . . . , e′n )) = (σ, c′m ) and c′m satisfiable}

A position is unfoldable:
Case 2a):
Some facts fit position o

Case 2b):
No facts fit position o

where:

– e′i = eval (Im , ei ) ∀i : 1..n
– ghtiko = g[t]|o if o ∈ Pos(g) and ghtiko = g otherwise.
– rhtiko = r[t]|o if o ∈ Pos(r ) and rhtiko = r otherwise.
Fig. 9. Unfolding of a program rule using a given interpretation

the transitive and reflexive closure of ❀ and e′ is in normal form according to
❀, ueval is a function that evaluates expressions by means of unfolding and I∞
is the limit of the interpretations found by repeatedly unfolding the program.
This equivalence is proved in the Appendix, Sect. B.3.
Note that this semantics is fully indeterministic; it is not meant to be used
in any kind of implementation and its only purpose is to serve as a pillar for
the demonstration of equivalence between the unfolding and an operational semantics. Therefore, the semantics is not lazy or greedy in itself. It is the choice
of reduction positions where the semantics’ rules are apllied what will make a
certain evaluation lazy or not.

5

Some Applications of the Unfolding Semantics

Declarative Debugging 6 With declarative debugging, the debugger consults the
internal structure of source code to find out what expressions depend on other expressions and turns this information into an Execution Dependence Tree (EDT).
6

The listings of unfolded code provided in this paper have been generated by our
unfolder. Source at http://www.github.com/josem-rey/unfolder and test environment at https://babel.ls.fi.upm.es/~ jmrey/online_unfolder/unfolding.html

14

e = f e1 . . . en , f ∈ FS n ,
(f t1 . . . tn |g = r) ∈ P
σ = mgu((t1 , . . . , tn ), (e1 , . . . , en )),
σ(g) ❀∗ True
e ❀ σ(r)

e = f e1 . . . en , f ∈ FS n ,
∄(Λ ∈ P such that Λ ≡ (f t1 . . . tn |g = r)
(rule)
σ = mgu((t1 , . . . , tn ), (e1 , . . . , en )), (rulebot)
σ(g) ❀∗ True)
e ❀ ⊥s

e = (p e1 . . . en ), e ❀p t, t ∈ T, p ∈ PF
(predef)
e❀t
ei ❀∗ False, i : 1, 2
(andfalse)
e1 ∧ e2 ❀ False

True ∧ True ❀ True

(andtrue)

(False ◮ e) ❀ ⊥s (ifthenfalse) (True ◮ e) ❀ e (ifthentrue)

Fig. 10. Operational Semantics

The debugger uses this information as well as answers from the user to blame
an error on some rule. We have experimentally extended the unfolder to collect
intermediate results as well as the sequence of rules that leads to every fact. This
additional information allows our unfolder to build the EDT for any program
run. Consider for example this buggy addition:
A1: addb Zero n = n
A2: addb Suc (Zero ) n = Suc (n)
A3: addb Suc (Suc (m)) n = Suc ( addb m n)
M24 : main24 = addb Suc (Suc ( Suc (Zero ))) Suc (Zero )

We can let the program unfold until main24 is fully evaluated. This happens in I3 ,
which contains the following fact for the main function (after much formatting):
root : main24 = Suc (Suc ( Suc (Zero ))) <M24>
n1: addb ( Suc (Suc (Suc ( Zero ))), Suc ( Zero ))= Suc ( Suc (Suc ( Zero)))<A3>
n2:addb (Suc ( Zero ), Suc (Zero )) = Suc ( Suc (Zero )) <A2>

Now, following the method described in [8], we can think of the sequence above
as a 3-level EDT in which the root and node n1 contain wrong values while the
node n2 is correct, putting the blame on rule A3.
The main reason that supports the use of unfolding for performing declarative debugging is that it provides a platform-independent environment to test
complex programs. This platform independence can help check the limitations
of some implementations (such of unreturned answers due to endless loops).
Test Coverage for a Program It is said that a test case for a program covers
those rules that are actually used to evaluate the test case. We would like to
reach full code coverage with the smallest test set possible. The unfolder can be
a valuable tool for finding such a test set if it is enhanced to record the list of
rules applied to reach every fact.

15

What must be done with the enhanced unfolder is to calculate interpretations
until all the rules appear at least once in the rule list associated to the facts that
do not contain any ⊥s and then apply a minimal set coverage algorithm to find
the set of facts that will be used as the minimal test set. For example:
R1:
R2:
A1:
A2:

rev [] = []
// List inversion
rev (x:xs) = append (rev xs) [x]
append [] x = x
append (x:xs) ys = x:( append xs ys)

The first interpretation contains:
∗ rev (Nil ) = Nil <R1>
∗ append(Nil ,b) = b <A1>
∗ append( Cons (b,c),d) = Cons (b,Bot )

<A2>

So, appending the empty list to any other achieves 50% coverage of append.
Reversing the empty list uses 1 rule for rev: the coverage rate is 50% too. I3 has:
∗ append( Cons (b, Nil ),c) = Cons (b,c) <A2 ,A1>
...
∗ rev ( Cons (b,Cons (c,Nil ))) = Cons (c,Cons (b,Nil ))
<R2 ,R2 ,R1 ,A1 ,A2 ,A1>

This shows that the minimal test set to test append must consist of appending
a one element list to any other list. Meanwhile, reversing a list with 2 elements
achieves a 100% coverage of the code: all the rules are used.
To close this section, we would like to mention that Abstract Interpretation
can be used along with unfolding to find properties of the programs under study
such as algebraic or demand properties. See examples 4, 5, 6 in the Appendix.

6

Conclusion and Future Work

We have shown that unfolding can be used as the basis for the definition of a
semantics for lazy, higher-order functional programs written in a kernel language
of conditional equations. This is done by adapting ideas from the s-semantics
approach for logic programs, but dealing with the aforementioned features was
not trivial, and required the introduction of two ad-hoc primitives to the kernel language: first, a syntactic representation of the undefined and second, a
matching operator that deals with partial information.
Effort has also been devoted to simplifying the code produced by the unfolder,
by erasing redundant facts and constraining the shape of acceptable facts. We
have provided a set of requirements for programs that ensure the safety of these
simplification procedures. We have also proven the equivalence of the proposed
unfolding semantics with an operational semantics for the kernel language.
We have implemented an unfolder for our kernel language. Experimenting
with it supports our initial claims about a more “implementable” semantics.
Regarding future work, we want to delve into the applications that have been
just hinted here, particularly declarative debugging and abstract interpretation.

16

Finally, we are working on a better characterization of the necessary conditions that functional programs must meet in order for different optimized versions of the clean method to work safely.

References
1. Alpuente, M., Falaschi, M., Vidal, G.: Narrowing-driven Partial Evaluation of Functional Logic Programs. In: Proc. ESOP’96. LNCS, vol. 1058. Springer (1996) 4
2. Alpuente, M., Falaschi, M., Moreno, G., Vidal, G.: Safe folding/unfolding with conditional narrowing. In: Proc. ALP’97. pp. 1–15. Springer LNCS (1997) 7
3. Antoy, S., Hanus, M.: Declarative programming with function patterns. In: Proc. of
LOPSTR’05. pp. 6–22. Springer LNCS (2005) 10
4. Bossi, A., Gabbrielli, M., Levi, G., Martelli, M.: The s-semantics approach: Theory
and applications. Journal of Logic Programming 19/20, 149–197 (1994) 1, 4
5. Burstall, R.M., Darlington, J.: A transformation system for developing recursive
programs. J. ACM 24(1), 44–67 (Jan 1977) 4
6. Hanus, M.: The integration of functions into logic programming: From theory to
practice. Journal of Logic Programming pp. 583–628 (1994) 5
7. Pettorossi, A., Proietti, M.: Perfect model checking via unfold/fold transformations.
In: Computational Logic, LNCS 1861. pp. 613–628. Springer (2000) 4
8. Pope, B., Naish, L.: Buddha - A declarative debugger for Haskell (1998) 14
9. Scott, D.: The lattice of flow diagrams (Nov 1970) 4

17

APPENDIX
This appendix is not part of the submission itself and is provided just as supplementary material for reviewers. It pursues the following goals:
1. To provide a pictorical representation of the functions involved in the unfolding process, which hopefully helps in grasping how the whole process works
(Sect. A).
2. To describe in what sense the unfolding and the operational semantics are
equivalent and to prove such equivalence (Sect. B).
3. To present a larger example that intends to clarify how the functions that
have been used actually work as well as additional examples (Sect. C).
4. To establish some results that support the validity of the code generated by
the unfolder (Sect. D).

A

Pictorial Representation of the Unfolding Process

Invocation

U

Data flow
unfold

clean

eval

umatch

hi | ci ∧ c′mi = bi

Runtime

match

Code

Fig. 11. Relation among the functions taking part in unfolding

Throughout Sect. 3 a number of auxiliary functions were presented. These functions are depicted in Fig. 11. The figure can be explained as follows:
The starting point is U . U does nothing but to call unfold and remove the
redundant facts by calling clean. It is then up to the user to call U again to
perform another step in the unfolding process.
The second level of the figure shows unfold, which takes a program rule and
unfolds it as much as possible. unfold calls itself with the output of its previous
execution until no more positions are left to unfold (arrow pointing downwards).
If unfold receives an input where at least one position is unfoldable, it calls eval
on the arguments of the unfoldable expression and then calls umatch to perform
the actual fitting between the unfoldable position and the head of some fact.

18

The last level of the figure (below the dashed line) represents the execution
of the unfolded code. This part is not related with the definition of the unfolding
operator, but with the execution of the unfolded code. The code is made of the
output of unfold whose guards are (possibly) extended with c′mi , the output from
umatch, which contains the invocations to match. Observe that the output from
umatch goes to the generated code only, not to the unfolding process.
To the best of our knowledge, this unfolding process is a first effort to formulate an unfolding operator beyond naı̈ve unfolding.

B
B.1

Equivalence between the Unfolding Semantics and the
Operational Semantics
Unfolding of an Expression

Let us define a function ueval that finds what is the normal form for a given
expression by means of unfolding. In short, what ueval does is to evaluate a given
(guarded) expression by unfolding it according to a given interpretation.
The function ueval has type ueval : Set (F ) × E → Set (E) and is defined as
shown in Fig. 12.
Note that any expression e is equivalent to (True ◮ e).
B.2

Trace of a Fact or an Expression

Given a fact F , belonging to any interpretation I, its trace is the list of pairs
(Λi , o) where Λi is a rule in rule(P ) ∪ {Λ⊥s ,f = f x1 . . . xn = ⊥s } ∀f ∈ FS n
and o is a position within the expression to which the next rule in the trace
is to be applied. This position indicates what subexpression within the current
expression is to be replaced by the body of the rule applied.
Let us define the function that returns all the traces associated to all the
facts derivable from a single rule (++ denotes list of lists concatenation that
returns the list of lists resulting from appending every list in the first argument
to every list in the second argument):
tr ′ : Set (F ) × R → [τ ]
where R is the type of program rules and τ is the type of traces.
– tr′ (I, f t1 . . . tn |c = b) = [ ] if f t1 . . . tn |c = b is a valid input for the case 1
of unfold .
– tr′ (I, f t1 . . . tn |c = b) = o.tr (I, F ) + +tr ′ (I, F ′ ) if the case 2a) of unfold
can be applied to f t1 . . . tn |c = b using fact F ∈ I at position o. F ′ is the
result of unfolding f t1 . . . tn |c = b as it is done in the aforementioned case
of unfold .
– tr′ (I, f t1 . . . tn |c = b) = [[(Λ⊥s ,f ′ , o)]] + +tr ′ (I, F ′ ) if the case 2b) of unfold
can be applied to f t1 . . . tn |c = b at position o. F ′ is the result of unfolding
f t1 . . . tn |c = b as it is done in case 2b) of unfold .

19
ueval : Set(F) × E → Set(E)
= {e} if no rule from evalAux applies
to
S any position of e
=
o ueval (I, e[uevalAux (I, e|o )]|o )
∀o such that a rule of uevalAux is
applicable to e|o .
-------------

ueval (I, e)
ueval (I, e)

uevalAux : Set(F) × E → E
uevalAux (I, p e1 . . . en )
if p e1 . . . en ❀p t (p ∈ PF n )

= t

uevalAux (I, (c1 ∧ . . . ∧ ci−1 ∧ snd (match(p, e)) ∧ ci+1 ∧ . . . ∧ cn ◮ e′ )) = σ(c1 ∧ ci−1 ∧ b ∧ ci+1 ∧ . . . ∧ cn ◮ e′ )
if match(p, e) = (σ, b)
uevalAux (I, True ∧ True)

= True

uevalAux (I, b1 ∧ b2 )
b1 , b2 ∈ Bool , b1 = False or b2 = False

= False

uevalAux (I, True ◮ e)

= e

uevalAux (I, False ◮ e)

= ⊥s

uevalAux (I, f e1 . . . en )
= σ ′ (c ◮ b)
′
if f ∈ FS n , ∃f t1 . . . tn |c = b ∈ I. σ = mgu((t1 , . . . , tn ), (e1 , . . . , en )) with σ ′ (c) = True

uevalAux (I, f e1 . . . en )
= ⊥s
′
if f ∈ FS n , ∄f t1 . . . tn |c = b ∈ I. σ = mgu((t1 , . . . , tn ), (e1 , . . . , en )) with σ ′ (c) = True
Fig. 12. The ueval function: Evaluating expressions by means of unfolding

The composition of a position o and a trace (denoted by o.tr (. . .) above) is
defined (for every trace in a given list) as:
– o.[ ] = [ ]
– o.[(Λ, o′ )|xs] = [(Λ, o.o′ )|o.xs]
The list of traces for a fact F with respect to an interpretation I (tr (I, F )) relies
on tr ′ :
tr : Set (F ) × F → [τ ]
tr (I, F ) = [[(ΛF , {})]] + +{τ such that τ ∈ tr ′ (I, ΛF )∧
unfold (ΛF , I) generates F according to the steps given by the trace τ }

20

where ΛF is the only program rule that can generate F .
Note that tr and tr ′ are mutually recursive.
The list of traces of an expression e according to interpretation I (denoted
Tr (I, e)) is defined as the tail of all the lists in tr(I, goal ′ = e) where goal ′ is a
new function name that does not appear in the program P and the tail of a list
is the same list after removing its first element.
B.3

Equivalence between the Unfolding and Operational Semantics

This section will show that the unfolding semantics and the operational semantics are equivalent in the following sense for any ground expression goal :
goal ❀∗ e′ ↔ e′ ∈ ueval (I∞ , goal )

(2)

where ❀∗ is the transitive and reflexive closure of ❀ and e′ is in normal form
according to ❀.
Given a program P , I∞ is the limit of the following sequence:
– I0 = ∅
S
– In+1 (n ≥ 0) = Λ∈rule(P ) unfold (In , Λ)
B.4

Proof of Equivalence

We are now proving that Eq. 2 holds.
→)
This part of the double implication will be proven by induction on the number
of ❀-steps that an expression requires to reach normal form.
Base case (n=0): If goal ❀0 e′ , then goal = e′ , which means that goal is
in normal form already. Therefore, goal has no full applications of symbols in
PF ∪ FS . In that case, ueval (I, goal ) = {goal } ∀I ∈ Set (F ).
Induction step:
Let us take as induction hypothesis that any expression goal such that
goal ❀n e′ (where e′ is in normal form) then e′ ∈ ueval (I∞ , goal ).
Let en+1 be an expression that requires n + 1 ❀-steps in order to reach
normal form. Then there must exist (at least) one expression en such that:
en+1 ❀ en ❀n e′
where e′ is in normal form. Now, if we prove that both en+1 and en unfold to
the same values (that is, ueval (I∞ , en+1 ) = ueval (I∞ , en )), then we can apply
the induction hypothesis to en to state that en ❀n e′ → e′ ∈ ueval (I∞ , en+1 ) =
ueval (I∞ , en ).
Let us check all the rules in the operational semantics for the single ❀ step
going from en+1 to en .
Rule rule

21

In this case, en+1 = f e1 . . . ea (f ∈ FS a ) and en = σ(r) (assuming that the
rule for f within program P is Λ ≡ f t1 . . . ta |g = r and σ = mgu((t1 , . . . , tn ), (e1 , . . . , en ))).
By reductio ad absurdum let us assume now that ueval (I∞ , en+1 ) 6= ueval (I∞ , en ).
Then,

ueval (I∞ , f e1 . . . ea ) 6= ueval (I∞ , σ(g ◮ r))
However, note that σ(Λ) is equal to the rule instance f e1 . . . ea |σ(g) = σ(r),
which states exactly the opposite of the equation above. We have reached a contradiction, which means that our initial hypothesis (namely, ueval (I∞ , en+1 ) 6=
ueval (I∞ , en )) is false.
Rule rulebot
In this case, en+1 = f e1 . . . ea (f ∈ FS a ) and en = ⊥s . If there is no rule in
P whose pattern can unify with en+1 while at the same time having a satisfiable
guard, it is sure that no fact in any interpretation derived from P will be such
that its head unifies with en+1 while at the same time having a satisfiable guard
(which forces uevalAux to use its last case). That means that en+1 cannot be
reduced to anything different from ⊥s . The same happens with en (which is
already equal to ⊥s ). Therefore, ueval (I∞ , en+1 ) = ueval (I∞ , en ) as we wanted
to prove.
Rule predef
In this case, en+1 = p e1 . . . ea and en = t (t ∈ T ) where p ∈ PF and
p e1 . . . ea is has value t according to the predefined functions known to the
environment being used.
Also in this case ueval (I, p e1 . . . ea ) = {t} and ueval (I, t) = {t} for any
interpretation I. This case simply evaluates predefined functions.
Rule andfalse
In this case, en+1 = e1 ∧ e2 and en = False when either e1 ❀∗ False or
e2 ❀∗ False. Let us assume without loss of generality that e1 ❀∗ False.
Since en+1 requires n + 1 ❀-steps to reach normal form, then e1 must take at
most n steps to reach its normal form. This means that the induction hypothesis
is applicable to e1 and therefore ueval (I∞ , e1 ) ⊃ {False}. This in turn means
that ueval (I∞ , e1 ∧ e2 ) ⊃ {False} as we wanted to prove (assuming that the
logical connector ∧ is defined as lazy conjunction in eval ).
The remaining rules (andtrue, ifthentrue, ifthenfalse) are proven in
a similar way.
Let us proceed now to the reverse implication.
←)
The proof will be driven by structural induction on the shape of the expression to be evaluated (goal ).
Let goal be an expression that has no full applications of any symbol of FS
or PF . Then, ueval (I∞ , goal ) = {goal } and ❀ cannot apply any rewriting, so
goal ❀∗ goal , as we wanted to prove.
Next, let goal = p e1 . . . en (p ∈ PF n ) and no ei has any full application of
any symbol in FS ∪ PF . Then, ueval (I∞ , goal ) = {t} if goal ❀p t. ❀ will apply

22

predef, ifthentrue, ifthenfalse, andtrue or andfalse to evaluate the
same predefined function and reach the same t.
Next, let goal = f e1 . . . en (f ∈ FS n ). If ueval (I∞ , goal ) includes e′ that is
because goal has a trace (since e′ is in normal form) That is, [(Λ1 , o1 ), . . . , (Λk , ok )] ∈
Tr (I∞ , goal ) for some k > 0. We are now going to prove that:
e′ ∈ ueval (I∞ , goal ) ∧ [(Λ1 , o1 ), . . . , (Λk , ok )] ∈ Tr (I∞ , goal )
→ goal ❀∗ e′ (using the exact sequence of rules given below)
Specifically, it will be proven that every trace element (Λ, o) is equivalent to the
following ❀-sequence at position o of the expression input for the trace element:
1. The rules dealing with predefined functions (namely, predef, ifthentrue,
ifthenfalse, andtrue, andfalse) will be applied to the expressions being
rewritten as many times as possible.
2. rule or rulebot: The rule rule will be applied if Λ 6= Λ⊥s ,f . rulebot
will be applied otherwise.
3. The rules dealing with predefined functions (namely, predef, ifthentrue,
ifthenfalse, andtrue, andfalse) will be applied to the expression returned by the previous step as many times as possible.
The proof will be driven by induction on the length of the trace for goal .
Base case: ([(Λ ≡ f p1 . . . pa |g = r, o = {})] ∈ Tr (I∞ , goal )).
If goal can be rewritten to normal form e′ by just using the rule Λ, that means
that Λ 6= Λ⊥s ,f (since e′ is assumed to be in normal form) and that I∞ must
countain a fact f t1 . . . ta |c = b, acording to the definition for tr ′ (second case),
+
′
such that ∃σ ′ = mgu((t1 , . . . , ta ), (e+
1 , . . . , ea )) and eval (I∞ , σ (c)) = True and
+
′
′
eval (I∞ , σ (b)) = e , (ei = eval (I∞ , ei )).
On the other hand, ❀ can apply rule to goal = f e1 . . . ea . This rule rewrites
goal to:
σ(g ◮ r)
+
mgu((p1 , . . . , pa ), (e+
1 , . . . , ea )).

Note that the application of eval
where σ =
here is equivalent to the application of all the cases of uevalAux except the last
two ones (let us call these first cases uevalAuxpredef ) which in turn have the
same effect than the ❀-rules predef, ifthentrue, ifthenfalse, andtrue,
andfalse as many times as necessary to evaluate any predefined function that
appears in any of the arguments to f . Let us remark that match is unnecessary
in ❀ since all the expressions handled by ❀ are ground and the substitution
returned by match generates the same ground expressions than σ in rule rule.
We also assume that match cannot be used in normal programs.
The same cases for predefined functions (uevalAuxpredef ) can be applied to
the expression above to get σ(eval (I∞ , g) ◮ eval (I∞ , r)).
+
By construction, we know that σ ′ (t1 , . . . , ta ) = σ(p1 , . . . , pa ) = (e+
1 , . . . , ea ).
Since any valid program in our setting can only have at most one rule that
matches the ground expression f e1 . . . en , then:

23

– eval (I∞ , σ ′ (b)) = eval (I∞ , σ(r)) = e′
– eval (I∞ , σ ′ (c)) = eval (I∞ , σ(g)) = True
Therefore, both unfolding and ❀ have used a fact and a rule which were sintactically indentical (once predefined functions have been evaluated) to find the
same answer for goal . This proves the base case.
Induction step: Now the length of the trace for goal is equal to l +1 (l > 0).
Let us assume, as induction hypothesis that:
e′ ∈ ueval (I∞ , goal ) → goal ❀∗ e′
provided that the trace for goal has exactly l elements
and using the sequence of ❀-rules given earlier for that trace)
Let us prove the equation for goals with trace of length l+1. In order to do that let
us consider that [(Λ1 , o1 ), . . . , (Λl+1 , ol+1 )] ∈ Tr (I∞ , goal ) and an intermediate
expression el whose trace is the same as before except for the first element.
Two cases have to be looked at here: One in which rulebot is applied as
first step (that is, Λ1 = Λ⊥s ,f ′ for some f ′ ) and one more where rule is applied
as first step (that is, Λ1 6= Λ⊥s ,f ′ ).
Let us begin with rulebot. If el = goal [⊥s ]|o1 , the following must be true:
– goal |o1 = f ′′ e′′1 . . . e′′f (f ′′ ∈ FS f )
– ∄(F ′′ ∈ I∞ such that F ′′ ≡ f ′′ t′′1 . . . t′′f |c′′ = b′′ and
′′+
′′+
σ ′ = mgu((t′′1 , . . . , t′′f ), (e′′+
= eval (I∞ , e′′j )
1 , . . . , ef )) where ej
′ ′′
and True ∈ ueval (I∞ , σ (c ))).
– If F ′′ does not exist that means that no rule for f ′′ originates a fact like
′′+
F ′′ which in turn means that no rule unifies with (e′′+
1 , . . . , ef ) either. This
forces ❀ to apply rulebot to el |o1 and the same does ueval (last rule).
Note that the sequence of ❀ rules applied in this case was (predef, ifthentrue, ifthenfalse, andtrue, andfalse)∗ , rulebot.
Since the trace for goal [⊥s ]|o1 has length l, the induction hypothesis is suitable for it and then:
e′ ∈ ueval (I∞ , el ) → el ❀∗ e′
by using the sequence of ❀-rules given earlier for el )
and since the normal form for goal is the same as the normal form for el by
definition of unfolding, we have that the trace for goal has the required shape.
Lastly, consider some goal whose trace is again
[(Λ1 , o1 ), . . . , (Λl+1 , ol+1 )] but where Λ1 6= Λ⊥s ,f . Let us apply uevalAuxpredef
(or, equivalently, predef, ifthentrue, ifthenfalse, andtrue, andfalse)
′′+
and
as many times as possible to the arguments of goal |o1 to get f ′′ e′′+
1 . . . ef
′′+
′′ ′′+
then rule (the only rule that ❀ can apply to f e1 . . . ef ) by using the rule

24

Λ1 ≡ f ′′ p′′1 . . . p′′f |g ′′ = r′′ and the unifier
′′+
σ = mgu((p′′1 , . . . , p′′f ), (e′′+
1 , . . . , ef )). Now, we can rewrite goal to:
goal [σ(g ′′ ◮ r′′ )]|o1
given that according to tr ′ ’s definition (second case), the rule Λ1 is applicable to
goal |o1 (since the trace of any fact begins by the rule which originates the fact and
unfold has been able to apply a fact derived from Λ1 to goal |o1 ). This means that
the expression above can be rewritten to goal [eval (I∞ , σ(g ′′ ◮ r′′ ))]|o1 which is
the new el . Note that the eval in the former expression is equivalent to (predef,
ifthentrue, ifthenfalse, andtrue, andfalse)∗ (which in turn is equivalent
to applying the cases of uevalAuxpredef as many times as necessary).
What we know now is:
– The normal form for goal is the same as the normal form for el since ❀
conserves the semantics by definition.
– The rewriting sequence from goal to its normal form is the same as the
rewriting sequence for el preceded by the rules applied above (i.e. (predef,
ifthentrue, ifthenfalse, andtrue, andfalse)∗ , rule, (predef, ifthentrue, ifthenfalse, andtrue, andfalse)∗ ).
– Since the length of the trace for el is equal to l, the induction hypothesis is
applieable to it and then:
e′ ∈ ueval (I∞ , el ) → el ❀∗ e′
by using the sequence of ❀-rules given earlier for el )
Since we have proved that, given an unfolding sequence, we are able to find
a precise sequence of ❀-rules that provokes the very same effect to any given
expression, we have also proved the ←) implication of the theorem.
B.5

Example

Let us present an example that may clarify some of the concepts involved in the
proof of equivalence. Consider this program:
f(x)=g(x+1)
g(x)=h(x+2)
h(x)=x+3
j (5)=6
f2(x,y)=x+y
goal =f(4)
goal2=f2(f(4),f (4))
goal3=K(j (5))

25

What we have here are a constructor (K), some test goals (goal, goal2 and
goal3) and some functions. A first function group (f,g,h) is such that f requires
the evaluation of g and h. We will see that the trace for f’s facts reflects this
issue. Next, we have two more unrelated functions. j and goal3 will be used to
demonstrate the usage of rulebot while f2 and goal2 will show why non-unique
traces exist.
The first interpretation generated by the unfolder is:
∗
∗
∗
∗

h(b) = b+3 <H>
j(5) = 6 <J>
f2(b,c) = b+c <F2>
goal3 = K(Bot ) <Goal3>

The sequences enclosed between < and > is the trace of every fact. It can be
seen, however, that the unfolder does not display the position of every step and
it does not display the usage of Λ⊥s ,j rules either (see the last fact).
So, the whole trace for the last fact would be
[(Goal3,{}), (Lambda Bot,{1})].
All the other facts have a trace of length 1. It can be seen that they are
identical to their respective program rules. This property supports the proof for
the base case of the induction since applying the rule to perform rewriting is
exactly the same as applying a fact with a trace length of one. Realize that even
though these facts cannot be unfolded any further, they require eval to reach a
normal form (since the addition needs to be evaluated after its arguments have
been bound to ground values).
Further interpretations provide more interesting traces. This is I4 :
∗
∗
∗
∗
∗
∗
∗
∗

h(b) = b+3 <H>
j(5) = 6 <J>
f2(b,c) = b+c <F2>
g(b) = b +2+3 <G,H>
goal3 = K(6) <Goal3 ,J>
f(b) = b +1+2+3 <F,G,H>
goal = 10 <Goal ,F,G,H>
goal2 = 20 <Goal2 ,F2 ,F,G,H,F,G,H>

Take a look at how the fact regarding goal reflects the dependency between f,
g and h. That fact has a trace of length 4 (it is very easy to follow how goal
is evaluated by looking at its trace). Removing the first element of its trace
(as needed in the induction step) yields the trace <F,G,H> for which there is a
fact (the fact for f). This means that in this case, the induction step says that
evaluating goal is the same as applying rule to find f(4) (eval is not needed in
this step) and then applying the induction hypothesis to f(4) whose trace is an
element shorter than that of goal.
Finally, consider how goal2 can be evaluated to normal form in multiple
orders. Since f2 demands both arguments, both of them must be taken to normal
form but the order in which is done is irrelevant. Since our unfolder does not
show the positions for the reduction steps all the traces for goal2 look the same
but more than one trace would appear if positions were taken into account.

26

B.6

Lemma: Applicability of Every Step Inside a Fact’s Trace

We have seen that the proof of equivalence between the operational semantics
and the unfolding semantics relies on the fact that every element inside a fact’s
trace is applicable to the expression resulting from applying all the trace steps
that preceded the steps under consideration. How can we be sure that a trace
step is always applicable to the expression on which that step must operate?.
This lemma states that this will always happen. Intuituvely, what the lemma
says is that the trace of a fact is nothing else that the sequence of rules that
unfold has applied to get from a program rule to a valid fact.
Lemma 3 (Applicability of Every Step Inside a Fact’s Trace). Let e be
an expression and let [(Λ1 , o1 ), . . . , (Λm , om )] ∈ Tr (I∞ , e). If e ❀∗ em′ (m′ ≥
0, m′ < m) and [(Λm′ +1 , om′ +1 ), . . . , (Λm , om )] ∈ Tr (I∞ , em′ ) then the following
assertions are true:
1. If Λm′ +1 = Λ⊥s ,f ′ then ∄(Λ ∈ rule(P ) = f ′ t′1 . . . t′n |g ′ = r′ such that
∃σ = mgu(f ′ t′1 . . . t′n , ueval (I∞ , em′ |om′ +1 )) and True ∈ ueval (I∞ , σ(g ′ )))
2. If Λm′ +1 6= Λ⊥s ,f ′ then Λm′ +1 ≡ f t1 . . . tn |g = r and
∃σ = mgu(f t1 . . . tn , eval (I∞ , em ′ |om ′ +1 )) and True ∈ ueval (I∞ , σ(g))

C

Additional Examples

Example 2 (Lazy Evaluation).
Think of the following code and its first interpretations:
first : [a] → a
first (x: ) = x
ones : [Int ]
ones = 1: ones
main : Int
main = first ones

I0 =I0⊥ = ∅
I1 =U (I0 ) = {ones=1:⊥s ,
first(x:xs)=x}
I1⊥ ={main=⊥s }
I2 =U (I1 ) = {ones=1:(1:⊥s ),
first(x:xs)=x, main=1}
I2⊥ =I1⊥

The semantics for this program is infinite: every step adds a 1 to the list generated
by ones.
Consider the step from I1 to I2 : when unfolding ones, a fact matching ones
is found in I1 (namely, ones=1:⊥s ) so this last value is replaced in the right side
of the rule. Since the new value for ones is greater than the existing fact and
both heads are a variant of each other, the function clean can remove the old
fact.The fact ones=1:⊥s can now be used to evaluate main. Since the new fact
main=1 is greater than the fact main=⊥s it replaces the existing one. The fact for
first remains unaltered.
Example 3 (Larger Example).
Let us present an example that intends to describe how all the functions and
concepts that we have seen throughout the paper work. Think of the following
program:

27
ite : Bool ∗ a ∗ a → a
ite (True ,t,e) = t
ite (False ,t,e) = e
gen : Int → [Int ]
gen n = n:( gen (n +1))
senior : Int → Bool
senior age = ite (age >64,True , False)
map : (a → b) ∗ [a] → [b]
map (f ,[])=[]
map (f ,(x:xs )) = (f x) : (map (f,xs))
main50 : [Bool ]
main50 = map (senior ,gen (64))

Let us see how this program is unfolded.
First, the initial interpretation (I0 ) is empty, by definition. At this point, the
function unfold is applied to every rule in turn, using I0 as the second argument.
This produces the following interpretation (I1 ):
∗
∗
∗
∗
∗

ite (True ,b,c) = b
ite (False ,b,c) = c
gen (b) = Cons (b,Bot )
map (b,Nil ) = Nil
map (b,Cons (c,d)) = Cons (b@[c],Bot )

How did we get here?. When a rule is applied to unfold, every full application
of a symbol in FS is replaced by the value assigned to the application in the
interpretation also applied to unfold. The actual matching between an expression
and some rule head is performed by umatch, which is called by unfold every time
an expression needs to be unfolded. In most cases, umatch behaves as a simple
unifier calculator but higher order brings complexity into this function (in ssemantics, where higher order does not exist, simple unification is used in the
place of umatch). In this case, the interpretation applied was the empty one, so,
the following has happened to every rule:
– The two rules for ite have no applications of user-defined functions, so nothing has to be done to them in order to reach a fact in normal form. That is
why they appear in I1 right away.
– The rule for gen is a little bit different since this rule does have an application
to a user-defined function. However, since I0 contains nothing about those
functions, all that unfold can do is to replace that invocation by the special
symbol Bot (represented by ⊥s in formulas) to represent that nothing is
known about the value of gen (b+1).
– The function senior has no facts inside I1 since the function clean removes
any unguarded fact with a body equal to ⊥s . This is precisely what has
happened since I0 contains no information about ite, so the resulting new
fact for senior would be ∗ senior age=Bot

28

– The first rule for map is left untouched since it has no full applications of
user-defined functions (as it happened with ite).
– The second rule for map generates the fact
∗ map(b,Cons(c,d)) = Cons(b@[c],Bot) where the Bot denotes that the value
for map(f,xs) is not contained inside I0 .
– And, finally, there is not any fact for main50 since the whole application of
map that appears at the root of the body is unknown, so it gets replaced by
Bot, which is in turn eliminated by clean (and moved into I1⊥ ).
Since we saw that two facts were removed by clean because they did not have a
guard and their body was equal to Bot, I1⊥ , has the following content:
∗ senior( age ) = Bot
∗ main50 = Bot

These two facts will be reinjected into the factset when I2 is calculated but in
this case, they do not have a noticeable effect on the results, so we will not insist
on them any more.
One more iteration of the unfolding operator generates I2 :
∗
∗
∗
∗
∗
∗
∗
∗

ite (True ,b,c) = b
ite (False ,b,c) = c
map (b,Nil ) = Nil
gen (b) = Cons (b, Cons (b+1, Bot ))
senior(b) | snd (match (True ,b>64)) = True
senior(b) | snd (match (False ,b>64)) = False
map (b,Cons (c, Nil )) = Cons (b@[c], Nil )
map (b,Cons (c, Cons (d,e))) =
Cons (b@[c],Cons (b@[d],Bot ))
∗ main50 = Cons (Bot ,Bot )

Remember that I2 has been calculated by taking I1 ∪ I1⊥ as the relevant interpretation. By definition of the unfolding operator, I2 includes all the facts that
were already present inside I1 (unless they are removed by clean).
Remember also that we are using the optimized version of clean (the one that
removes subsumed facts instead of enlarging the constraints of the subsuming
facts). Once these aspects have been settled, the calculations that lead to the
formation of I2 can be explained as follows:
– The two facts for ite are transferred directly from I1 into I2 . This is so since
they cannot be unfolded any further and besides, they are not overlapped
by any fact. The same happens with the first fact for map.
– The fact for gen is much more interesting: There are not two facts for
gen in I2 . There is only one. This is due to the application of clean in
unfold. What has happened here is that clean has compared the old fact
(∗ gen(b)=Cons(b,Bot)) to the new one
(∗ gen(b)=Cons(b,Cons(b+1,Bot))) and has removed the old one. The reason
for this is that both facts clearly overlap but the newest fact has a body
that is greater (according to ⊑) than that of the old fact. Given that the
optimized version of clean is being used (all the functions here are complete
and the rules are productive), the old fact is removed.

29

One more point of interest here: Note that the expression b+1 cannot be
further unfolded since the value for b is unknown at unfolding time. We will
see the opposite case later.
– The explanation for senior will be detailed later.
– The two facts for map have become three. This has happened as follows:
• The second rule for map, when unfolded using I1 ∪I1⊥ generates two facts:
∗ map (b,Cons (c,Nil )) = Cons (b@[c],Nil )
∗ map (b,Cons (c,Cons (d,e ))) = Cons (b@[c],Cons (b@[d],Bot ))

Those two facts overlap with the old fact
(∗ map(b,Cons(c,d)) = Cons(b@[c],Bot)), so this fact is removed by clean,
which brings us to the count of three facts for map.
– main50 has progressed slightly: The invocation of map within the body of
main50 has been replaced by the body of the second fact for map in I1 ∪ I1⊥
generating Cons(senior@[b],Bot). Since nothing is known about senior in
I1 ∪ I1⊥ , the final result is Cons(Bot,Bot).
The unfolding of senior requires special attention: In order to unfold the only
rule for this function, the call to ite is unfolded. However, the first argument for
ite must be fully known before proceeding. This is impossible at unfolding time
since age will receive its value later, at runtime. The only way to go in cases
like this is to assume certain hypotheses and to generate facts that record those
hypotheses. In this example, we are forced to assume that age>64 is True when
the first rule for ite is unfolded while age>64 is assumed to be False when the
second rule for ite is unfolded. These hypotheses are recorded in the guards for
the facts corresponding to senior.
The function responsible for generating these hypotheses is umatch (more
specifically, its second rule). This rule is used when an expression rooted by a
predefined function (here, <) has to be matched to some pattern term which
is not a variable (here, True and then False). In this case, umatch extends the
new fact’s guard by adding the new condition (here snd(match(True,b>64)))
(resp. False) and then proceeds as if the PF-rooted expression matched the
given pattern in order to continue generating hypotheses. In this case, umatch
would call itself with umatch(True,True), (resp. False) which is solved by using
umatch’s first rule which generates no more conditions or variable substitutions.
Unfolding once again yields I3 :
∗
∗
∗
∗
∗
∗
∗
∗
∗

ite (True ,b,c) = b
ite (False ,b,c) = c
map (b,Nil ) = Nil
senior(b) | snd ( match(True ,b>64)) = True
senior(b) | snd ( match(False ,b>64)) = False
map (b,Cons (c, Nil )) = Cons (b@[c], Nil )
gen (b) = Cons (b, Cons (b+1, Cons (b +1+1 , Bot )))
map (b,Cons (c, Cons (d, Nil ))) = Cons (b@[c],Cons (b@[d],Nil ))
map (b,Cons (c, Cons (d, Cons (e,f)))) =
Cons (b@[c],Cons (b@[d],Cons (b@[e],Bot )))
∗ main50 | snd (match( True ,64>64)),
snd (match( True ,65>64)) = Cons (True , Cons (True ,Bot ))

30
∗ main50 | snd (match( True ,64>64)), snd (match (False ,65>64)) =
Cons (True ,Cons (False ,Bot ))
∗ main50 | snd (match( True ,64>64)) = Cons (True , Cons (Bot ,Bot ))
∗ main50 | snd (match( False ,64>64)),
snd (match(True ,65>64)) = Cons (False ,Cons (True , Bot ))
∗ main50 | snd (match( False ,64>64)),
snd (match(False ,65>64)) = Cons (False ,Cons (False ,Bot ))
∗ main50 | snd (match( False ,64>64)) = Cons (False ,Cons (Bot , Bot ))
∗ main50 | snd (match( True ,65>64)) = Cons (Bot , Cons (True ,Bot ))
∗ main50 | snd (match( False ,65>64)) = Cons (Bot , Cons (False ,Bot ))
∗ main50 = Cons (Bot ,Cons (Bot ,Bot ))
∗ main50 | snd ( match(True ,65>64)), snd ( match(True ,64>64))=
Cons (True ,Cons (True ,Bot ))
∗ main50 | snd (match( True ,65>64)),
snd (match(False ,64>64)) = Cons (False ,Cons (True ,Bot ))
∗ main50 | snd (match( False ,65>64)),
snd (match( True ,64>64)) = Cons (True , Cons (False ,Bot ))
∗ main50 | snd (match( False ,65>64)),
snd (match( False ,64>64)) = Cons (False ,Cons (False ,Bot ))

We are not repeating all the details above. Instead, we just want to point out
some interesting aspects of this interpretation:
– The reader might have expected to find expressions like 64>64 fully reduced
(that is, replaced by False). That would be correct but boolean operators are
not evaluated due to a limitation in the implementation of our unfolder. In
this example, this limitation is a blessing in disguise since those expressions
are needed to understand the origin of some facts.
– An expression like b+1+1 has not been reduced to b+2 since it stands for
(b+1)+1. The function eval has returned the same expression that it is given
since it cannot be further evaluated.
– The combinatory explosion of facts denotes that the unfolder tries all possible
unfolding alternatives (in particular, those facts with less than two conditions
in the guard are the result of unfolding senior before ite, so the result for
senior cannot be other than an unguarded ⊥s ).
– Note that our Prolog implementation does not have an underlying constraint
solver, so the entailment condition of the guards that is used to sort overlapping facts is not checked. That is why the unfolder has generated facts that
should have been removed, such as main50 = Cons(Bot ,Cons(Bot ,Bot )).
– A value of 65 appears whenever the function eval has been applied to evaluate 64+1.
Example 4 (Unfolding and Abstract Interpretation). This example will show how
unfolding can be used to synthesize an abstract interpreter of a functional program. Think of the problem of the parity of addition. The sum of Peano naturals
can be defined as shown in Fig.1 (right).
We also know that the successor of an even number is an odd number and
viceversa. The abstract domain (the domain of parities) can be written as:
data Nat # = Suc c # Nat # | Even # | Odd #

31

Now, the user would define the abstract version for add together with the properties of Suc regarding parity:
add # : Nat # → Nat # → Nat #
add # Even # m = m
add # ( Suc c # n) m = Suc f # ( add # n m)
Suc f # : Nat # → Nat #
Suc f # Even # = Odd #
Suc f # Odd # = Even #

In order to enforce the properties of the successor in the abstract domain, a
catamorphism 7 linking Suc f# to Suc c# will be used:
C
C
C
C

s
s
s
s

: Nat # → Nat #
Even # = Even #
Odd # = Odd #
( Suc c # n) = Suc f # ( C s n)

Then, the unfolding process that has been described must be slightly modified:
after every normal unfolding step, every abstract term in a pattern must be
replaced by the term returned by the catamorphism. By doing this, the unfolding
of the previous program reaches a fixed point at I2 8 :
∗
∗
∗
∗
∗

add #( Even #,m) = m
Suc f #( Even #) = Odd #
Suc f #( Odd #) = Even #
add #( Odd #,Odd #) = Even #
add #( Odd #, Even #) = Odd #

Example 5 (Addition of Parities Revisited).
As an interesting point of comparison, consider this alternative version for
add#:
addr # : Nat # → Nat # → Nat #
addr # Even # m = m
addr # ( Suc c # n) m = addr # n ( Suc c # m)

The fixed point for this new function is as follows (also in I2 ):
∗
∗
∗
∗

addr #( Even #,b) = b
addr #( Odd #,b) = Suc #(b)
suc f #( Even #) = Odd #
suc f #( Odd #) = Even #

Example 6 (Demand Analysis).
The following example shows how abstraction can help to find program properties. This particular example investigates how to find demand properties for
the functions in a program. By demand properties we mean the level of definition
7

8

A catamorphism takes a term an returns the term after replacing constructors by a
corresponding operator.
The rules for the catamorphism do not take part in unfolding

32

that a function requires in its arguments in order to return a result strictly more
defined than ⊥s .
For the sake of simplicity, we are limiting our analysis to top-level positions
within the arguments although the method can be easily extended to cope with
deeper positions.
As before, we begin by defining the abstract domain. This example will run
on Peano Naturals, so the new domain reflects what elements are free variables
and what others are not:
data NatDemand # = Z# | S# NatDemand # | FreeNat #

As an example, we will use the well known function leq. leq x y returns whether
x is lesser or equal than y. The standard (unabstracted) version of leq is as
follows:
leq
leq
leq
leq

: Nat → Nat → Bool
Zero y = True
(Suc x) Zero = False
(Suc x) (Suc y) = leq x y

The abstracted version, which is useful for finding the demand properties for leq
at the top level positions of its arguments is as follows:
data Bool # = True # | False# | DontCareBool #
leq #
leq #
leq #
leq #

:: NatDemand # → NatDemand # → Bool #
Zero # FreeNat # = DontCareBool #
(Suc # x) Zero # = DontCareBool #
(Suc # x) ( Suc y) = leq # x y

Observe that those rule bodies that do not influence the demand properties of
the function have been abstracted to DontCareBool# (and not to True# and False#
in order to get an abstract representation that is as simple as possible while not
losing any demand information). Note that FreeNat# represents that a certain
argument is not demanded. This abstraction transformation can be mechanised:
Any singleton variable in a rule is sure not to be demanded so it is abstracted
to FreeNat#. The rest of variables are left as they are.
What we need next is to define the functions that assert when a term is not
free (that is, demanded when it appears as a function argument). We need one
such function for every data constructor of type NatDemand#:
FreeNat f # : NatDemand #
FreeNat f # = FreeNat #
Z f # : NatDemand #
Z f # = Z#
S
S
S
S

f#
f#
f#
f#

: NatDemand # → NatDemand #
FreeNat # = S# FreeNat #
Z# = S# Z#
(S# ) = S# FreeNat #

We also need the catamorphsims that link the functions above to the constructors
belonging to the type NatDemand#:

33
C freeNat : NatDemand #
C freeNat : FreeNat f #
C Z : NatDemand #
C Z : Z f#
C S : NatDemand # → NatDemand #
C S (S# x) = S f # ( C S x)

As we did in the previous example, we now have to apply the following steps to
a program composed of the rules for leq#, freeNat f#, Z f# and S f#:
– Apply an unfolding iteration.
– Apply the catamorphisms to the heads of the resulting facts.
– Evaluate the resulting head expressions.
The fixed point is reached at the second iteration (I2 ). It contains the following:
∗ leq #(Z#, FreeNat #) = DontCareBool #
∗ leq #(S#( FreeNat #),Z#) = DontCareBool #
∗ leq #(S#( FreeNat #),S#( FreeNat #)) = DontCareBool #
∗ z f # = Z#
∗ s f #( FreeNat #) = S#( FreeNat #)
∗ s f #(Z#) = S#( FreeNat #)
∗ s f #(S#(b)) = S#( FreeNat #)
∗ freeNat f # = FreeNat #

That means that leq# does not demand its second argument if the first one
is Z# (since FreeNat# represents no demand at all). However, leq# demands its
second argument if the first one is headed by S#. Note that we are considering
top level positions for the arguments only but that deeper positions can be easily
considered by just extending s f#.

D

Validity of the Unfolded Code

The lemma below supports the validity of the code generated by the unfolding
process:
D.1

Proof of Lemma 1

Let H be a fact generated by unfolding rule Λ and belonging to interpretation
In . Let {Si (i : 1..m)} be the set of facts that belong to In+1 , that have been
generated by unfolding Λ and which overlap with H.
By reductio ad absurdum, let us think that, even in the conditions stated, the
Si do not cover all the cases that H covers. Then, it must be possible to build at
least one fact S ′ that overlaps with H but that does not overlap with any fact
Si .
In order to build a fact like S ′ , the following options can be taken:

34

1. Choose H such that its pattern and/or guard does not match with any of
the rules for f .
2. When unfolding H, use a fact that has not been used when calculating the
facts {Si (i : 1..m)}.
However, condition 1 is impossible since all the function definitions are assumed
to be complete (i.e. there is no fact for f which does not match a rule) and
to have only generating rules. In addition, condition 2 is also impossible since
unfold uses all the existing facts by definition.
Note that the condition which requires that the rules be generative cannot
be dropped since a complete function having one or more non-generative rules
would have some facts removed from In+1 by clean, which would render the
function definition incomplete in that interpretation.
Therefore, no fact like S ′ can exist. We have reached a contradiction and
thus we have proved that under the conditions stated for P , clean can always
get rid of the most general fact.
D.2

Proof of Lemma 2

If program P does not have overlapping rules then any pair of rules l | g = r
and l′ | g ′ = r′ must meet one of the following conditions:
1. There is no unifier between l and l′ .
2. If a substitution σ is such that σ = mgu(l, l′ ), then the constraint g ∧ σ(g ′ )
is unsatisfiable.
At every application, the unfold function takes a rule and applies a substitution
to its pattern as well as a (possible) conjunction to its guard. Now:
1. If the two rules given do not overlap because l and l′ cannot be unified,
applying any substitution to them makes them even less unifiable.
2. If the two rules given do not overlap because l and l′ can be unified but
the conjunction of their guards cannot be satisfied, adding a conjunction to
either guards makes their combined satisfiability even less likely.
Up to this point, we have shown that the unfoldings of any two non overlapping rules cannot give rise to overlapping facts but the facts generated by the
unfolding of a single rule may still contain overlapping pairs. In order to prove
that the unfoldings of a single rule from a program P can be written without
overlappings, we need to use the function ueval that was defined in Sect. B.1.
We now want to prove that, for any single rule R belonging to a program P
without overlapping rules, the unfoldings of R carry the same meaning with or
without the cleaning phase. That is, let us call PR = unfold (R, I∞ ):
ueval (PR , c ◮ e) = ueval (clean(PR ), c ◮ e) ∀c ◮ e ∈ E

(3)

We will prove that Equation 3 holds by induction on the number of full applications of symbols of FS held in c and e combined.

35

Base case: If neither c nor e have any full application of symbols of FS ,
then both c and e are expressions (terms which may include calls to predefined
functions) and therefore cannot be unfolded any more. Their value (as computed
by ueval ) does not depend on the interpretation used, so Equation 3 trivially
holds.
Induction step: Let us assume that Equation 3 holds if c and e have a
combined total of n full applications of symbols of FS and let us try to prove that
Equation 3 holds when c and e have a combined total of n + 1 full applications
of symbols of FS .
In order to do that, let us define an expression e′ which has exactly one more
application of symbols of FS than e (the reasoning over c would be analogous).
Let us define e′ = e[f t1 . . . tn ]|o where e|o ∈ E which no full invocations of
symbols of FS , f ∈ FS , ti ∈ T . This guarantees that e′ has one more full
application of symbols of FS than e. Since the induction hypothesis holds for
c ◮ e, all we have to prove is:
ueval (PR , True ◮ f t1 . . . tn ) = ueval (clean P (PR ), True ◮ f t1 . . . tn )

(4)

Now, if PR does not contain overlapping facts or does not contain facts about
f at all, the Equation above trivially holds since the interpretations PR and
clean P (PR ) are the same by definition of clean.
Let us now assume that PR contains (maybe among others), the following
facts:
– F ≡ f p1 . . . pn | c = b
– Fi ≡ σi (f p1 . . . pn | c ∧ ci = b) (i : 1..m)
That is, the facts Fi overlap F and Fi are more specific than F . Then, by
definition of clean, clean P (PR ) will hold the facts Fi together with a new fact:
F ′ ≡ f p1 . . . pn | c ∧

^
(nunif ((p1 , . . . , pn ), σi (p1 , . . . , pn )) ∨ not (σi (ci ))) = b
i

Let χ = f t1 . . . tn . The following cases can occur:
– If χ is not unfoldable by F , then it is not unfoldable by any of the more
specific facts (the Fi and F ′ ), so Equation 4 holds.
– If χ is unfoldable by F but not by any of the Fi , then χ is unfoldable by F ′ ,
which returns the same result as F .
– Lastly, if χ is unfoldable by F and one of the Fi , then the left side of Equation
F
4 returns two values (let them be cF ◮ eF and cF
i ◮ ei ) which verify
F
F
F
F
c ◮ e ⊑ ci ◮ ei . Since all the functions have to be well-defined, the
value for χ has to be the greatest of the two mandatorily. The right side of
F
Equation 4 returns only the value cF
i ◮ ei by definition of clean (which will
have removed F from PR and replaced it by F ′ which will not be usable to
unfold χ).

