format: text

text:
# A Self-Similar Solution for the Propagation of a Relativistic Shock in an Exponential Atmosphere

## 1 Introduction

In a SuperNova (SN) explosion, the shock wave must ultimately emerge from the body of the star, and begin to propagate down the exponential density gradient of the stellar atmosphere. In Newtonian fluid dynamics, the propagation of such a shock is described by a self–similar solution (Raizer 1964; Grover and Hardy 1966; Hayes 1968). This self–similar solution is unavoidable (Raizer 1964). In fact, it turns out that, as the shock accelerates, a sonic point is formed, separating matter located immediately behind the shock from the flow’s initial conditions; this prevents pressure waves (i.e., causal information) to reach post–shock material from the the area where the flow’s initial conditions are set. Thus all flows will converge to the same solution, irrespective of their initial conditions. The lack of dependence upon initial conditions severely constrains the ensuing flow, by restricting the number of parameters upon which the shock evolution may depend; in fact, this constraint is so strong that only a single (self–similar) solution exists.

In the Newtonian solution, it is found that the shock velocity increases exponentially, in such a way that the shock reaches spatial infinity in a finite time. This is clearly impossible when account is taken of Special Relativity, and therefore the Newtonian solution must break down at high shock velocities, as expected. The question of precisely how the shock evolves in relativistic conditions has not been investigated so far.

This problem has acquired a new urgency within the HyperNova model (Paczyński 1998; MacFadyen & Woosley 1999) for Gamma Ray Bursts (GRBs). In fact, Meszaros and Rees (2001) have shown that, despite the large assumed energy release of the central engine, the outwardly moving shock in the large star hypothesized to give rise to the GRB can only reach a Lorentz factor of $`\mathrm{\Gamma }_i10`$ at the end of the H–envelope, and they had to invoke (without explicit computations) shock acceleration down the star exponential atmosphere to reach the required Lorentz factors of $`\mathrm{\Gamma }_f100300`$. The existence of a self-similar temporal structure in GRBs is also suggested by an analysis of their power spectra (Beloborodov, Stern, & Svensson 2000; see also Sivron 1998).

It is the purpose of this paper to derive a fully (Special) relativistic self–similar solution for the problem of shock propagation in an exponential atmosphere (Section 2), and to discuss its use in the HyperNova model for GRBs (Section 3).

## 2 Relativistic self–similar flow

We shall assume that a cold ($`T=0`$) material is stratified with density distribution $`\rho =\rho _{}\mathrm{exp}(kx)`$; the shock is supposed to move toward $`x=+\mathrm{}`$, thus with positive velocity $`v>0`$. The symmetry is assumed to be planar, since both the length scale of stellar atmospheres and the total extension of the atmosphere are much smaller than the stellar radius. In the Newtonian analog, the shock speed is set by a purely dimensional argument (e.g. Chevalier 1990): $`V=\alpha /kt`$, with $`\alpha `$ an adimensional constant to be determined. In the special relativistic problem, dimensional arguments alone fail because the presence of the light speed $`c`$ allows the construction of a new adimensional quantity ($`kct`$), thusly spoiling the above argument. We can however recover from this impasse by appealing to both dimensional and covariance arguments. The time–like part of the shock four–speed $`U_\mu `$ is of course determined by the identity $`U_\mu U^\mu =1`$, while the space–like part must be built in covariant fashion from the available quantities. Defining a four vector $`k_\mu =(0,k,0,0)`$, we can then write for the spatial part of $`U`$

$$U^a=\frac{dX^a}{ds}=\frac{\alpha k^a}{k_\mu k^\mu s}$$
(1)
where $`k_\mu k^\mu =k^2>0`$. This is the only sensible solution to our dimensional/covariant problem. We see from this that, as long as we use proper time, the structure of the problem is identical to that of the Newtonian analog. In particular, the shock reaches spatial infinity within a finite proper time. We may choose $`s=0`$ for the moment when this occurs, so that the flow is restricted to $`s<0`$. Incidentally, note that this implies $`\alpha <0`$. Physically, this makes perfect sense: as the shock accelerates, its proper time is contracted by its Lorentz factor ($`\mathrm{\Gamma }`$) with respect to the fluid time. The shock speed in terms of the fluid time can be obtained by remembering that $`dX/ds=v\mathrm{\Gamma }`$, and substituing in the above equation one finds ($`c=1`$ from now on)

$$s=\frac{\alpha }{kv\mathrm{\Gamma }}.$$
(2)
Taking the time derivative of both sides we obtain

$$\frac{kdt}{\alpha }=\mathrm{\Gamma }\left(\frac{d}{dv}\frac{1}{v\mathrm{\Gamma }}\right)dv$$
(3)
which can be immediately integrated to yield

$$\frac{kt}{\alpha }=\mathrm{log}\left(\frac{1+v}{1v}\right)^{1/2}\frac{1}{v}+\text{constant}.$$
(4)
The low speed limit $`v1`$ is $`kt/\alpha 1/v`$, in agreement with the Newtonian solution. The hyperrelativistic limit ($`v1`$) is

$$\frac{k(tt_i)}{\alpha }\mathrm{log}\mathrm{\Gamma }/\mathrm{\Gamma }_i$$
(5)
where we have introduced an initial shock Lorentz factor $`\mathrm{\Gamma }_i`$ at time $`t_i`$, for ease of use in the future. Since the shock moves essentially at speed $`1`$, we can rewrite the lhs of the above equation as $`\mathrm{log}(\rho /\rho _i)^{1/\alpha }`$, from which we see that the initial and the final (i.e., when the shock leaves the exponential atmosphere) shock Lorentz factors are related by

$$\frac{\mathrm{\Gamma }_f}{\mathrm{\Gamma }_i}=\left(\frac{\rho _f}{\rho _i}\right)^{1/\alpha }.$$
(6)
The above clearly shows that all we have left to do is to determine the value of the parameter $`\alpha `$. To this purpose, we must consider the fluid equations for the post–shock material, which we have found it convenient to take in the form given by Blandford and McKee (1976, their Eqs. 14-15)

$$\frac{d}{dt}(e\gamma ^4)=\gamma ^2\frac{e}{t}$$
(7)
$$\frac{d}{dt}\mathrm{log}(e^3\gamma ^4)=4\frac{v}{x}$$
(8)
$$\frac{n}{t}+\frac{}{x}(vn)=0$$
(9)
where $`d/dt=/t+v/x`$ is the convective derivative, and we have dropped curvature terms (which are contained in the Blandford and McKee equations), to keep with our planar symmetry approach. Here $`e`$ is the local energy density, $`\gamma `$ is the local fluid Lorentz factor, as seen from the reference frame of the unshocked material (to be distinguished from $`\mathrm{\Gamma }`$, the shock Lorentz factor in the same reference frame), and $`n`$ is the baryon number density always in the reference frame of the unshocked fluid. The above equations assume an hyperrelativistic equation of state for the post–shock material of the form $`p=e/3`$, which is correct in the limit $`\mathrm{\Gamma }\mathrm{}`$. Indeed, for the large shock Lorentz factors appropriate to this problem ($`\mathrm{\Gamma }10`$) Heavens & Drury (1988; see also Iwamoto 1989) showed that the adiabatic index of the flow is within $`1\%`$ of its asymptotic relativistic value of $`4/3`$, irrespective of the upstream temperature and plasma composition (see especially their Fig.2, and Eqs. 25-26). It should be remarked here that Eq. (6) remains valid whatever we assume for the equation of state, but the precise value of $`\alpha `$ depends instead on the particular choice of the equation of state.

The boundary conditions for this problem are provided by Taub’s jump conditions (Taub 1948), which again we take in the hyperrelativistic limit given by Blandford and McKee (1976):

$$e_2=2\mathrm{\Gamma }^2w_1,\gamma _2^2=\frac{1}{2}\mathrm{\Gamma }^2,n_2=2\mathrm{\Gamma }^2n_1.$$
(10)
Here the subscripts $`1,2`$ refer to pre– and post– shock quantities, respectively; $`n`$ and $`\gamma `$ are always defined in the unshocked fluid frame, and $`e`$ in the comoving frame. The enthalpy of the unshocked material, $`w_1`$, equals $`e_1`$ since this material is assumed to be cold. In our problem, $`e_1`$ is not a constant, because the atmosphere is stratified. We have

$$w_1=e_1=\rho _1=\rho _{}\mathrm{exp}(kX)=\rho _{}(\mathrm{\Gamma }/\mathrm{\Gamma }_i)^\alpha $$
(11)
so that, ultimately,

$$e_2=2\left(\frac{\rho _{}}{\mathrm{\Gamma }_i^\alpha }\right)\mathrm{\Gamma }^{2+\alpha }2q_{}\mathrm{\Gamma }^{2+\alpha }$$
(12)
which is the form we shall use in the following. An identical argument shows that

$$n_2=2\frac{n_{}}{\mathrm{\Gamma }_i^\alpha }\mathrm{\Gamma }^{2+\alpha }2z_{}\mathrm{\Gamma }^{2+\alpha },$$
(13)
where $`n_{}\rho _{}/m`$.

In order to search for a self–similar solution, we need to assume a form for the similarity variable. In the Newtonian analog, this is clearly $`\xi =k(xX)`$, where $`X`$ is the instantaneous shock location. In this problem, we take

$$\xi k(xX)\mathrm{\Gamma }^2.$$
(14)
The rationale for this is that, since post–shock material has a Lorentz factor which is $`\sqrt{2}`$ times smaller than the shock’s, the post–shock material falls behind the shock by an amount $`1/\mathrm{\Gamma }^2`$ as the shock covers an exponential length. Please notice that, with our notation, $`\xi <0`$ for the shocked material. The post–shock quantities $`\gamma ^2`$, $`e`$ and $`n`$ can then be taken of the form

$$\gamma ^2=g(\xi )\mathrm{\Gamma }^2,e=q_{}R(\xi )\mathrm{\Gamma }^{2+\alpha },n=z_{}\mathrm{\Gamma }^{2+\alpha }N(\xi )$$
(15)
with boundary conditions given by Eqs. (10) (the second one), (12), (13) as

$$g(0)=\frac{1}{2},R(0)=2,N(0)=2.$$
(16)
Substitution of Eqs. (14), (15) into Eqs. (7), (8) and (9) yields, after some algebra (the dot indicates derivation with respect to $`\xi `$)

$$\frac{\dot{R}}{R}=\frac{g(2/\alpha +1)(14\xi /\alpha +1/g)+(10/\alpha +3)}{3/23/2g6\xi /\alpha +(1g/2+2\xi g/\alpha )(14\xi /\alpha +1/g)}$$
(17)
$$\frac{\dot{g}}{g^2}=\frac{\dot{R}}{R}(1/g1/2+2\xi /\alpha )+(2/\alpha +1)$$
(18)
$$\frac{\dot{N}}{N}=\frac{2g\frac{2+\alpha }{\alpha }\frac{\dot{g}}{g}}{g(14\xi /\alpha )1}.$$
(19)
From these, we see what fixes $`\alpha `$: the denominator of the rhs of Eq. (17) goes to zero at a critical point $`\xi _c`$ and, unless the numerator simultaneously does the same (which will only occur for a special value of $`\alpha `$), a non–integrable singularity will ensue. The same phenomenon occurs in the Newtonian analog, where it has been shown that this critical point is a sonic point. It is exactly because there is a sonic point that a self–similar solution can develop: in fact, material between the shock and the sonic point is not in causal contact with post–sonic point material, and thus its properties cannot be determined by the problem’s initial conditions.

To keep the problem non–singular, we impose that the numerator and denominator of Eq. (17) vanish simultaneously, obtaining

$$g(\xi _c)(14\xi _c/\alpha )=\frac{8+2\alpha }{2+\alpha }$$
(20)
from the numerator, and

$$g(\xi _c)(14\xi _c/\alpha )=\frac{4\pm \sqrt{12}}{2}$$
(21)
for the denominator. The conditions above lead to two solutions for $`\alpha `$, one positive and another negative. The positive solution must be discarded because otherwise the shock would not reach spatial infinity for $`s0`$ (Eq. 1). We are therefore left with only one sensible solution,

$$\alpha =\frac{12\sqrt{192}}{6}4.309401.$$
(22)
The location of the sonic point, $`\xi _c`$, where both the numerator and the denominator vanish, is determined through numerical integration of Eqs. (17), (18) and (19). This yields $`\xi _c0.46`$. Also note that $`g(\xi )(14\xi /\alpha )g(0)=0.5`$, and therefore the denominator of Eq. (19) is always well-behaved. The full numerical solution for $`g(\xi )`$, $`R(\xi )`$ and $`N(\xi )`$ is illustrated in Fig. 1.

## 3 Application to GRBs

It can be seen from Eq. (6) that the necessary asymptotic Lorentz factor required for a proper modelling of the properties of GRBs, i.e. $`\mathrm{\Gamma }_f150`$ (remember that the Lorentz factor of the matter is only $`1/\sqrt{2}`$ that of the shock) can be reached by crossing a modest factor of $`10^5`$ density decrease in the exponential atmosphere (assuming $`\mathrm{\Gamma }_i10`$). Yet, the total energy of material moving at these large Lorentz factors is only modest. In fact, let us compute the distribution of kinetic energy with baryon number. Consider a cylindrical fluid element with surface area $`A`$ (with the normal along the direction of fluid motion $`x`$), and length $`dx`$ along the direction $`x`$. This element will have a bulk kinetic energy of $`dE=Amc^2n(x)\gamma (x)dx=A\rho _{}c^2\mathrm{\Gamma }^{1+\alpha }\mathrm{\Gamma }_i^\alpha N(\xi )g^{1/2}(\xi )k^1d\xi `$. What we want to know is the energy distribution at the moment in which the shock gets out of the exponential atmosphere. Let us indicate with $`\mathrm{\Gamma }_f`$ the shock Lorentz factor at that moment. Then

$$\gamma \frac{dE}{d\gamma }=2A\rho _ic^2k^1\mathrm{\Gamma }_i^\alpha \mathrm{\Gamma }_f^{1+\alpha }\frac{N(\xi )g^{3/2}(\xi )}{\dot{g}}$$
(23)
which can be coupled to the solution $`g=g(\xi )`$ to yield a parametric representation of $`\gamma dE/d\gamma `$, the distribution of kinetic energy with respect to the final Lorentz factor. The adimensional part of the function in the previous equation is plotted in Fig. 2. The numerical factor can be estimated using Eq. (6):

$$\gamma \frac{dE}{d\gamma }=10^{48}\mathrm{erg}\left(\frac{r_H}{10^{13}\mathrm{cm}}\right)^2\left(\frac{k^1}{10^{12}\mathrm{cm}}\right)\left(\frac{\rho _i}{10^9\mathrm{cm}^3}\right)\left(\frac{10}{\mathrm{\Gamma }_i}\right)^\alpha \left(\frac{\mathrm{\Gamma }_f}{150}\right)^{\alpha +1}\frac{2N(\xi )g^{3/2}(\xi )}{\dot{g}}.$$
(24)
In this expression, the values for $`r_H`$ (the edge of the H–shell), $`\rho _i`$ (the matter density at the end of the H–shell, and thus presumably at the beginning of the exponential atmosphere), and $`\mathrm{\Gamma }_i`$ (the shock Lorentz factor at the end of the H–shell $`=`$ beginning of the exponential atmosphere) are taken from Meszaros and Rees (2001). Taking the adimensional factor from Fig.2, we see that the kinetic energy falls short of the average isotropic burst energy (Schmidt 1999) by about three orders of magnitude (note that here what we are computing is the isotropic energy).

Before showing how to come out of this impasse, we need to consider which part of Fig. 2 can actually be obtained in a realistic model. The reason for this limitation comes from the fact that the idealized model presented here has been propagating down an exponential atmosphere forever, while in a realistic model only a finite amount of matter can have converged onto this self–similar solution, given the finite dimension of the star. For this reason, we have plotted in Fig. 2 three ticks, which correspond to the present position of matter which was located, before being reached by the shock, at $`5,10,15`$ exponential scale–lengths from the shock’s present location. If we think that the initial atmosphere extends for $`5,10,15`$ exponential scale–lengths, then we can believe the part of Fig. 2 located to the right of their respective tickmarks. Leftward of them, the true, physical solution will depart from the one shown here, and the total kinetic energy at the corresponding values of Lorentz factor will be much smaller than the values plotted (obviously, since the physical solution has finite mass and energy, which is not true for the idealized one).

Let us now suppose that the putative burst progenitor possesses a wide exponential atmosphere, spanning some $`9`$ orders of magnitude in density. Then, for an initial Lorentz factor $`\mathrm{\Gamma }_i10`$, the shock Lorentz factor at the end of the atmosphere is $`1000`$ (Eq. 6); once again, the overall energy of matter moving at this speed would be modest ($`10^{46}`$ erg), but Fig. 2 shows that most of the energy (before the cutoff implied by the finite extent of the atmosphere) will come out at a Lorentz factor $`0.2`$ of the shock’s factor, i.e. at $`\mathrm{\Gamma }_{matter}200`$. With the values above, the total energy then amounts to $`6\times 10^{52}`$ erg, in reasonable agreement with Schmidt’s (1999) isotropic estimates111 Spectral properties (i.e. line production) would be similar to those predicted by Kallaman, Meszaros & Rees (2001).. It should be noticed that inspection of the numerical solution for large values of the distance parameter $`\xi `$ shows the material to be cold ($`en`$), so that there will be negligible further acceleration of these slower shells by $`pdV`$ work, and $`\mathrm{\Gamma }_{\mathrm{matter}}200`$ remains a good estimate of the coasting Lorentz factor.

To summarize, the application of our solution to shock acceleration in the atmosphere of a massive star has shown that, in atmospheres with small density range, the amount of energy carried by material accelerated to the typical GRB Lorentz factors falls short of the GRB required energetics. However, for stars with a wide density range in their atmospheres ($`10^9`$ orders of magnitude), a sufficient quantity of energy is carried by later shells of material moving at the typical GRB Lorentz factors. In this model, the early emission would be dominated by an ultra–hard component, due to the very large–$`\mathrm{\Gamma }`$ shells slowing down in the ISM. This is at least qualitatively consistent with virtually all bursts studied in some detail by BeppoSAX (Frontera et al., 2000, see especially their Fig. 2), which exhibit, in their first few seconds only, spectra peaking beyond the instrument’s (GRBM) observing limit of $`700`$ keV.

RP thanks the Osservatorio Astronomico di Roma for its kind hospitality during the time that this work was carried out.


text:
# Three Optimisations for Sharing

## 1 Introduction

A set-sharing analyser will usually also track freeness and linearity. This is because freeness and linearity are cheap to maintain and result in more accurate, that is smaller, sharing abstractions which in turn improve the efficiency of the sharing component of abstract unification. However, current abstract unification algorithms for sharing, freeness and linearity are suboptimal. This paper considers how to improve the precision of sharing with freeness and linearity by considering the interaction of these components. These refinements do not incur a significant computational overhead. To this end three optimisations are given, along with examples of where precision is gained. Their cost is discussed and correctness proved.

The first optimisation follows from the observation that the algorithms for pair-sharing with linearity can sometimes out perform set-sharing with linearity (in terms of which pairs of variables may share). This is because of an independence check which pervades the set-sharing literature (from early work \[Langen, 1991\] to the most recent and comprehensive \[Bagnara et al., 2000\]). This check is in fact redundant. By removing this, the precision of abstract unification is improved, since linearity can be exploited more frequently.

Filé \[Filé, 1994\] observed that freeness can be used to decompose a sharing abstraction into a set of sharing abstractions. For each component of the decomposition, the sharing groups of that component do not (definitely) arise from different computational paths. Abstract unification can then be applied to each component and the resulting abstractions merged. This tactic has not been included in analysers owing to its prohibitive cost. The second optimisation is a lightweight refinement of abstract unification inspired by the decomposition. Though not as precise as the full decomposition, it does achieve the necessary balance between cost and benefit.

Thirdly, an optimisation for pruning sharing groups is presented. This tactic demonstrates that sharing in combination with freeness can improve groundness which, in turn, can improve sharing (even in the presence of rational trees). Put another way, it means that any optimal algorithm for sharing, freeness and linearity will have to consider subtle interactions between sharing, freeness and groundness.

One principle of set-sharing is that the number of sharing groups should be minimised. As well as increasing precision, this can improve efficiency and possibly avoid widening. A fourth technique is proposed which can prune the size of inputs to the abstract unification algorithm by considering the grounding behaviour of sets of equations. Reducing the size of the inputs (and intermediate abstractions) simplifies abstract unification and can thereby improve performance. Whilst the technique will not theoretically improve the precision of the overall result, in practice, a precision gain might be achieved if widening is avoided within the unification algorithm.

Correctness is expressed in terms of a novel concretisation map which characterises equations as their idempotent most general unifiers. This simplifies the correctness arguments and in particular enables the abstract unification algorithms to be proved correct for rational tree constraint solving (as adopted by SICStus Prolog and Prolog-III). To the best of the authors’ knowledge, this is the first proof of correctness for a sharing, freeness and linearity analysis in the presence of rational trees. (Previous work for rational tree unification has either focused on pair-sharing \[King, 2000\] or set-sharing without freeness and linearity \[Hill et al., 2002\]).

In summary, this paper provides the implementor with a number of low-cost techniques for improving the precision and efficiency of sharing analyses.

## 2 Preliminaries

### 2.1 Trees and terms

Let $`\epsilon `$ denote the empty sequence, . denote sequence concatenation, and $`\alpha `$ denote the length of a sequence $`\alpha ^{}`$. A tree (or term) over an alphabet of symbols $`F`$ is a partial map $`t:^{}F`$ such that $`t(\alpha )=t`$ if $`\alpha =\epsilon `$, otherwise $`t(\alpha )=t_i(\beta )`$ where $`\alpha =i.\beta `$ and $`t=f(t_1,\mathrm{},t_n)`$. Let $`T(F)`$ and $`T^{\mathrm{}}(F)`$ denote the set of finite and possibly infinite trees over $`F`$. Let $`U`$ denote a (denumerable) universe of variables such that $`FU=\mathrm{}`$, and let $`var(t)`$ = $`\{uU\alpha ^{}.t(\alpha )=u\}`$ where $`tT^{\mathrm{}}(FU)`$. Finally, $`|S|`$ denotes the cardinality of the set $`S`$.

### 2.2 Substitutions and equations

A substitution is a (total) map $`\theta :UT^{\mathrm{}}(FU)`$ such that $`dom(\theta )`$ = $`\{uU\theta (u)u\}`$ is finite. A substitution $`\theta `$ can be represented as a finite set $`\{x\theta (x)xdom(\theta )\}`$. Let $`rng(\theta )`$ = $`\{var(\theta (u))udom(\theta )\}`$ and let $`Sub`$ denote the set of substitutions. If $`\theta =\{x_it_i\}_{i=1}^n`$ then $`\theta (t)`$ denotes the tree obtained by simultaneously replacing each occurrence of $`x_i`$ in $`t`$ with $`t_i`$. For brevity, let $`\theta (x,\alpha )`$ = $`t(\alpha )`$ where $`\theta (x)`$ = $`t`$. An equation $`e`$ is a pair $`(s=t)`$ where $`s,tT^{\mathrm{}}(FU)`$. A finite set of equations is denoted $`E`$ and $`Eqn`$ denotes the set of finite sets of equations. Also define $`\theta (E)`$ = $`\{\theta (s)=\theta (t)(s=t)E\}`$. The map $`eqn:SubEqn`$ is defined $`eqn(\theta )`$ = $`\{x=t(xt)\theta \}`$. Where $`YU`$, projection out and projection onto are respectively defined $`Y.\theta `$ = $`\{xt\theta xY\}`$ and $`\overline{}Y.\theta `$ = $`(UY).\theta `$. Composition $`\theta \psi `$ of two substitutions is defined so that $`(\theta \psi )(u)=\theta (\psi (u))`$ for all $`uU`$. Composition induces the (more general than) relation $``$ defined by $`\theta \psi `$ iff there exists $`\delta Sub`$ such that $`\psi =\delta \theta `$. A renaming is a substitution $`\rho Sub`$ that has an inverse, that is, there exists $`\rho ^1Sub`$ such that $`\rho ^1\rho =id`$. The set of renamings is denoted $`Rename`$. A substitution $`\theta `$ is idempotent iff $`\theta \theta =\theta `$, or equivalently, iff $`dom(\theta )rng(\theta )=\mathrm{}`$.

### 2.3 Solved forms and most general unifiers

A substitution is in rational solved form iff it has no subset $`\{x_1x_2`$, $`\mathrm{}`$, $`x_nx_1\}`$ where $`n2`$. The subset of $`Sub`$ in rational solved form is denoted $`RSub`$. The set of unifiers of $`E`$ is defined by: $`unify(E)`$ = $`\{\theta Sub(s=t)E.\theta (s)=\theta (t)\}`$. The set of most general unifiers (mgus) and the set of idempotent mgus (imgus) are defined: $`mgu(E)=\{\theta unify(E)\psi unify(E).\theta \psi \}`$ and $`imgu(E)=\{\theta mgu(E)dom(\theta )rng(\theta )=\mathrm{}\}`$. Note that $`imgu(E)\mathrm{}`$ iff $`mgu(E)\mathrm{}`$ \[Lassez et al., 1988\]. An mgu can be renamed to obtain any other (as can an imgu).

###### Lemma 2.1 (Proposition 11 from \[Lassez et al., 1988\])

Let $`\theta imgu(E)`$. Then $`\varphi imgu(E)`$ iff there exists $`\{x_iy_i\}_{i=1}^n\theta `$ such that $`\varphi =\{x_iy_i,y_ix_i\}_{i=1}^n\theta `$.

One way to obtain an imgu is by considering limits of substitutions.

###### Definition 2.1

Let $`\{t_nn\}T^{\mathrm{}}(FU)`$. Then $`t=lim_n\mathrm{}t_n`$ iff for all $`k`$ there exists $`l`$ such that for all $`ml`$ and $`\alpha k`$, $`t(\alpha )=t_m(\alpha )`$. Furthermore, if $`\{\theta _nn\}Sub`$ then $`lim_n\mathrm{}\theta _n=\lambda x.lim_n\mathrm{}\theta _n(x)`$.

Note that $`lim_n\mathrm{}\theta ^n`$ exists iff $`\theta RSub`$ \[King, 2000\]. Henceforth $`\theta ^{\mathrm{}}`$ abbreviates $`lim_n\mathrm{}\theta ^n`$. If $`\theta RSub`$ then $`\theta ^{\mathrm{}}`$ is idempotent whereas if $`\theta `$ is idempotent then $`\theta ^{\mathrm{}}=\theta `$. The following lemmas detail how limits of substitutions and composition of substitutions relate to an mgu.

###### Lemma 2.2 (Lemmas 2.2, 4.3 and 4.4 from \[King, 2000\])

1. $`\theta ^{\mathrm{}}mgu(eqn(\theta ))`$ if $`\theta RSub`$.
2. $`\delta \theta ^{\mathrm{}}mgu(Eeqn(\theta ))`$ if $`\delta mgu(\theta ^{\mathrm{}}(E))`$.
3. $`(dom(\theta )rng(\theta )).\delta mgu(\theta (E))`$ if $`\delta \theta mgu(E)`$.

### 2.4 Linearity

Variable multiplicity is defined in order to formalise linearity. The significance of linearity is that unification of linear terms enables sharing to be described by more precise sharing abstractions (even in the presence of rational trees).

###### Definition 2.2

The variable multiplicity map $`\chi :T^{\mathrm{}}(FU)\{0,1,2\}`$ is defined: $`\chi (t)=\mathrm{max}(\{\chi (x,t)xU\})`$ where $`\chi (x,t)=\mathrm{min}(2,|\{\alpha t(\alpha )=x\}|)`$.

If $`\chi (t)=0`$, $`t`$ is ground; if $`\chi (t)=1`$, $`t`$ is linear; and if $`\chi (t)=2`$, $`t`$ is non-linear. The next lemma details the forms of sharing barred by the unification of linear terms.

###### Lemma 2.3 (Proposition 3.1 from \[King, 2000\])

If $`\theta mgu(\{s=t\})`$, $`xy`$ and $`var(\theta (x))var(\theta (y))\mathrm{}`$ then either: $`xvar(s)`$ and $`yvar(t)`$; or $`x,yvar(t)`$ and $`\chi (s)=2`$; or $`xvar(t)`$ and $`yvar(s)`$; or $`x,yvar(s)`$ and $`\chi (t)=2`$.

The correctness arguments for abstract unification require lemma 2.3 to be augmented with a new result – lemma 2.4. The proof of this lemma is analogous to that of lemma 2.3 detailed in \[King, 2000\].

###### Lemma 2.4

If $`\theta mgu(\{s=t\})`$ and $`\chi (\theta (x))=2`$ then either: $`xvar(s)var(t)`$; or $`xvar(t)`$ and $`\chi (s)=2`$; or $`xvar(s)`$ and $`\chi (t)=2`$.

### 2.5 Groundness and sharing abstractions

The abstract domains of interest in this paper are represented either as Boolean functions, or as sets or as sets of sets. Let $`X`$ denote a finite subset of $`U`$. The set of propositional formulae over $`X`$ is denoted by $`\text{Bool}_X`$ and $`Y`$ abbreviates the formula $`Y`$. The (bijective) map $`\text{model}_X:\text{Bool}_X\mathrm{}(\mathrm{}(X))`$ is defined by $`\text{model}_X(f)=\{MX\psi _X(M)f\}`$ where $`\psi _X(M)=M\{\neg yyXM\}`$. The groundness, sharing, freeness and linearity domains over $`X`$ are defined as follows:

###### Definition 2.3

$`Pos_X`$ = $`\{fBool_XXf\}`$, $`Sh_X`$ = $`\{S\mathrm{}(X)\mathrm{}S\}`$, $`Fr_X`$ = $`\mathrm{}(X)`$ and $`Lin_X`$ = $`\mathrm{}(X)`$.

If $`SSh_X`$, then each $`GS`$ is referred to as a sharing group.

These domains are connected to the concrete domain of sets of equations by Galois connections induced by the concretisation maps. This approach leads to succinct statements of correctness. To obtain well defined concretisations, maps abstracting substitutions are introduced. It is then observed that the abstractions for equivalent idempotent substitutions are the same.

###### Definition 2.4

The abstraction maps $`\alpha ^{Pos}:SubPos_U`$ and $`\alpha _X^{Sh}:SubSh_X`$ are defined: $`\alpha ^{Pos}(\theta )`$ = $`\{xvar(t)xt\theta \}`$, $`\alpha _X^{Sh}(\theta )`$ = $`\{occ(\theta ,u)XuU\}`$ and $`occ(\theta ,y)=\{uUyvar(\theta (u))\}`$.

###### Lemma 2.5

Let $`\theta ,\varphi imgu(E)`$. Then $`\alpha ^{Pos}(\theta )=\alpha ^{Pos}(\varphi )`$, $`\alpha _X^{Sh}(\theta )=\alpha _X^{Sh}(\varphi )`$, $`\theta (x)U`$ iff $`\varphi (x)U`$ and $`\chi (\theta (x))1`$ iff $`\chi (\varphi (x))1`$.

###### Proof 2.1.

By lemma 2.1 there exists $`\{x_iy_i\}_{i=1}^n\theta `$ such that $`\varphi =\rho \theta `$ where $`\rho =\{x_iy_i,y_ix_i\}_{i=1}^n`$.

1. Let $`xt\theta `$. Observe that $`\{x\rho (t),y_1x_1,\mathrm{},y_nx_n\}\rho \theta `$ and $`y_ivar(t)`$ iff $`x_ivar(\rho (t))`$, thus $`\alpha ^{Pos}(\varphi )xvar(\rho (t))(_{i=1}^ny_ix_i)xvar(t)`$. Hence $`\alpha ^{Pos}(\varphi )\alpha ^{Pos}(\theta )`$. The other direction is similar.
2. Observe that $`occ(\rho \theta ,y_i)=occ(\theta ,x_i)`$, $`occ(\rho \theta ,x_i)=occ(\theta ,y_i)`$ and $`occ(\rho \theta ,u)`$ = $`occ(\theta ,u)`$ for all $`udom(\rho )rng(\rho )`$. Hence $`\alpha _X^{Sh}(\theta )=\alpha _X^{Sh}(\varphi )`$.
3. and 4. Immediate.

Instead of defining concretisation in terms of a particular imgu (the limit of a rational solved form \[King, 2000\]), an arbitrary imgu is used. This new approach simplifies correctness proofs.

###### Definition 2.2.

The concretisation maps $`\gamma _X^{Pos}:Pos_X\mathrm{}(Eqn)`$, $`\gamma _X^{Sh}:Sh_X\mathrm{}(Eqn)`$, $`\gamma _X^{Fr}:Fr_X\mathrm{}(Eqn)`$ and $`\gamma _X^{Lin}:Lin_X\mathrm{}(Eqn)`$ are respectively defined by:

$$\begin{array}{cc}\hfill \gamma _X^{Pos}(f)=& \{EEqn\theta imgu(E).\alpha ^{Pos}(\theta )f\}\hfill \\ \hfill \gamma _X^{Sh}(S)=& \{EEqn\theta imgu(E).\alpha _X^{Sh}(\theta )S\}\hfill \\ \hfill \gamma _X^{Fr}(F)=& \{EEqn\theta imgu(E).xF.\theta (x)U\}\hfill \\ \hfill \gamma _X^{Lin}(L)=& \{EEqn\theta imgu(E).xL.\chi (\theta (x))1\}\hfill \end{array}$$

Each free variable is linear so that $`\gamma _X^{Fr}(F)\gamma _X^{Lin}(L)`$ = $`\gamma _X^{Fr}(F)\gamma _X^{Lin}(LF)`$. This paper is concerned with combined domains and the following combined concretisation maps will be useful: $`\gamma _X^{SF}(S,F)=\gamma _X^{Sh}(S)\gamma _X^{Fr}(F)`$ and $`\gamma _X^{SFL}(S,F,L)`$ = $`\gamma _X^{SF}(S,F)\gamma _X^{Lin}(L)`$.

A connection is established in \[Codish et al., 1999\] which sheds light on the relationship between sharing and Boolean functions. The corollary (also observed in the long version of \[Bagnara et al., 2000\]) explains how this can be used to improve precision of combined domains.

###### Lemma 2.3 (Observation 4.1 and lemma 5.1 from \[Codish et al., 1999\]).

$`\{XGG\alpha _X^{Sh}(\theta )\}model_X(\alpha ^{Pos}(\theta ))`$ where $`\theta `$ is idempotent.

###### Corollary 2.4.

$`\gamma _X^{Pos}(f)\gamma _X^{Sh}(S)=\gamma _X^{Pos}(f)\gamma _X^{Sh}(trim_X(f,S))`$ where $`trim_X(f,S)=\{GSXGmodel_X(f)\}`$.

Finally, the following auxiliary operations will be used throughout the paper. Let $`S,S_iSh_X`$. The relevance map is defined $`rel(t,S)=\{GS|var(t)G\mathrm{}\}`$; closure is defined $`S^{}=\{S^{}SS^{}G_1,G_2S^{}.G_1G_2S^{}\}`$; and pair-wise union is defined $`S_1S_2=\{G_1G_2G_1S_1G_2S_2\}`$. Observe that if $`var(rel(s,S))var(rel(t,S))=\mathrm{}`$ then $`var(\theta (s))var(\theta (t))=\mathrm{}`$ for all $`\theta imgu(E)`$ and $`E\gamma _X^{Sh}(S)`$. Thus the independence check $`var(rel(s,S))var(rel(t,S))=\mathrm{}`$ can verify that two terms $`s`$ and $`t`$ do not share under $`\theta `$ (or equivalently $`E`$).

## 3 Independence check in set-sharing

The following example demonstrates that pair-sharing can sometimes detect independence when standard set-sharing unification algorithms cannot.

###### Example 3.1.

Let $`X=\{u,v,w,x,y,z\}`$ and consider $`E\gamma _X^{SFL}(S,F,L)`$ where $`S=\{\mathrm{},\{u,w\}`$, $`\{v,w\}`$, $`\{x,y\}`$, $`\{x,z\}`$, $`\{w,x\}\}`$, $`F=\mathrm{}`$ and $`L=X`$. Let $`\theta ^{}imgu(E\{w=x\})`$. The set-sharing unification algorithms of \[Langen, 1991, Bagnara et al., 2000\] give the following abstraction $`S^{}=\{\mathrm{}\}(S_w^{}S_x^{})`$ for $`\theta ^{}`$ where $`S_w=\{\{u,w\},\{v,w\},\{w,x\}\}`$ and $`S_x=\{\{x,y\},\{x,z\},\{w,x\}\}`$. Observe that $`\{u,v,w\}S_w^{}`$ and $`\{x,y,z\}S_x^{}`$ and therefore $`S^{}`$ does not assert the independence of $`u`$ and $`v`$ (similarly $`y`$ and $`z`$). However, if $`S`$ is interpreted as a set of pairs, then the pair-sharing abstract unification algorithms of \[Codish et al., 1991, King, 2000\] both give the abstraction $`S\{\{w\},\{x\},\{u,x\},\{u,y\},\{u,z\},\{v,x\},\{v,y\},\{v,z\},\{w,y\},\{w,z\}\}`$ which states the independence of $`u`$ and $`v`$ (and similarly $`y`$ and $`z`$). Note that this different does not stem from a difference in the set-sharing and pair-sharing domains, but derives from the way in which linearity is exploited in the abstract unification algorithms.

The crucial difference between pair-sharing and set-sharing algorithms is that the former does not require the terms in the equation to be independent to exploit linearity. Put another way, to apply linearity the latter requires that $`var(rel(s,S))var(rel(t,S))=\mathrm{}`$ when solving the equation $`s=t`$ in the context of the sharing abstraction $`S`$. Lemmas 2.3 and 2.4 detail the forms of sharing that can arise in $`mgu(\{s^{}=t^{}\})`$ rational (and finite) tree unification where $`s^{}`$ and $`t^{}`$ are arbitrary terms. Observe that $`s^{}`$ and $`t^{}`$ are not required to be independent. Abstract unification algorithms with the independence check are safe. However, this check is not fundamental to combining sharing with linearity. By observing how to exploit linearity more fully, a more precise abstract unification algorithm can be obtained. This algorithm also explains why algorithms with the independence check are safe. The following abstract operator is used to approximate the multiplicity map in abstract unification. Lemma 3.3 asserts its correctness.

###### Definition 3.2.

$$\chi (t,S,L)=\{\begin{array}{ccccc}2\hfill & \mathrm{if}x\hfill & & \hfill var(S)& .\chi (x,t)=2\hfill \\ 2\hfill & \mathrm{if}x\hfill & & \hfill var(S)& .xvar(t)L\hfill \\ 2\hfill & \mathrm{if}x,y\hfill & & \hfill var(t)& .GS.xyx,yG\hfill \\ 1\hfill & \multicolumn{4}{c}{\mathrm{otherwise}}\end{array}$$

###### Lemma 3.3.

If $`E\gamma _X^{Sh}(S)\gamma _X^{Lin}(L)`$ and $`\theta imgu(E)`$ then $`\chi (\theta (t))\chi (t,S,L)`$.

###### Proof 3.4.

Suppose $`\chi (\theta (t))=2`$. One of the following holds:

* There exists $`xvar(t)`$ such that $`\chi (x,t)=2`$ and $`var(\theta (x))\mathrm{}`$. Then $`xvar(S)`$ so that $`\chi (t,S,L)=2`$.
* There exists $`xvar(t)`$ such that $`\chi (\theta (x))=2`$. Then $`xvar(S)`$ and $`xvar(t)L`$ so that $`\chi (t,S,L)=2`$.
* There exist $`x,yvar(t)`$ such that $`xy`$ and $`var(\theta (x))var(\theta (y))\mathrm{}`$. Then there exists $`GS`$ such that $`x,yG`$ so that $`\chi (t,S,L)=2`$.

The revised abstract unification algorithm (with the independence check removed) is detailed in definition 3.5, and theorem 3.6 establishes its correctness.

###### Definition 3.5 (Abstract unification 1).

Abstract unification $`amgu_1(S,F,L,s,t)=S^{},F^{},L^{}`$ is defined:

$$S_s=rel(s,S)S_t=rel(t,S)S^{}=(S(S_sS_t))S^{\prime \prime }G^{}=Xvar(S^{})$$

$$S^{\prime \prime }=\{\begin{array}{cccc}\hfill S_s& & S_t\hfill & \mathrm{if}sFtF\hfill \\ \hfill (S_s^{}S_t)& & (S_sS_t^{})\hfill & \mathrm{if}\chi (s,S,L)=\chi (t,S,L)=1\hfill \\ \hfill S_s^{}& & S_t\hfill & \mathrm{if}\chi (s,S,L)=1\hfill \\ \hfill S_s& & S_t^{}\hfill & \mathrm{if}\chi (t,S,L)=1\hfill \\ \hfill S_s^{}& & S_t^{}\hfill & \mathrm{otherwise}\hfill \end{array}$$

$$F^{}=\{\begin{array}{cc}F\hfill & \mathrm{if}sFtF\hfill \\ Fvar(S_s)\hfill & \mathrm{if}sF\hfill \\ Fvar(S_t)\hfill & \mathrm{if}tF\hfill \\ Fvar(S_sS_t)\hfill & \mathrm{otherwise}\hfill \end{array}$$

$$L^{}=F^{}G^{}\{\begin{array}{cc}L(var(S_s)var(S_t))\hfill & \mathrm{if}\chi (s,S,L)=1\chi (t,S,L)=1\hfill \\ Lvar(S_s)\hfill & \mathrm{if}\chi (s,S,L)=1\hfill \\ Lvar(S_t)\hfill & \mathrm{if}\chi (t,S,L)=1\hfill \\ Lvar(S_sS_t)\hfill & \mathrm{otherwise}\hfill \end{array}$$

A precision gain over previous algorithms follows since a closure is avoided if $`s`$ is linear but not $`t`$ (or vice versa) and $`s`$ and $`t`$ are not independent. When both $`s`$ and $`t`$ are linear, but not independent, two closures are required (as previously), but the resulting sharing abstraction may contain fewer elements owing to the pruning effect of intersection. When the independence check is satisfied, that is $`S_sS_t=\mathrm{}`$, it follows that $`(S_s^{}S_t)(S_sS_t^{})`$ = $`S_sS_t`$. This explains why algorithms with the independence check are safe. Note that if $`s`$ and $`t`$ are both linear, but not independent, an implementor might trade precision for efficiency by computing $`S_s^{}S_t`$ if $`|S_s||S_t|`$ and $`S_sS_t^{}`$ otherwise.

###### Theorem 3.6 (Correctness of abstract unification 1).

Let $`E\gamma _X^{SFL}(S,F,L)`$, $`var(s)var(t)X`$ and $`amgu_1(S,F,L,s,t)=S^{},F^{},L^{}`$. Then $`E\{s=t\}\gamma _X^{SFL}(S^{},F^{},L^{})`$.

###### Proof 3.7.

Put $`E^{}=\{s=t\}`$. Let $`\theta imgu(E)`$ and $`\theta ^{}imgu(EE^{})`$. Observe that $`unify(\theta (E^{}))unify(\theta (E^{})eqn(\theta ))=unify(E^{}eqn(\theta ))=unify(EE^{})\mathrm{}`$. Thus let $`\delta imgu(\theta (E^{}))=imgu(\theta ^{\mathrm{}}(E^{}))`$. By part 2 of lemma 2.2, $`\delta \theta ^{\mathrm{}}mgu(eqn(\theta )E^{})=mgu(EE^{})`$. Since $`dom(\theta )rng(\delta )=\mathrm{}`$, $`\delta \theta ^{\mathrm{}}=\delta \theta imgu(EE^{})`$.

1. To show $`\alpha _X^{Sh}(\delta \theta )S^{}`$, let $`yU`$ and consider $`occ(\delta \theta ,y)`$.

1. Suppose $`yrng(\delta \theta )`$.

    1. Suppose $`ydom(\delta \theta )`$, that is, $`\delta \theta (y)=y`$. Thus $`\theta (y)=y^{}`$ and $`\delta (y^{})=y`$. Suppose $`yy^{}`$. Then $`ydom(\theta )`$, thus $`yrng(\delta )`$ which is a contradiction. Therefore $`y=y^{}`$, giving $`\theta (y)=y`$ and $`\delta (y)=y`$.

        1. Suppose $`yvar(\theta (s))`$ and $`yvar(\theta (t))`$. Hence $`ydom(\delta )`$ and $`yrng(\delta )`$, so that $`occ(\delta \theta ,y)X`$ = $`occ(\theta ,y)XS`$. But $`var(s)occ(\theta ,y)=\mathrm{}`$ and similarly $`var(t)occ(\theta ,y)=\mathrm{}`$, so that $`occ(\delta \theta ,y)XS^{}`$.
            2. Suppose $`yvar(\theta (s))`$ and $`yvar(\theta (t))`$. Since $`\delta (y)=y`$, it follows that $`yvar(\delta \theta (s))=var(\delta \theta (t))`$. Suppose $`yrng(\delta )`$, then $`ydom(\theta )`$, hence $`yrng(\delta \theta )`$ which is a contradiction. Therefore $`yrng(\delta )`$, thus $`yvar(\theta (t))`$ which is a contradiction.
            3. Suppose $`yvar(\theta (s))`$ and $`yvar(\theta (t))`$. Analogous to the previous case.
            4. Suppose $`yvar(\theta (s))`$ and $`yvar(\theta (t))`$. Since $`\delta (y)`$ = $`y`$ and $`yrng(\delta \theta )`$, $`yrng(\theta )`$. Thus $`yvar(s)`$ and $`yvar(t)`$. Since $`yrng(\theta )`$, it follows that $`ydom(\theta )`$, therefore $`yrng(\delta )`$. Thus, $`occ(\delta \theta ,y)=occ(\theta ,y)`$. Therefore $`occ(\delta \theta ,y)XS_s`$ since $`var(s)X`$ and $`occ(\delta \theta ,y)XS_t`$ since $`var(t)X`$. Thus $`occ(\delta \theta ,y)XS^{}`$.
        2. Suppose $`ydom(\delta \theta )`$. Since $`yrng(\delta \theta )`$, $`occ(\delta \theta ,y)X=\mathrm{}S^{}`$.
    2. Suppose $`yrng(\delta \theta )var(\theta (E^{}))`$. Then $`ydom(\delta )`$ and $`yrng(\delta )`$ so that $`occ(\delta \theta ,y)=occ(\theta ,y)`$. Moreover, since $`yvar(\theta (E^{}))`$ it follows that $`occ(\delta \theta ,y)XS(S_sS_t)S^{}`$.
    3. Suppose $`yrng(\delta \theta )var(\theta (E^{}))`$. Since $`occ(\delta ,y)var(\theta (s))var(\theta (t))`$, $`occ(\delta \theta ,y)X=\{occ(\theta ,u)Xuocc(\delta ,y)\}=(R_s)(R_t)`$, where $`R_s=\{occ(\theta ,v)Xvvar(\theta (s))occ(\delta ,y)\}`$ and $`R_t=\{occ(\theta ,w)Xwvar(\theta (t))occ(\delta ,y)\}`$. If $`R_s=\mathrm{}`$, then $`yvar(\delta \theta (s))=var(\delta \theta (t))`$, hence $`R_t=\mathrm{}`$ and $`occ(\delta \theta ,y)X=\mathrm{}S^{}`$. Likewise $`occ(\delta \theta ,y)X=\mathrm{}S^{}`$ if $`R_t=\mathrm{}`$. Thus suppose $`R_s\mathrm{}`$ and $`R_t\mathrm{}`$. Since $`var(s)X`$, $`R_sS_s`$ and since $`var(t)X`$, $`R_tS_t`$.

    1. Suppose $`sF`$. Thus $`\theta (s)U`$, hence $`|R_s|=|var(\theta (s))|=1`$. Moreover $`\chi (\theta (s))1`$. Suppose $`|R_tR_s|>1`$. Thus there exists $`uv`$ such that $`u,vvar(\theta (t))var(\theta (s))`$ and $`var(\delta (u))var(\delta (v))\mathrm{}`$. This contradicts lemma 2.3, hence $`|R_tR_s|1`$. Thus $`occ(\delta \theta ,y)XS_sS_t`$.
        2. Suppose $`tF`$. Analogous to the previous case.
        3. Suppose $`\chi (s,S,L)=1`$. Thus $`\chi (\theta (s))1`$. As with case 1(c)i, it follows that $`|R_tR_s|1`$. Thus $`occ(\delta \theta ,y)XS_s^{}S_t`$.
        4. Suppose $`\chi (t,S,L)=1`$. Analogous to the previous case.
        5. Otherwise $`occ(\delta \theta ,y)XS_s^{}S_t^{}`$.
2. It is straightforward to show $`\delta \theta (x)U`$ for all $`xF^{}`$.
3. To show $`\chi (\delta \theta (x))1`$ for all $`xL^{}`$. Observe $`\chi (\delta \theta (x))=0`$ if $`xG^{}`$ and $`\chi (\delta \theta (x))=1`$ if $`xF^{}`$. Hence, let $`xLX`$ and suppose $`\chi (\delta \theta (x))=2`$.

1. Suppose $`\chi (s,S,L)=1`$. By lemma 3.3, $`\chi (\theta (s))1`$.

    1. Suppose there exist $`u,vvar(\theta (x))`$, $`uv`$ such that $`var(\delta (u))var(\delta (v))\mathrm{}`$. By lemma 2.3 either:

        1. $`uvar(\theta (s))`$ and $`vvar(\theta (t))`$, hence $`xocc(\theta ,u)XS_s`$, and therefore $`xL^{}`$.
            2. $`uvar(\theta (t))`$ and $`vvar(\theta (s))`$, hence $`xocc(\theta ,v)XS_s`$, and therefore $`xL^{}`$.
            3. $`u,vvar(\theta (s))`$. Hence $`xocc(\theta ,v)XS_s`$, and thus $`xL^{}`$.
        2. Suppose there exists $`uvar(\theta (x))`$ such that $`\chi (\delta (u))=2`$. By lemma 2.4, $`uvar(\theta (s))`$, thus $`xocc(\theta ,u)XS_s`$ and therefore $`xL^{}`$.
    2. Suppose $`\chi (t,S,L)=1`$. Analogous to the previous case.
    3. Otherwise observe that either:

    1. There exist $`u,vvar(\theta (x))`$, $`uv`$ such that $`var(\delta (u))var(\delta (v))\mathrm{}`$. Thus $`uvar(\theta (E^{}))`$ and $`xocc(\theta ,u)XS_sS_t`$. Hence $`xL^{}`$.
        2. There exists $`uvar(\theta (x))`$ such that $`\chi (\delta (u))=2`$. Thus $`uvar(\theta (E^{}))`$ and $`xocc(\theta ,u)XS_sS_t`$. Hence $`xL^{}`$.

###### Example 3.8.

Consider again example 3.1. Observe that $`amgu_1(S,F,L,w,x)=S^{},F^{},L^{}`$ where $`S^{}=\{\mathrm{}\}(S_w^{}S_x)(S_wS_x^{})`$ = $`\{\mathrm{},\{u,w,x\}`$, $`\{u,w,x,y\}`$, $`\{u,w,x,z\}`$, $`\{v,w,x\}`$, $`\{v,w,x,y\}`$, $`\{v,w,x,z\}`$, $`\{w,x\}`$, $`\{w,x,y\}`$, $`\{w,x,z\}\}`$, $`F^{}=\mathrm{}`$ and $`L^{}=\mathrm{}`$. This asserts the independence of $`u`$ and $`v`$ (similarly $`y`$ and $`z`$), as required.

The following example, adapted from \[Langen, 1991\], illustrates that closure can be required to abstract the unification of linear terms.

###### Example 3.9.

Let $`X=\{w,x,y,z\}`$ and observe $`E\gamma _X^{SFL}(S,F,L)`$ where $`E=\{w=f(x,y,z)\}`$, $`S=\{\mathrm{},\{w,x\},\{w,y\},\{w,z\}\}`$, $`F=\mathrm{}`$ and $`L=\{w,x,y,z\}`$. Let $`E^{}=\{w=f(z,x,y)\}`$ and note that $`\theta ^{}imgu(EE^{})`$ where $`\theta ^{}=\{wf(z,z,z),xz,yz\}`$. Thus $`EE^{}\gamma _X^{SFL}(S^{},F^{},L^{})`$ where $`S^{}=\{\mathrm{},\{w,x,y,z\}\}`$, $`F^{}=\mathrm{}`$ and $`L^{}=\{x,y,z\}`$. Indeed, if $`S_s=rel(w,S)=\{\{w,x\},\{w,y\},\{w,z\}\}`$ and $`S_t=rel(f(z,x,y),S)=\{\{w,x\},\{w,y\},\{w,z\}\}`$ then $`(S_s^{}S_t)(S_sS_t^{})`$ = $`\{\{w,x\}`$, $`\{w,y\}`$, $`\{w,z\}`$, $`\{w,x,y\}`$, $`\{w,x,z\}`$, $`\{w,y,z\}`$, $`\{w,x,y,z\}\}`$, thus $`amgu_1(S,F,L`$, $`w,f(z,x,y))`$ yields a safe, though conservative, abstraction. Closure is required to construct the $`\{w,x,y,z\}`$ sharing group.

## 4 Decomposition of set-sharing

Filé \[Filé, 1994\] observes that different sharing and freeness abstractions can represent the same equations, that is, $`\gamma _X^{SF}(S_1,F)=\gamma _X^{SF}(S_2,F)`$ does not imply that $`S_1=S_2`$. Therefore the relationship between $`Sh\times Fr`$ and the concrete domain is a Galois connection rather than an insertion. An insertion is constructed by using $`F`$ to decompose $`S`$ into a set of sharing abstractions $`K_F(S)`$ such that each $`BK_F(S)`$ does not include sharing groups that definitely arise from different computational paths. The following definition and lemma from \[Filé, 1994\] formalises this decomposition, henceforth referred to as the Filé decomposition.

###### Definition 4.1.

The map $`K_F(S):Sh\mathrm{}(Sh)`$ is defined by:

$$K_F(S)=\left\{B\right|\begin{array}{c}BSFvar(B)\\ G_1,G_2B.(G_1G_2G_1G_2F=\mathrm{})\end{array}\}$$

###### Lemma 4.2.

$`\gamma _X^{SF}(S,F)=\{\gamma _X^{SF}(B,F)BK_F(S)\}`$.

Using the above, abstract unification can be refined to $`\{amgu(B,F,L,s,t)|BK_F(S)\}`$. Abstract unification computed in this way does not merge sharing groups arising from different computational paths, and thereby improves precision. Calculating $`K_F(S)`$ is expensive and the number of calls to $`amgu`$ is $`|K_F(S)|`$ (which is potentially exponential in $`|S|`$). However, this tactic suggests lightweight refinements to closure ($``$) and pair-wise union ($``$) that recover some precision at little cost. Since two distinct sharing groups which contain a common free variable must arise from different computational paths, they cannot describe the same equation and therefore need not be combined. Definition 4.3 details the refined abstract unification algorithm and theorem 4.6 builds on lemma 4.4 to establish correctness.

###### Definition 4.3 (Abstract unification 2).

Abstract unification $`amgu_2(S,F,L,s,t)=S^{},F^{},L^{}`$ is defined:

$$S^{\prime \prime }=\{\begin{array}{cccc}\hfill (S_s^_F_FS_t)& \hfill & (S_s_FS_t^_F)\hfill & \mathrm{if}\chi (s,S,L)=\chi (t,S,L)=1\hfill \\ \hfill S_s^_F& _F\hfill & S_t\hfill & \mathrm{if}\chi (s,S,L)=1\hfill \\ \hfill S_s& _F\hfill & S_t^_F\hfill & \mathrm{if}\chi (t,S,L)=1\hfill \\ \hfill S_s^_F& _F\hfill & S_t^_F\hfill & \mathrm{otherwise}\hfill \end{array}$$

$$S_1_FS_2=\{G_1G_2|\begin{array}{c}G_1S_1G_2S_2G_1G_2G_1G_2F=\mathrm{}\end{array}\}$$

$$S^_F=\left\{S^{}\right|\begin{array}{c}SS^{}G_1,G_2S^{}.G_1G_2F=\mathrm{}G_1G_2S^{}\end{array}\}$$

where $`S^{}`$, $`S_s`$, $`S_t`$, $`F^{}`$ and $`L^{}`$ are defined as in definition 3.5.

Notice that the use of freeness is completely absorbed into $`_F`$ and $`_F`$. The following lemma demonstrates that $`_F`$ and $`_F`$ coincide with $``$ and $``$ for each element of the Filé decomposition. The correctness of abstract unification ($`amgu_2`$) follows from this result.

###### Lemma 4.4.

1. If $`BK_F(S)`$ and $`RB`$, then $`R^{}=R^_F`$.
2. If $`BK_F(S)`$ and $`R_1,R_2B`$, then $`R_1R_2=R_1_FR_2`$, $`R_1^{}R_2=R_1^{}_FR_2`$, $`R_1R_2^{}=R_1_FR_2^{}`$ and $`R_1^{}R_2^{}=R_1^{}_FR_2^{}`$.

###### Proof 4.5.

1. Proof by induction.

1. Suppose $`R=\mathrm{}`$. Then $`R^{}=\mathrm{}=R^_F`$.
    2. Suppose $`R=\{G\}R^{}`$. By the hypothesis, $`R_{}^{}{}_{}{}^{}=R_{}^{}{}_{}{}^{_F}`$. Since $`RB`$, then for all $`G^{}R^{}`$, $`G^{}GF=\mathrm{}`$. Hence $`R^{}=R^_F`$.
2. 1. To show $`R_1R_2=R_1_FR_2`$. Let $`G_iR_i`$. If $`G_1G_2F\mathrm{}`$ then $`G_1=G_2`$. Hence $`G_1G_2R_1_FR_2`$.
    2. To show $`R_1^{}R_2=R_1^{}_FR_2`$. Let $`G_1R_1^{}`$ and $`G_2R_2`$. Then $`G_1=Q_1`$ for some $`Q_1R_1`$. Put $`Y=G_1G_2F`$, $`Q_1^{}=\{GQ_1GY=\mathrm{}\}`$ and $`Q_1^{\prime \prime }=Q_1Q_1^{}`$. Observe that $`|Q_1^{\prime \prime }|1`$ and $`Q_1^{\prime \prime }\{G_2\}`$. Thus $`G_1G_2=(Q_1^{})G_2`$. Since $`(Q_1^{})G_2F=\mathrm{}`$ it follows that $`G_1G_2R_1^{}_FR_2`$.
    3. To show $`R_1R_2^{}=R_1_FR_2^{}`$. Analogous to the previous case.
    4. To show $`R_1^{}R_2^{}=R_1^{}_FR_2^{}`$. Let $`G_1R_1^{}`$ and $`G_2R_2^{}`$. Then $`G_i=Q_i`$ for some $`Q_iR_i`$. Put $`Y=G_1G_2F`$, $`Q_i^{}=\{GQ_iGY=\mathrm{}\}`$ and $`Q_i^{\prime \prime }=Q_iQ_i^{}`$. Observe that $`|Q_i^{\prime \prime }|1`$.

    1. Suppose $`|Q_1^{\prime \prime }|=\mathrm{}`$ or $`|Q_2^{\prime \prime }|=\mathrm{}`$. Then $`G_1G_2F=\mathrm{}`$, hence $`G_1G_2R_1^{}_FR_2^{}`$.
        2. Suppose $`|Q_1^{\prime \prime }|=|Q_2^{\prime \prime }|=1`$. Hence $`Q_1^{\prime \prime }=Q_2^{\prime \prime }`$, thus $`G_1G_2=G_1(Q_2^{})`$. Since $`G_1(Q_2^{})F=\mathrm{}`$ it follows that $`G_1G_2R_1^{}_FR_2^{}`$.

###### Theorem 4.6 (Correctness of abstract unification 2).

Let $`E\gamma _X^{SFL}(S,F,L)`$, $`var(s)var(t)X`$ and $`amgu_2(S,F,L,s,t)=S^{},F^{},L^{}`$. Then $`E\{s=t\}\gamma _X^{SFL}(S^{},F^{},L^{})`$.

###### Proof 4.7.

Observe $`E\gamma _X^{SF}(S,F)`$ and $`E\gamma _X^L(L)`$. By lemma 4.2, there exists $`BK_F(S)`$ such that $`E\gamma _X^{SF}(B,F)`$, hence $`E\gamma _X^{SFL}(B,F,L)`$. Observe that if $`sF`$ then $`S_s^_F=S_s`$ (and likewise for $`tF`$) and hence by lemma 4.4, $`amgu_1(B,F,L,s,t)=amgu_2(B,F,L,s,t)`$. By theorem 3.6, $`E\{s=t\}\gamma _X^{SFL}(amgu_1(B,F,L,s,t))`$ = $`\gamma _X^{SFL}(amgu_2(B,F,L,s,t))`$, thus $`E\{s=t\}\gamma _X^{SFL}(amgu_2(S,F,L,s,t))`$.

The proof explains why the standard freeness tactic is a specialised version of the Filé decomposition.

This refinement is only worthwhile if redundant sharing groups are introduced in analysis. Although it can be shown that projection and join do not introduce redundancy, the following example indicates that redundant sharing groups can arise in abstract unification ($`amgu_1`$) and that the refined abstract unification ($`amgu_2`$) can avoid some of these redundant sharing groups.

###### Example 4.8.

Let $`X=\{x,y,z\}`$, $`S=\{\mathrm{},\{x,y\},\{y,z\}\}`$, $`F=\{y\}`$ and $`L=\{y\}`$. Suppose $`s=x`$ and $`t=z`$. Then $`S_s=\{\{x,y\}\}`$ and $`S_t=\{\{x,z\}\}`$ so that $`amgu_1(S,F,L,x,z)=\{\mathrm{},\{x,y,z\}\},\mathrm{},\mathrm{}`$. However $`S_{s}^{}{}_{}{}^{_F}=\{\{x,y\}\}`$ and $`S_{t}^{}{}_{}{}^{_F}=\{\{x,z\}\}`$ and in particular $`S_{s}^{}{}_{}{}^{_F}_FS_{t}^{}{}_{}{}^{_F}=\mathrm{}`$ so that $`amgu_2(S,F,L,x,z)`$ = $`\{\mathrm{}\},\mathrm{},\{x,y,z\}`$.

The following example demonstrates that $`amgu_2`$ is not as precise as the full Filé decomposition.

###### Example 4.9.

Let $`X=\{x,y,z\}`$, $`S=\{\mathrm{},\{x\},\{z\},\{x,y\},\{y,z\}\}`$, $`F=\{x,y,z\}`$ and $`L=\{x,y,z\}`$. Suppose $`s=x`$ and $`t=z`$. Then $`S_s=\{\{x\},\{x,y\}\}`$ and $`S_t=\{\{z\},\{y,z\}\}`$, hence $`S_{s}^{}{}_{}{}^{_F}=S_s`$ and $`S_{t}^{}{}_{}{}^{_F}=S_t`$. Thus $`S_{s}^{}{}_{}{}^{_F}_FS_{t}^{}{}_{}{}^{_F}`$ = $`\{\mathrm{},\{x,z\},\{x,y,z\}\}`$. It follows that $`amgu_2(S,F,L,x,z)`$ = $`\{\mathrm{},\{x,z\},\{x,y,z\}\},F,L`$. However, the Filé decomposition gives $`K_F(S)=\{S_1,S_2,S_3,S_4\}`$ where $`S_1=\{\{x\},\{y,z\}\}`$, $`S_2=\{\mathrm{},\{x\},\{y,z\}\}`$, $`S_3=\{\{x,y\},\{z\}\}`$ and $`S_4=\{\mathrm{},\{x,y\},\{z\}\}`$. Moreover, $`amgu_1(S_2,F,L,x,z)`$ = $`amgu_1(S_4,F,L,x,z)`$ = $`\{\mathrm{},\{x,y,z\}\},F,L`$. Since $`S_1S_2`$ and $`S_3S_4`$, the Filé leads to the sharing abstraction $`\{\mathrm{},\{x,y,z\}\}`$, which is more precise.

## 5 Pruning of set-sharing

Pruning sharing groups is advantageous for efficiency and precision. By reducing the size of an abstraction, abstract unification works on smaller objects and is therefore faster, even if no precision is gained. Of course, the benefit of pruning for efficiency needs to outweigh its cost.

### 5.1 Pruning with freeness via groundness

Surprisingly, combined sharing and freeness information can improve groundness propagation and sharing even for rational tree unification. For example, the equation $`x=f(y,z)`$ can be abstracted by $`(xz)(xy)`$ if $`x`$ and $`y`$ are free variables that share. This is because, in this circumstance, finite tree unification fails for $`x=f(y,z)`$ whereas rational tree unification binds $`x`$ and $`y`$ to $`f(f(\mathrm{},z),z)`$. Abstract unification can use the freeness of variables in the equation to extract hidden groundness information (for distinct computational paths) and thereby prune sharing groups and improve precision. The proof of theorem 5.2 again uses the Filé decomposition.

###### Definition 5.1 (Abstract unification 3).

Abstract unification $`amgu_3(S,F,L,s,t)=S^{},F^{},L^{}`$ is defined:

$$S^{}=(S(S_sS_t))\{\begin{array}{cc}_{GS_s}trim_X(sY,\{G\}_FS_t)& \text{if}sFtU\hfill \\ _{GS_t}trim_X(Zt,S_s_F\{G\})& \text{if}tFsU\hfill \\ S^{\prime \prime }& \text{otherwise}\hfill \end{array}$$

where $`Y=var(t)(GF)`$, $`Z=var(s)(GF)`$, $`S_s`$, $`S_t`$, $`S^{\prime \prime }`$, $`F^{}`$ and $`L^{}`$ are defined as in definition 4.3.

###### Theorem 5.2 (Correctness of abstract unification 3).

Let $`E\gamma _X^{SFL}(S,F,L)`$, $`var(s)var(t)X`$ and $`amgu_3(S,F,L,s,t)=S^{},F^{},L^{}`$. Then $`E\{s=t\}\gamma _X^{SFL}(S^{},F^{},L^{})`$.

###### Proof 5.3.

Suppose $`sF`$. By lemma 4.2, there exists $`BK_F(S)`$ such that $`E\gamma _X^{SFL}(B,F)`$ and by theorem 4.6, $`E\{s=t\}\gamma _X^{Sh}(B^{})`$ where $`B^{}=(B(B_sB_t))(B_s_FB_t)`$, $`B_s=rel(s,B)`$ and $`B_t=rel(t,B)`$. Let $`\theta imgu(E)`$. Since $`sF`$, $`\theta (s)=x`$ for some $`xU`$. Furthermore, $`sG`$ for all $`GS_s`$. Since $`sF`$, $`B_s=\{G\}`$ where $`G=occ(\theta ,x)`$. Observe that $`\theta (y)=x`$ for all $`yGF`$. Since $`tU`$, $`\theta (t)U`$, hence $`\alpha _X^{Pos}(\{\theta (s)=\theta (t)\})sY`$. Moreover, $`mgu(E\{s=t\})=mgu(eqn(\theta )\{s=t\})=mgu(eqn(\theta )\{\theta (s)=\theta (t)\})`$. Thus $`\alpha _X^{Pos}(E\{s=t\})\alpha _X^{Pos}(\{\theta (s)=\theta (t)\})sY`$. The result follows by corollary 2.4. The $`tF`$ case is analogous and the otherwise case follows immediately from theorem 4.6.

The following example illustrates the gain of precision. Note that even the Filé decomposition cannot match this level of precision.

###### Example 5.4.

Let $`X=\{x,y,z\}`$, $`S=\{\mathrm{},\{x,y\},\{y\},\{z\}\}`$, $`F=\{x,y\}`$ and $`L=\{x,y\}`$. Suppose $`s=x`$ and $`t=f(y,z)`$. Consider the Filé decomposition, that is, $`K_F(S)=\{S_1,S_2,S_3,S_4\}`$ where $`S_1=\{\{x,y\}\}`$, $`S_2=\{\mathrm{},\{x,y\}\}`$, $`S_3=\{\{x,y\},\{z\}\}`$, $`S_4=\{\mathrm{},\{x,y\},\{z\}\}`$. Then $`amgu_1(S_4,F,L,x,f(y,z))`$ = $`S^{},\mathrm{},\mathrm{}`$ where $`S^{}=\{\mathrm{}`$, $`\{x,y\}`$, $`\{x,y,z\}\}`$. Since $`S_iS_4`$ for all $`i\{1,2,3\}`$, the decomposition results in the sharing abstraction $`S^{}`$. Moreover, $`amgu_2(S,F,L,x,f(y,z))`$ = $`S^{},\mathrm{},\mathrm{}`$. However, $`amgu_3(S,F,L,x,f(y,z))`$ = $`trim_X(xz,S^{}),\mathrm{},\mathrm{}`$ = $`\{\mathrm{},\{x,y,z\}\},\mathrm{},\mathrm{}`$ which is more precise.

###### Example 5.5.

Let $`X=\{x,y,z\}`$, $`S=\{\mathrm{},\{x,y\},\{y,z\}\}`$, $`F=\{y\}`$ and $`L=\{y\}`$. Suppose $`s=x`$ and $`t=z`$. Since $`x,zU`$, $`amgu_3(S,F,L,x,z)`$ = $`amgu_2(S,F,L,x,z)`$ = $`\{\mathrm{},\{x,y,z\}\},\mathrm{},\mathrm{}`$ whereas the Filé decomposition produces $`\{\mathrm{}\},\mathrm{},\{x,y,z\}`$ (see example 4.8).

Example 5.5 shows that $`amgu_3`$ is not uniformly more precise than the Filé decomposition, hence is sub-optimal. Nevertheless, this pruning tactic suggests that any optimal abstract unification algorithm for sharing, freeness and linearity, in the presence of groundness, will have to consider subtle interactions between the components.

### 5.2 Early pruning with groundness

Sharing abstractions can always be pruned by removing sharing groups which contain ground variables. Common practice is to schedule the solving of equations so as to first apply abstract unification to equations on ground terms \[Langen, 1991\]. Moreover, \[Muthukumar & Hermenegildo, 1992\] details a queueing/dequeueing mechanism for maximally propagating groundness among systems of equations. This can involve repeated searching. This section proposes a revision of this tactic that applies groundness to the complete set of equations (without repeated searching) and then uses the resulting groundness information to prune sharing before abstract unification is applied. The gain is that searching and scheduling are no longer required (the mechanism is single pass) and that the disjunctive groundness information captured by $`Pos`$ can be exploited so that abstract unification can potentially operate on smaller abstractions. Observe that groundness information will normally be tracked by $`Pos`$ anyway, thus the computational overhead is negligible. To formulate this strategy, abstract unification is lifted to sets of equations as follows:

###### Definition 5.6.

The map $`amgu_i(T,E)=\{T^{}T,E^{}T^{},\mathrm{}\}`$ is defined by the least relation $`(Share_X\times Fr_X\times Lin_X)^2`$ such that $`T,\{s=t\}Eamgu_i(T,s,t),E`$.

The following theorem states correctness of the early pruning using groundness for $`amgu_1`$, $`amgu_2`$ and $`amgu_3`$.

###### Theorem 5.7.

Let $`E\gamma _X^{Pos}(f)\gamma _X^{SFL}(S,F,L)`$, $`EE^{}\gamma _X^{Pos}(f^{})`$, $`Y=\{yXf^{}y\}`$, $`S^{}=trim_X(fY,S)`$, $`F^{}=Fvar(rel(Y,S))`$, $`L^{}=LY`$, $`var(E)X`$ and $`T^{}amgu_i(S^{},F^{},L^{},E^{})`$. Then $`EE^{}\gamma _X^{SFL}(T^{})`$.

###### Proof 5.8.

Let $`\theta imgu(E)`$ and $`\theta ^{}imgu(EE^{})`$. Since $`\theta ^{}unify(E)`$, $`\theta \theta ^{}`$ and there exists $`\zeta Sub`$ such that $`\zeta \theta =\theta ^{}`$. Since $`\theta ^{}unify(E^{})`$, $`\zeta unify(\theta (E^{}))`$ so that $`mgu(\theta (E^{}))\mathrm{}`$. Let $`\delta imgu(\theta (E^{}))=imgu(\theta ^{\mathrm{}}(E^{}))`$. By part 2 of lemma 2.2, $`\delta \theta =\delta \theta ^{\mathrm{}}mgu(eqn(\theta )E^{})=mgu(EE^{})`$. Thus there exists $`\rho Rename`$ such that $`\rho \delta \theta =\theta ^{}`$. Now $`var(\theta ^{}(y))=\mathrm{}`$ for all $`yY`$, hence $`var(\delta \theta (y))=\mathrm{}`$ for all $`yY`$. Put $`Z=\{var(\theta (y))yY\}`$, $`\varphi =\overline{}Z.\delta `$ and $`\psi =Z.\delta `$. Let $`zZ`$. Then there exists $`yY`$ such that $`zvar(\theta (y))`$. But $`var(\delta \theta (y))=\mathrm{}`$, hence $`rgn(\varphi )=\mathrm{}`$ and $`\delta =\psi \varphi `$. Thus $`\psi \varphi mgu(\theta (E^{}))`$ and by lemma 2.2 part 3, $`(dom(\varphi )rng(\varphi )).\psi mgu(\varphi \theta (E^{}))`$. Furthermore, $`(dom(\varphi )rng(\varphi )).\psi =\psi `$ hence $`\psi mgu(\varphi \theta (E^{}))`$. Since $`\varphi \theta `$ is idempotent, $`\psi mgu((\varphi \theta )^{\mathrm{}}(E^{}))`$. By lemma 2.2, part 2, $`\psi \varphi \theta =\psi (\varphi \theta )^{\mathrm{}}mgu(eqn(\varphi \theta )E^{})`$. Thus $`\theta ^{}imgu(eqn(\varphi \theta )E^{})`$.

To show $`eqn(\varphi \theta )\gamma _X^{Sh}(trim(fY,S))`$. Let $`uU`$. If $`occ(\varphi \theta ,u)=\mathrm{}`$ then $`occ(\varphi \theta ,u)XS`$ trivially. If $`occ(\varphi \theta ,u)\mathrm{}`$ then $`occ(\varphi \theta ,u)=occ(\theta ,u)`$ since $`rng(\varphi )=\mathrm{}`$. Thus $`occ(\varphi \theta ,u)XS`$. Therefore $`eqn(\varphi \theta )\gamma _X^{Sh}(S)`$. By lemma 2.2, part 2, $`\delta \theta mgu(Eeqn(\theta ))`$. But $`\theta ^{}mgu(Eeqn(\theta ))`$ and therefore there exists $`\rho Rename`$ such that $`\rho \delta \theta =\theta ^{}`$. Thus $`\alpha ^{Pos}(\delta \theta )\alpha ^{Pos}(\rho \delta \theta )=\alpha ^{Pos}(\theta ^{})Y`$. Observe that if $`\alpha ^{Pos}(\delta \theta )u`$ then $`\alpha ^{Pos}(\varphi \theta )u`$ hence $`\alpha ^{Pos}(\varphi \theta )Y`$. Since $`\alpha ^{Pos}(\varphi \theta )\alpha ^{Pos}(\theta )f`$, it follows that $`\alpha ^{Pos}(\varphi \theta )fY`$. Therefore $`eqn(\varphi \theta )\gamma _X^{Pos}(fY)`$. By corollary 2.4, $`eqn(\varphi \theta )\gamma _X^{Sh}(trim(fY,S))`$.

To show $`\varphi \theta (x)U`$ for all $`xF^{}`$. Let $`xF`$ and $`xvar(rel(Y,S))`$. Since $`xvar(rel(Y,S))`$, $`xocc(\theta ,u)X`$ or $`yocc(\theta ,u)X`$ for all $`uU`$ and $`yY`$. Since $`xX`$ and $`YX`$, $`var(\theta (x))var(\theta (y))=\mathrm{}`$ for all $`yY`$. Hence $`\theta (x)Z`$, thus $`\theta (x)dom(\varphi )`$, therefore $`\varphi \theta (x)U`$. Thus $`eqn(\varphi \theta )\gamma _X^{Fr}(F^{})`$.

To show $`\chi (\varphi \theta (x))1`$ for all $`xL^{}`$. Since $`rng(\varphi )=\mathrm{}`$, $`\chi (\varphi \theta (x))1`$ for all $`xL`$. Moreover, $`\alpha ^{Pos}(\varphi \theta )Y`$ and therefore $`\chi (\varphi \theta (x))1`$ for all $`xY`$. Thus $`eqn(\varphi \theta )\gamma _X^{Lin}(L^{})`$. The result then follows by induction on $`E`$ and theorems 3.6, 4.6 and 5.2.

The following example illustrates the computational advantages of early pruning.

###### Example 5.9.

Let $`X=\{u,v,x,y\}`$, $`S=\{\mathrm{},\{x\},\{y\},\{u\},\{v\}\}`$, $`F=\mathrm{}`$, $`L=\mathrm{}`$ and $`f=xy`$. Let $`E^{}=\{x=f(u,v),x=y\}`$ so that $`f^{}=(xy)(x(uv))(xy)`$ = $`xyuv`$. Then $`Y=\{x,y,u,v\}`$ so that $`fY=xyuv`$ and $`S^{}=trim_X(fY,S)`$ = $`\{\mathrm{}\}`$. Hence $`amgu_3(S,F,L,E^{})`$ reduces to $`amgu_3(S^{},F,L,E^{})`$ = $`\{\mathrm{}\},\mathrm{},\mathrm{}`$. Without this tactic, no equation of $`E^{}`$ will possess a ground argument and both calls to $`amgu_3`$ will involve non-trivial sharing group manipulation.

## 6 Conclusion

This paper has given correctness proofs for sharing analysis with freeness and linearity which hold in the presence of rational trees. The abstract unification algorithms are themselves novel – incorporating optimisations for both precision and efficiency. Specifically, the independence check which can prevent linearity from being exploited has been removed. In addition, refined closure and pair-wise union operations have been derived from the Filé decomposition. A further precision optimisation has been presented which exploits an interaction between sharing, freeness and groundness, which shows the subtlety that an optimal algorithm will need to address. These optimisations have been chosen to balance precision against efficiency whilst not changing the underlying representation of the abstract domains. They are ordered according to their anticipated degree of usefulness. This work provides the implementor with a suite of new optimisations for abstract unification algorithms for sharing, freeness and linearity.

#### Acknowledgements

We thank Gilberto Filé for kindly sending us a copy of his technical report. This work was supported, in part, by EPSRC grant GR/MO8769.


text:
# On a group associated to 𝑧²-1

## 1. Introduction

The purpose of this paper is to introduce, in a very concrete context, the construction of the *iterated monodromy group* of a branched covering of a Riemann surface. Our main focus will be on the covering of the Riemann sphere given by the map $`zz^21`$, whose group $`G`$ possesses many interesting algebraic and analytic properties. Our main guideline is that these properties derive from dynamic properties of the covering.

We will show:

###### Theorem 1.1.

Let $`G`$ be the iterated monodromy group (see Definition 2.2) of $`z^21`$. Then $`G`$ acts on the binary rooted tree, and is generated by

$$a=b,1(1,2),b=a,1.$$

where $`\sigma `$ permutes the top two branches of $`G`$, and $`x,y`$ describes the automorphism acting respectively as $`x`$ and $`y`$ on the left and right subtrees.

1. $`G`$ is weakly branch (Proposition 3.1);
2. $`G`$ is a torsion-free group (Proposition 3.4);
3. $`G`$ contains a free monoid of rank $`2`$, and hence has exponential growth (Proposition 3.5);
4. $`G`$ does not contain any non-abelian free group (Proposition 3.7);
5. $`G`$ is not solvable, but every proper quotient of $`G`$ is (free abelian)-by-(finite $`2`$-group) (Proposition 3.10);
6. $`G`$ has a presentation (Proposition 3.6)

$$G=a,b|[[a^p,b^p],b^p],[[b^p,a^{2p}],a^{2p}]\text{ for all }p\text{ a power of }2.$$

The Schur multiplier $`H_2(G,)`$ is free abelian of infinite rank.
7. $`G`$ has solvable word problem (Proposition 3.8);
8. $`G`$’s spectrum is a Cantor set, and is the intersection of a line and the Julia set of a degree-$`2`$ polynomial mapping in $`^3`$ (Proposition 4.1)

$$F(\lambda ,\mu ,\nu )=(\lambda ^2+2\lambda \nu 2\mu ^2,\lambda \nu +2\nu ^2,\mu ^2).$$
9. $`G`$’s limit space is the Julia set $`𝔍`$ of $`z^21`$ , and the Schreier graphs $`G/P_n`$ converge to $`𝔍`$ (Proposition 4.2).

The group $`G`$ has many properties in common with the group $`H`$ introduced by Brunner, Sidki and Vieira \[BSV99\]; the main difference is the existence of free monoids in $`G`$, which do not seem to exist in $`H`$. We also believe that most proofs for $`G`$ are simpler than the analogous statements for $`H`$; in particular, the spectrum on $`H`$ has not been computed.

## 2. Covering Maps and Groups

This section describes the general construction of a group from a rational map of the Riemann sphere $`\widehat{}`$.

Let $`f(z)`$ be a branched self-covering of $`\widehat{}`$. A point $`z\widehat{}`$ is *critical* if $`f^{}(z)=0`$, and is a *ramification point* if it is the $`f`$-image of a critical point. The *postcritical set* of $`f`$ is $`\{f^n(z):n1,z\text{ critical}\}`$.

Assume $`P`$ is finite, and write $`𝕄=\widehat{}P`$. Then $`f`$ induces by restriction a self-covering of $`𝕄`$.

Let $``$ be a generic point in $`𝕄`$, i.e. be such that the iterated inverse $`f`$-images of $``$ are all distinct. If $`f`$ has degree $`d`$, then for all $`n`$ there are $`d^n`$ points in $`f^n()`$, and these form naturally the $`n`$th *layer* $`T_n`$ of a $`d`$-regular rooted tree $`T=_{n0}T_n`$. The root of $`T`$ is $``$, and there is an edge between $`z`$ and $`f(z)`$ for all $`zT\{\}`$. In particular, write $`T_1=f^1()`$ the first layer of $`T`$.

Let $`\gamma `$ be a loop at $``$ in $`𝕄`$. Then for all $`vT_n`$ there is a unique lift $`\gamma _v`$ of $`\gamma `$ starting at $`v`$ such that $`f^n(\gamma _v)=\gamma `$; and furthermore the endpoint $`v^\gamma `$ of $`\gamma _v`$ also belongs to $`T_n`$.

###### Proposition 2.1.

For any such $`\gamma `$ the map $`vv^\gamma `$ is tree automorphism of $`T`$, and depends only on the homotopy class of $`\gamma `$ in $`\pi _1(𝕄,)`$.

###### Definition 2.2.

The *iterated monodromy group* $`G_T(f)`$ of $`f`$ is the subgroup of $`\mathrm{𝖠𝗎𝗍}(T)`$ generated by all maps $`vv^\gamma `$, as $`\gamma `$ ranges over $`\pi _1(𝕄,)`$.

This definition is actually independent of the choice of $``$:

###### Proposition 2.3.

Let $`^{}`$ be another generic basepoint, with tree $`T^{}`$, and choose a path $`p`$ from $``$ to $`^{}`$. Then there is an isomorphism $`\varphi :TT^{}`$ such that

commutes.

We write $`G(f)`$ for $`G_T(f)`$, defined up to conjugation in $`T`$. Abstractly, $`G(f)`$ is a quotient of $`\pi _1(𝕄,)`$, a free group of rank $`|P|1`$.

### 2.1. Recurrence

Choose now for each $`vT_1`$ a path $`\mathrm{}_v`$ from $``$ to $`v`$ in $`𝕄`$. Consider a loop $`\gamma `$ at $``$; then it induces a permutation of $`T_1`$ given by $`vv^\gamma `$, and for each $`vT_1`$ its lift $`\gamma _v`$ at $`v`$ yields a loop $`\mathrm{}_v\gamma _v\mathrm{}_{v^\gamma }^1`$ at $``$, again written $`\gamma _v`$.

###### Proposition 2.4.

$`\gamma _v`$ depends only on the class of $`\gamma `$ in $`G(f)`$.

We therefore have a natural wreath product embedding

$$\varphi :G(f)G(f)𝔖_{T_1}$$

mapping $`\gamma `$ to $`(v\gamma _v,vv^\gamma )`$. Enumerating $`T_1=\{v_1,v_2,\mathrm{},v_d\}`$, we write

$$\varphi (g)=g_{v_1},\mathrm{},g_{v_d}\pi _g,$$

where $`\pi _g`$ is the permutation of $`T_1`$ corresponding to $`g`$, in disjoint cycle notation.

Since $`G(f)`$ is finitely generated (by at most $`|P|1`$ elements), it can be completely described by a permutation of $`d`$ points and a sequence of $`d`$ elements of $`G(f)`$, written as products of generators. We will call this description a *wreath presentation*.

### 2.2. Main example

We study now the main example $`f(z)=z^21`$, and derive an explicit action of $`G=G(f)`$ on a “standard” binary rooted tree $`\{x,y\}^{}`$.

The postcritical set $`P`$ is $`\{0,1,\mathrm{}\}`$, so $`𝕄`$ is a thrice-punctured sphere and $`G`$ is $`2`$-generated.

For convenience, pick as base point $``$ a point close to $`(1\sqrt{5})/2`$; then $`T_1=\{x,y\}`$ with $`x`$ close to $``$ and $`y`$ close to $``$.

Consider the following representatives of $`\pi _1(𝕄,)`$’s generators: $`a`$ is a straight path approaching $`1`$, turning a small loop in the positive orientation around $`1`$, and returning to $``$. similarly, $`b`$ is a straight path approaching $`0`$, turning around $`0`$ in the positive orientation, and returning to $``$.

Let $`\mathrm{}_x`$ be a short arc from $``$ to $`x`$, and let $`\mathrm{}_y`$ be a half-circle above the origin from $``$ to $`y`$.

Let us compute first $`f^1(a)`$, i.e. the path traced by $`\pm \sqrt{z+1}`$ as $`z`$ moves along $`a`$. Its lift at $`x`$ moves towards $`0`$, passes below it, and continues towards $`y`$. Its lift at $`y`$ moves towards $`0`$, passes above it, and continues towards $`x`$. We have $`a_x=b`$ and $`a_y=1`$, so the wreath presentation of $`a`$ is $`\varphi (a)=b,1(x,y)`$.

Consider next $`f^1(b)`$. Its lift at $`x`$ moves towards $`1`$, loops around $`1`$, and returns to $`x`$. Its lift at $`y`$ moves towards $`1`$, loops and returns to $`y`$. We have $`b_x=a`$ and $`b_y=1`$, so the wreath presentation of $`b`$ is $`\varphi (b)=a,1`$.

## 3. Algebraic Properties

We will exploit as much as possible the wreath presentation of $`G=G(z^21)`$ to obtain algebraic information on $`G`$. Recall that $`G`$ is given with an action on the tree $`T=\{x,y\}^{}`$. We write $`xT,yT`$ the subtrees below $`x,y`$ respectively.

Most of our proofs are close adaptations of \[BSV99\].

###### Proposition 3.1.

$`G`$ is weakly branch, i.e. in $`G`$’s action on $`T`$

1. $`G`$ acts transitively on each layer $`T_n`$;
2. at every vertex $`v`$, there is a non-trivial $`gG`$ acting only on the subtree below $`g`$, and fixing its complement.

###### Proof.

$`G`$ acts transitively on $`T_1`$, since $`a`$ permutes its two elements. Now $`\mathrm{𝖲𝗍𝖺𝖻}(x)=a^2,b,b^a`$ maps onto $`G`$ by restriction of the action to $`xT`$; hence by induction acts transitively on each of its layers. Combining with the transitive action on $`T_1`$, we get a transitive action on all layers of $`T`$.

Consider next $`G^{}`$. From $`[a,b]=a^1b,b^1a`$ we get $`G^{}1`$. From the relation $`[b,a^2]=[a,b],1`$, we see that $`G^{}`$ contains $`G^{}\times 1`$ as a subgroup acting only on $`xT`$. This can be iterated, so $`G`$ contains a copy of $`G^{}`$ acting only below the vertex $`v`$. ∎

Consider again the embedding $`\varphi :GG𝔖_{x,y}`$; define a norm on the generators of $`G`$ by $`a=a^1=1`$ and $`b=b^1=\sqrt{2}`$, and extend it by the triangle inequality:

$$g=\mathrm{min}\{s_1+\mathrm{}+s_n:g=s_1\mathrm{}s_n,s_i\{a^{\pm 1},b^{\pm 1}\}\}.$$

###### Lemma 3.2.

If $`\varphi (g)=g_x,g_y\pi `$, then $`g_i\frac{g+1}{\sqrt{2}}`$ for all $`i\{x,y\}`$.

###### Proof.

Write in a minimal form $`g`$ as a product of $`N`$ letters $`a`$ (with signs) and $`M`$ letters $`b`$ (with signs). Then $`g_i`$ contains at most $`(N+1)/2`$ letters $`b`$ and $`M`$ letters $`a`$. ∎

From now on write $`c=[a,b]`$.

###### Proposition 3.3.

$`G^{}=c,c^a,c^{a^2}`$; we have $`G/G^{}=^2`$ generated by $`a,b`$ and $`G^{}/(G^{}\times G^{})=`$ generated by $`c`$.

###### Proof.

The first claim follows from computations: $`c^b=c`$, and $`c^{a^3}=(c^{a^2})^1cc^a`$.

Next, we have $`G^{}=(G^{}\times G^{})c`$; indeed $`c^a=[b,a],1c^1`$, and $`c^{a^2}=[b,a^1],[b,a]^bc`$.

Now assume for contradiction that $`a^mb^nG^{}`$ with $`|m|+|n|`$ minimal. Then clearly $`m`$ is even, say $`m=2p`$. We have, for some $`k`$ with $`|k||m|+|n|`$,

$$a^mb^n=b^pa^n,b^p=g,hc^k=ga^k,ha^{bk}$$

and therefore $`a^{nk}b^p`$ and $`a^kb^p`$ both belong to $`G^{}`$. This contradicts our assumption on minimality, so we have proven the second claim.

Assume finally that $`c^kG^{}\times G^{}`$ with $`|k|`$ minimal. Then $`a^kG^{}`$ which contradicts the second claim. ∎

###### Proposition 3.4.

$`G`$ is a torsion-free group.

###### Proof.

Since $`G`$ acts on the binary tree, it is residually a $`2`$-group, and its only torsion must be $`2`$-torsion. Assume for contraction that $`G`$ contains an element $`g`$ of order $`2`$, of minimal norm.

By Proposition 3.3 $`a`$ and $`b`$ are of infinite order. We may therefore assume $`g2`$. If $`g`$ fixes $`x`$, then its restrictions $`g_x`$ and $`g_y`$ are shorter by Lemma 3.2, and one of them has order $`2`$, contradicting $`g`$’s minimality.

If $`g`$ does not fix $`x`$, then we may write $`g=g_x,g_ya`$ for some $`g_x,g_yG`$. We then have $`h=g^2=g_xbg_y,g_yg_xb=1`$ and therefore $`g_yg_xb=1`$. Now for any element $`h`$ fixing $`x`$ we have $`h_xh_ya,b^2,G^{}`$; this last subgroup does not contain $`b`$ by Proposition 3.3, so we have a contradiction. ∎

###### Proposition 3.5.

The subsemigroup $`\{a,b\}^{}`$ of $`G`$ is free; therefore $`G`$ has exponential growth.

###### Proof.

Consider two words $`u,v`$ in $`\{a,b\}^{}`$ that are equal in $`G`$, and assume $`|u|+|v|`$ is minimal. We have $`u_x=v_x`$ and $`u_y=v_y`$ in $`G`$, which are shorter relations, so we may assume these words are equal by induction.

Now if $`u_x`$ and $`v_x`$ start with the same letter, this implies that $`u`$ and $`v`$ also start with the same letter, and cancelling these letters would give a shorter pair of words $`u,v`$ equal in $`G`$. ∎

###### Proposition 3.6.

$`G`$ has finite $`L`$-presentation

$$G=a,b|[[a^p,b^p],b^p],[[b^p,a^{2p}],a^{2p}]\text{ for all }p\text{ a power of }2.$$

The Schur multiplier $`H_2(G,)`$ is free abelian of infinite rank.

###### Proof.

This follows from the standard method in \[Bar02b\], since $`G`$ is contracting and $`G^{}`$ is finitely generated.

We first obtain all relations $`[[a^i,b],b]`$ for odd $`i`$, and their iterates under the substitution $`\sigma :ab,ba^2`$ induced by the inclusion of $`G^{}\times 1`$ in $`G^{}`$.

Then we note that $`[[a^i,b],b]`$ is a consequence of $`[[a,b],b]`$ and $`[[b,a^2],a^2]`$.

The Schur multiplier computation follows from Hopf’s formula $`H_2(G,)=(R[F,F])/[R,F]`$ for a group $`G=F/R`$ presented as quotient of a free group. The homomorphism $`\sigma `$ induces the standard shift on $`^{\mathrm{}}`$. ∎

The method of the following proof is inspired by the PhD thesis of Edmeia Da Silva \[Sil01\].

###### Proposition 3.7.

$`G`$ does not contain any non-abelian free subgroup.

###### Proof.

Take $`g,hG`$; we seek a relation $`w(g,h)`$ between them. Consider the standard metric $`|g|`$ on words, given by assigning length $`1`$ to each generator $`a^{\pm 1},b^{\pm 1}`$. Given any $`gG`$, we have $`|g_x||g|`$ and $`|g_y||g|`$; these inequalities are strict, unless $`gB=\{a^ib^na^j\text{ with }n,i,j\{0,1\}\}`$. We also have $`|g_xg_y||g|`$.

We define the following ordering on pairs $`(g,h)`$ of group elements: Write $`H=\mathrm{𝖲𝗍𝖺𝖻}_G(x)`$ the stabilizer of $`x`$. The height of $`(g,h)`$ is $`L(g,h)=|g|+|h|\frac{1}{3}\mathrm{\#}\{g,h\}H`$; that is, we order first by total length, and then by number of elements in $`\{g,h\}`$ fixing $`x`$.

The basis of the induction is that for $`(g,h)`$ of height at most $`2`$ these elements must be generators, and we have the relation, say, $`[[a,b],b]`$ among them.

If $`g,hH`$, they may be written as $`g=g_x,g_y`$ and $`h=h_x,h_y`$. Then either one of $`g_x,h_x`$ is not in $`B`$, so by induction there is a relation $`u(g_x,h_x)`$; or we consider the cases $`g_x=b^i,h_x=b^j`$ and $`g_x=a^1b^ia,h_x=a^1b^ja`$ which have a common power; and up to symmetry $`g_x=a^1b^ia,h_x=b^j`$ when we have the relation $`[g_x,h_x]`$. By the same argument, there is a relation $`v(g_y,h_y)`$. Consider now relation $`w=[u,v]`$; we have $`w(g,h)=[1,u(g_y,h_g),v(g_x,h_x),1]=1`$.

If at least one, say $`g`$, fixes $`x`$, we may write $`h=h_x,h_y(x,y)`$, and may proceed as above with $`g`$ and $`h^2`$, since $`L(g_x,h_xh_y)<L(g,h)`$ and $`L(g_y,h_xh_y)<L(g,h)`$.

If none of $`g,h`$ fixes $`x`$, we write $`g=g_x,g_y(x,y)`$ and $`h=h_x,h_y(x,y)`$, and consider the elements in the following table:

$$\begin{array}{cccccc}& & \multicolumn{2}{c}{g_xH}& \multicolumn{2}{c}{g_xH}\\ & & g_yH& g_yH& g_yH& g_yH\\ & & & & & \\ & h_yH& g^2,h^2& g^2,h^2& g^2,h^2& g^2,h^2\\ h_xH& h_yH& g^2,h^2& gh^1,hg^1& gh,hg& g^2,h^2\\ & & & & & \\ & h_yH& g^2,h^2& gh,hg& gh^1,hg^1& g^2,h^2\\ h_xH& h_yH& g^2,h^2& g^2,h^2& g^2,h^2& g^2,h^2\end{array}$$

By inspection, in the pair of elements $`e,f`$ corresponding to $`g,h`$ at both fix $`x`$, and their respective projections satisfy $`L(e_x,f_x)<L(g,h)`$ and $`L(e_y,f_y)<L(g,h)`$; therefore they satisfy relations $`u,v`$, and $`e,f`$ satisfy the relation $`[u,v]`$. ∎

###### Proposition 3.8.

The word problem is solvable in $`G`$.

###### Proof.

The solution to the word problem follows from Lemma 3.2; indeed take a word $`w`$ of length $`n`$. If it does not fix $`x`$, then it is not trivial. Otherwise its projections $`w_x,w_y`$ are shorter words, so can inductively be checked for triviality in $`G`$. Then $`w`$ is trivial in $`G`$ if and only if $`w_x`$ and $`w_y`$ are both trivial in $`G`$. ∎

Write now $`d=[c,a]`$ and $`e=[d,a]`$.

###### Proposition 3.9.

We have $`G^{\prime \prime }=(\gamma _3\times \gamma _3)`$, and $`\gamma _3=(\gamma _3\times \gamma _3)d,erangle`$.

In the lower central series of $`G`$ we have $`\gamma _1/\gamma _2=^2`$, $`\gamma _2/\gamma _3=`$, and $`\gamma _3/\gamma _4=/4`$. Therefore all quotients except the first two in the lower central series are finite.

In the lower $`2`$-central series defined by $`G_1=G`$ and $`G_{n+1}=[G,G_n]G_{n/2}^2`$, we have

$$dim_{𝔽_2}\mathrm{\Gamma }_n/\mathrm{\Gamma }_{n+1}=\{\begin{array}{cc}i+2\hfill & \text{ if }n=2^i\text{ for some }i;\hfill \\ \mathrm{max}\{i+1|\mathrm{\hspace{0.17em}2}^i\text{ divides }n\}\hfill & \text{ otherwise}.\hfill \end{array}$$

###### Proof.

We moreover claim we have the following generating sets:

$`\gamma _1`$ $`=a,b;`$
$`\gamma _2`$ $`=c=[a,b]=(a,a^b),c^{1a}=(c,1),c^{a^11}=(1,c);`$
$`\gamma _3`$ $`=d=[c,a],e=[d,a],[e^1,b]=(d,1),(e,1),(1,d),(1,e);`$
$`\gamma _4`$ $`=d^4,e,(d,1),(e,1),(1,d),(1,e).`$
Most follow from simple computations; let us justify $`d^4\gamma _4`$. Since it is clear that $`\gamma _4`$ contains $`e`$, we denote by $``$ congruence modulo $`e`$, which is weaker than congruence modulo $`\gamma _4`$. We have

$`d^2`$ $`d^2e=b^1a^1ba^2b^1aba^2`$
$`=b^1aba^2b^1a^1ba^2\text{ modulo }[a^{2b},a^2]=1`$
$`=(d^2e)^{a^b}d^2.`$
We have already computed $`G/G^{}=^2`$ in Proposition 3.3, and $`G^{}/\gamma _3=`$ is generated by $`c`$. This last computation gives $`\gamma _3/\gamma _4=/4`$.

Next, $`G^{\prime \prime }`$ is generated as a normal subgroup by $`[c,(c,1)]=(d,1)`$, so $`G^{\prime \prime }=\gamma _3\times \gamma _3`$.

For the $`2`$-central series see \[Bar02a\], where the argument is developed for the BSV group. ∎

###### Proposition 3.10.

$`G`$ is not solvable, but all its quotients are (free abelian)-by-(finite $`2`$-group).

###### Proof.

By Proposition 3.9, we have $`G^{\prime \prime }>\gamma _3\times \gamma _3`$, so $`G^{\prime \prime \prime }>G^{\prime \prime }\times G^{\prime \prime }`$, and hence $`G^{(n)}>G^{(n1)}\times G^{(n1)}`$ for all $`n`$. Assume for contradiction that $`G`$ is solvable; this means $`G^{(n)}=1`$ for some minimal $`n`$, a contradiction with the above statement.

Now consider a non-trivial normal subgroup $`N`$ of $`G`$. By \[Gri00, Theorem 4\], we have $`(\gamma _3)^{\times 2^n}<N`$ for some $`n`$. On the other hand, $`G`$ is an abelian-by-(finite $`2`$) extension of $`(\gamma _2)^{\times 2^n}`$. The result follows. ∎

## 4. Geometric and Analytic Properties

In this part we isolate results on the geometry of the action of $`G`$ on the boundary of the tree. The inspiration for this part is the paper \[BG00\] where computations of spectra were performed, and \[BGN02\] where the relation between the Schreier graphs of an i.m.g. group and the Julia set of its polynomial were explicited.

Consider first the spectrum computation. Given a group $`G`$ with generating set $`S`$ and a unitary representation $`\pi `$ on a Hilbert space $``$, its *spectrum* is

$$\mathrm{spec}(\pi )=\frac{1}{|S|}\mathrm{spec}_{B()}\left(\underset{sS}{}\pi (s)\right).$$

It is a closed subset of $``$; if $`S`$ is symmetric, then the spectrum is always contained in $``$.

The main representation of interest is the left-regular representation $`\rho `$ on $`\mathrm{}^2(G)`$. A result of Kesten \[Kes59\] shows that $`1`$ is in $`\mathrm{spec}(\rho )`$ if and only if $`G`$ is amenable.

Here we concentrate on the “natural” representation $`\pi `$ of $`G`$ on $`L^2(T`$, where $`T`$ is the boundary of the tree $`T`$. We denote by $`\pi _n`$ the representation of $`G`$ on the $`n`$th layer $`T_n`$.

Introduce for $`n0`$ the following homogeneous polynomials:

$$Q_n(\lambda ,\mu ,\nu )=det\left(\lambda +\mu (\pi _na+\pi _na^1)+\nu (\pi _nb+\pi _nb^1)\right).$$

Then the spectrum of $`\pi _n`$ is obtained by solving $`Q_n(\lambda ,\frac{1}{4},\frac{1}{4})=0`$.

We are not able to derive a closed form for $`Q_n`$; however we have the

###### Proposition 4.1.

Define the polynomial mapping $`F:^3^3`$ by

$$(\lambda ,\mu ,\nu )(\lambda ^2+2\lambda \nu 2\mu ^2,\lambda \nu +2\nu ^2),\mu ^2).$$

Then $`Q_n`$ is given by

$$Q_0(\lambda ,\mu ,\nu )=\lambda +2\mu +2\nu ;$$

$$Q_1(\lambda ,\mu ,\nu )=Q_0(\lambda ,\mu ,\nu )(\lambda 2\mu +2\nu );$$

and for $`n1`$,
$$Q_{n+1}(\lambda ,\mu ,\nu )=Q_n(F(\lambda ,\mu ,\nu )).$$

Define $`K`$ as the closure of the set of all backwards $`F`$-iterates of $`\{Q_1=0\}`$. Then the spectrum of $`\pi `$ is the intersection of $`\{\mu =\nu =\frac{1}{4}\}`$ with $`K`$.

###### Proof.

The first two follow from direct computation, using $`\pi _0(a)=\pi _0(b)=(1)`$, and

$$\pi _{n+1}(a)=\left(\begin{array}{cc}0& \pi _n(b)\\ 1& 0\end{array}\right),\pi _{n+1}(b)=\left(\begin{array}{cc}\pi _n(a)& 0\\ 0& 1\end{array}\right).$$

Next, we compute, writing $`a,b`$ for $`\pi _n(a),\pi _n(b)`$ respectively,

$`Q_{n+1}(\lambda ,\mu ,\nu )`$ $`=det\left(\begin{array}{cc}\lambda +\nu (a+a^1)& \mu (1+b)\\ \mu (b^1+1)& \lambda +2\nu \end{array}\right)`$
$`=det\left((\lambda +\nu (a+a^1))(\lambda +2\nu )\mu ^2(1+b)(b^1+1)\right)`$
$`=Q_n(\lambda ^2+2\lambda \nu 2\mu ^2,\lambda \nu +2\nu ^2),\mu ^2).`$
The claim follows. ∎

It seems difficult to obtain a more explicit description of $`\mathrm{spec}(\pi )`$, since the polynomials $`Q_n`$ do not factor well. For instance, $`Q_5`$ has an irreducible factor of degree $`5`$, and $`Q_5(\lambda ,\frac{1}{4},\frac{1}{4})`$ has Galois group $`S_5`$. Figure 1 displays the spectrum of $`\pi _6`$ and its associated spectral measure; from there we see that the spectrum of $`\pi `$ is a Cantor set.

Now we turn our attention to the Schreier graphs of $`G`$. These are graphs $`𝔊_n`$ with $`2^n`$ points corresponding to the vertices in $`T_n`$, with edges labelled $`a`$ and $`b`$ connecting $`v`$ to $`v^a,v^b`$ respectively for all $`vT_n`$.

These graphs are therefore $`4`$-regular graphs; the Green function of the random walk on $`𝔊_n`$ is given by the integral of $`1/(1t)`$ with respect to the spectral measure given above. The striking fact is the following:

###### Proposition 4.2.

The graphs $`𝔊_n`$ are planar, and can be drawn in $``$ in such a way that they converge in the Hausdorff metric to the Julia set $`𝔍`$ of $`z^21`$.

###### Proof.

This follows from \[BGN02\], since $`z^21`$ is hyperbolic. ∎

$`𝔊_n`$ is constructed as follows: it is built of two parts $`A_n,B_n`$ connected at a distinguished vertex. Each of these is $`4`$-regular, except at the connection vertex where each is $`2`$-regular, and $`A_n`$ contains only the $`a^{\pm 1}`$-edges while $`B_n`$ contains only the $`b^{\pm 1}`$-edges.

$`A_0`$ and $`B_0`$ are the graphs on $`1`$ vertex with a single loop of the appropriate label.

If $`n=2k`$ is even, then $`B_{2k+1}=B_{2k}`$, and $`A_{2k+1}`$ is obtained by taking an $`a`$-labelled $`2^{k+1}`$-gon $`v_0,\mathrm{},v_{2^{k+1}1}`$, and attaching to each $`v_i`$ with $`i0`$ a copy of $`B_{2j}`$ where $`j`$ is the largest power of $`2`$ dividing $`i`$. Its distinguished vertex is $`v_0`$.

If $`n=2k1`$ is odd, then $`A_{2k}=A_{2k1}`$, and $`B_{2k}`$ is obtained by taking an $`b`$-labelled $`2^k`$-gon $`v_0,\mathrm{},v_{2^k1}`$, and attaching to each $`v_i`$ with $`i0`$ a copy of $`A_{2j+1}`$ where $`j`$ is the largest power of $`2`$ dividing $`i`$. Its distinguished vertex is $`v_0`$.

The first Schreier graphs $`𝔊_n`$ of $`G`$ are drawn in Figure 2. Compare with the Julia set in Figure 3.