Damjan Bojadziev

A constructive view of Prolog

Journal of Logic Programming Vol. 3, No. 1, 1986, pp.69-74.

A constructive rationalization of Prolog is presented, covering the logical form of definite clauses and the role of negative (goal) clauses. This view is developed from the idea, taken from set theory, that a constructive theory can be obtained if classical reasoning is confined to a constructively limited basis. The syntax of definite clauses is seen as reflecting a constructive view of description in that it prevents the expression of incomplete and negative information; the purely negative clauses initiate a classical proof technique, operating on a definite axiomatic basis.

If you have seen a reference to this paper, please leave a message.

1. Introduction

Logic programming by means of Horn clauses, as realized in Prolog, can be interpreted from a constructive point of view. A connection with constructive logic* is apparent at the level of syntax (in the linguistic sense of the word): a constructive orientation is built into the logic of definite clauses at the level of formation rules, whereas the logical apparatus which the Prolog interpreter uses on the program clauses and the goals is quite classical. An analogous situation is sketched in Quine's remarks on Weyl's set theory in [11]: it is a constructive theory in which classical reasoning is retained, but applied to a constructively limited basis. This idea is transposed to the context of logic programming and used for a constructive rationalization of the limited expressive power of definite clause programs (absence of existential quantification, disjunction and negation) and the classical mechanism of their execution.

*The expression "constructive logic" is not used here in any precise sense; as Quine wrote in [11],
constructivism in mathematics is intolerance of methods that lead to affirming the existence of things of some sort without showing how to find one. This is not a sharp definition of constructivism; there is none, or no unique one. My vague word 'find' could mean 'compute', in the case of a number and 'construct' in some sense, in the case of a geometric figure or set.
After the extensive formal reinterpretation of logic programming based on the intuitionistic theory of inductive definitions, given by Hagiya and Sakurai in [5], the contribution of this article is to indicate what could be said about the subject in an informal and rather elementary fashion by applying a different, more "conservative" idea.

2. Prolog and clausal logic

The prevailing paradigm of mechanical theorem proving, in which the programming language Prolog has been developed, is reductio ad absurdum over the Skolem clausal form: the negation of the alleged theorem, transformed into clausal form, is adjoined to the clauses coming from the axioms, and from the resulting mass of clauses the resolution rule attempts to produce the empty clause of contradiction. At this general level, the only point of contact with constructive logic is the possible constructivity of proofs: a reductio ad absurdum proof of a (positive) existential statement is not in general bound to produce concrete (ground) instances of the quantified variable, which makes it constructively unacceptable. Moreover, when performing a reduction over the clausal form, it may happen that even when concrete instances of variables are produced, it would be a bit strained to speak of the constructivity of the proof. "Constructed" instances may contain terms introduced by the operation of Skolemization, if existential quantifiers were eliminated in the passage to clausal form. The result of this operation is not (within first order logic) equivalent to the original, but is semantically justified by the axiom of choice [4]: according to Curry [2], this axiom is not acceptable, at least to the intuitionistic branch of constructivism. The constructivity of a mechanical proof procedure may thus be merely formal: insofar as instances of variables involve Skolem terms, these instances are actually "made up", not properly constructed. The object whose existence is proved may be determined in a terminology which is not used in the original axiomatic description, but is instead introduced into it on a constructively dubious basis.

The language of pure Prolog as a syntactic restriction of the full clausal form is partly determined by the requirement that the disjunctions of the clausal form contain at most one positive literal. The way in which the restriction to one positive literal limits the expressive power of the original language is more readily apparent from the implicative form of the clauses. Rewriting the clause scheme

P1 v ... v Pn v ¬Q1 v ... v ¬Qm
as an implication and distinguishing the usual cases of
(a) conditional statements or rules
P1 v ... v Pn <== Q1 & ... & Qm
(b) unconditional statements of facts
P1 v ... v Pn <==
(c) purely negative clauses or denials
<== Q1 & ... & Qm
(d) the empty clause of contradiction
<==
it is seen that the restriction n =< 1 affects only conditional statements and facts and amounts to excluding disjunction from them. However, there is a further defining characteristic of the Prolog sublanguage of the clausal form, namely that denials function only as control statements to the theorem prover. At the general level of theorem proving in clausal logic this is true only of the empty clause, which serves as a Halt statement. In Prolog, this is also true of denials, which serve as Call statements: denials cannot be used in writing but only in calling programs.

3. Definite clause programs

According to the above restrictions, a pure Prolog program can consist of only two kinds of clauses, called definite clauses: restricted conditionals
(a')   P <== Q1 & ... & Qm
and simple facts
(b')   P <==
The reason for the qualifier "definite" is fairly obvious: the conditionals determine definite consequences of the facts, in the sense that they allow no "uncertainty" of the kind which is conveyed by using disjunction or existential quantification in the conclusions. There is no such uncertainty in the facts either: they do not include disjunctive statements or statements of indeterminate, unnamed existence. This discrimination of incomplete information suggests that the logical form of definite clauses can be seen as embodying a constructive conception of description, insofar as constructivism can be characterized as a radically different stance toward what is classically regarded as merely incomplete information. The absence of disjunctive facts and conclusions would correspond to the constructive view, according to which a proof of a disjunctive epitheorem demands the provability of at least one disjunct. As Curry [2] has put it, "we do not admit the possibility that we can be sure of P or Q without knowing which". A similar restriction applies at the level of quantification: in intuitionistic arithmetic, a statement of the form ($x)P(x) is provable only if some ground instance of the formula P(x) is also provable [13]. Thus, in view of the proposed constructive interpretation of definite clauses, even the general limitation of clausal form, namely that the existence of objects in conclusions must be expressed by naming them, loses this limitative character: what is classically seen as simply a Skolemized version appears as a "natural", primary medium of expression if a constructive viewpoint is adopted. Constraining the syntax to definite clauses conveniently prevents affirming something, e.g. ($x)P(x), which could not be affirmed anyway without first affirming something else, in this case P(n); a similar reversal of perspective accompanies the "loss" of disjunction.

The prohibition of disjunction and existential quantification in facts and conclusions need not extend to conditions of implicative clauses: the restriction to simple facts makes it possible to use them in this way without abandoning a constructive framework. Variables appearing in conditions only, such as "y" in the clause

(x,y)  P(x) <== Q(x,y)
can be understood as locally existentially quantified:
(x)  P(x) <== ($y) Q(x,y)
This use of existential quantification seems constructively acceptable, because an application of the rule is bound to instantiate the variable on definite facts or their (definite) consequences. Analogous considerations apply to the use of disjunctive conditions:
  R <== (P v Q) & S
Since this use of disjunction is eliminable, it can readily be tolerated, if disjunction is defined (as a predicate!) by the clauses:
  P v Q <== P
  P v Q <== Q
These clauses, which determine a constructively limited disjunction, simulate a transition to those clauses which would ensue if the disjunction were explicitly eliminated2.

2A real extension of the logical form of definite conditionals is brought about through the possibility of temporarily cutting off part of the axioms in order to block certain proof attempts. This can be used to implement a kind of negation formally within definite clause syntax, thus partly circumventing its defining restrictions. The clauses (for the predicate!) of this negation as failure [1],
  not(P) <== P & cut & 0=1
  not(P) <==
could be related to the tautology
  P ==> ¬ ¬ P
and its contrapositive. The notions of provability and "absurdity" (0=1) also enter in the definition of intuitionistic negation, but in a different manner.

In Heyting's axiomatization of intuitionistic logic, logical axioms are suitably restricted, while the rules of inference remain classical; in definite clause programs, it is extralogical axioms which are constructively restricted. The determination of a constructively restricted syntax of definite clauses can be interpreted in light of Quine's remarks [11] on the relationship between constructivism and intuitionistic logic3:

3The constructive view of definite clauses suggests that the predecessor of their procedural interpretation, given by Kowalski [8], could be sought in the interpretation of intuitionistic logic as a calculus of problems (Aufgabenrechnung), given by Kolmogorov [7].

One can practice and even preach a very considerable degree of constructivism without adopting intuitionistic logic. Weyl's constructive set theory is nearly as old as Brouwer's intuitionism, and it uses orthodox logic; it goes constructivist only in its axioms of existence of sets.

4. The Prologic of Horn clauses

The constructive view of definite clauses can be extended to Horn clauses if denials are understood in the limited Prolog way, as "rhetoric" and instrumental: their function is to activate programs consisting of definite clauses by provoking the theorem prover to refute them by exhibiting counterexamples. The exclusion of denials from programs themselves would correspond to the fact that constructivism defines truth as provability4, which means that negative statements do not belong on the same level as (positive) facts, from which proofs proceed. As Heyting would say, constructive negation cannot be mere "de facto" falsity [6].

4The conception of negation which a logician of constructive persuasion would be lead to consider (and reject) first is negation as unprovability: Curry [2] says that 'since an elementary statement of a deductive theory is true just when there is a demonstration of it ... one would most naturally say that such a statement is false just when no such demonstration exists'. This conception of negation is partly implemented in Prolog through negation as failure.

The connectives of negation and disjunction in the negative clause

(c')   (x,y,...) ¬Q1 v ... v ¬Qm
indicate the way in which the resolution machinery of the Prolog theorem prover operates on the clauses of a program and goals of the form
(c)   ($x,y,...) Q1 & ... & Qm
Thus, a constructive interpretation of logic programming by means of Horn clauses need not attempt to find a constructive interpretation of the negation and disjunction in (c'); rather, (c') should be understood as that negation of (c) which triggers the classical mechanism of reductio ad absurdum. The language of Prolog can thus be understood constructively as resulting from the exclusion of disjunction and negation from clausal logic, while its deductive machinery, which perform inferences over this restricted form, remains classical5.

5In view of the proposed constructive interpretation of Horn clauses, the fact of their theoretical sufficiency may remind one of the Kolmogorov-Gödel proof of the relative consistency of classical with respect to intuitionistic arithmetic [13]: the fact that any problem which can be expressed in clausal form can be reexpressed by means of Horn clauses, as indicated by Kowalski in [8], is reminiscent of the fact that every sentence of classical arithmetic which is a theorem can also be proved intuitionistically. This similarity may be interesting to note, but is rather superficial: the Kolmogorov-Gödel result depends on "homophonic" definitions (of classical connectives through intuitionistic ones) and does not involve passage to the metalanguage, whereas the result on Horn expressibility shows that the metalanguage can be structurally (but not lexically) weaker.

From a traditional logical point of view [5], the proof procedure of the Prolog interpreter is a special case of resolutional refutation. From the viewpoint of the proposed constructive interpretation, it is important that during the propagation of negations of existentially quantified statements through the implicative clauses and at their ultimate confrontation with the facts, instances of the variables are determined (correctly, if occur-checks are performed). The attempt at constructive interpretation at first appears somewhat unusual in that it is precisely the basic deductive mechanism of Prolog

<program> & ¬ ($x) P(x)  |-  
-----------------------------------
<program>  |-  ($x) P(x)
which is the constructively objectionable case of reductio ad absurdum (while the variant with interchanged "signs" of the existential predication is not) [10]. But the Prolog theorem prover performs such reductions over definite clauses, which ensures the constructivity of the procedure6. This constructivity will not be merely apparent: instances of variables will be "actually" constructed, expressed only in the terminology used in the text of the program.

6A constructive motivation can thus be found for Reiter's question [12] concerning the logical form of data bases which yield no indefinite answers to positive queries: a sufficient condition is that the data base be Horn.

Standard Prolog can be concisely described as definite clause logic in which one reasons analytically, always taking the clauses in their given order and first thinking through one condition of a rule before considering the next. This procedure is, however, not complete [9], which complicates the comparison between logical consequence and effective construction [3]. With incomplete systems for logic programming, such as the usual Prolog theorem prover, this comparison remains idealized at a crucial point.

References

  1. Clark, K.L., Negation as failure, in: H. Gallaire and J. Minker (eds.), Logic and data bases, Plenum, New York, 1978.
  2. Curry, H.B., Foundations of mathematical logic, Dover, 1963.
  3. Elcock, E.W., The pragmatics of Prolog: some comments, in: Logic Programming Workshop '83, 1983.
  4. Goldfarb, W.D., Logic in the twenties: the nature of the quantifier, J. Symbolic Logic 44:351-368 (1979)
  5. Hagiya, M. and Sakurai, T., The foundation of logic programming based on inductive definition, New Generation Comput. 2:59-77 (1984).
  6. Heyting, A., Intuitionism: an introduction, North-Holland, New York, 1966.
  7. Kolmogoroff, A.N., Zur Deutung der intuitionistischen Logik, Math. Z. 35:58-65 (1932)
  8. Kowalski, R.A., Logic for problem solving, North-Holland, New York, 1979.
  9. Lloyd, J.W., Foundations of logic programming, Springer, New York, 1984.
  10. Makinson, D.C., Topics in modern logic, Methuen, 1973.
  11. Quine, W.v.O., Philosophy of logic, Prentice-Hall, Englewood Cliffs, NJ, 1970.
  12. Reiter, R., On closed world data bases, in: H. Gallaire and J. Minker (eds.), Logic and data bases, Plenum, New York, 1978.
  13. Robbin, J.W., Mathematical logic - a first course, Benjamin, 1969.