1: \documentclass{tlp}
2: \usepackage{latexsym}
3: \usepackage{amssymb}
4: \begin{document}
5: \title[Three Optimisations for Sharing]
6: {Three Optimisations for Sharing}
7: \author[Jacob M.~Howe and Andy King]
8: {JACOB M.~HOWE\\
9: Department of Computing, City University,\\
10: London, EC1V OHB, UK. \\
11: email: \texttt{jacob@soi.city.ac.uk} \and
12: ANDY KING\\
13: Computing Laboratory,
14: University of Kent at Canterbury,\\
15: Canterbury, CT2~7NF, UK. \\
16: email: \texttt{a.m.king@ukc.ac.uk}}
17:
18: \maketitle
19:
20: \newtheorem{lemma}{Lemma}[section]
21: \newtheorem{proposition}{Proposition}[section]
22: \newtheorem{theorem}{Theorem}[section]
23: \newtheorem{corollary}{Corollary}[section]
24: \newtheorem{definition}{Definition}[section]
25: \newtheorem{example}{Example}[section]
26:
27: \def\Gr {Gr}
28: \def\Share {Sh}
29: \def\Free {Fr}
30: \def\Lin {Lin}
31: \def\nat {\mathbb{N}}
32: \def\opp {-}
33: \def\shr {\sim}
34: \def\reduce{\leadsto}
35:
36: \def\myshare {\mbox{\it Sharing\/}}
37: \def\mymodel {\mbox{\it model\/}}
38: \def\mybool {\mbox{\it Bool\/}}
39: \def\mypos {\mbox{\it Pos\/}}
40:
41: \begin{abstract}
42: In order to improve precision and efficiency sharing analysis
43: should track both freeness and linearity. The abstract unification
44: algorithms for these combined domains are suboptimal, hence there
45: is scope for improving precision. This paper proposes three
46: optimisations for tracing sharing in combination with
47: freeness and linearity.
48: A novel connection between equations and sharing
49: abstractions is used to establish correctness
50: of these optimisations even in the presence of rational trees.
51: A method for pruning intermediate
52: sharing abstractions to improve efficiency is also proposed. The
53: optimisations are lightweight
54: and therefore
55: some, if not all, of these optimisations will be of interest to the
56: implementor.
57:
58: \noindent Keywords: Abstract interpretation, sharing analysis,
59: freeness, linearity and rational trees.
60: \end{abstract}
61:
62: \section{Introduction}
63:
64: A set-sharing analyser will usually also track freeness and
65: linearity. This is because freeness and linearity are cheap to
66: maintain and result in more accurate, that is smaller, sharing
67: abstractions which in turn improve the efficiency of the sharing
68: component of abstract unification. However, current abstract
69: unification algorithms for sharing, freeness and linearity are
70: suboptimal. This paper considers how to improve the precision of
71: sharing with freeness and linearity by considering the interaction
72: of these components. These refinements do not incur a significant
73: computational overhead. To this end three optimisations are
74: given, along with examples of where precision is gained. Their
75: cost is discussed and correctness proved.
76:
77: The first optimisation follows from the observation that the
78: algorithms for pair-sharing with linearity can sometimes
79: out perform set-sharing with linearity (in terms of which pairs of
80: variables may share). This is because of an independence check
81: which pervades the set-sharing literature (from early work
82: \cite{L91} to the most recent and comprehensive \cite{BZH00}).
83: This check is in fact redundant. By removing this,
84: the precision of abstract unification is improved, since
85: linearity can be exploited more frequently.
86:
87: Fil{\'e} \cite{F94} observed that freeness can be used to
88: decompose a sharing abstraction into a set of sharing abstractions.
89: For each component of the decomposition, the sharing groups of
90: that component do not (definitely) arise from different computational
91: paths. Abstract unification can then be
92: applied to each component and the resulting abstractions merged.
93: This tactic has not been included in analysers owing to its
94: prohibitive cost. The second optimisation is a lightweight
95: refinement of abstract unification inspired by the decomposition.
96: Though not as precise as the full decomposition, it does achieve
97: the necessary balance between cost and benefit.
98:
99: Thirdly, an optimisation for pruning sharing groups is presented.
100: This tactic demonstrates that sharing in combination with freeness
101: can improve groundness which, in turn, can improve sharing (even
102: in the presence of rational trees). Put another way, it means that
103: any optimal algorithm for sharing, freeness and linearity will
104: have to consider subtle interactions between sharing, freeness and
105: groundness.
106:
107: One principle of set-sharing is that the number of sharing groups
108: should be minimised. As well as increasing precision, this can
109: improve efficiency and possibly avoid widening. A fourth technique
110: is proposed which can prune the size of inputs to the
111: abstract unification algorithm by considering the grounding
112: behaviour of sets of equations. Reducing the size of the inputs
113: (and intermediate abstractions) simplifies abstract unification
114: and can thereby improve performance. Whilst the technique will
115: not theoretically
116: improve the precision of the overall result, in practice,
117: a precision gain might be
118: achieved if widening is avoided within the unification algorithm.
119:
120: Correctness is expressed in terms of a
121: novel concretisation map which characterises equations as their
122: idempotent most general unifiers. This simplifies the correctness
123: arguments and in particular enables the
124: abstract unification algorithms to be proved correct
125: for rational tree constraint solving (as adopted by SICStus
126: Prolog and Prolog-III).
127: To the best of the authors' knowledge, this is the
128: first proof of correctness for a sharing, freeness and linearity
129: analysis in the presence of rational trees. (Previous work
130: for rational tree unification has either focused
131: on pair-sharing \cite{K00} or set-sharing without freeness and linearity
132: \cite{HBZ02}).
133:
134: In summary, this paper
135: provides the implementor with a
136: number of low-cost techniques for improving the precision and
137: efficiency of sharing analyses.
138:
139: \section{Preliminaries}
140:
141: \subsection{Trees and terms}
142:
143: Let $\varepsilon$ denote the empty sequence, $.$ denote sequence
144: concatenation, and $\|\alpha\|$ denote the length of a sequence
145: $\alpha \in \nat^{*}$. A tree (or term) over an alphabet of
146: symbols $F$ is a partial map $t : \nat^{*} \to F$ such that
147: $t(\alpha) = t$ if $\alpha = \varepsilon$, otherwise $t(\alpha) =
148: {t_i}(\beta)$ where $\alpha = i . \beta$ and $t = f(t_1, \ldots,
149: t_n)$. Let $T(F)$ and $T^{\infty}(F)$ denote the set of finite and
150: possibly infinite trees over $F$. Let $U$ denote a (denumerable)
151: universe of variables such that $F \cap U = \emptyset$, and let
152: $var(t)$ = $\{ u \in U \mid \exists \alpha \in \nat^{*} .
153: t(\alpha) = u \}$ where $t \in T^{\infty}(F \cup U)$. Finally,
154: $|S|$ denotes the cardinality of the set $S$.
155:
156: \subsection{Substitutions and equations}
157:
158: A substitution is a (total) map $\theta : U \to T^{\infty}(F \cup
159: U)$ such that $dom(\theta)$ = \linebreak \mbox{$\{ u \in U \mid
160: \theta(u) \neq u \}$} is finite. A substitution $\theta$ can be
161: represented as a finite set $\{ x \mapsto \theta(x) \mid
162: x \in dom(\theta) \}$. Let $rng(\theta)$ = $\cup \{
163: var(\theta(u)) \mid u \in dom(\theta) \}$ and let $Sub$ denote the
164: set of substitutions. If $\theta = \{ x_i \mapsto t_i
165: \}_{i=1}^{n}$ then $\theta(t)$ denotes the tree obtained by
166: simultaneously replacing each occurrence of $x_i$ in $t$ with
167: $t_i$. For brevity, let $\theta(x, \alpha)$ = $t(\alpha)$ where
168: $\theta(x)$ = $t$. An equation $e$ is a pair $(s = t)$ where $s, t
169: \in T^{\infty}(F \cup U)$. A finite set of equations is denoted $E$ and
170: $Eqn$ denotes the set of finite sets of equations. Also define
171: $\theta(E)$ = $\{ \theta(s) = \theta(t) \mid (s = t) \in E \}$.
172: The map $eqn : Sub \to Eqn$ is defined $eqn(\theta)$ = $\{ x = t
173: \mid (x \mapsto t) \in \theta \}$. Where $Y \subseteq U$,
174: projection out and projection onto are respectively defined
175: $\exists Y . \theta$ = $\{ x \mapsto t \in \theta \mid x \not\in Y
176: \}$ and $\overline{\exists} Y . \theta$ = $\exists (U \setminus Y)
177: . \theta$. Composition $\theta \circ \psi$ of two substitutions is
178: defined so that $(\theta \circ \psi)(u) = \theta(\psi(u))$ for
179: all $u \in U$. Composition induces the (more general than)
180: relation $\leq$ defined by $\theta \leq \psi$ iff there exists
181: $\delta \in Sub$ such that $\psi = \delta \circ \theta$. A
182: renaming is a substitution $\rho \in Sub$ that has an inverse,
183: that is, there exists $\rho^{-1} \in Sub$ such that $\rho^{-1}
184: \circ \rho = id$. The set of renamings is denoted $Rename$. A
185: substitution $\theta$ is idempotent iff $\theta \circ \theta =
186: \theta$, or equivalently, iff $dom(\theta) \cap rng(\theta) =
187: \emptyset$.
188:
189: \subsection{Solved forms and most general unifiers}
190:
191: A substitution is in rational solved form iff it has no subset $\{
192: x_1 \mapsto x_2$, $\ldots$, $x_n \mapsto x_1 \}$ where $n \geq 2$.
193: The subset of $Sub$ in rational solved form is denoted $RSub$. The
194: set of unifiers of $E$ is defined by: $unify(E)$ = $\{ \theta \in
195: Sub \mid \forall (s = t) \in E . \theta(s) = \theta(t) \}$. The
196: set of most general unifiers (mgus) and the set of idempotent mgus (imgus)
197: are defined: $mgu(E) = \{ \theta
198: \in unify(E) \mid \forall \psi \in unify(E) . \theta \leq \psi \}$
199: and $imgu(E) = \{ \theta \in mgu(E) \mid dom(\theta) \cap
200: rng(\theta) = \emptyset \}$. Note that $imgu(E) \neq \emptyset$ iff
201: $mgu(E) \neq \emptyset$ \cite{LMM88}. An mgu can
202: be renamed to obtain any other (as can an imgu).
203:
204: \begin{lemma}[\rm Proposition~11 from \cite{LMM88}]\label{lemma-lassez}
205: Let $\theta \in imgu(E)$. Then $\phi \in imgu(E)$ iff there exists
206: $\{ x_i \mapsto y_i \}_{i = 1}^{n} \subseteq \theta$ such that
207: $\phi = \{ x_i \mapsto y_i, y_i \mapsto x_i \}_{i = 1}^{n} \circ
208: \theta$.
209: \end{lemma}
210:
211: \noindent One way to obtain an imgu is by considering
212: limits of substitutions.
213:
214: \begin{definition}\label{defn-limits} \rm
215: Let $\{ t_{n} \mid n \in \nat \} \subseteq T^{\infty}(F \cup U)$.
216: Then $t = \lim_{n \to \infty} t_{n}$ iff for all $k \in \nat$
217: there exists $l \in \nat$ such that
218: for all $m \geq l$ and $\|\alpha\| \leq k$,
219: $t(\alpha) = {t_m}(\alpha)$. Furthermore, if $\{
220: \theta_{n} \mid n \in \nat \} \subseteq Sub$ then $\lim_{n \to
221: \infty} \theta_{n} = \lambda x . \lim_{n \to \infty}
222: {\theta_{n}}(x)$.
223: \end{definition}
224:
225: \noindent Note that $\lim_{n \to \infty} \theta^{n}$ exists iff
226: $\theta \in RSub$ \cite{K00}. Henceforth $\theta^\infty$
227: abbreviates $\lim_{n \to \infty} \theta^{n}$. If $\theta \in RSub$
228: then $\theta^\infty$ is idempotent whereas if $\theta$ is
229: idempotent then $\theta^\infty = \theta$. The following lemmas
230: detail how limits of substitutions and composition of
231: substitutions relate to an mgu.
232:
233: \begin{lemma}[\rm Lemmas~2.2, 4.3 and 4.4 from \cite{K00}]\label{lemma-subs}
234: \rm
235: \begin{enumerate}
236:
237: \item\label{case-one}
238: $\theta^{\infty} \in mgu(eqn(\theta))$ if $\theta \in RSub$.
239:
240: \item\label{case-two}
241: $\delta \circ \theta^{\infty} \in mgu(E \cup eqn(\theta))$
242: if $\delta \in mgu({\theta^{\infty}}(E))$.
243:
244: \item\label{case-three}
245: $\exists (dom(\theta) \setminus rng(\theta)) . \delta \in
246: mgu({\theta}(E))$
247: if $\delta \circ \theta \in mgu(E)$.
248:
249: \end{enumerate}
250: \end{lemma}
251:
252:
253: \subsection{Linearity}
254:
255: Variable multiplicity is defined in order to formalise
256: linearity. The significance of linearity is that
257: unification of linear terms enables sharing to
258: be described by more precise sharing
259: abstractions (even in the presence of rational trees).
260:
261: \begin{definition} \rm
262: The variable multiplicity map $\chi : T^{\infty}(F \cup U) \to
263: \{0, 1, 2\}$ is defined: $\chi(t) = \max(\{ \chi(x, t) \mid x \in
264: U \})$ where $\chi(x, t) = \min(2, |\{ \alpha \mid t(\alpha) =
265: x\}|)$.
266: \end{definition}
267:
268: \noindent If $\chi(t) = 0$, $t$ is ground; if $\chi(t) = 1$, $t$
269: is linear; and if $\chi(t) = 2$, $t$ is non-linear. The next
270: lemma details the forms of sharing barred by the unification of
271: linear terms.
272:
273: \begin{lemma}[Proposition 3.1 from \cite{K00}]\label{lemma-original-linearity} \rm
274: If $\theta \in mgu(\{s = t\})$, $x \neq y$ and $var(\theta(x))
275: \cap var(\theta(y)) \neq \emptyset$ then either: $x \in var(s)$
276: and $y \in var(t)$; or $x, y \in var(t)$ and $\chi(s) = 2$; or $x
277: \in var(t)$ and $y \in var(s)$; or $x, y \in var(s)$ and $\chi(t)
278: = 2$.
279: \end{lemma}
280:
281: \noindent The correctness arguments for abstract unification
282: require lemma~\ref{lemma-original-linearity} to be augmented with
283: a new result -- lemma~\ref{lemma-new-linearity}. The proof of this
284: lemma is analogous to that of lemma~\ref{lemma-original-linearity}
285: detailed in \cite{K00}.
286:
287: %\begin{definition}[\rm Alternating paths]
288: %If $E \in Eqn$, then the binary relations $\opp_{E}, \shr_{E} \,
289: %\subseteq (E \times \nat^{*})^2$ are the least symmetric relations
290: %such that:
291: %\begin{enumerate}
292: %
293: %\item
294: %$\langle e, 1.{\alpha_1} \rangle \opp_{E} \langle e, 2.{\alpha_2}
295: %\rangle$ if $e \in E$, $e(1.{\alpha_1}) \in U$ and
296: %$e(2.{\alpha_2}) \in U$
297: %
298: %\item
299: %$\langle e_1, {\alpha_1} \rangle \shr_{E} \langle e_2, {\alpha_2}
300: %\rangle$ if $e_1, e_2 \in E$, ${e_1}(\alpha_1) = {e_2}(\alpha_2)
301: %\in U$ and ($e_1 \neq e_2$ or $\alpha_1 \neq \alpha_2$).
302: %
303: %\end{enumerate}
304: %
305: %\noindent where $e(1.\alpha) = s(\alpha)$ and $e(2.\alpha) =
306: %t(\alpha)$ if $e = (s = t)$. A sequence ${\langle e_{1},
307: %\alpha_{1} \rangle}. {\langle e_{1}, \beta_{1} \rangle} \ldots$
308: %${\langle e_{n}, \alpha_{n} \rangle}. {\langle e_{n}, \beta_{n}
309: %\rangle} \in APath_{E}$ iff $\langle e_{i}, \alpha_{i} \rangle
310: %\opp_{E} \langle e_{i}, \beta_{i} \rangle$ for all $1 \leq i \leq
311: %n$ and $\langle e_{i}, \beta_{i} \rangle \shr_{E} \langle e_{i+1},
312: %\alpha_{i+1} \rangle$ for all $1 \leq i < n$ where $n \in \nat$.
313: %\end{definition}
314: %
315: %\noindent One key result on alternating paths is that a rational
316: %solved form $\theta$ exists for an equation $E$ (if one exists at
317: %all) whose alternating paths all occur in $E$. Specifically, if
318: %there exists an alternating path in $\theta$ whose ends points
319: %connect the variables $x$ and $y$, then the same must be true of
320: %$E$. This is formalised below.
321: %
322: %\begin{lemma}[\rm Lemmas 3.1 and 3.2 from \cite{K00}]\label{lemma-linearity} \rm
323: %\begin{enumerate}
324: %
325: %\item\label{case-another}
326: %Let $E \in Eqn$ and $unify(E) \neq \emptyset$. There exists
327: %$\theta \in RSub$ such that $mgu(E) = mgu(eqn(\theta))$. Moreover,
328: %if $\langle {e_{1}}', {\alpha_{1}}' \rangle \ldots \langle
329: %{e_{m}}', {\beta_{m}}' \rangle \in APath_{eqn(\theta)}$, there
330: %exists $\langle e_{1}, \alpha_{1} \rangle \ldots \langle e_{n},
331: %\beta_{n} \rangle \in APath_{E}$ with $e_{1}(\alpha_{1}) =
332: %{e_{1}}'({\alpha_{1}}')$ and $e_{n}(\beta_{n}) =
333: %{e_{m}}'({\beta_{m}}')$.
334: %
335: %\item\label{case-yet-another}
336: %If $\langle e, \alpha_{1} \rangle$ $\ldots$ $\langle e, \beta_{n}
337: %\rangle \in APath_{\{e\}}$ where $e = (s = t)$ then either:
338: %$\alpha_1 = 1.\alpha$ and $\beta_n = 2.\beta$; or $\alpha_1 =
339: %2.\alpha$, $\beta_n = 2.\beta$ and $\chi(s) = 2$; or $\alpha_1 =
340: %2.\alpha$ and $\beta_n = 1.\beta$; or $\alpha_1 = 1.\alpha$,
341: %$\beta_n = 1.\beta$ and $\chi(t) = 2$.
342: %
343: %\end{enumerate}
344: %\end{lemma}
345: %
346: %\noindent For brevity (to avoid detailing a solved form algorithm)
347: %part~\ref{case-another} is presented slightly differently from
348: %Lemma 3.1 of \cite{K00}. Part~\ref{case-another} and
349: %part~\ref{case-yet-another} provide the building blocks for the
350: %following lemma which details how non-linearity arises.
351:
352: \begin{lemma}\label{lemma-new-linearity} \rm
353: If $\theta \in mgu(\{s = t\})$ and $\chi(\theta(x)) = 2$ then
354: either: $x \in var(s) \cap var(t)$; or $x \in var(t)$ and $\chi(s)
355: = 2$; or $x \in var(s)$ and $\chi(t) = 2$.
356: \end{lemma}
357:
358: %\begin{proof}
359: %Let $E = \{ s = t \}$. By part~\ref{case-another} of
360: %lemma~\ref{lemma-linearity}, there exists $\psi \in RSub$ such
361: %that $mgu(E) = mgu(eqn(\psi))$. By part~\ref{case-one} of
362: %lemma~\ref{lemma-subs}, $\psi^{\infty} \in mgu(E)$, thus there
363: %exists $\rho \in Rename$ such that $\rho \circ \theta =
364: %\psi^{\infty}$. Hence $\chi({\psi^{\infty}}(x)) = 2$ and therefore
365: %there exists $y \in U$ and $\beta \neq \beta'$ such that
366: %${\psi^{\infty}}(x, \beta) = y = {\psi^{\infty}}(x, \beta')$.
367: %There exists $m \in \nat$ such that ${\psi^{m}}(x, \beta) = y =
368: %{\psi^{m}}(x, \beta')$. Thus there exists ${e_1}' = (x = t_1)$,
369: %${e_2}' = (x_2 = t_2)$, \ldots, ${e_m}' = (x_m = t_m)$, ${e_1}'' =
370: %(x = t'_1)$, ${e_2}'' = (x'_2 = t'_2)$, \ldots, ${e_m}'' = (x'_m =
371: %t'_m) \in eqn(\psi)$ where $t_1(\beta_1) = x_2$, \ldots,
372: %$t_{m-1}(\beta_{m-1}) = x_m$, $t_m(\beta_m) = y$, $t_1'(\beta_1')
373: %= x'_2$, \ldots, $t'_{m-1}(\beta'_{m-1}) = x'_m$, $t'_m(\beta'_w)
374: %= y$, $\beta = \beta_m$ and $\beta' = \beta'_m$. Hence $\langle
375: %{e_1}', 1 \rangle. \langle {e_1}', 2.\beta_1 \rangle$ $\ldots$
376: %$\langle {e_m}', 1 \rangle. \langle {e_m}', 2.\beta \rangle.
377: %\langle {e_m}'', 2.\beta' \rangle. \langle {e_m}'', 1 \rangle$
378: %$\ldots$ $\langle {e_1}'', 2.\beta'_1 \rangle. \langle {e_1}'', 1
379: %\rangle \in APath_{eqn(\psi)}$. By part~\ref{case-another} of
380: %lemma~\ref{lemma-linearity}, there exists $\langle e_{1},
381: %\alpha_{1} \rangle$ $\ldots$ $\langle e_{n}, \beta_{n} \rangle \in
382: %APath_{\{ s = t \}}$ with $e_{1}(\alpha_1) = x = {e_n}(\beta_n)$.
383: %The result follows by part~\ref{case-yet-another} of
384: %lemma~\ref{lemma-linearity}.
385: %\end{proof}
386:
387: \subsection{Groundness and sharing abstractions}
388:
389: The abstract domains of interest in this paper
390: are represented either as Boolean functions, or
391: as sets or as sets of sets. Let $X$ denote a finite subset of $U$.
392: The set of
393: propositional formulae over $X$ is denoted by $\mybool_X$
394: and $Y$
395: abbreviates the formula $\wedge Y$.
396: The (bijective) map
397: ${\mymodel_X} : \mybool_X \to \wp(\wp(X))$ is defined by
398: ${\mymodel_X}(f) =
399: \{ M \! \subseteq \! X \! \mid \! {\psi_X}(M) \models f \}$
400: where
401: ${\psi_X}(M) = M \land \land \{ \neg y \mid y \in X \! \setminus \! M \}$.
402: The groundness, sharing, freeness and linearity domains over $X$
403: are defined as follows:
404:
405: \begin{definition}
406: $Pos_{X}$ = $\{ f \in Bool_X \mid X \models f \}$, $\Share_{X}$ =
407: $\{ S \subseteq \wp(X) \mid \emptyset \in S \}$, $\Free_{X}$ =
408: $\wp(X)$ and $\Lin_{X}$ = $\wp(X)$.
409: \end{definition}
410:
411: \noindent If $S \in \Share_X$, then each $G \in S$ is referred
412: to as a sharing group.
413:
414: These domains are connected to the concrete domain of
415: sets of equations by Galois connections induced
416: by the concretisation maps.
417: This approach leads to
418: succinct statements of correctness. To obtain well defined
419: concretisations,
420: maps abstracting substitutions are introduced. It is then
421: observed that the abstractions for
422: equivalent idempotent substitutions are the same.
423:
424: \begin{definition} The abstraction maps $\alpha^{Pos} : Sub \to Pos_{U}$
425: and $\alpha^{\Share}_X : Sub \to \Share_{X}$ are defined:
426: $\alpha^{Pos}(\theta)$ = $\wedge \{ x \leftrightarrow var(t) \!
427: \mid \! x \mapsto t \in \theta \}$, $\alpha^{\Share}_X(\theta)$ =
428: $\{ occ(\theta, u) \cap X \mid u \in U \}$ and $occ(\theta, y) =
429: \{ u \in U \mid y \in var(\theta(u)) \}$.
430: \end{definition}
431:
432: \begin{lemma} Let $\theta, \phi \in imgu(E)$. Then
433: $\alpha^{Pos}(\theta) = \alpha^{Pos}(\phi)$,
434: $\alpha^{\Share}_X(\theta) = \alpha^{\Share}_X(\phi)$, $\theta(x)
435: \in U$ iff $\phi(x) \in U$ and $\chi(\theta(x)) \leq 1$ iff
436: $\chi(\phi(x)) \leq 1$.
437: \end{lemma}
438:
439: \begin{proof} By lemma~\ref{lemma-lassez} there exists
440: $\{ x_i \mapsto y_i \}_{i = 1}^{n} \subseteq \theta$ such that
441: $\phi = \rho \circ \theta$ where $\rho = \{ x_i \mapsto y_i, y_i
442: \mapsto x_i \}_{i = 1}^{n}$.
443: \begin{enumerate}
444:
445: \item Let $x \mapsto t \in \theta$.
446: Observe that
447: $\{ x \mapsto \rho(t), y_1 \mapsto x_1, \ldots, y_n \mapsto x_n \} \subseteq \rho \circ \theta$ and $y_i \in var(t)$ iff $x_i \in var(\rho(t))$, thus
448: $\alpha^{Pos}(\phi) \models x \leftrightarrow var(\rho(t))
449: \wedge (\wedge_{i=1}^{n} y_i \leftrightarrow x_i) \models x
450: \leftrightarrow var(t)$. Hence $\alpha^{Pos}(\phi) \models
451: \alpha^{Pos}(\theta)$. The other direction is similar.
452:
453: \item Observe that $occ(\rho \circ \theta, y_i) = occ(\theta, x_i)$,
454: $occ(\rho \circ \theta, x_i) = occ(\theta, y_i)$ and $occ(\rho
455: \circ \theta, u)$ = $occ(\theta, u)$ for all $u \not\in dom(\rho)
456: \cup rng(\rho)$. Hence $\alpha^{\Share}_X(\theta) =
457: \alpha^{\Share}_X(\phi)$.
458:
459: \item and 4. Immediate.
460:
461: \end{enumerate}
462: \end{proof}
463:
464: %If $unify(E) \subseteq unify(E')$ then $\alpha^{Pos}(E) \models
465: %\alpha^{Pos}(E')$.
466:
467: \noindent Instead of defining concretisation in terms
468: of a particular imgu (the limit of
469: a rational solved form \cite{K00}), an
470: arbitrary imgu is used. This new approach simplifies
471: correctness proofs.
472:
473: \begin{definition}\label{defn-concrete}
474: The concretisation maps \mbox{${\gamma^{Pos}_X} : Pos_X \to
475: \wp(Eqn)$}, \mbox{${\gamma^{\Share}_X} : \Share_X \to \wp(Eqn)$},
476: \linebreak \mbox{${\gamma^{\Free}_X} : \Free_X \to \wp(Eqn)$} and
477: \mbox{${\gamma^{\Lin}_X} : \Lin_X \to \wp(Eqn)$} are respectively
478: defined by:
479: \[ \begin{array}{r@{\; = \;}l}
480: {\gamma^{Pos}_X}(f) & \{ E \in Eqn \mid \exists \theta \in imgu(E)
481: . \alpha^{Pos}(\theta) \models f \}
482: \\
483: \gamma^{\Share}_{X}(S) & \{ E \in Eqn \mid \exists \theta \in
484: imgu(E) . \alpha^{\Share}_X(\theta) \subseteq S \}
485: \\
486: {\gamma^{\Free}_X}(F) & \{ E \in Eqn \mid \exists \theta \in
487: imgu(E) . \forall x \in F . \, \theta(x) \in U \}
488: \\
489: {\gamma^{\Lin}_X}(L) & \{ E \in Eqn \mid \exists \theta \in
490: imgu(E) . \forall x \in L . \chi(\theta(x)) \leq 1 \}
491: \end{array} \]
492: \end{definition}
493:
494: \noindent Each free variable is linear so that
495: $\gamma^{\Free}_X(F) \cap \gamma^{\Lin}_X(L)$ =
496: $\gamma^{\Free}_X(F) \cap \gamma^{\Lin}_X(L \cup F)$.
497: This paper
498: is concerned with combined domains and the following combined
499: concretisation maps will be useful: $\gamma_X^{SF}(\langle S, F
500: \rangle) = \gamma^{\Share}_X(S) \cap \gamma^{\Free}_X(F)$ and
501: $\gamma^{SFL}_X(\langle S, F, L \rangle)$ = $\gamma^{SF}_X(\langle
502: S, F \rangle) \cap \gamma^{\Lin}_X(L)$.
503:
504: A connection is established in \cite{CSS99} which sheds light on
505: the relationship between sharing and Boolean functions. The
506: corollary (also observed in the long version of \cite{BZH00})
507: explains how this can be used to improve precision of combined
508: domains.
509:
510: \begin{lemma}[\rm Observation~4.1 and lemma 5.1 from
511: \cite{CSS99}]\label{lemma-codish} $\{X \setminus G \mid G\in
512: \alpha^{\Share}_X(\theta)\} \subseteq
513: model_X(\alpha^{Pos}(\theta))$ where $\theta$ is idempotent.
514: \end{lemma}
515:
516: \begin{corollary}\label{cor-trim}
517: $\gamma^{Pos}_{X}(f) \cap \gamma^{\Share}_{X}(S) =
518: \gamma^{Pos}_{X}(f) \cap \gamma^{\Share}_{X}(trim_{X}(f, S))$
519: where $trim_X(f, S) = \{ G \in S \! \mid \! X \setminus G \in
520: model_{X}(f) \}$.
521: \end{corollary}
522:
523: Finally, the following auxiliary operations will be
524: used throughout the paper. Let $S, S_i \in \Share_X$. The relevance map is defined
525: $rel(t, S) = \{ G \in S | var(t) \cap G \neq \emptyset \}$;
526: closure is defined $S^{*} = \cap \{ S' \mid S \subseteq S' \wedge
527: \forall G_1, G_2 \in S' . G_1 \cup G_2 \in S' \}$; and pair-wise
528: union is defined $S_1 \uplus S_2 = \{ G_1 \cup G_2 \mid G_1 \in
529: S_1 \wedge G_2 \in S_2 \}$.
530: Observe that if
531: $var(rel(s, S)) \cap var(rel(t, S)) = \emptyset$
532: then $var(\theta(s)) \cap var(\theta(t)) = \emptyset$
533: for all $\theta \in imgu(E)$ and $E \in
534: \gamma^{\Share}_{X}(S)$. Thus the
535: independence check $var(rel(s, S)) \cap var(rel(t, S)) = \emptyset$
536: can verify that two
537: terms $s$ and $t$ do not
538: share under $\theta$ (or equivalently $E$).
539:
540: \section{Independence check in set-sharing}
541:
542: The following example demonstrates that pair-sharing can
543: sometimes detect independence when standard set-sharing
544: unification algorithms cannot.
545:
546: \begin{example}\label{exam-independence} Let
547: $X = \{ u, v, w, x, y, z \}$ and consider $E \in
548: \gamma_X^{SFL}(\langle S, F, L \rangle)$ where $S = \{ \emptyset,
549: \{ u, w \}$, $\{ v, w \}$, $\{ x, y \}$, $\{ x, z \}$, $\{ w, x
550: \}\}$, $F = \emptyset$ and $L = X$. Let $\theta' \in imgu(E \cup
551: \{ w = x \})$. The set-sharing unification algorithms of
552: \cite{L91,BZH00} give the following abstraction $S' = \{ \emptyset
553: \} \cup (S_w^{*} \uplus S_x^{*})$ for $\theta'$ where $S_w = \{ \{
554: u, w \}, \{ v, w \}, \{ w, x \}\}$ and $S_x = \{ \{ x, y \}, \{ x,
555: z \}, \{ w, x \}\}$. Observe that $\{ u, v, w \} \in S_w^{*}$ and
556: $\{ x,y,z \} \in S_x^{*}$ and therefore $S'$ does not assert the
557: independence of $u$ and $v$ (similarly $y$ and $z$). However, if
558: $S$ is interpreted as a set of pairs, then the pair-sharing
559: abstract unification algorithms of \cite{CDY91,K00} both give the
560: abstraction $S \cup \{ \{ w \}, \{ x \}, \{ u, x \}, \{ u, y \},
561: \{ u, z \}, \{ v, x \}, \{ v, y \}, \{ v, z \}, \{ w, y \}, \{ w,
562: z \} \}$ which states the independence of $u$ and $v$ (and
563: similarly $y$ and $z$). Note that this different does not stem
564: from a difference in the set-sharing and pair-sharing
565: \textit{domains}, but derives from the way in which linearity is
566: exploited in the abstract unification \textit{algorithms}.
567: \end{example}
568:
569: \noindent The crucial difference between pair-sharing and
570: set-sharing algorithms is that the former does not require the
571: terms in the equation to be independent to exploit linearity. Put
572: another way, to apply linearity the latter requires that
573: $var(rel(s, S)) \cap var(rel(t, S)) = \emptyset$ when solving
574: the equation $s = t$ in the context of the sharing abstraction $S$.
575: Lemmas~\ref{lemma-original-linearity}
576: and \ref{lemma-new-linearity} detail the forms of sharing that can
577: arise in $mgu(\{ s' = t' \})$ rational (and finite) tree
578: unification where $s'$ and $t'$ are arbitrary terms.
579: Observe that $s'$ and $t'$ are not required to be
580: independent. Abstract unification algorithms with the independence
581: check are safe. However, this check is not fundamental to
582: combining sharing with linearity. By observing how to exploit
583: linearity more fully, a more precise abstract unification
584: algorithm can be obtained. This algorithm also explains why
585: algorithms with the independence check are safe. The following
586: abstract operator is used to approximate the multiplicity map in
587: abstract unification. Lemma~\ref{lemma-chi} asserts its
588: correctness.
589:
590: \begin{definition}
591: \[
592: \chi(t, S, L) = \left\{ \begin{array}{ll@{\,}c@{\,}r@{}l}
593: 2 & \mathrm{if} \; \exists x & \in & var(S) & . \chi(x, t) = 2 \\
594: 2 & \mathrm{if} \; \exists x & \in & var(S) & . x \in var(t) \setminus L \\
595: 2 & \mathrm{if} \; \exists x, y & \in & var(t) & . \exists G \in S
596: . x \neq y \wedge x, y \in G \\
597: 1 & \multicolumn{4}{l}{\mathrm{otherwise}}
598: \end{array} \right.
599: \]
600: \end{definition}
601:
602: \begin{lemma}\label{lemma-chi} \rm If $E \in \gamma^{\Share}_X(S) \cap
603: \gamma^{\Lin}_X(L)$ and $\theta \in imgu(E)$ then $\chi(\theta(t))
604: \leq \chi(t, S, L)$.
605: \end{lemma}
606:
607: \newpage
608:
609: \begin{proof} Suppose $\chi(\theta(t)) = 2$. One of the
610: following holds:
611: \begin{itemize}
612:
613: \item There exists $x \in var(t)$ such that $\chi(x, t) = 2$ and
614: $var(\theta(x)) \neq \emptyset$. Then \mbox{$x \in var(S)$} so
615: that $\chi(t, S, L) = 2$.
616:
617: \item There exists $x \in var(t)$ such that $\chi(\theta(x)) = 2$.
618: Then $x \in var(S)$ and \linebreak $x \in var(t) \setminus L$ so
619: that $\chi(t, S, L) = 2$.
620:
621: \item There exist $x, y \in var(t)$ such that $x \neq y$
622: and $var(\theta(x)) \cap var(\theta(y)) \neq \emptyset$. Then
623: there exists $G \in S$ such that $x, y \in G$ so that $\chi(t, S,
624: L) = 2$.
625:
626: \end{itemize}
627: \end{proof}
628:
629: \noindent The revised abstract unification algorithm (with the
630: independence check removed) is detailed in
631: definition~\ref{defn-amgu}, and
632: theorem~\ref{theorem-amgu-correct}
633: establishes its correctness.
634:
635: \begin{definition}[Abstract unification 1]\label{defn-amgu}
636: Abstract unification
637: $amgu_1(\langle S, F, L \rangle, s, t) = \langle S', F', L' \rangle$
638: is defined:
639: \[
640: S_s = rel(s, S) \quad S_t = rel(t, S) \quad S' = (S \setminus (S_s
641: \cup S_t)) \cup S'' \quad G' = X \setminus var(S')
642: \]
643: \[
644: S'' = \left\{ \begin{array}{r@{\,}c@{\,}ll}
645: S_s & \uplus & S_t & \mathrm{if} \; s \in F \vee t \in F \\
646: (S_s^{*} \uplus S_t) & \cap & (S_s \uplus S_t^{*}) & \mathrm{if} \; \chi(s, S, L) = \chi(t, S, L) = 1 \\
647: S_s^{*} & \uplus & S_t & \mathrm{if} \; \chi(s, S, L) = 1 \\
648: S_s & \uplus & S_t^{*} & \mathrm{if} \; \chi(t, S, L) = 1 \\
649: S_s^{*} & \uplus & S_t^{*} & \mathrm{otherwise}
650: \end{array} \right.
651: \] \[
652: F' = \left\{ \begin{array}{ll}
653: F & \mathrm{if} \; s \in F \wedge t \in F \\
654: F \setminus var(S_s) & \mathrm{if} \; s \in F \\
655: F \setminus var(S_t) & \mathrm{if} \; t \in F \\
656: F \setminus var(S_s \cup S_t) & \mathrm{otherwise}
657: \end{array} \right.
658: \] \[
659: L' = F' \cup G' \cup \left\{ \begin{array}{ll} L \setminus
660: (var(S_s) \cap var(S_t)) & \mathrm{if} \; \chi(s, S, L) = 1
661: \wedge \chi(t, S, L) = 1 \\
662: L \setminus var(S_s) & \mathrm{if} \; \chi(s, S, L) = 1 \\
663: L \setminus var(S_t) & \mathrm{if} \; \chi(t, S, L) = 1 \\
664: L \setminus var(S_s \cup S_t) & \mathrm{otherwise}
665: \end{array} \right.
666: \]
667: \end{definition}
668:
669: \noindent
670: A precision gain over
671: previous algorithms follows
672: since a closure is avoided if $s$ is linear but not $t$ (or vice versa) and
673: $s$ and $t$ are not independent.
674: When both $s$ and $t$ are linear, but
675: not independent, two closures are required (as
676: previously), but the resulting sharing
677: abstraction may contain fewer elements owing to the pruning
678: effect of intersection. When the independence check
679: is satisfied, that is
680: $S_s \cap S_t =
681: \emptyset$, it follows that
682: $(S_s^{*} \uplus S_t) \cap (S_s \uplus S_t^{*})$ = $S_s \uplus S_t$.
683: This explains why algorithms with the independence check are safe.
684: Note that if
685: $s$ and $t$ are both linear, but not independent, an
686: implementor might trade precision for efficiency
687: by computing
688: $S_s^{*} \uplus S_t$ if $|S_s| \leq |S_t|$ and
689: $S_s \uplus S_t^{*}$ otherwise.
690:
691: \begin{theorem}[Correctness of abstract unification 1]\label{theorem-amgu-correct} \rm
692: Let $E \in \gamma_X^{SFL}(\langle S, F, L \rangle)$, $var(s) \cup
693: var(t) \subseteq X$ and $amgu_1(\langle S, F, L \rangle, s, t) =
694: \langle S', F', L' \rangle$. Then $E \cup \{ s = t \} \in
695: \gamma_X^{SFL}(\langle S', F', L' \rangle)$.
696: \end{theorem}
697:
698: \begin{proof}
699: Put $E' = \{ s = t \}$.
700: Let $\theta \in imgu(E)$ and $\theta' \in imgu(E \cup E')$.
701: Observe that $unify(\theta(E')) \supseteq
702: unify(\theta(E') \cup eqn(\theta)) =
703: unify(E' \cup eqn(\theta)) =
704: unify(E \cup E') \neq \emptyset$. Thus let
705: $\delta \in imgu(\theta(E')) = imgu({\theta^{\infty}}(E'))$.
706: By part~\ref{case-two} of lemma~\ref{lemma-subs},
707: $\delta \circ \theta^{\infty} \in mgu(eqn(\theta) \cup E') = mgu(E \cup E')$.
708: Since $dom(\theta) \cap rng(\delta) = \emptyset$,
709: $\delta \circ \theta^{\infty} = \delta \circ \theta \in imgu(E \cup E')$.
710: \begin{enumerate}
711:
712: \item To show $\alpha_X^{\Share}(\delta \circ \theta) \subseteq S'$,
713: let $y \in U$ and consider $occ(\delta \circ \theta, y)$.
714:
715: \begin{enumerate}
716: \item Suppose $y \not\in rng(\delta \circ \theta)$.
717:
718: \begin{enumerate}
719:
720: \item Suppose $y \not\in dom(\delta \circ \theta)$, that is,
721: $\delta \circ \theta(y) = y$. Thus
722: $\theta(y) = y'$ and $\delta(y')
723: = y$. Suppose $y \neq y'$.
724: Then $y \in dom(\theta)$, thus $y \not\in rng(\delta)$
725: which is a contradiction.
726: Therefore $y=y'$, giving $\theta(y) = y$ and
727: $\delta(y) = y$.
728:
729: \begin{enumerate}
730:
731: \item Suppose $y \not\in var(\theta(s))$ and $y \not\in var(\theta(t))$.
732: Hence $y \not\in dom(\delta)$ and \mbox{$y \not\in rng(\delta)$},
733: so that $occ(\delta \circ \theta, y) \cap X$ = $occ(\theta, y)
734: \cap X \in S$. But $var(s) \cap occ(\theta, y) = \emptyset$ and
735: similarly $var(t) \cap occ(\theta, y) = \emptyset$, so that
736: $occ(\delta \circ \theta, y) \cap X \in S'$.
737:
738: \item
739: Suppose $y \in var(\theta(s))$ and $y \not\in var(\theta(t))$.
740: Since $\delta(y) = y$, it follows that $y \in var(\delta \circ
741: \theta(s)) = var(\delta \circ \theta(t))$. Suppose $y \in rng(\delta)$,
742: then $y \not\in dom(\theta)$, hence $y \in rng(\delta \circ \theta)$
743: which is a contradiction. Therefore $y \not\in rng(\delta)$, thus
744: $y \in var(\theta(t))$ which is a contradiction.
745:
746: \item Suppose $y \not\in var(\theta(s))$ and $y \in var(\theta(t))$.
747: Analogous to the previous case.
748:
749: \item Suppose $y \in var(\theta(s))$ and $y \in var(\theta(t))$.
750: Since $\delta(y)$ = $y$ and $y \not\in rng(\delta \circ \theta)$, $y
751: \not\in rng(\theta)$. Thus $y\in var(s)$ and $y\in var(t)$.
752: Since $y\not\in rng(\theta)$, it follows that $y \not\in
753: dom(\theta)$, therefore $y\not\in rng(\delta)$.
754: Thus, $occ(\delta\circ \theta, y) = occ(\theta, y)$.
755: Therefore $occ(\delta\circ \theta, y) \cap X \in S_s$ since $var(s)
756: \subseteq X$ and
757: $occ(\delta \circ \theta, y) \cap X \in S_t$ since $var(t) \subseteq X$.
758: Thus $occ(\delta \circ \theta, y) \cap X \in S'$.
759: \end{enumerate}
760:
761: % the therefore follows because if \delta(x) = y then x = \theta(y).
762: % but \theta(y) = y, hence x = y and thus y\not\in rng(\delta).
763:
764: \item Suppose $y \in dom(\delta \circ \theta)$.
765: Since $y \not\in rng(\delta \circ \theta)$, $occ(\delta \circ
766: \theta, y) \cap X = \emptyset \in S'$.
767: \end{enumerate}
768:
769: \item Suppose $y \in rng(\delta \circ \theta) \setminus var(\theta(E'))$.
770: Then $y \not\in dom(\delta)$ and
771: $y \not\in rng(\delta)$ so that $occ(\delta\circ \theta, y)
772: = occ(\theta, y)$. Moreover, since $y \not\in var(\theta(E'))$
773: it follows that $occ(\delta\circ \theta, y) \cap X \in S \setminus (S_s
774: \cup S_t)
775: \subseteq S'$.
776:
777: \item Suppose $y \in rng(\delta \circ \theta) \cap var(\theta(E'))$.
778: Since $occ(\delta, y) \subseteq var(\theta(s)) \cup
779: var(\theta(t))$, $occ(\delta \circ \theta, y) \cap X = \cup \{
780: occ(\theta, u) \cap X \mid u \in occ(\delta, y) \} = (\cup R_s)
781: \cup (\cup R_t)$, where $R_s = \{ occ(\theta, v) \cap X \mid v \in
782: var(\theta(s)) \cap occ(\delta, y) \}$ and $R_t = \{ occ(\theta,
783: w) \cap X \mid w \in var(\theta(t)) \cap occ(\delta, y) \}$.
784: If
785: $R_s = \emptyset$, then $y \not\in var(\delta \circ \theta(s)) =
786: var(\delta \circ \theta(t))$, hence $R_t = \emptyset$ and
787: $occ(\delta \circ \theta, y) \cap X = \emptyset \in S'$. Likewise
788: $occ(\delta \circ \theta, y) \cap X = \emptyset \in S'$ if $R_t =
789: \emptyset$. Thus suppose $R_s \neq \emptyset$ and $R_t \neq
790: \emptyset$.
791: Since
792: $var(s) \subseteq X$, $R_s \subseteq S_s$ and since $var(t)
793: \subseteq X$, $R_t \subseteq S_t$.
794:
795: \begin{enumerate}
796:
797: \item\label{case-freeness}
798: Suppose $s \in F$. Thus $\theta(s) \in U$, hence $|R_s| =
799: |var(\theta(s))| = 1$. Moreover $\chi(\theta(s)) \leq 1$.
800: Suppose $|R_t \setminus R_s| > 1$.
801: Thus there exists $u \neq v$ such that $u, v \in
802: var(\theta(t)) \setminus var(\theta(s))$ and
803: $var(\delta(u)) \cap var(\delta(v)) \neq
804: \emptyset$. This contradicts lemma~\ref{lemma-original-linearity},
805: hence $|R_t \setminus R_s| \leq 1$. Thus $occ(\delta \circ \theta, y)
806: \cap X \in S_s \uplus S_t$.
807:
808: \item
809: Suppose $t \in F$. Analogous to the previous case.
810:
811: \item
812: Suppose $\chi(s, S, L) = 1$. Thus $\chi(\theta(s)) \leq 1$. As
813: with case~\ref{case-freeness}, it follows that $|R_t \setminus R_s| \leq 1$.
814: Thus $occ(\delta \circ \theta, y) \cap X \in S_s^{*} \uplus S_t$.
815:
816: \item
817: Suppose $\chi(t, S, L) = 1$. Analogous to the previous case.
818:
819: \item
820: Otherwise $occ(\delta \circ \theta, y) \cap X \in S_s^{*} \uplus
821: S_t^{*}$.
822:
823: \end{enumerate}
824:
825: \end{enumerate}
826:
827: \item It is straightforward to show
828: $\delta \circ \theta(x) \in U$ for all $x \in F'$.
829:
830: %Hence, let $x \in F$ and suppose $\delta \circ \theta(x) \not\in U$.
831: %Then $\theta(x) = y \in U$ and $\delta(y) \not\in U$.
832: %\begin{enumerate}
833: %
834: %\item Suppose $s \in F$. Then $\theta(s) = y \in U$, hence
835: %$\delta = \{ y \mapsto \theta(t) \}$ and $\theta(x) = y$.
836: %Therefore $x \in occ(\theta, y) \in S_s$.
837: %
838: %\item Suppose $t \in F$. Analogous to the previous case.
839: %
840: %\item Otherwise $y \in var(\theta(E'))$, hence
841: %$x \in occ(\theta, y) \in S_s \cup S_t$.
842: %
843: %\end{enumerate}
844:
845: \item To show $\chi(\delta \circ \theta(x)) \leq 1$ for all $x \in
846: L'$. Observe $\chi(\delta \circ \theta(x)) = 0$ if $x \in G'$ and
847: $\chi(\delta \circ \theta(x)) = 1$ if $x \in F'$. Hence, let $x
848: \in L \subseteq X$ and suppose $\chi(\delta \circ \theta(x)) = 2$.
849: \begin{enumerate}
850:
851: \item Suppose $\chi(s, S, L) = 1$. By lemma~\ref{lemma-chi},
852: $\chi(\theta(s)) \leq 1$.
853: \begin{enumerate}
854:
855: \item Suppose there exist $u, v \in var(\theta(x))$, $u \neq v$
856: such that $var(\delta(u)) \cap var(\delta(v)) \neq \emptyset$. By
857: lemma~\ref{lemma-original-linearity} either:
858: \begin{enumerate}
859:
860: \item $u \in var(\theta(s))$ and $v \in var(\theta(t))$, hence $x
861: \in occ(\theta, u) \cap X \in S_s$, and therefore $x \not\in L'$.
862:
863: \item $u \in var(\theta(t))$ and $v \in var(\theta(s))$, hence $x
864: \in occ(\theta, v) \cap X \in S_s$, and therefore $x \not\in L'$.
865:
866: \item $u, v \in var(\theta(s))$. Hence $x
867: \in occ(\theta, v) \cap X \in S_s$, and thus $x \not\in L'$.
868:
869: \end{enumerate}
870:
871: \item Suppose there exists $u \in var(\theta(x))$ such that
872: $\chi(\delta(u)) = 2$. By lemma~\ref{lemma-new-linearity}, $u \in
873: var(\theta(s))$, thus $x \in occ(\theta, u) \cap X \in S_s$ and
874: therefore $x \not\in L'$.
875:
876: \end{enumerate}
877:
878: \item Suppose $\chi(t, S, L) = 1$. Analogous to the previous case.
879:
880: \item Otherwise observe that either:
881: \begin{enumerate}
882:
883: \item There exist $u, v \in var(\theta(x))$, $u \neq v$
884: such that $var(\delta(u)) \cap var(\delta(v)) \neq \emptyset$.
885: Thus \mbox{$u \in var(\theta(E'))$} and $x \in occ(\theta, u) \cap X \in
886: S_s \cup S_t$. Hence $x \not\in L'$.
887:
888: \item There exists $u \in var(\theta(x))$ such that
889: $\chi(\delta(u)) = 2$. Thus \mbox{$u \in var(\theta(E'))$} and $x
890: \in occ(\theta, u) \cap X \in S_s \cup S_t$. Hence $x \not\in L'$.
891:
892: \end{enumerate}
893: \end{enumerate}
894: \end{enumerate}
895: \end{proof}
896:
897: \begin{example} Consider again example~\ref{exam-independence}.
898: Observe that $amgu_1(\langle S, F, L \rangle, w, x) = \langle S',
899: F', L' \rangle$ where $S' = \{ \emptyset \} \cup (S_w^{*} \uplus
900: S_x) \cap (S_w \uplus S_x^{*})$ = $\{ \emptyset, \{u,w,x\}$,
901: $\{u,w,x,y\}$, $\{u,w,x,z\}$, $\{v,w,x\}$, $\{v,w,x,y\}$,
902: $\{v,w,x,z\}$, $\{w,x\}$, $\{w,x,y\}$, $\{w,x,z\}\}$,
903: %\[
904: %S_w^{*} = \{ \{ u, w \}, \{ v, w \}, \{ w, x \}, \{u,v,w\},
905: %\{u,w,x\}, \{v,w,x\}, \{u,v,w,x\}\}
906: %\]
907: %\[S_x^{*} = \{ \{x, y \}, \{x, z \}, \{w, x \}, \{x,y,z\}, \{w,x,y\}, \{w,x,z\},
908: %\{w,x,y,z\} \}
909: %\]
910: %\[
911: %S_w^{*} \uplus S_x = \{ \{u,v,w,x\}, \{u,v,w,x,y\}, \{u,v,w,x,z\},
912: %\{u,w,x\}, \{u,w,x,y\}, \{u,w,x,z\}, \{v,w,x\}, \{v,w,x,y\},
913: %\{v,w,x,z\}, \{w,x,y\}, \{w,x\}, \{w,x,z\} \}
914: %\]
915: %\[ S_w \uplus S_x^{*} =
916: %\{ \{u,w,x\}, \{u,w,x,y\}, \{u,w,x,y,z\}, \{u,w,x,z\}, \{v,w,x\},
917: %\{v,w,x,y\}, \{v,w,x,y,z\}, \{v,w,x,z\}, \{w,x\}, \{w,x,y\},
918: %\{w,x,y,z\}, \{w,x,z\} \}
919: %\]
920: %\[ (S_w^{*} \uplus S_x) \cap (S_w \uplus S_x^{*}) =
921: %\{ \{u,w,x\}, \{u,w,x,y\}, \{u,w,x,z\}, \{v,w,x\}, \{v,w,x,y\},
922: %\{v,w,x,z\}, \{w,x,y\}, \{w,x\}, \{w,x,z\} \}
923: %\]
924: $F' = \emptyset$ and $L' = \emptyset$. This asserts the
925: independence of $u$ and $v$ (similarly $y$ and $z$), as required.
926: \end{example}
927:
928: \noindent The following example, adapted from \cite{L91},
929: illustrates that closure can be required to abstract
930: the unification of linear terms.
931:
932: \begin{example}\label{exam-check} Let
933: $X = \{w,x,y,z\}$ and observe $E \in \gamma_X^{SFL}(\langle S, F,
934: L \rangle)$ where $E = \{ w = f(x, y, z) \}$, $S = \{ \emptyset,
935: \{w,x\}, \{w,y\}, \{w,z\}\}$, $F = \emptyset$ and $L = \{w,x,y,z\}$.
936: Let $E' = \{ w = f(z, x, y) \}$ and note that $\theta' \in imgu(E
937: \cup E')$ where $\theta' = \{ w \mapsto f(z,z,z), x \mapsto z, y
938: \mapsto z \}$. Thus $E \cup E' \in \gamma_X^{SFL}(\langle S', F',
939: L' \rangle)$ where $S' = \{ \emptyset, \{w,x,y,z\}\}$, $F' =
940: \emptyset$ and $L' = \{x,y,z\}$. Indeed, if $S_s = rel(w, S) =
941: \{\{w,x\}, \{w,y\}, \{w,z\}\}$ and $S_t = rel(f(z, x, y), S) =
942: \{\{w,x\}, \{w,y\}, \{w,z\}\}$ then $(S_s^{*} \uplus S_t) \cap
943: (S_s \uplus S_t^{*})$ = $\{\{w,x\}$, $\{w,y\}$, $\{w,z\}$,
944: $\{w,x,y\}$, $\{w,x,z\}$, $\{w,y,z\}$, $\{w,x,y,z\}\}$, thus
945: $amgu_1(\langle S, F, L\rangle$, $w, f(z,x,y))$
946: yields a safe, though conservative, abstraction. Closure is
947: required to construct the $\{w,x,y,z\}$ sharing group.
948: \end{example}
949:
950: \section{Decomposition of set-sharing}
951:
952: Fil\'{e} \cite{F94} observes that different sharing and freeness
953: abstractions can represent the same equations, that is,
954: $\gamma^{SF}_X(\langle S_1, F \rangle) = \gamma^{SF}_X(\langle
955: S_2, F\rangle)$ does not imply that $S_1 = S_2$. Therefore the
956: relationship between $\Share \times \Free$ and the concrete domain is a
957: Galois connection rather than an insertion. An insertion is
958: constructed by using $F$ to decompose $S$ into a set of sharing
959: abstractions $K_F(S)$ such that each $B \in K_F(S)$ does not
960: include sharing groups that definitely arise from different
961: computational paths. The following definition and lemma from \cite{F94}
962: formalises this decomposition, henceforth referred to as the
963: Fil\'{e} decomposition.
964:
965: \begin{definition}
966: The map $K_F(S) : \Share \to \wp(\Share)$ is defined by:
967: \[
968: K_F(S) = \left\{ B \left|
969: \begin{array}{c}
970: B \subseteq S \qquad \wedge \qquad F \subseteq var(B) \qquad \wedge \\
971: \forall G_1, G_2 \in B . (G_1 \neq G_2 \rightarrow G_1 \cap G_2
972: \cap F = \emptyset)
973: \end{array}
974: \right. \right\}
975: \]
976: \end{definition}
977:
978: \begin{lemma}\label{lemma-k} $\gamma^{SF}_X(\langle S, F \rangle) =
979: \cup \{ \gamma^{SF}_X(\langle B, F \rangle) \mid B \in K_F(S) \}$.
980: \end{lemma}
981:
982: \noindent Using the above, abstract unification can be refined to
983: $\cup \{ amgu(\langle B, F, L \rangle, s, t) | B \in K_F(S)\}$.
984: Abstract unification computed in this way does not merge sharing groups arising
985: from different computational paths, and thereby improves precision.
986: Calculating $K_F(S)$ is expensive and
987: the number of calls to $amgu$ is $|K_F(S)|$ (which is
988: potentially exponential in $|S|$).
989: However, this tactic suggests lightweight refinements to
990: closure ($*$) and pair-wise union ($\uplus$) that recover some precision
991: at little cost.
992: Since two distinct sharing groups which contain a common free variable
993: must arise from different computational paths, they cannot describe
994: the same equation and therefore
995: need not be combined. Definition~\ref{defn-amgu2} details the
996: refined abstract unification algorithm and theorem~\ref{cor-amgu2}
997: builds on lemma~\ref{lemma-fiddly} to establish correctness.
998:
999: \begin{definition}[Abstract unification 2]\label{defn-amgu2}
1000: Abstract unification $amgu_{2}(\langle S, F, L \rangle, s, t) =
1001: \langle S', F', L' \rangle$ is defined:
1002: \[
1003: S'' = \left\{ \begin{array}{r@{\,}l@{\,}ll}
1004: (S_s^{*_{F}} \uplus_F S_t) & \cap & (S_s \uplus_F S_t^{*_{F}}) & \mathrm{if} \; \chi(s, S, L) = \chi(t, S, L) = 1 \\
1005: S_s^{*_{F}} & \uplus_F & S_t & \mathrm{if} \; \chi(s, S, L) = 1 \\
1006: S_s \,\,\,\, & \uplus_{F} & S_t^{*_{F}} & \mathrm{if} \; \chi(t, S, L) = 1 \\
1007: S_s^{*_{F}} & \uplus_{F} & S_t^{*_{F}} & \mathrm{otherwise}
1008: \end{array} \right.
1009: \]
1010: \[
1011: S_1 \uplus_F S_2 = \bigcup \left\{ G_1 \cup G_2 \left|
1012: \begin{array}{@{}c@{}}
1013: G_1 \in S_1 \wedge G_2 \in S_2 \wedge
1014: G_1 \neq G_2 \rightarrow G_1 \cap G_2 \cap F = \emptyset
1015: \end{array} \right. \right\}
1016: %S_1 \uplus_F S_2 = \bigcup \left\{ G_1 \cup G_2 \left|
1017: %\begin{array}{@{\,}l@{\;}c@{\;}l@{\;}c@{}}
1018: %G_1 \in S_1 & \wedge & G_2 \in S_2 & \wedge \\
1019: %G_1 \neq G_2 & \rightarrow & G_1 \cap G_2 \cap F = & \emptyset
1020: %\end{array} \right. \right\}
1021: \]
1022: \[
1023: S^{*_F} = \bigcap \left\{ S' \left|
1024: \begin{array}{@{}c@{}}
1025: S \subseteq S' \wedge \forall G_1, G_2 \in S' .
1026: G_1 \cap G_2 \cap F = \emptyset \rightarrow G_1 \cup G_2 \in S'
1027: \end{array} \right. \right\}
1028: %\begin{array}{@{\,}c@{}}
1029: %S \subseteq S' \quad \wedge \quad \forall G_1, G_2 \in S' . \\
1030: %G_1 \cap G_2 \cap F = \emptyset \rightarrow G_1 \cup G_2 \in S'
1031: %\end{array} \right. \right\}
1032: \]
1033: where $S'$, $S_s$, $S_t$, $F'$ and $L'$ are defined as in
1034: definition~\ref{defn-amgu}.
1035: \end{definition}
1036:
1037: \noindent Notice that the use of freeness is completely
1038: absorbed into $*_{F}$ and $\uplus_{F}$. The following lemma demonstrates that $\uplus_F$
1039: and $*_F$ coincide with $\uplus$
1040: and $*$ for each element of the Fil\'{e} decomposition. The correctness
1041: of abstract unification ($amgu_2$) follows from this result.
1042:
1043: \begin{lemma}\label{lemma-fiddly}
1044: \begin{enumerate}
1045: \item If $B \in K_F(S)$ and $R \subseteq B$,
1046: then $R^{*} = R^{*_F}$.
1047:
1048: \item If $B \in K_F(S)$ and $R_1, R_2 \subseteq B$,
1049: then $R_1 \uplus R_2 = R_1 \uplus_{F} R_2$, $R_1^{*} \uplus R_2 =
1050: R_1^{*} \uplus_{F} R_2$, $R_1 \uplus R_2^{*} = R_1 \uplus_{F}
1051: R_2^{*}$ and $R_1^{*} \uplus R_2^{*} = R_1^{*} \uplus_{F}
1052: R_2^{*}$.
1053: \end{enumerate}
1054: \end{lemma}
1055:
1056: \begin{proof}
1057: \begin{enumerate}
1058:
1059: \item Proof by induction.
1060: \begin{enumerate}
1061:
1062: \item Suppose $R = \emptyset$. Then $R^{*} = \emptyset = R^{*_F}$.
1063:
1064: \item Suppose $R = \{ G \} \cup R'$. By the hypothesis,
1065: ${R'}^{*} = {R'}^{*_F}$. Since $R \subseteq B$,
1066: then for all $G' \in R'$, $G' \cap G \cap F = \emptyset$.
1067: Hence $R^{*} = R^{*_F}$.
1068:
1069: \end{enumerate}
1070:
1071: \item \begin{enumerate}
1072:
1073: \item To show $R_1 \uplus R_2 = R_1 \uplus_{F} R_2$. Let $G_i \in
1074: R_i$. If $G_1 \cap G_2 \cap F \neq \emptyset$ then $G_1 = G_2$.
1075: Hence $G_1 \cup G_2 \in R_1 \uplus_{F} R_2$.
1076:
1077: \item To show $R_1^{*} \uplus R_2 = R_1^{*} \uplus_{F} R_2$.
1078: Let $G_1 \in R_1^{*}$ and $G_2 \in R_2$. Then $G_1 = \cup Q_1$ for
1079: some $Q_1 \subseteq R_1$. Put $Y = G_1 \cap G_2 \cap F$, $Q_1' =
1080: \{ G \in Q_1 \mid G \cap Y = \emptyset \}$ and $Q_1'' = Q_1
1081: \setminus Q_1'$. Observe that $|Q_1''| \leq 1$ and $Q_1''
1082: \subseteq \{ G_2 \}$. Thus $G_1 \cup G_2 = (\cup Q_1') \cup G_2$.
1083: Since $(\cup Q_1') \cap G_2 \cap F = \emptyset$ it follows that
1084: $G_1 \cup G_2 \in R_1^{*} \uplus_{F} R_2$.
1085:
1086: \item To show $R_1 \uplus R_2^{*} = R_1 \uplus_{F} R_2^{*}$. Analogous
1087: to the previous case.
1088:
1089: \item To show $R_1^{*} \uplus R_2^{*} = R_1^{*} \uplus_{F} R_2^{*}$.
1090: Let $G_1 \in R_1^{*}$ and $G_2 \in R_2^{*}$. Then $G_i = \cup Q_i$
1091: for some $Q_i \subseteq R_i$. Put $Y = G_1 \cap G_2 \cap F$, $Q_i'
1092: = \{ G \in Q_i \mid G \cap Y = \emptyset \}$ and $Q_i'' = Q_i
1093: \setminus Q_i'$. Observe that $|Q_i''| \leq 1$.
1094: \begin{enumerate}
1095:
1096: \item Suppose $|Q_1''| = \emptyset$ or $|Q_2''| = \emptyset$. Then
1097: $G_1 \cap G_2 \cap F =
1098: \emptyset$, hence $G_1 \cup G_2 \in R_1^{*} \uplus_{F} R_2^{*}$.
1099:
1100: \item Suppose $|Q_1''| = |Q_2''| = 1$. Hence $Q_1'' = Q_2''$,
1101: thus $G_1 \cup G_2 = G_1 \cup (\cup Q_2')$. Since $G_1 \cap (\cup
1102: Q_2') \cap F = \emptyset$ it follows that $G_1 \cup G_2 \in
1103: R_1^{*} \uplus_{F} R_2^{*}$.
1104:
1105: \end{enumerate}
1106: \end{enumerate}
1107: \end{enumerate}
1108: \end{proof}
1109:
1110: \begin{theorem}[Correctness of abstract unification 2]\label{cor-amgu2} \rm
1111: Let $E \in \gamma_X^{SFL}(\langle S, F, L \rangle)$, $var(s) \cup
1112: var(t) \subseteq X$ and $amgu_{2}(\langle S, F, L \rangle, s, t) =
1113: \langle S', F', L' \rangle$. Then $E \cup \{ s = t \} \in
1114: \gamma_X^{SFL}(\langle S', F', L' \rangle)$.
1115: \end{theorem}
1116:
1117: \begin{proof} Observe $E \in \gamma_X^{SF}(\langle S, F \rangle)$
1118: and $E \in \gamma_X^{L}(L)$. By lemma~\ref{lemma-k}, there exists
1119: $B \in K_F(S)$ such that $E \in \gamma_X^{SF}(\langle B, F
1120: \rangle)$, hence $E \in \gamma_X^{SFL}(\langle B, F, L \rangle)$.
1121: Observe that if $s \in F$ then $S_s^{*_F} = S_s$
1122: (and likewise for $t \in F$)
1123: and hence by lemma~\ref{lemma-fiddly}, $amgu_1(\langle B, F, L \rangle, s, t)
1124: = amgu_{2}(\langle B, F, L \rangle, s, t)$.
1125: By theorem~\ref{theorem-amgu-correct}, $E \cup \{ s = t
1126: \} \in \gamma_X^{SFL}(amgu_1(\langle B, F, L \rangle, s, t))$
1127: = $\gamma_X^{SFL}(amgu_2(\langle B, F, L \rangle, s, t))$,
1128: thus $E \cup \{ s = t
1129: \} \in \gamma_X^{SFL}(amgu_2(\langle S, F, L \rangle, s, t))$.
1130: \end{proof}
1131:
1132: \noindent The proof explains why
1133: the standard freeness tactic is a specialised
1134: version of the Fil\'{e} decomposition.
1135:
1136: This refinement is only
1137: worthwhile if redundant sharing groups are introduced in analysis.
1138: Although it can be shown that projection and join do not introduce
1139: redundancy, the following example indicates that redundant sharing
1140: groups can arise in abstract unification ($amgu_1$)
1141: and that the refined abstract unification ($amgu_2$) can avoid
1142: some of these redundant sharing groups.
1143:
1144: \newpage
1145:
1146: \begin{example}\label{exam-redundant} Let $X = \{ x, y, z \}$, $S = \{\emptyset, \{x, y\}, \{ y, z \}\}$,
1147: $F = \{ y \}$ and $L = \{ y \}$. Suppose $s= x$ and $t=z$. Then
1148: $S_s = \{ \{ x, y \} \}$ and $S_t = \{ \{ x, z \} \}$ so that
1149: $amgu_1(\langle S, F, L \rangle, x, z) = \langle \{ \emptyset, \{
1150: x, y, z \} \}, \emptyset, \emptyset \rangle$. However ${S_s}^{*_F}
1151: = \{ \{ x, y \} \}$ and ${S_t}^{*_F} = \{ \{ x, z \} \}$ and in
1152: particular ${S_s}^{*_F} \uplus_{F} {S_t}^{*_F} = \emptyset$ so
1153: that $amgu_2(\langle S, F, L \rangle, x, z)$ = $\langle \{
1154: \emptyset \}, \emptyset, \{ x, y, z \} \rangle$.
1155: \end{example}
1156:
1157: \noindent The following example demonstrates that $amgu_2$ is not
1158: as precise as the full Fil\'{e} decomposition.
1159:
1160: \begin{example} Let $X = \{x,y,z\}$,
1161: $S = \{ \emptyset, \{x\}, \{z\}, \{x,y\}, \{y,z\}\}$, $F = \{x, y,
1162: z\}$ and $L = \{x, y, z\}$. Suppose $s= x$ and $t=z$. Then ${S_s}
1163: = \{ \{ x \}, \{ x, y \} \}$ and ${S_t} = \{ \{ z \}, \{ y, z \}
1164: \}$, hence ${S_s}^{*_F} = {S_s}$ and ${S_t}^{*_F} = {S_t}$. Thus
1165: ${S_s}^{*_F} \uplus_F {S_t}^{*_F}$ = $\{ \emptyset, \{x, z\},
1166: \{x,y,z\}\}$. It follows that $amgu_2(\langle S, F, L \rangle, x,
1167: z)$ = $\langle \{ \emptyset, \{x, z\}, \{x,y,z\}\}, F, L \rangle$.
1168: However, the Fil\'{e} decomposition gives $K_F(S) = \{ S_1, S_2,
1169: S_3, S_4 \}$ where $S_1 = \{ \{x\}, \{y,z\} \}$, $S_2 = \{
1170: \emptyset, \{x\}, \{y,z\} \}$, $S_3 = \{ \{x,y\}, \{z\} \}$ and
1171: $S_4 = \{ \emptyset, \{x,y\}, \{z\} \}$. Moreover, $amgu_1(\langle
1172: S_2, F, L \rangle, x, z)$ = $amgu_1(\langle S_4, F, L \rangle, x,
1173: z)$ = $\langle \{ \emptyset, \{x,y,z\}\}, F, L \rangle$. Since
1174: $S_1 \subseteq S_2$ and $S_3 \subseteq S_4$, the Fil\'{e} leads to
1175: the sharing abstraction $\{ \emptyset, \{x,y,z\}\}$, which is more
1176: precise.
1177: \end{example}
1178:
1179: \section{Pruning of set-sharing}
1180:
1181: Pruning sharing groups is advantageous for efficiency and
1182: precision. By reducing the size of an abstraction, abstract
1183: unification works on smaller objects and is therefore faster,
1184: even if no precision is gained. Of course, the benefit
1185: of pruning for efficiency needs to outweigh its cost.
1186:
1187: \subsection{Pruning with freeness via groundness}
1188:
1189: Surprisingly, combined
1190: sharing and freeness information can
1191: improve groundness propagation and
1192: sharing even for rational tree unification. For example, the equation \mbox{$x = f(y, z)$}
1193: can be abstracted by $(x \leftrightarrow z) \wedge (x \leftrightarrow y)$
1194: if $x$ and $y$ are free variables that share. This is because,
1195: in this circumstance, finite tree
1196: unification fails for $x = f(y, z)$
1197: whereas rational tree
1198: unification binds $x$ and $y$ to $f(f(\ldots, z), z)$.
1199: Abstract unification can use the freeness of variables
1200: in the equation to extract hidden groundness information (for
1201: distinct computational paths)
1202: and thereby prune sharing groups and improve precision. The proof of theorem~\ref{cor-amgu3}
1203: again uses the Fil\'{e} decomposition.
1204:
1205: \begin{definition}[Abstract unification 3]\label{defn-amgu3}
1206: Abstract unification $amgu_{3}(\langle S, F, L \rangle, s, t) =
1207: \langle S', F', L' \rangle$ is defined:
1208: \[ S' = (S \setminus (S_s \cup S_t))
1209: \cup \left\{ \begin{array}{@{}cl@{}} \bigcup_{G \in S_s}
1210: trim_X(s \leftrightarrow Y, \{ G \} \uplus_{F} \!\! S_t)
1211: & \mbox{if} \; s \in F \wedge t \not\in U \\
1212: \bigcup_{G \in S_t} trim_X(Z \leftrightarrow t , S_s
1213: \uplus_{F} \!\! \{ G \}) & \mbox{if} \; t \in F \wedge s \not\in U \\
1214: S'' & \mbox{otherwise}
1215: \end{array} \right.
1216: \]
1217: where $Y = var(t) \setminus (G \cap F)$, $Z = var(s) \setminus (G
1218: \cap F)$, $S_s$, $S_t$, $S''$, $F'$ and $L'$ are defined as in
1219: definition~\ref{defn-amgu2}.
1220: \end{definition}
1221:
1222: \begin{theorem}[Correctness of abstract unification 3]\label{cor-amgu3} \rm
1223: Let $E \in \gamma_X^{SFL}(\langle S, F, L \rangle)$, $var(s) \cup
1224: var(t) \subseteq X$ and $amgu_{3}(\langle S, F, L \rangle, s, t) =
1225: \langle S', F', L' \rangle$. Then $E \cup \{ s = t \} \in
1226: \gamma_X^{SFL}(\langle S', F', L' \rangle)$.
1227: \end{theorem}
1228:
1229: \begin{proof}
1230: Suppose $s \in F$. By lemma~\ref{lemma-k}, there exists $B \in
1231: K_F(S)$ such that \mbox{$E \in \gamma_X^{SFL}(\langle B, F
1232: \rangle)$} and by theorem~\ref{cor-amgu2}, $E \cup \{ s = t \}
1233: \in \gamma^{\Share}_X(B')$ where $B' = (B \setminus (B_s \cup
1234: B_t)) \cup (B_s \uplus_{F} B_t)$, $B_s = rel(s, B)$ and $B_t =
1235: rel(t, B)$. Let $\theta \in imgu(E)$. Since $s \in F$, $\theta(s)
1236: = x$ for some $x \in U$. Furthermore, $s \in G$ for all $G \in
1237: S_s$. Since $s \in F$, $B_s = \{ G \}$ where $G = occ(\theta, x)$.
1238: Observe that $\theta(y) = x$ for all $y \in G \cap F$. Since $t
1239: \not\in U$, $\theta(t) \not\in U$, hence $\alpha_X^{Pos}(\{
1240: \theta(s) = \theta(t) \}) \models s \leftrightarrow Y$. Moreover,
1241: $mgu(E \cup \{ s = t \}) = mgu(eqn(\theta) \cup \{ s = t \}) =
1242: mgu(eqn(\theta) \cup \{ \theta(s) = \theta(t) \})$. Thus
1243: $\alpha_X^{Pos}(E \cup \{ s = t \}) \models \alpha_X^{Pos}(\{
1244: \theta(s) = \theta(t) \}) \models s \leftrightarrow Y$. The result
1245: follows by corollary~\ref{cor-trim}. The $t \in F$ case is
1246: analogous and the otherwise case follows immediately from
1247: theorem~\ref{cor-amgu2}.
1248: \end{proof}
1249:
1250: \noindent The following example illustrates the gain of precision.
1251: Note that even the Fil\'{e} decomposition cannot match this level
1252: of precision.
1253:
1254: \begin{example} \rm Let $X = \{ x, y, z \}$,
1255: $S = \{ \emptyset, \{x,y\}, \{y\}, \{z\} \}$, $F = \{ x, y \}$ and
1256: $L = \{ x, y \}$. \linebreak Suppose $s = x$ and $t = f(y, z)$.
1257: Consider the Fil\'{e} decomposition, that is, $K_F(S) = \{ S_1,
1258: S_2, S_3, S_4 \}$ where $S_1 = \{ \{ x, y \} \}$, $S_2 = \{
1259: \emptyset, \{ x, y \} \}$, $S_3 = \{ \{ x, y \}, \{ z \} \}$, \linebreak $S_4
1260: = \{ \emptyset, \{ x, y \}, \{ z \} \}$. Then $amgu_{1}(\langle
1261: S_4, F, L \rangle, x, f(y, z))$ = $\langle S', \emptyset,
1262: \emptyset \rangle$ where $S' = \{ \emptyset$, $\{x,y\}$,
1263: $\{x,y,z\} \}$. Since
1264: $S_i \subseteq S_4$
1265: for all $i \in \{ 1, 2, 3 \}$, the decomposition
1266: results in the sharing abstraction $S'$.
1267: Moreover, $amgu_{2}(\langle S, F, L \rangle, x, f(y, z))$ = $\langle S',
1268: \emptyset, \emptyset \rangle$.
1269: However,
1270: $amgu_{3}(\langle S, F, L \rangle, x, f(y, z))$ = $\langle
1271: trim_X(x \leftrightarrow z, S'), \emptyset, \emptyset \rangle$ =
1272: $\langle \{ \emptyset, \{x,y,z\} \}, \emptyset,
1273: \emptyset \rangle$ which is more precise.
1274: \end{example}
1275:
1276: \begin{example}\label{exam-optimal} Let $X = \{ x, y, z \}$,
1277: $S = \{\emptyset, \{x, y\}, \{ y, z \}\}$, $F = \{ y \}$ and $L =
1278: \{ y \}$. Suppose \linebreak $s= x$ and $t=z$. Since $x, z \in U$,
1279: $amgu_3(\langle S, F, L \rangle, x, z)$ = $amgu_2(\langle S, F, L
1280: \rangle, x, z)$ = $\langle \{ \emptyset, \{ x, y, z \} \},
1281: \emptyset, \emptyset \rangle$ whereas the Fil\'{e} decomposition
1282: produces $\langle \{ \emptyset \}, \emptyset, \{ x, y, z \}
1283: \rangle$ \linebreak (see example~\ref{exam-redundant}).
1284: \end{example}
1285:
1286: \noindent Example~\ref{exam-optimal} shows that $amgu_3$ is not
1287: uniformly more precise than the Fil\'{e} decomposition, hence is
1288: sub-optimal. Nevertheless, this pruning tactic suggests that any
1289: optimal abstract unification algorithm for sharing, freeness and
1290: linearity, in the presence of groundness, will have to consider
1291: subtle interactions between the components.
1292:
1293: \subsection{Early pruning with groundness}
1294:
1295: Sharing abstractions can always be pruned by removing sharing
1296: groups which contain ground variables. Common practice is to
1297: schedule the solving of equations so as to first apply abstract
1298: unification to equations on ground terms \cite{L91}. Moreover,
1299: \cite{MH92} details a
1300: queueing/dequeueing mechanism for maximally
1301: propagating groundness among systems of equations. This can
1302: involve repeated searching. This section proposes a revision of
1303: this tactic that applies groundness to the complete set of
1304: equations (without repeated searching) and then uses the resulting
1305: groundness information to prune sharing before abstract
1306: unification is applied. The gain is that searching and scheduling
1307: are no longer required (the mechanism is single pass) and that the
1308: disjunctive groundness information captured by $Pos$ can be
1309: exploited so that abstract unification can potentially operate on
1310: smaller abstractions. Observe that groundness information will
1311: normally be tracked by $Pos$ anyway, thus the computational
1312: overhead is negligible. To formulate this strategy, abstract
1313: unification is lifted to sets of equations as follows:
1314:
1315: \begin{definition} The map
1316: $amgu_{i}(T, E) = \{ T' \mid \langle T, E \rangle
1317: \rightsquigarrow^{\star} \langle T', \emptyset \rangle \}$ is
1318: defined by the least relation $\rightsquigarrow \, \subseteq
1319: (Share_{X} \times \Free_X \times Lin_X)^{2}$ such that $\langle T,
1320: \{ s = t \} \cup E \rangle \rightsquigarrow \langle amgu_{i}(T, s,
1321: t), E \rangle$.
1322: \end{definition}
1323:
1324: \noindent The following theorem states correctness of the early
1325: pruning using groundness for $amgu_1$, $amgu_2$ and $amgu_3$.
1326:
1327: \begin{theorem}\label{theorem-ground-safety} \rm
1328: Let $E \in \gamma^{Pos}_X(f) \cap \gamma^{SFL}_X(\langle S, F, L
1329: \rangle)$, $E \cup E' \in \gamma^{Pos}_X(f')$, \mbox{$Y = \{ y \in X
1330: \mid f' \models y \}$}, \mbox{$S' = trim_X(f \wedge Y, S)$},
1331: \mbox{$F' = F \setminus var(rel(Y, S))$}, \mbox{$L' = L \cup Y$},
1332: $var(E) \subseteq X$
1333: and \linebreak \mbox{$T' \in amgu_{i}(\langle S', F', L' \rangle, E')$}.
1334: Then $E \cup E' \in \gamma^{SFL}_X(T')$.
1335: \end{theorem}
1336:
1337: \begin{proof} \rm
1338: Let $\theta \in imgu(E)$ and $\theta' \in imgu(E \cup E')$. Since
1339: $\theta' \in unify(E)$, $\theta \leq \theta'$ and there exists
1340: $\zeta \in Sub$ such that $\zeta \circ \theta = \theta'$. Since
1341: $\theta' \in unify(E')$, $\zeta \in unify(\theta(E'))$ so that
1342: $mgu(\theta(E')) \neq \emptyset$. Let $\delta \in
1343: imgu(\theta(E')) = imgu(\theta^{\infty}(E'))$.
1344: By part~\ref{case-two} of lemma~\ref{lemma-subs},
1345: $\delta \circ \theta = \delta \circ \theta^{\infty} \in
1346: mgu(eqn(\theta) \cup E') = mgu(E \cup E')$.
1347: Thus there exists $\rho \in Rename$ such that
1348: $\rho \circ \delta \circ \theta = \theta'$.
1349: Now $var(\theta'(y)) = \emptyset$ for all $y \in Y$, hence
1350: $var(\delta \circ \theta(y)) = \emptyset$ for all $y \in Y$.
1351: Put $Z = \cup \{ var(\theta(y)) \mid
1352: y \in Y \}$, $\phi = \overline{\exists}Z .
1353: \delta$ and $\psi = \exists Z . \delta$.
1354: Let $z \in Z$. Then there exists $y \in Y$ such that
1355: $z \in var(\theta(y))$. But $var(\delta \circ \theta(y)) = \emptyset$,
1356: hence $rgn(\phi) = \emptyset$ and $\delta =
1357: \psi \circ \phi$. Thus $\psi \circ \phi \in mgu(\theta(E'))$ and
1358: by lemma~\ref{lemma-subs} part~\ref{case-three},
1359: ${\exists} (dom(\phi) \setminus rng(\phi)) . \psi \in
1360: mgu(\phi \circ \theta(E'))$. Furthermore, $\exists(dom(\phi)
1361: \setminus rng(\phi)) . \psi = \psi$ hence $\psi \in mgu(\phi
1362: \circ \theta(E'))$. Since $\phi \circ \theta$ is idempotent,
1363: \mbox{$\psi \in mgu((\phi \circ \theta)^{\infty}(E'))$}. By
1364: lemma~\ref{lemma-subs}, part~\ref{case-two}, $\psi \circ \phi
1365: \circ \theta = \psi \circ (\phi \circ \theta)^{\infty} \in
1366: mgu(eqn(\phi \circ \theta) \cup E')$.
1367: Thus $\theta' \in imgu(eqn(\phi \circ \theta) \cup E')$.
1368:
1369: To show
1370: $eqn(\phi \circ \theta) \in \gamma_X^{\Share}(trim(f \wedge Y, S))$.
1371: Let $u \in U$. If $occ(\phi \circ \theta, u) = \emptyset$ then $occ(\phi
1372: \circ \theta, u) \cap X \in S$ trivially. If $occ(\phi \circ
1373: \theta, u) \neq \emptyset$ then $occ(\phi \circ \theta, u) =
1374: occ(\theta, u)$ since $rng(\phi) = \emptyset$. Thus $occ(\phi
1375: \circ \theta, u) \cap X \in S$. Therefore $eqn(\phi \circ \theta)
1376: \in \gamma_X^{\Share}(S)$. By lemma~\ref{lemma-subs},
1377: part~\ref{case-two}, $\delta \circ \theta \in mgu(E \cup
1378: eqn(\theta))$. But $\theta' \in mgu(E \cup eqn(\theta))$ and
1379: therefore there exists $\rho \in Rename$ such that $\rho \circ
1380: \delta \circ \theta = \theta'$. Thus $\alpha^{Pos}(\delta \circ
1381: \theta) \models \alpha^{Pos}(\rho \circ \delta \circ \theta) =
1382: \alpha^{Pos}(\theta') \models Y$. Observe that if
1383: $\alpha^{Pos}(\delta \circ \theta) \models u$ then
1384: $\alpha^{Pos}(\phi \circ \theta) \models u$ hence
1385: $\alpha^{Pos}(\phi \circ \theta) \models Y$. Since
1386: $\alpha^{Pos}(\phi \circ \theta) \models \alpha^{Pos}(\theta)
1387: \models f$, it follows that $\alpha^{Pos}(\phi \circ \theta)
1388: \models f\wedge Y$. Therefore $eqn(\phi \circ \theta) \in
1389: \gamma_X^{Pos}(f \wedge Y)$. By corollary~\ref{cor-trim},
1390: $eqn(\phi \circ \theta) \in \gamma_X^{\Share}(trim(f \wedge Y, S))$.
1391:
1392: To show $\phi \circ \theta(x) \in U$ for all $x \in F'$.
1393: Let $x \in F$ and $x \not\in var(rel(Y, S))$.
1394: Since $x \not\in var(rel(Y, S))$, $x \not\in occ(\theta, u) \cap X$
1395: or $y \not\in occ(\theta, u) \cap X$ for all $u \in U$ and $y \in Y$.
1396: Since $x \in X$ and $Y \subseteq X$,
1397: $var(\theta(x)) \cap var(\theta(y)) = \emptyset$ for all $y \in Y$.
1398: Hence $\theta(x) \not\in Z$, thus $\theta(x) \not\in dom(\phi)$,
1399: therefore $\phi \circ \theta(x) \in U$.
1400: Thus $eqn(\phi \circ \theta) \in \gamma_X^{\Free}(F')$.
1401:
1402: To show $\chi(\phi \circ \theta(x)) \leq 1$ for all $x \in L'$.
1403: Since $rng(\phi) = \emptyset$, $\chi(\phi \circ \theta(x)) \leq 1$
1404: for all $x \in L$. Moreover, $\alpha^{Pos}(\phi \circ \theta) \models Y$
1405: and therefore $\chi(\phi \circ \theta(x)) \leq 1$
1406: for all $x \in Y$.
1407: Thus $eqn(\phi \circ \theta) \in \gamma_X^{\Lin}(L')$.
1408: The result then follows by induction on $E$ and
1409: theorems~\ref{theorem-amgu-correct}, \ref{cor-amgu2} and \ref{cor-amgu3}.
1410: \end{proof}
1411:
1412: \noindent The following example illustrates the
1413: computational advantages of early pruning.
1414:
1415: \begin{example} \rm
1416: Let $X = \{u,v,x,y\}$,
1417: $S = \{ \emptyset, \{x\}, \{y\}, \{u\}, \{v\} \}$,
1418: $F = \emptyset$,
1419: $L = \emptyset$ and
1420: $f = x \vee y$. Let $E' = \{ x = f(u, v), x = y \}$ so
1421: that $f' = (x \vee y) \wedge
1422: (x \leftrightarrow (u \wedge v)) \wedge
1423: (x \leftrightarrow y)$ = $x \wedge y \wedge u \wedge v$. Then
1424: $Y = \{ x, y, u, v \}$ so that $f \wedge Y = x \wedge y \wedge u \wedge v$
1425: and $S' = trim_X(f \wedge Y, S)$ = $\{ \emptyset \}$.
1426: Hence $amgu_3(\langle S, F, L \rangle, E')$
1427: reduces to $amgu_3(\langle S', F, L \rangle, E')$ =
1428: $\langle \{ \emptyset \}, \emptyset, \emptyset \rangle$. Without
1429: this tactic, no equation of $E'$ will possess a ground
1430: argument and both calls to $amgu_3$ will involve non-trivial
1431: sharing group manipulation.
1432: \end{example}
1433:
1434: \section{Conclusion}
1435:
1436: This paper has given correctness proofs for sharing analysis with
1437: freeness and linearity which hold in the presence of rational
1438: trees. The abstract unification algorithms are themselves novel --
1439: incorporating optimisations for both precision and efficiency.
1440: Specifically, the independence check which can prevent linearity
1441: from being exploited has been removed. In addition, refined
1442: closure and pair-wise union operations have been derived from the
1443: Fil{\'e} decomposition.
1444: A further precision optimisation has been presented which exploits
1445: an interaction between sharing, freeness and groundness, which
1446: shows the subtlety that an optimal algorithm will need to address.
1447: These optimisations have been chosen to balance precision against
1448: efficiency whilst not changing the underlying representation of the
1449: abstract domains. They are
1450: ordered according to
1451: their anticipated degree of usefulness.
1452: This work provides the implementor with a suite of new
1453: optimisations for abstract unification algorithms for sharing,
1454: freeness and linearity.
1455:
1456: \subsubsection*{Acknowledgements}
1457: We thank Gilberto~Fil\'{e} for kindly sending us a copy
1458: of his technical report.
1459: This work was supported, in part, by EPSRC grant
1460: GR/MO8769.
1461:
1462: %\bibliographystyle{tlp}
1463: %\bibliography{set}
1464:
1465: \begin{thebibliography}{}
1466:
1467: \bibitem[\protect\citename{Bagnara {\em et~al.}\relax, }2000]{BZH00}
1468: Bagnara, R., Zaffanella, E., \& Hill, P. (2000).
1469: \newblock Enhanced {S}haring {A}nalysis {T}echniques: {A} {C}omprehensive
1470: {E}valuation.
1471: \newblock {\em Pages 103--114 of:} {\em Proceedings of {P}rinciples and
1472: {P}ractice of {D}eclarative {P}rogramming}.
1473: \newblock ACM Press.
1474: \newblock Long version available at http://www.comp.leeds.ac.uk/hill.
1475:
1476: \bibitem[\protect\citename{Codish {\em et~al.}\relax, }1991]{CDY91}
1477: Codish, M., Dams, D., \& Yardeni, E. (1991).
1478: \newblock Derivation and {S}afety of an {A}bstract {U}nification {A}lgorithm
1479: for {G}roundness and {A}liasing {A}nalysis.
1480: \newblock {\em Pages 79--93 of:} {\em Proceedings of the {I}nternational
1481: {C}onference on {L}ogic {P}rogramming}.
1482: \newblock MIT Press.
1483:
1484: \bibitem[\protect\citename{Codish {\em et~al.}\relax, }1999]{CSS99}
1485: Codish, M., S{\o}ndergaard, H., \& Stuckey, P. (1999).
1486: \newblock Sharing and {G}roundness {D}ependencies in {L}ogic {P}rograms.
1487: \newblock {\em {T}ransactions on {P}rogramming {L}anguages and {S}ystems}, {\bf
1488: 21}(5), 948--976.
1489:
1490: \bibitem[\protect\citename{Fil\'{e}, }1994]{F94}
1491: Fil\'{e}, G. (1994).
1492: \newblock {\em Sharing $\times$ {F}ree: {S}imple and {C}orrect}.
1493: \newblock Tech. rept.~15. Dipartimento di Matematica, Universit\`{a} Degli
1494: Studi di Padova.
1495:
1496: \bibitem[\protect\citename{Hill {\em et~al.}\relax, }2002]{HBZ02}
1497: Hill, P., Bagnara, R., \& Zaffanella, E. (2002).
1498: \newblock Soundness, {I}dempotence and {C}ommutativity of {S}et-{S}haring.
1499: \newblock {\em Theory and {P}ractice of {L}ogic {P}rogramming}, {\bf 2}(2),
1500: 155--201.
1501:
1502: \bibitem[\protect\citename{King, }2000]{K00}
1503: King, A. (2000).
1504: \newblock Pair-{S}haring over {R}ational {T}rees.
1505: \newblock {\em Journal of {L}ogic {P}rogramming}, {\bf 46}(1--2), 139--155.
1506:
1507: \bibitem[\protect\citename{Langen, }1991]{L91}
1508: Langen, A. (1991).
1509: \newblock {\em Advanced {T}echniques for {A}pproximating {V}ariable {A}liasing
1510: in {L}ogic {P}rograms}.
1511: \newblock Ph.D. thesis, University of Southern California, Los Angeles.
1512:
1513: \bibitem[\protect\citename{Lassez {\em et~al.}\relax, }1988]{LMM88}
1514: Lassez, J-L., Maher, M., \& Marriott, K. (1988).
1515: \newblock Unification {R}evisited.
1516: \newblock {\em Pages 587--625 of:} {\em Foundations of {D}eductive {D}atabases
1517: and {L}ogic {P}rogramming}.
1518: \newblock Morgan Kaufmann.
1519:
1520: \bibitem[\protect\citename{Muthukumar \& Hermenegildo, }1992]{MH92}
1521: Muthukumar, K., \& Hermenegildo, M. (1992).
1522: \newblock Compile-time {D}erivation of {V}ariable {D}ependency using {A}bstract
1523: {I}nterpretation.
1524: \newblock {\em Journal of {L}ogic {P}rogramming}, {\bf 13}(2\&3), 315--347.
1525:
1526: \end{thebibliography}
1527:
1528: \end{document}
1529: