Uniform Algebras:

A Complete semantics for

Higher Order Logic programming with HOHH Formulae.

Mary DeMarco Wesleyan University

                  mdemarco@wesleyan.edu

James Lipton Wesleyan University

                                                 jlipton@wesleyan.edu

January 24, 2002

Abstract

This paper introduces a model theory for resolution on Higher Order Hereditarily Harrop formulae (HOHH), the logic underlying the lambda-Prolog programming language. Based on an intuitionistic sequent presentation of Church’s theory of types we call ICTT, the HOHH formalism was introduced by Miller and Nadathur in the late 1980’s and shown to be an instance of their notion of an abstract logic programming language in [17].

The classical Higher-order Horn fragment was shown sound and complete with respect to a semantics introduced by Wolfram in [22], and independently by Blair and Bai in [3], but none has ever been supplied for the full HOHH logic, with intuitionistic implication. HOHH with uniform proofs (a sequent calculus extension of resolution) is here shown sound and and complete with respect to Uniform Algebras, an indexed version of typed Omega-set semantics similar to that introduced by Fourman and Scott in [10]. We develop a bottom-up semantics based on these structures producing a least term model as the least fixed point of an appropriate continuous operator.

1 Introduction

The Lambda Prolog language was first developed in the late 1980’s. It is based on work of Miller, Nadathur, Pfenning, Scedrov, Felty and others aimed at adding to the expressive power of Horn Clause logic programming without sacrificing its declarative transparency by extending the original first-order core to include new connectives and proof rules from well-behaved fragments of higher-order intuitionistic type theory.

Since the classical and intuitionistic theories of both the first and higher-order Horn fragment coincide, the difference in focus between classical and intuitionistic logic has no practical consequences for these logics. The distinction, however, becomes essential when logical extensions that permit implication in goals and clauses are considered.

Intuitionistic formalisms are certainly a plausible candidate for logic programming extensions for a number if reasons. A logical formalism can hardly be considered declarative without the existence (EP) and disjunction (DP) properties: existential goals should not be logical consequences of a program unless some instance is, and backtracking through disjunctive alternatives should not sacrifice completeness. Both properties fail, in general, in classical extensions of Horn Logic, but hold in many intuitionistic extensions.

As it turns out, global satisfaction of EP and DP is not sufficient to guarantee completeness of a suitably operational backwards proof search: each intermediate state of proof search must also satisfy them as well, hence the hereditary or local Harrop requirement of lambda-Prolog programs.

Such operational considerations led Miller et. al. to formulate the general proof-theoretic principle of uniformity in [17], where a cut-free sequent calculus fragment is termed an abstract logic programming language if restriction to a certain class of immediately decomposable deductions, called uniform proofs, does not sacrifice theorems. A class of sequent proofs is uniform if every occurrence, in a deduction, of a sequent

Program ⊢ Goal

with a nonatomic goal may be assumed, without loss of generality, to result from an introduction of the principal goal connective. This guarantees that a backchaining proof search may be restricted to destruction of connectives in the goals until they are atomic without sacrificing completeness. A uniform system is said to admit a search-theoretic interpretation of connectives.^{1}

In HOHH the following new resolution steps arise in addition to back-chaining.

AUGMENT To infer P ⊢ D ⊃ G seek a proof of P ∪ {D} ⊢ G

GENERIC To infer P ⊢ ∀x.G seek a proof of P ⊢ G[c/x] for a fresh constant c,

where the logic is simply typed, contains λ-abstraction and βη reduction as well as suitably restricted higher-order formulae. Thus, implications are now permitted in goals (and in the tails of programs) in such a way as to preserve the Program ⊢ Goal syntax after application of the AUGMENT step, and so is explicit universal quantification.

Computationally, the gains are considerable. The AUGMENT rule permits dynamic loading of modules and a local assert, declaratively. The inclusion of higher-order logic permits declarative definition of higher-order predicates, and greatly facilitates, in conjunction with abstraction and reduction, declarative metaprogramming. These and many other gains are discussed extensively in [14].

Semantics: Declarative and Operational Over the past decade a series of papers have provided semantics for certain classical or intuitionistic fragments of HOHH (see [22, 3]) based on work by Henkin [13] and Andrews [1] on the semantics of Church’s classical Type theory [6]. Nadathur’s dissertation [20] provides a notion of term model for the HOHH fragment. Miller defines a Kripke-like bottom-up semantics for a first-order fragment [15] in which the syntax of programs is built into the notion of model.

In “A semantics for λProlog”, D.A. Wolfram [22] provided semantics for the classical higherorder Horn clause fragment of λProlog, a result which was independently established in Bai and Blair [3] and was built on work in Nadathur’s dissertation [20] and Andrews’ V -complexes [2]. However, the larger hereditarily Harrop fragment considered here requires intuitionistic logic and, consequently, an intuitionistic model theory. Until recently (see [8, 9]) no such semantics had been developed even for the intuitionistic Church’s type theory of which HOHH is an executable fragment.

Operationality: bottom-up semantics In [15], Miller produced an indexed variant of Kripke style models for a first-order fragment of lambda-Prolog in which the conventional definition of truth in Kripke semantics at a possible world p in an arbitrary poset:

p ⊩ A ⊃ B  iff for every q ≥ p,  q ⊩ A ⇒ q ⊩ B  (1)

1The notion of an abstract logic programming language developed by Miller et. al. ended up having a broader scope than we are considering here: uniform proof calculi may exist for carefully chosen presentations of linear and certain classical logics as well, see e.g. FORUM [5, 16].

is replaced by:

P | ⊧ D ⊃ G  iff  P, D | ⊧ G  (2)

where P and D must be program formulae and G a goal. Since the set of possible worlds is fixed in advance, and consists of formulae, this semantics –as far as programs are concerned– contains only term models. This paper addresses this problem by supplying arbitrary carriers for all types, including that of program formulae. We thus generalize Miller’s semantics in [15], and extend it to higher order logic with universal quantification in goals as well.

The reader should note that definition (2) essentially mimics resolution, for which reason we have termed it operational semantics. It is easily shown sound and complete for resolution, and admits a minimal Herbrand-style model, definable as a suitable fixed point.

What is harder is to show that it agrees with full semantic logical consequence. In other words, that an equivalent model of type (1) above exists. The formal difference above between (1) and (2) reflects, in the semantics, the difference between full provability and uniform provability. In our treatment below we also define two notions of model. The former actually defines what is meant by truth in ICTT, the latter provides an operational semantics, in the same sense, for resolution, and also admits a least Herbrand-style model. Since our aim here is to model logic programming, the general semantics for ICTT is briefly sketched. Details can be found in [8, 9].

1.1 The main obstacles

If it is to capture the declarative content of programs, a model theory for HOHH must interpret an intuitionistic fragment of Church’s type theory. In particular, it must be a model for the simply typed lambda-calculus, sound for βη (and hence extensional on functionals). It must also supply a carrier for predicates and interpret the logical constants. Since quantifiers and connectives are higher-order constants in the language, the interpretation of terms cannot be easily divorced from the meaning of propositions. This is one of the reasons we construct a model in which the object of truth values, a (parametrically) complete Heyting Algebra, is distinct from the carriers of the types of propositions.

There are, in addition, a series of requirements peculiar to logic programming that must be met to supply a semantics with respect to which resolution deductions on HOHH are sound and complete. We summarize them here.

Breaking truth-functionality of higher-order predicates: In lambda-prolog we observe the following behavior.

Program:

      module ntf.
      type p o.                               p :- q.
      type q o.                               q :- p.
      type f o -> o.                         f(p).

Queries:

      ?- f(p).
      solved
      ?- f(q).
      no
      ?- f(p & p).
      no

The logical equivalence of p and q, or of p and p ∧ p plays no role in the search for a proof of f(q) or of f(p ∧ p). In other words, the following inference fails in the underlying logic of lambda-Prolog, and in ICTT, when A, B are propositions and the type of p is o ⟶ o:

\frac{A ⟺ B}{p(A) ⟶ p(B)}

Thus, If HOHH-resolution is to be sound and complete with respect to our model theory, the meaning of the formula f(p ∧ p) must not be identified with f(p). Once again, this is achieved by separating the cHa object of truth values Ω from the carrier D_{o} of propositions. Although p and p ∧ p will have the same truth value in Ω, they will not be identified in D_{o}, making it possible to consistently assign different truth values to f(p ∧ p) and f(p).

The logical intensionality problem: Models must be extensional on lambda terms: if f and g are terms, say, of type α → β, with α not the type o of truth-values, and if for all individuals u in the model’s carrier of type α

[[f ]]u = [[g]]u

then

[[f ]] = [[g]]

However, we need to enforce a certain kind of meta-level failure of logical extensionality. Wolfram [22] gives an example of the non-extensional behavior of λProlog, which we translate into Church’s type-theoretic notation:

p X :- q X.  ∀x_{o}.(q_{oo}(x_{o}) ⊃ p_{oo}(x_{o}))
q X :- p X.  ∀x.(p(x) ⊃ q(x)
r p.  r_{o(oo)}(p_{oo})
?- r q.  The goal r_{o(oo)}(q_{oo})
no.  is not derivable from the program clauses above.

p and q are interpreted as two truth-valued functions which agree on all arguments, which must not be allowed, in general, to have the same meaning in a model.

This is also solved by distinguishing between the carriers of the types of logical formulae and the object Ω of truth-values. The logical equivalence of p and q on predicates takes place in Ω, not in the carrier of their type, so they are not required to have the same denotation in the carrier. This problem was solved using a different technique by Wolfram for the HOH fragment.

The variable indexing problem: We will need to construct a countable hierarchy of universes (signatures), in order to deal with the inconsistency that arises from allowing pre-existing logic variables to unify with constants introduced during execution for the sake of universal goals (see figure 1.1).

We will need a supply of countably many fresh variables and constants at each integer level i and at every type α, as is further explained in the development of the UCTT type theory, below.

The monotonicity problem: Because HOHH formulae include implication, and hence contain negatively occurring subformulae, the obvious choice for a least term model for a logic program is not describable as a union from below of a monotone sequence of finitely generated ICTT-model fragments. We solve this problem by extending Miller’s idea of indexed Kripke

Consider the following incorrect resolution “deduction” of

∀x.Qxx ⊃ ∃y∀z.Qyz

from the empty program.

?- ∀x.Qxx ⊃ ∃y∀z.Qyz
⇝^{⊃} ∀x.Qxx ?- ∃y∀z.Qyz
⇝^{∃} ∀x.Qxx ?- ∀z.Qyz
⇝^{∀} ∀x.Qxx ?- Qyc
⇝^{[c/y]} NULL

versus the following failed deduction in which a counter keeps track of changing signatures, and the (indexed) logic variable y_{0} created when signature 0 was the ambient signature, is inhibited from unification with constant c_{1} belonging to signature 1.

0 ∅ ?- ∀x.Qxx ⊃ ∃y∀z.Qyz
⇝^{⊃} 0 ∀x.Qxx ?- ∃y∀z.Qyz
⇝^{∃} 0 ∀x.Qxx ?- ∀z.Qy_{0}z
⇝^{∀} 1 ∀x.Qxx ?- Qy_{0}c_{1}
F AIL

Figure 1: Why indexing of variables is required

models [15] to allow for fibred or indexed carriers for all the logical components of programs and goals. We have carriers D_{i,a}, D_{i,r}, D_{i,g}, D_{i,h} that interpret atoms, rigid atoms, goals and propositions, and the appropriate functions between them (the additional index i is explained in the preceding paragraph). We also define a formal system (UCTT) in which these logical subtypes exist in the syntax.

2 The Calculus

Church’s calculus consists of a collection of higher-order functional types together with a simply typed lambda-calculus of terms. Connectives and quantifiers are explicit typed constants in the calculus which permits the formalization of full higher-order logic without adding any new operations. In more detail:

Type expressions are formed from a set of base types (which must include at least the type ι of individuals and o of truth values, or formulae) via the functional type: if α and β are types then so is α ⟶ β. Church’s notation for functional type expressions is sometimes more convenient because of its brevity: (βα) denotes the type α ⟶ β. Association, in Church’s notation, is to the left: αβγ denotes (αβ)γ, meaning γ ⟶ (β ⟶ α). We will use his notation interchangeably with arrow notation, especially with complex type expressions.

Terms are always associated with a type expression, and are built up from typed constants and typed variables (countably many at each type α): x_{α}^{1}, x_{α}^{2}, …, y_{α}^{1}, y_{α}^{2}, … according to the following definition:

1. A variable x_{α} is a term of type α.

2. A constant of type α is is a term of type α.

3. If t_{1} is a term of type α ⟶ β and t_{2} is a term of type α then t_{1}t_{2} is a term of type β.

4. If t is a term of type β then λx_{α}.t is a term of type α ⟶ β.

Terms may be displayed subscripted with their associated type, when convenient. We omit such subscripts from variables when clear from context, or when the information is of no interest.

Logical Constants The following logical constants are available to define formulas:

⊤_{o}, ⊥_{o}, ∧_{ooo}, ∨_{ooo}, ⊃_{ooo},

as well as

Σ_{o(oα)} and Π_{o(oα)},

the latter two existing at all types α.

Reduction We recall that the transitive closure of the operation on terms induced by permitting contraction of subterms that are β-redices, λx_{α}.t u, to t[u/x], the result of substituting (after renaming of bound variables if necessary to avoid capture) u for all free occurrences of x in t, is called β-reduction. Contraction of η-redices λx.tx to t when x does not occur freely in t induces η-reduction. In this paper we will refer to the combination of both reductions, βη-reduction as λ-reduction, and the reflexive, symmetric, transitive closure of this relation as λ-equivalence. In Church’s Theory, as in Miller and Nadathur’s work, a canonical listing of variables is used to ensure the existence of unique canonical normal forms (sometimes denoted ρ(t)) for each term t.

Definition 2.1 A formula is any term of type o. An atomic formula is a term of type o which is not λ-equivalent to any term whose head is a logical constant.

The meaning of the logical constants ∧, ∨ and ⊃ is evident, while Σ and Π are used to define the quantifiers ∃ and ∀: ∃x_{α}P_{o} is an abbreviation for Σ_{o(oα)}λx_{α}.P_{o} and ∀x_{α}P_{o} is an abbreviation for Π_{o(oα)}λx_{α}.P_{o}. Also f(x_{α}) is an abbreviation of (f_{βα}x_{α}).

2.1 Deduction

We will assume familiarity with Gentzen’s sequent calculus, and in particular the intuitionistic LJ (see e.g. [12]). We present here (in Fig. 2) a sequent system for the intuitionistic fragment of Church’s Theory of Types, which we call ICTT, almost identical to [17] of Miller, Nadathur et al.

In fig. 2, all sequents Γ ⟶ ⟶ Δ consist of a set of formulas (antecedents) Γ and a single formula Δ (consequent). The rules of inference shown in the figure consist of premisses the zero, one or two sequents above the line and conclusions the lone sequent below the line. Rules marked with an asterisk must not contain free occurrences of the index variable below the line. In rule λ, the primed and unprimed antecedents (resp. consequents) are λ-equivalent.

The following lemmas will prove useful. Their proofs are routine.

Lemma 2.2 There is a sequent proof of Γ, B ⟶ ⟶ B for any set of formulas Γ and any formula B.

Lemma 2.3 If Γ′ ⊇ Γ and Γ ⟶ ⟶ Δ then Γ′ ⟶ ⟶ Δ.

Lemma 2.4 If Γ, B(x_{α}) ⟶ ⟶ Δ or Γ ⟶ ⟶ B(x_{α}) and x_{α} does not occur in Γ or Δ, then Γ, B(t) ⟶ ⟶ Δ or Γ ⟶ ⟶ B(t), respectively, for any term t of type α.

Γ ⟶ ⟶ ⊤  Γ, A ⟶ ⟶ A  Γ, ⊥ ⟶ ⟶ ⊥

{Γ, B, C ⟶ ⟶ Δ \atop Γ, B ∧ C ⟶ ⟶ Δ} ∧_{L}  \begin{matrix}Γ ⟶ ⟶ B & Γ ⟶ ⟶ C \\ Γ ⟶ ⟶ B ∧ C \end{matrix} ∧_{R}

\begin{matrix}Γ, B ⟶ ⟶ Δ & Γ, C ⟶ ⟶ Δ \\ Γ, B ∨ C ⟶ ⟶ Δ \end{matrix} ∨_{L}  {Γ ⟶ ⟶ B_{i} \atop Γ ⟶ ⟶ B_{1} ∨ B_{2}} ∨_{R}

\begin{matrix}Γ ⟶ ⟶ B & Γ, C ⟶ ⟶ Δ \\ Γ, B ⊃ C ⟶ ⟶ Δ \end{matrix} ⊃_{L}  {Γ, B ⟶ ⟶ C \atop Γ ⟶ ⟶ B ⊃ C} ⊃_{R}

{Γ, P [t/x] ⟶ ⟶ Δ \atop Γ, ∀x.P ⟶ ⟶ Δ} ∀_{L}  {Γ ⟶ ⟶ P \atop Γ ⟶ ⟶ ∀x.P} ∀_{R} ∗

{Γ, P ⟶ ⟶ Δ \atop Γ, ∃x.P ⟶ ⟶ Δ} ∃_{L} ∗  {Γ ⟶ ⟶ P [t/x] \atop Γ ⟶ ⟶ ∃x.P} ∃_{R}

{Γ′ ⟶ ⟶ Δ′ \atop Γ ⟶ ⟶ Δ} λ  {Γ ⟶ ⟶ ⊥ \atop Γ ⟶ ⟶ B} ⊥_{R}

Figure 2: Higher-order Sequent Rules

Comparison with Church’s original calculus Calling this system the intuitionistic fragment of Church’s Theory of Types as presented in [6] requires a bit of justification, since his calculus includes a typed equality operator, a choice operator, and, because its logic is classical, all connectives are reduced to disjunction, negation and universal quantification. His proof system is composed of 6 rules of inference and 11 axiom schemas. If we remove those schemas which involve equality and the choice operator, we obtain a set of 6 axioms, the last of which is the clearly classical

∀x_{α}[p ∨ f_{oα}] ⊃ p ∨ Π_{o(oα)}f_{oα}.

If we leave only axiom schemas 1-5, we obtain a theory (IC) which, it can be shown, is equivalent to ICTT. We will not take the time to establish this here, but it is straightforward to show that IC axioms 1-5 are sound with respect to the semantics presented below, but that axiom 6 fails.

3 Models for ictt

We define a class of models for ictt with respect to which ictt is sound and complete.

Mitchell and Moggi [19] incorporate applicative structures into Kripke models to model equational reasoning in the typed lambda calculus. We use a similar approach to combine applicative structures with Heyting algebra semantics [21, Chap. 13, §4] for constructive logic.

Definition 3.1 A lattice is a partially ordered set with two operations ∧ and ∨, the meet and join, satisfying the following axioms for all members a, b and c of the set:

a ≤ a ∨ b b ≤ a ∨ b  (3)
a ∧ b ≤ a a ∧ b ≤ b  (4)

a ≤ c and b ≤ c implies a ∨ b ≤ c  (5)
c ≤ a and c ≤ b implies c ≤ a ∧ b  (6)

A lattice is distributive if for all members a, b and c of the partially ordered set,

a ∧ (b ∨ c) = (a ∧ b) ∨ (a ∧ c)  (7)
a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c)  (8)

The join ⋁ S of an arbitrary set S, if it exists, is the least upper bound of the set. Likewise, the meet ⋀ S would be its greatest lower bound.

The meet and join serve to model conjunction and disjunction, but we need an additional operator corresponding to implication. The following definition of a Heyting (or pseudo-Boolean) algebra is taken from [21].

Definition 3.2 A Heyting algebra H is a lattice with a least element ⊥ and an operation → defined on all pairs of elements of H such that

a ∧ b ≤ c if and only if a ≤ b → c  (9)

In a complete Heyting algebra, arbitrary meets and joins exist.

We will use Heyting algebras with certain arbitrary meets and joins corresponding to universal and existential quantification.

In [21] we also learn that a Heyting algebra is distributive and that if ⋁ B exists then

a ∧ ⋁ B = ⋁{a ∧ b : b ∈ B}  (10)

It is clear from (4) and (9) that a Heyting algebra has a top element, which we denote ⊤.

Example 3.3 The open subsets of ℝ form a Heyting algebra with ∨ denoting union, ∧ the interior of the intersection, ≤ the subset relation, ⊥ the empty set and a → b := ⋃{w : w∩a ⊆ b}. Then ⊤ is evidently ℝ and (10) holds, but the analogous statement

a ∨ ⋀ B = ⋀{a ∨ b : b ∈ B}

is false: let a be ℝ\\{0\} and B be the set of intervals \{(−\frac{1}{n}, \frac{1}{n}) : n ∈ ℕ\}. Here a∨⋀ B = a∨∅ = a but ⋀{a ∨ b : b ∈ B} = ⋀{ℝ : b ∈ B} = ℝ.

This false proposition corresponds to the formula A ∨ ∀x.B(x) iff ∀x.(A ∨ B(x)), which is not true in constructive logic and which we therefore do not want to force in all models. This formula corresponds in turn to Axiom 6^{α} of [6], which makes Church’s Theory of Types classical.

3.1 Applicative Structures

We will make use of the notion of applicative structures, a well-known semantical framework for the simply-typed lambda calculus, first introduced by H. Friedman in [11]. (See also [18].)

Definition 3.4 A typed applicative structure ⟨D, App, Const⟩ consists of a set D_{α} for each type α, a function App : D_{βα} × D_{α} → D_{β} for each pair (α, β) of types, and an intepretation function Const taking constants of type α to elements of D_{α}.

A typed applicative structure is extensional if for every f, g in D_{βα}, App(f, d) = App(g, d) for all d ∈ D_{α} implies f = g. Hence any two functions in the language which behave alike semantically must be identified in the semantics.

An assignment φ is a function from the free variables of the language into D which respects types. Given a typed applicative structure D, an environmental model consists of a (total) function [[ ]]_{φ} from the open terms of the language into D for each assignment φ such that [[λx_{α}.M_{β} ]]_{φ} ∈ D_{βα} and the following equalities hold:

[[c]]_{φ} = Const(c)  for constants c
[[x]]_{φ} = φ(x)  for variables x
[[(MN) ]]_{φ} = App( [[M ]]_{φ}, [[N ]]_{φ})
App( [[λx_{α}.M_{β} ]]_{φ}, d) = [[M ]]_{φ[x→d]}

The requirement that [[ ]]_{φ} be a total function, called the environment model condition in [18], insures that all lambda terms will have an interpretation.

Now we can define models for our intuitionistic theory of types. We add certain restrictions to typed applicative structures for ictt to handle the logical constants and predicates.

Definition 3.5 A Heyting applicative structure ⟨D, App, Const, Ω⟩ for ictt is a typed applicative structure with an associated Heyting algebra Ω and function ω from D_{o} to Ω such that for each f in D_{oα}, Ω contains the meets and joins

⋀{ω(App(f, d)) : d ∈ D_{α}} and ⋁{ω(App(f, d)) : d ∈ D_{α}},

and the following conditions are satisfied:

ω(Const(⊤_{o})) = ⊤_{Ω}
ω(Const(⊥_{o})) = ⊥_{Ω}
ω(App(App(Const(∧_{ooo}), d_{1}), d_{2})) = ω(d_{1}) ∧ ω(d_{2})
ω(App(App(Const(∨_{ooo}), d_{1}), d_{2})) = ω(d_{1}) ∨ ω(d_{2})
ω(App(App(Const(⊃_{ooo}), d_{1}), d_{2})) = ω(d_{1}) → ω(d_{2})
ω(App(Const(Σ_{o(oα)}), f)) = ⋁{ω(App(f, d)) : d ∈ D_{α}}
ω(App(Const(Π_{o(oα)}), f)) = ⋀{ω(App(f, d)) : d ∈ D_{α}}

A definition identifying D_{o} with Ω (i.e.,, restricting ω to the identity function) would be more natural but would make A ∧ B indiscernable from B ∧ A in the model and thereby identify the truth values of P_{oo}(A_{o} ∧ B_{o}) and P_{oo}(B_{o} ∧ A_{o}). This identity holds neither in ictt as presented here nor in hohh, to be considered in the next chapter.

An assignment is a function from the variables in the language to the elements of the model which allows us to give meaning to open terms. An assignment φ must satisfy φ(x_{α}) ∈ D_{α}.

Definition 3.6 A model for ictt is an assignment-indexed interpretation function ℌ = {ℌ( )_{φ} : φ an assignment} into a Heyting applicative structure ⟨D, App, Const, Ω⟩ which takes (possibly open) terms of type α into D_{α} and satisfies the following:

ℌ(c)_{φ} = Const(c)  for constants c
ℌ(x)_{φ} = φ(x)  for variables x
ℌ(M)_{φ} = ℌ(N)_{φ}  M λ-equivalent to N
ℌ((MN))_{φ} = App(ℌ(M)_{φ}, ℌ(N)_{φ})
App(ℌ(λx_{α}.M_{β})_{φ}, d) = ℌ(N)_{φ[d/x]})

Given a model ℌ and an assignment φ, we say that φ satisfies B in ℌ if ω(ℌ(B_{o})_{φ}) = ⊤_{Ω}; we abbreviate this assertion to ℌ ⊧_{φ} B_{o}. We say B_{o} is valid in ℌ (equivalently, ℌ ⊧ B_{o}) if ℌ ⊧_{φ} B_{o} for every assignment φ. We abbreviate ω(ℌ(B_{o})_{φ}) to [[B_{o}]]_{φ}. We also omit the subscript φ when our intentions are clear.

3.2 Soundness and Completeness

The following lemma is easy to prove and motivates the definition given below of the meaning of a sequent in a model.

Lemma 3.7 There is a sequent proof of Γ ⟶ ⟶ B ⊃ C if and only if there is a sequent proof of Γ, B ⟶ ⟶ C.

Definition 3.8 (Truth of sequents in a model) We define the meaning of a sequent in a model by

[[Γ ⟶ ⟶ Δ ]] := [[⋀ Γ ⊃ Δ ]]

where ⋀ Γ signifies the conjunction of the elements of Γ and where we recall that, in an intuitionistic calculus, the consequent Δ is restricted to a single formula.

Note that [[⋀ Γ ⊃ Δ ]] = ⊤ if and only if ⊤ ≤ [[⋀ Γ ⊃ Δ ]], which is to say ⊤ ≤ [[⋀ Γ ]] → [[Δ ]], which by the condition on → is equivalent to ⊤ ∧ [[⋀ Γ ]] ≤ [[Δ ]], which in turn is equivalent to [[⋀ Γ ]] ≤ [[Δ ]] by (4) and (6). We will abbreviate [[⋀ Γ ]] to [[Γ ]] and use the formulation [[Γ ]] ≤ [[Δ ]] or more explicitly, [[Γ ]]_{φ} ≤ [[Δ ]]_{φ}, henceforth.

The proofs of the following theorems can be found in [8, 9]

Theorem 3.9 (Soundness) If Γ ⟶ ⟶ Δ is provable in ictt then [[Γ ⟶ ⟶ Δ ]] equals ⊤_{Ω} in every model ℌ of ictt.

Theorem 3.10 (Completeness) If [[Γ ]] ≤ [[Δ ]] in all models ℌ, then there is a sequent proof of Γ ⟶ ⟶ Δ.

4 Stratifying logic to reflect Program Structure

In our definition of an operational logic and proof theory we formalize some of the metamathematics implicit in the interpretation and logic programs and in the structure of logical states. Since indexed constants and signature levels, and program-goal pairs are handled explicitly in the interpreter and in run-time logical states, they appear formally in the syntax. Each type is assumed to have indexed variables and constants. Programs and goals and their fundamental components have their own logical subtypes. In order not to encumber the syntax excessively, or make too great a departure from the type theory on which it is based, we have refrained from introducing indexed types to reflect computation stages, but in the semantics we will have stratified carriers for terms at different index levels. Our operational formal system is called UCTT, for the Uniform-proof (resolution) version of Church’s Theory of types.

Before presenting the calculus we review the definition of HOHH programs and goals, upon which UCTT based.

4.1 Higher-order Programs

Let H be the set of positive terms, the (λ-normal form) terms which do not include ⊥ or ⊃; A will refer to an atomic formula over H and A_{r} to a rigid atomic formula over H. In this case, an atomic formula is a λ-normal form term whose top-level symbol is not a logical constant, and a rigid atomic formula is an atomic formula whose top level symbol is also not a variable. Let G refer to a goal formula in λ-normal form, D to a definite clause (that is, a single program formula), and P to a set of program formulae; P ∪ D will stand for P ∪ {D}.

Definition 4.1 hohh program formulae D and goal formulae G are given by:

D ::= A_{r} | D ∧ D | G ⊃ A_{r} | ∀x.D
G ::= ⊤ | A | G ∨ G | G ∧ G | ∃x.G | D ⊃ G | ∀x.G

The hohh^{+} fragment is similar to this one, but A_{r} is restricted not to rigid atoms but to atomic formulae in which the head may not be “essentially existentially quantified”. λ-Prolog is, in fact, slightly stronger, even, than this fragment. See [14] for details.

In UCTT rigid atoms, atoms, programs and goals are simply the terms of the corresponding subtypes of the type h of logical formulae. Certain constants and functions are barred from the calculus to make it impossible to form illegal programs or goals. In particular, all terms appearing in atomic formulae are positive.

4.2 The UCTT calculus

The base types are the types ι of individuals, h of truth-values, a of atoms, r of rigid atoms, p of programs and g of goals. All other types are functional types βα. The logical constants are ⊤_{g}, ⊤_{h}, ∧_{ppp}, ∧_{ggg}, ∧_{hhh}, ∨_{ggg}, ∨_{hhh}, ⊃_{gpp}, ⊃_{prg}, Σ_{g(gα)}, Σ_{h(hα)}, Π_{g(gα)}, Π_{p(pα)} and Π_{h(hα)}. There may be no other constants or variables of types p or g, nor of functional types involving p or g. Constants of type rα and both constants and variables of type aα are allowed but no other functional types involving r or a are.

4.3 Signatures

As explained in an earlier section and in figure (1.1), we will need to construct a countable hierarchy of universes (signatures), in order to deal with the inconsistency that arises from allowing pre-existing logic variables to unify with constants introduced during execution for the sake of universal goals.

Let U_{0}(α) include all constants and variables of type α appearing in the original programs and goals along with countably many more logic variables; constants and variables of U_{0} are considered to be labelled with the integer 0. The set U_{i}(α) will include U_{i−1}(α) along with a new set of countably many logic variables and countably many fresh constants of type α.

A (positive) term over U_{i} contains only typed constants and variables from the set U_{i}(α). A program over U_{i} is a program whose terms are all over U_{i}. In the models, the restriction f_{i}(c_{j}) ∈ U_{max{i,j}} will be desirable, but in the syntax λ-conversions will not introduce undesirable indices.

4.4 UCTT Resolution Rules for hohh formulae

From now on, programs-formulae, goals, rigid atoms and atoms refer to λ-normal forms of terms of the correspoinding types p, g, r and a. We now present the proof theory for UCTT. Only goals may occur as theorems, only signature-program pairs as premisses.

Instead of a sequent system, we use an operational proof system so as better to model the behavior of programs. Rather than automate the ∧_{L} and ∀_{L} rules of the sequent calculus explicitly, we decompose the program into conjuncts and instances. For technical reasons we retain the original program clauses as well.

Definition 4.2 For a given program P over U_{i}, the extended program over U_{i}, denoted [i; P], is defined recursively as follows:

• If D ∈ P, then D ∈ [i; P].

• If D_{1} ∧ D_{2} ∈ [i; P], then D_{1} ∈ [i; P] and D_{2} ∈ [i; P].

• If ∀x_{α}.D_{β} ∈ [i; P], then ρ(D(t)) ∈ [i; P] for all positive terms t over U_{i}(α).

Note that we often identify programs, as sets of formulae, with the single formula obtained by taking the conjunction of its members, which leads to some abuse of notation. If P is a program formula, the first clause of the definition above would make no sense unless it read P ∈ [i; P]. But we understand it to apply to the program {P }.

Besides the familiar index restrictions, substitution must also respect sorts.

Definition 4.3 Let the signatures be given as above.

A state is a trio ⟨i; P | G⟩ where P is a program and G a goal, both over the signature U_{i}; i is referred to as the state index.

A state vector ⟨i_{1}; P_{1} | G_{1}⟩, …, ⟨i_{j}; P_{j} | G_{j}⟩, …, ⟨i_{n}; P_{n} | G_{n}⟩ is a finite sequence of states. State vectors will be abbreviated to 𝔄, ⟨i; P | G⟩, 𝔅, where 𝔄 and 𝔅 denote (possibly empty) finite sequences of states.

A null resolution vector is a state vector of the form ⟨i_{1}; P_{1} | ⊤⟩, …, ⟨i_{n}; P_{n} | ⊤⟩. It may be the empty sequence.

Note that the NULL vector may itself be a derivation with no steps.

State vectors are required on several accounts: the index provides for manipulation of universal quantification; the program is included because it may be augmented to prove conditional goals; and thus a vector of multiple states is necessary for the decomposition of conjunctive goals, since proof of the conjuncts may require different manipulations of index and program.

When a substitution is applied to a program P, it is understood to be applied to each clause of P. When applied to a state vector 𝔄, it is understood to be applied to the program and to the goal of each state in the vector. For example, if 𝔄 were the vector ⟨i_{1}; P_{1} | G_{1}⟩, …, ⟨i_{n}; P_{n} | G_{n}⟩, then 𝔄θ would be ⟨i_{1}; P_{1}θ | G_{1}θ⟩, …, ⟨i_{n}; P_{n}θ | G_{n}θ⟩.

We will call a substitution legal if it is legal in the usual sense of avoiding variable capture and is in addition restricted by the labels, so that only terms over the universe U_{i} are be substituted for a logic variable of label i. In the case of quantified variables, however, we use bracket notation to indicate that the replacement is made in accordance with the resolution rules for quantifiers regardless of the indices involved.

Resolution rules The resolution reduction rules for hohh are nearly identical to those of the first-order case. We make minor changes for handling higher-order terms. Legal substitutions preserve index-level and types. The operator ρ appearing in the instance and generic rules is lifted from Andrews and Miller’s papers. It is a map from lambda-terms to some suitably chosen canonical representation of their normal forms, obtained, e.g. by fixing some canonical order on all variables.

identity 𝔄, ⟨i; P | A′⟩, 𝔅 ⇝^{θ} 𝔄θ, 𝔅θ

where θ is legal, A atomic, A′θ =_{β} Aθ, and A ∈ [i; P].

backchain 𝔄, ⟨i; P | A′⟩, 𝔅 ⇝^{θ} 𝔄θ, ⟨i; P θ | Gθ⟩, 𝔅θ

where θ is legal, A atomic, (G ⊃ A) ∈ [i; P], and A′θ =_{β} Aθ.

or_{j} 𝔄, ⟨i; P | G_{1} ∨ G_{2}⟩, 𝔅 ⇝^{∨} 𝔄, ⟨i; P | G_{j}⟩, 𝔅

and 𝔄, ⟨i; P | G_{1} ∧ G_{2}⟩, 𝔅 ⇝^{∧} 𝔄, ⟨i; P | G_{1}⟩, ⟨i; P | G_{2}⟩, 𝔅

instance 𝔄, ⟨i; P | ∃x.G⟩, 𝔅 ⇝^{∃} 𝔄, ⟨i; P | ρ((λx.G)(v_{i}))⟩, 𝔅

where v_{i} is a fresh logic variable of label i.

augment 𝔄, ⟨i; P | D ⊃ G⟩, 𝔅 ⇝^{⊃} 𝔄, ⟨i; P ∪ D | G⟩, 𝔅

generic 𝔄, ⟨i; P | ∀x.G⟩, 𝔅 ⇝^{∀} 𝔄, ⟨i + 1; P | ρ((λx.G)(c_{i+1}))⟩, 𝔅

where c_{i+1} is a fresh constant of label i + 1.

4.5 Uniform Algebras

Our model theory for UCTT is a variant of Heyting Applicative Structure semantics for the intuitionistic version of Church’s Theory of types sketched earlier in the paper. It brings together several of the ideas discussed above: Miller’s indexed model theory for a first-order fragment of FOHH (we assign meaning to goals G with respect to ambient programs P), stratification of carriers to represent different index levels, separate carriers for programs and goals and their components, and an object Ω of truth values (a lattice with enough infinite suprema) distinct from the carrier of logical formulae. Like Miller’s model, carriers of programs have a Kripke-like (weak) poset structure. Unlike Miller’s model, the carriers of programs and goals do not consist of the programs and goals themselves, but of interpreted programs and goals. Thus our models are not term-models by default as far as formulae are concerned.

The interpretation of logic (program-goal pairs) in our semantics arises from the composition of two maps:

p × g ⟶^{𝔘×𝔘} D_{p} × D_{g} ⟶^{I} Ω

where p and g stand for the sets of terms of program and goal type respectively, mapped by 𝔘 into carriers of their type in some Uniform Applicative Structure 𝔇, defined below, and I = {I_{i} : i ∈ ℕ} is an integer-indexed family of maps from stratified carriers D_{i,p} × D_{i,g} into the object of truth values Ω. Readers familiar with Miller’s forcing notation [15] will see that our interpretation I_{i}(𝔘(P), 𝔘(G)) = ⊤_{Ω} of the program-goal pair P, G corresponds to his

I, P | ⊧ G.

But we generalize his forcing in a number of ways: we include universal quantification (which requires adding the signature-levels i ∈ ℕ), higher-order logic (which requires the presence of an applicative structure to model lambda-abstraction and application), and we factor our interpretation through a structure which supplies carriers D_{p}, D_{g} for programs as well as goals.

We now give the details.

Definition 4.4 A uniform applicative structure ⟨D, App, Const, Inc⟩ for uctt is a typed applicative structure with sets D_{i,α} for each index i and type α, and functions Inc_{pr} : D_{i,r} → D_{i,p}, Inc_{ga} : D_{i,a} → D_{i,g}, Inc_{ar} : D_{i,r} → D_{i,a}, Inc_{gh} : D_{i,h} → D_{i,g} and Inc_{(i+1)i} : D_{i,α} → D_{i+1,α} (and by composition Inc_{jk} for j > k). The interpretation of functions satisfies App(f, t) ∈ D_{max{i,j},β} for all f in D_{i,βα} and t ∈ D_{j,α} and Inc_{ij}(App(g, s)) = App(Inc_{ij}(g), Inc_{ij}(s)).

There is a distinguished element ⊤ of D_{0,g}. Also ⟨D_{i,p}, ≤_{p}, ∧_{ppp}, Π_{p(pα)}⟩ must be a pre-order with a commutative binary operation ∧_{ppp} and a unary operator Π_{p(pα)}, such that for p, q ∈ D_{i,p} and f ∈ D_{i,pα}, p ≤_{p} p, p ≤_{p} p ∧ q, ≤_{p} is transitive and App(f, d) ≤_{p} App(Π_{p(pα)}, f).

Next, we define an interpretation function from the uniform applicative structure into a Heyting algebra Ω. We distinguish the Heyting algebra operations with subscripts Ω where necessary.

Definition 4.5 An intepretation on a uniform applicative structure is a function I : i×D_{i,p}× D_{i,g} → Ω, i ∈ ℕ, defined for all goals with the condtion

I_{i}(Inc_{pr}(r), Inc_{ga}(Inc_{ar}(r))) = ⊤_{Ω}  (11)

for atoms and the following more familiar equalities involving goals:

I_{i}(p, ⊤) = ⊤_{Ω}  (12)
I_{i}(p, g ∧_{ggg} g′) = I_{i}(p, g) ∧_{Ω} I_{i}(p, g′)  (13)
I_{i}(p, g ∨_{ggg} g′) = I_{i}(p, g) ∨_{Ω} I_{i}(p, g′)  (14)
I_{i}(p, q ⊃_{ggp} g) = I_{i}(p ∧_{ppp} q, g)  (15)
I_{i}(p, App(Σ_{g(gα)}, f)) = ⋁_{d∈D_{i,α}} I_{i}(p, App(f, d))  for f ∈ D_{i,gα}  (16)
I_{i}(p, App(Π_{g(gα)}, f)) = ⋁_{d∈S} I_{i+1}(p, App(f, d))  for f ∈ D_{i,gα}  (17)

where S = D_{i+1,α} \ Inc_{(i+1)i}(D_{i,α}). We also add the following conditions on ≤_{p}:

p ≤_{p} p′ implies I_{i}(p, g) ≤_{Ω} I_{i}(p′, g)  (18)
(g ⊃_{pgr} r) ≤_{p} p implies I_{i}(p, g) ≤_{Ω} I_{i}(p, Inc_{ga}(Inc_{ar}(r)))  (19)

And finally, we interpret the logic in our structure.

Definition 4.6 A uniform algebra or model for uctt is a uniform applicative structure together with an assignment-indexed map 𝔘 from terms to D sending elements of U_{i}(α) to elements of D_{i,α}, in an injective fashion; that is, 𝔘(c) ∉ Inc_{(i+1)i}(𝔘(U_{i}(α))) for the fresh constants c ∈ U_{i+1}(α). We restrict the interpretation of functions so that App(𝔘(λx.t)_{φ}, d) = 𝔘(t)_{φ[d/x]} and require that the following simple conditions also be met:

𝔘(⊤_{g}) = ⊤
𝔘(t_{1}t_{2})_{φ} = App(𝔘(t_{1})_{φ}, 𝔘(t_{2})_{φ})
𝔘(P_{1} ∧ P_{2})_{φ} = 𝔘(P_{1})_{φ} ∧_{ppp} 𝔘(P_{2})_{φ}
𝔘(G_{1} ∧ G_{2})_{φ} = 𝔘(G_{1})_{φ} ∧_{ggg} 𝔘(G_{2})_{φ}
𝔘(G_{1} ∨ G_{2})_{φ} = 𝔘(G_{1})_{φ} ∨_{ggg} 𝔘(G_{2})_{φ}
𝔘(G ⊃ A_{r})_{φ} = 𝔘(G)_{φ} ⊃_{prg} 𝔘(A_{r})_{φ}
𝔘(P ⊃ G)_{φ} = 𝔘(P)_{φ} ⊃_{ggp} 𝔘(G)_{φ}
𝔘(Σλx.G)_{φ} = App(Σ_{g(gα)}, 𝔘(λx.G)_{φ})
𝔘(Πλx.P)_{φ} = App(Π_{p(pα)}, 𝔘(λx.P)_{φ})
𝔘(Πλx.G)_{φ} = App(Π_{g(gα)}, 𝔘(λx.G)_{φ})

The notation 𝔘(P) where P is a set of program formulae rather than a single program formula, is meant to denote 𝔘(⋀ P).

We have preprocessed the set of programs into equivalence classes by identifying P with ⋀ P, but if a finer model theory were desired, we could add operators ∪_{ppp} and ⊆_{ppp} to the definition of uniform algebra.

Lemma 4.7 (Substitution) If θ is a substitution \{(x_{1}, t_{1}), …, (x_{n}, t_{n})\}, abbreviated [\overline{t}/\overline{x}], then for any term N, 𝔘(Nθ)_{φ} = 𝔘(N)_{φ[\overline{𝔘(t)_{φ}}/\overline{x}]}.

4.6 Soundness and Completeness

The reader will notice that the Soundness and Completeness Theorems below are restricted to closed goals proved by closed programs. This condition does not restrict the expressive power of the language because whatever is supposed to be expressed by an open program or goal can be expressed in closed form using universal and existential quantification, respectively. Even variable-sharing between a program P and a goal G can be expressed using existential quantification of a new goal P′ ⊃ G where P′ is the conjunction of the clauses of P and the new program is empty.

To prove soundness and completeness we again make a distinction between the universes U_{i} and their ground versions V_{i}.

Theorem 4.8 Suppose 𝔇 is a state vector, x_{1}, …, x_{m} are the logic variables of 𝔇, j is the largest index appearing in 𝔇, and there is an SLD resolution of NULL from 𝔇. Then there are positive terms s_{1}, …, s_{m} over V_{j} such that for all ⟨i; P | G′⟩ in 𝔇, in any uniform algebra,

I_{i}(𝔘(P [s_{1}/x_{1}, …, s_{m}/x_{m}]), 𝔘(G′[s_{1}/x_{1}, …, s_{m}/x_{m}])) = ⊤_{Ω}.

Proof. The proof is by induction on the length n of the SLD derivation. Where convenient, we abbreviate [s_{1}/x_{1}, …, s_{m}/x_{m}] to [\overline{s}/\overline{x}].

Base case: If n = 0 then the vector is of the form ⟨i; P_{1} | ⊤⟩ ⋯ ⟨i; P_{n} | ⊤⟩. Then I_{i}(𝔘(P_{j}[\overline{s}/\overline{x}]), ⊤) = ⊤_{Ω} by (12), as desired.

Inductive cases: Assume that the theorem holds for all SLD derivations of length less than n. We consider the possible outermost resolution steps:

Without loss of generality, we consider the or_{1} rule, 𝔄, ⟨i; P | G_{1} ∨ G_{2}⟩, 𝔅 ⇝^{∨} 𝔄, ⟨i; P | G_{1}⟩, 𝔅. By induction we assume that for all states ⟨i; Q | H⟩ in 𝔄, ⟨i; P | G_{1}⟩, 𝔅, we have

I_{i}(𝔘(Q[s_{1}/x_{1}, …, s_{k}/x_{k}], 𝔘(H[s_{1}/x_{1}, …, s_{k}/x_{k}])) = ⊤_{Ω}.

Let x_{k+1}, …, x_{m} denote those logic variables of G_{2} not among x_{1}, …, x_{k}. Select any positive terms s_{k+1}, …, s_{m}. By (14),

I_{i}(𝔘(P [s_{1}/x_{1}, …, s_{m}/x_{m}]), 𝔘((G_{1} ∨ G_{2})[s_{1}/x_{1}, …, s_{m}/x_{m}])) = ⊤_{Ω},

and thus all the states of the desired state vector are true.

If the last SLD-step involved ⟨i; P | G_{1} ∧ G_{2}⟩ ⇝^{∧} ⟨i; P | G_{1}⟩, ⟨i; P | G_{2}⟩, we assume that both I_{i}(𝔘(P), 𝔘(G_{1})) = ⊤_{Ω} and I_{i}(𝔘(P), 𝔘(G_{2})) = ⊤_{Ω} under the substitution [\overline{s}/\overline{x}]. Then I_{i}(𝔘(P [\overline{s}/\overline{x}]), 𝔘((G_{1} ∧ G_{2})[\overline{s}/\overline{x}])) = ⊤_{Ω} follows from (13).

If the last SLD-step involved ⟨i; P | D ⊃ G⟩ ⇝^{⊃} ⟨i; P ∪ D | G⟩, assume that

I_{i}(𝔘((P ∪ D)[\overline{s}/\overline{x}]), 𝔘(G[\overline{s}/\overline{x}])) = ⊤_{Ω}.

Then I_{i}(𝔘(P [\overline{s}/\overline{x}]), 𝔘((D ⊃ G)[\overline{s}/\overline{x}])) = ⊤_{Ω} by (15).

In the case of 𝔄, ⟨i; P | A′⟩, 𝔅 ⇝^{θ} 𝔄θ, 𝔅θ ⇝ ⋯ ⇝ NULL, we have A′θ = Aθ, A′

atomic, and A ∈ [i; P]_{U}. We assume

I_{i}(𝔘(Qθ[r_{1}/y_{1}, …, r_{l}/y_{l}]), 𝔘(Hθ[r_{1}/y_{1}, …, r_{l}/y_{l}])) = ⊤_{Ω}

for each state ⟨i; Qθ | Hθ⟩ in 𝔄θ, 𝔅θ and rewrite θ ∘ [r_{1}/y_{1}, …, r_{l}/y_{l}] in the required form as [s_{1}/x_{1}, …, s_{k}/x_{k}]. Thus we have

I_{i}(𝔘(Q[s_{1}/x_{1}, …, s_{k}/x_{k}]), 𝔘(H[s_{1}/x_{1}, …, s_{k}/x_{k}])) = ⊤_{Ω}

for each state ⟨i; Q | H⟩ in 𝔄, 𝔅. We extend the above substitution to θ′ = [s_{1}/x_{1}, …, s_{m}/x_{m}], m ≥ k, which replaces any remaining logic variables in P or A′ by fresh variables. Note that the states of 𝔄θ′ and 𝔅θ′ are still sent to ⊤_{Ω}. Since Aθ′ ∈ [i; P θ′]_{V}, 𝔘(Aθ′) ≤_{p} 𝔘(P θ′), and by (11) and (18)

⊤_{Ω} =_{Ω} I_{i}(Inc(𝔘(Aθ′)), Inc(𝔘(Aθ′))) ≤_{Ω} I_{i}(𝔘(P θ′), Inc(𝔘(Aθ′))).

In the case of 𝔄, ⟨i; P | A′⟩, 𝔅 ⇝^{θ} 𝔄θ, ⟨i; P θ | Gθ⟩, 𝔅θ for G ⊃ A ∈ [i; P]_{U} and Aθ = A′θ,

we assume that

I_{i}(𝔘(Qθ[r_{1}/y_{1}, …, r_{k}/y_{k}]), 𝔘(Hθ[r_{1}/y_{1}, …, r_{k}/y_{k}])) = ⊤_{Ω}

holds for each state ⟨i; Qθ | Hθ⟩ of the latter state vector. As in the previous case, we rewrite θ ∘ [r_{1}/y_{1}, …, r_{l}/y_{l}] in the required form and extend it if necessary to θ′ = [s_{1}/x_{1}, …, s_{m}/x_{m}], replacing any logic variables in G ⊃ A with free variables. Again, I_{i}(𝔘(Qθ′), 𝔘(Hθ′)) = ⊤_{Ω} for all states in 𝔄, ⟨i; P | G⟩, 𝔅, A′θ′ = Aθ′, and (G ⊃ A)θ′ ∈ [i; P θ′]_{V}. Hence 𝔘((G ⊃ A)θ′) ≤_{p} 𝔘(P θ′) and using (19),

⊤_{Ω} = I_{i}(𝔘(P θ′), 𝔘(Gθ′)) ≤_{Ω} I_{i}(𝔘(P [s_{1}/x_{1}, …, s_{m}/x_{m}]), 𝔘(A[s_{1}/x_{1}, …, s_{m}/x_{m}])),

as desired.

For the resolution step involving ⟨i; P | ∃y.G⟩ ⇝^{∃} ⟨i; P | G[v/y]⟩, where v is a logic variable of label i, we assume

I_{i}(𝔘(P [s_{0}/v, s_{1}/x_{1}, …, s_{m}/x_{m}]), 𝔘(G[v/y][s_{0}/v, s_{1}/x_{1}, …, s_{m}/x_{m}])) = ⊤_{Ω}.

Then ⊤_{Ω} ≤ I_{i}(𝔘(P [s_{1}/x_{1}, …, s_{m}/x_{m}]), 𝔘((∃y.G)[s_{1}/x_{1}, …, s_{m}/x_{m}])) by (16).

For the resolution step involving ⟨i; P | ∀y_{α}.G⟩ ⇝^{∀} ⟨i + 1; P | G[c/y]⟩, where c is a constant of index i + 1, we assume I_{i+1}(𝔘(P), 𝔘(G[c/y])) = ⊤_{Ω} under [\overline{s}/\overline{x}]. Then (17) yields the desired result

⊤_{Ω} = ⋁_{d∈D_{i+1,α}} I_{i+1}(𝔘(p), 𝔘(App(f, d))) = I_{i}(𝔘(P [\overline{s}/\overline{x}]), 𝔘((∀y.G)[\overline{s}/\overline{x}])).

□

Corollary 4.9 (Soundness) If there is an SLD proof of a closed goal G from a closed program P, then for all uniform algebras 𝔘, I(𝔘(P), 𝔘(G)) = ⊤_{Ω}.

We now establish completeness of resolution. Let Ω be {⊤, ⊥}.^{2} Consider the uniform term algebra 𝔗 = ⟨D, App, Const, Inc⟩ with D_{α} the set of principal normal forms of closed uctt-terms of type α; let App and Const build the obvious terms and Inc be identity functions. Let P ≤_{p} P′ if [i; P] ⊆ [i; P′].

For this particular situation, we define a weak interpretation on atoms to be an indexed family of functions I = {I_{i} : i ∈ ℕ}, where for each natural number i, I_{i} : D_{i,p} × D_{i,a} → Ω satisfying p ≤_{p} q, i ≤ j implies I_{i}(p, a) ≤_{Ω} I_{j}(q, a). Let its extension to all goals, I_{i} : D_{i,p}×D_{i,g} → Ω, i ∈ ℕ satisfy only (12), (13), (14), (15), (16) and (17), but not necessarily the properties (18) and (19) enjoyed by interpretations.

Lemma 4.10 Weak interpretations form a complete lattice with the partial order

I ⊑ I′ := (∀i ∈ ℕ)I_{i} ⊑_{i} I′_{i}

where the order ⊑_{i} on the interpretation fibers I_{i} is defined pointwise.

2The reader should note that this does not make our semantics classical. See Section 4.7 for details.

Since the the order (on the I_{i} and the I) is built up pointwise, it is easily seen to inherit the structure of a complete lattice from Ω.

We define a “T_{P} ” operator on these weak interpretations in the usual way: T (I)_{i}(P, A) = ⊤_{Ω} if A ∈ [i; P]_{V} or there is a clause G ⊃ A in [i; P]_{V} such that I_{i}(P, G).

A more general definition, for arbitrary complete lattices Ω, which reduces to the preceding one for the two-valued Ω = {⊤, ⊥} is:

T (I)_{i}(P, A) = ⋁_{G⊃A∈[i;P]_{V}} I_{i}(P, G).  (20)

provided we adopt the convention that ⊤ ⊃ A ∈ [i; P] whenever the atom A is in [i; P].

Since T is defined in terms of a supremum, and the sup operation ⨆ on weak interpretations is defined pointwise, proof of the continuity of T on weak interpretations boils down to a straightforward commutation of Ω-suprema. By the Tarski-Knaster theorem, we obtain the fact that T has a least fixed point, and that it is the supremum of the chain I_{⊥}, T (I_{⊥}), T^{2}(I_{⊥}), . . ..

Lemma 4.11 The fixed point I = T^{∞}(I_{⊥}) is a genuine interpretation, not just a weak one. That is to say, in addition to satisfying (12), (13), (14), (15), (16) and (17) of definition (4.5) it also satisfies properties (18) and (19):

p ≤_{p} p′ implies I_{i}(p, g) ≤_{Ω} I_{i}(p′, g)
(g ⊃_{pgr} r) ≤_{p} p implies I_{i}(p, g) ≤_{Ω} I_{i}(p, Inc_{ga}(Inc_{ar}(r))).

The proof is straightforward. We will sketch the argument for the second property. Suppose P is a program, G a goal, and R a rigid atom, both closed, and that G ⊃ R ≤_{p} P, that is to say, for all i [i; G ⊃ R] ⊆ [i; P]. In particular, G ⊃ R ∈ [i; P]. By definition (20) of T, for any natural number n (and any index i)

(T^{n+1}(I_{⊥}))_{i}(P, R) = ⋁_{B⊃R∈[i;P]_{V}}(T^{n}(I_{⊥}))_{i}(P, B).

Since G ⊃ R lies in [i; P]_{V}, T^{n}(I_{⊥}))_{i}(P, G) is one of the terms in the supremum

⋁_{B⊃R∈[i;P]_{V}} T^{n}(I_{⊥}))_{i}(P, B).

Therefore, T^{n}(I_{⊥})_{i}(P, G) ≤ T^{n+1}(I_{⊥})_{i}(P, R). Taking suprema, we obtain (T^{∞}(I_{⊥}))_{i}(P, G) ≤ (T^{∞}(I_{⊥}))_{i}(P, R) as we wanted to show.

We use the fixed point of T to establish completeness.

Theorem 4.12 If I_{i}(𝔘(P), 𝔘(G)) = ⊤_{Ω} in all uniform algebras 𝔘, then there is an SLD derivation ⟨i; P | G⟩ ⇝ ⋯ ⇝ NULL whose substitutions are the identity on the free variables of P and G.

Proof. We consider the uniform algebra discussed above, and drop all reference to 𝔘, which is the identity here. In the usual fashion we can show T^{k}(I_{⊥})(i, P, G) = ⊤_{Ω} for some k. The proof is by induction on k.

Base case: For k = 1, the proof is by induction on the structure of G: If the goal is atomic, A, then T (I_{⊥})(i, P, A) = ⊤_{Ω} and A ∈ [i; P]_{V} ⊂ [i; P]_{U}. The desired SLD derivation ⟨i; P | A⟩ ⇝ NULL uses the identity rule. If the goal is ⊤, the associated NULL vector ⟨i; P | ⊤⟩ constitutes an SLD proof.

If the goal is of the form G_{1} ∨ G_{2}, then we have, say, T (I_{⊥})(i, P, G_{1}) = ⊤_{Ω}. By the induction hypothesis, we have a derivation ⟨i; P | G_{1}⟩ ⇝ ⋯ ⇝ NULL satisfying the condition on substitutions, which by the or rule extends to ⟨i; P | G_{1} ∨ G_{2}⟩ ⇝ ⟨i; P | G_{1}⟩ ⇝ ⋯ ⇝ NULL.

If the goal is G_{1} ∧ G_{2}, we assume ⟨i; P | G_{1}⟩ ⇝ ⋯ ⇝ NULL, where the free variables of P and G_{2} do not figure in the substitutions of the derivation, and ⟨i; P | G_{2}⟩ ⇝ ⋯ ⇝ NULL, under the analogous condition. We may interleave these derivations to obtain ⟨i; P | G_{1}⟩, ⟨i; P | G_{2}⟩ ⇝ ⋯ ⇝ NULL. By the and rule,

⟨i; P | G_{1} ∧ G_{2}⟩ ⇝ ⟨i; P | G_{1}⟩, ⟨i; P | G_{2}⟩ ⇝ ⋯ ⇝ NULL,

as desired.

In the case T (I_{⊥})(i, P, D ⊃ G′) = ⊤_{Ω}, we know T (I_{⊥})(i, P ∪ D, G′) = ⊤_{Ω} and so by the induction hypothesis, we have a derivation ⟨i; P ∪ D | G′⟩ ⇝ ⋯ ⇝ NULL satisfying the condition on substitutions. By the augment rule, we then have the desired SLD resolution ⟨i; P | D ⊃ G′⟩ ⇝ ⟨i; P ∪ D | G′⟩ ⇝ ⋯ ⇝ NULL.

For a goal of the form ∃x.G′, T (I_{⊥})(i + 1, P, G′[t/x]) = ⊤_{Ω} and by the induction hypothesis the derivation ⟨i; P | G′[t/x]⟩ ⇝ ⋯ ⇝ NULL for some term t over V_{i} satisfies the condition on substitutions. I.e., ⟨i; P [t/v] | G′[v/x][t/v]⟩ ⇝ ⋯ ⇝ NULL for a fresh variable v of index i. Since the substitution [t/v] is legal, by a lemma, ⟨i; P | G′[v/x]⟩ ⇝ ⋯ ⇝ NULL holds. This new derivation can be extended to ⟨i; P | ∃x.G′⟩ ⇝^{∃} ⟨i; P | G′[v/x]⟩ ⇝ ⋯ ⇝ NULL and this extended resolution satisfies the condition on substitutions.

For a goal of the form ∀x.G′, we know that T (I_{⊥})(i + 1, P, G′[c/x]) = ⊤_{Ω} for c ∈ V_{i+1} \ V_{i}. By the induction hypothesis, ⟨i + 1; P | G′[c/x]⟩ ⇝ ⋯ ⇝ NULL satisfies the condition on substitutions. Since c ∈ U_{i+1} \ U_{i}, this derivation can be extended with the generic rule to

⟨i; P | ∀x.G′⟩ ⇝^{∀} ⟨i + 1; P | G[c/x]⟩ ⇝ ⋯ ⇝ NULL.

Induction cases: Again, the proof for k > 1 is by induction on the structure of G. For an atomic goal A, according to either A ∈ [i; P]_{V} or T^{k−1}(I_{⊥})(i, P, G′) = ⊤_{Ω} and G′ ⊃ A ∈ [i; P]_{V}. The former case was handled above. In the latter, we have an SLD derivation ⟨i; P | G′⟩ ⇝ ⋯ ⇝ NULL by the induction hypothesis on k. Since G′ ⊃ A ∈ [i; P]_{U}, we apply the backchain rule with an empty substitution, extending the given derivation to ⟨i; P | A⟩ ⇝ ⟨i; P | G′⟩ ⇝ ⋯ ⇝ NULL.

The non-atomic cases are analogous to those for n = 1. □

Corollary 4.13 (Completeness) Let Ω be {⊤, ⊥}. If I_{i}(𝔘(P), 𝔘(G)) = ⊤_{Ω} in all uniform algebras 𝔘, then there is an SLD proof of G from P.

It should be noted that by a straightforward adaptation of the proof of the corresponding theorem in Miller et. al. [17], an SLD proof of G from P exists iff a proof of P ⟶ ⟶ G exists in ICTT. Thus, I_{i}(𝔘(P), 𝔘(G)) = ⊤_{Ω} in all uniform algebras 𝔘 if and only if [[P ⟶ ⟶ G]] = ⊤ in all ICTT uniform algebras 𝔈.

4.7 Remarks on Uniform Algebras

The use of Ω = {⊤, ⊥} corresponds to the two-valued forcing relationship in our first-order models and so the model used in the completeness theorem is just the higher-order analogue of the Miller model. In fact, if we let the pairs (i, p) for p ∈ D_{i,p} be the nodes of a Miller-style model with the order inherited from the preorders for D_{i,p} and the inclusion Inc_{ji}, we obtain an elementarily equivalent semantics by setting i, P ⊪ G when I_{i}(𝔘(P), 𝔘(G)) = ⊤_{Ω}. The case Ω = {⊤, ⊥} corresponds to a Kripke model with a classical metatheory, that is, a decidable forcing relation. It suffices to establish completeness.

In future work, we hope to explore the significance of varying Ω. Surely this wider class of models includes Miller-style models with a constructive metatheory, and it may capture other notions of operational semantics for logic programming. For example, it is not hard to show that c-semantics ([4, 7]) corresponds to an Ω given by the set of open substitutions.

References

[1] Peter Andrews. Resolution in type theory. Journal of Symbolic Logic, 36:414–432, 1971.

[2] Peter Andrews. General models and extensionality. Journal of Symbolic Logic, 37(2):395–397, 1972.

[3] Mino Bai and Harold Blair. General model theoretic semantics for higher-order horn logic programming. In Logic Programming and Automated Reasoning, International Conference LPAR’92, volume 624 of LNCS. Springer, 1992.

[4] A. Bossi, M. Gabrielli, G. Levi, and M. C. Meo. A compositional semantics for logic programs. Theoretical Computer Science, 122(1-2):3–47, 1994.

[5] Jawahar Chirimar. Proof Theoretic Approach to Specification Languages. PhD thesis, University of Pennsylvania, 1995.

[6] A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

[7] Marco Comini. An abstract interpretation framework for Semantics and Diagnosis of logic programs. PhD thesis, Dipartimento di Informatica, Universitá di Pisa, 1998.

[8] M. DeMarco. Higher Order Logic Programming in the Theory of Types. PhD thesis, Wesleyan University, 1999.

[9] M. DeMarco and J. Lipton. The semantics of and intuitionistic version of church’s type theory and higher order hereditary harrop logic programming. To appear.

[10] Michael Fourman and Dana S. Scott. Sheaves and logic. In Applications of Sheaves, volume 753 of Lecture Notes in Mathematics, pages 302–401. Springer, 1979.

[11] Harvey Friedman. Equality between functionals. In R. Parikh, editor, Logic Colloquium, volume 453 of Lecture Notes in Mathematics, pages 22–37. Springer, 1975.

[12] J.Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1998.

[13] Leon Henkin. Completeness in the theory of types. Journal of Symbolic Logic, 15:81–91, 1950.

[14] Dale Miller. λ-prolog: an introduction to the language and its logic. manuscript available at

http://www.cse.psu.edu/ dale.

[15] Dale Miller. A logical analysis of modules in logic programming. Journal of Logic Programming, pages 79–108, 1989.

[16] Dale Miller. A multiple-conclusion meta-logic. In Proceedings of the 1994 Symposium on Logics in Computer Science, pages 272–281, 1994.

[17] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 1990.

[18] John Mitchell. Foundations for Programming Languages. MIT Press, Cambridge, Massachusetts, 1996.

[19] John Mitchell and Eugenio Moggi. Kripke-style models for typed lambda calculus. Annals of Pure and Applied Logic, 51:99–124, 1991.

[20] G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, Department of Computer and Information Science, University of Pennsylvania, 1987.

[21] A. S. Troelstra and D. van Dalen. Constructivism in Mathematics: An Introduction, volume 2. Elsevier Science Publishers, 1988.

[22] D. A. Wolfram. A semantics for λ-prolog. Theoretical Computer Science, 136:277–289, 1994.