Arch. Math. Logic (1991) 30:297-310

Archive for

Mathematical

Logic

9 Springer-Verlag 1991

Between constructive mathematics and PROLOG* Gerhard Jiiger

Institut fiir Informatik und angewandte Mathematik, Universitiit Bern, Liinggassstrasse 51, CH-3012 Bern, Switzerland Dedicated to Professor Kurt Schiitte on the occasion of his 80th birthday Received August 7, 1989/in revised form August 9, 1990

It is no exaggeration to say that the synthesis of computing and mathematical logic has become one of the most active research areas in the general field of theoretical computer science. The reasons for this development may be manifold, but the following factors certainly deserve some special emphasis: - Mathematical logic is a (the) science of symbol manipulation and symbolic computation. - Logic is a framework for knowledge representation and knowledge engineering. - Logic concepts form a link between computing, artificial intelligence, expert systems, decision support systems and the like. One should also mention the raise of P R O L O G and the Japanese 5th generation computing and observe that during the last few years generations of new computers and computer architectures have been developed which are so powerful that now many theoretical concepts can be realized "on the machine" which had been considered unfeasible until recently. In a way, constructive mathematics at the top and P R O L O G at the bottom form the borderlines of the world of logical programming - one of the most fascinating areas of research where logic meets computer science. A lot is known about both extremes, and serious efforts are made to bridge the gap between the theoretical analysis of constructive mathematics and the practical experience one has gained in many P R O L O G like applications. In the following we give some examples of the interplay between logic and computer science where choice of topics is necessarily influenced by our personal scientific background. The red thread is the idea to survey several formalism for knowledge representation in a very wide sense. We emphasize the notions of proof and provability and try to convey principal concepts rather than precise technical details. However, this article is too brief to deal with these topics in detail; other topics cannot be discussed at all. * A preliminary version of this article has been published in the Proceedings Computer Congress, IFIP '89

11 th

World

298

G. Jfiger The world of logical programming (WLP) CONSTRUCTIVE MATHEMATICS

PROLOG

We propose three subjects of different levels of abstraction. First we discuss some general points concerning (constructive) type theory as the widest framework for most computer science activities. The second section is centered around the notion of abstract provability relation. This concept is an attempt to provide a uniform framework for various kinds of provability where also forms of nonmonotonic reasoning find their place. We study hierarchical and stratified logic programs and use them to illustrate several general principles which have to do with the relationship between various forms of deduction. The third section, finally, is dedicated to the attempt of reflecting negative information by induction principles. I would like to conclude this introduction with a personal remark. It is my wish to express my deepest gratitude for everything that I have learnt from Professor Schfitte. His personal example was very important for my scientific 9 education and in this sense also influenced the present paper.

1 Type theories Constructivity is a very important issue of mathematics, and the recent textbooks by Beeson [1] and Troelstra-van Dalen [42] give a comprehensive survey about the various approaches and the interconnections between them. The computational significance of constructive mathematics, on the other hand, has been discussed in numerous publications and certainly is an issue of some controversy. The traditional logical and proof-theoretic contributions to this field are mostly concerned with computability in principle whereas practical applications require detailed case studies as well as the development and analysis of relevant subtheories. For applications in computer science, constructive mathematics is interesting since it presents a natural framework for describing computationally meaningful concepts and establishes a close connection between proof and computation. As Dijkstra puts it in [10]: "The fundamentally close connections between proving and programming, as revealed by Constructive Type Theory, is beginning to have its impact: programs are deduced from constructive existence proofs and vice versa." Suppose that T is a constructive theory and ~ a proof of a sentence of the form (Vx e A) (3y e B)@(x,y)

(*)

Between constructivemathematicsand PROLOG

299

where A and B are suitable domains and q~a formula which is not too complicated. Then it is often possible to transform r~ into an algorithm f . such that (Vx e A) ([f~(x) e B ^ ~0(x,f~(x))] is true in the intended models of T. Assertion (.) is often considered as the specification of a given problem while the function f~ represents an algorithmic solution of (*). The transformation of the proof rc into the algorithm f~ reflects the procedural content of the constructive environment. If we choose the proper constructive framework, the transformation of a proof into an algorithm is possible with acceptable (polynomial) effort. However, results of this type have to be treated with care since they can only provide a worst case analysis of formal systems. In many interesting cases the algorithm f~ will not be a satisfactory solution of (*). Results become significantly better if one considers consructive theories as a theoretical basis of so called proof development systems. In the ideal case, a proof development system supports the creation of terms, formulas and proofs; it provides a framework for representing programs, stating their properties and proving their termination and correctness. Often one works interactively, and the derivation of a theorem goes in parallel with the design of its algorithm solution and the proof of the correctness of the solution. Proof theory is the link between formal theories and actual computation. Reducing proofs through cut elimination or similar normalization procedures is computing out a formula or a term into its normal form. Hence this corresponds to functional programming languages in which computation takes place by reduction of terms. The theoretical background of present proof development systems is provided by type theory and polymorphic typed lambda calculus P2C. This formalism has a very rich syntactic structure and an expressive power which is sufficient for what is needed today. The central computation rule of lambda calculus is the rewrite rule of fl reduction (2x. t) . aD t[a/x]

([3)

which says that the result of applying the function term 2x. t to the argument a is obtained by substituting a for the free occurrences of x in t. In a typed environment a type is assigned to each expression. Then (fl) is restricted to cases where a and x have the same type, and the termination of reductions by successively applying fl reduction can be proved; each term can be reduced to a so called normal form which does not permit further reductions. The most prominent system with this property is the theory of simple types which is developed for example in Girard [17], Schfitte [38] and Takeuti [41]. The main attraction of polymorphic type structures, which originate from the work of Girard and Reynolds (cf. e.g. [15, 16, 3, 5, 37]), is their strong uniformity. This is achieved by the availability of type variables and the extension of fl to the case where x ranges over types and a is a type. Constructivity comes back through Howard's formulae-as-types approach [19] where a type [A] is associated with each formula A. We may think of [A] as the collection of all (in some precise sense) legitimate proofs of A so that the provability of A reduces to the exhibition of an element of [A]. The constructive interpretation of the logical "-*" junctor for example is illustrated by the fact that

300

G. Jfiger

[ A ~ B ] has to be a subset of the set of all functions from [A] to [B], [ A ~ B ] C [B] ta] 9 A proof of ( A ~ B ) is an operation g which transforms a proof n of A into a proof g(n) of B. There are some very important approaches which exploit the abstract formal treatment of type theory for practically useful computer applications. De Bruijn's AUTOMATH project [9] is a longstanding forerunner in this respect. Constable's proof development system Nuprl [7] goes into the same direction. It is sensitive to the computational meaning of terms, assertions and proofs and designed in such a way that it can carry out the actions used to define that computational meaning. One should also mention the important work done in Edinburgh (cf. e.g. [11]) in connection with LCF and the typed programming language ML, the theory of constructions due to Coquand and Huet [8], and the Swedish group which tries to implement Martin-L6f theories [30, 31, 34, 35]. Feferman's papers [12-14] introduce a new kind of polymorphic type theories which have a constructive interpretation and share all advantages of P2C with respect to uniformity and flexible typing. He presents several examples which indicate t h a t - for applications in computer science- his weak theories are as useful as P2C. Hayashi [18] uses realizability interpretations for a variant of Feferman's theories in order to extract LISP programs from constructive proofs. The theories of types and names in Jfiger [22.] provide another approach to type theories in computer science. They are formulated in a 2-sorted language about object and types. Objects are the entities the computer manipulates with. They are directly accessible and explicitly represented in suitable form, possibly as bitstrings in a computer memory. Types, on the other hand, are abstract collections of objects. The novel point of our approach is that we make sure that every type X has a name nx which is an object. Types X are addressed via their names nx, and nx provides enough information so that (the extension of) X can be computed from nx.

2 Abstract provability relations The previous remarks referred to the upper part of our world of logical programming (WLP). Now we look at its lower part and the problem of knowledge representation which is central to all levels of (WLP). In the ideal world of logical programming, all knowledge about some specific domain is represented in a formal language L; the basic knowledge provides the axioms, and new knowledge is acquired by using an adequate notion of derivability. However, the traditional deductive approach of inference systems is too narrow for many applications and new forms of provability are required which make arrangements for default reasoning, common sense reasoning, nonmonotonic reasoning and the like. Let For L be the set of all L formulas, Pow(FOrL) the power set of For L and ~- the relation of classical provability. As usual we write UL for the Herbrand Universe of L (set of all ground L terms) and BL for the Herbrand base of L (set of all ground atomic L formulas). We denote any binary relation t~- on Pow(ForL) x For L as an abstract provability relation and introduce the following terminology.

Between constructive mathematics and PROLOG

301

1. Suppose that IH C Pow(ForL) x For L. 1. 1~- is called monotonic if we have for all q~6For L and S, T C F o r L

D e f i n i t i o n

SIF-~o and

SCT

=~ T[~-~o.

Otherwise I[- is called non-monotonic. 2. I}- is called correct if we have for all ~o~For L and T C F o r L TIH ~o=~ Zl-~o. 3. It- is called weakly correct if we have for all (0 ~ F o r z and T C F o r z TIH q~ and T consistent =~ Tu{q~} consistent. 4. A subset ~ C U~ is called (T, I}-) definable if there exists an n-ary relation symbol R such that we have for all fi = (al, ..., a,> ~ U~ ~ ~ ~,r

TIH R(fi) .

:~ is called T definable if ~ is (T, F-) definable. It is clear that ~ is an abstract provability relation which is monotonic and correct. In general the demand for the correctness of an abstract provability relation would be too restrictive whereas weak correctness is an adequate requirement. The following observation shows that it is impossible to simultaneously have correctness monotonicity negative information if one works in the limited environment of the so called normal logic programs (cf. e.g. Lloyd [29]). -

Definition 2. A normal logic program is a finite set T of formulas of the form A 1 A... AA.~B

with n > 0 where every Ai is a (positive or negative) literal and B a positive literal. If all A i are positive, we call T a definite logic program. Lemma 3. Suppose that T is a normal logic program, A a positive literal and I~- C Pow(ForL) x For L an abstract provability relation such that T I~- -7 A. Then we have 1. I~- is not correct. 2. I f I~- is weakly correct, then [~- is non-monotonic. This lemma can be easily generalized to more general situations (e.g. inductive theories). It is often considered as a justification for the need of non-monotonic reasoning in the context of subsystems of predicate logic. Many approaches to general forms of default reasoning can be conveniently studied in the context of default operators (cf. Jfiger [23]). Every partial operator A : Pow(ForL)--+Por(FOrL)

induces an abstract provability relation [~ defined by Tl~q~ :'~ A(T)~ q~

302

G. J/iger

for all formulas q~and all T ~ domain(A). The idea of this approach is the following: Tis the explicit description of a situation as it is given to us, and the transition from T to A(T) reflects the default component of our reasoning process. Often the amount of information that needs to be represented may be prohibitively large and logically intricate so that questions of computational complexity become very important. One of the most promising approaches to achieve efficiency is the restriction to positive information; negative information then has to be deduced by using suitable forms of default reasoning which often go along with meta-concepts. This strategy is followed for example in various versions of implemented P R O L O G . However, it is impossible to discuss this topic in detail. Instead we turn to a very special case which illustrates some general ideas and phenomena. Reiter's closed world assumption [36] is one of the most elementary and most rigid forms to introduce negative information. The closed world C W A ( T ) of a theory T is defined as the set of formulas C W A ( T ) : = T w {--7 A : A e B L A TI-/A} and gives rise to a total default operator C W A : Pow(FOrL)~Pow(FOrL);

T~CWA(T).

The corresponding abstract provability relation [~-cwa is non-monotonic and weakly correct for definite logic programs but not weakly correct for normal logic programs. In order to keep the notation as simple as possible we restrict ourselves to hierarchical and stratified programs (cf. [29]): They should be considered as representatives of the large class of structured programs and illustrate some results concerning their behaviour with respect to various proof methods. Definition 4. Let T be a normal logic program. 1. A level mapping for T is a function which assigns a non-negative integer to every relation symbol of T. IfA is a literal of T and a a level mapping for T, then a(A) is defined to be the non-negative integer which is assigned by ~ to the relation symbol of A. 2. T is called hierarchical if there exists a level mapping a for T such that we have for every element (A1 A... A A,--*B) of T: e(B)> e(Ai) for i = 1,..., n. 3. T is called stratified if there exists a level mapping fl for T such that we have for every elements (A 1 A... A A , ~ B ) of 72. - ~(B) > fl(ai) for i = 1..... n. - fl(B)> fl(Ai) for all Ai which are negative. Logic programs of these forms are important for practical applications of logic programming and provide a well structured class of theories which have an interesting proof theory. Every definite logic program and every hierarchical logic program is stratified. There are definite logic programs which are not hierarchical. Examples 5. 1. T 1 : = {A, A ~ B} is definite and hierarchical. 2. T2:= { ~ A ~ B } is hierarchical but not definite. 3. T3: = {P(0), e(x)--,P(s(x)), Q(1)} is definite but not hierarchical. 4. T4: = {P(0), P(x)--,t'(s(x)), Q(1), ~ e ( x ) ~ Q ( x ) } is stratified but not definite and not hierarchical.

Between constructive mathematics and PROLOG

303

At first glance it seems that hierarchical programs prevent recursive definitions of relations. However, this is not the case if we choose classical logic for the deduction provess, Theorem 6. Every set ~i C U~ which is definable by a definite logic program is also

definable by a hierarchical logic program. Instead of giving a proof of this theorem, we present an example which indicates how the recursive part of a definite logic program can be simulated through a hierarchical program.

Example 7. Let T be the definite logic program {P(0), P(x)~P(s(x)), Q(1)}. It is easy to see that the set ~ : = {0, s(0), s(s(O)).... } is definable by T. In order to define ~ hierarchically, we choose a new relation symbol R and consider the hierarchical program S given by

{P(0), P(x) ^

--7 P(s(x)) ~

R(y), P(x)--, R(x), Q(1)}.

Then we have for a e UL : T ~-P(a) r S~-R(a). One can argue whether classical logic is the adequate framework for dealing with stratified and hierarchical programs and reflecting their intended meaning. Attempts to replace it by intuitionistic or 3-valued logic seem to be very promising. If we take precautions for dealing with negative information, then the proof theory of hierarchical programs turns out to be extremely natural. Now we consider a version of the closed world assumption tailored for the use in connection with hierarchical programs. We assume that T is a hierarchical logic program and ~ minimal level mapping for T. The hierarchical closed world HCWA(T) of T is defined by recursion on n:

HCWAo(T): = Tw {--7A : A e BL, a(A) = 0 and T ~ A } HCWA. +,(T): = HCWA,(T) w {--7A : A e B E, a(A) = n + 1 and HCWA,(T)~A} HCWA(T):= U HCWA,(T). hen

The stratified closed world SCWA(T) of a stratified logic program T and its levels SCWA.(T) are defined accordingly.

Example 8. Let A and B be positive literals and T be the hierarchical logic program {-7A-~B}. Then we have: 1. CWA(T)={--7A~B, --7A,-TB} is inconsistent. 2. HCWA(T)=HCWAo(T)= {--3A~B, --7A} is consistent. Theorem 9. I f T is a hierarchical logic program, then HCWA(T) is consistent. There are hierarchical programs T with the property that the defining power of T is greater than the defining power of HCWA(T). It is also the case that the defining power of all definite logic programs plus CWA goes much beyond the defining power of all hierarchical programs plus HCWA. It is also possible to extend this entire approach to broader classes of theories (stratified logic programs, inductive theories, etc.) but we will not follow this line now and confine

304

G. J/iger

ourselves to quoting a result concerning the defining power of the stratified closed world assumption.

Definition 10. A subset ~ of the natural numbers N is called arithmetic if there exist a natural number n ~ N and an (n + 1)-ary recursive relation ~ such that we have for all m ~ N : m ~ ~t ~ l q ~ Yx x3x2...]x,~(xl, x2 .... , x,, m).

Theorem 11. All arithmetic subsets of the natural numbers N are definable by stratified logic programs and the stratified closed world assumption S C W A , More precisely this means: for every arithmetic subset ~ of N there exists a stratified logic program T and a relation symbol R such that we have for all m ~ N : m ~ ~ , ~ SCWA(T)f-R(s"(O)).

J/iger and St~irk [24] is concerned with an exact analysis of the defining power of stratified and hierarchical logic programs with and without appropriate closed world assumptions. This analysis also relates the defining power of stratified and hierarchical programs (with and without appropriate dosed worlds assumptions) very precisely to notions and hierarchies in classical definability theory.

3 Negative information and induction Induction principles are the mathematical way of introducing negative information. They are most commonly used in the form of complete induction on the natural numbers but also appear in many different forms (inductive definition of lists, expressions, terms, etc.). If we define a set E by stating that (i) E contains the natural number 0, and (ii) E is closed under addition of 2, then we often tacitly assume that E is the least set with this property and every element which is not of the form 0, 2, 4 .... does not belong to E. Therefore we strengthen the definition clauses (i) and (ii) by the default assumption that we are interested in the minimal solution of (i) and (ii). A general form of induction can be introduced as follows.

Definition 12. Let A(P, x) be a formula which contains no negative occurrences of the unary relation symbol P. Then we denote the sentence Vx[A(P, x) ~ P(x)]

(*)

as an inductive definition. A set I is called a fixed point of this inductive definition if we have (Vx[ A( I, x) ~ x ~ I].

J is the least fixed point of(*) i f J is a fixed point of(,) and a subset of every other fixed point of (*). In order to give a simple example, we consider the inductive definition of the even natural numbers mentioned above: Vx[x = 0 v 3y(P(y) A x = y + 2)~P(x)].

The set 2 N = { 0 , 2 , 4 , . . . } is the least fixed point; other fixed points are for example the sets of the integers Z and the set of the even integers 27Z.

Between constructive mathematics and PROLOG

305

I~emark 13. Let D(P) be the inductive definition Vx[A(P,x)~ P(x)]. Then we have: 1. D(P) has a least fixed point I. 2. If A(P, x) is recursively enumerable, then I is recursively enumerable. 3. Often there exist recursive fixed points although the least fixed point is recursively enumerable but not recursive. Inductive definitions D(P) of predicates P are typical candidates for passing on positive information. They state what is true provided that some (positive) assertion about P is true, but they do not state what is false. It is impossible to use the pure inductive definition of a predicate P in order to prove that a particular element does not belong to P. This can be only achieved by an additional default assumption that P is supposed to be a fixed point of D(P) (local default assumption) or the least fixed point of D(P) (global default assumption). McCarthy's notion of circumscription is an attempt to generalize the idea of inductive definability and to use it for knowledge representation systems in artificial intelligence and logic programming [32, 33]. In order to simplify the notation we will assume that T is a theory of the form

T=SFu{D(P)}. We assume further that SF is a set of formulas (stable facts) which do not contain the relation symbol P, and D(P) is a sentence which collects all information about P which is explicitly given to us. The circumscription of T with respect to P is the theory CIRp(T) which has as axioms: (i) SF; (ii) D(P); (iii) D(q~)AVx[q~(x)~P(x)] ~Vx[P(x)~q~(x)] for all formulas ~0. The axiom scheme (iii) is an induction principle which formalizes that there are no definable proper subsets of P which satisfy the condition D. Put in other words, we can say that (ii) and (iii) make sure that P is a minimal witness for D.

Examples 14. Let SF be a theory which contains the three distinct constants 0, 1 and 2 and a reasonable part of number theory. 1. T: = SF•{P(O) v (n(l) A n(2))}. Then CIRp(T) proves: P--= {0} v P = {1, 2}. 2. T:=SFu{P(O)AVx[P(x)~P(x')]. Then CIRp(T) proves for all formulas q~: ~0(0) ^ Vx [q~(x)~ q~(x')] ~Vx[n(x) ~ q~(x)]. 3. T: = SFu{Vx[(Vy >=x) ~ P(y)~P(x)]}. Then we have for all subsets I C IN: D(I) is ture r is infinite. Since there is no least infinite subset of the natural numbers, the last example shows that circumscription may transform a consistent theory T into an inconsistent CIRp(T). Accordingly the abstract provability relation I~cm is not correct, not even weakly correct in the general case; IF-'cmis nonmonotonic. The problem of the consistency of the circumscription method is a major topic and has been addressed in various publications (cf. e.g. J/iger [21,23], Lifschitz [27, 28]). Large classes of theories T could be isolated such that CIRe(T ) is guaranteed to be consistent. In the case of inductive definitions the situation is much simpler: As a consequence of Remark 13 we have that every theory T of the form SFu {D(P)} is consistent provided that D(P) is an inductive definition and SF a consistent theory which does not contain the relation symbol P.

306

G. Jgger

Theorem 15. Let T be of the form SFu{D(P)} where D(P) is an inductive definition and SF a consistent theory whose formulas do not contain the relation symbol P. Then we have:

1. CIRp(T ) is a conservative extension of T for all sentences which are positive in P. 2. CIRj,(T) is consistent. 3. [~IR is weakly correct for such T. A similar result holds for the case of iterated inductive definitions. Since for practical applications of circumscription most interesting cases are covered by theories consisting of stable facts and inductive definitions, it is guaranteed that circumscription can be used as a safe default rule in nearly all relevant situations. Besides that, circumscription is based on the mathematical concept of induction so that its mathematical foundations are clear. The real problem in the use of circumscription is a computational one: How can one detect the suitable instances of the induction scheme (iii)? Results are known which establish some connections between the (computational) complexity of circumscription and the (logical) complexity of the formulas in the induction scheme (iii). However, this is not the place to go into this direction, and instead we will turn to an interesting subsystem. Let T be again a theory of the form SF~{Vx[A(P,x)~P(x)]} with Vx[A(P, x)~P(x)] an inductive definition and SF as before. Then the completion COMe(T) of T with respect to P is defined as

COMe(T): =SFu{Vx[A(P, x ) ~ P(x)]}, i.e. the implication sign in the inductive definition is replaced by an equivalence. Hence the completion of T with respect to P only formalizes that P is an arbitrary fixed point of the inductive definition under consideration in contrast to CIRe(T ) which forces P to be the least (definable) fixed point. It is clear that COMe(T) is contained in CIRv(T); in general COMe(T) is prooftheoretically much weaker than CIRp(T). However, we gain a reduction of the induction scheme to a single axiom. Our default operator COM is closely related to Clark's program completion (cf. e.g. Clark [6], Lloyd [29]) which is often studied in P R O L O G environments in connection with the famous negation as failure rule, also due to Clark. Recent results of Kunen [25, 26] and Shepherdson [39, 40] relate negation as failure and program completion in the context of 3-valued logic and help a lot to clarify the logical status of this intricate rule. In the rest of this paper we will try to analyze circumscription and completion of theories from a different perspective. We will also take the opportunity to address some open problems and to make some comments about ongoing research in this direction. It is often argued that the Herbrand universe is the adequate universe for logic programming, logical data base, artificial intelligence, etc. and that it is better tailored for most applications than arbitrary first order structure. Therefore we restrict considerations to Herbrand structures (i.e. structures whose domain of individuals consists of UL) and define T ~ ~o: ~ q~ is valid in all Herbrand models of T

Between constructive mathematics and PROLOG

307

Let L< be a language with the constants 0, 1, 2, 3.... and the relation symbol <, and let T be the theory of linear orderings. Then N is a Herbrand model of ~ ~ is a model of T but obviously not a Herbrand model. For the treatment of negative information by inductions, it is interesting to observe that COMe(T ) and CIRI,(T) often agree on all Herbrand models although COMp(T) is strictly weaker than CIRe(T) if all first order models are taken into account. To give an example, we may consider the non-negative even integers as subset of the integers. First we generate the integers by the following definite logic program: {Z(0), Z(x)--* Z(s(x)), Z ( x ) ~ Z(m(x) )} where s(x) and m(x) are to be interpreted as x + 1 and - x , respectively. The Herbrand universe of this program is given by the set {0, s(O),m(0), s(s(O)), s(m(O)), ... }. Now the even numbers E can be introduced by the following inductive definition:

Vx[x = 0 v 3y(E(y) ^ x = s(s(y)))-* E(x)] . It is easy to check that the set {0, s(s(0)),...} is the only fixed point of this inductive definition over the Herbrand universe. Hence COME(...) and CIRE(...) agree for ~nThe inductive definitions which have exactly one fixed point over their Herbrand structures, we call them unitary inductive definitions, form an important subclass of all inductive definitions: - Many inductive definitions which are interesting for theoretical and/or practical reasons are unitary or can be transformed into unitary inductive definitions. If we restrict ourselves to Herbrand models and if the relation P can be introduced by an unitary inductive definition, then the computationally unfeasible theory CIRp(T) can be replaced by the much simpler COMe(T). Hence the property of being unitary permits the replacement of an axiom scheme (with infinitely many instances) by a single axiom. Most logic programs can be interpreted as (iterated) inductive definitions. Unitary inductive definitions correspond to programs with an especially nice declarative structure and are related to canonical programs due to Jaffar and Stuckey [20] and determinate programs due to Blair I-2]. One major open problem is to give a complete characterization of the unitary inductive definitions. Partial answers are known. However, the present results depend on fairly complicated term orderings, and it is not clear whether the methods employed so far will lead to a complete answer. The restriction to Herbrand universes is certainly justified if we work with finite universes (with a sufficiently small number of elements). In the general case, however, if infinite universes are allowed as well, a restriction to validity in all Herbrand models goes beyond first order logic. It is clear that Tt-q~ implies T ~ t p but the converse implication is not true in general. We obtain a syntactic counterpart of ~ if we extend the usual provability relation ~- by a new derivation rule. -

-

308

G. J~ger

Let al, a2, a3 be an enumeration of all elements of the Herbrand universe U v Then the Herbrand rule is the following infinitary rule of inference: ....

qg(ax), q~(a2),q~(a3), ... Vxg(x) A full implementation of this rule is impossible. But there exist several approximations which attempt to reflect the Herbrand structure in a suitable derivation process and make use of meta rules and strategies. The essential new point is that formally infinite deduction systems often grant a high degree ~of uniformity which is not possible in strictly finite systems. This uniformity has then to be exploited in order to represent infinite proofs by finite objects which can be handled by the machine. The situation is analogous to the treatment of n. This transcendental number can be considered as the infinite decimal fraction 3.14... or as a finite object which consists of the rules which have to be carried through to calculate this fraction. Infinitary deduction systems can also be applied to study the negation as failure rule and to find out how it relates to the closed world assumption. Formulated in a rather imprecise manner, we can essentially prove the following assertion. For every logic program T (satisfying several technical conditions which we omit) one can form an infinitary deduction system ID(T), the inductive hull of T, that possesses the following properties: (I) If A is a positive sentence, then we have

TF-A ~, ID(T)F-A ~ ID(T)~-~ (II) If B is a negative sentence, then we have

CWA...(T)F-B ,~ ID(T)F-B T~V B .r ID( T ) V ~ . Here T~VB is a shorthand notation for the fact that B is provable in T with help of the negation as failure rule. ID(T)P-~ means that in the infinitary deduction system I(DT) there exists a finite proof of B. Hence the restriction of ID(.) to finite proofs induces a default operator which corresponds to provability with the negation as failure rule. This operator is not first order definable but can be represented by strictly finite meta-considerations.

References 1. Beeson, M.J.: Foundations of constructive mathematics. Berlin: Springer 1985 2. Blair, H.A.: Decidability in Herbrand bases. In: Minker, J. (ed.) Proceedings Workshop Foundations of Deductive Databases and Logic Programming, Washington, CD, 1986 (draft) 3. Bruce,K., Meyer, A., Mitchell,J.: The semantics of second order lambda calculus.Inf. Control (to appear) 4. Buchholz, W., Feferman, S., Pohlers, W., Sieg, W.: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies. (Lect. Notes Math. Vol. 897) Berlin: Springer 1981 5. Cardelli, L., Wegner, P.: On understanding types, data abstraction and polymorphism. Comput. Surv. 17, 471 522 (1985)

Between constructive mathematics and PROLOG

309

6. Clark, K.L.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases. New York: Plenum Press 1978, pp. 293 322 7. Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing mathematics with the Nuprl proof development system. Englewood Cliffs: Prentice-Hall 1986 8. Coquand, T., Huet, G.: Constructions: a higher order proof system for mechanizing mathematics. In: Proceedings EUROCAL 85. (Lect. Notes Comput. Sci., Vol. 203, pp. 151-184) Berlin: Springer 1985 9. de Bruijn, N.G.: A survey of AUTOMATH. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism. New York: Academic Press 1980, pp. 57%606 10. Dijkstra, E.W.: A new science, from birth to maturity. In: Bauer, F.L., Dijkstra, E.W.: Zwanzig Jahre Institut frir Informatik. Report No. 95, Institut frir Informatik, ETH Zririch, ZiJrich, 1988 11. Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF. (Lect. Notes Comput. Sci., Vol. 78) Berlin: Springer 1979 12. Feferman, S.: A language and axiom for explicit mathematics. In: Algebra and Logic. (Lect. Notes Math., Vol. 450, pp. 87-139) Berlin: Springer 1975 13. Feferman, S.: A theory of variable types. Rev. Colomb. Mat. XIX, 95-105 (1985) 14. Feferman, S.: Polymorphic typed lambda-calculi in a type-free axiomatic framework. In: Sieg, W. (ed.) Logic and computation (Contemporary mathematics, vol. 106, pp. 101-136) Providence, Rhode Island: American Mathematical Society 1990 15. Girard, J.-Y.: Une extension de rinterpretation de Grdel a l'analyse, et son application a l'elimination des coupures darts ranalyse et la theorie des types. In: Proceedings 2nd Scandinavian Logic Symposium, pp. 63-92. Amsterdam: North-Holland 1971 16. Girard, J.-Y.: The system F of variable types, fifteen years later. Theor. Comput. Sci. 45, 159-192 (1986) 17. Girard, J.-Y.: Proof theory and logical complexity, vol. I. Napoli: Bibliopolis 1987 18. Hayashi, S., Nakano, H.: PX a computational logic. Report Research Institute for Mathematical Sciences, Kyoto University, Kyoto, 1987 19. Howard, W.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism. Amsterdam: Academic Press 1980, pp. 47%490 20. Jaffar, J., Stuckey, P.J.: Canonical logic programs. J. Logic Program. 2, 143-155 (1986) 21. J/iger, G.: Some contributions to the logical analysis of circumscription. In: Proceedings of CADE 86 - 8th International Conference on Automated Deduction. (Lect. Notes Comput. Sci., Vol. 230, pp. 154-171) Berlin: Springer 1986 22. J/iger, G.: Induction in the elementary theory of types and names. In: Brrger, E., Kleine Brining, H., Richter, M.M. (eds.) Proceedings CSL '87. (Lect. Notes Comput. Sci., Vol. 329, pp. 118-128) Berlin: Springer 1988 23. J/iger, G.: Non-monotonic reasoning by axiomatic extensions. In: Fenstad, J.E., Frolow, I.T., Hilpinen, R.: Proceedings 8th International Congress for Logic, Methodology and Philosophy of Science, pp. 93-110. Amsterdam: North-Holland 1989 24. J/iger, G., St/irk, R.: The defining power of stratified and hierarchical logic programs. Technical report IAM-90-004, Institut frir Informatik und angewandte Mathematik, Universit/it Bern, 1990 25. Kunen, K.: Negation in logic programming. J. Logic Program. 4, 289-308 (1988) 26. Kunen, K.: Signed data dependencies in logic programs. J. Logic Program. 7, 231-245 (1989) 27. Lifschitz, V.: Closed world data bases and circumscription. Artif. Intell. 27, 229-235 (1985) 28. Lifschitz, V.: On the satisfiability of circumscription. Artif. Intell. 28, 17-27 (1986) 29. Lloyd, J.W.: Foundations of logic programming. Berlin: Springer 1987 30. Martin-Lrf, P.: Constructive mathematics and computer programming. In: Proceedings 6th International Congress for Logic, Methodology and Philosophy of Science, pp. 153-175. Amsterdam: North-Holland 1982 31. Martin-Lrf, P.: Intuitionistic type theory. Napoli: Bibliopolis 1984 32. McCarthy, J.: Circumscription - a form of non-monotonic reasoning. Artif. Intell. 13, 27-39 (1980)

310

G. J/iger

33. McCarthy, J.: Applications of circumscription to formalizing common sense knowledge. Artif. Intell. 28, 89-118 (1986) 34. Nordstrom, B., Petersson, K.: Types and specifications. In: Proceedings IFIP '83, pp. 915-920. Amsterdam: North-Holland 1983 35. Nordstrom, B., Smith, J.: Propositions, types, and specifications in Martin-L6fs type theory. BIT 24, (3), 288-301 (1984) 36. Reiter, R.: On closed world data bases. In: Gallaire, H., Minker, J. (eds.) Logic and data bases, pp. 55-76. New York: Plenum Press 1978 37. Reynolds, J.C.: Towards a theory of type structure. In: Proceedings Colloque sur la Programmation. (Lect. Notes Comput. Sci., Vol. 19, pp. 408-425) Berlin: Springer 1974 38. Schiitte, K.: Proof theory. Berlin: Springer 1977 39. Shepherdson, J.C.: Negation in logic programming. In: Minker, J. (ed.) Deductive databases and logic programming, pp. 19-88. Los Altos: Kaufmann 1988 40. Shepherdson, J.C.: A sound and complete semantics for a version of negation as failure. Theor. Comput. Sci. 65, 343-371 (1989) 41. Takeuti, G.: Proof theory. Amsterdam: North-Holland 1975 42. Troelstra, A.S., van Dalen, D.: Constructivism in mathematics I, II. Amsterdam: NorthHolland 1988