1991 MTC Qual Question

John Mitchell Due Noon, Thursday April 11

This question is about resolution theorem proving and Prolog as a theorem prover. Since Prolog per se is not on the reading list, the relevant facts about Prolog are summarized here. So don’t panic.

The example theorem proving problem is type inference for combinatory logic. Combinatory logic is an algebraic theory over two constant symbols, S and K, and one binary operation called application, commonly written ·. It is standard to omit · and associate applications to the left. For example, we write SKK instead of (S · K) · K. We will not be concerned with the equational theory of combinatory logic, only the following proof system for giving types to combinatory terms that do not contain variables. If you are curious about combinatory logic but not familiar with it, you may want to take a quick look at the relevant sections of Hindley and Seldin.

The types we will use are given by the grammar

τ : : = t | τ → τ

where t may be any type variable. It is conventional to associate → to the right when parentheses are omitted. We are interested in proving statements of the form M : τ, where M is a variable-free term over S, K and ·, and τ is a type expression. The two axiom schemes are

K : t → s → t
S : (r → s → t) →(r → s) → r → t

and the single inference rule is

\frac{M : s → t, N : s}{MN : t}

Using this system, we can prove that SKK:t → t. This makes sense since SKK defines the identity function under application, i.e., SKKx = x. You will be asked to show that each variable-free combinatory term M has a most general type, and that this may be calculated by LD resolution in general, and Prolog in particular.

We now review the relevant facts about linear resolution for definite clauses (LD resolution) and Prolog. We assume some first order signature Σ with some number of constant symbols, function symbols and predicate symbols. A literal is an atomic formula P t_{1} … t_{n}, where P is an n-ary predicate symbols and t_{1},…, t_{n} are terms. It is common to also include the negation of an atomic formula as a literal, but we will not need negation. If ϕ is a first-order formula, it will be convenient to write ∀ϕ for the universal closure of ϕ and ∃ϕ for the existential closure of ϕ. For any literals A_{1},…, A_{j} and B_{1},…, B_{k}, we will write

A_{1},…, A_{j} ← B_{1},…, B_{k}

for the universally closed Horn sentence

∀[(B_{1} ∧… ∧ B_{k}) ⊃ (A_{1} ∨… ∨ A_{j})].

The notation A_{1},…, A_{j} ← B_{1},…, B_{k} is called clausal form. In Prolog programs, we use the ascii combination :- is instead of the symbol ←. A program clause, also called a definite clause is a clause of the form

A ← B_{1},…, B_{k}

with a single literal A, called the head, on the left and a list of zero or more literals, called the body, on the right. A program is a finite, nonempty set of program clauses. Note that while a Horn sentence may have an empty head or body, only the body of a program clause may be empty. The convention is that an empty disjunction is false (since for a disjunction to be true, there must exist a true disjunct) and an empty conjunction is true (since all of its conjuncts are true). This means that the empty clause, with empty head and body, is equivalent to true ⊃ false, and therefore contradictory.

We assume familiarity with basic facts about unification, the occurs check and most general unifiers. In particular, substitution θ′ is more general than θ if there is some θ′′ with θ = θ′′ ∘ θ′. If S is a set of formulas, it will be convenient to write θS for the set of formulas {θF | F ∈ S}.

Resolution is often described as a refutation proof method which, given a program P and goal G, tries to determine whether the program and goal are inconsistent. Since P and G are inconsistent iff P semantically implies the negation of G, we can also regard resolution as a direct proof procedure for semantic implication. We will be interested in goals which consist of a single clause ← A_{1},…, A_{k} with empty head. This is the clausal form of the first order sentence ∀[(A_{1} ∧ … ∧ A_{k}) ⊃ false] saying that the conjunction of the formulas in the body implies the empty disjunction. It is easy to see that P and a goal ← A_{1},…, A_{k} with empty head are inconsistent iff P implies ∃[A_{1} ∧… ∧ A_{k}], by simple first-order manipulation of negation. Therefore, if we write a goal with empty head as the set G = {A_{1},…, A_{k}} of literals in its body, resolution will succeed on P and G iff P implies ∃[A_{1} ∧ … ∧ A_{k}]. The property of resolution theorem proving which makes logic programming useful is that when resolution succeeds, we obtain a most general substitution θ such that P implies θA_{1} ∧…∧θA_{k}. We will state this precisely after briefly reviewing the resolution procedure.

Given program P and goal G = {A_{1},…, A_{k}}, we resolve to get goal G′ by the following steps:

1. Select some A ← B_{1},…, B_{k} from P and literal A_{i} from G with A and A_{i} unifiable.

2. Rename all variables in A ← B_{1},…, B_{k} to be distinct from those in P and G.

3. Let θ be the most general unifier of A and A_{i}.

4. Let G′ = θ(G − {A} ∪ {B_{1},…, B_{k}}) be the result of replacing A in G by B_{1},…, B_{k} and applying substitution θ to all the remaining formulas.

If P and G resolve to produce G′, then we write G →^{θ}_{P} G′, omitting P when clear from context. We say a resolution sequence

G →^{θ_{1}} G_{1} →^{θ_{2}} G_{2} →^{θ_{3}} … →^{θ_{n}} G_{n}

is successful if G_{n} is the empty set and unsuccessful (or fails) if G_{n} ≠ ∅ and we cannot further resolve G_{n} with P. If G →^{θ_{1}} … →^{θ_{n}} ∅ is a successful resolution sequence, then we call the composition θ_{n} ∘…∘θ_{1} of substitutions, restricted to the set of variables occurring in G, the answer substitution for this sequence. Given a program P, the LD-tree of goal G is the tree with root G, and G′′ a child of G′ whenever G′ →^{θ} G′′. We say LD resolution succeeds on P and G if there is a successful branch in the LD-tree, and fails otherwise.

Theorem: Let P be a program and let G = {A_{1},…, A_{k}} be a goal. There is a successful resolution sequence from G iff P semantically implies ∃[A_{1} ∧ … ∧ A_{k}]. If a successful resolution sequence has answer substitution θ, then θ is the most general substitution for variables free in G such that P semantically implies ∀[θA_{1} ∧… ∧ θA_{k}].

This theorem says that the LD tree of {A_{I},…, A_{k}} will have a successful branch whenever P semantically implies the existential formula ∃[A_{1} ∧ … ∧ A_{k}]. Prolog (with the occurs check enabled) implements a deterministic approximation to full search of the LD tree using depth-first search. To really say what this means, we would have to be specific about how children of each node are ordered. However, the exact order of resolutions in Prolog execution will not matter for this problem. The reason is that in the special case that the LD tree of G is finite, Prolog execution will succeed whenever there is a successful branch in the LD tree.

Now for the statement of the problem. Use a first-order signature with constants S, K, binary functions apply for application and arrow for → (both written in prefix notation) and binary predicate type. The intended meaning of type(M, t) is that combinatory term M has type t.

(a) Write a program P expressing the axioms and inference rules for typing combinatory terms.

(b) If M is a variable-free combinatory term, let us write M̄ for the corresponding first-order term, and similarly τ̄ for the first-order term for type expression τ (not necessarily variablefree). Show that M : τ is provable in the type inference system iff LD resolution succeeds on the goal type(M̄, t) with t a variable, giving answer substitution θ such that τ̄ is a substitution instance of θt. (Hint: This has a relatively easy proof using the theorem given and basic facts about first-order logic, such as soundness and completeness. If you get stuck on this part of the problem, please go on to the other parts anyway.)

(c) Show that if G consists of a single formula type(M̄, t), where M̄ is the first-order expression for variable-free combinatory term M and t is a variable, then the LD tree for G is finite.

(d) A type τ is a most general type for combinatory term M if M:τ is provable and, whenever M:τ′ is provable, τ′ is a substitution instance of τ. Show that for any variable-free combinatory term M, your program P, considered as a Prolog program, will either compute the most general type for M or halt with failure if M is not typable.

(e) Now that you have proved your Prolog program correct, try it and see of it works on a few examples, including SKK. See next page for running Prolog on theory.

(f) If we read → in type expressions as implication, then there is a variable-free combinatory term of type τ iff τ is an intuitionistically valid implicational formula. How well do you think your program works as a theorem prover for propositional intuitionistic implications? Propositional intuitionistic logic is pspace complete. Does this theorem prover come close to deciding provability in the optimal time?

Running SB-Prolog on Theory

SB-Prolog is a public domain Prolog compiler and interpreter which has been installed on Theory in /u1/jcm/sbprolog. (Thanks to Pat Lincoln for installing this and modifying the interpreter to unify with occurs check properly.) Here is a simple example which shows you how to use this.

First, prepare a file with your program. My example is this

p(a,a).
q(X) :- p(X,X).

which I put in a file called prlg.

Next, start SB-prolog by typing /u1/jcm/sbprolog/sbprolog. Use consult to load your program and then type your goal formula. Here is my example run.

/u1/jcm/sbprolog/sbprolog
SB-Prolog Version 3.1.1
Modified March 1991 To have a sound unification procedure.
| ?- consult(prlg).
yes
| ?- q(Y).
Y = a
yes
| ?- ctrl D
Halt.  Program terminated normally

In words, I ask whether the program implies a substitution instance of q(Y). The answer substitution returned is Y = a. Please note that variables start with either a capital letter or an underscore. You will probably notice that SB-Prolog is pretty flaky. For example, your program file must end in a newline. Otherwise, the interpreter quits without asking you for a goal.