text:
# A Polyvariant Binding-Time Analysis for Off-line Partial Deduction

## 1 Introduction

Partial evaluation and partial deduction are well-known techniques for specialising respectively functional and logic programs. While both depart from the same basic concept, there is quite a divergence between their application and overall approach. In functional programming, the most widespread approach is to use *off-line specialisers*. These are typically very simple and fast specialisers which take (almost) no control decisions concerning the degree of specialisation. In this context, the specialisation is performed as follows: First, a *binding-time analysis* (BTA) is performed on the program which annotates all its statements as either “reducible” or “non-reducible”. The annotated program is then passed to the off-line specialiser, which executes the statements marked reducible and produces residual code for the statements marked non-reducible. In logic programming, the *on-line* approach is almost the only one used. All work is done by a complex on-line specialiser which monitors the whole specialisation process and decides on the degree of specialisation while specialising the program. A few researchers have explored off-line specialisation, but lacking an appropriate notion of BTA, they worked with hand-annotated programs, something which is far from being practical. Until now, it was unclear how to perform BTA for logic programs.

The current paper remedies this situation. It develops a BTA for logic programs, not by translating the corresponding notions from functional programming to logic programming, but by departing from first principles. Given a logic program to be specialised, we develop a logic program which performs its on-line specialisation. The behaviour of this program is analysed and the results are used to take all decisions w.r.t. the degree of specialisation off-line. This turns the on-line specialiser into an off-line specialiser. A prototype has been built and the quality and speed of the off-line specialisation has been evaluated.

## 2 Background

### 2.1 Partial Deduction

In contrast to ordinary (full) evaluation, a partial evaluator receives a program $`P`$ along with only part of its input, called the static input. The remaining part of the input, called the dynamic input, will only be known at some later point in time. Given the static input $`S`$, the partial evaluator then produces a specialised version $`P_S`$ of $`P`$ which, when given the dynamic input $`D`$, produces the same output as the original program $`P`$. The goal is to exploit the static input in order to derive a more efficient program.

In the context of logic programming, full input to a program $`P`$ consists of a goal $`G`$ and evaluation corresponds to constructing a complete SLDNF-tree for $`P\{G\}`$. The static input is given in the form of a partially instantiated goal $`G^{}`$ (and the specialised program should be correct for all instances of $`G^{}`$).

A technique which produces specialised programs is known under the name of *partial deduction* . Its general idea is to construct a finite set of atoms $`𝒜`$ and a finite set of finite, but possibly incomplete SLDNF-trees (one for every111Formally, an SLDNF-tree is obtained from an atom or goal by what is called an unfolding rule. atom in $`𝒜`$) which “cover” the possibly infinite SLDNF-tree for $`P\{G^{}\}`$. The derivation steps in these SLDNF-trees correspond to the computation steps which have been performed beforehand and the specialised program is then extracted from these trees by constructing one specialised clause per non-failing branch.

In partial deduction one usually distinguishes two levels of control: the global control, determining the set $`𝒜`$, thus deciding which atoms are to be partially deduced, and the local control, guiding construction of the finite SLDNF-trees for each individual atom in $`𝒜`$ and thus determining what the definitions for the partially deduced atoms look like.

### 2.2 Off-line vs. On-line Control

The (global and local) control problems of partial evaluation and deduction in general have been tackled from two different angles: the so-called on-line versus off-line approaches. The on-line approach performs all the control decisions during the actual specialisation phase. The off-line approach on the other hand performs a (binding-time) analysis phase prior to the actual specialisation phase. This analysis starts from a description of which parts of the inputs will be “*static*” (i.e. sufficiently known) and provides *binding-time annotations* which encode the control decisions to be made by the specialiser, so that the specialiser becomes much more simple and efficient.

Partial evaluation of functional programs  has mainly stressed off-line approaches, while supercompilation of functional  and partial deduction of logic programs  have concentrated on on-line control.

On-line methods, usually obtain better specialisation, because no control decisions have to be taken beforehand, i.e. at a point where the full specialisation information is not yet available. The main reasons for using the off-line approach are to make specialisation itself more efficient and, due to a simpler specialiser algorithm, enable effective self-application (specialisation of the specialiser) .

Few authors discuss off-line specialisation in the context of logic programming , mainly because so far no automated binding-time analysers have been developed. This paper aims to remedy this problem.

## 3 Towards BTA for partial deduction

### 3.1 An on-line specialiser

The basic idea of BTA in functional programming is to model the flow of static input: the arguments of a function call flow to the function body, the result of a function flows back to the call expression. The expressions are annotated reducible when enough of their parameters are static, i.e. will be known at specialisation time, to allow the (partial) computation of the expression. Modelling the dataflow gives a system of inequalities over variables in a domain $`\{static,dynamic\}`$ whose least solution yields the best annotation.

This approach does not immediately translate to logic programs. Problems are that the dataflow in unification is bidirectional and that the degree of instantiation of a variable can change over its lifetime (see also ).

We follow a different approach and reconstruct binding-time analysis from first principles. We start with a Prolog program which performs the unfolding decisions of an on-line specialiser. However, whereas real on-line specialisers base their unfolding decisions on the history of the specialisation phase, ours bases its decisions solely on the actual arguments of the call (which can be more easily approximated off-line). This is in agreement with the off-line specialisers for functional languages which base their decision to evaluate or residualise an expression on the availability of the parameters of that expression. The next step will be to analyse the behaviour of this program (the binding-time analysis) and to use the results to make the unfolding decisions at compile time.

First we develop the on-line specialiser. Assuming that for each predicate $`p/m`$ a *test* predicate $`\mathrm{𝑢𝑛𝑓𝑜𝑙𝑑}\mathrm{\_}p/m`$ exists which decides whether to unfold a call or not, we obtain an on-line specialiser by replacing each call $`p(\overline{t})`$ by

$$(\mathrm{𝑢𝑛𝑓𝑜𝑙𝑑}\mathrm{\_}p(\overline{t})p(\overline{t});\mathrm{𝑚𝑒𝑚𝑜𝑖𝑠𝑒}\mathrm{\_}p(\overline{t}))$$

A call to $`\mathrm{𝑚𝑒𝑚𝑜𝑖𝑠𝑒}\mathrm{\_}p(\overline{t})`$ informs the specialiser that the call $`p(\overline{t})`$ has to be residualised. The specialiser has to check whether (a generalisation of) $`p(\overline{t})`$ has already been specialised —if not it has to initiate the specialisation of (a generalisation of) $`p(\overline{t})`$— and has to perform appropriate renaming of predicates to ensure that residual code calls the proper specialised version of the predicate it calls.

###### Example 1 (Funny append)

Consider the following on-line specialiser for a variant, $`\mathrm{𝑓𝑢𝑛𝑛𝑦𝑎𝑝𝑝}/\mathit{3}`$ of the $`\mathrm{𝑎𝑝𝑝𝑒𝑛𝑑}/\mathit{3}`$ predicate in which the first two arguments of the recursive call have been swapped:

funnyapp(\[\],X,X).  funnyapp(\[X|U\],V,\[X|W\]) :-   ( unfold\_funnyapp(V,U,W) -\> funnyapp(V,U,W)   ; memoise\_funnyapp(V,U,W) ).  unfold\_funnyapp(X,Y,Z) :- ground(X).

Specialising this program for a query funnyapp(\[a,b\],L,R) results in the specialised clause (the residual call is renamed as funnyapp\_1)

* funnyapp(\[a,b\],L,\[a|R1\]) :- funnyapp\_1(L,\[b\],R1).

Specialising the funnyapp program for the residual call funnyapp(L,\[b\],R1) gives (after renaming) the clauses

* funnyapp\_1(\[\],\[b\],\[b\]).
* funnyapp\_1(\[X|U\],\[b\],\[X,b|R\]) :- funnyapp\_2(U,\[\],R).

Once more specialising, now for the residual call funnyapp(U,\[\],R), gives

* funnyapp\_2(\[\],\[\],\[\]).
* funnyapp\_2(\[X|U\],\[\],\[X|U\]).

This completes the specialisation. Note that the sequence of residual calls is terminating in this example. In general, infinite sequences are possible. They can be avoided by generalising some arguments of the residual calls before specialising.

In the above example, instead of using ground(X) as condition of unfolding, one could also use the test nilterminated(X).This would allow to obtain the same level of specialisation for a query funnyappend(\[X,Y\],L,R). This test is another example of a so called *rigid* or *downward closed* property: if it holds for a certain term, it holds also for all its instances. Such properties are well suited for analysis by means of abstract interpretation.

### 3.2 From on-line to off-line

Turning the on-line specialiser into an off-line one requires to determine the $`\mathrm{𝑢𝑛𝑓𝑜𝑙𝑑}\mathrm{\_}p/n`$ predicates during a preceding analysis and to decide on whether to replace the $`(\mathrm{𝑢𝑛𝑓𝑜𝑙𝑑}\mathrm{\_}p(\overline{t})p(\overline{t});memoise(p(\overline{t})))`$ construct either by $`p(\overline{t})`$ or by $`memoise(p(\overline{t}))`$. The decision has to be based on a safe estimate of the calls $`\mathrm{𝑢𝑛𝑓𝑜𝑙𝑑}\mathrm{\_}p(\overline{t})`$ which will occur during the specialisation. Computing such safe approximations is exactly the purpose of *abstract interpretation* .

:- $`\{`$grnd(L1)$`\}`$ fap1(L1,L2,R) $`\{`$grnd(L1)$`\}`$.  fap1(\[\],X,X).  fap1(\[X|U\],V,\[X|W\]) :- $`\{`$grnd(X,U)$`\}`$   ( unf\_fap1(V,U,W) $`\{`$grnd(X,U,V)$`\}`$ -\>   $`\{`$grnd(X,U,V)$`\}`$ fap2(V,U,W) $`\{`$grnd(X,U,V,W)$`\}`$   ; $`\{`$grnd(X,U)$`\}`$ memo\_fap3(V,U,W) $`\{`$grnd(X,U)$`\}`$   ) $`\{`$grnd(X,U)$`\}`$.  unf\_fap1(X,Y,Z) :- $`\{`$grnd(Y)$`\}`$ ground(X) $`\{`$grnd(X,Y)$`\}`$.  memo\_fap3(X,Y,Z).

By adding to the code of Example 1 the fact memoise\_funnyapp(X,Y,Z)., and an appropriate handling of the Prolog built-in ground/1, one can run a goal-dependent *polyvariant* groundness analysis (using e.g. PLAI coupled with the set-sharing domain) for a query where the first argument is ground and obtain the above annotated program. The annotated code for the version fap2 is omitted because it is irrelevant for us. Indeed, inspecting the annotations for unf\_fap1 we see that the analysis cannot infer the groundness of its first argument. So we decide off-line not to unfold, we cancel the test and the then branch and simplify the code into:

:- $`\{`$grnd(L1)$`\}`$ fap1(L1,L2,R) $`\{`$grnd(L1)$`\}`$.  fap1(\[\],X,X).  fap1(\[X|U\],V,\[X|W\]) :- $`\{`$grnd(X,U)$`\}`$ memo\_fap3(V,U,W) $`\{`$grnd(X,U)$`\}`$.

The residual call to funnyappend has a different call pattern than the original call: its second argument is now ground. Thus we perform a second analysis and obtain (the annotated code for fap4 is omitted):

:- $`\{`$grnd(L2)$`\}`$ fap3(L1,L2,R) $`\{`$grnd(L2)$`\}`$.  fap3(\[\],X,X).  fap3(\[X|U\],V,\[X|W\]) :- $`\{`$grnd(V)$`\}`$   ( unf\_fap2(V,U,W) $`\{`$grnd(V)$`\}`$ -\>   $`\{`$grnd(V)$`\}`$ fap4(V,U,W) $`\{`$grnd(V)$`\}`$   ; $`\{`$grnd(V)$`\}`$ memo\_fap5(V,U,W) $`\{`$grnd(V)$`\}`$   ) $`\{`$grnd(V)$`\}`$.  unf\_fap2(X,Y,Z) :- $`\{`$grnd(X)$`\}`$ ground(X) $`\{`$grnd(X)$`\}`$.  memo\_fap5(X,Y,Z).

This time, the annotations for unf\_fap2 show that the groundness test will definitely succeed. So we decide off-line always to unfold and only keep the *then* branch. Moreover, the fap4 call has the same call pattern as the original call to funnyapp, so we also rename it as fap1. This yields the second code fragment:

:- $`\{`$grnd(L2)$`\}`$ fap3(L1,L2,R) $`\{`$grnd(L2)$`\}`$.  fap3(\[\],X,X).  fap3(\[X|U\],V,\[X|W\]) :- $`\{`$grnd(V)$`\}`$ fap1(V,U,W) $`\{`$grnd(V)$`\}`$

Applying the specialiser on these two code fragments for a query fap1(\[a,b\],L,R) gives the same specialised code as in Example 1. However, this time, no calls to unfold\_funnyapp have to be evaluated during specialisation.

### 3.3 Automation

To weave the step by step analysis sketched above in a single analysis, a special purpose tool has to be built. We implemented a system based on the abstract domain POS, also called PROP . It describes the state of the program variables by means of *positive* boolean formulas, i.e., formulas built from $`,`$ and $``$. Its most popular use is for groundness analysis. In that case, the formula $`X`$ expresses that the program variable $`X`$ is (definitely) bound to a ground term, $`XY`$ expresses that $`X`$ is bound to a ground term iff $`Y`$ is, so an eventual binding of $`X`$ to a ground term will be propagated to $`Y`$. This domain is extended with $`\mathrm{𝑓𝑎𝑙𝑠𝑒}`$ as bottom element and is ordered by boolean implication. Groundness analysis corresponds to checking the rigidity222A term is rigid w.r.t. a norm if all its instances have the same size w.r.t. the norm. of program variables w.r.t. the *termsize norm*333The termsize norm  includes all subterms in the measure of the term. and abstracts a unification such as $`X=[Y|Z]`$ by the boolean formula $`XYZ`$. However POS can also be used with other semi-linear norms . In e.g. normalised programs, it only requires to redefine the abstraction of the unifications. For example, with the *listlength norm*444The listlength norm  includes only the tail of the list in the measure of the list (and measures other terms as 0); nil-terminated lists are rigid under this norm., unification of $`X=[Y|Z]`$ is abstracted as $`XZ`$, and a formula $`X`$ means that the program variable $`X`$ is bound to a term with a bounded listlength, i.e. either the term is a nil-terminated list, or has a main functor which is not a list constructor.

The analyser has to decide the outcome of the $`\mathrm{𝑢𝑛𝑓𝑜𝑙𝑑}\mathrm{\_}p`$ test and has to decide which branch to take for further analysis while doing the analysis. Also it has to launch the analysis of the generalisations of the memoised calls. The generalisation we employ is to replace an argument which is not rigid under the norm used in the analysis by the abstraction of a fresh variable. These requirements exclude the direct use of the abstract compilation technique in the way advocated by e.g. . One problem of the scheme of  is that it handles constructs $`(ground(X)p(\overline{t});\mathrm{𝑚𝑒𝑚𝑜𝑖𝑠𝑒}(p(\overline{t})))`$ too inaccurately. The boolean formula is represented as a truth table, i.e. a set of tuples, and the analyser processes the truth table a tuple at a time. Therefore it cannot infer in a program point that $`X`$ is true, i.e. that $`X`$ is definitely ground, so it can never conclude that the else branch cannot be taken. The other problem is that the analyses launched for the *memoised* calls should not interfere (i.e. output should not flow back) with the analysis of the clauses containing the memoised calls. Note that defining $`\mathrm{𝑚𝑒𝑚𝑜𝑖𝑠𝑒}`$ as $`\mathrm{𝑚𝑒𝑚𝑜𝑖𝑠𝑒}\mathrm{\_}p(X_1,\mathrm{},X_n):\mathrm{𝑐𝑜𝑝𝑦}(X_1,Y_1),\mathrm{},\mathrm{𝑐𝑜𝑝𝑦}(X_n,Y_n)`$, and abstracting $`\mathrm{𝑐𝑜𝑝𝑦}(X,Y)`$ as $`XY`$ does not work: The abstract success state of executing $`p(Y_1,\mathrm{},Y_n)`$ will update the abstractions of $`X_1,\mathrm{},X_n`$.

Our prototype binding-time analyser currently consists of $`800`$ lines of Prolog code and uses XSB  as a generic tool for semantic-based program analysis . The boolean formulas from the POS domain are represented by their truth tables. This representation enables abstract operations to have straightforward implementations based on the projection and equi-join operations of the relational algebra. The disadvantage is that the size of truth tables quickly increases with the number of variables in a clause. The use of dedicated data structures like BDDs to represent the boolean formulas as in  often results in better performance but at the expense of substantial programming efforts.

The main part of the analyser can be seen as a source-to-source transformation (i.e. abstract compilation) that given the program $`P`$ to be analysed, produces an abstract program $`P^\alpha `$ with suitable annotations. The abstract program can be directly run under XSB (using tabling to ensure termination). The execution leaves the results of the analysis in the XSB *tables*. Each predicate $`p/n`$ of $`P`$ is abstracted to a predicate $`p^\alpha /2`$ whose arguments carry input and output *sets* of tuples. The core part of setting up the analysis is then to define the code for the abstract interpretation of each call (at a program point PP# of interest):

$$(\mathrm{𝑢𝑛𝑓𝑜𝑙𝑑}\mathrm{\_}p(\overline{X})p(\overline{X});\mathrm{𝑚𝑒𝑚𝑜𝑖𝑠𝑒}\mathrm{\_}p(\overline{X})).$$
(1)
is abstracted by the following code fragment:

* $`project(`$Args,TPPin,TC$`),`$
* ( $`\mathrm{𝑢𝑛𝑓𝑜𝑙𝑑}\mathrm{\_}p(`$TC$`)`$ -\>
* $`\mathrm{𝑢𝑛𝑓𝑜𝑙𝑑}(`$TC,PP$`{}_{\mathrm{\#}}{}^{})`$, $`p^\alpha (`$TC,TR$`)`$
* ; TR=TC, $`generalise(`$TC,TCG$`),`$ $`memo(`$TCG,PP$`{}_{\mathrm{\#}}{}^{}),`$ $`p^\alpha (`$TCG,\_$`)`$ ),
* $`equi\mathrm{\_}join(`$Args,TPPin,TR,TPP$`{}_{out}{}^{}),`$

Predicates $`unfold/2`$ and $`memo/2`$ which abstract the behaviour of each call in the form of (1) above are *tabled* predicates which have no effect on the computation, but only record information containing the results of the analysis. Their arguments are the current abstraction and the current program point. This information is then dumped from the XSB tables and is fed to the off-line specialiser. The variable TPPin holds the truth table which represents the abstraction of the program state in the point prior to the call. The call to $`project/3`$ projects the truth table on the positions Args of the variables $`\overline{X}`$ participating in the call. The result is TC (Tuples of the Call). The predicate $`unfold\mathrm{\_}p/1`$ (currently supplied by the user for each predicate $`p/n`$ to be analysed) inspects TC to decide whether there is sufficient information to unfold the call. If it succeeds the *then* branch is taken which analyses the effects of unfolding $`p/n`$. This is done by executing $`p^\alpha /2`$ with TC as abstraction of the call state. The analysis returns TR as abstraction of the program state reached after unfolding $`p/n`$. If the call to $`unfold\mathrm{\_}p/1`$ fails, the call is memoised, and the program state remains unchanged, so TR = TC. The generalisation of the memoised call also needs to be analysed; therefore the else branch first generalises the current state TC into TCG by erasing all dependencies for non-rigid arguments555A position is rigid if it has an “s” in each tuple e.g. $`generalise(`$\[p(s,s,s), p(s,d,d)\],TCG$`)`$ yields TCG = \[p(s,s,s), p(s,s,d), p(s,d,s), p(s,d,d)\]. and then calls $`p^\alpha /2`$ with TCG as initial state, but takes care not to use the returned abstract state as the bindings resulting from specialising memoised calls do not flow back. These actions effectively realise the intended functionality of $`\mathrm{𝑚𝑒𝑚𝑜𝑖𝑠𝑒}\mathrm{\_}p/1`$. Finally, the new program state TR over the variables $`\overline{X}`$ has to be propagated to the other program variables described by the initial state TPPin. This is achieved simply by taking the equi-join over the Args of TPPin and TR. The new program state is described by TPPout.

One of our examples (see Section 4.2) uses two different norms in the $`\mathrm{𝑢𝑛𝑓𝑜𝑙𝑑}`$ tests: the term norm which tests for groundness, and the listlength norm which tests for the boundedness of lists (whether lists are nil-terminated). This does not pose a problem for our framework, we simply use a truth table which encodes two boolean formulas, one for the term norm and one for the listlength norm.

## 4 Some Experiments and Benchmarks

We first discuss the parser and liftsolve examples from .

### 4.1 The parser example

A small generic parser for languages defined by grammars of the form $`S::=aS|X`$ ($`X`$ is a placeholder for a terminal symbol as well as the first argument to nont/3; arguments 2 and 3 represent the string to be parsed as a difference list):

* nont(X,T,R) :- t(a,T,V),nont(X,V,R).
* nont(X,T,R) :- t(X,T,R).
* t(X,\[X|Es\],Es).

A termination analysis can easily determine that calls to t/3 always terminate and that calls to nont/3 terminate if their second argument is ground. One can therefore derive the following unfold predicates:

* unfold\_t(X,S1,S2).
* unfold\_nont(X,T,R) :- ground(T).

Performing our analysis for the entry point :-  $`\{grnd(X)\}`$ nont(X,\_,\_) we obtain the following annotated program (dynamic arguments \[i.e. non-ground ones\] and non-reducible predicates \[i.e. memoised ones\] are underlined):

* nont(X,T,R) :- t(a,T,V), nont(X,V,R).
* nont(X,T,R) :- t(X,T,R).
* t(X,\[X|Es\],Es).

Feeding this information into the off-line system logen  and specialising nont(c,T,R), we obtain:

* nont\__0(\[a$`|`$B\],C) :- nont\__0(B,C).
* nont\__0(\[c$`|`$D\],D).

Analysing the same specialiser for :-  $`\{grnd(T)\}`$ nont(\_,T,\_) yields:

* nont(X,T,R) :- t(a,T,V), nont(X,V,R).
* nont(X,T,R) :- t(X,T,R).
* t(X,\[X|Es\],Es).

Feeding this information into logen and specialising nont(X,\[a,a,c\],R) yields:

* nont\__0(c,\[\]).
* nont\__0(a,\[c\]).
* nont\__0(a,\[a,c\]).

### 4.2 The liftsolve example

The following program is a meta-interpreter for the ground representation, in which the goals are “lifted” to the non-ground representation for resolution. To perform the lifting, an accumulating parameter is used to keep track of the variables that have already been encountered and generated. The predicate mng and l\_mng transform (a list of) ground terms (the first argument) into (a list of) non-ground terms (the second argument; the third and fourth arguments represent the incoming and outgoing accumulator respectively). The predicate solve uses these predicates to “lift” clauses of a program in ground representation (its first argument) and then use them for resolution with a non-ground goal (its second argument) to be solved.
solve(GrP,\[\]).  solve(GrP,\[NgH|NgT\]) :-   non\_ground\_member(term(clause,\[NgH$`|`$NgBdy\]),GrP),   solve(GrP,NgBdy), solve(GrP,NgT).  non\_ground\_member(NgX,\[GrH$`|`$\_GrT\]) :- make\_non\_ground(GrH,NgX).  non\_ground\_member(NgX,\[\_GrH$`|`$GrT\]) :- non\_ground\_member(NgX,GrT).  make\_non\_ground(G,NG) :- mng(G,NG,\[\],\_Sub).  mng(var(N),X,\[\],\[sub(N,X)\]).  mng(var(N),X,\[sub(N,X)$`|`$T\],\[sub(N,X)$`|`$T\]).  mng(var(N),X,\[sub(M,Y)$`|`$T\],\[sub(M,Y)$`|`$T1\]) :- N `\==` M, mng(var(N),X,T,T1).  mng(term(F,Args),term(F,IArgs),InS,OutS) :- lmng(Args,IArgs,InS,OutS).  lmng(\[\],\[\],Sub,Sub).  lmng(\[H|T\],\[IH$`|`$IT\],InS,OutS) :-   mng(H,IH,InS,InS1), lmng(T,IT,InS1,OutS).

The following unfold predicates can be derived by a termination analysis:

* unfold\_lmng(Gs,NGs,InSub,OutSub) :- ground(Gs), bounded\_list(InSub).
* unfold\_mng(G,NG,InSub,OutSub) :- ground(G), bounded\_list(InSub).
* unfold\_make\_non\_ground(G,NG) :- ground(G).
* unfold\_non\_ground\_member(NgX,L) :- ground(L).
* unfold\_solve(GrP,Query) :- ground(GrP).

Analysing the specialiser for the entry point solve(ground,\_) we obtain:

* solve(GrP,\[\]).
* solve(GrP,\[NgH$`|`$NgT\]) :-
non\_ground\_member(term(clause,\[NgH$`|`$NgBdy\]), GrP),
solve(GrP,NgBdy), solve(GrP,NgT).
* non\_ground\_member(NgX,\[GrH$`|`$\_GrT\]) :- make\_non\_ground(GrH,NgX).
* non\_ground\_member(NgX,\[\_GrH$`|`$GrT\]) :- non\_ground\_member(NgX,GrT).
* make\_non\_ground(G,NG) :- mng(G,NG, \[\],\_Sub).
* mng(var(N),X,\[\],\[sub(N,X)\]).
* mng(var(N),X,\[sub(N,X)$`|`$T\], \[sub(N,X)$`|`$T\]).
* mng(var(N),X,\[sub(M,Y)$`|`$T\], \[sub(M,Y)$`|`$T1\]) :- N `\==` M, mng(var(N),X,T,T1).
* mng(term(F,Args),term(F,IArgs), InS,OutS) :- lmng(Args,IArgs, InS,OutS).
* lmng(\[\],\[\],Sub,Sub).
* lmng(\[H$`|`$T\],\[IH$`|`$IT\], InS,OutS) :- mng(H,IH,InS,InS1), lmng1(T,IT, InS1,OutS).
* lmng1(\[\],\[\],Sub,Sub).
* lmng1(\[H$`|`$T\],\[IH$`|`$IT\], InS,OutS) :- mng1(H,IH,InS,InS1), lmng1(T,IT, InS1,OutS).
* mng1(var(N),X,\[\],\[sub(N,X)\]).
* mng1(var(N),X, \[sub(N,X)$`|`$T\],\[sub(N,X)$`|`$T\]).
* mng1(var(N),X, \[sub(M,Y)$`|`$T\],\[sub(M,Y)$`|`$T1\]) :- N $`\backslash `$== M, mng1(var(N),X,T,T1).
* mng1(term(F,Args),term(F,IArgs), InS,OutS) :- lmng1(Args,IArgs, InS,OutS).

One can observe that the call lmng1(T,IT, InS1,OutS) has not been unfolded. Indeed, the third argument InS1 is considered to be dynamic (non-ground) and the call to unfold\_lmng will thus not always succeed. However, based on the termination analysis, it is actually sufficient for termination if the third arguments to mng and lmng are bounded lists (as the listlength norm can be used in the termination proof). If we use our prototype to also keep track of bounded lists we obtain the desired result: the call lmng1(T,IT,InS1,OutS) can be unfolded as the first argument is ground and third argument can be inferred to be a bounded list. By feeding the so obtained annotations into logen  we obtain a specialiser which removes (most of) the meta-interpretation overhead. E.g. specialising

* solve(\[term(clause,\[term(q,\[var(1)\]), term(p,\[var(1)\])\]),
* term(clause,\[term(p,\[term(a,\[\])\])\])\],G)

yields the following residual program:

* solve\__0(\[\]).
* solve\__0(\[term(q,\[B\])|C\]) :- solve\__0(\[term(p,\[B\])\]),solve\__0(C).
* solve\__0(\[term(p,\[term(a,\[\])\])|D\]) :- solve\__0(\[\]),solve\__0(D).

### 4.3 Some Benchmarks

We now study the efficiency and quality of our approach on a set of benchmarks. Except for the parser benchmark all benchmarks come from the dppd benchmark library . We ran our prototype analyser, bta, that performs binding-time analysis and fed the result into the off-line compiler generator logen  in order to derive a specialiser for the task at hand. The ecce on-line partial deduction system  has been used for comparison (settings are the same as for ecce-x in , i.e. a mixtus like unfolding, a global control based upon characteristic trees but no use of conjunctive partial deduction). The interested reader can consult  to see how ecce compares with other systems.

All experiments were conducted on a Sun Ultra-1 running SunOS 5.5.1. ecce and logen were run using Prolog by BIM 4.1.0. bta was run on XSB 1.7.2.

In Table 1 one can see a summary of the transformation times. The columns under bta contain: the time to abstract and compile the program + the time for execution of the abstracted program (both under XSB). The column under logen contains the time to generate the specialiser with logen using the so obtained annotations. Observe, that for any given initial annotation, this has only to be performed once: the so obtained specialiser can then be used over and over again for different specialisation tasks. E.g. the same specialiser was used for the liftsolve.app and liftsolve.app4 benchmark. The ‘\*’ for liftsolve.app indicates the time for the abstract compilation only producing code for the groundness analysis. The extra arguments and instructions for the bounded list analysis were added by hand (but will be generated automatically in the next version of the prototype). The column under PD gives the time for the off-line specialisation. The last column of the table contains the ratio of running ecce over running the specialisers generated by bta + logen. As can be seen, the specialisers produced by bta + logen run 28 – 880 times faster than ecce. We conjecture that for larger programs (e.g liftsolve with a very big object program) this difference can get even bigger. Also, for 3 benchmarks the combined time of running bta + logen and then the so obtained specialiser was less than running ecce, i.e. our off-line approach fares well even in “one-shot” situations. Of course, to arrive at a fully automatic (terminating) system one will still have to add the time for the termination analysis, needed to derive the “unfold” predicates.

Table 2 compares the efficiency of the specialised programs (for the run time queries see ; for the parser example we ran $`\mathrm{𝑛𝑜𝑛𝑡}(c,[a^{17},c,b],\left[b\right])`$ 100 times). As was to be expected, the programs generated by the on-line specialiser ecce outperform those generated by our off-line system. E.g. for the match.kmp benchmark ecce is able to derive a Knuth-Morris-Pratt style searcher, while off-line systems (so far) are unable to achieve such a feat. However, one can see that the specialised programs generated by bta + logen are still very satisfactory. The most satisfactory application is liftsolve.app (as well as liftsolve.app4), where the specialiser generated by bta + logen runs 167 (resp. 880) times faster than ecce while producing residual code of equal (resp. almost equal) efficiency. In fact, the specialiser compiled the append object program from the ground representation into the non-ground one in just 0.006 s (to be compared with e.g. the compilers generated by sage  which run in the order of minutes). Furthermore, the time to produce the residual program and then running it is less than the time needed to run the original program for the given set of runtime queries. This nicely illustrates the potential of our approach for applications such as runtime code generation, where the specialisation time is (also) of prime importance.

## 5 Discussion

We have formulated a binding-time analysis for logic programs, and have reported on a prototype implementation and on an evaluation of its effectiveness. To develop the binding-time analysis, we have followed an original approach: Given a program $`P`$ to be analysed we transform it into an on-line specialiser program $`P^{}`$, in which the unfolding decision are explicitly coded as calls to predicates unfold\_p. The on-line specialiser is different from usual ones in the sense that it — like off-line specialisers — uses the availability of arguments to decide on the unfolding of calls. Next, we apply abstract interpretation —a binding-time analysis— to gather information about the run-time behaviour of $`P^{}`$. The information in the program points related to unfold\_p allows to decide whether the test will definitely succeed —in which case the unfolding branch is retained— or will possibly fail —in which case the branch yielding residual code is retained. The resulting program now behaves as an off-line specialiser as all unfolding decisions have been taken at analysis time.

An issue to be discussed in more detail is the termination of the specialisation. First, a specialiser has a global control component. It must ensure that only a finite number of atoms are specialised. In our prototype, we generalise the residual calls before generating a specialised version: arguments which are not rigid666I.e., “static” from functional programming becomes “rigid w.r.t. a given norm.” w.r.t. the norm used in the unfolding condition are replaced by fresh variables. This works well in practice but is not a sufficient condition for termination. In principle one could define the memoise\_p predicates as:

* memoise\_p($`\overline{X}`$) :- copy\_term($`\overline{X}`$,$`\overline{Y}`$), generalise($`\overline{Y}`$,$`\overline{Z}`$), p($`\overline{Z}`$).

and then generalise such that quasi-termination  of the program, where calls to p are tabulated, can be proven. In practice, the built-in copy\_term/2 and the built-ins needed to implement generalise/2 will make this a non-trivial task. Secondly, there is the local control component. It must ensure that the unfolding of a particular atom terminates. This is decided by the code of the transformed program. Defining the unfold\_p predicates by hand is error-prone and consequently not entirely reliable. In principle, one could replace the calls memoise\_p by true and apply off-the-shelf tools for proving termination of logic programs . Whether these will do well depends on how well they handle the $`\mathrm{𝑖𝑓}\mathrm{𝑡ℎ𝑒𝑛}\mathrm{𝑒𝑙𝑠𝑒}`$ construct used in deciding on the unfolding and the built-ins used in the rigidity test (e.g. the analysis has to infer that X is bounded and rigid w.r.t. the norm in the program point following a test ground(X)). It is likely that small extensions to these tools will suffice to apply them successfully in proving termination of the unfolding777After a small extension by its author, the system of  could handle small examples. However, so far we have not done exhaustive testing., at least when the unfolding conditions are based on rigidity tests with respect to the norms used by those termination analysis tools.

A more interesting approach for the local control problem is to automatically generate unfolding conditions by program analysis. Actually, one could apply a more general scheme for handling the unfolding than the one used so far. Having for each predicate p/n the original clauses with head p/n and transformed clauses with head pt/n, the transformed clauses could be derived from the original by replacing each call q/m by:

* ( terminates\_q($`\overline{t}`$) -\> q($`\overline{t}`$)
; ( unfold\_q($`\overline{t}`$) -\> qt($`\overline{t}`$) ; memoise\_q($`\overline{t}`$) ) )

In , Decorte and De Schreye describe how the constraint-based termination analysis of  can be adapted to generate a finite set of “most general” termination conditions (e.g. for append/3 they would generate rigidity w.r.t. the listlength norm of the first argument and rigidity w.r.t. the listlength norm of the third argument as the two most general termination conditions; for our funnyapp/3 they would generate rigidity of the first and second argument w.r.t. the listlength norm as the most general termination condition.). These conditions can be used to define the terminates\_q predicates. If they succeed, the call q($`\overline{t}`$) can be executed with the original code and is guaranteed to terminate. Moreover, as they are based on rigidity, they are very well suited to be approximated by our binding-time analysis. Actually, in all our benchmarks programs, we were using termination conditions for controlling the unfolding, so in fact we could have further improved the speed of the specialiser by not checking the condition on each iteration but using the above scheme.

Generating unfold\_q definitions is a harder problem. It is related to the generation of “safe” (i.e. termination ensuring) delay declarations in languages such as MU-Prolog and Gödel. This is a subtle problem as discussed in . For example, the condition (nonvar(X); nonvar(Z)) is not safe for a call append(X,Y,Z); execution, and in our case unfolding, could go on infinitely for some non-linear calls (e.g. append(\[a|L\],Y,L)). Also the condition nonvar/1 is not rigid. (For funnyapp/3 we had rigid conditions, however this is rather the exception than the rule.) A safe unfolding condition for append(X,Y,Z) is linear(append(X,Y,Z)), (nonvar(X); nonvar(Z)). Linearity is well suited for analysis (e.g. ), but a test nonvar(X) is not. Moreover, unless X is ground, the test is typically not invariant over the different iterations of a recursive predicate. A solution could be to switch to a hybrid specialiser: deciding the linearity test at analysis-time and the simple nonvar tests at run-time. But as said above, perhaps due to lack of a good application (for languages with delay, speed is more important than safety), there seems to be no work on generating such conditions.

Another hybrid approach is taken in a recent work independent of ours . This work also starts from the termination condition. When it is violated, the size of the term w.r.t. the norm used in the termination condition and the maximal reduction of the size in a single iteration is used to compute the number of unfolding steps. The program is transformed and calls to be unfolded are given an extra argument initialised with the allowed number of unfolding steps. An on-line test checks the value of the counter and the call is residualised when the counter reaches zero.

### Acknowledgements

M. Bruynooghe and M. Leuschel are supported by the Fund for Scientific Research - Flanders Belgium (FWO). K. Sagonas is supported by the Research Council of the K.U. Leuven. Some of the present ideas originated from discussions and joint work with Jesper Jørgensen, and from the PhD. work of Dirk Dussart , to both of whom we are very grateful. We thank Bart Demoen, Stefaan Decorte, Bern Martens, Danny De Schreye and Sandro Etalle for interesting discussions, ideas and comments.

## Appendix 0.A Specialised Programs generated by bta + logen

### 0.A.1 Parser

Original program:

```
nont(X,T,R) :- t(a,T,V),nont(X,V,R).
nont(X,T,R) :- t(X,T,R).
t(X,[X|Es],Es).

```

Partial deduction query:

```
nont(c,X,Y).

```

Specialised program (where nont(c,X,Y) has been renamed to nont\__0(X,Y)):

```
nont__0([a|B],C) :- nont__0(B,C).
nont__0([c|D],D).

```

### 0.A.2 Liftsolve.app

Original program:

```
solve(GrRules,[]).
solve(GrRules,[NgH|NgT]) :-
        non_ground_member(term(clause,[NgH|NgBody]),GrRules),
        solve(GrRules,NgBody),
        solve(GrRules,NgT).

non_ground_member(NgX,[GrH|_GrT]) :-
        make_non_ground(GrH,NgX).
non_ground_member(NgX,[_GrH|GrT]) :-
        non_ground_member(NgX,GrT).

make_non_ground(G,NG) :- mng(G,NG,[],Sub).

mng(var(N),X,[],[sub(N,X)]).
mng(var(N),X,[sub(N,X)|T],[sub(N,X)|T]).
mng(var(N),X,[sub(M,Y)|T],[sub(M,Y)|T1]) :-
        N \== M, mng(var(N),X,T,T1).
mng(term(F,Args),term(F,IArgs),InSub,OutSub) :-
        l_mng(Args,IArgs,InSub,OutSub).

l_mng([],[],Sub,Sub).
l_mng([H|T],[IH|IT],InSub,OutSub) :-
        mng(H,IH,InSub,IntSub),
        l_mng(T,IT,IntSub,OutSub).

```

Partial deduction query:

```
solve([term(clause,[term(app,[term(null,[]),var(l),var(l)])]),
       term(clause,[term(app,[term(cons,[var(h),var(x)]),var(y),
          term(cons,[var(h),var(z)])]),term(app,[var(x),var(y),var(z)])])],
        [term(app,[X1,X2,X3])]).

```

Specialised program:

```
solve__0([]).
solve__0([term(app,[term(null,[]),B,B])|C]) :-
  solve__0([]), solve__0(C).
solve__0([term(app,[term(cons,[D,E]),F,term(cons,[D,G])])|H]) :-
  solve__0([term(app,[E,F,G])]), solve__0(H).

```

### 0.A.3 Liftsolve.app4

Same original program as liftsolve.app.

Partial deduction query:

```
solve([term(clause,[term(app,[term(null,[]),var(l),var(l)])]),
       term(clause,[term(app,[term(cons,[var(h),var(x)]),var(y),
                              term(cons,[var(h),var(z)])]),
                    term(app2,[var(x),var(y),var(z)])]),
       term(clause,[term(app2,[term(null,[]),var(l),var(l)])]),
       term(clause,[term(app2,[term(cons,[var(h),var(x)]),var(y),
                               term(cons,[var(h),var(z)])]),
                    term(app3,[var(x),var(y),var(z)])]),
       term(clause,[term(app3,[term(null,[]),var(l),var(l)])]),
       term(clause,[term(app3,[term(cons,[var(h),var(x)]),var(y),
                               term(cons,[var(h),var(z)])]),
                    term(app4,[var(x),var(y),var(z)])]),
       term(clause,[term(app4,[term(null,[]),var(l),var(l)])]),
       term(clause,[term(app4,[term(cons,[var(h),var(x)]),var(y),
                               term(cons,[var(h),var(z)])]),
                    term(app,[var(x),var(y),var(z)])])],
       [term(app,[_X,_Y,_Z])])

```

Specialised program:

```
solve__0([]).
solve__0([term(app,[term(null,[]),B,B])|C]) :-
  solve__0([]),solve__0(C).
solve__0([term(app,[term(cons,[D,E]),F,term(cons,[D,G])])|H]) :-
  solve__0([term(app2,[E,F,G])]),solve__0(H).
solve__0([term(app2,[term(null,[]),I,I])|J]) :-
  solve__0([]),solve__0(J).
solve__0([term(app2,[term(cons,[K,L]),M,term(cons,[K,N])])|O]) :-
  solve__0([term(app3,[L,M,N])]),solve__0(O).
solve__0([term(app3,[term(null,[]),P,P])|Q]) :-
  solve__0([]),solve__0(Q).
solve__0([term(app3,[term(cons,[R,S]),T,term(cons,[R,U])])|V]) :-
  solve__0([term(app4,[S,T,U])]),solve__0(V).
solve__0([term(app4,[term(null,[]),W,W])|X]) :-
  solve__0([]),solve__0(X).
solve__0([term(app4,[term(cons,[Y,Z]),A_1,term(cons,[Y,B_1])])|C_1]) :-
  solve__0([term(app,[Z,A_1,B_1])]),solve__0(C_1).

```

### 0.A.4 Depth

Original program:

```
depth( true, 0 ).
depth( (_g1,_gs), _depth ) :-
    depth( _g1, _depth_g1 ),
    depth( _gs, _depth_gs ),
    max( _depth_g1, _depth_gs, _depth ).
depth( _goal, s(_depth) ) :-
    prog_clause( _goal, _body ),
    depth( _body, _depth ).

```

Partial deduction query:

```
depth(member(X,[a,b,c,m,d,e,m,f,g,m,i,j]),D).

```

Specialised program:

```
depth__0(true,0).
depth__0(member(B,C),s(D)) :-
  depth__0(append(E,[B|F],C),D).
depth__0(append([],G,G),s(H)) :-
  depth__0(true,H).
depth__0(append([I|J],K,[I|L]),s(M)) :-
  depth__0(append(J,K,L),M).

```

### 0.A.5 Match.Kmp

Original program:

```
match(Pat,T) :- match1(Pat,T,Pat,T).

match1([],Ts,P,T).
match1([A|Ps],[B|Ts],P,[X|T]) :-
        A\==B,match1(P,T,P,T).
match1([A|Ps],[A|Ts],P,T) :-
        match1(Ps,Ts,P,T).

```

Partial deduction query:

```
match([a,a,b],R).

```

Specialised program:

```
match1__4(B,C).
match1__3([B|C],[D|E]) :- \==(b,B), match1__1(E,E).
match1__3([b|F],G) :- match1__4(F,G).
match1__2([B|C],[D|E]) :- \==(a,B), match1__1(E,E).
match1__2([a|F],G) :- match1__3(F,G).
match1__1([B|C],[D|E]) :- \==(a,B), match1__1(E,E).
match1__1([a|F],G) :- match1__2(F,G).
match__0(B) :- match1__1(B,B).

```

### 0.A.6 Regexp.r1

Original program:

```
generate(empty,T,T).
generate(char(X),[X|T],T).
generate(or(X,Y),H,T) :- generate(X,H,T).
generate(or(X,Y),H,T) :- generate(Y,H,T).
generate(cat(X,Y),H,T) :- generate(X,H,T1), generate(Y,T1,T).
generate(star(X),T,T).
generate(star(X),H,T) :- generate(X,H,T1), generate(star(X),T1,T).

```

Partial deduction query:

```
generate(cat(star(or(char(a),char(b))),
         cat(char(a),cat(char(a),char(b)))),X1,[])

```

Specialised program:

```
generate__3([a|B],B).
generate__4([b|B],B).
generate__2(B,C) :- generate__3(B,C).
generate__2(D,E) :- generate__4(D,E).
generate__1(B,B).
generate__1(C,D) :- generate__2(C,E), generate__1(E,D).
generate__6(B,C) :- generate__3(B,D), generate__4(D,C).
generate__5(B,C) :- generate__3(B,D), generate__6(D,C).
generate__0(B,C) :- generate__1(B,D), generate__5(D,C).

```


format: text

text:
# Do shifting Bragg peaks of cuprate stripes reveal fractionally charged kinks ?

thanks:  J. Zaanen acknowledges the hospitality of the Institute of Theoretical Physics at the University of California, Santa Barbara where part of this work was done. This research was supported in part by the National Science Foundation under Grant No. PHY94-07194.

## Abstract

The stripe phases found in correlated oxides can be viewed as an ordering of the solitons associated with doping the Mott-insulating state. Inspired by the recent observation that the stripes tilt away from the main axis of the crystal lattice in the regime $`x1/8`$, we propose that a new type of stripe phase is realized in the large doping regime. This new phase should be viewed as a doped version of the microscopically insulating $`x1/8`$ stripes. The topological excitations associated with the extra doping are fractionally charged kinks along the stripes whose motions make the stripe fluctuate. We argue that the directional degree of freedom of the kinks might order, causing the stripe phase to tilt. Quantitative predictions follow for the doping dependence of the tilt angle, which in turn can be used to determine the fundamental charge quantum associated with the stripe phase.

In the last few years, overwhelming experimental evidence has accumulated that the holes in the cuprate materials, such as the high $`T_c`$ superconductors, form various types of striped phases tranquadaover ; sciencerep ; scienceper . The building blocks of such phases consist of domain walls which can be viewed as string-like configurations of holes that separate hole-free antiferromagnetic domains. Important information about the microscopic origin of stripes is contained in the doping dependence of the inverse of the stripe spacing, shown in Fig. 1A. This spacing can be obtained directly from the the distance $`\delta `$ between the measured Bragg-peaks (Fig. 1B). It was experimentally found that $`\delta `$ is to a good approximation directly proportional to doping $`x`$ for a variety of stripe systems like the nickelates Nickelates  and manganites Manganites . It is also found in cuprate stripe phases, but only in the doping regime where $`x1/8`$, while for $`x1/8`$, $`\delta `$ becomes roughly $`x`$ independent — see Fig. 1A Yamadaplot ; Uchida . In the regime $`x<0.05`$, the stripes become diagonal Wakimoto . Quite recently it was found Matsushita ; Lee ; Kimura  that in a number of cuprates the spin peaks tilt away from the $`(1,0)`$ or $`(0,1)`$ axis in reciprocal space. This puzzling behavior corresponds with a tilt of the stripe phase away from the main crystal axis of the perovskite planes in real space and seems characteristic for the $`x1/8`$ regime. We want to suggest here that this tilt might reflect the presence of fractionally charged solitons living on the stripes. This notion leads to an explicit relation between the $`\delta `$ versus $`x`$ dependence and the $`Y`$-shift, which, if confirmed experimentally, allows one to determine the topological charge of stripes.

The $`x1/8`$ stripes might be viewed as the condensation of the topological defects associated with doping the half-filled Mott-insulator ZaGu ; SteveK ; Pryadko  (see Fig. 2A). We here suggest that the $`x1/8`$ state should be viewed in turn as the condensation of the topological defects associated with doping the stripe state itself. This state is as indicated in Fig. 2B. The stripes for $`x1/8`$ are locally not different from the $`x1/8`$ stripes sketched in Fig. 2A, except that once in a while the stripe ‘steps sideways’: it forms kinks. These kinks carry half the fundamental charge quantum associated with the stripe-insulator of the $`x1/8`$ regime and as they move a stripe always in the same direction they cause the orientation of the stripe phase to deviate from the lattice axis, explaining the Y-shift. Although not based on phase separation between two different types of stripe fillings, our proposal shares the essential idea, that the crossover around $`x=1/8`$ and the charge density and orientation of stripes are related, with a suggestion of White and Scalapino WhiteScal .

Our central assumption is that the cuprate stripe phase in the $`x1/8`$ regime is insulating on the microscopic scale. Experimentally, the cuprate stripe phases are metallic-like and a popular viewpoint is that the electronic state on the stripes is metallic. However, the $`\delta =Sx`$ relation, where $`S`$ is the linear slope in the small $`x`$ limit, argues strongly against this internal metallicity. Its meaning, already suggested by earlier mean field calculations, is simply that every hole stabilizes a piece of charged stripe with a length which is an integer multiple of the lattice constant. This special stability when the electron charge and the lattice are commensurate, shows that the internal electronic state of a stripe is insulating on short length scales. At the same time, stripes which are internally insulating on microscopic scales are not necessarily inconsistent with metallic behavior on macroscopic scales. The stripe metal might correspond with a quantum-disordered stripe insulator, characterized by a growth of the quantum fluctuations when length- and time scales are increasing. Although we will not address this issue in any further detail, the remainder should be read as a suggestion for a critical experimental test of this hypothesis.

We follow the literature with regard to the nature of the reference insulator in the $`x1/8`$ regime WiNa ; ZaOl . The slope $`S`$ of the $`\delta `$ versus $`x`$ relationship for small $`x`$ implies that one hole stabilizes two charge stripe unit cells. Accordingly, the dynamics associated with the electrons along the stripe can be associated with that of a quarter filled one-dimensional fermion system ZXShen . It is well known that such a system can become Mott-insulating by breaking translational symmetry with real space charge periods $`2a`$ and $`4a`$, or wavevectors $`4k_F`$ and $`2k_F`$ respectively, where $`k_F=\pi /(4a)`$ ($`a`$ is the lattice constant). Schematically, the ordering pattern on the stripe is like $`\mathrm{}00\mathrm{}`$ and $`\mathrm{}0000\mathrm{}`$ for the $`4k_F`$ and $`2k_F`$ stripes, respectively. Here $`0`$ denotes the hole and $``$ the presence of a spin, which we expect to be disordered due to quantum fluctuations. At present it is not known which type of density wave order is realized on the stripe. All that really matters for the remainder of our discussion is that the $`4k_F`$ stripe should be considered as the condensation of the charge $`e`$ of one hole WiNa , while the $`2k_F`$ stripe is associated with the charge quantum of a pair of holes, $`2e`$ ZaOl .

Let us now turn to the $`x1/8`$ regime. The (near) independence of $`\delta (x)`$ as function of doping $`x`$ implies that a fraction of the holes $`x^{}=x\delta (x)/Sx1/8`$ cannot be ‘absorbed’ by the $`x1/8`$ insulator. These excess holes should dope the $`x1/8`$ state and it is expected that these holes dope the ‘soft’ insulator associated with the density wave on the charge stripes instead of the magnetic domains, the remnants of the ‘hard’ insulator of half-filling. Doped charge density wave states are well understood in the context of conventional 1D systems Haldane . A key concept was introduced by Schrieffer Schrieffer  in the study of polyacetyleen: the elementary excitations in such a system are not electrons but in fact parts of an electron. The reason is that these excitations can be viewed as electrons bound to topological defects in the density wave order parameter. That the charge of the electron fractionalizes in doped $`4k_F`$ density wave systems is easily seen by considering the strong coupling limit ZaOsvS . The undoped state with one (static) hole added at the central site is indicated in Fig. 3A. After a couple of hops a configuration is reached where the bare hole has decayed into two propagating excitations carrying half the hole charge ($`e/2`$) which are at the same time domain walls (kinks) in the density wave (Fig. 3B). Such an $`e/2`$ domain wall corresponds with a region of enhanced charge density, and hence an increased Coulomb energy. In contrast to a one-dimensional crystal, a stripe has the additional freedom of moving sidewards, thereby increasing the distance between the two holes associated with the domain wall ZaOsvS , as sketched in Fig. 3C. Thus, the fractionally charged domain walls also cause the stripe to step sidewards, modulating the position of the stripes in space, see Fig. 3D. If all the kinks are in the same direction, the net result is that the stripe takes on average an orientation in space which is tilted away from the lattice axis, very much like slanted phases that are found in lattice string models eskes .

Let us now consider a dense system of such ‘slanted’ stripes. In the presence of any stripe-stripe interaction this will condense at zero temperature in a stripe phase where all the stripes are tilted in the same direction: our explanation for the Y-shift. It is also expected that the kinks themselves order in a regular pattern at zero temperature. The argument is the usual one: the kink gas on a single stripe becomes at long wavelength a Luttinger liquid showing algebraic long range order. In the presence of any interaction between the Luttinger liquids on different stripes this will change into true long range order at zero temperature LiqCr .

The above considerations do not depend on the type of stripe density wave order, except that the charge $`q`$ of the kinks is different. How should the charge of the kinks be counted for $`2k_F`$ parent stripes? The rule is that the charge of the soliton is half the charge quantum associated with the parent. Since the $`2k_F`$ stripes can be considered as condensations of pairs of electrons, the charge associated with a charged kink in the $`2k_F`$ stripe becomes one electron charge. In terms of the strong coupling cartoon of Fig. 3, one should now associate two sites of the real lattice with one site in the lattice of Fig. 3C, so that Fig. 3D can be mapped back to the $`2k_F`$ case by inserting the doubled lattice and the doubled charges.

These general ideas can be illustrated with explicit calculations. Since we are considering fully ordered insulating states, mean-field theory is able to provide meaningful qualitative outcomes. The reference $`2k_F`$ and $`4k_F`$ stripe insulators actually both exist in the Hartree-Fock solutions of the Hubbard model as low lying, but weakly metastable states: the true mean-field ground state corresponds with filled stripes (1 hole per stripe unit cell) ZaOl ; Seibold . In Fig. 2D we show a typical example of a straight bond centred $`2k_F`$ stripe, calculated with the mean-field approximation, which strongly resembles the stripe patterns found in the density matrix renormalization group calculations by White and Scalapino for the $`tJ`$ model WhiteScalDMRG .

By constraining the distance between the stripes to be fixed, increasing the hole density and using appropriate boundary conditions, doped stripes can also be investigated in mean-field theory. We find that such doped stripes, if they exist as locally stable mean-field solutions, prefer localized fractionally charged kinks. A typical example is shown in Fig. 2B where the density of excess holes is indicated for a $`4k_F`$ stripe state at a hole density of $`x=0.139`$. In line with the qualitative arguments given above, every hole doped into the $`4k_F`$ $`x=1/8`$ reference insulator gives rise to two kinks, each carrying a charge of $`e/2`$ and moving the stripe sideways by one lattice constant. Although these ‘slanted’ stripes are quite stable solutions if the reference insulator is of the $`4k_F`$ variety, we did not manage to find stable solutions for the $`2k_F`$ stripes doped with additional holes — within mean field theory, such kinks tend to disintegrate.

In order to get some feeling of the relative stability of the $`4k_F`$ slanted phase we compared it with a straight stripe where an additional hole is simply inserted in the straight density wave ($`\mathrm{}000\mathrm{}`$). On the Hartree-Fock level, a stripe with two kinks of charge $`e/2`$ always has significantly lower energy (of order 0.01 $`t`$). We also checked that the sidesteps can be further stabilized by including a nearest-neighbour Coulomb interaction. The energetics associated with the relative transversal orientation of the kinks is a more delicate matter which will strongly depend on the distance between kinks. We believe that collective fluctuation effects will promote long range slanted order over zig-zag type stripe patterns, in much the same way as quantum fluctuations make lattice strings directed eskes .

Of course, our calculations merely serve to illustrate the principle — neither the question which possibility is realized in nature nor the question whether the ‘topological’ insulator is the proper reference state can be settled by these calculations. However, simple predictions follow which at least in principle can be checked by experiment. Most importantly, the charged kinks offer an explanation for the Y-shift which has already been observed in experiments. However, the kink notion implies that the superlattice peaks of the slanted stripe phase are located along the straight lines crossing the superlattice peaks associated with the $`1/8`$ phase as indicated in Fig. 1C. The reason is that the average distance between the stripes does not change when the stripes are making sidesteps, thereby leaving the distance between the peaks in reciprocal space along the horizontal axis in Fig. 1C unchanged.

Lattice commensuration effects make a transition to kinked stripes around $`x=1/8`$ most likely. However, due to complications associated with quenched disorder we have no prediction for whether there should be a sharp transition or a rapid but smooth cross-over. However, the scenario that there are no free holes, but that instead all holes go onto stripes, leads to an immediate relation between the $`\delta (x)`$ dependence and the $`Y`$-shift. Let us define the magnitude of the $`Y`$-shift as $`\delta k`$ and the fractional charge (in units of $`e`$) carried by the kink as $`q`$. Then $`x^{}=x\delta (x)/Sx1/8`$ is the hole density associated with doping the stripes in the $`x1/8`$ regime. It can be shown that the Y-shift obeys $`\delta k=\frac{x^{}}{2q}\frac{2\pi }{a}`$ and that $`\delta =(xx^{})\frac{2\pi }{a}`$ where $`a`$ is the lattice constant. So we have $`\delta +2q\delta k=\frac{2\pi }{a}x`$, independent of whether there is a crossover or sharp transition, and where it takes place. In Fig. 1D we show our prediction for the Y-shift as function of $`x`$ for the $`2k_F`$ and $`4k_F`$ cases, both for the case of a sharp transition at $`\frac{1}{8}`$ and for the same smooth crossover as in Fig. 1A. We have also indicated in this figure two experimental results for the Y-shift, where the $`x=0.15`$ point has been reported by Lee et al. Lee  for an oxygen doped sample of $`La_2CuO_4`$ and the $`x=0.13`$ point is measured in a $`La_{2x}Sr_xCuO_4`$ sample by Matsushita et al. Matsushita . There is also one experimental indication of a Y-shift at dopings slightly less than 1/8 by Kimura et al. Kimura , which suggests that there is a smooth crossover. Clearly an extensive experimental study is called for to establish whether the Y-shift is due to kinks and whether our relationship between $`\delta k`$ and $`\delta (x)`$ holds. The existing data seem to favour a kink charge of $`e`$ over charge $`e/2`$, suggesting that the elementary charge quantum associated with the stripe phase is $`2e`$. Given the proximity of a superconductor characterised by charge quantum $`2e`$, such a stripe charge-quantisation would obviously be quite interesting footnote2 .

We argued that the charged kinks themselves should order. It should therefore in principle be possible to observe the superlattice reflections of this kink lattice in diffraction experiments. As we argued, the kinks on single stripes will repel but the kink order from stripe to stripe is less easy to establish. On the one hand, the kinks carry charge and under the assumption that the screening length is of order or larger than the average kink separation the kinks would tend to maintain a maximum separation, thereby forming a Wigner crystal as indicated in Fig. 2C. However, one could imagine that elastic deformation energies are minimised when kinks line up as indicated in Fig. 2B. The precise realization of the kink superlattice is therefore a subtle, quantitative matter. Observation of this kink superlattice may be a formidable experimental challenge. However, given the conceptual implications implied by such an observation it should be given a high priority.

In conclusion, inspired by the tilting of the stripes seen at higher dopings we have proposed a scenario of stripe phases characterized by a proliferation of fractionally charged solitons. Remarkably, by studying merely the structural characteristics of this phase which is realized at higher dopings, the elementary charge quantum numbers of the stripes can be established. This is undoubtedly a crucial piece of information in the quest for the understanding of high $`T_c`$ superconductivity WiNa .