Under consideration for publication in Formal Aspects of Computing

Operational Semantics of Resolution
and Productivity in Horn Clause
Logic
Peng Fu1 and Ekaterina Komendantskaya1
1 Heriot-Watt University, Edinburgh, UK

Abstract. This paper presents a study of operational and type-theoretic properties of different resolution
strategies in Horn clause logic. We distinguish four different kinds of resolution: resolution by unification(SLD-resolution), resolution by term-matching, the recently introduced structural resolution, and partial (orlazy) resolution. We express them all uniformly as abstract reduction systems, which allows us to undertakea thorough comparative analysis of their properties. To match this small-step semantics, we propose to take
Howard’s System H as a type-theoretic semantic counterpart. Using System H, we interpret Horn formulas
as types, and a derivation for a given formula as the proof term inhabiting the type given by the formula.
We prove soundness of these abstract reduction systems relative to System H, and we show completeness of
SLD-resolution and structural resolution relative to System H. We identify conditions under which structural
resolution is operationally equivalent to SLD-resolution. We show correspondence between term-matching
resolution for Horn clause programs without existential variables and term rewriting.
Keywords: Logic Programming, Typed Lambda Calculus, Reduction Systems, Structural Resolution,
Termination, Productivity.

1. Introduction
Horn clause logic is a fragment of first-order logic that gives theoretical foundation to logic programming.
A set of Horn clauses is called a logic program. SLD-resolution is the most common algorithm in logic
programming for automatically inferring whether, given a logic program Φ and a first-order formula A,Φ ` σA holds for some substitution σ. SLD-resolution is semi-decidable as not all derivations by SLDresolution terminate. Terminating SLD-resolution is quite well understood (see for example the textbook by
Lloyd [Llo87]), and SLD-resolution has been successfully incorporated into a number of logic programming
language implementations. However, nonterminating SLD-resolution is more challenging to handle.
Example 1. Consider the following logic program defining the infinite stream of zeros. It consists of one
Horn clause:κ1 : ∀y.Stream(y) ⇒ Stream(Cons(0, y))
For query Stream(x), it gives rise to the following SLD-derivation:
Correspondence and offprint requests to: Peng Fu, e-mail: peng-fu@uiowa.edu, Ekaterina Komendantskaya, e-mail:ek19@hw.ac.uk

2

P. Fu and E. KomendantskayaΦ ` {Stream(x)} κ1 ,[Cons(0,y1 )/x] {Stream(y1 )} κ1 ,[Cons(0,y2 )/y1 ,Cons(0,Cons(0,y2 ))/x]{Stream(y2 )} κ1 ,[Cons(0,y3 )/y2 ,Cons(0,Cons(0,y3 ))/y1 ,Cons(0,Cons(0,Cons(0,y3 )))/x] {Stream(y3 )}...

At each derivation step, we record the clause that is used to make the resolution step and the computed
substitution. For this derivation, it is impossible to find a finite substitution σ such that Φ ` σ(Stream(x)).
Nevertheless, the query Stream(x) is computationally meaningful, since it computes the infinite stream ofzeros for x.
The importance of developing approaches for computing with infinite data structures in logic programming has been argued by van Emden, Lloyd, et al [Llo87] in the 80s and more recently the topic has been
revived by Gupta, Simon et al. [GBM+ 07, SBMG07]. In the classical approach [Llo87], a semantic view
was taken: if a nonterminating SLD-resolution derivation for Φ and A accumulates computed substitutions
σ0 , σ1 , . . . in such a way that (. . . (σ1 (σ0 (A)))) is an infinite ground formula, then (. . . (σ1 (σ0 (A)))) is said tobe computable at infinity. Computation at infinity is proven to be sound with respect to the greatest Herbrand model, i.e., given a logic program Φ, if a formula A is computable at infinity with respect to Φ, thenA is also in the greatest Herbrand model of Φ. Importantly for us, the notion of infinite formula computed at
infinity captures the modern-day notion of producing an infinite data structure. We will use the terminology
global productivity to describe computation at infinity. For example, the derivation shown in Example 1 isglobally productive, as it computes the infinite stream of zeros at infinity. However, this approach did not
result in implementation and in general proving global productivity is nontrivial.
An alternative approach has been proposed by Gupta, Simon et al. [GBM+ 07, SBMG07]: subgoals produced in the course of an infinite SLD-derivation can be memorized, and if any two subgoals are unifiable,
then the derivation is said to be closed coinductively. This approach was implemented as an extension to
Prolog and called CoLP (Coinductive Logic Programming). Its applications are limited, as CoLP does not
terminate for the SLD derivation that produces an infinite formula with irrational tree structure, as in thiscase the derivation does not feature any unifiable subgoals. CoLP’s approach was not intended to capture thenotion of global productivity. For example, the query P (x) for the clause P (y) ⇒ P (y) will exhibit a cycle
and will be coinductively proven by CoLP, but it will not compute an infinite formula at infinity. In otherwords, the derivation for P (x) is not globally productive despite being coinductively provable by CoLP.
In this paper, we introduce yet another approach to the potentially infinite derivations by the SLDresolution. When SLD-resolution produces a finite or infinite ground answer for a variable in the query, we
say the query is locally productive at that variable (see Definition 12). This gives us an alternative notion of
productivity for logic programming. In order to formally define this notion of local productivity, we introduce
a lazy version of resolution (called partial resolution). Firstly, we label those variables in the queries for which
we want to compute substitutions. Partial resolution then takes the labels into account when performing thecomputation, by giving priority to subgoals with labelled variables. The resolution will stop when all thelabels in the queries are eliminated, or in other words, when all required substitutions have been computed.
Finally, a third notion of productivity for logic programming, an observational productivity, has been
recently introduced by Johann, Komendantskaya et al [JKK15, KJM16]. It depends on a new kind of resolution (structural resolution). Structural resolution depends crucially on term-matching resolution, obtainedby restricting unification used in the SLD-resolution to term matching. Term-matching resolution is used ine.g. type class resolution [JJM97] in functional programming. It has different operational properties compared to the SLD-resolution. For example, taking the program in Example 1, the query Stream(x) can not
be reduced by term-matching resolution, as it is not possible to match Stream(Cons(0, y)) with Stream(x).
Structural resolution combines terminating term matching steps with unification steps. For example,
consider the following derivation (where → denotes a term-matching step, and ,→ applies the substitution
obtained by unification to the current query):Φ ` {Stream(x)} ,→κ1 ,[Cons(0,y1 )/x] {Stream(Cons(0, y1 ))} →κ1{Stream(y1 )} ,→κ1 ,[Cons(0,y2 )/y1 ,Cons(0,Cons(0,y2 ))/x] {Stream(Cons(0, y2 ))} →κ1{Stream(y2 )} ,→κ1 ,[Cons(0,y3 )/y2 ,Cons(0,Cons(0,y3 ))/y1 ,Cons(0,Cons(0,Cons(0,y3 )))/x] {Stream(Cons(0, y3 ))} →κ1{Stream(y3 )} ,→ ...
Note that the overall derivation is nonterminating, but all term-matching derivations are finite in the above
resolution trace. This separation of term-matching and unification allows the formulation of observational
productivity: given a program Φ and a query A, if a derivation for A is infinite, and it features only terminating

Operational Semantics of Resolution and Productivity in Horn Clause Logic3

term-matching resolution steps, then this derivation is called observationally productive. As discussed by
Komendantskaya, Johann et al. [KJ15, KJM16] observational productivity implies global productivity.
To illustrate these three notions of productivity, we consider three logic programs in the following table.
Name

Φ1

Φ2

Φ3

Program

P (x) ⇒ P (x)P (x) ⇒ P (K(x))

P (x, y) ⇒ P (x, G(y))

Query

P (x)

P (x)

P (x, y)Productivity

None

Global, Observational, Local
at x

Observational, Local at y

• Program Φ1 is not productive for the query P (x) by any of these three notions of productivity: it does
not compute an infinite ground formula, it is not terminating by term-matching resolution, and it does
not compute a ground answer for x.
• Program Φ2 is globally productive for the query P (x) as it computes an infinite formula P (K(K(...))).
We can see that Φ2 is observationally productive because it is terminating by term-matching resolution.
Also, Φ2 is locally productive at x for the query P (x) since SLD-resolution computes a ground infinite
answer K(K(...)) for the variable x.
• Program Φ3 is not globally productive for the query P (x, y) as SLD-resolution computes an infinite
formula P (x, G(G(...))) that is not ground. It is observationally productive, since the second argumentfor P is decreasing from right to left by the subterm relation, i.e. y <subterm G(y) and that ensurestermination of term-matching resolution. Note that Φ3 is not locally productive at x for the query
P (x, y), but it is locally productive at y since G(G(...)) is an infinite ground answer for y.
In this paper, we establish a framework for a comparative analysis of different kinds of resolution anddifferent notions of productivity. Firstly, we use a uniform style of small-step semantics for all these kindsof resolution and formulate them as abstract reduction systems. We call the resulting abstract reduction
systems LP-Unif, partial LP-Unif, LP-TM, and LP-Struct, respectively. Using this framework, we ask andanswer several research questions about operational properties and relations of these reduction systems. Are
LP-Unif and LP-Struct equivalent for terminating derivations, and under what conditions? Are LP-Unif and
LP-Struct equivalent for observationally productive programs? Since the termination of LP-TM is essential
for the observational productivity, are there any suitable program transformation methods to ensure LP-TM
termination?
We give a type-theoretic semantics to all these reduction systems. Notably, we take System H (based on
Howard’s work [How80]) as a calculus to capture the type-theoretic meaning of logic programming. We showthat LP-Unif, partial LP-Unif, LP-TM and LP-Struct are sound relative to System H. Moreover, LP-Unif iscomplete relative to System H, and under a meaning preserving transformation, LP-Struct is also complete
relative to System H.
We discover that, given a program Φ and a formula A, LP-Struct is operationally equivalent to LPUnif under two conditions: when all LP-Struct derivations for Φ are observaionally productive and when allclauses in Φ are non-overlapping. Thus the termination of LP-TM plays a crucial role not only in ensuringobservational productivity, but also in ensuring the operational equivalence of LP-Struct and LP-Unif, whichin its turn is crucial for our proofs of soundness and completeness of LP-Struct with respect to H.
We give a formal analysis of properties of LP-TM resolution. We show how LP-TM relates to term
rewriting systems by introducing a transformation method that translates any logic program without existential variables into a term rewriting system (we call this process functionalisation). After functionalisation,
standard term rewriting methods for detecting termination can be applied. We also give an alternative transformational method that renders all logic programs LP-TM terminating and non-overlapping. The method
is related to Kleene’s realizability method [Kle52], and we therefore call it realizability transformation.
The technical content of this paper is organized as follows.
• In Section 2, we prove soundness and completeness of LP-Unif with respect to the type system H. Thismeans H can be used to model logic programming.
• In Section 3, we formally define partial resolution as an abstract reduction system and call it partial

4

P. Fu and E. Komendantskaya

LP-Unif. Based on this formalism we define local productivity. Partial LP-Unif provides a possibility ofshifting the focus from deciding entailment for a given query to computing substitution answers.
• In Section 4, we formally define LP-Struct and identify two conditions that ensure that LP-Struct is
operationally equivalent to LP-Unif.
• In Section 5, we define functionalisation and show the exact relation of LP-TM to term rewriting systems.
We use existing termination detection techniques from term rewriting to detect termination of LP-TM.
• In Section 6, we define realizability transformation and show that this transformation preserves theoperational meaning of a logic program. We use it to show the equivalence of LP-Struct and LP-Unif for
the transformed program. As a corollary, we obtain the soundness and completeness of LP-Struct relative
to System H for the transformed program.
Finally, in Sections 7 and 8 we survey related work and conclude the paper.

2. Horn Formulas as Types
In this section, we use Howard’s type system H to model logic programming. We use an abstract reduction
system (called LP-Unif) to model the small-step semantics of the SLD-resolution. The purpose of this section
is to set up a type-theoretic framework for the rest of the paper, where Horn formulas are viewed as types ina type system and resolution corresponds to the proof construction. We show the correspondence between
the small-step semantics of resolution and System H. This result can be viewed as an alternative to theclassical-style soundness and completeness results for the SLD-resolution relative to Herbrand models. Using
System H as an alternative semantics for logic programming may be beneficial in two ways: (1) the usual
notion of an unsuccessful SLD-derivation can be understood as proving an implicative formula in which theunresolved subgoals comprise the antecedent (see Lemma 1). (2) It allows further extensions such as adding
fixpoint typing rule by Fu et al [FKSP16], which provides proofs for some nonterminating computations.
Definition 1 (Syntax).
Term t ::= x | K(t1 , ..., tn )Atomic Formula A, B, C, D ::= P (t1 , ..., tn )Formula F ::= A | F ⇒ F 0 | ∀x.F
Horn Formula/Horn Clause H ::= ∀x.A1 , ..., An ⇒ B
Proof Evidence p, e ::= κ | a | e e0 | λa.e
Axioms/Logic Programs Φ ::= · | κ : H, Φ | a : F, Φ
Proof evidence is given by lambda terms. We use capitalised words to denote function symbols. Constantevidence is denoted by κ. We write A1 , ..., An ⇒ B as a short hand for A1 ⇒ ... ⇒ An ⇒ B. We write∀x.F for quantifying over all free term variables in F , and [∀x].F denotes F or ∀x.F . We use A to denote
A1 , ..., An , when the number n is unimportant. If n is zero for A ⇒ B, then we write ⇒ B. Horn clauseformulas have the form ∀x.A ⇒ B, and queries are given by atomic formulas. We use FV(t) to denote theset of all free term variables in t.
The following is a type system based on Howard’s work [How80], intended to provide a type theoreticinterpretation for LP.
Definition 2 (Howard’s System H for logic programming).
(κ : H) ∈ Φ
Axiom
Φ`κ:H

(a : F ) ∈ Φ
Var
Φ`a:F

Φ ` e1 : F1 ⇒ F2 Φ ` e2 : F1App
Φ ` e1 e2 : F2

Φ ` e : ∀x.FInstΦ ` e : [t/x]F

Φ`e:F
Gen
Φ ` e : ∀x.F

Φ, a : F1 ` e : F2Abs
Φ ` λa.e : F1 ⇒ F2

Note that the type for the constant in the rule Axiom is required to be Horn formula. It has been
observed that the Cut rule and proper axioms in intuitionistic sequent calculus can emulate logic programming [GTL89](§13.4).
The following rule is a version of Cut rule, working only with Horn formulas.

Operational Semantics of Resolution and Productivity in Horn Clause Logic5Φ ` e1 : A ⇒ D Φ ` e2 : B, D ⇒ CCutΦ ` λa.λb.(e2 b) (e1 a) : A, B ⇒ C
We can use rules Abs and App to emulate Cut rule, thus the Cut rule is admissible in Howard’s system
H. We will use C to denote the deduction system that consists of rules Axiom, Cut, Inst, and Gen. The
subsystem C provides a natural framework to work with Horn formulas, but H is more expressive, since itallows full intuitionistic formulas, e.g. H would allow a formula of the form (F1 ⇒ F2 ) ⇒ F3 .
Definition 3. Beta-reduction on proof evidence is defined as the congruence closure of the following relation:(λa.e) e0 →β [e0 /a]e. We say a proof evidence e is strongly normalizing if e admits no infinite →β -reductions.
The following three theorems are standard for a type system such as H. For proofs we refer the reader
to Barendregt’s excellent book [Bar93].
Theorem 1 (Strong Normalization). If Φ ` e : F in H, then e is strongly realisable with respect tobeta-reduction on proof evidence.
Theorem 2 (Inversion). • If Φ ` a : F , then (a : F 0 ) ∈ Φ and σF 0 ≡ F for some substitution σ.
• If Φ ` κ : H, then (κ : ∀x.A1 , ..., An ⇒ B) ∈ Φ and σ(A1 , ..., An ⇒ B) ≡ H for some substitution σ.
• If Φ ` λa.e : F , then Φ, a : F1 ` e : F2 and σ(F1 ⇒ F2 ) ≡ F for some substitution σ.
• If Φ ` e1 e2 : F , then Φ ` e1 : F1 ⇒ F2 , Φ ` e2 : F1 and σF2 ≡ F for some substitution σ.
Theorem 3 (Type Preservation). System H is type preserving, i.e. if Φ ` e : F in H and e →β e0 , thenΦ ` e0 : F .
Note that system C as a type system is not type preserving. For example, consider Φ = (κ1 : A ⇒ B, κ2 :B ⇒ C, κ3 : C ⇒ D). In C, we have Φ ` λa.κ3 ((λb.κ2 (κ1 b)) a) : A ⇒ D. But λa.κ3 ((λb.κ2 (κ1 b)) a) →β
λa.κ3 (κ2 (κ1 a)) and Φ 6` λa.κ3 (κ2 (κ1 a)) : A ⇒ D in C. Thus we often work with C through its embeddingin H, which is type preserving and strongly normalising.
Definition 4 (Unification). We say that t is unifiable with t0 with substitution γ (denoted t ∼γ t0 ), if{t = t0 } ∗ γ according to the following rules:{K(t1 , ..., tn ) = K(s1 , ..., sn )} ∪ E

 {t1 = s1 , ..., tn = sn } ∪ E{K(t1 , ..., tn ) = G(s1 , ..., sm )} ∪ E

 ⊥{t = t} ∪ E

 E{K(t1 , ..., tn ) = x} ∪ E

 {x = K(t1 , ..., tn )} ∪ E{x = K(t1 , ..., tn )} ∪ E

 ⊥ if x ∈ FV(K(t1 , ..., tn )){x = t} ∪ E

 {x = t} ∪ [t/x]E if x ∈/ FV(t)Unification can be routinely extended to atomic formulas. The symbol ⊥ denotes failure of unification. The
following is a formulation of the SLD-resolution as a reduction system, as given in Nilsson and Maluszynski[NM90].
Definition 5 (LP-Unif reduction). Given a set of axioms Φ, we define a reduction relation on the multiset
of atomic formulas:Φ ` {A1 , ..., Ai , ..., An } κ,γ·γ 0 {γA1 , ..., γB1 , ..., γBm , ..., γAn } for any substitution γ 0 , if there exists κ :∀x.B1 , ..., Bn ⇒ C ∈ Φ such that C ∼γ Ai .
The second subscript in the reduction is intended as a state, it will be updated by composition along with
reductions. Notation γ · γ 0 should be read as follows: the old state γ 0 is updated, producing a new state γ · γ 0 .
We assume fresh names in the form of new numeric indices for the quantified variables each time the above
rule is applied. We writewhen we leave the associated state implicit. We use ∗ to denote the reflexive
and transitive closure of . Notation ∗γ is used when the final state along the reduction path is γ.

6

P. Fu and E. Komendantskaya

Given a program Φ and a set of queries {B1 , . . . , Bn }, SLD-resolution uses LP-Unif reduction to reduce{B1 , . . . , Bn }:Definition 6 (LP-Unif ). Given a logic program Φ, LP-Unif is given by the abstract reduction system(Φ, ).
Example 2. Consider the following logic program Φ, consisting of Horn formulas labelled by κ1 , κ2 , κ3 ,defining connectivity for a graph with three nodes:
κ1 : ∀x.∀y.∀z.Connect(x, y), Connect(y, z) ⇒ Connect(x, z)
κ2 : ⇒ Connect(N ode1 , N ode2 )κ3 : ⇒ Connect(N ode2 , N ode3 )The usual SLD-resolution for the query Connect(x, y) can be represented as the following LP-Unif reduction:Φ ` {Connect(x, y)} κ1 ,[x/x1 ,y/z1 ] {Connect(x, y1 ), Connect(y1 , y)} κ2 ,[N ode1 /x,N ode2 /y1 ,N ode1 /x1 ,y/z1 ]{Connect(N ode2 , y)} κ3 ,[N ode3 /y,N ode1 /x,N ode2 /y1 ,N ode1 /x1 ,N ode3 /z1 ] ∅The first reduction κ1 ,[x/x1 ,y/z1 ] unifies the query Connect(x, y) with the head of the rule κ1 (which isConnect(x1 , z1 ) after renaming) with the substitution [x/x1 , y/z1 ] (x1 is replaced by x and z1 is replaced byy). So the query is resolved with κ1 , producing the next queries: Connect(x, y1 ), Connect(y1 , y). Note thatthe substitution in the subscript ofis a state that will be updated alongside the derivation. In the final
state we have an answer [N ode3 /y, N ode1 /x] for the query Connect(x, y).

2.1. Soundness and Completeness of LP-Unif
We have introduced the Howard’s system H and LP-Unif. Now we will show the soundness of LP-Unif, i.e.,
we show that a reduction by LP-Unif corresponds to an intuitionistic proof. On the other hand, any firstorder ground evidence of type A in H corresponds to a successful LP-Unif reduction (which is the essenceof the completeness result).
Lemma 1 (Soundness Lemma). If Φ ` {A}C.

∗
γ {B1 , ..., Bn }, then Φ ` e : B1 , ..., Bn ⇒ γA for some e in

Proof. By induction on the length of the reduction.
• Base Case. Suppose the length is one, namely, Φ ` {A} κ,γ {B1 , ..., Bn }. It implies (κ : ∀x.B10 , ..., Bn0 ⇒C) ∈ Φ, γBi0 ≡ Bi and C ∼γ A. So we have Φ ` κ : γB10 , ..., γBn0 ⇒ γC by the rules Axiom and Inst.
• Step Case. Suppose Φ ` {A} ∗γ1 {A1 , ..., Ai , ..., An } κ,γ2 ·γ1 {γ2 A1 , ..., γ2 B1 , ..., γ2 Bm , ..., γ2 An }, whereκ : ∀x.B1 , ..., Bm ⇒ C and C ∼γ2 Ai . By inductive hypothesis (IH), we have Φ ` e1 : A1 , ..., An ⇒ γ1 A.
By Inst and Gen, we have Φ ` e1 : γ2 A1 , ..., γ2 Ai , ..., γ2 An ⇒ γ2 γ1 A and Φ ` κ : γ2 B1 , ..., γ2 Bm ⇒ Ai .
Since γ2 is idempotent, we have Φ ` κ : γ2 B1 , ..., γ2 Bm ⇒ γ2 Ai . Thus by Cut rule, we have Φ ` e0 :γ2 A1 , ..., γ2 B1 , ..., γ2 Bm , ..., γ2 An ⇒ γ2 γ1 A for some proof evidence e0 .

The soundness lemma above ensures that every LP-Unif reduction and its answer are meaningful. The
usual notion of failure in logic programming can be understood as proving an implicative formula in which
the antecedent is comprised of the failed subgoals. The notion of success corresponds to a proof of an atomic
formula. For example, consider the logic program Φ = κ1 : P3 (K) ⇒ P1 (K), κ2 : P2 (K) ⇒ P3 (K). We knowthat the query P1 (x) will fail. But by Lemma 1, we know the resolution for query P1 (x) will stop at P2 (K)with substitution [K/x], and we have the proof Φ ` λa.κ1 (κ2 a) : P2 (K) ⇒ [K/x]P1 (x) in C. So in a sense
the failed query P1 (x) is still meaningful under the type theoretic interpretation. In Section 3 we will use
LP-Unif in a way that it does not have to resolve all the queries, but it still computes useful answers for thevariable that we care about.
Theorem 4 (Soundness of LP-Unif ). If Φ ` {A}∗γ ∅ , then Φ ` e : ∀x. ⇒ γA for some e in C.

Operational Semantics of Resolution and Productivity in Horn Clause Logic

7

An evidence is ground if it does not contain free evidence variables. The proof of completeness relies on
the strong normalisation and the type preservation property of H. We first show that the normal form of
the proof given by a successful LP-Unif reduction is first-order. We then show that, if an atomic formula isinhabited by a ground evidence, there exists a successful LP-Unif reduction for it.
Definition 7 (First-Order Proof Evidence). We define first-order proof evidence as follows.
• A variable proof evidence a and a constant proof evidence κ are first-order.
• If n, n0 are first-order, then n n0 is first-order.
For example, (κ κ0 ) is considered first-order, but (κ (λa.κ0 (κ00 a))) is not first-order.
Proposition 1. If n, n0 are first-order, then [n0 /a]n is first-order.
Lemma 2. If Φ ` e : [∀x.]A ⇒ B in C, then either e is a proof evidence constant, variable or it isnormalisable to the form λa.n, where n is first-order normal proof evidence.
Proof. By induction on the derivation of Φ ` e : [∀x.]A ⇒ B.
• Base Case. Rule Axiom. Obvious.
• Step Case.
Φ ` e1 : A ⇒ D Φ ` e2 : B, D ⇒ CCutΦ ` λa.λb.(e2 b) (e1 a) : A, B ⇒ C
By IH, we know that e1 = κ or e1 = λa.n1 ; e2 = κ0 or e2 = λb.λd.n2 , where n1 , n2 are fist-order. We
know that e1 a will be normalizable to a first-order proof evidence. And e2 b will be normalized to either
κ0 b or λd.n2 . So by Proposition 1, we conclude that λa.λb.(e2 b) (e1 a) is normalizable to λa.λb.n forsome first-order normal term n.
• The Gen and Inst cases are straightforward.
Theorem 5. If Φ ` e : [∀x.] ⇒ B in C, then e is normalizable to a first-order proof evidence.
Now let us prove the completeness theorem.
Proposition 2. If e is a ground first-order evidence, then it is of the following form:• κ• κ n1 ... nl , where ni is ground first-order evidence for any i.
Theorem 6 (Completeness of LP-Unif ). If Φ ` n : ⇒ A where n is in ground first-order normal formin H, then Φ ` {A} ∗ ∅.
Proof. By induction on the structure of n.
• Base Case. n = κ. By inversion, we know κ : ∀x. ⇒ A0 ∈ Φ and γA0 ≡ A for some substitution γ. Thus
A0 ∼γ A, which implies Φ ` {A} κ,γ ∅.
• Step Case. n = κ n1 n2 ... nm . By inversion, we have κ : ∀x. C1 , ..., Cm ⇒ B ∈ Φ. To obtain Φ ` n : ⇒ A,
by inversion we have Φ ` κ : ∀x. C1 , ..., Cm ⇒ B with γm ...γ1 (B) ≡ A, and Φ ` n1 : ⇒ C1 , Φ ` n2 :⇒ γ1 C2 ..., Φ ` nm : ⇒ γm−1 ...γ1 Cm . By the rule Inst, we have Φ ` n1 : ⇒ γm ...γ1 C1 , Φ ` n2 : ⇒γm ...γ1 C2 ..., Φ ` nm : ⇒ γm ...γ1 Cm . Thus we have Φ ` {A} κ,γm ·...·γ1 {γm ...γ1 C1 , ..., γm ...γ1 Cm }.
By IH, we have Φ ` {γm ...γ1 C1 } ∗σ1 ∅. So Φ ` {A} κ,γm ·...·γ1 · ∗σ1 {σ1 γm ...γ1 C2 , ..., σ1 γm ...γ1 Cm }.
Again, we have Φ ` n2 : ⇒ σ1 γm ...γ1 C2 by rule Inst. By applying IH repeatedly, we obtain Φ ` {A} ∗ ∅.

3. Partial LP-Unif by Labelling
In the previous section, we have given a type-theoretic semantics to logic programming. According to it, ananswer for a given query is a substitution applied to a formula that is inhabited by a proof evidence. In that

8

P. Fu and E. Komendantskaya

sense, the soundness lemma (Lemma 1) gives type-theoretic meaning to any LP-Unif reduction, even if it isa partial derivation, i.e. has unresolved subgoals. In this section, we build upon this result, and propose alazy version of LP-Unif, drawing inspiration from lazy functional languages such as Haskell. In particular,
we propose to label certain variables in a given query, in order to prioritize those variables for which wewant to compute substitutions. Partial LP-Unif resolution will only resolve the subgoals that contain labelledvariables. This requires to extend the usual unification to account for labels. We call the resulting unification
algorithm labelled unification and the resulting reduction strategy – partial LP-Unif.
Definition 8. We extend the term definition:t ::= x | xv | K(t1 , ..., tn ), where xv is a labelled variable.
Definitions of a Horn formula and a formula are extended accordingly.
A label on a variable can be informally understood as a case-expression on a variable in lazy functional
language. When a query has a labelled variable, it forces resolution to compute a value for it. But since weare in logic programming, the only way to force such evaluation is through label propagation and elimination.
The following definition extends unification to achieve this.
We write tv to denote the labelled version of t, in which all the variables of t are labelled. Note that xv
is identical to (xv )v .
Definition 9 (Labelled Unification). We say that t is unifiable with t0 with substitution γ (denotedt ∼γ t0 ), if {t = t0 } ∗ γ according to the following rules:{K(t1 , ..., tn ) = K(s1 , ..., sn )} ∪ E

 {t1 = s1 , ..., tn = sn } ∪ E{K(t1 , ..., tn ) = G(s1 , ..., sm )} ∪ E

 ⊥{t = t} ∪ E

 E{K(t1 , ..., tn ) = x} ∪ E

 {x = K(t1 , ..., tn )} ∪ E{K(t1 , ..., tn ) = xv } ∪ E

 {xv = K(t1 , ..., tn )} ∪ E{x = K(t1 , ..., tn )} ∪ E

 ⊥ if x ∈ FV(K(t1 , ..., tn )){xv = K(t1 , ..., tn )} ∪ E

 ⊥ if xv ∈ FV(K(t1 , ..., tn )){x = t} ∪ E

 {x = t} ∪ [t/x]E if x ∈/ FV(t){xv = t} ∪ E

 {xv = tv } ∪ [tv /xv ](`t (E)) if xv ∈/ FV(t)We use `t (E) to denote a labelling operation that labels all the variables in E that occur in t. Formally,`t (E) is defined as σE, where [xv /x] ∈ σ for any x ∈ FV(t). The set of equations {x1 = t1 , ..., xn = tn } canbe viewed as a substitution. The labelled unification of terms can be extended routinely to the unificationof atomic formulas.
We write |t| to denote erasing all the labels in t. We write |σ| to denote removing all the labels in thesubstitution σ, and L(A) to denote the set of labelled variables in A. The following lemma shows that labelledunification is functionally equivalent to the usual (unlabelled) unification.
Lemma 3. If t 'γ t0 and FV(|t|) ∩ FV(|t0 |) = ∅, then |t| ∼|γ| |t0 |.
We use `γ (A) to denote another labelling operation that labels all variables in A that are labelled in thecodomain of γ. Formally, `γ (A) is defined as σA, such that, for any xv ∈ FV(codom(γ)), [xv /x] ∈ σ.
Definition 10 (Partial LP-Unif ). We define a reduction relation on a multiset of atomic formulas:Φ ` {A1 , ..., Ai , ..., An } *κ,γ·γ 0 {γA1 , ..., γ`γ (B1 ), ..., γ`γ (Bm ), ..., γAn } for any substitution γ 0 , if L(Ai ) 6= ∅and there exists κ : ∀x.B1 , ..., Bn ⇒ C ∈ Φ such that C 'γ Ai .
The labelling operation `γ is used in the above definition to make sure that the labels are correctly
propagated to B1 , ..., Bm . Consider Φ = κ1 : ⇒ P1 (Int), κ2 : ⇒ P2 (Int), κ3 : ∀x.P1 (x), P2 (x) ⇒ Q(List(x)),

Operational Semantics of Resolution and Productivity in Horn Clause Logic

9and the query Q(z v ). The labelled unifier of Q(z v ) and Q(List(x)) is γ = [List(xv )/z v ], we need to apply`γ to P1 (x) and P2 (x) to obtain the resolvents P1 (xv ) and P2 (xv ).
As a consequence of Lemma 3, the partial LP-Unif is essentially a control strategy for LP-Unif.
Lemma 4. If Φ ` {A1 , ..., Ai , ..., An } *κ,γ·γ 0 {γA1 , ..., γ`γ (B1 ), ..., γ`γ (Bm ), ..., γAn }, thenΦ ` {|A1 |, ..., |Ai |, ..., |An |} κ,|γ·γ 0 | {|γA1 |, ..., |γ`γ (B1 )|, ..., |γ`γ (Bm )|, ..., |γAn |}.
Note that the above lemma implies, as a corollary, that partial LP-Unif is sound with respect to H.
Definition 11. If Φ ` {A} *∗γ {B1 , ..., Bn }, L(A) 6= ∅ and L(Bi ) = ∅ for all i, then we say γ is the relative
answer for the labelled variables in A with respect to B1 , ..., Bn .
Comparing to LP-Unif, partial LP-Unif does not resolve subgoals without labelled variables, and therefore
it terminates as soon as all the labelled formulas are resolved. From the pragmatic perspective, the termination of partial LP-Unif signifies that we have obtained all the answers we need for the labelled variables, andthus no further computation is necessary. From the computational perspective, some queries may give rise
to nonterminating LP-Unif reduction and the partial LP-Unif strategy offers a lazy version of LP-Unif as analternative. This is a useful lightweight solution, as checking (non)termination for logic programming can be
at best only semi-decidable. From the theoretical perspective, relative answers are meaningful according to
type-theoretic semantics of Section 2 via Lemma 4.
Labels on variables give us a precise way to formalize the notion of local productivity we mentioned in
Introduction.
Definition 12 (Local Productivity). We say the queries A1 , ..., An are locally productive at the set oflabelled variables V iff ({A1 , ..., An }, V ) ∈ LProdm for any m ≥ 0. We define ({A1 , ..., An }, V ) ∈ LProdm asfollows:• ({A1 , ..., An }, V ) ∈ LProd0 for any A1 , ..., An , V .
• ({A1 , ..., An }, V ) ∈ LProdm+1 iff for all xv ∈ V , there exists Φ ` {A1 , ..., An } *∗γ {Q1 , ..., Ql } such thatγ(xv ) = K(t1 , ..., tn ) and ({Q1 , ..., Ql }, L(γ)) ∈ LProdm , where L(γ) denotes the set of labelled variablesin the codomain of γ.
Note that according to the definition, if a query is trivially locally productive at the empty set of labelledvariables and is trivially locally unproductive if the set of labelled variables are not a subset of the labelledvariables in the query. Thus in general it is more sensible to ask local productivity of a query at all its
labelled variables.
Local productivity is defined by quantifying over all natural numbers m on LProdm , this allows us toprove local productivity by induction on natural numbers. The requirement γ(xv ) = K(t1 , ..., tn ) in thedefinition of LProdm ensures that the answer for a labelled variable xv is at least observable at the function
symbol K.
To illustrate local productivity, let us consider the query P (xv ) and the logic program κ : ∀x.P (x) ⇒P (K(x)). We want to show that {P (xv )} is locally productive at xv for any variable x. We just need toshow for any x, ({P (xv )}, {xv }) ∈ LProdm for all m. We proceed by induction on m. Suppose m = 0,
we know that ({P (xv )}, {xv }) ∈ LProd0 . Suppose m = m0 + 1, we have a partial LP-Unif reduction Φ `{P (xv )} *[K(xv1 )/xv ] {P (xv1 )}. As [K(xv1 )/xv ]xv = K(xv1 ), we just need to show ({P (xv1 )}, {xv1 }) ∈ LProdm0 ,which is by the inductive assumption. This is a very simple case of showing local productivity. In general, it
is very challenging to prove local productivity in advance, and we leave this to future work.
Partial productivity and global productivity do not coincide, in general. For example, for a logic programκ : P (K) ⇒ P (K), the query P (xv ) is locally productive, but it is not globally productive, as, using
terminology of Lloyd [Llo87], no infinite term gets produced at infinity.
We give two further examples of performing finite computation on infinite data structures using partial
LP-Unif.
Example 3. Consider the following logic program Φ, that observes, via the N th predicate, elements of an
infinite stream of successive integers defined by F rom:
κ1 : ∀x.∀y.F rom(S(x), y) ⇒ F rom(x, Cons(x, y))κ2 : ∀x.∀y. ⇒ N th(Z, Cons(x, y), x)

10

P. Fu and E. Komendantskayaκ3 : ∀x.∀y.∀z.∀u.N th(x, z, u) ⇒ N th(S(x), Cons(y, z), u)
For the query N th(S(Z), y, z v ), F rom(S(Z), y), we only want to know the answer for z v , i.e., the 2nd elementin the stream generated by F rom(S(Z), y). We observe the following reduction:Φ ` {N th(S(Z), y, z v ), F rom(S(Z), y)} *κ3 ,γ1 ≡[Z/x1 ,Cons(y1 ,z1 )/y,uv1 /zv ]{N th(Z, z1 , uv1 ), F rom(S(Z), Cons(y1 , z1 ))} *κ2 ,γ2 ≡[xv2 /uv1 ,Cons(xv2 ,y2 )/z1 ]·γ1
{F rom(S(Z), Cons(y1 , Cons(xv2 , y2 )))} *κ1 ,γ3 ≡[Cons(xv2 ,y2 )/y3 ,S(Z)/y1 ,S(Z)/x3 ]·γ2
{F rom(S(S(Z)), Cons(xv2 , y2 ))} *κ1 ,[y4 /y2 ,S(S(Z))/xv2 ,S(S(Z))/x4 ]·γ3 {F rom(S(S(S(Z))), y4 )}Thus S(S(Z)) is the answer for z v relative to F rom(S(S(S(Z))), y4 ), i.e. the 2nd element in the stream
generated by F rom(S(Z), y) is S(S(Z)).
Example 4. Consider the following logic program Φ:κ1 : ∀x.∀y. ⇒ T ake(Z, App(x, y), N il)
κ2 : ∀x.∀y.∀z.∀r.T ake(x, z, r) ⇒ T ake(S(x), App(y, z), Cons(y, r))κ3 : ∀x.∀y.∀s.F ib(y, App(x, y), s) ⇒ F ib(x, y, App(x, s))
The formula F ib(y, App(x, y), s) ⇒ F ib(x, y, App(x, s)) is intended to generate (potentially infinitely long)
Fibonacci word. For example, A, B, A·B, B·(A·B), (A·B)·(B·(A·B))... (where “,” and “·” both are shorthandfor App, each element of the stream is the concatenation of the previous two) for query F ib(A, B, y v ). Now
let us execute the query T ake(S(S(S(Z))), y, z v ), F ib(A, B, y), Intuitively, that query computes the prefixof length 3 in a Fibonacci word:Φ ` {T ake(S(S(S(Z))), y, z v ), F ib(A, B, y)} *κ2 ,γ1 ≡[S(S(Z))/x1 ,App(y1v ,z1 )/y,Cons(y1v ,r1v )/zv ]{T ake(S(S(Z)), z1 , r1v ), F ib(A, B, App(y1v , z1 ))} *κ3 ,γ2 ≡[A/x2 ,B/y2 ,A/y1v ,s2 /z1 ]·γ1
{T ake(S(S(Z)), s2 , r1v ), F ib(B, App(A, B), s2 )} *κ2 ,γ3 ≡[S(S(Z))/x3 ,App(y3v ,z3 )/s2 ,Cons(y3v ,r3v )/r1v ]·γ2
{T ake(S(Z), z3 , r3v ), F ib(B, App(A, B), App(y3v , z3 ))} *κ3 ,γ4 ≡[B/x4 ,App(A,B)/y4 ,B/y3v ,s4 /z3 ]·γ3
{T ake(S(Z), s4 , r3v ), F ib(App(A, B), App(B, (App(A, B))), s4 )} *κ2 ,γ5 ≡[S(Z)/x5 ,App(y5v ,z5 )/s4 ,Cons(y5v ,r5v )/r3v ]·γ4
{T ake(Z, z5 , r5v ), F ib(App(A, B), App(B, (App(A, B))), App(y5v , z5 ))} *κ1 ,γ6 ≡[App(x6 ,y6 )/z5 ,N il/r5v ]·γ5{F ib(App(A, B), App(B, (App(A, B))), App(y5v , App(x6 , y6 )))}
*κ3 ,γ7 ≡[App(A,B)/x7 ,App(B,(App(A,B)))/y7 ,App(A,B)/y5v ,App(x6 ,y6 )/s7 ]·γ6{F ib(App(B, (App(A, B))), App(App(A, B), App(B, (App(A, B)))), App(x6 , y6 ))}We can see that [Cons(A, Cons(B, Cons(App(A, B), N il)))/z v ] is the answer relative toF ib(App(B, (App(A, B))), App(App(A, B), App(B, (App(A, B)))), App(x6 , y6 )), i.e. the prefix of length 3 ina Fibonacci word is indeed A, B, A · B.
Note that a relative answer γ for a query A can be meaningless under Herbrand model semantics, as
γA, or indeed any of its ground instances, may not be in the least or greatest Herbrand model of the logic
program. The following example illustrates this fact.
Example 5. Consider Example 3. Suppose the Horn formula κ1 is replaced with the following Horn formula:κ01 : ∀x.∀y.F alse(a), F rom(S(x), y) ⇒ F rom(x, Cons(x, y))where F alse(a) is a formula that does not unify with any clause in the given program. However, we canstill perform the same partial LP-Unif derivation for the query N th(S(Z), y, z v ), F rom(S(Z), y), just as wasshown in Example 3. But no instance of F rom(S(Z), y) will be contained in the least or greatest Herbrandmodel of that program.

3.1. Disscussion
This section presented an experiment in applying the type-theoretic semantics formulated in the earlier
section to a practical problem of establishing a sound lazy derivation strategy for resolution. It de-emphasizes
the usual notions of refutation and entailment in logic programming. Based on the type-theoretic semantics
given to resolution via soundness and completeness theorems of Section 2, every reduction path of a given

Operational Semantics of Resolution and Productivity in Horn Clause Logic

11

query is computationally meaningful. This generalizes the traditional declarative semantics approach to logic
programming, according to which only refutation – i.e. the reduction that lead to a normal form given by
the empty set – is given a model theoretic meaning.
Labels we introduced in this section allowed us to annotate the intention of making an observation,and the labelled unification was formulated to hereditarily preserve this intention. Thus, we achieved acomputational behavior that is similar to lazy functional programming languages, i.e. partial LP-Unif canmake finite observations on the infinite data.
Related work exists on supporting lazy computation in logic programming. One is by annotating eachpredicate to be inductive/coinductive [SBMG07], with the intention of resolving the inductive predicate
eagerly and memorizing the coinductive predicate at each step, so that one can stop the resolution wheneverthe current query is a variant of the previous memorized coinductive predicate. Our approach differs in thatmemorization and variant detection are not needed.

4. Structual Resolution
In this section, we represent structural resolution using the abstract reduction formalism we introducedin Section 2. We first define structural resolution as LP-Struct reduction, thereby also defining LP-TM
reduction, which replaces the unification in LP-Unif by term-matching. We then identify two conditions
under which LP-Unif and LP-Struct are operationally equivalent. These two conditions are the terminationof LP-TM and the non-overlapping requirement for Horn clauses.
Definition 13.
• Term-matching (LP-TM) reduction:Φ ` {A1 , ..., Ai , ..., An } →κ {A1 , ..., σB1 , ..., σBm , ..., An }, if there exists κ : ∀x.B1 , ..., Bn ⇒ C ∈ Φ suchthat σC ≡ Ai .
• Substitutional reduction:Φ ` {A1 , ..., Ai , ..., An } ,→κ,γ·γ 0 {γA1 , ..., γAi , ..., γAn } for any substitution γ 0 , if there existsκ : ∀x.B1 , ..., Bn ⇒ C ∈ Φ such that C ∼γ Ai .
When combining LP-TM reduction with substitutional reductions, we sometimes write →κ,γ , where thesecond subscript is used to store the substitution γ. The second subscript in the substitutional reduction isintended as a state (similar to LP-Unif), it will be updated along with reduction.
Given a program Φ and a set of queries {B1 , . . . , Bn }, LP-TM uses only term-matching reduction to
reduce {B1 , . . . , Bn }:Definition 14 (LP-TM). Given a logic program Φ, LP-TM is given by an abstract reduction system(Φ, →).
LP-TM is also sound w.r.t. the type system of Definition 2, which implies that we can obtain a proof foreach reductoin of the query.
Theorem 7 (Soundness of LP-TM). If Φ ` {A} →∗ {B1 , ..., Bn } , then Φ ` e : ∀x.B1 , ..., Bn ⇒ A in C.
Comparing the soundness lemma and Theorem 7, we see that for LP-TM, there is no need to accumulate
substitutions, this is due to the use of term-matching instead of unification for the LP-TM reduction.
We use →µ to denote a reduction path to a →-normal form. If the →-normal form does not exist, thenµ→ denotes an infinite reduction path. We write ,→1 to denote at most one step of ,→.
We can now formally define structural resolution within our formal framework. Given a program Φ anda set of queries {B1 , . . . , Bn }, LP-Struct first uses term-matching reduction to reduce {B1 , . . . , Bn } to anormal form, then performs one step substitutional reduction, and then repeats this process.
Definition 15 (Structural Resolution (LP-Struct)). Given a logic program Φ, LP-Struct is given by
an abstract reduction system (Φ, →µ · ,→1 ).
If a finite term-matching reduction path does not exist, then →µ · ,→1 denotes an infinite path. Whenwe write Φ ` {A}(→µ · ,→1 )∗ {C}, it means a nontrivial finite path will be of the shape Φ ` {A} →µ · ,→·...· →µ · ,→ · →µ {C}.
Now let us recall the execution trace of the query Stream(x) in Example 1 using LP-Struct:12

P. Fu and E. KomendantskayaΦ ` {Stream(x)} ,→κ1 ,[Cons(0,y1 )/x] {Stream(Cons(0, y1 ))} →κ1{Stream(y1 )} ,→κ1 ,[Cons(0,y2 )/y1 ,Cons(0,Cons(0,y2 ))/x] {Stream(Cons(0, y2 ))} →κ1{Stream(y2 )} ,→κ1 ,[Cons(0,y3 )/y2 ,Cons(0,Cons(0,y3 ))/y1 ,Cons(0,Cons(0,Cons(0,y3 )))/x] {Stream(Cons(0, y3 ))} →κ1{Stream(y3 )} ,→ ...

4.1. LP-Struct and LP-Unif
LP-Struct exibits different execution behavior compared to LP-Unif. In general, they are not equivalent. Consider the program and the finite LP-Unif derivation of Example 2. LP-Unif has a finite successful derivation
for the query Connect(x, y), but we have the following non-terminating reduction by LP-Struct:Φ ` {Connect(x, y)} →κ1 {Connect(x, y1 ), Connect(y1 , y)}→κ1 {Connect(x, y2 ), Connect(y2 , y1 ), Connect(y1 , y)} →κ1 ...
The diverging behavior above is due to the divergence of LP-TM reduction.
Definition 16 (LP-TM Termination). We say a program Φ is LP-TM terminating iff it admits no infinite→-reduction.
LP-TM termination is important for LP-Struct in two aspects: 1. It is one of the conditions that ensure
the operational equivalence of LP-Struct and LP-Unif. 2. The finiteness of LP-TM reduction is used indefining the observational productivity in logic programming.
The following example shows that LP-TM termination alone is not sufficient to establish that LP-Unifand LP-Struct are operationally equivalent.
Example 6. Consider the following logic program (we use K to denote a constant):
κ1 : ⇒ P (K)κ2 : ∀x.Q(x) ⇒ P (x)The program is LP-TM terminating. For query P (x), we have Φ ` {P (x)}there is only one reduction path Φ ` {P (x)} →κ2 {Q(x)} ,6 → for LP-Struct.

κ1 ,[K/x] ∅ with LP-Unif, but

Thus the termination of LP-TM is insufficient for establishing the relation between LP-Struct and LPUnif. In Example 6, the problem is caused by the overlapping heads P (K) and P (x). Motivated by thenon-overlapping condition for rewrite rules in term rewriting systems ([BN98], [Ter03]), we introduce thefollowing definition.
Definition 17 (Non-overlapping Condition). Axioms Φ are non-overlapping if for any κi : ∀x.B ⇒C, κj : ∀x.D ⇒ E ∈ Φ, there are no substitutions σ, δ such that σC ≡ δE.
The following lemma shows that an LP-TM step can be viewed as an LP-Unif step without affecting theaccumulated substiution.
Lemma 5. If Φ ` {D1 , ..., Di , ..., Dn } →κ,γ {D1 , .., σE1 , ..., σEm , ..., Dn }, with κ : ∀x.E ⇒ C ∈ Φ andσC ≡ Di for any γ, then Φ ` {D1 , ..., Di , ..., Dn } κ,γ {D1 , .., σE1 , ..., σEm , ..., Dn }.
Proof. Since for Φ ` {D1 , ..., Di , ..., Dn } →κ,γ {D1 , .., σE1 , ..., σEm , ..., Dn }, with κ : ∀x.E ⇒ C ∈ Φ andσC ≡ Di , we have Φ ` {D1 , ..., Di , ..., Dn } κ,σ·γ {σD1 , .., σE1 , ..., σEm , ..., σDn }. But dom(σ) ∈ FV(C),thus we have Φ ` {D1 , ..., Di , ..., Dn } κ,γ {D1 , .., σE1 , ..., σEm , ..., Dn }.
The following lemma shows that one LP-Struct step corresponds to several LP-Unif steps, given the
non-overlapping requirement.
Lemma 6. Suppose Φ is non-overlapping and {A1 , ..., An } are →-normal. If Φ ` {A1 , ..., An }(,→κ,γ · →µγ){C1 , ..., Cm }, then Φ ` {A1 , ..., An } ∗γ {C1 , ..., Cm }.
Proof. Given Φ ` {A1 , ..., An }(,→κ,γ · →µγ ){C1 , ..., Cm }, we know the actual reduction path can be rearranged
to the form Φ ` {A1 , ..., An } ,→κ,γ {γA1 , ..., γAn } →κ,γ {γA1 , ..., γB1 , ..., γBn , ..., γAn } →µγ {C1 , ..., Cm },where γAi ≡ γC with κ : ∀x.B ⇒ C ∈ Φ and Ai ≡ σB. Note that γ is unchanged along the term-matching
reduction. We have rearranged the →-step following right after ,→ using κ due to the property of LP-TM.

Operational Semantics of Resolution and Productivity in Horn Clause Logic

13

Note that to LP-TM reduce Ai we can only use κ, since otherwise it would mean with κ0 : ∀x.D ⇒ B ∈ Φ.
This implies γC ≡ γσB, contradicting the non-overlapping restriction. Thus we have Φ ` {A1 , ..., An } κ,γ{γA1 , ..., γB1 , ..., γBn , ..., γAn }. By Lemma 5, we have Φ ` {A1 , ..., An } κ,γ {γA1 , ..., γB1 , ..., γBn , ..., γAn }∗γ {C1 , ..., Cm }.
Lemmas 7, 8 and Theorem 8 show that for a non-overlapping program, LP-Unif is equivalent to LP-Struct
for terminating reductions.
Lemma 7. Given Φ is non-overlapping, if Φ ` {A1 , ..., An }(→µ · ,→1 )∗γ {C1 , ..., Cm } with {C1 , ..., Cm } in→µ · ,→1 -normal form, then Φ ` {A1 , ..., An } ∗γ {C1 , ..., Cm } with {C1 , ..., Cm } in -normal form.
Proof. Since Φ ` {A1 , ..., An }(→µ · ,→1 )∗γ {C1 , ..., Cm }, this means the reduction path must be of the formΦ ` {A1 , ..., An } →µ · ,→1 · →µ · ,→1 ... →µ · ,→1 · →µ {C1 , ..., Cm }. Thus Φ ` {A1 , ..., An } →µ ·(,→1 · →µ)·(,→1 ... →µ )·(,→1 · →µ ){C1 , ..., Cm }. By Lemma 5 and Lemma 6, we have Φ ` {A1 , ..., An } ∗γ {C1 , ..., Cm }with {C1 , ..., Cm } in -normal form.
Lemma 8. Given Φ is a non-overlapping, if Φ ` {A1 , ..., An } ∗γ {C1 , ..., Cm } with {C1 , ..., Cm } in normal form , then Φ ` {A1 , ..., An }(→µ · ,→1 )∗γ {C1 , ..., Cm } with {C1 , ..., Cm } in →µ · ,→1 -normal form.
Proof. By induction on the length of∗γ.

• Base Case. Φ ` {A1 , ..., Ai , ..., An }κ,γ {γA1 , ..., γB1 , ..., γBm ..., γAn } with κ : ∀x. B ⇒ C ∈ Φ,C ∼γ Ai and {γA1 , ..., γB1 , ..., γBm ..., γAn } in -normal form . We have Φ ` {A1 , ..., Ai , ..., An } ,→κ,γ{γA1 , ..., γAi , ..., γAn } →κ {γA1 , ..., γB1 , ..., γBm ..., γAn } with {γA1 , ..., γB1 , ..., γBm ..., γAn } in →µ· ,→-normal form. Note that there can not be another κ0 : ∀x.B ⇒ C 0 ∈ Φ such that σC 0 ≡ Ai ,since this would means γC ≡ γAi ≡ γσC 0 , violating the non-overlapping requirement.
∗• Step Case. Φ ` {A1 , ..., Ai , ..., An }κ,γ {γA1 , ..., γB1 , ..., γBl , ..., γAn }γ 0 {C1 , ..., Cm } with κ :∀x.B1 , ..., Bl ⇒ C ∈ Φ and C ∼γ Ai . We have Φ ` {A1 , ..., Ai , ..., An } ,→κ,γ {γA1 , ..., γAi , ..., γAn } →{γA1 , ..., γB1 , ..., γBm , ..., γAn }. By the non-overlapping requirement, there can not be another κ0 :∀x.D ⇒ C 0 ∈ Φ such that σC 0 ≡ Ai . By IH, we know Φ ` {γA1 , ..., γB1 , ..., γBm , ..., γAn }(→µ · ,→)∗γ 0 {C1 , ..., Cm }. Thus we conclude that Φ ` {A1 , ..., Ai , ..., An }(,→ · →)∗γ 0 {C1 , ..., Cm }.
Theorem 8. Suppose Φ is non-overlapping. Φ ` {A1 , ..., An } ∗γ {C1 , ..., Cm } with {C1 , ..., Cm } innormal form iff Φ ` {A1 , ..., An }(→µ · ,→1 )∗γ {C1 , ..., Cm } with {C1 , ..., Cm } in →µ · ,→1 -normal form.

-

The theorem above implies that for terminating and non-overlapping programs, LP-Unif is equivalent
to LP-Struct. But the termination requirement can be relaxed by only requiring the termination of the→-reduction, i.e. by requiring termination of LP-TM.
S
Lemma 9. If Φ ` {A} →κ,γ {B1 , ..., Bm } and dom(σ) ∩ (( i FV(Bi )) − FV(A)) = ∅, then Φ ` {σA} →κ,γ
{σB1 , ..., σBm }.
Note that the above
S lemma shows that the reduction → is closed under substitution only under the condition
that dom(σ) ∩ (( i FV(Bi )) − FV(A)) = ∅, i.e. the domain of the substitution must not contain any variable
that are in Bi but not in A for any i, otherwise it will not be the case. If Φ ` {A} →µ {B1 , ..., Bm }, we write[A] to mean the normal form of A, i.e. B1 , ..., Bm .
Theorem 9 (Equivalence of LP-Struct and LP-Unif ). Suppose Φ is non-overlapping and LP-TM terminating.
1. If Φ ` {A1 , ..., An }{B1 , ..., Bm }, then Φ ` {A1 , ..., An }(→µ · ,→1 )∗ {C1 , ..., Cl } and Φ ` {B1 , ..., Bm } →∗{C1 , ..., Cl }.
2. If Φ ` {A1 , ..., An }(→µ · ,→1 )∗ {B1 , ..., Bm }, then Φ ` {A1 , ..., An } ∗ {B1 , ..., Bm }.
Proof. 1. Suppose Φ ` {A1 , ..., An }κ,γ {γA1 , ..., γE1 , ..., γEl , ..., γAn }, with κ : E ⇒ D ∈ Φ andD ∼γ Ai . Suppose γD ≡ Ai , we have Φ ` {A1 , ..., An } →κ,γ {γA1 , ..., γE1 , ..., γEq , ..., γAn } →µγ{C1 , ..., Cl }. Suppose γD 6≡ Ai . In this case, we have Φ ` {A1 , ..., An } →µ {[A1 ], ..., Ai , ..., [An ]} ,→κ,γ{[γA1 ], ..., γAi , ..., [γAn ]} →κ,γ {[γA1 ], ..., γE1 , ..., γEq , ..., [γAn ]} →µγ {C1 , ..., Cl }. By Lemma 9, we know

14

P. Fu and E. Komendantskayathat Φ ` γA1 →µ {[γA1 ]}, ..., Φ ` γAn →µ {[γAn ]}. Thus Φ ` {γA1 , ..., γE1 , ..., γEq , ..., γAn } →µ{C1 , ..., Cl }.
2. We just need to show that if {A1 , ..., An } are →-normal and Φ ` {A1 , ..., An } ,→κ,γ {γA1 , ..., γAn } →µγ{B1 , ..., Bm }, then Φ ` {A1 , ..., An } ∗γ {B1 , ..., Bm }. Suppose Φ ` {A1 , ..., An } ,→κ,γ {γA1 , ..., γAn } →µγ{B1 , ..., Bm }, we have Φ ` {A1 , ..., An } ,→κ,γ {γA1 , ..., γAn } →κ {γA1 , ..., γC1 , ..., γCl , ..., γAn } →µγ{B1 , ..., Bm } with κ : C ⇒ D ∈ Φ and D ∼γ Ai . Thus we haveΦ ` {A1 , ..., An } κ,γ {γA1 , ..., γC1 , ..., γCl , ..., γAn }. By Lemma 5, we have Φ ` {A1 , ..., An } κ,γ{γA1 , ..., γC1 , ..., γCl , ...., γAn } ∗γ {B1 , ..., Bm }.
Note that the above theorem does not rely on the whole program termination, therefore it establishes
equivalence of LP-Unif and LP-Struct even for nonterminating programs such as the Stream example, aslong as they are LP-TM terminating and non-overlapping. This result has not been described in previous
work.

4.2. Discussion
Structural resolution was first introduced in Komendantskaya and Power’s work ([KP11], [KPS14]) under
the name of coalgebraic logic programming. It was further developed into a resolution method based on
resolution trees (called rewriting trees) generated by term-matching ([JKK15], [KJ15]). The formulation of
LP-Struct in this paper is based on the abstract reduction system framework, instead of the tree formalism
in previous work. As a consequence, for overlapping logic programs, the reduction-based LP-Struct behavesdifferently compared to the tree-based formalism (see e.g. Example 6). The novelty of our development inthis section is the articulation of the two conditions that ensure the operational equivalence of LP-Struct
and LP-Unif (Theorem 9).

5. Functionalisation of LP-TM
One of the features of LP-Struct is that it refines SLD-resolution by a combination of term-matching andunification. LP-TM itself is used in the type class context reduction [JJM97]. The termination behavior of
LP-TM is of practical interest. For example, termination for the type class inference is essential to achieve
decidability of the type inference in languages such as Haskell ([LPJ05] Section 5).
Of course, the termination of LP-TM also implies observational productivity in the context of LPStruct. As explained in Introduction and Section 4, LP-TM termination is not only essential to ensure theequivalence of LP-Struct and LP-Unif, but also is important to allow viewing the LP-TM reductions within
the nonterminating LP-Struct reduction as finite observations.
On the other hand, termination and nontermination detection are well-studied in the context of term
rewriting. In this section we show a method that reuses the techniques developed in term rewriting to detecttermination of LP-TM. We first define a process called functionalisation that transforms a set of Horn clauses
into a set of rewrite rules, where the execution of a query is seen as a process of rewriting the query to its
proof. As a result, termination and nontermination detection techniques from term rewriting can be applied
to LP-TM, assuming the logic program contains no existential variables.
In this section we work only withSthe Horn formulas without existential variables, i.e. for any Hornformula ∀x.A1 , ..., An ⇒ B, we have i FV(Ai ) ⊆ FV(B). The restriction that Horn clauses should notcontain existential variables comes directly from a similar requirement imposed in term-rewriting.
Since the idea of functionalisation is to view LP-TM resolution for a query as a rewriting process to its
proof evidence, the rewriting is defined on mixed terms, i.e. a mixture of atomic formulas and proof evidence.
Definition 18 (Mixed Terms).
Mixed termqMixed term context C

::=
::=

A | κ | q q0•|Cq|qC

Note that C can be ground. Let C[q1 , ..., qn ] mean replacing all the • in C from left to right by q1 , ..., qn .

Operational Semantics of Resolution and Productivity in Horn Clause Logic

15

Definition 19 (Functionalisation). We can construct a set of rewrite rule K(Φ) from a set of axioms Φ
as follows. For each κ : ∀x.A1 , ..., An ⇒ B ∈ Φ, we define a rewrite rule B → κ A1 ... An ∈ K(Φ) on mixed
terms. We call κ an axiom symbol.
Note that the evidence constant κ for A1 , ..., An ⇒ B becomes a mixed term function symbol of arity n,with A1 , ..., An as its arguments, which is denoted by κ A1 ... An .
Definition 20. We define a relation C → C 0 to mean that C 0 can be obtained from C by replacing a • in C
by some C1 , where C1 6≡ •. We also write the reflexive and transitive closure of this relation as →∗ .
The following lemmas show that each LP-TM step corresponds exactly to a rewrite step after functionalisation. As a consequence, it is possible to determine the termination behavior of LP-TM by analyzing thecorresponding term rewriting system.
Lemma 10. Φ ` {A1 , ..., An } → {A1 , ..., σB1 , ..., σBm , ..., An }, where κ : ∀x.B1 , ..., Bm ⇒ B ∈ Φ andσB ≡ Ai iff C[A1 , ..., Ai , ..., An ] → C 0 [A1 , ..., σB1 , ..., σBm , ..., An ], where C, C 0 do not contain any atomic
formulas and C → C 0 .
Proof. By Definition 19, κ : ∀x.B1 , ..., Bm ⇒ Ai ∈ Φ implies Ai → κ B1 ... Bm ∈ K(Φ), and vice versa. So
C 0 can be obtained by replacing the ith • in C by κ •1 ... •m .
Lemma 11. Φ ` {A1 , ..., An } →∗ {C1 , ..., Cl } iff C[A1 , ..., An ] →∗ C 0 [C1 , ..., Cl ], where C →∗ C 0 and C, C 0 do
not contain any atomic formulas.
Proof. We prove both direction together. By induction on the length of →∗ .
Base Case. By Lemma 10.
Step Case.
Left to Right:
Suppose Φ ` {A1 , ..., An } → {A1 , ..., σB1 , ..., σBm , ..., An } →∗ {C1 , ..., Cl }, with κ : ∀x.B1 , ..., Bm ⇒ B ∈ Φand σB ≡ Ai . Then we know C[A1 , ..., An ] → C 00 [A1 , ..., σB1 , ..., σBm , ..., An ]. Also, C → C 00 , where C 00 can beobtained from C by replacing its ith • by κ •1 ... •m . By IH, C 00 [A1 , ..., σB1 , ..., σBm , ..., An ] →∗ C 0 [C1 , ..., Cl ]with C 00 →∗ C 0 . So C[A1 , ..., An ] →∗ C 0 [C1 , ..., Cl ] with C →∗ C 0 .
Right to Left:
Suppose C[A1 , ..., An ] → C 00 [A1 , ..., σB1 , ..., σBm , ..., An ] →∗ C 0 [C1 , ..., Cl ] with C → C 00 →∗ C 0 , whereB → κ B1 ... Bm and σB ≡ Ai . So ∀x.B1 , ..., Bm ⇒ B ∈ Φ and σB ≡ Ai . Thus Φ ` {A1 , ..., An } →{A1 , ..., σB1 , ..., σBm , ..., An }. By IH, Φ ` {A1 , ..., σB1 , ..., σBm , ..., An } →∗ {C1 , ..., Cl }. Thus, we haveΦ ` {A1 , ..., An } →∗ {C1 , ..., Cl }.
Theorem 10. Φ ` {A} →∗ ∅ iff A →∗ e, and e is a ground evidence. As a consequence, the query A is
LP-TM (non)terminating iff A is (non)terminating for K(Φ).
Proof. By Lemma 11.
In practice, functionalisation can also be used to implement LP-TM, especially if computing the proof
evidence is the only goal. For example, this is the case for type class inference [FKSP16].
Now we demonstrate how to apply a convenient termination technique in term rewriting called dependency
pair method [AG00] to analyze the termination behavior of LP-TM.
Definition 21. We define the dependency pairs generated from K(Φ) to be E(K(Φ)) = {B → Ai | B →κ A1 ... An ∈ K(Φ)}.
Definition 22. A (potentially infinite) sequence of pairs q1 → q10 , q2 → q20 , ... in E(K(Φ)) is a K(Φ)-chain
iff there is a substitution σ with σqi0 ≡ σqi+1 for all i.
The above definition of K(Φ)-chain is using the condition σqi0 ≡ σqi+1 instead of σqi0 →∗ σqi+1 in term
rewriting [AG00]. Since the dependency pairs generated from a logic program will always be in the form of
A → B, where A, B are atomic formulas, rewriting under the predicate is not possible. This greatly simplifies
the termination detection for LP-TM.
Theorem 11 (Arts-Giesl [AG00]). K(Φ) is terminating iff no infinite K(Φ)-chain exist.
Theorem 11 allows us to detect the termination of K(A) by looking at the possible K(Φ)-chain.

16

P. Fu and E. Komendantskaya

Example 7. Consider the following program Φ:κ1 : ⇒ P (Int)κ2 : ∀x.P (x), P (List(x)) ⇒ P (List(x))
The dependency pairs of Φ are P (List(x)) → P (List(x)) and P (List(x)) → P (x). We can see P (List(x)) →P (List(x)) can form an infinite E(K(Φ))-chain, thus K(Φ) is not terminating. So Φ is not LP-TM terminating.

6. Realizability Transformation and LP-Struct
Functionalisation provides a way to detect LP-TM termination for LP-Struct. But sometimes there are
logic programs that are not LP-TM terminating but are still meaningful from the LP-Unif perspective (cf.
Example 2). For these programs, we still want to be able to use LP-Struct. To solve this problem, we define ameaning preserving realizability transformation that transforms any logic program into LP-TM terminatingone.
Realizability [Kle52](§82) is a technique that uses a number representing the proof of a number-theoretic
formula. The transformation described here is similar in the sense that we use a first-order term to represent
the proof of a Horn formula. More specifically, we use a first-order term as an extra argument for Hornformula to represent a proof of that formula.
Lemma 2 and Theorem 5 show that we can use a first-order term to represent a normalized proof evidence.
Definition 23 (Representing First-Order Proof Evidence). Let φ be a mapping from proof evidence
variables to first-order terms. We define a representation function J·Kφ from first-order normal proof evidence
to first-order terms.
• JaKφ = φ(a).
• Jκ p1 ...pn Kφ = Kκ (Jp1 Kφ , ..., Jpn Kφ ), where Kκ is a function symbol.

S
Let A ≡ P (t1 , ..., tn ) be an atomic formula and t0 be a term such that ( i FV(ti )) ∩ FV(t0 ) = ∅, we write
A[t0 ] to abbreviate a new atomic formula P (t1 , ..., tn , t0 ).
Definition 24 (Realizability Transformation). We define a transformation F on Horn formula and its
normalized proof evidence:• F (κ : ∀x.A1 , ..., Am ⇒ B) = κ : ∀x.∀y.A1 [y1 ], ..., Am [ym ] ⇒ B[Kκ (y1 , ..., ym )], where y1 , ..., ym are all
fresh and distinct.
• F (λa.n : [∀x].A1 , ..., Am ⇒ B) = λa.n : [∀x.∀y].A1 [y1 ], ..., Am [ym ] ⇒ B[JnK[y/a] ], where y1 , ..., ym are all
fresh and distinct.
The realizability transformation systematically associates a proof to each predicate, so that the proof
can be recorded alongside with reductions. Let F (Φ) mean applying the realizability transformation to every
axiom in Φ.
Example 8. The following logic program F (Φ) is the result of applying realizability transformation on the
program Φ in Example 2.
κ1 : ∀x.∀y.∀u1 .∀u2 .Connect(x, y, u1 ), Connect(y, z, u2 ) ⇒ Connect(x, z, Kκ1 (u1 , u2 ))κ2 : ⇒ Connect(N ode1 , N ode2 , Kκ2 )κ3 : ⇒ Connect(N ode2 , N ode3 , Kκ3 )Before the realizability transformation, we have the following judgement in H:Φ ` λb.(κ1 b) κ2 : Connect(N ode2 , z) ⇒ Connect(N ode1 , z)We can apply the transformation, we get:F (Φ) ` λb.(κ1 b) κ2 : Connect(N ode2 , z, u1 ) ⇒ Connect(N ode1 , z, J(κ1 b) κ2 K[u1 /b] )which is the same as

F (Φ) ` λb.(κ1 b) κ2 : Connect(N ode2 , z, u1 ) ⇒ Connect(N ode1 , z, Kκ1 (u1 , Kκ2 ))Operational Semantics of Resolution and Productivity in Horn Clause Logic

17

We write (F (Φ), ), to mean given axioms F (Φ), use LP-Unif to reduce a given query. Note that for aquery A in (Φ, ), it becomes a query A[t] for some t such that FV(A) ∩ FV(t) = ∅ in (F (Φ), ).
The following theorem shows that realizability transformation does not change the type-theoretic meaningof a program. This is important because it means we can apply different resolution strategies to resolve thequery on the transformed program without worrying about the change of meaning. Later we will see thatthe behavior of LP-Struct is different for the original program and the transformed program.
Theorem 12. If Φ ` e : [∀x].A ⇒ B in C and e normalized to n, then F (Φ) ` F (n : [∀x].A ⇒ B) in H.
Proof. By induction on the derivation of Φ ` e : [∀x].A ⇒ B.
• Base Case.
(κ : ∀x.A ⇒ B) ∈ ΦΦ ` κ : ∀x.A ⇒ B
In this case, we know that F (κ : ∀x.A ⇒ B) = κ : ∀x.∀y.A1 [y1 ], ..., An [yn ] ⇒ B[fκ (y1 , ..., yn )] ∈ F (Φ).
• Step Case.
Φ ` e1 : A ⇒ D Φ ` e2 : B, D ⇒ CΦ ` λa.λb.(e2 b) (e1 a) : A, B ⇒ C
By Lemma 2, we know that the normal form of e1 is κ1 or λa.n1 , and the normal form of e1 is κ2 or
λbd.n2 , with n1 , n2 are first-order.
– e1 ≡ κ1 , e2 ≡ κ2 . By IH, we know that Φ ` κ1 : A1 [y1 ], ..., An [yn ] ⇒ D[fκ1 (y1 , ..., yn )] and Φ ` κ2 :B1 [z1 ], ..., Bm [zm ], D[y] ⇒ C[fκ2 (z1 , ..., zm , y)]. So by Gen and Inst, we haveΦ ` κ2 : B1 [z1 ], ..., Bm [zm ], D[fκ1 (y1 , ..., yn )] ⇒ C[fκ2 (z, fκ1 (y))].
Then by the Cut rule, we haveΦ ` λa.λb.κ2 b (κ1 a) : A1 [y1 ], ..., An [yn ], B1 [z1 ], ..., Bm [zm ] ⇒ C[fκ2 (z, fκ1 (y))].
We can see that Jκ2 b (κ1 a)K[y/a,z/b] = fκ2 (z, fκ1 (y)).

– e1 ≡ λa.n1 , e2 ≡ λb.d.n2 . By IH, we know that Φ ` λa.n1 : A1 [y1 ], ..., A1 [y1 ] ⇒ D[Jn1 K[y/a] ] andΦ ` λb.d.n2 : B1 [z1 ], ..., Bm [zm ], D[y] ⇒ C[Jn2 K[z/b,y/d] ]. So by Gen and Inst, we haveΦ ` λb.d.n2 : B1 [z1 ], ..., Bm [zm ], D[Jn1 K[y/a] ] ⇒ C[Jn2 K[z/b,Jn1 K[y/a] /d] ].
Then by the Cut rule and beta reduction, we haveΦ ` λa.λb.([n1 /d]n2 ) : A1 [y1 ], ..., A1 [y1 ], B1 [z1 ], ..., Bm [zm ] ⇒ C[Jn2 K[z/b,Jn1 K[y/a] /d] ] in H. We knowthat J[n1 /d]n2 K[y/a,z/b] = Jn2 K[z/b,Jn1 K[y/a] /d] .

– The other cases are handle similarly.
• Step Case.
Φ ` λa.n : ∀x.A ⇒ B
Φ ` λa.n : [t/x]A ⇒ [t/x]BBy IH, we know that Φ ` λa.n : ∀x.∀y.A1 [y1 ], ..., An [yn ] ⇒ B[JnK[y/a] ]. By Inst rule, we have Φ ` λa.n :[t/x]A1 [y1 ], ..., [t/x]An [yn ] ⇒ [t/x]B[JnK[y/a] ]• Step Case.
Φ`e:FΦ ` e : ∀x.F
This case is straightforwardly by IH.
The following lemma and a theorem show that the extra argument can be used to record the term
representation of the corresponding proof.
Lemma 12. If F (Φ) ` {A1 [y1 ], ..., An [yn ]}in H with Jei K∅ = γyi for all i.

∗γ ∅, and y1 , ..., yn are fresh, then F (Φ) ` ei : ∀x. ⇒ γAi [γyi ]18

P. Fu and E. Komendantskaya

Proof. By induction on the length of the reduction F (Φ) ` {A1 [y1 ], ..., An [yn ]}∗γ ∅.

• Base Case. Suppose the length is one, namely, F (Φ) ` {A[y]} κ,γ1 ∅. Thus there exists (κ : ∀x. ⇒C[fκ ]) ∈ F (Φ)(here fκ is a constant), such that C[fκ ] ∼γ1 A[y]. Thus γ1 (C[fκ ]) ≡ γ1 A[γ1 y]. So γ1 y ≡ fκ
and γ1 C ≡ γ1 A. We have F (Φ) ` κ : ⇒ γ1 C[fκ ] by the Inst rule, thus F (Φ) ` κ : ⇒ γ1 A[γ1 y], hence
F (Φ) ` κ : ∀x. ⇒ γ1 A[γ1 y] by the Gen rule and JκK∅ = fκ .
• Step Case. Suppose∗
F (Φ) ` {A1 [y1 ], ..., Ai [yi ], ..., An [yn ]}κ,γ1 {γ1 A1 [y1 ], ..., γ1 B1 [z1 ], ..., γ1 Bm [zm ], ..., γ1 An [yn ]}γ ∅,where κ : ∀x.∀z.B1 [z1 ], ..., Bm [zm ] ⇒ C[fκ (z1 , ..., zm )] ∈ F (Φ), and C[fκ (z1 , ..., zm )] ∼γ1 Ai [yi ]. So
we know γ1 C[fκ (z1 , ..., zm )] ≡ γ1 Ai [γ1 yi ], γ1 yi ≡ fκ (z1 , ..., zm ), γ1 C ≡ γ1 Ai anddom(γ1 ) ∩ {z1 , ..., zm , y1 , .., yi−1 , yi+1 , yn } = ∅. By IH, we know that F (Φ) ` e1 : ∀x. ⇒ γγ1 A1 [γy1 ], ...,F (Φ) ` p1 : ∀x. ⇒ γγ1 B1 [γz1 ], ..., F (Φ) ` pm : ∀x. ⇒ γγ1 Bm [γzm ], ..., F (Φ) ` en : ∀x. ⇒ γγ1 An [γyn ] andJe1 K∅ = γy1 , ..., Jp1 K∅ = γz1 , ..., Jpm K∅ = γzm , ..., Jen K∅ = γyn . We can construct a proof ei = κ p1 ...pm
with ei : ∀x. ⇒ γγ1 Ai [γγ1 yi ], by first apply the Inst to instantiate the quantifiers of κ, then applying the
Cut rule m times. Moreover, we have Jκ p1 ...pm K∅ = fκ (Jp1 K∅ , ..., Jpm K∅ ) = γ(fκ (z1 , ..., zm )) = γγ1 yi .
Theorem 13. Suppose F (Φ) ` {A[y]}form and JpK∅ = γy.

∗γ ∅. We have F (Φ) ` p : ∀x. ⇒ γA[γy] in H, where p is in normal

Now we are able to show that realizability transformation will not change the unification reduction
behaviour.
Lemma 13. If Φ ` {A1 , ..., An }∗∅, then F (Φ) ` {A1 [y1 ], ..., An [yn ]}Proof. By induction on the length of Φ ` {A1 , ..., An }∗∗∅ with yi fresh for all i.

∅.

• Base Case. Suppose the length is one, namely, Φ ` {A} κ,γ1 ∅. There exists (κ : ∀x. ⇒ C) ∈ Φ suchthat C ∼γ1 A. Thus κ : ∀x. ⇒ C[fκ ] ∈ F (Φ) and (C[fκ ]) ∼γ1 [fκ /y] A[y]. So F (Φ) ` {A[y]} κ,γ1 [fκ /y] ∅.
• Step Case. Suppose Φ ` {A1 , ..., Ai , ..., An } κ,γ1 {γ1 A1 , ..., γ1 B1 , ..., γ1 Bm , ..., γ1 An } ∗γ ∅, where κ :∀x.B1 , ..., Bm ⇒ C ∈ Φ and C ∼γ1 Ai . So we know that κ : ∀x.∀z.B1 [z1 ], ..., Bm [zm ] ⇒ C[fκ (z)] ∈ F (Φ)
and C[fκ (z)] ∼γ1 [fκ (z)/yi ] Ai [yi ]. Thus we have the following reduction:
F (Φ) ` {A1 [y1 ], ..., Ai [yi ], ..., An [yn ]} κ,γ1 [fκ (z)/yi ]{γ1 [fκ (z)/yi ]A1 [y1 ], ..., γ1 [fκ (z)/yi ]B1 [z1 ], ..., γ1 [fκ (z)/yi ]Bm [zm ], ..., γ1 [fκ (z)/yi ]An [yn ]} ≡{γ1 A1 [y1 ], ..., γ1 B1 [z1 ], ..., γ1 Bm [zm ], ..., γ1 An [yn ]}∗By IH, F (Φ) ` {γ1 A1 [y1 ], ..., γ1 B1 [z1 ], ..., γ1 Bm [zm ], ..., γ1 An [yn ]}Lemma 14. If F (Φ) ` {A1 [y1 ], ..., An [yn ]}∗∅.

∅ with yi fresh for all i, then Φ ` {A1 , ..., An }Proof. By induction on the length of F (Φ) ` {A1 [y1 ], ..., An [yn ]}

∗

∗

∅.

∅.

• Base Case. Suppose the length is one, namely, F (Φ) ` {A[y]} κ,γ1 ∅.
We know that (κ : ∀x. ⇒ C[fκ ]) ∈ F (Φ) with C[fκ ] ∼γ1 A[y]. Thus C ∼γ1 −[fκ /y] A. So Φ ` {A}∅.
• Step Case. Suppose we have the following reduction:
F (Φ) ` {A1 [y1 ], ..., Ai [yi ], ..., An [yn ]} κ,γ1 {γ1 A1 [y1 ], ..., γ1 B1 [z1 ], ..., γ1 Bm [zm ], ..., γ1 An [yn ]} ∗γ ∅Note that κ : ∀x.∀z.B1 [zm ], ..., Bm [zm ] ⇒ C[fκ (z1 , ..., zm )] ∈ F (Φ) and C[fκ (z1 , ..., zm )] ∼γ1 Ai [yi ]. So
we know C ∼γ1 −[fκ (z)/yi ] Ai . Let γ = γ1 − [fκ (z)/yi ]. We haveΦ ` {A1 , ..., Ai , ..., An }κ,γ {γA1 , ..., γB1 , ..., γBm , ..., γAn } ≡ {γ1 A1 , ..., γ1 B1 , ..., γ1 Bm , ..., γ1 An }By IH, we know Φ ` {γ1 A1 , ..., γ1 B1 , ..., γ1 Bm , ..., γ1 An }Theorem 14. Φ ` {A}∗∅ iff F (Φ) ` {A[y]}

∗

∗

∅.

∅.

Example 9. Consider the logic program in Example 8. Realizability transformation does not change the behaviour of LP-Unif, we still have the following successful unification reduction path for query Connect(x, y, u):Operational Semantics of Resolution and Productivity in Horn Clause Logic

F (Φ) ` {Connect(x, y, u)}19

κ1 ,[x/x1 ,y/z1 ,Kκ1 (u3 ,u4 )/u] {Connect(x, y1 , u3 ), Connect(y1 , y, u4 )}

κ2 ,[Kκ2 /u3 ,N ode1 /x,N ode2 /y1 ,N ode1 /x1 ,b/z1 ,Kκ1 (Kκ2 ,u4 )/u]{Connect(N ode2 , y, u4 )}
κ3 ,[Kκ3 /u4 ,Kκ2 /u3 ,N ode3 /y,N ode1 /x,N ode2 /y1 ,N ode1 /x1 ,N ode3 /z1 ,Kκ1 (Kκ2 ,Kκ3 )/u] ∅There are logic programs that are overlapping and LP-TM nonterminating (as e.g. the program of Example 2), we would still like to obtain a meaningful execution behaviour for LP-Struct, especially if LP-Unifaready allows successful derivations for the programs. Luckily, we can apply realizability transformation tosuch programs and apply LP-Struct reduction.
Proposition 3. For any program Φ, F (Φ) is LP-TM terminating and non-overlapping.
Proof. First, we need to show →-reduction is strongly normalizing in (F (Φ), →). By Definition 24, we canestablish a decreasing measurement(from right to left, using the strict subterm relation) for each rule in
F (Φ), since the last argument in the head of each rule is strictly larger than the ones in the body. Then,non-overlapping property is due to the fact that all the heads of the rules in F (Φ) will be guarded by theunique function symbol in Definition 24.
Corollary 1 (Equivalence of LP-Unif and LP-Struct). F (Φ) ` {A1 , ..., An }(→µ · ,→1 )∗ {B1 , ..., Bm }iff F (Φ) ` {A1 , ..., An } ∗ {B1 , ..., Bm }.
Proof. By Theorem 9 and Proposition 3.
Using the above corollary and soundness and completeness of LP-Unif, we deduce as a corollary that
LP-Struct is sound and complete relative to system H for the transformed logic program.
Example 10. For the program in Example 8, the query Connect(x, y, u) can be reduced by LP-Structsuccessfully:
F (Φ) ` {Connect(x, y, u)} ,→κ1 ,[x/x1 ,y/z1 ,Kκ1 (u3 ,u4 )/u] {Connect(x, y, Kκ1 (u3 , u4 ))} →κ1{Connect(x, y1 , u3 ), Connect(y1 , y, u4 )},→κ2 ,[Kκ2 /u3 ,N ode1 /x,N ode2 /y1 ,N ode1 /x1 ,b/z1 ,Kκ1 (Kκ2 ,u4 )/u]{Connect(N ode1 , N ode2 , Kκ2 ), Connect(N ode2 , y, u4 )} →κ2 {Connect(N ode2 , y, u4 )},→κ3 ,[Kκ3 /u4 ,Kκ2 /u3 ,N ode3 /y,N ode1 /x,N ode2 /y1 ,N ode1 /x1 ,N ode3 /z1 ,Kκ1 (Kκ2 ,Kκ3 )/u]{Connect(N ode2 , N ode3 , Kκ3 )} →κ3 ∅Note that the answer for u is Kκ1 (Kκ2 , Kκ3 ), which is the first-order term representation of the proof of⇒ Connect(N ode1 , N ode3 ).
Realizability transformation uses the extra argument as decreasing measurement in the program toachieve termination of →-reduction. At the same time this extra argument makes the program non-overlapping.
Realizability transformation does not modify the proof-theoretic meaning and the execution behaviour of LPUnif. The next example shows that not every transformation technique for obtaining structurally decreasing
LP-TM reductions has such properties:
Example 11. Consider the following program:κ1 : ⇒ P (Int)κ2 : ∀x.P (x), P (List(x)) ⇒ P (List(x))
It is a folklore method to add a structurally decreasing argument as a measurement to ensure finiteness of→µ .
κ1 : ⇒ P (Int, 0)
κ2 : ∀x.∀y.P (x, y), P (List(x), y) ⇒ P (List(x), S(y))
We denote the above program as Φ0 . Indeed with the measurement we add, the term-matching reduction inΦ0 will be finite. But the reduction for query P (List(Int), z) using LP-Unif reduction will fail:Φ0 ` {P (List(Int), z)}κ2 ,[Int/x,S(y1 )/z] {P (Int, y1 ), P (List(Int), y1 )}{P (List(Int), 0)} 6

κ2 ,[0/y1 ,Int/x,S(0)/z]

20

P. Fu and E. Komendantskaya

However, the query P (List(Int)) on the original program using unification reduction will diverge. Divergenceand failure are operationally different. Thus adding arbitrary measurement may modify the execution behaviour of a program (and hence the meaning of the program). In contrast, by Theorems 12-14, realizability
transformation does not modify the execution behaviour of LP-Unif reduction.
Example 12. Consider the following non-LP-TM terminating and non-overlapping program and its version
after the realizability transformation:
Original program: κ : ∀x.P (x) ⇒ P (x)After transformation: κ : ∀x.∀u.P (x, u) ⇒ P (x, Kκ (u))
Both LP-Struct and LP-Unif will diverge for the queries P (x), P (x, y) in both original and transformed
versions. LP-Struct reduction diverges for different reasons in the two cases, one is due to divergence of→-reduction: Φ ` {P (x)} → {P (x)} → {P (x)} → .... The another is due to ,→-reduction: Φ ` {P (x, y)} ,→{P (x, fk (u))} → {P (x, u)} ,→ {P (x, Kk (u0 ))} → {P (x, u0 )} ,→ .... Note that a single step of LP-Unifreduction for the original program corresponds to infinite steps of term-matching reduction in LP-Struct.
For the transformed version, a single step of LP-Unif reduction corresponds to finite steps of LP-Structreduction.

7. Related Work
Proof Search, Logic Programming and Type Theory. To the best of our knowledge, studying logic programming proof-theoretically dates back to Girard’s suggestion to use the cut rule to model resolution for Hornformulas [GTL89, Chapter 13.4]. Miller et. al. [MNPS89] use cut-free sequent calculus to represent a proof
for a query. More specifically, given a query Q and a logic program P, Q has a refutation iff there is a
derivation in cut-free sequent calculus for P ` Q. Using sequent calculus as a proof theoretic framework
gives the flexibility to incorporate different kinds of formulas, e.g. classical formulas and linear formulas into
this framework.
Interactive theorem prover Twelf [PS99] pioneered implementation of proof search on top of a depedently
typed system called LF [HL07]. Similar to Twelf, we believe that type systems serve as a suitable foundation
for logic programming. Comparing to Twelf, we specify and analyze different resolution strategies (otherthan SLD-resolution) and study their intrinsic relations. We also pay more attention to various kinds ofproductivity compared to Twelf.
Structural Resolution. Structural resolution is a result of joint research efforts by Komendantskaya et.
al. ([JKK15], [KP11], [KPS14]). The goal of the analysis of structural resolution is to support sound coinductive reasoning in logic programming. For example, given the query T ake(S(S(S(Z))), y, z), F ib(A, B, y)in Example 4, one may want not only to obtain a substitution for z, but also a guarantee that the queries
to F ib are nonterminating and, moreover, that derivations for F ib will not fail if continued to infinity. To
support this, productivity analysis has been developed [KJ15, KJM16] as a compile time technique to detectobservational productivity of logic programs.
Coinductive Logic Programming. Gupta et al. [GBM+ 07]’s coinductive logic programming (CoLP) extends
SLD-resolution with a method to use atomic coinductive hypotheses. That is, during the execution, if thecurrent queries {C1 , ..., Ci , ..., Cn } contain a query Ci that unifies via γ with a C 0 in the earlier execution,then the next step of resolution will be given by {γC1 , ..., γCi−1 , γCi+1 , ..., γCn }. The coinductvie hyposesis
mechanism in CoLP can be viewed as a form of loop detection. However, CoLP cannot detect hypotheses
for more complex patterns of coinduction that produce coinductive subgoals that fail to unify. As discussed
in introduction, it is not a suitable tool to analyze the productivity of infinite data structures in logic
programming.
Proof Relevant Corecursive Resolution. In our previous work [FKSP16], we extended system H with
fixpoint operator to allow constructing corecursive proof evidence (given by proof terms containing fixpoint
operator) for certain nonterminating LP-TM reductions. The type system that we use to justify the corecursive proof evidence is an extension of Howard’s system H with the fixpoint typing rule. There, the main
challenge was to heuristically and automatically construct corecursive evidence for a given query.
Logic Programming by Term Matching. LP-TM reduction may seem to be a rare kind of resolution, but
it underlies many applications. The process of simplifying type class constraints is formally described as thenotion of context reduction by Peyton Jones et. al. [JJM97]. The context reduction process uses exactly theOperational Semantics of Resolution and Productivity in Horn Clause Logic

21

LP-TM reduction that we described in this paper. The logic-based multi-paradigm programming language
PiCAT [ZF13, ZKF15] makes extensive use of term-matching with explicit unification. For example, theFibonacci sequence in PiCAT is defined as follows:
fib(0,F) => F=1.
fib(1,F) => F=1.
fib(N,F),N>1 => fib(N-1,F1),fib(N-2,F2),F=F1+F2.
Through the functionalisation process, the existing termination detection techniques from term rewriting [Ter03] can be directly applied to LP-TM. Thus we think our work in Section 5 builds a useful link
between LP-TM and term rewriting.

8. Conclusions
We have shown that Howard’s system H is a suitable foundation for logic programming. We have provensoundness and completeness of LP-Unif with respect to the type system H. We have developed a partial LPUnif resolution strategy based on labels to control LP-Unif reductions and achieve a form of lazy computation.
Based on partial LP-Unif, we have also defined a new notion of local productivity.
We have formally defined structural resolution as LP-Struct, and showed that it in fact combines termmatching resolution with unification. We have shown that LP-Struct is operationally equivalent to LP-Unif
if the program is LP-TM terminating and non-overlapping. Realizability transformation was suggested as anefficient method to render all logic programs LP-TM terminating and non-overlapping. We have shown thatthe realizability transformation preserves the meaning of the logic program relative to H. The equivalence of
LP-Struct and LP-Unif has been shown, for the transformed program. As a result, we obtained the soundness
and completeness of LP-Struct with respect to H as a corollary.
We have paid a special attention to a study of LP-TM resolution. We have defined a process called
functionalisation that transforms a logic program without existential variables into a term rewriting system.
We have shown the exact relation of LP-TM and term rewriting system, and gave an example of using
dependency pair technique from term rewriting to detect the termination of LP-TM.
For future work, we would like to provide a method to establish local productivity for a given query andstudy the relation between global productivity and local productivity in more detail. We plan to implement
partial LP-Unif and explore its implications.

Acknowledgements
We thank the LOPSTR’15 anonymous referees for their helpful comments and suggestions for the earlier
conference versions of this paper. We thank Tom Schrijvers for exposing us to the nonterminating type classresolution problem and many helpful discussions. This work was funded by EPSRC grant EP/K031864/1-2.
A large part of this research was done at the University of Dundee.

References[AG00]

T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science,
236(12):133 – 178, 2000.
[Bar93]
H. P. Barendregt. Lambda calculi with types, handbook of logic in computer science (vol. 2): background: computational structures, 1993.
[BN98]
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, New York, NY, USA, 1998.
[FKSP16] P. Fu, E. Komendantskaya, T. Schrijvers, and A. Pond. Proof relevant corecursive resolution. In Functional and
Logic Programming - 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings,
pages 126–143, 2016.
+[GBM 07] G. Gupta, A. Bansal, R. Min, L. Simon, and A. Mallya. Coinductive logic programming and its applications. In
Logic Programming, pages 27–44. Springer, 2007.
[GTL89]J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge University Press, New York, NY, USA, 1989.
[HL07]
R. Harper and D. R. Licata. Mechanizing metatheory in a logical framework. Journal of Functional Programming,
17(4-5):613–673, 2007.
[How80]W. Howard. The formulae-as-types notion of construction. In J. Seldin and J. Hindley, editors, To H. B. Curry:
Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490. Academic Press, 1980.

22[JJM97][JKK15][KJ15][KJM16][Kle52][KP11][KPS14][Llo87][LPJ05][MNPS89][NM90][PS99][SBMG07][Ter03][ZF13][ZKF15]

P. Fu and E. Komendantskaya

S. P. Jones, M. Jones, and E. Meijer. Type classes: An exploration of the design space. In In Haskell Workshop,
1997.
P. Johann, E. Komendantskaya, and V. Komendantskiy. Structural resolution for logic programming. In TechnicalCommunications, ICLP, 2015.
E. Komendantskaya and P. Johann. Structural resolution: a framework for coinductive proof search and proof
construction in horn clause logic. ACM Transactions on Computational Logic, submitted, 2015.
E. Komendantskaya, P. Johann, and M.Schmidt. A productivity checker for logic programming. 2016.
S. C. Kleene. Introduction to metamathematics. North-Holland Publishing Company, 1952. Co-publisher: Wolters–
Noordhoff; 8th revised ed.1980.
E. Komendantskaya and J. Power. Coalgebraic derivations in logic programming. In CSL, pages 352–366, 2011.
E. Komendantskaya, J. Power, and M. Schmidt. Coalgebraic logic programming: from semantics to implementation.
Journal of Logic and Computation, 2014.
J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1987.
R. Lämmel and S. Peyton-Jones. Scrap your boilerplate with class: Extensible generic functions. In Proc. 10th
ACM SIGPLAN Int. Conference on Functional Programming, ICFP ’05, pages 204–215, New York, NY, USA,2005. ACM.
D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform proofs as a foundation for logic programming.
Technical report, 1989.
U. Nilsson and J. Maluszyński. Logic, programming and Prolog. Wiley Chichester, 1990.
F. Pfenning and C. Schürmann. System description: Twelfa meta-logical framework for deductive systems. In
Automated DeductionCADE-16, pages 202–206. Springer, 1999.
L. Simon, A. Bansal, A. Mallya, and G. Gupta. Co-logic programming: Extending logic programming with coinduction. In Automata, Languages and Programming, pages 472–483. Springer, 2007.
Terese. Term rewriting systems. Cambridge University Press, 2003.
N.-F. Zhou and J. Fruhman. A users guide to Picat. Available from http://picat-lang.org, 2013.
N.-F. Zhou, H. Kjellerstrand, and J. Fruhman. Constraint Solving and Planning with Picat. Springer, 2015.