text:
# A Generalization of the Lifting Lemma for Logic Programming

## Contents

1. Introduction
2. Preliminaries
3. Neutral Arguments for SLD-Derivation

1. Filters
    2. Derivation Neutral Filters: Operational Definition
    3. Model Theoretic Results Induced by DN Filters
4. Some Particular DN Filters

1. DN Sets of Positions
    2. DN Sets of Positions with Associated Terms
5. Atomic Queries with Infinite Derivations
6. Related Works
7. Conclusion
8. Bibliography
9. Proofs

## 1 Introduction

Since the seminal work of J. A. Robinson on resolution , many lifting lemmas have been proposed in the literature, see for instance  p. 84,  p. 848,  p. 47,  p. 60 or  where a stronger version than that of  is given. Lifting results are used as a tool to simplify proofs of completeness of resolution.

In this paper, we are interested in generalizing the lifting lemma presented in  where it is called the Lifting Theorem. Given a logic program $`P`$, our aim is the further design of a mechanism that generates *at compile-time* classes of queries that have an infinite SLD-derivation w.r.t. $`P`$. Towards this end, we propose a criterion in the form of a sufficient condition that enables us to identify infinite derivations.

Notice that such a condition can be easily designed from the Lifting Theorem that is proposed by Apt in , as we explain now. Assuming that the reader is familiar with the standard notations about logic programming reviewed in the next section, let us first recall the notion of a lift. An SLD-derivation $`\xi ^{}`$ is a *lift* of another SLD-derivation $`\xi `$ if there exists a prefix $`D`$ of $`\xi ^{}`$ that is more general than $`\xi `$ *i.e.* $`D`$ is of the same length than $`\xi `$ and in $`D`$ and $`\xi `$ the same clauses are used in the same order, atoms in the same positions are selected at each step and for each $`i`$, the $`i`$-th query of $`D`$ is more general than that of $`\xi `$. The following result holds.

###### Theorem 1.1 (Lifting )

Let $`P`$ be a logic program, $`Q`$ be a query and $`\eta `$ be a substitution. For every SLD-derivation $`\xi `$ of $`P\{Q\eta \}`$, there exists an SLD-derivation of $`P\{Q\}`$ which is a lift of $`\xi `$.

This theorem provides a sufficient condition that can be used to identify infinite SLD-derivations.

###### Corollary 1

Let $`P`$ be a logic program and $`A`$ be an atom. Suppose that there exists a sequence of SLD-derivation steps from $`A`$ to a query $`Q`$ using the clauses of $`P`$ and that $`Q`$ contains an atom $`B`$ that is more general than $`A`$. Then there exists an infinite SLD-derivation of $`P\{A\}`$.

###### Proof

Let $`A\underset{P}{\overset{+}{}}Q`$ denote that there exists a sequence of SLD-derivation steps from $`A`$ to $`Q`$ using the clauses of $`P`$. As $`B`$ is more general than $`A`$, by the Lifting Theorem 1.1 we have $`B\underset{P}{\overset{+}{}}Q_1`$ where $`Q_1`$ is a query that is more general than $`Q`$. So there exists $`B_1`$ in $`Q_1`$ that is more general than $`B`$. Iterating this process, we construct an infinite sequence of queries $`Q_1`$, $`Q_2`$, …and an infinite sequence of atoms $`B_1`$, $`B_2`$, …such that for $`i1`$, $`B_i`$ is in $`Q_i`$ and $`B_i\underset{P}{\overset{+}{}}Q_{i+1}`$. ∎

Nevertheless, such a condition is rather weak because it fails at identifying some simple loops. This is illustrated by the following example.

###### Example 1

Let $`c`$ be the clause $`p(x,y)p(f(x),z)`$. Then from the head of $`c`$ we get an SLD-derivation step $`p(x,y)\underset{c}{}p(f(x_1),z_1)`$. Since the atom $`p(f(x_1),z_1)`$ is not more general than $`p(x,y)`$, Corollary 1 cannot be used. Moreover,

$$p(f(x_1),z_1)\underset{c}{}p(f(f(x_2)),z_2)\underset{c}{}p(f(f(f(x_3))),z_3)\mathrm{}$$

As the first argument of $`p`$ grows from step to step, we will never be able to use Corollary 1 to show that there exists an infinite SLD-derivation of $`\{c\}\{p(x,y)\}`$. ∎

In this article, we extend the relation “is more general than” so that it takes into account only some arguments of the atoms, the others (which are called *neutral arguments*) being, roughly, disregarded. We show that the Lifting Theorem 1.1, and hence Corollary 1, can be extended to this new relation. Neutral arguments correspond to the following intuition. Suppose we have an SLD-derivation $`\xi `$ of a query $`Q`$ w.r.t. a logic program $`P`$. Let $`Q^{}`$ be the query obtained by replacing the neutral arguments of the atoms of $`Q`$ by any term. Then, there exists an SLD-derivation $`\xi ^{}`$ of $`Q^{}`$ w.r.t. $`P`$ such that $`\xi ^{}`$ is a lift of $`\xi `$ up to the neutral arguments.

###### Example 2

Consider Example 1 again. For any derivation step $`p(s_1,s_2)`$ $`\underset{c}{}p(s_3,s_4)`$ if we replace $`s_1`$ by any term $`t_1`$ then there exists a derivation step $`p(t_1,s_2)\underset{c}{}p(t_3,t_4)`$. Moreover, notice that $`s_4`$ and $`t_4`$ are variables, so $`p(t_3,t_4)`$ is more general than $`p(s_3,s_4)`$ up to the first argument of $`p`$. Consequently, by the intuition described above, the first argument of $`p`$ is neutral for derivation w.r.t. $`c`$. Finally, as $`p(x,y)\underset{c}{}p(f(x_1),z_1)`$ and $`p(f(x_1),z_1)`$ is more general than $`p(x,y)`$ up to the first argument which is neutral, by the extended version of Corollary 1 there exists an infinite SLD-derivation of the query $`p(x,y)`$ w.r.t. $`c`$. ∎

Last but not least, we offer two syntactic conditions of increasing power for easily identifying neutral arguments from mere inspection of the text of a logic program.

The paper is organized as follows. In Section 2, we review basic concepts concerning logic programming and introduce some notations. Then in Section 3 we give a generic presentation of what we mean for an argument to be neutral. In Section 4, we propose some particular concrete means for detecting neutral arguments. In Section 5, we apply our results to generate some queries that have an infinite SLD-derivation w.r.t. a given logic program. Finally, in Section 6 we discuss related works.

## 2 Preliminaries

We try to strictly adhere to the notations, definitions, and results presented in .

$`N`$ denotes the set of non-negative integers and for any $`nN`$, $`[1,n]`$ denotes the set $`\{1,\mathrm{},n\}`$. If $`n=0`$ then $`[1,n]=\mathrm{}`$.

From now on, we fix a language $``$ of programs. We assume that $``$ contains an infinite number of constant symbols. The set of relation symbols of $``$ is $`\mathrm{\Pi }`$, and we assume that each relation symbol $`p`$ has an *unique* arity, denoted $`arity(p)`$. $`TU_{}`$ (resp. $`TB_{}`$) denotes the set of all (ground and non ground) terms of $``$ (resp. atoms of $``$). A *query* is a finite sequence of atoms $`A_1,\mathrm{},A_n`$ (where $`n0`$). Queries are denoted by $`Q`$, $`Q^{}`$, … or by bold upper-case letters A, B, …

Let $`t`$ be a term. Then $`Var(t)`$ denotes the set of variables occurring in $`t`$. This notation is extended to atoms, queries and clauses. Let $`\theta :=\{x_1/t_1,\mathrm{},x_n/t_n\}`$ be a substitution. We denote by $`Dom(\theta )`$ the set of variables $`\{x_1,\mathrm{},x_n\}`$, and by $`Ran(\theta )`$ the set of variables appearing in $`t_1,\mathrm{},t_n`$. We define $`Var(\theta )=Dom(\theta )Ran(\theta )`$. Given a set of variables $`V`$, $`\theta |V`$ denotes the substitution obtained from $`\theta `$ by restricting its domain to $`V`$.

Let $`t`$ be a term and $`\theta `$ be a substitution. Then, the term $`t\theta `$ is called an *instance* of $`t`$. If $`\theta `$ is a *renaming* (*i.e.* a substitution that is a 1-1 and onto mapping from its domain to itself), then $`t\theta `$ is called a *variant* of $`t`$. Finally, $`t`$ is called *more general than $`t^{}`$* if $`t^{}`$ is an instance of $`t`$.

A *logic program* is a finite set of definite clauses. In program examples, we use the ISO-Prolog syntax. Let $`P`$ be a logic program. Then $`\mathrm{\Pi }_P`$ denotes the set of relation symbols appearing in $`P`$. Consider a non-empty query $`\text{A},B,\text{C}`$ and a clause $`c`$. Let $`H𝐁`$ be a variant of $`c`$ variable disjoint with $`\text{A},B,\text{C}`$ and assume that $`B`$ and $`H`$ unify. Let $`\theta `$ be an mgu of $`B`$ and $`H`$. Then $`\text{A},B,\text{C}\underset{c}{\overset{\theta }{}}(\text{A},𝐁,\text{C})\theta `$ is an *SLD-derivation step* with $`H𝐁`$ as its *input clause* and $`B`$ as its *selected atom*. If the substitution $`\theta `$ or the clause $`c`$ is irrelevant, we drop a reference to it.

Let $`Q_0`$ be a query. A maximal sequence $`Q_0\underset{c_1}{\overset{\theta _1}{}}Q_1\underset{c_2}{\overset{\theta _2}{}}\mathrm{}`$ of SLD-derivation steps is called an *SLD-derivation* of $`P\{Q_0\}`$ if $`c_1`$, $`c_2`$, …are clauses of $`P`$ and if the *standardization apart* condition holds, *i.e.*: each input clause used is variable disjoint from the initial query $`Q_0`$ and from the mgu’s and input clauses used at earlier steps. A finite SLD-derivation may end up either with the empty query (then it is a *successful* SLD-derivation) or with a non-empty query (then it is a *failed* SLD-derivation). We say $`Q_0`$ *loops* with respect to $`P`$ if there exists an infinite SLD-derivation of $`P\{Q_0\}`$.

Finally, we write $`Q\underset{P}{\overset{}{}}Q^{}`$ (resp. $`Q\underset{P}{\overset{+}{}}Q^{}`$) if there exists a finite prefix (resp. a finite non-empty prefix) ending at $`Q^{}`$ of an SLD-derivation of $`P\{Q\}`$.

Let $`E`$ and $`F`$ be two sets. Then, $`f:EF`$ denotes that $`f`$ is a function from $`E`$ to $`F`$ and $`f:EF`$ denotes that $`f`$ is a mapping from $`E`$ to $`F`$. The *domain* of a function $`f`$ from $`E`$ to $`F`$ is denoted by $`Dom(f)`$ and is defined as: $`Dom(f)=\{x|xE,f(x)\text{ exists}\}`$. Thus, if $`f`$ is a mapping from $`E`$ to $`F`$, then $`Dom(f)=E`$.

## 3 Neutral Arguments for SLD-Derivation

The basic idea in the work we present here relies on some arguments in clauses which we can be disregarded when unfolding a query. For instance, the second argument of the non-unit clause of the program

```
    append([],Ys,Ys).
    append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).

```

is such a candidate. Notice that a very common programming technique called *accumulator passing* (see for instance e.g. , p. 21–25), always produces such patterns.

###### Example 3

A classical example of the accumulator passing technique is the following program REVERSE.

```
    reverse(L,R) :- rev(L,[],R).
    rev([],R,R).
    rev([X|Xs],R0,R) :- rev(Xs,[X|R0],R).

```

Concerning termination, we may ignore the third *and* the second argument of the recursive clause of rev while unfolding a query with this clause. Only the first argument can stop the unfolding. ∎

But we can be more precise. Instead of only identifying arguments that can be totaly disregarded as in the above examples, we can try to identify arguments that can be replaced, when unfolding a query, by any terms for which a given condition holds. Consider for instance the program

```
    p(x,f(z)) :- q(x,y), p(y,f(z)).

```

If we unfold a query $`p(t_1,t_2)`$ with this program, then if we replace the second argument of $`p`$ by any instance $`t_3`$ of $`f(z)`$, we can still unfold $`p(t_1,t_3)`$.

In the sequel of this section, we give a technical tool to describe specific arguments inside a program and present an extension of the relation “is more general than”. Then we formalize the concept of derivation neutrality and we propose an extended version of the Lifting Theorem 1.1.

### 3.1 Filters

Let us first introduce the notion of a *filter*. We use filters in order to distinguish atoms some arguments of which satisfy a given condition. A condition upon atom arguments, *i.e.* terms, can be defined as a mapping in the following way.

###### Definition 1 (Term-Condition)

A *term-condition* is a mapping from $`TU_{}`$ to $`\{\mathrm{𝚝𝚛𝚞𝚎},\mathrm{𝚏𝚊𝚕𝚜𝚎}\}`$.

###### Example 4

The following mappings are term-conditions.

$$\begin{array}{cccc}\hfill f_{\mathrm{𝑡𝑟𝑢𝑒}}:& TU_{}& & \{\text{true},\text{false}\}\hfill \\ & t& & \text{true}\hfill \\ \hfill f_1:& TU_{}& & \{\text{true},\text{false}\}\hfill \\ & t& & \text{true}\text{ iff }t\text{ is an instance of }[x|y]\hfill \\ \hfill f_2:& TU_{}& & \{\text{true},\text{false}\}\hfill \\ & t& & \text{true}\text{ iff }t\text{ unifies with }h(a,x)\hfill \end{array}$$

Now we can precise what we exactly mean by a filter.

###### Definition 2 (Filter)

A *filter*, denoted by $`\mathrm{\Delta }`$, is a mapping from $`\mathrm{\Pi }`$ such that: for each $`p\mathrm{\Pi }`$, $`\mathrm{\Delta }(p)`$ is a function from $`[1,arity(p)]`$ to the set of term-conditions.

###### Example 5 (Example 4 continued)

Let $`\mathrm{\Pi }:=\{p\}`$ with $`p`$ a relation symbol whose arity equals 3. Then, $`\mathrm{\Delta }:=p1f_{\mathrm{𝑡𝑟𝑢𝑒}},\mathrm{\hspace{0.33em}2}f_1`$ is a filter. ∎

Notice that, given a filter $`\mathrm{\Delta }`$, the relation “is more general than” can be extended in the following way: an atom $`A:=p(\mathrm{})`$ is $`\mathrm{\Delta }`$-more general than $`B:=p(\mathrm{})`$ if the “is more general than” requirement holds for those arguments of $`A`$ whose position is not in the domain of $`\mathrm{\Delta }(p)`$ while the other arguments satisfy their associated term-condition.

###### Definition 3 ($`\mathrm{\Delta }`$-More General)

Let $`\mathrm{\Delta }`$ be a filter, $`A`$ and $`B`$ be two atoms and $`Q:=A_1,\mathrm{},A_n`$ and $`Q^{}:=B_1,\mathrm{},B_m`$ be two queries.

* Let $`\eta `$ be a substitution. Then *$`A`$ is $`\mathrm{\Delta }`$-more general than $`B`$ for $`\eta `$* if:

$$\{\begin{array}{c}A=p(s_1,\mathrm{},s_n)\hfill \\ B=p(t_1,\mathrm{},t_n)\hfill \\ i[1,n]Dom(\mathrm{\Delta }(p)),t_i=s_i\eta \hfill \\ iDom(\mathrm{\Delta }(p)),\mathrm{\Delta }(p)(i)(s_i)=\mathrm{𝚝𝚛𝚞𝚎}.\hfill \end{array}$$
* *$`A`$ is $`\mathrm{\Delta }`$-more general than $`B`$* if there exists a substitution $`\eta `$ s.t. $`A`$ is $`\mathrm{\Delta }`$-more general than $`B`$ for $`\eta `$.
* Let $`\eta `$ be a substitution. Then *$`Q`$ is $`\mathrm{\Delta }`$-more general than $`Q^{}`$ for $`\eta `$* if:

$$\{\begin{array}{c}n=m\text{ and}\hfill \\ i[1,n],A_i\text{ is }\mathrm{\Delta }\text{-more general than }B_i\text{ for }\eta .\hfill \end{array}$$
* *$`Q`$ is $`\mathrm{\Delta }`$-more general than $`Q^{}`$* if there exists a substitution $`\eta `$ s.t. $`Q`$ is $`\mathrm{\Delta }`$-more general than $`Q^{}`$ for $`\eta `$.

###### Example 6

Let $`\mathrm{\Pi }:=\{p\}`$ and $`A:=p(b,x,h(a,x))`$, $`B:=p(a,[a|b],x)`$, $`C:=p(a,[a|b],h(y,b))`$.

* Consider the filter $`\mathrm{\Delta }`$ defined in Example 5. Then, $`A`$ is not $`\mathrm{\Delta }`$-more general than $`B`$ and $`C`$ because, for instance, its second argument $`x`$ is not an instance of $`[x|y]`$ as required by $`f_1`$. On the other hand, $`B`$ is $`\mathrm{\Delta }`$-more general than $`A`$ for the substitution $`\{x/h(a,x)\}`$ and $`B`$ is $`\mathrm{\Delta }`$-more general than $`C`$ for the substitution $`\{x/h(y,b)\}`$. Finally, $`C`$ is not $`\mathrm{\Delta }`$-more general than $`A`$ because $`h(y,b)`$ is not more general than $`h(a,x)`$ and $`C`$ is not $`\mathrm{\Delta }`$-more general than $`B`$ because $`h(y,b)`$ is not more general than $`x`$.
* Consider the term-conditions defined in Example 4. Let $`\mathrm{\Delta }^{}:=p1f_{\mathrm{𝑡𝑟𝑢𝑒}},\mathrm{\hspace{0.33em}2}f_1,\mathrm{\hspace{0.33em}3}f_2`$. Then, $`A`$ is not $`\mathrm{\Delta }^{}`$-more general than $`B`$ and $`C`$ for the same reason as above. On the other hand, $`B`$ is $`\mathrm{\Delta }^{}`$-more general than $`A`$ and $`C`$ for any substitution and $`C`$ is $`\mathrm{\Delta }^{}`$-more general than $`A`$ and $`B`$ for any substitution. ∎

The following proposition states an intuitive result:

###### Proposition 1

Let $`\mathrm{\Delta }`$ be a filter and $`Q`$ and $`Q^{}`$ be two queries. Then $`Q`$ is $`\mathrm{\Delta }`$-more general than $`Q^{}`$ if and only if there exists a substitution $`\eta `$ such that $`Var(\eta )Var(Q,Q^{})`$ and $`Q`$ is $`\mathrm{\Delta }`$-more general than $`Q^{}`$ for $`\eta `$.

###### Proof

The proof of this proposition is given in Appendix 1. ∎

### 3.2 Derivation Neutral Filters: Operational Definition

Before we give a precise definition of the kind of filters we are interested in, we review the notion of a *lift*. The definition we propose below is the same as that of  p. 57 up to the arguments whose position is distinguished by a filter.

###### Definition 4 ($`\mathrm{\Delta }`$-Lift)

Let $`\mathrm{\Delta }`$ be a filter. Consider a sequence of SLD-derivation steps

$$\xi :=Q_0\underset{c_1}{}Q_1\mathrm{}Q_n\underset{c_{n+1}}{}Q_{n+1}\mathrm{}$$

We say that the sequence of SLD-derivation steps

$$\xi ^{}:=Q_0^{}\underset{c_1}{}Q_1^{}\mathrm{}Q_n^{}\underset{c_{n+1}}{}Q_{n+1}^{}\mathrm{}$$

is a *$`\mathrm{\Delta }`$-lift* of $`\xi `$ if

* $`\xi `$ is of the same or smaller length than $`\xi ^{}`$,
* for each $`Q_i`$ in $`\xi `$, $`Q_i^{}`$ is $`\mathrm{\Delta }`$-more general than $`Q_i`$,
* for each $`Q_i`$ in $`\xi `$, in $`Q_i`$ and $`Q_i^{}`$ atoms in the same positions are selected.

In the sequel of this paper, we focus on “derivation neutral” filters. The name “derivation neutral” stems from the fact that in any derivation of a query $`Q`$, the arguments of $`Q`$ whose position is distinguished by such a filter can be safely replaced by any terms satisfying the associated term-condition. Such a replacement does not modify the derivation process.

###### Definition 5 (Derivation Neutral)

Let $`\mathrm{\Delta }`$ be a filter and $`c`$ be a clause. We say that *$`\mathrm{\Delta }`$ is DN for $`c`$* if

* for each SLD-derivation step $`Q\underset{c}{}Q_1`$,
* for each query $`Q^{}`$ that is $`\mathrm{\Delta }`$-more general than $`Q`$,

there exists a query $`Q_1^{}`$ such that $`Q^{}\underset{c}{}Q_1^{}`$ and $`Q^{}\underset{c}{}Q_1^{}`$ is a $`\mathrm{\Delta }`$-lift of $`Q\underset{c}{}Q_1`$.

This definition is extended to finite sets of clauses: *$`\mathrm{\Delta }`$ is DN for a logic program $`P`$* if it is DN for each clause of $`P`$.

###### Example 7

The following examples illustrate the above definitions.

* Consider the following program APPEND:

```
      append([],Xs,Xs).                              % C1
      append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).  % C2

```

Consider the term-condition $`f_{\mathrm{𝑡𝑟𝑢𝑒}}`$ defined in Example 4, the set of relation symbols $`\mathrm{\Pi }:=\{append\}`$ and the filter $`\mathrm{\Delta }:=append2f_{\mathrm{𝑡𝑟𝑢𝑒}}`$. Then, $`\mathrm{\Delta }`$ is DN for `C2`. However, $`\mathrm{\Delta }`$ is not DN for APPEND because it is not DN for `C1`.
* Consider the following program MERGE:

merge(\[X|Xs\],\[Y|Ys\],\[X|Zs\]) :- merge(Xs,\[Y|Ys\],Zs).

Consider the term-condition $`f_1`$ defined in Example 4, the set of relation symbols $`\mathrm{\Pi }:=\{merge\}`$ and the filter $`\mathrm{\Delta }:=merge2f_1`$. Then, $`\mathrm{\Delta }`$ is DN for MERGE. ∎

Repeatedly using this definition, we get an extended version of the Lifting Theorem 1.1.

###### Theorem 3.1 ($`\mathrm{\Delta }`$-Lifting)

Let $`P`$ be a logic program and $`\mathrm{\Delta }`$ be a DN filter for $`P`$. Let $`\xi `$ be an SLD-derivation of $`P\{Q_0\}`$ and $`Q_0^{}`$ be a query that is $`\mathrm{\Delta }`$-more general than $`Q_0`$.

Then there exists an SLD-derivation of $`P\{Q_0^{}\}`$ that is a $`\mathrm{\Delta }`$-lift of $`\xi `$.

###### Proof

If $`\xi `$ is infinite, we can construct a required SLD-derivation $`\xi ^{}`$ whose length is infinite by repeatedly using Definition 5.

Now if $`\xi `$ is of finite length, then

* either $`\xi `$ is successful: in this case, we can construct a required SLD-derivation $`\xi ^{}`$ of the same length than $`\xi `$ by repeatedly using Definition 5,
* either $`\xi `$ fails. Suppose that $`\xi :=Q_0\underset{c_1}{}Q_1\mathrm{}Q_n\underset{c_{n+1}}{}Q_{n+1}`$. Then, by repeatedly using Definition 5, we can construct a finite sequence of SLD-derivation steps

$$Q_0^{}\underset{c_1}{}Q_1^{}\mathrm{}Q_n^{}\underset{c_{n+1}}{}Q_{n+1}^{}$$

that is a $`\mathrm{\Delta }`$-lift of $`\xi `$. But as $`Q_{n+1}^{}`$ is $`\mathrm{\Delta }`$-more general than $`Q_{n+1}`$, this sequence may not be a maximal one, *i.e.* from $`Q_{n+1}^{}`$ and $`P`$, we may derive $`Q_{n+2}^{}`$ and so forth. Hence, in this case, there may exist an SLD-derivation of $`P\{Q_0^{}\}`$ that is a $`\mathrm{\Delta }`$-lift of $`\xi `$ but of longer length than $`\xi `$. ∎

### 3.3 Model Theoretic Results Induced by DN Filters

Lifting lemmas are used in the literature to prove completeness of SLD-resolution. Now that we have established an extended Lifting Theorem, it may be worth to investigate its consequences from the model theoretic point of view.

Let $`E`$ be an atom or a query and $`\mathrm{\Delta }`$ be a filter. Then one may “expand” the atoms occurring in $`E`$ by replacing every argument whose position is distinguished by $`\mathrm{\Delta }`$ by any term that satisfies the associated term-condition.

###### Definition 6 (Expansion of atoms and queries by a filter)

Let $`\mathrm{\Delta }`$ be a filter.

* Let $`A`$ be an atom. *The expansion of $`A`$ w.r.t. $`\mathrm{\Delta }`$*, denoted $`[A]^\mathrm{\Delta }`$, is the set defined as

$$[A]^\mathrm{\Delta }:=\{BTB_{}|B\text{ is }\mathrm{\Delta }\text{-more general than }A\text{ for }ϵ\}$$

where $`ϵ`$ denotes the empty substitution.
* Let $`Q:=A_1,\mathrm{},A_n`$ be a query. *The expansion of $`Q`$ w.r.t. $`\mathrm{\Delta }`$*, denoted $`[Q]^\mathrm{\Delta }`$, is the set defined as:

$$[Q]^\mathrm{\Delta }:=\{(B_1,\mathrm{},B_n)|B_1[A_1]^\mathrm{\Delta },\mathrm{},B_n[A_n]^\mathrm{\Delta }\}.$$

Term interpretations in the context of logic programming were introduced in  and further investigated in  and . A term interpretation for $``$ is identified with a (possibly empty) subset of the term base $`TB_{}`$. So, as for atoms, a term interpretation can be expanded by a set of positions.

###### Definition 7 (Expansion of term interpretations by a filter)

Let $`\mathrm{\Delta }`$ be a filter and $`I`$ be a term interpretation for $``$. Then $`[I]^\mathrm{\Delta }`$ is the term interpretation for $``$ defined as:

$$[I]^\mathrm{\Delta }:=\underset{AI}{}[A]^\mathrm{\Delta }.$$

For any logic program $`P`$, we denote by $`𝒞(P)`$ its least term model.

###### Theorem 3.2

Let $`P`$ be a logic program and $`\mathrm{\Delta }`$ be a DN filter for $`P`$. Then $`[𝒞(P)]^\mathrm{\Delta }=𝒞(P)`$.

###### Proof

The inclusion $`𝒞(P)[𝒞(P)]^\mathrm{\Delta }`$ is trivial so let us concentrate on the other one *i.e.* $`[𝒞(P)]^\mathrm{\Delta }𝒞(P)`$. Let $`A^{}[𝒞(P)]^\mathrm{\Delta }`$. Then there exists $`A𝒞(P)`$ such that $`A^{}[A]^\mathrm{\Delta }`$. A well known result states:

$$𝒞(P)=\{BTB_{}|\text{there exists a successful SLD-derivation of }B\}$$
(1)
Consequently, there exists a successful SLD-derivation of $`A`$. Therefore, by the $`\mathrm{\Delta }`$-Lifting Theorem 3.1, there exists a successful SLD-derivation of $`A^{}`$. So by (1) $`A^{}𝒞(P)`$. ∎

## 4 Some Particular DN Filters

In this section, we consider some instances of the definitions of Section 3.

### 4.1 DN Sets of Positions

The first instance we consider corresponds to filters whose associated term-conditions are all equal to $`f_{\mathrm{𝑡𝑟𝑢𝑒}}`$ (see Example 4.) Within such a context, as the term-conditions are fixed, each filter $`\mathrm{\Delta }`$ is uniquely determined by the domains of the functions $`\mathrm{\Delta }(p)`$ for $`p\mathrm{\Pi }`$. Hence the following definition.

###### Definition 8 (Set of Positions)

A *set of positions*, denoted by $`\tau `$, is a mapping from $`\mathrm{\Pi }`$ to $`2^N`$ such that: for each $`p\mathrm{\Pi }`$, $`\tau (p)`$ is a subset of $`[1,arity(p)]`$.

###### Example 8

Let $`\mathrm{\Pi }:=\{\mathrm{𝑎𝑝𝑝𝑒𝑛𝑑},\mathit{append3}\}`$ with $`\mathrm{𝑎𝑟𝑖𝑡𝑦}(\mathrm{𝑎𝑝𝑝𝑒𝑛𝑑})=3`$ and $`\mathrm{𝑎𝑟𝑖𝑡𝑦}(\mathit{append3})=4`$. Then

$$\tau :=\mathrm{𝑎𝑝𝑝𝑒𝑛𝑑}\{2\},\mathit{append3}\{2,3\}$$

is a set of positions. ∎

Not surprisingly, the filter that is generated by a set of positions is defined as follows.

###### Definition 9 (Associated Filter)

Let $`\tau `$ be a set of positions and $`f_{\mathrm{𝑡𝑟𝑢𝑒}}`$ be the term-condition defined in Example 4. The filter $`\mathrm{\Delta }[\tau ]`$ defined as:

$$\text{for each }p\mathrm{\Pi },\mathrm{\Delta }[\tau ](p)\text{ is the mapping from }\tau (p)\text{ to }\{f_{\mathrm{𝑡𝑟𝑢𝑒}}\}$$

is called *the filter associated to $`\tau `$*.

###### Example 9 (Example 8 continued)

The filter associated to $`\tau `$ is

$$\mathrm{\Delta }[\tau ]:=\mathrm{𝑎𝑝𝑝𝑒𝑛𝑑}2f_{\mathrm{𝑡𝑟𝑢𝑒}},\mathit{append3}2f_{\mathrm{𝑡𝑟𝑢𝑒}},\mathrm{\hspace{0.33em}3}f_{\mathrm{𝑡𝑟𝑢𝑒}}.$$

Now we define a particular kind of sets of positions. These are named after “DN” because, as stated by Theorem 4.1 below, they generate DN filters.

###### Definition 10 (DN Set of Positions)

Let $`\tau `$ be a set of positions. We say that *$`\tau `$ is DN for a clause* $`p(s_1,\mathrm{},s_n)`$ $`\text{B}`$ if:

$$i\tau (p),\{\begin{array}{c}s_i\text{ is a variable}\hfill \\ s_i\text{ occurs only once in }p(s_1,\mathrm{},s_n)\hfill \\ \text{for each }q(t_1,\mathrm{},t_m)\text{B}:\hfill \\ j[1,m],s_iVar(t_j)j\tau (q).\hfill \end{array}$$

A set of positions is *DN for a program $`P`$* if it is DN for each clause of $`P`$.

The intuition of Definition 10 is the following. If for instance we have a clause $`c:=p(x,y,f(z))p(g(y,z),x,z)`$ then in the first two positions of $`p`$ we can put any terms and get a derivation step w.r.t. $`c`$ because the first two arguments of the head of $`c`$ are variables that appear exactly once in the head. Moreover, $`x`$ and $`y`$ of the head reappear in the body but again only in the first two positions of $`p`$. So, if we have a derivation step $`p(s_1,s_2,s_3)\underset{c}{}p(t_1,t_2,t_3)`$, we can replace $`s_1`$ and $`s_2`$ by any terms $`s_1^{}`$ and $`s_2^{}`$ and get another derivation step $`p(s_1^{},s_2^{},s_3)\underset{c}{}p(t_1^{},t_2^{},t_3^{})`$ where $`t_3^{}`$ is the same as $`t_3`$ up to variable names.

###### Example 10 (Example 8 continued)

$`\tau `$ is DN for the following program:

```
  append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).
  append3(Xs,Ys,Zs,Ts) :- append(Xs,Ys,Us), append(Us,Zs,Ts).

```

DN sets of positions generate DN filters.

###### Theorem 4.1

Let $`\tau `$ be a DN set of positions for a logic program $`P`$. Then $`\mathrm{\Delta }[\tau ]`$ is DN for $`P`$.

###### Proof

See Lemma 4 and Theorem 4.2 further. ∎

Notice that the set of DN sets of positions of a logic program is not empty as stated by the following proposition.

###### Proposition 2

Let $`P`$ be a logic program. Then $`\tau _0:=p\mathrm{}|p\mathrm{\Pi }`$ is DN for $`P`$.

###### Proof

By Definition 10. ∎

Moreover, an atom $`A`$ is $`\mathrm{\Delta }[\tau _0]`$-more general than an atom $`B`$ iff $`A`$ is more general than $`B`$. So, in the context of the filter $`\mathrm{\Delta }[\tau _0]`$, the $`\mathrm{\Delta }`$-Lifting Theorem 3.1 is the same as the Lifting Theorem 1.1.

### 4.2 DN Sets of Positions with Associated Terms

Now we consider another instance of the definitions of Section 3. As we will see, it is more general than the previous one. It corresponds to filters whose associated term-conditions have all the form “is an instance of $`t`$” where $`t`$ is a term that uniquely determines the term-condition. Hence the following definition.

###### Definition 11 (Sets of Positions with Associated Terms)

A *set of positions with associated terms*, denoted by $`\tau ^+`$, is a mapping from $`\mathrm{\Pi }`$ such that: for each $`p\mathrm{\Pi }`$, $`\tau ^+(p)`$ is a function from $`[1,arity(p)]`$ to $`TU_{}`$.

###### Example 11

Let $`\mathrm{\Pi }:=\{p,q\}`$ where the arity of $`p`$ and $`q`$ is 2. Then,

$$\tau ^+:=p2x,q2g(x)$$

is a set of positions with associated terms. ∎

The filter that is generated by a set of positions with associated terms is defined as follows.

###### Definition 12 (Associated Filter)

Let $`\tau ^+`$ be a set of positions with associated terms. The *filter associated to $`\tau ^+`$*, denoted by $`\mathrm{\Delta }[\tau ^+]`$, is defined as: for each $`p\mathrm{\Pi }`$, $`\mathrm{\Delta }[\tau ^+](p)`$ is the mapping

$$\begin{array}{ccc}Dom(\tau ^+(p))& & \text{The set of term-conditions}\hfill \\ i& & \{\begin{array}{ccc}TU_{}& & \{\mathrm{𝚝𝚛𝚞𝚎},\mathrm{𝚏𝚊𝚕𝚜𝚎}\}\hfill \\ t& & \mathrm{𝚝𝚛𝚞𝚎}\text{ iff }t\text{ is an instance of }\tau ^+(p)(i)\hfill \end{array}\hfill \end{array}$$

###### Example 12 (Example 11 continued)

The filter associated to $`\tau ^+`$ is

$$\mathrm{\Delta }[\tau ^+]:=p2f_1,q2f_2\text{ where}$$

$$\begin{array}{cccc}\hfill f_1:& TU_{}& & \{\text{true},\text{false}\}\hfill \\ & t& & \text{true}\text{ iff }t\text{ is an instance of }x\hfill \\ \hfill f_2:& TU_{}& & \{\text{true},\text{false}\}\hfill \\ & t& & \text{true}\text{ iff }t\text{ is an instance of }g(x)\hfill \end{array}$$

As for sets of positions, we define a special kind of sets of positions with associated terms.

###### Definition 13 (DN Sets of Positions with Associated Terms)

Let $`\tau ^+`$ be a set of positions with associated terms. We say that $`\tau ^+`$ is *DN for a clause* $`p(s_1,\mathrm{},s_n)\text{B}`$ if these conditions hold:

* (DN1) $`iDom(\tau ^+(p))`$, $`j[1,n]\{i\}`$: $`Var(s_i)Var(s_j)=\mathrm{}`$,
* (DN2) $`iu_i\tau ^+(p)`$: $`s_i`$ is more general than $`u_i`$,
* (DN3) $`iDom(\tau ^+(p))`$, $`q(t_1,\mathrm{},t_m)\text{B}`$, $`jDom(\tau ^+(q))`$: $`Var(s_i)Var(t_j)=\mathrm{},`$
* (DN4) $`q(t_1,\mathrm{},t_m)\text{B}`$, $`ju_j\tau ^+(q)`$: $`t_j`$ is an instance of $`u_j`$.

A set of positions with associated terms is *DN for a program $`P`$* if it is DN for each clause of $`P`$.

This definition says that any $`s_i`$ where $`i`$ is in the domain of $`\tau ^+(p)`$ (*i.e.* position $`i`$ is distinguished by $`\tau ^+`$): (DN1) does not share its variables with the other arguments of the head, (DN2) is more general than the term $`u_i`$ that $`i`$ is mapped to by $`\tau ^+(p)`$, (DN3) distributes its variables to some arguments $`t_j`$ of some atoms $`q(t_1,\mathrm{},t_m)`$ in B such that $`j`$ is in the domain of $`\tau ^+(q)`$ (*i.e.* position $`j`$ is distinguished by $`\tau ^+`$). Moreover, (DN4) says that any argument $`t_j`$, where $`j`$ is distinguished by $`\tau ^+`$, of any atom $`q(t_1,\mathrm{},t_m)`$ in B is such that $`t_j`$ is an instance of the term $`u_j`$ that $`j`$ is mapped to by $`\tau ^+(q)`$.

###### Example 13 (Example 11 continued)

$`\tau ^+`$ is DN for the following program:

```
    p(f(x),y) :- q(x,g(x)), p(x,g(y))
    q(a,g(x)) :- q(a,g(b))

```

The preceding notion is closed under renaming:

###### Proposition 3

Let $`c`$ be a clause and $`\tau ^+`$ be a set of positions with associated terms that is DN for $`c`$. Then $`\tau ^+`$ is DN for every variant of $`c`$.

###### Proof

The proof of this proposition is given in Appendix 1. ∎

Notice that a set of positions is a particular set of positions with associated terms in the following sense.

###### Proposition 4

Let $`\tau `$ be a set of positions and $`x`$ be any variable. Let $`\tau ^+`$ be the set of positions with associated terms defined as: for each $`p\mathrm{\Pi }`$, $`\tau ^+(p):=(\tau (p)\{x\})`$. Then, the following holds.

1. An atom $`A`$ is $`\mathrm{\Delta }[\tau ]`$-more general than an atom $`B`$ iff $`A`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`B`$.
2. For any clause $`c`$, $`\tau `$ is DN for $`c`$ iff $`\tau ^+`$ is DN for $`c`$.

###### Proof

The proof follows from these remarks.

* Item 1 is a direct consequence of the definition of “$`\mathrm{\Delta }`$-more general” (see Definition 3) and the definition of the filter associated to a set of positions (see Definition 9) and to a set of positions with associated terms (see Definition 12).
* Item 2 is a direct consequence of the definition of DN sets of positions (see Definition 10), and DN sets of positions with associated terms (see Definition 13). ∎

Finally, the sets of positions with associated terms of Definition 13 were named after “DN” because of the following result.

###### Theorem 4.2

Let $`P`$ be a logic program and $`\tau ^+`$ be a set of positions with associated terms that is DN for $`P`$. Then $`\mathrm{\Delta }[\tau ^+]`$ is DN for $`P`$.

###### Proof

The proof of this theorem is given in Appendix 2. ∎

For each predicate symbol $`p`$, let $`\varphi _p`$ be the function from $`[1,\mathrm{𝑎𝑟𝑖𝑡𝑦}(p)]`$ to $`TU_{}`$ whose domain is empty. As in the case of sets of positions, the set of DN sets of positions with associated terms of a logic program is not empty as stated by the following proposition.

###### Proposition 5

Let $`P`$ be a logic program. Then $`\tau _0^+:=p\varphi _p|p\mathrm{\Pi }`$ is DN for $`P`$.

###### Proof

By Definition 13. ∎

Moreover, an atom $`A`$ is $`\mathrm{\Delta }[\tau _0^+]`$-more general than an atom $`B`$ iff $`A`$ is more general than $`B`$. So, in the context of the filter $`\mathrm{\Delta }[\tau _0^+]`$, the $`\mathrm{\Delta }`$-Lifting Theorem 3.1 is the same as the Lifting Theorem 1.1.

## 5 Examples

In this section, we focus on *left derivations* *i.e.* we only consider the leftmost selection rule: $`QQ^{}`$ is a *left derivation step* if it is an SLD-derivation step whose selected atom is the first atom of $`Q`$ from the left. We say that *a query $`Q`$ left loops w.r.t. a program $`P`$* if there exists an infinite left derivation of $`P\{Q\}`$. Notice that the $`\mathrm{\Delta }`$-Lifting Theorem 3.1 provides a sufficient condition to identify left loops as it generates the following corollary.

###### Corollary 2 (from Theorem 3.1)

Let $`P`$ be a logic program and $`\mathrm{\Delta }`$ be a DN filter for $`P`$. If $`A\underset{P}{\overset{}{}}B_1,\text{B}_1`$ and $`B_1\underset{P}{\overset{+}{}}B_2,\text{B}_2`$ and $`B_2`$ is $`\mathrm{\Delta }`$-more general than $`B_1`$ then $`P\{A\}`$ left loops.

###### Proof

The proof is similar to that of Corollary 1.

This section presents some examples of atomic queries that have an infinite left derivation w.r.t. a given logic program. We use Corollary 2 with DN sets of positions and DN sets of positions with associated terms. In each case, it is not possible to conclude using the classical Lifting Theorem 1.1. The last example exhibits a case where we are not able conclude.

###### Example 14

Let $`\mathrm{\Pi }:=\{p\}`$ with $`p`$ a relation symbol whose arity equals 2 and let

$$c:=p(f(x),y)p(x,g(y)).$$

Then

$$\tau :=p\{2\}$$

is a DN set of positions for $`c`$. The filter associated to $`\tau `$ (see Definition 9) is

$$\mathrm{\Delta }[\tau ]:=p2f_{\mathrm{𝑡𝑟𝑢𝑒}}.$$

Notice that, by Theorem 4.1,

$$\mathrm{\Delta }[\tau ]\text{ is DN for }\{c\}.$$

Moreover, from the head $`p(f(x),y)`$ of $`c`$ we get

$$p(f(x),y)\underset{c}{}p(x^{},g(y^{})).$$

Applying Corollary 2, as $`p(x^{},g(y^{}))`$ is $`\mathrm{\Delta }[\tau ]`$-more general than $`p(f(x),y)`$, we get that

$$p(f(x),y)\text{ left loops w.r.t. }\{c\}.$$

We point out that we do not get this result from the classical Lifting Theorem 1.1 as $`p(x^{},g(y^{}))`$ is not more general than $`p(f(x),y)`$.

By the $`\mathrm{\Delta }`$-Lifting Theorem 3.1, we can also conclude that each query that is $`\mathrm{\Delta }[\tau ]`$-more general than $`p(f(x),y)`$ also left loops w.r.t. $`\{c\}`$. This means that each query of form $`p(t_1,t_2)`$ where $`t_1`$ is a term that is more general than $`f(x)`$ and $`t_2`$ is *any term* (because $`\tau (p)=\{2\}`$) left loops w.r.t. $`\{c\}`$. ∎

###### Example 15

Let $`\mathrm{\Pi }:=\{p\}`$ with $`p`$ a relation symbol whose arity equals 2 and let

$$c:=p(f(x),g(y))p(x,g(h(y))).$$

Notice that from the head $`p(f(x),g(y))`$ of $`c`$ we get

$$p(f(x),g(y))\underset{c}{}p(x^{},g(h(y^{}))).$$

The only DN set of positions for $`c`$ is $`\tau _0:=p\mathrm{}`$ because each argument of the head of $`c`$ is not a variable (see Definition 10). Hence, as $`p(x^{},g(h(y^{})))`$ is not $`\mathrm{\Delta }[\tau _0]`$-more general than $`p(f(x),g(y))`$, we can not conclude using $`\tau _0`$ that $`p(f(x),g(y))`$ left loops w.r.t. $`\{c\}`$.

However,

$$\tau ^+:=p2g(y)$$

is a set of positions with associated terms that is DN for $`\{c\}`$. Hence, by Theorem 4.2, the associated filter $`\mathrm{\Delta }[\tau ^+]`$ (see Definition 12) is DN for $`\{c\}`$. As $`p(x^{},g(h(y^{})))`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`p(f(x),g(y))`$, by Corollary 2 we get that

$$p(f(x),g(y))\text{ left loops w.r.t. }\{c\}.$$

By the $`\mathrm{\Delta }`$-Lifting Theorem 3.1, we can also conclude that each query that is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`p(f(x),g(y))`$ also left loops w.r.t. $`\{c\}`$. This means that each query of form $`p(t_1,t_2)`$ where $`t_1`$ is a term that is more general than $`f(x)`$ and $`t_2`$ is *any instance of $`g(y)`$* (because $`\tau ^+(p)=2g(y)`$) left loops w.r.t. $`\{c\}`$. ∎

###### Example 16

Let $`\mathrm{\Pi }:=\{p,q\}`$ with $`p`$ and $`q`$ two relation symbols whose arity equals 2. Let

$$\begin{array}{ccc}\hfill c_1:=& \hfill p(f(x),y)& q(x,g(x)),p(x,g(y))\hfill \\ \hfill c_2:=& \hfill q(a,g(x))& q(a,g(b))\hfill \end{array}$$

Then

$$\tau ^+:=p2y,q2g(x)$$

is a set of positions with associated terms that is DN for $`\{c_1,c_2\}`$. Hence, by Theorem 4.2, the associated filter $`\mathrm{\Delta }[\tau ^+]`$ (see Definition 12) is DN for $`\{c_1,c_2\}`$. Moreover, from the head $`q(a,g(x))`$ of $`c_2`$ we get

$$q(a,g(x))\underset{c_2}{}q(a,g(b)).$$

Applying Corollary 2, as $`q(a,g(b))`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`q(a,g(x))`$, we get that

$$q(a,g(x))\text{ left loops w.r.t. }c_2.$$

By the $`\mathrm{\Delta }`$-Lifting Theorem 3.1, each query of form $`q(t_1,t_2)`$ where $`t_1`$ is a term that is more general than $`a`$ and $`t_2`$ is *any instance of $`g(x)`$* (because $`\tau ^+(q)=2g(x)`$) left loops w.r.t. $`c_2`$. Notice that from the head $`p(f(x),y)`$ of $`c_1`$ we get

$$p(f(x),y)\underset{c_1}{}q(x^{},g(x^{})),p(x^{},g(y^{})).$$

As $`q(x^{},g(x^{}))`$ is such that $`x^{}`$ is more general than $`a`$ and $`g(x^{})`$ is an instance of $`g(x)`$, we get that $`q(x^{},g(x^{}))`$ left loops w.r.t. $`c_2`$. Consequently, $`p(f(x),y)`$ left loops w.r.t. $`\{c_1,c_2\}`$. So, again by the $`\mathrm{\Delta }`$-Lifting Theorem 3.1, each query of form $`p(t_1,t_2)`$, where $`t_1`$ is a term that is more general than $`f(x)`$ and $`t_2`$ is *any instance of $`y`$* (because $`\tau ^+(p)=2y`$) left loops w.r.t. $`\{c_1,c_2\}`$. ∎

###### Example 17

Let $`\mathrm{\Pi }:=\{p\}`$ with $`p`$ a relation symbol whose arity equals 2 and let

$$c:=p(x,x)p(f(x),f(x)).$$

As the arguments of the head of $`c`$ have one common variable $`x`$, the only set of positions with associated terms that is DN for $`c`$ is $`\tau _0^+`$ such that the domain of $`\tau _0^+(p)`$ is empty (see (DN1) in Definition 13). Notice that from the head $`p(x,x)`$ of $`c`$ we get

$$\begin{array}{c}p(x,x)\underset{c}{}p(f(x_1),f(x_1))\mathrm{}\hfill \\ \mathrm{}p(f^n(x_n),f^n(x_n))\underset{c}{}p(f^{n+1}(x_{n+1}),f^{n+1}(x_{n+1}))\mathrm{}\hfill \end{array}$$

As the arguments of $`p`$ grow from step to step, there cannot be any query in the derivation that is $`\mathrm{\Delta }[\tau _0^+]`$-more general than one of its ancestors. Consequently, we can not conclude that $`p(x,x)`$ left loops w.r.t $`c`$. ∎

## 6 Related Works

Some extensions of the Lifting Theorem with respect to infinite derivations are presented in , where the authors study numerous properties of finite failure. The non-ground finite failure set of a logic program is defined as the set of possibly non-ground atoms which admit a fair finitely failed SLD-tree w.r.t. the program. This denotation is shown correct in the following sense. If two programs have the same non-ground finite failure set, then any ground or non-ground goal which finitely fails w.r.t. one program also finitely fails w.r.t. the other. Such a property is false when we consider the standard ground finite failure set. The proof of correctness of the non-ground finite failure semantics relies on the following result. First, a derivation is called non-perpetual if it is a fair infinite derivation and there exists a finite depth from which unfolding does not instantiate the original goal any more. Then the authors define the definite answer goal of a non-perpetual derivation as the maximal instantiation of the original goal. A crucial lemma states that any instance of the definite answer goal admits a similar non-perpetual derivation. Compared to our work, note that we do need fairness as an hypothesis for the $`\mathrm{\Delta }`$-Lifting Theorem 3.1. On the other hand, investigating the relationships between non-ground arguments of definite answer and neutral arguments is an interesting problem.
Loop checking in logic programming is also a subject related to our work. In this area,  sets up some solid foundations. A loop check is a device to prune derivations when it seems appropriate. A loop checker is defined as *sound* if no solution is lost. It is *complete* if all infinite derivations are pruned. A complete loop check may also prune finite derivations. The authors shows that even for function-free programs (also known as Datalog programs), sound and complete loop checks are out of reach. Completeness is shown only for some restricted classes of function-free programs.

We now review loop checking in more details. To our best knowledge, among all existing loop checking mechanisms only OS-check , EVA-check  and VAF-check  are suitable for logic programs with function symbols. They rely on a structural characteristic of infinite SLD-derivations, namely, the growth of the size of some generated subgoals. This is what the following theorem states.

###### Theorem 6.1

Consider an infinite SLD-derivation $`\xi `$ where the leftmost selection rule is used. Then there are infinitely many queries $`Q_{i_1}`$, $`Q_{i_2}`$, … (with $`i_1<i_2<`$) in $`\xi `$ such that for any $`j1`$, the selected atom $`A_{i_j}`$ of $`Q_{i_j}`$ is an ancestor of the selected atom $`A_{i_{j+1}}`$ of $`Q_{i_{j+1}}`$ and $`\mathrm{𝑠𝑖𝑧𝑒}(A_{i_{j+1}})\mathrm{𝑠𝑖𝑧𝑒}(A_{i_j})`$.

Here, $`\mathrm{𝑠𝑖𝑧𝑒}`$ is a given function that maps an atom to its size which is defined in terms of the number of symbols appearing in the atom. As this theorem does not provide any sufficient condition to detect infinite SLD-derivations, the three loop checking mechanisms mentioned above may detect finite derivations as infinite. However, these mechanisms are *complete w.r.t. the leftmost selection rule* *i.e.* they detect all infinite loops when the leftmost selection rule is used.

OS-check (for OverSize loop check) was first introduced by Shalin  and was then formalized by Bol . It is based on a function $`\mathrm{𝑠𝑖𝑧𝑒}`$ that can have one of the three following definitions: for any atoms $`A`$ and $`B`$, either $`\mathrm{𝑠𝑖𝑧𝑒}(A)=\mathrm{𝑠𝑖𝑧𝑒}(B)`$, either $`\mathrm{𝑠𝑖𝑧𝑒}(A)`$ (resp. $`\mathrm{𝑠𝑖𝑧𝑒}(B)`$) is the count of symbols appearing in $`A`$ (resp. $`B`$), either $`\mathrm{𝑠𝑖𝑧𝑒}(A)\mathrm{𝑠𝑖𝑧𝑒}(B)`$ if for each $`i`$, the count of symbols of the $`i`$-th argument of $`A`$ is smaller than or equal to that of the $`i`$-th argument of $`B`$. OS-check says that an SLD-derivation may be infinite if it generates an atomic subgoal $`A`$ that is *oversized*, *i.e.* that has ancestor subgoals which have the same predicate symbol as $`A`$ and whose size is smaller than or equal to that of $`A`$.

EVA-check (for Extented Variant Atoms loop check) was introduced by Shen . It is based on the notion of *generalized variants*. EVA-check says that an SLD-derivation may be infinite if it generates an atomic subgoal $`A`$ that is a generalized variant of some of its ancestor $`A^{}`$, *i.e.* $`A`$ is a variant of $`A^{}`$ except for some arguments whose size increases from $`A^{}`$ to $`A`$ via a set of recursive clauses. Here the size function that is used applies to predicate arguments, *i.e.* to terms, and it is fixed: it is defined as the the count of symbols that appear in the terms. EVA-check is more reliable than OS-check because it is less likely to mis-identify infinite loops . This is mainly due to the fact that, unlike OS-check, EVA-check refers to the informative internal structure of subgoals.

VAF-check (for Variant Atoms loop check for logic programs with Functions) was proposed by Shen *et al.* . It is based on the notion of *expanded variants*. VAF-check says that an SLD-derivation may be infinite if it generates an atomic subgoal $`A`$ that is an expanded variant of some of its ancestor $`A^{}`$, *i.e.* $`A`$ is a variant of $`A^{}`$ except for some arguments $`t_{i_1},\mathrm{},t_{i_n}`$ such that: $`t_{i_1}`$ grows from $`A^{}`$ to $`A`$ into a function containing $`t_{i_1}`$, …, $`t_{i_n}`$ grows from $`A^{}`$ to $`A`$ into a function containing $`t_{i_n}`$. VAF-check is as reliable as and more efficient than EVA-check .

The main difference with our work is that we want to pinpoint *some* infinite derivations, based on syntactical properties of the program. We are not interested in completeness nor in soundness. Notice, however, that using the $`\mathrm{\Delta }`$-Lifting Theorem 3.1 as a loop checker leads to a device that is neither complete (see Example 17) nor sound since the Lifting Theorem 1.1 is a particular case of the $`\mathrm{\Delta }`$-Lifting Theorem 3.1.

## 7 Conclusion

We have presented a generalization of the lifting lemma for logic programming, which allows to disregard some arguments, termed neutral arguments, while checking for subsumption. We have investigated the model theoretic consequence of this generalization and have proposed two syntactic criteria for statically identifying neutral arguments.

A first application of this work has already been presented in , in the area of termination analysis of logic programs. We combine cTI , a termination inference tool with a non-termination inference analyzer whose correctness relies on our generalized lifting lemma. The resulting combined analysis may sometimes *characterize* the termination behavior of some concrete logic program w.r.t. to the left selection rule and the language we use to describe classes of queries.

Finally, this paper leaves numerous questions open. For instance, it might be interesting to try to generalize this approach to constraint logic programming . Can we obtain higher level proofs compared to those we give? Can we propose more abstract or semantically-based criteria for identifying neutral arguments?

Acknowledgements. We thank Ulrich Neumerkel for initial discussions on this topic and Roberto Bagnara for interesting suggestions.

## 8 Appendix 1

### 8.1 Proof of Proposition 1

By definition.

As $`Q`$ is $`\mathrm{\Delta }`$-more general than $`Q^{}`$, there exists a substitution $`\sigma `$ such that $`Q`$ is $`\mathrm{\Delta }`$-more general than $`Q^{}`$ for $`\sigma `$. Notice that $`Q`$ is also $`\mathrm{\Delta }`$-more general than $`Q^{}`$ for the substitution obtained by restricting the domain of $`\sigma `$ to the variables appearing the positions of $`Q`$ not distinguished by $`\mathrm{\Delta }`$. More precisely, let

$$T:=\{tTU_{}|p(t_1,\mathrm{},t_n)Q,i[1,n]Dom(\mathrm{\Delta }(p)),t=t_i\}$$

and

$$\eta :=\sigma |Var(T).$$

Then, $`Dom(\eta )Var(T)`$ *i.e.*

$$Dom(\eta )Var(Q)$$
(2)
and $`Q`$ is $`\mathrm{\Delta }`$-more general than $`Q^{}`$ for $`\eta `$.

Now, let $`xDom(\eta )`$. Then, as $`Dom(\eta )Var(T)`$, there exists $`A:=p(t_1,\mathrm{},t_n)Q`$ and $`i[1,n]Dom(\mathrm{\Delta }(p))`$ such that $`xVar(t_i)`$.

As $`Q`$ is $`\mathrm{\Delta }`$-more general than $`Q^{}`$ for $`\eta `$, there exists $`A^{}:=p(t_1^{},\mathrm{},t_n^{})`$ in $`Q^{}`$ such that $`A`$ is $`\mathrm{\Delta }`$-more general than $`A^{}`$ for $`\eta `$. But, as $`i[1,n]Dom(\mathrm{\Delta }(p))`$, we have $`t_i^{}=t_i\eta `$. So, as $`xVar(t_i)`$, $`x\eta `$ is a subterm of $`t_i^{}`$. Consequently, $`Var(x\eta )Var(t_i^{})`$, so $`Var(x\eta )Var(Q^{})`$.

So, we have proved that for each $`xDom(\eta )`$, $`Var(x\eta )Var(Q^{})`$, *i.e.* we have proved that

$$Ran(\eta )Var(Q^{}).$$
(3)
Finally, (2) and (3) imply that $`Dom(\eta )Ran(\eta )Var(Q,Q^{})`$ *i.e.* that

$$Var(\eta )Var(Q,Q^{}).$$

### 8.2 Proof of Proposition 3

Let $`c:=p(s_1,\mathrm{},s_n)\text{B}`$ and $`c^{}:=p(s_1^{},\mathrm{},s_n^{})\text{B}^{}`$ be a variant of $`c`$. Then, there exists a renaming $`\gamma `$ such that $`c^{}=c\gamma `$.

Let $`iDom(\tau ^+(p))`$. Suppose that there exists $`ji`$ such that $`Var(s_i^{})Var(s_j^{})\mathrm{}`$ and let us derive a contradiction.

Let $`x^{}Var(s_i^{})Var(s_j^{})`$. As $`s_j^{}=s_j\gamma `$, there exists $`xVar(s_j)`$ such that $`x^{}=x\gamma `$.

For such an $`x`$, as $`ji`$ and as $`Var(s_i)Var(s_j)=\mathrm{}`$ (because $`\tau ^+`$ is DN for $`c`$), we have $`xVar(s_i)`$. So, as $`\gamma `$ is a 1-1 and onto mapping from its domain to itself, we have $`x\gamma Var(s_i\gamma )`$<sup>1</sup><sup>1</sup>1 Because if $`x\gamma Var(s_i\gamma )`$, then either $`xVar(s_i)`$, either $`x\gamma Var(s_i)`$ and $`(x\gamma )\gamma =x\gamma `$. The former case is impossible because we said that $`xVar(s_i)`$. The latter case is impossible too because $`(x\gamma )\gamma =x\gamma `$ implies that $`x\gamma Dom(\gamma )`$ *i.e.* $`xDom(\gamma )`$ (because $`\gamma `$ is a 1-1 and onto mapping from its domain to itself); so, $`x=x\gamma `$ *i.e.*, as $`x\gamma Var(s_i)`$, $`xVar(s_i)`$. , *i.e.* $`x^{}Var(s_i^{})`$. Contradiction!

Consequently, $`Var(s_i^{})Var(s_j^{})=\mathrm{}`$.

Let $`iu_i\tau ^+(p)`$. As $`s_i`$ is more general than $`u_i`$ (because $`\tau ^+`$ is DN for $`c`$) and as $`s_i^{}`$ is a variant of $`s_i`$, $`s_i^{}`$ is more general than $`u_i`$.

Let $`iDom(\tau ^+(p))`$. Suppose that there exists $`q(t_1^{},\mathrm{},t_m^{})\text{B}^{}`$ and $`jDom(\tau ^+(q))`$ such that $`Var(s_i^{})Var(t_j^{})\mathrm{}`$. Let us derive a contradiction.

Let $`x^{}Var(s_i^{})Var(t_j^{})`$. As $`\text{B}^{}=\text{B}\gamma `$, there exists $`q(t_1,\mathrm{},t_m)\text{B}`$ such that $`q(t_1^{},\mathrm{},t_m^{})=q(t_1,\mathrm{},t_m)\gamma `$, *i.e.* $`t_j^{}=t_j\gamma `$. So, as $`x^{}Var(t_j^{})`$, there exists $`xVar(t_j)`$ such that $`x^{}=x\gamma `$.

For such an $`x`$, as the elements of $`Var(s_i)`$ only occur in those $`t_k`$ such that $`kDom(\tau ^+(q))`$ (because $`\tau ^+`$ is DN for $`c`$) and as $`xVar(t_j)`$ with $`jDom(\tau ^+(q))`$, we have $`xVar(s_i)`$. So, as $`\gamma `$ is a 1-1 and onto mapping from its domain to itself, we have $`x\gamma Var(s_i\gamma )`$ (see footnote 1), *i.e.* $`x^{}Var(s_i^{})`$. Contradiction!

Therefore, for each $`q(t_1^{},\mathrm{},t_m^{})\text{B}^{}`$ and $`jDom(\tau ^+(q))`$, we have $`Var(s_i^{})Var(t_j^{})=\mathrm{}`$.

Let $`q(t_1^{},\mathrm{},t_m^{})\text{B}^{}`$ and $`ju_j\tau ^+(q)`$. As $`t_j`$ is an instance of $`u_j`$ (because $`\tau ^+`$ is DN for $`c`$) and as $`t_j^{}`$ is a variant of $`t_j`$, $`t_j^{}`$ is an instance of $`u_j`$.

Finally, we have established that $`\tau ^+`$ is DN for $`c^{}`$. ∎

## 9 Appendix 2: DN Sets of Positions with Associated Terms Generate DN Filters

In this section, we give a proof of Theorem 4.2.

### 9.1 Context

All the results of this section are parametric to the following context:

* $`\tau ^+`$ denotes a set of positions with associated terms that is DN for a program $`P`$,
* $`Q\underset{c}{\overset{\theta }{}}Q_1`$ is an SLD-derivation step where

+ $`cP`$,
    + $`Q:=\text{A},p(t_1,\mathrm{},t_n),\text{C}`$ where $`p(t_1,\mathrm{},t_n)`$ is the selected atom,
    + $`c_1:=p(s_1,\mathrm{},s_n)\text{B}`$ is the input clause used,
* $`Q^{}:=\text{A}^{},p(t_1^{},\mathrm{},t_n^{}),\text{C}^{}`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`Q`$ *i.e.*, by Proposition 1, there exists a substitution $`\eta `$ such that $`Var(\eta )Var(Q,Q^{})`$ and $`Q^{}`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`Q`$ for $`\eta `$. Moreover, the position of $`p(t_1^{},\mathrm{},t_n^{})`$ in $`Q^{}`$ is the same as that of $`p(t_1,\mathrm{},t_n)`$ in $`Q`$.

### 9.2 Technical Definitions and Lemmas

###### Definition 14 (Technical Definition)

Let $`c_1^{}:=p(s_1^{},\mathrm{},s_n^{})\text{B}^{}`$ be a clause such that

* $`Var(c_1^{})Var(Q,Q^{})=\mathrm{}`$ and
* $`c_1=c_1^{}\gamma `$ for some renaming $`\gamma `$ satisfying $`Var(\gamma )Var(c_1,c_1^{})`$.

As $`c_1^{}`$ is a variant of $`c_1`$ and $`c_1`$ is a variant of $`c`$, then $`c_1^{}`$ is a variant of $`c`$. Moreover, as $`\tau ^+`$ is DN for $`c`$, by Proposition 3, $`\tau ^+`$ is DN for $`c_1^{}`$. So, by (DN2) in Definition 13, for each $`iu_i\tau ^+(p)`$ there exists a substitution $`\delta _i`$ such that $`u_i=s_i^{}\delta _i`$.

Moreover, as $`p(t_1^{},\mathrm{},t_n^{})`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`p(t_1,\mathrm{},t_n)`$, for each $`iu_i\tau ^+(p)`$, $`t_i^{}`$ is an instance of $`u_i`$. So, there exists a substitution $`\delta _i^{}`$ such that $`t_i^{}=u_i\delta _i^{}`$.

For each $`iDom(\tau ^+(p))`$, we set

$$\sigma _i\stackrel{def}{=}(\delta _i\delta _i^{})|Var(s_i^{}).$$

Moreover, we set:

$$\sigma \stackrel{def}{=}\underset{iDom(\tau ^+(p))}{}\sigma _i.$$

###### Lemma 1

The set $`\sigma `$ of Definition 14 is a well-defined substitution.

###### Proof

Notice that, as $`\tau ^+`$ is DN for $`c_1^{}`$, by (DN1) in Definition 13 we have

$$iDom(\tau ^+(p)),j[1,n]\{i\},Var(s_i^{})Var(s_j^{})=\mathrm{}.$$

Consequently,

$$i,jDom(\tau ^+(p)),ijDom(\sigma _i)Dom(\sigma _j)=\mathrm{}.$$

Moreover, for each $`iDom(\tau ^+(p))`$, $`\sigma _i`$ is a well-defined substitution. So, $`\sigma `$ is a well-defined substitution. ∎

###### Lemma 2 (Technical Lemma)

Let $`c_1^{}:=p(s_1^{},\mathrm{},s_n^{})\text{B}^{}`$ be a clause such that

* $`Var(c_1^{})Var(Q,Q^{})=\mathrm{}`$ and
* $`c_1=c_1^{}\gamma `$ for some renaming $`\gamma `$ satisfying $`Var(\gamma )Var(c_1,c_1^{})`$.

Let $`\sigma `$ be the substitution of Definition 14. Then, the substitution $`\sigma \eta \gamma \theta `$ is a unifier of $`p(t_1^{},\mathrm{},t_n^{})`$ and $`p(s_1^{},\mathrm{},s_n^{})`$.

###### Proof

The result follows from the following facts.

* For each $`iu_i\tau ^+(p)`$, we have:

$$s_i^{}\sigma =s_i^{}\sigma _i=s_i^{}\delta _i\delta _i^{}=(s_i^{}\delta _i)\delta _i^{}=u_i\delta _i^{}=t_i^{}$$

and $`t_i^{}\sigma =t_i^{}`$ because $`Dom(\sigma )Var(c_1^{})`$ and $`Var(Q^{})Var(c_1^{})=\mathrm{}`$. So, $`s_i^{}\sigma =t_i^{}\sigma `$ and $`s_i^{}\sigma \eta \gamma \theta =t_i^{}\sigma \eta \gamma \theta `$.
* For each $`i[1,n]Dom(\tau ^+(p))`$, we have:

$$s_i^{}\eta \gamma \theta =(s_i^{}\eta )\gamma \theta =s_i^{}\gamma \theta =(s_i^{}\gamma )\theta =s_i\theta $$

and

$$t_i^{}\eta \gamma \theta =(t_i^{}\eta )\gamma \theta =t_i\gamma \theta =(t_i\gamma )\theta =t_i\theta $$

and $`s_i\theta =t_i\theta `$ because $`\theta `$ is a unifier of $`p(s_1,\mathrm{},s_n)`$ and $`p(t_1,\mathrm{},t_n)`$ (because $`Q\underset{c}{\overset{\theta }{}}Q_1`$ with $`c_1`$ as input clause used). So,

$$s_i^{}\eta \gamma \theta =t_i^{}\eta \gamma \theta $$
(4)
* For each $`i[1,n]Dom(\tau ^+(p))`$, we also have:

+ $`s_i^{}\sigma =s_i^{}`$ because $`Dom(\sigma )=Var\left(\{s_j^{}|jDom(\tau ^+(p))\}\right)`$ and, by (DN1) in Definition 13, $`Var\left(\{s_j^{}|jDom(\tau ^+(p))\}\right)Var(s_i^{})=\mathrm{}`$;
    + $`t_i^{}\sigma =t_i^{}`$ because $`Dom(\sigma )Var(c_1^{})`$ and $`Var(Q^{})Var(c_1^{})=\mathrm{}`$.

Therefore, because of (4), $`s_i^{}\sigma \eta \gamma \theta =t_i^{}\sigma \eta \gamma \theta `$. ∎

### 9.3 $`\mathrm{\Delta }`$-Propagation

Now we extend the following Propagation Lemma that is proved by Apt in  p. 54–56.

###### Lemma 3 (Propagation)

Let $`G`$, $`G_1`$, $`G^{}`$ and $`G_1^{}`$ be queries such that $`G\underset{c}{}G_1`$ and $`G^{}\underset{c}{}G_1^{}`$ and:

* $`G`$ is an instance of $`G^{}`$
* in $`G`$ and $`G^{}`$ atoms in the same positions are selected.

Then, $`G_1`$ is an instance of $`G_1^{}`$.

First we establish the following result.

###### Lemma 4

Suppose that there exists an SLD-derivation step of form $`Q^{}\underset{c}{\overset{\theta ^{}}{}}Q_1^{}`$ where $`p(t_1^{},\mathrm{},t_n^{})`$ is the selected atom and the input clause is $`c_1^{}`$ such that $`Var(Q)Var(c_1^{})=\mathrm{}`$. Then, $`Q_1^{}`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`Q_1`$.

###### Proof

Notice that we have

$$Var(Q)Var(c_1)=Var(Q,Q^{})Var(c_1^{})=\mathrm{}.$$

Moreover, as $`c_1`$ is a variant of $`c_1^{}`$, there exists a renaming $`\gamma `$ such that

$$Var(\gamma )Var(c_1,c_1^{})\text{ and }c_1=c_1^{}\gamma .$$

Let $`c_1^{}:=p(s_1^{},\mathrm{},s_n^{})\text{B}^{}`$. Then,

$$Q_1=(\text{A},\text{B},\text{C})\theta \text{ and }Q_1^{}=(\text{A}^{},\text{B}^{},\text{C}^{})\theta ^{}.$$

$`\tau ^+`$ is DN for $`c`$ and $`c_1^{}`$ is a variant of $`c`$. So, by Proposition 3, $`\tau ^+`$ is DN for $`c_1^{}`$. Let $`\sigma `$ be the substitution of Definition 14.

* Let $`A^{}:=q(v_1^{},\mathrm{},v_m^{})\text{A}^{}`$. As $`\text{A}^{}`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than A for $`\eta `$, $`\text{A}^{}`$ and A have the same length. Moreover, if $`k`$ denotes the position of $`A^{}`$ in $`\text{A}^{}`$, then the $`k^{\text{th}}`$ atom of A has form $`q(v_1,\mathrm{},v_m)`$.

+ As $`A^{}`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`A`$ for $`\eta `$, for each $`ju_j\tau ^+(q)`$, $`v_j^{}`$ is an instance of $`u_j`$.
    + For each $`j[1,m]Dom(\tau ^+(q))`$ we have:

    $$v_j^{}\sigma \eta \gamma \theta =(v_j^{}\sigma )\eta \gamma \theta =v_j^{}\eta \gamma \theta $$

    because $`Dom(\sigma )=Var\left(\{s_i^{}|iDom(\tau ^+(p))\}\right)Var(c_1^{})`$ and $`Var(c_1^{})Var(Q^{})=\mathrm{}`$. Moreover,

    $$v_j^{}\eta \gamma \theta =(v_j^{}\eta )\gamma \theta =v_j\gamma \theta $$

    because $`\text{A}^{}`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than A for $`\eta `$. Finally,

    $$v_j\gamma \theta =(v_j\gamma )\theta =v_j\theta $$

    because $`Var(\gamma )Var(c_1,c_1^{})`$ and $`Var(c_1,c_1^{})Var(Q)=\mathrm{}`$.

Consequently, we have proved that

$$q(v_1^{},\mathrm{},v_m^{})\text{ is }\mathrm{\Delta }[\tau ^+]\text{-more general than }q(v_1,\mathrm{},v_m)\theta \text{ for }\sigma \eta \gamma \theta .$$

As $`q(v_1^{},\mathrm{},v_m^{})`$ denotes any atom of $`\text{A}^{}`$, we have proved that

$$\text{A}^{}\text{ is }\mathrm{\Delta }[\tau ^+]\text{-more general than }\text{A}\theta \text{ for }\sigma \eta \gamma \theta .$$
(5)
* Let $`A^{}:=q(v_1^{},\mathrm{},v_m^{})\text{B}^{}`$. As $`\text{B}=\text{B}^{}\gamma `$, then $`\text{B}^{}`$ and B have the same length. Moreover, if $`k`$ denotes the position of $`A^{}`$ in $`\text{B}^{}`$, then the $`k^{\text{th}}`$ atom of B has form $`q(v_1,\mathrm{},v_m)`$.

+ For each $`ju_j\tau ^+(q)`$, $`v_j^{}`$ is an instance of $`u_j`$ (because $`\tau ^+`$ is DN for $`c_1^{}`$ and (DN4) in Definition 13).
    + For each $`j[1,m]Dom(\tau ^+(q))`$ we have:

    $$v_j^{}\sigma \eta \gamma \theta =(v_j^{}\sigma )\eta \gamma \theta =v_j^{}\eta \gamma \theta $$

    because, by (DN3) in Definition 13,

    $$Var(v_j^{})Var\left(\{s_i^{}|iDom(\tau ^+(p))\}\right)=\mathrm{}$$

    with $`Dom(\sigma )=Var\left(\{s_i^{}|iDom(\tau ^+(p))\}\right)`$. Moreover,

    $$v_j^{}\eta \gamma \theta =(v_j^{}\eta )\gamma \theta =v_j^{}\gamma \theta $$

    because $`Var(\eta )Var(Q,Q^{})`$ and $`Var(c_1^{})Var(Q,Q^{})=\mathrm{}`$. Finally,

    $$v_j^{}\gamma \theta =(v_j^{}\gamma )\theta =v_j\theta $$

    because $`\text{B}=\text{B}^{}\gamma `$.

Consequently, we have proved that

$$q(v_1^{},\mathrm{},v_m^{})\text{ is }\mathrm{\Delta }[\tau ^+]\text{-more general than }q(v_1,\mathrm{},v_m)\theta \text{ for }\sigma \eta \gamma \theta .$$

As $`q(v_1^{},\mathrm{},v_m^{})`$ denotes any atom of $`\text{B}^{}`$, we have established that

$$\text{B}^{}\text{ is }\mathrm{\Delta }[\tau ^+]\text{-more general than }\text{B}\theta \text{ for }\sigma \eta \gamma \theta .$$
(6)
* Finally, by the same reasoning as for A and $`\text{A}^{}`$ above, we show that

$$\text{C}^{}\text{ is }\mathrm{\Delta }[\tau ^+]\text{-more general than }\text{C}\theta \text{ for }\sigma \eta \gamma \theta .$$
(7)

So, we conclude from (5), (6) and (7) that $`(\text{A}^{},\text{B}^{},\text{C}^{})`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`(\text{A},\text{B},\text{C})\theta `$ for $`\sigma \eta \gamma \theta `$ *i.e.* that

$$(\text{A}^{},\text{B}^{},\text{C}^{})\text{ is }\mathrm{\Delta }[\tau ^+]\text{-more general than }Q_1\text{ for }\sigma \eta \gamma \theta .$$
(8)
But, by the Technical Lemma 2, $`\sigma \eta \gamma \theta `$ is a unifier of $`p(s_1^{},\mathrm{},s_n^{})`$ and $`p(t_1^{},\mathrm{},t_n^{})`$. As $`\theta ^{}`$ is an mgu of $`p(s_1^{},\mathrm{},s_n^{})`$ and $`p(t_1^{},\mathrm{},t_n^{})`$ (because $`Q^{}\underset{c}{\overset{\theta ^{}}{}}Q_1^{}`$ with $`c_1^{}`$ as input clause), there exists $`\delta `$ such that $`\sigma \eta \gamma \theta =\theta ^{}\delta `$. Therefore, we conclude from (8) that $`(\text{A}^{},\text{B}^{},\text{C}^{})`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`Q_1`$ for $`\theta ^{}\delta `$. But this result implies that $`(\text{A}^{},\text{B}^{},\text{C}^{})\theta ^{}`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`Q_1`$ for $`\delta `$ *i.e.* that $`Q_1^{}`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`Q_1`$ for $`\delta `$. Finally, we have proved that $`Q_1^{}`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`Q_1`$.∎

Using the Propagation Lemma 3, the preceding result can be extended as follows.

###### Proposition 6 ($`\mathrm{\Delta }`$-Propagation)

If there exists an SLD-derivation step $`Q^{}\underset{c}{\overset{\theta ^{}}{}}Q_1^{}`$ where $`p(t_1^{},\mathrm{},t_n^{})`$ is the selected atom then $`Q_1^{}`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`Q_1`$.

###### Proof

Let $`c_1^{}`$ be the input clause used in $`Q^{}\underset{c}{\overset{\theta ^{}}{}}Q_1^{}`$. Take a variant $`Q^{\prime \prime }`$ of $`Q`$ such that

$$Var(Q^{\prime \prime })Var(c_1^{})=\mathrm{}$$

and a variant $`c_1^{\prime \prime }`$ of $`c`$ such that

$$Var(c_1^{\prime \prime })Var(Q^{\prime \prime })=\mathrm{}.$$

Then, the SLD-resolvent $`Q_1^{\prime \prime }`$ of $`Q^{\prime \prime }`$ and $`c`$ exists with the input clause $`c_1^{\prime \prime }`$ and with the atom selected in the same position as in $`Q`$. So, for some $`\theta ^{\prime \prime }`$, we have $`Q^{\prime \prime }\underset{c}{\overset{\theta ^{\prime \prime }}{}}Q_1^{\prime \prime }`$ with input clause $`c_1^{\prime \prime }`$. Consequently, we have:

$$Q\underset{c}{\overset{\theta }{}}Q_1\text{and}Q^{\prime \prime }\underset{c}{\overset{\theta ^{\prime \prime }}{}}Q_1^{\prime \prime }.$$

$`Q`$ and $`Q^{\prime \prime }`$ are instances of each other because $`Q^{\prime \prime }`$ is a variant of $`Q`$. So, by the Propagation Lemma 3 used twice, $`Q_1^{\prime \prime }`$ is an instance of $`Q_1`$ and $`Q_1`$ is an instance of $`Q_1^{\prime \prime }`$. So,

$$Q_1^{\prime \prime }\text{ is a variant of }Q_1.$$
(9)
But we also have

$$Q^{\prime \prime }\underset{c}{\overset{\theta ^{\prime \prime }}{}}Q_1^{\prime \prime }\text{and}Q^{}\underset{c}{\overset{\theta ^{}}{}}Q_1^{}$$

with input clauses $`c_1^{\prime \prime }`$ and $`c_1^{}`$, with $`Q^{}`$ that is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`Q^{\prime \prime }`$ (because $`Q^{\prime \prime }`$ is a variant of $`Q`$ and $`Q^{}`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`Q`$) and $`Var(Q^{\prime \prime })Var(c_1^{})=\mathrm{}`$. So, by Lemma 4,

$$Q_1^{}\text{ is }\mathrm{\Delta }[\tau ^+]\text{-more general than }Q_1^{\prime \prime }.$$
(10)
Finally, from (9) and (10) we have: $`Q_1^{}`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`Q_1`$. ∎

### 9.4 Epilogue

Theorem 4.2 is a direct consequence of the following result.

###### Proposition 7 (One Step $`\mathrm{\Delta }`$-Lifting)

Let $`c^{}`$ be a variant of $`c`$ variable disjoint with $`Q^{}`$. Then, for some $`\theta ^{}`$ and $`Q_1^{}`$,

* $`Q^{}\underset{c}{\overset{\theta ^{}}{}}Q_1^{}`$ where $`c^{}`$ is the input clause used,
* $`Q^{}\underset{c}{\overset{\theta ^{}}{}}Q_1^{}`$ is a $`\mathrm{\Delta }[\tau ^+]`$-lift of $`Q\underset{c}{\overset{\theta }{}}Q_1`$.

###### Proof

Let $`c_1^{}:=p(s_1^{},\mathrm{},s_n^{})\text{B}^{}`$ be a variant of $`c_1`$. Then there exists a renaming $`\gamma `$ such that $`Var(\gamma )Var(c_1,c_1^{})`$ and $`c_1=c_1^{}\gamma `$. Suppose also that

$$Var(c_1^{})Var(Q,Q^{})=\mathrm{}.$$

By the Technical Lemma 2, $`p(s_1^{},\mathrm{},s_n^{})`$ and $`p(t_1^{},\mathrm{},t_n^{})`$ unify. Moreover, as $`Var(c_1^{})Var(Q^{})=\mathrm{}`$, $`p(s_1^{},\mathrm{},s_n^{})`$ and $`p(t_1^{},\mathrm{},t_n^{})`$ are variable disjoint. Notice that the following claim holds.

###### Claim

Suppose that the atoms $`A`$ and $`H`$ are variable disjoint and unify. Then, $`A`$ also unifies with any variant $`H^{}`$ of $`H`$ variable disjoint with $`A`$.

###### Proof

For some $`\gamma `$ such that $`Dom(\gamma )Var(H^{})`$, we have $`H=H^{}\gamma `$. Let $`\theta `$ be a unifier of $`A`$ and $`H`$. Then, $`A\gamma \theta =A\theta =H\theta =H^{}\gamma \theta `$, so $`A`$ and $`H^{}`$ unify. ∎

Consequently, as $`c^{}`$ is a variant of $`c_1^{}`$ and $`c^{}`$ is variable disjoint with $`Q^{}`$, $`p(t_1^{},\mathrm{},t_n^{})`$ and the head of $`c^{}`$ unify. As they also are variable disjoint, we have

$$Q^{}\underset{c}{\overset{\theta ^{}}{}}Q_1^{}$$

for some $`\theta ^{}`$ and $`Q_1^{}`$ where $`p(t_1^{},\mathrm{},t_n^{})`$ is the selected atom and $`c^{}`$ is the input clause used. Moreover, by the $`\mathrm{\Delta }`$-Propagation Proposition 6, $`Q_1^{}`$ is $`\mathrm{\Delta }[\tau ^+]`$-more general than $`Q_1`$. ∎


format: text

text:
# Possible new 𝛾-ray pulsar detections for AGILE and GLAST missions: The outer gap model look at the Parkes pulsar Catalog

## 1. Introduction

The Parkes multibeam pulsar survey (PMPS, now containing 468 objects) is a large-scale survey of a narrow strip of the inner Galactic plane ($`|b|<5\mathrm{°}`$, $`260\mathrm{°}<l<50\mathrm{°}`$; Manchester et al. 2001). PMPS pulsars are generally thought to be potential counterparts of EGRET unidentified sources. However, only a handful of them are superposed with EGRET detections, and even less can be considered a plausible counterpart (e.g. D’Amico et al. 2001; Camilo et al. 2001; Torres et al. 2001b). PMPS pulsars are also thought of as natural candidates for new $`\gamma `$-ray detections by AGILE and GLAST missions. Nevertheless, this is strongly dependent on the high energy emission model assumed. Predicting which pulsars can (or cannot) be emitting $`\gamma `$-rays is essential in determining if these models are correct.

## 2. The outer gap model look at the Parkes catalog

There are basically two kinds of models for high energy emission from pulsars. In polar cap models, charged particles are accelerated in charged-depleted zones near the poles of the pulsar. $`\gamma `$-rays are produced through curvature-radiation-induced $`\gamma `$-B pair cascades (Harding 1981) or Compton-induced pair cascades (Dermer & Sturner 1994). For outer gaps, particle acceleration occurs in charged-depleted regions in the outer magnetosphere. There are two outer gap models: thin and thick outer gaps. Here we shall use the thick outer gap scenario because it can be applied to all radio pulsars, including mature ones (this is the case of most pulsars in our sample, whose mean characteristic age is 500 kyr).

In the thick outer gap model (Zhang & Cheng 1997), the size of the outer gap, $`f_s`$, is limited by pair production between the soft thermal X-rays from the stellar surface and the curvature photons with energy $`E_\gamma (f_s)`$ emitted by the primary e± accelerated in the gap. The energy of the soft X-ray photons, $`E_X(f_s)`$, is determined by the backflow of the gap’s e±. Therefore $`E_X(f_s)`$ is also a function of the gap size. Using $`E_X(f_s)E_\gamma (f_s)(mc^2)^2`$ , the size of the outer gap (the ratio between the outer gap volume and $`R_L^3`$, with $`R_L`$ the light cylinder radius) is: $`f_s=5.5P^{26/21}B_{12}^{4/7},`$ where $`P`$ is the pulsar period and $`B_{12}`$ the magnetic field in units of $`10^{12}`$ G (see Zhang & Cheng 1997; Zhang & Cheng 1997; 1998a,b for details). It should be noted that $`f_s`$ is bound to be less than 1 for this model to make sense. The $`\gamma `$-ray luminosity is: $`L_\gamma 3.6\times 10^{31}f_s^3B_{12}^2P^4\mathrm{erg}\mathrm{s}^1.`$ The integrated flux on Earth is then given by

$$F_\gamma ^{th}\frac{L_\gamma }{\mathrm{\Delta }\mathrm{\Omega }d^2\overline{E_c}}\frac{7\times 10^7}{d_{kpc}^2\mathrm{\Delta }\mathrm{\Omega }}\left(\frac{B_{12}}{P}\right)^{11/28}\mathrm{ph}\mathrm{cm}^2\mathrm{s}^1.$$
(1)
Here, $`\overline{E_c}`$ is an average energy of the radiated photons, $`\overline{E_c}10^3(P/B_{12})^{3/28}`$ erg, $`\mathrm{\Delta }\mathrm{\Omega }`$ is the beaming angle, and $`d`$ the distance to the pulsar. The theoretical efficiency of the model $`\eta _{th}=L_\gamma /\dot{E}`$ results in $`\eta _{th}83B_{12}^{12/7}P^{26/7}.`$ These formulae has been compared with data for the observed $`\gamma `$-ray pulsars, and for 350 radio pulsars with ages above 1 kyr and known $`\gamma `$-ray flux upper limits (Zhang & Cheng 1998a, see also Zhang et al. 2000). Zhang & Cheng (2002) have considered the outer gap model in relation with the soft gamma-ray repeaters, and Anchordoqui et al. (2002) used an outer gap scenario to study the neutrino production in X-ray binaries.

Tables 1 and 2 show PMPS pulsars for which $`f_s<1`$. Columns show the pulsar name, the period and period derivative, the characteristic age $`\tau =P/2\dot{P}`$, the spin-down luminosity ($`\dot{E}=4\pi ^2I\dot{P}/P^3`$, with $`I=10^{45}`$ g cm2), the magnetic field (assuming a dipole model, $`\dot{E}=2.8\times 10^{31}B_{12}^2P^4`$ erg s-1, with $`B_{12}`$ being the magnetic field in units of $`10^{12}`$ G), the distance (obtained using the model by Taylor and Cordes 1993), $`f_s`$, the theoretical expected efficiency, the $`\gamma `$-ray luminosity, the flux on Earth (assuming 1 sr beaming), and the comparison of the predicted flux with the sensitivity of forthcoming satellites. A y-mark represents that the flux is above AGILE (GLAST) sensitivity, considered as 5$`\times 10^8`$ ($`2\times 10^9`$) photons cm-2 s-1, respectively. It is clear that different beaming fractions can change the verdict on which pulsar will be possible to observe. Thus, the detection marks y and n are only indicative of what can one expect, but are not to be considered final predictions. On the contrary, PMPS pulsars not contained in these tables are unable to produce $`\gamma `$-rays if the outer gap model is correct, no matter any other possible uncertainty in distance or beaming angle.

Table 1 contains pulsars for which the efficiency is less than 20%, as for the observed 3EG $`\gamma `$-ray pulsars. Table 2 lists pulsars which have $`f_s<1`$, but produce much larger values of theoretical efficiencies. 60% of these pulsars have $`\dot{E}_{33}/d^2<0.5`$, which has been often used as an indicator for a low probability of detection (e.g. Thompson et al. 2001). While these pulsars could still be plausible outer gap $`\gamma `$-ray pulsar candidates from a strictly theoretical point of view, they are not phenomenologically favored.

In the thick outer gap model given by Zhang & Cheng (1997), the effects of magnetic inclination angle ($`\alpha `$) are not taken into account (Zhang & Cheng 2002). Under these effects, $`f_s`$ transforms into $`f_s\times c(\alpha )`$ where $`c(\alpha )=`$1, 0.9, 0.83, 0.70, 0.57 for inclination angles of 45, 55, 65, and 75 degrees (Cheng 2002). However, although $`f_s`$ will vary with $`\alpha `$, its value at $`R_L/2`$, where $`R_L`$ is the radius of light cylinder (see Cheng, Ruderman & Zhang, 2000) is a sensible approximation. In addition, most of the Parkes pulsars having $`f_s>1`$ have indeed $`f_s1`$, and so the $`\alpha `$-dependence is unimportant here.

## 3. Pulsar distances

The distances given in the PMPS were obtained applying the model for the Galactic distribution of electrons given by Taylor and Cordes (1993). Recently, Cordes and Lazio (2002) presented an improved model for this distribution. We have used Cordes and Lazio’s (2002) NE2001 code to compute these new distances using the dispersion measures given in the PMPS. Fig. 1a shows how they deviate from the previous estimations for all pulsars contained in Tables 1 and 2. Generally, new inferred values are smaller, what implies bigger fluxes, see Fig. 1b. For some particular cases -especially for those pulsars having the largest inferred 1993 distances- differences are notorious. Tables 1 and 2 give, as well, the newly computed distances and fluxes (separated by a /-symbol). These values affect the detection criterion for the AGILE mission. Using the newest electron model, there are 14% more $`f_s<1`$ pulsars with fluxes above the AGILE threshold. Note, however, that changing the distances to these new values does not affect the sample of possible outer gap pulsars: The latter is constructed using only intrinsic pulsar parameters.

## 4. Positional coincidences

There are four EGRET sources now found to be spatially coincident with newly discovered PMPS pulsars. Table 3 shows these new positional coincidences, obtained using FORREST (Sigl et al. 2001). In all these cases, the efficiencies required to produce the $`\gamma `$-ray sources are $`\eta 1000\%`$ (even for the reduced NE2001 distances), making the potential associations unphysical. None of the pulsars contained in Table 3 has $`f_s<1`$.

The possibly variable source (Torres et al. 2001) 3EG J1824$``$1514 has been proposed to be result of inverse Compton emission from a microquasar (Paredes et al. 2000). Although there are (considering all catalogs) three pulsars coincident with this source none pose a challenge for the microquasar interpretation. There are three pulsars in the 3EG J1903$`+`$0550 error box, but none is energetic enough as to produce it. 3EG J1903$`+`$0550 is also coincident with SNR G39.2$``$0.3 (Romero et al. 1999), which is in turn co-spatial with a giant molecular cloud. Torres et al. (2002) have shown that the interaction between the molecular cloud and the SNR could produce most of the flux observed by EGRET, similar to the case of G347.3-0.5 (Butt et al. 2001).

## 5. Concluding Remarks

In the framework of the outer gap model of $`\gamma `$-ray emission from pulsars, we have theoretically computed the $`\gamma `$-ray luminosity, the theoretical efficiency, and other parameters for all radio pulsars listed in the current version of the PMPS. Most pulsars (82% out of 468 reported in the latest release) are not $`\gamma `$-ray pulsars if the outer gap model is correct. Should AGILE or GLAST detect $`\gamma `$-ray emission coming from PMPS pulsars not contained in Tables 1 and 2, a different high energy emission should be operative. This is a definite prediction valid independently of our ignorance of the beaming angle or the distance. Tables 1 and 2 then show PMPS pulsars which, in the framework of the outer gap model, can be $`\gamma `$-ray detections for AGILE and GLAST. 13 of these pulsars are excellent candidates, having large values of $`\dot{E}`$ and $`\dot{E}_{33}/d^2`$, and low values of $`f_s`$ and $`\eta _{th}`$. The new model for the electron density in the galaxy (Cordes and Lazio 2002) reduce the pulsar distances reported in the PMPS, enlarging the predicted fluxes. The use of this new model is essential in determining the expected detection; corrections can be as large as 90%. Finally, four new PMPS pulsars are coinciding with previously detected EGRET sources. None of them qualify as a possible counterpart for their respective spatially coincident $`\gamma `$-ray source, nor they can emit $`\gamma `$-rays if the outer gap model is correct.

The work of D.F.T. was performed under the auspices of the U.S. D.O.E. (NNSA), by University of California Lawrence Livermore National Laboratory under contract No. W-7405-Eng-48. D.F.T. is LLNL’s Lawrence Fellow in Astrophysics. He thanks F. Camilo, G.E. Romero, C. Mauche, and K.S. Cheng for useful comments.


text:
# Orthogonality Catastrophe for Vortices in 𝑑-Wave Superconductors

(December 29, 2002)

## Abstract

The dynamics of magnetic vortices in the mixed state of $`d`$-wave superconductors is affected by interaction with quasiparticles near the gap nodes. We study this effect by computing the overlap of the ground state wave functions of the nodal quasiparticles in a two-dimensional $`d`$-wave superconductor as the ground state changes in response to the motion of the vortex. We find that the overlap is strongly suppressed. This orthogonality catastrophe is specific to a half-quantum vortex and disappears in the case of a doubly-quantized vortex. This implies strong inhibition of the motion of half-quantum vortices. The results allow us to develop a simple description of the quantum vortex creep at low temperatures.

Magnetic vortices in Cuprate superconductors Bla ; YesMalSha  behave rather differently compared to their counterparts in conventional materials. One of the characteristic features of the superconducting state of the Cuprates is the existence of the low-energy quasiparticles near the nodes of the $`d`$-wave gap. One is naturally led to ask: what is the influence of the interaction between the vortices and nodal quasiparticles on vortex dynamics?

Before answering this question, let us briefly describe our current knowledge. Vortex creep at low temperatures is believed to proceed by quantum tunneling. It has been argued that two forces govern vortex dynamics during tunneling: the Magnus force AoTho  and the friction force. Their ratio determines the “cleanness” of the material. The creep in the dirty, BlaGesVin  super-clean, Fei  and intermediate regimes Creep\_intermediate  has been studied theoretically.

Quasiparticles play prominent role in the vortex dynamics. In $`s`$-wave superconductors, finite gap in the bulk precludes the existence of low-energy extended states, however quasiparticle states localized in the cores of vortices, where the gap vanishes, exist. Core\_States  Transitions between these states give rise to the friction force and the renormalization of the Magnus force. KopKra  The situation with quasiparticle states localized inside vortex cores in $`d`$-wave superconductors is far less clear. Franz\_Tesanovic  On the other hand, extended states exist and are expected to strongly interact with vortices. Indeed, they have been argued Ashvin ; Vafek  to give a quantized value of thermal Hall conductance in the mixed state at low temperatures. This prediction is hard to verify since current experiments Zhang  are performed at relatively high temperatures. Durst  Quantum vortex creep, which is also expected to be sensitive to the interaction with quasiparticles, occurs at much lower temperatures and thus offers experimental information about the quasiparticle spectrum at a much lower energy scale.

To study the contribution of nodal quasiparticles to vortex action we calculate the overlap of the ground state wave functions of the nodal fermions as the ground state changes in response to the motion of the vortex. We find that this overlap is extremely small in the case of a half-quantum vortex. This implies that the motion of half-quantum vortices is strongly suppressed due to the interaction with nodal quasiparticles. Indeed, we argue that this orthogonality catastrophe provides the dominant contribution to the vortex action at temperatures relevant to quantum vortex creep. Based on this, we present a simple phenomenological description of the available experimental data.

Let us consider a vortex in a 2D $`d`$-wave superconductor. We use the Bogoliubov-de Gennes (BdG) equation to treat the interaction of quasiparticles with the vortex. Ashvin ; Mel'nikov . We first take advantage of the conservation of spin in the BCS theory by changing from the original electronic operators $`c`$ to the new fermions: $`\psi _{1k}=c_k`$, $`\psi _{2k}=c_k^{}`$. The new operators are combined to form a two-component spinor: $`\psi =(\psi _1,\psi _2)`$. The density of the $`\psi `$-particles $`\psi ^{}\psi `$ is the $`z`$-component of the spin density of the original electrons, and visa versa. Next, we concentrate on the variation of the phase of the order parameter $`\varphi (\stackrel{}{r})`$ around the vortex and neglect the variation of the amplitude. We then eliminate the phase winding by making a single-valued gauge transformation: $`\psi _1\mathrm{exp}[i\varphi (\stackrel{}{r})]\psi _1`$, $`\psi _2\psi _2`$. The BdG equation takes the form $`H\psi =\epsilon \psi `$ with the following Hamiltonian (we use units with $`\mathrm{}=c=1`$):

$$H=E(\stackrel{}{p}+\stackrel{}{a}+\stackrel{}{j}_s\sigma _z)\sigma _z+\mathrm{\Delta }(\stackrel{}{p}+\stackrel{}{a})\sigma _x.$$
(1)
Here, $`\sigma _z`$, $`\sigma _x`$ are Pauli matrices, $`\stackrel{}{p}=(p_x,p_y)`$ is the 2D momentum, $`E(\stackrel{}{p})`$ is the bare electron energy relative to the Fermi energy and $`\mathrm{\Delta }(\stackrel{}{p})`$ is the gap function. The presence of the vortex produces two contributions to the Hamiltonian: 1) There appears a “Doppler shift”. The superflow $`\stackrel{}{j}_s=\stackrel{}{}\varphi /2e\stackrel{}{A}`$ shifts the energies of the nodal quasiparticles similar to the classical Doppler effect. 2) The other contribution is of topological nature. It requires that a parallel transport of a quasiparticle around the vortex should lead to the change of its phase by $`\pi \nu `$, where $`\nu `$ is the vortex quantum number. This is enforced by the Chern-Simons gauge field $`\stackrel{}{a}=\stackrel{}{}\varphi /2`$ which satisfies $`\stackrel{}{}\times \stackrel{}{a}=\pi \nu \mathrm{}\delta (\stackrel{}{r})`$ (assuming the vortex is at the origin).

First, we would like to calculate the overlap between the ground state wave functions of the superconductor with and without the half-quantum vortex. The two terms in the Hamiltonian that were discussed above both perturb the system shifting the single quasiparticle eigenstates. An important difference between them is their spatial range. The superflow $`\stackrel{}{j}_s(\stackrel{}{r})`$ is screened at distances larger than the penetration depth. On the contrary, the field $`a(\stackrel{}{r})`$ decays as $`1/r`$ at all distances. Let us consider the Doppler shift term first. The solution of the orthogonality catastrophe problem OC  in the case of a short-range perturbing potential is given by:

$`|f|i|`$ $``$ $`N^A,`$ (2)
$`A`$ $`=`$ $`{\displaystyle \frac{1}{2}}\mathrm{Tr}[\widehat{\delta }(\epsilon _F)/\pi ]^2.`$ (3)
Here, $`|i`$ and $`|f`$ are the ground states of the system before and after the perturbing potential is switched on, $`N`$ is the total number of fermions in the system, and $`\widehat{\delta }(\epsilon )=(1/2i)\mathrm{ln}\widehat{S}(\epsilon )`$ is the phase shift matrix defined as the logarithm of the scattering matrix. The trace in the Eq. (3) is over all states at the Fermi energy. In our case the Fermi energy is zero. The density of states of nodal quasiparticles vanishes linearly with energy: there are no states at zero energy. This property of the phase space implies that the orthogonality exponent $`A`$ is zero for any scattering potential of finite range. This means that the Doppler shift term causes possibly quite large but finite reduction of the overlap. Absence of infrared divergence in this case has been found previously Cassanello\_Fradkin  in a different context.

Based on what was said above, we set in the following $`\stackrel{}{j}_s=0`$ in Eq. (1). Mel'nikov  The remaining perturbation of the system is the long-range vector Chern-Simons field $`\stackrel{}{a}(\stackrel{}{r})`$. Because the field decays slowly at infinity, it is not clear whether the above result for the orthogonality catastrophe for short-range potentials can be generalized to this case. It is also not clear whether at all one can use plane waves as asymptotic states to calculate the $`\widehat{S}`$ matrix: the asymptotic completeness has been proven only for short-range potentials in the Dirac equation. Thaller

For these reasons we shall adopt another approach. The field $`\stackrel{}{a}(\stackrel{}{r})`$ can be gauged away by a gauge transformation: $`\psi \psi \mathrm{exp}(i\nu \theta /2)`$, where $`\nu `$ is the vortex quantum number and $`\theta `$ is the polar angle. The BdG Hamiltonian Eq. (1) reduces to a free one:

$`H=E(\stackrel{}{p})\sigma _z+\mathrm{\Delta }(\stackrel{}{p})\sigma _x.`$ (4)
For a doubly-quantized vortex, $`\nu =2`$, this implies no orthogonality catastrophe between the ground states with and without such a vortex. On the other hand, for a singly-quantized vortex this transformation makes $`\psi `$ non-single valued. To take this into account, we introduce a cut $`𝒞`$ in the $`(x,y)`$ plane as shown in Fig. 1. The vortex is assumed to be at point $`A`$ at the origin. Since the cut should end on another half-quantum vortex, we introduce one at point $`B`$ for definiteness. We then impose a $`\pi `$-phase shift across the cut.

The distance $`L`$ between the two vortices can be interpreted in various ways: First, $`L`$ may be thought of as a long-distance cut-off. In another setting, one may consider an isolated vortex being moved from point $`A`$ to point $`B`$. This can be done by removing a vortex at point $`A`$ (inserting a vortex with negative vorticity) and creating one at point $`B`$. In this situation $`L`$ is the distance by which the vortex has been moved.

Having made the gauge transformation we can reformulate our original problem as that of finding the overlap of the ground state wave functions of the system before and after a $`\pi `$-phase shift across the cut shown in Fig. 1 was imposed. To this end, consider the dynamical overlap function which is defined as follows: Let $`|i`$ be the ground state wave function of the unperturbed system. We shall work in imaginary time to simplify calculations and avoid problems with time-ordering. At time $`\tau =0`$ the phase shift $`\pi `$ across the cut $`𝒞`$ is imposed. Let $`|\tau =U(\tau )|i`$, where $`U(\tau )`$ is the imaginary time evolution operator. Since in the limit $`\tau \mathrm{}`$ only the contribution from the new ground state to $`U(\tau )`$ survives, we have: $`lim_\tau \mathrm{}\tau |i=f|i`$, where $`|f`$ is the new ground state. Since $`\tau |i=i|U^{}(\tau )|i`$, the problem reduces to that of finding the expectation value of the evolution operator in the old ground state. We have:

$`U(\tau )`$ $`=`$ $`\mathrm{exp}\left\{i\pi Q(\tau )\right\},`$ (5)
$`Q(\tau )`$ $`=`$ $`{\displaystyle _0^\tau }J(\tau ^{})𝑑\tau ^{}.`$ (6)
Here, $`J(\tau )`$ is the total current through the cut $`𝒞`$ and $`Q(\tau )`$ is the net charge that has flowed through the cut between times $`0`$ and $`\tau `$ (here and below, unless mentioned otherwise, the charges and currents are those of the $`\psi `$-fermions). The meaning of the above expressions is quite transparent: Each fermion contributes phase $`\pi `$ to the path integral every time it crosses the cut. The operator $`U(\tau )`$ can thus be thought as a generator of counting statistics. Levitov\_Lee\_Lesovik

Since the unperturbed Hamiltonian is quadratic in the fermionic currents we can apply Gaussian averaging to obtain:

$`\tau |i=\mathrm{exp}\left\{A\right\},`$ (7)
$`A={\displaystyle \frac{\pi ^2}{2}}Q^2(\tau ).`$ (8)
To proceed, we need to find the current-current correlation function. We linearize the Hamiltonian Eq. (4) around one of the nodes (e.g. one at $`(k_F,0)`$): $`E(\stackrel{}{p})=v_Fp_x`$, $`\mathrm{\Delta }(\stackrel{}{p})=v_\mathrm{\Delta }p_y`$. The anisotropy parameter $`\alpha =v_F/v_\mathrm{\Delta }E_F/\mathrm{\Delta }`$ is quite large ($`\alpha 14`$ for YBCO). We then make $`\alpha =1`$ by rescaling the distances: $`p_xp_x/v_F`$, $`p_yp_y/v_\mathrm{\Delta }`$. This allows us to exploit the full “relativistic” invariance of the problem. Indeed, the imaginary time action (in the second-quantized notation) becomes:

$`S={\displaystyle \underset{p}{}}\overline{\psi }\sigma _\mu p_\mu \psi .`$ (9)
Here, $`p_\mu =(w,p_x,p_y)`$ is the 2+1 momentum, $`\overline{\psi }=i\psi ^{}\sigma _y`$. Pauli matrices $`\sigma _\mu `$ form a Clifford algebra: $`\{\sigma _\mu ,\sigma _\nu \}=2\delta _{\mu \nu }`$. The “relativistic” invariance is now explicit since both $`\sigma _\mu `$ and $`p_\mu `$ transform as 2+1 vectors under rotations of the Euclidean space-time and the action $`S`$ is therefore a scalar. The conserved current is:

$`j_\mu =\overline{\psi }\sigma _\mu \psi .`$ (10)
The current-current correlator is given (in the free theory) by the so-called bubble or vacuum polarization diagram:

$`j_\mu j_\nu _k={\displaystyle \frac{d^3q}{(2\pi )^3}\mathrm{Tr}\left[\sigma _\mu G(q)\sigma _\nu G(q+k)\right]}.`$ (11)
Here, $`G(q)=\sigma _\mu q_\mu /q^2`$ is the Green function of the Dirac equation. The correlator, as written, is given by an ultra-violet divergent expression. This divergence can be eliminated by an appropriate high-energy cut-off. Introduction of such a cut-off, however, will break the gauge invariance. A more physical way is to explicitly impose the current conservation condition: $`k_\mu j_\mu j_\nu _k=0`$. This way one obtains the well-known result (see QED\_3  for a related calculation):

$`j_\mu j_\nu _k={\displaystyle \frac{1}{16k}}\left(k^2\delta _{\mu \nu }k_\mu k_\nu \right).`$ (12)
The inverse Fourier transform of this correlator is:

$`j_\mu (r)j_\nu (0)=(^2\delta _{\mu \nu }_\mu _\nu ){\displaystyle \frac{1}{32\pi ^2r^2}},`$ (13)
where $`r_\mu =(\tau ^{},x,y)`$. The fluctuation of the charge $`Q^2(\tau )`$ that flowed through the cut $`𝒞`$ of length $`L`$ during time $`\tau `$ is then given by the integral over the segment $`\mathrm{\Omega }=\{r:0<\tau ^{}<\tau ,x=0,\mathrm{\hspace{0.17em}0}<y<L\}`$ of the hyperplane $`(\tau ,y)`$. Explicitly, one has:

$`Q^2(\tau )={\displaystyle _\mathrm{\Omega }}𝑑r_1{\displaystyle _\mathrm{\Omega }}𝑑r_2j_x(r_1)j_x(r_2),`$ (14)
Substituting Eq. (13) into Eq. (14) and using Gauss theorem twice, one obtains:

$`Q^2(\tau )={\displaystyle \frac{1}{32\pi ^2}}{\displaystyle _\mathrm{\Omega }}{\displaystyle _\mathrm{\Omega }}{\displaystyle \frac{dS(r_1)dS(r_2)}{(r_1r_2)^2}}.`$ (15)
Here, $`dS=dl`$ is the “surface” element of the boundary $`\mathrm{\Omega }`$, while $`dl`$ is the length element of the corresponding perimeter. The integral in Eq. (15) diverges as $`r_1r_2`$. This means that the exponent in the final result acquires an explicit cut-off dependence. A suitable way to introduce a short time cut-off is to replace:

$`{\displaystyle \frac{1}{(r_1r_2)^2}}{\displaystyle \frac{1}{(r_1r_2)^2+a^2}}.`$ (16)
The cut-off $`a`$ is, roughly, the inverse of the energy at which the linear Dirac dispersion breaks down. It would be justified to assume $`a1/\mathrm{\Delta }`$. The integral in Eq. (15) can now be easily evaluated. Plugging the result in Eq. (8) in the case where $`L,\tau \mathrm{\Delta }^1`$ one obtains:

$`A\mathrm{\Delta }\left(L+\tau \right).`$ (17)
This can be called a perimeter law for vortex action: the contribution of nodal fermions to the imaginary time action of a half-quantum vortex is proportional to the length of the vortex trajectory in the Euclidean space-time. The proportionality of the action to the perimeter of $`\mathrm{\Omega }`$ rather than its surface area is essentially due to the conservation of the number of $`\psi `$-particles. In terms of the original electrons, it is the conservation of the $`z`$-component of spin polarization.

Let us now discuss the implication of these results for the vortex dynamics in $`d`$-wave superconductors. First of all, Eq. (17) shows that the orthogonality catastrophe for a half-quantum vortex is very strong. Even when the length $`L`$ is finite (e.g. when the vortex moves over a small distance) the dynamical overlap of the two states vanishes in the limit $`\tau \mathrm{}`$. Certainly, finite temperature provides a cut-off: $`\tau _{th}1/T`$. This leads to the conclusion that the contribution of the nodal fermions to the imaginary time action at low temperatures is dominated by the second term in Eq. (17): $`A\mathrm{\Delta }/T`$. This, in turn, means that the dynamical magnetization relaxation rate $`Q(T)=1/S`$YesMalSha  where $`S`$ is the total tunneling action, vanishes linearly with temperature in the limit $`T0`$. Indeed, the diverging contribution $`A`$ to the action $`S`$ becomes the dominant one in the same limit. The fact that experiments YesMalSha  show a finite $`Q(0)`$ leads us to conclude that there is some other low-energy cut-off besides temperature. We speculate that it may appear as a consequence of a mini-gap in the Dirac spectrum of nodal quasiparticles. Such a mini-gap is expected in finite magnetic field as a result of curvature terms in the dispersion around the nodal point. Its magnitude has been estimated Ashvin  to be $`\delta =\kappa H`$, $`\kappa 0.5K\mathrm{Tesla}^1`$, where $`H`$ is the external magnetic field. Taking the mini-gap into account, we expect the following behavior of the magnetization relaxation rate at low temperatures:

$`Q(T)\{\begin{array}{cc}T/\mathrm{\Delta },& T\delta \\ \delta /\mathrm{\Delta },& T\delta \end{array}`$ (20)
This behavior is shown in Fig. 2. Qualitatively, the following picture emerges: There is a small energy scale $`\delta `$ set by the size of the mini-gap in the Dirac spectrum of nodal fermions. This energy scale defines a cross-over temperature between two regimes: a) For $`T\delta `$ the function $`Q(T)`$ is linear in $`T`$ with the coefficient $`1/\mathrm{\Delta }`$ which is little dependent on the details; b) For $`T\delta `$ the function $`Q(T)`$ saturates at a value $`\delta /\mathrm{\Delta }`$. Experimentally, YesMalSha  in the regime $`T\delta `$ typical slopes of $`Q(T)`$ are $`10^2K^1`$ which is consistent with the typical value $`\mathrm{\Delta }10^2K`$ for the Cuprates, although the linearity in $`T`$ is difficult to establish. Typical values of the cross-over temperature are $`\delta 1K`$ (i.e. for magnetic fields $`1T`$, in agreement with the theoretical estimate Ashvin ). The arguments above then predict $`Q(0)10^2`$, also in agreement with experiments. Note that in this simple picture we have omitted disorder effects on the spectrum of nodal quasiparticles, inter-vortex interactions etc. In particular, the Zeeman splitting is expected Ashvin  to change the simple $`\delta =\kappa H`$ behavior.

As an end note, we would like to point out one interesting consequence of the obtained results. As we have seen, the orthogonality catastrophe strongly inhibits the motion of half-quantum vortices, whereas the effect disappears for doubly-quantized vortices. This suggests a possible tendency of vortices to pair which would increase their mobility and, effectively, decrease their energy. This scenario is similar to the one used in recent studies of fractionalized phases Ring\_Exchange  and deserves further investigation.

In summary, we have found that the interaction between magnetic vortices and nodal quasiparticles in $`d`$-wave superconductors leads to a strong orthogonality catastrophe in response to the motion of half-quantum vortices. This effect strongly suppresses their mobility and is argued to give the dominant contribution to the vortex action at low temperatures. Based on these results, we have developed a simple description of the quantum creep of vortices in $`d`$-wave superconductors. We would like to thank A. Paramekanti, A. Ludwig and M. P. A. Fisher for discussions and criticism.