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

A N E N V I R O N M E N T T H E O R Y 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 J A M E S H A R O L D A N D R E W S B.Sc , 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 R E Q U I R E M E N T S F O R T H E D E G R E E O F M A S T E R O F S C I E N C E 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 presenting t h i s thesis i n p a r t i a l f u l f i l m e n t of the requirements for an advanced degree at the University of B r i t i s h Columbia, I agree that the Library s h a l l make i t f r e e l y available for reference and study. I further agree that permission for extensive copying of t h i s thesis for scholarly purposes may be granted by the head of my department or by his or her representatives. I t i s understood that copying or publication of t h i s thesis for f i n a n c i a l gain s h a l l not be allowed without my written permission. Department of CowPuret. QcxetJCE The University of B r i t i s h Columbia 1956 Main Mall Vancouver, Canada V6T 1Y3 Date QdJt, ( 4 / ^ 6 DE-6 (3/81) A b s t r a c t A formal semantics of Voda's Theory of Pairs is given which takes the natural-deduction form of Gilmore's first-order set theory. The complete proof theory corre-sponding 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 v i 1 Introduction 1 2 Research Background 3 2.1 Natural Deduction Semantics and Proof Theories 3 2.2 Truth-Value Gaps 5 2.3 Programming Language Semantics 6 2.4 Negation in Logic Programming 10 3 Environment Theory 14 3.1 Elementary Syntax 15 3.2 Formal Semantics 23 3.3 Proof theory C: Complete 30 3.4 Proof Theory R: R + -Maple 36 4 Alternat ive Formulations 52 4.1 Simulated Parallelism 52 4.2 Sequential Disjunction 56 4.2.1 Unchanged Semantics 57 4.2.2 Modified Semantics for Disjunction 58 4.2.3 Modified Semantics for Disjunction and Quantifiers 60 4.3 Parallel Conjunction 61 4.4 Negation as Failure 62 5 Conclusions and Future Work 66 Bibl iography 69 iii A C o m p l e t e n e s s P r o o f f o r C 71 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 83 iv List of Tables A{Extm{Seq)) 73 v A c k n o w l e d g e m e n t My family, friends, and workmates have all contributed to making these last two years enjoyable and educational. In particular, for interesting and often crucial discus-sions 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 Engi-neering 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 interpreta-tion 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 compu-tations 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 TP . 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 charac-terization 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 Theo-ries 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, ex-pressed 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 formu-lates 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 Kowal-ski [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 transfor-mation 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 Kowal-ski, and the resolution-based proof theory in the style of Apt and van Emden, a "pro-cedural 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 pa-pers ([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 defini-tions 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 10 2.4 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 "nega-tion as failure" by Clark [Cla78]. If a formula A is not true under any variable substi-tution, 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 nega-tion (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 el-ementary 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 discus-sion 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 Pi 5 P2,...; an infinite set of predicate names P i , P2,...; the constant symbol 0; and the 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 distin-guished 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. Definit ion 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. Definition 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. Definition 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. Definit ion 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 THEORY 18 Definition 3.1.5 A w-term is a term built up by pairing from the term 0 and the pointers wa. Definition 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 1,a 2>-- - c a n be- constructed such that a,- = wcc t + i , unless they are all identical. Proofs about algorithms which compute with environments, such as the Environment Solution Algorithm we shall encounter later, can use this property to prove such things as termination and compu-tational complexity. Definit ion 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, 3B, 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. Definit ion 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. Definit ion 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). Definit ion 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 2 ] {b := c} = [ax{b := c},a 2{b := c}] 3. ah{b := c} = (a{b := c})h 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 2 ) {b := c} = (ai{b := c} = a 2 {b := c}) 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. ( VA ) { 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 22 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. w([a,b]) = [a,b] 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) V B(a) 13. (3A)(a) EE 3A(wh,a{wt)) 14. (VA)(a) =WA.(wh,a(wt)) 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. Definition 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, +P2, +P3,...} of sentences with a + sign, and a set {—Mi, — M2, — M3,...} of sentences with a — sign. We can therefore represent S uniquely with the notation {M1,M2,M3,... —• Pu P2, P 3,...}. The Greek letters T and A , possibly subscripted, shall be used to represent sequences of (unsigned) sentences; thus, the standard form for a sequent shall be { r —• A}. Definit ion 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. And, 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. Definition 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 25 (c) + [ a , b ] / i = a , + a = [a ,b ] / i (d) + [ a , b ] t = b , + b = [ a , b ] t 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. Definit ion 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 - A & B (c) {-B} |-> - A & B CHAPTER 3. ENVIRONMENT THEORY 26 2. Disjunction: (a) { + A } h + A V B (b) { + 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 - 3 A where ai , a 2 , . . . is the enumeration of all the terms 5. Universal quantifier: (a) { +A ( [ a i , « ; ] ) , +A ( [ a 2 , u ; ] ) , . . . } | - + V A where a l 5 a 2 , . . . is the enumeration of all the terms (b) { - A ( [ a , « , ] ) } h - V A where a is some term Definit ion 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 27 such that T \-* o. We define the nth semantic successor of 5", succn(S), for all n > 0, as follows: succ°(S) is S, and succn+1(S) is succ(succn(S)). Definition 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. Definition 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. Definition 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. Definition 3.2.7 A sequent S is valid with respect to a program IT iff all interpreta-tions 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 (Closure Completeness and Consistency) For every base B and every sentence A , exactly one of the signed sentences ± A appears in Cl(B). CHAPTER 3. ENVIRONMENT THEORY 2 8 P r o o f . By induction on the complexity of A . All atomic sentences (complexity 0) are in B with exactly one sign, and the nth 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 as-signment 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 corre-spond 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 30 3.3 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 3. ENVIRONMENT THEORY 4 . { r ->• A , [a, b]h = a}, { r —• 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 - c} 2. Identity, left: { r ^ A,a=[b ,c ] } { r -> A , A { p := a » { r , A { p := b> -> A} { r , a = b —• A} 3. Conjunction (a) left: (b) right: { r , A , B —» A } { r , A & B —• A } { r ^ A , A > { r —» A , B } { r - • A , A & B } CHAPTER 3. ENVIRONMENT THEORY 32 4. Disjunction (a) left: (b) right: 5. Negation (a) left: (b) right: 6. Existential (a) left: {r, A -» A } { r , B -» A } {r, A V B —»• A } {r —• A , A , B } { T - » • A , A V B } {r-> A , A } {r , ->A —• A } {r, A —> A } { r ^ A , - A } {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 , 3 A } 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 , V A } 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. Proof. See Appendix A. T h e o r e m 3.3.2 (Thinning) If S is valid with respect to IT, then so is S U <S". Proof. Assume the premise, that is that S n Cl(B) is nonempty for all interpre-tations 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 (Cut) If S U { + A } and S U { - A } are valid with respect to II, then so is S. Proof. 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 —• A } (b) right: { r —• A , A } CHAPTER 3. ENVIRONMENT THEORY 36 2 . Cut: { r —>• A , A } { r , A —» A } { r - A } 3.4 Proof Theory R: R + -Maple This section presents a proof theory, R, which is similar to the language R + -Maple, described in [Vod86b]. The main differences are that R uses parallel disjunction and precomplete negation, whereas R + -Maple uses left-to-right sequential disjunction and negation as failure. Left-to-right disjunction and negation as failure are two compu-tational 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 (Substitutivity) If {T —• A} is a valid sequent, then so is { r ( [ p , u ; ] ) - A([p,ui])}. Proof. 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 = a'}, { r ' - » A',[a',b']f = b'}, { r ' A ' , a' = a'}, or { r ' . a ' a = a' A ' , a' = 0 } , with the terms in the indicated identity formulae possibly exchanged. Al 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 . Proof. By 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' B'} and {B' A'}, are just {A -> B} and {B - * A}, and so are trivially valid. 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 . . . —» . . . B . . . } {C & . . . A . . . -> C} {C & . . . A . . . - > . . . B . . . } {C & . . . A . . . C & . . . B . . . } Clearly {C —• C} is an axiom, and { . . . 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 A ' EE ... A ... V C . Similar to the cases in (1). 3. A ' EE . . . A . . . . In this case { A ' -> B ' } is {-•... A . . . - » • - i . . . B ...}. We have the derivation {. . . B . . . -> . . . A . . . } { — • - 1 . . . B . . . . . . . A . . . } { - . . . . A . . . - + - . . . . B . . . } and since {... B ... —> . . . A ...} 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 . . . ( [ P , U ; ] ) - + . . . B . . . ( [ P , K ; ] ) } {. . . A . . . ( [ p , W ] ) - + 3 . . . B . . . } { 3 . . . A . . . 3 . . . B . . . } CHAPTER 3. ENVIRONMENT THEORY 39 and by Lemma 3.4.1 and the induction assumption, {...A([j>,w})... . . .B([p,w]). . . } is -valid; therefore so is {A' -> B'}. 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 {... A B ...} and {... B A ...}. • Corol lary 3.4.3 (Rule Validity) If {A -> B} and {B -> A} are both valid se-quents, then the rule S U { ± . . . A . . . } S U { ± . . . B . . . } preserves validity. Proof. 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. Definition 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. Definit ion 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. En-vironment characterizations are so called because they completely characterize the values of all the parts of the environment variable w. In the original R + -Maple 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 be-cause 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 + -Maple, to denote the formula w = [w,0] (which is not true in any base). CHAPTER 3. ENVIRONMENT THEORY 41 Definit ion 3.4.6 The De Morgan negation of a part of an environment characteri-zation E , written neg(E), is a metatheoretic transformation of the formula E , defined as follows: 1. neg (fail) = w — w 2 . neg(w — a & N ) = ->w = a V negr (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. Proof. By induction, giving a derivation in C of the above sequent for each clause of the definition of neflr(E). • Definit ion 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. Proof. By 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 + -Maple , 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 con-sider them as metatheoretic abbreviations for distingushed formulae equivalent to the marked formula A ; for instance, down(A) = (pi = px) & A , up(A) = (p2 = p2) & A . 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. Proof. 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. B u p ( E v B ) } . 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 THEORY 44 {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 & A) & B. . . } ... down(E & (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 (A fe B)} {E fc A , B —> E fe (A fe B)"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 —> (E fe A ) & B} {E, A fe B —> (Efe 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 & 3A) . . . } 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 = afc 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 = afc 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 = afc N (e) Predicate call {—*• ... 3down((w = [b(wt), a{wt)} & N(tui)) fc A{wh))...} . . . d o u m ( E & P(b)). . . } where P(w) A is in IT and E = (ty = a & N) 2. Environment Solution: { - » . . . u p(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 Vup(B) . . . } 4. Failure: (a) Conjunction (b) Disjunction Validity preservation: {—• . . . up(fail)...} {—• . . . up(fail) & A ...} {—• ... down(A)...} {-• ...tip(fail) V A . . . } {A fail, A} (c) Existential {A -> fail V A} {wh = w, wt = 0 —• A , w — 0} {w = [w,0}^~K} {A -> A} {ty = [ty, 0] V A —> A} {—> . . . up(fail)...} {-•... 3up(fail)...} C H A P T E R 3. E N V I R O N M E N T T H E O R Y 47 (d) Universal 5. Success, no backtrack: . . . E & V-nup(fail)...} (a) Conjunction (b) Disjunction (c) Existential {-• . . . dotim(E & B) . . . } {-•... up(E) & B. . . } {-> . . . « p ( E V B) . . . } {-•... up(E) V B ...} { - » . . .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(E fc A ) V (C fc A ) . . . } { ^ . . . u p ( E v C ) & A . . . } CHAPTER 3. ENVIRONMENT THEORY 4 8 (b) Disjunction (c) Existential ... up(E V (C V A ) ) . . . } {-> . . . u p ( E v C ) V A . . . } {-> ... up(F V 3C). . . } {-•... 3up(E V C j . . . } where F is the quantifier dischargement of E (d) Universal {->... down(E fe G) fe V - . 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 , W ] ) ->C([p ,u ; ] ) } {F([p,u>])->F([P,H)} {-C([p > W]),C([p,u;]) ^} {F([p,u>]) -+ 3F> {V-^C,C([p,H) ->} { V ^ C , F ( [p , w}) ^T3F} {V^C,C([p, «,]) -> 3F} {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,W])),3F} {V-.C - » V-i (FvC ) , 3 F } " {E, V-C E ,3F} {E,V-nC - • V - . (F VC ) ,3F} {E, V-iC E & V-i(F V C), 3F} {E , -^3F ,V^C -^EfeVn(FVC)}  {E fe ^ 3F , V-^C - » E fe V^(F V C)} {(E fe -3F) & V--C E & V^(F V C)} (The proof of the inverse is similar.) CHAPTER 3. ENVIRONMENT THEORY 49 7. Negation: (a) Conjunction {->... down(E fc (^ A V ^ B))...} {-•... down(E & -.(A & B))...} (b) Disjunction {->... down(E fc (-.A fc -.B))...} {-•... dotim(E & -.(A V B))...} (c) Double negation {—•... doum(E & A)...} {—* ... down{E» & -i-iA)...} (d) Existential {->... down(E fc ViA)...} { - » . . . doum(E & -.3A) ...} (e) Universal {->... rfown(E fc 3-nA)...} {-•...down(E& -iVA)...} (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 precom-plete 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. Com-putation 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 imple-mentations 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 FORMULATIONS 54 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 upn, 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 downn or upn, 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 downn+1 or upn+1. 4. Each rule has the additional condition that the indicated conclusion subformula downn(A) 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 FORMULATIONS 5 5 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 indi-vidual 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 upn, for any n. 2. Similarly, the marker in the conclusion of each rule is of the form downn or upn, 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 upn, except in the rules for predicate evaluation, in which the marker in the premiss of each rule is of the form downn+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 right-most 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? On 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 de-scribes accurately our intuitive notion of truth and meaning, why then must our com-puter 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([a2,iw]) V A([a 3 , to]) V . . . , where a i , a 2 , a 3 , . . . is the enumeration 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. ALTERNATIVE FORMULATIONS 60 4.2.3 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 3A, 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 dis-junction in the computation rules. We can make the following conjecture in fairly informal language: Conjecture 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 nec-essary. 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 = a &: A)...} {—» ... down(w = 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) &; - i3y- iQ (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) : - - i Q ( 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 en-countered, 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 ob-tainable, 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 connec-tion 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 of Mathematics. Harper and Row, New York, 1966. [CG83] K. L. Clark and S. Gregory. PARLOG: 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 as Failure, pages 293-322. Plenum Press, New York, 1978. [Fit85] Melvin Fitting. A Kripke-Kleene semantics for logic programs. Journal of Logic Programming, 4:295-312, 1985. [Gen69] Gerhardt Gentzen. The Collected Papers of Gerhard Gentzen. North-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. Grundzuge der Theoretischen Logik. Springer, Berlin, 1938. [Kow74] Robert Kowalski. Predicate logic as programming language. In Information Processing 74 - Proceedings of the IFIP Conference, North-Holland, 1974. [Kri75] Saul Kripke. Outline of a theory of truth. Journal of Philosophy, 72:690-716, 1975. 69 BIBLIOGRAPHY 70 [Llo84] John W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1984. [Men64] Elliott Mendelson. Introduction to Mathematical Logic. D . van Nostrand, Princeton, 1964. [Nai84] Lee Naish. MU-Prolog S.ldb Reference Manual. University of Melbourne, 1984. [Sco75] Dana Scott. Combinators and Classes, pages 1-26. Volume 37 of Lecture Notes in Computer Science, Springer-Verlag, 1975. [Smu68] Raymond M . Smullyan. First-Order Logic. Springer-Verlag, Berlin, 1968. [Sto77] Joseph E . Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. The MIT Press, Cambridge, Massachusetts, 1977. [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 Pro-ceedings of the Third International Logic Programming Conference, 1986. [Vod86b] Paul J. Voda. Computation of full logic programs using one-variable envi-ronments. New Generation Computing, 4(2), 1986. [Vod86c] Paul J. Voda. Precomplete Negation and Universal Quantification. Tech-nical 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. Proof. («—) 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. Let the premisses be of the form Seq U Si,... Seq U Sn, and let the conclusion be of the form Seq U {A}. If Ti,...Tn are the constructed finite derivable subsets of the premisses, then clearly (Ti U . . . U Tn U { A } ) - (Si U . . . U 5„) is also derivable. 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 Extn(Seq) and Chkn(Seq), and the formula AtBatn(Seq), 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 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 Extn(Seq) which are not members of Chkn(Seq), AtBatn(Seq) is the earliest such signed sentence in the enumeration sequence ai,<72,... Otherwise, AtBatn(Seq) is undefined. 4. For n > 1, if AtBatn(Seq) is defined, then for 3n — 1 < m < 3n + 1, Extm(Seq) is Extn(Seq) U A(Extm(Seq)). A(Extm(Seq)) is defined by the following table. AtBatn(Seq) AiExts^Seq)) A{Ext3n(Seq)) A{Ext3n+1{Seq)) + a = [b,c] +[b,c] = a {+ah= b} {+at = c} {-a = 0} -a= [b,c] - [ b , c ] = a {—ah = b, — at = c, +a = 0} ±a = b (not pairs) {} + A & B {+A} {+B} —A & B {-A,-B} + A V B {+A,+B} -A V B {-A} {-B} ±-iA {TA} +3A {+A([a^w}),+A([a^w}),--'Va) - 3 A {-A([p»u;])}W +VA { + A ( [ p » -VA {-A([a?,«;]),-A([a?,H),.-.}^  ± P ( a ) Notes: (a) a", aj,... is the enumeration of all the terms generated from the parameter APPENDIX A. COMPLETENESS PROOF FOR C 74 set of Extn(Seq). (b) p n is a parameter not appearing in Extn(Seq). (c) A 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 +VA or — 3 A , then ChkZn^{Seq)... ChkSn+1(Seq) are [Chkn(Seq) U {AtBatn(Seq)}) - MU, where MU is the set of all signed sentences in Extn(Seq) of the form — V B or + 3 A . 6. If AtBatn(Seq) is defined and not of one of the above forms, then Chk3n-i(Seq)... Chk3n+i(Seq) are just Chkn(Seq) U {AtBatn(Seq)}. 7. If AtBatn(Seq) is undefined, then Ext3n-i{Seq)... ExtSn+i(Seq) are identical to Extn(Seq), and Chk3n-i(Seq)... Chk3n+i(Seq) are identical to Chkn(Seq). T h e o r e m A . . 4 (Tree Derivability) 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). Proof. 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 Extn(Seq) can be constructed by simply adding a step onto the proof of Ext2n{Seq). The other cases are very similar, except for case (4.6), which we will consider here. In case (4.6), if Ext2n{Seq) is derivable, then by Theorem 1 some finite subset of 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 S2, where Si is a subset of Extn(Seq), and all the formulae in S2 are of the form — [ t /x ]A. A proof for Si U {—(x) A } can be constructed by adding one step for every sentence in S2, replacing each by — ( x ) A . But Si U {— ( x )A} is clearly a subset of Extn(Seq), which is therefore derivable. • C o r o l l a r y A . . 5 If Extn(Seq) is not derivable, then either Ext2n(Seq) or Ext2n+i(Seq) is not derivable. P r o o f . This is just the contrapositive to Thm. 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 7 T i , 7 r 2 , . . . such that 1. iTi is 1, 2 . For all t > 1, 7r,- is either 37r,- — 1, 37r,-, or 27rt- + 1, and 3 . For no i > 1 is ExtTi(Seq) derivable. 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 TT\, 7 r 2 , . . . is the sequence mentioned in Cor. A..6 for a sequent Seq, then NDExU(Seq) is ExtT{{Seq), NDChki(Seq) is Chk^Seq), and NDAtBaU{Seq) is AtBat^(Seq). APPENDIX A. COMPLETENESS PROOF FOR C 76 T h e o r e m A..8 (Batt ing Order) Consider any underivable sequent Seq with a finite parameter set. If the signed sentence CT, is a member of NDExtj(Seq) but not of NDChkj(Seq), there is a k > j such that NDAtBatk(Seq) is CT,-. Proof. Let S be the set of signed sentences of the form — V A or +3A which are before CT,- in the enumeration, and let T be the set of signed sentences of all other forms before CT,- in the enumeration. Then let m„, for n > 1, be \S — NDChkn(Seq) \ + i * \T — NDChkn(Seq)\. For all A; such that NDAtBatk(Seq) is before CT,-, we can show that rrik > rrik+i- This is because if such an NDAtBatk(Seq) is of the form —(x)A, TOfc+i will be raj, — 1, and if it is of any other form, m k + i will be at least — i and at most — 1. Let CT,- appear in NDExtj(Seq), but not in NDChkj(Seq). It will thus appear in NDExtk(Seq) for all k > j . Now assume that there is no k > j such that CT,-is NDAtBatk(Seq). Thus, for all A; > j , 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 NDAtBatk(Seq) would have to be O i , contradicting our assumption. Therefore there must be some k > j such that NDAtBatk{Seq) is a,-. • APPENDIX A. COMPLETENESS PROOF FOR C 77 Corol lary A . . 9 If the signed sentence o~i appears in any NDExtj(Seq), then there is a k such that NDAtBatk(Seq) is <r,. Proof. For j > 1, every member of NDChkj(Seq) appears in NDExtj^Seq). If cr, appears in any NDExtj(Seq), there must be a smallest such j; therefore for that smallest 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 NDExti(Seq) exists. That is, there is a set (let us call it Ext*(Seq)) such that a signed sentence is in Ext* (Seq) if and only if it is in some NDExti(Seq), for some finite t > 1. T h e o r e m A..10 (Extension non-derivability) For any underivable sequent Seq with a finite parameter set, Ext* (Seq) is not derivable. Proof. Assume Ext* (Seq) is derivable. Then some finite subset of it is deriv-able. By our definition of Ext*(Seq), each member of this subset appears in some NDExU(Seq). But by our definitions, every NDExU(Seq) is a subset of NDExti+l(Seq), so there must be some 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 . .11 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. .12 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 . .13 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. .14 $(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 0 is in $(Seq). 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 80 all cases where both ±A { p := a} and =pA{p := b} are in Ext*(Seq), - a = b is in $(Seq). Clearly, the conditions for interpretations of IT on identity sentences are met, and no sentence can appear with both a -I- and — sign in $(Seq), so $(Seq) is an interpretation of II. • T h e o r e m A..16 (Extension Completeness) For any underivable sequent Seq whose parameter set is finite, Ext*(Seq) is not true in $(Seq). Proof. This is equivalent to saying that no signed sentence in Ext* (Seq) appears in the closure of $(Seq). The proof is by induction on the complexity of individual signed sentences in 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); so clearly, all signed sentences in Ext*(Seq) of complexity 0 are not in the closure of $(Seq). Assume that all sentences of complexity k in Ext* (Seq) are not in the closure. If a signed sentence of the form ±-iA and of complexity k + 1 is in Ext*(Seq), then it must be in some NDExti(Seq); therefore by Cor. A..9 there must be some j such that the formula is NDAtBatj(Seq)', therefore ^A is in NDExtj+i(Seq) and thus in Ext*(Seq); 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) is formed from a finite number of parameters. Therefore, there is some earliest NDExtk(Seq) whose parameter set contains all the parameters from which a is formed. Further, either A: = 1 or NDAtBatk-i(Seq) is of the form — 3 A (or +VA). So if a is in Ext*(Seq), it must be NDAtBatm(Seq) for some m > k, because even if o is an element of NDExt^Seq), it will not be an element of NDChkk(Seq), and so by Theorem A..8, must come "up to bat" again. We therefore must have ± A ( [ a , w]) in Ext*(Seq) for all a formed from parame-ters in the parameter set of Ext* (Seq). By our induction assumption, we must have =FA([a, w]) in the closure of $(Seq) for all such a. Because all parameters which are not members of the parameter set of Ext* (Seq) are made equivalent to one which is, =F-A([a, w]) must also be in the closure of $(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). • Corol lary A . . 17 No underivable sequent Seq whose parameter set is finite is true in $(Seq). APPENDIX A. COMPLETENESS PROOF FOR C 8 2 Proof. Since Ext* (Seq) has no intersection with the closure of $(Seq), no subset of it can have an intersection with the closure either. Seq, however, is a subset of Ext*(Seq), and therefore cannot be valid with respect to &(Seq). • Corol lary A. .18 (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 . . 19 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 . . 20 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 8 4 Definition B..21 An equation system is a formula of the form D x V D 2 V . . . V D„, where each disjunct D,- is of the form w = a,- & C t i i & C, ( 2 & ... & Ct,m,- a n d each conjunct C,^- is of the form b t i J- = c t | J- (an equation conjunct) or b t ) J- ^ c,(y (an inequality conjunct). Lemma B..22 If, in an equation system, for all equation conjuncts C t i J- of the disjunct D„ 1. bt|y is a pointer x,_y, 2. cii: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 t J - refers to another pointer b,-,* if b,-,* is a part of ct|y. Because each b,.* is referred to by some bitj, we can easily construct a list of pointers y i , y 2 , . ..y^.+i such that y,-+ 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 t>J- is a proper part of itself; that is, that +bija = b t | J-, for some 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 Dt- must be equivalent to fail. • APPENDIX B. ENVIRONMENT SOLUTION ALGORITHM 8 5 Definition B..23 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 ud, where w is the first transfinite limit ordinal and d is the greater of the depths of a and b. Environment Solution 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,-^ - ^ yt>J- for all 1 < j < m,-, or all disjuncts have been replaced 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,-ty such that a,/x = x and a ^ e, then for each such pointer: i. Replace every occurrence of x/? in D,-, for every /?, with 0. APPENDIX B. ENVIRONMENT SOLUTION ALGORITHM 86 ii. Create a new disjunct which is identical to D,-, except that every occur-rence 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 t )y such that a,/x EE X , 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 ct|J- points to a self-pointer; that is, a,/x EE X.) (d) Otherwise, if any conjunct b f i J- = cf>;- of depth measure u> 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^'-''-1, so the sum of the depth measures of the equality conjuncts has been decreased by at least w*-> - 2u di<i~ 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 8 7 (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 ct)y is either 0 or a pointer to the right of x, then for each such conjunct, replace occurrences of x in D,- by occurrences of ctiy, and eliminate the original 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. At 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 bi(y in an equality conjunct appears in some c,-^  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 t )y be an equality conjunct such that b,(y = x does not appear in any cik in an equality conjunct. i . Replace every occurrence of x in a,- with an occurrence of ctjy. 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 = ct>y. 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 ctiJ- was d. The depth measures of some conjuncts have been raised to ud. 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 wd will have been subtracted from the 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 re-placed 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,->;- ^ ct|y, where xt)y is a pointer to a self-pointer in a,-.) (m) Otherwise, if there are conjuncts of the form xtiy ^ [c£y, c*y], then for each such conjunct: i . Create a new disjunct which is identical to D,-, except that every occur-rence of xt|y is replaced by an occurrence of [x^y/^x^yi]. ii. Replace every occurrence of xt|y in D,- by an occurrence of 0. 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 xtiy in D t- by occurrences of [xtiy/i,xt|y<], 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 xt|y ^ y,,y, terminate returning (w — a,- & C,_i & . . . & Q j m . ) V D i V . . . V D,-_i V D,-+i V . . . V D„ . 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 = a & x x ^ y i & . . . & x m ^ y m ) V B , if and only if there is such an equation system. If such an equation system does not exist, the given equation system will be equivalent to fail. Proof. Note the following things about the algorithm. 1. All 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. All 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. The problematic clause is clause l(m). 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 computa-tion 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