Structural Resolution with Co-inductive Loop Detection

TL;DR

This paper introduces co-inductive structural resolution, combining co-SLD loop detection with structural resolution, and proves its soundness within logic programming semantics.

Contribution

It presents the operational semantics of co-inductive structural resolution, extending structural resolution with co-induction, and establishes its soundness.

Findings

Operational semantics for co-inductive structural resolution

Proof of soundness with respect to the greatest Herbrand model

Extension of structural resolution with co-inductive capabilities

Abstract

A way to combine co-SLD style loop detection with structural resolution was found and is introduced in this work, to extend structural resolution with co-induction. In particular, we present the operational semantics, called co-inductive structural resolution, of this novel combination and prove its soundness with respect to the greatest complete Herbrand model.

Equations

$$G=\leftarrow A_{\_}1,\dots ,A_{\_}n$$

$$G^{\prime }=\leftarrow (A_{\_}1,\dots ,A_{\_}k-1,B_{\_}1,\dots ,B_{\_}m,A_{\_}k+1,\dots ,A_{\_}n)\theta$$

$$G=\leftarrow (A_{\_}1,S_{\_}1),\dots ,(A_{\_}n,S_{\_}n)$$

$$G^{\prime}={\leftarrow\big{(}(A_{\_}1,S_{\_}1),\ldots,(A_{\_}{k-1},S_{\_}{k-1}),(B_{\_}1,S^{\prime}),\ldots,(B_{\_}m,S^{\prime}),(A_{\_}{k+1},S_{\_}{k+1}),\ldots,(A_{\_}n,S_{\_}n)\big{)}\theta}$$

$$G^{\prime}={\leftarrow\big{(}(A_{\_}1,S_{\_}1),\ldots,(A_{\_}{k-1},S_{\_}{k-1}),(A_{\_}{k+1},S_{\_}{k+1}),\ldots,(A_{\_}n,S_{\_}n)\big{)}\theta}$$

$$T_{\_}^{\prime }P(I)=\{A\in B_{\_}^{\prime }P\mid A\leftarrow A_{\_}1,\dots ,A_{\_}n\text{ is a ground instance of a clause in P and }\{A_{\_}1,\dots ,A_{\_}n\}\subseteq I\}$$

$$G=\leftarrow A_{\_}1,\dots ,A_{\_}n$$

$$G^{\prime }=\leftarrow (A_{\_}1,\dots ,A_{\_}k-1,B_{\_}1,\dots ,B_{\_}m,A_{\_}k+1,\dots ,A_{\_}n)\theta$$

$$G^{\prime }=\leftarrow (A_{\_}1,\dots ,A_{\_}n)\theta$$

$$G=\leftarrow (A_{\_}1,S_{\_}1),\dots ,(A_{\_}n,S_{\_}n)$$

$$G^{\prime }=\leftarrow (A_{\_}1,S_{\_}1),\dots ,(A_{\_}k-1,S_{\_}k-1),(B_{\_}1\theta ,S^{\prime }),\dots ,(B_{\_}m\theta ,S^{\prime }),(A_{\_}k+1,S_{\_}k+1),\dots ,(A_{\_}n,S_{\_}n)$$

$$G^{\prime}={\leftarrow\big{(}(A_{\_}1,S_{\_}1),\ldots,(A_{\_}n,S_{\_}n)\big{)}\theta}$$

$$G^{\prime}={\leftarrow\big{(}(A_{\_}1,S_{\_}1),\ldots,(A_{\_}{k-1},S_{\_}{k-1}),(A_{\_}{k+1},S_{\_}{k+1}),\ldots,(A_{\_}n,S_{\_}n)\big{)}\theta}$$

$$G\stackrel{\text{id}}{\to }G$$

$$G\underset{B}{\overset{\text{rule-1}}{\to }}{G}^{\prime }$$

$$G\sigma \underset{B}{\overset{\text{rule-1}}{\to }}{G}^{\prime }\sigma$$

$$G^{\prime }=\leftarrow (A_{\_}1,S_{\_}1),\dots ,(A_{\_}k-1,S_{\_}k-1),(B_{\_}1\gamma ,S^{\prime }),\dots ,(B_{\_}m\gamma ,S^{\prime }),(A_{\_}k+1,S_{\_}k+1),\dots ,(A_{\_}n,S_{\_}n)$$

$$B_{\_}0\gamma =A_{\_}k$$

$$B_{\_}0{\prec }_{\_}\gamma \sigma A_{\_}k\sigma .$$

$$G\sigma =\leftarrow (A_{\_}1\sigma ,S_{\_}1\sigma ),\dots ,(A_{\_}k\sigma ,S_{\_}k\sigma ),\dots (A_{\_}n\sigma ,S_{\_}n\sigma )$$

$$G\sigma \underset{B}{\overset{\text{rule-1}}{\to }}{G}^{\prime \prime }$$

$$G^{\prime \prime }=\leftarrow (A_{\_}1\sigma ,S_{\_}1\sigma ),\dots ,(A_{\_}k-1\sigma ,S_{\_}k-1\sigma ),(B_{\_}1\gamma \sigma ,S^{\prime \prime }),\dots ,(B_{\_}m\gamma \sigma ,S^{\prime \prime }),(A_{\_}k+1\sigma ,S_{\_}k+1\sigma ),\dots ,(A_{\_}n\sigma ,S_{\_}n\sigma )$$

$$G^{\prime \prime }=G^{\prime }\sigma$$

$$G\underset{{\theta }_{\_}k}{\overset{\text{rule-2}}{\to }}{G}^{\prime }$$

$${\sigma }_{\_}k={\theta }_{\_}k{\theta }_{\_}k+1\cdots {\theta }_{\_}n$$

$$G{\sigma }_{\_}k\stackrel{\text{id}}{\to }{G}^{\prime }{\sigma }_{\_}k+1$$

$$G{\theta }_{\_}k=G^{\prime }$$

$$G{\theta }_{\_}k{\sigma }_{\_}k+1=G^{\prime }{\sigma }_{\_}k+1$$

$${\theta }_{\_}k{\sigma }_{\_}k+1={\sigma }_{\_}k$$

$$G{\sigma }_{\_}k=G^{\prime }{\sigma }_{\_}k+1$$

Full text

1 Introduction

Co-inductive logic programming extends traditional logic programming by enabling co-inductive reasoning to deal with infinite SLD-derivation, which has practical implication in different fields of computing such as model checking, planning as well as type inference [22, 21, 3, 16].

One operational semantics of co-inductive logic programming is co-inductive SLD resolution (co-SLD) [22, 21], which combines loop detection with traditional SLD resolution, so that it can be used to reason co-inductively about infinite rational terms. An alternative operational semantics for co-inductive logic programming is co-algebraic logic programming  [16, 14], which adopts a more general co-induction rule and uses structural resolution instead of SLD resolution as its induction rule.

The distinctive features of co-algebraic logic programming, compared with co-SLD, include that the co-inductive reasoning mechanism of the former goes beyond loop detection; as a result the computed formulae by the former are allowed to be either rational terms or (finite observation of) irrational terms. Moreover, structural resolution [14, 12] allows for analysis of productivity [14] of logic programs. Productivity, also known as computations at infinity [18, ch. 4], concerns computation of infinite data structures by non-terminating derivations. Productivity is studied not only in logic programming community, but also in functional programming community, where they developed decision algorithm for co-recursive list and stream definitions [20, 9]. Those distinctive features make co-algebraic logic programming an ideal basis for developing productivity decision algorithms.

In this paper we explore a combination of co-SLD style loop detection with structural resolution, resulting in a novel operational semantics called co-inductive structural resolution (co-S-resolution for short), and we prove its soundness with respect to the greatest complete Herbrand model. An implementation is also presented as a contribution.

Co-inductive structural resolution is created as an intermediate semantics between co-SLD and co-algebraic logic programming. On the one hand, it inherits loop detection from co-SLD, which is a simpler co-inductive reasoning mechanism compared with the co-inductive mechanism of co-algebraic logic programming. On the other hand, it uses structural resolution as co-algebraic logic programming does, allowing for analysis of productivity. Introducing such an intermediate semantics has its practical implication: there are two challenges involved in the design of productivity decision algorithms, which are 1) productivity analysis with structural resolution and 2) co-inductive reasoning beyond loop detection; introducing the intermediate semantics makes it possible to deal with these two challenges one at a time, so co-S-resolution prepares future development of a productivity decision algorithm that uses loop detection, which in turn will prepare even further algorithm development that goes beyond loop detection. These points will be further discussed in Section 4.

An overview of the rest of the paper is as follows. In Section 2 we will introduce preliminary concepts that cover substitution and unification with rational trees, co-SLD and structural resolution, and greatest fix point, which will prepare us for further theory construction in later sections. In Section 3 we will introduce the semantics for co-inductive structural resolution and prove its soundness. In Section 4 we will have a review of related work, discuss the importance of co-S-resolution for productivity decision, and conclude the paper. Appendix A presents the implementation.

2 Preliminaries

We assume readers’ understanding of standard definition of first order term and the modelling of (possibly infinite) terms by trees. “Term” and “tree” are used interchangeably in this paper. Details about these concepts can be found in [18, 7].

Definition 1** (Rational Term).**

A rational term [6, 11, 4, 22] refers to a (possibly non-ground and possibly infinite) term (or tree) that has a finite amount of distinct sub-terms (or sub-trees). A rational term is also known as a regular term [7, 10].

Our definition for substitution with rational trees (referred to as substitution for short hereinafter) inherits the principle of substitution with finite trees in logic programming [18].

Definition 2** (Substitution).**

A substitution is a mapping of the form $S=\{x_{\_}1/t_{\_}1,\ldots,x_{\_}n/t_{\_}n\}$ where $x_{\_}1,\ldots,x_{\_}n$ are distinct variables, $t_{\_}1,\ldots,t_{\_}n$ are rational terms, and $\forall\ i,j\in\{1,\ldots,n\}$, $x_{\_}i$ does not occur in $t_{\_}j$. Moreover, $\epsilon$ denotes the empty substitution.

Example 2.1**.**

Let $\theta=\{x_{\_}1/f(f(\ldots)),x_{\_}2/g(x_{\_}3)\}$ be a substitution. Applying $\theta$ to the term $p(x_{\_}1,x_{\_}2)$ is denoted by $p(x_{\_}1,x_{\_}2)\theta$, which evaluates to $p(f(f(\ldots)),g(x_{\_}3))$.

Composition of substitutions is defined in the same way as in [18, Sec. 4].

Definition 3** (Unification).**

Given two rational terms $t_{\_}1$ and $t_{\_}2$, unification is the process of finding a substitution (unifier) $\theta$ such that $t_{\_}1\theta=t_{\_}2\theta$, i.e. applying $\theta$ separately to $t_{\_}1$ and $t_{\_}2$ yields the same tree. This relation is denoted by $t_{\_}1\sim_{\_}\theta t_{\_}2$.

The standard approach to rational term unification [19, 7, 6, 8, 24] involves systems of equations of finite terms, and transforms that turn equation systems to their reduced form as the output of the unification algorithm. The reduced form equation system can further be solved to obtain a solution in the domain of rational trees [7]. We omit the details of the unification algorithm for rational trees and the details of solving equation systems, which can be found in the above literature.

Remark*.*

Our definition of substitution refers to solutions of reduced form equation systems. Consider the unification problem $p(X)\sim p(f(X))$. The standard approach regards $p(X)\sim p(f(X))$ as an equation system $\{p(X)=p(f(X))\}$ and reduces it to the reduced form $\{X=f(X)\}$, which is called a substitution in the standard sense. Locally in this paper we solve the reduced form $\{X=f(X)\}$ to obtain the solution $\{X=f(f(\ldots))\}$ and call this solution a substitution. We believe that our treatment of substitution can emphasize the variables that are to be instantiated and will make the theory about co-inductive structure resolution easier to formulate and understand.

Term matching is a concept closely related to unification, and is prerequisite for rewriting reduction in structural resolution [14, 12]. We extend applicable terms for matching from finite trees to rational trees by building the concept of rational tree term matching on the concept of rational tree unification.

Definition 4** (Term Matching).**

Given two rational terms $t_{\_}1$, $t_{\_}2$ and a unifier $\sigma$, if $\sigma$ also satisfies that $t_{\_}1\sigma=t_{\_}2$, then it is said that $t_{\_}1$ subsumes $t_{\_}2$, or $t_{\_}1$ matches against $t_{\_}2$. This relation is denoted by $t_{\_}1\prec_{\_}\sigma t_{\_}2$. $\sigma$ is called a matcher for $t_{\_}1$ against $t_{\_}2$.

Remark* (Uniqueness of matcher).*

If two terms have matchers $\sigma_{\_}1$ and $\sigma_{\_}2$, then $\sigma_{\_}1$ equals to $\sigma_{\_}2$ when restricted to variables that occur in the terms. Nevertheless, a matcher $\sigma$ for term $t_{\_}1$ against $t_{\_}2$ is intended to be identity on variables not in $t_{\_}1$.

The symbolic notation for unification ($\sim$) and matching ($\prec$) follows [14]. Note that ($\sim$) is a symmetric relation but ($\prec$) is not symmetric. Sometimes $t_{\_}1\prec t_{\_}2$ may fail to convey which term subsumes (i.e. matches against) which. A mnemonic tip is to regard the “precede” symbol ($\prec$) as the “less than” symbol ($<$) and derive from $t_{\_}1\prec t_{\_}2$ that $t_{\_}2$ might be bigger (i.e. contains more symbols) than $t_{\_}1$.

Example 4.1**.**

1. a)

$p(x)\sim_{\_}\theta p(f(x))$ where $\theta=\{x/f(f(f(\ldots)))\}$. $\theta$ is not a matcher. 2. b)

$p(x_{\_}1,x_{\_}1)\sim_{\_}\theta p(f(y_{\_}1),y_{\_}1)$ where $\theta=\{x_{\_}1/f(f(f(\ldots))),y_{\_}1/f(f(f(\ldots)))\}$. $\theta$ is not a matcher. 3. c)

$p(x_{\_}1,x_{\_}2)\sim_{\_}\theta p(f(y_{\_}1),y_{\_}1)$ where $\theta=\{x_{\_}1/f(y_{\_}1),x_{\_}2/y_{\_}1\}$. $\theta$ is a matcher and $p(x_{\_}1,x_{\_}2)\prec_{\_}\theta p(f(y_{\_}1),y_{\_}1)$.

We now introduce the operational semantics of the well-known SLD-resolution ($\mathbf{L}$inear resolution for $\mathbf{D}$efinite clauses with $\mathbf{S}$election function) [18, 23] as a precursor of co-SLD and of structural resolution.

Definition 5** (SLD-resolution).**

Given a logic program P and goal

[TABLE]

if there exists in P a clause $B_{\_}0\leftarrow B_{\_}1,\ldots,B_{\_}m$ (with freshly renamed variables), such that $B_{\_}0\sim_{\_}\theta A_{\_}k$ for some $k\in\{1,\ldots,n\}$, then by SLD-resolution we derive

[TABLE]

Remark*.*

The notation of the form $(A_{\_}1,\ldots,A_{\_}n)\theta$ denotes application of $\theta$ to every $A_{\_}i,\ i\in\{1,\ldots,n\}$.

In the following definition of co-SLD we introduce a set $S$ for each predicate $A$ in a goal [4], where $S$ records all previous goals (or their instances) that are relevant to the co-inductive proof of $A$.

Definition 6** (co-SLD resolution).**

Given a logic program P and a goal

[TABLE]

the next goal $G^{\prime}$ can be derived by one of the following two rules:

If there exists in P a clause $B_{\_}0\leftarrow B_{\_}1,\ldots,B_{\_}m$ (with freshly renamed variables), such that $B_{\_}0\sim_{\_}\theta A_{\_}k$ for some $k\in\{1,\ldots,n\}$, then let $S^{\prime}=S_{\_}k\cup\{A_{\_}k\}$, we derive

[TABLE] 2. 2.

(Loop Detection) If $A_{\_}k\sim_{\_}\theta B$ for some $k\in\{1,\ldots,n\}$ and some $B\in S_{\_}k$, we derive

[TABLE]

Remark*.*

The notation of the form \big{(}(A_{\_}1,S_{\_}1),\ldots,(A_{\_}n,S_{\_}n)\big{)}\theta denotes application of $\theta$ to every $A_{\_}i$ and to every member of every $S_{\_}i$, $i\in\{1,\ldots,n\}$.

Definition 7** (co-SLD Derivation/Refutation).**

A co-SLD derivation consists of a possibly infinite sequence of goals $G_{\_}0,G_{\_}1,\ldots$ where $G_{\_}0$ is of the form $\leftarrow(A_{\_}1,\emptyset),\ldots,(A_{\_}m,\emptyset)\ (m\geq 0)$, and for all $i\geq 0$, $G_{\_}{i+1}$ is derived from $G_{\_}i$ using co-SLD resolution. A finite co-SLD derivation ending with the empty goal is called an co-SLD refutation111Logic programming works by refuting the goal, which is the negation of the proposition that is to be proven. .

Definition 8** (Computed Substitution).**

Given a co-SLD refutation $\mathcal{D}$, let $\theta_{\_}1,\theta_{\_}2,\ldots,\theta_{\_}n$ be the sequence of unifiers computed in $\mathcal{D}$ in the same order as they were computed, their composition $\theta_{\_}1\theta_{\_}2\cdots\theta_{\_}n$ is called the computed substitution from $\mathcal{D}$.

Co-SLD is co-inductively sound [4, 22]. Co-inductive soundness is defined in terms of the greatest complete Herbrand model. We assume the standard definition of complete Herbrand interpretation and complete Herbrand base [18, Sec. 25], which, compared with Herbrand interpretation/base, allow for infinite ground terms and atoms in addition to finite ones.

Definition 9** ($T^{\prime}_{\_}P$ operator).**

Let P be a logic program and $B^{\prime}_{\_}P$ be P’s complete Herbrand base. The complete immediate consequence operator $T^{\prime}_{\_}P:\ 2^{B^{\prime}_{\_}P}\mapsto 2^{B^{\prime}_{\_}P}$ is defined as follows. Let $I\subseteq B^{\prime}_{\_}P$ be a complete Herbrand interpretation. Then

[TABLE]

Definition 10** (Greatest complete Herbrand model).**

Let P be a program. The greatest fix point $\text{gfp}(T^{\prime}_{\_}P)=\cup\{I\mid I\subseteq T^{\prime}_{\_}P(I)\}$ of $T^{\prime}_{\_}P$ is called the greatest complete Herbrand model of P.

More details on $T^{\prime}_{\_}P$ operator and its fix points can be found in e.g. [18, Sec. 26]. We now justify the loop detection rule of co-SLD with an example.

Example 10.1**.**

Consider the following program P which defines co-recursively all streams of 0’s and 1’s.

bit(0)$\leftarrow$

bit(1)$\leftarrow$

bit-stream(cons(X,Xs)) $\leftarrow$ bit(X), bit-stream(Xs)

The co-SLD refutation for goal $\leftarrow$bit-stream(cons(0,Xs)), following the left-first computation rule, is finished by one step of loop detection which unifies bit-stream(Xs) and bit-stream(cons(0,Xs)) with unifier $\theta$={Xs/cons(0,cons(0,…))}. Note that

bit-stream(cons(0,Xs)) $\leftarrow$ bit(0), bit-stream(Xs) (*)

is an instance of the program clause, to which we can apply unifier $\theta$ and we get another program clause instance

bit-stream(cons(0,cons(0,…))) $\leftarrow$ bit(0), bit-stream(cons(0,cons(0,…))) (**)

We regard () and (**) as proof trees [5, Sec. 1.6], and notice that applying the loop detection rule extends () into (), whose set $I$ of nodes satisfies $I\subseteq T^{\prime}_{\_}P(I)$, therefore $I$ is a subset of gfp($T^{\prime}_{\_}P$). The establishment of the relation $I\subseteq T^{\prime}_{\_}P(I)$ is mainly due to the reasoning that for each atom $A\in I$ (or, for each node $A$ of proof tree ()), there exists a program clause instance whose head is $A$, and whose body is a subset of $I$, so that if $A$ is in $I$, then $A$ is in $T^{\prime}_{\_}P(I)$, indicating $I\subseteq T^{\prime}_{\_}P(I)$. Such reasoning applies to all co-SLD refutation that involves use of loop detection.

Definition 11** (Structural Resolution).**

Given a logic program P and goal

[TABLE]

the next goal $G^{\prime}$ is derived using one of the following two rules:

(Rewriting Reduction) If there exists in P a clause $B_{\_}0\leftarrow B_{\_}1,\ldots,B_{\_}m$ (with freshly renamed variables), such that $B_{\_}0\prec_{\_}\theta A_{\_}k$ for some $k\in\{1,\ldots,n\}$, then we derive

[TABLE] 2. 2.

(Substitution Reduction) If there exists in P a clause $B_{\_}0\leftarrow B_{\_}1,\ldots,B_{\_}m$ (with freshly renamed variables), such that $B_{\_}0\sim_{\_}\theta A_{\_}k$ but not $B_{\_}0\prec_{\_}\theta A_{\_}k$ for some $k\in\{1,\ldots,n\}$, then we derive

[TABLE]

Remark*.*

About rewriting reduction, notice that it is a special case of SLD-resolution, and since matcher $\theta$ only instantiates variables from the renamed clause $B_{\_}0\leftarrow B_{\_}1,\ldots,B_{\_}m$ without instantiating variables from goal $G$, the derived goal $G^{\prime}$ can also be written as $G^{\prime}={\leftarrow A_{\_}1,\ldots,A_{\_}{k-1},(B_{\_}1,\ldots,B_{\_}m)\theta,A_{\_}{k+1},\ldots,A_{\_}n}$. About substitution reduction, notice that it is, by nature, instantiation of universal quantifier.

Definition 12** (S-Derivation/Refutation).**

A structural resolution derivation (S-derivation for short) consists of a possibly infinite sequence $G_{\_}0,G_{\_}1,\ldots$ of goals such that for all $i\geq 0$, $G_{\_}{i+1}$ is derived from $G_{\_}i$ using structural resolution, without consecutive use of substitution reduction. A finite S-derivation ending with the empty goal is called an S-refutation.

Definition 13** (Computed Substitution).**

Given a S-refutation $\mathcal{D}$, let $\theta_{\_}1,\theta_{\_}2,\ldots,\theta_{\_}n$ be the sequence of unifiers computed in $\mathcal{D}$ due to application of substitution reduction, sorted in the same order as they were computed, their composition $\theta_{\_}1\theta_{\_}2\cdots\theta_{\_}n$ is called the computed substitution from $\mathcal{D}$.

Example 13.1**.**

Consider the program:

[TABLE]

Given goal $\leftarrow p(X),r(X)$ the next goal is $\leftarrow p(f(X_{\_}1)),r(f(X_{\_}1))$ by substitution reduction on $p(X)$ (with renamed clause $p(f(X_{\_}1))\leftarrow q(X_{\_}1)$ and unifier $\theta_{\_}1=\{X/f(X_{\_}1)\}$), then the next goal is $\leftarrow q(X_{\_}1),r(f(X_{\_}1))$ by rewriting reduction on $p(f(X_{\_}1))$ (with renamed clause $p(f(X_{\_}2))\leftarrow q(X_{\_}2)$ and matcher $\{X_{\_}2/X_{\_}1\}$), then the next goal is $\leftarrow q(a),r(f(a))$ by substitution reduction on $q(X_{\_}1)$ (with unifier $\theta_{\_}2=\{X_{\_}1/a\}$). Two more steps of rewriting reduction derive the empty goal $\leftarrow$ which terminates successfully the resolution and the computed substitution is the composition $\theta_{\_}1\theta_{\_}2=\{X/f(a),X_{\_}1/a\}$.

For more details on structural resolution, see [14, 12, 16]. Next we introduce the combination of structural resolution and co-SLD style loop detection.

3 Co-inductive Structural Resolution

We introduce the declarative and operational semantics of co-inductive structural resolution. For the operational semantics we introduce how it was formulated and prove its co-inductive soundness.

3.1 Declarative Semantics

The declarative semantics of co-inductive structural resolution is chosen to be the greatest fixed point over the complete Herbrand base [18, ch. 4][24], as for co-SLD [22, 21, 4]. In fact, it was a conjecture [13] that some form of combination of structural resolution and loop detection is correct w.r.t. the greatest complete Herbrand model as co-SLD is, since they share the same co-induction mechanism and their inductive components (structural resolution and SLD resolution, respectively) are both sound and complete w.r.t. the least Herbrand model [14].

3.2 Operational Semantics

The implementation presented in Appendix A played important role in formulation of the operational semantics. The implementation was created by integrating existing implementation of structural resolution [17] and co-SLD [2], which showed plausible behaviour. So the implementation was then abstracted to obtain the operational semantics, whose soundness was later proved. The upshot is that the implementation had come before the formulation of the operational semantics, but was then verified as the soundness of the operational semantics was proved. In this section we present the operational semantics.

Definition 14** (Co-inductive Structural Resolution).**

Given a logic program P and goal

[TABLE]

the next goal $G^{\prime}$ can be derived by one of the following three rules:

(Rewriting Reduction) If there exists in P a clause $B_{\_}0\leftarrow B_{\_}1,\ldots,B_{\_}m$ (with freshly renamed variables), such that $B_{\_}0\prec_{\_}\theta A_{\_}k$ for some $k\in\{1,\ldots,n\}$, then let $S^{\prime}=S_{\_}k\cup\{A_{\_}k\}$, we derive

[TABLE] 2. 2.

(Substitution Reduction) If there exists in P a clause $B_{\_}0\leftarrow B_{\_}1,\ldots,B_{\_}m$ (with freshly renamed variables), such that $B_{\_}0\sim_{\_}\theta A_{\_}k$ but not $B_{\_}0\prec_{\_}\theta A_{\_}k$ for some $k\in\{1,\ldots,n\}$, then we derive

[TABLE] 3. 3.

(Loop Detection) If $A_{\_}k\sim_{\_}\theta B$ for some $k\in\{1,\ldots,n\}$ and some $B\in S_{\_}k$, we derive

[TABLE]

Notice that the Loop Detection rule for co-inductive structural resolution is the same as its counterpart in co-SLD, and rule-1 of co-inductive structural resolution is a special case of rule-1 of co-SLD.

Definition 15** (co-S-Derivation/Refutation).**

A co-inductive structural resolution derivation is a possibly infinite sequence $G_{\_}0,G_{\_}1,\ldots$ where $G_{\_}0$ is of the form $\leftarrow(A_{\_}1,\emptyset),\ldots,(A_{\_}m,\emptyset)\ (m\geq 0)$, and for all $i\geq 0$, $G_{\_}{i+1}$ is derived from $G_{\_}i$ by co-S-resolution without consecutive use of substitution reduction. A finite co-S-derivation ending with the empty goal is called a co-S-refutation.

Definition 16** (Computed Substitution).**

Given a co-S-refutation $\mathcal{D}$, let $\theta_{\_}1,\theta_{\_}2,\ldots,\theta_{\_}n$ be the sequence of unifiers computed in $\mathcal{D}$ due to application of rule-2 or rule-3, sorted in the same order as they were computed, their composition $\theta_{\_}1\theta_{\_}2\cdots\theta_{\_}n$ is called the computed substitution from $\mathcal{D}$.

Example 16.1**.**

Consider program:

[TABLE]

In the following co-S-refutation, for each goal we always select the left most predicate to resolve.

1. Goal 1:

\leftarrow\big{(}q(X),\emptyset\big{)} 2. Goal 2:

\leftarrow\big{(}p(X),\{q(X)\}\big{)},\big{(}r(X),\{q(X)\}\big{)} (rule-1. $q(X_{\_}1)\leftarrow p(X_{\_}1),r(X_{\_}1).~{}\{X_{\_}1/X\}$) 3. Goal 3:

\leftarrow\big{(}p(s(X_{\_}2)),\{q(s(X_{\_}2))\}\big{)},\big{(}r(s(X_{\_}2)),\{q(s(X_{\_}2))\}\big{)} (rule-2. $p(s(X_{\_}2))\leftarrow q(X_{\_}2).~{}\theta_{\_}1=\{X/s(X_{\_}2)\}$) 4. Goal 4:

\leftarrow\big{(}q(X_{\_}2),\{p(s(X_{\_}2)),q(s(X_{\_}2))\}\big{)},\big{(}r(s(X_{\_}2)),\{q(s(X_{\_}2))\}\big{)} (rule-1. $p(s(X_{\_}3))\leftarrow q(X_{\_}3).~{}\{X_{\_}3/X_{\_}2\}$) 5. Goal 5:

\leftarrow\big{(}r(s(s(s(\ldots)))),\{q(s(s(s(\ldots))))\}\big{)} (rule-3. $q(X_{\_}2)\sim_{\_}{\theta_{\_}2}q(s(X_{\_}2)).~{}\theta_{\_}2=\{X_{\_}2/s(s(s(\ldots)))\}$) 6. Goal 6:

$\leftarrow$ (rule-1. $r(X_{\_}4)\leftarrow.~{}\{X_{\_}4/s(s(s(\ldots)))\}$)

The answer to Goal 1 is given by computed substitution $\theta_{\_}1\theta_{\_}2=\{X/s(s(s(\ldots))),X_{\_}2/s(s(s(\ldots)))\}$. Loop detection is used once for reduction from Goal 4 to Goal 5, and predicate $q(X_{\_}2)$ in Goal 4 is co-inductively proved.

3.3 Soundness Proof

In this section, the main result shows that given a goal $G$, if there is a co-S-refutation for $G$, with computed substitution $\sigma$, then there is a co-SLD refutation for $G\sigma$, with computed substitution $\epsilon$ (i.e. the empty substitution). Therefore if co-SLD is sound, then $G\sigma\epsilon=G\sigma$ is in the greatest complete Herbrand model, meaning that co-S-resolution is also sound.

We will define a transformation algorithm that step-by-step transforms a co-S-refutation of goal $G$ into a co-SLD refutation of goal $G\sigma$. The transformation is via an intermediate derivation, called co-rewriting-id derivation, which simply consists of co-SLD resolution steps interleaved with identity reduction steps (c.f. Definition 17). So given a co-S-refutation, it will be firstly transformed into a co-rewriting-id refutation, which will then be trivially transformed into a co-SLD refutation. The transformation from a co-S-refutation to a co-rewriting-id refutation is done during a sequential traverse of the co-S-refutation, starting from the initial goal. According to the three lemmas (i.e. Lemma 1, 2 and 3, defined later), each goal reduction step in the co-S-refutation establishes a co-rewriting-id reduction step, and all co-rewriting-id reduction steps established during the traverse form the co-rewriting-id refutation. The following are details of the proof.

Definition 17** (Identity Reduction).**

Given some goal $G$, the reduction from $G$ to itself, is called identity reduction, denoted by

[TABLE]

Definition 18** (co-Rewriting-ID Resolution).**

Given a program and some goal $G$, the next goal $G^{\prime}$ can be derived from $G$ using one of following three rules:

The same as rule 1 in Definition 14. 2. 2.

Identity reduction. 3. 3.

The same as rule 3 in Definition 14.

Definition 19** (co-Rewriting-ID Derivation/Refutation).**

A co-rewriting-id derivation is a possibly infinite sequence $G_{\_}0,G_{\_}1,\ldots$ where $G_{\_}0$ is of the form $\leftarrow(A_{\_}1,\emptyset),\ldots,(A_{\_}m,\emptyset)\ (m\geq 0)$, and for all $i\geq 0$, $G_{\_}{i+1}$ is derived from $G_{\_}i$ by co-rewriting-id resolution without consecutive use of identity reduction. A finite co-rewriting-id derivation ending with the empty goal is called a co-rewriting-id refutation.

Definition 20** (Computed Substitution).**

Given a co-rewriting-id refutation $\mathcal{D}$, let $\theta_{\_}1,\theta_{\_}2,\ldots,\theta_{\_}n$ be the sequence of unifiers computed in $\mathcal{D}$ due to application of rule-3, sorted in the same order as they were computed, their composition $\theta_{\_}1\theta_{\_}2\cdots\theta_{\_}n$ is called the computed substitution from $\mathcal{D}$.

Proposition 1**.**

Given a program, for any goal $G$, if there is a co-rewriting-id refutation for $G$ with computed substitution $\theta$, then there is a co-SLD refutation for $G$ with the same computed substitution $\theta$.

Proof.

Suppose $\mathcal{D}=G_{\_}0,\ldots,G_{\_}n$ is a co-rewriting-id refutation for $G=G_{\_}0$ with computed substitution $\theta$. By simultaneously removing from $\mathcal{D}$ all $G_{\_}{i+1}\ (i\in[0,n-1])$ such that $G_{\_}i\xrightarrow{\textrm{id}}G_{\_}{i+1}$, the resulting derivation $\mathcal{D^{\prime}}$ constitutes a co-SLD derivation with computed substitution $\theta$. Moreover, $\mathcal{D^{\prime}}$ is a special case of co-SLD derivation since Definition 18-rule 1 is a special case of Definition 6-rule 1. ∎

Theorem 1**.**

Given a program, for any goal $G$, if there is a co-S-refutation for $G$ with computed substitution $\sigma$, then there is a co-rewriting-id refutation for $G\sigma$ with computed substitution $\epsilon$ (the empty substitution).

The proof of Theorem 1 is based on properties of co-inductive structural resolution rules, formulated in the following three lemmas.

Lemma 1** (Rewriting Preservation).**

Let

[TABLE]

be a goal reduction using rule-1 (as defined in Definition 14), and $B$ the program clause involved in the reduction.

Then for any substitution $\sigma$, it holds that

[TABLE]

Proof.

Assume

• •

$G={\leftarrow(A_{\_}1,S_{\_}1),\ldots,(A_{\_}k,S_{\_}k),\ldots,(A_{\_}n,S_{\_}n)}$ and

• •

$B$ has the form $B_{\_}0\leftarrow B_{\_}1,\ldots,B_{\_}m\ (m\geq 0)$ and

• •

$B_{\_}0\prec_{\_}\gamma A_{\_}k$, for some $k\in[1,n]$.

By Definition 14, rule-1,

[TABLE]

where $S^{\prime}=S_{\_}k\cup\{A_{\_}k\}.$

Since $B_{\_}0\prec_{\_}\gamma A_{\_}k$ (by the above assumption), it means (by Definition 4) that

[TABLE]

Then for all $\sigma$, if we apply $\sigma$ to both sides of (2), we have $B_{\_}0\gamma\sigma=A_{\_}k\sigma$, which means (by associativity of substitution [18, Sec. 4] and Definition 4) that

[TABLE]

Now consider $G\sigma$, by notational convention,

[TABLE]

Because of (3) and (4), we can have reduction

[TABLE]

where, by Definition 14, rule-1,

[TABLE]

where $S^{\prime\prime}=S_{\_}k\sigma\cup\{A_{\_}k\sigma\}.$

Compare (1) and (6), we have, by notational convention,

[TABLE]

By (5) and (7), we reach the conclusion of Lemma 1. ∎

Hereinafter we adopt the following notation for substitution compositions. Given a sequence of substitutions $\theta_{\_}1,\theta_{\_}2,\ldots,\theta_{\_}n$, for all $k\in\{1,\ldots,n\}$, let $\sigma_{\_}k$ denote the composition $\theta_{\_}k\theta_{\_}{k+1}\cdots\theta_{\_}n$. For example, let $\theta_{\_}1,\theta_{\_}2,\theta_{\_}3,\theta_{\_}4$ be a sequence of 4 substitutions, then $\sigma_{\_}1=\theta_{\_}1\theta_{\_}2\theta_{\_}3\theta_{\_}4$, $\sigma_{\_}2=\theta_{\_}2\theta_{\_}3\theta_{\_}4$, $\sigma_{\_}3=\theta_{\_}3\theta_{\_}4$ and $\sigma_{\_}4=\theta_{\_}4$.

Lemma 2** (Instantiation Preservation).**

Let

[TABLE]

be a goal reduction using rule-2 (as defined in Definition 14), where $\theta_{\_}k$ is the unifier involved in the reduction, and let

[TABLE]

for some $n>k$ and some (arbitrary and possibly $\epsilon$) substitutions $\theta_{\_}{k+1},\ldots,\theta_{\_}n$.

Then

[TABLE]

Remark*.*

The sequence of $\theta$’s in Lemma 2 will come from co-S-resolution steps when Lemma 2 is used to prove Theorem 1.

Proof.

From the premise of Lemma 2, we have

[TABLE]

Applying $\sigma_{\_}{k+1}(=\theta_{\_}{k+1}\cdots\theta_{\_}n)$ to both sides of (8) we have

[TABLE]

Note that in (9)

[TABLE]

therefore by associativity of substitution, (9) can be written as

[TABLE]

hence the identity reduction $G\sigma_{\_}k\xrightarrow{\ \textrm{id}\ }G^{\prime}\sigma_{\_}{k+1}$. ∎

Lemma 3** (Loop Detection Preservation).**

Let

[TABLE]

be a goal reduction using rule-3 (as defined in Definition 14), where $\theta_{\_}k$ is the unifier involved in the reduction, and let

[TABLE]

for some $n>k$ and some (arbitrary and possibly $\epsilon$) substitutions $\theta_{\_}{k+1},\ldots,\theta_{\_}n$.

Then

[TABLE]

Proof.

Assume

[TABLE]

and

[TABLE]

for some $k\in[1,n]$ and some

[TABLE]

By Definition 14, rule-3,

[TABLE]

From (11) and Definition 3,

[TABLE]

Applying $\sigma_{\_}{k+1}(=\theta_{\_}{k+1}\cdots\theta_{\_}n)$ to both sides of (14), we have $A_{\_}k\theta_{\_}k\sigma_{\_}{k+1}=B\theta_{\_}k\sigma_{\_}{k+1}$, then due to $\sigma_{\_}k=\theta_{\_}k\sigma_{\_}{k+1}$ and associativity of substitution,

[TABLE]

which means

[TABLE]

Consider $G\sigma_{\_}k$, which can be written as

[TABLE]

Due to (12), it holds that

[TABLE]

From (16) and (18), $G\sigma_{\_}k$ as in (17) can be reduced using Definition 14 rule 3, resulting in

[TABLE]

which can be rewritten in a simpler form

[TABLE]

The reduction of $G\sigma_{\_}k$ is denoted by

[TABLE]

Comparing (13) with (19), we conclude, by associativity of substitution, that

[TABLE]

and with (20) we reach the conclusion of Lemma 3. ∎

Next we give an algorithm that outputs co-rewriting-id refutations, giving a co-S-refutation as input. This algorithm constitutes our proof of Theorem 1 and we will provide an example to demonstrate the algorithm at work.

Proof of Theorem 1.

Given a goal $G=G_{\_}0$, assume $\mathcal{D}=G_{\_}0,\ldots,G_{\_}n$ is a co-S-derivation, and $\theta_{\_}1,\ldots\theta_{\_}m$ is the sequence of unifiers computed during derivation $\mathcal{D}$ due to the use of Definition 14 rule 2 or 3. Let $\theta_{\_}{m+1}=\epsilon$ so $\sigma_{\_}1=\theta_{\_}1,\ldots\theta_{\_}m\theta_{\_}{m+1}$ is the computed substitution for goal $G$.

Definition 14 is the default domain when we mention rule 1,2 or 3 in this proof. We build the co-rewriting-id derivation $\mathcal{D^{\prime}}$ of $G\sigma_{\_}1$ using the following algorithm.

For each $i\in\{0,\ldots,n-1\}$, starting from $i=0$ and in the ascending order of $i$, (*)

• •

If

[TABLE]

then write down, by Lemma 1,

[TABLE]

where

[TABLE]

$x$ is well-defined in the second case because of the condition (*).

• •

If

[TABLE]

then write down, by Lemma 2,

[TABLE]

• •

If

[TABLE]

then write down, by Lemma 3,

[TABLE]

∎

Remark*.*

Compare the specific co-S-refutation for goal $G_{\_}0$, which has computed substitution $\sigma_{\_}1=\theta_{\_}1\theta_{\_}2\theta_{\_}3\theta_{\_}4$ where $\theta_{\_}4=\epsilon$, with the co-rewriting-id refutation for goal $G_{\_}0\sigma_{\_}1$ generated by the algorithm.

[TABLE]

Theorem 2** (Soundness).**

Co-inductive structural resolution is sound with respect to the greatest complete Herbrand model. In other words, if a goal $G$ has a co-S-derivation with computed substitution $\sigma$, then $G\sigma$ is in the greatest model.

Proof.

Given a program and some goal $G$, assume $G$ has a co-S-derivation with computed substitution $\sigma$. By Theorem 1 $G\sigma$ has a co-rewriting-id derivation with computed substitution $\epsilon$, then by Proposition 1 $G\sigma$ has a co-SLD derivation with computed substitution $\epsilon$. Since co-SLD is sound with respect to the greatest complete Herbrand model, $G\sigma\epsilon=G\sigma$ is in the model. ∎

4 Related Work and Conclusion

Existing soundness proof for co-SLD helped this work. A soundness proof of co-SLD, based on co-induction, is provided in [21], in which it was established by a lemma that if some goal $G$ has co-SLD derivation with computed substitution $\sigma$, then $G\sigma$ also has a co-SLD derivation. This idea inspired the author to explore if a goal has a co-S-derivation, whether there is also a co-S-derivation for the same goal with computed answer applied. Another soundness proof of co-SLD is given in [4], which is based on the theory of infinite tree logic programming formulated in [11]. The infinite tree derivation proposed in [11] selects all sub-goal altogether rather than one sub-goal at a time, and it is sound with respect to the greatest model. In [4] the soundness of co-SLD is proved by showing that any co-SLD derivation can be unfolded into an infinite tree derivation, therefore the soundness of co-SLD derivation is backed by the soundness of infinite tree derivation. Our proof in this paper obviously is inspired by such technique in [4], which relates different derivations and reuses previous results.

As a by-product of our proof, we can use the same arguments to show that soundness and completeness of structural resolution can be proved based on soundness and completeness of SLD resolution. For soundness, if a goal $G$ has a successful structural resolution derivation with computed substitution $\sigma$, then $G\sigma$ has a successful rewriting-id derivation, which is a special case of SLD derivation. For completeness, it needs to be shown that every SLD derivation has a corresponding structural resolution derivation, by splitting each non-rewriting step in SLD derivation into one step of substitution reduction followed by one step of rewriting reduction.

Future work will involve development of a productivity semi-decision algorithm based on co-inductive structural resolution. Now we have a sketch of the role that will be played by co-S-resolution. Given a non-terminating SLD derivation, necessarily some (maybe none) of its SLD resolution steps are rewriting reductions. A class of programs are characterized for their termination for rewriting [14, 15], called observationally productive programs. Since all consecutive rewriting steps are finite for such programs, in a non-terminating SLD derivation of some observationally productive program, there necessarily are infinite steps of non-rewriting SLD resolution steps. This fact will be crucial for productivity analysis since only non-rewriting steps can produce unifiers that may accumulate and instantiate the original goal into an infinite tree at infinity. Since the notion of productivity relies on rewriting reduction, productivity analysis is made easier by S-resolution compared with using SLD resolution; hence the advantage of structural resolution over SLD resolution. Moreover, loop detection needs to be combined with S-resolution to serve as a finite implementation of non-terminating productive S-derivations; finding a way for such a combination, proving its co-inductive soundness, and implementing it, are the contributions of this paper.

Acknowledgement

I would like to thank my supervisor Dr. Ekaterina Komendantskaya for her support and discussion. I would like to thank Dr. Joe Wells and anonymous reviewers for their constructive comments.

Appendix A Implementation of Co-Inductive Structural Resolution

SWI-Prolog (Multi-threaded, 64 bits, Version 7.2.3)

http://www.swi-prolog.org

%--------------------------------------------------------- clause_tree(true,_) :- !. clause_tree((G,R), Hypo) :- !, % Note 1 clause_tree(G, Hypo), clause_tree(R, Hypo).

clause_tree(A,Hypo) :- find_loop(A,Hypo).

clause_tree(A, Hypo) :- % rewriting reduction unifying_and_matching_rule(A, Body), clause_tree(Body, [A|Hypo]). % Note 2

clause_tree(A, Hypo) :- % substitution reduction. unifying_not_matching_rule(A, _), clause_tree(A, Hypo). % Note 3

%--------------------------------------------------------- find_loop(A,[B|]) :- A = B. find_loop(A,[|C]) :- find_loop(A,C).

% choose clauses whose heads unifies with the goal, % and specifically, matches the goal. unifying_and_matching_rule(A, Body) :- copy_term(A,A_copy), % Note 4 clause(A_copy,,Ref), % Note 5 clause(A1,,Ref), % Note 6 subsumes_term(A1,A), % Note 7 clause(A,Body,Ref). % Note 8

% choose clauses whose head unifies with the goal, % and specifically, does not match the goal. unifying_not_matching_rule(A, Body) :- copy_term(A,A_copy), clause(A_copy,,Ref), clause(A1,,Ref), + subsumes_term(A1,A), clause(A,Body,Ref). %--------------------------------------------------------

1. Note 1

Clauses deal with mutually exclusive cases, hence the cuts. 2. Note 2

A is not instantiated by finding a matching clause. 3. Note 3

A is instantiated by finding a unifying but not matching clause. 4. Note 4

At run time variable A is bound to the current (atomic sub-)goal $G$, A_copy then is a variant $\acute{G}$ of $G$ with fresh variables. Built-in copy_term/2 is used to make a copy of $G$ to use in the next procedure clause(A_copy,_,Ref) to search for a unifying rule without instantiating variables from $G$. 5. Note 5

At run time, this procedure finds some clause whose head unifies with the variant $\acute{G}$ of the current (atomic sub-)goal $G$ and get the clause’s reference number $n$ that is bound to Ref. The term $\acute{G}$ bound to A_copy may be instantiated. The body of the found clause, which may be instantiated, is discarded as indicated by “_”. 6. Note 6

Use the reference number Ref to get a copy of the found clause by the previous procedure ‘clause(A_copy,,Ref)’. Only the head, which is bound to A1, of the clause is needed for subsumes check, and the body of the clause is discarded as shown by ‘’. 7. Note 7

Term matching is checked by using built-in predicate subsumes_term/2, which does not instantiate variables. Any binding made for subsumes check will be undone by implementation of subsumes_term/2. 8. Note 8

If the subsumes check is passed by the found unifying clause, then use a fresh copy of this particular clause, as specified by Ref, to reduce the goal. Variables in the term $t$ bound to A will not be instantiated because the clause head subsumes $t$ as has been checked, but variables in the body of the clause, which is bound to Body, are instantiated by sub-terms from $t$.

One of the anonymous reviewers of this paper suggested that

“The two clauses for rewriting and substitution reduction can be merged into a single one to make the interpreter more compact and efficient (but maybe a bit less readable).”

And he/she suggested the following code:

clause_tree(A, Hypo) :- copy_term(A,A_copy), clause(A_copy,,Ref), clause(A1,,Ref), subsumes_term(A1,A) *-> clause(A,Body,Ref), clause_tree(Body, [A|Hypo]) ; clause(A,Body,Ref), clause_tree(A, Hypo).

% Example object programs % ------------------------- % trace: clause_tree(a,[]) a :- a1,a2. a1 :- b1,b2. b1 :- c1,c2. a2. b2. c1. c2. %-------------------------- % trace: clause_tree(p(X),[]). p(s(X)) :- p(X),p(X). % non-linear co-recursion %-------------------------- % trace: clause_tree(cond_f(X),[]). cond_c(s(a)). cond_e(s()). cond_f(X) :- cond_e(X),cond_c(X). %-------------------------- % trace: clause_tree(q(X),[]). r(). p(s(X)) :- q(X). q(X) :- p(X),r(X).