Solvable set/hyperset contexts: II. A goal-driven unification algorithm for the blended case

Agostino Dovier^{∗}  Eugenio G. Omodeo^{†}  Alberto Policriti^{‡}

August 13, 1998

Abstract A universe composed by rational ground terms is characterized, both constructively and axiomatically, where the interpreted construct with , which designates the operation of adjoining one element to a set, coexists with free Herbrand functors. Ordinary syntactic equivalence must be superseded by a bisimilarity relation ≈, between trees labeled over a signature, that suitably reflects the semantics of with . Membership (definable as “d ∈ t =_{Def} ( t with d) ≈ t”) meets the non-well-foundedness property characteristic of hyperset theory.

A goal-driven algorithm for solving the corresponding unification problem is provided, it is proved to be totally correct, and exploited to show that the problem itself is NP-complete. The results are then extended to the treatment of the operator less , designating the one-element removal operation.

Applications to the automaton matching and type-finding problems are illustrated. Keywords: Semantic unification, bisimulations, hypersets, set theory, NP-completeness.

Introduction

Graphs are widely used among basic data structures for representing both terms and sets (cf. [9, 1]). Such representation is particularly convenient and useful for algorithmic manipulations in fields like declarative programming, semantics of concurrency, and automated deduction. In view of applications in these and other fields, it is rather natural to assume the finiteness of graphs that are to represent terms or sets; however, it is often convenient not to impose the additional constraint of acyclicity. By resorting to cyclic representations one is in fact enabled, to a limited but significant extent, to treat infinite terms (cf. [23]) and non-well-founded sets (cf. [1]).

Well-established applications of the latter, today often called hypersets, regard the handling of automata, and the modeling of linguistic self-referential situations [7]. Supposedly, many more applications will be found in the modeling of shared information systems: web-like databases [22], query languages for semi-structured information [11], etc. Even though issues of computational complexity still set a limit to such applications, hypersets and the related notion of bisimulation offer the best conceptual framework for the treatment of circular phenomena.

In this paper we study rational terms (cf. [24]) and circular sets, combined into a very expressive and selfreferential abstract type. Instances of the latter type, called blended ( or hybrid) hypersets, are represented by graphs labeled over a signature. The signature is, of course, to comprise one or more symbols denoting operations over hypersets; it will also comprise free symbols, including at least one constant. The share of the signature needed to represent purely set-theoretic terms consists of the ∅ constant and the binary with operator whose semantics can be intuitively conveyed by the following identity:

∗Univ. di Verona, Dip. Scientifico-Tecnologico. Strada Le Grazie, 3, 37134-Verona (I). dovier@sci.univr.it

†Univ. di L’Aquila, Dip. di Matematica Pura ed Applicata. Via Vetoio Loc. Coppito, 67100-L’Aquila (I). omodeo@univaq.it

‡Univ. di Udine, Dip. di Matematica e Informatica. Via delle Scienze, 208. 33100-Udine (I). policrit@dimi.uniud.it

x with y = x ∪ {y} .

The very modest set-theoretic signature constituted by these two symbols alone, already suffices for the representation of the so-called hereditarily finite sets and hypersets.

The main focus of this paper is the design of a goal-driven unification algorithm for blended hypersets. After specifying such an algorithm, we show how to extend it into a more versatile set-constraint manager capable of dealing with negative information: to wit, we take into account the binary function symbol less whose intuitive semantics is conveyed by the identity

x less y = x \ {y} .

The unification algorithm to be presented has a rather traditional structure, à la Martelli-Montanari (cf. [25]): when applied to rational terms that do not involve the set-theoretic constructs, it in fact behaves very much like well-established algorithms, such as those proposed in [9, 26].

As already said, hypersets of the kind to be studied here result from a combination of entities from two domains. In order to precisely specify our unification problem, an axiomatization of the context under study is needed. We propose a theory of rational terms and hypersets, minimal in some sense, that can serve as a kernel for other, richer and accordingly more specialized, theories. In the context of such theories, our unification algorithm can still be exploited.

From the axiomatic part of our study, an interesting kinship emerges between the axiom that Maher introduced in [24] to guarantee completeness of the theory of infinite trees, and the axiom of bisimulation named AFA in [1]. Both axioms are adopted below, because our theory was aimed at achieving as much completeness as possible—though with least possible commitment.

It is worth emphasizing here that the theory to which our unification algorithm refers is not —nor would easily be— axiomatized in merely equational terms. The price we have to pay for this is that we cannot rely much on the vast literature on unification (cf., e.g., [5]), which is mainly focused with equational theories. To what extent and how our results can be recast in more conventional terms is a main issue left open by this paper. A promising approach for this is perhaps indicated by [19]; however, our current approach is closer to tableau-handling techniques than to rewriting techniques.

We also carry out a complexity analysis, leading to the conclusions that the proposed unification algorithm is in NP and that the unification problem under study is NP-complete. Various studies on the complexity of this problem, even restricted to sets (cf., among others, [21, 4, 32, 18]) show its intrinsic difficulty, so that proposals for more efficient set-unification algorithms are necessarily based on assumptions strongly limiting their field of application (cf. [31]).

The paper is organized as follows: after laying down in Section 1 an intuitive rationale for the hyperset notion, we characterize in Section 2 the universe of blended hypersets, both constructively and axiomatically. Section 3 presents hyperset unification as a very high-level paradigm to solve the deterministic finite-state automaton equivalence problem, along with a less classical, but nevertheless interesting, automaton matching problem. Section 4 is devoted to describing the blended hyperset unification algorithm, whose soundness, completeness, and termination are then proved, and whose complexity behavior is analyzed. In Section 5 it is shown how to extend the algorithm to deal with the negative information introduced by the removal operator less . Finally, we end with an application of blended hyperset unification to the type-finding problem, illustrated in Section 6: it turns out that while ordinary sets in type expressions suffice for the modeling of union data types, hypersets can play a role in the modeling of recursive types.

Although this article is a continuation of [28], it should be readable as a self-contained paper. There is, however, a dependency on a decision algorithm of [28] in the (rather marginal) Section 5.

1 Naive approach to hyperset theory, based on the analogy with terms

In this preliminary section, where we proceed in somewhat naive terms, we will contrast ordinary (nested) sets with entities of a much richer variety, to be called —after [6, 7]— hypersets. These are also known by the name non-well-founded sets in the thorough study [1]. Indeed, hypersets violate a principle widely agreed upon in the field of Set Theory since von Neumann introduced, in 1928, the regularity axiom: traditional membership is a well-founded relation over sets—the situation, with hypersets, is antithetic.

In parallel, we will contrast ordinary terms of first-order logic with terms of the generalized kind treated, e.g., in [23], Ch. 6. The latter have become familiar to researchers in the field of Logic Programming by the name of infinite terms. We will recognize a tight analogy between terms and sets: to state it simply,

sets are to hypersets as ordinary terms are to infinite terms.

In view of this parallel, the unified (or “blended”, or “hybrid”) data structure to be investigated in this paper, encompassing both hypersets and generalized terms, will come out quite naturally.

After characterizing the domain of blended hypersets, \overline{I H I}_{Σ} (where Σ is a signature—see below), we will tackle the problem of solving systems of equations over \overline{I H I}_{Σ}. In order to study this problem in greater generality, a convenient starting point is to consider particularly heavily constrained systems

\{ \begin{matrix}X_{0} & = & \{ X_{01}, …, X_{0m_{0}} \} \\ X_{1} & = & \{ X_{11}, …, X_{1m_{1}} \} \\ ⋮ & ⋮ & ⋮ \\ X_{n} & = & \{ X_{n1}, …, X_{nm_{n}} \} \end{matrix}

of set equations. In this initial stage, we are assuming that the left-hand sides, namely X_{0}, …, X_{n}, are distinct from one another (even though some of the sets they represent might coincide); moreover, each one of the X_{ij}s in a right-hand side must be the same as one of the symbols X_{h} on the left. As for n and the m_{i}s, they simply are non-negative integers: n, m_{0}, …, m_{n} ∈ IN, as infinite sets are beyond the scope of this paper.

By traditional methods, a system of this form admits a solution if and only if there is an ordering X_{π_{0}}, …, X_{π_{n}} of the X_{h}s such that any X_{π_{h}j} occurring in the right-hand side of the π_{h}-th equation is one of X_{π_{h+1}}, …, X_{π_{n}}, for h = 0, 1, …, n.^{1} Moreover, when this non-circularity condition holds, uniqueness of the solution ensues from extensionality (which is the postulate stating that two sets are equal if and only if they have the same members) and from the bi-implications ∀ z ( z ∈ { v_{1}, …, v_{k}} ↔ ⋁_{j=1}^{k} z = v_{j} ), one for each k ≥ 0, that summarize the semantics of the construct { , …, }.

To move from ordinary sets to hypersets, we are to postulate that any system of the above form, whether circular or not, admits a solution, and that such a solution is always unique.

1A proof of this fact goes as follows. If a solution X_{0} = ξ_{0}, …, X_{n} = ξ_{n} exists, the X_{h}s can be ordered so that the ranks of the corresponding ξ_{h}s do not increase: this ordering will meet the desired property. Conversely, if a permutation π with the stated property exists, then m_{π_{n}} = 0 and, accordingly, X_{π_{n}} = ∅; moreover, the value of X_{π_{h}} can be determined from those of X_{π_{h+1}}, …, X_{π_{n}}, for all h < n.

For example, both the equation X = { X } and the system

X_{0} = { X_{4}, X_{3} }
X_{1} = { X_{2}, X_{3} }
X_{2} = { X_{3} }
X_{3} = { X_{1} }
X_{4} = { }

have solutions. Indicating by Ω the hyperset such that Ω = { Ω }, we readily recognize that X_{1} = X_{2} = X_{3} = Ω, X_{4} = ∅, X_{0} = { ∅, Ω } is a solution to the system. This solution hence must be the only one—otherwise stated, one can infer X_{1} = X_{2} and X_{1} = X_{3} from the equalities X_{1} = { X_{2}, X_{3} }, X_{2} = { X_{3} }, X_{3} = { X_{1} }, by virtue of the new postulate, stronger than extensionality. Of course ∅ ≠ Ω and Ω ≠ { ∅, Ω }, because ∀ z (z ∉ ∅), ∀ z (z ∈ Ω ↔ z = Ω), and ∀ z (z ∈ { ∅, Ω } ↔ (z = ∅ ∨ z = Ω)) all three hold, and therefore ∅ has no members, Ω has exactly one, and { ∅, Ω } has two.

Let us now switch to the realm of terms by considering a ‘flat’ system

\{ \begin{matrix}X_{0} & = & f_{0}( X_{01}, …, X_{0m_{0}} ) \\ ⋮ & ⋮ & ⋮ \\ X_{n} & = & f_{n}( X_{n1}, …, X_{nm_{n}} ) , \end{matrix}

analogous to the one above, where f_{0}, …, f_{n} belong to a signature Σ. This means that Σ is a collection of symbols, and that every symbol s ∈ Σ has an associated degree (or “arity”) ar(s) ∈ IN, stating the legal number m of arguments of s in any well-formed expression of the form s(t_{1}, …, t_{m}). In particular, a system like the one above would be ill-formed unless m_{i} = ar(f_{i}) held for i = 0, …, n. This is the only new requirement: just as before, X_{0}, …, X_{n} must be distinct variables from whose collection each X_{ij} is drawn. Variables are now assumed to range over the domain G I_{Σ} commonly known as the Herbrand universe generated by Σ. This domain consists of all ground terms over the signature: accordingly, to solve the system one must substitute every X_{h} by a ground term γ_{h} so that every equality gets transformed into a syntactic identity.

The same non-circularity condition discussed earlier in connection with the solvability of a system by ordinary sets, is a necessary and sufficient condition for the solvability, over G I_{Σ}, of the new system. As before, the solution X_{i} ↦ γ_{i}, if one exists, is obviously unique.

One way to move from ordinary terms to infinite terms, is by postulating that every system of the above form —even one with infinitely many equations— admits a solution, and that the solution is unique. In circular cases —or when n is infinite— i.e., when the system contains equations X_{i_{0}} = f_{i_{0}}(…, X_{i_{1}}, …), X_{i_{1}} = f_{i_{1}}(…, X_{i_{2}}, …), … that form an infinite chain, some of the γ_{i}s, instead of being drawn from G I_{Σ}, will be drawn from a larger domain \overline{\overline{G} I}_{Σ}, known as the completion of the Herbrand universe over Σ (cf. [23]). If we allowed the number n + 1 of equations to range from one to infinity, then the whole of \overline{\overline{G} I}_{Σ} would be spanned by the solutions to flat systems over Σ; but since we will limit our consideration to finite systems, our γ_{i}s will come from a domain \overline{G I}_{Σ} intermediate between G I_{Σ} and \overline{\overline{G} I}_{Σ}. The terms in \overline{G I}_{Σ} are usually said to be rational, and various methods exist for specifying them (grammars and tree automata [16, 10], axioms [24], etc.).

In order to combine sets with ordinary terms and hypersets with infinite terms, the first step will be to assume that Σ comprises two symbols, ∅ and with , of respective degrees 0 and 2. By with , used as a left-associative infix operator, we intend to designate the operation of inserting an element into a set—or, more generally, into a hyperset. An expression of the form { w_{1}, …, w_{k} } will be regarded, accordingly, as an abridged notation for ∅ with w_{k} with⋯with w_{1}; more generally,

\{ w_{1}, …, w_{k} | z \} =_{Def}  \underbrace{(⋯ (}_{k} z with w_{k}) with⋯with w_{1} )
{ w_{1}, …, w_{k} } =_{Def} { w_{1}, …, w_{k} | ∅ }

Any ground term whose outermost functor differs from with will be regarded as a memberless entity, named a color. Either ∅ (our name for the ‘official’ empty set) is the sole color, which happens only when Σ = {∅, with}, or there are also other colors; these are the two cases called pure and blended, respectively. Quite unconventionally, we will allow insertions like C with X for any color C distinct from ∅, regarding any hyperset that results from an insertion of this kind as something distinct from ∅ with X.

Unlike other functors, which merely play the role of syntactic constructors, with has an intended meaning; hence we can no longer insist that every flat system has a unique solution. For example, the equation X_{0} = { ∅ | X_{0} } (which means X_{0} = X_{0} ∪ {∅}) is satisfied by any set to which ∅ belongs, and hence has the infinitely many solutions

X_{0} = \{ ∅, \underbrace{\{⋯ \{}_{k} ∅ \} ⋯\}\} , k = 0, 1, 2, …

—and many more. As will emerge from the next section, to circumvent the new difficulty it suffices to restrict one’s consideration to systems

⋀_{h=0}^{n} X_{h} = f_{i}(X_{h1}, …, X_{h,ar(f_{i})}) ,

as above, whence one cannot extract an infinite chain

X_{h_{0}} = { | X_{h_{1}} } , X_{h_{1}} = { | X_{h_{2}} } , X_{h_{2}} = { | X_{h_{3}} } , …

of equations (clearly with repetitions). In a theory of blended hypersets, one will postulate that every system of equations subject to this restriction admits one and only one solution. In a theory of blended sets, the existence (and uniqueness) of a solution will presuppose non-circularity, as usual.

We have been approaching the notion of hyperset in terms of single-solution systems of equations. We now address the question: what is an hyperset, precisely? A reasonable way of answering would be to circumscribe, from among single-solution systems of equations, ‘canonical’ systems of a suitable kind. In each system, the left-hand side X_{0} of the first equation could be taken as the variable of interest. Roughly, a system should be regarded as canonical when every equation in it irredundantly contributes to the determination of the value ξ of the variable of interest. One could identify tout court the canonical system with the hyperset ξ.

Irredundancy presupposes, among others, injectivity: that is, the values of distinct variables should be different. But how can one ascertain that this requirement is fulfilled? An answer is contained in the constructive notion of bisimulation in the next section. From now on, to clarify the presentation, singlesolution systems will be represented by graphs labeled over Σ, while their variables will be represented by nodes of such graphs.

2 Characterization of blended hypersets

In this section the notion of blended hyperset will be defined precisely, both constructively (in Section 2.1) and axiomatically (in Section 2.2).

2.1 Intended hyperset model

The entities that form a Herbrand universe are sometimes characterized as being finite trees coherently labeled over a signature Σ. It is easy to adjust this abstract view of ground terms to the terms that form the completion of a Herbrand universe: to do this, it will suffice to withdraw the requirement that labeled trees must have finitely many nodes. From this graph-theoretical perspective, syntactic equivalence between terms turns out to coincide with the notion of isomorphism between labeled, ordered trees.

Given a term T , one can ‘fold’ it by fusing two nodes ν, μ of T into a single node whenever the subterms rooted at ν, μ are equivalent to each other. This will yield an ordered multi-graph P, both rooted and directed, retaining information of all essential features of T : the picture of T , as we call it. If there are no infinite paths in P, this indicates that the original T was already finite: this is the case of an ordinary term. When P is finite, T (which might be infinite) is said to be a rational term.

If one restricts one’s own attention to rational terms and represents them suitably (e.g., by their pictures), then, at least assuming the signature Σ to be finite, even infinite terms can be algorithmically construed and manipulated.

In the case under study, the construction of the universe is not entirely free. We are assuming, in fact, that Σ comprises a symbol, namely with , to which a special, fixed meaning is attributed (cf. Section 1). The intuitive semantics of this construct must reflect into the criteria we adopt for equivalencing labeled trees. Such criteria cease accordingly, in our specialized context, to be purely syntactic. At an even more fundamental level, we will have to discard certain trees labeled over Σ, that cannot be regarded as ground terms due to the semantics of with .

To proceed more formally, let us start by recalling a classical definition (cf. [23]), which still awaits a minor adaptation to our aims:

Definition 1 A ground term (over Σ) is a mapping T : dom(T ) ⟶ Σ such that

• the domain dom(T ) of T is a non-empty ordered tree whose root is [ ];

• for all ν in dom(T ), ar(T (ν)) = | { i : [ν, i] in dom(T ) } | , where [ν, i] stands for the i-th son of ν.^{2}

□

To avoid under-specified situations, we then add:

Groundness restriction. The requirement henceforth becomes integral part of the definition of (ground) term that there be no infinite sequence ν_{0}, ν_{1}, ν_{2}, … of nodes with T (ν_{i}) = with and ν_{i+1} = [ν_{i}, 1] for all i.

□

To see why the presence of a path ν_{0}, ν_{1}, ν_{2}, … as above, in a term, would conflict with the very notion of groundness, let us examine the two graphs of Fig. 1. Either of them is the picture of a labeled tree that violates the groundness restriction. The left arc in either graph indicates —if anything— self-inclusion; hence

2We follow [23] in identifying [ [ a_{1}, …, a_{n}], a_{n+1} ] with [ a_{1}, …, a_{n}, a_{n+1} ], to keep the notation simple.

[figure: (a); •; with; •; ∅; X_{a} = { ∅ | X_{a} }; (b); •; with; X_{b} = { X_{b} | X_{b} }]

Figure 1: The terms depicted by these graphs cannot be regarded as ground.

it conveys no information about the entity (X_{a} and X_{b} respectively) represented by the root. The second arc of Fig. 1(a) indicates that ∅ must belong to X_{a}, a property which is clearly insufficient to characterize X_{a}. The right arc of Fig. 1(b) indicates that X_{b} must belong to itself. If X_{b} were to be an ordinary set, this would be an absurdity, but we are dealing with hypersets here. Since membership can form cycles among such entities, we are again facing an under-specified situation.

Our next step will be to get rid of irrational terms (an example of set-theoretic irrational term is the one whose picture is the graph of Fig. 2). Preliminary to that, we need the notion of bisimulation, which in turn presupposes the following couple of auxiliary notions.

For every term T and any ν in dom(T ), let τ_{0}, …, τ_{g} and μ_{0}, …, μ_{g−1} be the sequences of nodes such that: τ_{0} = ν; T (τ_{i}) = with, τ_{i+1} = [τ_{i}, 1] and μ_{i} = [τ_{i}, 2] for i = 0, …, g − 1; T (τ_{g}) ≠ with. We denote by Color(ν) the node τ_{g} and say that the μ_{i}s are the ∈-predecessors of ν.

Definition 2 Let T_{0}, T_{1} be terms. A relation B ⊆ dom(T_{0}) × dom(T_{1}) is said to be a bisimulation between T_{0} and T_{1} iff: i) [ ] B [ ] , ii) when ν_{0} B ν_{1}, the following hold:

• Color_{0}(ν_{0}) B Color_{1}(ν_{1}), T_{0}(ν_{0}) = T_{1}(ν_{1}), and moreover

• to every ∈-predecessor ϱ_{b} of ν_{b} in T_{b} ( b = 0 or b = 1), there corresponds at least one ∈-predecessor ϱ_{1−b} of ν_{1−b} in T_{1−b} such that ϱ_{0} B ϱ_{1};

• if T_{0}(ν_{0}) ≠ with, then [ν_{0}, i] B [ν_{1}, i] for i = 1, …, ar(T_{0}(ν_{0})).

We write T_{0} ≈ T_{1} iff there is a bisimulation B between T_{0} and T_{1}. □

Bisimulations are, in a sense, isomorphisms complying with the intended (hyperset) semantics of with. Accordingly, T will be regarded as a rational term iff it has only finitely many subterms that cannot bisimulate one another. To make this idea precise, let us denote by T ⌈ν the subterm of T issuing from a given node ν.

Definition 3 A ground term T is said to be rational iff there are ν_{0}, …, ν_{n} in dom(T ) such that for every μ in dom(T ) there is an i, 0 ≤ i ≤ n, fulfilling T ⌈ν_{i} ≈ T ⌈μ. □

In conclusion, indicating by \overline{G I}_{Σ} , G I_{Σ} the family of all rational ground terms over Σ and its subfamily consisting of the terms that have finitely many nodes, our hyperset universe and set universe will be

\overline{I H I}_{Σ} =_{Def} \overline{G I}_{Σ}/ ≈ , IHI_{Σ} =_{Def} G I_{Σ}/ ≈

respectively. Representing by T^{≈} the ≈-class of T , the element insertion operation and membership relation over these universes can be straightforwardly defined as

T_{0}^{≈} with_{Σ} T_{1}^{≈} =_{Def} W^{≈} , T_{1}^{≈} ∈_{Σ} T_{0}^{≈} iff_{Def} W ≈ T_{0} ,

∘

•  •  •  • …

•  •  •  • …

X_{0} X_{1} X_{2} X_{3}

U_{0}

U_{1} U_{2} U_{3} U_{4} [figure] [figure] [figure] [figure]

\underline{\underline{Legenda:}}

\begin{matrix}T (•) = with \\ T (∘) = ∅ \end{matrix}

X_{i} = { X_{i+1} , U_{i} }

U_{0} = ∅

U_{i+1} = { U_{i} } ( i = 0, 1, 2, …)

Figure 2: This graph is the picture of an irrational term T representing a cycle-free hyperset X_{0}. Notice that X_{0}, as well as every element in its transitive closure, is finite.

X_{1} = k(g(X_{3}))
X_{2} = k(k(X_{3}))
X_{3} = h(h(g(X_{3})))

• •

• •

• • [figure]

X_{1} ⇀ k k ↼ X_{2}
X_{4} ⇀ g k ↼ X_{5}
X_{6} ⇀ h h ↼ X_{3}

X_{1} = k(X_{4}) X_{2} = k(X_{5})
X_{3} = h(X_{6}) X_{4} = g(X_{3})
X_{5} = k(X_{3}) X_{6} = h(X_{4})

Figure 3: Two renderings (the one on the right ‘flat’) of the same ground labeled graph.

where W is a tree whose root, labeled with, has left and right subtree isomorphic to T_{0}, T_{1} respectively.

Every symbol f other than with in Σ is interpreted à la Herbrand, that is to say, as the operation sending each m-tuple T_{1}^{≈}, …, T_{m}^{≈} with m = ar(f) into T^{≈}, where T ([]) = f and T ⌈[i] ≈ T_{i}, for i = 1, …, m.

As was done in [28] with reference to the pure case only, we could provide criteria for choosing a canonical representative out of each ≈-class: representatives could then be taken as hypersets proper.

Let us now generalize our discussion by adjoining to our former signature Σ a denumerably infinite collection V of new symbols of degree 0, named variables. Labeled graphs, and in particular terms, whose labeling may involve variables, or that may violate the above-stated groundness restriction, will be said to be hollow. As will emerge from Section 4, every hollow, rooted and finite graph depicts a collection of ground terms, obtainable from it via substitutions.

As illustrated by Fig. 2 and Fig. 3, any ground labeled graph G (possibly with cycles) can be variously rendered, up to isomorphism, as a conjunction (consisting of a single element when G is finite and acyclic; infinite when G is not rational) of first-order equalities ⋀_{ν in C} (X_{ν} = t_{ν}) over the signature Σ ∪ V, where

• C is a collection of nodes of G comprising all nodes of G devoid of entering arcs, along with at least one node lying on ϖ for each infinite path ϖ of G;

• the X_{ν}s belong to V, hence they are not used as labels in G, and they are distinct from one another; the t_{ν}s are first-order terms^{3} over the signature Σ ∪ {X_{ν} : ν in C}.

To do that, one views G as a collection { G_{ν} : ν in C } of finite acyclic rooted graphs labeled over Σ ∪ { X_{ν} : ν in C }, each ν in C bearing the label X_{ν} and each G_{ν} being in a sense ‘grafted’ into ν; then one takes as t_{ν} the first-order term that straightforwardly corresponds to G_{ν}.^{4}

3Notice the distinction we are making between first-order (concrete) terms and terms in the graph-theoretical sense.

4When G is rooted, finite and acyclic, so that its rendering is X = t, X not occurring in t, t itself is called rendering of G.

Viewed this way, a rational ground labeled graph G is just a special case of what is usually called a Herbrand system:

Definition 4 A Herbrand system is a finite collection {ℓ_{1} = r_{1}, …, ℓ_{n} = r_{n}} of first-order equalities,^{5} where ℓ_{1}, r_{1}, …, ℓ_{n}, r_{n} are terms over the signature Σ ∪ V. A Herbrand system E is said to be flat if every equality e in E has either the form X = Y, or the form X = g(Y_{1}, …, Y_{n}) with g in Σ. □

Solving general systems of this kind over hypersets is the main unification task coped with in this paper, that we will tackle in Section 4.

2.2 Axiomatic view of the blended hyperset universe

To state our axioms about hypersets, we will use a first-order language comprising the constant ∅, infix operators with and less , the (infix) predicates = and ∈, and a number of functors to which we will resort in order to express most of our axioms without using existential quantifiers. We often use {w_{1}, …, w_{k} | z} and {w_{1}, …, w_{k}} to shorten notation, as explained in Section 1.

It goes without saying that = meets the usual properties of equality (see, e.g., [27]), which we collectively denote by the label (=).

The symbols x, y, z, u, v, x_{i}, x_{i}^{b}, y_{i} will stand for distinct variables implicitly universally quantified in front of each axiom.

We begin with (a suitable adaptation of) the extensionality axiom, according to which any two entities that have the same color and the same elements are equal. Formally

(E) ( ∀z (z ∈ x ↔ z ∈ y) ∧ color of(x) = color of(y) ) ⟶ x = y .

Then we have axioms concerning the empty entities named colors (in particular the null set ∅) and the element adjunction and element removal operations, with and less .

(N_{0 ,1} ) v ∉ color of(u)  color of(∅) = ∅
(W_{0 ,1} ) v ∈ { y | u } ↔ (v ∈ u ∨ v = y) color of({ y | u }) = color of(u)
(L_{0 ,1} ) v ∈ u less y ↔ (v ∈ u ∧ v ≠ y) color of(u less y) = color of(u)

The anti-diagonal and self-loop axioms below ensure, for example, that for any color y and any tuple v_{1}, …, v_{m} of hypersets, the system

x ∉ v_{1} ∧ ⋯ ∧ x ∉ v_{m} ∧ x ∉ x ∧ color of( x) = y

of constraints, as well as the equation

x = {x, v_{1}, …, v_{m} | y}

can be satisfied (one independently of the other).^{6}

5Depending on the context, a Herbrand system E may be seen at times as a set/system of equations, at times as a conjunction of equality atoms.

6The role and importance of these two axioms first emerged from [29] (cf. also [28]).

(D_{∉}) ( x = anti diagonal( u , y) ∧ ( v ∈ u ∨ v = x) ) ⟶

                          ( color of( x) = color of( y) ∧ x ∉ v)

(D_{∈}) x = self loop( u , y) ⟶

( color of( x) = color of( y) ∧ ( v ∈ x ↔ ( v ∈ u ∨ v = x) ) )

We are arriving at the axioms essentially expressing our own weak version of Aczel’s anti-foundation axiom AFA (see [1]). We name such axioms anti-regularity, (R̸), and hyper-extensionality, (H). To introduce these two schemes in informal terms close to the contents of Section 1, let us consider a system

⋀_{j=0}^{n} x_{j} ≡ {x_{j1}, …, x_{jm_{j}}} ,

where n ≥ 0, m_{j} ≥ 0 for all j, x_{0}, …, x_{n} are distinct variables, each x_{ij} is one of x_{0}, …, x_{n}, and the j-th ‘congruence’ of the system is a short for ∀ z ( z ∈ x_{j} ↔ ⋁_{k=1}^{m_{j}} z = x_{jk}). Anti-regularity states that each such system admits a solution with pre-assigned colors for the x_{j}s. Hyper-extensionality states that the solution is uniquely determined by the colors, even if we consider a more general system of congruences

⋀_{j=0}^{n} x_{j} ≡ {x_{j1}, …, x_{jm_{j}} | z_{j}} ,

where z is a fixed ‘residue’ (in the preceding system, z_{j} = ∅ for all j).

In the formal specification below, we employ distinct auxiliary variables x_{0}^{0}, …, x_{n}^{0}, x_{0}^{1}, …, x_{n}^{1}, and indicate by x_{j1}^{b}, …, x_{jm_{j}}^{b} the variables x_{h}^{b} such that x_{h} occurs inside the right-hand side of the j-th congruence.

(R̸) ∃ x_{0} ⋯ ∃ x_{n} ⋀_{j=0}^{n} ( color of( x_{j} ) = color of( y_{j} ) ∧
∀ z ( z ∈ x_{j} ↔ ⋁_{k=1}^{m_{j}} z = x_{jk}))
(H) ( ⋀_{j=0}^{n} ( color of( x_{j}^{0} ) = color of( x_{j}^{1} ) ∧
( ⋀_{b=0}^{1} ⋀_{i=0}^{n} ( x_{i}^{b} ∈ x_{j}^{b} ↔ ⋁_{k=1}^{m_{j}} x_{i}^{b} = x_{jk}^{b}) ) ∧
∀ z ( ( z ∈ x_{j}^{0} ∧ ⋀_{i=0}^{n} z ≠ x_{i}^{0} ) ↔ ( z ∈ x_{j}^{1} ∧ ⋀_{i=0}^{n} z ≠ x_{i}^{1} ) )))
⟶ ⋀_{j=0}^{n} x_{j}^{0} = x_{j}^{1}

Let us incidentally observe that (R̸) is a sort of weak form of Aczel’s AFA_{1}, while (H) corresponds to AFA_{2}. Notice also that the adoption of (H) makes the extensionality axiom (E) redundant (cf. [29, 28]).

The following five axioms are Clark’s freeness assumptions (cf. [8]), an adaptation of Reiter’s weak domain closure assumption (cf. [30]), and a statement, antithetic to the occurs-check scheme (cf. [8, 30]), which generalizes (R̸).

Here we assume that our signature Σ contains solely ∅, with and the free functors mentioned in previous sections. In particular less, color of, and any other functor introduced to state the axioms in this section, are not in Σ. We are to assume that f, g, and all f_{ν}s appearing below, belong to Σ; also, g is to be distinct from both with and f. Finally, let A = max{ ar(h) : h in Σ , h ≠ with }.

Axiom (U_{0} ) will only be included when Σ has finite cardinality. Every instance of (¬OC) results from a finite ground graph G labeled over Σ, where it is not restrictive to assume that G is cyclic. The variables x_{ν_{0}}, …, x_{ν_{ℓ}} are in one-to-one correspondence with the nodes ν_{0}, …, ν_{ℓ} of G; we are indicating by f_{ν} the label of the node ν, by n_{ν} the degree of f_{ν}, and by μ_{j}^{ν} the j-th son of ν. The uniqueness requirement was introduced by Maher in [24] in order to achieve completeness of his theory of infinite trees: this makes it very similar to AFA. Such kinship will be exploited in a continuation of this paper to carry out a reduction of the blended hyperset unification problem to the pure hyperset unification problem (cf. [13]).

(F_{0} )  f( x_{1} , …, x_{n}) ≠ g( y_{1} , …, y_{m})
(F_{1} )  g( x_{1} , …, x_{n}) = g( y_{1} , …, y_{n}) ⟶ ( x_{1} = y_{1} ∧ ⋯ ∧ x_{n} = y_{n})
(U_{0} )  x = color of( u) ⟶ ∃ x_{1} ⋯ ∃ x_{A} ⋁_{h in Σ\{ with }} x = h(x_{1}, …, x_{ar(h)})
(U_{1} )  color of( f( x_{1} , …, x_{n}) ) = f( x_{1} , …, x_{n})
(¬OC) ∃! x_{ν_{0}} ⋯ x_{ν_{ℓ}} ⋀_{ν node of G} x_{ν} = f_{ν}(x_{μ_{1}^{ν}}, …, x_{μ_{nν}^{ν}})

Remarks 1

1. To obtain from the preceding theory of hypersets a corresponding theory of sets, we should drop (D_{∈}), (R̸) and (¬OC), adopting a classical regularity axiom and a suitable version of the occurs-check scheme of axioms (cf. [14]).

2. It is immediate to see that (U_{1} ) generalizes (N_{1} ); also, it is plain to deduce (N_{0} ) from the remaining axioms, including (U_{0} ). Hence one shall not list (N_{0 ,1} ) among the axioms when Σ is finite. □

3 Expressiveness of equation systems over hypersets: an example

One of the most common exploitations of hypersets is as a means to model deterministic finite-state automata. As we will now see, the notions introduced so far provide a well-suited framework for conceiving automaton manipulation algorithms based on this kind of modeling. Another, rather distant, application of hypersets will be considered in Section 6.

A deterministic finite automaton (DFA for short) consists of a set Q = {q_{0}, …, q_{N}} of states, an alphabet S = {s_{1}, …, s_{M}} (with 0 < M < ∞), a partial transition function d : Q × S ⟶ Q. Moreover, one of the states —say q_{0}— is singled out as the initial state, and there is a set F ⊆ Q of accepting states (for a full explanation of DFAs see, for instance, [2, 12]).

Given a DFA A as just said, one can construct a corresponding Herbrand system E_{A} involving as many unknowns and equations as A has states, in the signature Σ = {with, ∅, false, true} ∪ S where all symbols save with have degree 0. E_{A} consists of the equations (one for each i = 0, …, N)

X_{i} = {f_{i}} ∪ ⋃_{h=1}^{M}δ_{ih}

where

f_{i} is the truth value of q_{i} ∈ F ,
δ_{ih} = ∅ if d(q_{i}, s_{h}) is undefined ,
δ_{ih} = {{ s_{h}, X_{j} }} if d(q_{i}, s_{h}) = q_{j} .

Even though E_{A} is not written in flattened form, it should be clear from the discussion in Section 1 —echoed by the axioms (R̸) and (H) in Section 2.2— that E_{A} has a unique solution over hypersets: we can take the hyperset value of X_{0} in this solution as a representation, more essential than the automaton itself, of the regular language L(A) accepted by A.

This is essentially the same technique for translating finite automata into hypersets provided in [7], where it is shown that graph bisimilarity (cf. our Def. 2 of ≈) faithfully reflects equivalence between deterministic automata.

To illustrate how one can test whether or not L(A) = L(B), for given DFAs A and B, let us consider the following automata with alphabet {a, b}:

[figure: q_{0}; q_{1}; q_{2}; q_{0}; q_{1}; a; a; b; a; b; a; a; b; DFA A; DFA B]

Here, the sets of accepting states are F_{A} = {q_{1}, q_{2}} and F_{B} = {q_{1}}, respectively.

In our framework, these automata can be modeled by the systems:

E_{A} = { X_{0} = {false, {a, X_{1}}},
X_{1} = {true, {a, X_{2}}, {b, X_{1}}},
X_{2} = {true, {a, X_{2}}, {b, X_{1}}} } ,
E_{B} = { X′_{0} = {false, {a, X′_{1}}},
X′_{1} = {true, {a, X′_{1}}, {b, X′_{1}}} } .

Both of these admit a solution, but it is not obvious that the system E_{A} ∪ E_{B} ∪ { X_{0} = X′_{0} } resulting from their combination has a solution as well: the latter system contains in fact a pair of equations sharing the same left-hand side, X_{0}.

We are facing an instance of the blended hyperset unification problem to be discussed in full generality later on. In the case at hand, the answer to the problem will be affirmative, because we can directly check on the automata that T_{A} ≈ T_{B} under a bisimulation B, where T_{A} and T_{B} are the values yielded for X_{0} and X′_{0} by E_{A} and E_{B}.

The problem of testing the equivalence of two deterministic automata is NL-complete (cf. [20]) and can be solved by very fast algorithms (cf. [2, 17]). However, it would be wrong to expect from this deceptively simple example that hyperset unification could be performed by suitably adapted versions of those algorithms. Via a reduction to hyperset unification, we can solve the more general problem of establishing whether a partially defined DFA can be completed into a given deterministic automaton, a problem that we will show to be NP-complete.

As an example of this kind of one-way matching, let us consider the problem of establishing whether the following partially defined automaton C,^{7}

[figure: q_{0}; q_{1}; Q; a; H; K; b]

7Note that a priori this automaton could even be non-deterministic.

where H, K, and Q are unknown, can be instantiated so as it accepts the same language as the previously seen DFA A. In other words, we are to solve the system E_{A} ∪ E_{C} ∪ {X_{0} = Q_{0}}, where E_{C} reads:

Q_{0} = {false, {a, Q_{1}}},
Q_{1} = {true, {b, Q_{1}}, {H, Q_{2}}},
Q_{2} = {F_{2}, {K, Q_{1}}},
{F_{2} | } = {false, true},
{H, K | } = {a, b} .

Two solutions indeed exist: one of them yields Q_{0} = X_{0}, Q_{1} = Q_{2} = X_{1}, H = a, K = b.

4 Hyperset unification

The following notation is used below. Capital letters X, Y, Z, etc. represent variables; f, g, etc. stand for functional symbols (i.e. elements of Σ); ≡ denotes the syntactic identity relation between first-order terms over Σ ∪ V; φ_{Y}^{X} denotes the result of replacing every occurrence of the variable X by Y in a quantifier-free first-order expression φ, and vars(φ) denotes the set of all variables occurring in φ; dom(λ) and ran(λ) denote the set of first, respectively second, components of a binary relation λ. Hereafter we only need to consider substitutions of the following kind:

Definition 5 A (ground) substitution is a mapping γ from a finite subset of V to the universe \overline{G I}_{Σ}. □

4.1 The unification problem

One can apply a substitution γ to a hollow graph G, thereby obtaining a ground G^{γ}, when dom(γ) ⊇ V ∩ ran(G): to do that, one will graft an isomorphic copy of γ(X) in place of each node ν labeled G(ν) = X, for all X in dom(γ). After observing that every first-order term t is the concrete rendering of an acyclic rooted graph G_{t} labeled over Σ ∪ V (see ending remarks of Section 2.1), one realizes that the notation t^{γ} makes sense too, provided dom(γ) ⊇ vars(t). Thus we are ready to define:

Definition 6 A solution to a Herbrand system E is a substitution γ that solves all equations in E at once. That is, for all ℓ = r in E, both dom(γ) ⊇ vars(ℓ) ∪ vars(r) and ℓ^{γ} ≈ r^{γ} hold. □

There are systems of equations of special forms for which a solution can be determined quite easily.

Definition 7 A Herbrand system E is said to be in solvable form if each equation in it has one of the forms:

• X = Y, with Y distinct from X and X not occurring elsewhere in E;

• X = f(Y_{1}, …, Y_{n}), or in particular X = { Y_{2} | Y_{1}}, with X not occurring as left-hand side of any other equation in E.

A Herbrand system in solvable form is said to be explicit if it contains no subsystem of the following zipper form:

X_{0} = {Y_{0}|X_{1}}, …, X_{m−1} = {Y_{m−1}|X_{m}}, X_{m} = {Y_{m}|X_{0}}

(for m = 0 this reduces to the single equation X_{0} = {Y_{0}|X_{0}}). □

To justify this nomenclature, let us see how readily a solution to a system in solvable form can be found when the system is explicit. One can proceed to enlarge the system with all equations Y = ∅, where each Y is a variable that, although occurring in the system, does not occur as left-hand side of any of its equations. The ground image γ(X) of each variable X in a solution γ, can thus be read directly off the system. (Trivially, the solution to the enlarged system is unique up to ≈; however the original system could have had many other solutions.)

More generally, a system in solvable form can be modified until it becomes explicit. Every modification step will introduce new variables; however each solution to the modified system can be restricted to the old variables giving a solution to the previous system. Thus, at the end, any solution to the explicit system will also be a solution to the original system. To see this, note that γ(X_{0}) ≈ γ(X_{1}) ≈ ⋯ ≈ γ(X_{m}) must hold in any solution γ, when there is a zipper X_{0} = {Y_{0}|X_{1} }, …, X_{m−1} = {Y_{m−1}|X_{m}}, X_{m} = {Y_{m}|X_{0}}. Therefore, as long as a there is a subsystem of this kind, we can replace it by the equations

K_{1} = {Y_{0}|K_{0}}, …, K_{m} = {Y_{m−1}|K_{m−1}}, X_{0} = {Y_{m}|K_{m}}, …, X_{m} = {Y_{m}|K_{m}} ,

where K_{0}, …, K_{m} are new variables. While the system resulting from this modification is still in solvable form, it is closer to explicit form, because the number of zippers has been reduced.

We are now ready to state the unification problem in very specific terms. Systems in solvable form can, for that sake, be employed as templates of the solutions to a given system:

Definition 8 Given a Herbrand system E, solving E amounts to producing a finite set of Herbrand systems in solvable form E_{1}, …, E_{m}, such that

• for every solution γ to E, at least one of the E_{i}s has a solution σ such that γ(X) = σ(X) for all X in vars(E)∩ vars(E_{i});

• for any solution σ to any of the E_{i}s, every substitution γ such that dom(γ) ⊇ vars(E) and γ(X) = σ(X) for all X in vars(E) ∩ dom(σ), is a solution to E. □

Each system in solvable form covers a family of solutions. The intuitive meaning of the definition above, apart from the technical requirement concerning variables, is the following: the set {E_{1}, …, E_{m}} solves E if any solution to E is also a solution for at least one of the E_{i}s; moreover, every solution to any E_{i} is also a solution to E. Notice that we are not requiring that the various E_{i}s be independent: this means that there can be solutions to E that are solutions to more than one of the E_{i}s. The features of our theory make it hard to develop here a syntactic criterion for comparing the generality of two systems in solvable form, and, accordingly, finding suitable notions of most general unifier (mgu) and of complete set of mgus (see, e.g., [5]). Of course, a preorder can be imposed on systems as follows: given two systems E and E′, E is more general than E′ if any solution to E is also a solution to E′. From this semantic standpoint, the above set {E_{1}, …, E_{m}} contains (possibly properly) a minimal set of most general systems in solvable form (or templates of solutions) for E.

4.2 NP-hardness of the problem of finding a single hyperset unifier

One-way matching between automata, that is, the problem of instantiating a partially defined automaton so as to make it equivalent to a fully specified DFA (see end of Section 3), will turn out to be NP-complete. For the moment let us prove its NP-hardness, by reducing to it the propositional 3-SAT problem: it will emerge from Section 4.5, after the hyperset unification problem has been algorithmically settled, that the problem can be solved non-deterministically in polynomial time.

Given the formula

Φ = (ℓ_{11} ∨ ℓ_{12} ∨ ℓ_{13}) ∧ ⋯ ∧ (ℓ_{n1} ∨ ℓ_{n2} ∨ ℓ_{n3})

where, for i = 1, 2, 3 and j = 1, …, n,

ℓ_{ji} ≡ a_{ji} or ℓ_{ji} ≡ ¬a_{ji} and a_{ji} ∈ {d_{1}, …, d_{k}}

for a suitable k ≤ 3 · n, we introduce distinct unknowns P_{1}, N_{1}, …, P_{k}, N_{k}, and define the transformation function f as follows:

f(ℓ) = \{ \begin{matrix}P_{i} & if ℓ ≡ d_{i}, \\ N_{i} & if ℓ ≡ ¬d_{i}. \end{matrix}

Thus, in order to solve the instance Φ of 3-SAT, it is sufficient to check whether there exists an instantiation making the automaton

[figure: q_{0}; q_{1}; q_{k}; q_{k+n}; ⋯; ⋯; P_{1}, N_{1}; P_{2}, N_{2}; P_{k}, N_{k}; 0, f(ℓ_{11}),; f(ℓ_{12}), f(ℓ_{13}); 0, f(ℓ_{n1}),; f(ℓ_{n2}), f(ℓ_{n3})]

equivalent to the fully specified automaton below:^{8}

[figure: q_{0}; q_{1}; q_{k}; q_{k+n}; ⋯; ⋯; 0, 1; 0, 1; 0, 1; 0, 1; 0, 1]

Notice that the technique presented in Section 3 for expressing automaton equivalence as a unification problem would not work properly for non-deterministic automata: the equivalence problem for such automata is known to reside at a higher level of complexity (it is in fact PSPACE-complete—cf. [15]).

4.3 A unification algorithm, Hyper unify

Special chains of inclusions, introduced by the following definition, will play an important role in our subsequent discussion:

Definition 9 A path in a Herbrand system E is a sequence X_{0} ←^{Y_{0}} X_{1} ←^{Y_{1}} ⋯ ←^{Y_{n}} X_{n+1} of labeled edges such that X_{i} = {Y_{i}|X_{i+1}} is in E for all i in {0, …, n}. □

We now discuss the unification algorithm Hyper unify described in Fig. 4. This algorithm gets an input E which, without loss of generality, is assumed to be flat (cf. Def. 4).

Hyper unify performs a non-deterministic search. When reaching the leaf of a successful branch of the search tree, it will output a system E_{i} in solvable, explicit, form. The whole search tree will be finite.

The algorithm makes also use of an auxiliary data structure, C, to keep track of a number of temporary assumptions of the form W ∉ V. Action Fail 1 may detect a failure situation by checking whether one of the constraints Y ∉ X in C conflicts with the fact that Y must belong to X, by E.

In its present version, Hyper unify initializes C internally, and does not produce any information about it in the output. We will see, however, in Section 5, that Hyper unify can be enhanced to deal with negated membership literals. Then an initial value for C will be submitted as part of the input, and the final value of C will be retained with the output.

Hyper unify(E: Herbrand system); C := ∅; repeat \underline{Preamble:} repeat

1. discard any reflexive equations X = X from E;

2. for each equation e ≡ X = Y in E such that X occurs somewhere else in E, do begin E := (E _{Y}^{X} ∪ { X = Y }) \ { Y = Y }; C := C _{Y}^{X} end;

3. as long as there is a zipper X_{0} ←^{Y_{0}} X_{1} ←^{Y_{1}} ⋯ ←^{Y_{n−1}} X_{n} ←^{Y_{n}} X_{0}

(with X_{0}, …, X_{n} distinct from one another) in E, do begin

E := (E \ { X_{0} = {Y_{0}|X_{1}}, …, X_{n−1} = {Y_{n−1}|X_{n}}, X_{n} = {Y_{n}|X_{0}}}) ∪

{ X_{0} = {Y_{0}|K_{0}}, …, X_{0} = {Y_{n}|K_{n}}, X_{1} = X_{0}, …, X_{n} = X_{0} }; C := C ∪ { Y_{0} ∉ K_{0}, …, Y_{n} ∉ K_{n} };

end;

4. as long as there is a path X_{0} ←^{Y_{0}} X_{1} ←^{Y_{1}} ⋯ ←^{Y_{n}} X_{n+1} ←^{Y_{0}} X_{n+2}

(with Y_{0}, …, Y_{n} distinct from one another) in E, do E := (E \ { X_{0} = {Y_{0}|X_{1}}}) ∪ { X_{1} = X_{0} };

5. close C with respect to the rule: X ←^{Y} V in E, Z ∉ X in C implies Z ∉ V in C; until nothing has been modified by the last iteration; Turning point:

Fail 1: if there is an edge X ←^{Y} V in E with Y ∉ X in C,

then exit with failure; /* this check could immediately follow action 5 */ Fail 2: if there are equations X = f(X_{1}, …, X_{n}), and X = g(Y_{1}, …, Y_{m}) in E with f ≢ g,

then exit with failure; Succeed: if E is in solvable form, then exit with success returning E;

\underline{Actions:} select arbitrarily an equation e in E enabling one of the following actions

(a) e ≡ X = f(X_{1}, …, X_{n}), f ≢ with, and there is an e′ ≡ X = f(Y_{1}, …, Y_{n}) in E \ {e}: E := (E \ {e′}) ∪ { X_{1} = Y_{1}, …, X_{n} = Y_{n} }; /* removing e′ is inessential */

(b) e ≡ X = {Y |V }, and there is an e′ ≡ X = {Z|W } in E \ {e}

(note that X ≢ V and X ≢ W, thanks to action 3); perform one of the following actions: (b.1) E := (E \ {e′}) ∪ { Y = Z, V = W }; /* removing e′ is inessential */

(b.2) E := E ∪ { X = V };

(b.3) E := E ∪ { X = W };

(b.4) E := (E \ {e′}) ∪ { V = {Z|N}, W = {Y |N}}; C := C ∪ { Y ∉ N, Z ∉ N }; forever.

Figure 4: Hyperset unification algorithm

Before we undertake analyzing the complexity of Hyper unify —after which, the correctness proof will be supplied— let us develop a little nomenclature and some preliminary remarks and comments. It will be useful to think of a (non-deterministic) execution of Hyper unify as consisting of segments classified as follows:

Phase: An iteration of the outer repeat, consisting of a preamble (i.e., a full execution of the inner repeat), followed by the checks performed at the turning point, and (unless a termination has occurred) by one of the five actions (a), (b.1)–(b.4) (when more than one of these is viable, one is arbitrarily chosen).

Stage: A series of consecutive phases that

• immediately follows either initialization or an execution of action (b.4);

• either goes on forever, or terminates at the turning point, or ends with an execution of action (b.4);

• does not comprise any execution of action (b.4), save, possibly, at the end.

(An important fact we will discover later on is that no stage consists of infinitely many phases: this will rule out the second of the above three possibilities.)

Notice that new variables are introduced into E by actions 3 and (b.4) (they are the K_{i}s and the Ns, respectively).

As we are about to discuss, we can think that an equivalence relation between variables is being implicitly calculated by Hyper unify. Initially, each variable makes an equivalence class by itself; then, the equivalence relation gets refined by the preamble of each phase. Once they have become equivalent, two variables are to represent the same hyperset; accordingly, as soon as a variable formerly generated by action 3 or (b.4) becomes equivalent to an initial variable, we identify the two with one another and cease to regard the generated variable as ‘new’ any more.

Let us now clarify the main purpose of each preamble, which is to decompose the system E into subsystems of the form

X_{1} ; ⋮ ; X_{ℓ} \} = R = \{ \begin{matrix}f_{1}(Y_{11}, …, Y_{1a_{1}}) \\ ⋮ & ⋮ \\ f_{m}(Y_{m1}, …, Y_{ma_{m}}) \end{matrix}

with ℓ + m ≥ 1 (hopefully with f_{i} ≡ f_{j} for all pairs of i and j). These subsystems will be mutually independent in the sense that

• no left-hand variable X_{i} appears, globally, more than once;

• no representative variable R occurs as left-hand side of a variable-variable equation; apart from this, R is entirely free to occur in right-hand sides.

Of course we may assume that representative variables are distinct in different subsystems; thus, when m ≤ 1 holds for each one of the subsystems, a solvable form results from the preamble.

As for the equivalence relation over variables hinted at above, it can be characterized at the end of each preamble as being the reflexive and transitive closure of the relation {[X, R] : X = R in E}.

8To stay strictly inside the realm of pure (hyper)sets, one could replace 0 by ∅, and 1 by {∅}.

4.4 Termination of the Hyper unify algorithm

In this subsection we prove the termination of Hyper unify; that is, we show that every branch of the search tree of Hyper unify eventually breaks off, reporting failure or success. A rather coarse assessment of the maximum length of a branch will result from initial analysis; this will be refined into a polynomial bound on the overall complexity of the algorithm in Section 4.5.

To measure the size of the input system E, we adopt the following two parameters:

• v_{0}, the number of distinct variables in E;

• s_{0}, the number of occurrences of functional symbols in E (including with).

For reasons to become clear soon, both the termination proof and the complexity analysis will mainly consists in determining upper bounds for the number of stages, i.e. for the number of actions (b.4) performed along a branch.

Remarks 2 1. A new variable Q always shows up, at creation time, in a context V = {Y |Q} (where V ≢ Q and Y ≢ Q); later on, it can be moved to a different context by actions 2, or (b.2)–(b.3). Anyway, it will never come to occupy a label position over an edge X ←^{Q} W: that is to say, no equality X = {Q|W } will ever go into E unless after Q has become equivalent to a pre-existing label, in which case we no longer regard it as ‘new’.

2. It follows from the preceding observation and from the presence of actions 3 and 4 in Hyper unify that no path X_{0} ←^{Y_{1}} X_{1} ←^{Y_{2}} ⋯ ←^{Y_{n}} X_{n} can have length n > v_{0} at the end of any preamble.

3. If an edge X_{0} ←^{Y_{0}} X_{1} drawing its origin from an action 3 or (b.4) becomes part of a zipper X_{0} ←^{Y_{0}} X_{1} ←^{Y_{1}} ⋯ ←^{Y_{0}} X_{0}, a failure will take place at the next turning point. This follows from the fact that the creation of the edge X_{0} ←^{Y_{0}} X_{1} causes the constraint Y_{0} ∉ X_{1} to be put in C; however the path in question will cause action 3 to place the equation X_{0} = X_{1} in E, which will fire a Fail 1 termination.

4. The preceding observation implies that the overall number of arcs introduced by action 3 is less than the number of occurrences of with in the initial system, bounded by s_{0}. □

The following lemma implies that the algorithm terminates provided action (b.4) is performed a finite number k of times (cf. Corollary 2). Later on, with Lemma 3, we will place a finite bound on k.

Lemma 1 Consider a stage of a computation of Hyper unify(E). Let v and s be the number of inequivalent variables (initial or not) and the number of occurrences of functional symbols in E, as they are at the beginning of that stage. Then the stage comprises at most 1 + v + s_{0} + s phases.

Proof. First note that no action other than (b.4) increases s.

The number v might increase due to executions of action 3, which however cannot be exploited more than s_{0} times, as noticed in Remark 2.4. This potential increase of v accounts for the addendum s_{0} in the thesis of the lemma.

We can henceforth focus on actions (a), (b.1)–(b.3), namely the ones from which a non-deterministic choice is performed in every non-final phase.

(a) and (b.1) cause s to decrease; actions (b.2) and (b.3), although leaving s unchanged, set the ground for either a reduction of v in the next preamble or a Fail 1 termination at the next turning point.

Corollary 2 Suppose action (b.4) is performed a finite number k of times during a computation of Hyper unify(E). Then the computation comprises at most (k + 1) · v_{0} + (k + 2) · s_{0} + (k + 1)^{2} phases.

Proof. Let N_{1}, …, N_{k} be the variables introduced by the successive executions of action (b.4). We can split the sequence of phases performed by Hyper unify(E) into k + 1 successive stages determined by the introduction of the N_{i}s.

\begin{aligned}& & N_{1} & & N_{2} & & & & N_{k−1} & & N_{k} \\ • & ⟶ & • & ⟶ & • & ⟶ & ⋯ & ⟶ & • & ⟶ & • & ⟶ & ∘ \end{aligned}

The first stage is based on a system with size parameters v_{0} and s_{0}; hence, by Lemma 1, it contains no more than 1 + v_{0} + s_{0} + s_{0} phases. After the application of action (b.4), both s and v get increased at most by one; therefore the second stage, again by Lemma 1, contains no more than 1 + (v_{0} + 1) + (s_{0} + 1) + s_{0} phases. The overall situation is summarized by the following diagram:

\begin{aligned}& & N_{1} & & N_{2} & & & & N_{k} \\ • & \overrightarrow{}_{1+v_{0}+s_{0}+s_{0}} & • & \overrightarrow{}_{1+(v_{0}+1)+(s_{0}+1)+s_{0}} & • & ⟶ & ⋯ & ⟶ & • & \overrightarrow{}_{1+(v_{0}+k)+(s_{0}+k)+s_{0}} & ∘ \end{aligned}

The number of phases forming a whole computation is hence bounded by ∑_{i=0}^{k}(1 + (v_{0} + i) + (s_{0} + i) + s_{0}); however, it is appropriate to consider the addendum s_{0} only once, because it represents an upper bound on the number of edges introduced by action 3, which is a global quantity. Thus, no more than (k + 1) · v_{0} + (k + 2) · s_{0} + (k + 1)^{2} phases can be performed.

It should be clear, already, that each phase lasts finitely long: we will be more specific on this by assessing the complexity of a preamble in Section 4.5.

Let us now indicate by E_{i} and C_{i} the values of E and C when the turning point is reached for the (i+1)-st time. Any E_{i} induces an equivalence relation ∼_{i} among variables, as explained at the end of Section 4.3.

To place a bound on the number k of times (b.4) gets executed, we will define in terms of ∼_{i} a tuple τ_{i} of natural numbers so that modifications of E, C made during the i-th phase may cause τ_{i+1} to differ from τ_{i}. Changes of τ will invariably lower it w.r.t. the lexicographic well-ordering of tuples, without affecting its length. τ gets lowered whenever a new variable is introduced, which happens, in particular, with (b.4). This by itself ensures —in view of Corollary 2— the termination of Hyper unify.

Notice that any lowering of a tuple [x_{0}, …, x_{ℓ}] w.r.t. this ordering can be achieved by elementary decrease actions of the following kind:

• a component x_{j}, with x_{j} > 0, gets decremented by one; simultaneously (if j < ℓ)

• a component x_{i}, with i > j, is incremented by h units, with h ≥ 0.

In the case at study, we will be able to show that such decrease actions will always have 0 ≤ h ≤ 2; correspondingly, a decrease action will be named:

destruction: if h = 0,

climbing: if h = 1,

generation: if h = 2.

To introduce τ, let us consider the set

L_{i} = { Y : X = { Y | W } in E_{i}}

of all Y s occurring in a context X ←^{Y} W within E_{i}. By Remarks 2.1–2, |L_{i}| ≤ |L_{0}| for all i ≥ 0. Moreover, as easily seen, |L_{i}| = |L_{0}/∼_{i} |. We define τ_{i} to be the tuple τ_{i} = [x_{0}, …, x_{|L_{0}|}] , where each x_{j} is the cardinality of the following set:

{ equations of the form = { | W } in E_{i} : |L_{0}| − |L_{i}| + |{ Y : Y ∉ W in C_{i} }| = j } .

The initial value τ_{0} of τ clearly has x_{0} ≤ s_{0} and x_{1} = ⋯ = x_{|L_{0}|} = 0.

Lemma 3 A stage always lowers the value of τ except, possibly, when a Fail 1 exit is about to take place.

Proof. Actions 1, (a), (b.2), and (b.3) do not affect τ. Action (b.1) always affects τ as a destruction action.

The complexity function compl(τ) has been carefully chosen in order that action 2, whose effect is a sequence of destruction and generation actions, cannot increase it.

Actions 3 and 5 may leave τ unchanged or affect it as climbing actions; action 4 might cause τ to increase, but in this case Fail 1 will immediately cause termination.

If neither Y ∉ W nor Z ∉ V belongs to C, then action (b.4) makes τ lower (it can be viewed as a generation action). Unless this is the case, an immediate combination of action 3 with Fail 1 will lead to termination.

Theorem 4 (termination) Let E be a flat system. Then Hyper unify(E) always terminates, no matter what sequence of non-deterministic choices has been made.

Proof. Lemma 3 ensures that a only finite number of actions (b.4) occur along a branch of the computation. The claim follows, by Corollary 2.

One may wonder whether the above translation of Hyper unify actions into chains of destruction, climbing, and generation actions, may disclose a time complexity assessment sharper than a simple termination result. Unfortunately, this is not the case.

It can be shown that, starting with a tuple [x_{0}, …, x_{ℓ}] of natural numbers, no more than

3^{ℓ} · x_{0} + 3^{ℓ−1} · x_{1} + ⋯ + 3^{0} · x_{ℓ} ≤ (x_{0} + ⋯ + x_{ℓ}) · 3^{ℓ}

consecutive destruction, climbing, and generation actions can be performed.

This exponential bound cannot be improved significantly without refining the technique: if, as in our case, the initial tuple has the form

[s_{0}, \underbrace{0, …, 0}_{ℓ−1}] ,

a chain consisting of s_{0} · (2^{ℓ} − 1) generation actions followed by s_{0} · 2^{ℓ} destructions is a priori conceivable. However, as we will now see, a similar chain does not reflect the behavior of any concrete Hyper unify computation.

4.5 NP-completeness of the problem of finding a single hyperset unifier

In this subsection we prove that Hyper unify belongs to the complexity class NP. It hence follows that the hyperset unifiability problem is NP-complete, in view of the reduction of 3-SAT to pure hyperset matching seen in Section 4.2.

For the termination proof, an adequately abstract view of the data structure E, C manipulated by Hyper unify was provided above by the tuple τ: the decrease actions performed on τ somehow mimicked the basic actions of Hyper unify. Here, before undertaking the complexity analysis, we must resort to a subtler abstract interpretation.

We will represent E by a multi-graph G_{E}, and C by a function lev : vars(E) ⟶ IN. We momentarily defer the characterization of lev. As for G_{E}, its constituents are:

• nodes N_{E} = {V_{1}, V_{2} : V_{1} = { | V_{2} } in E};

• labels L_{E} = {Y : = { Y | } in E};

• directed labeled edges A_{E} = {V_{1} ←^{Y} V_{2} : V_{1} = {Y |V_{2}} in E}.

Conceptually, the pair G_{E}, lev gets updated at every turning point, like τ. As we have already proved termination, we are in a position to refer to the final value of either of these structures. (Obviously, G_{E} and lev, as well as their final values, depend on the course of a non-deterministic computation.)

The following two examples are aimed at conveying an intuitive grasp of why each non-deterministic branch contains a number of phases (equivalently, a number of (b.4) actions) polynomially related to the size v_{0} + s_{0} of E.

Example 3 Starting with the set E = {X = {A|V_{1}}, X = {B|V_{2}}, X = {C|V_{3}}} of membership constraints, a branch that maximizes the number of stages will yield the following final value for G_{E}. Indicating by the arrow ← ∘ any edge removed by action (b.4), we have

V_{1}
↙ ∘^{A}  ↖^{B}
X ← ∘^{B} V_{2} ← ∘^{A} N_{1}
↖^{C}  ↖^{C}  ↖^{C}
V_{3} ←^{B} N_{2} ←^{A} N_{3}

Notice that the unification algorithm does not generate a variable corresponding to each subset of a threeelement set, a reason being that once the edge X ←^{A} V_{1} has been removed, it becomes impossible to re-exploit it in conjunction with X ←^{C} V_{3} to fire an action (b.4). □

Example 4 A branch that maximizes the number of phases for the Herbrand system

\begin{aligned}E & = & \{ & X = \{ Y_{1} | A_{1} \}, A_{1} = \{ Y_{2} | A_{2} \}, A_{2} = \{ Y_{3} | A_{3} \}, \\ & & & X = \{ Z_{1} | B_{1} \}, B_{1} = \{ Z_{2} | B_{2} \} \}, \end{aligned}

expressing the set unification problem {Y_{1}, Y_{2}, Y_{3} | A_{3}} = {Z_{1}, Z_{2} | B_{2}}, will yield the following final value for G_{E}:

A_{3}
↙ ∘^{Y_{3}} ↖^{Z_{1}}
A_{2}  N_{2}^{(3)}
↙ ∘^{Y_{2}}  ↖^{Z_{1}}  ↙ ∘^{Y_{3}}  ↖^{Z_{2}}
A_{1}  N_{2}^{(2)}  N_{1}^{(4)}
↙ ∘^{Y_{1}}  ↖^{Z_{1}}  ↙ ∘^{Y_{2}}  ↖^{Z_{2}}  ↙^{Y_{3}}
X  N_{1}^{(1)}  N_{1}^{(3)}
↖^{Z_{1}}  ↙ ∘^{Y_{1}}  ↖^{Z_{2}}  ↙^{Y_{2}}
B_{1}  N_{1}^{(2)}
↖^{Z_{2}} ↙^{Y_{1}}
B_{2}
□

Inspection of these examples leads to the following observations:

Remarks 5 1. If one subtracts the initial number of edges in G_{E} from the number of edges in the final G_{E} —counting also those that were removed by (b.4)— one obtains twice the overall number \overline{β} of (b.4) actions.

2. The evolution of G_{E} progressively limits the possibility to apply action (b.4): calling into play again the decrease actions of Section 4.4, this means that generation actions (the only potential source of exponentiality) become less and less viable. Sometimes the termination guarantee does not come from this phenomenon, but, rather, from the presence of C-constraints. This does not emerge from the two examples just seen, but can be seen from studying a system like the following: X = { | A }, X = { | B }, Y = { | A }, Y = { | B } .

3. If a node X eventually inserted into G_{E} has incoming edges in some phase, at least one incoming edge will always be alive, till the end of the computation. □

It is now time to introduce lev:

Definition 10 Given the pair E, C, a level-mapping is a function lev : vars(E) ⟶ IN, satisfying the following conditions:

• for all edge V_{1} ←^{Y} V_{2} of G_{E}, if Y ∉ V_{2} belongs to C, then lev(V_{2}) = lev(V_{1}) + 1, otherwise lev(V_{2}) ≤ lev(V_{1}) + 1;

• for all equations V_{1} = V_{2} in E, lev(V_{1}) = lev(V_{2}). □

Remark 6 In the absence of negative information, a trivial level-mapping can be obtained by simply setting to 0 all variables. On the other hand, it may be the case that a level-mapping does not exist, as the following example shows:

X ⟵^{Y_{1}} V
↖^{Y_{2}}  ↙^{Y_{3}}  Y_{3} ∉ V, Y_{2} ∉ W both belonging to C .
W

Plainly, if a level-mapping lev for E, C exists at all, it is not unique: one may ‘tune’ its construction so as it meet the condition

for all variables V, lev(V) ≤| L_{E} |

(cf. the definition of the L_{i}s in Section 4.4). This new condition —to be taken from now on as part of the definition of a level-mapping— can easily be fulfilled, e.g., by setting lev(W) = 0 for at least one node W in each connected component of (the undirected graph underlying) G_{E}. □

W.r.t. a level-mapping lev, we say that an edge X ←^{Y} V (or, more generally, an ordered pair X, V) is of level i if lev(V) = i.

Definition 11 Let E′ be the system in solvable form resulting from a (non-deterministic) computation of Hyper unify with input E: hence any variable generated in such a computation occurs in E′. Let, moreover, lev be a level-mapping for E′ (hence for E). Then,

• α(i) stands for the number of edges of level i in G_{E}. Also, \overline{α} =_{Def} ∑_{i=0}^{∞} α(i) = ∑_{i=0}^{|L_{E}|} α(i).

• β(i) stands for the number of edges of level i introduced in the computation by action (b.4) (regardless of whether such edges survive in G_{E′}). Let also \overline{β} =_{Def} ∑_{i=0}^{∞} β(i) = ∑_{i=0}^{|L_{E}|} β(i). □

In view of Corollary 2, in order to guarantee the NP-completeness of Hyper unify, it is sufficient to place polynomial bounds both on the total number \frac{\overline{β}}{2} of executions of (b.4) and on the number of actions taking place within a single phase.

Theorem 5 In a successful branch of Hyper unify(E), if no variable X generated by action (b.4) ever joins another variable Y (in the sense that either X = Y or Y = X is put into E), then \overline{β} is O(\overline{α}^{3}).

Proof. First of all, let us focus on a couple of conditions necessary for an action (b.4) to take place:

• two ‘parent’ edges of level j concur to the action, where j + 1 is the level of the two edges to be created—one of these parent edges will be deleted by the action;

• since the parent edges must enter the same node, the latter cannot have a single incoming edge when the action is fired.

Based on these remarks, we derive the following:

• β(0) = 0 and β(1) ≤ 2 · α(0).

• The presence of two generated edges at level j − 1 implies that there is a node at level j − 1. The overall number of generated nodes of level j − 1 is \frac{β(j−2)}{2}; hence the assumption that generated nodes never join —implying that nodes, once generated, persist in G_{E} retaining an incoming edge— ensures, for j ≥ 2, that

β(j) ≤ 2 · (α(j − 1) + β(j − 1) − \frac{β(j − 2)}{2}) .

By unfolding these constraints on β, we obtain

β(j) ≤ 2 · (∑_{i=1}^{j} i · α(j − i)) .

Since | L_{E} |≤ α, we conclude:

\overline{β} = ∑_{j=0}^{|L_{E}|} β(j) ≤ 2 · (∑_{j=1}^{|L_{E}|} ∑_{i=1}^{j} i · α(j − i)) = O(\overline{α}^{3}) .

We are left with the task of showing that the assumption that generated variables never join can be discarded from the statement of Theorem 5. To this end, notice that two variables of level j + 1 becoming equivalent might generate a situation in which action (b.4) can be performed. However, an inspection of Hyper unify (cf. proof of Theorem 6 below) shows that at the same time two edges of level j come to coincide. As a consequence, the overall number of actions (b.4) (and hence \overline{β}) cannot increase.

Theorem 6 In any computation of Hyper unify, no more than O(\overline{α}^{3}) = O ((s_{0})^{3}) new variables can be generated.

Proof. In view of Theorem 5, we only need to show the following fact: if a variable N introduced by action (b.4) as the tail of two edges V ←^{Y} N and W ←^{Z} N of level i joins another variable A, then a pair of edges of level i has not been used to generate two edges of level i + 1.

In fact, in order for N to be unified with A, a series N = A_{1}, A_{1} = A_{2}, …, A_{n} = A of equalities must be inferred by Hyper unify. To get the first equation N = A_{1}, the unification algorithm must perform action (b) with one of the two equations V = { Y | N } or W = { Z | N }, together with an equation V = { C | B } or W = { C | B }. A simple inspection of the four subcases of action (b) shows that (b.1) is the only subcase that introduces an equation N = B without leading to a subsequent Fail 1 (note that B ≡ A). This means that in such branch of a computation, the edges V ←^{C} B (or W ←^{C} B) and V ←^{Y} N (or W ←^{Z} N) of level i cannot be used to fire action (b.4) and hence to generate two edges of level i + 1.

Corollary 7 (NP-completeness) Let E be a flat system. Then every single branch generated during the execution of Hyper unify(E) consists in a number of phases polynomially bounded in v_{0} + s_{0}.

Proof. From Theorem 6 we know that the number k of variables generated by action (b.4) of the algorithm is polynomially bounded in v_{0} + s_{0}. The thesis follows from Corollary 2.

As already said, for a full NP-completeness proof we must place a bound also on the number of actions within a phase. This is relatively easy, as we know from the last propositions that a polynomial bound exists for the number of new variables and functional symbols (edges) that can be introduced:

• action 1 can be performed ad most once for each variable; the same happens with 2;

• action 3 can be performed in total a number of times not exceeding s_{0}, as noticed in Remark 2.4;

• the number of times action 4 gets executed is bounded by the number of edges;

• action 5 consists of an update of a system of constraints that relate to one another a polynomially bounded number of variables.

4.6 Soundness and completeness of the Hyper unify algorithm

In this section we will prove that the set unification algorithm Hyper unify presented above is sound and complete with respect to the axiomatic set theory introduced in Section 2.2. These important properties of the algorithm can be phrased as follows (proof to be supplied later on):

Theorem 8 Let E_{1}, …, E_{k} be the systems in solvable form produced as output by Hyper unify(E). Then the following holds:

(W), (E), (L), (=), (F_{0} ), (F_{1} ) ⊢ (E ↔ ∃Q_{1} ⋯ ∃Q_{m} ⋁_{i=1}^{k} E_{i}) ,

where Q_{1}, …, Q_{m} are all variables in the E_{i}s that do not occur in E. □

In order to achieve greater generality, we will prove the above result as a consequence of an analogous result concerning a variant procedure named Hyper unify_{∗}(E, C)—see Lemma 9 below. Although strictly akin to Hyper unify, Hyper unify_{∗} will not be guaranteed to terminate. The only differences between the two procedures are:

• C is regarded as a new input parameter. Therefore, it shall not be initialized to ∅ inside Hyper unify_{∗};

• in actions 3 and (b.4), situations where Hyper unify places a new pair into C, Hyper unify_{∗} is free to do the same or to leave C unchanged. (Note that the only remaining action that may affect C, which is action 5, remains as before.)

Preliminary to stating the generalization of Theorem 8, we need a few definitions.

Definition 12 A Unify-tree is a directed unordered, non-empty tree, each of whose nodes ν bears labels E_{ν}, C_{ν} meeting the following conditions:

• E_{ν} is a flat Herbrand system;

• C_{ν} is a collection of literals of the form Y ∉ Q, with Y and Q variables.

• A relationship reflecting the behavior of Hyper unify_{∗} holds between E_{ν}, C_{ν} on the one hand and the tuple E_{μ_{1}}, C_{μ_{1}}, …, E_{μ_{p}}, C_{μ_{p}}, where μ_{1}, …, μ_{p} are the distinct children of ν, on the other. The relationship is as follows:

If the values of E and C are set to E_{ν} and C_{ν} at the beginning of a phase, then, depending on the first action that will affect either of them in the subsequent execution of Hyper unify_{∗}, one has that:

1, 2, 3, 4, 5, (a): p = 1 and E_{μ_{1}} and C_{μ_{1}} are possible values of E, C after the execution of the modifying

action; (b): p = 4 and E_{μ_{i}} and C_{μ_{i}} are possible values of E, C after the execution of (b.i); none: p = 0. In this case, ν will be called a failure or a success leaf in agreement with the kind of

exit that takes place (cf. actions Fail 1, Fail 2, and Succeed).

A fringe of a Unify-tree is a set S of nodes such that: every maximal path of the tree contains at most one node from S, and, if it contains none, it ends with a failure leaf. □

It should be clear from this definition that for any given pair E_{∗}, C_{∗}, a Unify-tree whose root is labeled E_{∗}, C_{∗} exists. Unify-trees correspond in fact to the parallel executions of Hyper unify_{∗}(E_{∗}, C_{∗}): there are two sources of parallelism in Hyper unify_{∗}, namely action (b) and some freedom in putting literals into C. However, it is only the branching caused by action (b) that gets represented by a single Unify-tree.

Among others, a Unify-tree originates from the specific execution of Hyper unify_{∗} that is entirely alike to an execution of Hyper unify, except for the different initialization of C. In this execution, C literals are added whenever possible; moreover, the Unify-tree will be finite in this special case (cf. Theorem 4), and its set of success leaves will constitute a fringe.

Lemma 9 Let T be a Unify-tree, with root ϱ. Then, for any fringe S of T , the following holds:

(W), (E), (L), (=), (F_{0} ), (F_{1} ) ⊢ ((E_{ϱ} ∧ C_{ϱ}) ↔ ∃Q_{1} ⋯ ∃Q_{m} ⋁_{ν in S}(E_{ν} ∧ C_{ν})) ,

where Q_{1}, …, Q_{m} are all the variables in the E_{ν}s that do not occur in E_{ϱ} ∧ C_{ϱ}.

Proof. To prove the thesis, since

(W), (E), (=), (F_{0} ) ⊢ ¬(E_{μ} ∧ C_{μ})

trivially holds for every failure leaf μ, it will suffice to check that every single action of Hyper unify_{∗} leads from a node ν to nodes μ_{1}, ⋯, μ_{p} such that

(W), (E), (L), (=), (F_{1} ) ⊢ ((E_{ν} ∧ C_{ν}) ↔ ∃Z_{1} ⋯ ∃Z_{ℓ} ⋁_{i=1}^{p}(E_{μ_{i}} ∧ C_{μ_{i}})) ,

where Z_{1}, …, Z_{ℓ} are the new variables (if any). In the following, each number on the left indicates the action being analyzed.

1. X = X, being true by (=), can be discarded from E_{ν}.

2. For any formula φ, X = Y ∧ φ(X, Y) is equivalent to X = Y ∧ φ(Y, Y) by (=).

3. Viewed as a formula, a zipper X_{0} ←^{Y_{0}} X_{1} ←^{Y_{1}} ⋯ ←^{Y_{n−1}} X_{n} ←^{Y_{n}} X_{0} yields X_{i} = X_{0}, hence Y_{i} ∈ X_{0}, for i = 0, …, n—by (E) and (W). Accordingly, by assigning X_{0} lessY_{i} to K_{i}, one has both X_{0} = {Y_{i}|K_{i}} and Y_{i} ∉ K_{i} for all i—by (W) and (L).

It follows that

(W), (E), (L) ⊢ (E_{ν} ∧ C_{ν}) → ∃K_{0} ⋯ ∃K_{n} (E_{μ_{1}} ∧ C_{ν} ∧ ⋀_{i=0}^{n} Y_{i} ∉ K_{i}) .

Conversely, as is easily seen,

(W), (=) ⊢ (E_{μ_{1}} ∧ C_{ν}) → (E_{ν} ∧ C_{ν}) .

4. From X_{0} ←^{Y_{0}} X_{1} ←^{Y_{1}} ⋯ ←^{Y_{n}} X_{n+1} ←^{Y_{0}} X_{n+2}, by (W) and (E), it follows that X_{0} = X_{1}. In fact, Y_{0} ∈ X_{n+1}, whence Y_{0} ∈ X_{n}, ⋯, Y_{0} ∈ X_{1}. Hence, the insertion of Y_{0} into X_{1} has no effect and, thanks to (=), the equality X_{0} = {Y_{0}|X_{1}} can be simplified into X_{0} = X_{1}.

Applied hyperset unification 27

5. E_{ν} ∧ C_{ν} is equivalent to E_{μ_{1}} ∧ C_{μ_{1}} by virtue of (W) alone.

(a) X = f(X_{1}, …, X_{n})∧X = f(Y_{1}, …, Y_{n}) is equivalent to X = f(X_{1}, …, X_{n})∧X_{1} = Y_{1} ∧⋯∧X_{n} = Y_{n}. One direction follows from (F_{1} ), and the other from (=).

(b) It is easy to infer from (W), (E), (L), and (=), that the following Venn diagrams describe all possible situations under which e ∧ e′ ≡ X = {Y |V } ∧ X = {Z|W } holds:

Y = Z :  X = V = W ; Y • ; 1  \begin{matrix}X = V \\ Y • & W \\ 2 \end{matrix}  \begin{aligned}& X = W \\ V & Y • \\ & 3 \end{aligned}  \begin{matrix}X \\ Y • & V = W \\ 4 \end{matrix}

Y ≠ Z :  X = V = W ; Y • Z• ; 5 \begin{aligned}& X = V \\ W & Y • Z• \\ & 6 \end{aligned}  \begin{matrix}X = W \\ Y • Z• & V \\ 7 \end{matrix}  \begin{aligned}& X \\ W & Y • Z• & \begin{matrix}V \\ N \end{matrix} \\ & 8 \end{aligned}

Moreover, the same axioms yield that: (b.1) diagrams 1, 4 describe all possibile situations under which (e ∧ Y = Z ∧ V = W) holds; (b.2) diagrams 1, 2, 5, 6 describe all possibile situations under which (e ∧ e′ ∧ X = V) holds; (b.3) diagrams 1, 3, 5, 7 describe all possibile situations under which (e ∧ e′ ∧ X = W) holds; (b.4) diagrams 1, 8 describe all possibile situations under which ∃N (e∧V = {Z|N}∧W = {Y |N}∧Y ∉

N ∧ Z ∉ N) holds. We conclude from this diagram analysis that the following holds

\begin{aligned}(e ∧ e′) & ↔ & ((e ∧ Y = Z ∧ V = W) ∨ (e ∧ e′ ∧ X = V) ∨ (e ∧ e′ ∧ X = W)∨ \\ & & ∃N (e ∧ V = \{Z|N\} ∧ W = \{Y |N\} ∧ Y ∉ N ∧ Z ∉ N)) . \end{aligned}

Either one of the literals Y ∉ N, Z ∉ N, or both, can be removed from the right-hand side of this bi-implication, because ∃N (e ∧ V = {Z|N} ∧ W = {Y |N}) easily yields e′.^{9}

Proof of Theorem 8 Let us consider the Unify-trees T_{0}, T_{1} corresponding to the executions of Hyper unify_{∗}(E, ∅) that respectively add C literals

• whenever possible,

• never.

9Note that since the pairs (1, 8), (4, 5), (6, 7) of diagrams are incompatible, none of the alternatives (b.1)–(b.4) in Hyper unify is superfluous.

T_{0} corresponds to the execution of Hyper unify(E); hence it is finite, by Theorem 4. The preceding lemma, referred to the fringe S_{0} consisting of all success leaves of T_{0}, gives

E ↔ ∃Q_{1} ⋯ ∃Q_{m} ⋁_{ν in S_{0}}(E_{ν} ∧ C_{ν}) .

T_{1} clearly contains an isomorphic copy T′_{0} of T_{0}: every node μ in T_{0} is labeled E_{μ}, C_{μ}, while the corresponding node μ′ is labeled E_{μ}, ∅ in T′_{0}. We consider the fringe S_{1} of T_{1} consisting of all nodes ν′ s.t. ν either belongs to S_{0} or is a Fail 1 leaf of T_{0}. Again by Lemma 9, we have

E ↔ ∃Q_{1} ⋯ ∃Q_{m}∃Q_{m+1} ⋯ ∃Q_{m+k} ⋁_{ν′ in S_{1}} E_{ν} .

Assuming ∃Q_{1} ⋯ ∃Q_{m} ⋁_{ν in S_{0}}E_{ν} , one readily obtains ∃Q_{1} ⋯ ∃Q_{m+k} ⋁_{ν′ in S_{1}}E_{ν} , whence E follows. Con-

versely, from E, one derives ∃Q_{1} ⋯ ∃Q_{m} ⋁_{ν in S_{0}}(E_{ν} ∧ C_{ν}), which entails ∃Q_{1} ⋯ ∃Q_{m} ⋁_{ν in S_{0}} E_{ν}.

We conclude with the desired thesis: E ↔ ∃Q_{1} ⋯ ∃Q_{m} ⋁_{ν in S_{0}}E_{ν}.

An easy corollary of Theorem 8 is that Hyper unify solves E in the sense of Definition 8. As a matter of fact, any solution to E is also a solution to (at least) one of the E_{i}s (provided a mapping for the new variables Q_{1}, …, Q_{m} is made explicit). As said after Definition 8, the set {E_{1}, …, E_{k}} can be seen as a complete set of templates of solutions for E. Unfortunately, the various E_{i}s are not necessarily independent, as it emerges from the following example:

Example 7 Let E consist of the equations:

X = {A | C}, X = {B | D}, C = {B | Z}, D = {A | Z}, Z = ∅

Two possible non-deterministic computations return the systems:

\begin{aligned}E_{1} & = & \{A = B, C = D, X = \{B | D\}, D = \{B | Z\}, Z = ∅\} , \\ E_{2} & = & \{X = \{A | C\}, C = \{B | Z\}, D = \{A | Z\}, Z = ∅, N = Z\} \end{aligned}

(to get the former, start by applying action (b.1); for the latter, apply first (b.4) —which generates a new variable N— and then (b.1) twice) It is clear that E_{2} covers all the solutions of E_{1} plus those in which A and B are mapped into different hypersets. Thus, E_{1} is more general than E_{2}. □

Algorithms for detecting overlaps between solvable form systems will hopefully emerge from ongoing research. More specifically, let us assume that E_{0}, …, E_{n+1} are solvable form systems and that W are the ‘relevant’ variables they share. That is, one regards solutions γ_{i}, γ_{j} for E_{i}, E_{j} as being the ‘same’ solution when γ_{i}|_{W} = γ_{j}|_{W}. One would like to

1. determine whether every solution to E_{0} also solves at least one of E_{1}, …, E_{n+1};

2. determine whether all solutions of E_{0} also are solutions to E_{1};

3. determine whether E_{0} and E_{1} have any solutions in common.

A solution to 2 seems to be at hand, whereas the more general problems 1 and 3 remains as yet somewhat puzzling.

5 Hyper unify as a set-constraint manager

We have seen in the preceding section that any system E involving with , ∅, and free functors, can be rewritten, equivalently, as a finite disjunction E_{1}, …, E_{k} of systems in solvable form.

We now extend this result by showing that the unification algorithm introduced in Section 4 is in fact sufficiently general to support the treatment of the operator less (to be interpreted in agreement with (L_{0 ,1} ) of Section 2.2). In the new broader context, however, the negative information contained in C must be retained as output of the system.

In order to handle flat systems of equations that involve less, we might choose to install into Hyper unify the explicit treatment of pairs e, e′ of equations of the following forms:

e ≡ X = V less Y, e′ ≡ X = W less Z;
e ≡ X = V less Y, e′ ≡ X = { Z | W };
e ≡ X = V less Y, e′ ≡ X = f(Y_{1}, …, Y_{n}), where f ≢ less , f ≢ with .

A simpler line of attack is to resort to the following non-deterministic pre-processing technique:

for every equation V = X less Y, add to E either

1. X = { Y | V }; or
2. X = V;

moreover, do C := C ∪ { Y ∉ V }.

Clearly, 1 reflects the case when Y ∈ X holds, while 2 corresponds to the case Y ∉ X. The correctness of our approach is based on the following lemma:

Lemma 10 \begin{aligned}(W), (E), (L) & ⊢ & V = X less Y ↔ \\ & & ( ( Y ∉ V ∧ X = \{ Y | V \}) ∨ ( Y ∉ X ∧ V = X) ) . \end{aligned} □

It is easy to modify the proof of Theorem 8 so as to show that the input system E is provably equivalent to the disjunction ⋁_{i} ∃N_{i_{1}} ⋯ ∃N_{i_{k_{i}}} (E_{i} ∧C_{i}) taken over all pairs E_{i}, C_{i} that result from the successful branches, and N_{i_{1}}, …, N_{i_{k_{i}}} denote all variables, present in E_{i} ∧ C_{i} but not in the original E, introduced along the i-th such branch.

Somewhat disturbingly, such conjunctions are not guaranteed to be useful in general. Consider the following unsatisfiable system: E = {X = { Y, X }, Y = { X }, Z = { B | A }, Z = X less Y }.^{10} By using the rewriting of less (case 1.) and two applications of action (b.1) of Hyper unify we obtain the system {B = X = { Y, X }, Z = Y = { X }, A = ∅} together with the constraint Y ∉ Z. The system alone is satisfiable and, by Aczel’s AFA, implies X = Y = Z. Hence, its conjunction with the constraint Y ∉ Z placed into C by the preprocessor, contradicts, very much like E does, AFA—in our restricted axiomatization of Section 2.2 it contradicts (H). An approach to eliminate useless disjuncts would be to exploit the decision test specified in Section 6 of [28], but the latter works only in a context where free functors are not allowed to occur. Therefore, given E_{i} in solvable form and C_{i}, we test for satisfiability the following formula, implicitly keeping into account the freeness axioms:

C_{i} ∪ { equations of the form X = Y or of the form X = {Y |V } in E_{i} } ∪ F_{0}(E_{i}) ∪ F_{1}(E_{i}) ∪ U(E_{i}) , where the formulae placed in F_{0}(E_{i}), F_{1}(E_{i}), and U(E_{i}), as indicated below, force the correct interpretation w.r.t. the axioms (F_{0} ), (F_{1} ), and (U_{0 ,1} ), respectively:^{11}

10For the sake of readability, we are not rewriting E into equi-satisfiable flat form.

• F_{0}(E_{i}) =_{Def} { X ≠ Y : X = f(V_{1}, …, V_{m}), Y = g(Z_{1}, …, Z_{n}) both in E_{i}, and f ≢ g }.

• F_{1}(E_{i}) =_{Def} ⋃_{f∈Σ\{ with }} F_{1}(f, E_{i}), where for each f, assuming that X_{1} = f(Y_{1}^{(1)}, …, Y_{n}^{(1)}), …, X_{k} = f(Y_{1}^{(k)}, …, Y_{n}^{(k)}) are all equations of the form X = f(Y_{1}, …, Y_{ar(f)}) in E_{i}, we have

F_{1}(f, E_{i}) =_{Def} { ( ⋀_{h=1}^{n} Y_{h}^{(i)} = Y_{h}^{(j)}) ↔ X_{i} = X_{j} : 0 < i < j ≤ k } .

• Let {X_{1} = t_{1}, …, X_{m} = t_{m}} be the entire set ⋃_{f∈Σ\{ with }}{ equations of the form X = f(Y_{1}, …, Y_{ar(f)}) in E_{i} }; then

U(E_{i}) =_{Def} A = {A_{1}, …, A_{m}} ∧ ⋀_{={W | } in E_{i}}W ∉ A ∧ ⋀_{j=1}^{m} X_{j} = {A_{j}}

where A, A_{1}, …, A_{m} are new variables not occurring in E_{i}.

The formulae in U(E_{i}) reflect the fact that different uninterpreted terms must denote different colors, by introducing sets A_{1}, …, A_{m} suitably witnessing differences.

It is easy to prove that the above translation preserves satisfiability.

6 Type-finding through hyperset unification

This section is devoted to illustrating, through an example, how hyperset unification can be exploited for the task (more engaging than type-checking) of type-finding. As in Chapter 6 of [3] —with slight adaptations to our needs— we can inductively define type expressions as follows:

1. a basic type (such as boolean, char, integer, real) is a type expression;

2. there are type variables at will, each of them being a type expression;

3. if t is a type expression and n_{1}, n_{2} are natural numbers, then array(⟨n_{1},n_{2}⟩,t) is a type expression;

4. if t_{11}, …, t_{1m_{1}}, …, t_{n1}, …, t_{nm_{n}} are type expressions and i_{1}, …, i_{n} are field names (i.e. identifiers), then record({⟨i_{1}, {t_{11}, …, t_{1m_{1}}}⟩, …,⟨i_{n}, {t_{n1}, …, t_{nm_{n}}}⟩}) is a type expression;

5. if t is a type expression, then pointer(t) is a type expression.

Analogues of type expressions in our sense —and, in fact, of our ground type expressions— can be found in the declarations of a most typical programming language such as Pascal.^{12} We may think, for example, that the Pascal declaration type vector = array [1..10] of char binds the identifier vector to the type expression array(⟨1, 10⟩, char). The rationale for admitting type variables in the context of type-finding is that the problem, here, is to detect from the way constructs are used in a program the types of program Pascal-like program Type constraint

11A set {φ_{1}, ⋯, φ_{ℓ}} of formulae is being identified with the conjunction ⋀_{j=1}^{ℓ} φ_{j}, as usual.

12Our ongoing illustration is based on a Pascal-like language only for the purpose of readability: it is well-known that the applications of type-finding based on unification go well beyond the tiny example to be elaborated here, and that this approach does not presuppose the language, to which type-finding is applied, to be imperative.

new(p);  ⇒ P = pointer(P_{1}),
p↑.next := nil;  ⇒ P_{1} = record({⟨next,{P }⟩ | R_{1}}),
p↑.mode := true;  ⇒ P_{1} = record({⟨mode, {boolean | C_{1}}⟩ | R_{2}}),
p↑.date := 1965;  ⇒ P_{1} = record({⟨date, {integer | D_{1}}⟩ | R_{3}}),
new(q);  ⇒ Q = pointer(Q_{1}),
q↑.mode := false;  ⇒ Q_{1} = record({⟨mode, {boolean | C_{2}}⟩ | R_{4}}),
q↑.date := p;  ⇒ Q_{1} = record({⟨date, {P | D_{2}}⟩ | R_{5}}),
q↑.next := p;  ⇒ Q_{1} = record({⟨next,{Q}⟩ | R_{6}}),
P = Q

Figure 5: A type system in action

variables whose declarations are missing. An automatic inference process aimed at solving this, must somehow represent partially specified types. Hollow types, that is, type expressions involving variables, represent incompletely known types. Moreover, they can represent polymorphic data types.

Sets serve two purposes in the type language. As argument of the record constructor, a set reflects our intention to attribute no significance to the ordering of fields; for instance, both of the Pascal types

record next : list; data : char end  record data : char; next : list end

would be rendered by the same type expression in our framework.

Moreover, sets conveniently represent the union of types (the very same idea was exploited, e.g., in [33, 34]). In this brief discussion type union has a limited import, as we are using it only for multiply-valued record fields.

For recursive data types (such as lists or trees), a representation by rational terms is appropriate. For such a representation, Herbrand systems are, of course, very convenient.

A type constraint is a system of equations interrelating type expressions. Among others, a type system comprises rules for associating type constraints with the various parts of a program: it is in this fashion that specific instances of the type-finding problem are generated.

Figure 5 illustrates how a type solver works. For the sake of simplicity, we are only considering straight code inside a single procedure body, and our type analysis will be based on the following assumptions:

• next is a keyword, whose meaning is: the expression ⟨id⟩↑.next has the same data type as ⟨id⟩;

• the data type of the keyword nil matches any pointer data type.

P and Q represent the types of p and q, respectively.

Figure 6 shows a system in solvable form returned by the Hyper unify algorithm, upon elaboration of the type constraint above. One observes that recursive types are modeled through membership cycles.

P = pointer( record({
⟨next, {P }⟩,
⟨mode, {boolean | C_{1}}⟩,
⟨date, {integer, P | D_{1}}⟩,
| R_{1}}))
next mode date  ∘→ ; boolean ; integer  next mode date  ∘→ ; boolean ; ∘→

Figure 6: A solution to the type constraint

Acknowledgements

We are grateful to Giorgio Levi, who encouraged us in pursuing to an end the research reported in this paper.

We are much obliged to Gianfranco Rossi, whose qualified contribution emerges from a large part of the paper. Davide Aliffi and Enrico Pontelli actively contributed to the early phases of the discussion. Angelo Monti acted as a consultant on the complexity issues related to finite automata.

Partial funding came from the Italian National Research Council (CNR coordinated project SETA), from Compulog 2 (Esprit project 6810), from MURST 40% projects (Calcolo algebrico e simbolico, Logica matematica e applicazioni, Tecniche formali per la specifica, l’analisi, la verifica, la sintesi e la trasformazione di sistemi software), and from MURST 60% (Programmazione logica con insiemi).

References

[1] Aczel., P. Non-well-founded sets. Vol. 14 of Lecture Notes, Center for the Study of Language and Information. Stanford, 1988.

[2] Aho, A. V., Hopcroft, J. E., and Ullman, J. D. The Design and Analysis of Computer Algorithms. Addison-Wesley, 1974.

[3] Aho, A. V., Sethi, R., and Ullman, J. D. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1985.

[4] Arenas-Sánchez, P., and Dovier, A. A Minimality Study for Set Unification. The Journal of Functional and Logic Programming, 7, 1997.

[5] Baader, F., and Schulz, K. U. Unification Theory. In W. Bibel and P. H. Schmitt Eds., Automated Deduction: a basis for applications, Vol 1, Kluwer academic publisher, 1998.

[6] Barwise, J., and Moss, L. Hypersets. The Mathematical Intelligencer, 13(4) (1991), pp. 31–41.

[7] Barwise, J., and Moss, L. Vicious Circles: On the Mathematics of Non-Wellfounded Phenomena, Lecture Notes, Center for the Study of Language and Information. Stanford, 1996.

[8] Clark, K. L. Negation as Failure. In Logic and Databases, H. Gallaire and J. Minker, Eds., Plenum Press, 1978, pp. 293–321.

[9] Colmeraurer, A. Prolog and Infinite Trees. In Logic Programming, K. L. Clark and S.-Å. Tärnlund, Eds., Academic Press, New York, 1982, pp. 231–251.

[10] Comon, H., Dauchet, M., Gilleron, R., Lugiez, D., Tison, S., and Tommasi, M. Tree automata techniques and applications. (Forthcoming book).

[11] Cortesi, A., Dovier, A., Quintarelli, E., and Tanca, L. Operational and Abstract Semantics of a Query Language for Semi-Structured Information. In P. Fraternali, U. Geske, C. Ruiz, and D. Seipel, editors, Proceedings of 6th International Workshop on Deductive Databases and Logic Programming DDLP’98, pages 127–139. GMD Report 22, June 1998.

[12] Davis, M. D., Sigal, R., and Weyuker, E. J. Computability, complexity, and languages - Fundamentals of theoretical computer science. Academic Press, Computer Science ad scientific computing, 1994.

[13] Dovier, A. Computable Set Theory and Logic Programming. PhD thesis, University of Pisa, 1996.

[14] Dovier, A., Omodeo, E. G., Pontelli, E., and Rossi, G.-F. {log}: A Language for Programming in Logic with Finite Sets. The Journal of Logic Programming, 28(1), 1996, pp. 1-44.

[15] Garey, M. R., and Johnson, D. S. Computers and Intractability — A Guide to the Theory of NP-Completeness. W. H. Freeman and Company, New York, 1979.

[16] Gecseg, F., and Steinby, M. Tree automata. Akadmiai Kiado, Budapest, 1984.

[17] Hopcroft, J. E. An n log n algorithm for minimizing states in a finite automaton, In Kohavi and Paz eds., Theory of Machines and Computations. Academic Press, 1971, pp. 189–196.

[18] Hibti, M. Décidabilité et complexité de systèmes de contraintes ensemblistes. PhD thesis N.464, Université de Franche-Comté, 1995.

[19] Inverardi, P., and Nesi, M. Infinite Normal Forms for Non-Linear Term Rewriting Systems Theoretical Computer Science, 152(2): 285-303 (1995).

[20] Jones, N. D., and Lien, Y. E. New problems complete for nondeterministic log space, Mathematical Systems Theory, 10, 1976, pp. 1–17.

[21] Kapur D., and Narendran P. NP-Completeness of the Set Unification and Matching Problems. In J. H. Siekmann Ed., CADE 1986, LNCS 230, Springer Verlag, Berlin, pp. 489-495.

[22] Lisitsa, A. P., and Sazonov, V. Yu. Bounded hyperset theory and web-like data bases. In G. Gottlob, A. Leitsch, and D. Mundici, editors, Computational Logic and Proof Theory, 5th Kurt Gödel Colloquium, volume 1289 of LNCS, pages 172–185. Springer-Verlag, Berlin, 1997.

[23] Lloyd, J. W. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. Second edition.

[24] Maher, M. J. Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees. In Proceedings of 3^{rd} Symposium Logic in Computer Science (Edinburgh, 1988), pp. 349–357.

[25] Martelli, A., and Montanari, U. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems 4 (1982), pp. 258–282.

[26] Martelli, A., and Rossi, G. Stepwise Development of an Algorithm for Unification over Infinite Terms. Computers and Artificial Intelligence, 9(3), (1990), pp. 209–239.

[27] Mendelson, E. Introduction to Mathematical Logic. Van Nostrand, Princeton, N. J., 1979.

[28] Omodeo, E. G., and Policriti, A. Solvable set/hyperset contexts: I. Some decision procedures for the pure, finite case. Comm. Pure Appl. Math., 48(9/10) (special issue dedicated to J. T. Schwartz), 1995, pp. 1123–1155.

[29] Omodeo, E. G., and Policriti, A. Decision procedures for set/hyperset contexts. In Design and implementation of symbolic computation systems (1993), A. Miola, Ed., Vol. 722 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 192–215.

[30] Shepherdson, J. C. Negation in Logic Programming. In Foundations of Deductive Databases and Logic Programming, J. Minker, Ed., Morgan Kaufmann, 1988, pp. 19–88.

[31] Shmueli, O., Tsur, S., and Zaniolo, C. Compilation of Set Terms in the Logic Data Language (LDL). Journal of Logic Programming 12, 1 (1992), pp. 89–120.

[32] Stolzenburg, F. Membership-Constraint and Complexity in Logic Programming with Sets. In F. Baader and K. U. Schulz, editors, Proc. First Int’l Workshop on Frontier of Combining Systems, pages 285–302. Kluwer Academic Publishers, 1996.

[33] Tenenbaum, A. M. Type determination for very high level languages. Courant Computer Science Rep. 3, Courant Inst. of Mathematical Sciences, New York Univ., New York, 1974.

[34] Weiss, G. Recursive data types in SETL: automatic determination, data language description, and efficient implementation. Computer Science Dept., Tech. Rep. 201, Courant Inst. of Mathematical Sciences, New York Univ., New York, 1986.