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

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

Item Metadata

Download

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

Full Text

T H E 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 T H E REQUIREMENTS FOR T H E D E G R E E OF MASTER OF SCIENCE in T H E FACULTY OF G R A D U A T E STUDIES (DEPARTMENT OF C O M P U T E R SCIENCE)  We accept this thesis as conforming to the required standard  T H E UNIVERSITY OF BRITISH COLUMBIA July 1988 © Brian J. Ross, 1988  In  presenting  degree freely  at  this  the  available  copying  of  department publication  of  in  partial  fulfilment  University  of  British  Columbia,  for  this or  thesis  reference  thesis by  this  for  his thesis  and  scholarly  or for  her  Department  V6T  DE-6(3/81)  1Y3  Columbia  I further  purposes  gain  the  requirements  I agree  shall  that  agree  may  representatives.  financial  permission.  The University of British 1956 Main Mall Vancouver, Canada  study.  of  be  It not  is  that  the  Library  permission  granted  by  understood be  for  allowed  an  advanced  shall for  the that  without  make  it  extensive  head  of  my  copying  or  my  written  Abstract The feasibility of using Horn clauses as a means of describing and transforming imperative programs 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 representations. 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 automatic 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 translated 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 Semantics  4  2.1.2  Logical Semantics  5  2.1.3  Denotational Semantics  8  2.1.4  Operational Semantics  9  2.1.5  Algebraic Semantics  9  3  4  2.2  Program Transformation  2.3  Partial Evaluation  9 12  A n Imperative Language Called Bruce  14  3.1  Design Motivations  14  3.2  Syntax  15  3.3  Operational Semantics  16  A Horn Clause Semantics  23  4.1  Design Goals  23  4.2  Basic Bruce Semantics  25 iii  5  6  7  4.3  Program Branches  30  4.4  Logic Program Interpretation and Completeness  33  4.5  Translating Logic to Bruce  35  4.6  Example Translations  37  A Bruce-Logic Translation System  46  5.1  The logic generator  46  5.2  The Brucifier  52  The Partial Evaluation of Bruce Programs  59  6.1  Partial evaluation and program transformation  59  6.2  Implementation  61  6.3  Example transformations  64  Discussion  69  7.1  Related work  69  7.2  Conclusions and further work  72  Bibliography  77  A Partial Evaluator Source  82  B  89  Bruce Parser  C Branch Handling  106  D Bruce Generation  117  E  Program Printing Utilities  131  F  Miscellaneous Code  138  G Binary G C D Basic Semantics  163  H  166  Partially Evaluated Binary G C D Semantics  iv  List of Figures 3.1  Syntax of expressions  15  3.2  Syntax of higher-level constructs  17  3.3  Definition of Comp  19  3.4  Definition of Buildenv  20  3.5  Example Program  21  3.6  Buildenv Output  21  4.1  Logical semantics of Bruce constructs (no branching)  27  4.2  Branching out of two loops  32  4.3  Converting Branches  37  4.4  Consecutive assignments  37  4.5  While loop  38  4.6  Two alternate Bruce realizations  38  4.7  Subprogram invocation  39  4.8  Branching within a chain  40  4.9  Bruce equivalent  40  . . .  4.10 End of file control scheme (initial)  41  4.11 Logical Form  42  4.12 Derived result  43  4.13 Jumping into a repeat loop  44  4.14 Bruce equivalent  45  5.1  Chain rules  47  5.2  While-loop rule  48  5.3  Branching into two loops  49  v  5.4  Basic semantics  50  5.5  Label program  51  5.6  Label program predicate  51  5.7  Final semantics  53  5.8  Branch out of two loops  54  5.9  Basic semantics  54  5.10 Final semantics  55  5.11 Distributed program predicate  55  5.12 While loop matching  56  5.13 Derived Bruce program  57  5.14 Derived Bruce program  58  6.1  Partial evaluator  62  6.2  Goal inhibition  6  6.3  Binary powers  65  6.4  Residual programs (n = 5)  65  6.5  Residual programs (x = 2, n = 5)  65  6.6  Binary gcd (u = 7)  66  6.7  A suspended test  67  6.8  Polyvariant logical result  67  6.9  Polyvariant Bruce result  68  vi j  3  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 transformation 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 opportunities 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 programming 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 prog source. In particular, we will show that imperative programs can be economically described 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 correct 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 logical representation reflect corresponding changes to the source program. Interpreting the semantics as a logic program means that one specific type of program transformation - partial 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 define 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 implementing 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 evaluated 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  F o r m a l  2.1.1  P r o g r a m  Semantics  Goals of P r o g r a m Semantics  Programming languages are complex systems. Since conventional programming languages are tailored around the architecture of von Neumann machines, operations in these languages 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 firstorder 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 Pascal).  etal. 73] has a treatment of  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 below), 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 However, Hoare logic has been criticized for its often unsound and ad hoc  etal. 77].  axioms, and  dissatisfaction has arisen to the ways in which different program constructs have been handled [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 firstorder 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 programming discipline in which programs are constructed from logical specifications using firstorder 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 conventional 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 subsidiary 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 extended 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 theorem 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 interpretations 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 program 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 mathematically 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, implementability issues are not dealt with.  CHAPTER 2. REVIEW  2.1.4  9  O p e r a t i o n a l 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  A l g e b r a i c 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  P r o g r a m  T r a n s f o r m a t i o n  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 reliable 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 "program transformation" is a general one; it has been used in reference to program transformation 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 methodology, as one can consider the original program given to optimizing transformation systems as the "specification" used by synthesis systems. Program transformation differs from program 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 program 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 simplifications. 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 general 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 transformation 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 motivated by correctness considerations; transformations applied to programs are always assured 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 approaches 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 systems 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.  2.3  REVIEW  Partial  12  E v a l u a t i o n  P a r t i a l e v a l u a t i o n , or m i x e d c o m p u t a t i o n , is a c o m p u t a t i o n a l p a r a d i g m w h i c h is currently g a i n i n g more attention i n research i n logic and functional p r o g r a m m i n g , as well as convent i o n a l p r o g r a m t r a n s l a t i o n . P a r t i a l evaluation can be applied i n areas such as p r o g r a m exec u t i o n , p r o g r a m o p t i m i z a t i o n and transformation, compiler generation, c o m p i l e r - c o m p i l e r generation, a n d m e t a - p r o g r a m m i n g . [Ershov 82] gives a n i n t r o d u c t i o n to the concept, and outlines how p a r t i a l evaluation can be characterized i n either a functional or operational fashion. (1) F u n c t i o n a l l y : given a p r o g r a m P w h i c h computes some function f(X, obtaining a  Y),  p a r t i a l evaluation is the process of  residual p r o g r a m P w h i c h computes the function f(x,Y) = g(Y), where the  d a t a value of  x  X is x. P is also k n o w n as the projection of P onto x. (2) O p e r a t i o n a l l y : x  a p r o g r a m P defines a set C of elementary computations.  C itself is partitionable into  subsets C U C", where C are called permissible computations, a n d C" are suspendable computations.  P a r t i a l evaluation is the process w h i c h executes C  p r o g r a m P^ w h i c h defines the c o m p u t a t i o n  and forms a residual  C".  These t w o characterizations are generalized i n [Ershov 82] [Ershov 85], i n w h i c h p a r t i a l evaluation is defined by a m a p p i n g :  M-.PxD^PxD where P are programs and D are d a t a domains. T h i s m a p p i n g can be parameterized by an ordered set {p} i n w h i c h po a n d p\ are m i n i m a l and m a x i m a l values i n the set respectively. po represents the case when no d a t a is available to the p a r t i a l evaluator; p\ is the case when a l l the d a t a is available. T h i s metric - the availability of d a t a - effectively describes the nature of p a r t i a l evaluation: depending on the availability of d a t a , some parts of a p r o g r a m can be executed, while other portions w h i c h need undefined d a t a values are left as residual results. T h e most difficult p r o b l e m faced when p a r t i a l l y evaluating a p r o g r a m is controlling the evaluation process. P a r t i a l evaluation first requires the fixing of d a t a values , usually  CHAPTER 2. REVIEW  13  m e a n i n g that p r o g r a m parameters are set. Processing commences by executing a l l the code i n w h i c h the necessary d a t a is defined, while retaining the code w h i c h uses u n k n o w n d a t a values. However, undefined values i n a c o m p u t a t i o n escalate d u r i n g processing according to the d a t a flow i n the p r o g r a m : any value w h i c h uses an undefined value subsequently becomes undefined, and computations using i t become suspendable.  P r o g r a m constructs  such as loops thus present the p o s s i b i l i t y of the infinite generation of residual code. T h e user is given the responsibility of i n d i c a t i n g the h a l t i n g conditions for a p a r t i c u l a r a p p l i c a t i o n . M o s t implementations of p a r t i a l evaluators have been done i n either L i s p or P r o l o g . T h i s is because programs can be treated as d a t a quite naturally w i t h i n these languages, w h i c h is a n advantage when i m p l e m e n t i n g m e t a - p r o g r a m m i n g environments.  A n early  L i s p - b a s e d i m p l e m e n t a t i o n o f a p a r t i a l evaluator is i n [Beckman etal. 76], w h i c h is used for p r o g r a m o p t i m i z a t i o n . [ F u t a m u r a 71] first suggested the use of p a r t i a l evaluation i n the creation o f c o m p i l e r - c o m p i l e r s , w h i c h are programs that transform interpreters i n t o compilers.  [Jones etal. 85] i m p l e m e n t e d a p a r t i a l evaluator i n L i s p w h i c h was used t o  generate compilers and a c o m p i l e r - c o m p i l e r . T w o p a r t i a l evaluators based i n P r o l o g are given i n [Venken 85] and [Takeuchi etal. 85]. T h e V e n k e n system can process full P r o l o g programs; cuts a n d system predicates w i t h side-effects are handled.  However, c o n t r o l  facilities are l i m i t e d to s i m p l y recursion detection and predicate tagging. T h e Takeuchi system does not handle m e t a - l o g i c a l operators such as cut, but has extensive facilities w i t h w h i c h the user can c o n t r o l the p a r t i a l evaluation.  Chapter 3 A n Imperative Language Called Bruce  3.1  D e s i g n  M o t i v a t i o n s  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 conventional 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 C P U and store. All programs written in imperative languages 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(e ...,e ) u  k  | (&i V b ) \ (h A b ) 2  2  | (->&)  where r is a relational operator (eg. <,>,<=, etc.), Expr: e ::=  x \c \ f(e , ...,e ) where x is a variable, c is a constant, / is a function (eg. +, *, / , etc.), x  k  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 Bruce . 1  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  S y n t a x  Brian Ross's Unfriendly Computational Environment  CHAPTER 3. AN IMPERATIVE  LANGUAGE  CALLED  BRUCE  16  T h e s y n t a x of B r u c e is similar to that of P a s c a l [ W i r t h et al. 78] and " C " [ K e r n i g h a n et al. 78] For the sake of brevity, we forego m i n u t e syntactic details i n the following definitions w i t h no loss of generality. A s a result, labels and constants are assumed to have conventional denotations. F i g u r e 3.1 has a B N F - s t y l e g r a m m a r i n d i c a t i n g the construction of boolean a n d m a t h e m a t i c a l expressions.  M o s t c o m m o n relational and arithmetic operators m a y be used.  W e assume that conventional operator bindings are adopted, and t h a t parentheses can be dropped w i t h o u t resulting i n interpretive ambiguities. F i g u r e 3.2 has a B N F - s t y l e s y n t a x of B r u c e programs. Items enclosed i n brackets, such as statement labels, are o p t i o n a l . Items w i t h an overbar (as i n a) represent lists of items. A n environment E contains a l l the programs to be executed i n a p a r t i c u l a r a p p l i c a t i o n , a n d represents the entire c o m p u t a t i o n a l environment.  A p r o g r a m P is a conventional  p r o g r a m or s u b p r o g r a m . A p r o g r a m is denned b y a unique p r o g r a m name  Prognamei,  parameter a n d l o c a l variable definitions, and a p r o g r a m body. Parameters m a y be variable or  call by address parameters (the vector a), or call by value parameters (the vector e).  N o t e that there are no d a t a types i n B r u c e . A chain  Q (also referred to as a train) is  a sequence of one or more statements separated by semi-colons. E a c h statement can be optionally l a b e l l e d . F i n a l l y , a statement S represents a basic B r u c e construct. assignments a n d tests are allowed.  Standard  Skip commands are n u l l instructions w h i c h have no  effect whatsoever. C o n t r o l constructs such as while and repeat loops m a y be used, as well as more p r i m i t i v e constructs such as branches. L a s t l y , subprograms can be invoked w i t h  call statements, where the first list of parameters are variables to be passed by address, a n d the second list are expressions to be passed by value.  3.3  O p e r a t i o n a l  Semantics  E s t a b l i s h i n g an operational semantics involves the definition of an abstract machine or interpreter.  T h e style of this operational semantics is based on those i n [de B r u i n 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 : Var —> 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: E =< oi,o ,...,o-k,... > 2  A function fC is denned as: J. o  k  if E does not terminate if E' =< o~o,...,o~k >  IC simply returns the final result state of terminating computation sequences. A concatenation operator * will be used to construct computation sequences from other sequences.  If < <7 , ...,<7(, > A  and < o , ...,cr > y  z  then E * E =< 1  2  <7 ,...,<7(,,CT , ...,CT 0  V  2  >  CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE  19  1. Comp<E,P, S > <r  Comp < E, P, S; skip » a  2. Comp < E, P, skip > a  <<T>  3. Comp < E, P, skip; Q » a  <cr>* Comp <E,P, Q><T  4. Comp <E,P,  < <r[V < e » <r/x] = <r' > * Comp < £ , P, Q >  x := e; Q > <r  < <T > * (Comp < E, Pt, Q* » a' = £') *Comp<E,P,Q » a - "  5. Comp < £ , P, ca// P,(t>, e);Q > o-  where P,(2,y) : {Q'} € £7, <r,- is a fresh state for P,, *' = (^/z])[V(e-)/2/] <r" = af>,/C(E'),G)  6. Comp<E,P, if(b)then{Qi}else{Q };Q > o2  3  Comp < E, P, Qi; Q » <r Comp <E,P, Q ;Q ><r  (if W « 6 » = true) (if W « 6 >= /a/se)  3  2  3  7 . Comp<E,P, i'/(6)i/ien{Q };Q >cr  Comp < £ , P , t7(6)f/ien{Q }e/se{sifcip}.;Q2 » <*  8. Comp<^E,P, while(b){Qi};Q > a  Comp<. £,P i/(&){Qi;u>/»7e(6){Q }};Q » *  9. Comp < .E , P, repeat{Qi}until(b); Q > a  Comp< ^ P . Q i j i / ^ i r e p e a t i Q j u n t i / ^ l j Q a >  10. Comp < E, P,goto /<;<?> c  < cr > * Comp < E,P,Q' > a where Q' = Buildenv(P Qi),U : Q,- 6 P  1  2  1  2  1  2  )  1  t  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 o . n  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  2  CHAPTER 3. AN IMPERATIVE  f  LANGUAGE  < Q »  CALLED BRUCE  -  < Q; while(b){Q';Q}; Buildenv(P, Q*) > Buildenv(P, Q) = < Q;if(-~b){repeat{Q';Q}until(b)};Buildenv(P,Q*) >  < Q\ Buildenv(P, Q*) >  20  iiP:{Q';Q)  if Q belongs to a while HQ belongs to a repea  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 operational 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  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  21  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,. Using 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 program 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 > (T = K.(Comp < E,Q,Q > o ) 0  0  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 feature 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  T h i s chapter introduces a new semantic methodology for i m p e r a t i v e programs. In particular, a H o r n clause semantics is presented for the B r u c e language of chapter 3. Section 4.1 discusses some of the philosophical motivations b e h i n d the design of the semantics. T h e logical semantics for basic B r u c e programs, t h a t i s , ones i n w h i c h branches are not used, is given i n section 4.2. T h e semantics of branches is then detailed i n section 4.3. Section 4.4 discusses the interpretation of the semantics as logic programs, a n d addresses some completeness issues. Some examples of a c t u a l translations of B r u c e programs conclude the chapter i n section 4.6.  4.1  D e s i g n  Goals  T h e r e are a n u m b e r of design motivations for the logical semantics being i n t r o d u c e d i n this chapter. Since c o m p u t a t i o n is to be defined solely b y the state of the store, the m i n i m a l requirement for the semantics is that it has enough expressive c a p a b i l i t y w i t h w h i c h to describe this characterization of c o m p u t a t i o n . T h i s requirement should not be an obstacle, as predicate logic has proved to be a powerful t o o l i n the semantics of c o m p u t a t i o n a n d p r o g r a m m i n g languages (see section 2.1.2). O u r m a i n m o t i v a t i o n , however, is to define a semantic system w h i c h allows efficient a n d powerful transformations of i m p e r a t i v e - s t y l e programs, namely, those w r i t t e n i n B r u c e .  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 transformation 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 termination 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 relationship between the source language and its corresponding semantic representation. The predicative programming paradigm offers a solution in this regard. The scheme is to define 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 computation 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 semantics means that a richer, sounder, and more automatable transformation system might be possible.  CHAPTER 4. A HORN CLAUSE  4.2  B a s i c  B r u c e  SEMANTICS  25  S e m a n t i c s  We now present the semantics of Bruce programs having no branches . In section 3.3 a 1  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 <= C i A  C  2  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 S ) A (Si k  Ti A ... A T )... A (Tj ^ W\ A ...) A ...) m  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 values . 2  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  27  SEMANTICS  1. Programs: Progname(a,e)  : local x { Q }  =  |= Progname(< a,-,e"j >,< a/,e,- >) <= Q(<ai,ei,Xi>,<a ,e ,x >) }  f  f  2. Chains: Q = Si;5 ;...;5j.  d  2  =  |= Q(vi, v ) = 5i(t}<, d ) A 5 (t;i, U2) A ... A £*(€«,_!,£*) f  2  3.Null operation: 1 = true  sfcip 4. Assignment: a: := e  =  f  5.Program invocation: ca// P(< vi  Vj >,  [= as0n(t;,-, v ,e,vj) x  def  < e i , e k >)  =  |= callasgn(v,x\, AP(<  e\) A ... A ca//as<7n(t>,xjfc, ej,)  Vl,...,Vj,Xi,...,X  k  >,Vf)  6.(a) Test: l/ien { { Qi }} H »7 ( 6 ) Men else { <? }  f  2  |= By) «= 6 A Q i f a , €/)) A (ifi(vi, v ) <r - - 6 A Q(i>,-,«/)) f  2  0 / )  4= 6 A Q^,  6.(b) Test: 1/  ( 6 )  then { Qi }  d  =  |= ( i / < ( « j , A (ifi(v Vi) it  vj))  -16)  7. While loops: tu/u/e ( 6 ) { Q }  d  =  |= (whilei(vi,vj) <= d A Q ^ i , ^ ) Awhilei(v2,Vf)) A (whilei(vi,  Vi) • £ = - > 6 )  8. Repeat loops: repeat  { Q } tmii/  ( 6 )  def =  |=.(repeflrf,-(uj,«/) •£= Q(C,-, €2) A->b A repeati(v , A (repeal (v,-, €/) A 6 )  Figure 4.1: Logical semantics of Bruce constructs (no branching)  2  v/))  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 inputoutput 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 mechanisms. There are four elementary relations representing assignments (line 4), boolean tests, skip statements (line 3), and value parameter evaluation when invoking subprograms. asgn(v{,v ,e, vj) is an elementary relation which represents a state variant. v x  x  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 v in vj with the value of expression e in the context of input x  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 subprogram in question. The input and output vectors within this relation are constructed to match the particular parameter conventions of the program being invoked. A n inputoutput 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  P r o g r a m  B r a n c h e s  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) in which  Q(vi,Vf)  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  (i) P (ii) , ' while (b )i  <*= while(bi){while(b2){goto end}}; end : S <$= (bi Awhile(b2){goto end};while(bi)W -<bi);end:S ^  , ., ,1 w  u>m/e ( 6 2 ) !  }  <7<rfo end  32  SEMANTICS  (bi A(b?/\ goto end;while(b2)v -"62); while(b\) V -161);end : 5 61 A 62 A 50*0 end;u;/ii/e(62); w/ii/e(6i);end : 5  (it;)  V 61 A -162 A while(b\);end : 5 V -161 A end : 5 (t>)  ««=  b Ab Aend(v ,Vf) 1  2  i  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 = Ri A ... A Rj-i A labeli(vi, vj) f  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 disjunction of terms. 3. Remove terms and chains of code which sequentially follow the branch.  CHAPTER 4. A HORN CLAUSE  33  SEMANTICS  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 straightforward 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  P r o g r a m  Interpretation a n d  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, w h i c h represents an i n v o c a t i o n of the program: |= ->P(Vi,Vf) The  i n p u t parameters to P w o u l d be appropriately set i n the u,- i n p u t vector. T h e axioms  a n d goal clause for P has a logic p r o g r a m interpretation [Clocksin etal. 81], a n d has b o t h a procedural a n d declarative semantics [van E m d e n etal. 76].  T h u s , t h r o u g h the logic  p r o g r a m m i n g p a r a d i g m , the complete logical semantics of a p r o g r a m can be treated as a logic p r o g r a m , a n d can be executed using S L D N F resolution [Lloyd 84]. In order t o more closely ally our semantics w i t h the logic p r o g r a m m i n g concept, we henceforth use the P r o l o g n o t a t i o n from [Clocksin etal. 81] w i t h w h i c h to write the semantics. T h e t y p i c a l form of a H o r n clause is now: P^Ci  AC A...AC 2  d f c  =  P : -C C , U  ...,C .  2  k  A l s o , i n p u t - o u t p u t vectors w i l l now be w r i t t e n i n terms of P r o l o g lists:  v =< vi,...,v > = [vi,v ,...,v ] d  k  We  2  k  assume that any P r o l o g interpreter used t o execute the semantics has available t o i t  the a r i t h m e t i c a n d boolean expression evaluators V a n d W from the operational semantics. The stronger.  logic p r o g r a m i n t e r p r e t a t i o n of the semantics also makes the axioms logically T h e p r o b l e m w i t h the "bare" logical interpretation o f the axioms is that the  logical i m p l i c a t i o n s used i n the formulas are only p a r t i a l specifications of the behavior of mechanisms. F o r example, a mechanism M described by two clauses is logically equivalent to the following:  . |= (M <= C i ) A ( M  C) 2  = \= M  ( dV C) 2  T h i s states that M is satisfied i f C\ or C are satisfied, or b o t h . However, this is only a 2  p a r t i a l specification o f the behavior o f M, as when C\ a n d C are b o t h false, M is still 2  satisfied. W h a t we need is for the i m p l i c a t i o n i n each predicate t o b e read as a logical equivalence, o r iff.  CHAPTER 4. A HORN CLAUSE SEMANTICS  35  Fortunately, when the semantics are interpreted as a logic program, the predicates become logically complete specifications. The completion of a logic program is a logical characterization given the effects of SLDNF resolution on program interpretation [Lloyd 84]. If p(h,...,t ) <=  Li,...,L  n  m  is one of k clauses denning p, we first transform each clause into p(xi, ...,x„) where x\,...,x  n  3yi..3y ((xi  = ti) A ... A (x = t ) A L\ A .. A L )  d  n  n  m  are new variables, and yi,...,yd are the variables of the original clause. The  predicate for p is thus p(x ...,x ) u  E V...v£jt  n  x  where each Ei has the form 3y ..3y ((xi 1  d  = f ) A ... A (x = t ) A I A .. A L ) n  x  n  m  x  The completed definition of p is then Vx ...Vx (p(x , ...,x ) ^ ^ V ... V E ) 1  n  1  n  k  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  t o  B r u c e  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 c replaced by its equivalent definition. Finally, this reference to c\ is 2  CHAPTER  4.  A HORN  CLAUSE  37  SEMANTICS  A : |= (p(vi,v ) f  <= ci(vi,v )  A(c (vi,vj)  c (v ,Vf))  A  2  2  2  Ci(«,-,fJ/))  2  5 : |= (j>(0i,G/) <= i(ut»u ) A A(ci(vi,v ) ^=x:=y+l) A(c (vi,Vf) ><=ci (!>,•,!>/))  c (v ,v ))  c  2  2  2  f  f  2  C : |=(p(®i,^/)  c l : x := y + 1 A  A(c (vi,v ) 2  c (v ,v )) 2  2  f  <=ci(vi,vj))  f  D : |= (p(vi, v )  c l : X := y + 1 A ci(t> , v )) 2  f  E : |= (p(vi, Vf)  <= (cl : x := y + l;goto  f  cl)  Figure 4.3: Converting Branches prog([x],[])  : {  x := x  + 1;  x := x  +3  prog([Xl],[X2])  }  : -  asgn([Xl],X3,Xl asgn([X3),X4,X3  + 1,[X3]), + 2,[X4]),  asgn([X4],X2,X4  + 3, [X2]).  Figure 4.4: Consecutive assignments replaced with a branch, since the code for c\ has already been converted. 4.6  E x a m p l e  Translations  This section presents some example translations of Bruce programs into logic, and vice versa. A l l 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.  CHAPTER  4.  A HORN  CLAUSE  38  SEMANTICS  p([yi,Xl,JVl],[Y2,Xl,iVl]) : as5n([yi,Xl,7Vl],y3,l,[F3,Xl,iVl]), wW/cl([r3, X I , Nl], [Y2, X2, y := i ; while (n > 0) { n := n — 1; y := y * x  } }  N2]).  whilel([Yl,Xl,Nl],[Y2,X2,N2]) : Nl > 0, asgn{[Yl,Xl,Nl],N3,Nl - 1,[Y1,X1,N3]), asgn([Y 1, X I , JV3], y 3 , Y1 * X I , [F3, X I , iV3]), w/iz/el([y3, X I , JV3], [Y2, X 2 , iV2]). w/ii/el([yi,Xl,iVl],[yi,Xl,iVl]) - . i V l > 0.  : -  Figure 4.5: While loop  y:=  i;  w/ii7e (n > 0) { n := n — 1; y := y * x  OR  }  P{[y],[x,n]) : { y:=l; w/iz/el : i'/ (n > 0) { n := n — 1; y := y * x; goto whilel  }  }  } 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  39  SEMANTICS  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  40  SEMANTICS  prog([Xl,Yl),[X2,Y2}) :11([X1,Y1],[X2,Y2]). 10([X1,Y1],[X2,Y2))  :+ l,[X3,yi]),  asgn([Xl,Yl],X3,Yl  asgn([X3, Y1],Y3, X3 + 2, [X3, Y3]), P«f([., * [ ] ) : {  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 ' '~ V  }  «([X3,y3 X2,y2l). U  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, X I + 2, [XI, Y3]), /3([Xl,F3],[X2,y2]). 13([X1,Y1],[X2,Y2}) :asgn([Xl,Yl],Y3,Xl + 3,[Xl,YZ}), ,4([X1, Y3], [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 infigure4.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.  C H A P T E R 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 + testl([Y 1, NQ, X4, E o / l ] , [Y2, N2, X2, whilel([Yl,Nl,Xl,Eofl],[Yl,N2,Xl,Eofl]) -itrue, asgn([Yl,Nl,Xl,Eofl],N2,Nl  :l,[Yl,N6,X4,Eofl}), Eof2}). :-  - 1,[Y1,N2,X1,Eofl]).  testl([Yl,Nl,Xl,Eofl],[Y2,N2,X2,Eof2]) Eofl =:= true, end([Y 1, /VI, X I , 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  C H A P T E R 4. A HORN  CLAUSE  SEMANTICS  44  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]).  progl([x,y},[}) :{ x := x + 1; y.= y + 2; repeat { x := x + 3; / l : y := a; 4- 4 } until (x —:= y); goto ll }  11({X1,Y1],[X2,Y2}) :asgn([Xl, Y1], Y3, XI + 4, testl{[Xl,Y3],[X3,Y4}), ll([X3,Y4],[X2,Y2]). testl([Xl,Yl],[X2,Y2]) -XI =:=Y1,  [Xl,Y3]),  :-  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, [ X 3 , y 3 ] ) , -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, [ X 3 , y 3]), X 3 =:=  y3.  Figure 4.13: J u m p i n g into a repeat loop  CHAPTER 4. A HORN CLAUSE  SEMANTICS  progl([x,y},[]) : { x := x + 1; y.= y + 2; repeatl : repeat { x := x + 3; y := x + 4 } unii'Z (x =:= y); 4- 4;  ll: y := x  1/ ( n l =:= y) {  goto repeatl  }; }  goto 11  Figure 4.14: Bruce equivalent  45  Chapter 5 A  Bruce-Logic Translation  System  A B r u c e - L o g i c t r a n s l a t i o n system has been implemented i n C P r o l o g [Pereira et al. 84]. T h i s system comprises the front-end (logic generator) and b a c k - e n d ( B r u c e generator or Brucifier)  of a B r u c e transformation system discussed i n chapter 6. T h e complete source  l i s t i n g of the t r a n s l a t i o n system can be found i n the appendices.  5.1  T h e logic  generator  T h e logic generator reads a B r u c e program and generates its logical equivalent. It operates i n three stages:  1. A B r u c e p r o g r a m is read and parsed using a definite clause translation g r a m m a r ( D C T G ) [ A b r a m s o n 84].  T h e n , an i n i t i a l semantics is created directly from the  parse tree of the D C T G . T h i s semantics is complete and adequate i n the case when no b r a n c h i n g exists i n the p r o g r a m , pointedly i l l u s t r a t i n g the semantic clarity of structured, branchless p r o g r a m m i n g . 2. S h o u l d b r a n c h i n g be found i n the p r o g r a m , l a b e l program definitions are created for all the l a b e l l e d code i n the p r o g r a m .  46  CHAPTER  5.  A BRUCE-LOGIC  chain  ::=  TRANSLATION  SYSTEM  47  stat S AA  <:> code(Code,In,Out,Defns) chain <:>  ::= stat S, AA  :: — [';'],  S code(Code,In,Out,Defns). AAi  chain Q AA  code(Code,In,Out,Defns) ::— genjchain(Code, In, Out, Defns, genjzhain{Code,In,Out,Defns,S,Q) S code(Sl,In,X,Dl), Q code(S2,X, Out, D2), fuse((Sl,S2),Code), append(Dl, D2, De fns).  S,Q). : —  AA  AA  F i g u r e 5.1: C h a i n rules 3. A g a i n , i n the case of branches, the semantics are restructured to reflect the effect of branches on p r o g r a m c o n t r o l .  T h e rest of this section discusses these steps i n more detail. The  creation of semantics for basic B r u c e programs (section 4.2) is efficiently done  through the use of a D C T G . T h e D C T G specifies how B r u c e programs are to be parsed, and once parsed, how semantics are to be generated for the B r u c e constructs. E a c h D C T G rule has associated w i t h i t a syntactic  component and a semantic  component. T h e syntactic  component contains a B N F - s t y l e g r a m m a r rule for a p o r t i o n of the B r u c e s y n t a x .  The  semantic component specifies actions w h i c h are to take place at the node of the parse tree associated w i t h that g r a m m a r rule. In our i m p l e m e n t a t i o n , a semantic rule builds up a p o r t i o n of the logical a x i o m associated w i t h the context of the g r a m m a r rule i n question. T w o rules describing the c o m p o s i t i o n of chains are i n figure 5.1. Items w i t h i n braces are matched w i t h strings i n the i n p u t , while stat and chain  are references to g r a m m a r rules.  T h e first rule parses single statement chains, and the second parses m u l t i p l e statement ones. In the case of single statement chains, the code is directly retrieved at the g r a m m a r  CHAPTER  5. A BRUCE-LOGIC  while  ::= [while,  1  TRANSLATION  ('], booLexpr^B,  SYSTEM  48  [')','{'], chain^Q,  ['}']  <:> code(Code,In,Out,Defns) genjwhilecode(Code,In, addjcurrJabellist(while,  :: — Out, Defns,B, Loop Jabel).  Q,  LoopJabel),  F i g u r e 5.2: W h i l e - l o o p rule rule for t h a t statement. predicate genjchain  I n the m u l t i p l e - s t a t e m e n t case, the semantic rule calls a P r o l o g  w h i c h obtains the code for the statement at node S i n the parse tree  and adds i t to the code for the rest of the chain at node Q. O b t a i n i n g the code for c h a i n Q results i n a recursive i n v o c a t i o n of the same g r a m m a r rule  chain.  A t y p i c a l D C T G rule w h i c h parses a statement is the one for while 5.2. T h e s y n t a c t i c component uses the g r a m m a r rules booljexpr  a n d chain.  Code for the semantic rule code returns the axioms created for the while argument Defns  loops i n figure T h e argument l o o p , a n d the  returns axioms generated when parsing the loop body. T h e semantic rule  uses a predicate genjwhilecode,  w h i c h generates the predicative text of the a x i o m for the  l o o p . O t h e r B r u c e constructs are h a n d l e d similarly. Some b o o k k e e p i n g is done to ease r e c o m p i l a t i o n of the semantics i n t o B r u c e later. P r o g r a m parameters a n d variables are m a p p e d to i n p u t - o u t p u t vectors by their relative positions w i t h i n the vectors. Consequently, the parameter and variable names, as well as their relative ordering i n the p r o g r a m , are retained. I n a d d i t i o n , some features of the C P r o log interpreter itself are e x p l o i t e d . It is convenient for B r u c e to share the b u i l t i n a r i t h m e t i c a n d r e l a t i o n a l operators used b y C P r o l o g , as this eases the evaluation of expressions later. T h e existence of a b r a n c h i n a B r u c e p r o g r a m requires the generation of l a b e l predicates a n d the r e s t r u c t u r i n g of the axioms. B o t h these operations use the existing a x i o m set d u r i n g their processing, rather t h a n operate on the original B r u c e source p r o g r a m . L a b e l predicate generation involves creating a predicate for each labelled statement i n the p r o g r a m . T h e definition of a l a b e l predicate is the predicative meaning of the code generated b y the  CHAPTER  5.  A BRUCE-LOGIC  TRANSLATION  prog([x,y],[])  49  SYSTEM  : {  repeat { while (x < 0) { x := x + 1; 11: y := x 4- 2  }; x := y - f - 3 } u n i t / (x =:= y ) ;  V := y + 4; jfoio / l ; y := y + 5  Figure 5.3: B r a n c h i n g i n t o two loops  Buildenv  function from Bruce's o p e r a t i o n a l semantics. T o derive these predicates from the  existing a x i o m s , conjunctions of goals w h i c h compose the control context of the labelled statement are collected. C o l l e c t i n g these goals requires traversing the axioms from the statement up t h r o u g h its parent mechanisms u n t i l the top p r o g r a m a x i o m is reached. T h e predicate generated is refined somewhat by using the fact t h a t branches are semantically represented b y l a b e l p r o g r a m calls, w h i c h can be treated as p r o g r a m continuations.  The  predicate can thus be t e r m i n a t e d as soon as a b r a n c h is reached, since the continuation for the b r a n c h accounts for the rest of the c o m p u t a t i o n . F i g u r e 5.3 has a p r o g r a m w h i c h contains a b r a n c h i n t o the m i d d l e of two nested loops. T h e semantics i n i t i a l l y generated are i n figure 5.4. T h e p r o g r a m b r a n c h is represented by a goal goto(v{,ll,Vf), label(ll)  w h i c h is an "unprocessed" b r a n c h . T h e l a b e l ll is tagged b y a goal  i n the first clause of whilel,  w h i c h is removed after a l a b e l p r o g r a m predicate has  been created for i t . T h e l a b e l p r o g r a m as denned b y Buildenv  for ll is i n figure 5.5, a n d  the corresponding l a b e l p r o g r a m predicate is i n figure 5.6. T h e predicate is m u c h more terse t h a n the l a b e l p r o g r a m , since code i n the l a b e l program is logically described by existing predicates from the basic semantics. N o t e the a d d i t i o n of a predicate testl,  which  is used for describing the control w h i c h occurs when b r a n c h i n g in to the repeat l o o p .  CHAPTER  5.  A BRUCE-LOGIC  TRANSLATION  SYSTEM  prog([Xl,Yl],[X2,Y2]) : repeatl([Xl,Yl], [X3,73]), asgn([XZ, 7 3 ] , 7 4 , 7 3 + 4, [ X 3 , 7 4 ] ) , oio([X3,74],/l,[X2,75]), asgn{[X2, 7 5 ] , 7 2 , 7 5 + 5, [ X 2 , 7 2 ] ) . 5  repea*l([Xl,7l],[X2,72]) w/u.el([Xl,7l],[X3,73]), a s f f n ( [ X 3 , 7 3 ] , X 4 , 7 3 + 3, [ X 4 , 7 3 ] ) , ^ X 4 =:= 7 3 , repeail([X4,73],[X2,72]). repea*l([Xl,7l],[X2,72]) : w/w/el([Xl,7l],[X3,72]), asgn([X3, Y2], X 4 , Y2 + 3, [ X 2 , 7 2 ] ) , X2 =:= Y2. whilel([Xl,Yl],[X2,Y2]) : X I < 0, a s n ( [ X l , 7 1 ] , X 3 , X l - f 1,[X3,71]), label(ll), asgn([X3, YI], 7 3 , X 4 + 2, [ X 3 , 7 3 ] ) , w/u7el([X3,73],[X2,72]). 5  w/n7el([Xl,7l],[Xl,7l]) : ^ X l < 0.  F i g u r e 5.4: B a s i c semantics  50  5. A BRUCE-LOGIC  Buildenv(prog{...},ll  TRANSLATION  SYSTEM  : 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  F i g u r e 5.5: L a b e l program  «1([X1,71],[X2,72]) : o s c / n ( [ X l , y 1], Y 3 , X I + 2, [ X I , Y 3 ] ) , u>/n7el([Xl,Y3],[X3,Y4]), asgn([X3, 7 4 ] , X 4 , 7 4 + 3, [ X 4 , 7 4 ] ) , *esfl([X4,74],[X5,75]), asgn([X5,75], 7 6 , 7 5 + 4, [ X 5 , 7 6 ] ) , 50fo([X5,76],/l,[X2,72]). iesil([Xl,7l],[X2,72]) : ^ X l =:= 7 1 , repea*l([Xl,7l], [X2,72]). iesfl([Xl,7l],[Xl,71]) X I =:= 7 1 .  : -  F i g u r e 5.6: L a b e l program predicate  CHAPTER  5.  A BRUCE-LOGIC  TRANSLATION  SYSTEM  52  T h e b r a n c h restructuring a l g o r i t h m is a refined version of the d i s t r i b u t i o n procedure o u t l i n e d i n section 4.3. T h e process begins by searching for an instance of an unprocessed b r a n c h goal. W h e n such a goal is discovered, the goals following that goal are t h r o w n away, a n d the goal is replaced by a l a b e l p r o g r a m c a l l . T h e n the ancestor clauses of the predicate containing the b r a n c h are restructured.  However, instead of d i s t r i b u t i n g terms  of the whole p r o g r a m predicate, o n l y the clauses whose control is affected b y a branch are inspected. In a d d i t i o n , predicative formulas are retained where possible, i n order to m i n i m i z e t e x t u a l changes to the semantics. T h e net effect of the restructuring is t h a t every a x i o m whose control is affected b y the b r a n c h is altered as specified i n section 4.3. In terms of the p r o g r a m i n figure 5.3, the resulting branch restructuring i n figure 5.7 is not very interesting. T h e m a i n p r o g r a m predicate has its branch goal replaced b y a l a b e l p r o g r a m relation for ll, and the goal following it has been lost. T h e branch i n the l a b e l p r o g r a m predicate has also been replaced. W h a t is of more interest is the p r o g r a m b r a n c h i n figure 5.8, whose basic semantics are i n figure 5.9.  T h e restructured semantics i n figure 5.10 illustrates the effect of the  single b r a n c h on the control of the two loops. These predicates are a derivation of the d i s t r i b u t e d p r o g r a m predicate i n figure 5.11, i n w h i c h c o m m o n terms have been factored out and assigned to existing predicate names.  5.2  T h e  Brucifier  C o m p i l i n g a logical representation back i n t o B r u c e is the inverse of generating the logic from B r u c e . P a t t e r n m a t c h i n g is performed on the axioms of a semantic representation to search for matches w i t h logical definitions corresponding to B r u c e constructs. T h e schema m a t c h i n g used when converting predicates i n t o B r u c e is basically a backwards interpret a t i o n of the basic semantics of figure 4.1 i n chapter 4. A measure of n o n d e t e r m i n i s m is encoded i n t o the Brucifier i n order to account for the fact that there is often more t h a n one B r u c e i m p l e m e n t a t i o n derivable for a given set of axioms. T h i s nondeterminism means  CHAPTER  5.  A BRUCE-LOGIC  TRANSLATION  SYSTEM  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], X 4 , Y3 + 3, [X4, ^ X 4 =:= Y3, repeatl([X4, Y3], [X2, Y2]). repeatl([Xl,Yl],[X2,Y2}) whilel([Xl,Yl],[X3,Y2]), asgn([X3,Y4],X2,Y2  F3]),  :+  3,[X2,y2]),  X 6 = : = Y2.  whilel([Xl,Yl],[X2,Y2})  :-  X I < 0, a5 n([Xl,yi],X3,Xl + l,[X3,yi]), f f  asgn([X3,  Yl], Y3, X 4 + 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 ( [ X 3 , Y4], X4, Y4 + 3, [ X 4 , y 4 ] ) , fe5fl([X4,y4],[X5,y5]),  asgn([X5,  Y5], Y6, Y5 + 4, [X5, Y6]),  Zl([X5,y6],[X2,y2]). fesil([Xl,yi],[X2,y2]) : -nXl = : = y i , repeail([Xl,yi],[X2,y2]).  testl([Xl,Yl],[Xl,Yl]) X I =:= Yl.  :-  F i g u r e 5.7: F i n a l semantics  53  CHAPTER  5. A BRUCE-LOGIC  TRANSLATION  prog2([x,y],[]):  SYSTEM  {  while (x > 0) { while (x < 0) { x := x + 1; c/ofo 12  }; x := 7/4-2  }; I2:y:=  y + 3  Figure 5.8: B r a n c h out of two loops  pro 2([Xl,71],[X2,72]) : w/u/e2([Xl,71],[X2,73]), label(l2), asgn([X2,73], Y2,73 + 5, [X2,72]). 5  w/™/e2([Xl,7l],[X2,72])  : -  X I > 0, w/u7el([Xl,71],[X3,73]), a s n ( [ X 3 , 7 3 ] , X 4 , 7 3 4- 3, [ X 4 , 7 3 ] ) , w/iz7e2([X4,73],[X2,72]). 5  w/n/e2([Xl,7l],[Xl,71]) - . X I > 0.  : -  w/u7el([Xl,71],[X2,72]) : X I < 0, asgn([Xl, 7 1 ] , X 3 , X I + 1, [ X 3 , 7 1 ] ) , fifoto([X3,7l],Z2,[X4,73]), w/»/el([X4,73],[X2,72]). w/n7el([Xl,71],[Xl,71]) - . X I < 0.  : -  Figure 5.9: Basic semantics  54  CHAPTER  5.  A BRUCE-LOGIC  TRANSLATION  prog2([Xl,Yl],[X2,Y2])  SYSTEM  : -  io/n7e2([Xl,71],[X2,72]). while2([Xl,Yl],[X2,Y2\) XI  : -  > 0,  whilel([Xl,Yl],[X2,Y2]). while2([Xl,Yl],[Xl,Y2}) : - . X I > 0, asgn([Xl, Y1], Y2, YI + 5, [ X I , 7 2 ] ) . w/izZel([Xl,7l],[X2,72]) : X I < 0, asgn([Xl, Y1], X 3 , X I + 1, [ X 3 , 7 1 ] ) , /2([X3,71],[X2,72]). w/«7el([Xl,71],[X2,72]) : - . X I < 0, ast/n([Xl,7l],X3,71 + 3,[X3,7l]), w/u7e2([X3,71],[X2,72]). /2([X1,71],[X1,72]):asgn([Xl,  7 1 ] , 7 2 , 7 1 + 5, [ X I , 7 2 ] ) .  F i g u r e 5.10: F i n a l semantics  prog2  ((x > 0) A (x < 0); x := x + 1 A /2(t>,-,  v ))  V((x > 0) A -.(x < 0); x := y + 2; while(x V(-.(x > 0) A 12 : y := y + 3)  f  > 0); 12 : y := y + 3)  F i g u r e 5.11: D i s t r i b u t e d p r o g r a m predicate  55  CHAPTER  5.  A BRUCE-LOGIC  TRANSLATION  56  SYSTEM  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).  F i g u r e 5.12: W h i l e loop m a t c h i n g that repeated calls to the Brucifier for a given set of axioms may result i n different B r u c e programs. There are two m a i n m a t c h i n g modules used by the Brucifier. A m o d u l e called template-match  takes the axioms for a goal and matches t h e m w i t h the logical definitions of  B r u c e constructs. S u c h m a t c h i n g often requires the logical m a n i p u l a t i o n of predicates, for example, factoring out c o m m o n terms and unfolding predicate definitions. T h i s m o d u l e also assures that the B r u c e statements generated for a list of goals are sequenced properly. D e p e n d i n g on the nature of the transformations performed on the semantics, goals m a y have to be ordered w i t h respect to the d a t a flow of their i n p u t - o u t p u t vectors. A t y p i c a l m a t c h i n g rule is i n figure 5.12. T h e predicate isja-while  succeeds i f clauses A a n d  B represent a n instance of a while l o o p . Body are the goals i n the loop's body, and are matched t h r o u g h use of the other m a t c h i n g module (called templatejmatch-goals  i n our  i m p l e m e n t a t i o n ) . W h e n this succeeds, the B r u c e code defining this loop is constructed. T h e other module, templatejmatch.goals,  is used for m a t c h i n g goals i n chains. After  the goals are ordered, a B r u c e construct is derived for each goal. E l e m e n t a r y relations such as assignments are converted directly i n t o B r u c e at this stage. M o r e complex mechanisms (those w i t h external definitions) are converted to B r u c e by invoking template-match  on  the axioms defining the predicate to w h i c h the goal is referring. O n e p e c u l i a r i t y of our m a t c h i n g a l g o r i t h m is that branches always refer to code w h i c h has been previously converted.  I n other words, the first branch i n a program w i l l be  unfolded, and subsequent references to it w i l l refer to this unfolded p o r t i o n 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 } u n i i / (a; =:= y ) ;  y••=y + 4; t/ := a; + 2;  ^ofo whilel  } F i g u r e 5.13: D e r i v e d B r u c e p r o g r a m consequence of this is that branches a m o n g statements i n a single chain t e n d to be unfolded, a n d m i g h t just disappear as a result. F o r an example of this phenomena, see the p r o g r a m i n figure 4.9 of section 4.6 L a s t l y , the conversion of B r u c e expressions, such as those i n assignments a n d boolean tests, requires the use of i n f o r m a t i o n about the names of variables a n d parameters and their relative ordering i n the i n p u t - o u t p u t vectors. T h i s information was saved d u r i n g the p a r s i n g of the p r o g r a m . T h e B r u c i f i e d results for the logic programs i n figures 5.7 and 5.10 are i n figures 5.13 a n d 5.14 respectively.  CHAPTER  5. A BRUCE-LOGIC  TRANSLATION  prog2([x,y},[]):  SYSTEM  {  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 T h e Partial Evaluation of B r u c e Programs  6.1  P a r t i a l evaluation a n d p r o g r a m  transformation  Once a p r o g r a m is translated i n t o its logical representation, m a n y types of transformations are possible.  D e d u c t i v e transformations a n d t e r m r e w r i t i n g are two possibilities w h i c h  w o u l d likely incorporate a m i x t u r e of heuristics and user c o n t r o l i n order to be p r a c t i c a l . W e chose p a r t i a l evaluation as our p r o g r a m transformation scheme, as it is easily automated. T h e p a r t i a l evaluation of logic programs is also a logically sound transformation f o r m a l i s m , since the m e t a - i n t e r p r e t a t i o n of logic programs i n a p a r t i a l evaluation context is based o n S L D N F resolution, w h i c h is s o u n d . T h i s means that resulting transformed B r u c e programs are correct. M o s t i m p o r t a n t l y , p a r t i a l evaluation most clearly illustrates the u t i l i t y of our H o r n clause semantics and its u n d e r l y i n g execution m o d e l . P a r t i a l e v a l u a t i o n is a c o m p u t a t i o n a l m o d e l w h i c h distinguishes executable, code from non-executable, suspendable  permissible  code [Ershov 82] [Ershov 85]. I n i m p e r a t i v e pro-  grams, permissible code is t h a t w h i c h has a l l the necessary store values denned i n order to, for example, evaluate an expression or test. Suspendable code is that i n w h i c h a needed value is undefined. In a p r o g r a m transformation setting, i n p u t parameters to the program are usually fixed so t h a t the p a r t i a l evaluator specializes the p r o g r a m w i t h respect to that  59  CHAPTER  6.  THE PARTIAL  EVALUATION  OF BRUCE  PROGRAMS  60  set of i n p u t . P a r t i a l evaluation then entails executing a l l permissible code, d u r i n g w h i c h a l l suspendable code is retained as a p a r t i a l l y evaluated p r o g r a m . T h i s residual  program  is an o p t i m i z e d , transformed version of the original p r o g r a m . T h e following t e r m i n o l o g y a n d results are from [Lloyd etal. 87]. T h e p a r t i a l evaluat i o n of logic programs has been formally shown to be correct a n d complete, albeit under p a r t i c u l a r conditions. A semantic theory composed i n our H o r n clause semantics can be considered to be a definite  logic p r o g r a m , since the negation operator used i n negated  goals only operates on closed boolean expressions i n w h i c h resolution is never used; we could have used a weaker operator, but chose not to for convenience sake. L e t P' be a p a r t i a l l y evaluated p r o g r a m wrt a source p r o g r a m P and goal G.  P' is sound i f correct  answers for P' and G are also correct for P and G. T h e p a r t i a l evaluation of our semantics is therefore s o u n d , since the p a r t i a l evaluation of a l l definite logic programs is sound. T h e p a r t i a l evaluation of definite programs is not necessarily complete. P' is complete i f correct answers for P and G are correct for P' and G. However, P' m a y be specialized w r t goal G, w h i c h means that some reference i n P' to a specialized clause of P m a y n o longer be satisfiable. L l o y d ' s m e t h o d of ensuring completeness is to enforce a "closedness" c o n d i t i o n o n P'. T h i s c o n d i t i o n states that any predicate i n P' must r e m a i n general enough t o satisfy a l l goals w h i c h refer to i t , w h i c h essentially i n h i b i t s the p a r t i a l evaluation from becoming too specialized. W e m a i n t a i n completeness i n a different manner. G i v e n a p r o g r a m P , a general predicate h of P , a n d a goal G , we p a r t i a l l y evaluate P w r t G to o b t a i n a p r o g r a m P' c o n t a i n i n g a specialized predicate h'. Should references to h exist i n P ' w h i c h are too general for the specialized predicate h', we supplement P ' w i t h h:  P" = P ' U {h}  W i t h respect to the theory Th(P)  defined b y the axioms for P , P ' being sound means  that |= (Th(P')  \= h  Th(P)  \= h)  C H A P T E R 6. THE PARTIAL  EVALUATION  OF B R U C E  PROGRAMS  61  However, P " s incompleteness implies  \=-i(Th(P)\=h T h e supplemented theory  Th(P")  is t o t a l l y correct:  \=(Th(P)\=h 6.2  We  Th(P')[=h)  o-  Th(P")\=h)  I m p l e m e n t a t i o n  transform B r u c e programs b y p a r t i a l l y evaluating the H o r n clause semantics for t h e m .  Once a B r u c e p r o g r a m is translated i n t o logic, its representation is asserted i n t o the P r o l o g environment, a n d the p a r t i a l evaluator is applied to it w i t h respect to given parameter settings.  A residual p r o g r a m is eventually created.  S h o u l d this p r o g r a m be incomplete,  it is m a d e complete by a d d i n g to it required clauses from the o r i g i n a l general p r o g r a m . T h e n , using predicative p r o g r a m m i n g , the derived predicate is compiled back i n t o B r u c e , resulting i n a transformed, o p t i m i z e d B r u c e p r o g r a m . Our  p a r t i a l evaluator takes the f o r m of a meta-interpreter w r i t t e n i n C P r o l o g , and is  based o n implementations i n [Venken 85], [Takeuchi  etal.  85], and [Pereira  etal.  87]. T h e  core of the evaluator is i n figure 6.1. T h e first clause of mix p a r t i a l l y evaluates conjunctions of goals, the results of w h i c h are c o m b i n e d together. Clause (2) executes goals w h i c h have been determined to be b u i l t i n b y the  builtinjexecutable  utility. E x a m p l e s of such goals  are the boolean and relational operators used i n B r u c e tests. Clause (4) solves goals b y unifying a goal w i t h a clause, a n d p a r t i a l l y evaluating the resulting body. C P r o l o g ' s u t i l i t y a u t o m a t i c a l l y unifies the goal w i t h a clause each time  clause  clause  succeeds.  T h e most difficult p r o b l e m faced when p a r t i a l l y evaluating a program is determining when to i n h i b i t the p a r t i a l evaluation process.  mix  by the  inhibited  u t i l i t y (see figure 6.2).  G o a l i n h i b i t i o n is done i n clause (3) of O u r system provides b o t h automatic and  user-controlled goal i n h i b i t i o n . B u i l t i n goals and subprogram calls are i n h i b i t e d b y the first two clauses of  inhibited.  A n o t h e r a u t o m a t i c feature checks that the variables used i n  CHAPTER  6.  THE PARTIAL  EVALUATION  OF BRUCE  % ( l ) split multiple goals mix((Goal, Rest), Result,Recur)  PROGRAMS  : —  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  62  CHAPTER  6.  THE PARTIAL  EVALUATION  OF BRUCE  % ( 1 ) builtin goals inhibited(Goal,_) :— builtin(Goal),  %(2) subprogram inhibited(Goal,J) functor(Goal, storematch(N  calls : — Name, _), ame, _, _, _, _),  t. %(3) key variables are inhibited(Goal, _) : — not varJnst(Goal),  uninstantiated  j,  %(4) loop detected inhibited(Goal, Recur) : — member3(Goal, Recur), I.  %(5) no clause for goal inhibited(Goal, _) : — not i  clause(Goal,S),  Figure 6.2: Goal inhibition  PROGRAMS  63  CHAPTER  6.  THE PARTIAL  EVALUATION  OF BRUCE  64  PROGRAMS  a loop test are g r o u n d before that loop is unfolded (clause (3) of inhibited).  W h e n a Bruce  p r o g r a m is i n i t i a l l y parsed, a record is kept of the variables used b y the test expression of each if  statement and l o o p . T h e p a r t i a l evaluator uses this information to i n h i b i t goals  corresponding to these constructs should their test variables be uninstantiated. T h e fourth clause of inhibited  checks for loops. F i n a l l y , any goal w h i c h cannot be unified w i t h a clause  is i n h i b i t e d . I n a d d i t i o n to these five strategies, the user is allowed to enforce his or her o w n i n h i b i t i o n schemes s i m p l y b y asserting i n t o P r o l o g their o w n inhibited  clause. T h i s is v i t a l  when the p r o g r a m contains complex l o o p i n g mechanisms caused by the use of branches. It is also possible for the user to override any automatic i n h i b i t i o n strategy.  6.3  Example transformations  F i g u r e 6.3 has a B r u c e p r o g r a m power w h i c h computes integral powers using a b i n a r y power a l g o r i t h m (from [Ershov 82]). T h e two varinst  clauses, generated d u r i n g parsing, are used  to i n d i c a t e to the p a r t i a l evaluator when to i n h i b i t the clauses corresponding to the two loops i n the p r o g r a m . B o t h clauses specify that the t h i r d d a t a object (the value parameter n) must be instantiated before p a r t i a l l y evaluating the loops. W h e n power is p a r t i a l l y evaluated w i t h respect to n = 5, p a r t i a l execution yields the residual logic p r o g r a m a n d B r u c e p r o g r a m i n figure 6.4. Note that a side effect of p a r t i a l evaluation is that some vector values become g r o u n d . W h e n converting such a relation back i n t o B r u c e , the ground terms i m p l i c i t l y represent assignments of constants to variables. P a r t i a l l y evaluating power w i t h b o t h x — 2 a n d n = 5 produces a program w h i c h s i m p l y sets the output parameter to the result (figure 6.5). A n example of code simplification is the b i n a r y gcd p r o g r a m of figure 6.6 (from [ K n u t h 81]). W e assert goal i n h i b i t i o n clauses specifying that u must be ground before the l a b e l programs 61 a n d 62 are unfolded, and t must be ground before 64 is unfolded. E v a l u a t i n g the p r o g r a m w i t h u = 7 results i n a residual p r o g r a m w h i c h is somewhat simpler t h a n the o r i g i n a l , though not a great deal more efficient. T h e logical form of bingcd transformed equivalent can be found i n appendices C and D respectively.  a n d its  CHAPTER  6.  THE PARTIAL  EVALUATION  OF BRUCE  65  PROGRAMS  power([Yl,Xl,Nl],[Y2,Xl,Nl]) :asgn([Yl,Xl,Nl],Y3,l,[Y2,Xl,Nl]), while2([Y3, XI, Nl], [Y2, X2, N2]).  power([y],[x,n]) : { y:= 1; while (n > 0) { while (((n//2) * 2) = := n ) { n := n / / 2 ; x := x * x  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}) - i V l / / 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]).  }; n := n — 1; y := y * a:  }  }  while2([Yl,Xl,Nl],[Yl,Xl,Nl]) -.JV1 > 0. varinst(whilel, varinst(while2,  :-  [f, f, i]). [f, f,i]).  Figure 6.3: Binary powers power2([y],[x,n]): 1 * x;  power([Yl,Xl,5],[Y2,Xl,5]) : asgn([l,Xl,4],Y3,l * XI,[y3,Xl,4]), a5 n([y3,Xl,2],X2,Xl *X1,[F3,X2,2]), asgn([Y3,X2, l],X3,X2 * X2, [Y3,X3,1]), asgn([Y3, X 3 , 0 ] , Y2, Y4 * X 3 , [Y2, X3,0]). f f  x * x; y* x  Figure 6.4: Residual programs (n = 5)  power([yi,2,5],[32,2,5]).  power3([y],[x,n]) : { y := 32  } Figure 6.5: Residual programs (x = 2,n = 5)  {  CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS  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 ;  6in£fcd([srcd], : /oca/ { t := 0 - v; u := 7; k := 0; i e s M : if (((t//2) * 2) =:= t) { 63 : * := * / / 2 ;  goto testA  goto 61; 62: * / ( ( ( « / / 2 ) * 2 ) = \ = «) { t := 0 - v]  } e/se {  if (t > 0) {  goto 64 }; t := u ;  u := f  } e/se { v := 0 - *  63 : i := t//2; 6 4 : * 7 ( ( ( t / / 2 ) * 2) = : = * ) { 50/0 63  }; t := u — v; if (* = \ = 0 ) { goto 63  }; »7 (* > o) { u := t  }  }  e/se { •u := 0 - t  else { call power([p],[2, k]); gcd := u * p  }; t := u — v; i/(t = \ = 0 ) { <7o2o 63  }  }  }  }; ca// power([p], [2, A;]); gcd  u*p  } F i g u r e 6.6: B i n a r y gcd (u = 7)  66  CHAPTER  6.  THE PARTIAL  EVALUATION  OF BRUCE  p{[y,z],[x,cl,c2]) local [ r l , r 2 ] { if {x>z){  PROGRAMS  :  rl := c l + l ; r2 := c l - 1  } else { rl := c2 - 1; 7-2 := c2 + 1  }; y:=y + rl; z := z + r2  } F i g u r e 6.7: A suspended test  p([7l,Zl,Xl,3,5],[72,Z2,Xl,3,5]) : ^ X l > ZI, a s g n ( [ 7 l , Z l , X l , 3 , 5 , 4 , 6 ] , 7 2 , 7 l -f 4 , [ 7 2 , Z I , X I , 3 , 5 , 4 , 6 ] ) , asgn([Y2, ZI, XI, 3 , 5 , 4 , 6 ] , Z 2 , ZI + 6, [ 7 2 , 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, [ 7 2 , Z I , X I , 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  2([y,z],[x,cl,c2]) local [rl,r2] { if [x > z) { y:=y + 4; z := z + 2  P  PROGRAMS  68  :  } else { y:=y + 4; z := z + 6  } } Figure 6.9: P o l y v a r i a n t B r u c e result Logic elegantly handles polyvariant  computational  schemes, w h i c h are s i m p l y those  w h i c h e n t a i l p a r t i a l l y evaluating the bodies of tests a n d loops whose tests have been suspended.  In logic, this is n a t u r a l l y handled by unfolding the suspended test's denning  clauses, a n d retaining the suspended test expression as a goal. F i g u r e 6.7 shows a B r u c e p r o g r a m w i t h a suspended test (assume x is undefined).  F i g u r e 6.9 shows the p a r t i a l l y  evaluated logical result for c l = 3 and c2 = 5, and its B r u c e realization is i n figure 6.3.  Chapter 7 Discussion  C o m p a r i s o n s are given between the work i n this thesis a n d related work. T h i s is followed by a general discussion of the thesis, along w i t h future research possibilities.  7.1  R e l a t e d  w o r k  T h e H o r n clause semantics we use is semantically founded on those given i n [Hehner 84a] and [Hehner etal. 86], w h i c h i n t u r n is similar i n spirit w i t h logics used i n p r o g r a m verification [ B u r s t a l l 69] [Floyd 67] [Hoare 69]. Hehner's semantics describe the behavior of most of B r u c e - descriptions w h i c h we borrow, albeit i n a simplified and stylistically altered form. W e also extend the i m p e r a t i v e constructs h a n d l e d by i n c l u d i n g p r o g r a m branches and c a l l - b y - v a l u e s u b p r o g r a m arguments. Since Hehner uses his logical semantics to study general characteristics of programs a n d c o m p u t a t i o n , his semantics is m u c h more descriptive t h a n ours. H i s system has provisions for describing the e v a l u a b i l i t y of expressions, the t e r m i n a t i o n of mechanisms, a n d the type checking of data.  O u r semantics ignores such  features, as we are concerned w i t h the representation of correct and t e r m i n a t i n g programs w h i c h are to be transformed. He also employs full first-order predicate calculus i n his semantics, whereas we use a subset of predicate calculus - H o r n clauses. A stylistic difference between his s y s t e m a n d ours is that he uses fairly informal n a m i n g schemes when describi n g s y n t a c t i c entities of a p r o g r a m , where we e x p l i c i t l y represent syntactic constructs w i t h  69  CHAPTER  7. DISCUSSION  70  uniquely named predicates. Moss also uses H o r n clause logic to semantically describe i m p e r a t i v e programs [Moss 81] [Moss 82]. T h e description of a language i n his system takes the form of a sophisticated interpreter w h i c h fully describes the syntax and o p e r a t i o n a l semantics of the language. T h e s y n t a x is w r i t t e n u s i n g a metamorphosis grammar, w h i c h is closely a k i n to the D C T G we use. H i s semantic rules, like ours, take the form of pure P r o l o g predicates. However, the nature of his semantics differs substantially from ours. Moss's semantic methodology is very robust, as his p r i m e m o t i v a t i o n is to describe the complete s y n t a x and operational semantics of different p r o g r a m m i n g languages using pure H o r n clause logic, thereby p r o v i n g the u t i l i t y and generality of Prolog's descriptive capabilities. A theory i n his system is a set of axioms w h i c h fully describe the operational semantics of a language, and the d o m a i n of discourse of the theory is the universe of possible programs w r i t t e n i n the language. P r o g r a m s are translated i n t o various first-order terms w h i c h take the form of convenient d a t a structures.  These terms are i n t u r n m a n i p u l a t e d b y predicates describing various  functions of the operational semantics for the language.  T h e d o m a i n of discourse of his  logical axioms is thus programs and their abstract operational components. H e essentially creates pure P r o l o g interpreters for languages. O u r semantics uses a lower level of abstraction t h a n that of M o s s , since a theory i n our system describes the c o m p u t a t i o n a l behavior of a single i m p e r a t i v e program. W e use logical axioms to represent the functionality of the program's components, and reserve as our d o m a i n of discourse the domains of the store and expressions. T h e i m m e d i a t e advantage of such a low level description of c o m p u t a t i o n is the a b i l i t y of m a p p i n g , i n b o t h directions, between the source language and logical representation. In a d d i t i o n , the close relationship between the axioms a n d p r o g r a m means that optimizations of the axioms directly reflect improvements i n the corresponding i m p e r a t i v e p r o g r a m . C l a r k a n d van E m d e n have used H o r n clause logic for verifying flowcharts, w h i c h can be interpreted as l o w level representations of i m p e r a t i v e computations [Clark etal. 81]. T h e y describe a  flowchart's  c o n t r o l i n terms of H o r n clauses, and then use a technique  CHAPTER  7.  DISCUSSION  71  called consequence verification to prove various properties of the c o m p u t a t i o n . T h e style of their semantics is very similar to ours. T h e i r low level description of control relates to our semantics i n t h a t u n i q u e l y n a m e d predicates represent unique c o m p u t a t i o n a l mechar nisms. I n a d d i t i o n , they use logical variable renaming to describe updates to the store. However, their system is intended for use i n program verification, so they m a k e no attempt to associate their axioms w i t h p r o g r a m m i n g language constructs. O u r methodology for p a r t i a l l y evaluating i m p e r a t i v e programs offers interesting comparisons w i t h work done b y E r s h o v [Ershov 82] [Ershov 85]. E r s h o v p a r t i a l l y evaluates programs by s y m b o l i c a l l y executing t h e m using an algebraic r e w r i t i n g system.  These  r e w r i t i n g rules are a p p l i e d to the text of a p r o g r a m , and eventually y i e l d a p a r t i a l l y evaluated result. T h e m e t a - i n t e r p r e t a t i o n of our logical semantics very closely parallels the effects of his transformations. Analogies between the transformation system presented i n [Ershov 85] and S L D N F resolution of H o r n clause semantics are as follows:  1. Term reduction:  E r s h o v reduces expressions by replacing a t e r m by its d o m a i n value.  In our system, this occurs w h e n a n asgn, callasgn  or boolean test is resolved a n d the  expression value obtained is carried forward i n the computation by the i n p u t - o u t p u t vectors i n relations. 2. Variable reduction:  E r s h o v uses variable reduction to carry an assigned value of a  variable to other statements using that variable. In our system, Prolog's unification a u t o m a t i c a l l y "passes" the value of a variable among goals i n a clause, and resolvents of a goal. 3. Assignment  reduction:  E r s h o v removes any assignment whose variable value has been  distributed, throughout the code.  U n d e r S L D resolution, assignments (as w i t h a l l  goals) a u t o m a t i c a l l y "disappear" once they are resolved. 4. If and while loop reduction:  These reductions are used to simulate the c o n t r o l of tests  a n d loops. A g a i n , S L D resolution parallels these operations.  CHAPTER  7.  72  DISCUSSION  In fact, the traces of p r o g r a m transformations given b y E r s h o v are very analogous to goal traces o b t a i n e d w h e n executing our semantics i n P r o l o g . W e believe that our approach to the transformation of i m p e r a t i v e programs has advantages over E r s h o v ' s approach. T h e m a i n strength of our f o r m a l i s m is that transformations performed o n H o r n clause semantics have semantic interpretations i n logic. P e r f o r m i n g p r o g r a m transformations i n logic means that the transformations can be verified for correctness i n logic itself: any valid logical manipulation a correctness-preserving  program  transformation.  of the axioms is guaranteed  of being  W e exploit this fact i n this thesis by  p r o v i n g t h a t our p a r t i a l evaluation of H o r n clause semantics is logically sound, since the p a r t i a l e v a l u a t i o n of logic programs can be considered a pure logical transformation scheme [Lloyd etal. 87]. O n the other h a n d , E r s h o v ' s transformation system does not have any strong formal semantic i n t e r p r e t a t i o n . Consequently, p a r t i a l evaluation i n his system is not formally proved to be correctness preserving. O u r logical semantics offers a substantial improvement to previous techniques for polyvariant p a r t i a l evaluation, w h i c h entails p a r t i a l l y evaluating the bodies of tests a n d loops whose tests have been suspended [Ershov 85] [Bulyonkov 84]. Previous h a n d l i n g of this has been by e x p l i c i t l y m a i n t a i n i n g m e m o r y states of alternate computations, w h i c h is required by the u n d e r l y i n g algebraic transformation scheme.  In logic, this is handled b y s i m p l y  treating the test as a suspendable goal, w h i c h is retained d u r i n g the m e t a - i n t e r p r e t a t i o n process. Separate m e m o r y states are a u t o m a t i c a l l y retained d u r i n g the evaluation of different clauses, since memory states are e x p l i c i t l y stored as terms of the clauses.  7.2  Conclusions and further work  W e have i l l u s t r a t e d the a p p l i c a b i l i t y of H o r n clause logic as a tool for transforming i m p e r ative programs. W e described the semantics of a n o n t r i v i a l imperative language using a relatively economical set of logical axioms. U s i n g the predicative p r o g r a m m i n g p a r a d i g m , direct t r a n s l a t i o n between semantical representations and the source language is possible. T h i s semantics is also ideally suited to m a n y types of transformations, the one we presented  CHAPTER  7.  DISCUSSION  73  being p a r t i a l e v a l u a t i o n . O u r semantics are essentially a logical characterization of the operational semantics for B r u c e . O u r approach to the design of the semantics was to first define B r u c e i n terms of an abstract m a c h i n e , a n d then create logical axioms for different B r u c e constructs modelled o n the behavior of B r u c e ' s operational semantics. W h e t h e r this intermediate abstract defi n i t i o n of B r u c e was t r u l y required is debatable, as the H o r n clause definition of constructs is just as i n t u i t i v e as the abstract operational definitions, i f not more so. T h e semantics are also abstract enough t h a t machine-dependent features of the language are m i n i m i z e d , preventing it f r o m being as machine-oriented as other operational semantic systems. O u r h a n d l i n g of branches i n B r u c e uses b o t h logical semantics and algebraic semantics. T h e logical semantics comes i n t o play d u r i n g the i n i t i a l expansion of the p r o g r a m predicate, since we use the basic a x i o m a t i c definitions of p r o g r a m constructs d u r i n g the expansion process. D i s t r i b u t i n g terms of the p r o g r a m predicate, as well as r e m o v i n g the control context of the b r a n c h , are essentially algebraic operations w h i c h are based on logical considerations. O u r defense of this approach is that the  formula of a x i o m derivation  has become more c o m p l i c a t e d . W h e n no branches exist, the surface structure of program statements d i r e c t l y define the axioms. W i t h branches, we must use a more sophisticated inspection of the p r o g r a m s y n t a x i n order to derive the axioms. One possible extension of this work is to enhance the semantics to handle more complex i m p e r a t i v e languages. T h e inclusion of complex d a t a types w o u l d be a relatively s t r a i g h t forward extension, and w o u l d be especially useful given the preponderance of i m p e r a t i v e programs u s i n g arrays and other d a t a structures.  A real test w o u l d be to derive a H o r n  clause semantics i n the style of this work for an existing p r o g r a m m i n g language such as Pascal. W o r t h investigation is whether this style of logical semantics is applicable to other heterogeneous p r o g r a m m i n g paradigms, such as functional programs. Such research w o u l d be i n effect searching for a general description of c o m p u t a t i o n .  It is likely that a more  general semantics w o u l d have m u c h more complex domains t h a n that of ours, since other  CHAPTER  7.  DISCUSSION  74  p r o g r a m m i n g paradigms treat programs as d a t a m u c h more easily t h a n do i m p e r a t i v e languages.  D e n o t a t i o n a l semantics might therefore offer some insight i n t o the  content of the domains of such a representation.  semantic  In a d d i t i o n , algebraic semantics might  play a role i n denning a more generally applicable semantic formalism. M u c h of the t e x t u a l processing w h i c h we do to our semantics, such as factoring, code d i s t r i b u t i n g , and branch processing, are simple algebraic manipulations of the logical formulas. T h e m a n i p u l a t i o n of more complex semantic expressions might be more easily denned i n terms of algebraic rules. However, it is advantageous to m a i n t a i n a logical basis to the methodology, as predicate logic permits meaningful interpretations and analysis of the domains being described. T h i s thesis offers some p h i l o s o p h i c a l views on the disciplines of p r o g r a m m i n g and prog r a m m i n g language design.  A n immediate result of this work is t h a t i m p e r a t i v e pro-  grams are easily described or simulated b y logic programs.  O n e might conjecture from  this that logic p r o g r a m m i n g subsumes i m p e r a t i v e p r o g r a m m i n g i n terms of c o m p u t a t i o n a l power. L o g i c programs are certainly capable of c o m p u t i n g any T u r i n g - c o m p u t a b l e funct i o n [ T a r n l u n d 77]. However, a logic program interpreted as a logical theory is governed by the same principles of u n d e c i d a b i l i t y and effective c o m p u t a b i l i t y as its i m p e r a t i v e brethren [Boolos et al. 80]. W e should instead surmise that logic programs subsume i m p e r a t i v e ones i n terms of descriptive  power, since the logic program interpretation of our semantics uses a  relatively l i m i t e d subset of Prolog's full descriptive and c o m p u t a t i o n a l capabilities. P r o l o g programs as w r i t t e n b y P r o l o g programmers use m u c h more complex unification schemes t h a n those used i n our semantics. In a d d i t i o n , "real" P r o l o g programs are often w r i t t e n nondeterministically, w h i c h means that arguments to predicates might be either i n p u t or o u t p u t i n nature.  O u r H o r n clause semantics are strictly deterministic logic programs,  being declarative descriptions of deterministic computations. O u r semantics offers some insight into alternation trees and and/or models of programm i n g [Harel 80]. I n a logic p r o g r a m m i n g context context, an alternation tree description of c o m p u t a t i o n is just a restatement of the inherent logical semantics of pure P r o l o g program. Logic programs can be interpreted as and/or trees (or alternation trees), i n w h i c h clauses  CHAPTER  7.  DISCUSSION  of a predicate represent or-branches, a n d the goals of a clause represent  75  and-branches.  T h e tree itself is composed of alternate instances of and-nodes a n d o r - n o d e s (hence the t e r m alternation tree) i n w h i c h and-nodes are the parents o f o r - n o d e s , a n d vice versa. A successful c o m p u t a t i o n of the tree requires that a l l the and-nodes under a n o r - n o d e must be successful before the o r - n o d e is successful; similarly, at least one o r - n o d e under an crod-node must be successful before that a n d - n o d e succeeds. Besides h a v i n g theoretical i m p o r t a n c e i n the semantics o f p r o g r a m m i n g , the alternation tree interpretation of logic programs has applications i n parallel processing [Shapiro 87]. T h e parallel execution of an  and/or tree means that the or-nodes a n d arid-nodes of the tree a l l take the f o r m of  producers a n d consumers of d a t a . T h e d a t a p a t h between the nodes is dependent o n the p a r t i c u l a r variable usage i n the P r o l o g p r o g r a m . D a t a transfer between the nodes is done through the unification process. C a s t i n g an i m p e r a t i v e p r o g r a m i n t o our H o r n clause semantics means that a n  and/or  m o d e l of c o m p u t a t i o n is i m m e d i a t e l y defined for i t . A s w i t h a l l pure logic programs, the alternation tree description of the H o r n clause semantics of a B r u c e p r o g r a m allows the direct derivation of an  and/or m o d e l of c o m p u t a t i o n . In a d d i t i o n , this alternation tree gives  an i n i t i a l parallel execution m o d e l for the p r o g r a m . However, a d a t a flow analysis of the tree w o u l d p r o b a b l y be needed i n order to derive an efficient m o d e l of parallel c o m p u t a t i o n . P a r t i a l evaluation is a scheme w h i c h transforms a general p r o g r a m i n t o a more specialized one. However, efficiency is gained at the expense of generality. T h e ideal goal of p r o g r a m transformation is t o transform a program i n t o a more efficient form w i t h o u t a n y loss of generality. E x i s t i n g systems w h i c h do such transformations are unfortunately not very automatable.  Nevertheless, i t w o u l d be interesting to use o u r semantics i n a more  deductive transformational environment. It is likely that heuristics and user c o n t r o l w o u l d play a large role i n such a transformation system. A n o t h e r interesting a p p l i c a t i o n of our semantics is its use i n a transformation system w h i c h transforms a n i n p u t i m p e r a t i v e prog r a m i n t o a more " s t y l i z e d " version. A l s o w o r t h attention is the use of our semantics i n a p r o g r a m verification system, w h i c h w o u l d again rely o n heuristic a n d user control.  CHAPTER  7.  DISCUSSION  76  F u r t h e r w o r k i n controlling the p a r t i a l evaluation of i m p e r a t i v e programs is needed. Inh i b i t i n g recursion on p o l y v a r i a n t computations is difficult to implement i n our system. T h i s can be overcome somewhat b y p a r t i a l l y evaluating each clause i n the program predicate i n d i v i d u a l l y . However, i t is not obvious how constant values can be elegantly propagated to these clauses using this scheme. C o n t r o l l i n g the p a r t i a l evaluation process seems t o be a research topic problematic t o the field of p a r t i a l evaluation i n general [Lloyd etal. 87]. E r s h o v expresses the need for a systems p r o g r a m m i n g language ( S P L ) i n w h i c h p r o g r a m transformation could be based [Ershov 82]. W e believe that our technique offers a more solid semantic foundation for p r o g r a m transformation t h a n his algebraic transformations, and c l a i m that H o r n clause logic using P r o l o g ' s execution m o d e l is a p r i m e candidate for E r s h o v ' s S P L . F i r s t and foremost, pure P r o l o g has a well-founded u n d e r l y i n g m a t h e m a t i c a l m o d e l , n a m e l y first-order predicate logic. U s i n g logic i m m e d i a t e l y leads to the o p p o r t u n i t y of using the m a n y theoretical results, tools a n d techniques w h i c h have been established i n m a t h e m a t i c a l logic throughout the years. I n a d d i t i o n , using the predicative p r o g r a m m i n g p a r a d i g m , there is a strong and n a t u r a l relationship t o the semantics of a language and its syntactic r e a l i z a t i o n . F i n a l l y , P r o l o g has already proven its a p p l i c a b i l i t y i n m a n y systems p r o g r a m m i n g applications, for example, [ A b r a m s o n etal. 88], [Moss 81], and [Shapiro 83].  References  [ A b r a m s o n 84]  H . A b r a m s o n . Definite Clause T r a n s l a t i o n G r a m m a r s . In Proc. Logic Programming Symp., I E E E , A t l a n t i c C i t y , N e w Jersey, F e b r u ary 1984.  [ A b r a m s o n etal. 88]  H . A b r a m s o n , M . C r o c k e r , B . Ross, and D . Westcott.  A  Fifth  G e n e r a t i o n Translator W r i t i n g System: Towards an E x p e r t System for C o m p i l e r Development. In Fifth  Generation  Comp.  Sys.  Conf.,  I F I P S , T o k y o , J a p a n , 1988. s u b m i t t e d . [Allison 86]  L l o y d A l l i s o n . A practical introduction to denotational semantics. V o l u m e 23 of Cambridge Computer Science Texts, C a m b r i d g e U n i versity Press, 1986.  [Apt 81]  K . R . A p t . T e n years of Hoare's logic: a survey. TOPLAS, 1981.  [Ashcroft etal. 82]  E . A . Ashcroft and W . W . W a d g e . R for Semantics. ACM Transactions on Programming Languages and Systems, 4(2):283-294, A p r i l 1982.  [Backus 78]  J o h n B a c k u s . C a n P r o g r a m m i n g B e L i b e r a t e d from the v o n N e w m a n n Style? CACM, 21(8):613-641, A u g u s t 1978.  [Beckman etal. 76]  L . B e c k m a n , A . H a r a l d s o n , O . Oskarsson, and E . Sandewall. A part i a l evaluator and its use as a p r o g r a m m i n g t o o l . Artificial Intelligence, 7:319-357, 1976.  [Bibel 75]  W . B i b e l . Pradikatives programmieren. I n GI - 2. Fachtagung uber Automatentheorie und Formale Sprachen, pages 274-283, Springer, 1975.  [Bibel 85]  W . Bibel. P r e d i c a t i v e p r o g r a m m i n g revisited. In Mathematical method of specification and synthesis of software systems '85, pages 25-40, W e n d i s c h - R e i t z , E . G e r m a n y , A p r i l 1985.  77  3:431-483,  REFERENCES  [Boolos et al. 80]  78  George Boolos and R i c h a r d Jeffrey. Computability  and Logic.  Cam-  bridge U n i v e r s i t y Press, 1980. [Boyer et al. 79]  R . S . Boyer and J . S . M o o r e . A Computational graph Series, A c a d e m i c Press, 1979.  [Broy 84]  M a n f r e d B r o y . A l g e b r a i c M e t h o d s for P r o g r a m C o n s t r u c t i o n : T h e P r o j e c t C I P . In P . Pepper, editor, Program Transformation and Programming Environments, pages 199-222, Springer-Verlag, 1984.  [Bulyonkov 84]  M . A . B u l y o n k o v . P o l y v a r i a n t M i x e d C o m p u t a t i o n for A n a l y z e r P r o grams. Acta Informatica,  [Burstall 69]  R . M . Burstall.  ACM  Mono-  21:473-484, 1984.  F o r m a l D e s c r i p t i o n of P r o g r a m Structure and Se-  mantics i n F i r s t Order L o g i c . Intelligence  Logic.  In M i c h i e M e l t z e r , editor,  Machine  5, pages 79-98, E l s e v i e r , 1969.  [Clark etal. 81]  K . L . C l a r k and M . H . van E m d e n . Consequence Verification of Flowcharts. IEEE Transactions on Software Engineering, SE7 ( l ) : 5 2 - 6 0 , J a n u a r y 1981.  [Clint etal. 72]  M . C l i n t and C . A . R . Hoare. P r o g r a m m i n g P r o v i n g : J u m p s and F u n c t i o n s . Acta Informatica, 1:214-224, 1972.  [Clocksin etal. 81]  W . F . C l o c k s i n and C S . M e l l i s h . Programming V e r l a g , 1981.  [Cook 78]  S . A . C o o k . Soundness and completeness of an a x i o m system for p r o g r a m verification. SI AM Journal of Computing, 7(l):70-90,1978.  in Prolog.  Springer-  [Darlington etal. 73] J . D a r l i n g t o n and R . M . B u r s t a l l . A System w h i c h A u t o m a t i c a l l y Improves P r o g r a m s . I n IJCAI, pages 479-485, X X X , 1973. [de B r u i n 81]  A . de B r u i n . G o t o Statements: Semantics a n d D e d u c t i o n Systems. Acta Informatica,  15:385-424, 1981.  [Ershov 82]  A n d r e i P . E r s h o v . M i x e d C o m p u t a t i o n : P o t e n t i a l A p p l i c a t i o n s and P r o b l e m s for S t u d y . Theoretical Computer Science 18, 18:41-67, 1982.  [Ershov 85]  A n d r e i P . E r s h o v . O n M i x e d C o m p u t a t i o n : Informal A c c o u n t of the Strict and P o l y v a r i a n t C o m p u t a t i o n a l Schemes. In M . B r o y , editor, Control Flow and Data Flow: Concepts of Distributed Programming, pages 107-120, Springer-Verlag, 1985.  [Floyd 67]  R . W . F l o y d . A s s i g n i n g M e a n i n g s to P r o g r a m s . In Proc. Symp. Math., pages 19-32, A m e r . M a t h . S o c , 1967.  Appl.  79  REFERENCES  [ F u t a m u r a 71]  Y . F u t a m u r a . P a r t i a l evaluation of c o m p u t a t i o n process - an app r o a c h to a compiler-compiler. Systems - Comput. Controls, 2(5):45-50, 1971.  [Gordon 79]  M . Gordon.  The Denotational  Description  of Programming  Lan-  V o l u m e 99 of Lecture  Notes  guages. Springer-Verlag, N e w Y o r k , 1979. [Guessarian 81]  Irene Guessarian. Algebraic in Computer  [Harel 80]  Semantics.  Science, Springer-Verlag, 1981.  David Harel.  A n s / O r Programs:  P r o g r a m m i n g . ACM Transactions  A N e w A p p r o a c h to Structured on Programming  Languages  and  Systems, 2 ( l ) : l - 1 7 , J a n u a r y 1980. CACM,  [Hehner 84a]  E r i c C . R . Hehner. P r e d i c a t i v e P r o g r a m m i n g P a r t I. 27(2):134-143, F e b r u a r y 1984.  [Hehner 84b]  E r i c C . R . Hehner. Predicative P r o g r a m m i n g P a r t II. CACM,  27(2),  F e b r u a r y 1984. [Hehner et al. 86]  E r i c C . R . Hehner, Lorene E . G u p t a , a n d A n d r e w J . M a l t o n . P r e d i c a t i v e M e t h o d o l o g y . Acta Informatica, 23:487-505, 1986.  [Hoare 69]  C . A . R . Hoare. CACM,  A n A x i o m a t i c Basis for C o m p u t e r P r o g r a m m i n g .  12(10):576-583, October 1969.  [Hoare 85]  C . A . R . Hoare. P r o g r a m s are Predicates. In C . A . R . Hoare a n d J . C . Shepherdson, editors, Mathematical Logic and Programming Languages, pages 141-155, P r e n t i c e - H a l l , 1985.  [Hoare etal. 73]  C . A . R . Hoare a n d N . W i r t h . A n a x i o m a t i c definition of the prog r a m m i n g language P A S C A L . Acta Informatica, 2:335-355, 1973.  [Jones etal. 85]  N . D . Jones, P . Sestoft, a n d H . Sondergaard. A n E x p e r i m e n t i n Part i a l E v a l u a t i o n : the Generation of a C o m p i l e r Generator. SIGPLAN Notices, 20(8):82-87, A u g u s t 1985.  [ K e r n i g h a n etal. 78] B . W . K e r n i g h a n a n d D . M . R i t c h i e . The C Programming P r e n t i c e - H a l l , 1978.  Language.  [ K n u t h 81]  D o n a l d E . K n u t h . Seminumerical Algorithms. V o l u m e 2 of The Art of Computer Programming, Addison-Wesley, 2 n d e d i t i o n , 1981.  [Lloyd 84]  J.W. Lloyd. 1984.  [Lloyd et al. 87]  J . W . L l o y d a n d J . C . Shepherdson. Partial Evaluation in Logic Programming. T e c h n i c a l R e p o r t CS-87-09, U n i v e r s i t y of B r i s t o l , December 1987.  Foundations  of Logic Programming.  Springer-Verlag,  REFERENCES  [Loeckx etal. 84]  80  J . L o e c k x and K . Sieber. The Foundations  of Program  Verification.  W i l e y - T e u b n e r , 1984. [Loveman 77]  D . B . L o v e m a n . P r o g r a m Improvement b y Source-to-Source Transformation. JACM,  24(1):121-145, J a n u a r y 1977.  [ M a n n a etal. 77]  Zohar M a n n a and R i c h a r d W a l d i n g e r . Studies gramming Logic. Elsevier N o r t h - H o l l a n d , 1977.  [Moss 81]  Christopher D . S . Moss. Languages using Predicate  The Formal  in Automatic  Description  of  Pro-  Programming  Logic. P h D thesis, I m p e r i a l College, L o n -  d o n , U . K . , J u l y 1981. [Moss 82]  C h r i s t o p h e r D . S . M o s s . H o w to Define a Language U s i n g P r o l o g . In Conference  Record of the 1982 ACM  tional Programming,  Symposium  on Lisp and  Func-  pages 6 7 - 7 3 , A C M , 1982.  [O'DonneU 82]  M . J . O ' D o n n e U . A C r i t i q u e of the Foundations of Hoare S t y l e P r o g r a m m i n g Logics. CACM, 25(12):927-935, December 1982.  [Partsch et al. 83]  H . P a r t s c h a n d R . Steinbruggen. P r o g r a m T r a n s f o r m a t i o n Systems. Computing Surveys, 15(3):199-236, September 1983.  [Pepper 84]  P . Pepper, editor. Program  and Programming  Envi-  F . Pereira, D . W a r r e n , D . B o w e n , and L . Pereira. C-Prolog  User's  ronments. [Pereira etal. 84]  Manual,  Transformation  Springer-Verlag, 1984.  version 1.5 edition, November 1984.  [Pereira etal. 87]  Fernando C . N . P e r e i r a and S t u a r t M . Shieber. Prolog and NaturalLanguage Analysis. V o l u m e 10 of CSLI Lecture Notes, C S L I , 1987.  [Robinson 65]  J . A . R o b i n s o n . A M a c h i n e - O r i e n t e d L o g i c Based on the R e s o l u t i o n P r i n c i p l e . JACM, 12(1):23-41, J a n u a r y 1965.  [Shapiro 83]  E . Y . Shapiro. Systems Programming  in Concurrent  Prolog. Techni-  cal R e p o r t T R - 0 3 4 , I C O T , T o k y o , J a p a n , November 1983. [Shapiro 87]  E h u d S h a p i r o . Concurrent  [Stoy 77]  J . Stoy. Denotational  [Takeuchi etal. 85]  A . T a k e u c h i and K . F u r u k a w a . Partial Evaluation grams and its Application to Meta Programming. port T R - 1 2 6 , I C O T , T o k y o , J a p a n , J u l y 1985.  [ T a r n l u n d 77]  S. T a r n l u n d . H o r n Clause C o m p u t a b i l i t y . BIT,  Prolog vol. 1 and 2. M I T Press, 1987.  Semantics.  M I T Press, 1977. of Prolog ProT e c h n i c a l Re-  17:215-226, 1977.  REFERENCES  [Tennent 77]  81  R . D . Tennent. Language Design methods B a s e d o n Semantic P r i n ciples.  [Tennent 81]  Acta Informatica, 8:97-112, 1977.  R . D . Tennent. 1981.  Principles of Programming Languages. P r e n t i c e - H a l l ,  [van E m d e n etal. 76] M . H . v a n E m d e n a n d R . A . K o w a l s k i . T h e Semantics of Predicate Logic as a P r o g r a m m i n g Language. JACM, 23(4):733-742, O c t o b e r 1976. [Venken 85]  R a f V e n k e n . A P r o l o g Meta-Interpreter for P a r t i a l E v a l u a t i o n a n d its A p p l i c a t i o n to Source t o Source Transformation a n d Q u e r y O p t i m i s a t i o n . I n T . O ' S h e a , editor, Advances in Artificial Intelligence, pages 347-356, Elsevier Science Publishers B . V . ( N o r t h H o l l a n d ) , 1985.  [ W i r t h etal. 78]  N i k l a u s W i r t h a n d K a t h l e e n Jensen.  Pascal User Manual and Re-  port. Springer-Verlag, 2d edition, 1978.  Appendix A  Partial Evaluator Source % *** % *** Mixed % *** % *** % *** % *** % ***  % % % %  -  Computation Brian  J.  routines  Ross  Dept. of Computer Science University of British Columbia  mix(Goal,Mixed): Goal — top goal to mix (with parameter Mixed — Mixed Prolog result  settings)  % % mix/2 finds the Prolog result, given a top level goal. % A Prolog program must be asserted in the Prolog environment % 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  mix(Goal,Mixed) : — setof( Results,Goal" top_mixer(Goal,Results),P), add_old_prolog(P,Mixed),  % %  top_mixer(Goal,Result):  82  before this  complete.  APPENDIX  A.  PARTIAL  EVALUATOR  %  Goal  — top goal to  %  Result  — resulting  %  % topjnixer  mix  mixed  drive the mixed  SOURCE  Prolog  program  computation.  top_mixer(Goal,Result) :— clause(Goal,Body), mix(Body,Result2,[Goal]), set_mix_result (Result2 ,Result 3), set_mix_ans( G o a l , R e s u l t 3 , R e s u l t ) .  % %  set_mix_ans(A,B,C):  %  A  — Goal which has been mixed  %  B  — mixed  %  C  —the form  result of the result to be passed back to calling  program  % % set_mix_ans simply formats the result of the mixed % the form of a Prolog program.  computation  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 % environment. % further % %  The algorithm  interpretation  used simply  the current  tries to solve the Goals,  when Goal inhibition  conditions  are  Prolog  halting  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  mix((Goal,Rest),Result,Recur) :—  % split multiple goals  I •>  mix(Goal,GResult,Recur), mix(Rest,RResult,Recur), fuse((GResult,RResult),Result). mix(Goal,true,_) :— builtin_execut able( Goal),  % execute builtin's  I  Goal. mix(Goal,Goal,Recur) :— inhibited(Goal,Recur),  % halt interpretation  mix(Goal,Result,Recur) :— clause(Goal,Body), mix(Body,R lt2,[Goal|Recur]), set_mix_result (Result2,Result).  % interpret goal  esu  %  % 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,_,_,_,_), %  84  APPENDIX  A.  PARTIAL  EVALUATOR  inhibited(Goal,_) :—  SOURCE  not v a r j n s t ( G o a l ) , ! .  i n h i b i t e d ( G o a l , R e c u r ) :— member3(Goal,Recur),!. i n h i b i t e d ( G o a l ^ ) :—  % %  not clause(Goal,_),!.  unknown_vars(Goal):  %  Goal  :  — current  goal being  interpreted  % % unknownjvars  checks if the builtin  % as part of its executable structure  Goal has any uninstantiated (tests,  variables  expressions).  unknown_vars(asgn(_,_,E,_)) :— i •>  extract v a r s ( E , F ) , F \ = = []. unknown_vars(callasgn(_,_,E)) :— i extract v a r s ( E , F ) , F \ = = []. unknown_vars(Test) :— is_a_test(Test), i •i  extract v a r s ( T e s t , F ) , F \ = = " [].  %  % executable_builtin  tests if a goal is builtin  % This may be specialized  for individual  builtin_executable(Goal) :— builtin(Goal), not u n k n o w n v a r s ( G o a l ) , I.  % % builtin  goal list:  b u i l t i n ( t r u e ) : - !. b u i l t i n ( a s g n ( _ , _ ^ J ) : - !. builtin(callasgn(_,_,_)) : - !. b u i l t i n ( T e s t ) : - is_a_test(Test), !.  and  builtin  executable. utilities  in the  future.  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.  v a r J n s t ( G o a l ) :— 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  % addjoldjprolog/  2 completes  the mixed prolog  to make it 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  complete  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( M i x e d , R , D o n e , 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 Ans — final result  processed  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 b u i l t i n ( G o a l ) , 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 b u i l t i n ( G o a l ) ,  :—  APPENDIX  A.  not i  PARTIAL  EVALUATOR  SOURCE  88  head_exists(Goal,Mixed),  •>  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  %  Clause  — a general clause matching  goal 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( N a m e ,Template), functor(Template,Name,Arity), clause(Template,Body).  % % % %  head_exists(Goal,Clauses): Goal — partially ground Clauses — Prolog clauses  goal  % % head_exists tests if a clause with a partially % Head exists in Clauses. head_exists(Goal,[(H:-B)|Rest]) ground_eq( G o a l , H ) . head_exists(Goal,[_|Rest]) :— head_exists(Goal,Rest).  :-  ground head corresponding  to  Appendix B Bruce  Parser  % *** % *** Bruce parser  and predicate  generator  % *** % ***  _ Brian  % ***  Dept.  % ***  University  % ***  J.  Ross  of Computer of British  Science 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 Bruce program being parsed. This grammar expects a list of lexical tokens, as is generated by 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 % Extra arguments are described where appropriate.  env ::= prog""P, env"E <:> code(Code) ::—  89  the Westcott's  construct  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 ::= [ ' l o c a l ' ] , 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 ::= l a b e l * * 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).  ::-  S""code(Code,In,Out,Defns).  stat ::= while* "S  <:> code(Code,In,Out,Defns) stat ::= repeat" *S  <:> code(Code,In,Out,Defns)  ::— S" c o d e ( C o d e , I n , O u t , D e f n s ) . A  stat ::= b r a n c h " "S  <:> code(Code,In,Out,Defns)  ::— S" "code(Code,In,Out,Defns).  stat ::= skip**S  <:> code(Code,In,Out,Defns) stat ::=  ::—  S"*code(Code,In,Out,Defns).  assignment* A A  <:> 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 ::= l a b e r * V , [ ' : = ' ] , any_expr"*E <:> code(Code,In,Out,Defns) ::— gen_asgn(Code,In,Out,Defns,V,E). test ::= [ ' i f ' , ' ( ' ] ,  bool_expr" " B ,  chain*"Ql, ['}'], [else,'-C»], c h a i n * * Q 2 , [ ' } ' ]  <:> code(Code,In,Out,Defns) ::— gen_testcode(Code,In,0ut,Defns,B,Ql,Q2,If_label), add_curr_labellist(if,If_label). test ::= [ ' i f , ' ( ' ] , b o o l _ e x p r " " B , [ ' ) ' , ' { ' ] , c h a i n " " Q l , [ ' } ' ] <:> code(Code,In,Out,Defns) ::— g e n _ t e s t c o d e ( C o d e , I n , O u t , D e f n s , B ) Q l ) ' ' ,H_label), add_curr_labellist(if,If_label). proc_call ::= [call], l a b e l " * P , [ ' ( ' ] , vax_list""V, [ ' , ' ] , e x p r _ o u t p u t s * * E , [ ' ) ' ] <:>  code(Code,In,Out,Q) ::— gen_callcode(Code,In,Out,P,V,E). while ::= [ w h i l e , ' ( ' ] , b o o l _ e x p r * " B , [ ' ) ' , ' { ' ] , c h a i n * " Q , [ ' } ' ] <:> code(Code,In,Out,Defns) ::— gen_whilecode(Code,In,Out,Defns,B,Q,Loop_label), add_curr_labellist(while,Loop_label). repeat ::= [ r e p e a t , ' { ' ] , c h a i n " * Q , [ ' } ' , u n t i l , ' ( ' ] , b o o l _ e x p r " " B , <:> code(Code,In,Out,Defns) ::— gen_repeatcode(Code,In,Out,Defns,B,Q,Loop_label), add_curr_labellist(repeat,Loop_label). b r a n c h ::= [goto], l a b e l " " L <:>  [')']  APPENDIX  B. BRUCE PARSER  code(Code,In,Out,[]) ::— gen_goto(Code,In,Out,L), goto_found.  % % Some miscellaneous label  ::=  expression  rules  ...  [id(Name)]  <:> code(Name). any_expr ::= e x p r " " E <:> code(Expr,In) : : - E*"code(Expr,In). any_expr ::= b o o l _ e x p r " " B <:> c o d e ( E x p r , I n ) ::— B " " c o d e ( E x p r , I n ) . bool_expr ::= <:> code(true,_).  [true]  bool_expr ::= <:> code(false,_).  [false]  bool_expr ::= l a b e l " " V <:> code(Code,In) : : -  V""code(Name),var_match(Name,In,Code).  bool_expr ::= [ ' ( ' ] , a n y _ e x p r " " A , r e l o p " " B , any_expr*"C,  [')']  < > :  code((E),In) : : - A " " c o d e ( E l , I n ) , B " " c o d e ( E 2 ) , C " "code(E3,In), E =.. [ E 2 , E 1 , E 3 ] . b o o l . e x p r ::= [ ' ( ' ] , b o o l _ e x p r " " A , b i n b o o l _ o p " " B , b o o l _ e x p r " " C , <:> code((E),In) : : - A " " c o d e ( E l , I n ) , B " " c o d e ( E 2 ) , C " " c o d e ( E 3 , I n ) , E =.. [ E 2 , E 1 , E 3 ] . bool_expr ::= [ ' ( ' , ' " ' ] , b o o l _ e x p r " " A ,  [')']  APPENDIX  B. BRUCE  94  PARSER  <:> 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  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  expr_outputs ::= ['['], exprjist""V, [']'] <:> code(Code,In) : : - V""code(Code,In).  logical variable  substitutions...  operator  APPENDIX  B.  % Generates  BRUCE  a label  95  PARSER  list...  l a b e l j i s t ::= label* " L , [ ' , ' ] , l a b e l j i s t " " V <:> code([Label|Labels]) : : - L * * c o d e ( L a b e l ) , V " * c o d e ( L a b e l s ) . labeljist <:>  ::= label* * L  code([Label]) labeljist  ::— L * *code(Label).  ::= []  <:> code([]). % Generates exprjist  an expression  list  ...  ::= e x p r " " E , [ ' , ' ] , e x p r _ l i s t " " L  <:> code(Code,In) ::— E""code(Expr,In), L * *code(Elist,In), append( [Expr] ,Elist ,Code). exprjist  ::= b o o l _ e x p r " " B , [ ' , ' ] ,  exprjist""L  <:> code(Code,In) ::— B " *code(Expr,In), L""code(Elist,In), append( [Expr] , E l i s t , C o d e ) . exprjist  ::=  expr""E  <:> code([Code],In) : : - E " *code(Code,In). exprjist  ::=  bool_expr""B  <:> code([Code],In) ::— exprjist  ::= []  <:> code( [],_).  B""code(Code,In).  APPENDIX  B.  BRUCE  PARSER  % % Some  semantic  primitives  % asgn(In,Var,Expr,Out) % in logical variable  is satisfied by evaluating Var, where In contains  % needed by Expr, and Out is the final output % variable  Var  Expr  and saving the value  input values which may be value (variant  with  logical  changed).  a s g n ( I n , V a r , E x p r , O u t ) :— 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.  c a l l a s g n ( I n , V a r , E x p r ) :— value(Expr,Var). % skip always  succeeds.  skip(_,_). skip_branch(_,Dest,_) : - w r i t e l ( n l , ' I g n o r i n g b r a n c h t o % label inserts  do  ',Dest,nl).  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  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), Q l " *code(Chainl,In,02,D2), gen_label(test,Label), Code =.. [Label,In,Out], Testhead =.. [Label,In,02], Testhead2 =.. [Label,In,In],  97  APPENDIX B. BRUCE PARSER  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),  98  APPENDIX  B. BRUCE PARSER  99  0 / *code(Chainl,In,02,D2), gen_label(repeat, L a b e l ) , C o d e = . . [Label,In,Out], L o o p h e a d l =.. [ L a b e l , I n , 0 3 ] , L o o p h e a d 2 =.. [ L a b e l , I n , 0 2 ] , L o o p c a l l =.. [ L a b e l , 0 2 , 0 3 ] , c o p y ( ( L o o p h e a d l :— ( C h a i n l , ~ ( B o o l t e s t ) , L o o p c a l l ) ) , L o o p l ) , copy((Loophead2 :— ( C h a i n l , B o o l t e s t ) ) , L o o p 2 ) , 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( V l i s t ,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( C a l l j n v a r s ,Call_invals,In_args), gen_vec(In_args,Out_args), set_outputs(In, C a l l j n v a r s , 0 u t _ a r g s , 0 u t ) , C a l l =.. [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( V n a m e ,In ,Var_i), vec_variant (In, V a r j ,Var_f , 0 u t ) .  % 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, F l a g s ) .  y *** 0  % *** Syntax % ***  definitions  white_space_char(32). white_space_char( 10). white_space_char(9). white_space_char (12).  for  lexical  % space % carriage return % tab % form feed  ?-op(900,fx,'-'). ?-op(1100,yfx,'#'). ?-op(1000,yfx,'&').  op_chars("+" , m a t h ( ' + ' ) ) . op_chars("-",matli('-')). op_chars("*" ,math( ' * ' ) ) . op_chars("/",math('/')). op_chars("//",math( ' / / ' ) ) • op_chars("":",bool('&')). op_chars("#",bool(' #')). op_chars(" ' " ,bool( ' " * ) ) . op_chars("< ,rel('<')). M  Westcott's  analyzer  APPENDIX  B. BRUCE  PARSER  op.charst'^Vel^')). op_chars( "=< " ,rel( '=<'))• op_chars(">=",rel( ' > = ' ) ) . op_chars( "=:=" ,rel( ' = : = ' ) ) . op_chars(''=\= ,rel(> = \ = ' ) ) . M  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  " T : - not T . A # B :-  (A;B).  A k B :- A,B. v a l u e ( E x p r , V a l ) :—  routines...  APPENDIX  B. BRUCE  103  PARSER  V a l is E x p r .  % *** % *** 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 % Type (test,while,repeat,label).  a new unique number for the  get_gen_num(test,Num) :— gen_nums ( N u m , X , Y , Z ) , N e x t is N u m + 1, abolish(gen_nums,4), tassert(gen_nums(Next,X,Y,Z)). get_gen_num(while,Num) :— gen_nums(X,Num,Y,Z), N e x t is N u m + 1, abolish(gen_nums,4), tassert(gen_nums(X,Next,Y,Z)). get_gen_num(repeat,Num) :— gen_nums(X,Y,Num,Z), N e x t is N u m + 1, abolish(gen_nums,4), tassert(gen_nums(X,Y,Next,Z)). get_gen_num(labei,Num) :— gen_nums(X,Y,Z,Num), N e x t is N u m + 1, abolish(gen_nums,4), tassert(gen_nums(X,Y,Z,Next)).  %  structure  APPENDIX  B.  BRUCE  PARSER  % gen_label(Labeltype,Label)  104  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, % Prog is the current program being processed.  and asserts that  n e w J a b e l l i s t ( P r o g ) :— (retract(labellist(Prog ,_));true), tassert(labellist(Prog,[],[])), tabolish(curr_prog,l), w  tassert(curr_prog(Prog)), ; #  % % add_curr_labellist(Type,Label) adds Label to the label list for % program being processed, determined by currjprog. add_curr_labellist(label,Label) curr_prog(Prog),  the  current  :-  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, % % add_approp_labellist % contains Label.  Newlabel):  adds Newlabel  to the general label list which also  APPENDIX  B. BRUCE PARSER  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)) : f u n c t o r ( H ,Name,_), labellist(_,_,Labels), member2( N a m e , L a b els).  105  Appendix C Branch Handling  % *** % *** Prolog  % *** % *** % *** % ***  % ***  branch transformation  _ Brian  J.  utilities  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 predicates, processjbranchesj3 is called to iterate through all clauses. For each one with a goto, the goto goal is changed the appropriate label program. Then the parent predicates of 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  within descendent the Prolog into a call to the clause  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  branch_restruct(Prolog,Clause,Head,Newprolog)  now.  :-  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 % The branchjrestruct % up the tree.  is called on the parent,  causing  a recursive  restruct_parent(Prolog,Head,Ivec,Code,Newprolog) :— parent_clause(Prolog,Head,Parent,Phead,Left,Goal,Right), not l a b e l p g m ( P a r e n t ) , set_code(Phead,Left,Goal,Right,Ivec,Code), branch_restruct(Prolog,Parent,Phead,Newprolog),  % % restruct_sibling % if one exists.  adds Code to the end of the sibling  of  Clause,  in  Code. restructuring  APPENDIX  C. BRANCH  HANDLING  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 ( R i g h t , ( 0 2 , 0 2 ) ,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) :— H e a d =.. [ N a m e , I l , O l ] , get_prev_IO(Right,(Il,Il),I2,02), N e w h e a d =.. [ N a m e , I l , 0 2 ] ,  108  APPENDIX  C.  BRANCH  HANDLING  list_to_body ( R i g h t , B o d y ) , copy((Newhead : - Body),Code), !. restruct_clause2(Head,Left,[],Code) :— H e a d =.. [ N a m e , I l , 0 1 ] , get_prev_IO (Left,(II ,11) ,12,02), N e w h e a d =.. [ N a m e , I l , 0 2 ] , list_to_body(Left,Body), c o p y ( ( N e w h e a d :— B o d y ) , C o d e ) , I.  restruct_clause2(Head,Left,Right,Code)  :—  copy((Head,Left,Right),(Head2,Left2,Right2)), Head2 =.. [ N a m e , I l , 0 1 ] , get_prev_IO(Left2,(Il,Il),I2,02), get_prev_IO(Right2,(02,02),I3,03), 0 2 = 13, N e w h e a d =.. [ N a m e , I l , 0 3 ] , append(Left2,Right2,B), list_to_body(B,Body), c o p y ( ( N e w h e a d :— B o d y ) , C o d e ) , 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) :— H e a d =.. [ N a m e , I l , O l ] , 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), c o p y ( ( N e w h e a d :— B o d y ) , N e w c l a u s e ) , i  APPENDIX  C.  % createjabelcall  BRANCH  HANDLING  changes a goal in goto format  to a label call.  create_labelcall(goto(In,Label,Out),Call) :— C a l l =.. [ L a b e l , I n , O u t ] , I.  %  :  % chop_branch_chains(Prolog, % label program  Clauses, Collect)  takes each clause  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), N e w p r o l o g = [Newclause |New2]), i  % *** % *** Label program % ***  generation  with  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), g e n j a b elprogs (Prolog3 ,P r olog3 ,Ne wprolog), !_  g e n J a b e l p r o g s ( P r o l o g , [ j R ] , N e w p r o l o g ) :— 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), t  t  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) :— f u n c t o r ( G ,Lab,_), labellist(_^,Labels), member2(Lab,Labels),  descendent_branches(Prolog,Goal) :—  APPENDIX  C. BRANCH  HANDLING  find_clause(Prolog,Goal,Clause), r e m o v e j 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 :— B o d y ) ) :— 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,_), g e t j a b el_r efs ( P rolog , N ame, [], [ A ,B ]), test_if_repeat(A,B,OutT,Test,Body),  114  APPENDIX  C. BRANCH  115  HANDLING  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 % The output  creates the control  %  Control  %  Defns = [(Testl  % all suitably  environment  for a repeat  construct.  is =  [Body,Test] :-  ~Test,Head),(Testl  :-  Test)]  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, V o u t ) , H e a d A = . . [Testlabel,Vec2,Vout], H e a d B = . . [Testlabel,Vec2,Vec2], C a l l = . . [Name,Vec2,Vout], list_to_body(["(Test2),Call],BodyA), copy ((~HeadA: - B o d y A ) ,D 1), copy((HeadB: -Test2) ,D2), add_approp_labellist(Label,Testlabel), merge_goals(I3,03,Rightgoals,Vec2,Vout,[HeadA] , I n , O u t , C o n t r o l ) .  % % 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  fin d_goal( Clause, H e a d ,Left , L ab el , R i g h t ) , 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 , L a b el, S), i  116  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. b r u c i f y ( E n v , B r u c e ) :— 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( [] , B r u c e , B r u c e ) . brucify_programs([Progname,Prog|Rest],Collect,Bruce) :— get_label_refs(Prog,Progname,[],Clauses), get_IO (Clauses,In,_),  117  APPENDIX  D.  BRUCE  118  GENERATION  template_match(Progname,In,Prog,Clauses,B»[]j_)» r e r n u n u s e d j a b 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, % Matches  Clauses  % NOTE:  Should  %  Clauses,Bruce,Labels,Newlabels):  to known bruce construct the dataflow  definitions.  of goals be altered, include  the two lines noted  below.  template_match(_,_,_,[],_,_,_) :— !,fail. template_matcli(Prognarrie ,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,_), u  template_match_goals(Progname,In,Prolog,Ordered,Bruce,Labels,Newlabels). % repeat: template_match(Progname,Vec,Prolog,[A,B]»B »Labels,Newlabels) is_a_repeat(Progname,A,B)Test,Body), get_IO(A Out), ruce  :—  w  template_match^oals(Progname,Out,Prolog,Body,Bruce_body,Labels,Newlabels), append_list([[repeat,' { ' ] , B n i c e _ b o d y , [ ' } > , u n t i l , ' ( ' , T e s t , ' ) ']],Bruce). %  while:  t e m p l a t e _ m a t c h ( P r o g n a m e , V e c , P r o l o g , [ A , B ] » B r u c e , L a b e l s , N e w l a b e l s ) :— is_a_while(Progname,A,B,Test,Body), getJO(A Out), template_match^oals(Progname,Out,Prolog,Body,Bruce_body,Labels,Newlabels), append_list([['while ( ' , T e s t , ' ) ' , ' { ' ] , B r u c e _ b o d y , [ » } ' ] ] , B r u c e ) . M  % 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(A Out), M  template_match^oals(Progname,Out,Prolog,Thengoals,Thencode,Labels,Newlabels2), (Elsegoals = =  Q ->  append_list([['if Newlabels =  ('/Test,')»,'{'],Thencode,['}']],Bruce),  Newlabels2  template_match^oaIs(Progname,Out,Prolog,Elsegoals,Elsecode,Newlabels2,Newlabels), append_list([[' i f (' , T e s t , ' ) ' , ' { ' ] , T h e n c o d e , [ ' } ' ,else,' { ' ], Elsecode,['}']],Bruce)). template_match(Progname,Vec,Prolog,Clauses,Bruce,Labels,Newlabels) :— factor (Clauses ,Prolog,NewClauses , N e w P r o l o g ) , 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,' : = ' , E x p r 2 ] , B , B r u c e ) .  :—  A P P E N D I X D. B R U C E  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) :— G o a l = . . [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), C a l l = . . [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([' c a l l ' , C a l l 2 ] , B , B r u c e ) .  % case (e) template_match^oals(Progname,Vec,Prolog,[Goal|Rest],[goto,Name],Labels,Labels) :— functor(Goal,Name,_), member 2 ( N a m e ,L ab els).  % gen_impl_asgns(Prognarne Vec,Goal,Asgns), % chain_append(Asgns,[goto,Name],Bruce). l  % remove?? % 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  121  GENERATION  gen_impl_asgns(Progname,Vec,In,Asgns), template_match_goals(P rogname , 0 ut ,Prolog,Rest , B r u c e B ,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 % creates Bruce code if they match.  test construct,  and  i s _ a n _ i f ( P r o g n a m e , A , B ) B e t e s t , T h e n , E l s e ) :— test_if_if(A,B,I,Test,Then,Else), convert_bruce_expr(Progname,I,Test,Brucetest). ruc  % % is_a_while(Progname,A,B,Brucetest,Body): % Tests A and B for a match with a Bruce % creates Bruce code if they match.  while construct,  and  i s _ a _ w h i l e ( P r o g n a m e , A , B ) B u c e t e s t , B o d y ) :— test_if_while(A,B,I,Test,Body), convert_bruce_expr(Progname,I,Test,Brucetest). r  %  ;  % is_a_repeat(Progname,A,B,Brucetest,Body): % Tests A and B for a match with a Bruce repeat % creates Bruce code if they match.  construct,  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 % tests TA and TB in BodyA and BodyB % will return new complementary tests, if c o m p l e m e n t a r y _ t e s t s ( B o d y A , B o d y B , T A , T B ) :— member2(TA,BodyA), is_a_test(TA), member2(TB,BodyB),  an instance of (ie. TA = ~TB). any.  complementary Repeated calls  APPENDIX  D.  BRUCE  122  GENERATION  is_a_test(TB), complementary ( T A , T B ) .  % % convert_bruce_expr(Progname In,Expr,Conv)  created a copy of Expr  l  %  the appropriate  %  The  %  variables  Bruce  variable  names,  based on ordering  in  result is in Conv, as we don't want to bind the actual (lose dataflow  having In. logical  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...  b r u c e _ h e a d e r ( P r o g n a m e , [ A , ' : ' ,local,Locals]) :— storematch(Progname,Vars,Ref,Val,Locals), A = . . [Progname,Ref,Val].  % % recursive_call(Call, Goals, C) is satisfied % Call exists in the Goals list.  if a recursive  call C to header  recursive_call(Call,Goals,C) :— copy(Call,C), member2( C , G o a l s ) , same_out_vars(Call,C).  %  ;  % collect_callasgns(Goals,Vars,Calls) % which assign values to variables collect_callasgns([] _,[]) %  finds  instances  listed in Vars.  of callasgn  goals in  The results are in  :— !.  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, V a r s, D ) ,  Goals  Calls.  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,Callasgns ,W), u  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). r e m _ u n u s e d _ l a b e l s ( 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  find_goto(Label,[goto,Label|J) find_goto(Label,[S|R])  a branch to label Label in the Bruce  code.  : - !.  :-  nnd_goto(Label,R), I.  % % test_if_if checks if A and B match % The matching  criteria  %  (a) complementary  %  (b) Both  with an if construct  of  Bruce.  are: tests in A and B  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 , H e a d B , B o d y 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), H e a d = . . [_,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 , H e a d B , B o d y B ) , complementary_tests(BodyA,BodyB,TA,TB), dep_in_vars(TA,HeadA), dep_in_vars(TB , H e a d B ) , (BodyA = = [TA],  APPENDIX  D.  BRUCE  (Test,Head,Goals) = BodyB ==  125  GENERATION  (TB,HeadB,BodyB)  [TB],  (Test,Head,Goals) =  (TA,HeadA,BodyA)),  recursive_call(Head,Goals,Call), remove i t e m s 2 ( [ T e s t , C a l l ] , G o a l s , B o d y ) , L.IJ.  Head =..  % % test_if_while checks if A and B match with a repeat construct % The matching criteria are: tests in A and  of  Bruce.  %  (a) complementary  B.  % %  (b) One clause contains a recursive call matching the head. (c) The test in that clause is dependent on the headers input  % %  (d)  The  test in the other clause uses variables variables list.  % %  (e)  The  remaining the same  goals which should (permutation).  test_if_repeat(A,B,0,Test,Body)  variables.  in the headers  output  compose the repeat body are  :—  split_clause( A ,Head A ,B ody A ) , split_clause(B , H e a d B , B o d y B ) , complementary_tests(BodyA,BodyB , T A , T B ) , (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 , C a l l ) , dep_out_vars(Test,H2), remove_item(Test,B2,Body), remove_items2([Tl,Call],Bl,New2), permutation(Body,New2), . H 2 = . . [_,_,0].  % % set_then_else(TA,HeadA,NewA, % Test, Then, Else, and Head  TB,HeadB,NewB, appropriately.  Test, Then,Else,Head)  set_then_else(TA,HeadA,[],TB,HeadB , N e w B , T B , N e w B , [ ] , H e a d B ) NewB \ = = i  [],  :-  sets  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,Vars .,_^), set_asgns (P rogname ,In, Var s ,In, Asgns). v  APPENDIX  D. BRUCE  GENERATION  %  % 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( P r o g n a m e , Vec, S, S 2), chain_append([Var,' : = ' , S 2 ] , 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), m e m b e r 2 ( B , Clauses), A \== B, factor_goals(A,B,NewClause,NewDefns), remove_items( [ A , B ] , P r o l o g , X 1), append([NewClause|NewDefns],Xl,NewProlog), I.  127  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 o d y B , 0 r d B ) , (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. s p a w n _ c l a u s e ( l e f t , H e a d A , C o m m o n A , R e s t A , H e a d B , C o m m o n B , R e s t B , N e w l , [ N e w 2 , N e w 3 ] ) :— spawn_left_main(Head A , C o m m o n A ,Rest A , N e w l a b e l , N e w l ) , spawnJeft_aux(Newlabel,HeadA,CommonA,RestA,HeadB,CommonB,RestB,New2,New3),  s p a w n _ c l a u s e ( r i g h t , H e a d A , C o m m o n A , R e s t A , H e a d B , C o m m o n B , R e s t B , N e w l , [ N e w 2 , N e w 3 ] ) :— spawn_right_main(HeadA , C o m m o n A ,Rest A , N e w l a b e l , N e w l ) , spawn_right_aux(Newlabel,HeadA,CommonA,RestA,HeadB,CommonB,RestB,New2,New3),  APPENDIX  D.  BRUCE  129  GENERATION  spawn_left_main(Head,Conimon,Rest,Newlabel,(Head3 : - B o d y ) ) : copy((Head,Common,Rest),(Head2,Common2,Rest2)), get_prev_IO(Common2,Head2,I2,02), gen_label(label,Newlabel), gen_vec(I2,New0ut), H e a d A =.. [ N a m e J n J , C a l l =.. [Newlabel,02,New0ut], Head3 =.. [Name,In,NewOut], list_to_body(CommonA,Xl), fuse((Xl,Call),Body),  s p a w n _ l e f t _ a u x ( N e w l a b e l , H e a d A , C o m m o n A , R e s t A , H e a d B , C o m m o n B , R e s t B , ( H e a d 2 :— B o d y 2 ) , ( H e a d 3 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  :— B o d y ) ) :—  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],  C a l l =.. [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  get_prev_IO(RestA2,HeadA2,IA,OA), get_prev_IO(RestB2,HeadB2,IB,OB), Head2 =.. [ N e w l a b e l , I A , O A ] , Head3 =.. [ N e w l a b e l , I B , O B ] , list_to_body(RestA2,Body2), list_to_body(RestB2,Body3),  130  Appendix E Program Printing  % *** % *** Bruce  % ***  % ***-  _  % *** % *** % ***  program Brian  J.  pretty  printer  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 b r u c e ( [ A | B ] ) :— nl, print b r u c e 2 ( A , 0 ) , nl, print_bruce(B), I,  print_bruce2( [ ] . print_bruce2( [' {' | R] ,Tab) : N e x t t a b is T a b + 3,  131  Utilities  APPENDIX  E. PROGRAM  PRINTING  UTILITIES  w r i t e l Q ' {' ,nl,tab(Nexttab)]), print_bruce2(R,Nexttab). p r i n t . b r uce2( [ ' } ' , ' ; ' | R ] , T a b ) : N e x t t a b is T a b - 3, w r i t e l ( [ n l , t a b ( N e x t t a b ) , ' } ; ' ,nl,tab(Nexttab)]), print_bruce2(R,Nexttab). p r i n t _ b r u c e 2 ( [ ' } ' , » u n t i l ' |R],Tab) : N e x t t a b is T a b - 3, writel([nl,tab(Nexttab),'} u n t i l ' ] ) , print_bruce2(R,Nexttab). print_bruce2(['}','}'|R],Tab) : N e x t t a b is T a b - 3, N e x t t a b 2 is N e x t t a b - 3, w r i t e l ( [ n l , t a b ( N e x t t a b ) , ' } ' , n l , t a b ( N e x t t a b 2 ) , ' } ' ,nl,tab(Nexttab2)]), print_bruce2(R,Nexttab2). print_bruce2(['>' | R ] , T a b ) : N e x t t a b is T a b - 3, w r i t e l ( [ n l , t a b ( N e x t t a b ) , ' } ' ,nl,tab(Nexttab)]), print_bruce2(R,Nexttab). print_bruce2([S, ;' |R],Tab) : w r i t e l ( [ 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...") y *** Q  %  % printjprolog/2 prints a beautified version of P into file File.  APPENDIX  %  E. PROGRAM  It calls print_prolog/1  PRINTING  to do the actual  UTILITIES  133  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  print_clause([]). print_clause(C) :— beautify ( C ) , C =.. [(:-)|[Head|Body]], writel(Head,' : - ',nl), print_goals(Body). print_clause(C) :— w r i t e l ( C , ' . »,nl).  %  print_goals(G)  prints  print_goals([]). print_goals([(A,B)|R]) : -  the goals in list G, 1 per line.  it.  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  135  UTILITIES  Vnames2 \ = = Vnames, set_names( Rest, Vnames). set_names([A|Rest],Vnames) : -  A =.. U g l . Ar  s  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)  % and returns  finds  the appropriate  out what type of mechanism  variable  name  Name  represents  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 v a r ( V ) , !, set_name(V,Name) :— retract(save_no(Name,Num)), N e x t is N u m + 1, atom_append(Name,Next,New), capitolize(New,Newname), V = Newname, t assert (save_no( N ame , N e x t ) ) ,  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  reset_name_numbering :— abolish(save_no,2). reset_name_numbering.  PRINTING  UTILITIES  137  Appendix F Miscellaneous  Code  % *** % *** Main  % ***  driver  % ***  _ Brian  % ***  Dept.  J.  % *** y ***  University  Ross  of Computer of British  Science Columbia  0  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," ) *',nl), print prolog(PFile,Mixed), 1  % 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  m i x p r o l o g ( F i l e , C a l l ) :— writel('* Reading P r o l o g i n  1 1  ',File,'"  *',nl),  [File],  %  mixcall(Call),  parse(File) :— translate(File,Prolog), w r i t e l ( n l , ' * DONE.  *',nl),  I.  translate(File,Prolog) : start_up, alt_read_file ( F i l e , D at a), writel('* " ' , F i l e , ' " read  *\nl),  % lexical(Lex,Data), writel('* L e x i c a l succeeds *',nl),  %  env(Tree,Lex,[]), writel('* Parse succeeds *',nl),  % pretty (Tree),  %  gen_prolog(File,Tree, Prolog), atom_append(File,'.pro' ,PFile), writel('* P r o l o g generated (see ' " j P F i l e , " ' ) print_prolog( P F i l e ,Prolog), assert_prolog(Prolog),  *',nl),  % brucify(Prolog,B), atom_append(File,' . b r u ' , B F i l e ) , writel('* Bruce generated (see " » , B F i l e , ' " ) print_bruce(BFile,B),  *',nl),  % lexical(Lex,Data) converts the characters Data into lexical tokens % in Lex. l e x i c a l ( L e x , D a t a ) :— lex(Lex,_,Data,[]).  APPENDIX  F. MISCELLANEOUS  CODE  140  % some cleaning up... s t a r t j i p :— tabolish, reset_gen_nums,  gen_prolog(File,Tree,Prolog) :— Tree" "code(Code), flatten(Code,Prol), writel('* B a s i c 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,' . l a b ' , L F i l e ) , writel('* . . . (see "',LFile,'") *',nl), print_prolog(LFile,Pro2),  % process_branches(Pro2,Prolog), writel('* Branches processed *',nl) Prolog = P r o l ) ,  % *** % *** 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  o r d e r ( G o a l s , A , B ) :— vars_used(A,VAI,VAO), vars_used(B,VBI,VBO), VAO == V B I , o r d e r ( G o a l s , A , B ) :— varsused(A,VAI,VAO), vars_used(B,VBI,VBO), VAI == V B O , i  fail. o r d e r ( G o a l s , A , B ) :— is_a_test(B), extract_vars(B,VB), vars_used(A,VAI,VAO), subset(VB,VAO), !,  o r d e r ( G o a l s , A , B ) :— is_a_test(A), extract_vars(A,VA), vars_used(B,VBI,VBO), subset(VA,VBO),  I faU. o r d e r ( G o a l s , 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),  141  APPENDIX  F.  MISCELLANEOUS  142  CODE  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)  or a subset of the output variables  variables in  in A are  dependent  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  same_out_vars(A,B) :— vars_used(A,_,OutA), vars_used(B , _ , O u t B ) , OutA == OutB, i  %  % order_clause_goals(L,S)  orders goals in L, resulting  order_clause_goals(L,S) :— insort(L,S).  % % from  Clocksin  insort(0,D) - !• insort([X|L],M)  & Mellish,  :-  pp.146  ...  in  S.  variables.  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  vec_variant(Initial,Varj ,Var_f,Final) :— break(Var_i,A,[B|C] .Initial), append(A,[Var_f|C],Final), i  Var_i is replaced by Var_f.  APPENDIX  F.  MISCELLANEOUS  CODE  % % match_vars(A,B,C) % variable  matches  variable  144  ;  names in A with their  values, as are listed in B, resulting  in  logical  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) % with its corresponding  matches each variable output variable,  as determined  in  Vars 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 ( V a r , A , B , A n s ) ) .  % *** % *** % ***  List  utilities  % % program_separate(Env,Labels,Collect,Prolog) % the sections used by the original Bruce % The Labels list these predicate names.  separates predicates source programs.  into  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 ( E n v ,Rest , B ) , append(Refs,B,A)).  %  _  % getjabeljrefs(Env, Label, Collect,Result) collects all the clauses in Env % named by Label.  g e t j a b el_refs( [] , L abel ,Refs ,Refs). get_label_refs([(Head  : - B o d y ) | R e s t ] , L a b e l , C o l l e c t , R e f s ) :—  i •>  .  (functor(Head,Label,_)  —>  get_label_refs(Rest,Label,[(Head  : - Body)|Collect],Refs)  i g e t j a b el_refs (Rest , L abel, Collect ,Refs)). getJabel_refs([Clause|Rest],Label,Collect,Refs) :— i •>  (functor(Clause,Label,_) —> get Jabel_refs(Rest, L a b e l , [Clause| Collect],Refs) g e t j a b el_refs (Res t , L abel,Collect, Refs)).  f *** % *** Miscellaneous Prolog utilities... % *** 0  %  % member routine in which the Items may be uninstantiated % (logical variable matching). member(_,[|) : - !,fail. m e m b e r ( I t e m , [ X | J ) :— I t e m = = 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 % (corresponding variables may be different)  equivalent.  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  ! •)  A =.. [Name|ArgsA], B =.. [ N a m e | A r g s B ] , 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 n m e m b e r ( N u m , L i s t , I t e m ) :— nmember( 1 , N u m , L i s t ,Item), I.  nmember(N,N,[Item|_],Item). nmember(Curr,Num,L|Rest],Ans) :— N e x t is C u r r + 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])  ::-  147  APPENDIX  F. MISCELLANEOUS  CODE  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), f u s e ( ( t r u e , A ) , B ) :— fuse(A,B)> f u s e ( ( " , " ) , " ) : - !. 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),  148  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 u t ) . 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) % without  removes all the variables  used in V into list A,  duplicates.  e x t r a c t _ v a r s ( V , A ) :— extract_vars(V,[],A), I  e x t r a c t _ v a r s ( V , C o l l e c t , A ) :— var(V), (member(V,Collect) - > A = Collect A = [V | Collect]). e x t r a c t _ v a r s ( X , A , A ) :— ( X = = [] ; a t o m ( X ) ) . extract_vars([V|R],Collect,A) : extract_vars(V,Collect , X ) , ext ract_vars( R , X , A ) . extract v a r s ( X , C o l l e c t , 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]))c o m p l e m e n t a r y ( A , B ) : - n o t ( n o t ( B =.. [ ' " " ' , A ] ) ) .  %  % remove_item(Item,List,Newlist) % resulting  in  removes the first instance  of Item in  List,  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 split_clause((Head :— B o d y ) , H e a d , B o d y l i s t ) args_to_list(Body,Bodylist), i  %  % Copy structure  A into B, so that it has unique  copy(A,B) : assert(copied(A)), retract(copied(B)), I  variables  Body.  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 A  :-  \ = = Q,  \== 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,[|). p e r m u t a t i o n ( [ 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]) : W r i t e =.. [ W r i t e R t n , A ] , Write,nl, write_list(vert,WriteRtri,B), I.  write_list(horz,WriteRtn,[A]) :—  APPENDIX F. MISCELLANEOUS CODE  154  i  •>  Write =.. [WriteRtn,A], Write. w r i t e j i s t ( h o r z , W r i t e R t n , [ A | B]) : Write =.. [WriteRtn,A], Write, write(','), w r i t e j i s t (horz , W r i t e R t n , 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), L e f t l \ = = [], R i g h t l \ = = [], count(Rightl,N), append(Left2,Right2,L2), count(Right2,N).  :-  duo_split(left,L 1 , L e f t l , R i g h t 1 ,L2,Left2,Right2) rev(Ll,RLl), rev(L2,RL2),  :-  append(RLeftl,RRightl,RLl), R L e f t l \ = = Q, R R i g h t l \ = = [], 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 H e a d = 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 : - B o d y ) ) :— list_to_body ( L e f t , B o d y ) .  APPENDIX  F. MISCELLANEOUS  CODE  156  make_clause(Head,[],Right,(Head : - B o d y ) ) :— list_to_body(Right,Body). make_clause(Head,Left,Right,(Head :— B o d y ) ) :— app end( Left , R i g h t , G o a l s ) , 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,_,_,[]) :- !. m e r g e _ g o a l s ( _ , _ , _ , I A , O A , A , I n , O u t , 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 :— B o d y ) ) :— copy((Clause,Vec,Code),(Clause2,Vec2,Code2)), split_clause(Clause2,Head,Goals), Head =.. [ N a m e , I l , O l ] , 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 Phead,  — the found parent clause 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. % be its own  Recursive  calls are not used —  % sibling_clause  (Prolog, Clause, Sibling)  finds  a sibling for  :—  Clause from  sibling_clause(Prolog,Clause,Sibling) :— split_clause(Clause,Head,_), copy(Head,Item), member2(Sibling,Prolog), split_clause(Sibling,Item,_), S i b l i n g \ = = Clause.  % assertjprolog(P)  tasserts  assert_prolog(_) : - !. assert_prolog([Clause|Rest]) tassertz(Clause),  all the code in list P.  :—  assert_prolog(Rest),  |  #  %  % Make  cannot  parent.  parent_clause(Prolog,Head,Paxent,Phead,Left,Goal,Right) copy ( H e a d , G o a l ) , member 2 ( P arent ,P rolog), split_clause(Parent,Phead,Goals), not P h e a d = H e a d , append(Left,[Goal|Right],Goals).  %  a clause  an atom like Name  into one which is  capitolized.  Prolog.  APPENDIX  F. MISCELLANEOUS  CODE  c a p i t o l i z e ( N a m e , C a p s ) :— name(Name,[A|L]), A >=  97,  A =<  122,  A 2 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  158  APPENDIX  F. MISCELLANEOUS  endpffile(-l) ?.  159  CODE  :-  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  %  later  removal.  assert  clauses,  tassert(Clause) :— set_rem_clause( Clause), assert(Clause),  plus  update  a tag  to  be used  for  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 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  t a b o l i s h ( P r e d , A r i t y ) :— rem_clause(Pred,Arity), abolish(Pred,Arity), retract(rem_clause(Pred,Arity)). tabolish(_,_).  utility  is used  elsewhere.  APPENDIX  F. MISCELLANEOUS  CODE  % remove all clauses asserted by tassert utilities t a b o l i s h :— rem_clause(Name,Arity), abolish(Name,Arity), fail, t a b o l i s h :— abolish(rem_clause,2).  % list writing routine (written by Doug Westcott) writel([A|B]) : write_item(A), writel(B), writel(Q) : -  w r i t e l ( 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]),  161  APPENDIX  F. MISCELLANEOUS  CODE  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, w r i t e j t e m ( X ) :— var(X), write(X), write item(nl) :— nl, write_item(tab(N)) tab(N), write_item(X) :— write(X),  :—  162  Appendix G Binary G C D Basic  bingcd([Gcdl,Ul,Vl],[Gcd2,U2,V2])  Semantics  :-  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  164  SEMANTICS  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 G C D 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  test6([Gcdl,Ul,Vl,Kl,Pl,Tl],[Gcd2,Ul,Vl,K2,P2,Tl]) ~T1=\=0,  SEMANTICS  :-  asgn([Gcdl,Ul,Vl,Kl,Pl,Tl],K2,Kl,[Gcdl,Ul,Vl,K2,Pl,Tl]), callasgn( [ G c d l , U 1 , V 1 , K 2 ,P 1 , T 1] , T m p 1,2), caUasgn([Gcdl,Ul,Vl,K2,Pl,Tl],Tmp2,K2), power([P 1 , T m p l , T m p 2 ] , [ P 2 , T m p 3 , T m p 4 ] ) , 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:

        

Citations by CSL (citeproc-js)

Usage Statistics

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