Under consideration for publication in Theory and Practice of Logic Programming  1

A Correct, Precise and Efficient Integration of Set-Sharing, Freeness and Linearity for the

Analysis of Finite and Rational Tree Languages∗

PATRICIA M. HILL

School of Computing, University of Leeds, Leeds, U.K.

                            (e-mail: hill@comp.leeds.ac.uk)

ENEA ZAFFANELLA, ROBERTO BAGNARA

Department of Mathematics, University of Parma, Italy

                      (e-mail: {zaffanella,bagnara}@cs.unipr.it)

Abstract

It is well-known that freeness and linearity information positively interact with aliasing information, allowing both the precision and the efficiency of the sharing analysis of logic programs to be improved. In this paper we present a novel combination of set-sharing with freeness and linearity information, which is characterized by an improved abstract unification operator. We provide a new abstraction function and prove the correctness of the analysis for both the finite tree and the rational tree cases. Moreover, we show that the same notion of redundant information as identified in (Bagnara et al. 2002; Zaffanella et al. 2002) also applies to this abstract domain combination: this allows for the implementation of an abstract unification operator running in polynomial time and achieving the same precision on all the considered observable properties.

KEYWORDS: Abstract Interpretation; Logic Programming; Abstract Unification; Rational Trees; Set-Sharing; Freeness; Linearity.

1 Introduction

Even though the set-sharing domain is, in a sense, remarkably precise, more precision is attainable by combining it with other domains. In particular, freeness and linearity information has received much attention by the literature on sharing analysis (recall that a variable is said to be free if it is not bound to a non-variable term; it is linear if it is not bound to a term containing multiple occurrences of another variable).

∗ The present work has been funded by MURST projects “Automatic Program Certification by Abstract Interpretation”, “Abstract Interpretation, type systems and control-flow analysis”, and “Automatic Aggregate- and Number-Reasoning for Computing: from Decision Algorithms to Constraint Programming with Multisets, Sets, and Maps”; by the Integrated Action Italy-Spain “Advanced Development Environments for Logic Programs”; by the University of Parma’s FIL scientific research project (ex 60%) “Pure and applied mathematics”; and by the UK’s Engineering and Physical Sciences Research Council (EPSRC) under grant M05645.

As argued informally by Søndergaard (Søndergaard 1986), the mutual interaction between linearity and aliasing information can improve the accuracy of a sharing analysis. This observation has been formally applied in (Codish et al. 1991) to the specification of the abstract mgu operator for the domain ASub. In his PhD thesis (Langen 1990), Langen proposed a similar integration with linearity, but for the set-sharing domain. He has also shown how the aliasing information allows to compute freeness with a good degree of accuracy (however, freeness information was not exploited to improve aliasing). King (King 1994) has also shown how a more refined tracking of linearity allows for further precision improvements.

The synergy attainable from a bi-directional interaction between aliasing and freeness information was initially pointed out by Muthukumar and Hermenegildo (Muthukumar and Hermenegildo 1991; Muthukumar and Hermenegildo 1992). Since then, several authors considered the integration of set-sharing with freeness, sometimes also including additional explicit structural information (Codish et al. 1993; Codish et al. 1996; Filé 1994; King and Soper 1994).

Building on the results obtained in (Søndergaard 1986), (Codish et al. 1991) and (Muthukumar and Hermenegildo 1991), but independently from (Langen 1990), Hans and Winkler (Hans and Winkler 1992) proposed a combined integration of freeness and linearity information with set-sharing. Similar combinations have been proposed in (Bruynooghe and Codish 1993; Bruynooghe et al. 1994a; Bruynooghe et al. 1994b). From a more pragmatic point of view, Codish et al. (Codish et al. 1993; Codish et al. 1995) integrate the information captured by the domains of (Søndergaard 1986) and (Muthukumar and Hermenegildo 1991) by performing the analysis with both domains at the same time, exchanging information between the two components at each step.

Most of the above proposals differ in the carrier of the underlying abstract domain. Even when considering the simplest domain combinations where explicit structural information is ignored, there is no general consensus on the specification of the abstract unification procedure. From a theoretical point of view, once the abstract domain has been related to the concrete one by means of a Galois connection, it is always possible to specify the best correct approximation of each operator of the concrete semantics. However, empirical observations suggest that sub-optimal operators are likely to result in better complexity/precision trade-offs (Bagnara et al. 2000). As a consequence, it is almost impossible to identify “the right combination” of variable aliasing with freeness and linearity information, at least when practical issues, such as the complexity of the abstract unification procedure, are taken into account.

Correct and Efficient Integration of Set-Sharing, Freeness and Linearity 3

Given this state of affairs, we will now consider a domain combination whose carrier is essentially the same as specified by Langen (Langen 1990) and Hans and Winkler (Hans and Winkler 1992). (The same domain combination was also considered by Bruynooghe et al. (Bruynooghe et al. 1994a; Bruynooghe et al. 1994b), but with the addition of compoundness and explicit structural information.) The novelty of our proposal lies in the specification of an improved abstract unification procedure, better exploiting the interaction between sharing and linearity. As a matter of fact, we provide an example showing that all previous approaches to the combination of set-sharing with freeness and linearity are not uniformly more precise than the analysis based on the ASub domain (Codish et al. 1991; King 2000; Søndergaard 1986), whereas such a property is enjoyed by our proposal.

By extending the results of (Hill et al. 2002) to this combination, we provide a new abstraction function that can be applied to any logic language computing on domains of syntactic structures, with or without the occurs-check; by using this abstraction function, we also prove the correctness of the new abstract unification procedure. Moreover, we show that the same notion of redundant information as identified in (Bagnara et al. 2002; Zaffanella et al. 2002) also applies to this abstract domain combination. As a consequence, it is possible to implement an algorithm for abstract unification running in polynomial time and still obtain the same precision on all the considered observables: groundness, independence, freeness and linearity.

This paper is based on (Zaffanella 2001, Chapter 6), the PhD thesis of the second author. In Section 2, we define some notation and recall the basic concepts used later in the paper. In Section 3, we present the domain SFL that integrates set-sharing, freeness and linearity. In Section 4, we show that SFL is uniformly more precise than the domain ASub, whereas all the previous proposals for a domain integrating set-sharing and linearity fail to satisfy such a property. In Section 5, we show that the domain SFL can be simplified by removing some redundant information. In Section 6, we provide an experimental evaluation using the China analyzer (Bagnara 1997). In Section 7, we discuss some related work. Section 8 concludes with some final remarks. The proofs of the results stated here are not included but all of them are available in an extended version of this paper (Hill et al. 2003).

2 Preliminaries

For a set S, ℘(S) is the powerset of S. The cardinality of S is denoted by #S and the empty set is denoted by ∅. The notation ℘_{f}(S) stands for the set of all the finite subsets of S, while the notation S ⊆_{f} T stands for S ∈ ℘_{f}(T). The set of all finite sequences of elements of S is denoted by S^{∗}, the empty sequence by ϵ, and the concatenation of s_{1}, s_{2} ∈ S^{∗} is denoted by s_{1} . s_{2}.

2.1 Terms and Trees

Let Sig denote a possibly infinite set of function symbols, ranked over the set of natural numbers. Let Vars denote a denumerable set of variables, disjoint from Sig. Then Terms denotes the free algebra of all (possibly infinite) terms in the signature Sig having variables in Vars. Thus a term can be seen as an ordered labeled tree, possibly having some infinite paths and possibly containing variables: every inner node is labeled with a function symbol in Sig with a rank matching the number of the node’s immediate descendants, whereas every leaf is labeled by either a variable in Vars or a function symbol in Sig having rank 0 (a constant). It is assumed that Sig contains at least two distinct function symbols, with one of them having rank 0.

If t ∈ Terms then vars(t) and mvars(t) denote the set and the multiset of variables occurring in t, respectively. We will also write vars(o) to denote the set of variables occurring in an arbitrary syntactic object o.

Suppose s, t ∈ Terms: s and t are independent if vars(s) ∩ vars(t) = ∅; we say that variable y occurs linearly in t, more briefly written using the predication occ lin(y, t), if y occurs exactly once in mvars(t); t is said to be ground if vars(t) = ∅; t is free if t ∈ Vars; t is linear if, for all y ∈ vars(t), we have occ lin(y, t); finally, t is a finite term (or Herbrand term) if it contains a finite number of occurrences of function symbols. The sets of all ground, linear and finite terms are denoted by GTerms, LTerms and HTerms, respectively.

2.2 Substitutions

A substitution is a total function σ: Vars → HTerms that is the identity almost everywhere; in other words, the domain of σ,

dom(σ) =^{def} { x ∈ Vars | σ(x) ≠ x },

is finite. Given a substitution σ: Vars → HTerms, we overload the symbol ‘σ’ so as to denote also the function σ: HTerms → HTerms defined as follows, for each term t ∈ HTerms:

σ(t) =^{def} \begin{cases}t, & if t is a constant symbol; \\ σ(t), & if t ∈ Vars; \\ f(σ(t_{1}), …, σ(t_{n})), & if t = f(t_{1}, …, t_{n}). \end{cases}

If t ∈ HTerms, we write tσ to denote σ(t). Note that, for each substitution σ and each finite term t ∈ HTerms, if tσ ∈ Vars, then t ∈ Vars.

If x ∈ Vars and t ∈ HTerms \ {x}, then x ↦ t is called a binding. The set of all bindings is denoted by Bind. Substitutions are denoted by the set of their bindings, thus a substitution σ is identified with the (finite) set

{ x ↦ xσ | x ∈ dom(σ) }.

We denote by vars(σ) the set of variables occurring in the bindings of σ. We also define range(σ) =^{def} ⋃{ vars(xσ) | x ∈ dom(σ) }.

A substitution is said to be circular if, for n > 1, it has the form

{x_{1} ↦ x_{2}, …, x_{n−1} ↦ x_{n}, x_{n} ↦ x_{1}},

where x_{1}, …, x_{n} are distinct variables. A substitution is in rational solved form if it has no circular subset. The set of all substitutions in rational solved form is denoted by RSubst. A substitution σ is idempotent if, for all t ∈ Terms, we have tσσ = tσ. Equivalently, σ is idempotent if and only if dom(σ) ∩ range(σ) = ∅. The set of all idempotent substitutions is denoted by ISubst and ISubst ⊂ RSubst.

The composition of substitutions is defined in the usual way. Thus τ ∘ σ is the substitution such that, for all terms t ∈ HTerms,

t(τ ∘ σ) = tστ

and has the formulation

τ ∘ σ = { x ↦ xστ | x ∈ dom(σ) ∪ dom(τ), x ≠ xστ }.  (1)

As usual, σ^{0} denotes the identity function (i.e., the empty substitution) and, when i > 0, σ^{i} denotes the substitution (σ ∘ σ^{i−1}).

For each σ ∈ RSubst and s ∈ HTerms, the sequence of finite terms

σ^{0}(s), σ^{1}(s), σ^{2}(s), …

converges to a (possibly infinite) term, denoted σ^{∞}(s) (Intrigila and Zilli 1996; King 2000). Therefore, the function rt: HTerms × RSubst → Terms such that

rt(s, σ) =^{def} σ^{∞}(s)

is well defined. Note that, in general, this function is not a substitution: while having a finite domain, its “bindings” x ↦ rt(x, σ) can map a domain variable x into a term rt(x, σ) ∈ Terms \ HTerms. However, as the name of the function suggests, the term rt(x, σ) is granted to be rational, meaning that it can only have a finite number of distinct subterms and hence, be finitely represented.

Example 1 Consider the substitutions

σ_{1} = {x ↦ f(z), y ↦ a} ∈ ISubst,
σ_{2} = {x ↦ f(y), y ↦ a} ∈ RSubst \ ISubst,
σ_{3} = {x ↦ f(x)}  ∈ RSubst \ ISubst,
σ_{4} = {x ↦ f(y), y ↦ f(x)} ∈ RSubst \ ISubst,
σ_{5} = {x ↦ y, y ↦ x}  ∉ RSubst.

Note that there are substitutions, such as σ_{2}, that are not idempotent and nonetheless define finite trees only; namely, rt(x, σ_{2}) = f(a). Similarly, there are other substitutions, such as σ_{4}, whose bindings are not explicitly cyclic and nonetheless define rational trees that are infinite; namely, rt(x, σ_{4}) = f(f(f(⋯))). Finally note that the ‘rt’ function is not defined on σ_{5} ∉ RSubst.

2.3 Equality Theories

An equation is of the form s = t where s, t ∈ HTerms. Eqs denotes the set of all equations. A substitution σ may be regarded as a finite set of equations, that is, as the set { x = t | (x ↦ t) ∈ σ }. We say that a set of equations e is in rational solved form if { s ↦ t | (s = t) ∈ e } ∈ RSubst. In the rest of the paper, we will often write a substitution σ ∈ RSubst to denote a set of equations in rational solved form (and vice versa). As is common in research work involving equality, we overload the symbol ‘=’ and use it to denote both equality and to represent syntactic identity. The context makes it clear what is intended.

Let {r, s, t, s_{1}, …, s_{n}, t_{1}, …, t_{n}} ⊆ HTerms. We assume that any equality theory T over Terms includes the congruence axioms denoted by the following schemata:

s = s,  (2)

s = t ↔ t = s,  (3)
r = s ∧ s = t → r = t,  (4)
s_{1} = t_{1} ∧ ⋯ ∧ s_{n} = t_{n} → f(s_{1}, …, s_{n}) = f(t_{1}, …, t_{n}).  (5)

In logic programming and most implementations of Prolog it is usual to assume an equality theory based on syntactic identity. This consists of the congruence axioms together with the identity axioms denoted by the following schemata, where f and g are distinct function symbols or n ≠ m:

f(s_{1}, …, s_{n}) = f(t_{1}, …, t_{n}) → s_{1} = t_{1} ∧ ⋯ ∧ s_{n} = t_{n},  (6)
¬(f(s_{1}, …, s_{n}) = g(t_{1}, …, t_{m})).  (7)

The axioms characterized by schemata (6) and (7) ensure the equality theory depends only on the syntax. The equality theory for a non-syntactic domain replaces these axioms by ones that depend instead on the semantics of the domain and, in particular, on the interpretation given to functor symbols.

The equality theory of Clark (Clark 1978), denoted FT , on which pure logic programming is based, usually called the Herbrand equality theory, is given by the congruence axioms, the identity axioms, and the axiom schema

∀z ∈ Vars : ∀t ∈ (HTerms \ Vars) : z ∈ vars(t) → ¬(z = t).  (8)

Axioms characterized by the schema (8) are called the occurs-check axioms and are an essential part of the standard unification procedure in SLD-resolution.

An alternative approach used in some implementations of logic programming systems, such as Prolog II, SICStus and Oz, does not require the occurs-check axioms. This approach is based on the theory of rational trees (Colmerauer 1982; Colmerauer 1984), denoted RT . It assumes the congruence axioms and the identity axioms together with a uniqueness axiom for each substitution in rational solved form. Informally speaking these state that, after assigning a ground rational tree to each variable which is not in the domain, the substitution uniquely defines a ground rational tree for each of its domain variables. Note that being in rational solved form is a very weak property. Indeed, unification algorithms returning a set of equations in rational solved form are allowed to be much more “lazy” than one would expect. We refer the interested reader to (Jaffar et al. 1987; Keisu 1994; Maher 1988) for details on the subject.

In the sequel we use the expression “equality theory” to denote any consistent, decidable theory T satisfying the congruence axioms. We also use the expression “syntactic equality theory” to denote any equality theory T also satisfying the identity axioms.

We say that a substitution σ ∈ RSubst is satisfiable in an equality theory T if, when interpreting σ as an equation system in rational solved form,

T ⊢ ∀(Vars \ dom(σ)) : ∃ dom(σ) . σ.

Let e ∈ ℘_{f}(Eqs) be a set of equations in an equality theory T. A substitution σ ∈ RSubst is called a solution for e in T if σ is satisfiable in T and T ⊢ ∀(σ → e); we say that e is satisfiable if it has a solution. If vars(σ) ⊆ vars(e), then σ is said to be a relevant solution for e. In addition, σ is a most general solution for e in T if T ⊢ ∀(σ ↔ e). In this paper, a most general solution is always a relevant solution of e. When the theory T is clear from the context, the set of all the relevant most general solutions for e in T is denoted by mgs(e).

Example 2 Let e = {g(x) = g(f(y)), f(x) = y, z = g(w)} and

σ = {x ↦ f(y), y ↦ f(x), z ↦ g(w)}.

Then, for any syntactic equality theory T, we have T ⊢ ∀(σ ↔ e). Since σ ∈ RSubst, then σ and hence e is satisfiable in RT . Intuitively, whatever rational tree t_{w} is assigned to the parameter variable w, there exist rational trees t_{x}, t_{y} and t_{z} that, when assigned to the domain variables x, y and z, will turn σ into a set of trivial identities; namely, let t_{x} and t_{y} be both equal to the infinite rational tree f(f(f(⋯))), which is usually denoted by f^{ω}, and let t_{z} be the rational tree g(t_{w}). Thus σ is a relevant most general solution for e in RT . In contrast,

τ = {x ↦ f(y), y ↦ f(x), z ↦ g(f(a))}

is just a relevant solution for e in RT . Also observe that, for any equality theory T,

T ⊢ ∀(σ → {x = f(f(x))})

so that σ does not satisfy the occurs-check axioms. Therefore, neither σ nor e are satisfiable in the Herbrand equality theory FT . Intuitively, there is no finite tree t_{x} such that t_{x} = f(f(t_{x})).

We have the following useful result regarding ‘rt’ and satisfiable substitutions that are equivalent with respect to any given syntactic equality theory.

Proposition 3 Let σ, τ ∈ RSubst be satisfiable in the syntactic equality theory T and suppose that T ⊢ ∀(σ ↔ τ). Then

rt(y, σ) ∈ Vars ⟺ rt(y, τ) ∈ Vars,  (9)
rt(y, σ) ∈ GTerms ⟺ rt(y, τ) ∈ GTerms,  (10)
rt(y, σ) ∈ LTerms ⟺ rt(y, τ) ∈ LTerms.  (11)

2.4 Galois Connections and Upper Closure Operators

Given two complete lattices (C, ≤_{C}) and (A, ≤_{A}), a Galois connection is a pair of monotonic functions α: C → A and γ: A → C such that

∀c ∈ C : c ≤_{C} γ(α(c)),  ∀a ∈ A : α(γ(a)) ≤_{A} a.

The functions α and γ are said to be the abstraction and concretization functions, respectively. A Galois insertion is a Galois connection where the concretization function γ is injective.

An upper closure operator (uco) ρ: C → C on the complete lattice (C, ≤_{C}) is a monotonic, idempotent and extensive^{1} self-map. The set of all uco’s on C, denoted by uco(C), is itself a complete lattice. For any ρ ∈ uco(C), the set ρ(C), i.e., the image under ρ of the lattice carrier, is a complete lattice under the same partial order ≤_{C} defined on C. Given a Galois connection, the function ρ =^{def} γ ∘α is an element of uco(C). The presentation of abstract interpretation in terms of Galois connections can be rephrased by using uco’s. In particular, the partial order ⊑ defined on uco(C) formalizes the intuition of an abstract domain being more precise than another one; moreover, given two elements ρ_{1}, ρ_{2} ∈ uco(C), their reduced product (Cousot and Cousot 1979), denoted ρ_{1} ⊓ ρ_{2}, is their glb on uco(C).

2.5 The Set-Sharing Domain

The set-sharing domain of Jacobs and Langen (Jacobs and Langen 1989), encodes both aliasing and groundness information. Let VI ⊆_{f} Vars be a fixed and finite set of variables of interest. An element of the set-sharing domain (a sharing set) is a set of subsets of VI (the sharing groups). Note that the empty set is not a sharing group.

Definition 4 (The set-sharing lattice.) Let SG =^{def} ℘(VI ) \ {∅} be the set of sharing groups. The set-sharing lattice is defined as SH =^{def} ℘(SG), ordered by subset inclusion.

The following operators on SH are needed for the specification of the abstract semantics.

Definition 5 (Auxiliary operators on SH .) For each sh, sh_{1}, sh_{2} ∈ SH and each V ⊆ VI , we define the following functions: the star-union function (·)^{⋆}: SH → SH , is defined as

sh^{⋆} =^{def} { S ∈ SG | ∃n ≥ 1 . ∃S_{1}, …, S_{n} ∈ sh . S = S_{1} ∪ ⋯ ∪ S_{n} };

the extraction of the relevant component of sh with respect to V is encoded by rel: ℘(VI ) × SH → SH defined as

rel(V, sh) =^{def} { S ∈ sh | S ∩ V ≠ ∅ };

the irrelevant component of sh with respect to V is thus defined as

\overline{rel}(V, sh) =^{def} sh \ rel(V, sh);

the binary union function bin: SH × SH → SH is defined as

bin(sh_{1}, sh_{2}) =^{def} { S_{1} ∪ S_{2} | S_{1} ∈ sh_{1}, S_{2} ∈ sh_{2} };

1 Namely, c ≤_{C} ρ(c) for each c ∈ C.

the self-bin-union operation on SH is defined as

sh^{2} =^{def} bin(sh, sh);

the abstract existential quantification function aexists: SH ×℘(VI ) → SH is defined as

aexists(sh, V) =^{def} { S \ V | S ∈ sh, S \ V ≠ ∅ } ∪ { {x} | x ∈ V }.

In (Bagnara et al. 1997; Bagnara et al. 2002) it was shown that the domain SH contains many elements that are redundant for the computation of the actual observable properties of the analysis, definite groundness and definite independence. The following formalization of these observables is a rewording of the definitions provided in (Zaffanella et al. 1999; Zaffanella et al. 2002).

Definition 6 (The observables of SH .) The groundness and independence observables (on SH ) ρ_{Con}, ρ_{PS} ∈ uco(SH ) are defined, for each sh ∈ SH , by

ρ_{Con}(sh) =^{def} { S ∈ SG | S ⊆ vars(sh) },
ρ_{PS}(sh) =^{def} { S ∈ SG | (P ⊆ S ∧ #P = 2) ⟹ (∃T ∈ sh . P ⊆ T) }.

Note that, as usual in sharing analysis domains, definite groundness and definite independence are both represented by encoding possible non-groundness and possible pair-sharing information.

The abstract domain PSD (Bagnara et al. 2002; Zaffanella et al. 2002) is the simplest abstraction of the domain SH that still preserves the same precision on groundness and independence.

Definition 7 (The pair-sharing dependency lattice PSD.) The operator ρ_{PSD} ∈ uco(SH ) is defined, for each sh ∈ SH , by

ρ_{PSD}(sh) =^{def} { S ∈ SG | ∀y ∈ S : S = ⋃{ U ∈ sh | y ∈ U ⊆ S } }.

The pair-sharing dependency lattice is PSD =^{def} ρ_{PSD}(SH ).

In the following example we provide an intuitive interpretation of the approximation induced by the three upper closure operators of Definitions 6 and 7.

Example 8 Let VI = {v, w, x, y, z} and consider^{2} sh = {vx, vy, xy, xyz}. Then

ρ_{Con}(sh) = {v, vx, vxy, vxyz, vxz, vy, vyz, vz, x, xy, xyz, xz, y, yz, z},
ρ_{PS}(sh) = {v, vx, vxy, vy, w, x, xy, xyz, xz, y, yz, z},

2 In this and all the following examples, we will adopt a simplified notation for a setsharing element sh, omitting inner braces. For instance, we will write {xy, xz, yz} to denote {{x, y}, {x, z}, {y, z}}.

ρ_{PSD}(sh) = {vx, vxy, vy, xy, xyz}.

When observing ρ_{Con}(sh), the only information available is that variable w does not occur in a sharing group; intuitively, this means that w is definitely ground. All the other information encoded in sh is lost; for instance, in sh variables v and z never occur in the same sharing group (i.e., they are definitely independent), while this happens in ρ_{Con}(sh).

When observing ρ_{PS}(sh), it should be noted that two distinct variables occur in the same sharing group if and only if they were also occurring together in a sharing group of sh, so that the definite independence information is preserved (e.g., v and z keep their independence). On the other hand, all the variables in VI occur as singletons in ρ_{PS}(sh) whether or not they are known to be ground; for instance, {w} occurs in ρ_{PS}(sh) although w does not occur in any sharing group in sh.

By noting that ρ_{PSD}(sh) ⊂ ρ_{Con}(sh) ∩ ρ_{PS}(sh), it follows that ρ_{PSD}(sh) preserves both the definite groundness and the definite independence information of sh; moreover, as the inclusion is strict, ρ_{PSD}(sh) encodes other information, such as variable covering (the interested reader is referred to (Bagnara et al. 2002; Zaffanella et al. 2002) for a more formal discussion).

2.6 Variable-Idempotent Substitutions

One of the key concepts used in (Hill et al. 2003) for the proofs of the correctness results stated in this paper is that of variable-idempotence. For the interested reader, we provide here a brief introduction to variable-idempotent substitutions, although these are not referred to elsewhere in the paper.

The definition of idempotence requires that repeated applications of a substitution do not change the syntactic structure of a term and idempotent substitutions are normally the preferred form of a solution to a set of equations. However, in the domain of rational trees, a set of solvable equations does not necessarily have an idempotent solution (for instance, in Example 2, the set of equations e has no idempotent solution). On the other hand, several abstractions of terms, such as the ones commonly used for sharing analysis, are only interested in the set of variables occurring in a term and not in the concrete structure that contains them. Thus, for applications such as sharing analysis, a useful way to relax the definition of idempotence is to ignore the structure of terms and just require that the repeated application of a substitution leaves the set of variables in a term invariant.

Definition 9 (Variable-idempotence.) A substitution σ ∈ RSubst is variable-idempotent^{3} if and only if for all t ∈ HTerms we have

vars(tσσ) = vars(tσ).

3 This definition, which is the same as that originally provided in (Hill et al. 1998), is slightly stronger than the one adopted in (Hill et al. 2002), which disregarded the domain variables of the substitution. The adoption of this stronger definition allows for some simplifications in the correctness proofs for freeness and linearity.

The set of variable-idempotent substitutions is denoted VSubst.

As any idempotent substitution is also variable-idempotent, we have ISubst ⊂ VSubst ⊂ RSubst.

Example 10 Consider the following substitutions which are all in RSubst.

σ_{1} = {x ↦ f(y)}  ∈ ISubst ⊂ VSubst,
σ_{2} = {x ↦ f(x)}  ∈ VSubst \ ISubst,
σ_{3} = {x ↦ f(y, z), y ↦ f(z, y)} ∈ VSubst \ ISubst,
σ_{4} = {x ↦ y, y ↦ f(x, y)}  ∉ VSubst.

3 The Domain SFL

The abstract domain SFL is made up of three components, providing different kinds of sharing information regarding the set of variables of interest VI : the first component is the set-sharing domain SH of Jacobs and Langen (Jacobs and Langen 1989); the other two components provide freeness and linearity information, each represented by simply recording those variables of interest that are known to enjoy the corresponding property.

Definition 11 (The domain SFL.) Let F =^{def} ℘(VI ) and L =^{def} ℘(VI ) be partially ordered by reverse subset inclusion. The abstract domain SFL is defined as

SFL =^{def} { ⟨sh, f, l⟩ | sh ∈ SH , f ∈ F, l ∈ L }

and is ordered by ≤_{S}, the component-wise extension of the orderings defined on the sub-domains. With this ordering, SFL is a complete lattice whose least upper bound operation is denoted by alub_{S}. The bottom element ⟨∅, VI , VI ⟩ will be denoted by ⊥_{S}.

3.1 The Abstraction Function

When the concrete domain is based on the theory of finite trees, idempotent substitutions provide a finitely computable strong normal form for domain elements, meaning that different substitutions describe different sets of finite trees.^{4} In contrast, when working on a concrete domain based on the theory of rational trees, substitutions in rational solved form, while being finitely computable, no longer satisfy this property: there can be an infinite set of substitutions in rational solved form all describing the same set of rational trees (i.e., the same element in the “intended” semantics). For instance, the substitutions

σ_{n} = \{x ↦ \overbrace{f(⋯ f(}^{n} x) ⋯)\},

4 As usual, this is modulo the possible renaming of variables.

for n = 1, 2, …, all map the variable x into the same infinite rational tree f^{ω}.

Ideally, a strong normal form for the set of rational trees described by a substitution σ ∈ RSubst can be obtained by computing the limit σ^{∞}. The problem is that σ^{∞} can map domain variables to infinite rational terms and may not be in RSubst.

This poses a non-trivial problem when trying to define “good” abstraction functions, since it would be really desirable for this function to map any two equivalent concrete elements to the same abstract element. As shown in (Hill et al. 2002), the classical abstraction function for set-sharing analysis (Cortesi and Filé 1999; Jacobs and Langen 1989), which was defined only for substitutions that are idempotent, does not enjoy this property when applied, as it is, to arbitrary substitutions in rational solved form. In (Hill et al. 1998; Hill et al. 2002), this problem is solved by replacing the sharing group operator ‘sg’ of (Jacobs and Langen 1989) by an occurrence operator, ‘occ’, defined by means of a fixpoint computation. However, to simplify the presentation, here we define ‘occ’ directly by exploiting the fact that the number of iterations needed to reach the fixpoint is bounded by the number of bindings in the substitution.

Definition 12 (Occurrence operator.) For each σ ∈ RSubst and v ∈ Vars, the occurrence operator occ: RSubst × Vars → ℘_{f}(Vars) is defined as

occ(σ, v) =^{def} { y ∈ Vars | n = #σ, v ∈ vars(yσ^{n}) \ dom(σ) }.

For each σ ∈ RSubst, the operator ssets: RSubst → SH is defined as

ssets(σ) =^{def} { occ(σ, v) ∩ VI | v ∈ Vars } \ {∅}.

The operator ‘ssets’ is introduced for notational convenience only.

Example 13 Let

σ = {x_{1} ↦ f(x_{2}), x_{2} ↦ g(x_{3}, x_{4}), x_{3} ↦ x_{1}},
τ = {x_{1} ↦ f(g(x_{3}, x_{4})), x_{2} ↦ g(x_{3}, x_{4}), x_{3} ↦ f(g(x_{3}, x_{4}))}.

Then dom(σ) = dom(τ) = {x_{1}, x_{2}, x_{3}} so that occ(σ, x_{i}) = occ(τ, x_{i}) = ∅, for i = 1, 2, 3 and occ(σ, x_{4}) = occ(τ, x_{4}) = {x_{1}, x_{2}, x_{3}, x_{4}}. As a consequence, supposing that VI = {x_{1}, x_{2}, x_{3}, x_{4}}, we obtain ssets(σ) = ssets(τ) = {VI }.

In a similar way, it is possible to define suitable operators for groundness, freeness and linearity. As all ground trees are linear, a knowledge of the definite groundness information can be useful for proving properties concerning the linearity abstraction. Groundness is already encoded in the abstraction for set-sharing provided in Definition 12; nonetheless, for both a simplified notation and a clearer intuitive reading, we now explicitly define the set of variables that are associated to ground trees by a substitution in RSubst.

Definition 14 (Groundness operator.) The groundness operator gvars: RSubst → ℘_{f}(Vars) is defined, for each σ ∈ RSubst, by

gvars(σ) =^{def} { y ∈ dom(σ) | ∀v ∈ Vars : y ∉ occ(σ, v) }.

Example 15 Consider σ ∈ RSubst where

σ = {x_{1} ↦ x_{2}, x_{2} ↦ f(a), x_{3} ↦ x_{4}, x_{4} ↦ f(x_{2}, x_{4})}.

Then gvars(σ) = {x_{1}, x_{2}, x_{3}, x_{4}}. Observe that x_{1} ∈ gvars(σ) although x_{1}σ ∈ Vars. Also, x_{3} ∈ gvars(σ) although vars(x_{3}σ^{i}) = {x_{2}, x_{4}} ≠ ∅ for all i ≥ 2.

As for possible sharing, the definite freeness information can be extracted from a substitution in rational solved form by observing the result of a bounded number of applications of the substitution.

Definition 16 (Freeness operator.) The freeness operator fvars: RSubst → ℘(Vars) is defined, for each σ ∈ RSubst, by

fvars(σ) =^{def} { y ∈ Vars | n = #σ, yσ^{n} ∈ Vars }.

As σ ∈ RSubst has no circular subset, y ∈ fvars(σ) implies yσ^{n} ∈ Vars \ dom(σ).

Example 17 Let VI = {x_{1}, x_{2}, x_{3}, x_{4}, x_{5}} and consider σ ∈ RSubst where

σ = {x_{1} ↦ x_{2}, x_{2} ↦ f(x_{3}), x_{3} ↦ x_{4}, x_{4} ↦ x_{5}}.

Then fvars(σ) ∩ VI = {x_{3}, x_{4}, x_{5}}. Thus x_{1} ∉ fvars(σ) although x_{1}σ ∈ Vars. Also, x_{3} ∈ fvars(σ) although x_{3}σ ∈ dom(σ).

As in previous cases, the definite linearity information can be extracted by observing the result of a bounded number of applications of the considered substitution.

Definition 18 (Linearity operator.) The linearity operator lvars: RSubst → ℘(Vars) is defined, for each σ ∈ RSubst, by

lvars(σ) =^{def} { y ∈ Vars | n = #σ, ∀z ∈ vars(yσ^{n}) \ dom(σ) : occ lin(z, yσ^{2n}) }.

In the next example we consider the extraction of linearity from two substitutions. The substitution σ shows that, in contrast with the case of set-sharing and freeness, for linearity we may need to compute up to 2n applications, where n = #σ; the substitution τ shows that, when observing the term yτ^{2n}, multiple occurrences of domain variables have to be disregarded.

Example 19 Let VI = {x_{1}, x_{2}, x_{3}, x_{4}} and consider σ ∈ RSubst where

σ = {x_{1} ↦ x_{2}, x_{2} ↦ x_{3}, x_{3} ↦ f(x_{1}, x_{4})}.

Then lvars(σ) ∩ VI = {x_{4}}. Observe that x_{1} ∉ lvars(σ). This is because x_{4} ∉ dom(σ), x_{1}σ^{3} = f(x_{1}, x_{4}) so that x_{4} ∈ vars(x_{1}σ^{3}) and x_{1}σ^{6} = f(f(x_{1}, x_{4}), x_{4}) so that occ lin(x_{4}, x_{1}σ^{6}) does not hold. Note also that occ lin(x_{4}, x_{1}σ^{i}) holds for i = 3, 4, 5.

Consider now τ ∈ RSubst where

τ = {x_{1} ↦ f(x_{2}, x_{2}), x_{2} ↦ f(x_{2})}.

Then lvars(τ) ∩ VI = VI . Note that we have x_{1} ∈ lvars(τ) although, for all i > 0, x_{2} ∈ dom(τ) occurs more than once in the term x_{1}τ^{i}.

The occurrence, groundness, freeness and linearity operators are invariant with respect to substitutions that are equivalent in the given syntactic equality theory.

Proposition 20 Let σ, τ ∈ RSubst be satisfiable in the syntactic equality theory T and suppose that T ⊢ ∀(σ ↔ τ). Then

ssets(σ) = ssets(τ),  (12)
gvars(σ) = gvars(τ),  (13)
fvars(σ) = fvars(τ),  (14)
lvars(σ) = lvars(τ).  (15)

Moreover, these operators precisely capture the intended properties over the domain of rational trees.

Proposition 21 If σ ∈ RSubst and y, v ∈ Vars then

y ∈ occ(σ, v) ⟺ v ∈ vars(rt(y, σ)),  (16)
y ∈ gvars(σ) ⟺ rt(y, σ) ∈ GTerms,  (17)
y ∈ fvars(σ) ⟺ rt(y, σ) ∈ Vars,  (18)
y ∈ lvars(σ) ⟺ rt(y, σ) ∈ LTerms.  (19)

It follows from (16) and (18) that any free variable necessarily shares (at least, with itself). Also, as Vars ∪ GTerms ⊂ LTerms, it follows from (17), (18) and (19) that any variable that is either ground or free is also necessarily linear. Thus we have the following corollary.

Corollary 22 If σ ∈ RSubst, then

fvars(σ) ⊆ vars(ssets(σ)),
fvars(σ) ∪ gvars(σ) ⊆ lvars(σ).

We are now in position to define the abstraction function mapping rational trees to elements of the domain SFL.

Definition 23 (The abstraction function for SFL.) For each substitution σ ∈ RSubst, the function α_{S}: RSubst → SFL is defined by

α_{S}(σ) =^{def} ⟨ssets(σ), fvars(σ) ∩ VI , lvars(σ) ∩ VI ⟩,

The concrete domain ℘(RSubst) is related to SFL by means of the abstraction function α_{S}: ℘(RSubst) → SFL such that, for each Σ ∈ ℘(RSubst),

α_{S}(Σ) =^{def} alub_{S}{ α_{S}(σ) | σ ∈ Σ }.

Since the abstraction function α_{S} is additive, the concretization function is given by the adjoint (Cousot and Cousot 1977)

γ_{S}(⟨sh, f, l⟩) =^{def} { σ ∈ RSubst | ssets(σ) ⊆ sh, fvars(σ) ⊇ f, lvars(σ) ⊇ l }.

With Definition 23 and Proposition 20, one of our objectives is fulfilled: substitutions in RSubst that are equivalent have the same abstraction.

Corollary 24 Let σ, τ ∈ RSubst be satisfiable in the syntactic equality theory T and suppose T ⊢ ∀(σ ↔ τ). Then α_{S}(σ) = α_{S}(τ).

Observe that the Galois connection defined by the functions α_{S} and γ_{S} is not a Galois insertion since different abstract elements are mapped by γ_{S} to the same set of concrete computation states. To see this it is sufficient to observe that, by Corollary 22, any abstract element d = ⟨sh, f, l⟩ ∈ SFL such that f ⊈ vars(sh), as is the case for the bottom element ⊥_{S}, satisfies γ_{S}(d) = γ_{S}(⊥_{S}) = ∅; thus, all such d’s will represent the semantics of those program fragments that have no successful computations. Similarly, by letting V = (VI \ vars(sh)) ∪ f, it can be seen that, for any l′ such that V ∪l = V ∪l′, we have, again by Corollary 22, γ_{S}(d) = γ_{S}(⟨sh, f, l′⟩).

Of course, by taking the abstract domain as the subset of SFL that is the codomain of α_{S}, we would have a Galois insertion. However, apart from the simple cases shown above, it is somehow difficult to explicitly characterize such a set. For instance, as observed in (Filé 1994), if

d = ⟨{xy, xz, yz}, {x, y, z}, {x, y, z}⟩ ∈ SFL

we have γ_{S}(d) = γ_{S}(⊥_{S}) = ∅. It is worth stressing that these “spurious” elements do not compromise the correctness of the analysis and, although they can affect the precision of the analysis, they rarely occur in practice (Bagnara et al. 2000; Zaffanella 2001).

3.2 The Abstract Operators

The specification of the abstract unification operator on the domain SFL is rather complex, since it is based on a very detailed case analysis. To achieve some modularity, that will be also useful when proving its correctness, in the next definition we introduce several auxiliary abstract operators.

Definition 25 (Auxiliary operators in SFL.) Let s, t ∈ HTerms be finite terms such that vars(s) ∪ vars(t) ⊆ VI . For each d = ⟨sh, f, l⟩ ∈ SFL we define the following predicates: s and t are independent in d if and only if ind_{d} : HTerms^{2} → Bool holds for (s, t), where

ind_{d}(s, t) =^{def} (rel(vars(s), sh) ∩ rel(vars(t), sh) = ∅);

t is ground in d if and only if ground_{d} : HTerms → Bool holds for t, where

ground_{d}(t) =^{def} (vars(t) ⊆ VI \ vars(sh));

y ∈ vars(t) occurs linearly (in t) in d if and only if occ lin_{d} : VI × HTerms → Bool holds for (y, t), where

occ lin_{d}(y, t) =^{def} ground_{d}(y) ∨ (occ lin(y, t) ∧ (y ∈ l)
∧ ∀z ∈ vars(t) : (y ≠ z ⟹ ind_{d}(y, z)));

t is free in d if and only if free_{d} : HTerms → Bool holds for t, where

free_{d}(t) =^{def} (t ∈ f);

t is linear in d if and only if lin_{d} : HTerms → Bool holds for t, where

lin_{d}(t) =^{def} ∀y ∈ vars(t) : occ lin_{d}(y, t).

The function share with_{d} : HTerms → ℘(VI ) yields the set of variables of interest that may share with the given term. For each t ∈ HTerms,

share with_{d}(t) =^{def} vars(rel(vars(t), sh)).

The function cyclic_{x}^{t}: SH → SH strengthens the sharing set sh by forcing the coupling of x with t. For each sh ∈ SH and each (x ↦ t) ∈ Bind,

cyclic_{x}^{t}(sh) =^{def} \overline{rel}(\{x\} ∪ vars(t), sh) ∪ rel(vars(t) \ \{x\}, sh).

As a first correctness result, we have that the auxiliary operators correctly approximate the corresponding concrete properties. Theorem 26 Let d ∈ SFL, σ ∈ γ_{S}(d) and y ∈ VI . Let also s, t ∈ HTerms be two finite terms such that vars(s) ∪ vars(t) ⊆ VI . Then

ind_{d}(s, t) ⟹ vars(rt(s, σ)) ∩ vars(rt(t, σ)) = ∅;  (20)
ind_{d}(y, t) ⟺ y ∉ share with_{d}(t);  (21)
free_{d}(t) ⟹ rt(t, σ) ∈ Vars;  (22)
ground_{d}(t) ⟹ rt(t, σ) ∈ GTerms;  (23)
lin_{d}(t) ⟹ rt(t, σ) ∈ LTerms.  (24)

Example 27 Let VI = {v, w, x, y, z} and consider the abstract element d = ⟨sh, f, l⟩ ∈ SFL, where

sh = {v, wz, xz, z},  f = {v},  l = {v, x, y, z}.

Then, by applying Definition 25, we obtain the following.

• ground_{d}(x) does not hold whereas ground_{d}(h(y)) holds.

• free_{d}(v) holds but free_{d}(h(v)) does not hold.

• Both ind_{d}(w, x) and ind_{d}(f(w, y), f(x, y)) hold whereas ind_{d}(x, z) does not hold; note that, in the second case, the two arguments of the predicate do share y, but this does not affect the independence of the corresponding terms, because y is definitely ground in the abstract element d.

• Let t = f(w, x, x, y, y, z); then occ lin_{d}(w, t) does not hold because w ∉ l; occ lin_{d}(x, t) does not hold because x occurs more than once in t; occ lin_{d}(y, t) holds, even though y occurs twice in t, because y is definitely ground in d; occ lin_{d}(z, t) does not hold because both x and z occur in term t and, as observed in the point above, ind_{d}(x, z) does not hold.

• For the reasons given in the point above, lin_{d}(t) does not hold; in contrast, lin_{d}(f(y, y, z)) holds.

• share with_{d}(w) = {w, z} and share with_{d}(x) = {x, z}; thus, both w and x may share one or more variables with z; since we observed that w and x are definitely independent in d, this means that the set of variables that w shares with z is disjoint from the set of variables that x shares with z.

• Let t = f(w, z); then

cyclic_{z}^{t}(sh) = \overline{rel}(\{w, z\}, sh) ∪ rel(\{w\}, sh)
= {v} ∪ {wz}
= sh \ {xz, z}.

An intuitive explanation of the usefulness of this operator is deferred until after the introduction of the abstract mgu operator (see also Example 31).

We now introduce the abstract mgu operator, specifying how a single binding affects each component of the domain SFL in the context of a syntactic equality theory T.

Definition 28 (amgu_{S}.) The function amgu_{S}: SFL×Bind → SFL captures the effects of a binding on an element of SFL. Let d = ⟨sh, f, l⟩ ∈ SFL and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let also

sh′ =^{def} cyclic_{x}^{t}(sh_{−} ∪ sh′′),

where

sh_{x} =^{def} rel({x}, sh),  sh_{t} =^{def} rel(vars(t), sh),
sh_{xt} =^{def} sh_{x} ∩ sh_{t},  sh_{−} =^{def} \overline{rel}(\{x\} ∪ vars(t), sh),

sh′′ =^{def} \begin{cases}bin(sh_{x}, sh_{t}), & if free_{d}(x) ∨ free_{d}(t); \\ bin(sh_{x} ∪ bin(sh_{x}, sh_{xt}^{⋆}), \\ sh_{t} ∪ bin(sh_{t}, sh_{xt}^{⋆})), & if lin_{d}(x) ∧ lin_{d}(t); \\ bin(sh_{x}^{⋆}, sh_{t}), & if lin_{d}(x); \\ bin(sh_{x}, sh_{t}^{⋆}), & if lin_{d}(t); \\ bin(sh_{x}^{⋆}, sh_{t}^{⋆}), & otherwise. \end{cases}

Letting S_{x} =^{def} share with_{d}(x) and S_{t} =^{def} share with_{d}(t), we also define

f′ =^{def} \begin{cases}f, & if free_{d}(x) ∧ free_{d}(t); \\ f \ S_{x}, & if free_{d}(x); \\ f \ S_{t}, & if free_{d}(t); \\ f \ (S_{x} ∪ S_{t}), & otherwise; \end{cases}

l′ =^{def} (VI \ vars(sh′)) ∪ f′ ∪ l′′,

where

l′′ =^{def} \begin{cases}l \ (S_{x} ∩ S_{t}), & if lin_{d}(x) ∧ lin_{d}(t); \\ l \ S_{x}, & if lin_{d}(x); \\ l \ S_{t}, & if lin_{d}(t); \\ l \ (S_{x} ∪ S_{t}), & otherwise. \end{cases}

Then

amgu_{S}(d, x ↦ t) =^{def} \begin{cases}⊥_{S}, & if d = ⊥_{S} ∨ (T = FT ∧ x ∈ vars(t)); \\ ⟨sh′, f′, l′⟩ & otherwise. \end{cases}

The next result states that the abstract mgu operator is a correct approximation of the concrete one.

Theorem 29 Let d ∈ SFL and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Then, for all σ ∈ γ_{S}(d) and τ ∈ mgs(σ ∪ {x = t}) in the syntactic equality theory T, we have τ ∈ γ_{S}(amgu_{S}(d, x ↦ t)).

We now highlight the similarities and differences of the operator amgu_{S} with respect to the corresponding ones defined in the “classical” proposals for the integration of set-sharing with freeness and linearity, such as (Bruynooghe et al. 1994a; Bruynooghe et al. 1995; Hans and Winkler 1992; Langen 1990). Note that, when comparing our domain with the proposal in (Bruynooghe et al. 1994a), we deliberately ignore all those enhancements that depend on properties that cannot be represented in SFL (i.e., compoundness and explicit structural information).

• In the computation of the set-sharing component, the main difference can be observed in the second, third and fourth cases of the definition of sh′′: here we omit one of the star-unions even when the terms x and t possibly share. In contrast, in (Bruynooghe et al. 1994a; Hans and Winkler 1992; Langen 1990) the corresponding star-union is avoided only when ind_{d}(x, t) holds. Note that when ind_{d}(x, t) holds in the second case of sh′′, then we have sh_{xt} = ∅; thus, the whole computation for this case reduces to sh′′ = bin(sh_{x}, sh_{t}), as was the case in the previous proposals.

• Another improvement on the set-sharing component can be observed in the definition of sh′: the cyclic_{x}^{t} operator allows the set-sharing description to be further enhanced when dealing with explicitly cyclic bindings, i.e., when x ∈ vars(t). This is the rewording of a similar enhancement proposed in (Bagnara 1997) for the domain Pos in the context of groundness analysis. Its net effect is to recover some groundness and sharing dependencies that would have been unnecessarily lost when using the standard operators. When x ∉ vars(t), we have cyclic_{x}^{t}(sh_{−} ∪ sh′′) = sh_{−} ∪ sh′′.

• The computation of the freeness component f′ is the same as specified in (Bruynooghe et al. 1994a; Hans and Winkler 1992), and is more precise than the one defined in (Langen 1990).

• The computation of the linearity component l′ is the same as specified in (Bruynooghe et al. 1994a), and is more precise than those defined in (Hans and Winkler 1992; Langen 1990).

In the following examples we show that the improvements in the abstract computation of the sharing component allow, in particular cases, to derive better information than that obtainable by using the classical abstract unification operators.

Example 30 Let VI = {x, x_{1}, x_{2}, y, y_{1}, y_{2}, z} and σ ∈ RSubst such that

σ =^{def} {x ↦ f(x_{1}, x_{2}, z), y ↦ f(y_{1}, z, y_{2})}.

By Definition 23, we have d =^{def} α_{S}({σ}) = ⟨sh, f, l⟩, where

sh = {xx_{1}, xx_{2}, xyz, yy_{1}, yy_{2}},  f = VI \ {x, y},  l = VI .

Consider the binding (x ↦ y) ∈ Bind. In the concrete domain, we compute (a substitution equivalent to) τ ∈ mgs(σ ∪ {x = y}), where

τ = {x ↦ f(y_{1}, y_{2}, y_{2}), y ↦ f(y_{1}, y_{2}, y_{2}), x_{1} ↦ y_{1}, x_{2} ↦ y_{2}, z ↦ y_{2}}.

Note that α_{S}({τ}) = ⟨sh_{τ} , f_{τ} , l_{τ} ⟩, where sh_{τ} = {xx_{1}yy_{1}, xx_{2}yy_{2}z}, so that the pairs of variables P_{x} = {x_{1}, x_{2}} and P_{y} = {y_{1}, y_{2}} keep their independence.

When evaluating the sharing component of amgu_{S}(d, x ↦ y), using the notation of Definition 28, we have

sh_{x} = {xx_{1}, xx_{2}, xyz},  sh_{t} = {xyz, yy_{1}, yy_{2}},
sh_{xt} = {xyz},  sh_{−} = ∅.

Since both lin_{d}(x) and lin_{d}(y) hold, we apply the second case of the definition of sh′′ so that

sh_{x} ∪ bin(sh_{x}, sh_{xt}^{⋆}) = {xx_{1}, xx_{1}yz, xx_{2}, xx_{2}yz, xyz},

sh_{t} ∪ bin(sh_{t}, sh_{xt}^{⋆}) = {xyy_{1}z, xyy_{2}z, xyz, yy_{1}, yy_{2}},
sh′′ = bin(sh_{x} ∪ bin(sh_{x}, sh_{xt}^{⋆}), sh_{t} ∪ bin(sh_{t}, sh_{xt}^{⋆}))
= {xx_{1}yy_{1}, xx_{1}yy_{1}z, xx_{1}yy_{2}, xx_{1}yy_{2}z, xx_{1}yz,
xx_{2}yy_{1}, xx_{2}yy_{1}z, xx_{2}yy_{2}, xx_{2}yy_{2}z, xx_{2}yz,
xyy_{1}z, xyy_{2}z, xyz}.

Finally, as the binding is not cyclic, we obtain sh′ = sh′′. Thus amgu_{S} captures the fact that pairs P_{x} and P_{y} keep their independence.

In contrast, since ind_{d}(x, y) does not hold, all of the classical definitions of abstract unification would have required the star-closure of both sh_{x} and sh_{t}, resulting in an abstract element including, among the others, the sharing group S = {x, x_{1}, x_{2}, y, y_{1}, y_{2}}. Since P_{x} ∪ P_{y} ⊂ S, this independence information would have been unnecessarily lost.

Similar examples can be devised for the third and fourth cases of the definition of sh′′, where only one side of the binding is known to be linear. The next example shows the precision improvements arising from the use of the cyclic_{x}^{t} operator.

Example 31 Let VI = {x, x_{1}, x_{2}, y} and σ =^{def} {x ↦ f(x_{1}, x_{2})}. By Definition 23, we have

d =^{def} α_{S}({σ}) = ⟨sh, f, l⟩, where

sh = {xx_{1}, xx_{2}, y},  f = VI \ {x},  l = VI .

Let t = f(x, y) and consider the cyclic binding (x ↦ t) ∈ Bind. In the concrete domain, we compute (a substitution equivalent to) τ ∈ mgs(σ ∪ {x = t}), where

τ = {x ↦ f(x_{1}, x_{2}), x_{1} ↦ f(x_{1}, x_{2}), y ↦ x_{2}, }.

Note that if we further instantiate τ by grounding y, then variables x, x_{1} and x_{2} would become ground too. Formally we have α_{S}({τ}) = ⟨sh_{τ} , f_{τ} , l_{τ} ⟩, where sh_{τ} = {xx_{1}x_{2}y}. Thus, as observed above, y covers x, x_{1} and x_{2}. When abstractly evaluating the binding, we compute

sh_{x} = {xx_{1}, xx_{2}},  sh_{t} = {xx_{1}, xx_{2}, y},
sh_{xt} = sh_{x},  sh_{−} = ∅.

Since both lin_{d}(x) and lin_{d}(t) hold, we apply the second case of the definition of sh′′, so that

sh_{x} ∪ bin(sh_{x}, sh_{xt}^{⋆}) = sh_{x}^{⋆} = {xx_{1}, xx_{1}x_{2}, xx_{2}},
sh_{t} ∪ bin(sh_{t}, sh_{xt}^{⋆}) = {xx_{1}, xx_{1}x_{2}, xx_{1}x_{2}y, xx_{1}y, xx_{2}, xx_{2}y, y},
sh′′ = bin(sh_{x} ∪ bin(sh_{x}, sh_{xt}^{⋆}), sh_{t} ∪ bin(sh_{t}, sh_{xt}^{⋆}))
= {xx_{1}, xx_{1}x_{2}, xx_{1}x_{2}y, xx_{1}y, xx_{2}, xx_{2}y}.

Thus, as x ∈ vars(t), we obtain

sh′ = cyclic_{x}^{t}(sh_{−} ∪ sh′′)
= \overline{rel}(\{x\} ∪ vars(t), sh′′) ∪ rel(vars(t) \ \{x\}, sh′′)

= ∅ ∪ rel({y}, sh′′)
= {xx_{1}x_{2}y, xx_{1}y, xx_{2}y}.

Note that, in the element sh_{−} ∪ sh′′ = sh′′ (which is the abstract element that would have been computed when not exploiting the cyclic_{x}^{t} operator) variable y covers none of variables x, x_{1} and x_{2}. Thus, by applying the cyclic_{x}^{t} operator, this covering information is restored.

The full abstract unification operator aunify_{S}, capturing the effect of a sequence of bindings on an abstract element, can now be specified by a straightforward inductive definition using the operator amgu_{S}.

Definition 32 (aunify_{S}.) The operator aunify_{S}: SFL × Bind^{∗} → SFL is defined, for each d ∈ SFL and each sequence of bindings bs ∈ Bind^{∗}, by

aunify_{S}(d, bs) =^{def} \begin{cases}d, & if bs = ϵ; \\ aunify_{S}(amgu_{S}(d, x ↦ t), bs′), & if bs = (x ↦ t) . bs′. \end{cases}

Note that the second argument of aunify_{S} is a sequence of bindings (i.e., it is not a substitution, which is a set of bindings), because amgu_{S} is neither commutative nor idempotent, so that the multiplicity and the actual order of application of the bindings can influence the overall result of the abstract computation. The correctness of the aunify_{S} operator is simply inherited from the correctness of the underlying amgu_{S} operator. In particular, any reordering of the bindings in the sequence bs still results in a correct implementation of aunify_{S}.

The ‘merge-over-all-path’ operator on the domain SFL is provided by alub_{S} and is correct by definition. Finally, we define the abstract existential quantification operator for the domain SFL, whose correctness does not pose any problem.

Definition 33 (aexists_{S}.) The function aexists_{S}: SFL × ℘_{f}(VI ) → SFL provides the abstract existential quantification of an element with respect to a subset of the variables of interest. For each d =^{def} ⟨sh, f, l⟩ ∈ SFL and V ⊆ VI ,

aexists_{S}(⟨sh, f, l⟩, V ) =^{def} ⟨aexists(sh, V), f ∪ V, l ∪ V ⟩.

The intuition behind the definition of the abstract operator aexists_{S} is the following. As explained in Section 2, any substitution σ ∈ RSubst can be interpreted, under the given equality theory T, as a first-order logical formula; thus, for each set of variables V, it is possible to consider the (concrete) existential quantification ∃V . σ. The goal of the abstract operator aexists_{S} is to provide a correct approximation of such a quantification starting from any correct approximation for σ.

Example 34 Let VI = {x, y, z} and σ = {x ↦ f(v_{1}, v_{2}), y ↦ g(v_{2}, v_{3}), z ↦ f(v_{1}, v_{1})}, so that, by Definition 23,

d = α_{S}({σ}) = ⟨{xy, xz, y}, ∅, {x, y}⟩.

Let V = {y, z} and consider the concrete element corresponding to the logical formula ∃V . σ. Note that T ⊢ ∀(τ ↔ ∃V . σ), where τ = {x ↦ f(v_{1}, v_{2})}. By applying Definition 33, we obtain

aexists_{S}(d, V) = ⟨{x, y, z}, {y, z}, {x, y, z}⟩ = α_{S}({τ}).

It is worth stressing that such an operator does not affect the set VI of the variables of interest. In particular, the abstract element aexists_{S}(d, V) still has to provide correct information about variables y and z. Intuitively, since all the occurrences of y and z in ∃V . σ are bound by the existential quantifier, the two variables of interest are un-aliased, free and linear.

Note that an abstract projection operator, i.e., an operator that actually modifies the set of variables of interest, is easily specified by composing the operator aexists_{S} with an operator that simply removes, from all the components of SFL and from the set of variables of interest VI , those variables that have to be projected out.

4 A Formal Comparison Between SFL and ASub

As we have already observed, Example 30 shows that the abstract domain SFL, when equipped with the abstract mgu operator introduced in Section 3.2, can yield results that are strictly more precise than all the classical combinations of setsharing with freeness and linearity information. In this section we show that the same example has another interesting, unexpected consequence, since it can be used to formally prove that all the classical combinations of set-sharing with freeness and linearity, including those presented in (Bagnara et al. 2000; Bruynooghe et al. 1994a; Hans and Winkler 1992; Langen 1990), are not uniformly more precise than the abstract domain ASub (Søndergaard 1986), which is based on pair-sharing.

To formalize the above observation, we now introduce the ASub domain and the corresponding abstract semantics operators as specified in (Codish et al. 1991). The elements of the abstract domain ASub have two components: the first one is a set of variables that are known to be definitely ground; the second one encodes both possible pair-sharing and possible non-linearity into a single relation defined on the set of variables. Intuitively, when x ≠ y and (x, y) ∈ VI^{2} occurs in the second component, then x and y may share a variable; when (x, x) ∈ VI^{2} occurs in the second component, then x may be non-linear. The second component always encodes a symmetric relation; thus, for notational convenience and without any loss of generality (King 2000), we will represent each pair (x, y) in such a relation as the sharing group S = {x, y}, which will have cardinality 1 or 2 depending on whether x = y or not, respectively.

Definition 35 (The domain ASub_{⊥}.) The abstract domain ASub_{⊥} is defined as ASub_{⊥} =^{def} {⊥_{ASub}} ∪ ASub, where

ASub =^{def} \{ ⟨G, R⟩ ∈ ℘(VI ) × SH | \begin{matrix}G ∩ vars(R) = ∅, \\ ∀S ∈ R : 1 ≤ #S ≤ 2 \end{matrix} \}.

For i ∈ {1, 2}, let κ_{i} = ⟨G_{i}, R_{i}⟩ ∈ ASub. Then

κ_{1} ⪯_{ASub} κ_{2} ⟺^{def} G_{1} ⊇ G_{2} ∧ R_{1} ⊆ R_{2}.

The partial order ⪯_{ASub} is extended on ASub_{⊥} by letting ⊥_{ASub} be the bottom element.

Let u, v ∈ VI and κ = ⟨G, R⟩ ∈ ASub. Then u ⟷^{κ} v is a shorthand for the condition {u, v} ∈ R, whereas u ⟺^{κ} v is a shorthand for u = v ∨ {u, v} ∈ R.

It is well-known that the domain ASub_{⊥} can be obtained by a further abstraction of any domain such as SFL that is based on set-sharing and enhanced with linearity information. The following definition formalizes this abstraction.

Definition 36 (α_{ASub} : SFL → ASub_{⊥}.) Let d = ⟨sh, f, l⟩ ∈ SFL. Then

α_{ASub}(d) =^{def} \begin{cases}⊥_{ASub}, & if d = ⊥_{S}; \\ ⟨G, R⟩, & otherwise; \end{cases}

where

G =^{def} { x ∈ VI | x ∉ vars(sh) },
R =^{def} { {x} ⊆ VI | x ∈ vars(sh) ∧ x ∉ l }
∪ { {x, y} ⊆ VI | x ≠ y ∧ ∃S ∈ sh . {x, y} ⊆ S }.

The definition of abstract unification in (Codish et al. 1991) is based on a few auxiliary operators. The first of these introduces the concept of abstract multiplicity for a term under a given abstract substitution, therefore modeling the notion of definite groundness and definite linearity.

Definition 37 (Abstract multiplicity.) Let κ = ⟨G, R⟩ ∈ ASub and let t ∈ HTerms be a term such that vars(t) ⊆ VI . We say that y ∈ vars(t) occurs linearly (in t) in κ if and only if occ lin_{κ}: VI × HTerms → Bool holds for (y, t), where

occ lin_{κ}(y, t) =^{def} y ∈ G ∨ (occ lin(y, t) ∧ ∀z ∈ vars(t) : {y, z} ∉ R).

We say that t has abstract multiplicity m in κ if and only if χ_{κ}(t) = m, where χ_{κ}: HTerms → {0, 1, 2} is defined as follows

χ_{κ}(t) =^{def} \begin{cases}0, & if vars(t) ⊆ G; \\ 1, & if ∀y ∈ vars(t) : occ lin_{κ}(y, t); \\ 2, & otherwise. \end{cases}

For any binding x ↦ t, the function χ_{κ}: Bind → {0} ∪ {1, 2}^{2} is defined as follows

χ_{κ}(x ↦ t) =^{def} \begin{cases}0, & if χ_{κ}(x) = 0 or χ_{κ}(t) = 0; \\ (χ_{κ}(x), χ_{κ}(t)), & otherwise; \end{cases}

It is worth noting that, modulo a few insignificant differences in notation, the multiplicity operator χ_{κ} defined above corresponds to the abstract multiplicity operator χ^{A}, which was introduced in (Codish et al. 1991, Definition 3.4) and provided with an executable specification in (King 2000, Definition 4.3). Similarly, the next definition corresponds to (Codish et al. 1991, Definition 4.3).

Definition 38 (Sharing caused by an abstract equation.) For each κ ∈ ASub and (x ↦ t) ∈ Bind, where V_{x} = {x} and V_{t} = vars(t) are such that V_{x} ∪ V_{t} ⊆ VI , the function soln: ASub × Bind → ASub is defined as follows

soln(κ, x ↦ t) =^{def} \begin{cases}⟨V_{x} ∪ V_{t}, ∅⟩, & if χ_{κ}(x ↦ t) = 0; \\ ⟨∅, bin(V_{x}, V_{t})⟩, & if χ_{κ}(x ↦ t) = (1, 1); \\ ⟨∅, bin(V_{x}, V_{x} ∪ V_{t})⟩, & if χ_{κ}(x ↦ t) = (1, 2); \\ ⟨∅, bin(V_{x} ∪ V_{t}, V_{t})⟩, & if χ_{κ}(x ↦ t) = (2, 1); \\ ⟨∅, bin(V_{x} ∪ V_{t}, V_{x} ∪ V_{t})⟩, & if χ_{κ}(x ↦ t) = (2, 2); \end{cases}

where the function bin: ℘(VI )^{2} → SH , for each V, W ⊆ VI , is defined as follows

bin(V, W) =^{def} { {v, w} ⊆ VI | v ∈ V, w ∈ W }.

The next definition corresponds to (Codish et al. 1991, Definition 4.5).

Definition 39 (Abstract composition.) Let κ, κ′ ∈ ASub, where κ = ⟨G, R⟩ and κ′ = ⟨G′, R′⟩.

Then κ ∘ κ′ =^{def} ⟨G′′, R′′⟩, where

G′′ =^{def} G ∪ G′,
R′′ =^{def} \{ \{u, v\} ∈ SH | \begin{matrix}\{u, v\} ∩ G′′ = ∅, \\ (u ⟷^{κ} v) ∨ (∃x, y . u ⟺^{κ} x ⟷^{κ′} y ⟺^{κ} v) \end{matrix} \}.

We are now ready to define the abstract mgu operator for the domain ASub_{⊥}. This operator can be viewed as a specialization of (Codish et al. 1991, Definition 4.6) for the case when we have to abstract a single binding.

Definition 40 (Abstract mgu for ASub_{⊥}.) Let κ ∈ ASub_{⊥} and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Then

amgu_{ASub}(κ, x ↦ t) =^{def} \begin{cases}⊥_{ASub}, & if κ = ⊥_{ASub}; \\ κ ∘ soln(κ, x ↦ t), & otherwise; \end{cases}

By repeating the abstract computation of Example 30 on the domain ASub, we provide a formal proof that all the classical approaches based on set-sharing are not uniformly more precise than the pair-sharing domain ASub.

Example 41 Consider the substitutions σ, τ ∈ RSubst and the abstract element d ∈ SFL as introduced in Example 30.

By Definition 36, we obtain κ = α_{ASub}(d) = ⟨∅, R⟩, where

R = {xx_{1}, xx_{2}, xy, xz, yy_{1}, yy_{2}, yz},

When abstractly evaluating the binding x ↦ y according to Definition 40, we compute the following:

χ_{κ}(x ↦ y) = (1, 1),
soln(κ, x ↦ y) = ⟨∅, {xy}⟩,
amgu_{ASub}(κ, x ↦ y) = κ ∘ soln(κ, x ↦ y) = ⟨∅, R′′⟩,

where

R′′ = R ∪ {x, xy_{1}, xy_{2}, x_{1}y, x_{1}y_{1}, x_{1}y_{2}, x_{1}z, x_{2}y, x_{2}y_{1}, x_{2}y_{2}, x_{2}z, y, y_{1}z, y_{2}z, z}.

Note that {x_{1}, x_{2}} ∉ R′′ and {y_{1}, y_{2}} ∉ R′′, so that these pairs of variables keep their independence. In contrast, as observed in Example 30, the operators in (Bagnara et al. 2000; Bruynooghe et al. 1994a; Hans and Winkler 1992; Langen 1990) will fail to preserve the independence of these pairs.

We now show that the abstract domain SFL, when equipped with the operators introduced in Section 3.2, is uniformly more precise than the domain ASub. In particular, the following theorem states that the abstract operator amgu_{S} of Definition 28 is uniformly more precise than the abstract operator amgu_{ASub}.

Theorem 42 Let d ∈ SFL and κ ∈ ASub_{⊥} be such that α_{ASub}(d) ⪯_{ASub} κ. Let also (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Then

α_{ASub}(amgu_{S}(d, x ↦ t)) ⪯_{ASub} amgu_{ASub}(κ, x ↦ t).

Similar results can be stated for the other abstract operators, such as the abstract existential quantification aexists_{S} and the merge-over-all-path operator alub_{S}. It is worth stressing that, when sequences of bindings come into play, the specification provided in (Codish et al. 1991, Definition 4.7) requires that the grounding bindings (i.e., those bindings such that χ_{κ}(x ↦ t) = 0) are evaluated before the non-grounding ones. Clearly, if we want to lift the result of Theorem 42 so that it also applies to the operator aunify_{S}, the same evaluation strategy has to be adopted when computing on the domain SFL; this improvement is well-known (Langen 1990, pp. 66-67) and already exploited in most implementations of sharing analysis (Bagnara et al. 2000).

5 SFL_{2}: Eliminating Redundancies

As done in (Bagnara et al. 2002; Zaffanella et al. 2002) for the plain set-sharing domain SH , even when considering the richer domain SFL it is natural to question whether it contains redundancies with respect to the computation of the observable properties.

It is worth stressing that the results presented in (Bagnara et al. 2002) and (Zaffanella et al. 2002) cannot be simply inherited by the new domain. The concept of “redundancy” depends on both the starting domain and the given observables: in the SFL domain both of these have changed. First of all, as can be seen by looking at the definition of amgu_{S}, freeness and linearity positively interact in the computation of sharing information: a priori it is an open issue whether or not the “redundant” sharing groups can play a role in such an interaction. Secondly, since freeness and linearity information can be themselves usefully exploited in a number of applications of static analysis (e.g., in the optimized implementation of concrete unification or in occurs-check reduction), these properties have to be included in the observables.

We will now show that the domain SFL can be simplified by applying the same notion of redundancy as identified in (Bagnara et al. 2002). Namely, in the definition of SFL it is possible to replace the set-sharing component SH by PSD without affecting the precision on groundness, independence, freeness and linearity. In order to prove such a claim, we now formalize the new observable properties.

Definition 43 (The observables of SFL.) The (overloaded) groundness and independence observables ρ_{Con}, ρ_{PS} ∈ uco(SFL) are defined, for each ⟨sh, f, l⟩ ∈ SFL, by

ρ_{Con}(⟨sh, f, l⟩) =^{def} ⟨ρ_{Con}(sh), ∅, ∅⟩,
ρ_{PS}(⟨sh, f, l⟩) =^{def} ⟨ρ_{PS}(sh), ∅, ∅⟩;

the freeness and linearity observables ρ_{F} , ρ_{L} ∈ uco(SFL) are defined, for each ⟨sh, f, l⟩ ∈ SFL, by

ρ_{F} (⟨sh, f, l⟩) =^{def} ⟨SG, f, ∅⟩,
ρ_{L}(⟨sh, f, l⟩) =^{def} ⟨SG, ∅, l⟩.

The overloading of ρ_{PSD} working on the domain SFL is the straightforward extension of the corresponding operator on SH : in particular, the freeness and linearity components are left untouched.

Definition 44 (Non-redundant SFL.) For each ⟨sh, f, l⟩ ∈ SFL, the operator ρ_{PSD} ∈ uco(SFL) is defined by

ρ_{PSD}(⟨sh, f, l⟩) =^{def} ⟨ρ_{PSD}(sh), f, l⟩.

This operator induces the lattice SFL_{2} =^{def} ρ_{PSD}(SFL).

As proved in (Zaffanella et al. 2002), we have that ρ_{PSD} ⊑ (ρ_{Con} ⊓ ρ_{PS}); by the above definitions, it is also clear that ρ_{PSD} ⊑ (ρ_{F} ⊓ ρ_{L}); thus, ρ_{PSD} is more precise than the reduced product (ρ_{Con} ⊓ ρ_{PS} ⊓ ρ_{F} ⊓ ρ_{L}). Informally, this means that the domain SFL_{2} is able to represent all of our observable properties without precision losses.

The next theorem shows that ρ_{PSD} is a congruence with respect to the aunify_{S}, alub_{S} and aexists_{S} operators. This means that the domain SFL_{2} is able to propagate the information on the observables as precisely as SFL, therefore providing a completeness result.

Theorem 45 Let d_{1}, d_{2} ∈ SFL be such that ρ_{PSD}(d_{1}) = ρ_{PSD}(d_{2}). Then, for each sequence of bindings bs ∈ Bind^{∗}, for each d′ ∈ SFL and V ∈ ℘(VI ),

ρ_{PSD}(aunify_{S}(d_{1}, bs)) = ρ_{PSD}(aunify_{S}(d_{2}, bs)),
ρ_{PSD}(alub_{S}(d_{1}, d′)) = ρ_{PSD}(alub_{S}(d_{2}, d′)),
ρ_{PSD}(aexists_{S}(d_{1}, V)) = ρ_{PSD}(aexists_{S}(d_{2}, V)).

Finally, by providing the minimality result, we show that the domain SFL_{2} is indeed the generalized quotient (Cortesi et al. 1998; Giacobazzi et al. 1998) of SFL with respect to the reduced product (ρ_{Con} ⊓ ρ_{PS} ⊓ ρ_{F} ⊓ ρ_{L}).

Theorem 46 For each i ∈ {1, 2}, let d_{i} = ⟨sh_{i}, f_{i}, l_{i}⟩ ∈ SFL be such that ρ_{PSD}(d_{1}) ≠ ρ_{PSD}(d_{2}). Then there exist a sequence of bindings bs ∈ Bind^{∗} and an observable property ρ ∈ {ρ_{Con}, ρ_{PS}, ρ_{F} , ρ_{L}} such that

ρ(aunify_{S}(d_{1}, bs)) ≠ ρ(aunify_{S}(d_{2}, bs)).

As far as the implementation is concerned, the results proved in (Bagnara et al. 2002) for the domain PSD can also be applied to SFL_{2}. In particular, in the definition of amgu_{S} every occurrence of the star-union operator can be safely replaced by the self-bin-union operator. As a consequence, it is possible to provide an implementation where the time complexity of the amgu_{S} operator is bounded by a polynomial in the number of sharing groups of the set-sharing component.

The following result provides another optimization that can be applied when both terms x and t are definitely linear, but none of them is definitely free (i.e., when we compute sh′′ by the second case stated in Definition 28).

Theorem 47 Let sh ∈ SH and (x ↦ t) ∈ Bind, where \{x\} ∪ vars(t) ⊆ VI . Let sh_{−} =^{def} \overline{rel}(\{x\} ∪ vars(t), sh), sh_{x} =^{def} rel({x}, sh), sh_{t} =^{def} rel(vars(t), sh), sh_{xt} =^{def} sh_{x} ∩ sh_{t}, sh_{W} =^{def} rel(W, sh), where W = vars(t) \ {x}, and

sh^{⋄} =^{def} bin(sh_{x} ∪ bin(sh_{x}, sh_{xt}^{⋆}), sh_{t} ∪ bin(sh_{t}, sh_{xt}^{⋆})).

Then it holds

ρ_{PSD}(cyclic_{x}^{t}(sh_{−} ∪ sh^{⋄})) = \begin{cases}ρ_{PSD}(sh_{−} ∪ bin(sh_{x}, sh_{t})), & if x ∉ vars(t); \\ ρ_{PSD}(sh_{−} ∪ bin(sh_{x}^{2}, sh_{W})), & otherwise. \end{cases}

Therefore, even when terms x and t possibly share (i.e., when sh_{xt} ≠ ∅), by using SFL_{2} we can avoid the expensive computation of at least one of the two inner binary unions in the expression for sh^{⋄}.

6 Experimental Evaluation

Example 30 shows that an analysis based on the new abstract unification operator can be strictly more precise than one based on the classical proposal. However, that example is artificial and leaves open the question as to whether or not such a phenomenon actually happens during the analysis of real programs and, if so, how often. This was the motivation for the experimental evaluation we describe in this section. We consider the abstract domain Pos × SFL_{2} (Bagnara et al. 2001), where the non-redundant version SFL_{2} of the domain SFL is further combined, as described in (Bagnara et al. 2001, Section 4), with the definite groundness information computed by Pos and compare the results using the (classical) abstract unification operator of (Bagnara et al. 2001, Definition 4) with the (new) operator amgu_{S} given in Definition 28. Taking this as a starting point, we experimentally evaluate eight variants of the analysis arising from all possible combinations of the following options:

1. the analysis can be goal independent or goal dependent;

2. the set-sharing component may or may not have widening enabled (Zaffanella et al. 1999);

3. the abstract domain may or may not be upgraded with structural information using the Pattern(·) operator (see (Bagnara et al. 2000) and (Bagnara et al. 2001, Section 5)).

The experiments have been conducted using the China analyzer (Bagnara 1997) on a GNU/Linux PC system. China is a data-flow analyzer for (constraint) logic programs performing bottom-up analysis and deriving information on both callpatterns and success-patterns by means of program transformations and optimized fixpoint computation techniques. An abstract description is computed for the calland success-patterns for each predicate defined in the program. The benchmark suite, which is composed of 372 logic programs of various sizes and complexity, can be considered representative.

The precision results for the goal independent comparisons are summarized in Table 1. For each benchmark, precision is measured by counting the number of independent pairs as well as the numbers of definitely ground, free and linear variables detected. For each variant of the analysis, these numbers are then compared by computing the relative precision improvements and expressing them using percentages. The benchmark suite is then partitioned into several precision equivalence classes and the cardinalities of these classes are shown in Table 1. For example, when considering a goal independent analysis without structural information and without widenings, the value 5 found at the intersection of the row labeled ‘0 < p ≤ 2’ with the column labeled ‘I’ should be read: “for five benchmarks there has been a (positive) increase in the number of independent pairs of variables which is less than or equal to two percent.” Note that we only report on independence and linearity (in the columns labeled ‘I’ and ‘L’, respectively), because no differences have been observed for groundness and freeness. The precision class labeled ‘unknown’ identifies those benchmarks for which the analyses timed-out (the time-out threshold was

Goal  Without Widening With Widening
Independent  w/o SI with SI w/o SI with SI
Prec. class  I L I L I L I L
5 < p ≤ 10  — 2 — 2 — 2 — 2
2 < p ≤ 5  — — — — — — — 1
0 < p ≤ 2  5 5 9 6 6 6 12 8
same precision 357 355 337 338 366 364 360 361
unknown  10 10 26 26 — — — —

Table 1. Classical Pos × SFL_{2} versus enhanced one: precision.

fixed at 600 seconds). Hence, for goal independent analyses, a precision improvement affects from 1.6% to 3% of the benchmarks, depending on the considered variant.

When considering the goal dependent analyses, we obtain a single, small improvement, so that no comparison tables are included here: the improvement, affecting linearity information, can be observed when the abstract domain includes structural information.

With respect to differences in the efficiency, the introduction of the new abstract unification operator has no significant effect on the computation time: small differences (usually improvements) are observed on as many as 6% of the benchmarks for the goal independent analysis without structural information and without widenings; other combinations register even less differences.

We note that it is not surprising that the precision and efficiency improvements occur very rarely since the abstract unification operators behave the same except under very specific conditions: the two terms being unified must not only be definitely linear, but also possibly non-free and share a variable.

7 Related Work

Sharing information has been shown to be important for finite-tree analysis (Bagnara et al. 2001; Bagnara et al. 2001). This aims at identifying those program variables that, at a particular program point, cannot be bound to an infinite rational tree (in other words, they are necessarily bound to acyclic terms). This novel analysis is irrelevant for those logic languages computing over a domain of finite trees, while having several applications for those (constraint) logic languages that are explicitly designed to compute over a domain including rational trees, such as Prolog II and its successors (Colmerauer 1982; Colmerauer 1990), SICStus Prolog (Swedish Institute of Computer Science, Programming Systems Group 1995), and Oz (Smolka and Treinen 1994). The analysis specified in (Bagnara et al. 2001) is based on a parametric abstract domain H × P, where the H component (the Herbrand component) is a set of variables that are known to be bound to finite terms, while the parametric component P can be any domain capturing aliasing, groundness, freeness and linearity information that is useful to compute finite-tree information. An obvious choice for such a parameter is the domain combination SFL. It is worth noting that, in (Bagnara et al. 2001), the correctness of the finitetree analysis is proved by assuming the correctness of the underlying analysis on the parameter P. Thus, thanks to the results shown in this paper, the proof for the domain H × SFL can now be considered complete.

Codish et al. (Codish et al. 2000) describe an algebraic approach to the sharing analysis of logic programs that is based on set logic programs. A set logic program is a logic program in which the terms are sets of variables and standard unification is replaced by a suitable unification for sets, called ACI1-unification (unification in the presence of an associative, commutative, and idempotent equality theory with a unit element). The authors show that the domain of set-substitutions, with a few modifications, can be used as an abstract domain for sharing analysis. They also provide an isomorphism between this domain and the set-sharing domain SH of Jacobs and Langen. The approach using set logic programs is also generalized to include linearity information, by suitably annotating the set-substitutions, and the authors formally state the optimality of the corresponding abstract unification operator lin-mgu_{ACI1} (Lemma A.10 in the Appendix of (Codish et al. 2000)). However, this operator is very similar to the classical combinations of set-sharing with linearity (Bruynooghe et al. 1994a; Hans and Winkler 1992; Langen 1990): in particular, the precision improvements arising from this enhancement are only exploited when the two terms being unified are definitely independent. As we have seen in this paper, such a choice results in a sub-optimal abstract unification operator, so that the optimality result cannot hold. By looking at the proof of Lemma A.10 in (Codish et al. 2000), it can be seen that the case when the two terms possibly share a variable is dealt with by referring to an example:^{5} this one is supposed to show that all the possible sharing groups can be generated. However, even our improved operator correctly characterizes the given example, so that the proof is wrong. It should be stressed that the amgu_{S} operator presented in this paper, though remarkably precise, is not meant to subsume all of the proposals for an improved sharing analysis that appeared in the recent literature (for a thorough experimental evaluation of many of these proposals, the reader is referred to (Bagnara et al. 2000; Zaffanella 2001)). In particular, it is not difficult to show that our operator is not the optimal approximation of concrete unification.

In a very recent paper (Howe and King 2003), J. Howe and A. King consider the domain SFL and propose three optimizations to improve both the precision and the efficiency of the (classical) abstract unification operator. The first optimization is based on the same observation we have made in this paper, namely that the independence check between the two terms being unified is not necessary for ensuring the correctness of the analysis. However, the proposed enhancement does not fully exploit this observation, so that the resulting operator is strictly less precise than our amgu_{S} operator (even when the operator cyclic_{x}^{t} does not come into play). In fact, the first optimization of (Howe and King 2003) is not uniformly more precise than the classical proposals. The following example illustrates this point.

5 The proof refers to Example 8, which however has nothing to do with the possibility that the two terms share; we believe that Example 2 was intended.

Example 48

Let VI = {x, y, z_{1}, z_{2}, z_{3}}, (x ↦ y) ∈ Bind and d =^{def} ⟨sh, ∅, VI ⟩, where sh = {xz_{1}, xz_{2}, xz_{3}, yz_{1}, yz_{2}, yz_{3}}.

Since x and y are linear and independent, amgu_{S} as well as all the classical abstract unification operators will compute d_{1} = ⟨sh_{1}, ∅, {x, y}⟩, where

sh_{1} =^{def} bin(sh_{x}, sh_{y}) = {xyz_{1}, xyz_{1}z_{2}, xyz_{1}z_{3}, xyz_{2}, xyz_{2}z_{3}, xyz_{3}}.

In contrast, a computation based on (Howe and King 2003, Definition 3.2), results in the less precise abstract element d_{2} = ⟨sh_{2}, ∅, {x, y}⟩, where

sh_{2} =^{def} bin(sh_{x}^{⋆}, sh_{y}) ∩ bin(sh_{x}, sh_{y}^{⋆}) = sh_{1} ∪ {xyz_{1}z_{2}z_{3}}.

The second optimization shown in (Howe and King 2003) is based on the enhanced combination of set-sharing and freeness information, which was originally proposed in (Filé 1994). In particular, the authors propose a slightly different precision enhancement, less powerful as far as precision is concerned, which however seems to be amenable for an efficient implementation. The third optimization in (Howe and King 2003) exploits the combination of the domain SFL with the groundness domain Pos.

8 Conclusion

In this paper we have introduced the abstract domain SFL, combining the setsharing domain SH with freeness and linearity information. While the carrier of SFL can be considered standard, we have provided the specification of a new abstract unification operator, showing examples where this operator achieves more precision than the classical proposals. The main contributions of this paper are the following:

• we have defined a precise abstraction function, mapping arbitrary substitutions in rational solved form into their most precise approximation on SFL;

• using this abstraction function, we have provided the mandatory proof of correctness for the new abstract unification operator, for both finite-tree and rational-tree languages;

• we have formally shown that the domain SFL is uniformly more precise than the domain ASub; we have also provided an example showing that all the classical approaches to the combinations of set-sharing with freeness and linearity fail to satisfy this property;

• we have shown that, in the definition of SFL, we can replace the set-sharing domain SH by its non-redundant version PSD. As a consequence, it is possible to implement an algorithm for abstract unification running in polynomial time and still obtain the same precision on all the considered observables, that is groundness, independence, freeness and linearity.

32 P. M. Hill, E. Zaffanella, and R. Bagnara

Acknowledgment

We recognize the hard work required to review technical papers such as this one and would like to express our real gratitude to the Journal referees for their critical reading and constructive suggestions for preparing this improved version.

References

Bagnara, R. 1997. Data-flow analysis for constraint logic-based languages. Ph.D. thesis,

Dipartimento di Informatica, Università di Pisa, Pisa, Italy. Printed as Report TD-1/97. Bagnara, R., Gori, R., Hill, P. M., and Zaffanella, E. 2001. Finite-tree analysis for

constraint logic-based languages. In Static Analysis: 8th International Symposium, SAS 2001, P. Cousot, Ed. Lecture Notes in Computer Science, vol. 2126. Springer-Verlag, Berlin, Paris, France, 165–184.

Bagnara, R., Hill, P. M., and Zaffanella, E. 1997. Set-sharing is redundant for pair-sharing. In Static Analysis: Proceedings of the 4th International Symposium, P. Van Hentenryck, Ed. Lecture Notes in Computer Science, vol. 1302. Springer-Verlag, Berlin, Paris, France, 53–67.

Bagnara, R., Hill, P. M., and Zaffanella, E. 2000. Efficient structural information analysis for real CLP languages. In Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning (LPAR 2000), M. Parigot and A. Voronkov, Eds. Lecture Notes in Artificial Intelligence, vol. 1955. Springer-Verlag, Berlin, Réunion Island, France, 189–206.

Bagnara, R., Hill, P. M., and Zaffanella, E. 2002. Set-sharing is redundant for

pair-sharing. Theoretical Computer Science 277, 1-2, 3–46. Bagnara, R., Zaffanella, E., Gori, R., and Hill, P. M. 2001. Boolean functions for

finite-tree dependencies. In Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2001), R. Nieuwenhuis and A. Voronkov, Eds. Lecture Notes in Artificial Intelligence, vol. 2250. Springer-Verlag, Berlin, Havana, Cuba, 579–594.

Bagnara, R., Zaffanella, E., and Hill, P. M. 2000. Enhanced sharing analysis techniques: A comprehensive evaluation. In Proceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, M. Gabbrielli and F. Pfenning, Eds. Association for Computing Machinery, Montreal, Canada, 103–114.

Bagnara, R., Zaffanella, E., and Hill, P. M. 2001. Enhanced sharing analysis techniques: A comprehensive evaluation. Submitted for publication. Available at http:

//www.cs.unipr.it/~bagnara/.

Bruynooghe, M. and Codish, M. 1993. Freeness, sharing, linearity and correctness — All at once. In Static Analysis, Proceedings of the Third International Workshop, P. Cousot, M. Falaschi, G. Filé, and A. Rauzy, Eds. Lecture Notes in Computer Science, vol. 724. Springer-Verlag, Berlin, Padova, Italy, 153–164. An extended version is available as Technical Report CW 179, Department of Computer Science, K.U. Leuven, September 1993.

Bruynooghe, M., Codish, M., and Mulkers, A. 1994a. Abstract unification for a composite domain deriving sharing and freeness properties of program variables. In Verification and Analysis of Logic Languages, Proceedings of the W2 Post-Conference Workshop, International Conference on Logic Programming, F. S. de Boer and M. Gabbrielli, Eds. Santa Margherita Ligure, Italy, 213–230.

Bruynooghe, M., Codish, M., and Mulkers, A. 1994b. A composite domain for freeness, sharing, and compoundness analysis of logic programs. Technical Report CW 196, Department of Computer Science, K.U. Leuven, Belgium. July.

Bruynooghe, M., Codish, M., and Mulkers, A. 1995. Abstracting unification: A key step in the design of logic program analyses. In Computer Science Today: Recent Trends and Developments, J. van Leeuwen, Ed. Lecture Notes in Computer Science, vol. 1000. Springer-Verlag, Berlin, 406–425.

Clark, K. L. 1978. Negation as failure. In Logic and Databases, H. Gallaire and J. Minker,

Eds. Plenum Press, Toulouse, France, 293–322. Codish, M., Dams, D., Filé, G., and Bruynooghe, M. 1993. Freeness analysis for

logic programs — and correctness? In Logic Programming: Proceedings of the Tenth International Conference on Logic Programming, D. S. Warren, Ed. MIT Press Series in Logic Programming. The MIT Press, Budapest, Hungary, 116–131. An extended version is available as Technical Report CW 161, Department of Computer Science, K.U. Leuven, December 1992.

Codish, M., Dams, D., Filé, G., and Bruynooghe, M. 1996. On the design of a correct

freeness analysis for logic programs. Journal of Logic Programming 28, 3, 181–206. Codish, M., Dams, D., and Yardeni, E. 1991. Derivation and safety of an abstract

unification algorithm for groundness and aliasing analysis. See Furukawa (1991), 79–93. Codish, M., Lagoon, V., and Bueno, F. 2000. An algebraic approach to sharing analysis

of logic programs. Journal of Logic Programming 42, 2, 111–149. Codish, M., Mulkers, A., Bruynooghe, M., Garcìa de la Banda, M., and Hermen-

egildo, M. 1993. Improving abstract interpretations by combining domains. In Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. ACM Press, Copenhagen, Denmark, 194–205. Also available as Technical Report CW 162, Department of Computer Science, K.U. Leuven, December 1992.

Codish, M., Mulkers, A., Bruynooghe, M., Garcìa de la Banda, M., and Hermenegildo, M. 1995. Improving abstract interpretations by combining domains. ACM Transactions on Programming Languages and Systems 17, 1 (Jan.), 28–44.

Colmerauer, A. 1982. Prolog and infinite trees. In Logic Programming, APIC Studies in Data Processing, K. L. Clark and S. Å. Tärnlund, Eds. Vol. 16. Academic Press, New York, 231–251.

Colmerauer, A. 1984. Equations and inequations on finite and infinite trees. In Proceedings of the International Conference on Fifth Generation Computer Systems (FGCS’84). ICOT, Tokyo, Japan, 85–99.

Colmerauer, A. 1990. An introduction to Prolog-III. Communications of the ACM 33, 7,

69–90. Cortesi, A. and Filé, G. 1999. Sharing is optimal. Journal of Logic Programming 38, 3,

371–386. Cortesi, A., Filé, G., and Winsborough, W. 1998. The quotient of an abstract in-

terpretation for comparing static analyses. Theoretical Computer Science 202, 1&2, 163–192.

Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages. ACM Press, New York, 238–252.

Cousot, P. and Cousot, R. 1979. Systematic design of program analysis frameworks. In Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages. ACM Press, New York, 269–282.

34 P. M. Hill, E. Zaffanella, and R. Bagnara

Filé, G. 1994. Share × Free: Simple and correct. Tech. Rep. 15, Dipartimento di Matem-

atica, Università di Padova. Dec. Furukawa, K., Ed. 1991. Logic Programming: Proceedings of the Eighth International

Conference on Logic Programming. MIT Press Series in Logic Programming. The MIT Press, Paris, France.

Giacobazzi, R., Ranzato, F., and Scozzari, F. 1998. Complete abstract interpretations made constructive. In Proceedings of 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS’98), J. Gruska and J. Zlatuska, Eds. Lecture Notes in Computer Science, vol. 1450. Springer-Verlag, Berlin, 366–377.

Hans, W. and Winkler, S. 1992. Aliasing and groundness analysis of logic programs through abstract interpretation and its safety. Tech. Rep. 92–27, Technical University of Aachen (RWTH Aachen).

Hill, P. M., Bagnara, R., and Zaffanella, E. 1998. The correctness of set-sharing. In Static Analysis: Proceedings of the 5th International Symposium, G. Levi, Ed. Lecture Notes in Computer Science, vol. 1503. Springer-Verlag, Berlin, Pisa, Italy, 99–114.

Hill, P. M., Bagnara, R., and Zaffanella, E. 2002. Soundness, idempotence and commutativity of set-sharing. Theory and Practice of Logic Programming 2, 2, 155– 201.

Hill, P. M., Bagnara, R., and Zaffanella, E. 2003. On the analysis of set-sharing, freeness and linearity for finite and rational tree languages. Tech. Rep. 2003.08, School of Computing, University of Leeds. Available at http://www.comp.leeds.ac.

uk/research/pubs/reports.shtml.

Howe, J. M. and King, A. 2003. Three optimisations for sharing. Theory and Practice

of Logic Programming 3, 2, 243–257. Intrigila, B. and Zilli, M. V. 1996. A remark on infinite matching vs infinite unifica-

tion. Journal of Symbolic Computation 21, 3, 2289–2292. Jacobs, D. and Langen, A. 1989. Accurate and efficient approximation of variable

aliasing in logic programs. In Logic Programming: Proceedings of the North American Conference, E. L. Lusk and R. A. Overbeek, Eds. MIT Press Series in Logic Programming. The MIT Press, Cleveland, Ohio, USA, 154–165.

Jaffar, J., Lassez, J.-L., and Maher, M. J. 1987. Prolog-II as an instance of the logic programming scheme. In Formal Descriptions of Programming Concepts III, M. Wirsing, Ed. North-Holland, Amsterdam, 275–299.

Keisu, T. 1994. Tree constraints. Ph.D. thesis, The Royal Institute of Technology,

Stockholm, Sweden. Also available in the SICS Dissertation Series: SICS/D–16–SE. King, A. 1994. A synergistic analysis for sharing and groundness which traces linearity.

In Proceedings of the Fifth European Symposium on Programming, D. Sannella, Ed. Lecture Notes in Computer Science, vol. 788. Springer-Verlag, Berlin, Edinburgh, UK, 363–378.

King, A. 2000. Pair-sharing over rational trees. Journal of Logic Programming 46, 1–2,

139–155. King, A. and Soper, P. 1994. Depth-k sharing and freeness. In Logic Programming: Pro-

ceedings of the Eleventh International Conference on Logic Programming, P. Van Hentenryck, Ed. MIT Press Series in Logic Programming. The MIT Press, Santa Margherita Ligure, Italy, 553–568.

Langen, A. 1990. Advanced techniques for approximating variable aliasing in logic programs. Ph.D. thesis, Computer Science Department, University of Southern California. Printed as Report TR 91-05.

Maher, M. J. 1988. Complete axiomatizations of the algebras of finite, rational and infinite trees. In Proceedings, Third Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Edinburgh, Scotland, 348–357.

Muthukumar, K. and Hermenegildo, M. 1991. Combined determination of sharing and freeness of program variables through abstract interpretation. See Furukawa (1991), 49–63. An extended version appeared in (Muthukumar and Hermenegildo 1992).

Muthukumar, K. and Hermenegildo, M. 1992. Compile-time derivation of variable dependency using abstract interpretation. Journal of Logic Programming 13, 2&3, 315– 347.

Smolka, G. and Treinen, R. 1994. Records for logic programming. Journal of Logic

Programming 18, 3, 229–258. Søndergaard, H. 1986. An application of abstract interpretation of logic programs:

Occur check reduction. In Proceedings of the 1986 European Symposium on Programming, B. Robinet and R. Wilhelm, Eds. Lecture Notes in Computer Science, vol. 213. Springer-Verlag, Berlin, 327–338.

Swedish Institute of Computer Science, Programming Systems Group 1995. SICStus Prolog User’s Manual, release 3 #0 ed. Swedish Institute of Computer Science, Programming Systems Group.

Zaffanella, E. 2001. Correctness, precision and efficiency in the sharing analysis of real logic languages. Ph.D. thesis, School of Computing, University of Leeds, Leeds, U.K.

Available at http://www.cs.unipr.it/~zaffanella/.

Zaffanella, E., Bagnara, R., and Hill, P. M. 1999. Widening Sharing. In Principles and Practice of Declarative Programming, G. Nadathur, Ed. Lecture Notes in Computer Science, vol. 1702. Springer-Verlag, Berlin, Paris, France, 414–431.

Zaffanella, E., Hill, P. M., and Bagnara, R. 1999. Decomposing non-redundant sharing by complementation. In Static Analysis: Proceedings of the 6th International Symposium, A. Cortesi and G. Filé, Eds. Lecture Notes in Computer Science, vol. 1694. Springer-Verlag, Berlin, Venice, Italy, 69–84.

Zaffanella, E., Hill, P. M., and Bagnara, R. 2002. Decomposing non-redundant sharing by complementation. Theory and Practice of Logic Programming 2, 2, 233–261.