UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

An environment theory with precomplete negation over pairs Andrews, James H. 1986

Your browser doesn't seem to have a PDF viewer, please download the PDF to view this item.

Item Metadata


831-UBC_1986_A6_7 A54.pdf [ 3.94MB ]
JSON: 831-1.0051879.json
JSON-LD: 831-1.0051879-ld.json
RDF/XML (Pretty): 831-1.0051879-rdf.xml
RDF/JSON: 831-1.0051879-rdf.json
Turtle: 831-1.0051879-turtle.txt
N-Triples: 831-1.0051879-rdf-ntriples.txt
Original Record: 831-1.0051879-source.json
Full Text

Full Text

AN ENVIRONMENT THEORY W I T H P R E C O M P L E T E N E G A T I O N O V E R PAIRS By JAMES HAROLD ANDREWS B . S c , University of British Columbia,  1982  A THESIS S U B M I T T E D IN P A R T I A L F U L F I L L M E N T O F T H E REQUIREMENTS FOR T H E D E G R E E OF M A S T E R OF SCIENCE in T H E F A C U L T Y O F G R A D U A T E STUDIES ( D E P A R T M E N T O F C O M P U T E R SCIENCE)  We accept this thesis as conforming to the required standard  T H E U N I V E R S I T Y O F BRITISH C O L U M B I A September  1986  © James Harold Andrews,  1986  In p r e s e n t i n g  t h i s t h e s i s i n p a r t i a l f u l f i l m e n t of  requirements f o r an advanced degree at the  the  University  of B r i t i s h Columbia, I agree t h a t the L i b r a r y s h a l l make it  f r e e l y a v a i l a b l e f o r reference  and  study.  I further  agree t h a t p e r m i s s i o n f o r e x t e n s i v e copying o f t h i s t h e s i s f o r s c h o l a r l y purposes may department or by h i s or her  be granted by  the head of  representatives.  my  It is  understood t h a t copying or p u b l i c a t i o n o f t h i s t h e s i s f o r f i n a n c i a l gain  s h a l l not be allowed without my  permission.  Department o f  CowPuret.  QcxetJCE  The U n i v e r s i t y of B r i t i s h Columbia 1956 Main Mall Vancouver, Canada V6T  1Y3  Date  DE-6  (3/81)  QdJt,  (4/^6  written  Abstract  A formal semantics of Voda's Theory of Pairs is given which takes the naturaldeduction form of Gilmore's first-order set theory. The complete proof theory corresponding to this semantics is given. Then, a logic programming system is described in the form of a computational proof theory for the Gilmore semantics. This system uses parallel disjunction and the technique of precomplete negation; these features are shown to make it more complete than conventional logic programming languages. Finally, some alternative formulations are explored which would bring the logic programming system described closer to conventional systems. The semantic problems arising from these alternatives are explored. Included in appendices are the proof of completeness of the complete proof theory, and the environment solution algorithm which is at the heart of precomplete negation over pairs.  ii  C o n t e n t s  Abstract  ii  Acknowledgement  vi  1  Introduction  1  2  Research Background  3  2.1 2.2 2.3 2.4 3  Natural Deduction Semantics and Proof Theories Truth-Value Gaps Programming Language Semantics Negation in Logic Programming  Environment Theory 3.1 Elementary Syntax 3.2 Formal Semantics 3.3 Proof theory C : Complete 3.4 Proof Theory R: R - M a p l e  14 15 23 30 36  Alternative Formulations 4.1 Simulated Parallelism 4.2 Sequential Disjunction 4.2.1 Unchanged Semantics 4.2.2 Modified Semantics for Disjunction 4.2.3 Modified Semantics for Disjunction and Quantifiers 4.3 Parallel Conjunction  52 52 56 57 58 60 61  4.4  62  +  4  5  3 5 6 10  Negation as Failure  Conclusions and Future Work  66  Bibliography  69 iii  A  Completeness P r o o f for C  71  B  Environment Solution Algorithm  83  iv  List of Tables A{Ext {Seq))  73  m  v  Acknowledgement  My family, friends, and workmates have all contributed to making these last two years enjoyable and educational. In particular, for interesting and often crucial discussions about my thesis work I would like to thank Karl Abrahamson, Peter Apostoli, Paul Gilmore, Rick Morrison, and of course Paul Voda. This work has been supported by scholarships from the Natural Sciences and Engineering Research Council and from Bell-Northern Research Ltd., for which I am greatly appreciative.  vi  Chapter 1 Introduction Kowalski [Kow74] expressed the paradigm of logic programming as "the interpretation of sentences in predicate logic as programs, of derivations as computations and of proof procedures as feasible executors of predicate logic programs." This paradigm is now generally accepted.  However, since the popularization of Prolog the connec-  tion between logic programming and mathematical logic has sometimes seemed vague. Research has largely diverged into two styles: the implementation of systems which are computationally powerful but theoretically far from formal logic, and the study of systems that are formally well-founded but computationally uninteresting. Recent research has attempted to reassert the connection between traditional logic and useful programming. In Paul Voda's work, a Theory of Pairs (TP) is developed as an axiomatic first-order theory, in order to provide a logical foundation for computations over a simple, recursively-defined domain. Then, programming languages are embedded in that theory, in the sense that each programming language is defined by  1  CHAPTER  1.  INTRODUCTION  2  a proof theory which can prove a subset of the theorems of T P . The main contribution of this part of Voda's work is not the particular programming languages set forth, but rather the enclosing structure given by the Theory of Pairs, and the simple but rigourous association of languages with logic. This thesis makes three main contributions.  Firstly, it expresses the relatively  informal semantics of Voda's original papers by a natural deduction Gilmore semantics. Secondly, it provides a complete proof theory in the style of Gilmore, which can be used as a tool to prove properties of programs and programming systems.  Thirdly,  it describes a language which handles negation in a way which comes much closer to complete classical negation than does negation as failure, the most popular treatment of negation in logic programming. This precomplete negation was defined by the author following suggestions by Voda, and is the main feature of the language.  Voda has described precomplete negation  over the domain of integers in [Vod86c]; Gilmore [Gil86a] has described a very similar technique for computing negation in a database-oriented set theory. The domain of this paper is that of the pairs; however, in the formal semantics and the proof theories described in these pages, all variables are collapsed into a single variable which takes values ranging over the environments. So it seems a good characterization to describe the theory as "an environment theory with precomplete negation over pairs".  Chapter 2 Research Background The present thesis could be seen as making contributions to applications of natural deduction first-order logic with truth-value gaps; programming language semantics; and the treatment of negation in logic programming. In this chapter we trace some of the background of these areas of research.  2.1  Natural Deduction Semantics and Proof Theories  Until the time of Gentzen, the proof theories most studied were those classified as "axiomatic", that is characterized by many axioms and few rules of deduction. The proof theory presented by Hilbert and Ackermann [HA38], for instance, contains modus ponens as the sole rule of deduction. Such proof theories are consistent and complete with respect to the standard semantics, as proved by Godel (see for instance [Men64]); however, the rules of deduction are not necessarily clearly related to the semantics.  3  CHAPTER  2.  RESEARCH  BACKGROUND  4  Gentzen's approach [Gen69] was to define a proof theory using few axioms and many rules of deduction, and to emphasize the purely syntactic, proof-theoretic component of formal first-order logic. The basic elements of his proof theory were sequents, rather than individual formulae. He proved consistency of his system by showing that the empty sequent (the basic form of contradiction) could not be derived in the proof theory. The Hauptsatz, or Main Theorem, leading to this conclusion was his proof of cut elimination. This was the proof that a derivation using applications of the cut rule, the only rule of inference which decreased the number of formulae in a sequent, could be manipulated to remove all such applications. The rules of deduction of Gentzen's system looked very much like the semantic entailment rules - hence the description of it as a "natural deduction" system.  In  such a system, consistency and completeness of the proof theory with respect to the semantics can be proven in a simple manner, and without the use of the cut-elimination result. Such proofs, however, still resort to the intuitive notions of set and number which form the basis of model theory. Following on this work, Beth [Bet66] and Smullyan [Smu68], among others, expressed proofs in the form of "semantic" or "analytic tableaux", which are equivalent to Gentzen-style sequent proofs. These presentations considered the basic elements of the proof theory as trees of formulae rather than as structured sequences. Gilmore, in his presentation of first-order logic [Gil86b], adopts a style of proof  CHAPTER  2.  RESEARCH  BACKGROUND  5  theory much closer to that of Gentzen. Sentences are given a "sign" denoting truth value, as in Smullyan. Sequents are once again the basic proof-theoretic elements, but are considered as sets of signed sentences rather than sequences of formulae. This leads to a straightforward definition of validity based on intuitive notions of set theory. The main purpose of Gilmore's work, however, is to present extensions of classical first- and second-order logic which define a formal set theory. This set theory resolves the standard set-theory paradoxes (see for instance [Bet66]) by refusing to assign a truth value to paradoxical sentences. It is on the first-order version of Gilmore's set theory, for a specific domain of constants (the domain of pairs) that the present work is largely built. The analogues of set terms are programmatic predicate definitions. Definitions can be made which would lead the language into infinite computation. Calls to predicates with such definitions are not assigned the same truth value in all bases, and therefore are effectively of indeterminate truth value.  2 . 2  T r u t h - V a l u e  G a p s  Kripke, in his presentation of a truth-value semantics for language [Kri75] which is similar to Gilmore's for set theory, discusses these truth-value gaps, arguing from a philosophical viewpoint that it is not always possible to determine the truth of an assertion. He points out that the existence of a truth-value gap does not imply the existence of a third truth value, only that some formulae cannot be assigned a truth  CHAPTER  2.  RESEARCH  BACKGROUND  6  value. He proposes a transfiriite hierarchy of truth definitions for a hierarchy of abstract languages, one of which languages (at some ordinal) will be able to refer to its own truth definition. Around the same time, Scott [Sco75] proposes a similar hierarchy for a logic based on the lambda-calculus. However, he describes the hierarchy only up to to. Naturally only the first of the hierarchy of truth predicates corresponds to computable truth. Fitting [Fit85] accepts the gappy first-order truth definition as a given. He formulates the standard fixpoint semantics of logic programs (see below) in a three-valued setting, although the third value is described as meaning only "undefined". In the sequel we will present the extended first-order logic of environment with only two truth values. As Scott points out, "[an undefined formula] could indeed be given a truth value if we would want to be perverse, but there is no need to be so". However, we will sometimes act as if this third truth value exists for the purpose of clarity; we will say that a sentence takes the undefined truth value, or takes the ? sign, when that sentence's truth value is not determinate in all bases.  2.3  Programming Language Semantics  The traditional method of defining the semantics of algorithmic languages is that of operational semantics, in which an abstract machine is defined which computes the language. One problem with operational semantics is the possible need to define the  CHAPTER  2.  RESEARCH  BACKGROUND  7  semantics of the abstract machine, and so on down to the bit flow level; the other problem is deeper. What is actually defined by operational semantics is simply a characterization of the computations performed by the system. This characterization could be expressed either semantically or syntactically; the syntactic expression leads to a proof theory, while the semantic expression leads to a model theory with respect to which the proof theory is trivially complete (trivially because the semantics is no more than a transcription of the proof theory into semantic concepts).  Denotational semantics [Sto77] solves  the first problem of the operational approach by basing the language on well-studied notions of set and function, but fails to solve the problem of semantic triviality. A n operational semantics for logic programming is given by van Emden and Kowalski [vEK76], but they consider it useful only as a characterization of the computations. The fixpoint semantics they give has become the standard semantical model for Prolog and logic programming in general. Fixpoint semantics arises from the observation that the set of all Herbrand interpretations for a set of Horn clauses (a Prolog program) form a complete lattice under the subset relation. Thus each program is seen as defining a separate first-order theory with a separate semantics. The goal of computation is seen as finding the least fixpoint of a monotone transformation on this lattice (the predicate-application transformation). This is then proved to be the least upper bound of all the interpretations, on the lattice, of the clauses of  CHAPTER 2. RESEARCH BACKGROUND  8  the goal. The standard proof theory for logic programs is some application of the resolution principle, such as SLD-resolution [AvE82]. Although SLD-resolution is complete, it is not deterministic, i.e., not systematic, to use the terminology of Smullyan. Therefore, if it is to be considered as a proof theory for a computational system there must be a further description of the method of generating proofs for the system to be fully characterized. Lloyd, therefore, adds to a fixpoint semantics in the style of van Emden and Kowalski, and the resolution-based proof theory in the style of Apt and van Emden, a "procedural semantics" for finding resolution proofs, which is really a form of operational semantics. Voda presents a markedly less complex view of logic programming. In a series of papers ([Vod84], [Vod85], [Vod86b]), he describes a first-order theory of basic data types, the Theory of Pairs; he then presents logic programming systems as proof theories which can prove subsets of conservative extensions of that theory. Predicate definitions are conservative extensions; queries are theorems to be derived; and solutions are the completely deterministic derivations of the queries which are defined by the programming systems. Logical semantics is not discussed in any depth in Voda's work. The traditional truth-functional semantics, in which individual sentences are assigned truth values  CHAPTER 2. RESEARCH BACKGROUND  9  based on their constituent subformulae, suffices. What computer scientists often refer to as "semantics" - that is, the flow of data and control in a computation - is absorbed into the proof theory and ceases to be a semantic issue at all. No lattice theory is needed because the concepts of program, query, and solution are completely proof-theoretic; no procedural semantics is needed because the proof theory is deterministic and completely describes the computation. The domain of the fixpoint semantics, in most treatments, is the set of constant symbols which appear in the program. The program is in this sense like a database which specifies all the objects known about in the theory. In the Theory of Pairs, on the other hand, the domain is the set of terms generated by the 0-ary generator 0 and the binary generator [—,— ] of pairing. These pairs correspond to the S-expressions of Lisp. The constant symbols can then be defined as being equivalent to specific pairs. The present thesis builds on Voda's concepts of semantics by expressing the Theory of Pairs as the basis for a family of non-deterministic natural deduction proof theories. It presents on the one hand the natural deduction semantics corresponding to that family, and on the other hand a deterministic proof theory which is sound with respect to the semantics, and which proves a large subset of the theorems of that family.  CHAPTER 2. RESEARCH BACKGROUND  2.4  10  Negation in Logic Programming  Van Emden and Kowalski's original conception of a logic program was as a set of Horn clauses to which some variant of resolution or Modus Ponens could be applied [vEK76]. This restriction to Horn clauses has been recognized, at least since [Cla78], as being insufficient to express all databases of formulae of first-order logic. Accordingly, most Prolog systems have retained a Horn clause-like syntax but have moved outside the domain of Horn clauses by adding some ability to negate a formula. This negation is generally computed by the inference rules collectively called "negation as failure" by Clark [Cla78]. If a formula A is not true under any variable substitution, the formula ->A is inferred to be true. The main problem with this approach is that if the formula A is true under some non-null variable substitution, nothing can be said about the formula ->A. Only in the case of a null substitution can ->A safely be inferred to be false. This logical pitfall was apparently not avoided by many Prolog implementations. In some systems bindings occurring within negations are not retracted when other clauses using the same variables are computed. In others, the bindings are retracted but the negated goal is considered to have failed; the effect is that by finding one substitution, the system assumes that all substitutions succeed. Clark recognized the drawbacks of negation as failure. Since he was studying in the  CHAPTER 2. RESEARCH BACKGROUND  11  domain of logic databases, his solution was to maintain the restriction of the database (the analogue of a program) to Horn clauses, and to restrict queries to those in which all negative conjuncts contained only variables which had been fully instantiated by other, positive conjuncts. He informally proved the completeness of computations under this restriction. A n alternate solution (expressed within a Lloyd-style theory of logic programming) is to delay the evaluation of any negative conjunct in a goal or predicate body until all the terms in the conjunct are ground; that is, until the computation of other conjuncts has restricted all variables in the conjunct to stand for single terms. Lloyd [Llo84] has proven that this scheme is sound, and some Prolog interpreters such as MU-Prolog [Nai84] have implemented it. Voda's formalism of logic programming, in itself, does not solve the problem of handling of negation. Proof theories such as that involving one-variable environments [Vod86b] contain a version of negation as failure which does not use delayed negation (and therefore is less powerful than IC-Prolog), but which blocks when variable bindings are changed within the negated formula (ensuring soundness). However, recent work by Voda and the author has led to a "precomplete" negation which is significantly more powerful than negation as failure. This result has been achieved in part because of the clarity of the truth-functional semantics of Voda's system. Precomplete negation may be characterized as the computational technique of  CHAPTER 2. RESEARCH  BACKGROUND  12  treating negated identity formulae as constraints to be retained as variable bindings are retained, and of using those constraints to compute whether given additional bindings or constraints can successfully be added. As presented here, negated formulae are solved by pushing the negation down through the formula by De Morgan's laws. When the negation reaches an equality subformula, an algorithm (similar to but more general than unification) is used which solves for equations of the form a / b as well as of the form a = b. Gilmore [Gil86a] uses a similar technique for computing negation over database queries; however, the emphasis there is on the solution of either variable-free queries or queries involving enumeration of a finite domain. Gilmore's theory, being a general set theory, is also able to handle such things as quantification over sets, which is not attempted here. We concentrate, rather, on the details of finding all terms which satisfy recursively-defined predicates over a specific domain, which Gilmore's work does not explore deeply. This method therefore decides almost all positive formulae containing negations. Some formulae it does not decide are of the form A V - i A , in which A contains a reference to a predicate causing infinite computation.  Although the truth value of  each subformula in such a sentence is indeterminate, the entire sentence should be true in a logic with classical excluded middle. Since the language described here does not have such an excluded middle, it is similar to intuitionistic logic, but it might not prove  CHAPTER 2. RESEARCH BACKGROUND  13  the same set of theorems. The system could be made classically complete by letting it decide excluded-middle formulae. Voda argues, however [Vod86a], that decreased completeness is desirable for logic progranaming to avoid inefficient computation, and is in fact needed only for full theorem-proving.  Chapter 3 Environment Theory This chapter gives the formal details of the system we call environment theory. The elementary syntax, that is the linguistic structure of proof-theoretic objects, is described in section 3.1; due to the natural-deduction structure of the system, many of these syntactic elements form the basis of its formal semantics, described in section 3.2. As usual, some naive set theory is assumed in the presentation of the semantics. Section 3.3 presents a proof theory which is complete, in a strong sense, with respect to the semantics. This proof theory is therefore a valuable tool with which to analyze other proof theories. It is used as such in section 3.4, which presents a strong, though not complete, proof theory. It is this latter proof theory, R, which attains a high level of determinism by the use of precomplete negation. The main point of this presentation is to provide some underpinning to the proof theory R, which is implementable as a logic programming system. The structure of all of environment theory is therefore dependant, in a retrograde way, on decisions taken  14  CHAPTER 3. ENVIRONMENT THEORY  15  in the design of R. Rather than interleave a discussion of these design considerations with the discussion of the theory, we have chosen to expound on the primary design in this chapter. In the next chapter we will discuss some important variants that would have arisen from following different paths in the design process, and their relative merits.  3.1  Elementary Syntax  The elementary syntax will be used in both the logical semantics and the proof theory. In classical model theory, a mapping must be defined between model-theoretic and proof-theoretic elements; in the tradition followed here, such a mapping is unnecessary. Many of the concepts here are explained more fully in [Vod86b] and [Gil86b], and are simply summarized here. As the basic syntactic units of our theory, we shall have an infinite set of parameters P i P2,...; an infinite set of predicate names P i , P2,...; the constant symbol 0; and the 5  variable name w. We shall use boldface p, q , r and P , Q , R , possibly subscripted, as meta-variables ranging over parameters and predicate names, respectively. Informally, terms will be built up from the parameters and w, using the pairing function (which builds up data structures) and the projection functions (which take them apart). We follow Voda's one-variable formulation, in which all quantified entities are parts of a single environment, denoted by the variable w. The domain of this  CHAPTER 3. ENVIRONMENT THEORY  16  variable is the terms. However, in the deterministic proof theory R, we will use only terms which belong to the subclass of environments; this subclass will be seen to have some useful properties. While w is called a variable here, it may be more useful to think of it as a distinguished parameter, since it will never fully be within the scope of any quantifier. The projection functions are the symbols h (head) and t (tail).  These functions  correspond to the C A R and C D R functions of Lisp. D e f i n i t i o n 3.1.1 A projection is a (possibly empty) sequence of symbols h and t. We shall use Greek letters as meta-variables ranging over projections.  The empty  projection will be denoted by e. Projections can be concatenated in the manner of character strings; if 7 contains the sequence of symbols represented by a, followed by those represented by /?, then we can say that af3 is identical to 7. D e f i n i t i o n 3.1.2 a is a term iff either 1. a is a parameter, the variable w, or the constant 0; or 2. a is of the form ba, where b is a term; or 3. a is of the form [b, c], where b and c are terms. We shall use boldface lower-case letters a, b, c, possibly subscripted, as meta-variables ranging over terms.  Similarly, we shall use x, y, z, possibly subscripted, as meta-  variables ranging over the terms of the form wa; these terms will be called pointers.  CHAPTER 3. ENVIRONMENT THEORY  17  The functions h and t take apart terms built up by pairing. The effect of these functions can be seen best in the definition of the metatheoretic notion of a part of a term, which we will need in later discssion.  D e f i n i t i o n 3.1.3 For a term a and projection a, part a of a, denoted a / a , is defined as follows. 1. a/e is a; 2. [a,b}/h/3 is a / 0 ; 3. [a,b]/t/? is b//?; 4. Otherwise, a / a is undefined.  The characterization of the terms wa as "pointers" is useful primarily when we think of terms as data structures within computer memory, or as abstract trees (see [Vod86b]). Pointers appearing within a term to be bound to w can be seen as referring to other parts of that term; that is, pointing to the left or right, or to themselves.  D e f i n i t i o n 3.1.4 If, for a term a, a / a = wa, that occurrence of the pointer ma is said to be a self-pointer. If a/ahfi = wcd^i, that pointer is said to point to the right. If a./at(3 = wah^i, that pointer is said to point to the left. (Note: we use the symbol = to mean "is identical to", that is in the sense of metatheoretic or syntactic identity.)  CHAPTER  3.  ENVIRONMENT  D e f i n i t i o n 3.1.5  THEORY  18  A w-term is a term built up by pairing from the term 0 and the  pointers wa.  D e f i n i t i o n 3,1.6  A proper environment is a w-term in which every pointer is either a  self-pointer or points to the right. A n environment is either a proper environment or the term [w, 0], which is often written as fail.  Environments have two very useful properties. For every term a, if w = a then there exists an environment a' such that w = a' [Vod86b]. Thus, for the purposes of computing over terms, it is sufficient to compute over environments. For every environment a, no infinite chain of parts a ,a >-- 1  2  c  a  n  be- constructed  such that a,- = wcc i, unless they are all identical. Proofs about algorithms which t+  compute with environments, such as the Environment Solution Algorithm we shall encounter later, can use this property to prove such things as termination and computational complexity.  D e f i n i t i o n 3.1.7  A is a formula iff either:  1. A is of the form a = b, where a and b are terms; or 2. A is of the form P(a), where a is a term; or 3. A is of the form B V C or B & C , where B and C are formulae. 4. A is of the form - * B , 3 B , or V B , where B is a formula; or  CHAPTER 3. ENVIRONMENT THEORY  19  If A is of one of the first two forms, it is also an atomic formula. If all terms appearing in the formula are w-terms, it is also a w-formula.  We shall use boldface capital letters A , B , C , possibly subscripted, as meta-variables ranging over formulae. Note the absence of quantified variables after the quantifiers 3 and V. Since we are using Voda's one-variable formulation, a quantifier itself can be thought of as generating a new variable to be referred to within its scope. The new variable is the head of the environment w, and the environment outside the scope of the quantifier is referred to as wt within the quantifier.  D e f i n i t i o n 3.1.8 Because what a pointer signifies depends on the formula it appears in, each pointer is actually an alias of some other pointer within a given formula. 1. A n occurrence of a pointer wa is an alias of itself within an atomic formula. 2. If an occurrence of wa is an alias of to/3 within A or B , it is also an alias of w(3 within A & B , A V B , or - i A . 3. If an occurrence of wa is an alias of wt(3 within A , it is an alias of w/3 within 3 A or V A .  Readers may think of the parameters as being free in any formula in which they appear, and the terms wa as being free within the scope of n quantifiers if and only if a  CHAPTER  3. ENVIRONMENT  THEORY  20  begins with n or more t's. But since a formula with such "free variables" will still take on a truth value in the semantics, without substitutions for the free variables, notions of free and bound variables are largely irrelevant. We have the following definitions.  D e f i n i t i o n 3.1.9 A sentence is a formula. (We will use this word when we wish to emphasize the lack of free variables in any well-formed formula.) A signed sentence is a sentence preceded by a + or — sign.  Definition  3.1.10 The complexity of a formula A , comp(A), is the following.  1. The complexity of a = b and P(a) are 0. 2. The complexity of ->A, 3A, and V A are comp(A) + 1. 3. The complexity of A & B is the greater of comp(A) and comp(B). The complexity of a signed sentence ± A is comp(A).  Definition  3.1.11 a{b := c} represents the term a, with all occurrences of the sub-  term b substituted by occurrences of the subterm c (strong substitution). Formally, b{b := c} = c, and if the term being substituted in is not identical to b, then:  1. 0{b := c} = 0 2. [ a i , a ] { b := c} = [a {b 2  x  := c } , a { b :=  3. ah{b := c} = (a{b := c})h  2  c}]  CHAPTER  3.  ENVIRONMENT  THEORY  21  4. a*{b := c} = (a{b := c})t  Strong substitution in a formula, A { b := c } , is defined similarly.  1. (ai - a ) { b := c } = ( a i { b := c } = a { b := c}) 2  2  2. P ( a ) { b := c} = P ( a { b := c}) 3. ( n A ) { b : = c } E n A { b : = c } 4. ( A & B ) { b := c} = A { b := c } & B { b := c } 5.  ( A V B ) { b := c} = A { b := c} & B { b := c}  6. ( 3 A ) { b := c} = 3 A { b := c } 7. ( V A ) { b := c } = V A { b := c }  Note that the last two subcases of strong substitution in a formula do not always adequately handle the renaming of parts of the environment; that is, they make the same mistake with renaming often made in early axiomatic first-order theories. Often, we will want to remedy this by substituting for all aliases of w in a term or formula. We will also want to do so in a contextual manner, with wt being substituted by the tail of the substituting term, and so on. Such a substitution, while achieving the desired semantic intent, will also preserve the form of a term as a w-term or an environment [Vod84].  CHAPTER  3. ENVIRONMENT  THEORY  Definition  3.1.12 The contextual substitution of a term b for w in another term a,  written a(b), or in a formula A , written A ( b ) , is defined as follows.  1. 0(a) = 0 2. [a,b](c) = [a(c),b(c)] 3. wa(w(3) = w/3 a 4. wa(0) = 0 5. ([a,b]) = [a,b] w  6. wha([a, b]) = wa(a) 7. iw£a([a,b]) EE wa(b) 8. (a = b)(c) EE a(c) = b(c) 9. P(a)(b)EEP(a(b)) 10. (-A)(a) EE - A ( a ) 11. ( A & B)(a) EE A(a) & B(a) 12. ( A V B)(a) EE A(a) 13. (3A)(a) EE  V  B(a)  3A(wh,a{wt))  14. (VA)(a) =WA.(wh,a(wt))  22  CHAPTER  3. ENVIRONMENT  THEORY  23  The basic elements of the proof theory will be sequents.  These are defined as  sets, following Smullyan, rather than as Gentzen's purely syntactic entities, in order to simplify the relationships between the syntax and semantics.  D e f i n i t i o n 3.1.13 A sequent is a possibly infinite set of signed sentences with either the + or the — sign. A finite sequent is a sequent with a finite set of elements.  We will often use a notation similar to that of Gentzen to represent sequents. Every sequent S is the union of a set {+Pi, +P , +P3,...} 2  set {—Mi, — M , — M ,...} 2  3  of sentences with a + sign, and a  of sentences with a — sign. We can therefore represent S  uniquely with the notation {M ,M ,M ,... 1  2  3  —• P P , P ,...}. The Greek letters T and u  2  3  A , possibly subscripted, shall be used to represent sequences of (unsigned) sentences; thus, the standard form for a sequent shall be { r —• A } .  D e f i n i t i o n 3.1.14 If P is a predicate name and A is a sentence, then P(u>) +-» A is a predicate definition. We shall refer to a finite set of predicate definitions as a program.  3.2  Formal Semantics  The model-theoretic part of environment theory consists of a definition of a base, that is one assignment of signs to atomic sentences, and rules for constructing the set of sentences entailed by a base. As with the definition of sequent in the last section, much of the formal semantics relies on informal notions of sets and natural numbers.  CHAPTER 3. ENVIRONMENT THEORY  24  This material is derivative of the semantic definitions of [Gil86b], but differs in several important respects.  Bases are restricted to those which satisfy identity over  pairs, which has special properties in addition to those of standard identity. The quantifiers take the one-variable interpretation described informally in the last section. A n d , most important to the structure of the semantics, we will be interested only in bases which are interpretations of a given program n , in the sense that they satisfy a substitutivity criterion derived from IT.  D e f i n i t i o n 3.2.1 A base B is a set of signed atomic sentences such that the following conditions hold. 1. For every atomic sentence A , exactly one of + A and — A is a member of B. (Completeness and atomic excluded middle.) 2. For every atomic sentence A , terms a and b, and parameter p, whenever ± A { p := a} and =pA{p := b} are both in B, — a = b is in B. 3. For all terms a, +a = a is in B.  (This clause and the one preceding define  standard identity.) 4. For all terms a and b, the following signed sentences are in B: (a)  +0 = 0a, 0a = 0  (b) — [a,b] = [a, b]a, —[a,b]a = [a,b] for all nonempty a  CHAPTER  3.  ENVIRONMENT  THEORY  (c)  +[a,b]/i =  a ,+ a =  (d)  +[a,b]t =  b,+b=[a,b]t  25  [a,b]/i  5. For all terms a , b , and c , whenever all of +ah = b , +at = c , and — a = 0) are in B, + a = [ b , c ] is in 8. 6. For all terms a , b , and c , whenever one of —ah — b , — a t = c , or + a = 0) is in B, — a = [ b , c ] is in B. (This clause and the two preceding define the special properties of identity between pairs.)  Bases give the truth value for atomic sentences; the truth value for non-atomic sentences can be derived inductively.  We use the concepts of semantic entailment,  semantic successor, and closure of a base to collect all the semantic consequences of the sentences in a base.  D e f i n i t i o n 3.2.2  We shall say that a set of signed sentences entails another signed  sentence ( { ± A , ± B , . . . } |—• ± C ) in the following cases, assuming that A and B are formulae. 1. Conjunction:  (a) {+A,+B} h + A & B (b) {-A}  h  (c) {-B}  |-> - A & B  - A & B  CHAPTER  3.  ENVIRONMENT  THEORY  26  2. Disjunction: (a) { + A } h (b) { + B }  + A V B h + A v B  (c) { - A , - B } \-> - A  V  B  3. Negation: { ± A } |-* + ->A 4. Existential quantifier: (a) {+A([a,ui])}|- + 3 A where a is some term (b) { - A ( [ a  1 ) W  ] ) , - A ( [ a , «;]),•••} 2  h  - 3A  where a i , a , . . . is the enumeration of all the terms 2  5. Universal quantifier: (a) { + A ( [ , « ; ] ) , + A ( [ a , u ; ] ) , . . . } 2  a i  where a  l5  |- + V A  a , . . . is the enumeration of all the terms 2  (b) { - A ( [ a , « , ] ) } h - V A where a is some term  D e f i n i t i o n 3.2.3 The semantic successor of a set of signed sentences S, succ(S), is the set of signed sentences a for which either a G S, or there exists a subset T of S  CHAPTER  3. ENVIRONMENT  THEORY  such that T \-* o. We define the n  th  as follows: succ°(S)  27  semantic successor of 5", succ (S),  is S, and succ (S) n+1  for all n > 0,  n  is  succ(succ (S)). n  D e f i n i t i o n 3.2.4 The closure of a base B, Cl(B), is the union of all the semantic successors of B. That is, a signed sentence is in Cl(B) iff it is in succ (B) for some %  finite i.  D e f i n i t i o n 3.2.5 A base B is an interpretation of a program IT if, for every predicate definition P(u>)  A in IT, and every term a, whenever ± A ( a ) is in C7(B), ± P ( a ) is  in B.  D e f i n i t i o n 3.2.6 A base S is a model of a sequent S (equivalently, S is true in B) iff S D C7(S) ^ 0; that is, if there is a signed sentence o such that o € S and a £ succ*(B) for some t.  D e f i n i t i o n 3.2.7 A sequent S is valid with respect to a program IT iff all interpretations of II are models of S; that is, iff S is true in all interpretations of II.  Note that these definitions of truth and validity obtain precisely because intuitive set theory is used for defining both the model-theoretic notions of base and entailment, and the proof-theoretic notion of sequent.  T h e o r e m 3.2.8 ( C l o s u r e Completeness a n d Consistency) For every base B and every sentence A , exactly one of the signed sentences ± A appears in Cl(B).  CHAPTER  3. ENVIRONMENT  THEORY  28  P r o o f . B y induction on the complexity of A . All atomic sentences (complexity 0) are in B with exactly one sign, and the n  th  semantic successor of B contains all the signed  sentences of complexity n + 1; the semantic entailment rules determine uniquely the sign of each sentence.  •  Bases vary in the assignment of sign to individual atomic sentences, and the assignment of values to parameters and the variable w. The set of interpretations of an individual program is smaller than the set of all bases; the only variability is in the assignment of values to the parameters and w, and the assignment of sign to predicate calls for which the corresponding defining sentence is never computed. For every predicate name P defined by a program II, there is a set of predicate call formulae P ( a ) whose sign must be the same in all interpretations of II.  If the  definition P(u>) <-+ 0 = 0 is in II, for example, + P ( a ) must be in all interpretations of II. However, if the definition P(iu) <-»• P(u>) is in n , then P ( a ) can be given any sign in interpretations of n ; and if P(tt>) «-+ ->P(u;) is in n , then no interpretations of n exist! As we will see, the predicate call formulae whose signs are not determined correspond exactly to those predicate calls whose computation causes a search down an infinite branch of the solution tree; that is, in programming language terms, infinite recursion.  Some complex predicate definitions may result in success for some calls,  failure for some calls, and infinite recursion for others; the first class corresponds to  CHAPTER 3. ENVIRONMENT THEORY  29  formulae assigned a +, the second to formulae assigned a —, and the third to formulae assigned different signs in different bases. Since the sign of some predicate calls is not determined, it may be helpful to imagine the existence of a third truth value, "unknown", represented by the sign ?. Then a truth table with this third sign, for the above definitions of conjunction and disjunction, may be given as follows. Conjunction: ? +  —? —— — — ? ? —? — ] disjunction:  +  +  + — ? + + + + — + — ? ? + ? ? V  These tables illustrate the fact that a formula's sign is determined in all bases if and  only if there is enough information to determine that sign. The sign of both immediate subformulae is not always necessary for this determination, but at least one is. For the purposes of this exposition, it is more useful to assume the existence of only two truth values, because this gives such properties as excluded middle for all formulae, which aid in some proofs. However, readers may find it helpful to relate the material that follows to the formulation with three truth values.  CHAPTER 3. ENVIRONMENT THEORY  3.3  30  Proof theory C : Complete  We present here a complete natural deduction proof theory for the environment theory semantics. This proof theory cannot be used to directly implement a theorem-prover or logic programming system; the high degree of non-determinacy means that there must be additional information about how such things as eigenvalues of existential formulae are searched for. The next section can be seen as an attempt to put more information about implementation details into a proof theory, to make it more deterministic. In fact, this can be seen to be the thrust of much of Voda's recent work. Such a proof theory has the same value as in set theories (see for instance [Gil86b]); that is, it allows one to give a computably verifiable derivation of a valid sequent. It will be used later to prove important properties of the computational proof theory. Although we refer to C as one proof theory, it is in fact a family of proof theories C+IT, which are identical save for the rules dealing with the introduction of formulae including predicates defined in the program II. Axioms are of one of the following forms, for any terms a and b and atomic formula A: 1.  {r,  A  —•  A,  A}  2. { r , [a,b] = [a,b]a ->• A } , {I\ [a,b]a = [a,b] -» A } for nonempty a 3. { r ->• A , 0 a = 0}, { r - * A , 0 =  0a>  CHAPTER  4.  3.  ENVIRONMENT  { r ->• A , [a, b]h = a}, { r  THEORY  —• A , a =  [a, b]h}  5. { r - » A , [a, b]t = b}, { r -> A , b = [a, b]t} 6. { r ^  A,a =  a}  The rules of inference of C+IT, for any program IT, follow.  1. Pairing (a) left: { r , ah = b, at = c - » A , a = 0 } {I\a  = [b,c] —• A}  (b) right: {r,a =  0->  A} { r  A,ah = b} { r -> A , a i -  { r ^  A,a=[b,c]}  2. Identity, left: { r -> A , A { p := a » { r , A { p := b> -> A} {r,a = b  —• A}  3. Conjunction (a) left: { r , A , B —» A } {r, A &  B  —• A }  (b) right: { r ^ {r  A , A >  {r  - • A , A  —» A &  , B }  B }  c}  CHAPTER 3. ENVIRONMENT THEORY  32  4. Disjunction  (a) left: {r, A -»  { r , B -»  A }  {r, A  V  —»•  B  A }  A }  (b) right: {r — • {T  A ,  -»• A ,  A,B}  A  V B }  5. Negation (a) left: {r->  A ,  A}  {r,->A —• A } (b) right: {r, A —> { r ^  A }  A , - A }  6. Existential (a) left: {r,A([p,t»])- A } {r, 3 A  —»• A }  for some parameter p which does not appear in the conclusion (b) right: {r-» A , A ( [ a , u ; ] ) }  { r ^ A,3A} for some term a  CHAPTER 3. ENVIRONMENT THEORY  33  7. Universal (a)  left: {F, A([a,w]) - » A} { r , V A —• A} for some term a  (b) right: {r-.A,A([p,u,])} { r ^ A,VA} for some parameter p which does not appear in the conclusion 8. Predicate introduction (a) left: {r,A(a)-+A} { r , P ( a ) —• A} where the definition P(w) *-* A is in II (b) right: {r->A,A(a)> {r^A,P(a)} where the definition P(tu) «-> A is in II  These rules can all be proved to preserve validity; that is, if the premiss of rule application is a valid sequent, then the conclusion is a valid sequent. We can derive with these rules the intuitive truths that 0 is not equal to any pair:  CHAPTER  3.  ENVIRONMENT  THEORY  34  {Oh = a, Ot = b - » 0 = 0} {0=[a,b] -}  That every term is either 0 or a pair:  {-• ah = ah, a — 0} {-> at = at, a - 0} {a = 0 ->• a = 0} {—• a = \ah,at\,a = 0} And that no term is both 0 and a pair: {a = 0, ah = b, at = c —> a = 0} {a = 0,a = [b,c] ->}  Somewhat longer derivations show that the sequents {[a, b] = [c, d] —• a = c &; b = d} and {a = c & b = d —• [a, b] = [c,d]} are derivable.  T h e o r e m 3.3.1  (Completeness)  If a sequent S is valid with respect to II, then it  is derivable in C with respect to IT using the above rules.  P r o o f . See Appendix A .  T h e o r e m 3.3.2  ( T h i n n i n g ) If S is valid with respect to IT, then so is S U <S".  P r o o f . Assume the premise, that is that S n Cl(B) is nonempty for all interpretations B of II. Then clearly (S U S') D Cl(B) is also nonempty for all such B, and is therefore also valid with respect to IT. •  CHAPTER  3.  ENVIRONMENT  THEORY  35  T h e o r e m 3.3.3 ( C u t ) If S U { + A } and S U { - A } are valid with respect to II, then so is S.  P r o o f . Assume S is not valid with respect to some IT. Then there must exist some B which is an interpretation of II but not a model of S; that is, such that 5 n Cl(B) ^ 0. By the Closure Completeness Theorem (3.2.8), exactly one of — A or + A must be a member of C7(S); therefore, either  S'U+A  or  5 U — A  must have an empty intersection  with B. Contrapositively, if both S U + A and S U — A have non-empty intersections with B, then there is no II with respect to which S is not valid; that is, S is valid.  •  Theorems 3.3.2 (Thinning) and 3.3.3 (Cut) motivate us to add two rules to C to facilitate derivations. These rules are, as shown by the Completeness theorem, not necessary to ensure completeness of C , but have been found to be useful in shortening derivations.  1. Thinning  (a) left: {r,  A  {r  —•  —•  A}  (b) right:  A, A}  CHAPTER 3. ENVIRONMENT THEORY  2.  36  Cut: { r —>• A , A } { r , A —» A } { r - A }  3.4  Proof Theory R: R - M a p l e +  This section presents a proof theory, R, which is similar to the language R - M a p l e , +  described in [Vod86b]. The main differences are that R uses parallel disjunction and precomplete negation, whereas R - M a p l e uses left-to-right sequential disjunction and +  negation as failure. Left-to-right disjunction and negation as failure are two computational techniques which were considered for this proof theory, but were rejected for reasons explained in the next chapter. Again, R is used to refer to a family of proof theories R+IT, where IT is any program. To assist in the proof of validity of R, we will need to prove some preliminary theorems. L e m m a 3.4.1  ( S u b s t i t u t i v i t y ) If {T —• A} is a valid sequent, then so is  { r ( [ p , u ; ] ) - A([p,ui])}. P r o o f . If { r —• A} is an axiom of C , then {r([p, w]) —• A([p, w])} must be of one of the forms {I" - * A ' . O a = 0 } , {V, [a',b'] = [a',b']a - * A'}, {I" -> A ' , [a',b']h = { r ' - » A',[a',b']f = b'},  {r'  A ' , a' = a'},  or { r ' . a ' a = a'  a'},  A ' , a' = 0 } , with  the terms in the indicated identity formulae possibly exchanged. A l l of these are also axioms of C and therefore valid.  CHAPTER 3. ENVIRONMENT THEORY  37  If { r —• A } is not an axiom of C but is valid, then it must have a derivation in C . We can transform the proof tree of {r —• A} into a tree with {j?([p,u;]) —»• A([p,u;])} at the root by first replacing all occurrences of p by occurrences of some other parameter (to preserve the validity of 3-left rule applications), and then replacing all occurrences of w in the tree by occurrences of [p,u>]. Axioms will be transformed into axioms by this transformation, and valid rule applications into valid rule applications. The resulting tree will therefore be a well-formed proof tree of C , and by consistency of C {r([p,if]) ->• A([p,tw])} will be valid. T h e o r e m 3.4.2 (Expansion)  •  If { A —• B} and {B —• A } are both valid, then so  are {... A . . . —• . . . B . . . } and {... B . . . —• . . . A . . . } . That is, so are { A ' —• B'} and {B' —> A'}, where A ' is any formula of which A is a subformula, and B ' is just A ' with the subformula A replaced by the subformula B .  P r o o f . B y induction on the difference in complexity between A and A ' . Let the complexity of A be *. Assume that { A —»• B} and {B —• A } are both valid. Let P(j) be the proposition that { A ' —> B'} and {B' —> A'} are valid, where A ' is any formula of complexity j of which A is a subformula, and B ' is just A ' with an occurrence of A replaced by an occurrence of B . I. j - » = 0. { A ' are trivially valid.  B'} and {B'  A'}, are just { A -> B} and {B - * A } , and so  CHAPTER 3. ENVIRONMENT THEORY  38  II. j — i > 0. Assume that P(j) holds for all % < j < k, and consider P(A; + 1). The complexity of A ' is k + 1, and A must be one of several forms.  1. A ' == C & . . . A  We have the derivation { C , . . . A . . . ->  {C  &  C}  . . . A . . . -> {C  &  { C , . . . A . . . —» . . . B . . . }  C}  {C  . . . A . . .  C &  ... A . . .  Clearly {C —• C} is an axiom, and  &  -> . . .  B...}  ...B...}  {...A...  —•  ...B...,C}  is valid by the  induction assumption and Theorem 3.3.2. The derivation of { B ' —• A ' } is similar, as are the derivations for the case when A ' EE . . . A . . . & C .  2. A ' EE C V . . . A  3. A ' EE  A  ' EE ... A . . . V C . Similar to the cases in (1).  . . . A . . . . In this case { A ' -> B ' } is {-•... A . . . - » • - i . . . B ...}.  We have  the derivation {. . . B . . .  -> . . .  {—• - 1 . . . B . . . . . . . { - . . . . A . . . -+  and since {...  B ... —> . . . A ...}  A...} A...}  -....B...}  is valid by the induction assumption, so is  { A ' - » • B ' } . The derivation of { B ' - » • A ' } is similar.  4. A ' EE 3 . . . A  We have the derivation {• . . A . . . ( [ , U ; ] ) - + . . . B . . . ( [ P , K ; ] ) } {. . . A . . . ( [ p , ] ) - + 3 . . . B . . . } P  W  {3...A...  3...B...}  CHAPTER 3. ENVIRONMENT THEORY  39  and by Lemma 3.4.1 and the induction assumption, . . . B ( [ p , w ] ) . . . } is -valid; therefore so is {A' -> B'}.  {...A([j>,w})...  The  derivation of {B' —• A'} is similar.  5. A ' = V . . . A —  Similar to the cases in (4).  III. Since P(t) is true, and if P(fc) is true then P(/s + 1) is true, P(j) is true for all j > i; therefore, if { A —• B} and {B —• A } are both valid, so are {... and {...  B  C o r o l l a r y 3.4.3  A ...}.  A  B  ...}  •  ( R u l e V a l i d i t y ) If { A -> B}  and {B  -> A } are both valid se-  quents, then the rule  S U { ± . . . A...} SU{±...B...} preserves validity.  P r o o f . Assume that { A —> B} and {B —*• A } are valid. By Theorem 3.4.2, the sequent {qp . . . A . . . , ± . . . B ...}  is valid; by applying the thinning rule of C , we can  show that S U {=F . . . A . . . , ± . . . B . . . }  is also valid. If S U { ± . . . A ...}  is valid, then  by an application of the cut rule of C , we can derive the sequent S U { ± . . . B . . . } ; therefore it is valid as well, and the rule preserves validity. • What the above corollary shows is that if we want to prove that each of the rules of some proof theory preserve validity when they are in the stated form, it suffices to  CHAPTER  3.  ENVIRONMENT  THEORY  40  show that the two related sequents have derivations in proof theory C . Since all of the rule schemes of the proof theory R are of the stated form, we can employ this corollary to great advantage in proving the validity of R.  D e f i n i t i o n 3.4.4  A constraint list is a formula either of the form wot = wa or of the  form ->wa — w{3 & N , where (3 is to the right of a and N is a constraint list.  D e f i n i t i o n 3.4.5  A n environment characterization is a formula either of the form fail  or of the form w = a & N , where a is an environment and N is a constraint list.  In the sequel the symbols E and F stand for environment characterizations. vironment characterizations  En-  are so called because they completely characterize the  values of all the parts of the environment variable w. In the original R - M a p l e lan+  guage, the role of environment characterizations was played by identity formulae of the form w = a. This was sufficient to describe the bindings of the environment parts because negation as failure was used to compute negated formulae; it was not necessary, therefore, to express negative information. It will turn out (see Appendix B) that every conjunction of formulae of the form w — a or ->tu = a is equivalent to a disjunction of environment characterizations, although this disjunction may be infinitely long when expanded. We will use the symbol fail in the same was as in R - M a p l e , to denote the formula +  w = [w,0] (which is not true in any base).  CHAPTER  3.  ENVIRONMENT  D e f i n i t i o n 3.4.6 The De Morgan zation E , written neg(E),  THEORY  negation  41  of a part of an environment characteri-  is a metatheoretic transformation of the formula E , defined  as follows: 1. neg (fail) = w — w 2 . neg(w — a & N ) = ->w = a V n e g r ( N )  3. neg(-<wa = w/3 & N ) = wa = w/3 V neg(N) 4. neg(wa  = wa) = fail  T h e o r e m 3.4.7 The De Morgan negation of any environment characterization is equivalent to - i E ; that is, the sequent {neg(E)  ->E} is valid.  P r o o f . By induction, giving a derivation in C of the above sequent for each clause of the definition of neflr(E). •  D e f i n i t i o n 3.4.8 The quantifier dischargement  of a part of an environment character-  ization E , written rfts(E), is a metatheoretic transformation of the formula E , defined as follows:  1. cfo's(fail) = fail 2 . dis(w = [a,b(wt)\ & N ) = w = b &; dis(N) 3. dis(->wta  = wt/3 & N ) = -nua = w/3 & dis(N)  CHAPTER  3. ENVIRONMENT  THEORY  42  4. dis(-iwha = w@ & N ) = d t ' s ( N ) 5. dis(wta = wta) = wet = wa  T h e o r e m 3.4.9 The quantifier dischargement of any environment characterization is equivalent to 3 E ; that is, the sequent {dis(E) —• 3 E } is valid.  P r o o f . B y induction, giving a derivation in C of the above sequent for each clause of the definition of cfo's(E).  •  We now move to the formal definition of the proof theory R+II.  It is similar  in structure to R - M a p l e , but it uses formula markers in the style of [Vod85]. Two +  markers, up(A) and down(A), are introduced to mark computations descending deeper into the formula tree, and computations returning upward with partial solutions in the form of environment characterizations. These markers can easily be introduced by extending the environment theory semantics to include them, with the entailment rules {A}  |—• up(A) and {A} — (>  down(A), and the appropriate additions to proof theory C . Alternatively, we can consider them as metatheoretic abbreviations for distingushed formulae equivalent to the marked formula A ; for instance, down(A) = (pi = p ) & A , up(A) = (p = p ) & A . x  2  2  We have the following theorem:  T h e o r e m 3.4.10 If p and q are parameters, and { A —* B} and {B —• A } are both  CHAPTER  3.  ENVIRONMENT  THEORY  43  valid sequents, then the rule  5u{±...p = pfcA...} SU{±...q = q & B . . . } preserves validity.  P r o o f . Similar to that of Theorem 3.4.2. This theorem effectively states that we can ignore the markers for the purposes of proving rule validity; that is, that they are truly markers which will have significance only to the flow of control of the computation. While the proof is considered to proceed from axioms to conclusions, the course of the computation is considered to proceed from the bottom of the derivation to the top. We can consider a proof of a sequent of the form {—• 3down(w = [wh, wt] & A(u>h))} to be a query which asks whether there are any bindings for the variable w which will result in the formula A being true. The axioms of R+IT are the sequents of the form 1. {—• 3up(E)}, or of the form 2.  Bup(EvB)}.  The environment characterization E of the axiom is the "solution" to the query (the sequent at the bottom of the proof), in the sense that it can be proven from the computed derivation of {—>  3down(w =  [wh, wt] & A(wh))} that a derivation for  CHAPTER  3.  ENVIRONMENT  44  THEORY  { E —• A } exists. Further solutions can be obtained from an axiom of the second form by computation on the backtrack formula B . The rules of deduction for R+IT follow. Some rules are accompanied by proofs of validity preservation employing Corollary 3.4.3. 1. Downward:  (a) Conjunction ... down(E ... down(E  & A) & B...} & (A & B))...}  Validity preservation: {E, A , B -> A } {E, A , B —> B } {E, A , B -+E}  {E, A , B —> A fc B}  {E, A , B — > • E fe ( AfeB)}  { E fc A , B —> E fe ( AfeB)"J {(E & A ) & B -> E & ( A & B)} {E, A , B -> E} {E, A , B -> A } {E, A , B -> E fe A }  {E, A , B -> B}  {E, A , B —> ( EfeA ) & B } {E, A fe B —> ( E f e A ) fe B } { E & ( A & B ) -> ( E & A ) fe B}  (b) Disjunction {-•... down(Ei & A ) V down(E  & B)...}  {-•... doum(E & ( A V B ) ) . . . } (c) Existential ... 3down((w = [wh, a(wt)} fe N(wt)) fc A ) ...} {-• . . . <foum(E & 3 A ) . . . }  CHAPTER  3.  ENVIRONMENT  THEORY  45  where E is of the form w = a & N Validity preservation: {ty = a, N -> w = a} {w = a, N —»• N} {ty = a, N -> w = a & N} {w = a & N - > u ; =  a&N}  {w = a f c N , A ( b ) - » w = a f c N}  {(w = a fc N ) , A ( b ) -»• A(b)}  {w = a fc N , A(b) - » (w = a fc N ) & A(b)}~ some pairing, identity, and cut rule applications ~{w = a fc N , A(b) -> ((!6 = [bfe, a(bt)] fc N(bt)) fc A(b))} {w = a fc N , A ( b ) - » 3((w = [tyfe,a(w*)] fc N{wt)) fc A)} {w = a fc N , 3 A - » 3((w = \wh,a(wt)] fc N(wt)) fc A)} {(w = a f c N ) & 3 A -»• 3((ty = [wh,a(wt)} fc N(wt)) fc A)} where b = [p, ty] (The proof of the inverse is similar.) (d) Universal {->... E & V^down((w = [wh, a(wt)] & N(wt)) & - . A ) . . . }  {-*  ... down(E & V A ) . . . }  where E is of the form w = a f c N (e) Predicate call [b(wt), {—*• ... 3down((w = a{wt)} & N(tui)) fc A{wh))...} ...doum(E& P(b))...} where P(w)  A is in IT and E = (ty = a & N )  2. Environment Solution: { - » . . . up(B)...} {-•... doum(E & A ) . . . }  CHAPTER  3.  ENVIRONMENT  THEORY  46  where A is of the form a = b or of the form -<a = b, and B is the result of the Environment Solution Algorithm (see appendix B) applied to the formula E & A , and there are no subformulae of the form up(C) in the conclusion.  3. Upward normalization:  {-> ... up(B) V A  ...}  {-• . . . A V u p ( B ) . . . } 4. Failure: (a) Conjunction {—• . . . up(fail)...} {—• . . . up(fail) & A  ...}  (b) Disjunction {—• ...  down(A)...}  {-• ...tip(fail) V A . . . } Validity preservation: {A  fail, A }  { A -> fail V A } {wh = w, wt = 0 —• A , w — 0} {w = [w,0}^~K} {ty = [ty, 0] V A —> A }  (c)  Existential {—> . . . up(fail)...} {-•... 3up(fail)...}  {A -> A }  C H A P T E R 3. E N V I R O N M E N T  THEORY  47  (d) Universal ...E&  V-nup(fail)...}  5. Success, no backtrack:  (a) Conjunction {-• . . . dotim(E & B ) . . . } {-•... up(E) & B . . . } (b) Disjunction {-> . . . « p ( E V B ) . . . } {-•... up(E) V B ...} (c) Existential {-»  ...up(F)...}  {->... 3up(E)...} where F is the quantifier dischargement of E (d) Universal {-• . . . doum(E & G ) . . . } { - » . . . E & V-nup(F)...} where G is the De Morgan negation of the quantifier dischargement of F  6. Success with backtrack:  (a) Conjunction {-> ... down(EfcA ) V ( CfcA ) . . . } {^...up(EvC) & A...}  CHAPTER  3. ENVIRONMENT  48  THEORY  (b) Disjunction ... up(E V ( C V A ) ) . . . } {-> . . . u p ( E v C ) V A . . . } (c) Existential {-> ... up(F V 3 C ) . . . } {-•... 3up(E V C j . . . } where F is the quantifier dischargement of E (d) Universal {->... down(EfeG )feV - . C ...} {-* . . . E & V - n u p ( F V C ) . . . }  where G is the De Morgan negation of the quantifier dischargement of F Validity preservation: {C([p, ])->C([p,u;])} W  {F([p,u>])->F([P,H)}  {-C([p ]),C([p,u;]) ^}  {F([p,u>]) -+ 3F> { V ^ C , F ( [ p , w}) ^ T 3 F }  {V-^C,C([p,H) ->} { V ^ C , C ( [ p , «,]) -> 3F}  >W  {V-.C,(F([p,u;]) V C ( [ p , « ] ) ) -  3F}  {V-.C,(F([p,u;]) vC([p,tt>])) -+3F} { V - C - -.(F([p,u;]) V C ( [ p , ] ) ) , 3 F } {V-.C - » V - i ( F v C ) , 3 F } " E,3F} {E,V-nC - • V - . ( F V C ) , 3 F } {E, V-iC E & V-i(F V C), 3F} W  {E, V-C  {E,-^3F,V^C -^EfeVn(FVC)} { Efe^ 3 F , V-^C - » EfeV ^ ( F V C)} {(Efe- 3 F ) & V--C E & V ^ ( F V C)}  (The proof of the inverse is similar.)  CHAPTER  3.  ENVIRONMENT  49  THEORY  7. Negation: (a) Conjunction {->... down(Efc(^A V ^B))...} {-•... down(E  & -.(A & B))...}  (b) Disjunction {->... down(Efc(-.Afc-.B))...} {-•... dotim(E &  -.(A V B))...}  (c) Double negation {—•... doum(E & A)...} {—* ... down{E»  & -i-iA)...}  (d) Existential {->... down(EfcViA)...} { - » . . . doum(E & -.3A)  ...}  (e) Universal  3-nA)...} {-•...down(E& -iVA)...}  {->... rfown(E fc  (f) Predicate call {->... E & V-*foum((u; = [b(tuf), a(wt)] & N(w*)) & A(wh))...} {-•... doum(E & ^ P ( b ) ) . . . } where P(tu) <-+ A is in II and E = (iu = a fc N)  A brief description of the computation may be in order. A stream of computation "descends" into the formula tree where a down marker appears. If the formula to be processed is a conjunction, the computation descends into the left-hand conjunct; if it  CHAPTER  3.  ENVIRONMENT  THEORY  50  is a disjunction, the computation "splits" into two separate streams, each marked; if it is a quantified formula, the computation moves inside the quantifier; if it is a predicate call, the appropriate predicate body is substituted; and if it is a negated formula, the negation is pushed down farther by De Morgan's laws. When a leaf node in the formula tree (a subformula of the form a = b or -ia = b) is reached, the environment solution algorithm (a generalization of unification) is applied, and the partial solution obtained begins to "ascend" the formula tree again, moving back through any quantifiers it left behind. For simplicity's sake, only one stream of computation is allowed to be ascending at a time, hence the restriction on the environment solution rule. When an stream ascends to the level of a disjunction, the formula is normalized by making and ascending stream the left-hand one. If at any time in its ascent the formula meets a conjunction (whose computation was previously suspended), it descends into the conjunct; otherwise, it ascends all the way to the top level, effectively reporting a solution to the original query. The proof theory R is not fully deterministic, because in any computation there can be several subformulae with down markers, where computation can take place. However, at each down marker, there is only one rule which can possibly apply to that marked subformula. The next chapter describes a fully deterministic proof theory which is equivalent to R. R is precomplete with respect to the given semantics in the following informal sense.  CHAPTER  3. ENVIRONMENT  THEORY  51  For any program IT and most sentences A, if the sequent {—> 3A(wh)} is derivable in C+IT, then the equivalent sequent {—• 3down(w = w & A(wh))} is derivable in R+IT. However, sentences A of the form P(a) V -iP(a), where the definition of P causes computation of P(a) to diverge, do not have this property, although they clearly receive the + sign in all bases. This behaviour of R suggests that it could be equivalent to a proof theory having some restricted form of excluded middle. The excluded middle of intuitionistic theories seems too weak; there are some theorems of R which would not be theorems of an intuitionistic system, such as {—• 3down(w = [wh, wt] & V(wh = 0 V -*wh = 0))  However, we cannot have full classical excluded middle, due to the unprovability in R of the sentences noted above. The search for an equivalent classical-style proof theory could be restated as the search for a reductionist semantics with respect to which R is a consistent and complete proof theory. By "reductionist" we here mean a semantics which assigns truth value to individual atomic sentences, and to non-atomic sentences based solely on the truth values of their constituent subformulae. As we shall see in the next chapter, R, rather than variants of R employing left-to-right disjunction or negation as failure, seems more likely to yield a solution to this search.  Chapter 4 Alternative Formulations In this chapter, we will explore some alternative ways in which the evironment theory of the last chapter could be formulated and presented. These include formulations with a sequential evaluation of disjunction; those with negation as failure rather than precomplete negation; and those designed with greater efficiency and ease of implementation in mind.  4.1  Simulated Parallelism  The computational rules given in the last chapter assume a parallel algorithm. Computation goes on at the down(...)  nodes in the formula tree, and when it reaches a  disjunction, the computation forks; that is, where there was one down(...) subformula there are now two, and computation proceeds at each node. If we are trying to develop a sequential implementation, we have two main choices. We could alter the rules for disjunction so that they are truly sequential, but as dis-  52  CHAPTER  4.  ALTERNATIVE  FORMULATIONS  53  cussed in the next section, this approach has its disadvantages. If we still wish to use the parallel algorithm, however, we could simulate parallel computation by the use of the device known in recursive function theory as dovetailing. A n interpreter (universal function) simulates the evaluation of a program (the Godel number of a partial recursive function) by processing each individual instruction in the program. Similarly, a dovetailing interpreter simulates the evaluation of two or more programs by processing an instruction from each program, then the next instruction from each program, and so on. The dovetailing in an environment-theory computational proof theory could take place on several levels. The highest would be on the level of the operating system; this is basically what a timesharing operating system does all the time. A n intermediate level would be to simulate parallelism within the interpreter, but to retain the rules and data structures of a truly parallel computation. The lowest level would be to express the parallelism in the computational rules. The two higher levels are not interesting from a logical point of view. However, a study of the lowest level provides some useful insights into the issues behind implementations of logic programming. The purpose of the computational "markers" [Vod85] is to incorporate some notion of program control into the formulae being computed, and into the computational rules. To incorporate the flow of control in a dovetailing implementation, we could  CHAPTER  4. ALTERNATIVE  54  FORMULATIONS  augment the markers with an integer indicating the current stage of computation of the subformula. Consider the proof theory R D I , defined as being identical to R except for the following modifications. 1. The marker in the axioms, instead of being of the form up, is of the form up , n  for any n. (We could call this n the marker counter; the markers with counters could be defined with parameters in the same way as the original markers, since we have a denumerable number of parameters.) 2. Similarly, the marker in the conclusion of each rule is of the form down  n  or up , n  for any n . 3. When the marker counter in the conclusion of a rule is n, the marker in the premiss of each rule is of the form down  n+1  or  up . n+1  4. Each rule has the additional condition that the indicated conclusion subformula down (A) n  is the leftmost subformula with the same marker counter as the right-  most marker. We claim that proof theory R D I is complete in the same sense that R is; that is, that RD1+II can prove all sequents of the form {—* 3down(w = [wh, wt] & A)} proven by R+II. Each branch of the computation is executed, one rule application at a time, with the rule applications going from leftmost to rightmost marker and then resuming at the leftmost marker. Of course, in an implementation the marker counters would  CHAPTER  4.  ALTERNATIVE  55  FORMULATIONS  not be necessary; each marker would have an associated data structure which pointed to the next marker to be evaluated. Actually, it is not necessary to execute the branches in parallel at the level of individual rule applications. It suffices to stop an infinite downward sequence of evaluation resulting from a recursive predicate definition. Consider the proof theory RD2, defined as being identical to R except for the following modifications.  1. The marker in the axioms, instead of being of the form up, is of the form up , n  for any n. 2. Similarly, the marker in the conclusion of each rule is of the form down  n  or  up , n  for any n. 3. When the marker counter in the conclusion of a rule is n, the marker in the premiss of each rule is of the form down" or up , n  except in the rules for predicate  evaluation, in which the marker in the premiss of each rule is of the form  down . n+1  4. Each rule has the additional condition that the indicated conclusion subformula down" (A) is the leftmost subformula with the same marker counter as the rightmost marker.  Again, we claim that RD2 is complete in the same sense that R is. It may be possible to increase the granularity of the computation even more, by incorporating  CHAPTER  4.  ALTERNATIVE  FORMULATIONS  56  into the marker information about (for instance) what predicates have been called since the last pause in computation on the branch.  4.2  Sequential Disjunction  Many implementations of logic programming languages use a left-to-right sequential computation of disjunction; that is, if the equivalent of the formula A v B is about to be decided, the computation proceeds by first deciding A , and if all solutions from A lead to failure, by then deciding B . The main reason for this implementation approach is to ensure that the exponential explosion of space required by parallel disjunction does not occur. Other reasons include the inefficiency of implementing disjunctive parallelism on the operating system level, and the difficulty of implementing a sequential simulation of parallelism by dovetailing. Altering our proof theory R so that it uses sequential disjunction is fairly simple. The rule for downward movement into a disjunction would become: ... d o u m ( E & A) V  B...}  {-> ... down(E & ( A V B ) ) . . . } and the rule for failure of one branch of a disjunction would become: {—• ...  down(A)...}  {—• . . . up(fail) V A . . . } These rules would essentially suspend computation of the right-hand disjunct until all solutions from the left-hand disjunct had led to failure.  CHAPTER  4.  ALTERNATIVE  FORMULATIONS  57  But here we run into a semantical question: what is the real meaning of this sequential disjunction? There are several approaches we can take to an answer.  4.2.1  Unchanged Semantics  One approach is to simply retain the old semantics for environment theory. Sequential disjunction can be proven to be sound with respect to the standard model theories; the proofs of soundness of the various resolution strategies which employ it basically do this [Llo84]. Sequential disjunction is not complete with respect to the standard model theories, however. Consider the top-level goal w = a & ( A V B ) .  If A is a predicate with a  definition that goes into infinite recursion, B will never be computed even if we can see intuitively that w = a & B can be proven. We will not get all possible solutions from a sequential disjunction, and in fact we may not get any, even when solutions exist. The same can be said for any formula which contains a disjunction or a call to a predicate which contains a disjunction. This is a significant divergence from the accepted semantics of disjunction, but it can be argued that this lack of completeness is unimportant. As long as we are always proving correct things, and the set of things we can prove is sufficiently large for our purposes, why do we need completeness? O n the other hand, the above argument could be used to question the need for a  CHAPTER  4.  ALTERNATIVE  FORMULATIONS  58  semantics in the first place; if we need only validity but not completeness, then surely our definition of truth can become arbitrarily trivial, mimicking the computation and declaring everything computed to be true as true. But if the standard semantics describes accurately our intuitive notion of truth and meaning, why then must our computer systems implement a significantly reduced notion of truth and meaning? What, in fact, is the notion of truth and meaning implemented by sequential disjunction? Most logic prograrriming theorists have not dealt with this question. Its answer requires modifications to the semantics of the programming system.  4.2.2  Modified Semantics for Disjunction  A first stab at the answer is provided by a modification to the semantics for disjunction. We want the truth value of a disjunction to remain the same for the case when the left-hand disjunct is defined, but to be undefined (in the three-valued logic analogue, to receive the ? sign) when the left-hand disjunct is undefined, regardless of the value of the right-hand disjunct. Let us call this model theory SD, for "sequential disjunction". The entailment rules for the other connectives remain the same. The truth table for disjunction becomes the following. V  +  —  ?  + + + + ? + —  ?  ?  —? 1  (Compare with that in the section on Formal Semantics, above.)  The rules for  CHAPTER  4.  ALTERNATIVE  FORMULATIONS  59  entailment involving disjunction become: {+A}  h + ( A v B )  { - A , ± B } |-> ± ( A V B ) Proof theory C can be modified in a similar manner in order to retain its completeness. But have we acheived completeness for proof theory R? We have for the propositional case, but lose it when we introduce quantifiers. For example, the sequent {—> 3((->wh = 0 & P(w)) V (wh = 0))} is valid in SD due to the validity of the sequent — { *• (->0 = 0 & P([0, w])) V (0 = 0)}, but if we compute with it by the rules for existential quantifier, and the predicate call P(u>) goes into infinite recursion, it will never find the answer - exactly the situation in which we wanted the truth value to be indeterminate. The reason for this discrepancy becomes clearer when we note that the existential quantifier is in some sense an infinite disjunction. 3 A is essentially stating the same thing as A([ai,tw]) V A([a ,iw]) V A ( [ a , to]) V . . . , where a i , a , a , . . . is the enumeration 2  3  2  3  of all the terms and where the disjunction is computed in parallel. We have succeeded in modelling the sequential nature of the explicit, propositional disjunction, but not the sequential algorithm we must employ when computing the implicit disjunction of the quantifiers. If we still want to achieve completeness, it seems we must modify the semantics of the quantifiers as well.  CHAPTER  4.2.3  4.  ALTERNATIVE  FORMULATIONS  60  Modified Semantics for Disjunction and Quantifiers  Unfortunately, when we try to develop a consistent truth definition for the existential quantifier, we run into problems almost immediately. Recall that no formula which contains a disjunction is guaranteed to yield all solutions under sequential disjunction. We can define the truth value of 3 ( A V B) as being the same as the value of 3 A V 3B, and the value of 3 A , where A is an atomic formula, as before. But 3 ( A & B) cannot be defined as easily. Such a sentence will be transformed into some disjunction 3(C V D) by the computation algorithm, and we must know what disjunction it is to define its truth value. In other words, since we cannot use proof-theoretic constructs in the semantics (e.g., by referring to the computability of a formula), it seems we must mimic the computation in the definition of the existential quantifier. The same argument applies for the universal quantifier, since its definition in the Gilmore semantics depends on an infinite conjunction which is transformed to a disjunction in the computation rules.  We can make the following conjecture in fairly  informal language:  C o n j e c t u r e 4.2.1  If M is a semantics of a computational logic which contains the  standard connectives and quantifiers, and P is a deterministic proof theory of that computational logic which uses sequential disjunction, and P is complete with respect  CHAPTER  4. ALTERNATIVE  FORMULATIONS  61  to M , then the definition of truth in M mimics the computations in P. In other words, M is a trivial semantic characterization of the proof theory P.  We cannot, at this point, prove the above conjecture (partly because its language is not sufficiently rigourous). We feel that another promising area for further research will be to express this conjecture more rigorously and prove it. We must make decisions on the design of our logic programming systems based on the proof of this conjecture: do we wish them to be complete only with respect to a trivial semantics, or should we have the goal of making them as complete as possible with respect to the fairly intuitive and well-accepted truth-functional semantics of mathematical logic? We make the second choice, and use parallel disjunction rather than sequential. The fact that parallel disjunction can be sequentially simulated using dovetailing (simulated parallelism) is another factor in favour of making this choice.  4.3  Parallel Conjunction  If the use of left-to-right sequential disjunction creates such a wide gap between proof theory and any non-trivial semantics, why then does the proof theory R use sequential conjunction? The answer lies in what we want to use the proof theory for. In logic programming, we are interested mainly in the use of the proof theory for generating sets of variable bindings which make a query true. We are not necessarily interested in using the proof theory to refute things.  CHAPTER  4. ALTERNATIVE  FORMULATIONS  62  When sequential disjunction is used, the system may not be able to find solutions to a query of the form A V B when solutions to B exist. When sequential conjunction is used, on the other hand, the processing of a query of the form A & B must always result in solutions if they exist, because both A and B must be true in the same base. The system will be unable to prove that a query of the form A & B is unsatisfiable in general, although many unsatisfiable queries will be able to be so proven. Although a parallel conjunction would be desirable, we conclude that it is not necessary. The good reasons for using sequential disjunction - lessening of the exponential explosion of space usage and simplicity of algorithm - also hold in the case of sequential conjunction.  4.4  Negation as Failure  The standard method of computing negation is the general paradigm known as negation as failure [Cla78]. No negation as failure is complete with respect to classical semantics, but certain types have been proved to be sound [Llo84]; indeed, a great deal of recent research has gone into such soundness proofs. In Voda's paper describing environments [Vod86b], the language described uses a version of negation as failure. When a computation moves into a negation, it does so essentially by the following rule: {—•  ...  w  {—»  = a& ...  ->down(w  down(w  = a &: A)...}  = a & ->A)...}  CHAPTER  4.  ALTERNATIVE  FORMULATIONS  63  But if the sentence is then transformed by the computation into an equivalent one of the form w = a & ->u; = b , where b is different from a, the computation blocks. Conditions on the environment are expressed by a single environment equation of the form w = a, and therefore cannot express the conjunctive condition. The analogue in Prolog is the situation when a computation moves into a negated formula without all terms in the formula ground, i.e., assigned a value. If any bindings take place within the evaluation of the formula, the bindings cannot be passed through the negation, or the computation will become unsound, so the computation must block, reporting that the goal formula can be neither proven nor refuted. The method of preference for avoiding this problem is delayed negation; see for instance [CG83]. The computation of a negation is delayed until such time as all the terms in the negated formula have become ground due to results from other conjunctive subgoals. Once all terms are ground, the computation of negation as failure can be proven to be both sound and complete. The obvious difficulty with this approach is that if the negated formula is not part of a conjunction, there are no other conjunctive subgoals to produce values, and thus there is no way to ground the terms in the negated formula. Lloyd [Llo84] ignores this case. However, there is one important situation where it arises consistently; namely, when the universal quantifier is used or simulated. Consider the standard first-order logic formula P(x) & VyQ(x,y). Since Prolog  CHAPTER  4.  ALTERNATIVE  FORMULATIONS  64  has no explicit quantifiers, but only implicit universal quantifiers at the beginnings of predicate definitions, we must express such a formula in a different way if we are to compute it. First we note that the formula is equivalent to P(x) &; - i 3 y - i Q ( x , y), and then note that the only way to obtain an existential quantifier in that position is to define a predicate containing the formula being quantified. Thus, the formula must be computed in Prolog by defining the predicate R by the clause R(x)  : -  -iQ(x,y).  and deciding the goal P(x),-.R(x). Clearly, the body of R is exactly the type of formula which is not decidable by negation as failure. Since this situation arises every time a universal quantifier is encountered, we must conclude that it is not feasible to have full universal quantification in a system with negation as failure. In addition to the conflict with universal quantification, there are difficulties in defining the semantics of negation as failure.  Here we run into many of the same  problems as we did with sequential disjunction.  Let us assume that we want our  negation as failure rule to be complete with respect to the semantics. We want the formula to = a & —ifail to take the same sign as the formula to = a, and the formula to = a & ->to = a to take the sign — (the cases decided by negation as failure). However, we want the formula to = a & ->to = b t o take the sign ? (i.e., to be of undefined truth  CHAPTER  4. ALTERNATIVE  FORMULATIONS  65  value) when w = a •/* w = b, since this is the case negation as failure cannot decide. Again, the truth value of the formula in question depends on the surrounding formulae. But what, then, is the truth value of a formula of the form A & - i B ? It depends on the order of the solutions which are computed from the individual formulae A and B ; that is, it depends on things which we cannot deduce without doing the computation. With either true parallel disjunction, simulated parallel disjunction, or left-to-right sequential disjunction, the order of solutions obtained cannot be predicted. We expect a similar result to that for sequential disjunction will obtain; namely, that negation as failure is a complete procedure only with respect to a trivial semantics.  Chapter 5 Conclusions and Future Work We have shown that the semantics of Voda's Theory of Pairs can be expressed formally by a system similar to Gilmore's natural deduction first-order set theory. Using Voda's technique of describing programming languages as proof theories, we have given a language which can prove a large subset of possible logic programming queries. While not complete with respect to the given semantics, this language is precomplete in some well-defined sense, mainly due to its improved treatment of negation.  To show the  soundness of the language with respect to the semantics, we have used the complete natural deduction proof theory corresponding to the semantics as an effective analytic tool. Future work arising from this study covers a fairly wide area. Theoretically, the goal of studying logic programming formally is to develop improved logic programming languages; it would be desirable to implement the language described here. A n attempt to implement the language may expose inconsistencies in the definition, and may lead  66  CHAPTER  5. CONCLUSIONS  AND  FUTURE  WORK  67  to an improved language which corresponds better to actual computation. This line of research follows along the same path as previous work by Voda: the attempt to describe, in standard logic, the data and control structures used in the interpreter of a programming language. We are not entirely satisfied with our definition of environment characterization and the environment solution algorithm. We feel that a less complex notation may be obtainable, which expresses the negative information of the characterization as compactly as the environment expresses positive information. It would also be nice if the form of environment characterization so obtained had the property that the environment solution algorithm on it terminated on all failures as well as on all successes. The key requirement for an environment characterization, however, is that it can pass outside a quantifier easily, discharging the quantified variable with a minimum of computational effort. The semantic characterizability of left-to-right sequential disjunction and negation as failure is also an interesting area. If we cannot give a semantics with respect to which a language using these techniques is complete, other than a trivial one, any assertion that such a language corresponds to formal logic is considerably weakened. A n analysis of the issues here would seem to demand a formal definition of a semantics, and also definitions of the acceptability and triviality of a semantics. It is not clear at this stage what these definitions would look like.  CHAPTER  5. CONCLUSIONS  AND FUTURE  WORK  68  Finally, we have a strong but, for now, intuitive feeling that there is a connection between logic programming with precomplete negation and such set theories as Gilmore's, with its form of excluded middle. To be able to prove the equivalence of a precomplete logic prograrnming language with some formulation of predicate calculus with restricted excluded middle may be a result of some theoretical importance.  Bibliography [AvE82]  Krzysztof R. Apt and Maarten H . van Emden. Contributions to the theory of logic programming. Journal of the Association  for Computing  Machinery,  29(3):841-862, July 1982. [Bet66]  Evert W . Beth. Foundations 1966.  [CG83]  K . L . Clark and S. Gregory. PARLOG:  of Mathematics.  Harper and Row, New York,  A Parallel Logic Programming  Lan-  guage. Technical Report D O C 83/5, Department of Computing, Imperial College, London, 1983. [Cla78]  Keith L . Clark. Negation York, 1978.  [Fit85]  Melvin Fitting. A Kripke-Kleene semantics for logic programs. Journal of Logic Programming,  as Failure, pages 293-322. Plenum Press, New  4:295-312, 1985.  [Gen69]  Gerhardt Gentzen. The Collected Papers Holland, Amsterdam, 1969.  [Gil86a]  Paul C . Gilmore. Computer Science 504 Course Notes. University of B. C . Department of Computer Science, Vancouver, B . C , 1986.  [Gil86b]  Paul C . Gilmore. Natural deduction based set theories: a new resolution of the old paradoxes. Journal of Symbolic Logic, 51(2):393-411, June 1986.  [HA38]  David Hilbert and W . Ackermann. Springer, Berlin, 1938.  [Kow74]  Robert Kowalski. Predicate logic as programming language. In Information Processing  [Kri75]  74 - Proceedings of the IFIP  of Gerhard  Grundzuge  Gentzen.  der Theoretischen  North-  Logik.  Conference, North-Holland, 1974.  Saul Kripke. Outline of a theory of truth. Journal of Philosophy, 72:690-716, 1975. 69  70  BIBLIOGRAPHY  [Llo84]  John W . Lloyd. Foundations 1984.  [Men64]  Elliott Mendelson. Introduction Princeton, 1964.  [Nai84]  Lee Naish. MU-Prolog 1984.  [Sco75]  Dana Scott.  to Mathematical Logic. D . van Nostrand,  S.ldb Reference Manual.  University of Melbourne,  Combinators and Classes, pages 1-26.  Notes in Computer  Science, Springer-Verlag,  [Smu68]  Raymond M . Smullyan. First-Order  [Sto77]  Joseph E . Stoy.  Programming 1977.  Springer-Verlag, Berlin,  of Logic Programming.  Denotational  Volume 37 of Lecture  1975.  Logic. Springer-Verlag, Berlin, 1968.  Semantics:  The Scott-Strachey  Approach to  Language Theory. The M I T Press, Cambridge, Massachusetts,  [vEK76]  Maarten H . van Emden and Robert A . Kowalski. The semantics of predicate logic as a programming language. Journal of the Association for Computing Machinery, 23(4):733-742, October 1976.  [Vod84]  Paul J. Voda. Theory of Pairs, Part I: Provably Recursive Functions.  Tech-  nical Report 84-25, Department of Computer Science, University of British Columbia, Vancouver, December 1984. [Vod85]  Paul J. Voda. A view of programming languages as symbiosis of meaning and computations. New Generation Computing, 3:71-100, 1985.  [Vod86a] Paul J. Voda. Choices in, and limitations of, logic programming. In Proceedings of the Third International Logic Programming  Conference,  1986.  [Vod86b] Paul J. Voda. Computation of full logic programs using one-variable environments. New  Generation  Computing, 4(2),  1986.  [Vod86c] Paul J. Voda. Precomplete Negation and Universal Quantification. Technical Report 86-9, Department of Computer Science, University of British Columbia, Vancouver, April 1986.  Appendix A Completeness Proof for C In the body of this appendix, we will assume that the proof theory referred to is always the proof theory C described above, augmented by the rules concerning the program IT. That is, "derivability" will mean "derivability in C+II", etc. We will also assume that the signed sentences of the theory can be enumerated with the enumeration 01,0-2,0-3,...  T h e o r e m A . . 1 (Subset) A sequent is derivable if and only if some finite subset of it is derivable.  P r o o f . («—) If a finite subset of a sequent is derivable, we can construct a derivation of the whole sequent by simply augmenting every sequent in the proof by the remainder of the sequent. Clearly this derivation will be correct. (—•) We can construct one finite derivable subset from the derivation of any sequent. For an axiom, the subset is the one or two formulae required to be in it by the definition  71  APPENDIX  A.  COMPLETENESS  PROOF  FOR C  72  of axiom. Assume that for all sequents derivable with n steps, we can build such a subset. Consider any sequent derivable with n + 1 steps. form  Seq  U  Si,... Seq  U  Let the premisses be of the  S , and let the conclusion be of the form Seq n  U  {A}.  Ti,...T are the constructed finite derivable subsets of the premisses, then clearly n  (Ti U . . . U T U { A } ) - (Si U . . . U 5 „ ) is also derivable. n  A finite derivable subset of any derivable sequent can thus be built up by induction.  • D e f i n i t i o n A . . 2 The parameter set of a sequent is the set of all parameters in all the terms appearing in that sequent.  Intuitively, we will prove the completeness of C by proving that any non-derivable sequent must not be valid. We will do this by extending the sequent by the addition of formulae, forming a chain of non-derivable sequents whose union will be the foundation for a base in which the sequent is not true. This chain will be one path through the Ext tree, defined as follows.  D e f i n i t i o n A . . 3 The sets  Ext (Seq) and Chk (Seq), and the formula AtBat (Seq), n  n  n  for any sequent Seq with a finite parameter set, form an infinite trinary tree in which every node n has nodes 3n — 1, 3n, and Sn+1  as children. These constructs can be  If  APPENDIX A. COMPLETENESS PROOF FOR C  73  thought of as the "extensions" of Seq, the "check sets" corresponding to each extension, and the "formula at bat" in each extension. Their definition is mutually recursive.  1. Exti(Seq) is Seq. 2. Chki(Seq) is the empty set, {}. 3. If there are members of Ext (Seq) which are not members of Chk (Seq), n  n  AtBat (Seq) is the earliest such signed sentence in the enumeration sequence n  ai,<72,... Otherwise, AtBat (Seq) is undefined. n  4. For n > 1, if AtBat (Seq) is defined, then for 3n — 1 < m < 3n + 1, Ext (Seq) n  m  is Ext (Seq) U A(Ext (Seq)). A(Ext (Seq)) is defined by the following table. AtBat (Seq) AiExts^Seq)) A{Ext (Seq)) A{Ext {Seq)) + a = [b,c] {+ah= b } {+at = c} {-a = 0} +[b,c] = a n  m  m  n  3n  -a= [b,c]  -[b,c] = a ±a = b (not pairs) +A&B —A & B +AVB -A V B ±-iA +3A -3A +VA -VA ±P(a) Notes: (a)  a", aj,...  3n+1  {—ah = b, — at = c, +a = 0}  {} {+B}  {+A} {-A,-B} {+A,+B} {-A}  {-B} {TA}  {+A([a^w}),+A([a^w}),--'V  a)  {-A([p»u;])}W {+A([p»  {-A([a?,«;]),-A([a?,H),.-.}^  is the enumeration of all the terms generated from the parameter  APPENDIX A. COMPLETENESS PROOF FOR C  74  set of Ext (Seq). n  (b) p (c) A  is a parameter not appearing in Extn(Seq).  n  p  is the definition of predicate P in the program IT; i.e., P(iw)  A  p  is in  n.  5. If AtBatn(Seq) is defined and of the form + V A or — 3 A , then  Chk ^{Seq)... Chk (Seq) are [Chk (Seq) U {AtBat (Seq)}) - MU, where Zn  Sn+1  n  n  MU is the set of all signed sentences in Ext (Seq) of the form  —  n  V B or + 3 A .  6. If AtBatn(Seq) is defined and not of one of the above forms, then  Chk -i(Seq)... Chk i(Seq) are just Chk (Seq) 3n  3n+  7. If AtBatn(Seq) is undefined, then  n  U  {AtBat (Seq)}. n  Ext -i{Seq)... Ext +i(Seq) are identical to 3n  Sn  Ext (Seq), and Chk -i(Seq)... Chk i(Seq) are identical to Chk (Seq). n  3n  3n+  n  T h e o r e m A . . 4 (Tree D e r i v a b i l i t y ) If, for some sequent Seq with a finite parameter set, ExtSn-i(Seq), Ext3n(Seq), and Ext3n+\{Seq) are derivable, then so is Extn(Seq).  P r o o f . The proof is by case analysis on the cases given in the table in definition A..3.  Consider case (4.4), for example.  If Ext2n(Seq) is derivable, then a proof for  Ext (Seq) can be constructed by simply adding a step onto the proof of Ext {Seq). n  2n  The other cases are very similar, except for case (4.6), which we will consider here. In case (4.6), if Ext2 {Seq) is derivable, then by Theorem 1 some finite subset of n  it is derivable. Call this finite subset S. If S is also a subset of Extn{Seq), then by  APPENDIX  A.  COMPLETENESS  PROOF  FOR  C  75  Theorem 1 that is derivable as well. Otherwise, S must be of the form SiU S , where 2  Si is a subset of Ext (Seq), and all the formulae in S are of the form n  2  —  [t/x]A. A  proof for Si U {—(x) A } can be constructed by adding one step for every sentence in S , 2  replacing each by — ( x ) A . But  Si  U  { — ( x ) A } is clearly a subset of  Ext (Seq), which n  is therefore derivable. •  C o r o l l a r y A . . 5 If Extn(Seq) is not derivable, then either  Ext (Seq) or Ext i(Seq) 2n  2n+  is not derivable.  P r o o f . This is just the contrapositive to T h m . A..4. •  C o r o l l a r y A . . 6 If Seq is not derivable, then there is an infinite sequence of integers 7Ti,  7r ,... 2  1.  iTi  such that  is 1,  2 . For all t > 1, 7r,- is either 37r,- — 1, 37r,-, or 27r - + 1, and t  3 . For no i > 1 is Ext (Seq) derivable. Ti  P r o o f . The proof is by induction, using Cor. A..5 in the induction step.  D e f i n i t i o n A . . 7 If then  TT\, 7 r , . . . 2  •  is the sequence mentioned in Cor. A..6 for a sequent Seq,  NDExU(Seq) is Ext {Seq), NDChki(Seq) is Chk^Seq), and NDAtBaU{Seq)  is AtBat^(Seq).  T{  APPENDIX A. COMPLETENESS PROOF FOR C  76  T h e o r e m A..8 ( B a t t i n g O r d e r ) Consider any underivable sequent Seq with a finite parameter set.  If the signed sentence CT, is a member of  NDChkj(Seq), there is a k >  such that  j  NDExtj(Seq) but not of  NDAtBatk(Seq) is  CT,-.  P r o o f . Let S be the set of signed sentences of the form — V A or + 3 A which are beforeCT,-in the enumeration, and let T be the set of signed sentences of all other forms beforeCT,-in the enumeration. Then let m „ , for n > 1, be  \S — NDChk (Seq) \ + i * n  \T — NDChk (Seq)\. For all A; such that NDAtBat (Seq) is before CT,-, we can show n  that  k  rrik > rrik+i- This is because if such an NDAtBatk(Seq) is of the form  TOfc+i will be raj, — 1, and if it is of any other form, most  m k + i  will be at least  —(x)A,  — i and at  — 1.  Let CT,- appear in  NDExtj(Seq), but not in NDChkj(Seq). It will thus appear  in  NDExtk(Seq) for all k >  is  NDAtBatk(Seq). Thus, for all A; >  j.  Now assume that there is no j,  k >  j  such that CT,-  there is some signed sentence before cr,- in  the enumeration which appears in NDExtk(Seq) but not in NDChkk(Seq). We can conclude, since m  n  is decreasing for all k > j, that there is some k at which m  k  is  zero. But the only way that could happen would be if all signed sentences before o",- in the enumeration were in  NDChkk(Seq), in which case NDAtBat (Seq) would have k  to be O i , contradicting our assumption. Therefore there must be some k > j such that  NDAtBat {Seq) is a,-. • k  APPENDIX A. COMPLETENESS PROOF FOR C  C o r o l l a r y A . . 9 If the signed sentence a k such that  o~i appears in any NDExtj(Seq), then there is  NDAtBatk(Seq) is <r,.  P r o o f . For  j > 1, every member of NDChkj(Seq) appears in NDExtj^Seq). If  cr, appears in any smallest  77  NDExtj(Seq), there must be a smallest such j; therefore for that  j, a, is a member of NDExtj(Seq) but not of NDChkj(Seq), and the result  of Theorem 3 holds.  •  With the informal notions about sets that we have been using, we can assert that the "infinite union" of the sequents us call it some  NDExti(Seq) exists. That is, there is a set (let  Ext*(Seq)) such that a signed sentence is in Ext* (Seq) if and only if it is in  NDExti(Seq), for some finite t > 1.  T h e o r e m A..10 ( E x t e n s i o n non-derivability) For any underivable sequent Seq with a finite parameter set,  Proof.  Assume  Ext* (Seq) is not derivable.  Ext* (Seq) is derivable. Then some finite subset of it is deriv-  able. B y our definition of  Ext*(Seq), each member of this subset appears in some  NDExU(Seq). But by our definitions, every must be some  NDExU(Seq) is a subset of NDExt (Seq), so there i+l  NDExtj(Seq) in which every member of this subset appears. This  would make  NDExtj(Seq) derivable as well, contradicting our assumptions about the  formation of  Ext*(Seq). Therefore, Ext*(Seq) cannot be derivable. •  APPENDIX A. COMPLETENESS PROOF FOR C  78  C o r o l l a r y A . . 1 1 Whenever a signed sentence ± A appears in Ext*(Seq), the signed sentence =pA does not also appear.  P r o o f . If it did, Ext* (Seq) would be an axiom, and therefore derivable. •  C o r o l l a r y A . . 1 2 No signed sentence of the form + a = a appears in Ext*(Seq).  P r o o f . If it did, Ext* (Seq) would be an axiom, and therefore derivable. •  C o r o l l a r y A . . 1 3 Whenever the signed sentences —a = b and + A { p := a } appear in Ext*(Seq), the signed sentence — A { p := b } does not also appear.  P r o o f . If it did, the finite subset of Ext*(Seq), { + A { p := a } , — A { p := b } , —a = b } could be derived from the two sequents { + A { p := a } , — A { p := a } } and { + A { p := b } , — A { p := b } } , so Ext*(Seq) would also be derivable. •  D e f i n i t i o n A . . 1 4 $(Seq), which we will prove to be the falsifying interpretation of Seq, is defined as follows. Let us assume, without loss of generality, that the parameter p  0  is a member of the parameter set of Seq. 1. If ± A is in Ext*(Seq) for A of the form a = b or P ( a ) , then T A is in $(Seq). 2. For all terms a , + a = a is in $(Seq). 3. For all terms a and b, the following signed sentences are in $(Seq): (a) +0 = 0a, 0a = 0  APPENDIX  A. COMPLETENESS  PROOF FOR C  79  (b) — [a,b] = [a, b ] a , —[a, b ] a = [a, b] for all nonempty a (c) + [ a , b ] / i = a , + a = [a, b]h  (d) + [ a , b ] t = b , + b = [a,b]t 4. If the parameter set of Ext*(Seq) does not contain all the parameters, then, for all parameters p,- not in that set, the signed sentence +p,- = p is in $(Seq). 0  5. If both ± A { p := a } and + a = b are in $(Seq), then ± A { p := b } is in $(Seq). 6. If both ± A { p := a } and T A { p := b } are in $(Seq), then — a = b is in $(Seq). 7. For all other atomic sentences A , + A is in $(Seq).  T h e o r e m A . . 1 5 ( $ I n t e r p r e t a t i o n ) For any underivable sequent Seq with a finite parameter set, $(Seq) is an interpretation of II.  P r o o f . That all atomic sentences are represented in one sign or another is obvious from clause 6 of the definition of $(Seq). No sentence in the set by virtue of clause 1 is represented with both + and — signs, because by Cor. A . . 11 no sentence is in Ext* (Seq) with both + and — signs. The signed sentence + a = b can enter $(Seq) only if a and b are identical, or if —a = b is in Ext* (Seq)  (in which case by Cor. A..13 not both of ± A { p := a} and  ^ A l p : = b } can be in $(Seq)), or if a is not in the parameter set of Ext*(Seq), or if there is no A such that both ± A { p := a } and T A { p := b } are in $(Seq). In  APPENDIX A. COMPLETENESS PROOF FOR C  all cases where both ± A { p  $(Seq).  80  := a} and =pA{p := b} are in  Ext*(Seq),  - a = b is in  Clearly, the conditions for interpretations of IT on identity sentences are met,  and no sentence can appear with both a -I- and — sign in interpretation of II.  $(Seq),  so  $(Seq)  is an  •  T h e o r e m A..16 ( E x t e n s i o n Completeness) For any underivable sequent Seq whose parameter set is finite,  Ext*(Seq)  is not true in  $(Seq).  P r o o f . This is equivalent to saying that no signed sentence in in the closure of  $(Seq).  signed sentences in  Ext* (Seq)  appears  The proof is by induction on the complexity of individual  Ext*(Seq).  By the definition of $(Seq), if ± A is in Ext* (Seq) for A of the form a = b or P(a), then =fA is in  $(Seq);  not in the closure of  so clearly, all signed sentences in Ext*(Seq) of complexity 0 are  $(Seq).  Assume that all sentences of complexity  k in Ext* (Seq)  a signed sentence of the form ±-iA and of complexity must be in some  NDExti(Seq);  that the formula is in  Ext*(Seq);  k+  are not in the closure. If  1 is in  Ext*(Seq),  therefore by Cor. A..9 there must be some  NDAtBatj(Seq)',  therefore ^ A is in  NDExtj i(Seq) +  then it  j such and thus  therefore by our induction assumption ± A must be in the closure of  $(Seq);  therefore by the semantic successor rules ^ - I A must also be in the closure of  $(Seq);  therefore ±->A cannot be in the closure of  $(Seq).  APPENDIX A. COMPLETENESS PROOF FOR C  81  The other cases for signed sentences a are similar, except for the case where a is of the form + 3 A (or — V A ) , which will be covered here. Every term a which appears in  Ext* (Seq)  earliest  is formed from a finite number of parameters. Therefore, there is some  NDExtk(Seq)  whose parameter set contains all the parameters from which a  is formed. Further, either A: = 1 or So if  o  a  is in  Ext*(Seq),  is an element of  NDAtBatk-i(Seq)  it must be  NDExt^Seq),  NDAtBat (Seq) m  is of the form — 3 A (or + V A ) . for some  it will not be an element of  m > k,  because even if  NDChk (Seq), k  and so  by Theorem A..8, must come "up to bat" again. We therefore must have ± A ( [ a , ters in the parameter set of  w])  in  Ext* (Seq).  =FA([a, w]) in the closure of  $(Seq)  not members of the parameter set of  Ext*(Seq)  for all a formed from parame-  B y our induction assumption, we must have  for all such a. Because all parameters which are  Ext* (Seq)  =F-A([a, w]) must also be in the closure of  are made equivalent to one which is,  $(Seq)  for all terms formed from those pa-  rameters as well; in other words, for all terms a. By the semantic successor rules, we must therefore have — 3 A (+VA) in the closure of  <&(Seq),  and therefore  o is  not in  the closure. By induction, we can therefore say that  Ext*(Seq)  is not true in  $(Seq). •  C o r o l l a r y A . . 1 7 No underivable sequent Seq whose parameter set is finite is true in  $(Seq).  APPENDIX  A.  P r o o f . Since  COMPLETENESS  Ext* (Seq)  PROOF  FOR C  has no intersection with the closure of  of it can have an intersection with the closure either.  Ext*(Seq),  82  $(Seq),  no subset  Seq, however, is a subset of  and therefore cannot be valid with respect to  &(Seq). •  C o r o l l a r y A . . 1 8 (Completeness) Every valid finite sequent is derivable.  Proof.  Consider any underivable finite sequent Seq. The parameter set of Seq  must be finite; therefore, there is a base, $(5ec/), in which it is not true; therefore it is not valid. Conversely, therefore, every valid sequent is derivable. • Cor. A..18 is the main result of this appendix. It tells us that the proof theory C we have developed for environment theory is complete; that is, that every finite sequent which is valid, and therefore desirable to be derived, is in fact derivable.  Appendix B Environment Solution Algorithm D e f i n i t i o n B . . 1 9 A pointer x in an environment a is dereferenced if a / x = x . A n environment a is dereferenced if all pointers it contains are dereferenced; that is, if all pointers either are self-pointers or point to self-pointers.  L e m m a B . . 2 0 There is a terminating algorithm which converts every environment a to an equivalent dereferenced environment a ' .  P r o o f . There are a finite number of undereferenced pointers x in a (pointers such that a / x  x ) . Starting at the rightmost such pointer, at part y of a , set a / y to  a / ( a / y ) . The altered environment will be equivalent to the original, and all pointers in a / y will now point to self-pointers; therefore the number of undereferenced pointers will have been lowered. Repeat with the rightmost undereferenced pointer until the number of such pointers reaches 0.  •  83  APPENDIX  B.  ENVIRONMENT  SOLUTION  ALGORITHM  84  Definition B..21 An equation system is a formula of the form D  x  D  V  2  V . . . V D„,  where each disjunct D,- is of the form w = a,- & C i & C , & ... & Ct,m,ti  (2  a n  d each  conjunct C,^- is of the form b - = c - (an equation conjunct) or b - ^ c, y (an inequality tiJ  t|J  (  t)J  conjunct). Lemma B..22 If, in an equation system, for all equation conjuncts C - of the disjunct tiJ  D„ 1. b y is a pointer x,_y, t|  2. c  ii:i  is a pair [cj^c^-], and  3. each of the pointers x,_ - appears in some c,^, where C , ^ is an equation conjunct, ;  then the disjunct Dj is equivalent to fail; that is, the sequent {—D,} is valid. Proof.  Assume the stated conditions. Let us say that a pointer b - refers to tJ  another pointer b,-,* if b,-,* is a part of c y. Because each b,.* is referred to by some t|  b j, we can easily construct a list of pointers y i , y , . ..y^.+i such that y,it  2  +1  refers to  j/,- for all 1 < t < m,-. Clearly there must be some b,-^- which appears twice in the list. This implies that b - is a proper part of itself; that is, that +bija t>J  = b -, for some t|J  nonempty a, is in any base whose closure contains +D,-. Since this is not allowed by the semantics of pair identity, —D,- must be in the closure of all bases, and D - must t  be equivalent to fail. •  APPENDIX  B. ENVIRONMENT  D e f i n i t i o n B..23  SOLUTION  ALGORITHM  85  The depth of 0 and of all pointers is 0; the depth of a pair is the  greater of the depths of its head and tail. The depth measure of an equation a = b or inequality a ^ b is u , where w is the first transfinite limit ordinal and d is the greater d  of the depths of a and b.  E n v i r o n m e n t S o l u t i o n A l g o r i t h m . The algorithm considers the disjuncts as a linear list. The addition of a disjunct to the end of the list is done in the natural way, by increasing the value of m,-. The conjuncts within each top-level disjunct are also treated as a list, and can be added to or eliminated individually. Throughout, the order of terms in an equality or inequality is disregarded; any reference to (say) an equation of the form a = b can be considered as referring also to equations of the form b = a. 1. Repeat, for all disjuncts D,- not of the form fail, until either one disjunct D,- is such that Cij = x,-^- ^ y - for all 1 < j < m,-, or all disjuncts have been replaced t>J  by fail:  (a) If a,- is not dereferenced, dereference a^. (From lemma B..20 we know that this procedure terminates.) (b) Otherwise, if there is a pointer x a appearing in any C,- y such that a,/x = x t  and a ^ e, then for each such pointer: i. Replace every occurrence of x/? in D,-, for every /?, with 0.  APPENDIX  B. ENVIRONMENT  SOLUTION  86  ALGORITHM  ii. Create a new disjunct which is identical to D,-, except that every occurrence of x in a,- is replaced by an occurrence of [xh, xi]. (This loop terminates because there are a finite number of dangling pointers in the original D,-, and no new dangling pointers are introduced into D,- by the procedure.) (c) Otherwise, if there is any pointer x appearing in any C y such that a,/x EE X , t)  then for each such pointer, replace it by a,/x.  (Since there are a finite  number of pointers in the list of conjuncts, this procedure clearly terminates. After this step, due to the definition of a dereferenced environment, every pointer x in every b,-j or c - points to a self-pointer; that is, a,/x EE X.) t|J  (d) Otherwise, if any conjunct b - = c - of depth measure u> '' fiJ  f>;  di  is such that  hij EE [b£-,b*j-] and c,-,,- EE [c^-,c|y], then for each such conjunct, replace the conjunct by b£ - = c£y and create a new conjunct of the form h*j = c*j. ;  (The depth measure of each new conjunct must be < w^'-'' , so the sum of -1  the depth measures of the equality conjuncts has been decreased by at least w*->  -  2u <i~ .) di  1  (e) Otherwise, if there are any conjuncts of the form 0 = 0, eliminate them. (Each elimination decreases the sum of the equality conjunct depth measures byl.)  APPENDIX  B. ENVIRONMENT  SOLUTION  ALGORITHM  87  (f) Otherwise, if any conjunct is of the form 0 = [c* •,<:*•], replace the entire disjunct by fail. (g) Otherwise, if any conjunct is of the form x = c,_y or its inverse, where c y is t)  either 0 or a pointer to the right of x, then for each such conjunct, replace occurrences of x in D,- by occurrences of c y, and eliminate the original ti  conjunct.  (Due to the fact that all pointers pointed to self-pointers, the  environment remains fully dereferenced, and all pointers in all conjuncts still point to self-pointers. The depths of the other conjuncts have not been changed, but one conjunct has been eliminated, so the sum of the equality conjunct depth measures has been decreased. A t this point in the algorithm, we can assume without loss of generality that every equality conjunct is of the form x = [c£y,c'y].) (h) Otherwise, if every pointer b y in an equality conjunct appears in some c,-^ i(  in an equality conjunct, then by Lemma B..22, replace the entire disjunct by fail. (i) Otherwise, if there are still equality conjuncts in the disjunct, let C y be t)  an equality conjunct such that b, y = x does not appear in any c (  ik  equality conjunct. i. Replace every occurrence of x in a,- with an occurrence of c y. tj  in an  APPENDIX  B. ENVIRONMENT  SOLUTION  ALGORITHM  88  ii. A finite number of pointers in a,- will now point to a self-pointer to the left. For each such pointer y at part a,/z, replace all occurrences of y in a,- by occurrences of z. (This will effectively shift all pointers so that they point to the right.) iii. Eliminate the original conjunct, x = c y. t>  iv. Replace every occurrence of x in the disjunct with an occurrence of a,/x. (These occurrences can only be on the left hand side of conjuncts.) Say that the depth of the original c - was d. The depth measures of some tiJ  conjuncts have been raised to u . d  However, at the next repetition of step 4a,  because all right hand sides are pairs, they will all be split into two conjuncts of depth d — 1. Therefore, a factor of w will have been subtracted from the d  sum of the equality conjunct depth measures, but only a finite number of factors of w  <i_1  will have been introduced. There will therefore have been a  net decrease in the sum of the equality conjunct depth measures. (j) Otherwise, if there are conjuncts of the form [b£j-,b*j-] ^ [c£ •,<:'•], then for each such conjunct, i. Replace the conjunct by b£y ^ c£y. ii. Create a new disjunct which is identical to D * , except that C,-^ is replaced by b{j ^ cjy.  APPENDIX B. ENVIRONMENT SOLUTION ALGORITHM  89  (k) Otherwise, if there are conjuncts of the form 0 ^ 0 or x ^ x, replace the entire disjunct by fail. (1) Otherwise, if there are conjuncts of the form 0 ^ [c£y,c'y], eliminate them. (At this point we can assume without loss of generality that all conjuncts are of the form x,- - ^ c y, where x y is a pointer to a self-pointer in a,-.) >;  t|  t)  (m) Otherwise, if there are conjuncts of the form x y ^ [c£y, c*y], then for each ti  such conjunct: i. Create a new disjunct which is identical to D,-, except that every occurrence of x y is replaced by an occurrence of [x^y/^x^yi]. t|  ii. Replace every occurrence of x y in D,- by an occurrence of 0. t|  iii. Eliminate the original conjunct. (n) Otherwise, there must be conjuncts of the form x,-y ^ 0.  For each such  conjunct, replace all occurrences of x y in D - by occurrences of [x y/i,x y<], ti  t  ti  t|  and eliminate the original conjunct.  2. If all disjuncts are of the form fail, terminate returning fail.  3. Otherwise, if one disjunct D,- is such that a,- is a proper environment and each C,-y is of the form x y ^ y,,y, terminate returning (w — a,- & C,_i & . . . & Q t|  D i V . . . V D,-_i V D,-+i V . . . V D „ .  j m  .) V  APPENDIX B. ENVIRONMENT SOLUTION ALGORITHM  90  End of algorithm.  T h e o r e m B..24  Given an equation system, the environment solution algorithm above  will terminate finding an equivalent equation system of the form (ty = yi & ... & x  m  a & x  x  ^  ^ y ) V B , if and only if there is such an equation system. If such an m  equation system does not exist, the given equation system will be equivalent to fail.  P r o o f . Note the following things about the algorithm. 1. A l l of the clauses contain a condition and an action; the action is performed if and only if the condition holds and none of the conditions in the previous clauses hold. 2. A l l of the actions in all the clauses terminate individually. 3. If the action in clause 1(a) has been performed for a particular disjunct D,-, none of the subsequent clauses will allow its condition to become true again; similarly for clauses 1(b) and 1(c). 4. As long as there are equality conjuncts in a particular disjunct, one of the clauses 1(d) - l(i) will be performed on that disjunct at every repetition of the loop. 5. The action in each of the clauses 1(d) - l(i), when applied to any disjunct D , , causes the sum of the depth measures of the equality conjuncts to decrease; therefore, since the sum of the depth measures is always a countable ordinal, by  APPENDIX  B.  ENVIRONMENT  SOLUTION  ALGORITHM  91  transfinite induction the conditions on all the clauses must not hold after some finite number of repetitions.  6. None of the clauses l(j) - l(n) causes any of the conditions in the previous clauses to become true.  7. The action in each of the clauses l(j) - l(n), when applied to any disjunct D,-, causes the sum of the depth measures of the remaining conjuncts to decrease. Again, by transfinite induction these clauses can be repeated only a finite number of times for each D,-.  From the above points it should be clear that for each disjunct, each clause in step (1) can be applied to it only a finite number of times before it becomes converted to one of the success forms. However, by that time it may have generated more disjuncts at the end of the list. Each original disjunct can generate only a finite number of additional disjuncts by virtue of clause 1(b), because the new disjunct created there will have either fewer dangling pointers, or one pointer will be dangling at a lower level. Similarly, only a finite number of additional disjuncts can be created by virtue of clause l(j), because the new disjunct will have a lower sum of depth measures than the original. problematic clause is clause l(m).  The  APPENDIX B. ENVIRONMENT SOLUTION ALGORITHM  92  Consider the disjunct w = a & (x ^ y & x ^ [y,z] & w = to). When clause l(m) is applied to this disjunct, it will create a new disjunct of the form to = a &  ([xh,xt]  y & [xh, xt] ^ [y, z] & to = to). Clause l(j) will then be applied, converting the new disjunct to the form to = a & ([x/i,x<] ^ y & x / i ^ y & : i o = to) and creating another disjunct. But the new disjunct will be of the same form as the original; therefore an infinite production of new disjuncts will be generated, unless the algorithm terminates due to some other disjunct succeeding. However, note that at each iteration of this creation of disjuncts, the depth of the environment a,- will be increased.  If the entire disjunction has a solution, however,  it must have a solution with an environment of finite depth. Therefore, the infinite iteration of applications of clause l(m) can only take place if the entire equation system has no solution. The algorithm will convert the equation system to an equivalent one of the solution form if such an equivalent form exists; if one does not exist, the equation system will be equivalent to fail, and in that case the algorithm may or may not terminate.  •  Thus, the environment solution algorithm is similar to the rest of the computation algorithm in the following sense. If a sequent containing only + E & a = b or + E &; ->a = b is valid, where E is an environment characterization, then the algorithm will terminate finding an environment characterization F such that {F —> E & a = b} is valid. However, if the sequent is not valid, there is no guarantee that the algorithm  APPENDIX  B. ENVIRONMENT  SOLUTION  ALGORITHM  93  will invariably so conclude. Although this is sufficient for the purposes of this theory, it is not entirely satisfying, since we may be able to describe deterministically the set of all equation systems which fail. In doing so, we will be forced to change the form or use of an environment characterization. We should preserve the property of the environment characterization that it be easy to pass back through a quantifier, and this may not be easy to do.  


Citation Scheme:


Citations by CSL (citeproc-js)

Usage Statistics



Customize your widget with the following options, then copy and paste the code below into the HTML of your page to embed this item in your website.
                            <div id="ubcOpenCollectionsWidgetDisplay">
                            <script id="ubcOpenCollectionsWidget"
                            async >
IIIF logo Our image viewer uses the IIIF 2.0 standard. To load this item in other compatible viewers, use this url:


Related Items