Finite-Tree Analysis

for Constraint Logic-Based Languages^{⋆}

Roberto Bagnara^{1}, Roberta Gori^{2}, Patricia M. Hill^{3}, and Enea Zaffanella^{1}

1 Department of Mathematics, University of Parma, Italy.

               {bagnara,zaffanella}@cs.unipr.it

2 Department of Computer Science, University of Pisa, Italy.

                       gori@di.unipi.it

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

                    hill@comp.leeds.ac.uk

Abstract. Logic languages based on the theory of rational, possibly infinite, trees have much appeal in that rational trees allow for faster unification (due to the omission of the occurs-check) and increased expressivity. Note that cyclic terms can provide a very efficient representation of grammars and other useful objects. Unfortunately, the use of infinite rational trees has problems. For instance, many of the built-in and library predicates are ill-defined for such trees and need to be supplemented by run-time checks whose cost may be significant. Moreover, some widelyused program analysis and manipulation techniques are only correct for those parts of programs working over finite trees. It is thus important to obtain, automatically, a knowledge of those program variables (the finite variables) that, at the program points of interest, will always be bound to finite terms. For these reasons, we propose here a new data-flow analysis that captures such information. We present a parametric domain where a simple component for recording finite variables is coupled with a generic domain (the parameter of the construction) providing sharing information. The sharing domain is abstractly specified so as to guarantee the correctness of the combined domain and the generality of the approach.

1 Introduction

The intended computation domain of most logic-based languages^{1} includes the algebra (or structure) of finite trees. Other (constraint) logic-based languages, such as Prolog II and its successors [10, 12], SICStus Prolog [36], and Oz [34], refer to a computation domain of rational trees. A rational tree is a possibly infinite tree with a finite number of distinct subtrees and, as is the case for finite trees,

⋆ This work has been partly supported by MURST project “Certificazione automatica di programmi mediante interpretazione astratta.” Some of this work was done during visits of the fourth author to Leeds, funded by EPSRC under grant M05645.

1 That is, ordinary logic languages, (concurrent) constraint logic languages, functional logic languages and variations of the above.

where each node has a finite number of immediate descendants. These properties will ensure that rational trees, even though infinite in the sense that they admit paths of infinite length, can be finitely represented. One possible representation makes use of connected, rooted, directed and possibly cyclic graphs where nodes are labeled with variable and function symbols as is the case of finite trees.

Applications of rational trees in logic programming include graphics [18], parser generation and grammar manipulation [10, 21], and computing with finitestate automata [10]. Other applications are described in [20] and [23]. Going from Prolog to CLP, [31] combines constraints on rational trees and record structures, while the logic-based language Oz allows constraints over rational and feature trees [34]. The expressive power of rational trees is put to use, for instance, in several areas of natural language processing. Rational trees are used in implementations of the HPSG formalism (Head-driven Phrase Structure Grammar) [32], in the ALE system (Attribute Logic Engine) [8], and in the ProFIT system (Prolog with Features, Inheritance and Templates) [19].

While rational trees allow for increased expressivity, they also come equipped with a surprising number of problems. As we will see, some of these problems are so serious that rational trees must be used in a very controlled way, disallowing them in any context where they are “dangerous”. This, in turn, causes a secondary problem: in order to disallow rational trees in selected contexts one must first detect them, an operation that may be expensive.

The first thing to be aware of is that almost any semantics-based program manipulation technique developed in the field of logic programming —whether it be an analysis, a transformation, or an optimization— assumes a computation domain of finite trees. Some of these techniques might work with the rational trees but their correctness has only been proved in the case of finite trees. Others are clearly inapplicable. Let us consider a very simple Prolog program:

                     list([]).
                     list([ |T]) :- list(T).

Most automatic and semi-automatic tools for proving program termination and for complexity analysis agree on the fact that list/1 will terminate when invoked with a ground argument. Consider now the query

                     ?- X = [a|X], list(X).

and note that, after the execution of the first rational unification, the variable X will be bound to a rational term containing no variables, i.e., the predicate list/1 will be invoked with X ground. However, if such a query is given to, say, SICStus Prolog, then the only way to get the prompt back is by pressing ^C. The problem stems from the fact that the analysis techniques employed by these tools are only sound for finite trees: as soon as they are applied to a system where the creation of cyclic terms is possible, their results are inapplicable. The situation can be improved by combining these termination and/or complexity analyses by a finiteness analysis providing the precondition for the applicability of the other techniques.

The implementation of built-in predicates is another problematic issue. Indeed, it is widely acknowledged that, for the implementation of a system that provides real support for the rational trees, the biggest effort concerns proper handling of built-ins. Of course, the meaning of ‘proper’ depends on the actual built-in. Built-ins such as copy_term/2 and ==/2 maintain a clear semantics when passing from finite to rational trees. For others, like sort/2, the extension can be questionable:^{2} both raising an exception and answering Y = [a] can be argued to be “the right reaction” to the query

                    ?- X = [a|X], sort(X, Y).

Other built-ins do not tolerate infinite trees in some argument positions. A good implementation should check for finiteness of the corresponding arguments and make sure “the right thing” —failing or raising an appropriate exception— always happens. However, such behavior appears to be uncommon. A small experiment we conducted on six Prolog implementations with queries like

                    ?- X = 1+X, Y is X.
                    ?- X = [97|X], name(Y, X).
                    ?- X = [X|X], Y =.. [f|X].

resulted in infinite loops, memory exhaustion and/or system thrashing, segmentation faults or other fatal errors. One of the implementations tested, SICStus Prolog, is a professional one and implements run-time checks to avoid most cases where built-ins can have catastrophic effects.^{3} The remaining systems are a bit more than research prototypes, but will clearly have to do the same if they evolve to the stage of production tools. Again, a data-flow analysis aimed at the detection of those variables that are definitely bound to finite terms would allow to avoid a (possibly significant) fraction of the useless run-time checks. Note that what has been said for built-in predicates applies to libraries as well. Even though it may be argued that it is enough for programmers to know that they should not use a particular library predicate with infinite terms, it is clear that the use of a “safe” library, including automatic checks which ensure that such predicates are never called with an illegal argument, will result in more robust systems. With the appropriate data-flow analyses, safe libraries do not have to be inefficient libraries.

Another serious problem is the following: the ISO Prolog standard term ordering cannot be extended to rational trees [M. Carlsson, Personal communication, October 2000]. Consider the rational trees defined by A = f(B, a) and B = f(A, b). Clearly, A == B does not hold. Since the standard term ordering is total, we must have either A @< B or B @< A. Assume A @< B. Then f(A, b) @< f(B, a), since the ordering of terms having the same principal functor is inherited by the ordering of subterms considered in a left-to-right fashion. Thus B @< A must hold, which is a contradiction. A dual contradiction

2 Even though sort/2 is not required to be a built-in by the standard, it is offered as

such by several implementations. 3 SICStus 3.8.5 still loops on ?- X = [97|X], name(Y, X).

is obtained by assuming B @< A. As a consequence, applying one of the Prolog term-ordering predicates to one or two infinite terms may cause inconsistent results, giving rise to bugs that are exceptionally difficult to diagnose. For this reason, any system that extends ISO Prolog with rational trees ought to detect such situations and make sure they are not ignored (e.g., by throwing an exception or aborting execution with a meaningful message). However, predicates such as the term-ordering ones are likely to be called a significant number of times, since they are often used to maintain structures implementing ordered collections of terms. This is another instance of the efficiency issue mentioned above.

In this paper, we present a parametric abstract domain for finite-tree analysis, denoted by H × P. This domain combines a simple component H (the finiteness component), recording the set of definitely finite variables, with a generic domain P (the parameter of the construction), providing sharing information. The term “sharing information” is to be understood in its broader meaning, which includes variable aliasing, groundness, linearity, freeness and any other kind of information that can improve the precision on these components, such as explicit structural information. Several domain combinations and abstract operators, characterized by different precision/complexity trade-offs, have been proposed to capture these properties (see [5] for an account of some of them). By giving a generic specification for this parameter component, in the style of the open product construct proposed in [14], it is possible to define and establish the correctness of the abstract operators on the finite-tree domain independently from any particular domain for sharing analysis.

The paper is structured as follows. The required notations and preliminary concepts are given in Section 2. The finite-tree domain is then introduced in Section 3: Section 3.1 provides the specification of the parameter domain P; Section 3.2 defines the abstraction function for the finiteness component H ; Section 3.3 defines the abstract unification operator for H × P. A description of some ongoing work on the subject is given in Section 4 where a possible instance of the parameter P is also specified. We conclude in Section 5.

A longer version of this paper with proofs of the results presented here is available as a technical report [1].

2 Preliminaries

2.1 Infinite Terms and Substitutions

For a set S, ℘(S) is the powerset of S, whereas ℘_{f}(S) is the set of all the finite subsets of S. Let Sig denote a possibly infinite set of function symbols, ranked over the set of natural numbers. It is assumed that Sig contains at least one function symbol having rank 0 and one having rank greater than 0. 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).

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. If a occurs more than once in a multiset M we write a M.

Suppose s, t ∈ Terms: s and t are independent if vars(s) ∩ vars(t) = ∅; if y ∈ vars(t) and ¬(y mvars(t)) we say that variable y occurs linearly in t, more briefly written using the predication occ lin(y, 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. As we have specified that Sig contains function symbols of rank 0 and rank greater than 0, GTerms ∩ HTerms ≠ ∅ and GTerms \ HTerms ≠ ∅.

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 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 σ. 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.

If t ∈ HTerms, we write tσ to denote σ(t) and t[x/s] to denote t{x ↦ s}. 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(σ), x ≠ xστ } ∪ { x ↦ xτ | x ∈ dom(τ) \ dom(σ) }.

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, s ∈ HTerms, the sequence of finite terms

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

converges to a (possibly infinite) term, denoted σ^{∞}(s) [25, 29]. 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 ↦ t can map a domain variable x into a term t ∈ Terms \ HTerms.

2.2 Equations

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).

Languages such as Prolog II, SICStus and Oz are based on RT , the theory of rational trees [10, 11]. This is a syntactic equality theory (i.e., a theory where the function symbols are uninterpreted), augmented with a uniqueness axiom for each substitution in rational solved form. Informally speaking these axioms state that, after assigning a ground rational tree to each non-domain variable, the substitution uniquely defines a ground rational tree for each of its domain variables. Thus, any set of equations in rational solved form is, by definition, satisfiable in RT . 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 usually expect. We refer the interested reader to [27, 28, 30] for details on the subject.

Given a set of equations e ∈ ℘_{f}(Eqs) that is satisfiable in RT , a substitution σ ∈ RSubst is called a solution for e in RT if RT ⊢ ∀(σ → e), i.e., if every model of the theory RT is also a model of the first order formula ∀(σ → e). If in addition vars(σ) ⊆ vars(e), then σ is said to be a relevant solution for e. Finally, σ is a most general solution for e in RT if RT ⊢ ∀(σ ↔ e). In this paper, the set of all the relevant most general solution for e in RT will be denoted by mgs(e).

2.3 The Concrete Domain

Throughout the paper, we assume a knowledge of the basic concepts of abstract interpretation theory [15, 16].

For the purpose of this paper, we assume a concrete domain constituted by pairs of the form (Σ, V), where V is a finite set of variables of interest and Σ is a (possibly infinite) set of substitutions in rational solved form.

Definition 1. (The concrete domain.) Let D^{♭} =^{def} ℘(RSubst) × ℘_{f}(Vars). If (Σ, V) ∈ D^{♭}, then (Σ, V) represents the (possibly infinite) set of first-order formulas { ∃Δ . σ | σ ∈ Σ, Δ = vars(σ)\V } where σ is interpreted as the logical conjunction of the equations corresponding to its bindings.

Concrete domains for constraint languages would be similar. If the analyzed language allows the use of constraints on various domains to restrict the values of the variable leaves of rational trees, the corresponding concrete domain would have one or more extra components to account for the constraints (see [2] for an example).

The concrete element ({{x ↦ f(y)}}, {x, y}) expresses a dependency between x and y. In contrast, ({{x ↦ f(y)}}, {x}) only constrains x. The same concept can be expressed by saying that in the first case the variable name ‘y’ matters, but it does not in the second case. Thus, the set of variables of interest is crucial for defining the meaning of the concrete and abstract descriptions. Despite this, always specifying the set of variables of interest would significantly clutter the presentation. Moreover, most of the needed functions on concrete and abstract descriptions preserve the set of variables of interest. For these reasons, we assume the existence of a set VI ∈ ℘_{f}(Vars) that contains, at each stage of the analysis, the current variables of interest.^{4} As a consequence, when the context makes it clear that Σ ∈ ℘(RSubst), we will write Σ ∈ D^{♭} as a shorthand for (Σ, VI ) ∈ D^{♭}.

3 An Abstract Domain for Finiteness Analysis

Finite-tree analysis applies to logic-based languages computing over a domain of rational trees where cyclic structures are allowed. In contrast, analyses aimed at occurs-check reduction [17, 35] apply to programs that are meant to compute on a domain of finite trees only, but have to be executed over systems that are either designed for rational trees or intended just for the finite trees but omit the occurs-check for efficiency reasons. Despite their different objectives, finite-tree and occurs-check analyses have much in common: in both cases, it is important to detect all program points where cyclic structures can be generated.

4 This parallels what happens in the efficient implementation of data-flow analyzers. In fact, almost all the abstract domains currently in use do not need to represent explicitly the set of variables of interest. In contrast, this set is maintained externally and in a unique copy, typically by the fixpoint computation engine.

Note however that, when performing occurs-check reduction, one can take advantage of the following invariant: all data structures generated so far are finite. This property is maintained by transforming the program so as to force finiteness whenever it is possible that a cyclic structure could have been built.^{5} In contrast, a finite-tree analysis has to deal with the more general case when some of the data structures computed so far may be cyclic. It is therefore natural to consider an abstract domain made up of two components. The first one simply represents the set of variables that are guaranteed not to be bound to infinite terms. We will denote this finiteness component by H (from Herbrand).

Definition 2. (The finiteness component.) The finiteness component is the set H =^{def} ℘(VI ) partially ordered by reverse subset inclusion.

The second component of the finite-tree domain should maintain any kind of information that may be useful for computing finiteness information.

It is well-known that sharing information as a whole, therefore including possible variable aliasing, definite linearity, and definite freeness, has a crucial role in occurs-check reduction so that, as observed before, it can be exploited for finite-tree analysis too. Thus, a first choice for the second component of the finite-tree domain would be to consider one of the standard combinations of sharing, freeness and linearity as defined, e.g., in [5, 6, 22]. However, this would tie our specification to a particular sharing analysis domain, whereas the overall approach seems to be inherently more general. For this reason, we will define a finite-tree analysis based on the abstract domain schema H ×P, where the generic sharing component P is a parameter of the abstract domain construction. This approach can be formalized as an application of the open product operator [14].

3.1 The parameter component P

Elements of P can encode any kind of information. We only require that substitutions that are equivalent in the theory RT are identified in P.

Definition 3. (The parameter component.) The parameter component P is an abstract domain related to the concrete domain D^{♭} by means of the concretization function γ_{P} : P → ℘(RSubst) such that, for all p ∈ P,

(σ ∈ γ_{P} (p) ∧ (RT ⊢ ∀(σ ↔ τ))) ⟹ τ ∈ γ_{P} (p).

The interface between H and P is provided by a set of predicates and functions that satisfy suitable correctness criteria. Note that, for space limitations, we will only specify those abstract operations that are useful to define abstract unification on the combined domain H × P. The other operations needed for a full description of the analysis, such as renamings, upper bound operators and projections, are very simple and, as usual, do not pose any problems.

5 Such a requirement is typically obtained by replacing the unification with a call to unify with occurs check/2. As an alternative, in some systems based on rational trees it is possible to insert, after each problematic unification, a finiteness test for the generated term.

Definition 4. (Abstract operators on P.) Let s, t ∈ HTerms be finite terms. For each p ∈ P, we define the following predicates: s and t are independent in p if and only if ind_{p} : HTerms^{2} → Bool holds for (s, t), where

ind_{p}(s, t) ⟹ ∀σ ∈ γ_{P} (p) : vars(rt(s, σ)) ∩ vars(rt(t, σ)) = ∅;

s and t share linearly in p if and only if share lin_{p} : HTerms^{2} → Bool holds for (s, t), where

share lin_{p}(s, t) ⟹ ∀σ ∈ γ_{P} (p) :
∀y ∈ vars(rt(s, σ)) ∩ vars(rt(t, σ)) :
occ lin(y, rt(s, σ)) ∧ occ lin(y, rt(t, σ));

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

ground_{p}(t) ⟹ ∀σ ∈ γ_{P} (p) : rt(t, σ) ∈ GTerms;

t is ground-or-free in p if and only if gfree_{p} : HTerms → Bool holds for t, where

gfree_{p}(t) ⟹ ∀σ ∈ γ_{P} (p) : rt(t, σ) ∈ GTerms ∨ rt(t, σ) ∈ Vars;

s and t are or-linear in p if and only if or lin_{p} : HTerms^{2} → Bool holds for (s, t), where

or lin_{p}(s, t) ⟹ ∀σ ∈ γ_{P} (p) : rt(s, σ) ∈ LTerms ∨ rt(t, σ) ∈ LTerms;

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

lin_{p}(s) ⟺^{def} or lin_{p}(s, s).

For each p ∈ P, the following functions compute subsets of the set of variables of interest: the function share same var_{p} : HTerms × HTerms → ℘(VI ) returns a set of variables that may share with the given terms via the same variable. For each s, t ∈ HTerms,

share same var_{p}(s, t) ⊇ \{ y ∈ VI | \begin{matrix}∃σ ∈ γ_{P} (p) . \\ ∃z ∈ vars(rt(y, σ)) . \\ z ∈ vars(rt(s, σ)) ∩ vars(rt(t, σ)) \end{matrix} \};

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

share with_{p}(t) =^{def} { y ∈ VI | y ∈ share same var_{p}(y, t) }.

The function amgu_{P} : P×Bind → P correctly captures the effects of a binding on an element of P. For each (x ↦ t) ∈ Bind and p ∈ P, let

p′ =^{def} amgu_{P} (p, x ↦ t).

For all σ ∈ γ_{P} (p), if τ ∈ mgs(σ ∪ {x = t}), then τ ∈ γ_{P} (p′).

As it will be shown in Section 4.1, some of these generic operators can be directly mapped into the corresponding abstract operators defined for well-known sharing analysis domains. However, the specification given in Definition 4, besides being more general than a particular implementation, also allows for a modular approach when proving correctness results.

3.2 The abstraction function for H

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.^{6} 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) ⋯)\}

for n = 1, 2, …, all map the variable x into the same rational tree (which is usually denoted by 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 we may end up with σ^{∞} ∉ RSubst, as σ^{∞} can map domain variables to infinite rational terms.

This poses a non-trivial problem when trying to define a “good” abstraction function, since it would be really desirable for this function to map any two equivalent concrete elements to the same abstract element. As shown in [24], the classical abstraction function for set-sharing analysis [13, 26], which was defined for idempotent substitutions only, does not enjoy this property when applied, as it is, to arbitrary substitutions in rational solved form. A possibility is to look for a more general abstraction function that allows to obtain the desired property. For example, in [24] the sharing-group operator sg of [26] is replaced by an occurrence operator, occ, defined by means of a fixpoint computation. We now provide a similar fixpoint construction defining the finiteness operator.

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

Definition 5. (Finiteness functions.) For each n ∈ ℕ, the finiteness function hvars_{n}: RSubst → ℘(Vars) is defined, for each σ ∈ RSubst, by

hvars_{0}(σ) =^{def} Vars \ dom(σ)

and, for n > 0, by

hvars_{n}(σ) =^{def} hvars_{n−1}(σ) ∪ { y ∈ dom(σ) | vars(yσ) ⊆ hvars_{n−1}(σ) }.

For each σ ∈ RSubst and each i ≥ 0, we have hvars_{i}(σ) ⊆ hvars_{i+1}(σ) and also that Vars \ hvars_{i}(σ) ⊆ dom(σ) is a finite set. By these two properties, the following fixpoint computation is well defined and finitely computable.

Definition 6. (Finiteness operator.) For each σ ∈ RSubst, the finiteness operator hvars: RSubst → ℘(Vars) is given by hvars(σ) =^{def} hvars_{ℓ}(σ) where ℓ =^{def} ℓ(σ) ∈ ℕ is such that hvars_{ℓ}(σ) = hvars_{n}(σ) for all n ≥ ℓ.

The following proposition shows that the hvars operator precisely captures the intended property.

Proposition 1. If σ ∈ RSubst and x ∈ Vars then

x ∈ hvars(σ) ⟺ rt(x, σ) ∈ HTerms.

Example 1. Consider σ ∈ RSubst, where

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

Then,

hvars_{0}(σ) = Vars \ {x_{1}, x_{2}, x_{3}, x_{4}},
hvars_{1}(σ) = Vars \ {x_{1}, x_{3}, x_{4}},
hvars_{2}(σ) = Vars \ {x_{3}, x_{4}}
= hvars(σ).

Thus, x_{1} ∈ hvars(σ), although vars(x_{1}σ) ⊆ dom(σ).

The abstraction function for H can then be defined in the obvious way.

Definition 7. (The abstraction function for H .) The abstraction function α_{H}: RSubst → H is defined, for each σ ∈ RSubst, by

α_{H}(σ) =^{def} VI ∩ hvars(σ).

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

α_{H}(Σ) =^{def} ⋂{ α_{H}(σ) | σ ∈ Σ }.

Since the abstraction function α_{H} is additive, the concretization function is given by its adjoint [15]:

γ_{H}(h) =^{def} { σ ∈ RSubst | α_{H}(σ) ⊇ h }.

With these definitions, we have the desired result: equivalent substitutions in rational solved form have the same finiteness abstraction.

Theorem 1. If σ, τ ∈ RSubst and RT ⊢ ∀(σ ↔ τ), then α_{H}(σ) = α_{H}(τ).

3.3 Abstract unification on H × P

The abstract unification for the combined domain H × P is defined by using the abstract predicates and functions as specified for P as well as a new finiteness predicate for the domain H .

Definition 8. (Abstract unification on H × P.) A term t ∈ HTerms is a finite tree in h if and only if the predicate hterm_{h} : HTerms → Bool holds for t, where hterm_{h}(t) =^{def} vars(t) ⊆ h.

The function amgu_{H}: (H × P) × Bind → H captures the effects of a binding on an H element. Let ⟨h, p⟩ ∈ H × P and (x ↦ t) ∈ Bind. Then

amgu_{H}(⟨h, p⟩, x ↦ t) =^{def} h′,

where

h′ =^{def} \begin{cases}h ∪ vars(t), & if hterm_{h}(x) ∧ ground_{p}(x); \\ h ∪ \{x\}, & if hterm_{h}(t) ∧ ground_{p}(t); \\ h, & if hterm_{h}(x) ∧ hterm_{h}(t) \\ & ∧ ind_{p}(x, t) ∧ or lin_{p}(x, t); \\ h, & if hterm_{h}(x) ∧ hterm_{h}(t) \\ & ∧ gfree_{p}(x) ∧ gfree_{p}(t); \\ h \ share same var_{p}(x, t), & if hterm_{h}(x) ∧ hterm_{h}(t) \\ & ∧ share lin_{p}(x, t) \\ & ∧ or lin_{p}(x, t); \\ h \ share with_{p}(x), & if hterm_{h}(x) ∧ lin_{p}(x); \\ h \ share with_{p}(t), & if hterm_{h}(t) ∧ lin_{p}(t); \\ h \ (share with_{p}(x) ∪ share with_{p}(t)), & otherwise. \end{cases}

The abstract unification function amgu: (H × P) × Bind → H × P, for any ⟨h, p⟩ ∈ H × P and (x ↦ t) ∈ Bind, is given by

amgu(⟨h, p⟩, x ↦ t) =^{def} ⟨amgu_{H}(⟨h, p⟩, x ↦ t), amgu_{P} (p, x ↦ t)⟩.

In the computation of h′ (the new finiteness component resulting from the abstract evaluation of a binding) there are eight cases based on properties holding for the concrete terms described by x and t.

1. In the first case, the concrete term described by x is both finite and ground. Thus, after a successful execution of the binding, any concrete term described by t will be finite. Note that t could have contained variables which may be possibly bound to cyclic terms just before the execution of the binding.

2. The second case is symmetric to the first one. Note that these are the only cases when a “positive” propagation of finiteness information is correct. In contrast, in all the remaining cases, the goal is to limit as much as possible the propagation of “negative” information, i.e., the possible cyclicity of terms.

3. The third case exploits the classical results proved in research work on occurscheck reduction [17, 35]. Accordingly, it is required that both x and t describe finite terms that do not share. The use of the implicitly disjunctive predicate or lin_{p} allows for the application of this case even when neither x nor t are known to be definitely linear. For instance, as observed in [17], this may happen when the component P embeds the domain Pos for groundness analysis.^{7}

4. The fourth case exploits the observation that cyclic terms cannot be created when unifying two finite terms that are either ground or free. Groundor-freeness [5] is a safe, more precise and inexpensive replacement for the classical freeness property when combining sharing analysis domains.

5. The fifth case applies when unifying a linear and finite term with another finite term possibly sharing with it, provided they can only share linearly (namely, all the shared variables occur linearly in the considered terms). In such a context, only the shared variables can introduce cycles.

6. In the sixth case, we drop the assumption about the finiteness of the term described by t. As a consequence, all variables sharing with x become possibly cyclic. However, provided x describes a finite and linear term, all finite variables independent from x preserve their finiteness.

7. The seventh case is symmetric to the sixth one.

8. The last case states that term finiteness is preserved for all variables that are independent from both x and t. Note that this case is only used when none of the other cases apply.

The following result, together with the assumption on amgu_{P} as specified in Definition 4, ensures that abstract unification on the combined domain H × P is correct.

Theorem 2. Let ⟨h, p⟩ ∈ H ×P and (x ↦ t) ∈ Bind, where {x}∪vars(t) ⊆ VI . Let also σ ∈ γ_{H}(h) ∩ γ_{P} (p) and h′ = amgu_{H}(⟨h, p⟩, x ↦ t). Then

τ ∈ mgs(σ ∪ {x = t}) ⟹ τ ∈ γ_{H}(h′).

7 Let t be y. Let also P be Pos. Then, given the Pos formula ϕ =^{def} (x ∨ y), both ind_{ϕ}(x, y) and or lin_{ϕ}(x, y) satsify the conditions in Definition 4. Note that from ϕ we cannot infer that x is definitely linear and neither that y is definitely linear.

4 Ongoing and Further Work

4.1 An instance of the parameter domain P

As discussed in Section 3, several abstract domains for sharing analysis can be used to implement the parameter component P. One could consider the wellknown set-sharing domain of Jacobs and Langen [26]. In such a case, all the non-trivial correctness results have already been established in [24]: in particular, the abstraction function provided in [24] satisfies the requirement of Definition 3 and the abstract unification operator has been proven correct with respect to rational-tree unification. Note however that, since no freeness and linearity information is recorded in the plain set-sharing domain, some of the predicates of Definition 4 need to be grossly approximated.

Therefore, a better choice would be to consider the abstract domain SFL [5] (see also [6]) that represents possible sharing. This domain incorporates the set-sharing domain of Jacobs and Langen with definite freeness and linearity information; the information being encoded by two sets of variables, one satisfying the property of freeness and the other, the property of linearity.

Definition 9. (The set-sharing domain SH .) The set SH is defined by SH =^{def} ℘(SG), where SG =^{def} ℘(VI ) \ {∅} is the set of sharing groups. SH is ordered by subset inclusion.

Definition 10. (The domain SFL.) Let F =^{def} ℘(VI ) and L =^{def} ℘(VI ) be partially ordered by reverse subset inclusion. The domain SFL is defined by the Cartesian product SFL =^{def} SH × F × L ordered by ‘≤_{S}’, the component-wise extension of the orderings defined on the sub-domains.

Note that a complete definition, besides explicitly dealing with the set of relevant variables VI , would require the addition of a bottom element ⊥ representing the semantics of those program fragments that have no successful computations.

In the next definition we introduce a few well-known operations on the setsharing domain SH . These will be used to define the operations on the domain SFL.

Definition 11. (Abstract operators on SH .) For each sh ∈ SH and each V ⊆ VI , the extraction of the relevant component of sh with respect to V is given by the function rel: ℘(VI ) × SH → SH defined as

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

For each sh ∈ SH and each V ⊆ VI , the function \overline{rel}: ℘(VI ) × SH → SH gives the irrelevant component of sh with respect to V. It is defined as

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

The function (·)^{⋆}: SH → SH , called star-union, is given, for each sh ∈ SH , by

sh^{⋆} =^{def} { S ∈ SG | ∃n ≥ 1 . ∃T_{1}, …, T_{n} ∈ sh . S = ⋃_{i=1}^{n} T_{i} }.

For each sh_{1}, sh_{2} ∈ SH , the function bin: SH × SH → SH , called binary union, is given by

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

It is now possible to define the implementation, on the domain SFL, of all the predicates and functions specified in Definition 4.

Definition 12. (Abstract operators on SFL.) For each d = ⟨sh, f, l⟩ ∈ SFL, for each s, t ∈ HTerms, where vars(s) ∪ vars(t) ⊆ VI , let R_{s} = rel(vars(s), sh) and R_{t} = rel(vars(t), sh). Then

ind_{d}(s, t) =^{def} (R_{s} ∩ R_{t} = ∅);
ground_{d}(t) =^{def} (vars(t) ⊆ VI \ vars(sh));
occ lin_{d}(y, t) =^{def} ground_{d}(y) ∨ (occ lin(y, t) ∧ (y ∈ l)
∧ ∀z ∈ vars(t) : (y ≠ z ⟹ ind_{d}(y, z)));
share lin_{d}(s, t) =^{def} ∀y ∈ vars(R_{s} ∩ R_{t}) :
y ∈ vars(s) ⟹ occ lin_{d}(y, s)
∧ y ∈ vars(t) ⟹ occ lin_{d}(y, t);
free_{d}(t) =^{def} ∃y ∈ VI . (y = t) ∧ (y ∈ f);
gfree_{d}(t) =^{def} ground_{d}(t) ∨ free_{d}(t);
lin_{d}(t) =^{def} ∀y ∈ vars(t) : occ lin_{d}(y, t);
or lin_{d}(s, t) =^{def} lin_{d}(s) ∨ lin_{d}(t);
share same var_{d}(s, t) =^{def} vars(R_{s} ∩ R_{t});
share with_{d}(t) =^{def} vars(R_{t}).

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 V_{xt} = {x} ∪ vars(t) ⊆ VI . Let R_{x} = rel({x}, sh) and R_{t} = rel(vars(t), sh). Let also

sh′ =^{def} \overline{rel}(V_{xt}, sh) ∪ bin(S_{x}, S_{t}),
S_{x} =^{def} \begin{cases}R_{x}, & if free_{d}(x) ∨ free_{d}(t) ∨ (lin_{d}(t) ∧ ind_{d}(x, t)); \\ R_{x}^{⋆}, & otherwise; \end{cases}

S_{t} =^{def} \begin{cases}R_{t}, & if free_{d}(x) ∨ free_{d}(t) ∨ (lin_{d}(x) ∧ ind_{d}(x, t)); \\ R_{t}^{⋆}, & otherwise; \end{cases}

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

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

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

Then amgu_{S}(d, x ↦ t) =^{def} ⟨sh′, f′, l′⟩.

It is worth noting that, when observing the term finiteness property, set-sharing is strictly more precise than pair-sharing, since a set-sharing domain is strictly more precise when computing the functions share same var_{p} and share lin_{p}.^{8} This observation holds regardless of the pair-sharing variant considered, including ASub [9, 35], PSD [3] and Sh^{PSh} [33].

It remains for us to establish that the relations and functions given in Definition 12 satisfy all the requirements of Definitions 3 and 4. This will require a proof of the correctness, with respect to rational unification, of the abstract operators defined on the domain SFL, thereby generalizing and extending the results proved in [24] for the set-sharing domain of Jacobs and Langen.

Note that the domain SFL is not the target of the generic specification given in Definition 4; more powerful sharing domains can also satisfy this schema, including all the enhanced combinations considered in [5]. For instance, as the predicate gfree_{d} defined on SFL does not fully exploit the disjunctive nature of its generic specification gfree_{p}, the precision of the analysis may be improved by adding a domain component explicitly tracking ground-or-freeness, as proposed in [5]. The same argument applies to the predicate or lin_{d}, with respect to or lin_{p}, when considering the combination with the groundness domain Pos.

In order to provide an experimental evaluation of the proposed finiteness analysis, we are implementing H × P where the P component is the SFL domain extended with some of the enhancements described in [5]. One of these

8 For the expert: consider the abstract evaluation of the binding x ↦ y and the description ⟨h, d⟩ ∈ H × SFL, where h = {x, y, z} and d = ⟨sh, f, l⟩ is such that sh = {{x, y}, {x, z}, {y, z}}, f = ∅ and l = {x, y, z}. Then z ∉ share same var_{d}(x, y) so that we have h′ = {z}. In contrast, when using a pair-sharing domain such as PSD, the element d is equivalent to d′ = ⟨sh′, f, l⟩, where sh′ = sh ∪ {{x, y, z}}. Hence we have z ∈ share same var_{d′}(x, y) and h′ = ∅. Thus, in sh the information provided by the lack of the sharing group {x, y, z} is redundant when observing pairsharing and groundness, but it is not redundant when observing term finiteness.

enhancements uses information about the actual structure of terms. It has been shown in [2] that this structural information, provided by integrating the generic Pattern(·) construction with SFL, can have a key role in improving the precision of sharing analysis and, in particular, allowing better identification where cyclic structures may appear. Thus, it is expected that structural information captured using Pattern(H ×P) can improve the precision of finite-tree analysis; both with respect to the parametric component P and the finiteness component H itself.

4.2 Term-Finiteness Dependencies

The parametric domain H × P captures the negative aspect of term-finiteness, that is, the circumstances under which finiteness can be lost. When a binding has the potential for creating one or more rational terms, the operator amgu_{H} removes from h all the variables that may be bound to non-finite terms. However, term-finiteness has also a positive aspect: there are cases where a variable is guaranteed to be bound to a finite term and this knowledge can be propagated to other variables. Guarantees of finiteness are provided by several built-ins like

unify_with_occurs_check/2, var/1, name/2, all the arithmetic predicates, and

so forth. SICStus Prolog also provides an explicit acyclic_term/1 predicate.

The term-finiteness information provided by the h component of H × P does not capture the information concerning how finiteness of one variable affects the finiteness of other variables. This kind of information, usually termed relational information, is very important as it allows the propagation of positive finiteness information. An important source of relational information comes from dependencies. Consider the terms t_{1} =^{def} f(x), t_{2} =^{def} g(y), and t_{3} =^{def} h(x, y): it is clear that, for each assignment of rational terms to x and y, t_{3} is finite if and only if t_{1} and t_{2} are so. We can capture this by the Boolean formula t_{3} ↔ (t_{1} ∧ t_{2}). The reasoning is based on the following facts:

1. t_{1}, t_{2}, and t_{3} are finite terms, so that the finiteness of their instances depends only on the finiteness of the terms that take the place of x and y.

2. t_{3} covers both t_{1} and t_{2}, that is, vars(t_{3}) ⊇ vars(t_{1}) ∪ vars(t_{2}); this means that, if an assignment to the variables of t_{3} produces a finite instance of t_{3}, that very same assignment will necessarily result in finite instances of t_{1} and t_{2}. Conversely, an assignment producing non-finite instances of t_{1} or t_{2} will forcibly result in a non-finite instance of t_{3}.

3. Similarly, t_{1} and t_{2}, taken together, cover t_{3}.

The important point to notice is that the indicated dependency will continue to hold for any further simultaneous instantiation of t_{1}, t_{2}, and t_{3}. In other words, such dependencies are preserved by forward computations (since they proceed by consistently instantiating program variables).

Consider the abstract binding x ↦ t where t is a finite term such that vars(t) = {y_{1}, …, y_{n}}. After this binding has been successfully performed, the destinies of x and t concerning term-finiteness are tied together forever. This tie can be described by the dependency formula

x ↔ (y_{1} ∧ ⋯ ∧ y_{n}),  (1)

meaning that x will be bound to a finite term if and only if, for each i = 1, …, n, y_{i} is bound to a finite term. While the dependency expressed by (1) is a correct description of any computation state following the application of the binding x ↦ t, it is not as precise as it could be. Suppose that x and y_{k} are indeed the same variable. Then (1) is logically equivalent to

x → (y_{1} ∧ ⋯ ∧ y_{k−1} ∧ y_{k+1} ∧ ⋯ ∧ y_{n}).  (2)

Correct: whenever x is bound to a finite term, all the other variables will be bound to finite terms. The point is that x has just been bound to a non-finite term, irrevocably: no forward computation can change this. Thus, the implication (2) holds vacuously. The precise and correct description for the state of affairs caused by the cyclic binding is, instead, the negated atom ¬x, whose intuitive reading is “x is not (and never will be) finite.”

Following the intuition outlined above, in [4] we have studied a domain, whose carrier is the set of all Boolean functions, for representing and propagating finiteness dependencies. We believe that coupling this new domain with H × P can greatly improve the precision of the analysis.

5 Conclusion

Several modern logic-based languages offer a computation domain based on rational trees. On the one hand, the use of such trees is encouraged by the possibility of using efficient and correct unification algorithms and by an increase in expressivity. On the other hand, these gains are countered by the extra problems rational trees bring with themselves and that can be summarized as follows: several built-ins, library predicates, program analysis and manipulation techniques are only well-defined for program fragments working with finite trees.

In this paper we propose an abstract-interpretation based solution to the problem of detecting program variables that can only be bound to finite terms. The rationale behind this is that applications exploiting rational trees tend to do so in a very controlled way. If the analysis we propose proves to be precise enough, then we will have a practical way of taking advantage of rational trees while minimizing the impact of their disadvantages.

References

1. R. Bagnara, R. Gori, P. M. Hill, and E. Zaffanella. Finite-tree analysis for constraint logic-based languages. Quaderno 251, Dipartimento di Matematica, Uni-

    versità di Parma, 2001. Available at http://www.cs.unipr.it/~bagnara/.

2. R. Bagnara, P. M. Hill, and E. Zaffanella. Efficient structural information analysis for real CLP languages. In M. Parigot and A. Voronkov, editors, Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning (LPAR 2000), volume 1955 of Lecture Notes in Computer Science, pages 189–206, Reunion Island, France, 2000. Springer-Verlag, Berlin.

3. R. Bagnara, P. M. Hill, and E. Zaffanella. Set-sharing is redundant for pair-sharing. Theoretical Computer Science, 2001. To appear.

4. R. Bagnara, E. Zaffanella, R. Gori, and P. M. Hill. Boolean functions for finite-tree dependencies. Quaderno 252, Dipartimento di Matematica, Università di Parma,

2001. Available at http://www.cs.unipr.it/~bagnara/.

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

6. M. Bruynooghe, M. Codish, and A. Mulkers. 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 1994.

7. J. A. Campbell, editor. Implementations of Prolog. Ellis Horwood/Halsted Press/Wiley, 1984.

8. B. Carpenter. The Logic of Typed Feature Structures with Applications to Unification-based Grammars, Logic Programming and Constraint Resolution, volume 32 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, New York, 1992.

9. M. Codish, D. Dams, and E. Yardeni. Derivation and safety of an abstract unification algorithm for groundness and aliasing analysis. In K. Furukawa, editor, Logic Programming: Proceedings of the Eighth International Conference on Logic Programming, MIT Press Series in Logic Programming, pages 79–93, Paris, France, 1991. The MIT Press.

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

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

12. A. Colmerauer. An introduction to Prolog-III. Communications of the ACM, 33(7):69–90, 1990.

13. A. Cortesi and G. Filé. Sharing is optimal. Journal of Logic Programming, 38(3):371–386, 1999.

14. A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combinations of abstract domains for logic programming: Open product and generic pattern construction. Science of Computer Programming, 38(1–3), 2000.

15. P. Cousot and R. Cousot. 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, pages 238–252, 1977.

16. P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511–547, 1992.

17. L. Crnogorac, A. D. Kelly, and H. Søndergaard. A comparison of three occur-check analysers. In R. Cousot and D. A. Schmidt, editors, Static Analysis: Proceedings of the 3rd International Symposium, volume 1145 of Lecture Notes in Computer Science, pages 159–173, Aachen, Germany, 1996. Springer-Verlag, Berlin.

18. P. R. Eggert and K. P. Chow. Logic programming, graphics and infinite terms. Technical Report UCSB DoCS TR 83-02, Department of Computer Science, University of California at Santa Barbara, 1983.

19. G. Erbach. ProFIT: Prolog with Features, Inheritance and Templates. In Proceedings of the 7th Conference of the European Chapter of the Association for Computational Linguistics, pages 180–187, Dublin, Ireland, 1995.

20. M. Filgueiras. A Prolog interpreter working with infinite terms. In Campbell [7], pages 250–258.

21. F. Giannesini and J. Cohen. Parser generation and grammar manipulation using Prolog’s infinite trees. Journal of Logic Programming, 3:253–265, 1984.

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

23. S. Haridi and D. Sahlin. Efficient implementation of unification of cyclic structures. In Campbell [7], pages 234–249.

24. P. M. Hill, R. Bagnara, and E. Zaffanella. Soundness, idempotence and commutativity of set-sharing. Theory and Practice of Logic Programming, 2001. To appear.

Available at http://arXiv.org/abs/cs.PL/0102030.

25. B. Intrigila and M. Venturini Zilli. A remark on infinite matching vs infinite unification. Journal of Symbolic Computation, 21(3):2289–2292, 1996.

26. D. Jacobs and A. Langen. Accurate and efficient approximation of variable aliasing in logic programs. In E. L. Lusk and R. A. Overbeek, editors, Logic Programming: Proceedings of the North American Conference, MIT Press Series in Logic Programming, pages 154–165, Cleveland, Ohio, USA, 1989. The MIT Press.

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

28. T. Keisu. Tree Constraints. PhD thesis, The Royal Institute of Technology, Stockholm, Sweden, May 1994.

29. A. King. Pair-sharing over rational trees. Journal of Logic Programming, 46(1– 2):139–155, 2000.

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

31. K. Mukai. Constraint Logic Programming and the Unification of Information. PhD thesis, Department of Computer Science, Faculty of Engineering, Tokio Institute of Technology, 1991.

32. C. Pollard and I. A. Sag. Head-Driven Phrase Structure Grammar. University of Chicago Press, Chicago, 1994.

33. F. Scozzari. Abstract domains for sharing analysis by optimal semantics. In J. Palsberg, editor, Static Analysis: 7th International Symposium, SAS 2000, volume 1824 of Lecture Notes in Computer Science, pages 397–412, Santa Barbara, CA, USA, 2000. Springer-Verlag, Berlin.

34. Gert Smolka and Ralf Treinen. Records for logic programming. Journal of Logic Programming, 18(3):229–258, 1994.

35. H. Søndergaard. An application of abstract interpretation of logic programs: Occur check reduction. In B. Robinet and R. Wilhelm, editors, Proceedings of the 1986 European Symposium on Programming, volume 213 of Lecture Notes in Computer Science, pages 327–338. Springer-Verlag, Berlin, 1986.

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