Open Collections

UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

The semantics and transformation of imperative programs using horn clauses Ross, Brian James 1988

You don't seem to have a PDF reader installed, try download the pdf

Item Metadata

Download

Media
UBC_1988_A6_7 R63.pdf [ 6.82MB ]
Metadata
JSON: 1.0051940.json
JSON-LD: 1.0051940+ld.json
RDF/XML (Pretty): 1.0051940.xml
RDF/JSON: 1.0051940+rdf.json
Turtle: 1.0051940+rdf-turtle.txt
N-Triples: 1.0051940+rdf-ntriples.txt
Original Record: 1.0051940 +original-record.json
Full Text
1.0051940.txt
Citation
1.0051940.ris

Full Text

THE SEMANTICS AND TRANSFORMATION OF IMPERATIVE PROGRAMS USING HORN CLAUSES By BRIAN JAMES ROSS B.C.Sc., University of Manitoba, 1984 A THESIS SUBMITTED IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF MASTER OF SCIENCE in THE FACULTY OF GRADUATE STUDIES (DEPARTMENT OF COMPUTER SCIENCE) We accept this thesis as conforming to the required standard THE UNIVERSITY OF BRITISH COLUMBIA July 1988 © Brian J. Ross, 1988 In presenting this thesis in partial fulfilment of the requirements for an advanced degree at the University of British Columbia, I agree that the Library shall make it freely available for reference and study. I further agree that permission for extensive copying of this thesis for scholarly purposes may be granted by the head of my department or by his or her representatives. It is understood that copying or publication of this thesis for financial gain shall not be allowed without my written permission. Department The University of British Columbia 1956 Main Mall Vancouver, Canada V6T 1Y3 DE-6(3/81) Abstract The feasibility of using Horn clauses as a means of describing and transforming imperative pro-grams is explored. A logical semantics is derived for a typical imperative language. The style of this semantics permits direct translations between the source language and semantical represen tations. Given the use of Horn clause logic in logic programming, the semantics is particularly useful since models of computation associated with logic programs can be applied to it. Treating the semantics as a logic program means that, in a program transformation context, the semantic representation is particularly well suited to partial evaluation. To support these ideas, an au tomatic translation system has been implemented which permits translation between programs written in an imperative language and their logical equivalents. In addition, a partial evaluator has been written which meta-interprets the logical representation of an imperative program to produce a partially evaluated result. Using predicative programming, this result can be trans lated back into the original source code. Thus the system as a whole performs source-to-source transformations of imperative programs. ii Contents Abstract ii List of Figures v Acknowledgement vii 1 Introduction 1 2 Review 4 2.1 Formal Program Semantics 4 2.1.1 Goals of Program Semantics2.1.2 Logical Semantics 5 2.1.3 Denotational Semantics 8 2.1.4 Operational Semantics 9 2.1.5 Algebraic Semantics2.2 Program Transformation2.3 Partial Evaluation 12 3 An Imperative Language Called Bruce 14 3.1 Design Motivations3.2 Syntax 15 3.3 Operational Semantics 16 4 A Horn Clause Semantics 23 4.1 Design Goals 24.2 Basic Bruce Semantics 5 iii 4.3 Program Branches 30 4.4 Logic Program Interpretation and Completeness 33 4.5 Translating Logic to Bruce 5 4.6 Example Translations 37 5 A Bruce-Logic Translation System 46 5.1 The logic generator 45.2 The Brucifier 52 6 The Partial Evaluation of Bruce Programs 59 6.1 Partial evaluation and program transformation6.2 Implementation 61 6.3 Example transformations 4 7 Discussion 9 7.1 Related work 67.2 Conclusions and further work 72 Bibliography 77 A Partial Evaluator Source 82 B Bruce Parser 89 C Branch Handling 106 D Bruce Generation 117 E Program Printing Utilities 131 F Miscellaneous Code 138 G Binary GCD Basic Semantics 163 H Partially Evaluated Binary GCD Semantics 166 iv List of Figures 3.1 Syntax of expressions 15 3.2 Syntax of higher-level constructs 17 3.3 Definition of Comp 9 3.4 Definition of Buildenv 20 3.5 Example Program . . . 1 3.6 Buildenv Output4.1 Logical semantics of Bruce constructs (no branching) 27 4.2 Branching out of two loops 32 4.3 Converting Branches4.4 Consecutive assignments 7 4.5 While loop 38 4.6 Two alternate Bruce realizations 34.7 Subprogram invocation 9 4.8 Branching within a chain 40 4.9 Bruce equivalent4.10 End of file control scheme (initial) 41 4.11 Logical Form 42 4.12 Derived result 3 4.13 Jumping into a repeat loop 44 4.14 Bruce equivalent 45 5.1 Chain rules 7 5.2 While-loop rule 8 5.3 Branching into two loops 49 v 5.4 Basic semantics 50 5.5 Label program 1 5.6 Label program predicate5.7 Final semantics 53 5.8 Branch out of two loops 4 5.9 Basic semantics5.10 Final semantics 55 5.11 Distributed program predicate 55.12 While loop matching 6 5.13 Derived Bruce program 7 5.14 Derived Bruce program 58 6.1 Partial evaluator 62 6.2 Goal inhibition 63 6.3 Binary powers 5 6.4 Residual programs (n = 5) 66.5 Residual programs (x = 2, n = 5)6.6 Binary gcd (u = 7) 6 6.7 A suspended test 67 6.8 Polyvariant logical result6.9 Polyvariant Bruce result 8 vi j Acknowledgement I owe special thanks to my supervisor, Harvey Abramson. His advice and guidance were directly responsible for the success of this thesis. Thanks are also due to Wolfgang Bibel for his helpful suggestions, and for reading the thesis. I also owe thanks to Paul Voda for directing me to Hehner's work; to Doug Westcott for technical assistance and the use of his lexical analysis code; to Matthew Crocker for helpful discussions and moral support; and to the Department of Computer Science for its financial assistance. Finally, my gratitude to my parents, Jack and Marlene Ross, for their unwavering love and support throughout the years. vii Chapter 1 Introduction An imperative programming language is one whose design is motivated by the architecture of a von Neumann machine [Backus 78]. Such languages typically involve the update of a "state", which is usually taken to be the current state of the machine's memory. The vast majority of computer applications still make predominant use of imperative programming. Engineering and scientific applications rely on the use of FORTRAN. The "C" language has found a niche as a systems programming language, to a large extent replacing assembler language programming. The Pascal language is currently in vogue as a general purpose programming language. Given the widespread existence of imperative programs, there is still a need to explore new techniques of analysis for this class of programs. Predicate logic continues to enjoy extensive use in the verification and transforma tion of imperative-style programs [Loeckx etal. 84] [Hoare 85]. With the advent of logic programming and other computational models for predicate logic there are increased op portunities to apply the logical analysis of programs in semi-automated environments. This thesis explores the feasibility of using Horn clause logic to describe and transform imperative programs. Although declarative logic programming and imperative program ming represent opposite stylistic philosophies, we will demonstrate that logic programming offers interesting possibilities as a tool for analyzing its "imperative ancestor". The motivating principle behind this thesis is that valid logical manipulations of a 1 CHAPTER 1. INTRODUCTION 2 program's logical semantics reflect correctness-preserving transformations of the program's source. In particular, we will show that imperative programs can be economically de scribed in Horn clause logic, and that there exist logically valid transformations of these Horn clause axioms which represent useful program transformations of the source. First, the thesis introduces a new logical semantics for imperative-style programs. Given a cor rect and executable program written in an imperative language, we define for it a logical semantics through the inspection of its syntax. The style of this semantics is most related to ones given by Hehner [Hehner 84a] [Hehner etal. 86], but is somewhat simplified, given its intended use for program transformation. Using the predicative programming paradigm, the logical semantics and source language are intertranslatable. Thus, changes to the log ical representation reflect corresponding changes to the source program. Interpreting the semantics as a logic program means that one specific type of program transformation - par tial evaluation - is particularly suitable, since the semantics can be executed using SLDNF resolution. To support the above argument, we implement an imperative program transformation system. We first define a Horn clause semantics for a generic imperative language. Given an operational semantics for the language defined in terms of an abstract machine, we de fine logical axioms for basic language constructs which describe their operational behavior. The semantics for a program takes the form of a logical theory which describes the complete computational behavior of the program. We prove the feasibility of this semantics by imple menting an automatic translation system which transforms imperative programs into their logical equivalents, and vice versa. We then implement a partial evaluator which, given a logic program representation of a program, meta-interprets it to produce a partially evalu ated result. Using predicative programming, this partially evaluated result is translatable into its imperative equivalent. This implementation as a whole is thus a source-to-source transformation system for imperative programs. Chapter 2 reviews the areas of formal program semantics, program transformation, and partial evaluation - topics all relevant to this thesis. Chapter 3 defines a generic CHAPTER 1. INTRODUCTION 3 imperative language called Bruce. Design motivations for the language are discussed, and the language syntax and operational semantics are presented. Chapter 4 presents a new Horn clause semantics for Bruce. Motivations behind the design of the semantics are discussed. Then the semantics themselves are presented, along with some example translations. An implementation of a Bruce-logic translation system is outlined in chapter 5. A technique for optimizing Bruce programs is presented in chapter 6. An evaluation of the work concludes the thesis in chapter 7. Chapter 2 Review Brief reviews of some areas of computer science relevant to this thesis are now presented. Section 2.1 surveys the field of formal program semantics. Program transformation is discussed in section 2.2. Section 2.3 introduces the concept of partial evaluation. 2.1 Formal Program Semantics 2.1.1 Goals of Program Semantics Programming languages are complex systems. Since conventional programming languages are tailored around the architecture of von Neumann machines, operations in these lan guages are primarily motivated by hardware considerations. The functionality of program segments as they relate to the original problem specification is often not obvious to the programmer. This occurs because people do not normally define problems and solutions in terms of the hardware of a machine, but instead use natural language, mathematics, or some other human-oriented language. The task of computer programming is to convert a human-oriented specification into a machine-oriented programming language. The difference of expressiveness between programs and problem specifications becomes especially relevant when one wants to formally verify the correctness of a program. Formally proving facts about programs is difficult, since there are two levels of formal abstraction being addressed: (1) the program specification language, and (2) the programming lan-4 CHAPTER 2. REVIEW 5 guage itself, which is a formal language. Relating these two formal systems together is the task of formal program semantics, which have been established to allow people to more easily reason about programs and programming languages. Program semantics provide a means of associating programs and programming languages with objects representing their meaning. For example, these objects might be integers representing the input and output of a program module, and the means of deriving facts about the integers might take the form of functions, logical predicates, or algebraic equations. The main point is that any semantic system adopted must allow correct conclusions to be reached about the program being analyzed, and should ideally provide useful calculi with which these conclusions can be derived with the least amount of effort. A number of methodologies exist which differ in both their models of implementation and their intended purposes as tools for program and language analysis. The main semantic models are: (1) logical semantics, (2) denotational semantics, (3) operational semantics, and (4) algebraic semantics. These systems have found uses in the areas of language description and design, and program verification, synthesis, and transformation. Since some semantic methodologies are specialized for particular analytical purposes, not all semantic paradigms are used for the entire aforementioned list of applications. On the other hand, systems such as the denotational semantics have proved to be quite general in their applicability. We now briefly survey the four major semantic methodologies. Since this thesis focuses on the use of logical semantics, the section on this formalism will be emphasized accordingly. For a good comparative discussion of semantics, see [Moss 81]. [Loeckx etal. 84] presents a comprehensive overview, as well as many example applications. 2.1.2 Logical Semantics The term "logical semantics" can easily lead to confusion, as predicate logic has been used in analyzing programs in a variety of different ways. The term has historically come to represent the use of a specialized form of logic known as Hoare logic. However, the CHAPTER 2. REVIEW 6 last decade has seen other applications of predicate logic as a semantic formalism for programming languages and computation. We distinguish three distinct uses of logic in the field of program semantics: (i) Hoare logics and program verification, (ii) the logical description of computation, and (iii) logic programming. Seminal papers by [Floyd 67] [Hoare 69] [Burstall 69] established the utility of first-order predicate logic as a tool for analyzing the behavior of imperative programs. Out of this work, Hoare logics became established as a standard methodology for program verification. [Apt 81] has a comprehensive review of the field, and [Loeckx etal. 84] has example applications. Hoare logic has defined for it a standard set of axioms and inference rules which are common to most imperative languages; new languages must have new axioms and calculi defined for them (for example, [Hoare etal. 73] has a treatment of Pascal). The axioms specify the computational behavior of program constructs under particular conditions, outlining any logical inferences derivable when these conditions are satisfied. Once an axiom set is established for a language, it is applied to a program to formally prove some property of the code. Hoare logic is a major program verification tool. Its predicate logic basis gives it intuitive appeal. It uses a "flatter" domain space than denotational semantics (see be low), the domain typically being variable values, which lends considerable simplicity to users interested in program verification. In addition, work in theorem proving has shown the applicability of Hoare-style logic in semi-automated environments [Manna etal. 77]. However, Hoare logic has been criticized for its often unsound and ad hoc axioms, and dissatisfaction has arisen to the ways in which different program constructs have been han dled [O'Donnell 82]. Hoare logic is also unsuitable in applications requiring more abstract representations of programming languages, and does not address language implementation at all. Whereas Hoare logic is a specialized logic useful in verification, unconstrained first-order predicate logic has found a niche as a general purpose description language for computation and the programming process. One particular paradigm founded in logic CHAPTER 2. REVIEW 7 is predicative programming. Generally speaking, predicative programming is a program ming discipline in which programs are constructed from logical specifications using first-order logic. Bibel established the term in [Bibel 75], and further illustrates the formal synthesis of programs from logical specifications in [Bibel 85]. Hehner uses the term in a similar sense, with the additional perspective that it is possible to freely intersperse con ventional imperative-style program code with logic during program analysis and synthesis if one treats syntactic constructs of a programming language as predicates [Hehner 84a] [Hehner etal. 86]. In his system, each construct in a language has a semantic defined for it which can be (i) composed in first-order predicate calculus, (ii) defined in terms of sub sidiary language constructs, which are likewise logically denned, or (iii) a combination of language constructs and logic. In a mixture of program code and logic, the code portions represent implementable parts of the computation, while the logic represents semantic descriptions. Using predicative programming, the transformation and analysis of code is assured of being logically sound. In addition, predicative programming provides a degree of elegance in merging these two different formal languages into one analytical framework. Hehner defines logical semantics for a typical imperative language in [Hehner 84a] and [Hehner etal. 86]. Examples are given using these semantics in verification and synthesis, as well as illustrating sophisticated aspects of programming. This style of semantics is ex tended in [Hehner 84b] and [Hoare 85] to describe computations which utilize interprocess communication. A key advantage of logic worth mentioning is that it is easily automated. Work in the orem proving has enabled the implementation of program transformation and verification systems. Systems such as those described in [Boyer etal. 79] and [Manna etal. 77] utilize logical semantics as an underlying formalism. Logic programming is an active field of computer science. It is a paradigm which uses Robinson's resolution principle [Robinson 65] to solve programs written as Horn clauses, a subset of first-order predicate logic. A logic program can have many semantic interpreta tions applied to it, namely, a declarative or model theoretic semantics, and a procedural CHAPTER 2. REVIEW 8 or proof theoretic semantics [Clark etal. 81], The programming language Prolog is the current realization of the logic programming ideal [Clocksin etal. 81]. The relevance logic programming has to program semantics is that the statements of a declarative Prolog pro gram can be directly interpreted as statements of logic. This means that there is no need for Hoare-style logics to be applied to the program when analyzing it, since the program's semantics are explicit in the program text. 2.1.3 Denotational Semantics Denotational semantics is a formalism invented by Scott and Strachey (see [Stoy 77] for an introduction). In general terms, denotational semantics refers to the interpretation of the meaning of a program strictly in terms of the meaning of its constituent parts. It is a math ematically founded model of program semantics concerned with the theory of domains, and whose basis language is the lambda calculus. In denotational semantics, the meaning of a program is described in terms of a function from some domain to another. The definition of this function may be in terms of other functions, many of which might have complex domains. The strength of denotational semantics lies in its generality. It has been used to describe many different programming languages, such as Algol-like languages [Gordon 79] and Prolog [Allison 86]. Denotational semantics is arguably more descriptively powerful than semantics based in logic due to the high level of abstraction available. Consequently, it has been used in program verification and transformation [Stoy 77], as well as language description and design [Tennent 77] However, its simplicity has suffered at the sake of generality. Denotational descriptions of languages are often very complicated, suggesting that language description is not necessarily a natural application [Ashcroft etal. 82]. The domains which might be required by a particular language are often too abstract for the programmer trying to prove a simple fact about a program segment. In addition, imple-mentability issues are not dealt with. CHAPTER 2. REVIEW 9 2.1.4 Operational Semantics Operational semantics characterize languages in terms of the machine's behavior when processing them. An operational semantics requires the definition of an abstract machine or interpreter for the language in question. This abstract machine must have incorporated within it precise definitions of behavior for the language constructs. Operational semantics are important in describing programming languages from a design and implementation standpoint, but are typically of less use in program verification and transformation. See [Cook 78], [de Bruin 81], and [Moss 81] for examples of operational definitions of languages. 2.1.5 Algebraic Semantics The latest semantic formalism is algebraic semantics [Guessarian 81]. Algebraic semantics attempts to simplify the semantic notation and analytical calculi of program analysis to its most basic elements. In this scheme, programs are recast into algebraic expressions. Proving program properties is then transformed into proving algebraic problems. For example, to prove the equivalence of two programs, one would define algebraic schemas for the programs, and then through the use of analytical techniques such as induction and term rewriting prove that the program schema are reducible to a common algebraic representation. Algebraic semantics are used in program verification and transformation [Guessarian 81], and synthesis [Broy 84]. 2.2 Program Transformation A comprehensive review of program transformation systems up to 1983 is in [Partsch et al. 83], upon which most of the following discussion is based. We forego mentioning many specific transformation systems in this section, and instead survey the systems most relevant to this thesis in section 2.3. [Pepper 84] also contains a detailed treatment of the field. Software engineering up to now has relied on the programmer's expertise in encoding and debugging. This is a process which has proved error prone, and as a consequence, CHAPTER 2. REVIEW 10 expensive. As a result, much research effort is currently being directed into developing more automated programming environments, and is inspiring coordinated developments in software engineering, artificial intelligence, and programming languages. These automatic programming systems, although still at the experimental stage, will eventually allow reli able programs to be produced with the least amount of technical intervention on the part of the programmer. One key area of automatic programming is program transformation. The term "pro gram transformation" is a general one; it has been used in reference to program transfor mation proper, as well as program synthesis and verification. We use the term to mean the conversion of a program into one which is more efficient or contains some desired quality not found in the original program. Program synthesis, on the other hand, is the creation of a program from a formal specification. Both these applications share much basic method ology, as one can consider the original program given to optimizing transformation systems as the "specification" used by synthesis systems. Program transformation differs from pro gram compilation in that transformations are typically applied at a higher level than the translations done by compilers. The result of a program transformation is usually a pro gram in the same source language exhibiting profound improvements, whereas compilers produce code which is more elementary than the source, and is "peep hole" optimized at best. Two basic approaches to program manipulation are found in transformation systems. The generative approach takes a small kernel of basic program transformation schemas and generates more complex ones from them. These schemas might be implemented as general principles of transformation, as is done in section 2.3, rather than through the use of rules per sae. The catalog approach assumes the existence of a knowledge base of program transformations. This collection of transformations might contain programming and data domain knowledge, language specific features, and efficiency information. An advantage of knowledge-based systems is that they can be upgraded with new rules when necessary. CHAPTER 2. REVIEW 11 An important factor in any transformation system is the type of rule set used, as the types and scope of the transformation rules ultimately determine the power of the system as a whole. The most elementary class of rules are the schematic or pattern replacement ones. They specify local optimizations of a program, such as boolean and algebraic simpli fications. A more powerful class are those which are global. These rules have repercussions on an algorithmic scale, and may specify information dealing with flow analysis and gen eral programming principles. Lastly, there exist rules which are both local and global in applicability, such as fold and unfold transformations [Darlington etal. 73]. The internal representation of programs and rules is also of importance. Some systems rely on formal program semantics as an underlying representation for programs and trans formation rules [Manna etal. 77]. Other systems simply use syntactic representations for programs on which textual "source-to-source" transformations are applied [Loveman 77]. There are philosophical differences between these approaches. Formal approaches are mo tivated by correctness considerations; transformations applied to programs are always as sured of being sound, sometimes at the expense of transformational efficiency. Syntactic approaches, on the other hand, are more intuitionistic and efficient, but are prone to erroneous modifications should a transformation rule be faulty. A reconciliation is in ap proaches founded in algebraic semantics [Broy 84], which simplify the representation of programs and rule sets while maintaining correctness considerations. Different degrees of automation exist in transformation systems. User controlled sys tems give the user the responsibility of applying transformations to a program. The system acts as a repository of powerful editing commands, and does assorted bookkeeping tasks in order to simplify programming. At the other extreme are the fully automated systems. They require the use of heuristics to control the transformation process in order to be practical. Semi-automated systems share features of both these approaches, acting as intelligent editors for the programmer. CHAPTER 2. REVIEW 12 2.3 Partial Evaluation Partial evaluation, or mixed computation, is a computational paradigm which is currently gaining more attention in research in logic and functional programming, as well as conven tional program translation. Partial evaluation can be applied in areas such as program exe cution, program optimization and transformation, compiler generation, compiler-compiler generation, and meta-programming. [Ershov 82] gives an introduction to the concept, and outlines how partial evaluation can be characterized in either a functional or operational fashion. (1) Functionally: given a program P which computes some function f(X, Y), partial evaluation is the process of obtaining a residual program Px which computes the function f(x,Y) = g(Y), where the data value of X is x. Px is also known as the projection of P onto x. (2) Operationally: a program P defines a set C of elementary computations. C itself is partitionable into subsets C U C", where C are called permissible computations, and C" are suspendable computations. Partial evaluation is the process which executes C and forms a residual program P^ which defines the computation C". These two characterizations are generalized in [Ershov 82] [Ershov 85], in which partial evaluation is defined by a mapping: M-.PxD^PxD where P are programs and D are data domains. This mapping can be parameterized by an ordered set {p} in which po and p\ are minimal and maximal values in the set respectively. po represents the case when no data is available to the partial evaluator; p\ is the case when all the data is available. This metric - the availability of data - effectively describes the nature of partial evaluation: depending on the availability of data, some parts of a program can be executed, while other portions which need undefined data values are left as residual results. The most difficult problem faced when partially evaluating a program is controlling the evaluation process. Partial evaluation first requires the fixing of data values , usually CHAPTER 2. REVIEW 13 meaning that program parameters are set. Processing commences by executing all the code in which the necessary data is defined, while retaining the code which uses unknown data values. However, undefined values in a computation escalate during processing according to the data flow in the program: any value which uses an undefined value subsequently becomes undefined, and computations using it become suspendable. Program constructs such as loops thus present the possibility of the infinite generation of residual code. The user is given the responsibility of indicating the halting conditions for a particular application. Most implementations of partial evaluators have been done in either Lisp or Prolog. This is because programs can be treated as data quite naturally within these languages, which is an advantage when implementing meta-programming environments. An early Lisp-based implementation of a partial evaluator is in [Beckman etal. 76], which is used for program optimization. [Futamura 71] first suggested the use of partial evaluation in the creation of compiler-compilers, which are programs that transform interpreters into compilers. [Jones etal. 85] implemented a partial evaluator in Lisp which was used to generate compilers and a compiler-compiler. Two partial evaluators based in Prolog are given in [Venken 85] and [Takeuchi etal. 85]. The Venken system can process full Prolog programs; cuts and system predicates with side-effects are handled. However, control facilities are limited to simply recursion detection and predicate tagging. The Takeuchi system does not handle meta-logical operators such as cut, but has extensive facilities with which the user can control the partial evaluation. Chapter 3 An Imperative Language Called Bruce 3.1 Design Motivations This thesis concentrates on the semantics and transformation of imperative programs, which are those written in languages tailored around the architecture of von Neumann machines [Backus 78]. A von Neumann machine is an abstract simplification of the con ventional computer, having a central processing unit (CPU), a memory or store, and a two-way data bus between them. Imperative languages consequently make predominant use of: (a) variables, which represent values in the store (b) control statements, which are extensions of the CPU's jump and test abilities, and (c) assignment statements, which imitate data passing between the CPU and store. All programs written in imperative lan guages share a fundamental computational methodology based on the above features, and the mappings between different imperative languages are usually trivial. A very general view of a computation on a von Neumann machine is: 1. the computer is initialized with variable values 2. as execution proceeds, the variable values are processed 3. execution eventually terminates with result values in particular variables. 14 CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 15 BoolExpr: b ::= true | false \ r(eu...,ek) | (&i V b2) \ (h A b2) | (->&) where r is a relational operator (eg. <,>,<=, etc.), Expr: e ::= x \c \ f(ex, ...,ek) where x is a variable, c is a constant, / is a function (eg. +, *, /, etc.), Figure 3.1: Syntax of expressions Other side effects usually result during a computation, such as output to a printer or screen, or movement of a robot arm or disk head. However, our view of computation will be restricted solely to the observable effects to the program variable values kept in the store. The rest of this chapter introduces an imperative language called Bruce1. Bruce is intended to be a generic language incorporating many traditional imperative features, such as destructive variable assignments, structured control mechanisms, and subprogram modules. For expository reasons, Bruce also includes branches or goto statements as a more primitive control construct. Although Bruce is by no means as robust as languages such as Pascal or "C", it is sophisticated enough to permit interesting and nontrivial programs to be written in it. In addition, the semantics and transformations we apply to Bruce programs later in this thesis should be easily extended to real programming'languages used in production environments. The definition of Bruce will be in two parts. Section 3.2 outlines the Bruce syntax. This is followed by a presentation of Bruce's operational semantics in section 3.3. This operational semantics will be the basis for the logical semantics introduced in chapter 4. 3.2 Syntax Brian Ross's Unfriendly Computational Environment CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 16 The syntax of Bruce is similar to that of Pascal [Wirth et al. 78] and "C"[Kernighan et al. 78] For the sake of brevity, we forego minute syntactic details in the following definitions with no loss of generality. As a result, labels and constants are assumed to have conventional denotations. Figure 3.1 has a BNF-style grammar indicating the construction of boolean and math ematical expressions. Most common relational and arithmetic operators may be used. We assume that conventional operator bindings are adopted, and that parentheses can be dropped without resulting in interpretive ambiguities. Figure 3.2 has a BNF-style syntax of Bruce programs. Items enclosed in brackets, such as statement labels, are optional. Items with an overbar (as in a) represent lists of items. An environment E contains all the programs to be executed in a particular application, and represents the entire computational environment. A program P is a conventional program or subprogram. A program is denned by a unique program name Prognamei, parameter and local variable definitions, and a program body. Parameters may be variable or call by address parameters (the vector a), or call by value parameters (the vector e). Note that there are no data types in Bruce. A chain Q (also referred to as a train) is a sequence of one or more statements separated by semi-colons. Each statement can be optionally labelled. Finally, a statement S represents a basic Bruce construct. Standard assignments and tests are allowed. Skip commands are null instructions which have no effect whatsoever. Control constructs such as while and repeat loops may be used, as well as more primitive constructs such as branches. Lastly, subprograms can be invoked with call statements, where the first list of parameters are variables to be passed by address, and the second list are expressions to be passed by value. 3.3 Operational Semantics Establishing an operational semantics involves the definition of an abstract machine or interpreter. The style of this operational semantics is based on those in [de Bruin 81] CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 17 Environment: E ::= UP Programs: P ::= Prognamei(a,e) : [local x] { Q } where Progname, and each variable name v £ {a, e,x} is unique in E Chains: Q ::= [Za6e/,:]5 | [label, :] S;Q where each label labeli is unique in E Statements: S ::= skip \ v := e \ if (b) then {Q} else { Q' } | if (b) then {Q} | call Pi(v, e) | while (b) { Q } | repeat { Q } tmii/ (6) | where 6 G BoolExpr,e £ Expr,v £ variable names, Pi £ Programs Figure 3.2: Syntax of higher-level constructs CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 18 and [Cook 78]. This semantics is semi-formal in the sense that mathematical notation is descriptively useful in the operational definitions. However, there is no attempt in utilizing unnecessary rigor in this semantics, as the intent is to illustrate in elementary terms the effects of program statements on the store. We will characterize a computation by its effect on the store, and in particular, the effect on the values of the program variables. A state,cr, is a static representation of the computer store at an instant in time of the computation, and is our basic semantic unit, a is defined as a function which maps program variables to their current values in the domain space Domain: A variant o[e/v] of a state a is a state a' in which a' differs from a only in the mapping of variable v, which is mapped to e. c[e/v] represents the multiple application of a variant to a vector of elements. o~[V(e)/v] represents the multiple application of a variant in which the valuations of e are substituted. A computation sequence, denoted E, is an ordered list of successive states produced during the execution of a program: IC simply returns the final result state of terminating computation sequences. A concate nation operator * will be used to construct computation sequences from other sequences. a : Var —> Domain E =< oi,o2,...,o-k,... > A function fC is denned as: J. if E does not terminate ok if E' =< o~o,...,o~k > If < <7A, ...,<7(, > and < oy, ...,crz > then E1 * E2 = < <70, ...,<7(,,CTV, ...,CT2 > CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 19 1. Comp<E,P, S > <r 2. Comp < E, P, skip > a 3. Comp < E, P, skip; Q » a 4. Comp <E,P, x := e; Q > <r 5. Comp < £, P, ca// P,(t>, e);Q > o-6. Comp<E,P, if(b)then{Qi}else{Q2};Q3> o-7. Comp<E,P, i'/(6)i/ien{Q1};Q2>cr 8. Comp<^E,P, while(b){Qi};Q2 > a 9. Comp < .E1, P, repeat{Qi}until(b); Q2 > a 10. Comp < E, P,goto /<;<?> c Comp < E, P, S; skip » a <<T> <cr>* Comp <E,P, Q><T < <r[V < e » <r/x] = <r' > * Comp < £, P, Q > oJ < <T > * (Comp < E, Pt, Q* » a' = £') *Comp<E,P,Q »a-" where P,(2,y) : {Q'} € £7, <r,- is a fresh state for P,, *' = (^/z])[V(e-)/2/] <r" = af>,/C(E'),G) Comp < E, P, Qi; Q3 » <r (if W « 6 »= true) Comp <E,P, Q2;Q3><r (if W « 6 >= /a/se) Comp < £,P, t7(6)f/ien{Q1}e/se{sifcip}.;Q2 » <* Comp<. £,P)i/(&){Qi;u>/»7e(6){Q1}};Q2 » * Comp< ^P.Qiji/^irepeatiQjunti/^ljQa > < cr > * Comp < E,P,Q' > a where Q' = Buildenv(PtQi),U : Q,- 6 P Figure 3.3: Definition of Comp Now that the notational tools are defined, the actual operation semantics for Bruce can be established. The first step is to provide a means of interpreting expressions. Two functions, V and W, evaluate arithmetic and boolean expressions respectively "in the usual way": V : Exp —> o —• Domain W : BoolExp —• a —• {true, false} Here, Domain might refer to the natural numbers. A function Comp is used to build S (figure 3.3). The state sequence S for a terminating computation starts at an initial state CTQ, and ends at a state on. Comp takes as its arguments the environment E, a program P, a chain Q, and a state a. E is a source where all available program definitions may be found - a necessity when processing subprogram CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 20 Buildenv(P, Q) = -f <Q» - iiP:{Q';Q) < Q; while(b){Q';Q}; Buildenv(P, Q*) > if Q belongs to a while < Q;if(-~b){repeat{Q';Q}until(b)};Buildenv(P,Q*) > HQ belongs to a repeat < Q\ Buildenv(P, Q*) > if Q belongs to an if where S{Q';Q};Q*, ie. S is the parent statement containing subchain Q, and Q* is the chain following S Figure 3.4: Definition of Buildenv calls. P defines which labels may be used as branch destinations. The chain Q is the program code currently being processed, a is the current state of the store. Some features of Comp are worth explanation. Line 1 simplifies Comp so that op erational definitions are not duplicated for single- and multiple-statement chains. Lines 2 and 3 define the skip instruction. In line 4, an assignment results in a state variant's creation of a new state cr', which is used by the following chain. Tests (lines 6 and 7) are handled by the execution of the appropriate chain of code according to the value of the test expression. While loops (line 8) are processed by reducing the construct into a test. The body of the test is composed to simulate the iterative nature of the loop should the loop test be positive. Repeat loops (line 9) are handled similarly. Subprogram invocation (line 5) is more complex. A stack mechanism is assumed to exist so that nested subprogram calling, including recursion, can occur. When calling a new program, the pre-existing arguments to Comp are implicitly saved on the stack, and a "fresh" state cr,- is created for the new subprogram to be executed. Before executing the subprogram, multiple variants are performed on 0{ in order to initialize the store with the values of the variable and value parameters being passed. The subprogram is then executed, eventually producing a state sequence S*. Finally, changes in the variable parameters which may have occurred during the subprogram call must be accounted for. This is a mechanical process which we give to a function a. a takes as arguments the old state cr, the final state of £', and the variable parameter vector v, and returns a new state with a set appropriately. State variants would be used in the creation of this new state. CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 21 KMLUM a := 1; goto gl; while (a < b) { repeat { gl: a := a + 2 } until (a == b); a := a + 3; }; a := a + 4 } Figure 3.5: Example Program a := a + 2; .7 Ha ==&)){ repeat { a := a + 2 } imii/ (a == 6); }; a := a + 3; to/w'/e (a < b) { repeat { a := a + 2 } unii/ (a == 6); a := a + 3; }; a := a + 4 Figure 3.6: Buildenv Output CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 22 When processing branches (line 10), Comp makes use of an auxiliary function Buildenv (figure 3.4). The branch itself results in no change to the state, and the chain following the branch is ignored, which reflects the destructive nature branches have on command sequencing. Following the branch is the computation of the chain of code at label,. Us ing Buildenv, the control context normally found at the branch destination is recreated. Buildenv creates a chain of program code by taking the chain at the destination label and appending appropriate control code for successive parent constructs, resulting in a chain of code which has an appropriate control context. For example, figure 3.5 is a Bruce pro gram containing a branch into two nested loops. Figure 3.6 contains the code generated by Buildenv for the label gl. Once Comp is defined, we complete the operational semantics of a program using a function M, which is the meaning function of a program: M < P > (T0 = K.(Comp < E,Q,Q > o0) where P : {Q} € E. This can be thought of as the initial module executed in order to start Comp's evaluation of the program. In summary, the Bruce abstract machine (BAM) executes by code manipulation (Comp), expression evaluation (V and W), and writing values to the store (state variants). The fea ture of this operational semantics worth special attention is the way control is processed by Comp. If one were to observe the contents of Compos chain argument, one would see an ever-changing chain of program instructions. This chain reflects the control context of the program at any particular moment in the computation. This somewhat parallels the way people "hand compute" programs, in that tracing a program's flow of control involves the implicit textual context of statements, in particular, the constructs in which they are nested and the code textually following them. The Bruce machine does this by explicitly constructing this context. Chapter 4 A Horn Clause Semantics This chapter introduces a new semantic methodology for imperative programs. In partic ular, a Horn clause semantics is presented for the Bruce language of chapter 3. Section 4.1 discusses some of the philosophical motivations behind the design of the semantics. The logical semantics for basic Bruce programs, that is, ones in which branches are not used, is given in section 4.2. The semantics of branches is then detailed in section 4.3. Section 4.4 discusses the interpretation of the semantics as logic programs, and addresses some completeness issues. Some examples of actual translations of Bruce programs conclude the chapter in section 4.6. 4.1 Design Goals There are a number of design motivations for the logical semantics being introduced in this chapter. Since computation is to be defined solely by the state of the store, the minimal requirement for the semantics is that it has enough expressive capability with which to describe this characterization of computation. This requirement should not be an obstacle, as predicate logic has proved to be a powerful tool in the semantics of computation and programming languages (see section 2.1.2). Our main motivation, however, is to define a semantic system which allows efficient and powerful transformations of imperative-style programs, namely, those written in Bruce. 23 CHAPTER 4. A HORN CLAUSE SEMANTICS 24 The fact that the semantics is to be used in a program transformation environment means that its semantic scope can be constrained somewhat, especially when compared to the scope of semantic systems used in program verification environments. The program trans formation system to be used in this thesis will take as input an imperative program, and will produce a transformed, optimized program as output. A key assumption is that the source program being input is to be considered complete and correct, both syntactically and semantically. This assumption greatly simplifies the scope of the semantics, as we do not have to deal with such issues as the well-formedness of the source code, the termina tion of mechanisms, the evaluability of expressions, and the matching of data types. More general semantic systems, such as that presented in [Hehner 84a], address such issues. A major goal of the semantics is that there should exist a strong and natural rela tionship between the source language and its corresponding semantic representation. The predicative programming paradigm offers a solution in this regard. The scheme is to de fine for every construct of the source language a predicative meaning. This proves to be advantageous when converting between the source and logic, as program constructs can be considered to be predicate labels for their corresponding semantic definitions. Such a mapping between the source language and logic can be utilized in both directions, which is an ideal situation since such conversions will be required by the program transformation process. Finally, it is prudent to consider the recent accomplishments in defining models of com putation for first-order predicate logic. In particular, work in logic programming has shown the suitability and practicality of Prolog in various theoretical and practical applications. What is especially worth noting is that Prolog is well suited to many types of program transformations. A program written in pure Prolog (one without meta-logical operators) can have many types of transformations applied to it, in fact, any transformation which can be proved to be logically valid. Ascribing a logic programming model to our seman tics means that a richer, sounder, and more automatable transformation system might be possible. CHAPTER 4. A HORN CLAUSE SEMANTICS 25 4.2 Basic Bruce Semantics We now present the semantics of Bruce programs having no branches1. In section 3.3 a computational environment E is denned as a particular set of programs. In logic, this environment defines a theory Th(E) = (B,A) where B = (F, P) is a predicative basis, and A is a set of axioms. The basis is composed of a set of function symbols F and a set of predicate symbols P. F contains all the arithmetic, relational, and boolean functors, as well as the domain dependent constants, used in Bruce. P contains the atoms asgn and callasgn, the propositional constants true and false, plus additional predicates dependent upon the structure of the programs in E. The axioms A, collectively known as the program predicate, are created through the principles of predicative programming. The composition of these axioms reflect the syntactic structure of the program, and will be detailed shortly. A mechanism is a basic module of computation which has observable, well denned behavior. Mechanisms are defined by particular syntactic structures of the programming language whose behavior have been predefined in logic. Bruce constructs which exhibit well defined behavior, such as programs, assignments, if tests, loops, and branches, are treated as mechanisms. Mechanisms are also defined by computational events which occur during the execution of a program, such as the evaluation of value parameters during subprogram invocation. Mechanisms fall into two categories: (1) elementary mechanisms, such as assignments, which are described in logic by atoms, and (2) complex mechanisms, which is any construct which requires a predicative definition. Satisfiability in this logical semantics denotes that a mechanism is implementable. An unsatisfiable program predicate, one which evaluates to logical false, is unimplementable or under specified. A consequence of this convention is that the logical values true and false are themselves program specifications, being the universally satisfiable and unsatis-'This semantics is used in the initial stages of defining the semantics of program branches in section 4.3. CHAPTER 4. A HORN CLAUSE SEMANTICS 26 fiable program specifications respectively. We restrict our logical semantics so that all axioms for complex mechanisms are written as Horn clauses. A Horn clause is a formula of predicate logic having the form V(/J <= Ci A C2 A ... A Cfc) where H is termed the head, and the conjunction of C,'s is called the body. The Cj's are typically input-output relations in most axioms. The informal semantics of this formula is: if the relations C, all hold for some particular instances of memory states, then H holds. The C, relations which represent complex mechanisms require their own subsequent Horn clause definitions, and so on. A program predicate thus has the form: |= V((P <= Si A ... A Sk) A (Si Ti A ... A Tm)... A (Tj ^ W\ A ...) A ...) where the S;'s, T,'s, and W,'s are input-output relations. Input-output relations have included as arguments two state vectors, one for the input state of the computation, and the other for the output state. For example, in the relation if2(vi,Vf) the vectors Vi and Vf represent the initial and final store states during the execution of the mechanism if 2. Each input-output vector represents the state a of the computer's store at a particular instant in time. The elements of input-output vectors are logical variables whose scope is the clause within which they are used, and whose domains are the value domains of the variables used in Bruce. Each element represents the value of a particular variable parameter, value parameter, or local variable during an instant of the computation. Under some circumstances vector elements might be set to domain values2. Such values represent implicit assignments to the Bruce objects that the vector elements represent. Figure 4.1 presents the axiomatic semantics of Bruce constructs without branches. The semantics are logical descriptions of the behavior of Comp in Bruce's operational semantics (figure 3.3). Generally speaking, each complex mechanism in a program is represented by 2 We will see such a phenomenon occur in chapter 6. CHAPTER 4. A HORN CLAUSE SEMANTICS 27 1. Programs: Progname(a,e) : local x { Q } = |= Progname(< a,-,e"j >,< a/,e,- >) <= Q(<ai,ei,Xi>,<a},ef,xf>) 2. Chains: Q = Si;52;...;5j. d= |= Q(vi, vf) = 5i(t}<, d) A 52(t;i, U2) A ... A £*(€«,_!,£*) 3.Null operation: sfcip 1= true 4. Assignment: a: := e =f [= as0n(t;,-, vx,e,vj) 5.Program invocation: def ca// P(< vi Vj >, < ei,ek >) = |= callasgn(v,x\, e\) A ... A ca//as<7n(t>,xjfc, ej,) AP(< Vl,...,Vj,Xi,...,Xk >,Vf) 6.(a) Test: l/ien { Qi } else { <?2 } A (ifi(vi, vf) <r --6 A Q2(i>,-,«/)) »7 (6) Me  Qi } Hf |= By) «= 6 A Qifa, €/)) 6.(b) Test: 1/ (6) then { Qi } d= |= (i/<(«j, 0/) 4= 6A Q^, vj)) A (ifi(vitVi) -16) 7. While loops: tu/u/e (6) { Q } d= |= (whilei(vi,vj) <= dAQ^i,^) Awhilei(v2,Vf)) A (whilei(vi, Vi) •£= ->6) 8. Repeat loops: def repeat { Q } tmii/ (6) = |=.(repeflrf,-(uj,«/) •£= Q(C,-, €2) A->b A repeati(v2, v/)) A (repeal (v,-, €/) A 6) Figure 4.1: Logical semantics of Bruce constructs (no branching) CHAPTER 4. A HORN CLAUSE SEMANTICS 28 a uniquely named predicate. Our scheme is to generate unique predicate names through numbering. For example, a program with three if tests has generated for it three predicates named ifl, if2, and i/3. The only relevance that a predicate name has is that it is unique; the label name itself is only for notational convenience. When a predicate is being converted into Bruce code, the fact that the predicate might be called if2 does not necessarily imply that it represents an if test, since only the logical form of the predicate is used for the translation. Line 1 specifies the high level semantics of programs, as well as the composition of input-output vectors. A program Progname is defined by the predicative meaning of its main program chain Q. The change to the store when executing Progname is indicated by the changes to the input-output vectors used within the relations for Progname and Q. Within all predicates, input-output vector elements are mapped to their Bruce objects by their positions in the vector. In particular, a program Progname having variable parameters a, value parameters e, and local variables x uses the vector format < a, e,x > throughout the rest of the program predicate. The manner in which vector values are shared between Progname and Q depends upon the nature of the store objects in question. Since local variables (x) are only active during the execution of the program body, they are not used in the predicate header. In addition, value parameters (e) are not changed by the program's execution; thus their final values in the program header are the same as their initial values. The composition of statements is represented in Bruce by chains, which are statements separated by the sequencing operator ";". In logic, this is represented by conjuncting the relations for each statement in the chain (line 2). Intermediate input-output vectors are used to "pass" the value of the store among the relations. As was mentioned above, the relations themselves often have auxiliary definitions. Elementary relations, represented by atoms, define the behavior of elementary mech anisms. There are four elementary relations representing assignments (line 4), boolean tests, skip statements (line 3), and value parameter evaluation when invoking subpro grams. asgn(v{,vx,e, vj) is an elementary relation which represents a state variant. vx CHAPTER 4. A HORN CLAUSE SEMANTICS 29 is a logical variable which represents the element in the output vector vj corresponding to the store location for variable x. vj is the state which results after substituting the value of the logical variable vx in vj with the value of expression e in the context of input state Vi. Boolean tests, which are represented by the boolean expression 6 throughout the definitions, are also elementary relations. They implicitly use the input vector appropriate to the context of the test within each definition, skip instructions are simply denned by logical true. Subprogram invocation (line 5) is represented by an input-output relation for the sub program in question. The input and output vectors within this relation are constructed to match the particular parameter conventions of the program being invoked. An input-output vector with the variable parameters followed by the value parameters is constructed, as is shown in the definition. However, the value parameter elements first require that each expression being passed is evaluated with respect to the current state of the store (v). callasgn(v,x,e) is an elementary relation which equates the value of expression e in the context of the next state v with a logical variable x. These expression values are then placed into the subprogram relation's input vector. The output vector of the subprogram relation represents the final state of the parameters after execution has completed. Since only the variable parameters could have possibly changed, the final values of these elements are appropriately distributed to the current program state. This distribution of parameter values means that any relation following the subprogram call has the final parameter values placed within its input vector. Should the call be the last statement of a chain, then the values may affect the output vector of the predicative header to which the chain belongs. Test constructs have straight-forward definitions. A Bruce if construct with then and else alternatives (line 6(a)) always has one of the two test bodies executed according to the outcome of the boolean test. The corresponding logical semantic mirrors this fact: if the boolean test is true, then chain Q\ is executed, which is abbreviated in the definition by an input-output relation for the chain. Otherwise chain Q2 is executed. In actuality, these chains are represented by conjunctions of relations (as in line (2)). An if construct CHAPTER 4. A HORN CLAUSE SEMANTICS 30 with no else alternative is represented by a clause with a null body (line 6(b)). This is a simplified representation for a chain containing the skip statement used by Comp, which in our semantics is denned as true (line 3). While loops (line 7), are defined by two clauses, one denning the iterative case, and the other the exit condition. The iterative clause specifies a relation which holds if the while test is true, in which case the loop body is executed, and the loop itself iterates. Iteration is defined by a recursive restatement of the relation for the while construct. The treatment of repeat loops (line 8) is similar to that of while loops. 4.3 Program Branches Branches add a dimension of complexity to the semantics of Bruce. A program branch has consequences on the composition of commands, as it destroys statement sequencing. In addition, branching alters the logical semantics of constructs. For example, a branch can be used to jump out of one or more nested loops - an action which dramatically corrupts their normal semantics. The semantics of such a loop is now dependent on the contents of that loop's body. The existence of branches therefore means that the syntactic "surface structure" of a statement is not sufficient for derivation of the semantics. Instead, the semantics are now dependent on code within the statement. Two distinct phenomena occur during the execution of a branch. First, when a branch is executed, every mechanism which is active is in effect halted. In other words, the current control context of the program is terminated. Second, a new control context found at the branch destination is then used to commence subsequent execution. Defining the logical semantics of branches is likewise done in two steps: defining new control contexts, and terminating old control contexts. First, the activation of new control contexts is defined. Our treatment of branches makes use of the concept of continuations [Clint etal. 72] [Stoy 77] [Tennent 81]. In a language with branching, a continuation for a statement is the expected results of all the program computation which will temporally CHAPTER 4. A HORN CLAUSE SEMANTICS 31 follow the statement's execution. The meaning of a branch is therefore the direct effect on the store, which is none, plus the effect of the continuation which, in the case of branches, is the effect of executing the code at the statement label. We treat a branch as a call to the label program identified by the branch destination label: goto labels d= labeli(v{,Vf) Here, v/ represents the final state of the store for the rest of the mechanism's execution, in effect, the continuation for the program. The label program itself is' defined in Bruce's operational semantics by the output of the Buildenv function, which recreates the control context of a labelled statement. Using predicative programming, we define the logical meaning of a branch destination by simply generating a predicate for the code created by Buildenv. Hence, we define for each labelled statement in a program a label program predicate: labeli(vi,vj) Q(vi,Vf) in which Q(vi,Vf) is the predicative meaning of the code generated by Buildenv for that label. The next step is to account for the termination of the current control context caused by a branch. The control context of any statement of a program can be determined as follows. Consider a statement S whose control context is to be found. We expand the program predicate, starting from the main chain, by replacing each parent construct of 5 by its logical definition. This continues until we reach S. Next, distributivity about logical or(v) is used to create a disjunction of terms. This distribution about "V" should be done so that the sequencing of terms is not altered, as this sequence reflects the relative order in which tests and statements are executed during computation. Each disjunct is composed of a mixture of chains of code conjuncted with boolean tests, which is a situation acceptable in predicative programming given the interchangeability of code and logic. Semantically, each disjunct describes a trace of the program control that can occur during execution. The control context of the statement S is represented by the conjunction of relations following each instance of S in the predicate. CHAPTER 4. A HORN CLAUSE SEMANTICS 32 (i) P <*= while(bi){while(b2){goto end}}; end : S (ii) <$= (bi Awhile(b2){goto end};while(bi)W , -<bi);end:S ' while (b )i ^ (bi A(b?/\ goto end;while(b2)v , ., ,1 w -"62); while(b\) V -161);end : 5 u>m/e (62)! <7<rfo end } (it;) 61 A 62 A 50*0 end;u;/ii/e(62); w/ii/e(6i);end : 5 V 61 A -162 A while(b\);end : 5 V -161 A end : 5 } (t>) ««= b1Ab2Aend(vi,Vf) V 61 A -162 A while(bi);end : 5 V -161 A end : 5 where end(v{,vj) -<= S(v;,t;/) Figure 4.2: Branching out of two loops To determine the effect that a branch has on the control context, we must first expand the program predicate as previously described. This expansion produces the semantic description of the control context following the branch. Given the appearance of a branch in a disjunct of the predicate, the termination of the control context at that branch is defined as Ri A ... A Rj-i A goto label, A Rj A ... A Rk =f Ri A ... A Rj-i A labeli(vi, vj) where Rj A ... A Rk is the control context for the branch. The disappearance of Rj A... A Rk from the predicate is equivalent to removing its effect on control. This restructuring is then applied to each disjunct containing the branch. The net effect of the restructuring is to "pre—compile" the effects of the branch on sequencing into the predicate. In summary, the predicative restructuring procedure is as follows: 1. Expand statements by their semantic definitions until a branch is revealed. 2. Distribute the chains of code over the logical or (v) connective until we get a dis junction of terms. 3. Remove terms and chains of code which sequentially follow the branch. CHAPTER 4. A HORN CLAUSE SEMANTICS 33 4. Replace the branch by a call to its label program. 5. (Optional) Simplify the disjunction by factoring common terms using distributivity. Of course, logical manipulations can be economized and predicative equivalences can be preserved when expanding and simplifying the program predicate. Figure 4.2 shows a program where a branch removes control out of two nested loops (relations are abbreviated). One expansion of each loop (step (hi)) is required in order to produce the chain containing the branch. In step (iv), the chains are distributed through the internal disjunctions, creating a single disjunction of chains. Finally, step (v) shows the removal of the chain following the branch, and the replacement of the branch with a call to the label program (see first disjunct). With respect to the theory Th(E) outlined in section 4.2, the incorporation of branches in the semantics means that the predicative basis B is supplemented with relations for the label programs, and that the axioms A are supplemented with label program predicates. However, an unfortunate aspect of branches is that we can no longer rely on a straight forward inspection of the program syntax in order to derive program axioms, as is used by the basic semantics, but must instead use the restructuring procedure outlined above. Even though the methodology of deriving axioms has become much less elegant, we still end up with a semantic description for the program which is as logically sound as for programs without branches. Only the formula for axiom derivation has suffered in terms of complexity. 4.4 Logic Program Interpretation and Completeness Given a program P, we define for it a set of Horn clauses which define the input-output behavior of P and its constituent parts. One last clause to be added to the semantics is a CHAPTER 4. A HORN CLAUSE SEMANTICS 34 goal clause, which represents an invocation of the program: |= ->P(Vi,Vf) The input parameters to P would be appropriately set in the u,- input vector. The axioms and goal clause for P has a logic program interpretation [Clocksin etal. 81], and has both a procedural and declarative semantics [van Emden etal. 76]. Thus, through the logic programming paradigm, the complete logical semantics of a program can be treated as a logic program, and can be executed using SLDNF resolution [Lloyd 84]. In order to more closely ally our semantics with the logic programming concept, we henceforth use the Prolog notation from [Clocksin etal. 81] with which to write the seman tics. The typical form of a Horn clause is now: P^Ci AC2A...ACfc d= P : -CUC2, ...,Ck. Also, input-output vectors will now be written in terms of Prolog lists: v =< vi,...,vk > d= [vi,v2,...,vk] We assume that any Prolog interpreter used to execute the semantics has available to it the arithmetic and boolean expression evaluators V and W from the operational semantics. The logic program interpretation of the semantics also makes the axioms logically stronger. The problem with the "bare" logical interpretation of the axioms is that the logical implications used in the formulas are only partial specifications of the behavior of mechanisms. For example, a mechanism M described by two clauses is logically equivalent to the following: . |= (M <= Ci) A (M C2) = \= M (d V C2) This states that M is satisfied if C\ or C2 are satisfied, or both. However, this is only a partial specification of the behavior of M, as when C\ and C2 are both false, M is still satisfied. What we need is for the implication in each predicate to be read as a logical equivalence, or iff. CHAPTER 4. A HORN CLAUSE SEMANTICS 35 Fortunately, when the semantics are interpreted as a logic program, the predicates be come logically complete specifications. The completion of a logic program is a logical char acterization given the effects of SLDNF resolution on program interpretation [Lloyd 84]. If p(h,...,tn) <= Li,...,Lm is one of k clauses denning p, we first transform each clause into p(xi, ...,x„) 3yi..3yd((xi = ti) A ... A (xn = tn) A L\ A .. A Lm) where x\,...,xn are new variables, and yi,...,yd are the variables of the original clause. The predicate for p is thus p(xu...,xn) Ex V...v£jt where each Ei has the form 3y1..3yd((xi = fx) A ... A (xn = tn) A Ix A .. A Lm) The completed definition of p is then Vx1...Vxn(p(x1, ...,xn) ^^V ... V Ek) This is the logical meaning of a predicate given the effects of SLDNF resolution, and is assumed implicit in all pure Prolog programs. This means that our logical axioms are complete specifications. 4.5 Translating Logic to Bruce Once a program is denned in terms of the preceding semantics, its semantic representation can be transformed and analyzed using the laws of first-order predicate logic. In a program transformation environment, the intent is for the semantics to be manipulated to produce a result which yields greater efficiency or some other desired quality not found in the original source program. This optimized representation should then be transformed back into the source language using predicative programming. CHAPTER 4. A HORN CLAUSE SEMANTICS 36 Compiling a logical representation back into Bruce is the inverse of generating the logic from Bruce. Given a set of axioms, they are matched "backwards" to the Bruce constructs using the axiom schema in figure 4.1 of section 4.2. However, it is possible that a direct match is not possible between the axioms being matched and the definitions for Bruce constructs. As a consequence, logical manipulation of the axioms might be required until a match can be obtained. The conversion of basic Bruce constructs is straight-forward. However, the conversion of branches and branch destinations needs clarification. Branches are treated as label program relations in our semantics. These label programs have embedded in them the continuation of the computation, or in other words, the result of the rest of the computation. As a result, there should never be instances of other goals making use of the output vector of a branch relation. Instead, the output of a label relation is given to the output of the clause within which it resides: P(vi,Vf) •<= C\(vi,V2) A ... A Branch(vk,Vf) Therefore, any complex relation (that is, one with a predicative definition) which is the final goal' of a clause can be considered as a branch. The branch destination is simply the Bruce code derived for the predicate describing the branch relation, prepended with a unique destination label. The placement of the destination code within the Bruce program can become somewhat involved, as the code should not interfere with the control of other program constructs. A solution to this is to unfold the first instance of a branch. When a branch relation is first discovered, instead of creating a branch statement to it, the relation is replaced by the code defining the destination, which is labelled with a destination label. Subsequent branch relations referring to this destination will simply refer to this unfolded code, and can be replaced with branches to it. An example of branch translation is in figure 4.3. Predicate A contains the logical semantics to be converted. Predicate B has the predicate for c\ converted to its Bruce realization. This assignment is unfolded into p in predicate C, and is given the label c\. D has the reference to c2 replaced by its equivalent definition. Finally, this reference to c\ is CHAPTER 4. A HORN CLAUSE SEMANTICS 37 A : |= (p(vi,vf) <= ci(vi,v2) A c2(v2,Vf)) A(c2(vi,vj) Ci(«,-,fJ/)) 5 : |= (j>(0i,G/) <= ci(ut»u2) A c2(v2,vf)) A(ci(vi,vf) ^=x:=y+l) A(c2(vi,Vf) ><=ci (!>,•,!>/)) C : |=(p(®i,^/) cl : x := y + 1 A c2(v2,vf)) A(c2(vi,vf) <=ci(vi,vj)) D : |= (p(vi, vf) cl : X := y + 1 A ci(t>2, vf)) E : |= (p(vi, Vf) <= (cl : x := y + l;goto cl) Figure 4.3: Converting Branches replaced with a branch, since the code for c\ has already been converted. 4.6 Example Translations This section presents some example translations of Bruce programs into logic, and vice versa. All the examples are generated by an automatic translation system, particulars of which are discussed in chapter 5. Figure 4.4 contains a simple Bruce program with three consecutive assignments to a variable parameter x, along with its semantics. The sequential nature of the Bruce program is captured in the semantics by the naming of the logical variables in the input-output vectors. The result of the final assignment is given to the header for prog. The converted result for the semantics is identical to the original program. prog([x],[]) : { x := x + 1; x := x + 3 prog([Xl],[X2]) :-asgn([Xl],X3,Xl + 1,[X3]), asgn([X3),X4,X3 + 2,[X4]), asgn([X4],X2,X4 + 3, [X2]). } Figure 4.4: Consecutive assignments CHAPTER 4. A HORN CLAUSE SEMANTICS 38 y := i; while (n > 0) { n := n — 1; y := y * x } } y:= i; w/ii7e (n > 0) { n := n — 1; y := y * x } } p([yi,Xl,JVl],[Y2,Xl,iVl]) :-as5n([yi,Xl,7Vl],y3,l,[F3,Xl,iVl]), wW/cl([r3, XI, Nl], [Y2, X2, N2]). whilel([Yl,Xl,Nl],[Y2,X2,N2]) :-Nl > 0, asgn{[Yl,Xl,Nl],N3,Nl - 1,[Y1,X1,N3]), asgn([Y 1, XI, JV3], y3, Y1 * XI, [F3, XI, iV3]), w/iz/el([y3, XI, JV3], [Y2, X2, iV2]). w/ii/el([yi,Xl,iVl],[yi,Xl,iVl]) : --.iVl > 0. Figure 4.5: While loop P{[y],[x,n]) : { y:=l; w/iz/el : i'/ (n > 0) { n := n — 1; y := y * x; goto whilel } } OR Figure 4.6: Two alternate Bruce realizations A more complex Bruce program is in figure 4.5. Two clauses, collectively defining the predicate whilel, describe the while loop. Because changes to the value parameters x and n are not available to any calling mechanisms, the two input-output vector elements corresponding to these objects are not altered in the header for p. Two possible Bruce realizations for the semantics are in figure 4.6. The first program is the same as the original source. The second one, however, replaces the while loop by a branch and test mechanism. Figure 4.7 contains the treatment of subprogram invocations. The four expressions making up the call-by-value argument list are each given callasgn relations, and the logical variables representing the valuation of the expressions are passed to the subprogram. Note the distribution of the new variable argument values into the subsequent assignments occurring after the subprogram call. CHAPTER 4. A HORN CLAUSE SEMANTICS 39 progA([a,b,c],[x,y,z]) : local[games,work] { x := 3; work := 6; call proc([a, b, work], [5,x, y, (3 4- 4)]); c := 8; z := 10 } proc([q,w,e],[rr,r,t,y]) : { q := w } progA([Al,Bl,Cl,Xl,Yl,Zl],[A2,B2,C2,Xl,Yl,Zl]) : -asgn([Al,Bl,Cl,Xl,Yl,Zl,Gal,Wol],X2,3,[Al,Bl,Cl,X2,Yl,Zl,Gal,Wol]), asgn([Al,Bl,Cl,X2,Yl,Zl,Gal,Wol],Wo2,Q,[Al,Bl,Cl,X2,Yl,Zl,Gal,Wo2]), callasgn([Al, Bl, CI, X2, Yl, Zl, Gal, Wo2], Tl, 5), callasgn([Al, Bl,Cl, X2,Yl, Zl, Gal, Wo2],T2, X2), callasgn([Al, Bl, Cl, X2, Yl, Zl, Gal, Wo2], T3, Yl), callasgn([Al, Bl, Cl, X2, Y1, Zl, Gal, Wo2],T4,3 + 4), proc([Al, Bl, Wo2, Tl, T2, T3, T4], [A2, B2, Wo3, T5, T6, Tl, T8]), asgn([A2, B2, C1,X2,Y1,Z1, Gal, Wo3], C2,8, [A2,B2, C2, X2, Yl, Zl, Gal, WoZ]), asgn([A2, B2, C2, X2, Y1,Z1, Gal, WoZ), Z2,10, [A2,B2, C2, X2, Yl, Z2, Gal, WoZ]). proc([Ql,Wl,El,Rrl,Rl,Tl,Yl],[Q2,Wl,El,Rrl,Rl,Tl,Yl]) : -asgn([Ql,Wl,El,Rrl,Rl,Tl,Yl],Q2,Wl,[Q2,Wl,El,Rrl,Rl,Tl,Yl]). Figure 4.7: Subprogram invocation CHAPTER 4. A HORN CLAUSE SEMANTICS 40 prog([Xl,Yl),[X2,Y2}) :-11([X1,Y1],[X2,Y2]). 10([X1,Y1],[X2,Y2)) :-asgn([Xl,Yl],X3,Yl + l,[X3,yi]), asgn([X3, Y1],Y3, X3 + 2, [X3, Y3]), P«f([., *[]):{ «([X3,y3UX2,y2l). goto 11; I0:x:=y+1; l2:y:=x + 2; goto 13; l4:x:=y + 4; goto end; l3:y:=x + 3; goto 14; 11 : x := y+ 1; end^-x asgn([Xl,Yl],Y3,Xl + 3,[Xl,YZ}), 'V'~ ,4([X1, Y3], [X2, Y2}). } 11([X1,Y1],[X2,Y2]) :-asgn([Xl,Yl],X3,Yl + 1,[X3,Y1]), /2([X3,yi],[X2,y2]). /2([Xl,yi],[X2,F2]) :-asgn([Xl, Y1], Y3, XI + 2, [XI, Y3]), /3([Xl,F3],[X2,y2]). 13([X1,Y1],[X2,Y2}) :-/4([Xl,yi],[X2,F2]) :-asgn([Xl,Yl],X3,Yl + 4,[X3,Y1]), end([X3,yi],[X2,y2]). end([Xl,yi],[Xl,y2]) : -as^n([Xl,yi],y2,Xl,[Xl,y2]). Figure 4.8: Branching within a chain prog([x,y],[]) : { x := y + 1; y:=x + 2; y:=x + 3; x := y + 4; y.-x } Figure 4.9: Bruce equivalent CHAPTER 4. A HORN CLAUSE SEMANTICS 41 prog([y,n],[]): local [x,eof] { n := 0; while (true) { call read([x], [ ]); n := n + 1; if (eof =:= true) { goto end }; y •= y + x };. end : n := n — 1 } Figure 4.10: End of file control scheme (initial) A treatment of program branches is illustrated in figure 4.8. A label predicate is created for each labelled statement in the program. The converted Bruce program in figure 4.9 illustrates an interesting side-effect of the conversion algorithm: since the first instance of any branch is unfolded, the branches in the original program are lost. A more complex branching scheme is illustrated in figure 4.10. This program uses a common control strategy for exiting loops based on an end-of-file condition. The reference to eof represents a system call which signals the end of the input stream. Figure 4.11 has the logical equivalent of the source, and the Bruce program derived from it is in figure 4.12. The old loop structure is lost, as it never represented a true while loop anyway. This new program outlines the control which was implicit in the original source. Note that it would have been possible to simplify the program predicate (for example, the tests true and -ttrue) before generating the final program. One final example is the program in figure 4.13, which contains a jump into the middle of a repeat loop. The program derived after translation into logic (figure 4.14) illustrates the complexity in control which may arise when using jumps. CHAPTER 4. A HORN CLAUSE SEMANTICS prog([Yl,Nl],[Y2,N2}) :-asgn([Y 1,7Y1, X3, EofZ], N4,0, [71,7Y4, X3, EofZ]), whilel([Yl, N4, X3, EofZ], [Y2, N2, XI, Eofl]). whilel{[Yl,Nl,Xl,Eofl],[Y2,N2,X2,Eof2]) : -true, read([Xl],[X4}), asgn{[Yl,Nl,X4,Eofl],N6,Nl + l,[Yl,N6,X4,Eofl}), testl([Y 1, NQ, X4, Eo/l], [Y2, N2, X2, Eof2}). whilel([Yl,Nl,Xl,Eofl],[Yl,N2,Xl,Eofl]) : --itrue, asgn([Yl,Nl,Xl,Eofl],N2,Nl - 1,[Y1,N2,X1,Eofl]). testl([Yl,Nl,Xl,Eofl],[Y2,N2,X2,Eof2]) : -Eofl =:= true, end([Y 1, /VI, XI, Eofl], [Y2, N2, X2, Eof2]). testl([Yl,Nl,Xl,Eofl],[Y2,N2,X2,Eof2]) : --\Eofl =:= true, asgn([Yl,Nl,Xl,Eofl],Y4,Yl + Xl,[Y4,Nl,Xl,Eofl]), whilel([Y4, N1,X1, Eofl], [Y2, N2, X2, Eo f2]). end([Yl,Nl,Xl,Eofl],[Yl,N2,Xl,Eofl]) : -asgn([Yl,Nl,Xl,Eofl],N2,Nl - l,[yi, JV2,Xl,£o/l]). Figure 4.11: Logical Form CHAPTER 4. A HORN CLAUSE SEMANTICS prog([y,n],[]) : local [x,eof]{ n := 0; whilel : if (true) { call read([x], [ ]); n := n + 1; if (eof =:= <rue) { n := n — 1 } e/se { y := y + x; goto whilel } } else { n := n — 1 } } Figure 4.12: Derived result CHAPTER 4. A HORN CLAUSE SEMANTICS 44 progl([x,y},[}) : { x := x + 1; y.= y + 2; repeat { x := x + 3; /l : y := a; 4- 4 } until (x —:= y); goto ll } progl([Xl,Yl],[X2,Y2}) :-asgn([Xl, Yl], X3,X1 + 1, [X3, Yl}), asgn{[X3,Yl],Y3,Yl + 2,[X3,Y3]), repeatl([X3,Y3],[X4,Y4]), ll([X4,Y4),[X2,Y2]). 11({X1,Y1],[X2,Y2}) :-asgn([Xl, Y1], Y3, XI + 4, [Xl,Y3]), testl{[Xl,Y3],[X3,Y4}), ll([X3,Y4],[X2,Y2]). testl([Xl,Yl],[X2,Y2]) : --XI =:=Y1, repeaa([Xl,yi],[X2,r2]). testl{[Xl,Yl],[Xl,Yl]) : -X1=:=Y1. repeatl([Xl,yi],[X2,y2]) :-asgn{[Xl, Y1], X3, XI + 3, [X3, Yl]), asgn([X3, Yl], Y3, X3 + 4, [X3,y3]), -X3 =:= y3, repeafl([X3,y3],[X2,y2]). repea<l([Xl,yi],[X3,y7]) :-asgn([Xl,Yl],X3,Xl + 3,[X3,yi]), asgn([X3, Y1], Y3, X3 + 4, [X3, y 3]), X3 =:= y3. Figure 4.13: Jumping into a repeat loop CHAPTER 4. A HORN CLAUSE SEMANTICS 45 progl([x,y},[]) : { x := x + 1; y.= y + 2; repeatl : repeat { x := x + 3; y := x + 4 } unii'Z (x =:= y); ll: y := x 4- 4; 1/ (nl =:= y) { goto repeatl }; goto 11 } Figure 4.14: Bruce equivalent Chapter 5 A Bruce-Logic Translation System A Bruce-Logic translation system has been implemented in CProlog [Pereira et al. 84]. This system comprises the front-end (logic generator) and back-end (Bruce generator or Brucifier) of a Bruce transformation system discussed in chapter 6. The complete source listing of the translation system can be found in the appendices. 5.1 The logic generator The logic generator reads a Bruce program and generates its logical equivalent. It operates in three stages: 1. A Bruce program is read and parsed using a definite clause translation grammar (DCTG) [Abramson 84]. Then, an initial semantics is created directly from the parse tree of the DCTG. This semantics is complete and adequate in the case when no branching exists in the program, pointedly illustrating the semantic clarity of structured, branchless programming. 2. Should branching be found in the program, label program definitions are created for all the labelled code in the program. 46 CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 47 chain ::= statAAS <:> code(Code,In,Out,Defns) :: — SAAicode(Code,In,Out,Defns). chain ::= statAAS, [';'], chainAAQ <:> code(Code,In,Out,Defns) ::— genjchain(Code, In, Out, Defns, S,Q). genjzhain{Code,In,Out,Defns,S,Q) : — SAAcode(Sl,In,X,Dl), QAAcode(S2,X, Out, D2), fuse((Sl,S2),Code), append(Dl, D2, De fns). Figure 5.1: Chain rules 3. Again, in the case of branches, the semantics are restructured to reflect the effect of branches on program control. The rest of this section discusses these steps in more detail. The creation of semantics for basic Bruce programs (section 4.2) is efficiently done through the use of a DCTG. The DCTG specifies how Bruce programs are to be parsed, and once parsed, how semantics are to be generated for the Bruce constructs. Each DCTG rule has associated with it a syntactic component and a semantic component. The syntactic component contains a BNF-style grammar rule for a portion of the Bruce syntax. The semantic component specifies actions which are to take place at the node of the parse tree associated with that grammar rule. In our implementation, a semantic rule builds up a portion of the logical axiom associated with the context of the grammar rule in question. Two rules describing the composition of chains are in figure 5.1. Items within braces are matched with strings in the input, while stat and chain are references to grammar rules. The first rule parses single statement chains, and the second parses multiple statement ones. In the case of single statement chains, the code is directly retrieved at the grammar CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 48 while ::= [while,1 ('], booLexpr^B, [')','{'], chain^Q, ['}'] <:> code(Code,In,Out,Defns) :: — genjwhilecode(Code,In, Out, Defns,B, Q, LoopJabel), addjcurrJabellist(while, Loop Jabel). Figure 5.2: While-loop rule rule for that statement. In the multiple-statement case, the semantic rule calls a Prolog predicate genjchain which obtains the code for the statement at node S in the parse tree and adds it to the code for the rest of the chain at node Q. Obtaining the code for chain Q results in a recursive invocation of the same grammar rule chain. A typical DCTG rule which parses a statement is the one for while loops in figure 5.2. The syntactic component uses the grammar rules booljexpr and chain. The argument Code for the semantic rule code returns the axioms created for the while loop, and the argument Defns returns axioms generated when parsing the loop body. The semantic rule uses a predicate genjwhilecode, which generates the predicative text of the axiom for the loop. Other Bruce constructs are handled similarly. Some bookkeeping is done to ease recompilation of the semantics into Bruce later. Program parameters and variables are mapped to input-output vectors by their relative positions within the vectors. Consequently, the parameter and variable names, as well as their relative ordering in the program, are retained. In addition, some features of the CPro-log interpreter itself are exploited. It is convenient for Bruce to share the builtin arithmetic and relational operators used by CProlog, as this eases the evaluation of expressions later. The existence of a branch in a Bruce program requires the generation of label predicates and the restructuring of the axioms. Both these operations use the existing axiom set during their processing, rather than operate on the original Bruce source program. Label predicate generation involves creating a predicate for each labelled statement in the program. The definition of a label predicate is the predicative meaning of the code generated by the CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 49 prog([x,y],[]) : { repeat { while (x < 0) { x := x + 1; 11: y := x 4- 2 }; x := y-f-3 } unit/ (x =:= y); V := y + 4; jfoio /l; y := y + 5 Figure 5.3: Branching into two loops Buildenv function from Bruce's operational semantics. To derive these predicates from the existing axioms, conjunctions of goals which compose the control context of the labelled statement are collected. Collecting these goals requires traversing the axioms from the statement up through its parent mechanisms until the top program axiom is reached. The predicate generated is refined somewhat by using the fact that branches are semantically represented by label program calls, which can be treated as program continuations. The predicate can thus be terminated as soon as a branch is reached, since the continuation for the branch accounts for the rest of the computation. Figure 5.3 has a program which contains a branch into the middle of two nested loops. The semantics initially generated are in figure 5.4. The program branch is represented by a goal goto(v{,ll,Vf), which is an "unprocessed" branch. The label ll is tagged by a goal label(ll) in the first clause of whilel, which is removed after a label program predicate has been created for it. The label program as denned by Buildenv for ll is in figure 5.5, and the corresponding label program predicate is in figure 5.6. The predicate is much more terse than the label program, since code in the label program is logically described by existing predicates from the basic semantics. Note the addition of a predicate testl, which is used for describing the control which occurs when branching into the repeat loop. CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 50 prog([Xl,Yl],[X2,Y2]) :-repeatl([Xl,Yl], [X3,73]), asgn([XZ, 73], 74, 73 + 4, [X3, 74]), 5oio([X3,74],/l,[X2,75]), asgn{[X2, 75], 72, 75 + 5, [X2, 72]). repea*l([Xl,7l],[X2,72]) w/u.el([Xl,7l],[X3,73]), asffn([X3,73],X4,73 + 3, [X4,73]), ^X4 =:= 73, repeail([X4,73],[X2,72]). repea*l([Xl,7l],[X2,72]) :-w/w/el([Xl,7l],[X3,72]), asgn([X3, Y2], X4, Y2 + 3, [X2,72]), X2 =:= Y2. whilel([Xl,Yl],[X2,Y2]) :-XI < 0, as5n([Xl,71],X3,Xl-f 1,[X3,71]), label(ll), asgn([X3, YI], 73, X4 + 2, [X3,73]), w/u7el([X3,73],[X2,72]). w/n7el([Xl,7l],[Xl,7l]) : -^Xl < 0. Figure 5.4: Basic semantics 5. A BRUCE-LOGIC TRANSLATION SYSTEM Buildenv(prog{...},ll : y := x + 2) <=> y := x + 2; while(x < 0) { x := x + 1; y :=x + 2 }; x := y + 3; if (-,(x =:= y)) { repeat { while (x < 0) { x := x 4-1; y := x + 2 };• x := y + 3 } until (x —.— y) } y := y + 4; (7o£o 11; y := y + 5 Figure 5.5: Label program «1([X1,71],[X2,72]) :-osc/n([Xl, y 1], Y3, XI + 2, [XI, Y3]), u>/n7el([Xl,Y3],[X3,Y4]), asgn([X3, 74], X4,74 + 3, [X4,74]), *esfl([X4,74],[X5,75]), asgn([X5,75], 76,75 + 4, [X5,76]), 50fo([X5,76],/l,[X2,72]). iesil([Xl,7l],[X2,72]) : -^Xl =:= 71, repea*l([Xl,7l], [X2,72]). iesfl([Xl,7l],[Xl,71]) : -XI =:= 71. Figure 5.6: Label program predicate CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 52 The branch restructuring algorithm is a refined version of the distribution procedure outlined in section 4.3. The process begins by searching for an instance of an unprocessed branch goal. When such a goal is discovered, the goals following that goal are thrown away, and the goal is replaced by a label program call. Then the ancestor clauses of the predicate containing the branch are restructured. However, instead of distributing terms of the whole program predicate, only the clauses whose control is affected by a branch are inspected. In addition, predicative formulas are retained where possible, in order to minimize textual changes to the semantics. The net effect of the restructuring is that every axiom whose control is affected by the branch is altered as specified in section 4.3. In terms of the program in figure 5.3, the resulting branch restructuring in figure 5.7 is not very interesting. The main program predicate has its branch goal replaced by a label program relation for ll, and the goal following it has been lost. The branch in the label program predicate has also been replaced. What is of more interest is the program branch in figure 5.8, whose basic semantics are in figure 5.9. The restructured semantics in figure 5.10 illustrates the effect of the single branch on the control of the two loops. These predicates are a derivation of the distributed program predicate in figure 5.11, in which common terms have been factored out and assigned to existing predicate names. 5.2 The Brucifier Compiling a logical representation back into Bruce is the inverse of generating the logic from Bruce. Pattern matching is performed on the axioms of a semantic representation to search for matches with logical definitions corresponding to Bruce constructs. The schema matching used when converting predicates into Bruce is basically a backwards interpre tation of the basic semantics of figure 4.1 in chapter 4. A measure of nondeterminism is encoded into the Brucifier in order to account for the fact that there is often more than one Bruce implementation derivable for a given set of axioms. This nondeterminism means CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 53 prog([Xl,Yl],[X2,Y2}) :-repeatl([Xl,Yl],[X3,Y3]), asgn([X3, Y3], Y4, Y3 + 4, [X3, Y4\), ll([X3,Y4],[X2,Y2]). repeafl([Xl,yi],[X2,y2]) :-whilel([Xl,Yl],[X3,Y3]), asgn([X3, Y3], X4, Y3 + 3, [X4, F3]), ^X4 =:= Y3, repeatl([X4, Y3], [X2, Y2]). repeatl([Xl,Yl],[X2,Y2}) : -whilel([Xl,Yl],[X3,Y2]), asgn([X3,Y4],X2,Y2 + 3,[X2,y2]), X6=:= Y2. whilel([Xl,Yl],[X2,Y2}) :-XI < 0, a5ffn([Xl,yi],X3,Xl + l,[X3,yi]), asgn([X3, Yl], Y3, X4 + 2, [X3,Y3]), w/ii'/el([X3,y3],[X2,y2]). whilel([Xl,Yl],[Xl,Yl]) : --.XI < 0. /l([Xl,yi],[X2,y2]) :-asgn([Xl,Yl], Y3,XI + 2, [X1,Y3]), u;/iz/el([Xl,y3],[X3,y4]), a^n([X3, Y4], X4, Y4 + 3, [X4,y4]), fe5fl([X4,y4],[X5,y5]), asgn([X5, Y5], Y6, Y5 + 4, [X5, Y6]), Zl([X5,y6],[X2,y2]). fesil([Xl,yi],[X2,y2]) : --nXl =:=yi, repeail([Xl,yi],[X2,y2]). testl([Xl,Yl],[Xl,Yl]) : -XI =:= Yl. Figure 5.7: Final semantics CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 54 prog2([x,y],[]): { while (x > 0) { while (x < 0) { x := x + 1; c/ofo 12 }; x := 7/4-2 }; I2:y:= y + 3 Figure 5.8: Branch out of two loops pro52([Xl,71],[X2,72]) :-w/u/e2([Xl,71],[X2,73]), label(l2), asgn([X2,73], Y2,73 + 5, [X2,72]). w/™/e2([Xl,7l],[X2,72]) :-XI > 0, w/u7el([Xl,71],[X3,73]), as5n([X3,73], X4,73 4- 3, [X4,73]), w/iz7e2([X4,73],[X2,72]). w/n/e2([Xl,7l],[Xl,71]) : --.XI > 0. w/u7el([Xl,71],[X2,72]) :-XI < 0, asgn([Xl, 71], X3, XI + 1, [X3,71]), fifoto([X3,7l],Z2,[X4,73]), w/»/el([X4,73],[X2,72]). w/n7el([Xl,71],[Xl,71]) :--.XI < 0. Figure 5.9: Basic semantics CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 55 prog2([Xl,Yl],[X2,Y2]) :-io/n7e2([Xl,71],[X2,72]). while2([Xl,Yl],[X2,Y2\) :-XI > 0, whilel([Xl,Yl],[X2,Y2]). while2([Xl,Yl],[Xl,Y2}) :--.XI > 0, asgn([Xl, Y1], Y2, YI + 5, [XI, 72]). w/izZel([Xl,7l],[X2,72]) : -XI < 0, asgn([Xl, Y1], X3, XI + 1, [X3,71]), /2([X3,71],[X2,72]). w/«7el([Xl,71],[X2,72]) :--.XI < 0, ast/n([Xl,7l],X3,71 + 3,[X3,7l]), w/u7e2([X3,71],[X2,72]). /2([X1,71],[X1,72]):-asgn([Xl, 71], 72,71 + 5, [XI,72]). Figure 5.10: Final semantics prog2 ((x > 0) A (x < 0); x := x + 1 A /2(t>,-, vf)) V((x > 0) A -.(x < 0); x := y + 2; while(x > 0); 12 : y := y + 3) V(-.(x > 0) A 12 : y := y + 3) Figure 5.11: Distributed program predicate CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 56 template jmatch(Progname, Vec, Prolog, [A, B],Bruce,Labels, Newlabels) : — isjajwhile(Progname, A, B,Test, Body), getJO(A,.,Out), template jrnatch.goals(Progname,Out, Prolog, Body, BruceJbody, Labels, Newlabels), append Jist([['whileC ,Test,')',' {'], Bruce J)ody, ['}']], Bruce). Figure 5.12: While loop matching that repeated calls to the Brucifier for a given set of axioms may result in different Bruce programs. There are two main matching modules used by the Brucifier. A module called tem plate-match takes the axioms for a goal and matches them with the logical definitions of Bruce constructs. Such matching often requires the logical manipulation of predicates, for example, factoring out common terms and unfolding predicate definitions. This module also assures that the Bruce statements generated for a list of goals are sequenced prop erly. Depending on the nature of the transformations performed on the semantics, goals may have to be ordered with respect to the data flow of their input-output vectors. A typical matching rule is in figure 5.12. The predicate isja-while succeeds if clauses A and B represent an instance of a while loop. Body are the goals in the loop's body, and are matched through use of the other matching module (called templatejmatch-goals in our implementation). When this succeeds, the Bruce code defining this loop is constructed. The other module, templatejmatch.goals, is used for matching goals in chains. After the goals are ordered, a Bruce construct is derived for each goal. Elementary relations such as assignments are converted directly into Bruce at this stage. More complex mechanisms (those with external definitions) are converted to Bruce by invoking template-match on the axioms defining the predicate to which the goal is referring. One peculiarity of our matching algorithm is that branches always refer to code which has been previously converted. In other words, the first branch in a program will be unfolded, and subsequent references to it will refer to this unfolded portion of code. A CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 57 prog([x,y],[]): { repeat { whilel : while (x < 0) { x := x + 1; y := x + 2 }; x := y + 3 } unii/ (a; =:= y); y ••= y + 4; t/ := a; + 2; ^ofo whilel } Figure 5.13: Derived Bruce program consequence of this is that branches among statements in a single chain tend to be unfolded, and might just disappear as a result. For an example of this phenomena, see the program in figure 4.9 of section 4.6 Lastly, the conversion of Bruce expressions, such as those in assignments and boolean tests, requires the use of information about the names of variables and parameters and their relative ordering in the input-output vectors. This information was saved during the parsing of the program. The Brucified results for the logic programs in figures 5.7 and 5.10 are in figures 5.13 and 5.14 respectively. CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM prog2([x,y},[]): { while2 : if (x > 0) { if (x<0){ x := x + l; y := y + 5 } e/se { x := y+ 3; <7oto while2 } } else { y y + 5 } } Figure 5.14: Derived Bruce program Chapter 6 The Partial Evaluation of Bruce Programs 6.1 Partial evaluation and program transformation Once a program is translated into its logical representation, many types of transformations are possible. Deductive transformations and term rewriting are two possibilities which would likely incorporate a mixture of heuristics and user control in order to be practical. We chose partial evaluation as our program transformation scheme, as it is easily automated. The partial evaluation of logic programs is also a logically sound transformation formalism, since the meta-interpretation of logic programs in a partial evaluation context is based on SLDNF resolution, which is sound. This means that resulting transformed Bruce programs are correct. Most importantly, partial evaluation most clearly illustrates the utility of our Horn clause semantics and its underlying execution model. Partial evaluation is a computational model which distinguishes executable, permissible code from non-executable, suspendable code [Ershov 82] [Ershov 85]. In imperative pro grams, permissible code is that which has all the necessary store values denned in order to, for example, evaluate an expression or test. Suspendable code is that in which a needed value is undefined. In a program transformation setting, input parameters to the program are usually fixed so that the partial evaluator specializes the program with respect to that 59 CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 60 set of input. Partial evaluation then entails executing all permissible code, during which all suspendable code is retained as a partially evaluated program. This residual program is an optimized, transformed version of the original program. The following terminology and results are from [Lloyd etal. 87]. The partial evalua tion of logic programs has been formally shown to be correct and complete, albeit under particular conditions. A semantic theory composed in our Horn clause semantics can be considered to be a definite logic program, since the negation operator used in negated goals only operates on closed boolean expressions in which resolution is never used; we could have used a weaker operator, but chose not to for convenience sake. Let P' be a partially evaluated program wrt a source program P and goal G. P' is sound if correct answers for P' and G are also correct for P and G. The partial evaluation of our semantics is therefore sound, since the partial evaluation of all definite logic programs is sound. The partial evaluation of definite programs is not necessarily complete. P' is complete if correct answers for P and G are correct for P' and G. However, P' may be specialized wrt goal G, which means that some reference in P' to a specialized clause of P may no longer be satisfiable. Lloyd's method of ensuring completeness is to enforce a "closedness" condition on P'. This condition states that any predicate in P' must remain general enough to satisfy all goals which refer to it, which essentially inhibits the partial evaluation from becoming too specialized. We maintain completeness in a different manner. Given a program P, a general predicate h of P, and a goal G, we partially evaluate P wrt G to obtain a program P' containing a specialized predicate h'. Should references to h exist in P' which are too general for the specialized predicate h', we supplement P' with h: P" = P' U {h} With respect to the theory Th(P) defined by the axioms for P, P' being sound means that |= (Th(P') \= h Th(P) \= h) CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 61 However, P"s incompleteness implies \=-i(Th(P)\=h Th(P')[=h) The supplemented theory Th(P") is totally correct: \=(Th(P)\=h o- Th(P")\=h) 6.2 Implementation We transform Bruce programs by partially evaluating the Horn clause semantics for them. Once a Bruce program is translated into logic, its representation is asserted into the Prolog environment, and the partial evaluator is applied to it with respect to given parameter settings. A residual program is eventually created. Should this program be incomplete, it is made complete by adding to it required clauses from the original general program. Then, using predicative programming, the derived predicate is compiled back into Bruce, resulting in a transformed, optimized Bruce program. Our partial evaluator takes the form of a meta-interpreter written in CProlog, and is based on implementations in [Venken 85], [Takeuchi etal. 85], and [Pereira etal. 87]. The core of the evaluator is in figure 6.1. The first clause of mix partially evaluates conjunctions of goals, the results of which are combined together. Clause (2) executes goals which have been determined to be builtin by the builtinjexecutable utility. Examples of such goals are the boolean and relational operators used in Bruce tests. Clause (4) solves goals by unifying a goal with a clause, and partially evaluating the resulting body. CProlog's clause utility automatically unifies the goal with a clause each time clause succeeds. The most difficult problem faced when partially evaluating a program is determining when to inhibit the partial evaluation process. Goal inhibition is done in clause (3) of mix by the inhibited utility (see figure 6.2). Our system provides both automatic and user-controlled goal inhibition. Builtin goals and subprogram calls are inhibited by the first two clauses of inhibited. Another automatic feature checks that the variables used in CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 62 %(l) split multiple goals mix((Goal, Rest), Result,Recur) : — i mix(Goal, G Result, Recur), mix(Rest, RResult, Recur), fuse((G Result, RResult), Result). %(2) execute builtin's mix(Goal,true,J) : — builtin jexecutable(Goal), i Goal. %(3) halt interpretation mix (Goal, Goal, Recur) : — inhibited(Goal, Recur), \. %(4) interpret goal mix(Goal, Result, Recur) : — clause(Goal, Body), mix(Body, Result2, [Goal\Recur]), setjmixjresult(Result2, Result). Figure 6.1: Partial evaluator CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 63 %(1) builtin goals inhibited(Goal,_) :— builtin(Goal), %(2) subprogram calls inhibited(Goal,J) : — functor(Goal, Name, _), storematch(N ame, _, _, _, _), t. %(3) key variables are uninstantiated inhibited(Goal, _) : — not varJnst(Goal), j, %(4) loop detected inhibited(Goal, Recur) : — member3(Goal, Recur), I. %(5) no clause for goal inhibited(Goal, _) : — not clause(Goal,S), i Figure 6.2: Goal inhibition CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 64 a loop test are ground before that loop is unfolded (clause (3) of inhibited). When a Bruce program is initially parsed, a record is kept of the variables used by the test expression of each if statement and loop. The partial evaluator uses this information to inhibit goals corresponding to these constructs should their test variables be uninstantiated. The fourth clause of inhibited checks for loops. Finally, any goal which cannot be unified with a clause is inhibited. In addition to these five strategies, the user is allowed to enforce his or her own inhibition schemes simply by asserting into Prolog their own inhibited clause. This is vital when the program contains complex looping mechanisms caused by the use of branches. It is also possible for the user to override any automatic inhibition strategy. 6.3 Example transformations Figure 6.3 has a Bruce program power which computes integral powers using a binary power algorithm (from [Ershov 82]). The two varinst clauses, generated during parsing, are used to indicate to the partial evaluator when to inhibit the clauses corresponding to the two loops in the program. Both clauses specify that the third data object (the value parameter n) must be instantiated before partially evaluating the loops. When power is partially evaluated with respect to n = 5, partial execution yields the residual logic program and Bruce program in figure 6.4. Note that a side effect of partial evaluation is that some vector values become ground. When converting such a relation back into Bruce, the ground terms implicitly represent assignments of constants to variables. Partially evaluating power with both x — 2 and n = 5 produces a program which simply sets the output parameter to the result (figure 6.5). An example of code simplification is the binary gcd program of figure 6.6 (from [Knuth 81]). We assert goal inhibition clauses specifying that u must be ground before the label pro grams 61 and 62 are unfolded, and t must be ground before 64 is unfolded. Evaluating the program with u = 7 results in a residual program which is somewhat simpler than the original, though not a great deal more efficient. The logical form of bingcd and its transformed equivalent can be found in appendices C and D respectively. CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 65 power([y],[x,n]) : { y:= 1; while (n > 0) { while (((n//2) * 2) = n := n//2; x := x * x }; n := n — 1; y := y * a: } } := n){ power([Yl,Xl,Nl],[Y2,Xl,Nl]) :-asgn([Yl,Xl,Nl],Y3,l,[Y2,Xl,Nl]), while2([Y3, XI, Nl], [Y2, X2, N2]). whilel([Yl,Xl,Nl],[Y2,X2,N2]) : -Nl/12*2=:= Nl, asgn([Yl,Xl,Nl],N3,Nl//2,[Yl,Xl,N3]), asgn([Yl,Xl,N4],X3,Xl*Xl,[Yl,X3,N3]), whilel{[Y I, X3, N3], [Y2, X2, N2]). whilel([Yl,Xl,Nl],[Yl,Xl,Nl}) :--iVl//2*2=:= Nl. while2([Yl,Xl,Nl],[Y2,X2,N2]) : -Nl > 0, whilel([Yl,Xl, Nl], [Y3, X3, N3]), asgn([Y3,X3,N3],N4, N3 - I, [Y3,X3,N4]), asgn([Y3,X3,N4],Y4, Y3 * X3, [Y4,X3,N4\), while2([Y4, X3, N4], [Y2, X2, N2]). while2([Yl,Xl,Nl],[Yl,Xl,Nl]) : --.JV1 > 0. varinst(whilel, [f, f, i]). varinst(while2, [f, f,i]). Figure 6.3: Binary powers power([Yl,Xl,5],[Y2,Xl,5]) : -asgn([l,Xl,4],Y3,l * XI,[y3,Xl,4]), a5ffn([y3,Xl,2],X2,Xl *X1,[F3,X2,2]), asgn([Y3,X2, l],X3,X2 * X2, [Y3,X3,1]), asgn([Y3, X3,0], Y2, Y4 * X3, [Y2, X3,0]). power2([y],[x,n]): { 1 * x; x * x; y * x Figure 6.4: Residual programs (n = 5) power([yi,2,5],[32,2,5]). Figure 6.5: Residual programs (x = 2,n = 5) power3([y],[x,n]) : { y := 32 } CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 66 bingcd([gcd], [u,v]) : local [k,p,t]{ k := 0; 61: i/ (((«//2) * 2) = \ = «) { goto 62 }; if (((v//2) * 2) = \ = u) { goto 62 }; k := k + 1; u := u//2; v := w//2; goto 61; 62: */(((«//2)*2) = \ = «) { t := 0 - v] goto 64 }; t := u; 63 : i := t//2; 64: *7(((t//2)* 2) =:=*){ 50/0 63 }; »7 (* > o) { u := t } e/se { •u := 0 - t }; t := u — v; i/(t = \ = 0){ <7o2o 63 }; ca// power([p], [2, A;]); gcd u*p } 6in£fcd([srcd], : /oca/ { t := 0 - v; u := 7; k := 0; iesM : if (((t//2) * 2) =:= t) { 63 : * := *//2; goto testA } e/se { if (t > 0) { u := f } e/se { v := 0 - * }; t := u — v; if (* = \ = 0){ goto 63 } else { call power([p],[2, k]); gcd := u * p } } } Figure 6.6: Binary gcd (u = 7) CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS p{[y,z],[x,cl,c2]) : local [rl,r2]{ if {x>z){ rl := cl + l; r2 := cl - 1 } else { rl := c2 - 1; 7-2 := c2 + 1 }; y:=y + rl; z := z + r2 } Figure 6.7: A suspended test p([7l,Zl,Xl,3,5],[72,Z2,Xl,3,5]) : -^Xl > ZI, asgn([7l,Zl,Xl,3,5,4,6],72,7l -f 4,[72,ZI,XI,3,5,4,6]), asgn([Y2, ZI, XI, 3,5,4,6], Z2, ZI + 6, [72, Z2, XI, 3,5,4,6]). p([7l,Zl,Xl,3,5],[72,Z2,Xl,3,5]) : -XI > ZI, as0n([7l,Zl,Xl,3,5,4,2],72,71 + 4, [72, ZI, XI, 3,5,4,2]), a55n([72,Zl,Xl,3,5,4,2],Z2,Zl + 2,[72,Z2,Xl,3,5,4,2]). Figure 6.8: Polyvariant logical result CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 68 P2([y,z],[x,cl,c2]) : local [rl,r2] { if [x > z) { y:=y + 4; z := z + 2 } else { y:=y + 4; z := z + 6 } } Figure 6.9: Polyvariant Bruce result Logic elegantly handles polyvariant computational schemes, which are simply those which entail partially evaluating the bodies of tests and loops whose tests have been sus pended. In logic, this is naturally handled by unfolding the suspended test's denning clauses, and retaining the suspended test expression as a goal. Figure 6.7 shows a Bruce program with a suspended test (assume x is undefined). Figure 6.9 shows the partially evaluated logical result for cl = 3 and c2 = 5, and its Bruce realization is in figure 6.3. Chapter 7 Discussion Comparisons are given between the work in this thesis and related work. This is followed by a general discussion of the thesis, along with future research possibilities. 7.1 Related work The Horn clause semantics we use is semantically founded on those given in [Hehner 84a] and [Hehner etal. 86], which in turn is similar in spirit with logics used in program ver ification [Burstall 69] [Floyd 67] [Hoare 69]. Hehner's semantics describe the behavior of most of Bruce - descriptions which we borrow, albeit in a simplified and stylistically altered form. We also extend the imperative constructs handled by including program branches and call-by-value subprogram arguments. Since Hehner uses his logical semantics to study general characteristics of programs and computation, his semantics is much more descrip tive than ours. His system has provisions for describing the evaluability of expressions, the termination of mechanisms, and the type checking of data. Our semantics ignores such features, as we are concerned with the representation of correct and terminating programs which are to be transformed. He also employs full first-order predicate calculus in his se mantics, whereas we use a subset of predicate calculus - Horn clauses. A stylistic difference between his system and ours is that he uses fairly informal naming schemes when describ ing syntactic entities of a program, where we explicitly represent syntactic constructs with 69 CHAPTER 7. DISCUSSION 70 uniquely named predicates. Moss also uses Horn clause logic to semantically describe imperative programs [Moss 81] [Moss 82]. The description of a language in his system takes the form of a sophisticated interpreter which fully describes the syntax and operational semantics of the language. The syntax is written using a metamorphosis grammar, which is closely akin to the DCTG we use. His semantic rules, like ours, take the form of pure Prolog predicates. However, the nature of his semantics differs substantially from ours. Moss's semantic methodology is very robust, as his prime motivation is to describe the complete syntax and operational semantics of different programming languages using pure Horn clause logic, thereby proving the utility and generality of Prolog's descriptive capabilities. A theory in his system is a set of axioms which fully describe the operational semantics of a language, and the domain of discourse of the theory is the universe of possible programs written in the language. Programs are translated into various first-order terms which take the form of convenient data structures. These terms are in turn manipulated by predicates describing various functions of the operational semantics for the language. The domain of discourse of his logical axioms is thus programs and their abstract operational components. He essentially creates pure Prolog interpreters for languages. Our semantics uses a lower level of abstraction than that of Moss, since a theory in our system describes the computational behavior of a single imperative program. We use logical axioms to represent the functionality of the program's components, and reserve as our domain of discourse the domains of the store and expressions. The immediate advantage of such a low level description of computation is the ability of mapping, in both directions, between the source language and logical representation. In addition, the close relationship between the axioms and program means that optimizations of the axioms directly reflect improvements in the corresponding imperative program. Clark and van Emden have used Horn clause logic for verifying flowcharts, which can be interpreted as low level representations of imperative computations [Clark etal. 81]. They describe a flowchart's control in terms of Horn clauses, and then use a technique CHAPTER 7. DISCUSSION 71 called consequence verification to prove various properties of the computation. The style of their semantics is very similar to ours. Their low level description of control relates to our semantics in that uniquely named predicates represent unique computational mechar nisms. In addition, they use logical variable renaming to describe updates to the store. However, their system is intended for use in program verification, so they make no attempt to associate their axioms with programming language constructs. Our methodology for partially evaluating imperative programs offers interesting com parisons with work done by Ershov [Ershov 82] [Ershov 85]. Ershov partially evaluates programs by symbolically executing them using an algebraic rewriting system. These rewriting rules are applied to the text of a program, and eventually yield a partially eval uated result. The meta-interpretation of our logical semantics very closely parallels the effects of his transformations. Analogies between the transformation system presented in [Ershov 85] and SLDNF resolution of Horn clause semantics are as follows: 1. Term reduction: Ershov reduces expressions by replacing a term by its domain value. In our system, this occurs when an asgn, callasgn or boolean test is resolved and the expression value obtained is carried forward in the computation by the input-output vectors in relations. 2. Variable reduction: Ershov uses variable reduction to carry an assigned value of a variable to other statements using that variable. In our system, Prolog's unification automatically "passes" the value of a variable among goals in a clause, and resolvents of a goal. 3. Assignment reduction: Ershov removes any assignment whose variable value has been distributed, throughout the code. Under SLD resolution, assignments (as with all goals) automatically "disappear" once they are resolved. 4. If and while loop reduction: These reductions are used to simulate the control of tests and loops. Again, SLD resolution parallels these operations. CHAPTER 7. DISCUSSION 72 In fact, the traces of program transformations given by Ershov are very analogous to goal traces obtained when executing our semantics in Prolog. We believe that our approach to the transformation of imperative programs has advan tages over Ershov's approach. The main strength of our formalism is that transformations performed on Horn clause semantics have semantic interpretations in logic. Performing program transformations in logic means that the transformations can be verified for cor rectness in logic itself: any valid logical manipulation of the axioms is guaranteed of being a correctness-preserving program transformation. We exploit this fact in this thesis by proving that our partial evaluation of Horn clause semantics is logically sound, since the partial evaluation of logic programs can be considered a pure logical transformation scheme [Lloyd etal. 87]. On the other hand, Ershov's transformation system does not have any strong formal semantic interpretation. Consequently, partial evaluation in his system is not formally proved to be correctness preserving. Our logical semantics offers a substantial improvement to previous techniques for poly variant partial evaluation, which entails partially evaluating the bodies of tests and loops whose tests have been suspended [Ershov 85] [Bulyonkov 84]. Previous handling of this has been by explicitly maintaining memory states of alternate computations, which is required by the underlying algebraic transformation scheme. In logic, this is handled by simply treating the test as a suspendable goal, which is retained during the meta-interpretation process. Separate memory states are automatically retained during the evaluation of dif ferent clauses, since memory states are explicitly stored as terms of the clauses. 7.2 Conclusions and further work We have illustrated the applicability of Horn clause logic as a tool for transforming imper ative programs. We described the semantics of a nontrivial imperative language using a relatively economical set of logical axioms. Using the predicative programming paradigm, direct translation between semantical representations and the source language is possible. This semantics is also ideally suited to many types of transformations, the one we presented CHAPTER 7. DISCUSSION 73 being partial evaluation. Our semantics are essentially a logical characterization of the operational semantics for Bruce. Our approach to the design of the semantics was to first define Bruce in terms of an abstract machine, and then create logical axioms for different Bruce constructs modelled on the behavior of Bruce's operational semantics. Whether this intermediate abstract def inition of Bruce was truly required is debatable, as the Horn clause definition of constructs is just as intuitive as the abstract operational definitions, if not more so. The semantics are also abstract enough that machine-dependent features of the language are minimized, preventing it from being as machine-oriented as other operational semantic systems. Our handling of branches in Bruce uses both logical semantics and algebraic seman tics. The logical semantics comes into play during the initial expansion of the program predicate, since we use the basic axiomatic definitions of program constructs during the expansion process. Distributing terms of the program predicate, as well as removing the control context of the branch, are essentially algebraic operations which are based on logi cal considerations. Our defense of this approach is that the formula of axiom derivation has become more complicated. When no branches exist, the surface structure of program statements directly define the axioms. With branches, we must use a more sophisticated inspection of the program syntax in order to derive the axioms. One possible extension of this work is to enhance the semantics to handle more complex imperative languages. The inclusion of complex data types would be a relatively straight forward extension, and would be especially useful given the preponderance of imperative programs using arrays and other data structures. A real test would be to derive a Horn clause semantics in the style of this work for an existing programming language such as Pascal. Worth investigation is whether this style of logical semantics is applicable to other heterogeneous programming paradigms, such as functional programs. Such research would be in effect searching for a general description of computation. It is likely that a more general semantics would have much more complex domains than that of ours, since other CHAPTER 7. DISCUSSION 74 programming paradigms treat programs as data much more easily than do imperative languages. Denotational semantics might therefore offer some insight into the semantic content of the domains of such a representation. In addition, algebraic semantics might play a role in denning a more generally applicable semantic formalism. Much of the textual processing which we do to our semantics, such as factoring, code distributing, and branch processing, are simple algebraic manipulations of the logical formulas. The manipulation of more complex semantic expressions might be more easily denned in terms of algebraic rules. However, it is advantageous to maintain a logical basis to the methodology, as predicate logic permits meaningful interpretations and analysis of the domains being described. This thesis offers some philosophical views on the disciplines of programming and pro gramming language design. An immediate result of this work is that imperative pro grams are easily described or simulated by logic programs. One might conjecture from this that logic programming subsumes imperative programming in terms of computational power. Logic programs are certainly capable of computing any Turing-computable func tion [Tarnlund 77]. However, a logic program interpreted as a logical theory is governed by the same principles of undecidability and effective computability as its imperative brethren [Boolos et al. 80]. We should instead surmise that logic programs subsume imperative ones in terms of descriptive power, since the logic program interpretation of our semantics uses a relatively limited subset of Prolog's full descriptive and computational capabilities. Prolog programs as written by Prolog programmers use much more complex unification schemes than those used in our semantics. In addition, "real" Prolog programs are often written nondeterministically, which means that arguments to predicates might be either input or output in nature. Our Horn clause semantics are strictly deterministic logic programs, being declarative descriptions of deterministic computations. Our semantics offers some insight into alternation trees and and/or models of program ming [Harel 80]. In a logic programming context context, an alternation tree description of computation is just a restatement of the inherent logical semantics of pure Prolog program. Logic programs can be interpreted as and/or trees (or alternation trees), in which clauses CHAPTER 7. DISCUSSION 75 of a predicate represent or-branches, and the goals of a clause represent and-branches. The tree itself is composed of alternate instances of and-nodes and or-nodes (hence the term alternation tree) in which and-nodes are the parents of or-nodes, and vice versa. A successful computation of the tree requires that all the and-nodes under an or-node must be successful before the or-node is successful; similarly, at least one or-node under an crod-node must be successful before that and-node succeeds. Besides having theoretical importance in the semantics of programming, the alternation tree interpretation of logic programs has applications in parallel processing [Shapiro 87]. The parallel execution of an and/or tree means that the or-nodes and arid-nodes of the tree all take the form of producers and consumers of data. The data path between the nodes is dependent on the particular variable usage in the Prolog program. Data transfer between the nodes is done through the unification process. Casting an imperative program into our Horn clause semantics means that an and/or model of computation is immediately defined for it. As with all pure logic programs, the alternation tree description of the Horn clause semantics of a Bruce program allows the direct derivation of an and/or model of computation. In addition, this alternation tree gives an initial parallel execution model for the program. However, a data flow analysis of the tree would probably be needed in order to derive an efficient model of parallel computation. Partial evaluation is a scheme which transforms a general program into a more spe cialized one. However, efficiency is gained at the expense of generality. The ideal goal of program transformation is to transform a program into a more efficient form without any loss of generality. Existing systems which do such transformations are unfortunately not very automatable. Nevertheless, it would be interesting to use our semantics in a more deductive transformational environment. It is likely that heuristics and user control would play a large role in such a transformation system. Another interesting application of our semantics is its use in a transformation system which transforms an input imperative pro gram into a more "stylized" version. Also worth attention is the use of our semantics in a program verification system, which would again rely on heuristic and user control. CHAPTER 7. DISCUSSION 76 Further work in controlling the partial evaluation of imperative programs is needed. In hibiting recursion on polyvariant computations is difficult to implement in our system. This can be overcome somewhat by partially evaluating each clause in the program predicate individually. However, it is not obvious how constant values can be elegantly propagated to these clauses using this scheme. Controlling the partial evaluation process seems to be a research topic problematic to the field of partial evaluation in general [Lloyd etal. 87]. Ershov expresses the need for a systems programming language (SPL) in which program transformation could be based [Ershov 82]. We believe that our technique offers a more solid semantic foundation for program transformation than his algebraic transformations, and claim that Horn clause logic using Prolog's execution model is a prime candidate for Ershov's SPL. First and foremost, pure Prolog has a well-founded underlying mathematical model, namely first-order predicate logic. Using logic immediately leads to the opportunity of using the many theoretical results, tools and techniques which have been established in mathematical logic throughout the years. In addition, using the predicative programming paradigm, there is a strong and natural relationship to the semantics of a language and its syntactic realization. Finally, Prolog has already proven its applicability in many systems programming applications, for example, [Abramson etal. 88], [Moss 81], and [Shapiro 83]. References [Abramson 84] H. Abramson. Definite Clause Translation Grammars. In Proc. Logic Programming Symp., IEEE, Atlantic City, New Jersey, Febru ary 1984. [Abramson etal. 88] H. Abramson, M. Crocker, B. Ross, and D. Westcott. A Fifth Generation Translator Writing System: Towards an Expert System for Compiler Development. In Fifth Generation Comp. Sys. Conf., IFIPS, Tokyo, Japan, 1988. submitted. [Allison 86] [Apt 81] [Ashcroft etal. 82] [Backus 78] [Beckman etal. 76] [Bibel 75] [Bibel 85] Lloyd Allison. A practical introduction to denotational semantics. Volume 23 of Cambridge Computer Science Texts, Cambridge Uni versity Press, 1986. K.R. Apt. Ten years of Hoare's logic: a survey. TOPLAS, 3:431-483, 1981. E.A. Ashcroft and W.W. Wadge. R for Semantics. ACM Transac tions on Programming Languages and Systems, 4(2):283-294, April 1982. John Backus. Can Programming Be Liberated from the von New-mann Style? CACM, 21(8):613-641, August 1978. L. Beckman, A. Haraldson, O. Oskarsson, and E. Sandewall. A par tial evaluator and its use as a programming tool. Artificial Intelli gence, 7:319-357, 1976. W. Bibel. Pradikatives programmieren. In GI - 2. Fachtagung uber Automatentheorie und Formale Sprachen, pages 274-283, Springer, 1975. W. Bibel. Predicative programming revisited. In Mathemati cal method of specification and synthesis of software systems '85, pages 25-40, Wendisch-Reitz, E. Germany, April 1985. 77 REFERENCES 78 [Boolos et al. 80] [Boyer et al. 79] [Broy 84] [Bulyonkov 84] [Burstall 69] [Clark etal. 81] [Clint etal. 72] [Clocksin etal. 81] [Cook 78] [Darlington etal. 73] [de Bruin 81] [Ershov 82] [Ershov 85] [Floyd 67] George Boolos and Richard Jeffrey. Computability and Logic. Cam bridge University Press, 1980. R.S. Boyer and J.S. Moore. A Computational Logic. ACM Mono graph Series, Academic Press, 1979. Manfred Broy. Algebraic Methods for Program Construction: The Project CIP. In P. Pepper, editor, Program Transformation and Programming Environments, pages 199-222, Springer-Verlag, 1984. M.A. Bulyonkov. Polyvariant Mixed Computation for Analyzer Pro grams. Acta Informatica, 21:473-484, 1984. R.M. Burstall. Formal Description of Program Structure and Se mantics in First Order Logic. In Michie Meltzer, editor, Machine Intelligence 5, pages 79-98, Elsevier, 1969. K.L. Clark and M.H. van Emden. Consequence Verification of Flowcharts. IEEE Transactions on Software Engineering, SE-7(l):52-60, January 1981. M. Clint and C.A.R. Hoare. Programming Proving: Jumps and Functions. Acta Informatica, 1:214-224, 1972. W.F. Clocksin and CS. Mellish. Programming in Prolog. Springer-Verlag, 1981. S.A. Cook. Soundness and completeness of an axiom system for program verification. SI AM Journal of Computing, 7(l):70-90,1978. J. Darlington and R.M. Burstall. A System which Automatically Improves Programs. In IJCAI, pages 479-485, XXX, 1973. A. de Bruin. Goto Statements: Semantics and Deduction Systems. Acta Informatica, 15:385-424, 1981. Andrei P. Ershov. Mixed Computation: Potential Applications and Problems for Study. Theoretical Computer Science 18, 18:41-67, 1982. Andrei P. Ershov. On Mixed Computation: Informal Account of the Strict and Polyvariant Computational Schemes. In M. Broy, editor, Control Flow and Data Flow: Concepts of Distributed Programming, pages 107-120, Springer-Verlag, 1985. R.W. Floyd. Assigning Meanings to Programs. In Proc. Symp. Appl. Math., pages 19-32, Amer. Math. Soc, 1967. REFERENCES 79 [Futamura 71] [Gordon 79] [Guessarian 81] [Harel 80] [Hehner 84a] [Hehner 84b] [Hehner et al. 86] [Hoare 69] [Hoare 85] [Hoare etal. 73] [Jones etal. 85] [Kernighan etal. 78] [Knuth 81] [Lloyd 84] [Lloyd et al. 87] Y. Futamura. Partial evaluation of computation process - an ap proach to a compiler-compiler. Systems - Comput. - Controls, 2(5):45-50, 1971. M. Gordon. The Denotational Description of Programming Lan guages. Springer-Verlag, New York, 1979. Irene Guessarian. Algebraic Semantics. Volume 99 of Lecture Notes in Computer Science, Springer-Verlag, 1981. David Harel. Ans/Or Programs: A New Approach to Structured Programming. ACM Transactions on Programming Languages and Systems, 2(l):l-17, January 1980. Eric C.R. Hehner. Predicative Programming Part I. 27(2):134-143, February 1984. CACM, Eric C.R. Hehner. Predicative Programming Part II. CACM, 27(2), February 1984. Eric C.R. Hehner, Lorene E. Gupta, and Andrew J. Malton. Pred icative Methodology. Acta Informatica, 23:487-505, 1986. C.A.R. Hoare. An Axiomatic Basis for Computer Programming. CACM, 12(10):576-583, October 1969. C.A.R. Hoare. Programs are Predicates. In C.A.R. Hoare and J.C. Shepherdson, editors, Mathematical Logic and Programming Lan guages, pages 141-155, Prentice-Hall, 1985. C.A.R. Hoare and N. Wirth. An axiomatic definition of the pro gramming language PASCAL. Acta Informatica, 2:335-355, 1973. N.D. Jones, P. Sestoft, and H. Sondergaard. An Experiment in Par tial Evaluation: the Generation of a Compiler Generator. SIGPLAN Notices, 20(8):82-87, August 1985. B.W. Kernighan and D.M. Ritchie. The C Programming Language. Prentice-Hall, 1978. Donald E. Knuth. Seminumerical Algorithms. Volume 2 of The Art of Computer Programming, Addison-Wesley, 2nd edition, 1981. J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1984. J.W. Lloyd and J.C. Shepherdson. Partial Evaluation in Logic Pro gramming. Technical Report CS-87-09, University of Bristol, Decem ber 1987. REFERENCES 80 [Loeckx etal. 84] [Loveman 77] [Manna etal. 77] [Moss 81] [Moss 82] [O'DonneU 82] [Partsch et al. 83] [Pepper 84] [Pereira etal. 84] [Pereira etal. 87] [Robinson 65] [Shapiro 83] [Shapiro 87] [Stoy 77] [Takeuchi etal. 85] J. Loeckx and K. Sieber. The Foundations of Program Verification. Wiley-Teubner, 1984. D. B. Loveman. Program Improvement by Source-to-Source Trans formation. JACM, 24(1):121-145, January 1977. Zohar Manna and Richard Waldinger. Studies in Automatic Pro gramming Logic. Elsevier North-Holland, 1977. Christopher D.S. Moss. The Formal Description of Programming Languages using Predicate Logic. PhD thesis, Imperial College, Lon don, U.K., July 1981. Christopher D.S. Moss. How to Define a Language Using Prolog. In Conference Record of the 1982 ACM Symposium on Lisp and Func tional Programming, pages 67-73, ACM, 1982. M.J. O'DonneU. A Critique of the Foundations of Hoare Style Pro gramming Logics. CACM, 25(12):927-935, December 1982. H. Partsch and R. Steinbruggen. Program Transformation Systems. Computing Surveys, 15(3):199-236, September 1983. P. Pepper, editor. Program Transformation and Programming Envi ronments. Springer-Verlag, 1984. F. Pereira, D. Warren, D. Bowen, and L. Pereira. C-Prolog User's Manual, version 1.5 edition, November 1984. Fernando C.N. Pereira and Stuart M. Shieber. Prolog and Natural-Language Analysis. Volume 10 of CSLI Lecture Notes, CSLI, 1987. J.A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. JACM, 12(1):23-41, January 1965. E. Y. Shapiro. Systems Programming in Concurrent Prolog. Techni cal Report TR-034, ICOT, Tokyo, Japan, November 1983. Ehud Shapiro. Concurrent Prolog vol. 1 and 2. MIT Press, 1987. J. Stoy. Denotational Semantics. MIT Press, 1977. A. Takeuchi and K. Furukawa. Partial Evaluation of Prolog Pro grams and its Application to Meta Programming. Technical Re port TR-126, ICOT, Tokyo, Japan, July 1985. [Tarnlund 77] S. Tarnlund. Horn Clause Computability. BIT, 17:215-226, 1977. REFERENCES 81 [Tennent 77] R.D. Tennent. Language Design methods Based on Semantic Prin ciples. Acta Informatica, 8:97-112, 1977. [Tennent 81] R.D. Tennent. Principles of Programming Languages. Prentice-Hall, 1981. [van Emden etal. 76] M.H. van Emden and R.A. Kowalski. The Semantics of Predicate Logic as a Programming Language. JACM, 23(4):733-742, October 1976. [Venken 85] Raf Venken. A Prolog Meta-Interpreter for Partial Evaluation and its Application to Source to Source Transformation and Query Op timisation. In T.O'Shea, editor, Advances in Artificial Intelligence, pages 347-356, Elsevier Science Publishers B.V. (North Holland), 1985. [Wirth etal. 78] Niklaus Wirth and Kathleen Jensen. Pascal User Manual and Re port. Springer-Verlag, 2d edition, 1978. Appendix A Partial Evaluator Source % *** % *** Mixed Computation routines % *** % *** - Brian J. Ross % *** Dept. of Computer Science % *** University of British Columbia % *** % % mix(Goal,Mixed): % Goal — top goal to mix (with parameter settings) % Mixed — Mixed Prolog result % % mix/2 finds the Prolog result, given a top level goal. % A Prolog program must be asserted in the Prolog environment before this % routine can run. The steps taken are: % 1. Find the mixed result using topjnixer % 2. Clean up the result from topjnixer. % 3. Add Prolog predicates to make the resulting program complete. mix(Goal,Mixed) : — setof( Results,Goal" top_mixer(Goal,Results),P), add_old_prolog(P,Mixed), % % top_mixer(Goal,Result): 82 APPENDIX A. PARTIAL EVALUATOR SOURCE % Goal — top goal to mix % Result — resulting mixed Prolog program % % topjnixer drive the mixed computation. top_mixer(Goal,Result) :— clause(Goal,Body), mix(Body,Result2,[Goal]), set_mix_result (Result2 ,Result 3), set_mix_ans( Goal,Result3,Result). % % set_mix_ans(A,B,C): % A — Goal which has been mixed % B — mixed result % C —the form of the result to be passed back to calling program % % set_mix_ans simply formats the result of the mixed computation % the form of a Prolog program. set_mix_ans(Goal,true,Goal) :— !. set_mix_ans(Goal,(_:—true),Goal) :— !. set_mix_ans(Goal,A,(Goal:—A)) :— !. % % mix(Goals,Result,Recur): % Goals — Goals to be mixed % Result — Mixed result % Recur — recursion list % % mix/ 5 is the core of the mixed computation utility. % It is a meta—interpreter which executes the Goals under the current Prolog % environment. The algorithm used simply tries to solve the Goals, halting % further interpretation when Goal inhibition conditions are satisfied: % 1. The goal is a builtin predicate, but it has uninstantiated % variables which prevent it from being executed. % 2. The goal has uninstantiated variables which must be % instantiated according to the 'var_inst' clause. % 3. The goal occurs in the recursion list — a loop las been detected. % 4- No clause exists for solving the goal. % Whenever one of these conditions arise, the goal is saved as a mixed result. APPENDIX A. PARTIAL EVALUATOR SOURCE 84 mix((Goal,Rest),Result,Recur) :— I •> mix(Goal,GResult,Recur), mix(Rest,RResult,Recur), fuse((GResult,RResult),Result). mix(Goal,true,_) :— builtin_execut able( Goal), I Goal. % split multiple goals % execute builtin's mix(Goal,Goal,Recur) :— inhibited(Goal,Recur), % halt interpretation mix(Goal,Result,Recur) :— clause(Goal,Body), mix(Body,Result2,[Goal|Recur]), set_mix_result (Result2,Result). % interpret goal % % set_mix_result(A,B): % A — Mixed result % B — returned result % % setjnixjresult reformats the mixed result. set_mix_result((_:—A),A) :— !. set_mix_result(A,A) :— !. % % inhibited(Goal,Recur): % Goal — current Goal being interpreted % Recur — Current recursion list % % inhibited checks if any Goal inhibition condition exists. mhibited(Goal%_) :- builtm(Goal),! inhibited(Goal^) :— functor(Goal,Name,_), storematch(Name,_,_,_,_), APPENDIX A. PARTIAL EVALUATOR SOURCE inhibited(Goal,_) :— not varjnst(Goal),!. inhibited(Goal,Recur) :— member3(Goal,Recur),!. inhibited(Goal^) :— not clause(Goal,_),!. % :  % unknown_vars(Goal): % Goal — current goal being interpreted % % unknownjvars checks if the builtin Goal has any uninstantiated variables % as part of its executable structure (tests, expressions). unknown_vars(asgn(_,_,E,_)) :— i •> extract vars(E,F), F \== []. unknown_vars(callasgn(_,_,E)) :— i extract vars(E,F), F \== []. unknown_vars(Test) :— is_a_test(Test), i •i extract vars(Test,F), F \==" []. % % executable_builtin tests if a goal is builtin and executable. % This may be specialized for individual builtin utilities in the future. builtin_executable(Goal) :— builtin(Goal), not unknownvars(Goal), I. % % builtin goal list: builtin(true) :- !. builtin(asgn(_,_^J) :- !. builtin(callasgn(_,_,_)) :- !. builtin(Test) :- is_a_test(Test), !. APPENDIX A. PARTIAL EVALUATOR SOURCE % % varJnst(Goal): % Goal — current goal being interpreted % % var_inst takes Goal and compares its input vector with the variable % instantiation flag settings in the Goal's corresponding var_inst clause. % Each variable in the input vector corresponding to a "i" (instantiated) % setting must be an instantiated/ground variable; else failure. varJnst(Goal) :— Goal =.. [Name,Vec|J, var_inst(Name,Inst), i •> var_inst2(Vec,Inst). var_inst(_). var_inst2([],Q). var_inst2([_|R],[f|S]) :-i var_inst2(R,S). var_inst2([V|R],[i|S]) :-i nonvar(V), var_inst2(R,S). % : % add_old_prolog(Mixed,New): % Mixed — mixed Prolog program % New — Mixed with added Prolog to make it complete % % addjoldjprolog/ 2 completes the mixed prolog program. add_old_prolog(Mixed,New) :-add_old_prolog(Mixed,Mixed,[],New). % % add_old_prolog(Mixed, Clauses,Done,Ans): % Mixed — Mixed result so far % Clauses — clauses yet to check for completeness % Done — names of predicates completed so far % Ans — final result APPENDIX A. PARTIAL EVALUATOR SOURCE % % add_old_prolog/4 adds to the current Prolog program in Mixed clauses from % the Prolog environment to make it complete. It calls add_old_prolog2 on the % list of goals in each clause of Clause, until all of Clause has been % processed. The names of the predicates completed are stored in Done. add_old_prolog(Mixed,[],_,Mixed). add_old_prolog(Mixed,[A|R],Done,S) :— split_clause(A,u,Goals), add_old_prolog2(Mixed,Goals,Done,Done2,More), Mixed \== More, add_old_prolog(More,More,Done2,S). add_old_prolog(Mixed, [A | R] ,Done,S) :— add_old_prolog( Mixed ,R,Done,S). % ; % add_old_prolog2(Mixed, Goals, OldDone,NewDone,Ans): % Mixed — Current mixed program % Goals — goal list to process % OldDone — predicates processed so far % NewDone — all the predicates processed after Goals processed % Ans — final result % % add_old_prolog2 completes the Prolog program Mixed with respect to the % goal list Goals. Should a partially ground goal not have a corresponding % partially ground header in Mixed, the general predicate is copied from % the Prolog environment and added to Mixed. The name of the predicate is % saved to avoid duplication later. add_old_prolog2(Mixed,0,Done,Done,Mixed). add_old_prolog2(Mixed,[Goal|Rest],Done,Done2,More) :— not builtin(Goal), functor(Goal,Name,_), member(Name,Done), i add_old_prolog2(Mixed,Rest,Done,Done2,More). add_old_prolog2(Mixed,[Goal|Rest],Done,Done2,More) :— not builtin(Goal), APPENDIX A. PARTIAL EVALUATOR SOURCE 88 not head_exists(Goal,Mixed), i •> setof( Clause ,get_clause(Goal,Clause),More2), append(Mixed,More2,More3), functor(Goal,Name,_), add_old_prolog2(More3,Rest,[Name|Done],Done2,More). add_old_prolog2(Mixed,[_|Rest],Done,Done2,More) :— add_old_prolog2(Mixed,Rest,Done,Done2,More). % \ % get_clause(Goal,Clause): % Goal — (possibly partially) ground goal % Clause — a general clause matching Head % % get_clause retrieves a clause to solve Head without unifying anything in % Head. get_clause(Goal,(Template:—Body)) :— functor(Goal,Name,Arity), current_predicat e( Name ,Template), functor(Template,Name,Arity), clause(Template,Body). % % head_exists(Goal,Clauses): % Goal — partially ground goal % Clauses — Prolog clauses % % head_exists tests if a clause with a partially ground head corresponding to % Head exists in Clauses. head_exists(Goal,[(H:-B)|Rest]) :-ground_eq( Goal ,H). head_exists(Goal,[_|Rest]) :— head_exists(Goal,Rest). Appendix B Bruce Parser % *** % *** Bruce parser and predicate generator % *** % *** _ Brian J. Ross % *** Dept. of Computer Science % *** University of British Columbia % *** % % This DCTG grammar contains the Bruce syntax. % (BRUCE: Brian Ross's Unfriendly Computation Environment) % The semantic portions allow compilation of a Prolog equivalent for the % Bruce program being parsed. % This grammar expects a list of lexical tokens, as is generated by Westcott's % lexical analyzer. % % The semantics produce a list whose elements are Prolog clauses. % The usual structures being passed through the semantics are: % Code — the code for this construct % In — the initial variable vector % Out — the output variable vector % Defns — list of Prolog code created through the parsing of a construct % Extra arguments are described where appropriate. env ::= prog""P, env"E <:> code(Code) ::— 89 APPENDIX B. BRUCE PARSER P"*code(C), E""code(Defns), append(C,Defns,Code). env ::= Q <:> code([]). prog ::= prog_header""P, ['{'], chain""Q, ['}'] <:> code(Code) ::— gen_prog(Code,P,Q). progjieader ::= label""!, ['('], var_list""V, [','], var_list""E, [')',':'], decls""D <:> code(P,VI,EI,Locals,Evars,In,Out) ::-gen_headercode(P,VI,EI,Locals,In,Out,Evars,L,V,E,D,Proglabel), newJabellist(Proglabel). decls ::= ['local'], var_list*"L <:> code(Code) ::— L""code(Code). decls ::= [] <:> code(Q). chain ::= stat""S, [';'], chain""Q <:> code(Code,In,Out,Defns) ::— gen_chain(Code,In,Out,Defns,S,Q). chain ::= stat""S <:> code(Code,In,Out,Defns) ::- S""code(Code,In,Out,Defns). chain ::= label"*L, [':'], stat""S, [';'], chain""Q <:> code((label(Label),Code),In,Out,Defns) ::— gen_chain(Code,In,Out,Defns,S,Q), L" "code(Label), APPENDIX B. BRUCE PARSER add_curr_labellist(label,Label). chain ::= label**L, [':'], stat"*S <:> code((label(Label),Code),In,Out,Defns) ::-S* "code(Code,In,Out,Defns), L" "code(Label), add_curr_labellist(label,Label). % % The following are calls to the statement constructs stat ::= test""S <:> code(Code,In,Out,Defns) ::— S" *code(Code,In,Out,Defns). stat ::= proc_cair*S <:> code(Code,In,Out,Defns) ::— S""code(Code,In,Out,Defns). stat ::= while* "S <:> code(Code,In,Out,Defns) ::- S""code(Code,In,Out,Defns). stat ::= repeat" *S <:> code(Code,In,Out,Defns) ::— S" Acode(Code,In,Out,Defns). stat ::= branch" "S <:> code(Code,In,Out,Defns) ::— S" "code(Code,In,Out,Defns). stat ::= skip**S <:> code(Code,In,Out,Defns) ::— S"*code(Code,In,Out,Defns). stat ::= assignment*AA <:> code(Code,In,Out,Defns) ::- A**code(Code,In,Out,Defns). % % The following are rules which create Prolog construct. APPENDIX B. BRUCE PARSER 92 skip ::= [skip] <:> code(skip(In,In),In,In,[]). assignment ::= laber*V, [': = '], any_expr"*E <:> code(Code,In,Out,Defns) ::— gen_asgn(Code,In,Out,Defns,V,E). test ::= ['if','('], bool_expr" "B, chain*"Ql, ['}'], [else,'-C»], chain**Q2, ['}'] <:> code(Code,In,Out,Defns) ::— gen_testcode(Code,In,0ut,Defns,B,Ql,Q2,If_label), add_curr_labellist(if,If_label). test ::= ['if,'('], bool_expr""B, [')','{'], chain""Ql, ['}'] <:> code(Code,In,Out,Defns) ::— gen_testcode(Code,In,Out,Defns,B)Ql)'' ,H_label), add_curr_labellist(if,If_label). proc_call ::= [call], label"*P, ['('], vax_list""V, [','], expr_outputs**E,[')'] <:> code(Code,In,Out,Q) ::— gen_callcode(Code,In,Out,P,V,E). while ::= [while,'('], bool_expr*"B, [')','{'], chain*"Q, ['}'] <:> code(Code,In,Out,Defns) ::— gen_whilecode(Code,In,Out,Defns,B,Q,Loop_label), add_curr_labellist(while,Loop_label). repeat ::= [repeat,'{'], chain"*Q, ['}',until,' ('], bool_expr""B, [')'] <:> code(Code,In,Out,Defns) ::— gen_repeatcode(Code,In,Out,Defns,B,Q,Loop_label), add_curr_labellist(repeat,Loop_label). branch ::= [goto], label""L <:> APPENDIX B. BRUCE PARSER code(Code,In,Out,[]) ::— gen_goto(Code,In,Out,L), goto_found. % % Some miscellaneous expression rules ... label ::= [id(Name)] <:> code(Name). any_expr ::= expr""E <:> code(Expr,In) ::- E*"code(Expr,In). any_expr ::= bool_expr""B <:> code(Expr,In) ::— B""code(Expr,In). bool_expr ::= [true] <:> code(true,_). bool_expr ::= [false] <:> code(false,_). bool_expr ::= label" "V <:> code(Code,In) ::- V""code(Name),var_match(Name,In,Code). bool_expr ::= ['('], any_expr""A, relop""B, any_expr*"C, [')'] <:> code((E),In) ::- A""code(El,In), B""code(E2), C" "code(E3,In), E =.. [E2,E1,E3]. bool.expr ::= ['('], bool_expr""A, binbool_op""B, bool_expr""C, <:> code((E),In) ::- A""code(El,In), B""code(E2), C""code(E3,In), E =.. [E2,E1,E3]. bool_expr ::= ['(','"'], bool_expr""A, [')'] APPENDIX B. BRUCE PARSER 94 <:> code("(E),In) ::- A~code(E,In). expr ::= ['('], expr" "A, math_op""B, expr""C, [')'] <:> code((E),In) ::- A""code(El,In), B""code(E2), C" "code(E3,In), E =.. [E2,E1,E3]. % E2 should be defined as a CProlog operator expr ::= [const(Num)] <:> code(Num,_). expr ::= label* "V <:> code(Code,In) ::- V*"code(Name),var_match(Name,In,Code). binbool_op ::= [bool(C)] <:> code(C). relop ::= [rel(C)] <:> code(C). mathpp ::= [math(C)] <:> code(C). % % Lists... % A list of variable labels ... varjist ::= ['['], labeljist""V, [»]'] <:> code(Code) ::— V" "code(Code). % A list of expressions, with appropriate logical variable substitutions... expr_outputs ::= ['['], exprjist""V, [']'] <:> code(Code,In) ::- V""code(Code,In). APPENDIX B. BRUCE PARSER 95 % Generates a label list... labeljist ::= label* "L, [','], labeljist""V <:> code([Label|Labels]) ::- L**code(Label), V"*code(Labels). labeljist ::= label* *L <:> code([Label]) ::— L* *code(Label). labeljist ::= [] <:> code([]). % Generates an expression list ... exprjist ::= expr""E, [','], expr_list""L <:> code(Code,In) ::— E""code(Expr,In), L* *code(Elist,In), append( [Expr] ,Elist ,Code). exprjist ::= bool_expr""B, [','], exprjist""L <:> code(Code,In) ::— B" *code(Expr,In), L""code(Elist,In), append( [Expr] ,Elist,Code). exprjist ::= expr""E <:> code([Code],In) ::- E" *code(Code,In). exprjist ::= bool_expr""B <:> code([Code],In) ::— B""code(Code,In). exprjist ::= [] <:> code( [],_). APPENDIX B. BRUCE PARSER % % Some semantic primitives % asgn(In,Var,Expr,Out) is satisfied by evaluating Expr and saving the value % in logical variable Var, where In contains input values which may be % needed by Expr, and Out is the final output value (variant with logical % variable Var changed). asgn(In,Var,Expr,Out) :— value(Expr,Var). % callasgn(In, Var,Expr) evaluates Expr, saving the value in Var. % The In vector is not directly used. % This is needed to pass expression values in procedure calls. callasgn(In,Var,Expr) :— value(Expr,Var). % skip always succeeds. skip(_,_). skip_branch(_,Dest,_) :- writel(nl,'Ignoring branch to ',Dest,nl). % label inserts do nothing... labelfj. % % Prolog code construction ... % These routines construct Prolog code for the particular constructs % in question. In doing so, they may call semantic portions of the % tree. The code from these calls, if any, is passed back in Defns. % % gen_prog(Code,P,Q): % P — points to header portion of tree % Q — points to main program chain % % Returns in list Code: % p(In,Out) :— Body PLUS definitions for rest of program APPENDIX B. BRUCE PARSER 97 gen_prog(Code,P,Q) :-P"code(Header,VJnp,Ejnp,Locals,Evars,In,Out), Q-*code(Body,In,02,Defns), gen_vec( V_inp ,X 1), append(Xl,Evars,Out), append(Xl,_,02), Pgm =.. [(:-),Header,Body], append([Pgm],Defns,Code). % % genjieadercode (Code, VI, EI, Locals, In, Out, Evars, L, V, E, D, Prog): % Asserts storematch(Prog)B,VI)EI,LOC) % where Prog — program name, % B — label list of var params, val params, and locals resp. % VI — label list of var params % EI — label list of val params % Locals — label list of locals gen_headercode(Code,VI,EI,Locals,In,Out,Evars,L,V,E,D,Prog) :— I/"code(Prog), V"code(VI), E~code(EI), Dcode(Locais), append_list([VI,EI,Locals] ,Varnames), gen_vec( VI ,1 vars), gen_vec(EI,Evars), gen_vec(Locals,Lvars), append(Ivars,Evars,HeaderInp), append(HeaderInp,Lvars,In), Code =.. [Prog,HeaderInp,Out], tassert(storematch(Prog,Varnames,VI,EI,Locals)). % gen_testcode(Code,In,Out,Dems,B)Ql)'' ,Label) :— gen_vec(In,Out), B""code(Booltest,In), Ql" *code(Chainl,In,02,D2), gen_label(test,Label), Code =.. [Label,In,Out], Testhead =.. [Label,In,02], Testhead2 =.. [Label,In,In], APPENDIX B. BRUCE PARSER 98 copy((Testhead :— (Booltest,Chainl)),Testl), copy((Testhead2 :- "(Booltest)),Test2), append([Testl,Test2],D2,Defns). gen_testcode(Code,In,Out,Defns,B,Ql,Q2,Label) :— Q2 \== gen_vec(In,Out), B"*code(Booltest,In), Ql""code(Chainl,In,02,D2), Q2" "code(Chain2,In,03,D3), gen_label(test,Label), Code =.. [Label,In,Out], Testheadl =.. [Label,In,02], Testhead2 =.. [Label,In,03], copy((Testheadl :- (Booltest,Chainl)),Testl), copy((Testhead2 :- (~(Booltest),Chain2)),Test2), append([Testl,Test2],[D2|D3],Defns). % gen_whilecode(Code,In,Out,Defns,B,Q,Label) :-gen_vec(In,Out), gen_vec(In,03), B""code(Booltest,In), Q""code(Chainl,In,02,D2), genjab el( while ,L abel), Code =.. [Label,In,Out], Loopheadl =.. [Label,In,03], Loophead2 =.. [Label,In,In], Loopcall =.. [Label,02,03], copy((Loopheadl :— (Booltest,Chainl,Loopcall)),Loopl), copy((Loophead2 :— "(Booltest)),Loop2), gen_var_inst(Label,Booltest,In,Var_inst), append([Loopl,Loop2,Var_inst],D2,Defns). % % gen_repeatcode(Code,In, Out,Defns,B,Q): gen_repeatcode(Code,In,Out,Defns,B,Q,Label) :— gen_vec(In,Out), gen_vec(In,03), B""code(Booltest,02), APPENDIX B. BRUCE PARSER 99 0/ *code(Chainl,In,02,D2), gen_label(repeat, Label), Code =.. [Label,In,Out], Loopheadl =.. [Label,In,03], Loophead2 =.. [Label,In,02], Loopcall =.. [Label,02,03], copy((Loopheadl :— (Chainl,~(Booltest),Loopcall)),Loopl), copy((Loophead2 :— (Chainl,Booltest)),Loop2), gen_var_inst(Label,Booltest,In,Var_inst), append([Loopl,Loop2,Var_inst],D2,Defns). % gen_callcode(Code,In,Out,P,V,E) :-P*"code(Proc), V"-code(VUst), E""code(Elist,In), match_vars( Vlist ,In,Call_iiivars), % gen_vec(Vlist,I2), % append(I2,I3,In), set_expressions(In,Elist,Call_invals,Ecode), set_expressions(I3 ,Elist ,Call_invals,Ecode), append( Calljnvars ,Call_invals,In_args), gen_vec(In_args,Out_args), set_outputs(In, Calljnvars, 0ut_args,0ut), Call =.. [Proc,In_args,Out_args], (Ecode == " -> Code = Call; fuse((Ecode,Call),Code)). gen_asgn(asgn(In,Var_f,Expr,Out),In,Out,[],V,E) :— V" "code(Vname), E""code(Expr,In), var_match( Vname ,In ,Var_i), vec_variant (In, Varj ,Var_f ,0ut). % gen_chain(Code,In,Out,Defns,S,Q) :— S""code(Sl,In,X,Dl), Q""code(S2,X,Out,D2), APPENDIX B. BRUCE PARSER fuse((Sl,S2),Code), append(Dl,D2,Defns). % % gen_goto(Code,In,Out,L): % Code — goto construct % In — input variable vector % Out — output variable vector % L — points to label gen_goto(goto(In,Label,Out),In,Out,L) :— L"*code(Label), gen_vec(In,Out). % % set_expressions(In,Elist,Call_invals,Ecode) converts expressions in Elist % into callasgn statements in Ecode. Calljnvals are the variables created % to assign the expression values to before the call. se^expressions^^Q,''). set_expressions(In,[VarA|A],[VarB | B] ,D) :— var(VarA), set_expressions(In,A,B,C), fuse((callasgn(In,VarB,VarA),C),D). set_expressions(In,[Expr|A],[Var|B],C) :— set_expressions(In,A,B ,D), (D = " -> C = callasgn(In,Var,Expr); C = (callasgn(In,Var,Expr),D)). % % gotojound asserts 'found_a_branch' if a branch is detected during % parsing. goto_found :— found_a_branch,!. goto_found :— tassert(found_a_branch). % % gen_var_inst generates an instantiation vector for a construct. % This vector simply states which variables are used in the constructs % test, which is used by the mixer later. APPENDIX B. BRUCE PARSER 101 gen_var_inst(Label,Test,Vec,var_inst(Label,Inst)) :-ext rac t_vars( Tes t ,T vars), gen_var_inst2(Tvars,Vec,Inst), j, % % gen_var_inst2 creates a Flags vector which consists of letters '%' and % '/'. V corresponds to each variable in Vec which is found in TestVars; % otherwise 'f is inserted. gen_var_inst2(_,0,0) :- !. gen_var_inst2(Vars,[Var|Rest],[Flag|Flags]) :-(member(Var,Vars) — > Flag = i Flag = f), gen_var_inst2(Vars,Rest, Flags). y0 *** % *** Syntax definitions for Westcott's lexical analyzer % *** white_space_char(32). white_space_char( 10). white_space_char(9). white_space_char (12). ?-op(900,fx,'-'). ?-op(1100,yfx,'#'). ?-op(1000,yfx,'&'). % space % carriage return % tab % form feed op_chars("+" ,math(' + ')). op_chars("-",matli('-')). op_chars("*" ,math( '*')). op_chars("/",math('/')). op_chars("//",math( '//'))• op_chars("":",bool('&')). op_chars("#",bool(' #')). op_chars(" ' " ,bool( '"*)). op_chars("<M,rel('<')). APPENDIX B. BRUCE PARSER op.charst'^Vel^')). op_chars( "=< " ,rel( '=<'))• op_chars(">=",rel( '>=')). op_chars( "=:=" ,rel( ' = : = ')). op_chars(''=\=M ,rel(> =\=')). punct_chars("{",'{'). punct_chars("}",'}'). punct_chars(",",','). punct_chars("('V ('). punct_chars(")",')'). punct_chars(" [",' ['). punct_chars("] ",']'). punct_chars(";",';'). punct_chars(":",':'). punct_chars(" :=",' : = '). reserved(local,local). reserved(if4f). reserved(else,else). reserved( while ,while). reserved(repeat,repeat). reserved(until,until). reserved(call,call). reserved(goto,goto). reserved(skip,skip). reserved(true,true). reserved(false,false). constant_form( C ,const (C)). % *** % *** expression evaluation routines... % *** "T :- not T. A # B :- (A;B). A k B :- A,B. value(Expr,Val) :— APPENDIX B. BRUCE PARSER 103 Val is Expr. % *** % *** label generation and numbering % *** % % reset_gen_nums sets genjnums to 1. reset_gen_nums :— abolish(gen_nums,4), tassert(gen_nums(l,1,1,1)). % test, while, repeat, label % - % get_gen_num(Type,Num) returns a new unique number for the structure % Type (test,while,repeat,label). get_gen_num(test,Num) :— gen_nums (Num,X,Y,Z), Next is Num + 1, abolish(gen_nums,4), tassert(gen_nums(Next,X,Y,Z)). get_gen_num(while,Num) :— gen_nums(X,Num,Y,Z), Next is Num + 1, abolish(gen_nums,4), tassert(gen_nums(X,Next,Y,Z)). get_gen_num(repeat,Num) :— gen_nums(X,Y,Num,Z), Next is Num + 1, abolish(gen_nums,4), tassert(gen_nums(X,Y,Next,Z)). get_gen_num(labei,Num) :— gen_nums(X,Y,Z,Num), Next is Num + 1, abolish(gen_nums,4), tassert(gen_nums(X,Y,Z,Next)). % APPENDIX B. BRUCE PARSER 104 % gen_label(Labeltype,Label) generates a new Label for structure Labeltype. gen_label(Labeltype,Label) :— get_gen_num(Labeltype,Num), atom_append(Labeltype,Num,Label), % % newjabellist resets the labellist for program Prog, and asserts that % Prog is the current program being processed. newJabellist(Prog) :— (retract(labellist(Progw,_));true), tassert(labellist(Prog,[],[])), tabolish(curr_prog,l), tassert(curr_prog(Prog)), ;# % % add_curr_labellist(Type,Label) adds Label to the label list for the current % program being processed, determined by currjprog. add_curr_labellist(label,Label) :-curr_prog(Prog), retract(labellist(Prog,Listl,List2)), append([Label],Listl,Newlistl), append([Label],List2,Newlist2), tassert(labellist(Prog,Newlistl,Newlist2)), !_ add_curr_labellist(_,Label) :— curr_prog(Prog), retract(labellist(Prog,Listl,List2)), append([Label],Listl,Newlist), tassert(labellist(Prog,Newlist,List2)), I. % % add approp labellist (Label, Newlabel): % % add_approp_labellist adds Newlabel to the general label list which also % contains Label. APPENDIX B. BRUCE PARSER 105 add_approp_labeIlist(Label,Newlabel) :— labellist(A,Listl,B), member2(Label,Listl), retract(labellist(A,Listl,B)), append([Newlabel],Listl,Newlist), tassert(labellist(A,Newlist,B))> i % labelpgm(Clause) is satisfied if Clause is a label program. labelpgm((H:-B)) :-functor(H ,Name,_), labellist(_,_,Labels), member2( Name,Lab els). Appendix C Branch Handling % *** % *** Prolog branch transformation utilities % *** % *** _ Brian J. Ross % *** Dept. of Computer Science % *** University of British Columbia % *** % % process_branches(Prolog,Newprolog) transforms the clauses in Prolog so % that branches are properly handled. First, all chains of goals following % branches are removed (label programs may exist which contain the code % being thrown away). % Then the prolog is transformed to account for the branches within descendent % predicates, processjbranchesj3 is called to iterate through all the Prolog % clauses. For each one with a goto, the goto goal is changed into a call to % the appropriate label program. Then the parent predicates of the clause % with this goto are transformed. process_branches(Prolog,Newprolog) :— process_branches(Prolog,Prolog,Prolog2), chop_branch_chains(Prolog2,Prolog2,Newprolog), process_branches(Prolog,[],Prolog) :— !. process_branches(Prolog,[Clause|_],Newprolog) :— nnd_goal(Clause,Head,Left,goto(X,Y,Z),Right), 106 APPENDIX C. BRANCH HANDLING create_labelcall(goto(X,Y,Z),Call), branch_restruct(Prolog,Clause,Head,Prolog2), insert_goal(Prolog2,Clause,Head,Left,[Call],Right,Prolog3), process_branches(Prolog3,Prolog3,Newprolog), process_branches(Prolog,[JR],Newprolog) :-process_branches(Prolog,R,Newprolog), I, % % branchjrestruct restructures Prolog given a clause with a branch call/ % ancestor of a branch call, Goal. % Case 1: Clause has a parent: % Ancestors of Clause are restructured, and code returned is used to % restructure the sibling of Clause. % Case 2: Clause has no parent: % Clause is a main program clause, and is left alone for now. branch_restruct(Prolog,Clause,Head,Newprolog) :-restruct_parent(Prolog,Head,Pvec,Pcode,New2), restruct_sibling(New2,Clause,Pvec,Pcode,Newprolog), branch_restruct(Prolog%_,_,Prolog) :— I. % % restruct_parent finds the non—label—program parent of Head. % It then pulls goals from the right of the call to Head, resulting in Code. % The branchjrestruct is called on the parent, causing a recursive restructuring % up the tree. restruct_parent(Prolog,Head,Ivec,Code,Newprolog) :— parent_clause(Prolog,Head,Parent,Phead,Left,Goal,Right), not labelpgm(Parent), set_code(Phead,Left,Goal,Right,Ivec,Code), branch_restruct(Prolog,Parent,Phead,Newprolog), % % restruct_sibling adds Code to the end of the sibling of Clause, % if one exists. APPENDIX C. BRANCH HANDLING 108 restruct_sibling(Prolog,Clause,Vec,Code,Newprolog) :— sibling_clause(Prolog,Clause,Sibling), append_goals(Sibling,Vec,Code,Newsibling), remove_item(Sibling,Prolog,New2), append([Newsibling],New2,Newprolog), restruct_sibling(Prolog,_,_,_,Prolog) :- !. % % setjcode returns the goals to the right of Goal, should they exist, along % with their input vector. set_code(Head,Left,Goal,[],_,[]) :— set_code(Head,Left,Goal,Right,In,Code) :— get_IO([Head],Il,01), append(Left,Goal,G), get_prev_IO(G,(Il,Il),I2,02), get_prev_IO (Right ,(02,02) ,13,03), copy ((13 ,Right) ,(In ,Code)), !. % % restruct_clause restructures a clause by merging Left and Right together. % restruct_clause2 and restruct_prog do the actual reconstruction. restruct_clause(Head,Left,Call,Newclause) :— functor(Head,Name,_), storematch(Name^v_,_,_), i restruct_prog(Head,Left,Call,Newclause). restruct_clause(Head,Left,Call,Newclause) :— restruct_clause2(Head,Left,Call,Newclause), I restruct_clause2(Head,[],Right,Code) :— Head =.. [Name,Il,Ol], get_prev_IO(Right,(Il,Il),I2,02), Newhead =.. [Name,Il,02], APPENDIX C. BRANCH HANDLING list_to_body (Right, Body), copy((Newhead :- Body),Code), !. restruct_clause2(Head,Left,[],Code) :— Head =.. [Name,Il,01], get_prev_IO (Left,(II ,11) ,12,02), Newhead =.. [Name,Il,02], list_to_body(Left,Body), copy((Newhead :— Body),Code), I. restruct_clause2(Head,Left,Right,Code) :— copy((Head,Left,Right),(Head2,Left2,Right2)), Head2 =.. [Name,Il,01], get_prev_IO(Left2,(Il,Il),I2,02), get_prev_IO(Right2,(02,02),I3,03), 02 = 13, Newhead =.. [Name,Il,03], append(Left2,Right2,B), list_to_body(B,Body), copy((Newhead :— Body),Code), I. % ; % restruct_prolog is almost like restruct_clause2. % It creates a program clause by merging the goals in Left and % Right, but removing local variables from the header 10 vectors. restruct_prog(Head,Left,Right ,Newclause) :— Head =.. [Name,Il,Ol], get_prev_IO(Left,(Il,Il),I2,02), get_prev_IO(Right,(02,02),I3,03), gen_vec(01,04), append(04,_,03), Newhead =.. [Name,Il,04], append(Left,Right,B), list_to_body(B,Body), copy((Newhead :— Body),Newclause), i APPENDIX C. BRANCH HANDLING % createjabelcall changes a goal in goto format to a label call. create_labelcall(goto(In,Label,Out),Call) :— Call =.. [Label,In,Out], I. % :  % chop_branch_chains(Prolog, Clauses, Collect) takes each clause with % label program call and throws away any goals following it. chop_branch_chains(_,[|,[|) :- !. chop_branch_chains(Prolog,[Clause | R] ,T) :— split_clause(Clause,Head,Goals), check_for_branches(Prolog,Goals,Goals2), restruct_clause(Head,[],Goals2,Newclause), chop_branch_chains(Prolog,R,S), (member3(Newclause,S) —> T = S T = [Newclause|S]), !_ chop_branch_chains(Prolog,[Clause|R],[Clause|T]) :— chop_branch_chains(Prolog,R,T), !. insert_goal(Prolog,Clause,Head,Left,Goal,Right,Newprolog) :— append_list([Left,Goal,Right],Goals), list_to_body(Goals,Body), Newclause =.. [(:—),Head,Body], (member3(Newclause,Prolog) — > Newprolog = Prolog remove_item(Clause,Prolog,New2), Newprolog = [Newclause |New2]), i % *** % *** Label program generation % *** APPENDIX C. BRANCH HANDLING 111 % % gen_labelprogs(Prolog,Labelprogs) creates a new prolog environment which % contains predicates for the label programs in Prolog. It calls a % genjabelprogs/ 3 version, where the second argument iterates through % the clauses. % The goals for the label program are obtained, and a label program is created. % Then all label references for the program just created are removed from the % prolog environment. gen_labelprogs(Prolog,Newprolog) :— gen_labelprogs(Prolog,Prolog,Newprolog), gen_labelprogs(Prolog,[],Prolog) :— !. gen_labelprogs(Prolog,[Clause|R],Newprolog) :— find_goal(Clause,Head,Left,label(Label),Right), get_goals(Prolog,Clause,Head,Left,Label,Right,In,Out,Goals ,Defns), create_labclause(Label,In,Out,Goals,Labelprog), append_list([[Labelprog],Defns,Prolog],Prolog2), rem_pred_labels(Prolog2,label(Label),Prolog3), genjab elprogs (Prolog3 ,P r olog3 ,Ne wprolog), !_ genJabelprogs(Prolog,[jR],Newprolog) :— genjab elprogs(Prolog,R,Newprolog), i_ % % getjgoals retrieves the goals to be used for a label program. % If a goal in Right contains a branch, then all the goals % up to and including that goal are used for the label program. % Otherwise, the goals of the parent construct are obtained, and the % result is appended to the goals in Right. get_goals(Prolog,Clause,Head,Left,_,Right,In,Out,Goals,[]) :— branch_under_goals(Prolog,Head,Left,Right,In,Out,Goals), tt get_goals(Prolog,Clause,Head,Left,Label,Right,In,Out,Goals,Defns) :— create_construct_control(Prolog,Head,Left,Label,Right,Cin,Cout,Control,Defnsl), APPENDIX C. BRANCH HANDLING parent_goals(Prolog,Head,Pin,Pout,Pgoals,Defns2), append(Defnsl,Defns2,Defns), merge_goals(Cin,Cout,Control,Pin,Pout,Pgoals,In,Out,Goals), I, % % parentjgoals recursively obtains the parent goals to be used by a % label program. The successive parent goals to the right of the call to a % child predicate are obtained and concatenated together. This recursion % stops when (a) the top predicate is reached, or (b) a branch has been % detected under a goal. parent_goals2 is used as a subsidiary call. % Note that label programs are not considered parents. parentj*oals(Prolog,Head,In,Out,Goals,Defns) :— parent_clause(Prolog,Head,Parent,Phead,Left,Goal,Right), not labelpgm(Parent), append(Left,[Goal],L2), functor(Goal,Goallabel,_), get_goals(Prolog,Parent,Phead,L2,Goallabel,Right,In,Out,Goals,Defns). parent_goals(_,_^.,_,0 ,Q). % : % branchjunderjgoals obtains all the goals up to and including a goal in Right % which contains a branch. It fails should no branches be found under any goal % in Right. branch_under_goals(Prolog,Head,Left,Right,In,Out,Goals) :— check_for_branches(Prolog,Right,Goals2), get_IO([Head],HJ, get_prev_IO (Left ,(11,11) ,_,In2), get_prev_IO(Goals2,(In,In),_,Out2), copy((In2,Out2,Goals2),(fn,Out,Goals)). % % check_for_branches does a search for branches under Goals. % It keeps all the goals in Goals up to and including the first one with a % descendent branch. It fails should no descendent branches be found. check_for_branches(_,u,u) :— !,fail. check_for_branches(Prolog,[goto(I,L,0)|_],[goto(I,L,0)]). APPENDIX C. BRANCH HANDLING check_for_branches(Prolog,[Goal|J,[Goal]) :— functor(Goal,Name,_), labellist(_,_,Labels), member(Name,Labels). check_for_branches(Prolog,[Goal|R],[Goal]) :— descendent_branches(Prolog,Goal). check_for_branches(Prolog,[Goal|R],[Goal|S]) :-checkJbrJ>ranches(Prolog,R,S). % % descendent_branch.es performs a recursive search for branches under goal G. % For efficency, G is analyzed for it's goal type so that needless % search is not done on goals with no descendents (assignments, program calls, % etc). descendent_branches2 is called to iterate through new goal lists % obtained during the search. descendent_branches(Prolog,G) :-member2( G, [asgn(_,_,_,J ,callasgn(_,_,_) ,label(_) ,goto(_,_,_)]), ! fail. descendent_branches(Prolog,T) :— is_a_test(T), fail. descendent_branches(Prolog,Call) :— functor(Call,Prog,_), storematch(Prog^^^,_), I fail. descendent_branches(Prolog,G) :— functor(G ,Lab,_), labellist(_^,Labels), member2(Lab,Labels), descendent_branches(Prolog,Goal) :— APPENDIX C. BRANCH HANDLING 114 find_clause(Prolog,Goal,Clause), removej tem( Clause ,P rolog ,Prolog2), split_clause(Clause,_,Body), descendent_branches2(Prolog2,Body). descendent_branches2(_,Q) :— !,fail. descendent_branches2(_,[goto(_^,_)|J) :- !. descendent_branches2(Prolog,[Goal|J) :-descendent_branches(Prolog,Goal), descendent_branches2(Prolog,[_|R]) :-descendent_branches2(Prolog,R), % % createjabclause creates a label program. create_labclause(Lab,In,Out,[],Clause) :— Header =.. [Lab,In,Out], copy(Header,Clause). create_labclause(Lab,In,Out,Goals,(Header :— Body)) :— copy((In,Out,Goals),(I2,02,Goals2)), Header =.. [Lab,l2,02], list_to_body(Goals2,Body). % % create_construct_control creates a list of goals, Control, which comprise % the particular control sequence needed when junping into the construct % at the point Right. With brace, there are two cases: % (l) jumping into a repeat — since repeat tests are done at the end of % the loop, the repeat test must be simulated. This requires % calling create_repeat_control to create this special control. % (2) jumping into any other mechanism — simply return the goals to the % right of the jump point. create_construct_control(Prolog,Head,Left,Label,Right,In,Out,Control,Defns) :— functor(Head,Name,_), getjab el_r efs (P rolog ,N ame, [], [ A ,B ]), test_if_repeat(A,B,OutT,Test,Body), APPENDIX C. BRANCH HANDLING 115 create_repeat_control(OutT,Test3ody,Label,Head,Left,Right,In,Out,Control,Defns). create_construct_control(Prolog,Head,Left^,Right,In,Out,Control,[]) :— get_IO([Head],IlJ, get_prev_I0(Left,(Il,Il),_,02), get_prev_IO(Right,(02,02),I3,03), copy((Right,l3,03),(Control,In,Out)). % % create_repeat_control creates the control environment for a repeat construct. % The output is % Control = [Body,Test] % Defns = [(Testl :- ~Test,Head),(Testl :- Test)] % all suitably tidied. % The name for Test is externally saved through calling add_approp_labellist. create_repeat_control(Vec,Test,Body,Label,Head,Left,Right,In,Out,Control,[Dl,D2]) :— copy((Vec,Test,Body),(Vec2,Test2,Body2)), copy((Head,Left,Right),(Head2,Left2,Right2)), append(Left2,Rightgoals,Body2), % get goals after jump point functor(Head,Name,_), get_I0([Head2],Il,_), get_prev_IO(Left2,~(Il,Il),_,02), get_prev_IO(Rightgoals,(02,02),I3,03), gen_label(test ,Testlabel), gen_vec(Vec2, Vout), HeadA =.. [Testlabel,Vec2,Vout], HeadB =.. [Testlabel,Vec2,Vec2], Call =.. [Name,Vec2,Vout], list_to_body(["(Test2),Call],BodyA), copy ((~HeadA: - BodyA) ,D 1), copy((HeadB: -Test2) ,D2), add_approp_labellist(Label,Testlabel), merge_goals(I3,03,Rightgoals,Vec2,Vout,[HeadA] ,In,Out,Control). % % remjpredjabels simply removes all goals of the form Label from Clauses. % This is done so that we don't construct duplicate label programs. rem_pred_labels([],_,[]) :- !. rem_pred_labels([Clause|R],Label,[Newclause|S]) :-APPENDIX C. BRANCH HANDLING 116 fin d_goal( Clause, Head ,Left ,L ab el ,Right), make_clause(Head,Left,Rigbt,Newclause), rem_pred_labels(R,Label,S), rem_pred_labels([Clause|R],Label,[Clause|S]) :— rem_pred_lab els (R,Lab el, S), i Appendix D Bruce Generation % *** % *** Bruce code generation facility % *** % *** _ Brian J. Ross % *** Dept. of Computer Science % *** University of British Columbia % *** % % brucify(Env) converts the entire Prolog environment in list Env % into Bruce code. brucify(Env,Bruce) :— bagof([P | Q] ,X * labellist (P,Q ,X) .Labels), copy (Env,Env2), program_separate(Env2,Labels,[],Prolog), brucify_programs(Prolog,[],Bruce). % % brucify_programs(Programs,Collect,Result) converts each prolog program % in Programs to Bruce code. brucify_programs( [] ,Bruce,Bruce). brucify_programs([Progname,Prog|Rest],Collect,Bruce) :— get_label_refs(Prog,Progname,[],Clauses), get_IO (Clauses,In,_), 117 APPENDIX D. BRUCE GENERATION 118 template_match(Progname,In,Prog,Clauses,B»[]j_)» rernun usedjab els (B ,B 2), create_outval_asgns(Progname,Clauses,Asgns), chain_append(B2,Asgns,Body), bruce_header(Progname,Header), append_list([Header,[' {' ] >Body,['}' ]] ,Bruce_prog), brucify_programs(Rest,[Bruce_prog|Collect],Bruce). % % templatejnatch(Progname,Prolog, Clauses,Bruce,Labels,Newlabels): % Matches Clauses to known bruce construct definitions. % NOTE: Should the dataflow of goals be altered, include the two lines noted % below. template_match(_,_,_,[],_,_,_) :— !,fail. template_matcli(Prognarrieu,Prolog,[Clause],Bruce,Labels,Newlabels) :— % split_clause(Clause,Head,Goals), % < see note above % order_clausejgoals(Goals, Ordered), % <— see note above split_clause( Clause, Head .Ordered), get_IO([Head],In,_), template_match_goals(Progname,In,Prolog,Ordered,Bruce,Labels,Newlabels). % repeat: template_match(Progname,Vec,Prolog,[A,B]»Bruce»Labels,Newlabels) :— is_a_repeat(Progname,A,B)Test,Body), get_IO(AwOut), template_match^oals(Progname,Out,Prolog,Body,Bruce_body,Labels,Newlabels), append_list([[repeat,' {'],Bnice_body,['} > ,until,' (' ,Test,') ']],Bruce). % while: template_match(Progname,Vec,Prolog,[A,B]»Bruce,Labels,Newlabels) :— is_a_while(Progname,A,B,Test,Body), getJO(AMOut), template_match^oals(Progname,Out,Prolog,Body,Bruce_body,Labels,Newlabels), append_list([['while (' ,Test,')','{'],Bruce_body,[»}']],Bruce). % if: template_match(Progname,Vec,Prolog,[A,B],Bruce,Labels,Newlabels) :-APPENDIX D. BRUCE GENERATION 119 is_an_if(Progname,A,B,Test,Thengoals,Elsegoals), getjb(AMOut), template_match^oals(Progname,Out,Prolog,Thengoals,Thencode,Labels,Newlabels2), (Elsegoals == Q -> append_list([['if ('/Test,')»,'{'],Thencode,['}']],Bruce), Newlabels = Newlabels2 template_match^oaIs(Progname,Out,Prolog,Elsegoals,Elsecode,Newlabels2,Newlabels), append_list([[' if (' ,Test,')','{'],Thencode,['}' ,else,' {' ], Elsecode,['}']],Bruce)). template_match(Progname,Vec,Prolog,Clauses,Bruce,Labels,Newlabels) :— factor (Clauses ,Prolog,NewClauses ,NewProlog), template_match(Progname,Vec,NewProlog,NewClauses,Bruce,Labels,Newlabels). % ; ___ % template_match_goals(Progname,Prolog, Goallist,Bruce,Labels,Newlabels): % Matches each goal in Goallist to a construct. % One of three situations is possible: % (a) Finished — empty Goal list % (b) Goal is an assignment: a Bruce assignment is created % (c) Goal is a call assignment: it is temporarily ignored until the % corresponding call is found. % (d) Goal is a procedure call: a Bruce proc. call is created. % (e) Goal refers to a structure previously created: create a % branch to it. % (f) Goal refers to a structure previously created, but step (e) failed: % then fail (unknown structure). % (g) none of the above: then the goal must be a call to a more complex % mechanism. All the clauses relevant to that goal are % extracted, and a template match is performed on them. % case (a) template_match_goals(_,_,_,[],[] ,L,L). % case (b) template_match^oaIs(Progname,_,Prolog,[asgn(In,Var,Expr,Out)|Rest],Bruce,Labels,Newlabels) :— i •> template_match_goals(Progname,Out,Prolog,Rest,B,Labels,Newlabels), convert_bruce_expr(Progname,In,Expr,Expr2), convert_bruce_expr(Progname,Out,Var,Var2), chain_append([Var2,' : = ' ,Expr2],B,Bruce). APPENDIX D. BRUCE GENERATION 120 % case (c) template_matchj!;oals(Progn^ :— i append(Rest,[callasgn(A,B,C)],Rest2), template_match_goals(Progname,Vec,Prolog,Rest2,Bruce,Label,Newlabels). % case (d) template_match_goals(Progname,Vec,Prolog,[Goal|Rest],Bruce,Labels,Newlabels) :— Goal =.. [Prog,In,Out], storematch(Prog,Vars,Ref,Val,_), i •J collect_callasgns(Rest,In,Calls), gen_vec(Val,Vl), append(Refvec,Vl,In), create_val_vector(Vl ,Calls,Ivec,Valvec), Call =.. [Prog,Refvec,Valvec], remove_items2(Calls,Rest,Rest2), template_match_goals(Progname,Out,Prolog,Rest2,B»Labels,Newlabels), convert_bruce_expr(Progname,Vec,Call,Call2), chain_append([' call' ,Call2],B, Bruce). % case (e) template_match^oals(Progname,Vec,Prolog,[Goal|Rest],[goto,Name],Labels,Labels) :— functor(Goal,Name,_), member 2 (Name ,L ab els). % gen_impl_asgns(PrognarnelVec,Goal,Asgns), % remove?? % chain_append(Asgns,[goto,Name],Bruce).  remove?? % case (f) template_match_goals(_,_,_,[Goal|J ,_,Labels,_) :— functor(Goal,Name,_), member2(Name,Labels), j fail. % case (g) template_match_goals(Progname,Vec,Prolog,[Goal|Rest],Bruce,Labels,Newlabels) :— functor(Goal,Name,_), get_label_refs(Prolog,Name,[],Clauses), template_match(Progname,Vec,Prolog,Clauses,BruceA,[Name|Labels],Newlabels2), get_IO([Goal],In,Out), APPENDIX D. BRUCE GENERATION 121 gen_impl_asgns(Progname,Vec,In,Asgns), template_match_goals(P rogname ,0 ut ,Prolog,Rest ,BruceB ,Newlabels2,Newlabels), append([Name,': '],BruceA,Xl), chain_append(Asgns,Xl,X2), chain_append(X2,BruceB,Bruce). % % is_an_if(Progname,A,B,Brucetest, Then,Else) % Tests if goals A,B can be matched with a Bruce test construct, and % creates Bruce code if they match. is_an_if(Progname,A,B)Brucetest,Then,Else) :— test_if_if(A,B,I,Test,Then,Else), convert_bruce_expr(Progname,I,Test,Brucetest). % % is_a_while(Progname,A,B,Brucetest,Body): % Tests A and B for a match with a Bruce while construct, and % creates Bruce code if they match. is_a_while(Progname,A,B)Brucetest,Body) :— test_if_while(A,B,I,Test,Body), convert_bruce_expr(Progname,I,Test,Brucetest). % ; % is_a_repeat(Progname,A,B,Brucetest,Body): % Tests A and B for a match with a Bruce repeat construct, % creates Bruce code if they match. is_a_repeat(Progname,A,B)Brucetest,Body) ._ test_if_repeat(A,B,0,Test,Body), convert_bruce_expr(Progname,0,Test,Brucetest). % % complementary_tests(BodyA,BodyB,TA,TB) finds an instance of complementary % tests TA and TB in BodyA and BodyB (ie. TA = ~TB). Repeated calls % will return new complementary tests, if any. complementary_tests(BodyA,BodyB,TA,TB) :— member2(TA,BodyA), is_a_test(TA), member2(TB,BodyB), APPENDIX D. BRUCE GENERATION 122 is_a_test(TB), complementary (TA,TB). % % convert_bruce_expr(PrognamelIn,Expr,Conv) created a copy of Expr having % the appropriate Bruce variable names, based on ordering in In. % The result is in Conv, as we don't want to bind the actual logical % variables (lose dataflow information). convert_bruce_expr(Progname,In,Expr,Conv) :_ copy((In,Expr),(In2,Conv)), set_all_to_vars(In2,In3), storematch(Progname,In3,_,_,_), % % A bruce program header is created... bruce_header(Progname,[A,':' ,local,Locals]) :— storematch(Progname,Vars,Ref,Val,Locals), A =.. [Progname,Ref,Val]. % % recursive_call(Call, Goals, C) is satisfied if a recursive call C to header % Call exists in the Goals list. recursive_call(Call,Goals,C) :— copy(Call,C), member2( C, Goals), same_out_vars(Call,C). % ; % collect_callasgns(Goals,Vars,Calls) finds instances of callasgn goals in Goals % which assign values to variables listed in Vars. The results are in Calls. collect_callasgns([]%_,[]) :— !. collect_callasgns([callasgn(A,Var,B)|R],Vars,[callasgn(A,Var,B)|D]) :-member(Var,Vars), collect_callasgns(R,Vars,D), !. collect_callasgns([_|R],Vars,D) :— collect_callasgns(R, Var s, D), APPENDIX D. BRUCE GENERATION % % create_val_vector(Vars,Calls,Valvec) creates a value parameter list % for a Bruce procedure call. % Variables in Vars which have a corresponding callasgn in Calls are replaced % with the expression in that callasgn. Otherwise that variable is used. create_val_vector([],_,_,[]) :— !. create_val_vector([V| R] ,Callasgns ,1 vec,[T | W]) :— (collect_callasgns(Callasgns,[V] ,[callasgn(Ivec,_,Expr)]) — > create_val_vector(R,Callasgnsu,W), T = Expr create_val_vector(R,Callasgns,Ivec,W), T = V), % % chain_append(A,B,C) appends lists A and B together, such that if B is % nonempty, a semicolon is inserted between them. chain_append(A,[],A) :— !. chain_append([],A,A) :— !. chain_append(A,B>C) :— append_list([A,['; '],B],C), I. % % rem_unused_labels(Bruce,Newbruce) removes labels from the bruce source % which have no branches onto them. rem_unused_labels(Bruce,Newbruce) :— rem_unused_lab els(Bruce ,B ruce,Newbruce), I, rem_unused_lab els (_, Q, D). rem_unused_labels(U,[L,':' |R],[L,' :' |A]) :-find_goto(L,U), rem_unused_labels(U,R)A.). rem_unused_labels(U,[L,': '|R],A) :— rem_unused_lab els( U ,R, A). APPENDIX D. BRUCE GENERATION rem_unused_labels(U,[S | R],[S |A]) :— rem_unused_labels(U,R,A). % find_goto(Label,Bruce) finds a branch to label Label in the Bruce code. find_goto(Label,[goto,Label|J) :- !. find_goto(Label,[S|R]) :-nnd_goto(Label,R), I. % % test_if_if checks if A and B match with an if construct of Bruce. % The matching criteria are: % (a) complementary tests in A and B % (b) Both tests are dependent on their header input variables test_if_if(A,B,I,Test,Then,Else) :-split_clause( A ,Head A ,B ody A), split_clause(B ,HeadB ,Body B), complementary_tests(BodyA,BodyB,TA,TB), dep_in_vars(TA,HeadA), dep_in_vars(TB,HeadB), remove_item(TA,BodyA,NewA), remove_item(TB,BodyB,NewB), set_then_else(TA,HeadA,NewA,TB,HeadB,NewB,Test,Then,Else,Head), Head =.. [_,I,J. % % test_if_while checks if A and B match with a while construct of Bruce. % The matching criteria are: % (a) complementary tests in A and B. % (b) Both tests are dependent on their header input variables % (c) One of the clauses has a body consisting only of the test. % (d) The other clause contains a recursive call matching the head. test_if_while(A,B,I,Test,Body) :-split_clause(A,HeadA,BodyA), split_clause(B ,HeadB ,Body B), complementary_tests(BodyA,BodyB,TA,TB), dep_in_vars(TA,HeadA), dep_in_vars(TB ,HeadB), (BodyA == [TA], APPENDIX D. BRUCE GENERATION 125 (Test,Head,Goals) = (TB,HeadB,BodyB) BodyB == [TB], (Test,Head,Goals) = (TA,HeadA,BodyA)), recursive_call(Head,Goals,Call), remove items2([Test,Call],Goals,Body), Head =.. L.IJ. % % test_if_while checks if A and B match with a repeat construct of Bruce. % The matching criteria are: % (a) complementary tests in A and B. % (b) One clause contains a recursive call matching the head. % (c) The test in that clause is dependent on the headers input variables. % (d) The test in the other clause uses variables in the headers output % variables list. % (e) The remaining goals which should compose the repeat body are % the same (permutation). test_if_repeat(A,B,0,Test,Body) :— split_clause( A ,Head A ,B ody A), split_clause(B ,HeadB,BodyB), complementary_tests(BodyA,BodyB ,TA,TB), (recursive_call(HeadA,BodyA,Call), (Tl,Bl,Test,H2,B2) = (TA,BodyA,TB,HeadB,BodyB) recursive_call(HeadB,BodyB,Call), (Tl,Bl,Test,H2,B2) = (TB,BodyB,TA,HeadA,BodyA)), dep_in_vars(T 1 ,Call), dep_out_vars(Test,H2), remove_item(Test,B2,Body), remove_items2([Tl,Call],Bl,New2), permutation(Body,New2), . H2 =.. [_,_,0]. % % set_then_else(TA,HeadA,NewA, TB,HeadB,NewB, Test, Then,Else,Head) sets % Test, Then, Else, and Head appropriately. set_then_else(TA,HeadA,[],TB,HeadB ,NewB,TB,NewB,[],HeadB) :-NewB \== [], i APPENDIX D. BRUCE GENERATION set_then_else(TA,HeadA,NewA,TB,HeadB,Q,TA,NewA,[],HeadA) :-NewA \== 0, ;# set_then_else(TA,HeadA,NewA,TB,HeadB,NewB,TB,NewB,NewA,HeadB) :-functor(TA,'"'J, !_ set_then_else(TA,HeadA,NewA,TB,HeadB,NewB,TA,NewA,NewB,HeadA) :- !. % % set_all_to_vars copies A to B, replacing nonvar items with new var ones. set_all_to_vars([],[]) :— !. set_aU_to_vars([A|B],[A|D]) :-var(A), i •» set_all_to_var s( B ,D). set_all_to_vars([A|B],[C|D]) :-set_all_to_vars(B,D), % create_outval_asgns creates an assignment for each call—by—value % parameter for program Progname if that parameter has a ground value in % programs output vector (which can occur through mixed computation). create_outval_asgns(Progname,[(H:—B)],Asgns) :— get_IO([H],_,Out), storematc^Progname^Re-i-*-)-)) gen_vec(Ref,Refvec), append(Refvec>_,Out), set_asgns(Progname,Out,Ref,Refvec,Asgns), % % gen_impl_asgns checks the In vector: for each ground item in In, % an implicit assignment is created. These % assignments represent the effects of the mixed computation. gen_impl_asgns(Progname,Vec,In,Asgns) :— i storematch(Progname,Varsv.,_^), set_asgns (P rogname ,In, Var s ,In, Asgns). APPENDIX D. BRUCE GENERATION 127 % % setjasgns creates an implicit assignment for each item in Vec having % a ground value. set_asgns(_,_,_,0,0) :- !.' set_asgns(Progname,Vec,[Var|R],[S|T],A) :— nonvar(S), t set_asgns(Progname,Vec,R,T,Q), convert_bruce_expr( Progname, Vec, S, S 2), chain_append([Var,' : = ',S2],Q,A). set_asgns(Progname,Vec,[_|R],[_|T],A) :— i set_asgns(Progname,Vec,R,T,A). % *** % *** Prolog factoring utilities % *** % ; % factor (Clauses, Prolog, [NewClause],NewProlog) tries to factor out common % goals in Clauses. Goals may be factored if: % (a) the factorable goals are common between two clauses % (b) dataflow among them is the same % factor extracts two different clauses from Clauses, and calls factorjgoals to % factor out the common goals, if any. % If factor_goals succeeds, then the old clauses are removed from the Prolog % environment, and the new restructured clause NewClause plus the additional % definitions are inserted into the environment, resulting in NewProlog. factor(Clauses,Prolog,[NewClause],NewProlog) :— member2(A,Clauses), member2(B, Clauses), A \== B, factor_goals(A,B,NewClause,NewDefns), remove_items( [A,B ] ,Prolog,X 1), append([NewClause|NewDefns],Xl,NewProlog), I. APPENDIX D. BRUCE GENERATION 128 % % factor_goals(A,B,NewClause,NewDefns) attempts to factor out common goals in % clauses A and B. If common goals are found, the disjoint goals are % removed from the clauses, and are put into a new predicate defined in % NewDefns. Clauses A and B are merged, resulting in NewClause. % % Factorjgoals first orders the goals in A and B w.r.t. dataflow. % Then common goals on the left side of the goal body are found. % If not successful, common goals on the right side are searched for. % If common goals can be extracted, spawn_clause is called to do the % Prolog code maintenance. factor_goals(A,B,NewClause,NewDefns) :— split_clause( A ,Head A ,B ody A), split_clause(B,HeadB,BodyB), order_clause_goals(BodyA,OrdA), or der_clause_goals (B ody B ,0 r dB), (Side = left, duo_split(left,OrdA,CommonA,RestA,OrdB,CommonB,RestB) Side = right, duo_spUt(right,OrdA,RestA,CommonA,OrdB,RestB,CommonB)), permutation(CommonA,CommonB), spawn_clause(Side,HeadA,CommonA,RestA,HeadB,CommonB,RestB,NewClause,NewDefns). % % Spawn_clause creates new Prolog code, given common goal sets CommonA and % CommonB. The two cases are when common goals are found on the left and % right sides of the clauses. The Prolog code creation involves % merging the two clauses into one containing the common goals plus call to % the new predicate, and creating a new predicate containing the disjoint % goals, spawnjeftjnain, spawn_left_aux, etc., do the actual prolog % transformation, dividing the Prolog clause on its left or right side. spawn_clause(left,HeadA,CommonA,RestA,HeadB,CommonB,RestB,Newl,[New2,New3]) :— spawn_left_main(Head A ,CommonA ,Rest A ,Newlabel,Newl), spawnJeft_aux(Newlabel,HeadA,CommonA,RestA,HeadB,CommonB,RestB,New2,New3), spawn_clause(right,HeadA,CommonA,RestA,HeadB,CommonB,RestB,Newl,[New2,New3]) :— spawn_right_main(HeadA ,Common A ,Rest A ,Newlabel,Newl), spawn_right_aux(Newlabel,HeadA,CommonA,RestA,HeadB,CommonB,RestB,New2,New3), APPENDIX D. BRUCE GENERATION 129 spawn_left_main(Head,Conimon,Rest,Newlabel,(Head3 :- Body)) :-copy((Head,Common,Rest),(Head2,Common2,Rest2)), get_prev_IO(Common2,Head2,I2,02), gen_label(label,Newlabel), gen_vec(I2,New0ut), HeadA =.. [NameJnJ, Call =.. [Newlabel,02,New0ut], Head3 =.. [Name,In,NewOut], list_to_body(CommonA,Xl), fuse((Xl,Call),Body), spawn_left_aux(Newlabel,HeadA,CommonA,RestA,HeadB,CommonB,RestB,(Head2 :— Body2),(Head3 copy((HeadA,CommonA,RestA,HeadB,CommonB,RestB), (HeadA2,CommonA2,RestA2,HeadB2,CommonB2,RestB2)), get_prev_IO(CommonA2,HeadA2,_,OA), getj>revJO(CommonB2,HeadB2,_,OB), get_prev_IO(RestA2,(OA,OA),I2,02), get_prev_IO(RestB2,(OB,OB),I3,03), Head2 =.. [Newlabel,I2,02], Head3 =.. [Newlabel,I3,03], list_to_body(RestA2,Body2), list_to_body(RestB2,Body3), spawn_right_main(Head,Common,Rest,Newlabel,(Head2 :— Body)) :— copy((Head,Common,Rest),(Head2,Common2,Rest2)), get_prev_IO (Rest 2,Head2,12,0 2), get_prev_IO(Common2,(02,02),I3,03), gen_label(label,Newlabel), gen_vec(I2,NewOut), Head2 =.. [Name,In,Out], Call =.. [Newlabel,I2,I3], list_to_body(Common2,Xl), fuse((Call,Xl),Body), i_ spawn_right_aux(Newlabel,HeadA,CommonA,RestA,HeadB,CommonB,RestB,(Head2 :- Body2),(Head copy((HeadA,CommonA,RestA,HeadB,CommonB,RestB), (HeadA2,CommonA2,RestA2,HeadB2,CommonB2,RestB2)), APPENDIX D. BRUCE GENERATION 130 get_prev_IO(RestA2,HeadA2,IA,OA), get_prev_IO(RestB2,HeadB2,IB,OB), Head2 =.. [Newlabel,IA,OA], Head3 =.. [Newlabel,IB,OB], list_to_body(RestA2,Body2), list_to_body(RestB2,Body3), Appendix E Program Printing Utilities % *** % *** Bruce program pretty printer % *** % ***- _ Brian J. Ross % *** Dept. of Computer Science % *** University of British Columbia % *** print_bruce(File,B) telling(Old), tell(File), print_bruce(B), told, telling(Old), I, print_bnice(Q) :— !. print bruce([A|B]) :— nl, print bruce2(A,0), nl, print_bruce(B), I, print_bruce2( []. print_bruce2( [' {' | R] ,Tab) : -Nexttab is Tab + 3, 131 APPENDIX E. PROGRAM PRINTING UTILITIES writelQ' {' ,nl,tab(Nexttab)]), print_bruce2(R,Nexttab). print.br uce2( ['}',';' | R],Tab) : -Nexttab is Tab - 3, writel([nl,tab(Nexttab),'};' ,nl,tab(Nexttab)]), print_bruce2(R,Nexttab). print_bruce2(['}',»until' |R],Tab) :-Nexttab is Tab - 3, writel([nl,tab(Nexttab),'} until']), print_bruce2(R,Nexttab). print_bruce2(['}','}'|R],Tab) :-Nexttab is Tab - 3, Nexttab2 is Nexttab - 3, writel([nl,tab(Nexttab),'}' ,nl,tab(Nexttab2),'}' ,nl,tab(Nexttab2)]), print_bruce2(R,Nexttab2). print_bruce2(['>' |R],Tab) :-Nexttab is Tab - 3, writel([nl,tab(Nexttab),'}' ,nl,tab(Nexttab)]), print_bruce2(R,Nexttab). print_bruce2([S,,;' |R],Tab) :-writel([S,';' ,nl,tab(Tab)]), print_bruce2(R,Tab). print_bruce2([local|R],Tab) :-writel([nl,local,' ']), print_bruce2(R,Tab). print_bruce2([S|R],Tab) :-writel([S,' ']), print_bruce2(R,Tab). % *** % *** Prolog program pretty printer ("Peter Piper picked...") yQ *** % % printjprolog/2 prints a beautified version of P into file File. APPENDIX E. PROGRAM PRINTING UTILITIES 133 % It calls print_prolog/1 to do the actual printing. print_prolog(File,P) :— telling(Old), tell(File), print_prolog(P), told, telling(Old), print_prolog(P) :— copy(P,Q), print_prolog2(Q), print_prolog2([]). print_prolog2([A|B]) :-print clause(A), nl, print_prolog2(B). % print_clause(C) beautifies clause C, and then writes it. print_clause([]). print_clause(C) :— beautify (C), C =.. [(:-)|[Head|Body]], writel(Head,' :- ',nl), print_goals(Body). print_clause(C) :— writel(C,' . »,nl). % print_goals(G) prints the goals in list G, 1 per line. print_goals([]). print_goals([(A,B)|R]) :-APPENDIX E. PROGRAM PRINTING UTILITIES print_goals([A,B|R]). print_goals([G]) :— tab(5), writel(G,'. »,nl). print_goals([G|R]) :-tab(5), writel(G,' ,',nl), print_goals(R). % % beautify(C) sets all the logical variables in clause C to atoms which % represent their Bruce names, which were saved during parsing. % The name numbering is reset each time beautify is invoked. beautify((H:-B)) :-H =.. [Name|Args], nnd_names(Name,Vnames), reset_name_numbering, args_to_list(B,Goals), set_names( [H | Goals], Vnames), beautify (_). % % set_names(Goallist,Varnames) sets the logical variables in the list of goals % to their corr. names in Varnames. % Temporary variables found in 'callasgn' goals are names "tmp". % Goals which represent subprogram calls are skipped (vars are set elsewhere). % Otherwise, each list in a goal's argument list, which is an 10 vector, % is processed. set_names ([],_). set_names([callasgn(_,X,_)|Rest],Vnames) :— set_name( X ,tmp), set_names(Rest,Vnames). set_names([A|Rest],Vnames) :— A =..[Name|_], storematch(Name,Vnames2,_,_,_), APPENDIX E. PROGRAM PRINTING UTILITIES 135 Vnames2 \== Vnames, set_names( Rest, Vnames). set_names([A|Rest],Vnames) :-A =.. UArgsl. save_lists(Args,Vecs), set_vec_names (Vecs, Vnames), set_names(Rest,Vnames). set_names([_|Rest],Vnames) :-set_names (Rest, Vnames). % % save_lists(L, Vecs) saves each list argument in list L into Vecs. save_lists([],[]). save_lists([A|B],Vecs) :— var (A), save_lists(B ,Vecs). save_lists([A|B],[A|Vecs]) :-functor (A,' .',_)> save_lists(B,Vecs). save_lists([_|B],Vecs) :— save_lists(B ,Vecs). % % find_names(Name,Varnames) finds out what type of mechanism Name represents % and returns the appropriate variable name list. nnd_names(Name,Vnames) :— storematch(Name,Vnames,_,_,_). nnd_names(Name,Vnames) :— labellist(N,L^), member(Name,L), storematch(N, Vnames M_,_). % % set_vec_names(Varlist,Namelist) sets the logical variables in each vector in APPENDIX E. PROGRAM PRINTING UTILITIES % Veclist to atoms. set_vec_names2(Vec,Namelist) sets each logical variable in % Vec to an atom created from the corr. Bruce variable Namelist. set_vec_names( _ _). set_vec_nam.es([V|Rest],Vnames) :— set_vec_names2(V,Vnames), set_vec_names(Rest,Vnames). set_vec_names2([] _). set_vec_names2([V|R],[N|S]) :-set_name(V,N), set_vec_names2(R,S). % % set_name(V,Name) unifies logical variable V to an atom representing the % Prolog variable name. The atom is based on the Bruce variable name Name. % A counter is kept for each variable name, which is updated for each % successful unification. set_name(V,Name) :— not var(V), !, set_name(V,Name) :— retract(save_no(Name,Num)), Next is Num + 1, atom_append(Name,Next,New), capitolize(New,Newname), V = Newname, t assert (save_no( N ame ,Next)), set_name(V,Name) :— atom_append(Name,l,New), capitolize( New ,Newname), V = Newname, t assert (s ave_no( N ame, 1)). % % Reset the variable counters... APPENDIX E. PROGRAM PRINTING UTILITIES 137 reset_name_numbering :— abolish(save_no,2). reset_name_numbering. Appendix F Miscellaneous Code % *** % *** Main driver % *** % *** _ Brian J. Ross % *** Dept. of Computer Science % *** University of British Columbia y0 *** mixbruce(File,Call) :— translate(File,Prolog), mixcall(File,Call), I, mixcall(File,Call) :— writel('* Mixing program ... *',nl), mix(Call,Mixed), atom_append(File,' .pmix' ,PFile), writel('* Mixing complete (see "^PFile,"1) *',nl), print prolog(PFile,Mixed), % brucify (Mixed ,B r uce), atom_append(File,'.bmix' ,BFile), writel('* Bruce generated (see "'jBFile,'") *',nl), print_bruce(BFile,Bruce), writel(nl,'* DONE. *',nl), I. 138 APPENDIX F. MISCELLANEOUS CODE mixprolog(File,Call) :— writel('* Reading Prolog in 11',File,'" *',nl), [File], % mixcall(Call), parse(File) :— translate(File,Prolog), writel(nl,'* DONE. *',nl), I. translate(File,Prolog) :-start_up, alt_read_file (File, D at a), writel('* "',File,'" read *\nl), % lexical(Lex,Data), writel('* Lexical succeeds *',nl), % env(Tree,Lex,[]), writel('* Parse succeeds *',nl), % pretty (Tree), % gen_prolog(File,Tree, Prolog), atom_append(File,'.pro' ,PFile), writel('* Prolog generated (see '"jPFile,"') *',nl), print_prolog( PFile ,Prolog), assert_prolog(Prolog), % brucify(Prolog,B), atom_append(File,' .bru',BFile), writel('* Bruce generated (see "»,BFile,'") *',nl), print_bruce(BFile,B), % lexical(Lex,Data) converts the characters Data into lexical tokens % in Lex. lexical(Lex,Data) :— lex(Lex,_,Data,[]). APPENDIX F. MISCELLANEOUS CODE 140 % some cleaning up... startjip :— tabolish, reset_gen_nums, gen_prolog(File,Tree,Prolog) :— Tree" "code(Code), flatten(Code,Prol), writel('* Basic semantics created *',nl), atom_append(File,'. bas' ,BFile), writel('* ... (see "',BFile,'") *',nl), print_prolog( B File,Prol), (found_a_branch — > gen_labelprogs(Prol,Pro2), writel('* Label programs created *',nl), atom_append(File,' .lab',LFile), writel('* ... (see "',LFile,'") *',nl), print_prolog(LFile,Pro2), % process_branches(Pro2,Prolog), writel('* Branches processed *',nl) Prolog = Prol), % *** % *** Prolog dataflow checking utilities % *** % % order(Goals,A,B) is satisfied if B is dependent on A wrt data flow % One of five tests is performed to determine dataflow ordering: % (a) B's input matches A's output — succeeds. % (b) A's input matches B's output — failure. % (c) variables in test B are a subset of mechanism A's output — succeed. % (d) like (c), but A and B reversed % (e) No direct correlation with A and B, so the list of remaining goals % is used for a recursive dataflow check. APPENDIX F. MISCELLANEOUS CODE 141 order(Goals,A,B) :— vars_used(A,VAI,VAO), vars_used(B,VBI,VBO), VAO == VBI, order(Goals,A,B) :— varsused(A,VAI,VAO), vars_used(B,VBI,VBO), VAI == VBO, i fail. order(Goals,A,B) :— is_a_test(B), extract_vars(B,VB), vars_used(A,VAI,VAO), subset(VB,VAO), !, order(Goals,A,B) :— is_a_test(A), extract_vars(A,VA), vars_used(B,VBI,VBO), subset(VA,VBO), I faU. order(Goals,A,B) :— remove_items([A,B],Goals,G2), member2(C,G2), remove_item(C,G2,G3), order(G3,A,C), order(G3,C,B), % % dep_in_vars(A,B) succeeds if the (input) variables in A are dependent % or a subset of the input variables in B. dep_in_vars(Test,B) :— is_a_test(Test), extract_vars(Test,TV), vars_used (B ,In,_), subset(TV,In), APPENDIX F. MISCELLANEOUS CODE 142 dep_in_vars(A,B) :— vars_used(A,InA,_), vars_used(B ,InB,_), subset(InA,InB), % % dep_out_vars(A,B) succeeds if the (input) variables in A are dependent % or a subset of the output variables in B. dep_out_vars(Test,B) :— is_a_test(Test), extract_vars(Test,TV), vars_used(B,_,Out), subset(TV,Out), dep_in_vars(A,B) :— vars_used(A,InA,_), vars_used(B,_,OutB), subset(InA,OutB), I % % same_out_vars(A,B) succeeds if A and B have the same output variables. same_out_vars(A,B) :— vars_used(A,_,OutA), vars_used(B ,_,OutB), OutA == OutB, i % % order_clause_goals(L,S) orders goals in L, resulting in S. order_clause_goals(L,S) :— insort(L,S). % % from Clocksin & Mellish, pp.146 ... insort(0,D) - !• insort([X|L],M) :-APPENDIX F. MISCELLANEOUS CODE 143 nsort(L,N), insortx(X,N,M), insortx(X,[A|L],[A|M]) :-order([A|L],A,X), ! •? insortx(X,L,M). insortx(X,L,[X|L]). % *** % *** some variable vector utilities % *** % % gen_vec(A,B) creates a list of 'fresh' variables of the same size as list A. gen_vec([],[]). gen_vec([Name|A],[New|B]) :-gen_vec(A,B)-% % var_match(Name,Input,Var) matches variable Name with the variable names % in storematch for the current program. The corresponding logical variable % in Input is returned in Var. var_match(Name,Input,Var) :— curr_prog(Prog), storemat ch( P rog, Var s,_,_,_), append(A,[Name|B],Vars), count(A,S), T is S + 1, nmember(T,Input,Var), I. % % A variant of Initial is created, in which Var_i is replaced by Var_f. vec_variant(Initial,Varj ,Var_f,Final) :— break(Var_i,A,[B|C] .Initial), append(A,[Var_f|C],Final), i APPENDIX F. MISCELLANEOUS CODE 144 % ;  % match_vars(A,B,C) matches variable names in A with their logical % variable values, as are listed in B, resulting in C. match_vars( [],_, _). match_vars([A|L],Input,[V|R]) :— var_mat ch (A ,Input, V), match_vars(L,Input,R). 7o % set_outputs(Vars,In,Out,Ans) matches each variable in Vars % with its corresponding output variable, as determined by In and Out. set_outputs( [],_,_,[]). set_outputs([Var|A],In,Out,[Outvar|D]) :— set_output(Var,In,Out,Outvar), set_outputs(A,In,Out,D). set_output(Var,__.,Var). set_output(Var,[I|A],[0|B],Ans) :-(Var == I -> Ans = O; set_out put (Var, A ,B, Ans)). % *** % *** List utilities % *** % % program_separate(Env,Labels,Collect,Prolog) separates predicates into % the sections used by the original Bruce source programs. % The Labels list these predicate names. program_separate(Env,[],Prolog,Prolog). program_separate(Env,[[Prog|Labels]|Rest],Collect,Prolog) :— get_pgms(Env,[Prog|Labels],Some), (Some == [] -> program_separate(Env,Rest,Collect,Prolog) program_separate(Env,Rest,[Prog,Some|Collect],Prolog)). % APPENDIX F. MISCELLANEOUS CODE % get_pgms(Env,Labels, Collect,Result) collects all the clauses in Env % which are listed in Labels list. get_pgms(Env,[],[]). get_pgms(Env,[Label|Rest],A) :-get_label_refs(Env,Label,[] ,Refs), (Refs == Q -> get_pgms(Env ,Rest, A) i get_pgms (En v ,Rest ,B), append(Refs,B,A)). % _ % getjabeljrefs(Env, Label, Collect,Result) collects all the clauses in Env % named by Label. getjab el_refs( [] ,L abel ,Refs ,Refs). get_label_refs([(Head :- Body)|Rest],Label,Collect,Refs) :— i •> . (functor(Head,Label,_) — > get_label_refs(Rest,Label,[(Head :- Body)|Collect],Refs) i getjab el_refs (Rest ,L abel, Collect ,Refs)). getJabel_refs([Clause|Rest],Label,Collect,Refs) :— i •> (functor(Clause,Label,_) —> get Jabel_refs(Rest, Label, [Clause| Collect],Refs) getjab el_refs (Res t ,L abel,Collect, Refs)). f0 *** % *** Miscellaneous Prolog utilities... % *** % % member routine in which the Items may be uninstantiated % (logical variable matching). member(_,[|) :- !,fail. member(Item,[X|J) :— Item = = X. member(Ans,[_|Rest]) :-APPENDIX F. MISCELLANEOUS CODE 146 member(Ans,Rest). % member2 doesn't handle logical variable objects. member2(Item,[Item |_]). member2(Ans,[_|Rest]) :— member2(Ans,Rest). % memberS tests if the ground parts of terms are equivalent. % (corresponding variables may be different) member3(Goal,[]) :- !,fail. member3(Goal,[Item|_]) :— ground_eq(Goal,Item). member3(Goal,L|R]) :-member3(Goal,R). % \ % ground_eq(A,B) tests if the ground portions of A and B are equivalent. % In other words, terms A and B must be equal, except that variables may be % renamed. ground_eq(A,B) :— var(A), var(B), ground_eq(A,B) :— (var(A) ; var(B)), I fail. ground_eq(A,B) :— A == B, I, ground_eq([Al|A2],[Bl|B2]) :-i ground_eq(Al,Bl), ground_eq(A2,B2). ground_eq(A,B) APPENDIX F. MISCELLANEOUS CODE 147 ! •) A =.. [Name|ArgsA], B =.. [Name|ArgsB], ground_eq(ArgsA,ArgsB). % atomjappend appends atom names together. atom_append(Atoml,Atom2,Newatom) :-name(Atoml,A), name(Atom2,B)> append(A,B,C), name(Newatom,C), i % % Count the number of elements in a list count(Q,0) :- !. count(L|L],N) :-count(L,M), N is M + 1, % % nmember(N,L,I) retrieves the Nth element I of list L nmember(Num,List,Item) :— nmember( 1 ,Num,List ,Item), I. nmember(N,N,[Item|_],Item). nmember(Curr,Num,L|Rest],Ans) :— Next is Curr + 1, nmember(Next,Num,Rest,Ans). % % break(Item,Front,End,List) breaks List up into Front and End, such % that Item is the first item in End. break(Item,[],[A|B],[A|B]) :-Item == A. break(Item,[B|R],E,[B|C]) :-APPENDIX F. MISCELLANEOUS CODE 148 Item \== B, break(Item,R,E,C). % args_to_list(A,B) converts the argument structure A to a list B. args_to_list(A,[A]) :— var(A), args_to_list(A,Tl) :-A =.. [V,X,A1], args_to_list(X,Xl), args_to_list(Al,T), append(Xl,T,Tl), args_to_list(A,[A]) :— !. % fuse a multi— layered goal list into one flat goal list. fuse((A,true),B) :-fuse(A,B), fuse((true,A),B) :— fuse(A,B)> fuse((","),") :- !. fuse((A,"),E) :-fuse(A,E), fuse((",A),E) :-fuse(A,E), fuse(((",B),C),E) :-fuse((B,C),E), fuse(((A,B),C),(D,E)) :-fuse(A,D), fuse((B,C),E), fuse((A,B),(D,E)) :-fuse(A,D), APPENDIX F. MISCELLANEOUS CODE fuse(B,E), fuse(E,E). % % get the input and output vectors for an ORDERED list of goals. get_IO((H:-B),In,Out) :-I •> var s_used (H ,In ,0 ut). get_IO(Goallist,In,Out) :-member2(First,Goallist), vars_used(First,In,_), rev(Goallist,Rev), member2(Last,Rev), vars_used(Last,_,Out), i % % get_prev_IO(Goals,Prev,In,Out) determines the In and Out vectors % for the list of Goals. Should Goals be composed of calls which do not % have intrinsic 10 vectors, the 10 vectors of Prev are returned instead. get_prev_I0(Goals,_,In,Out) :— get_IO(Goals,In,Out), get_prev_I0(_,Prev,In,0ut) :— get_I0([Prev],In,0ut), % % get a term's input and output variable vectors ... vars_used(A,_,_) :— is_a_test(A), !? fail. vars_used(A,In,Out) :— A =.. [_,ln,0ut], vars_used(asgn(In,_^.,0ut),ln,0ut) :— APPENDIX F. MISCELLANEOUS CODE varsjised(goto(In,_,Out),In,Out) :— % % extract_vars(V,A) removes all the variables used in V into list A, % without duplicates. extract_vars(V,A) :— extract_vars(V,[],A), I extract_vars(V,Collect,A) :— var(V), (member(V,Collect) -> A = Collect A = [V | Collect]). extract_vars(X,A,A) :— (X == [] ; atom(X)). extract_vars([V|R],Collect,A) :-extract_vars(V,Collect ,X), ext ract_vars( R ,X, A). extract vars(X,Collect,A) :— X =.. UL], extract_vars(L,Collect,A). % test if a term is an expression (namely, a boolean test) ... is_a_test(Thing) :— functor(Thing,Name,_), name(Name,String), (op_chars(String,bool(_));op_chars(String,rel(_))), is_a_test(Thing) :-member(Thing,[true,false]), % : % test if two expressions are complementary APPENDIX F. MISCELLANEOUS CODE 151 complementary(A,B) :- not(not(A =.. ['~',B]))-complementary(A,B) :- not(not(B =.. ['""',A])). % % remove_item(Item,List,Newlist) removes the first instance of Item in List, % resulting in Newlist. remove_item(_,[|,[|) :— !. remove_item(Item,[Item|X],X) :— remove_item(Item,[X|Y] ,[X|Ans2]) :-remove_item(Item,Y,Ans2), !. % % remove_item2(Item,List,Newlist) removes the first instance of Item in List, % resulting in Newlist. It differs from removejtem in that no unification % is done when matching items. remove_item2(_,Q,Q) :— !. remove_item2(ItemA,[ItemB|X],X) :— Item A == ItemB, ;# remove_item2(Item,[X|Y],[X|Ans2]) :-removeJtem2(Item,Y,Ans2), % split the clause into its Head, and a list of the goals in the Body. split_clause((Head :— Body),Head,Bodylist) args_to_list(Body,Bodylist), i % % Copy structure A into B, so that it has unique variables copy(A,B) :-assert(copied(A)), retract(copied(B)), I APPENDIX F. MISCELLANEOUS CODE % % flatten a multi—layered list into a one—dimension list. flatten(Q,Q) :- !. flatten([[]|A],B) :-flatten(A,B), I, flatten([[A|B]|C],D) :-flatten([A|[B|C]],D), flatten([A|B],[A|C)) :-A \== Q, A \== LU, flatten(B,C), |# % % permutation(A,B) checks if the items in list A are a variation of those % in list B, in terms of ordering. permutation(Q,[|). permutation([A|B],C) :— C \== [], remove_item(A,C,D), permutation(B,D), i, % % append2 is a deterministic append. append2([],L,L) :— !. append2([X|R],L,[X|Rl]) :- append2(R,L,Rl). % % append_list(L,R) appends the lists found in list L together, resulting % in R. append_list([],[]) :— !. append_list([A],A) :— !. append_list([A,[]],A) :- !. append_list([A,B|C],D) :-append(A,B)E), APPENDIX F. MISCELLANEOUS CODE 153 append_list([E|C],D), % % subset(A,B) succeeds if the elements in A are all in B. subset( []_,). subset([X|R],U) :-member(X,U), subset(R,U), I, % ; % remove_items(A,B,C) removes the items in list A from list B, resulting in C. remove_iteiris( [], A, A). remove_items([A|B],C,D) :— remove_item(A,C,E), removejtems(B,E,D), I. % % remove_items2(A,B,C) removes the items in list A from list B, resulting in C. % Unlike removejtems, no unification is done when item matching. remove_items2([],A,A). remove_items2([A|B],C,D) :— remove_item2(A,C,E), remove_items2(B,E,D), !_ % % writeJist(Direction, Write,List) writes the List in the desired % direction(vert,horz), using the goven write routine Write. write_list(__.,[]) :- !. write_list(vert,WriteRtn,[A|B]) :-Write =.. [WriteRtn,A], Write,nl, write_list(vert,WriteRtri,B), I. write_list(horz,WriteRtn,[A]) :— APPENDIX F. MISCELLANEOUS CODE 154 i •> Write =.. [WriteRtn,A], Write. writejist(horz,WriteRtn,[A | B]) : -Write =.. [WriteRtn,A], Write, write(','), writejist (horz ,WriteRtn ,B). % % convert a list of goals to a body of goals list_to_body([],") :- !. list_to_body([A],A) :- !. list_to_body([A|C],(A,D)) :-list_to_body(C,D), i % % duo_split(Side,LI,Leftl,Rightl,L2,Lefts,Right2) splits Ll and L2 into % equal size, non-null parts, depending if Side is 'left' or 'right'. duo_split(right,Ll,Leftl,Rightl,L2,Left2,Right2) :-append( Left 1 ,Right 1 ,L 1), Leftl \== [], Rightl \== [], count(Rightl,N), append(Left2,Right2,L2), count(Right2,N). duo_split(left,L 1 ,Leftl,Right 1 ,L2,Left2,Right2) :-rev(Ll,RLl), rev(L2,RL2), append(RLeftl,RRightl,RLl), RLeftl \== Q, RRightl \== [], count(RRightl,N), append(RLeft2,RRight2,RL2), count(RRight2,N), rev(RLeftl,Rightl), rev(RLeft2,Right2), APPENDIX F. MISCELLANEOUS CODE rev(RRightl,Leftl), rev(RRight2,Left2). % % list reverser... rev(X,RX) :-revx(X,[],RX),!. revx(Q,R,R) :-revx([X|Y],Z,R) :-revx(Y,[X|Z],R). % % find_clause(Prolog,Head, Clause) finds a clause in Prolog with head Head. % Repeated calls return new results. find_clause(Prolog,Head,Clause) :— member2(Clause,Prolog), split_clause( Clause,Head2 ^), not not Head = Head2. % % find_goal(Clause,Head,Left,Goal,Right) finds Goal within the body of % Clause. Left and Right are the goals on each side of the goal. fmd_goal(Clause,Head,Left,Goal,Right) :— split_clause(Clause,Head,Goals), append(Left,[Goal|Right], Goals), !, % % make_clause (Head, Left, Right, Clause) appends lists Left and Right together, % converts them into a body structure, and forms a clause with head Head. % Note: There must already exists proper input—output between the constructs make_clause(Head,[],[],Head). make_clause(Head,Left,[],(Head :- Body)) :— list_to_body (Left,Body). APPENDIX F. MISCELLANEOUS CODE 156 make_clause(Head,[],Right,(Head :- Body)) :— list_to_body(Right,Body). make_clause(Head,Left,Right,(Head :— Body)) :— app end( Left ,Right, Goals), list_to_body(Goals,Body). % % mergejjoalsflA^AfAJB^B^JnfOu^G) appends goal lists A and B into G, % while assuring that the 10 of the two lists is merged. In and Out contain % the 10 of the result. merge_goals(_,_,Q_.,_,0,_,_,[]) :- !. merge_goals(_,_,_,IA,OA,A,In,Out,G) :— copy((IA,OA,A),(In,Out,G)), i_ merge_goals(IA,OA,A^_.,0,In,Out,G) :— copy((IA,OA,A),(In,Out,G)), I. merge_goals(IA,OA,A,IB,OB,B,In,Out,G) :-copy((IA,OA,A,IB,OB,B),(In,OA2,A2,IB2,Out,B2)), OA2 = IB2, append(A2,B2,G), I, % % append_goals(Clause,Vec,Code,Newclause) adds the goals in Code to the goals % of Clause, resulting in Newclause. append_goals(Clause,Vec,Code,(Newhead :— Body)) :— copy((Clause,Vec,Code),(Clause2,Vec2,Code2)), split_clause(Clause2,Head,Goals), Head =.. [Name,Il,Ol], get_prev_IO(Goals,(Il,Il),I2,Vec2), append(Goals,Code2,G), get_IO(G,I3,03), Newhead =.. [Name,Il,03], list_to_body(G,Body), APPENDIX F. MISCELLANEOUS CODE % : % parent_clause(Prolog,Head,Parent,Phead,Left,Goal,Right): % Prolog — current prolog environment % Head — clause to find a parent for % Parent — the found parent clause % Phead, Left, Goal, Right — the breaking up of Parent such that % Phead is the head, Goal is the call to Head, and Left/Right % are goals to the left and right of Goal % % A parent clause is found. Recursive calls are not used — a clause cannot % be its own parent. parent_clause(Prolog,Head,Paxent,Phead,Left,Goal,Right) :— copy (Head, Goal), member 2 (P arent ,P rolog), split_clause(Parent,Phead,Goals), not Phead = Head, append(Left,[Goal|Right],Goals). % sibling_clause (Prolog, Clause, Sibling) finds a sibling for Clause from Prolog. sibling_clause(Prolog,Clause,Sibling) :— split_clause(Clause,Head,_), copy(Head,Item), member2(Sibling,Prolog), split_clause(Sibling,Item,_), Sibling \== Clause. % % assertjprolog(P) tasserts all the code in list P. assert_prolog(_) :- !. assert_prolog([Clause|Rest]) :— tassertz(Clause), assert_prolog(Rest), |# % % Make an atom like Name into one which is capitolized. APPENDIX F. MISCELLANEOUS CODE 158 capitolize(Name,Caps) :— name(Name,[A|L]), A >= 97, A =< 122, A2 is A - 32, name(Caps,[A2|L]), capitolize(Name,Name). % % Read: (written by Doug Westcott) % % The following routines allow the reading of a file's contents into % prolog in the form of a list of characters' ASCII numbers (the usual % prolog representation of a string). % alt_read_file(File,Contents) :— read_file(File,Contentsl), reduce_white_space( Content s 1 ,Contents), I, read_file(File,Contents) :— seeing(OldFile), see(File), getO(Char), read_filel(Char,Q,RContents), seen, seeing(OldFile), reverse(RContents,Contents), !. read_nlel(Char,Sofar,Sofar) :— end_of_file(Char), I, read_filel(Char,Sofar,Contents) :— getO(Newchar), read_filel(Newchar,[Char|Sofar],Con tents), i APPENDIX F. MISCELLANEOUS CODE 159 endpffile(-l) :-?. reduce_white_space(01d,New) :— change_to_spaces(01d,Mid), reduce_spaces(Mid,New), ;# change_to_spaces([Char|Chars],[NewChar|NewChars]) :-change_to_space(Char,NewChar), l •, change_to_spaces(Chars,NewChars), I. change_to_spaces([],[]) :— I. change_to_space(09,32). changeJo_space(10,32). change_to_space( 11,32). change_to_space( 12,32). change_to_space(X,X). reduce_spaces([32,321Chars],NewChars) :-reduce_spaces([32|Chars],NewChars), reduce_spaces([Char|Chars],[Char|NewChars]) :— reduce_spaces(Chars,NewChars), reduce_spaces([],[]) :— % *** % *** Tagged assertion utilities % *** % % tassert routines assert clauses, plus update a tag to be used for % later removal. tassert(Clause) :— set_rem_clause( Clause), assert(Clause), APPENDIX F. MISCELLANEOUS CODE I. tasserta(Clause) :— set_rem_clause( Clause), asserta( Clause), tassertz(Clause) :— set_rem_clause( Clause), assertz(Clause), % ; % set rem_clause tag. If predicate exists already before a tag has been set, % then do not set a remove tag, as this predicate is used elsewhere. set_rem_clause((Head :— Goals)) :— functor(Head,Name,Arity), set_rem_clause2(Name,Arity), set_rem_clause( Clause) :— functor(Clause,Name,Arity), set_rem_clause2(Name,Arity), set_rem_clause2(Name,Arity) :— rem_clause(Name,Arity), I. set_rem_clause2(Name,Arity) :— current_predicate(Name,Head), functor(Head,Name,Arity), set_rem_clause2(Name,Arity) :— i assertz(rem_clause(Name,Arity)). % % remove a predicate asserted with tassert utility tabolish(Pred,Arity) :— rem_clause(Pred,Arity), abolish(Pred,Arity), retract(rem_clause(Pred,Arity)). tabolish(_,_). APPENDIX F. MISCELLANEOUS CODE 161 % remove all clauses asserted by tassert utilities tabolish :— rem_clause(Name,Arity), abolish(Name,Arity), fail, tabolish :— abolish(rem_clause,2). % list writing routine (written by Doug Westcott) writel([A|B]) :-write_item(A), writel(B), writel(Q) :-writel(A) :— writel([A]), 1. writel(A,B) :-writel([A,B]), !. writel(A,B,C) :-writel([A,B,C]), j. writel(A,B,C,D) :-writel([A,B,C,D]), writel(A,B,C,D,E) :-writel([A,B,C,D,E]), ;# writel(A,B,C,D,E,F) :-writel([A,B,C,D,E,F]), writel(A,B,C,D,E,F,G) :-writel([A,B,C,D,E,F,G]), APPENDIX F. MISCELLANEOUS CODE 162 writel(A,B,C,D,E,F,G,H) :-writel([A,B,C,D,E,F,G,H]), writel(A,B,C,D,E,F,G,H,I) :-writel([A,B,C,D,E,F,G,H,I]), !. writel(A,B,C,D,E,F,G,H,I,J) :-writel([A,B,C,D,E,F,G,H,I,J]), i, writejtem(X) :— var(X), write(X), write item(nl) :— nl, write_item(tab(N)) :— tab(N), write_item(X) :— write(X), Appendix G Binary GCD Basic Semantics bingcd([Gcdl,Ul,Vl],[Gcd2,U2,V2]) :-asgn([Gcdl,Ul,Vl,Kl,Pl,Tl],K2,0,[Gcdl,Ul,Vl,K2,Pl,Tl]), testl([Gcdl,Ul,Vl,K2,Pl,Tl],[Gcd2,U2,V2,K3,P2,T2]). testl([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-U1//2*2=\=U1, b2([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]). testl([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-"U1//2*2=\=U1, test2([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]). test2([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-V1//2*2=\=V1, b2([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]). test2([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-~V1//2*2=\=V1, asgn([Gcdl,Ul,Vl,Kl,Pl,Tl],K3,Kl+l,[Gcdl,Ul,Vl,K3,Pl,Tl]), asgn([Gcdl,Ul,Vl,K3,Pl,Tl],U3,Ul//2,[Gcdl,U3,Vl,K3,Pl,Tl]), asgnQGcdl.US^LKS^LTlivs.Vl/^iGcdLUS.VS^S.Pl.Tl]), bl([Gcdl,U3,V3,K3,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]). test3([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-Ul//2*2=\=U1, asgn([Gcdl,Ul,Vl,Kl,Pl,Tl],T3,0-Vl,[Gcdl,Ul,Vl,Kl,Pl,T3]), b4([Gcdl,Ul,Vl,Kl,Pl,T3],[Gcd2,U2,V2,K2,P2,T2]). 163 APPENDIX G. BINARY GCD BASIC SEMANTICS 164 test3([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :--U1//2*2=\=U1, asgn([Gcdl,Ul,Vl,Kl,Pl,Tl],T3,Ul,[Gcdl,Ul,Vl,Kl,Pl,T3]), asgn([Gcdl,Ul,Vl,Kl,Pl,T3],T4,T3//2,[Gcdl,Ul,Vl,Kl,Pl,T4]), test4([Gcdl,Ul,Vl)Kl,Pl,T4],[Gcd2)U2,V2,K2,P2,T2]). test4([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-T1//2*2=:=T1, b3([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]). test4([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-•T1//2*2=:=T1, test5([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd3,U3,V3,K3,P3,T3]), asgn([Gcd3,U3,V3,K3,P3,T3],T4,U3-V3,[Gcd3,U3,V3,K3,P3,T4]), test6([Gcd3,U3,V3,K3,P3,T4],[Gcd2,U2,V2,K2,P2,T2]). test5([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcdl,U2,Vl,Kl,Pl,Tl]) :-T1>0, asgn([Gcdl,Ul,Vl,Kl,Pl,Tl],U2,Tl,[Gcdl,U2,Vl,Kl,Pl,Tl]). test5([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcdl,Ul,V2,Kl,Pl,Tl]) :-~T1>0, asgn([Gcdl,Ul,Vl,Kl,Pl,Tl],V2,0-Tl,[Gcdl,Ul,V2,Kl,Pl,Tl]). test6([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-T1=\=0, b3([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]). test6([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,Ul,Vl,K2,P2,Tl]) :-~T1=\=0, asgn([Gcdl,Ul,Vl,Kl,Pl,Tl],K2,Kl,[Gcdl,Ul,Vl,K2,Pl,Tl]), callasgn([Gcdl,Ul,Vl,K2,Pl,Tl],Tmpl,2), callasgn([Gcdl,Ul,Vl,K2,Pl,Tl],Tmp2,K2), power([Pl,Tmpl,Tmp2],[P2%.137447,_137448]), asgn([Gcdl,Ul,Vl,K2,P2,Tl],Gcd2,Ul*P2,[Gcd2,Ul,Vl,K2,P2,Tl]). bl([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) testl([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]). b2([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-test3([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]). APPENDIX G. BINARY GCD BASIC SEMANTICS b3([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-asgnCfGcdl^^V^Kl.P^TlJ.TS^l/^^Gcd^Ul.Vl.K^Pl.Ta]), test4([Gcdl,Ul,Vl,Kl,Pl,T3],[Gcd2,U2,V2,K2,P2,T2]). b4([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-test4([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]). Appendix H Partially Evaluated Binary GCD Semantics bingcd([Gcdl,7,Vl],[Gcd2,U2,V2]) :-asgn([Gcdl,7,Vl,0,Pl,Tl],T3,0-Vl,[Gcdl,7,Vl,0,Pl,T3]), b4([Gcdl,7,Vl,0,Pl,T3],[Gcd2,U2,V2,D7,P2,T2]). test4([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-T1//2*2=:=T1, b3([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]). test4([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-~T1//2*2=:=T1, test5([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd3,U3,V3,K4,P4,T3]), asgn([Gcd3,U3,V3,K3,P3,T3],T3,U3-V3,[Gcd3,U3,V3,K3,P3,T4]), test6([Gcd3,U3,V3,K3,P3,T4],[Gcd2,U2,V2,K2,P2,T2]). test5([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcdl,U2,Vl,Kl,Pl,Tl]) :-T1>0, asgn([Gcdl,Ul,Vl,Kl,Pl,Tl],U2,Tl,[Gcdl,U2,Vl,Kl,Pl,Tl]). test5([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcdl,Ul,V2,Kl,Pl,Tl]) :-"T1>0, asgn([Gcdl,Ul,Vl,Kl,Pl,Tl],V2,0-Tl,[Gcdl,Ul,V2,Kl,Pl,Tl]). test6([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-T1=\=0, b3([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]). 166 APPENDIX H. PARTIALLY EVALUATED BINARY GCD SEMANTICS test6([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,Ul,Vl,K2,P2,Tl]) :-~T1=\=0, asgn([Gcdl,Ul,Vl,Kl,Pl,Tl],K2,Kl,[Gcdl,Ul,Vl,K2,Pl,Tl]), callasgn( [Gcdl ,U 1 ,V1 ,K2 ,P 1 ,T 1] ,Tmp 1,2), caUasgn([Gcdl,Ul,Vl,K2,Pl,Tl],Tmp2,K2), power([P 1 ,Tmpl,Tmp2] ,[P2,Tmp3,Tmp4]), asgn([Gcdl,Ul,Vl,K2,P2,Tl],Gcd2,Ul*P2,[Gcd2,Ul,Vl,K2,P2,Tl]). b3([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-asgn([Gcdl,Ul,Vl,Kl,Pl,Tl],T3,Tl//2,[Gcdl,Ul,Vl,Kl,Pl,T3]), test4([Gcdl,Ul,Vl,Kl,Pl,T3],[Gcd2,U2,V2,K2,P2,T2]). b4([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]) :-test4([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,U2,V2,K2,P2,T2]). 

Cite

Citation Scheme:

    

Usage Statistics

Country Views Downloads
Norway 7 0
China 5 35
United States 5 4
France 3 0
Japan 2 0
Pakistan 1 0
Kazakhstan 1 0
Austria 1 0
Poland 1 0
City Views Downloads
Oslo 7 0
Shenzhen 5 26
Unknown 5 5
Ashburn 4 0
Tokyo 2 0
Islamabad 1 0
Anaheim 1 1
Aqtau 1 0

{[{ mDataHeader[type] }]} {[{ month[type] }]} {[{ tData[type] }]}
Download Stats

Share

Embed

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"
                            src="{[{embed.src}]}"
                            data-item="{[{embed.item}]}"
                            data-collection="{[{embed.collection}]}"
                            data-metadata="{[{embed.showMetadata}]}"
                            data-width="{[{embed.width}]}"
                            async >
                            </script>
                            </div>
                        
                    
IIIF logo Our image viewer uses the IIIF 2.0 standard. To load this item in other compatible viewers, use this url:
http://iiif.library.ubc.ca/presentation/dsp.831.1-0051940/manifest

Comment

Related Items