A Type-theoretic Approach to Resolution ?
Peng Fu, Ekaterina KomendantskayaComputer Science, University of Dundee

Abstract. We propose a new type-theoretic approach to SLD-resolution
and Horn-clause logic programming. It views Horn formulas as types, andderivations for a given query as a construction of the inhabitant (a proofterm) for the type given by the query. We propose a method of programtransformation that allows to transform logic programs in such a waythat proof evidence is computed alongside SLD-derivations. We discuss
two applications of this approach: in recently proposed productivity theory of structural resolution, and in type class inference.
Keywords: Logic Programming, Typed lambda calculus, Realizability
Transformation, Reduction Systems, Structural Resolution.

1

Introduction

Logic Programming (LP) is a programming paradigm based on first-order Hornformulas. Informally, given a logic program Φ and a query A, LP provides amechanism for automatically inferring whether or not Φ ` A holds, i.e., whether
or not Φ logically entails A. The inference mechanism is based on the SLDresolution, which uses the resolution rule together with first-order unification.
Example 1. 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(Node1 , Node2 )κ3 : ⇒ Connect(Node2 , Node3 )In the above program, Connect is a predicate, and Node1 – Node3 are constants.
SLD-derivation for the query Connect(x, y) can be represented as the following
reduction:Φ ` {Connect(x, y)} κ1 ,[x/x1 ,y/z1 ]{Connect(x, y1 ), Connect(y1 , y)} κ2 ,[Node1 /x,Node2 /y1 ,Node1 /x1 ,y/z1 ]{Connect(Node2 , y)} κ3 ,[Node3 /y,Node1 /x,Node2 /y1 ,Node1 /x1 ,Node3 /z1 ] ∅The first reduction κ1 ,[x/x1 ,y/z1 ] unifies the query Connect(x, y) with the headof the rule κ1 (which is Connect(x1 , z1 ) after renaming) with the substitution[x/x1 , y/z1 ] (x1 is replaced by x and z1 is replaced by y). 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.
?

This work was funded by EPSRC grant EP/K031864/1.

Viewing a program as a collection of Horn clauses, the above derivation
first assumed that Connect(x, y) is false, and then deduced a contradiction (anempty goal) from the assumption. As every SLD-derivation is essentially a proof
by contradiction, traditionally the exact content of such proofs plays little role indetermining entailment. However, it is desirable to have methods which capture
the proof-theoretic content of SLD-derivations. For example, one may wish toreason in a proof-relevant way, and compute not just Φ ` A, but Φ ` p : A,
where p is the proof-witness for the query A and the program Φ. LP and its
dialects are used as part of type inference engines underlying functional [11,6]
and dependently typed [4] languages. These applications require proof-relevant
automated reasoning.
In type class inference (e.g. Haskell), a type class can be seen as an atomic
formula and an instance declaration – as a Horn formula. The instance resolution
process in type class inference can then be seen as an SLD-derivation, with one
additional requirement: this SLD-derivation must compute the evidence for thetype class (or construct a dictionary). For example, the following declaration
specifies a way to construct equality class instances for datatypes List and Char:κ1 : ∀x.Eq(x) ⇒ Eq(List(x))κ2 : ⇒ Eq(Char)

Here List is a function symbol, Char is a constant and x is a variable; κ1 , κ2 will
be used as primitives for the evidence construction. When we make a comparisonof two lists of characters, such as (eq [0 a0 ] [0 b0 ]), the compiler will insert theevidence d of the type Eq(List(Char)) in (eq d [0 a0 ] [0 b0 ]). The construction ofthis evidence can be viewed as resolving the query Eq(List(Char)), which iswitnessed by applying Horn formulas κ1 and κ2 . Thus, (κ1 κ2 ) is the evidence
we want for d.
In order to specify the proof-theoretic meaning of derivations, we introduce a
type-theoretic approach to recover the notion of proof in LP. It has been noticed¬B∨D
can be expressed by means
by Girard [3], that the resolution rule A∨BA∨D
A⇒B B⇒Dof the cut rule in intuitionistic sequent calculus:. Although theA⇒Dresolution rule is classically equivalent to the cut rule, the cut rule is better suitedfor performing computation while preserving constructive content. In Section 2
we present a type system reflecting this intuition: if p1 is the proof of A ⇒ B
and p2 is the proof of B ⇒ D, then λx.p2 (p1 x) is the proof of A ⇒ D. Thus,
proof can be recorded alongside with each cut rule.
We prove that SLD-resolution is sound with respect to the type system (Section 2). We give a formulation of SLD-resolution in the form of a reduction rule,called LP-Unif. The soundness result shows that, given a logic program Φ anda query A, if A can be LP-Unif reduced to the empty goal with a substitution γ
as an answer, then a proof term can be constructed for γA.
In Section 3, we introduce a technique called realizability transformation,
that, given a program Φ, produces a program F (Φ) in which one extra argument
is added to every predicate, in order to record the proof-evidence in derivations.
The proof evidence is computed by applying substitution to variables held by2this additional argument in the course of running SLD-resolution. Let us revisit
the List example. Its transformed version will look as follows:κ1 : ∀x.∀u1 .Eq(x, u1 ) ⇒ Eq(List(x), fκ1 (u1 ))κ2 : ⇒ Eq(Char, cκ2 )The query Eq(List(Char)) of the original program becomes Eq(List(Char), u)
after the transformation, where u is a variable. The derivation reaches the empty
goal and outputs the substitution [fκ1 (cκ2 )/u], which corresponds to the proof
term (κ1 κ2 ) for the query Eq(List(Char)).
Realizability transformation bears resemblance to Kleene’s [7] method under
the same name. We show that realizability transformation preserves the prooftheoretic meaning of the original program and the computational behaviour of
LP-Unif reductions. With the help of the transformation, we prove completenessof LP-Unif with repect to the type system.
Together, Sections 2 and 3 introduce a method of constructing proof evidence in the process of LP derivations. Recently, a variant of resolution for Horn
Clauses, called structural resolution (S-resolution) has been introduced [5]. Sresolution represents derivations by SLD-resolution as a combination of derivations by term-matching and by substitution. We explain this idea in detail in
Section 4. The main reason for separating out two components of SLD-resolution
in such a way is to make use of structural properties of term-matching that havealready been exploited in functional programming and term-rewriting. In particular, S-resolution allowed to define a theory of universal productivity for LP that
resembles a similar theory in functional programming[2]: given a potentially infinite derivation by S-resolution, termination of term-matching derivations thatcomprise it determines productivity of the derivation (or in other words, observability of finite fragments of the infinite computation).
We conjecture that the combination of the two ideas – the theory of productivity introduced by S-resolution and the proof-witness construction introducedin this paper bear promise for future development of resolution-based methods.
This is why, in Section 4 we give a full formal study of how these two methods canbe formally combined. We show how S-resolution can be represented by meansof LP-Struct reductions, combining term-matching reductions and unification.
We extend the type-theoretic semantics to S-Resolution. We define conditions
which guarantee equivalence of S-Resolution and SLD-resolution, one of whichhappens to be exactly the property of productivity. We use the realizability
transformation as a method for guaranteeing productivity of programs.
Finally, in Section 5 we conclude and explain how the combination of SResolution and the type-theoretic approach of this paper could be used in nonterminating cases of type class inference. Detailed proofs for lemmas and theorems in this paper may be found in the extended version1 .
1

Extended version is available at both authors’ homepages.

3

2

A Type System for LP: Horn-Formulas as Types

We first formulate a type system to model LP. We show that LP-Unif is soundwith respect to the type system.
Definition 1.
Term t ::= x | f (t1 , ..., tn )Atomic Formula A, B, C, D ::= P (t1 , ..., tn )(Horn) Formula F ::= [∀x].A1 , ..., An ⇒ A
Proof Term p, e ::= κ | a | λa.e | e e0
Axioms/LP Programs Φ ::= · | κ : F, ΦFunctions of arity zero are called term constants, FV(t) returns all free term
variables of t. We use A to denote A1 , ..., An , when the number n is unimportant.
If n is zero for A ⇒ B, then we write ⇒ B. Note that B is an atomic formula,but ⇒ B is a formula, we distinguish the notion of atomic formulas from (Horn)formulas. The formula A1 , ..., An ⇒ B can be informally read as “the conjunctionof Ai implies B”. We write ∀x.F for quantifying over all the free term variables in
F ; [∀x].F denotes F or ∀x.F . LP program B ⇐ A are represented as ∀x.A ⇒ B
and query is an atomic formula. Proof terms are lambda terms, where κ denotes
a proof term constant and a denotes a proof term variable. We write A 7→σ A0(resp. A ∼γ A0 ) to mean A is matchable (resp. unifiable) to A0 with substitution
σ (resp. γ), i.e. σA ≡ A0 (resp. γA ≡ γA0 ).
The following is a new formulation of a type system intended to provide atype theoretic interpretation for LP.
Definition 2 (Horn-Formulas-as-Types System for LP).
e : F gene : ∀x.F

e1 : A ⇒ D e2 : B, D ⇒ C
cut
λa.λb.(e2 b) (e1 a) : A, B ⇒ C

e : ∀x.F(κ : ∀x.F ) ∈ Φ
inst
axiom
e : [t/x]Fκ : ∀x.F

Note that the notion of type is identified with Horn formulas (atomic intuitionistic sequent), not atomic formulas. The usual sequent turnstile ` is internalized
as intuitionistic implication ⇒. The rule for first order quantification ∀ is placedoutside of the sequent. The cut rule is the only rule that produces new proof
terms. In the cut rule, λa.t denotes λa1 ....λan .t and t b denotes (...(t b1 )...bn ).
The size of a is the same as A and the size of b is the same as B, and a, b are
not free in e1 , e2 .
Our formulation is given in the style of typed lambda calculus and sequentcalculus, the intention for this formulation is to model LP type-theoretically. It
has been observed that the cut rule and proper axioms in intuitionistic sequentcalculus can emulate LP [3](§13.4). Here we add a proof term annotation andmake use of explicit quantifiers. Our formulation uses Curry-style in the sensethat for the gen and inst rule, we do not modify the structure of the proof4

terms. Curry-style formulation allows us to focus on the proof terms generated
by applying the cut rule.
Below is a formulation of SLD-derivation as a reduction system [9].
Definition 3 (LP-Unif reduction). Given 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
along with reductions. We assume implicit renaming of all quantified variables
each time the above rule is applied. We writewhen we leave the underlining
state implicit. We use ∗ to denote the reflexive and transitive closure of .
Notation ∗γ is used when the final state along the reduction path is γ.
Given a program Φ and a set of queries {B1 , . . . , Bn }, LP-Unif uses only
unification reduction to reduce {B1 , . . . , Bn }:Definition 4 (LP-Unif ). Given a logic program Φ, LP-Unif is given by an
abstract reduction system (Φ, ).
∗Lemma 1. If Φ ` {A1 , ..., An }γ ∅, then there exist proofs e1 : ∀x. ⇒γA1 , ..., en : ∀x. ⇒ γAn , given axioms Φ.

Proof. By induction on the length of the reduction.
Base Case. Suppose the length is one, namely, Φ ` {A} κ,γ ∅. It implies that
there exists (κ : ∀x. ⇒ C) ∈ Φ, such that C ∼γ A. So we have κ : ⇒ γC by the
inst rule. Thus κ : ⇒ γA by γC ≡ γA. Hence κ : ∀x. ⇒ γA by the gen rule.
Step Case. Suppose Φ ` {A1 , ..., Ai , ..., An } κ,γ {γA1 , ..., γB1 , ..., γBm , ..., γAn }∗γ 0 ∅, where κ : ∀x.B1 , ..., Bm ⇒ C and C ∼γ Ai . By inductive hypothesis(IH),
we know that there exist proofs e1 : ∀x. ⇒ γ 0 γA1 , ..., p1 : ∀x. ⇒ γ 0 γB1 , ..., pm :∀x. ⇒ γ 0 γBm , ..., en : ∀x. ⇒ γ 0 γAn . We can use inst rule to instantiate thequantifiers of κ using γ 0 · γ, so we have κ : γ 0 γB1 , ..., γ 0 γBm ⇒ γ 0 γC. Sinceγ 0 γAi ≡ γ 0 γC, we can construct a proof ei = κ p1 ... pm with ei : ⇒ γ 0 γAi , byapplying the cut rule m times. By gen, we have ei : ∀x. ⇒ γ 0 γAi . The substitution generated by the unification is idempotent, and γ 0 is accumulated fromγ, i.e. γ 0 = γ 00 · γ for some γ 00 , so γ 0 γAj ≡ γ 00 γγAj ≡ γ 00 γAj ≡ γ 0 Aj for any j.
Thus we have ej : ∀x. ⇒ γ 0 Aj for any j.
Theorem 1 (Soundness of LP-Unif ). If Φ ` {A}proof e : ∀x. ⇒ γA given axioms Φ.

∗γ ∅ , then there exists a

For example, by the soundness theorem above, the derivation in Example 1yields the proof (λb.(κ1 b) κ3 ) κ2 for the formula ⇒ Connect(node1 , node3 ).
Naturally, we would want to prove the following completeness theorem: If
e : ∀x. ⇒ A, then Φ ` {A} ∗γ ∅ for some γ. It is tempting to prove thistheorem by induction on the derivation of e : ∀x. ⇒ A. However, it becomesquite involved. We will discuss a simpler way to prove this theorem at the endof the next section, where we take advantage of the realizability transformation.
5

3

Realizability Transformation

We define realizability transformation in this section. Realizability [7](§82) isa 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 afirst order term to represent the proof of a formula. More specifically, we use afirst order term as an extra argument for a formula to represent a proof of that
formula. Before we define the transformation, we first state several basic results
about the type system in Definition 2.
Theorem 2 (Strong Normalization). Let beta-reduction on proof terms be
the congruence closure of the following relation: (λa.p)p0 →β [p0 /a]p. If e : F ,then e is strongly normalizable with respect to beta-reduction on proof terms.
The proof of strong normalization (SN) is an adaptation of Tait-Girard’s
reducibility proof. Since the first order quantification does not impact the proof
term, the proof is very similar to the SN proof of simply typed lambda calculus.
Lemma 2. If e : [∀x.]A ⇒ B given axioms Φ, then either e is a proof term
constant or it is normalizable to the form λa.n, where n is first order normal
proof term.
Theorem 3. If e : [∀x.] ⇒ B, then e is normalizable to a first order proof term.
Lemma 2 and Theorem 3 show that we can use first order terms to represent
normalized proof terms; and thus pave the way to realizability transformation.
Definition 5 (Representing First Order Proof Terms). Let φ be a mapping from proof term variables to first order terms. We define a representation
function J·Kφ from first order normal proof terms to first order terms.
– JaKφ = φ(a).
– Jκ p1 ...pn Kφ = fκ (Jp1 Kφ , ..., Jpn Kφ ), where fκ is a function symbol.
Definition
6. Let A ≡ P (t1 , ..., tn ) be an atomic formula, we write A[t0 ], whereS( i FV(ti )) ∩ FV(t0 ) = ∅, to abbreviate a new atomic formula P (t1 , ..., tn , t0 ).
Definition 7 (Realizability Transformation). We define a transformation
F on a formula and its normalized proof term:– F (κ : ∀x.A1 , ..., Am ⇒ B) = κ : ∀x.∀y.A1 [y1 ], ..., Am [ym ] ⇒ B[fκ (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 eachpredicate, so that the proof can be recorded alongside with reductions.
Example 2. The following logic program is the result of applying realizability
transformation on the program in Example 1.
6κ1 : ∀x.∀y.∀u1 .∀u2 .Connect(x, y, u1 ), Connect(y, z, u2 ) ⇒ Connect(x, z, fκ1 (u1 , u2 ))κ2 : ⇒ Connect(node1 , node2 , cκ2 )κ3 : ⇒ Connect(node2 , node3 , cκ3 )Before the realizability transformation, we have the following judgement:λb.(κ1 b) κ2 : Connect(node2 , z) ⇒ Connect(node1 , z)We can apply the transformation, we get:λb.(κ1 b) κ2 : Connect(node2 , z, u1 ) ⇒ Connect(node1 , z, J(κ1 b) κ2 K[u1 /b] )which is the same asλb.(κ1 b) κ2 : Connect(node2 , z, u1 ) ⇒ Connect(node1 , z, fκ1 (u1 , cκ2 ))Observe that the transformed formula:Connect(node2 , z, u1 ) ⇒ Connect(node1 , z, fκ1 (u1 , cκ2 )) is provable by λb.(κ1 b) κ2
using the transformed program.
Let F (Φ) mean applying the realizability transformation to every axiom in
Φ. We write (F (Φ), ), to mean given axioms F (Φ), use LP-Unif to reduce agiven query. Note that for query A in (Φ, ), it becomes query A[t] for some tsuch that FV(A) ∩ FV(t) = ∅ in (F (Φ), ).
The following theorem shows that realizability transformation does not change
the proof-theoretic meaning of a program. This is important because it means
we can apply different resolution strategies to resolve the query on the transformed program without worrying about the change of meaning. Later we will
see that the behavior of LP-Struct is different for the original program and thetransformed program.
Theorem 4. Given axioms Φ, if e : [∀x].A ⇒ B holds with e in normal form,
then F (e : [∀x].A ⇒ B) holds for axioms F (Φ).
The other direction for the theorem above is not true if we ignore the transformation F , namely, if e : ∀x. ⇒ A[t] for axioms Φ, it may not be the case thate : ∀x. ⇒ A, since the axioms Φ may not be set up in a way such that t is a
representation of proof e. The following theorem shows that the extra argument
is used to record the term representation of the corresponding proof.
Theorem 5. Suppose F (Φ) ` {A[y]} ∗γ ∅. We have p : ∀x. ⇒ γA[γy] for
F (Φ), where p is in normal form and JpK∅ = γy.
Now we are able to show that realizability transformation will not change
the unification reduction behaviour.
Lemma 3. Φ ` {A1 , ..., An }∗∅ iff F (Φ) ` {A1 [y1 ], ..., An [yn ]}∗∅.

Proof. For each direction, by induction on the length of the reduction. Each
proof will be similar to the proof of Lemma 1.
Theorem 6. Φ ` {A}∗∅ iff F (Φ) ` {A[y]}
7

∗

∅.

Example 3. Consider the logic program after realizability transformation in Example 2. Realizability transformation does not change the behaviour of LPUnif, we still have the following successful unification reduction path for query
Connect(x, y, u):
F (Φ) ` {Connect(x, y, u)} κ1 ,[x/x1 ,y/z1 ,fκ1 (u3 ,u4 )/u]{Connect(x, y1 , u3 ), Connect(y1 , y, u4 )}
κ2 ,[cκ2 /u3 ,node1 /x,node2 /y1 ,node1 /x1 ,b/z1 ,fκ1 (cκ2 ,u4 )/u]{Connect(node2 , y, u4 )}

κ3 ,[cκ3 /u4 ,cκ2 /u3 ,node3 /y,node1 /x,node2 /y1 ,node1 /x1 ,node3 /z1 ,fκ1 (cκ2 ,cκ3 )/u] ∅Now let us come back to the completeness theorem. The following lemmashows that completeness result holds for the transformed program.
Lemma 4. For F (Φ), if n : ⇒ A[JnK∅ ] where n is in normal form, then F (Φ) `{A[JnK∅ ]} ∗ ∅.
Proof. By induction on the structure of n.
– Base Case: n = κ. In this case, JnK∅ = fκ , κ : ∀x. ⇒ A0 [fκ ] ∈ F (Φ)
and γ(A0 [fκ ]) ≡ A[fκ ] for some substitution γ. Thus A0 [fκ ] ∼γ A[fκ ], which
implies F (Φ) ` {A[fκ ]} κ,γ ∅.
– Step Case: n = κ n1 n2 ... nm . In this case, JnK∅ = fκ (Jn1 K∅ , ..., Jnm K∅ ), κ :∀xy. C1 [y1 ], ..., Cm [ym ] ⇒ B[fκ (y1 , ..., ym )] ∈ F (Φ). To obtain n : ⇒ A[JnK∅ ],we have to use κ : ∀x. C1 [Jn1 K∅ ], ..., Cm [Jnm K∅ ] ⇒ B[fκ (Jn1 K∅ , ..., Jnm K∅ )]with γ(B[fκ (Jn1 K∅ , ..., Jnm K∅ )]) ≡ A[JnK∅ ]. By the inst rule, we have κ :γC1 [Jn1 K∅ ], ..., γCm [Jnm K∅ ] ⇒ γB[fκ (Jn1 K∅ , ..., Jnm K∅ )]. Furthermore, it has
to be the case that n1 : ⇒ γC1 [Jn1 K∅ ], ..., nm : ⇒ γCm [Jnm K∅ ]. Thus wehave F (Φ) ` {A[JnK∅ ]} κ,γ {γC1 [Jn1 K∅ ], ..., γCm [Jnm K∅ ]}. By IH, we have
F (Φ) ` {γC1 [Jn1 K∅ ]} ∗γ1 ∅. So F (Φ) ` {A[JnK∅ ]} κ,γ · ∗γ1{γ1 γC2 [Jn2 K∅ ], ..., γ1 γCm [Jnm K∅ ]. Again, we have n2 : ⇒ γ1 γC2 [Jn2 K∅ ], ..., nm :⇒ γ1 γCm [Jnm K∅ ]. By applying IH repeatedly, we obtain F (Φ) ` {A[JnK∅ ]} ∗∅.
Lemma 5. For F (Φ), if F (Φ) ` {A1 [t1 ], ..., An [tn ]}all i, then Φ ` {A1 , ..., An } ∗ ∅.
Proof. By induction on the length of∗∗∅ with FV(ti ) = ∅ for.

– Base Case: F (Φ) ` {A[fκ ]} ∗ ∅. We have κ : ⇒ A0 ∈ Φ such that A0 ∼γ A.
Thus Φ ` {A} κ ∅.
– Step Case: F (Φ) ` {A1 [t1 ], ..., Ai [ti ], ..., An [tn ]} κ,γ{γA1 [t1 ], ..., γB1 [t01 ], ..., γBl [t0l ], ..., γAn [tn ]} ∗ ∅ with ti ≡ fκ (t01 , ..., t0l ) andκ : B1 , ..., Bl ⇒ C ∈ Φ where C ∼γ Ai . So by IH, we have Φ ` {A1 , ..., An } κ,γ{γA1 , ..., γB1 , ..., γBl , ..., γAn } ∗ ∅.
Now we are ready to prove the completeness result.
Theorem 7 (Completeness). If n : [∀x]. ⇒ A, where n is in normal form,
then Φ ` {A} ∗γ ∅.
8

Proof. By Theorem 4, we have n : [∀x]. ⇒ A[JnK∅ ] holds in F (Φ). By Lemma
4, we have F (Φ) ` {A[JnK∅ ]} ∗ ∅. By Lemma 5, we have Φ ` {A} ∗γ ∅.
The completeness result relies on realizability transformation to record theproof steps for a query, so the LP-Unif reduction can just follow the proof steps toreduce the query to the empty set. Together with Theorem 1, this proof systemgives new semantics for derivations in LP.

4

Structual Resolution

S-resolution [5] is a newly proposed alternative to SLD-resolution that allows asystematic separation of derivations into term-matching and unification steps.
A logic program is called productive if the term-matching reduction is terminating for any query. For productive programs with coinductive meaning, finite
term-rewriting reductions can be seen as measures of observation in an infinite
derivation. The ability to handle corecursion in a productive way is an attractive
computational feature of S-resolution.
Example 4. The following program defines the predicate Stream:κ1 : ∀x.∀y.Stream(y) ⇒ Stream(Cons(x, y))It will result in infinite LP-Unif reduction:Φ ` {Stream(Cons(x, y))} κ1 ,[x/x1 ,y/y1 ] {Stream(y)}{Stream(y2 )} κ1 ,[Cons(x3 ,y3 )/y2 ] . . .

κ1 ,[Cons(x2 ,y2 )/y]But it will yield finite term-matching reduction since Stream(y) can not bematched by the head of κ1 (Stream(Cons(x, y))):Φ ` {Stream(Cons(x, y))} →κ1 {Stream(y)} 6→

In general, term-matching reductions are not complete relative to LP-Unif reductions, but we can combine them with substitutional steps to complete derivations. This is exactly the idea behind S-resolution.
Example 5. The following program defines bits and lists of bits:
κ1 : ⇒ Bit(0)κ2 : ⇒ Bit(1)κ3 : ⇒ BList(Nil)κ4 : ∀x.∀y.BList(y), Bit(x) ⇒ BList(Cons(x, y))

LP-Unif would give a complete reduction:Φ ` {BList(Cons(x, y))} κ4 ,[x/x1 ,y/y1 ] {Bit(x), BList(y)}{BList(y)} κ3 ,[Nil/y,0/x,0/x1 ,Nil/y1 ] ∅κ1 ,[0/x,0/x1 ,y/y1 ]But term-matching reduction will not be able to compute an answer in this case.
Φ ` {BList(Cons(x, y))} →κ4 {Bit(x), BList(y)} 6→

9

This is why, S-resolution combines term-matching reductions with additional
substitutional steps, in order to compute the same answer:Φ ` {BList(Cons(x, y))} →κ4 {Bit(x), BList(y)} ,→κ1 ,[0/x] {Bit(0), BList(y)} →κ1 ,[0/x]{BList(y)} ,→κ3 ,[0/x,Nil/y] {BList(Nil)} →κ3 ,[0/x,Nil/y] ∅Completing derivation for Stream in the same way will result in an infinite
derivation, in which every term-matching reduction is finite.
In this section, we embed S-resolution into the type theoretic framework wehave developed in the previous sections. We first define S-derivations in termsof LP-Struct reductions, in the uniform style with LP-Unif reductions, thereby
also defining LP-TM reductions, which resemble reductions in term-rewriting
systems [10]. We then prove that LP-Unif and LP-Struct are operationally equivalent subject to two conditions: productivity and non-overlapping. Finally, weshow how realizability transformation can be used to guarantee productivity oflogic programs in the setting of S-resolution.
4.1

S-resolution in the Type-Theoretic Setting

Definition 8.
– Term-matching(LP-TM) reduction:Φ ` {A1 , ..., Ai , ..., An } →κ,γ 0 {A1 , ..., σB1 , ..., σBm , ..., An } for any substitution γ 0 , if there exists κ : ∀x.B1 , ..., Bn ⇒ C ∈ Φ such that C 7→σ 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 .
The second subscript of term-matching reduction is used to store the substitutions obtained by unification, it is only used when we combine term-matching
reductions with substitutional reductions. The second subscript in the substitutional reduction is intended as a state, it will be updated along with reductions.
Given a program Φ and a set of queries {B1 , . . . , Bn }, LP-TM uses only
term-matching reduction to reduce {B1 , . . . , Bn }:Definition 9 (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 for each successful query.
Theorem 8 (Soundness of LP-TM). If Φ ` {A} →∗ ∅ , then there exists a
proof e : ∀x. ⇒ A given axioms Φ.
Comparing Theorem 1 and Theorem 8, we see that for LP-TM, there is noneed to accumulate substitutions, and the resulting formula is proven as stated.
This difference is due to the use of term-matching instead of unification for the
reduction. The following example shows that the LP-TM is incomplete withrespect to the type system.
10

Example 6. Consider the following program Φ.
κ1 : ⇒ Q(C)
κ2 : ∀x.∀y.Q(x) ⇒ P (y)For query P (C), we have Φ ` {P (C)} →κ2 {Q(x)} 6→. However, there exist a
proof (κ2 κ1 ) : ⇒ P (C), by instantiating x, y to C in κ2 .
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 S-Resolution within our formal framework. Givena program Φ and a set of queries {B1 , . . . , Bn }, LP-Struct first uses termmatching reduction to reduce {B1 , . . . , Bn } to a normal form, then performs
one step substitutional reduction, and then repeats this process.
Definition 10 (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. When we write Φ ` {A}(→µ · ,→1 )∗ {C}, it means a nontrivial
finite path will be of the shape Φ ` {A} →µ · ,→ ·...· →µ · ,→ · →µ {C}.
Now let us see the execution trace of Stream using LP-Struct:Φ ` {Stream(Cons(x, y))} →κ1 {Stream(y)} ,→κ1 ,[Cons(x2 ,y2 )/y]{Stream(Cons(x2 , y2 ))} →κ1 ,[Cons(x2 ,y2 )/y]{Stream(y2 )} ,→κ1 ,[Cons(x3 ,y3 )/y2 ,Cons(x2 ,Cons(x3 ,y3 ))/y]{Stream(Cons(x3 , y3 ))} →κ1 ,[Cons(x3 ,y3 )/y2 ,Cons(x2 ,Cons(x3 ,y3 ))/y] {Stream(y3 )} . . .

Note that the overall reduction is infinite, but each LP-TM reduction is finite.
4.2

LP-Struct and LP-Unif

The next question one may ask is how LP-Struct compares to LP-Unif. They
are not equivalent. Consider the program and the finite LP-Unif derivation of
Example 1. 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.
Therefore, the program of Example 1 is not productive in the sense of [8,5].
Definition 11 (Productivity). We say a program Φ is productive iff every→-reduction is finite.
Perhaps LP-Unif and LP-Struct are operationally equivalent for all productive programs? The following example shows this is not the case.
11

Example 7.
κ1 : ⇒ P (C)κ2 : ∀x.Q(x) ⇒ P (x)Here C is a constant. The program is →-terminating. However, for query P (x),we have Φ ` {P (x)} κ1 ,[C/x] ∅ with LP-Unif, but Φ ` {P (x)} →κ2 {Q(x)} 6,→
for LP-Struct.
Thus, productivity is insufficient for establishing the relation between LPStruct and LP-Unif. In Example 7, the problem is caused by the overlapping
heads P (C) and P (x). Motivated by the notion of non-overlapping rules in term
rewriting systems ([10,1]), we introduce the following definition.
Definition 12 (Non-overlapping Condition). Axioms Φ are non-overlapping
if for any two formulas ∀x.B ⇒ C, ∀x.D ⇒ E ∈ Φ, there are no substitution σ, δsuch that σC ≡ δE.
Theorem 9. Suppose Φ is non-overlapping. Φ ` {A1 , ..., An } ∗γ {C1 , ..., Cm }with {C1 , ..., Cm } in -normal form iff Φ ` {A1 , ..., An }(→µ · ,→1 )∗γ {C1 , ..., Cm }with {C1 , ..., Cm } in →µ · ,→1 -normal form.
The theorem above still requires the termination of the to establish equivalence LP-Unif and LP-Struct. We can weaken this requirement by only requiring
termination of the →-reduction, i.e. by requiring productivity.
Theorem 10 (Equivalence of LP-Struct and LP-Unif ).
non-overlapping and productive.

Suppose Φ is

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 }.
Note that the above theorem does not rely on termination of LP-Unif reductions and therefore establishes equivalence of LP-Unif and LP-Struct evenfor coinductive programs like Stream of Example 4, as long as they are productive and non-overlapping. This effect of productivity has not been described inprevious work.
4.3

Realizability Transformation and LP-Struct

Even when programs are overlapping and unproductive (as e.g. the program of
Example 1), we would still like to obtain a meaningful execution behaviour for
LP-Struct, especially if LP-Unif allows successful derivations for the programs.
Luckily, we already have a method to achieve that, it is the realizability transformation defined in Section 3:
Proposition 1. For any program Φ, F (Φ) is productive and non-overlapping.
12

Proof. First, we need to show →-reduction is strongly normalizing in (F (Φ), →).
By Definition 7, we can establish a decreasing measurement(from right to left,
using the strict subterm relation) for each rule in F (Φ), since the last argumentin the head of each rule is strictly larger than the ones in the body. Then, nonoverlapping property is due to the fact that all the heads of the rules in F (Φ)
will be guarded by the unique function symbol in Definition 7.
Corollary 1.
F (Φ) ` {A1 , ..., An }(→µ · ,→1 )∗ {B1 , ..., Bm } iff F (Φ) ` {A1 , ..., An }{B1 , ..., Bm }.

∗Proof. By Theorem 10 and Theorem 1.
Example 8. For the program in Example 2, the query Connect(x, y, u) can be
reduced by LP-Struct successfully:
F (Φ) ` {Connect(x, y, u)} ,→κ1 ,[x/x1 ,y/z1 ,fκ1 (u3 ,u4 )/u]{Connect(x, y, fκ1 (u3 , u4 ))} →κ1 {Connect(x, y1 , u3 ), Connect(y1 , y, u4 )},→κ2 ,[cκ2 /u3 ,node1 /x,node2 /y1 ,node1 /x1 ,b/z1 ,fκ1 (cκ2 ,u4 )/u]{Connect(node1 , node2 , cκ2 ), Connect(node2 , y, u4 )} →κ2 {Connect(node2 , y, u4 )},→κ3 ,[cκ3 /u4 ,cκ2 /u3 ,node3 /y,node1 /x,node2 /y1 ,node1 /x1 ,node3 /z1 ,fκ1 (cκ2 ,cκ3 )/u]{Connect(node2 , node3 , cκ3 )} →κ3 ∅Note that the answer for u is fκ1 (cκ2 , cκ3 ), which is the first order term representation of the proof of ⇒ Connect(node1 , node3 ).
Realizability transformation uses the extra argument as decreasing measurement in the program to achieve 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 behaviourof LP-Unif. The next example shows that not every transformation techniquefor obtaining structurally decreasing LP-TM reductions has such properties:
Example 9. 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 unification will fail:Φ0 ` {P (List(Int), z)} κ2 ,[Int/x,s(y1 )/z]{P (Int, y1 ), P (List(Int), y1 )} κ2 ,[0/y1 ,Int/x,s(0)/z] {P (List(Int), 0)} 6

13

However, the query P (List(Int)) on the original program using unification reduction will diverge. Divergence and failure are operationally different. Thus adding
arbitrary measurement may modify the execution behaviour of a program (andhence the meaning of the program). In contrast, by Theorems 4-6, realizability
transformation does not modify the execution behaviour of unification reduction.
Example 10. Consider the following non-productive 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, fκ (u))
Both LP-Struct and LP-Unif will diverge for the queries P (x), P (x, y) in bothoriginal 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, fk (u0 ))} → {P (x, u0 )}...
Note that a single step of LP-Unif reduction 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-Struct reduction, which is exactly the correspondence we were looking for.

5

Conclusions and Future Work

We proposed a type system that gives a proof theoretic interpretation for LP:
Horn formulas correspond to the notion of type, and a successful query yields afirst order proof term. The type system also provided us with a precise tool toshow that realizability transformation preserves both proof-theoretic meaning of
the program and the operational behaviour of LP-Unif.
We formulated S-resolution as LP-Struct reduction, which can be seen as a
reduction strategy that combines term-matching reduction with substitutional
reduction. This formulation allowed us to study the operational relation between LP-Struct and LP-Unif. The operational equivalence of LP-Struct and
LP-Unif is by no means obvious. Previous work ([5,8]) only gives soundness andcompleteness of LP-Struct with respect to the Herbrand models. We identified
that productivity and non-overlapping are essential for showing their operational
equivalence.
Realizability transformation proposed here ensures that the resulting programs are productive and non-overlapping. It preserves the proof-theoretic meaning of the program, in a formally defined sense of Theorems 4-6. It is general,applies to any logic program, and can be easily mechanised. Finally, it allows to
automatically record the proof content in the course of reductions, as Theorem 5
establishes, which helps to prove completeness of LP-Unif (Theorem 7).
With the proof system for LP-reductions we proposed, we are planning tofurther investigate the interaction of LP-TM/Unif/Struct with typed functional
14

languages. We expect to find a tight connection between our work and the typeclass inference, cf. [11,6].
In the context of type class inference [11,6], the infinite term-matching behaviour seems pervasive. The example below specifies a possible equality instancedeclaration for nested datatype such asdata Bush a = Nil | Con a (Bush (Bush a)):
κ1 : Eq(x), Eq(Bush(Bush(x))) ⇒ Eq(Bush(x))κ2 : ⇒ Eq(Char)

Here Bush is a function symbol, Char is a constant and x is variable. Consider
the query Eq(Bush(Char)), both LP-Unif and LP-Struct will generate an infinite
reduction path by repeatedly applying κ1 . Using the realizability transformation,
we can obtain a well-behaved (productive) program:κ1 : Eq(x, y1 ), Eq(Bush(Bush(x)), y2 ) ⇒ Eq(Bush(x), fκ1 (y1 , y2 ))κ2 : ⇒ Eq(Char, cκ2 )The substitution for u in the query Eq(Bush(Char), u) will be an infinite term.
But we need a finite representation for such infinite term to construct a dictionary. Such coinductive dictionary construction is the subject of our further
investigations. We would also like to investigate generalizing the type-theoretic
approach from Horn formulas to implicational intuitionistic formulas, the typesystem in this case will correspond to a version of simply type lambda calculus.

References
1. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University
Press, New York, NY, USA, 1998.
2. Y. Bertot and E. Komendantskaya. Inductive and coinductive components ofcorecursive functions in coq. Electronic notes in theoretical computer science,
203(5):25–47, 2008.
3. J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge University
Press, New York, NY, USA, 1989.
4. G. Gonthier, B. Ziliani, A. Nanevski, and D. Dreyer. How to make ad hoc proof
automation less ad hoc. ACM SIGPLAN Notices, 46(9):163–175, 2011.
5. P. Johann, E. Komendantskaya, and V. Komendantskiy. Structural resolution for
logic programming. In Technical Communications, ICLP, 2015.
6. M. P. Jones. Qualified types: theory and practice. Cambridge University Press,
2003.
7. S. C. Kleene. Introduction to metamathematics. North-Holland Publishing Company, 1952. Co-publisher: Wolters–Noordhoff; 8th revised ed.1980.
8. E. Komendantskaya, J. Power, and M. Schmidt. Coalgebraic logic programming:from semantics to implementation. Journal of Logic and Computation, 2014.
9. U. Nilsson and J. Maluszyński. Logic, programming and Prolog. Wiley Chichester,1990.
10. Terese. Term rewriting systems. Cambridge University Press, 2003.
11. P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad hoc. In
Symposium on Principles of Programming Languages, pages 60–76. ACM, 1989.

15

A

Proof of Theorem 2 and 3

We are going to prove a nontrival property about the type system that we justset up. The proof is a simplification of Tait-Girard’s reducibility method.
Definition 13 (Reducibility Set). Let N denotes the set of all strong normalizing proof terms. We define reducibility set REDF by induction on structureof F :– p ∈ REDA1 ,...,An ⇒B with n ≥ 0 iff for any pi ∈ N , p p1 ... pn ∈ N .
– p ∈ RED∀x.A1 ,...,An ⇒B iff p ∈ REDA1 ,...,An ⇒B .
Lemma 6. REDA⇒B = REDφA⇒φB .
Lemma 7. If p ∈ REDF , then p ∈ N .
Proof. By Induction on F :– Base Case: F is of the form A1 , ..., An ⇒ B. By definition, p p1 ... pn ∈ N
for any pi ∈ N . Thus p ∈ N .
– Step Case: F is of the form ∀x.A1 , ..., An ⇒ B. p ∈ RED∀x.A1 ,...,An ⇒B impliesp ∈ REDA1 ,...,An ⇒B . Thus by IH, p ∈ N .
Lemma 8. If e : F , e ∈ REDF .
Proof. By induction on derivation of e : F .
– Base Case:κ : ∀x. ⇒ B
This case κ ∈ N .
– Base Case:κ : ∀x.A1 , ..., An ⇒ B
Since κ is a constant, thus for any pi ∈ N , κ p1 ... pn ∈ N . So κ ∈REDA1 ,...,An ⇒B , thus κ ∈ RED∀x.A1 ,...,An ⇒B .
– Step Case:e1 : A ⇒ D e2 : B, D ⇒ C
cut
λa.λb.(e2 b) (e1 a) : A, B ⇒ C
We need to show λa.λb.(e2 b) (e1 a) ∈ REDA,B⇒C . By IH, we know that(e2 b) (e1 a) ∈ N . Let p1 ∈ N, ..., pn ∈ N, q1 ∈ N, ..., qm ∈ N . We are goingto show for any e with (λa.λb.(e2 b) (e1 a)) p q →β e, then e ∈ N . Weproceed by induction on (µ((e2 b) (e1 a)), µ(p), µ(q)), where µ is a function
to get the length of the reduction path to normal form.
• Base Case: (µ((e2 b) (e1 a)), µ(p), µ(q)) = (0, ..., 0). The only reduction
possible is (λa.λb.(e2 b) (e1 a)) p q →β (e2 q) (e1 p). We know that(e2 q) (e1 p) ∈ N .
• Step Case: There are several possible reductions, but all will decrease(µ((e2 b) (e1 a)), µ(p), µ(q)), thus we conclude that by induction hypothesis.
So λa.λb.(e2 b) (e1 a) ∈ N .
16

– Step Case:e : ∀x.Finste : [t/x]F
By IH, we konw that e ∈ RED∀x.F , so by definition we know that e ∈ REDF .
By Lemma 6, e ∈ RED[t/x]F .
– Step Case:e : F gene : ∀x.F
By IH, we know that e ∈ REDF , so we know that e ∈ RED∀x.F .
Theorem 11 (Strong Normalization). If e : F , then e ∈ N .
Proof. By Lemma 8.
Definition 14 (First Orderness). We say p is first order inductively:– A proof term variable a or proof term constant κ is first order.
– if n, n0 are first order, then n n0 is first order.
Lemma 9. If n, n0 are first order, then [n0 /a]n is first order.
Lemma 10. If e : [∀x.]A ⇒ B, then either e is a proof term constant or it isnormalizable to the form λa.n, where n is first order normal term.
Proof. By induction on the derivation of e : [∀x.]A ⇒ B.
– Base Cases: Axioms, in this case e is a proof term constant.
– Step Case:e1 : A ⇒ D e2 : B, D ⇒ C
cut
λa.λb.(e2 b) (e1 a) : A, B ⇒ C
By IH, we know that e1 = κ or e1 = λa.n1 ; e2 = κ0 or e2 = λbd.n2 . We
know that e1 a will be normalizable to a first order proof term. And e2 b will
be normalized to either κ0 b or λd.n2 . So by Lemma 9, we conclude that
λa.λb.(e2 b) (e1 a) is normalizable to λa.λb.n for some first order normal
term n.
– The other cases are straightforward.
Theorem 12. If e : [∀x.] ⇒ B, then e is normalizable to a first order proof
term.
Proof. By lemma 10, subject reduction and strong normalization theorem.

B

Proof of Theorem 4

Theorem 13. Given axioms Φ, if e : [∀x].A ⇒ B holds with e in normal form,
then F (e : [∀x].A ⇒ B) holds for axioms F (Φ).
Proof. By induction on the derivation of e : [∀x].A ⇒ B.
17

– Base Case:κ : ∀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
cut
λa.λb.(e2 b) (e1 a) : A, B ⇒ C
We know that the normal form of e1 must be κ1 or λa.n1 ; the normal formof e1 must be κ2 or λbd.n2 , with n1 , n2 are first order.
• e1 ≡ κ1 , e2 ≡ κ2 . By IH, we know that F (κ1 : A ⇒ D) = κ1 :A1 [y1 ], ..., A1 [y1 ] ⇒ D[fκ1 (y1 , ..., yn )] and F (κ2 : B, D ⇒ C) = κ2 :B1 [z1 ], ..., Bm [zm ], D[y] ⇒ C[fκ2 (z1 , ..., zm , y)] hold. 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 ], ..., A1 [y1 ], 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 ≡ λbd.n2 . By IH, we know that F (λa.n1 : A ⇒ D) =λa.n1 : A1 [y1 ], ..., A1 [y1 ] ⇒ D[Jn1 K[y/a] ] and F (λbd.n2 : B, D ⇒ C) =λbd.n2 : B1 [z1 ], ..., Bm [zm ], D[y] ⇒ C[Jn2 K[z/b,y/d] ] hold. So by gen andinst, we have
λbd.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 reductions, 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] ]. 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
inst
λa.n : [t/x]A ⇒ [t/x]BBy IH, we know that F (λa.n : ∀x.A ⇒ B) = λa.n : ∀x.∀y.A1 [y1 ], ..., An [yn ] ⇒B[JnK[y/a] ] holds for F (Φ). By Inst rule, we instantiate yi with yi , we haveλa.n : [t/x]A1 [y1 ], ..., [t/x]An [yn ] ⇒ [t/x]B[JnK[y/a] ]– Step Case:e : F gene : ∀x.F
This case is straightforwardly by IH.
18

C

Proof of Theorem 5

Lemma 11. If F (Φ) ` {A1 [y1 ], ..., An [yn ]} ∗γ ∅, and y1 , ..., yn are fresh, thenthere exists proofs e1 : ∀x. ⇒ γA1 [γy1 ], ..., en : ∀x. ⇒ γAn [γyn ] with Jei K∅ = γyigiven axioms F (Φ).
Proof. By induction on the length of the reduction.
– 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 thatC[fκ ] ∼γ1 A[y]. Thus γ1 (C[fκ ]) ≡ γ1 A[γ1 y]. So γ1 y ≡ fκ and γ1 C ≡ γ1 A.
We have κ : ⇒ γ1 C[fκ ] by the inst rule, thus κ : ⇒ γ1 A[γ1 y], hence κ :∀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 [zm ], ..., Bn [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 there
exists proofs e1 : ∀x. ⇒ γγ1 A1 [γy1 ], ..., p1 : ∀x. ⇒ γγ1 B1 [γz1 ], ..., pm :∀x. ⇒ γγ1 Bm [γzm ], ..., en : ∀x. ⇒ γγ1 An [γyn ] and Je1 K∅ = γy1 , ..., Jp1 K∅ =γz1 , ..., Jen K∅ = γyn . We can construct a proof ei = κ p1 ...pm with ei :∀x. ⇒ γγ1 Ai [γγ1 yi ], by first use 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 14. Given axioms Φ, suppose F (Φ) ` {A[y]}∀x. ⇒ γA[γy] where p is in normal form and JpK∅ = γy.

∗γ∅. We have p :Proof. By Lemma 11.

D

Proof of Lemma 3

Lemma 12. If Φ ` {A1 , ..., An }with yi fresh.

∗∅, then F (Φ) ` {A1 [y1 ], ..., An [yn ]}∗∅Proof. By induction on the length of reduction.
– Base Case. Suppose the length is one, namely, Φ ` {A} κ,γ1 ∅. Then there
exists (κ : ∀x. ⇒ C) ∈ Φ such that C ∼γ1 A. Thus κ : ∀x. ⇒ C[fκ ] ∈ F (Φ)
and (C[fκ ]) ∼γ1 [fκ /y] A[y]. So F (Φ) ` A[y]∅.
– Step Case. SupposeΦ ` {A1 , ..., Ai , ..., An } κ,γ1 {γ1 A1 , ..., γ1 B1 , ..., γ1 Bm , ..., γ1 An } ∗γ ∅,where κ : ∀x.B1 , ..., Bm ⇒ C ∈ Φ, C ∼γ1 Ai . So we know that
κ : ∀x.B1 [z1 ], ..., Bm [zm ] ⇒ C[fκ (z)] ∈ F (Φ) and C[fκ (z)] ∼γ1 [fκ (z)/yi ]Ai [yi ]. Thus 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 ]} ∗ ∅.
19

Lemma 13. If F (Φ) ` {A1 [y1 ], ..., An [yn ]}∗∅, then Φ ` {A1 , ..., An }∗∅.

Proof. By induction on the length of reduction.
– Base Case. Suppose the length is one, namely, F (Φ) ` {A[y]} κ,γ1 ∅. Thus
there exists (κ : ∀x. ⇒ C[fκ ]) ∈ F (Φ) such that C[fκ ] ∼γ1 A[y]. ThusC ∼γ1 −[fκ /y] A. So Φ ` A∅.
– 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 [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 } ∗ ∅.

E

Proof of Theorem 9

Lemma 14. If Φ ` {D1 , ..., Di , ..., Dn } →κ,γ {D1 , .., σE1 , ..., σEm , ..., Dn }, with
κ : ∀x.E ⇒ C ∈ Φ and C 7→σ 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 7→σ Di , we have Φ ` {D1 , ..., Di , ..., Dn } κ,σ·γ{σD1 , .., σE1 , ..., σEm , ..., σDn }. But dom(σ) ∈ FV(C), thus we haveΦ ` {D1 , ..., Di , ..., Dn } κ,γ {D1 , .., σE1 , ..., σEm , ..., Dn }.
Lemma 15.
Given Φ is non-overlapping, if Φ ` {A1 , ..., An }(,→κ,γ · →µγ ){C1 , ..., Cm }, thenΦ ` {A1 , ..., An } ∗γ {C1 , ..., Cm }.
Proof. Given Φ ` {A1 , ..., An }(,→κ,γ · →µγ ){C1 , ..., Cm }, we know the actual reduction path must be of the form Φ ` {A1 , ..., An } ,→κ,γ {γA1 , ..., γAn } →κ,γ{γA1 , ..., γB1 , ..., γBn , ..., γAn } →µγ {C1 , ..., Cm }. Note that γ is unchanged along
the term-matching reduction. The → following right after ,→ can not use a different rule other than κ, it would mean γAi ≡ γC with κ : ∀x.B ⇒ C ∈ Φ
and Ai ≡ σB 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 14, we have Φ ` {A1 , ..., An } κ,γ{γA1 , ..., γB1 , ..., γBn , ..., γAn } ∗γ {C1 , ..., Cm }Lemma 16. 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 14 and Lemma 15, we have Φ ` {A1 , ..., An } ∗γ
{C1 , ..., Cm } with {C1 , ..., Cm } in -normal form.
20Lemma 17. 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 ∈ Φ suchthat σC 0 ≡ Ai , since this would means γC ≡ γAi ≡ γσC 0 , violating thenon-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 }.

F

Proof of Theorem 10

We assume a non-overlapping and productive program Φ in this section.
Lemma 18. If Φ ` {A1 , ..., An }{B1 , ..., Bm }, then Φ ` {A1 , ..., An }(→µ1 ∗· ,→ ) {C1 , ..., Cl } and Φ ` {B1 , ..., Bm } →∗ {C1 , ..., Cl }.
Proof. Suppose Φ ` {A1 , ..., An } κ,γ {γA1 , ..., γE1 , ..., γEl , ..., γAn }, with κ :E ⇒ D ∈ Φ and D ∼γ Ai . Suppose D 67→γ Ai . In this case, we have Φ `{A1 , ..., An } ,→κ,γ · →κ,γ {γA1 , ..., γE1 , ..., γEq , ..., γAn } →µγ {C1 , ..., Cl }. Suppose D 7→γ Ai , we have Φ ` {A1 , ..., An } →κ,γ {γA1 , ..., γE1 , ..., γEq , ..., γAn } →µγ{C1 , ..., Cl }.
Lemma 19. If Φ ` {A1 , ..., An } ,→κ,γ {γA1 , ..., γAn } →µγ {B1 , ..., Bm }, thenΦ ` {A1 , ..., An } ∗γ {B1 , ..., Bm }.
Proof. Suppose Φ ` {A1 , ..., An } ,→κ,γ {γA1 , ..., γAn } →µγ {B1 , ..., Bm }, wehave Φ ` {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 14, we have Φ ` {A1 , ..., An } κ,γ{γA1 , ..., γC1 , ..., γCl , ...., γAn } ∗γ {B1 , ..., Bm }.
Lemma 20. If Φ ` {A1 , ..., An }(→µ · ,→1 )∗γ {B1 , ..., Bm }, then Φ ` {A1 , ..., An }{B1 , ..., Bm }.
Proof. By Lemma 19.

21∗γ