Concurrency in Proof Normalization and Logic Programming

1. Introduction

Proof normalization has a long history in mathematical logic [Prawitz 1965]. The significant result for computer science is as follows: I/ there is a proof of the formula 3z(A(z)), one can get an answer t, which satisfies A(t), after normalizing the proof.

This realizes a computation, which is appropriately called logic programming. However, it is less efficient than Prolog.

[Goad 1980] proposes an extended >.-calculus, named p­ calculus, to represent proofs. P-calculus terms are executed efficiently. [Hagiya 1982] noticed that most part of a proof is irrelevant for the computation. He introduces new notions to eliminate the unnecessary normalization steps.

This paper describes a new approach to improve the use­ fulness of the proof normalization. Our method is to attach proofs to Skolem functions, which enables us to normalize eagerly. Eager normalization produces a partial answer in advance. Using this capability, proof normalization can be performed concurrently rather than one proof at a time. Concurrency here means the same as in Concurrent Pro­ log [Shapiro 1983]. We apply our method to an example from Concurrent Prolog [Takeuchi 1984] and compare this to computation in Concurrent Prolog.

2. Logical Framework

Proof normalization is elegantly explained using a natural deduction system. Figure 1 summarizes the inference rules for natural deduction, which are used in this paper.

A typical proof in natural deduction is illustrated in Figure 2. This proof includes a rule of induction (IND). The proof concludes 3z(t + y = z). The assumptions are: (1) 0 + y = y and (2) Vxw(x + w = z :J s(x) + w = s(z)). Two other formulas enclosed in brackets, [a + y = c] and [3z(a+y = z)], arenot considered tobe assumptions. The formal definition is given below.

Definition 1 At applications· of :JI, 3E, and IND rules, certain assumptions (indicated by brackets in figure 1} are said to be "discharged" by the rule. The conclusion of a proof is said to depend on the assumptions that have not been discharged.

Sometimes, it is important to distinguish between variables. In Figure 2, there are five variables: z, y, z, w, a and c. Variables z, z and w are called bound variables. Variable y is a free variable. Two variables a and c are both called proper parameters, which are defined below.

Definition 2 In applications of the rule VI, 3E and IND, the variable "a" (see Figure 1} is called the proper pa­ rameter o/ the inference rule.

The proper parameterB Iook like free variables, however, they are bound not by the quantifiers (V and 3), but by the inference rules. The precise definition of the bound variable is given by the formulae...as_types approach [ Goad 1980].

3. Computation by normalization

In short, proof normalization reduces the redundant part in natural deduction proofs ([Prawitz 1965] and [Troelstra 1973]). Here, we explain only two reduction rules which are relevant to this paper.

Reduction rules

1. E-reduction rule: H a proof has an 31-rule imme­ diately followed by an 3E-rule, the proof is simpli­ fied by cancelling both applications of rules. Here, IT and IT'(a) stand for subproofs. a in IT'(a) indicates a proper parameter.
2. IND-reduction rule: IND-reduction rule simplifies the term t if the term is of the form 0 or s(t).

Definition 3 A proof n is said to be normal, i/ no reduc­ tion rule is applicable to IT.

Before stating the key property of a normal proof, the con­ cept of the Harrop formula should be introduced.

Definition 4 The class of Harrop formulas is defined in­ ductively as follows:

1. Every atomic formula is a Harrop formula.
2. !!. I/ A and B are Harrop formulas, then A A B and 'v'xA(x) are Harrop formulas.
3. lf B is a Harrop formula, then A :::) B is a Harrop formula, regardless of the form of A.

The Harrop formula has no positive V nor 3, except in the left hand side of the implications (:::)).

Proposition 1 A normal proof of3zA(z), where assump­ tions are only Harrop formulas, contains a subproof of A(t) for a suitable term t.

We can normalize the proof in Figure 2 to calculate the sum of two numbers because the two assumptions are both Harrop formulas, and the proof satisfies the condition of Proposition 1.

4. Attaching proofs

Although proof normalization provides a theoretically justi­ fied computation, it does not always produce a satisfactory answer. Consider the example in Figure 3, in which A(x,z) stands for (x+y=z). The uppermost applications of'v'E and :::)E are abridged to 1r(a). We want to add two terms s(a) and y, where a is some term. Normalization cannot give the answer because the term a does not take the form of s(t) nor 0. The IND-reduction rule cannot be applied further .

STEP 3: cannot apply IND-reduction, becauae tt ia

not 0 nor a(t) . GET STUCK!

Figure 3: Addition of two terms, s(a) and y

We solve the problem by attaching proofs to Skolem functions. The new method is as follows:

Attaching proofs:

1. Eliminate the existential quantifiers in the conclusion of an IND rule, using Skolem functions.

• In the example, 3z(A(a, z)) is converted into A(a, f(a)), where f is a Skolem function.
• Attach the proof of the conclusion to the Skolem func­ tion. It means that one can use proof normalization in the future to get the value of the Skolem function. In the example, the proof of 3z(A(a,z)) is attached to f.

Now we can continue the normalization and get the answer z = s(f(a)) in figure 4. The answer is called partial because it contains a Skolem function.

The method of attaching proofs is similar to the se­ mantic attachment in FOL [Weyhrauch 1980]. In FOL, a Lisp function can be attached to a predicate. Whereas, in our method, a proof is attached instead of a Lisp function. Our attachment is performed inside the logic programming world.

Theoretical consideration

1. Syntactically, the elimination of the existential quan­ tifiers converts a non-Harrop formula into a Harrop formula, which becomes an assumption of the proof. This assures the condition of Proposition 1, and nor­ malization can proceed further.
2. The method is applicable to the formula of the form 'v'x3z(A(x,z)). This type of formula appears every­ where in computer science.
3. The reason for the special treatment of the conclusion of IND is that it has the similar properties to the assumptions in a proof. For further details, see the definition of "spine" in [Troelstra 1973].

STEP 3 : using Skolem function

Figure 4: Addition of two terms (continued)

5. Concurrent normalization

Using the notion of partial answer, proof normalization can be performed concurrently. In this section, the example given in Concurrent Prolog [Takeuchi 1984] is computed, using proof normalization.

Example 1 Concurrent Prolog

1. integers(N,[NIS]) :- N1:=N+1 I integers(Nl,S).
2. outstream([NIS]) :- write(N),outstream(S?).
3. :- integers(O,S),outstream(S?).

First, we treat clauses (1) and (2) separately. Each clause provides an assumption, which is used in the proof.

Example 2 Proof of integer stream

The rightmost assumption is equivalent to clause {1}.

The leftmost assumption, 3y3z(integers(y, x)), asserts that "integers" is not an empty relation and it is taken as an axiom. The proof uses the going-down induction (INDt) which is a variation of the usual induction rule [Manna and Waldinger 1971]. The reduction rule for INDt is defined

analogously to the usual induction IND. If the attachment technique is used, one can normalize the proof in Example 2 to getan answer z = [Oig(1)], where g(x) is a Skolem func­ tion for 3z(integers(x,z)), and "1" means s(O). Further normalization of the attached proof gives g(1) = [1lg(2)], g(2) = [2lg(3)] and so on. This type of infinite list is called a stream.

The second proof corresponds to clause (2). It uses linear list induction (IND[ ]). Linear list induction is an­ other variation of the IND rule, obtained through identify­ ing 0 +-+ [ ] i.e. NIL-list, and s(y) +-+ [xly] i.e. CONS(x,y). The reduction rule for IND[ ] is Straightforward and treats the induction term [xly] as s(t).

Example 3 Proof of outstream

The rightmost assumption is equivalent to clause {2} .

The upper left assumption, 'v'x(write(x)), always holds because "write" can print any term. (For simplicity, we ig­ nore errors in printing.) The other assumption, outstream([]), is a termination condition for "outstream" and taken as an axiom. It should be noted here that predicate "write(N)" is a built-in predicate in Concurrent Prolog, and it has a side effect to write the term N. How should it be handled in normalization? Again, the attaching technique solves the problem. This time a program is attached to a Skolem function. We do not specify any programming language here. To attach a program, there should be an existential quantifier. Thus, write(x) is modified to have an explicit output variable: wri te«< (x, z). The new predicate is con­ sidered "built-in"; that means that 'v'x3z(write@(x,z)) is an axiom. Formally, write(a) in Example 3 is replaced by the subproof below:

In the subproof, a Skolem function p(a) is used. A cer­ tain program is attached to function p(a) to print the term "a" when "a" is substituted by some term. This requires more explanation:

When a term is printed?

A term can be printed anytime unless it is bound. That is, no bound variables in the scope of Vor 3, or no proper parameters can be printed.

In the example, "a" is printed after it is substituted. If the proof is normalized after giving t = [/ ooibar], "f oo" will be printed, because it is substituted for "a" in the proof.

At last, two proofs are combined to produce the same effect as clause (3) in Concurrent Prolog. Figure 5 illus­ trates only a few steps of the normalization. However, it is easy to see that computation is performed concurrently. The INDL subproof produces the Iist, and IND[ ] subproof consumes the Iist. The condition on the print function pro­ tects the proper parameter from being printed before it is substituted. This realizes a kind of synchronization, which is attained by the read-only annotation in Concurrent Pro­ log [Shapiro 1983] [Takeuchi 1984].

6. Conclusion

In this paper we propose a new method of proof normaliza­ tion, which utilizes Skolem functions to normalize a proof eagerly. Each Skolem function represents an existential variable (:Jz), and the relation is preserved by attaching proofs to Skolem functions.

Our method facilitates concurrent normalization. Con­ current Prolog is formally well-explained by our method.

It is easy to see that Prolog itself is closely related to proof normalization because: (1) Prolog always generates normal proofs, and (2) AHorn clause is necessarily a Harrop formula. Thus, Prolog computation can be considered as a special kind of proof normalization.

ACKNOWLEDGEMENT

I would like to thank Dr. Carolyn Talcott at Stanford Uni­ versity for many valuable comments.