IMPLEMENTATION OF A LOGIC PROGRAMMING LANGUAGE: R-MAPLE AND ITS EXTENSION TO INCLUDE FUNCTIONS by Benjamin Yu B.Sc. ( Hons.), The University of British Columbia, 1982. A THESIS SUBMITTED IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF MASTER OF SCIENCE in THE FACULTY OF GRADUATE STUDIES (Department of Computer Science) We accept this thesis as conforming to the required standard THE UNIVERSITY OF BRITISH COLUMBIA October 1984 © Benjamin Yu, 1984 In presenting t h i s thesis i n p a r t i a l f u l f i l m e n t of the requirements for an advanced degree at the University of B r i t i s h Columbia, I agree that the Library s h a l l make i t f r e e l y available for reference and study. I further agree that permission for extensive copying of t h i s thesis for scholarly purposes may be granted by the head of my department or by h i s or her representatives. I t i s understood that copying or publication of t h i s thesis for f i n a n c i a l gain s h a l l not be allowed without my written permission. Department of Computer Science The University of B r i t i s h Columbia 1956 Main Mall Vancouver, Canada V6T 1Y3 Date 12 October, 1984 DE-6 (3/81) - ii -Abstract The use of logic as a language for communication with computers has been exploited in various research areas. R-Maple is a logic programming language, designed by Paul Voda, which improves on some of the short-comings of Prolog. The implementation details of R-Maple will be discussed. R-Maple is a relational programming language which has relations as its basic objects. It can be extended to include functions to form a functional and relational programming language. The advantage is to increase readability and efficiency during compu-tation. RF-Maple is such a language which results from combining the features of R-Maple with a functional language F-Maple. The semantics of RF-Maple needs to be defined formally. The currently available methods of formalizing the semantics of a programming language are either too complex or insufficient for the task. The theory of pairs [Voda2 84] can be used in formalizing the seman-tics of RF-Maple. However, introduction of types to the theory is not straight forward. Hence RF-Maple is modified to become a typeless language and its semantics is defined using the theory of pairs. - iii -Table of Contents 1. Introduction 1 2. Logic Programming 4 2.1 Implemented Systems 5 2.2 Deficiencies of Existing Systems 6 3. Introduction to R-Maple 8 3.1 Concrete Syntax of R-Maple Programs 10 3.2 Transformation as Computation 15 3.3 Abstract Syntax of R-Maple 20 4. Implementation of R-Maple 27 4.1 Data Structure 27 4.2 Construction of the R-Maple Tree 29 4.3 Transformation of the R-Maple Tree 30 4.4 Processes • •• 31 4.5 Backward Movement of a Process 34 4.6 Free and Bound Variables 36 4.7 Hardward Consideration 40 4.8 Examples of R-Maple Abstract Program 41 5. Motivation for A Functional and Relational Programming Language 49 5.1 Description of F-Maple 50 5.2 Terms over F-Maple Types 52 5.3 Examples of F-Maple Programs 54 5.4 Computation of F-Maple Programs 55 5.5 Description of RF-Maple 56 5.6 Examples of RF-Maple Programs 59 6. Background of Semantics Theory 64 6.1 The Operational Approach 65 6.2 The Denotational Approach 66 6.3 The Axiomatic Approach ••• 67 7. Theory of Pairs 69 7.1 Semantics of RF-Maple 71 7.2 Typeless RF-Maple 72 7.3 Formalization of the Semantics of TRF-Maple in TP 76 8. Future Work 88 9. Conclusion 01 Reference A p p e n d i x A A p p e n d i x B A p p e n d i x C A p p e n d i x D A p p e n d i x E - V -Acknowledgement I would like to express my appreciation to Dr. Paul Voda for his continual sup-port and guidance throughout the preparation of this thesis. His expertise and immense interest in programming languages and logic certainly motivates me to continue in my study and research. I would like to thank Dr. Karl Abrahamson for his careful reading of my thesis. I would like to thank the Natural Sciences and Engineering Research Council for their financial support. I would also like to thank my family, friends and my beloved fiancee for their continual prayer sup-port and encouragement during the course of my program. Most of all, I would like to give all thanks and praises to my Lord and Saviour Jesus Christ, without Him this thesis would never have been completed. Chapter 1 Introduction 1. Introduction Recently, considerable amount of attention is given to the fifth generation computing especially with the Japanese effort in designing a whole new genera-tion of computing machine. With the advance in machine technology', a parallel effort in designing software that utilizes the machine technology is necessary. Of foremost importance is the need of a programming language that will allow the user to interact with the computer more efficiently and with less mistakes being made. The programming language PROLOG which is used widely in many different areas of research in artificial intelligence, and before, PLANNER and CONNTVER, etc. all have received considerable attention. However, there are deficiencies in each of these languages. R-Maple grew out as a logic progamming language that is based on predicate logic but with the added control feature that is lacking in other logic programming languages. Its features will be described in later sections. R-Maple is a logic programming language which does not allow functions as terms. This is a limitation as a logic programming language because this requires that all functions to be written as relations. Not only relations do not have the expressive power of functions, they require more overhead to com-pute due to their backtracking nature. To overcome this limitation, RF-Maple is designed to retain the features of a logic programming language like R-Maple but with the added feature of allowing functions as its terms. It is a combination of two languages, R-Maple and F-Maple. The latter being a typed language and Chapter 1 Introduction . .2 provides, not only for semantic extensibility (new types and functions), but also for syntactic extensibility. In order to determine the correctness of the RF-Maple language, it is necessary to formally define its semantics. The currently available methods of formalizing the semantics are either too complex or inadequate for the task. The theory of pairs, TP, is based on first order logic especially designed to cater to formalizing the semantics of functional and logic programming language. To define the semantics of RF-Maple it is necessary to introduce types into the theory of pairs. This is not that straight forward. Hence, typeless RF-Maple is designed to simulate the result that can be obtained in RF-Maple. The theory of pairs is used to define the semantics of TRF-Maple. This thesis is composed of three main parts. The first part is on the imple-mentation of R-Maple. The second part is on the design of RF-Maple, and finally, the third part is on the definition of typeless RF-Maple (TRF-Maple) and the formalizing of its semantics using the theory of pairs. Chapter 2 will begin with a background of currently available logic programming languages. Chapter 3 is the description of R-Maple and Chapter 4 is the implementation details of the language. Chapter 5 is the description of RF-Maple, how the two languages R-Maple and F-Maple are combined to form a functional and relational program-ming language. Chapter 6 begins the background of the current methods in defining the formal semantics of programming languages. Chapter 7 describes the theory of pairs as a way of defining the semantics of a programming language. Since introduction of types to TP is not that straight forward, typeless RF-Maple (TRF-Maple) is designed that could simulate the computation of typed RF-Maple. This section also shows how the semantics of TRF-Maple can be Chapter 1 Introduction .. 3 formalized in the theory of pairs. Chapter 8 is a discussion on future work that may be continued. 4 C h a p t e r 2 L o g i c P r o g r a m m i n g 2. Logic Programming T h e i d e a of p r o g r a m m i n g i n logic can be traced back to the first logic pro-g r a m m i n g languages, P R O L O G , developed by A l a i n C o l m e r a u e r a n d P h i l l i p e R o u s s e l i n 1972 [Kowa]. L o g i c is an i m p o r t a n t t o o l i n the analysis a n d presenta-t i o n of arguments. It investigates whether assumptions i m p l y conclusions, independently of t h e i r t r u t h or falsity and independently of their subject m a t t e r [ K o w a 79]. L o g i c is used as a language for c o m m u n i c a t i o n w i t h computers because of its h i g h e r - l e v e l a n d more h u m a n - o r i e n t e d nature t h a n other f o r m a l -isms specifically developed for computers [ K o w a 79]. A p r o g r a m m e r can i n i t i a l l y ignore p r o c e d u r a l details a n d concentrate on the (declarative) essentials of the a l g o r i t h m . H a v i n g the p r o g r a m b r o k e n d o w n i n t o s m a l l independently m e a n i n g -f u l u n i t s , it is m u c h easier to u n d e r s t a n d . Design flaws are less l i k e l y to result , perhaps because it is more difficult to m a k e a " l o g i c a l e r r o r " i n a p r o g r a m w h e n its logic is a c t u a l l y expressed i n logic [Warr 77]. T h e m e a n i n g of p r o g r a m s expressed i n c o n v e n t i o n a l languages is defined i n terms of the b e h a v i o u r they i n v o k e w i t h i n the computer. F o r example, a p r o -g r a m m e r u s i n g a c o n v e n t i o n a l language, l i k e P a s c a l , A d a , e t c . , needs to be aware of the i n c r e m e n t a l changes (or side effects) m a d e to variables. O n the other h a n d , the m e a n i n g of programs expressed in logic can be defined i n m a c h i n e -independent , h u m a n - o r i e n t e d terms [ K o w a 79]. T h e r e are no side effects i n logic programs. T h e v a l u e of an expression (its meaning) is determined solely b y the Chapter 2 Logic Programming .. 5 values of its constituent parts. Thus should the same expression occurs twice in the same context, it denotes the same value at both occurences. 2.1. Implemented Systems The first logic programming system called PROLOG based on the procedural interpretation of Horn clause was designed and implemented in 1972. A Horn clause : B <- Alt .... , Am m>0 is interpreted as a procedure whose body {A j .... , Am } is a set of procedure calls A;. Top down derivations are computations. Generation of a new goal statement from an old one by matching the selected procedure call with the name B of a procedure is a procedure invocation [Kowa 79]. A more detailed descrip-tion of PROLOG can be found in [Clos & Mell 80]. Another system which is also based on logic is the programming language PLANNER by Carl Hewitt [Hewi 69]. It was originally written in LISP. PLANNER accepts declarative information, as in predicate calculus. This is in the form of expressions which represent "facts" about the world. These are manipulated by the theorem-prover according to some fixed uniform process set by the system. PLANNER can also accept imperative information, telling it how to go about proving a subgoal, or to make use of an assertion. It has the full power of a general programming language to evaluate functions which can depend on both the data base and the subgoal tree, and to use its results to con-trol the further proof by making assertions, deciding what theorems are to be used, and specifying a sequence of steps to be followed [Suss, Wino & Char]. Section 2.1 Implemented Systems .. 6 Due to the inefficiencies of backtracking in PLANNER, another programming language also based on logic, called CONNIVER [Suss & Mcde 72] is developed. CONNTVER is a PLANNER-like programming language in which the program-mer writes both problem-solving procedures and search strategies. 2.2. Deficiencies of Existing Systems It has been demostrated that PROLOG can be used in a variety of applica-tons such as natural language systems [Colm 75], [Dahl & Samb 76], compiler writing [Colm 75] [Warrl 77], algebraic manipulation [Berg & Kano 75], definite > clause translation grammar [Abra 84], and the automatic generation of plans and programs [Warr 74]. However, PROLOG does have its deficiencies. PROLOG has a very weak control component. Conceptually at least, the control com-ponent is entirely absent in PROLOG. The decision on how to sequence compu-tations and what to do in parallel is left entirely to the PROLOG interpreter act-ing as a virtual executing machine [Voda 83]. Even concurrent PROLOG with the use of the commitment operator and read only variables is not that straight forward. The lack of control in PROLOG can be seen in the following example where the use of the cut operator is necessary. P { z ) - Q \ x ) , \ , R ( z ) P [x ) «- S (x ) *-P(a) This is a very common situation when a programmer relies on implicit control built into the PROLOG interpreter. Assume that during the refutation of P(a) the test Q(a) is satisfied but not R(a). The next clause for P(x) should be tried. However, due to the use of the cut operator, no backtracking takes place. The Section 2.2 Deficiencies of Existing Systems .. 7 programmer might have intended the second clause to be as follows: P(z)<-~ Q(z),S(x) but because of the difficulties with negation in PROLOG clauses, and for reasons of efficiency, a cut operator is used. Cuts cannot be explained in logic within the context of a clause and without an ordering of clauses (Voda 83]. PLANNER and CONNPVER, on the other hand, allow control primitives for guiding search strategies. But this is exactly what is not desirable in a language where a programmer should only focus on the nature of the problem rather than the behaviour of the program inside the machine. .. 8 Chapter 3 Introduction to R-Maple 3. I n t r o d u c t i o n to R - M a p l e R-Maple is a relational concurrent programming language based on predicate logic developed at the University of British Columbia by Paul Voda. The philo-sophy behind R-Maple is to allow the programmer to view the computation of programs as an attempt to prove the program using certain axioms and rules of inference. The advantage is that, in trying to solve a problem, the programmer can lay down statements that are true and let the computing machine draw con-clusion from it, or to prove the theorem that he/she wants it to prove. This style of programming using logic is contrasted with the conventional way of program-ming using languages like Pascal, Ada, etc. in that, in the later case, a program-mer needs to think also in terms of what the computer should do and when. [Hend 80] The following is a brief description of R-Maple. A full description of the language can be found in [Voda 83]. R-Maple is a relational programming language as opposed to a functional programming language. A functional programming language has functions as its basic objects and functions have a many-to-one correspondence between the argu-ments and the results (or between the domain and range). A relational program-ming language, on the other hand, has relations as its basic objects, and relations can have multiple results corresponding to an input argument, (ie. relations have a many-to-many correspondence between the domain and range). Since R-Maple is a relational programming language, this adds to R-Maple the possibility of Chapter 3 Introduction to R-Maple .. 9 achieving non-determinism which is not available in functional programming language. R-Maple is an applicative language as opposed to an imperative language. By applicative language, it means that the value for an expression or a relation (or its meaning) is determined solely by the values of its constituent parts. Thus, should the same expression occur twice in the same context, it denotes the same value at both occurences. On the other hand, an imperative language computes by effect. This means that in using an imperative language, one must think in terms of the incremental changes made to variables by successive assignments [Hend 80]. The same procedure declared in an imperative language may produce different results due to the effectual assignments to variables. It is the absence of this ability to effect changes to values of variables which characterizes purely applicative languages like R-Maple. As mentioned earlier, R-Maple is based on predicate logic. Programs of R-Maple correspond to formulas of predicate calculus. As will be seen in Chapter 7, the task of specifying the semantics of TRF-Maple where R-Maple is one of its component languages becomes rather straight forward. The syntax of R-Maple can be viewed from two main aspects. The first aspect is called the concrete syntax which is a fairly rich syntactic structure that makes the program readable and easy to understand. The second aspect is called abstract syntax which is less readable by humans but may be easily composed and decomposed by other programs. The first part of this thesis which is on the implementation of R-Maple concentrates on this latter aspect, (ie. taking a pro-Chapter 3 Introduction to R-Maple ..10 gram written in abstract syntax and interpreting it). A programmer writing a R-Maple program would, however, use the concrete syntax. Thereafter, it is con-verted into the abstract syntax by a compiler, and finally executed by the R-Maple interpreter. The concrete syntax of R-Maple will be described first followed by the abstract syntax. 3.1. Concrete Syntax of R-Maple Programs R-Maple is a logic programming language, where, each program of R-Maple can be read as a formula of predicate logic. A formula written in first order predicate logic can be easily translated into the concrete syntax of R-Maple because there is a correspondence between keywords used in R-Maple with those used in logic. The following table summarizes the corresponedence. R-Maple: Logic: R-Maple: Logic: program formula expression term prog, variable indiv. variable invocation atomic formula find 3 quantifier ; and |j conjunction or and orp disjunction Hence, an R-Maple program such as: find x in x := 5; x >3 can be directly translated to a first order logic formula as: 3z (x = 5,& x >3). Also, the program written in R-Maple as: find x in (x := 5 or x := 6 or i := 77); x >10. can be written as a first order logic formula as: Section 3.1 Concrete Syntax of R-Maple Programs ..11 3x ( ( i = 5 V x = 6 V x = 77) & x >10). R-Maple provides sequential and parallel connectives. That is, if A and B denote two programs, then A ; B denote the logic formula A & B. Moreover, it tells the R-Maple interpreter that A is to be executed and completed before B is to be executed. This is contrasted with the parallel connective |[ where A || B instructs the interpreter to start a process in both A and B in parallel. The meaning of A ; B and A \\ B are the same since both denote the logic formula A & B. But the control, which directs the behaviour of the machine is different. This might have significant consequences in proving some theorems on the R-Maple machine such as : p (* ); (5>7) where computation of p (x ) diverges. The corresponding formula in first order logic is false since 7 is always greater than 5. However, to compute this formula in R-Maple using the sequential connective will lead to an infinite loop or a deadlock since the predicate p (x ) diverges. On the other hand, computing p (x ) || (5>7) on the R-Maple machine will correctly produce the answer. It should be noted that proving the following theorem on the R-Maple machine pro-duces the correct result even though p (x ) diverges. / alse ; p (x ) Computation will converge with the correct result / alse . Sequential and parallel disjunctive are also provided in R-Maple and their behaviour in the executing machine is similar to the case described for the con-nectives earlier. Section 3.1 Concrete Syntax of R-Maple Programs .. 12 Conditional tests are also provided in the concrete syntax of R-Maple. They take the usual form of the IF-THEN-ELSE statement. For example, if x > 3 then s (x ) else t (x). Its declarative reading is: ( i > 3 ) - > s ( x ) & (x<3)-*t(x). A user may use predicates predefined by the system or those defined by the user himself or herself. Each predicate can take the form with output arguments or without. Those that take the first form are called tests and those that take the second form are called generators. A bar | is used to seperate the input argu-ments from the output arguments in the concrete syntax of generators. Some examples of system predefined tests are: eq (x.y), ne (x,y), It (x,y), etc., which are tests for equality, inequality, and other comparison tests for two numbers x and y. Examples of system predefined generators are: add (x,y |z), sub (x,y |z), div (x,y |z), rem (x,y |z), etc., which are generators for addition, subtraction, division, and the remainder function etc. for two numbers x and y with the output in z. The user is given the freedom to use either infix or prefix form for the system defined predicates. In infix form, the user is allowed to use symbols such as +, -, >, etc. instead of the function name. All infix forms are converted to prefix forms during the compilation process from concrete to abstract sytax. For the rest of the discussion on R-Maple, all system defined predicates used in the exam-ples are presented in infix form. Users can define his/her predicates by preceding the program with a predi-Section 3.1 Concrete Syntax of R-Maple Programs .. 13 cate name and the input and output variables (if any). Thus, a predicate to test whether a number is even or not can be first defined in first order logic as: Even (x ) = 3r ( rem (x,2,r ) & r = 0) where rem (x ,y ,z ) is a predicate to compute the remainder of x divided by y with the result in z. Since there is a predefined generator "rem" and also the predefined test "eq" (for test of equality) in R-Maple, the formula can be simply translated as: r Even (x ) is find r in rem (x,2 | r ); eq (r,0). The user can then use the predefined predicate in other parts of another program. R-Maple does not allow the output variable of a predicate to be initially instan-tiated during the invocation. Hence, although the declarative reading for the Even predicate is also: Even (x ) = rem (x ,2,0) R-Maple does not allow the predicate rem to be invoked as rem (z,2 | 0). On the other hand, the input argument may be left uninstantiated during the invocation. The use of the uninstantiated input argument will be suspended until another proccess assigns a value to it. This will be discussed in more details in later sections. Although R-Maple allows the definition of predicates with any number of input arguments, in essence, the compiler translates the input and output argu-ments to a single argument as an expression. The syntax of an expression is as follows. Section 3.1 Concrete Syntax of R-Maple Programs ..14 The simplest form of an R-Maple expression can be a literal or a variable. The formation rules for a literal are: a) each numeral is a literal, b) the symbol "nil" is a literal, c) if s and t are literals, so is [s,t]. If Exprl and Expr2 are expressions, then so is [ Expr \,Expr2]. This final form is often referred as a consed expression and resembles closely to that in LISP. Appendix A gives the full description for R-Maple expressions in BNF notation. The input and output arguments of a predicate is translated to an expres-sion of the form [Exprlyy ] where y is the output argument and Expr^ is the expression for the input arguments. The latter can be either a single argument or any number of arguments represented as a single expression. For example, the invocation of a predicate f oo with three input arguments, w, x and y, and one output argument, z, is taken to be a predicate with an argument of the form foo {[[w,[x ,y ]],z ]). To allow accessing of the individual argument, R-Maple provides the find construct to be of the form: find [hd ,tl ] = a in Prog where a can be "split" into two expressions with hd = head of the pair a and tl == tail of the pair a for further processing. This construct can also be referred as a split operation in R-Maple. Hence, for example: foo {x ) = find [hd,tl ] = x in find [hdl,tll] = hd in print {hd 1); print {tl 1); tl :=hd 1. This predicate can be invoked in a program as: find y in foo {[[l,2],y ]). Section 3.1 Concrete Syntax of R-Maple Programs ..15 When executed, the program will print the value 1 which is the head of the head of the input argument, and also the value 2 which is the tail of the head of the input argument. Finally, the predicate is satisfied with y = 1. Appendix B gives the full description for R-Maple programs and the definition of predicates in BNF notation. 3.2. Transformation, as Computation Computation of a R-Maple program is a series of transformation until the most simple atomic formula <trueop ,nil > or </alseop ,nil > results. A com-putation proceeds by steps which successfully modify the original program. The following describes briefly the transformation schema that are applicable for the R-Maple machine. The transformation schemas are listed out in Appendix C in a more formal and rigorous format. They appear also in [Voda 83]. Computation is performed by application of rewriting rules of the form A => B where both sides contain the operator !. Transformation of system defined predicates Lt, Le, Gt, and Ge to true or false can proceed only if the arguments are not variables. Otherwise, transforma-tion is suspended until the appropriate arguments are obtained. Predicates of identity, Eq and Ne do not require both arguments to be fully reduced. This sometimes permits an earlier decision on expression still containing variables. When two expressions of the form [Expr x ,Expr_\ and [Expr^Expr^] are tested for equality, two processes are created to compare Expri with Expr^ and Expr2 with Expr4 in parallel. More sub-processes may be created from these Section 3.2 Transformation as Computation ..16 processes. If any of these processes reduces to false even if some of the other processes are not finished in their execution, the entire test can be quickly reduced to false. Invocation of the predicate Print is delayed until its arguments becomes a quoted expression. Then the literal is printed out and the invocation is reduced to T! Arithmetic predicates, Add, Sub, Mul, Div, and Rem, are also delayed until the appropriate arguments are obtained. In the case of user defined predicates, invocation of predicates is first preceded by substitution of the formal argument with the actual argument. The process may then proceed to transform the body of the invoked predicate. Invocation of the predicate Return is a bit different from the invocation of other predicates. This will be discussed later. Other unconditional schemas of transformations include the negation scheduling, conjunction scheduling, disjunction scheduling, truth table transfor-mations. These transformations preserve the intended meaning unconditionally, i.e. they do not rely on lists of definitions. Most of these transformations are relatively straight forward. One thing to note is that in the transformation of a parallel disjunction or conjunction, two processes are created to execute the left and right branch in parallel whereas in the sequential case, the original process is used to execute the left branch. Only when the transformation of the left branch is reduced to true or false will the right branch be transformed. Section 3.2 Transformation as Computation ..17 Decisions can be expressed with the help of sequential or parallel and's, or's, and not's but the efficiency of computations is improved by having if-then-else as a basic operator. In the transformation of if Prog! then Prog2 else Prog%, once Prog 1 is reduced to true or false, the if-then-else construct is transformed into either Prog2 or Prog3. Execution continues with their transformation. The execution of the split operation (or find [ Vari,Var2\ = Expr in Prog ) is delayed until the expression to be split is not a program variable. A consed expression can be immediately split into two constituents. Constituents of the consed expression are then substituted in Prog for the appropriate variable. Transformation for the find construct is a search operation which intro-duces a scope in which a value or values of the variable declared will be searched for. Execution immediately transfers to the body of the find construct to search for the value of the variable. When the value for a variable is "found", the predicate Return is invoked so that the find construct for that variable may be discharged. For every invocation of the predicate Return for a variable "x", there needs to be a corresponding find for the variable "x". In R-Maple, when the predicate Return is invoked, the value that is found for the variable should be "moved" back to the find so that the searching process may be discharged. [Note that the schema for the transfor-mation of the find construct is a forward movement of the process, allowing the body to be executed. The Return predicate serves as an initiation of the back-Section 3.2 Transformation as Computation .. 18 ward movement of the process to discharge the find ]. During the backward movement of the variable to its corresponding find , there might be other find along the backward move. For example: find x i n .... find y i n .... x :=4 ! ; . . - . ; y :=6 or represented in logic as: 3x .... ly (.... x — 4 y = 6 ) Also, during the backward move, a parallel or sequential "and" or "or" may be encountered. In those cases, there needs to be some mechanisms to store the type of nodes that are encountered along the backward move so that further execution may be resumed later. The transformation schema for the predicate Return is: Return (Expr \ Var ) => bfindss a i n ( V a r : = E x p r ; T ) o r F where T represent true and F represent false, bf indss is one of four new con-structs to be introduced into the transformation schemas of R-Maple. The other three are: bfindsp, bfindps, bfindpp. The prefix of these "opcodes", bfind, indicates that these are for backward find. All have the syntax of the form: b f i n d a i n ( V a r : = E x p r a n d P r o g i ) o r P r o g 2 P r o g j and P r o g 2 are R-Maple programs and b f i n d must be one of bfindss, bfindsp, bfindps, or bfindpp. The postfix "ss", "sp", "ps", and "pp" are used when the find is finally discharged. They are used to indicate whether the a n d and o r are sequential or parallel, "ss" indicates that both a n d and o r are sequential operations, "sp" indicates that a n d is sequential and o r is parallel, while "ps" indicates that a n d is parallel and o r is sequential, and "pp" indicates that both a n d and o r are parallel operations. Their use is apparent in the Section 3.2 Transformation as Computation .. 19 transformation schemas presented in Appendix C. These transfromation schemas indicate how the postfix of bfind is changed so that information about the sequential or parallel boolean operations on the move backwards may be preserved. Also, in some cases, a new process may be started to preserve the meaning of parallel boolean operations. So far, nothing has been said about a. a is a list of variables. Initially, when Return is invoked, a is empty. During the backward move, the value of a variable x may be moved back through a find on a different variable y. In this case, y will be added to the list of a. The rewriting continues until the program is transformed into the form where no rewriting rules are applicable. This can either fail to terminate, ter-minate normally (in the form T !), or remain deadlocked. It should be noted that the executing machine is not a full theorem prover and that if the program never terminates, it does not mean that the original program was not a theorem. (For instance, the earlier example : P; 5>7 will never terminate if P does not ter-minate although the declarative reading of the formula is false. But since the sequential conjunction ; is used, the executing machine will try to compute P before starting to compute 5>7 and therefore the whole program will never ter-minate.) It should be noted that computations of R-Maple are invariant to the declarative reading of programs. This is because each rewriting rule is justified by a logical tautology. For example, computations for tests employ the truth tables of logical and the moving back of a value for a variable to its corresponding Section 3.2 Transformation as Computation .. 20 "find" is possible because of the tautologies: ly ( x = a & A V ly {x = a & {A & C ) V (B Be C )} ly {x = a Si A M B)\l C ^ ly {x — a SL A M (B V C )}. provided y does not occur in C. If y occurs in C, it must be systematically changed to a different variable. There are no rewriting rules for guiding an assignment through a negation. This is because there is no good declarative reading for such a transformation. A program that attempts this will result in a deadlock. Moreover, there is no need for this in logic programs as the practice of Prolog confirms. By the employment of logical connectives, the use of explicit quantifiers ( find ) coupled with the use of if statements, all the cuts and commits of Prologs can be eliminated. Moreover, a wide scale of control behaviours is possible without compromising the declarative reading of programs [Voda & Yu 84]. 3 . 3 . Abstract Syntax of R-Maple Programs written in concrete syntax are compiled into abstract syntax. Abstract R-Maple programs are directly interpreted on the R-Maple machine. The following is a summary of the formation rules for abstract R-Maple pro-grams. They are slightly different from that described originally in [Voda 83] and this syntax is recognized by the currently implemented R-Maple interpreter. Meta-variables which are syntactic variables ranging over terms, are used in the description of the formation rules. The following syntactic variables will be used. Section 3.3 Abstract Syntax of R-Maple 21 N u m l N u r a 1 , N u m 2 , • • • to range over numerals L i t , L i t i , L i t 2 , • • • to range over literals V a r , V a r 1 , V a r 2 , • • • to range over program variables P r e d , P r e d 1 , P r e d 2 , • • • to range over program predicates E x p r , E x p r j , E x p r 2 , • • • to range over expressions P r o g , P r o g j , P r o g 2 , • • • to range over programs Syntactic variables are used in the standard way of logic and they should not be confused with non-terminals of context-free grammars. Syntactic variables of the same kind, but with different subscripts, range over their domains independently. Two or more occurrences of the same syntactic variable in a schema have to be replaced by the same sequence of symbols. Formation rule for program variables: <. varop , N u r n > is a program variable. Formation rule for program predicates: <predop , N u m > is a program predicate. Formation rules for expressions: a) <quoteop , L i t > and V a r , are expressions. b) If E x p r j and E x p r 2 are not both quoted then <pairop , E x p r 1 , E x p r 2 > is an expression. An expression is quoted if it is of the form < quoteop , L i t > . An expression is consed if it is of the form <pairop , E x p r j , E x p r 2 > . Formation rules for programs: <trueop ,nil >, </alseop ,nil >, <attrop ,predop , N u m , E x p r > , <ifop , P r o g , , P r o g 2 , P r o g 3 > , < / i n d o p ,varop , N u m , P r o g > , <.splitcp ,varop ,Nnml,varop , N u m 2 , E x p r , P r o g > , <orsop ,Prog!,Prog2>, <orpop , P r o g j , P r o g 2 > , < andsop , P r o g j , P r o g 2 > , < andpop , P r o g ! , P r o g 2 > , < not op , P r o g > , <def op ,predop , N u m , , v a r o p , N u m 2 , P r o g > are programs. The formation rules for the last group of operators in R-Maple are: Section 3.3 Abstract Syntax of R-Maple .. 22 <wheress , a , V a r , E x p r , P r o g 1 , P r o g 2 > !, <wheresp , a r , V a r , E x p r , P r o g 1 , P r o g 2 > !, < whereps , a , V a r , E x p r , P r o g j , P r o g 2 > !, < wherepp , a , V a r , E x p r , P r o g j , P r o g 2 > ! . This last group of operators are called processes or program-counters. They indi-cate where in the program transformation takes place. These operators are con-structed by the executing machine and are not used in the translation from con-crete syntax to abstract syntax. Their use is equivalent to the bfind operator described in the transformation schema in the last section. More will be dis-cussed on this latter. The symbol ! is used to denote a process in execution. Thus, P! indicates that there is a process executing the program P. Since wheress , wheresp , whereps , and wherepp denote a processes in execution, the symbol ! is included in their formation rules. Each formation rule is delimited by the angle brackets (although in the actual input to the R-Maple interpreter, they are not used). The keyword that follows each open angle bracket < can be thought of as an opcode for the R-Maple machine and the rest being the argu-ments for the opcode. Hence, in the following discussion, the terms "keyword" and "opcode" will be used interchangeably. As can be seen in the formation rules for the abstract syntax of R-Maple, it is closely related to the concrete syntax. For each variable used in a R-Maple program, it is translated to the abstract form of <varop ,Num>. Two or more occurrences of the same variable in the same context are translated with the same value for Num. Similarly, program predicates are translated to the abstract form of <predop ,Num>. The abstract syntax for a literal is < quoteop , L i t > . Thus, the numeral Section 3.3 Abstract Syntax of R-Maple .. 23 672 is represented in the system as <quoteop ,672>. Since a literal is an expres-sion, < quoteop ,Lit> is said to be a quoted expression. Given two expressions Expr-j, Expr 2 which are not both quoted, then <.pairop ,Expr 1Expr 2> is an expression. This concept is slightly modified in the following discussion and in the implementation of R-Maple. Pairop is used also in pairing two quoted literals as well as non-quoted literals. That is, no matter what Expr x and Expr 2 stand for, <pairop jExpr^Expr^ is also an expression. This corresponds to [ Expr 1 (Expr 2 ] in the concrete syntax. An expression of the form <pairop,Expr! Expr 2> is. referred to as a consed expression in R-Maple abstract syntax. The concept of consed and quoted expressions corresponds to the consed and quoted S-expressions in LISP. Note that the modified pairop con-struct resembles closely to the cosed expression in LISP. A list is represented in R-Maple using the pairop operation. All lists are represented as pairs of sub-lists. A list must be terminated by the literal nil at the end. This is slightly modified in the implementation since a 0 is used instead to indicate end of a list. For example, the list [ 1,2,3,4,0 ] is taken as [ 1,[ 2,[ 3,[ 4,0 ] ] ] ] and is represented in abstract R-Maple syntax as : <.pairop ,<quoteop ,1>,<pairop ,<quoteop ,2>,<pairop ,<.quoteop ,3>, <Cpairop ,<quoteop ,4>,<quoteop ,0>>>>>. Since R-Maple is a logic programming language, every formula to be proved is to be reduced to either true or false. Therefore, the system provides the pro-grams <trueop ,nil >, and </alseop ,nil >. <attrop ,predop ,Num,Expr> is translated from a call to a predicate where Num is the unique value assigned to the predicate when it was defined and Expr is the argument to the predicate. Section 3.3 Abstract Syntax of R-Maple .. 24 E x p r may be a consed or a quoted expression. The former allows more than one input arguments to be passed into the predicate program. For example, if the predicate expects two input arguments and one output arguments, then passing the actual input arguments of the numbers 53 and 63 and the output argument of < varop ,33 > calls for an expression of the form: <pairop ,<pairop ,<quoteop 53> , <quoteop 63>>,<varop , 33>>. The if-then-else concrete syntax of R-Maple is translated to <«'/ op , P r o g j P r o g 2 P r o g 3 > where P r o g j is a test to be reduced to true or false. If true, P r o g 2 will be executed, else P r o g 3 will be executed. The find statement is translated to </indop ,varop , N u m , P r o g > where Num is the number assigned to the output variable and which is to be "found" in the program P r o g . As can be seen, this is a direct translation of the find statement in concrete syntax to the abstract syntax. The other form for find where an expression can be split into two of its constituents such as: find [ hd | tl ] = a i n P r o g has its corresponding abstract syntax as: <splitop ,varop ,Y&Thvarop , V a r 2 , E x p r , P r o g > where E x p r must be a consed expression. E x p r will be split into two expres-sions. The head will be bound to V a r j and the tail will be bound to V a r 2 -These variables can then be used in the evaluation of the program Prog. The sequential and parallel conjunctive and disjunctive constructs of R-Maple are translated to <andsop , P r o g j P r o g 2 > , <andpop , P r o g 1 P r o g 2 > , < orsop , P r o g ! P r o g 2 > , <orpop , P r o g j P r o g 2 > where andsop indicates a Section 3.3 Abstract Syntax of R-Maple .. 25 sequential and, andpop indicates a parallel and, orsop indicates a sequential or, and finally, orpop indicates a parallel or. P r o g 1 and P r o g 2 are to be reduced to true and false (if possible) to allow the boolean comparison to proceed. The last boolean operation is the negation operation. Its abstract syntax is of the form <notop , P r o g ! > . User defined predicates in R-Maple is translated into abstract syntax of the form < def op ,predop ,T^umhvarop , N u m 2 , P r o g > . N u m j is assigned by the translator from concrete syntax to abstract syntax to give the predicate a unique number so that the predicate body can be invoked later. N u m 2 is the number assigned to the variable used as the argument in the program body P r o g . As seen in the presentation of the concrete syntax of R-Maple, this does not restrict the user to define predicates using only one argument since multiple arguments may be retrieved from the formal argument variable by the "split" operation in the body of the program P r o g . For example: <Cdef op ,predop ,45,varop ,3,<spIitop ,varop ,l,varop ,2,varop ,3,....,>> This predicate can then be invoked, say, with the arguments: <pairop ,<quoteop ,123>,<quoteop ,432>>. The rest of the formation rules for the abstract syntax of R-Maple including wheress , wheresp , whereps , and wherepp are used for returning values assigned to variables during the execution of the program. They are not used in the trans-lation of R-Maple programs from concrete syntax to abstract syntax. All have the syntax of the form: < w h e r e , a , V a r , E x p r , P r o g j , P r o g 2 > Section 3.3 Abstract Syntax of R-Maple ..26 where must be one of wheress , wheresp , whereps , or wherepp . Since the user never generates code using the formation rules for processes, there is no direct corresponding concrete syntax to the abstract syntax of where . However, in the discussion for backward move of a value to its corresponding find , the bfind operator was introduced in the transformation schema. This is, in essence, the corresponding concrete syntax for the abstract syntax of where . The terms bfind and where will be used interchangeably for the rest of the discussion. Usually, when the term bfind is used, the transformation schemas are being referred to, whereas when the term where is used, the abstract syntax is being referred to. Appendix D summarizes the formation rules of the abstract syntax discussed so far by showing the equivalence between the abstract syntax and their semantics in first order logic. The meaning component of an abstract program will be given by a naming function denoted by "*" which is defined on the domain of abstract program. Thus the intended meaning of a program -4 is the meaning of the for-mula A * . Chapter 4 Implementation of R-Maple 4. Implementation of R-Maple R-Maple was written in C and runs under the Unix f operating system Ver-sion 7. The basic operations of the R-Maple machine are 1) accept input in abstract syntax, 2) build a binary tree structure based on the input, 3) manipu-late the tree by transforming it according to the transformation rules discussed in Section 3.2. Each of these operations will be described in more details in the fol-lowing sections. First, the data structures used in the implementation will be dis-cussed. 4.1. Data Structure The binary tree to be constructed is stored in an array [1, max_storage_sizeJ of records where max_storage_size is currently 2000. Each record, containing 7 fields, is used to represent a node. Since the tree to be constructed is a binary tree, there are two main fields in each record which store the data value for the left and right branch of a node. Their field names are head_value and tail_value. A node may contain the address of another node or a data value. Therefore, a bit is used to indicate for each of these two fields, head_value and tail_value, whether the content is a pointer or a data value. These are the fields is_ptr_in_head and ptr_is_in_tail. They are set to 1 if the head_value or the tail_value is a pointer, and 0 if it is a data value which can either be an opcode, f Unix is a trademark o f Bell Laboratories. Section 4.1 Data Structure .. 28 a numeral, etc.. or a data value. Each node has also a field to indicate which process is currently executing the node. The field is referred to as ex_proc. Processes will be discussed next. A backward pointer, backward_ptr, is also included in the record for pointing at a parent node in the tree. Its use will become apparent later. The structure of each node is represented in C as: struct cell { unsigned is_ptr_in_head :1; unsigned ptr_is_in_tail :1; int exjproc ; int head_value; int tail_value; int backwardjptr; } Appendix E shows the basic tree structures that will be constructed correspond-ing to each formation rules of the abstract syntax of R-Maple. Only the fields head_value and tail_value are shown. Once the tree is constructed, a process is assigned to transform the tree starting at the root until it is reduced to true or false. As will be seen later, exe-cution of the abstract program is equivalent to the transformation of the tree structure. Therefore, the terms "execution" and "transformation" will be used interchangeably for the rest of this discussion. A process may be required to traverse down the tree to reduce a subtree before further transformation of the entire tree may proceed. Information about which part of the tree a process is executing and its status are stored in a process control block (PCB). Each pro-cess has its own PCB. The data structure for the process contains also 7 fields. These include 4 boolean flags which indicate whether the process is unassigned, Section 4.1 Data Structure .. 29 running, suspended, or finished. The use of these flags will be explained in the section on Processes (Section 4.4). The data structure for a process control block is encoded in C as follows. struct process_control_block { unsigned unassigned :1; unsigned running :1; unsigned suspended :1; unsigned finished :1; int b!ock_process; int procjroot; int progjmark; } 4.2. Construction of the R-Maple Tree The input function of the interpreter has two main subfunctions: 1) to ensure that the abstract syntax is correct, and 2) to build the tree structure. A one-symbol-look-ahead parser is used to analyse the input. At the top entry level to the parser, a program or a definition of a predicate is expected. A program can be recognized by the first keyword which must be one of trueop , / alseop, attrop , andsop , andpop , orsop , orpop , notop , if op , f indop , and splitop . A definition can be recognized by the keyword defop. Once the keyword is recog-nized, the parser can recursively call itself to parse the rest of the input whenever the parser expects a sub-program, (eg. <i/op ,Progx Prog 2Prog 3>), or it can call another procedure to parse a variable or an expression etc.. The abstract program can span several input lines and must be terminated by a period. The binary tree is built through a call to a procedure to allocate a cell and then filling the cell with appropriate information. In many cases, the head value Section 4.2 Construction of the R-Maple Tree .. 30 contains the data and the tail value contains a pointer. For example, <quoteop ,3> is represented as: A nil pointer is represented by setting the bit is_ptr_in_head or ptr_is_in_tail (depending on whether it is the head or the tail that contains the nil pointer) to 1. The contents for head_value or the tail_value will then contain the value -1. In some cases when both the head value and tail value are pointers to other nodes, the two bits is_ptr_in_hea.d and ptr_is_in_tail are both set to 1. 4.3. Transformation of the R-Maple Tree Once the tree is constructed, a process is assigned to the root of the tree. The field procjroot and prog_mark are updated with the address of the root node. Execution of a R-Maple tree is equivalent to the transformation of the tree structure based on the transformation schema described in section 3.2. Hence, computation of R-Maple programs reduces to a sequence of pruning the tree, modifying the structure, copying parts of the tree etc.. As will be seen clearer in Chapter 7, the transformations of a TRF-Maple tree which is similar in concept as the transformations of a R-Maple tree is not only a syntactic manipulation but they are also semantically correct. quoteop y Section 4.4 Processes .. 31 4.4. Proceses A process can be in any one of four states. It can be either unassigned, run-ning, suspended, or finished. A process that is unassigned is an idle process. It is ready to be assigned for the execution of any parts of a tree structure. Initially, all processes are unassigned. A process is running when it is already assigned a subtree to be executed and there is a processor assigned to the process. The corresponding PCB field is set to 1 when the process is selected to start the exe-cution by a processor. It is reset to 0 when the process is blocked and another process starts its execution. Each process is allowed to continue to execute until one of the following conditions is encountered. In this case, the process is said to be suspended (or blocked). This allows a fair distribution of the use of the pro-cessors to each process. A process is suspended when 1) the process needs to traverse to one of the child nodes to execute a subtree. In this case, the pointer to the current tree node (prog_mark) is changed to point to the child node. The backward pointer of the child node is updated to point to the current node. The process is then stopped temporarily for other processes to proceed. 2) A process can be stopped when the current process is explicitly blocked by another process. An example is in the execution of andpop or orpop. The process executing at either of these nodes will be blocked while two new processes will be assigned to execute the left and right subtree in parallel. Execution of the parent process will resume when one of the child processes is finished. 3) When there is insufficient data for further processing, the process will also be stopped. This may happen during a comparison test such as x > 5 where x is still a variable. Such situation occurs when there is a parallel process to assign x a value. In this case, the Section 4.4 Processes .. 32 process executing x >5 will not be able to proceed until the assignment is made. In this case, no change is made to the PCB for this process. A process is suspended (or blocked) when at least one other process must execute to comple-tion before the process may assume execution. Finally, a process is finished when it has succeeded to reduce a subtree to either true or false. The node or the root of the subtree where each process is originally assigned to execute is stored in the field proc_root of the PCB. This iield is used to ter-minate the process later if the finished flag is set and the process is currently pointing at the root. Another field prog_mark is used to store the node in the tree structure where the process is currently manipulating. The value in prog_mark is changed whenever the process needs to traverse up or down the tree. This field is checked to see if it is equal to proc_root when the finished flag is set. If they are equal, this process will be terminated as mentioned above. The last field block_process is used to store the process number that is blocked by the current process. The blocked (or suspended) process will be reactivated when the current process is finished and terminated. When a process reduces a subtree to either true or false, or when the predi-cate Return is invoked, it begins an upward traversal back towards the root of the tree where it was originally being activated. This is achieved by tracing the pointer stored in the field backward_ptr. Further transformations and backward move continues until the process reaches its root whereupon it is terminated and become unassigned. There are two cases when a backward move of a process is invoked. One is when a process successfully transformed a subtree to true or Section 4.4 Processes .. 33 false. The second case is when the predicate Return is invoked. In both cases, a backward move of the process will begin. Processes are assigned as specified in the transformation schema. There is a master process which continually monitors the status of the processes. When a process terminates execution, the rest of the processes are scanned to see if any of them may resume execution. Execution may result in a deadlock v/hen all processes are not able to transform their subtrees. An example is : find x in x > 5 || print (x). In this case, the processes are waiting for the assignment of a value to the vari-able x. The result is that each process will keep on trying to transform the tree but with no avail. Processes can be killed by other processes. Hence, even if a process goes into deadlock forever, another process may kill the process thus allowing the whole program to finish. For example: find z in print (x ) orp T => find x in print (x ) ! orp T ! => find x in T\ => Tl Also, processes are killed or terminated when subtrees are deallocated. In the above example, if x is assigned a value eventually, the subtree for print (x ) is deallocated because of the transformation schema: Prog ! orp T ! => T ! Hence, the process executing print (x ) is terminated. When copying subtrees, the processes in the subtree are also copied. This means that new processes are created for the new subtree. For example, during the backward move of the Section 4.4 Processes ..34 where node to an andpop node, both the subtrees branching from the andpop node contains processes. Therefore, during the transformation, the branch that is copied must also have new processes created for the copied structure. This is achieved by scanning the new subtree with the original subtree in parallel, and assigning new processes to the new subtree whenever a process is found in the original subtree. During a backward move of a process, there might be occasions when, at the same time, a forward process executing the same part of the subtree is encoun-tered. In those cases, care must be taken that nodes are not accidentally deleted so that the other process may not be able to proceed. 4.5. Backward Movement of a Process When a subtree is reduced to true or false, the process traces the backward pointer to its parent node. In the case where the parent node is andpop or orpop where two processes were created, the transformation schemas call for a deletion of one of the branches. For example: the transformation schema T\ j| Prog! ! => Prog! ! collapses the tree structure to the structure of Prog! only. Also, the process that was executing Progj will be terminated and Progj will be reassigned the process executing its parent node. Once Prog! is reduced to trueop or / alseop , the process will again move backward until its root has been reached. A process may also move backwards when the predicate Return is invoked. Execution of the predicate Return may result in a deadlock if the variable to be Section 4.5 Backward Movement of a Process .. 35 assigned also exists in the expression at the same time. For example: x:—\ [ [ 1,2 ],3 ],x ] results in a deadlock. Therefore, the expression to be assigned to the variable must be ensured that it does not contain the variable. This is achieved by a simple recursive procedure which traverses the structure of the expression to make sure that the variable is not contained in it. If the vari-able does not occur in the expression, the tree structure for the invocation of the predicate Return is modified to the tree structure of wheress as follows. whereas / varop The process executing the wheress node will automatically traverse backward. The only allowable nodes that the backward traversal may encounter are the sequential and parallel and's and or's, and the find nodes. No other nodes are allowed to be in the backward traversal path. This implies that the R-Maple program: n o t x :=4; P r o g Section 4.5 Backward Movement of a Process .. 38 is illegal since Return cannot pass through a notop node. This restriction is valid because there is no good declarative reading for such a transformation. The transformaion schemas described in Appendix C indicates that all resulting struc-tures after the transformation results in having the b f i n d opcode. 4.6. Free a n d B o u n d V a r i a b l e s Attention must be given to the free and bound variables in several instances. Most of them are related in the replacement of an expression to a variable. This may occur during the invocation of a user defined predicate or when the predi-cate Return is being invoked and the process is about to discharge the find node. The other instances occur during the execution of the where node. Each will be discussed in detail. When a user defines a predicate of the form <def op ,predop ,Nnml,varop ,Num2,Prog>, the predicate is assigned a unique numeric value for Num of 25 or over. All predicates defined by the system such as addition, subtraction, etc. are assigned numeric values of less than 25. This allows the interpreter to distinguish whether a call is made to a system defined predicate or user defined predicate. This dis-tinguishing between system predicate and user defined predicates is necessary because when a user defined predicate is invoked, the R-Maple machine loads the body of the predicate from the system so that execution may proceed, whereas when a system predicate is invoked, no copying of any predicate body is made. Execution of a system predicate is immediate. That is, for example, invoking the Section 4.6 Free and Bound Variables ..37 test for equality system predicate "Eq", the system checks for the operands sup-plied along with the invocation and the test is done immediately. The tree structure for the body of the user defined predicate is stored in the system. The structure of Prog serves as a master copy of the body of the predi-cate. When the predicate is invoked, the body is copied to a working area so that the tree may be executed. The address for the root node of the body is stored in an array called predicate_info where the predicate number, Num!, is used as an index to it. The variable number, Num2, is stored in another array called pred_output_var with the predicate number, Numt, also being used as an index. When the predicate is invoked by a call such as < altrop ,predop ,Num1,Expr>, the location of the master copy of the body of the predicate is retrieved by searching the array predicate_info using the predi-cate number as index. The variable number for the argument is also retrieved from the array pred_output_var. The body of the predicate is then copied to a new location. The input argument, Expr, is assigned to the argument variable of the predicate. That is, for each occurence of <varop,Num2>, it will be replace by a copy of the input expression Expr. This is in accordance with the transformation schema for the definition of predicates and the invocation of predicates in section 3.2. Hence, assigning an expression to a variable is equivalent to replacing the nodes for the variable by a copy of the expression. When assigning expressions to a variable in a tree structure, it is important that the variables that are free in an expression do not become bound after the expres-sion is substituted in the tree structure. For example, Section 4.6 Free and Bound Variables .. 38 (find y in x ) {x := .. y ..} should not result in the variable y being bound. In order to ensure this, the expression is first scanned to obtain a list of all the free variables in it. Then in the process of replacing the variables in the body of the predicate by the expres-sion, whenever a find node is encountered and the variable that follows the find node is one of the free variables in the expression, all occurrences of that variable will be replaced by another variable in the subtree starting at the node where the find node occurs. Hence, for the above example, the tree structure is changed to: (find yy in x ) {ar:= .. y ..} Now the replacement of x may proceed to obtain: (find yy in y ). Variables are not replaced in a tree structure if the parent node is a find node even if the variable that follows is the same as the variable to be replaced. That is no substitution is made for (find x in x ) {x .= .. y ..} because the x which follows the find is a bound variable for its body. Hence no substitution is necessary for the entire subtree. Replacement of this kind also occurs during a backward movement of a process upon invocation of the predi-cate Return . Replacement of the variable takes place when the backward move-ment reaches the corresponding find node whereupon, the find node is discharged. Refer to the transformation schema in Appendix C for more details. Another instance when free and bound variables require special attention is during the backward move of bf indss, bfindsp, bfindps, and bf indpp when Section 4.6 Free and Bound Variables ..39 either an andsop or an andpop is encountered. In this case, the and structure is collapsed into a where structure. The transformation schema for bfind is shown below. Variables that are free in Prog 3 but are bound in a must have their occurences changed in Expr and Prog^ Otherwise, the free variable in Prog 3 will be taken as bound variables after the transformation since the vari-ables in a are going to be discharged eventually in a find node. The transfor-mation schema for a bfind construct with an and node as its parent node is shown below. The structure : {bfind a in [ ( m :=Expr ) and Progj ] or Prog2} and Prog 3 is transformed to: bfind a in { [ ( m :=Expr ) and ( Prog! and Prog 3) ] or ( Prog 2 and Prog 3) } An example where care must be given to free and bound variables is when a structure like the following occurs. {bfind z in [ { rn :=Ezpr ) and ( trueop end z:=1 ) ] or Progj } and a :=z + 1 In the expression, a :=z + 1, the z is bound to a find which is a parent of the and. If the structure is transformed according to the transformation schema without paying any attention to the binding of variables, the tree structure will become: bfind z in { ( m:=Ezpr ) and ( z:—l and a :=z 4- 1 ) } or Prog! Note that the expression z :=1 has the variable z bound to a find that is already encountered during the backward move. This is indicated by the pres-ence of z in the a list of where . Now, when the find node for tn is finally Section 4.6 Free and Bound Variables .. 40 reached, the find node will be discharged and the variables in a wll be put into a new find node. The resulting structure is: find z in z :=1 and a:=z + 1 Notice that inconsistency arises for the binding of the variable z in a:—z + 1. To ensure that the variables are correctly bound, variables that are free in the branch Prog 3 in Figure 1 but are bound in a must have their occurrences changed consistently to another variable in Expr and Progj. For the above example, the correct transformation should be: {bfind zz in [ ( m:—Expr ) and ( true and zz.—l ) ] orProgj} and a :=z + 1 which will eventually be transformed to as: find zz in zz \ — \ and a :—z +1 4.7. Hardware Consideration The R-Maple interpreter was originally developed on a PDP 11/23 machine running Unix f. Due to the slowness of the processor, the interpreter was ported to an Amdahl V8 running the MTS operating system. However, the compiler on the Amdahl machine could only handle data structure with a maximum size of 8K. The array which stores the tree structure of a R-Maple program exceeds this limitation. The development of the interpreter was finally ported to a VAX 11 / 780. Since the interpreter was written in C, there was relatively no problem in porting from one machine to another. All the above machines are uniprocessor systems. Therefore, the "processes" that are created during the execution of a t U n i x is a t r a d e m a r k of B e l l L a b o r a t o r i e s . Section 4.7 Hardware Consideration .. 41 R-Maple program needs to share the same processor. This implementation of R-Maple was mainly to test out the feasibility of computation based on the rewrit-ing rules as described earlier. No attempt is made in improving the efficiencies of the interpreter. 4.8. Examples of R-Maple Abstract Program The following is a series of R-Maple programs written in concrete and abstract syntax, the latter of which can be executed by the interpreter. The first example is a demonstration of the use of parallel processes. The program basi-cally tests whether the variable <varop ,1> is greater than 10 when at the same time, it tries to assign to it various values. The program backtracks when the value assigned is not greater than 10. The corresponding concrete syntax is as follows : find x in (x > 10 || {x :=3 orp x :=8 orp x :=88)); print (x ) The abstract program that is accepted by the R-Maple interpreter is as follows: findop varop 1 andsop andpop attrop predop 5 pairop varop 1 quoteop 10 orpop attrop predop 8 pairop varop 1 quoteop 3 orpop attrop predop 8 pairop varop 1 quoteop 8 attrop predop 8 pairop varop 1 quoteop 88 attrop predop 7 varop 1. The output of this program is: 88 Section 4.8 Examples of R-Maple Abstract Program 42 The next example is a program to append two lists. This demonstrates the use of the splitop operation. The predicate is assigned a predicate number of 30. The concrete syntax is as follows (predicate name "Append" and variable names are used in the presentation instead of the use of predicate number and variable numbers.): Append (argument) is find [1st ,result ] = argument in find [ 1st l,lst 2 ] = 1st in if 1st 1 = nil then result :— 1st 2 else find [ hd ,tl ] = 1st 1 in find re3 1 in Append {{[ tl ,lst 2 ]res 1 ]); result ;=\hd,resl] The abstract syntax is : defop predop 30 varop 1 splitop varop 2 varop 3 varop 1 splitop varop 4 varop 5 varop 2 ifop attrop predop 1 pairop varop 4 quoteop 0 attrop predop 8 pairop varop 3 varop 5 splitop varop 6 varop 7 varop 4 findop varop 8 andsop attrop predop 30 pairop pairop varop 7 varop 5 varop 8 attrop predop 8 pairop varop 3 pairop varop 6 varop 8. The predicate can be invoked in a program of the form: find x in Append ([ [ 4,1,0 ], [ 2,0 ],x ]); print (ar). The corresponding abstract syntax is : findop varop 10 andsop attrop predop 30 pairop pairop pairop quoteop 4 pairop quoteop 1 quoteop 0 pairop quoteop 2 quoteop 0 varop 10 attrop predop 7 varop 10. The output is as follows: [ 4 , ( 1 , [ 2 , 0 ] ] ] Section 4.8 Examples of R-Maple Abstract Program .. 43 The third example is a program that computes the Fibonacci Sequence. The predicate takes in an input argument specifying the nth Fibonacci number. The concrete syntax is shown below: Fib (x ) is find [ in ,n ] = x in if m — 0 then n :=2 else if tn = 1 then n :=3 else find p in p :=m - 1; find q in q :=m - 2; find r in Fib ([ p ,r ]); find s in Fib ([ g ,s ]); find J in £ :=r + s ; n:=r That is, given a number n, if n = 0, its Fibonacci number is 2, if n = 1, then its Fibonacci number is 3. Otherwise, the Fibonacci number of n is equal to the sum of the Fibonacci number of n -1 and n -2. The abstract program is as fol-lows. defop predop 30 varop 1 splitop varop 2 varop 3 varop 1 ifop attrop predop 1 pairop varop 2 quoteop 0 attrop predop 8 pairop varop 3 quoteop 2 ifop attrop predop 1 pairop varop 2 quoteop 1 attrop predop 8 pairop varop 3 quoteop 3 findop varop 4 andsop attrop predop 10 pairop pairop varop 2 quoteop 1 varop 4 findop varop 5 andsop attrop predop 10 pairop pairop varop 2 quoteop 2 varop 5 findop varop 6 andsop attrop predop 30 pairop varop 4 varop 6 findop varop 7 andsop attrop predop 30 pairop varop 5 varop 7 findop varop 8 andsop attrop predop 9 pairop pairop varop 6 varop 7 varop 8 attrop predop 8 pairop varop 3 varop 8. The predicate can be invoked as in the following program : find x in Fib ([ 5,x ]); print (x). The abstract program is translated as : findop varop 9 andsop attrop predop 30 pairop quoteop 5 varop 9 attrop predop 7 varop 9. The output is : Section 4.8 Examples of R-Maple Abstract Program 44 21 Although the above example does the job of computing the Fibonacci number, it requires double exponential time. A more efficient implementation can be as fol-lows: Fib (y ) is find [input,output ] = y find [x,restl] = input in find [max,rest2] = rest 1 in find [slast ,last ] = rest 2 in if x = 0 then output :=slast else if x = max then output :=last else find n in n :=slast + last; find /Ti in fn :=max -f- 1; find p in Fib ([ [ x ,m ,last ,n ],p ]); output :—p This program computes the Fibonacci number by computing the Fibonacci sequence and storing the last two Fibonacci numbers found. The last Fibonacci number found is checked to see if it is the Ficonacci number required. Basically, the predicate is called with 4 input arguments and 1 output argument. The argument x is the nth Fibonacci number to be computed, slast and last are the last two Fibonacci number found. 7?iax indicates that last is the mth Fibonacci number generated and if max is equal to x then the program returns the result in last. The abstract syntax is as follows: defop predop 30 varop 12 splitop varop 6 varop 5 varop 12 splitop varop 1 varop 8 varop 6 splitop varop 2 varop 9 varop 8 splitop varop 3 varop 4 varop 9 ifop attrop predop 1 pairop varop 1 quoteop 0 attrop predop 8 pairop varop 5 varop 3 ifop attrop predop 1 pairop varop 1 varop 2 attrop Section 4.8 Examples of R-Maple Abstract Program 45 predop 8 pairop varop 5 varop 4 findop varop 10 andsop attrop predop 9 pairop pairop varop 3 varop 4 varop 10 findop varop 11 andsop attrop predop 9 pairop pairop varop 2 quoteop 1 varop 11 findop varop 13 andsop attrop predop 30 pairop pairop varop 1 pairop varop 11 pairop varop 4 varop 10 varop 13 attrop predop 8 pairop varop 5 varop 13. The program can be invoked by the following statement: find x in Fib ([[5,1,2,3],* ]); print {x ) It will compute the fifth Fibonacci number where the first two Fibonacci numbers are 2 and 3. The 1 in the input argument specifies that the maximum Fibonacci number known so far is the first one, namely 3. The abstract syntax is as fol-lows: findop varop 1 andsop attrop predop 30 pairop pairop quoteop 5 pairop quoteop 1 pairop quoteop 2 quoteop 3 varop 1 attrop predop 7 varop 1. The output is the same as that shown in the last implementation. The next example is another example to show the backtracking feature of R-Maple. It takes in an initial value as input and then it keeps on generating integers starting at the initial value until the resulting value is equal to 11. The program in concrete syntax is: Gen (x ) is ( print (x ); x — 11 ) or find y in y :=x + 1 ; Gen (y ). The abstract program is : defop predop 30 varop 1 orsop andsop attrop predop 7 varop 1 attrop predop 1 pairop varop 1 quoteop 11 findop varop 2 andsop attrop predop 9 pairop pairop varop 1 quoteop 1 varop 2 attrop predop 30 varop 2. The predicate can be simply invoked by the abstract program: attrop predop 30 quoteop 1. The result is : Section 4.8 Examples of R-Maple Abstract Program 46 1 2 11 The final example is a program that performs the quicksort algorithm. Two predicates are defined. One is used to partition a list into two lists such that all the elements of the first list is less than the elements of the second list. The second predicate is used to append an unsorted list to a sorted list to produce the final sorted list. Therefore to sort an unsorted list, the call is to append the unsorted list to a nil sorted list to produce the sorted list. The concrete syntax of the predicate to partition two lists is presented first. partition (ar ) is Section 4.8 Examples of R-Maple Abstract Program 47 find [ input ,res ] = x in find [ 1st ,num ] = input in if 1st = nil then res :=[ 0,0 ] else find [ hd ,tl ] — 1st in find r in partition ([ [ tl ,num ],r ]); find [ 5 ,/ ] = r in if num < Arf then res :=[ 3 ,[ hd ,1 ] ] else res :=[ [ ],/ ] The abstract syntax for the predicate partition is as follows: defop predop 30 varop 1 splitop varop 2 varop 3 varop 1 splitop varop 4 varop 5 varop 2 ifop attrop predop 1 pairop varop 4 quoteop 0 attrop predop 8 pairop varop 3 pairop quoteop 0 quoteop 0 splitop varop 6 varop 7 varop 4 findop varop 8 andsop attrop predop 30 pairop pairop varop 7 varop 5 varop 8 splitop varop 9 varop 10 varop 8 ifop attrop predop 3 pairop varop 5 varop 6 attrop predop 8 pairop varop 3 pairop varop 9 pairop varop 6 varop 10 attrop predop 8 pairop varop 3 pairop pairop varop 6 varop 9 varop 10. The concrete syntax for the append is shown below : append (x ) is find [ input, output ] = x in find [ sorted,unsorted ] — input in if unsorted = nil then output :=sorted else find [ head,tail ] = unsorted in find p in partition ([ [ tail,head ],p ))', find [ s ,1 ] — p in find rn in append ([ [ sorted,I ],m ]) || append ([ [ [ head,m ],s ],sorted ]) Two partitioned sublists s and / are sorted in parallel. This is the speeded ver-sion of quicksort where the concatenation of the two sorted sublists is done on the fly. The abstract program is : defop predop 31 varop 1 splitop varop 2 varop 3 varop 1 splitop varop 4 varop 5 varop 2 ifop attrop predop 1 pairop varop 5 quoteop 0 attrop predop 8 pairop varop 3 varop 4 splitop varop 6 varop 7 varop 5 findop varop 8 andsop attrop predop 30 pairop pairop varop 7 varop 6 varop 8 splitop varop 9 varop 10 varop 8 findop varop 11 andpop attrop predop 31 pairop pairop varop 4 varop 10 varop 11 attrop predop 31 pairop pairop pairop varop 6 varop 11 varop 9 varop 3. Section 4.8 Examples of R-Maple Abstract Program The quicksort program can be invoked as : find x in append ([ [ 0,[ 4,1,2,3,0 ] ],x ]); print (x ). The abstract program is: findop varop 1 andsop attrop predop 31 pairop pairop quoteop 0 pairop quoteop 4 pairop quoteop 3 pairop quoteop 2 pairop quoteop 1 quoteop 0 varop 1 attrop predop 7 varop 1. The output is: [1, [ 2 , ( 3 , [ 4 , 0 ] ] ] ] .. 49 Chapter 5 A Functional and Relational Programming Language S. Motivation For A Functional and Relational Programming; Language R-Maple, as mentioned before, is a logic programming language with relation as its basic object. Hence, it lacks the expressive power of functions. For exam-ple, if a(x) is a function, it can be composed in the arguments of another function or relation such as b(l,a(x)). On the other hand, if "a" is a relation taking one input argument and generating an output value, then the predicate "a" needs to have two arguments such as a (ar | y ) where ar is the input argument and y is the output argument. Composition of relations is not so readily available. It can be achieved, however, by 3 y { a (ar | y ) & b (l,y ) }. Some relations expressed in R-Maple can actually generate a unique result for each input argument. Therefore, in essence, they are functions. The disadvantage of expressing func-tions as relations is that extra information is kept for backtracking purposes which is never used in the case for functions. A purely functional programming language, on the other hand, does not have the non-deterministic characteristic of relations. Therefore, a combination of a functional programming language with a relational programming language can result with the best of the two worlds. R-Maple can be combined with a functional programming language to allow func-tions as basic objects, so that the readability of programs and the speed of execu-tion may be improved. The language RF-Maple is the result of extending the features of a functional programming language called F-Maple to include the Chapter 5 A Functional and Relational Programming Language .. 50 features of R-Maple. The next two sections will describe the language F-Maple followed by the description of RF-Maple. Both of these sections are described in full details in [Voda & Yu 84]. The following is only an abstract from the paper. 5.1. Description of F-Maple F-Maple (F stands for Functional) is a typed language. It provides not only for semantic extensibility, but also for syntactic extensibility. By this, it means that a user is allowed not only to define new types and funcions but also he/she is allowed to design the syntax of the data types and the syntax of a function invocation. Although syntactic extensibility for data types has been explored by various researchers such as [Kand 83] and [Malu 81], F-Maple allows syntactic extensibility for functions as well. Examples in the following will demonstrate the ease of use and the extensibility nature of the language. The basic types of F-Maple are number and string. From these basic types, a user can define new data types by means of generating productions. Generat-ing productions are similar to the productions used in a context free grammar. The left hand side is a non-terminal specifying the name of the new data type. Non-terminals are capitalized while terminals are not. Non-terminals are used to indicate types while terminals, which are used only on the right hand side, contri-bute to the syntax of the data type. The non-terminals on the right hand side specifies what other data types the new data type is composed of. Terminals can be added to express the data type in a relatively readable structure. For exam-ple, the data type of a list of numbers Numlist can be defined as follows: Numlist —> nil Section 5.1 Description of F-Maple 51 Numlist —» head Number and tail Numlist Symbols may be used as terminals in the generating productions. The data type for a complex numbers Complex can be defined as follows: Complex —> Number + Number i The non-terminals occuring on the right hand side of the generating production can be F-Maple basic types or user defined data types. Enumerated types can be defined by productions which do not contain any non-terminals on the right hand side. The type Bool is one example and can be specified by: Bool —*• true Bool —• / alse Parameterized types can be added into F-Maple. This is achieved by adding a parameter to the non-terminal on the left hand side of the generating production. For example, to define a generic type constructor List (T) which is the type for a list whose elements are of type T, the following productions are needed: List (T) —+ nil List (T) -> head T and tail List (T) Note that the definition for List ( Number ) is the same as for Numlist defined earlier. Another example is the generic type constructor for a binary tree whose nodes are of type T, Bin tree (T). It can be defined as follows: Bintree (T) —* empty Bintree (T) —*• node T left Bintree (T) and right Bintree (T) Values of a data type are generated from sentences produced from a non-terminal. For example, a data value of type Numlist is: Section 5.1 Description of F-Maple ..52 head 1 and tail ( head 2 and tail ( head 6 and nil ) ) This denotes a list of numbers containing elements 1, 2, and 6. Parenthesis play a special role in data values in that they improve readability. For this reason, they are not supposed to be used as terminals in the generating productions. Another example of a data value of Complex type is: 42 + 35 i and finally, an example of a data value of a genertic data type Bintree (Number) is: node 5 left (node 2 left empty and right empty ) and right empty It can be seen that the use of grammars in defining data types allows the user to have complete control over the syntax. 5.2. Terms over F-Maple Types Terms over F-Maple types are used to specify functions in F-Maple. Three new kinds of term construct will be introduced. These are called function, case, and variable productions. Each term has a type. Function productions specifies the syntax of the function invocation and the type of the arguments expected. They are distinguished from the generating pro-ductions in that they will be written with => as the produces symbol. Hence, example of function productions may be as follows: Bool => search Bintree (Number ) for Number Numlist => append Numlist after Numlist Non-terminals used on the right hand side specify the types of formal arguments Section 5.2 Terms over F-Maple Types .. 53 while non-terminals on the left hand side specify the type of the function result. Thus, the first function takes two arguments, one of which is a binary tree whose nodes are numbers and the other is a number. The function returns a boolean value. The second function takes two formal arguments both of type Numlist, and the result of the function is also a Numlist. Function productions specify the data types for the function result and its arguments, and also the syntax of the function. Terms which are produced by the function productions in conjunction with the generating productions are transformed in such a way that the final term can be produced only by the generating productions. This implies the final term cannot be further reduced. For example, the term: append nil after ( head 5 + 7 and tail nil ) is produced from the second function production above and the generating pro-duction for Numlist. Computation of F-Maple reduces this term to the basic term: head 12 and tail nil Note that this term cannot be further reduced. The case production is the main term construct used in the definition of the computation rule for functions in F-Maple. Case productions are of the fol-lowing form: S => case T o f o , | S a2 | S an | S where each a,- is called a case label. The case production is legal if and only if the case labels correspond exactly to all the generating productions for the type Section 5.2 Terms over F-Maple Types .. 54 T . The computation rule for append may be specified as follows. append Ls 1 after Ls2 — case Ls 2 of nil | Ls 1 head H and tail T \ head H and tail ( append Ls I after T) The variables Ls 1 and Ls 2 used in the body of append denote the two arguments expected during the invocation of the function. The variables are automatically declared by the addition of two new variable productions which are examples of the third term construct: Numlist => Ls 1 Numlist => Ls 2 Note that variables are also capitalized for readability purposes. When append is invoked, Ls 2 will be bound to the actual argument of type Numlist. Since a Numlist can be nil or can be a structure with head and tail value, the structure of Ls 2 is tested in the case statement. In the case that Ls 2 is a structure with head and tail, the head is given the name H, while the tail is given the name T. These variables can be used in the body of the production of the second case. Two new variables are declared in the second clause of case . Number => H Number => L 5.3. Examples of F-Maple Programs An example of F-Maple program is the searching function of an ordered binary tree: Bool => search Bintree (I") for T Its body can be defined as : Section 5.3 E x a m p l e s of F - M a p l e P r o g r a m s 55 search Tree for Value = case Tree o f empty \ false node V left Lt and right Rt \ case V < Value of true | search Rt for Value false | case Value < V of true | search Lt for Va/ue / a/se | true T h e above d e f i n i t i o n presupposes the c o m p a r i s o n f u n c t i o n s , < , for each concrete t y p e T used. F o r i n s t a n c e , for B i n t r e e ( N u m b e r ) , the f o l l o w i n g p r o d u c t i o n is needed : Bool => Number < Number A n o t h e r example of a F - M a p l e p r o g r a m is a f u n c t i o n to reverse a n u m b e r Numlist => reverse Numlist after Numlist Its body is: reverse L after M = case L of nil | M head H and tail T \ reverse T after (head H and tail M) T h e reversed list of L appended to M is returned when the f u n c t i o n is i n v o k e d . 5.4. C o m p u t a t i o n o f F - M a p l e P r o g r a m s N o a t t e m p t is made to include any explicit c o n t r o l m e c h a n i s m i n F - M a p l e . T h e c o m p u t a t i o n is b y lazy e v a l u a t i o n . O n e p o i n t t h a t needs to be m e n t i o n e d is t h a t the freedom of extending the syntax of d a t a types and terms m a y lead to ambiguous grammars b e i n g Section 5.4 Computation of F-Maple Programs ... 56 introduced into F-Maple. Rather than attempting to parse the basic values or terms, an interactive structure editor is used to prompt the user for the value of the type needed at any moment. The advantage is that this eliminates the need for the user to type in the long descriptive names as terminals because he simply enters the needed value- to the production. 5.5. Description of RF-Maple In combining a functional and relational programming language together, there is a choice of introducing functions in a relational environment, or introduc-ing relations in a functional environment. In the first case, the standard predi-cate logic with functions as terms is obtained. The second case leads to a logic without formulas but only with terms. This kind of logic is called term logic. In the design of RF-Maple, term logic is opted for. The advantage is that no change needs to be made to cater to functions in the new language. Relations are treated as functions with Boolean values. Since functions in a functional pro-gramming language have all of their arguments as input arguments only, rela-tions without output arguments (which is equivalent to tests in R-Maple) can be simply introduced into a functional programming language. An extension needs to be made to a functional programming language, however, to permit Boolean functions with output arguments for those relations which have output argu-ments. The term "generators" will be used for functions with output arguments in RF-Maple. Computations of RF-Maple is similar to the computations of R-Maple and F-Maple. Functions are computed by lazy evaluation of F-Maple and generators Section 5.5 Description of RF-Maple .. 57 by the rewriting rules of R-Maple. It should be noted that generators are slower to compute because of backtracking whereas functions execute without this over-head. RF-Maple has four new constructs in addition to those of F-Maple. These are the parallel and, parallel or, assignment, and find constructs. Conjunction and disjunction can be sequential or parallel. Sequential con-junction and disjunction can be predefined using the case construct as follows: Bool => Bool ; Bool A ; B = case A of true \ B f alse \ f alse and Bool => Bool or Bool A or B = case A of true \ true f alse \ B Parallel conjunction and disjunction can be introduced by two new productions: Bool => Bool || Bool Bool => Bool orp Bool Control will be passed on to the two bodies as is the case in R-Maple. Assignments are of the form : Bool ==> a := T where a is an identifier declared as T => a for any type T. Find productions are of the form : Bool => find a: T in Bool where a is an identifier and T is a type. For each find production, two more pro-ductions are automatically added. These are the variable production T => a Section 5.5 Description of RF-Maple 58 and the assignment production Bool => a:— T . The productions may be used in the body of find . An example of a generator in RF-Maple is: Bool => generate Number from Bintree (Number ) generate X from Tree = case Tree of empty \ f alse node V left Lt and right Rt | X := V or generate X from Lt o r p generate X from Rt All find productions are of the form : Bool = > f i n d a: T i n Bool where a is an identifier and T is a type. For each find production, two more pro-ductions are automatically added. These are the variable production T = > a and the assignment production Bool => a : = T . The productions may be used in the body of find . For example: find X : Number i n generate X from node 2 left node 8 left empty and right empty and right node 5 left empty and right empty ; 7 <X This term reduces to true after one backtrack to obtain the value 8, thus satisfy-ing the test 7 <X. Through the use of all eight productions, one can create arbitrarily compli-cated terms over any user defined types. Section 5.6 Examples of RF-Maple Programs 59 5 . 6 . Examples of RF-Maple Programs An example will be given for the RF-Maple implementation of parallel Quicksort. It is a generator of type Bool. Bool => sort Numlist into Numlist sort II into 01 — append already sorted (nil ) after H giving sorted Ol The body of sort calls another generator append The definition of the generator append is a recursive one. Bool => append already sorted Numlist after Numlist giving sorted Numlist append already sorted SI after Ul giving sorted Ol — case Ul of nil | Ol :=Sl head N and tail T \ case partition T by N of small Sml and large Lrg | find X: Numlist in append already sorted SI after Lrg giving sorted X \\ append already sorted ( head N and tail X ) after Sml giving sorted Ol Two partitioned sublists Sml and Lrg are sorted in parallel as in the example for the R-Maple version of quicksort presented in section 4.8. The predicate above is a generator. The program partition, however, can be written as a function yielding two lists. The relevant definitions are as follows. Pair —• small Numlist and large Numlist Pair => partition Numlist by Number partition NI by Num = case NI of Section 5.6 Examples of RF-Maple Programs 60 nil | small nil and large nil head H and tail T\ case partition T by Num of small S and large L \ case Num < H of true | small S and large ( head H and tail L ) f alse | small ( head H and tail S ) and large L The next example is a program that counts the nodes of a binary tree. The program is written as a function that returns the count. The function production is as follows: Number => count nodes of Bintree (Number ) The definition is then : count nodes of Tree — case Tree of empty | 0 node V left Lt and right Rt \ 1 + count nodes of Lt + count nodes of Rt (0) The program can be easily converted to add up the value of all the nodes of the binary tree. This can be achieved by replacing the number 1 by the variable V in(0). The next example is a generator which generates the Fibonacci number. It is written as a generator to demonstrate the use of the find and assignment construct. Bool => fib of Number after Number and Number with Number yielding Number fib of X af ter M and N with K yielding Y = case X — 0 of true | Y-—M false | case X — K of Section 5.6 Examples of RF-Maple Programs .. 61 true | Y:=N false | find T:Number in fib of X after N and M + N with K + 1 yielding T; Y:=T The program assumes that the subtraction and addition function have been defined. The program uses the same algorithm as the corresponding program written in R-Maple in section 4.8. It keeps the last two Fibonacci numbers found and keep on generating a new Fibonacci number until the new number is the nth number required. In the program above, M and TV" are the last two Fibonacci numbers found and X is the nth Fibonacci number required. K indicates that ./V is the mth Fibonacci number. Hence when K equals X the program returns N. The generator can be invoked with the following statement. find X-.Number in / ib of 5 af ter 2 and 3 with 1 yielding X This will generate the fifth Fibonacci number with the first two Fibonacci numbers as 2 and 3. The final example appears also in the paper [Voda & Yu 84]. It illustrates cooperation of concurrent processes using partially instantiated streams as described in [Shap2 83]. The RF-Maple version of the queue manager will be presented. Streams are means by which processes communicate. They are represented using lists. Messages are sent and kept in queues. The queue manager accepts two kinds of messages. They are: Message (T) —* enqueue T Message (T) —* dequeue T Section 5.6 Examples of RF-Maple Programs ..62 for putting and retrieving elements of type T from the queue. As in Shapiro's program, the queue manager is communicating with two users via a merge pro-cess. The relevant types are : Bool => user 1 with stream List (Message (T)) Bool => user2 with stream List (Message (T)} Bool => merge List (T) with List (T) yielding List (T) Bool => queue with front List (T) end List (T) and messages List (Message (T)) These are invoked by : find 51, 52, 53 : List {Message (T))in user I with stream 51 |j user 2 with stream 52 || merge 51 with 52 yielding 53 || find Q : List (T) in queue with front Q end Q and messages 53 The predicate bodies for user 1 and user 2 will not be given. Merge must be a primitive in RF-Maple. The body for queue is as follows : queue with front H end T and messages M — case M of nil | true head Hm and tail Tm | case Hm of enqueue V \ find Nt in T:= head V and tail Nt || queue with front H end Nt and messages Tm dequeue V \ V:= head of H \\ queue with front (tail ofH ) end T and messages Tm The first case terminates the cooperation of processes when the list of messages is Section 5.6 Examples of RF-Maple Programs ..63 exhausted. Otherwise, the head of the list of messages contains the message enqueue or dequeue . In the first case, the end of the queue is partially instan-tiated with the pair composed of the value to be enqueued and the rest as yet not instantiated. The queue manager is then recursively invoked with the rest of the messages. In the latter case, V should be instantiated with the value at the head of the front. The queue manager then proceeds recursively with the rest of the messages. Head and tail are projection functions. Head is defined as follows : T=> head of List (T) head of L = case L o f nil | 0 head A and tail B \ A Similarly for tail. It is assumed that for each I 1 used there is a production T —> 0 giving a distinguished constant 0 of type T. Note also that if the queue is empty when a dequeue message comes, //, and thus head of H, will not be instantiated. Therefore, the user process trying to use V will be delayed when trying to deter-mine the structure of V in a case construct. It will be allowed to proceed when an enqueue message from the second user arrives. Hence, it is necessary to res-tart the queue manager in parallel. 64 Chapter 6 Semantics Theory 8. Background Of Semantics Theory Various methods have been proposed for describing the formal semantics of programming languages. The motives behind the need for formalizing the seman-tics of programming languages is that first, the notation used in a programming language may have a different meaning in another. For example, the meaning of an expression like / (x) depends on the different rules about parameter passing in different languages [Stoy 77]. Second, computers require that programs presented to them follow a precise set of rules. The rules are often difficult to describe precisely and this is another reason for requiring great care and formality [Stoy 77]. Initially, the objective was to give a sufficiently precise description for implementers of the languages to construct a correct compiler. Nowadays, the emphasis is more on a description sufficiently precise for programmers to make rigorous statements about the behaviour of the programs they write. In the future, the most important benefit will probably be to language designers, who will be guided towards the design of better (cleaner) programming languages, with simpler formal descriptions [Stoy 77]. Three main methods for giving formal semantics description of programming languages will be described briefly in the following section. The semantics of RF-Maple will be described in yet another formal semantics in Chapter 7. Section 6.1 The Operational Approach ..65 6.1. The Operational A p p r o a c h In this approach, the semantics of the programming language is defined in terms of the change of state of an "abstract" machine by each of its instructions. The idea is that although the abstract machine is probably completely unrealistic from a practical point of view, it is so simple that no misunderstanding can possi-bly arise with respect to its order code [Stoy 77]. The SECD machine described in [Hend 80] is an example of the definition of the LISP programming language by operational semantics. This approach does not fully define the semantics of a programming language because there is still the problem of rigorously defining the abstract machine. That is, giving a formal semantics for the machine code still needs to be done. In this sense, the operational approach seems to be push-ing the problem of defining a programming language further into defining the abstract machine. Another problem with the operational approach as suggested by [Dijk 72] is that the method tends to be regarded as one which gives the result only of specific computations. By feeding the abstract machine with a set of input, it will generate the appropriate output. However, it is much more useful to be able to consider the class of all the computations that can possibly be evoked by the program, or even by a class of functions [Stoy 77]. This is in essence, defining a function such that for any input, the function will give the output which the programming language is intended to give. This leads to the second approach which has this objective in mind. Section 6.2 The Denotational Approach ..66 6.2. The Denotational Approach Semantic valuation functions are used to map syntactic constructs in the program to the abstract values (numbers, truth, values, functions, etc.) which they denote [Stoy 77]. The definitions of semantic functions will be denotational, that is to say, structured so that the meaning of any composition phrase is expressed in terms of the meanings of its immediate constituents [Tenn 81]. A legal program is given a precise meaning as function from its inputs to its ouputs. For example, the semantics of binary numerals may be formalized in the follow-ing table [Tenn 81]. Abstract syntax N £ Nml binary numerals N ::= 0 | 1 | NO | N l Semantic domain N — {zero }+ N natural numbers = {0,1,2,3 .... } Semantic function Nf : Nml -> N A T [ [ o ] ] = o A 7 [ [ l ] ] = l Nf [ [ NO ] ] = 2* Nf [ [ N ] ] • Nf [ [ N l ] ] = 2* Nf [ [ N ] ] + 1 The three sections of the table define (a) Nml, the syntactic domain of binary numerals whose syntax can be derived from the context free rule, (b) N, the semantic domain of natural numbers, and (c) the semantic function, Nf , using one "equation" for each of the possible forms of binary numeral [Tenn 81]. The problem of using models of denotational semantics with practical programs is that it is quite difficult to prove even simple properties of programs. The reason is that the denotational semantics stresses the model-theoretical part and under-plays the importance of derivations within a formal theory [Voda 84]. Section 6.3 The Axiomatic Approach .. 67 6.3. T h e A x i o m a t i c A p p r o a c h An axiom is associated with each kind of statement in the programming language, which states what one may assert after execution of that statement in terms of what was true beforehand [Stoy 77]. This approach grew out of Floyd's work [Floy 67] and the work of Hoare [Hoar 69]. An example of its use is as fol-lows: consider a simple program that exchanges the values of two variables. Assume that before the program is executed, X and Y have some initial values X0 and Y0. It is desirable to prove that after the program is executed, X — Y0 and Y = X0. To achieve this, input and output assertions are included as com-ments in the program. The assertion X = X0 & Y = Y0 is included at the beginning of the program and the assertion X = Y0 & Y = X0 is included at the end of the program. These assertions are not to be executed by the program, but they serve as the way the programmer expects his program to behave. The essence of the approach is to generate from a commented program a set of state-ments called the verification conditions. If these statements and the input asser-tions are true, then the other assertions the programmer has put in his program are correct. Whereas the programmer's assertions are intended to hold only when control passes through the appropriate point, the verification conditions should be true in general, and they can be proved by a deductive system that knows nothing about sequential processing, loops, recursion, or other concepts about the flow of control of the particular program [Mann & Wald 77]. This approach has made an important contribution to the art of proving the correctness of pro-grams. There is a minimum of new notation. However, this approach does not Section 6.3 The Axiomatic Approach clearly define computation. .. 69 Chapter 7 Theory of Pairs 7 . T h e o r y o f P a i r s The methods for formalizing the semantics of a programming language described above seems to be either too complex or insufficient for the task. The difficulty in defining the semantics of a programming language using any of the above methods increases when the language allows assignments to variables. R-Maple is a declarative programming language which does not have any side effects and therefore, a weaker formal theory is sufficient in formalizing its semantics. Paul Voda [Voda 84] proposes to explain the semantics of a declara-tive programming language by means of two formal theories. One formal theory gives denotations to programs while the other one, which is actually a sub-theory of the first theory, specifies the operations of the computing machine executing the programs in that the computations correspond exactly to proofs in the weaker theory [Voda 84]. This formal theory is called the theory of pairs, TP. It is a first order theory with the power equivalent to the Peano Arithmetic which is a formal way of axiomatization of the natural number theory. As will be seen in the description of the theory, it is more suitable for programming languages because it is based on an equivalent of S-expression in LISP. The advantage is that S-expressions allow the encoding of data structure and programs in similar fashions. The domain of the intended interpretation of TP consists of the individual 0 and is closed under the operation of pairing. Hence, 0, [0,0], [ [0,[0,0] ],0], Chapter 7 Theory of Pairs ..70 [ [0,(0,0] ],[ [0,0],0] ] are examples of individuals in the domain of TP which are denoted by literals. The term 0 denotes the individual 0. If the terms n and m denote the individuals n and m respectively, then [n,m] denotes the ordered pair of n and m. The numerals will be used as an abbreviation for terms as follows: 0 = 0 1 = [o,o] 2 =(0,(0,0]] For the following discussion, [a ,b ,c ] will be written in place of [ a,[ b ,c ] ]. A Lisp-like list composed of the elements a x o 2 > . . . . , o B will be written as [aha2....anp] Two pairs are equal if the corresponding components are equal and no pair is equal to 0. The atomic formulae in TP are s=t and s £ t for any terms s and t. In addition to the logical symbols such as connectives and quantifiers of the first order predicate calculus, the regular first order logical axioms, TP includes the following axioms. Axioms of Identity: x =x x =x ' & y —y ' & x —y —+ x '=y ' x=x'& y=y'& x G y x'G y' x=x'& y=y'-* [x,y ]=[x',y'] Also, TP includes the non-logical axioms of uniqueness of pairing, two axioms of membership and the axiom schema of induction. Non-Logical Axioms: [ x ,y ]=[ x\y '} — x—x ' & y =y ' x £ 0 Chapter 7 Theory of Pairs ..71 Q£ £ | y *r J 4—• y ^ £ £ P (0) & V z V j f {P {x ) & P (y ) - P ([ x ,y })} -> VxP (x ) TP is a formal theory. The intended model for TP is satisfied in the domain of pairs. The model gives precise meaning to all functions and predicates intro-duced into TP. To formalize a functional programming language in TP, the language is defined as subclasses of terms of TP. Each function can be intro-duced as a conservative extension of TP by a new symbol satisfying its (recur-sive) definition. Similarly, a predicate of a logic programming language can be formalized in TP, and each predicate can be introduced into TP by a predicate symbol. The interpretation of TP then gives the denotation to the function or predicate. By using the power of the predicate logic, TP gives meaning to a program-ming language. The control of the language is computed by rewrite rules which will be invariant under the meaning of programs being computed. In summary, TP gives meaning to programs. To formalize a programming language in TP, a subtheory S needs to be constructed which gives meaning to functions or rela-tions in the language in that the proofs in S correspond exactly to computation. RF-Maple will be formalized in TP by setting up a sub-theory of TP whose proofs correspond exactly to the computations. 7.1. Semantics of RF-Maple RF-Maple is a typed programming language. Introduction of types to a logic system like that of TP is not straight forward. In defining the semantics of RF-Maple, no typing theory will be introduced into TP. The semantics of RF-Maple Section 7.1 Semantics of RF-Maple ..72 will be defined, instead, as a typeless language. This does not mean that the language to be defined in TP does not compute what RF-Maple does. Operation-ally, they are equivalent. The difference in defining RF-Maple as a typed language requires the introduction of types info TP formally, whereas, defining RF-Maple as a typeless language requires only a modification in the data struc-ture used in the computation. The next section is a description of typeless RF-Maple. The language will be referred to as TRF-Maple. 7.2. T y p e l e s s R F - M a p l e TRF-Maple differs from typed RF-Maple in that no neAV types can be defined in the language. The only allowable types in TRF-Maple are numerals and pairs. However, by manipulating the structure of a data value, say prepend a data value with a tag, the same result may be obtained like that of typed RF-Maple. For example, if every data value used in typeless RF-Maple is a pair, and that the head of the pair is taken as a tag which indicates the intended form of the data value in the tail of the pair, then, by the manipulation of the tag, a pro-gram written in typeless RF-Maple can simulate the effect that can be obtained in typed RF-Maple. Moreover, the operations of the typeless RF-Maple can be correctly defined semantically in TP, as will be seen in section 7.3. The difference between TRF-Maple and RF-Maple is that in TRF-Maple, the user has to be aware of the need to manipulate the tag to achieve the same result as that of typed RF-Maple (where types can be defined by generating productions, function productions, etc.). Section 7.2 Typeless RF-Maple .. 73 Basically typeless RF-Maple is equivalent to RF-Maple in all aspects except the following points. 1) The only allowable data values in typeless RF-Maple, as mentioned above, are numerals and pairs. Hence, values such as [l,[2,3j], [ [ 1,2 ],[3,4] ] are legal values in typeless RF-Maple. 2) There are no more gen-erating productions since no new types may be defined. 3) There are no more function productions since all functions will return the same type. 4) There are no more variable productions since all variables are of the same type also. 5) Since there are no types defined in the language, the case construct is modified so that the comparison is between two data values rather than on the data forms. More specifically, the labels for the case x • • • statement are numbers representing the tags (which are the intended data forms for the variable x). The comparison in the case statement is based on the head of x with the numbers in the labels. Since the head of x is the tag for its data value in the tail, the com-parison in the case statement is actually between tags (or intended data forms). Also, the labels must be numbered in sequence starting with the label 0. That is, the possible data forms for a variable or data value must be assigned tags in sequence with the first data form numbered 0. 6) The find construct need not specify the type of the variable to be bound. That is, the find construct can be of the form: find a in • • 7) the function hd and tl are system functions in TRF-Maple which select the head or tail of a data value. These are not needed in R-Maple because R-Maple provides the "split" operation which essentially allows the selection of head and Section 7.2 Typeless RF-Maple .. 74 tail. In F-Maple and typed RF-Maple, a value can be mapped onto its data type in the label of the case construct and the parts of a data value can be readily retrieved. In TRF-Maple, the hd and tl functions need to be introduced as sys-tem functions to allow accessing of data in a pair. 8) Finally, because functions can have functions as its arguments, the binding operator let is used which allows the function argument to be evaluated once, and prevents the function argument to be evaluated several times if it is needed in several places. An example of a program written in TRF-Maple is the generator which gen-erates a number from a binary tree of numbers. The program written in typed RF-Maple has been presented already in section 5.5. generate X from Tree — let Y-.— Tree in case Y of 0 | [1,0] 1 | X:=Y.tl.hd or generate X from Y.tl.tl.hd o r p generate X from Y.tl.tl.tl An empty tree structure represented in TRF-Maple can be: [0,0] where the first 0 is the tag indicating that the tree structure is empty. The tree structure with a data node and left and right branch represented in TRF-Maple can be: \\,\node\left,right)\\ where left and right have a data structure either of the first form or the second form. The 1 indicates that the tree structure is non-empty, and that the tail of the whole structure contains the data values for the node and left and right Section 7.2 Typeless RF-Maple ..75 branch. The let binding operator ensures that the argument Tree to be evaluated only once. In case a function is passed to the argument Tree, the function argument will be evaluated once, and the result bound to the variable Y. The case operator selects the sub-program to be computed based on the comparison between the head of variable Y and the labels. If the head of Y is 0, then the data value for falsehood is returned (ie. [1,0]), else, the program assigns to X the value of the node (which is Y.hd.tl) and prepares for backtrack using the or operator. Notice that programs written in typeless RF-Maple is not as readable as their equivalent in typed RF-Maple. It is the user's responsibility to assign tags to his/her intended data forms. The data forms for truth and falsehood are often used in RF-Maple, therfore, the data value [0,0] will be used consistently to denote a true value, and [ 1,0] will be used to denote a false value. The constant True and False will be used to abbreviate the terms [0,0] and [1-0]-Note that the tag for a binary tree with left and right branch is the same as the tag for the data value for falsehood. Tags in different types can be the same, therefore, it is the user's responsibility to check that correct intended typing is enforced. For example, when the above program is invoked, the variable Tree needs to have the intended form. In essence, typeless RF-Maple forces the user to be aware of the manipula-tion of the tag whereas, in typed RF-Maple, type checking is left to the executing machine. Section 7.3 Formalization of the Semantics of TRF-Maple .. 76 7.3. Formalization of the Semantics of TRF-Maple in T P In formalizing the semantics of TRF-Maple, T P is rephrased as a term logic. Term logic [Herm 70] does not make a distinction between a term and a formula. This implies that logical connectives and quantifiers are just functions. The func-tions for sequential and parallel connectives will be introduced into TP. A l l data values in TRF-Maple except numbers are prepended with a tag as an indication of the intended form. For each possible form of a data type, the first possible form .is assigned a tag of value 0, the second 1, .. and so on. Hence, if the tag for the form nil is 0, the tag for head Number and tail Numlist is 1, then the data value head 1 and tail head 2 and tail nil represented in RF-Maple is represented as [ 1,[ 1,[ 1,[2,[0,0] ] ] ] ] in TRF-Maple. This is relatively cryptic in its form. Therefore, the following functions can be defined: N I L = [0,0] {X,Y} = [1 ,X ,Y] where X is intended to be a number and Y as a Numlist, either N I L or {X,Y}. Hence, the list above can be abbreviated by {1,{2,NTL}}. The use of the tag in the computation rules will become apparent when they are presented in the fol-lowing. The programs of TRF-Maple are a subclass of terms called TRF-terms. TRF-terms are composed from 0 and variables by pairing. True = [0,0] will be used to indicate a true value, False = [1,0] is taken as a false value. A list is always terminated by a NIL . Atomic TRF-formulae are composed of atomic for-mulae by connectives, negation, and existential quantifier. They are just func-Section 7.3 Formalization of the Semantics of TRF-Maple .. 77 tions satisfying the following identites: [0,0] V [0,0] = [ l , a ] V [0,0] = [0,0] V [ l , a ] = [0,0] [ l , a ] V [ l , d ] = [ l ,0] [0,0] & [0,0] = [0,0] [ l , a ] & [0,0] = [0,0] & [ l , a ] = [ l , a ] & [ l , c ] = [1,0] -n [0,0] = [1,0] - [ l , a ] = [ 0 , 0 ] where a , c, and d can be any RF-terms. The find construct of TRF-Maple is introduced as the 3 function in TP. For any term a , the term (3 ar a ) denotes a function of all free variables in a but ar. (3 ar a ) = T r u e if there is a literal n such that a {x:=n } = T r u e and (3 ar a ) = F a l s e otherwise. All functions F (x ) must be introduced into the theory of TP as one place functions in such a way that \-TP F(x ) — a. Ail functions are evaluated using lazy evaluation. Lazy evaluation allows a delay in evaluating the arguments passed on to a function. The only disadvantage of lazy evaluation is that it is shallow. By this, it means that when the control reaches a pair for evaluation, it does not evaluate the pair but it reverses. This is not desirable on the outermost level where the evaluation would stop after one shal-low reduction. For this reason, markers are introduced to force the full evalua-tion on the top level. Five markers are introduced into TP by the definitions to satisfy: do (ar ) = wait (x ) = down (ar ) = up (ar ) = x The markers "do", "wait", "down", and "up" are called processes. They mark the positions where the computation takes place. The marker "do" goes down in a RF-term while the marker "wait" delays the computation of a term until another term is reduced. The marker "down" is used in the lazy evaluation of Section 7.3 Formalization of the Semantics of TRF-Maple .. 78 function arguments. They are used to force the evaluation cf all the arguments of a function The marker "up" forces the full evaluation to the top level. Functions hd, and tl are introduced into TP with the obvious properties: \-TP hd ([a ,b]) = a \-TP tl ([a ,b]) = b \-TP hd (0) = tl (0) = 0 hd (a) will be abbreviated to &.hd. Similarly tl (a) will be abbreviated to &.tl. Other functions that need to be defined are: x || y = x & y x orp y — x V y x:=y — x —y The case construct is introduced into TP to satisfy the following properties. case (0) = case (0,y ) = 0 case ([0,a],y ) = y.hd case (j[m,n],a],y ) = case ([n,a],y./7 ) The case construct of TRF-Maple are rewritten as case (V,P) where V is the tagged value on which the case decision is to be made and P is the list of all sub-programs for each case arranged according to the increasing order of its corresponding tag value. For example, the case construct: case V of 0\Progx [0,0] | Prog2 is equivalent to the function case of the form: case (V.hd ,[Progh\Prog2,mL]]) If the tagged value Y.hd has a tag of 0, then the result is the sub-program corresponding to the first generating production of the data form of V. This is essentially the head of the list of sub-programs. Othenvise, the function is recur-Section 7.3 Formalization of the Semantics of TRF-Maple ..79 sively invoked with the tail of the tag V.hd and the tail of the list of sub-programs. Notice also, that the list of sub-programs is terminated by a NIL at the end. The operator let is introduced into TP to serve as an environment where variables are allowed to be shared. (let v.=a in b ) = 6 {v:=a } This allows the evaluation of function using lazy evaluation. This is because the evaluation of an argument in a function invocation can be delayed by assigning it a variable in the let operator. / (g (2))=> let x:=g (2) in / (x ) In the example, by using the let operator, evaluation of g (2) will not take place until the argument is needed in the evaluation of the body of / (x ). Once g (2) is evaluated, its value is stored in the let operator so that other referrence to g (2) can be immediately recovered. By using the let operator, function argument needs to be evaluated once even though several references of that argument are made. Also, the result from a function inside the program can be bound to a variable using the let operator so that it may be referred to in different places. The backward shipment of assignments through enclosing disjunctions and conjunctions by employing the associativity and distributivity of the connectives until the assignment reaches the existential quantifier. For example: { (up(x : = a ) & A ) V B } V C = > {up (x : = a ) & A } V ( B V C ) Section 7.3 Formalization of the Semantics of TRF-Maple ..80 { ( u p ( x : = a ) & A ) V B} & C => {up(*:=a) & ( A & C )} V ( B & C ) When the assignment reaches its quantifier, the quantifier is split for a possible backtrack and discharged in one side of disjunction. 3 x { ( u p ( x : = a ) & A ) V B}=> 3x (up (x : = a ) & A) V 3x B => {let x : = a i n do (A)} V 3xB The function Partition will be introduced into TP which partitions a list into a pair of lists by a number and returns the partitioned list is given here. The expanded name of the function defined in TRF-Maple, say Partition X by N, is represented in the usual functional notation such as Partition (X,N ). In addition to the functions defined earlier to improve reada-bility for tagged data values, (ie. NIL, {x,y} , etc ), the function < x , y > is used to define a pair of Numiist x and y . \-TP Partition (Nl ,Num ) = let Y:=Nl i n case (Y,[ <NIL,NTL>, let X.^Partition (Y.tl.tl,Num ) in case (X, [case (Num <Y.tl.hd.tl, [ <X.tl.hd,{ Y.tl.hd ,X.tl.tl}> <{ Y.tl.hd ,XM.hd },XMM > ) ]) ]) The use of projection functions hd and tl are necessary to bypass the tag of the data value to access the value itself. Notice that in the definition of the function Partition, the variable X is introduced in the let operator to refer to the result of the function invocation Partition (Y.tl.tl,Num ). If the result is not shared on the outermost level among the sub-programs of the case construct, then the function needs to be invoked each time the value is needed. Also, the variable Y is used to bind to Section 7.3 Formalization of the Semantics of TRF-Maple .. 81 the argument NI. In case NI is passed a function as the argument, the result of the function argument is bound to the variable Y so that future reference to the argument is readily available, and only one evaluation of the function is needed. A sequence of existential quantifiers is abbreviated into the form 3aA where a is a sequence of variables. The empty sequence can be included by setting 3A to stand for A . a n d will be used to stand for either sequential or parallel con-junction, similarly o r . The axioms and inference rules of TRF-terms can be specified as follows. However, they do not represent the only set of axioms and inference rules appli-cable in the computation of TRF-Maple programs. An implementation of TRF-Maple may follow a whole new set of rewriting rules. The only requirement is that there can be no ambiguity in the choice of which axiom or inference rule to use in any circumstance during the computation. a) I n i t i a l A x i o m s are of the form A = down (do ( A ) ) for every RF-term A not containing markers. b) F u n c t i o n A x i o m s are of the form F (x ) = A where A is a RF-term not containg markers and having at most the variable x free. It is required that VTP F (x ) = A . c) C o m p u t a t i o n A x i o m s are the following ones for each RF-terms A , B , C , a , b , c, and d . The variable v does not occur in the term a. t will be used to indicate the tag for the constructed value which is the intended data form Section 7.3 Formalization of the Semantics of TRF-Maple 82 of the value. It should be noted again that T r u e = [ 0,0 ] is used to denote the true value in TRF-Maple, and F a l s e = [1,0] is used to denote the false value in TRF-Maple. T u r n - a r o u n d G r o u p . do ( v : = a ) = (up ( v : = a ) & T r u e ) V F a l s e provided that v is not free in a . I d e n t i t y G r o u p . do (0= [ a , b ] ) = up ( F a l s e ) do ( [a,b]=0) = up ( F a l s e ) do (0=0) = up ( T r u e ) do ( [ a , b ] = [ c , d ] ) = do ( a = c ) & b = d N e g a t i o n G r o u p . do ( i A ) = i do ( A ) - i up ( T r u e ) = up ( F a l s e ) -•wp(False) = up ( T r u e ) D i s j u n c t i o n G r o u p . do ( A V B ) = do ( A ) V B do ( A o r p B ) = do ( A ) o r p do ( B ) up ( T r u e ) o r B = up ( T r u e ) up ( F a l s e ) V B = do ( B ) up ( F a l s e ) o r p B = B {3a (up(v:=a) a n d A ) o r B } o r j C = 3a{up (v :=a) a n d A } o f ( B o r j C ) (1) A o r p B = B o r p A (2) In (1) o r = o r and B = B unless o r j = o r p . In the latter case o r = o r p and if o r = V then B = do ( B ) . Section 7.3 Formalization of the Semantics of TRF-Maple 83 In (2) B has one of the forms tz^(True), up (False), or 3a{«p (v:=a) and C} or D and A is not of any of these forms. This prevents the computation to use this rule over and over again. Conjunction Group. do (A & B) = do (A) & B do ( A || B) = do (A) & do (B) up (False) and B — up (False) up (True) & B = do (B) up (True )|| B = B {3a (up(v:=a) and A) or B} andj C = 35{up(v:=a) and (A andx C)} of (B and t C) (3) A || B = B || A (4) where in (3) some of the bound variables in a must be renamed yielding a, v, a, and A should a free variable of C become bound inside 3a. Also and == and, of == or, A = A and B = B unless andj == || . In the latter case and = || and of = orp . If also and = & then A = do (A). Similarly, if or = V then B ES do (B). In (4) B has one of the forms up (True), up (False), or 3a{up (v:=a) and C} or D and A is not of any of these forms. This again prevents the computation to use this rule over and over again. Quantifier Group. do (3vA) = 3v do (A) 3v up (True) = up (True) 3v up (False) — up (False) 3w{3a (up (v:=a) and A) or B} = 3a{up (v:=a) and 3wA} or 3wB (5) Section 7.3 Formalization of the Semantics of TRF-Maple ..84 3w{3or (up ( v : = a ) a n d A ) o r B } = 3w,o{u/)(v:=a) a n d A } o r 3wB (6) In (5) and (6) the variable vf is different from v . In (5) the variable w does not occur in a , whereas in (6) it does. The case when the variable w is the same as v is presented in the l e t rule. C a s e G r o u p do (case ( x , P ) ) = c a s e (do ( x ) , P ) case (do ( [ a , b ] ) , P ) = case ({do ( a ) , b ] , P ) case {[do ( O K b U P , ^ ] ) = do (P,) case {[do ([a ,d]),b], [P l l P 2 ]) = case {[do ( d ) , b ] , P 2 ) d) R e p l a c e m e n t R u l e . A = • • • B • • • , B = C A = • • C • • where B = C is a Computation axiom. e) F o r c i n g G r o u p . down (do (0)) = up (0 ) down( do ( [ a , b ] ) ) = [ down (do ( a ) ),b ] [«p(a),b] = [a,,down (do ( b ) ) ] [a,«p(b)j = up ( [ a , b j ) f) P r o j e c t i o n G r o u p . do (a.hd ) = do (sL).hd do (a.f/ ) = do (a).tl do ([&,b]).hd = do (a.) do ([a,bj).« == do ( b ) g) T e r m i n a t i o n R u l e s . A = up (B ) A = B Section 7 .3 Formalization of the Semantics of TRF-Maple .. 85 h) F u n c t i o n C a l l R u l e . a = le t a, • • • do (/ ( b ) ) • • • , / (x ) = c a = le t a, • • • x : = b , i n • • • do ( c ) • • • where / (x ) = c is . a Function Axiom and all free variables of b have binding occurrences in a. In order to maintain the uniqueness of bindings the variable x has to be renamed to a new variable x in the binding x : = b and in the term c{x:=x}. In order to assure the uniqueness of derivations it is stipulated that the sequence of bindings a is the shortest sequence binding all free variables of the term b . i) W a i t I n t r o d u c t i o n R u l e . a = le t o r , u : = b i n • • • do ( u ) • • • a = l e t a, u:=do ( b ) i n • • • wait ( u ) • • • j) W a i t E l i m i n a t i o n R u l e s . a = l e t a, u:=rfo (0) i n • • • wait ( u ) • • • a = l e t a, u:=0 i n • • • do (0) • • • a = l e t a, u:=do ( [ a , b ] ) i n • • • wait ( u ) • • • a = l e t a, v : = a , w : = b , u : = [ v , w ] i n • • • do ([ v , w ] ) • • • where in (7) the introduced variables v and w do not occur in a and b . During the course of computation, several wait markers may be introduced. The sequence of wait elimination is last in last out. That is the latest wait gets eliminated first. k) L e t R u l e s l e t a i n • • • do ( let x : = a i n b ) • • • l e t a , x : = a i n • • do ( b ) • • Section 7.3 Formalization of the Semantics of TRF-Maple where x is to be renamed to x if x occurs free outside of b. let a in .... 3v{3/? (up (v:=a) and A) or B}.... let a, v:=a in .... 3/?A or 3v3/33 A = A unless and = & . In the latter case A = do (A). Also, v is to be renamed to v if v occurs free outside A and 3v3/? B. let a in up (b ) up(b ) As a simple example, let us introduce the following functions by explicit definition into TP as: FTP f (V ) = case (y,[((0,0],y.</], [0,y.f/J/],NIL]) \-TP g (x ) = case (x,[ [ 0,x.tl.tl ], [ [0,0 ],x.tl.tl. hd ], NIL]) This is a legal function because it takes in a value and simply returns another value. The steps of the computation of g (f ([ [0,0],[0,[0,0] ] ])) is partly given by the following proof. A will be used to abbreviate g (f ([[0,0],[0,[0,0]]])). A = down(do (g (f ([ [0,0],[0,[0,0] ] ])))) A = letx:=/ ([[0,0],[0,[0,0]]]) in down(do (case (x ,[[Q,x.tI.tl ], [[0,0], x.U.tihd ],NIL]))) A = lets:=/ ([[0,0],[0,[0,0]]]) in down(case (do (x ),[ [0,y.tl.tl ],[ [0,0),y.tl.tl.hd ],NIL])) A = letx:=<f0 (/ ([[0,0],[0,(0,0]]•])) in down (case (wait (x ),[[0,y.titl ],[[0,0),y.tl.tl.hd ],NIL])) A = lety:=[[0,0],[0,[0,0]]] in x:=case (do (y ),[[[0,0],y.tl ],[0,y.t!M ], NIL])) in • • • A == let a :=[0,0],6 :=[0,[0,0] ],y :=( a ,b ] in x:=case(do ({a,b])---A = let a:=[0,0],6:=[0,[0,0]],y:=[a,6 ] in x:=case ([do {[a),b]---A = let a 1:=0,a2'-=0,a :=[ o1)a2], • • • Section 7 .3 Formalization of the Semantics of TRF-Maple i n ar:=case ([do ([ aha2]),[[ [0,0},yM ],[0,yMM ], N I L ] ) • • A = l e t a 1:=0,a2:==0)a : = = [ ai>fl2l> ' ' ' i n ar:=case ([do (a2),[[0,y.tl.tl ], N I L ] ) • • • A = l e t ai.=0,a2.=0,a :=[ aha2], • • • i n ar : = c a s e ([ do (0 ),[ [0,y.tl.tl ], N I L ]) • • • A = le t a i = 0 • • • x:=do ([0,y.tl.tl ]) i n down (case (wait (ar ) A = l e t • • • z1:=0,y1:=«.W.f/,z:=[ari,y1] i n down (case (do ([ i hy 2 ]),[ [ 0,x.tl.tl ], [ [ 0,0),x.tl.tl.hd ], N I L ] ) A = l e t • • • x1:=0,y1:=y.r/.f/,ar:=[ar1,w1] i n rfoum(case ([do (x1),yl] ),[[0,x.tl.tl ], [[0,0],x.tl.tl.hd }, N T L ] ) A = le t • • • zx:=0,y a: j.yj] i n down (case ([ rfo (oj.wj ),[ [0,xM.tl ], [ [0,0\,x.tl.tl.hd ], N I L ] ) A = l e t • • • Xi.=0, • • • i n down (do [0,x.tl.tl ]) A ==[0,0] 88 Chapter 8 Future Work 8. F u t u r e W o r k Considerable amount of improvement can be made to the implementation of R-Maple. For simplicity sake, the interpreter currently assigns expressions to variables using substitution of the expression. Invocation of predicates is by sub-stitution also. This amounts to a lot of copying of tree structure during the exe-cution especially when the expression to be assigned to a variable is large. In fact, during a trace of a program execution, most of the time is spent copying trees, scanning trees, etc.. A more efficient improvement can be the use of environments. This allows the value assigned to variables to be retrieved and shared more efficiently. Also, some kind of administrative manager can be set up if subtrees are allowed to be shared. Currently, there is no sharing of subtrees allowed. If sharing is allowed, this will save considerably much time since fewer subtrees need to be copied. In the current implementation, extra keywords are used for the abstract syn-tax which is not actually necessary. For example, the keyword predop in <attrop,predop....>, is not necessary since the compiler that generates the code in abstract syntax is supposedly to be error free and the interpreter can assume that the number of the predicate to be invoked is supposed to follow the attrop opcode. The inclusion of these extra keywords for the current implementation is only for the sake of improved readability. Future implementation can improve in this regard. Also, the current implementation for the execution of the equality Chapter 8 Future Work .. 89 test is not done in parallel. According to [Voda 83], during an equality test, the tests for both branches of the two consed expression are to be done in parallel. The current implementation checks each expression to see if there are any unas-signed variables. If not, then the equality test for each node may proceed. Oth-erwise, the process is blocked until the whole expression contains no variables. So far, no compiler is available to translate a program written in concrete syntax to abstract syntax. A front-end processor that will accomplish this task is very desirable. Another point is that, although nondeterminism is available in R-Maple, the actual implementation does not produce results that will reflect this nature. If arguments are allowed to be entered interactively during execution, some form of nondeterminism may result. R-Maple can also be made to allow the use of any constants. In the current implementation, only numerals and pairs are allowed. Also, a debugger will be useful during a trace of the execution of a R-Maple program. Finally, if an algorithm is available to allow copying of tree structure to be done more efficiently, this can significantly improve the perfor-mance of the R-Maple machine. RF-Maple is still under implementation. A working system will demonstrate clearer the feasibility of the language and its ease of use. Again, the system can bring out the nondeterministic nature of the language clearer if arguments are allowed to be entered during execution. Introduction of types into a formal logic system such as TP is still not clear and straight forward. If types can be easily introduced into TP, then the seman-tics of RF-Maple can be defined without having to convert the language into a Chapter 8 Future Work typeless one before the semantics can be defined. 91 Chapter 9 Conclusion 9. Conclusion It has been demonstrated that a logic programming language can be based entirely on the rewriting rules as described in section 3.4. Moreover, the rewrit-ing rules correspond to a declarative reading in first order logic. The interpreter for R-Maple is considerably easy and straight forward to implement also because again, the operation of the interpreter is based on logic. R-Maple can be extended to include functions as can be seen from the description of RF-Maple. This allows some predicates which has the many-to-one correspondence between the input and the output to be encoded as a function. Functions can be executed more efficiently, since no backtracking is needed. Also, RF-Maple allows the user to define his or her own types according to his / her liking. Finally, it has been shown that TRF-Maple is semantically correct by its formalization using the Theory of Pairs. The semantics of R-Maple can also be said to be defined opera-tionally. 92 References [Abra 84] Abramson, H.: Definite Clause Translation Grammars, Proceedings 1984 International Symposium on Logic Programming, Feb 6-9,1984, New Jersey. [Berg & Kano 75] Bergman, M. and Kanoui, H.: Sycophante: Systeme de calcul formal et d'integration symbolique sur ordinateur, Groupe d'Intelligence Artificielle, Marseille-Luminy, October 1975. [Colm 75] Colmerauer, A.: Les grammaires de Metamorphose, Groupe d'Intelligence Artificielle, Marseille-Luminy, Nov 1975. [Cloc Sc Mell 81] Clocksin, W.F. and Mellish, C.S.: Programming in Prolog, Springer- Verlag, Belin Heidelberg, New York 1981. [Dahl & Samb 76] Dahl, V. and Sambuc, R.: Un systeme de banque de donnees en logique du premier ordre, en vue de sa consultation en langue naturelle, Groupe d'Intelligence Artificielle, Marseitte-Luminy, September 1976. [Dijk 72] Dijkstra, E.W.: Talks on Programming Methodology; Advanced Course on Systems Architecture, Grenoble 1972 [memo EWD 356]. [Floy 67] Floyd, R.W.: Assigning Meanings to Progarms, Proceeding of Symposia in Applied Math, 1967. [Herm 70] Hermes H: Term Logic with Choice Operator, Lecture Notes in Mathematics, no. 6, Springer Berlin 1970. [Hend80] Henderson, Peter: Functional Programming Application and Implementation, Prentice Hall International Series in Computer Science, Englewood Cliffs, 1980. [Hewi 69] Hewitt, C: PLANNER; A Language for Proving Theorem in Robots, Proc IJCAI, Washington, D.C, 1969. [Hoar 69] Hoare, C.A.R.: An Axiomatic Basics for Computer Program, Communication of ACM, 1969. [Kand 83] Kanda, A; Abramson, H. and Syrotiuk, V.: A Functional Programming Language Based on Data Types as Context Free Grammars; (submitted for publication), December 1983. References 93 [Kowa] Kowalski, Richard: History of Logic Programming. [Kowa 79] Kowalski, Richard: Logic for Problem Solving, North Holland, Amsterdam, 1979. [Malu 81] Malusynski, J and Nilsson, J.: A Notion of Grammatical Unification Applica-ble to Logic Programming Languages, Department of Computer Science, Technical University of Denmark, Doc, ID 967, August 1981. [Mann & Wald 77] Manna, Zoher & Waldinger, Richard: Studies in Automatic Programming Logic, Artificial Intelligence Series, North Holland, New York, 1977. [Shapl 83] Shapiro, E.A.: A Subset of Concurrent Prolog and its Interpreter, TR3, Insti-tute for New Generation Computer Technology, January 1983. [Shap2 83] Shapiro, E.A.; Takeuchi Akikazu:Object Oriented Programming In Con-current PROLOG; Journal of New Generation Computing, Volume 1, Number 1, 1983. [Stoy 77] Stoy, Joseph E.: Denotational Semantics: The Scott Strachey Approach to Programming Language Theory, MIT Press, Cambridge, Masachucetts 1977. [Suss, Wino & Char] Sussman, Gerald Jay, Winograd, Terry and Charniad, Eugene: Micro-PLANNER Reference Manual. [Suss, McDe 72] Sussman, G.J., McDermott, D.V.: Why Conniving is Better than Planning, AI Memo No 255, MIT Project Mac April 1972. [Tenn 81] Tennet, R.D.: Principle of Programming Languages, Prentice Hall Interna-tional Series in Computer Science, Englewood Cliffs, 1981. [Voda 83] Voda, P.J.:R-Maple: A Concurrent Programming Language Based on Predi-cate Logic, Part I: Syntax and Computation; Technical Report of Depart-ment Computer Science UBC, Vancouver, August 1983. [Vodal] Voda, P.J.:F-Maple: A Simple Typed Extensible Functional Programming Language Designed as an Operating System (in preparation). [Voda & Yu 84] Voda, P.J. and Yu, B.: RF-Maple: A Logic Programming Language with Functions, Types, and Concurrency, Proc International Conference on Fifth Generation Computer Systems, Tokyo, November, 1984. References 94 [Voda2 84] Voda, P.J.: A View of Programming Languages As Symbiosis of Meaning and Control, Technical Report of Department Computer Science, UBC, Van-couver, May, 1984. [Warr74] Warren, David H.D.: Warplan: a system for generating plans, DCL Memo 76, Dept. of Al, Edingburgh, June 1974. [Warr77] Warren, David H.D.: Implementing PROLOG - Compiling Predicate Logic Programs, Vol. 1, DAI Research Report { 39 } under , 1977. [Warrl77] Warren, David H.D.: Compiler writing and Logic programming, forthcoming report, Dept. of AI, Edingburgh, 1977. ..95 Appendix A Concrete Syntax of R-Maple Numerals, Constants, Variables, Predicates and Expressions in BNF notation The BNF rules for numerals are as follows. N u m : : = D i g i t | N u m D i g i t D i g i t : : = 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 I d e n t : : = L e t t e r | I d e n t L e t t e r | I d e n t D i g i t L e t t e r : : = a \ b \ c \ d \ e \ f \ g \ h \ i \ j\k\l\m\n\o\p\q\r\ 8\t\u\v\w\x\y\z Constants are identifiers different from reserved words. Initially there is only one constant in R-Maple: C o n s t : : = nil BNF productions for program predicates are as follows. P r e d : : = C l e t t e r | C l e t t e r D i g i t | C l e t t e r I d e n t C l e t t e r A \ B \ C \ D \ E \ F \ G \ I \ J \ K \L \M \N \ 0 \P \ Q \R \S \ T\U\V\W\X\Y\Z BNF productions for expression are as follows. E x p r : : = M e x p r | M e x p r + E x p r | M e x p r - E x p r M e x p r : : = S e x p r | S e x p r X M e x p r | S e x p r d i v M e x p r | S e x p r r e m M e x p r S e x p r : : = V a r | N u m | C o n s t | [ E x p r , E x p r s ] | C o n s t ( E x p r s ) | D e s c r | ( E x p r ) D e s c r : : = . P r e d | . P r e d ( E x p r s ) E x p r s : : = E x p r | E x p r , E x p r s .. 96 Appendix B Concrete Syntax of R-Maple Programs in BNF notation Programs consist of decisions ( i f ), searches ( find ), disjunctions ( or, o r p ), conjunctions (" ; " , " || "), negations ( n o t ), invocations, com-parisons, assignments ( := ), success ( T ), and failure ( F ). P r o g : : = D p r o g | i f P r o g t h e n P r o g else P r o g | find D e c l s i n P r o g | D p r o g : : = C p r o g j C p r o g or D p r o g | C p r o g o r p D p r o g C P r o g : : = S p r o g | S p r o g ; C p r o g | S p r o g || C p r o g | S p r o g : : = T | F | n o t S p r o g j S p r o g ! | A t o m p | V a r : = E x p r | ( P r o g ) A t o m p : : = I n v o c | E x p r R e l o p E x p r R e l o p : : = e q | n e | l t | le j g t | ge I n v o c : : = P r e d ( E x p r s ) | P r e d ( E x p r s o p t | V a r ) E x p r s o p t : : = E x p r s | D e c l s : : = D e c l | D e c l j D e c l s D e c l : : = V a r | S v a r s : = E x p r | P r e d ( E x p r s o p t | S v a r s ) S v a r : := V a r | [ S v a r , S v a r s ] S v a r s : : = S v a r | S v a r , S v a r s The BNF production for concrete syntax of predicate definitions is as fol-lows: D e f : : = P r e d ( S v a r s ) is P r o g | P r e d ( S v a r s o p t | V a r ) i s P r o g | C l a u s e s S v a r s o p t : : = S v a r s | 97 Appendix C Transformational Schemas for Computation of R-Maple Programs Transformation for the invocation of predefined predicates Lt, Le, Gt, and Ge are as follows: Ordering Trans/ormation ( P r e d = Lt ,Le ,Gt ,Ge ): P r e d (<pairop ,<quoteop ,\At{> ,<quoteop ,Lit2>> )! => I T ! if P r e d * ( L i t ^ L i t o ) v F ! othenvise Transformations for test for equality are as follows: ^ ( E x p r ^ E x p r J ! = > Identity Transformations: E x p r i , E x p r 2 are not variables Eq ( E x p r 2 , E x p r 5 ) ! || Eq ( E x p r 3 , E x p r 6 ) ! T! F ! if E x p r 1 * = < E x p r 2 * , E x p r 3 * > & E x p r 4 = < E x p r 5 * , E x p r 6 * > E x p r j * — nil & E x p r j* = nil otherwise Ne ( E x p r 2 , E x p r 5 ) ! o r p Ne ( E x p r 3 , E x p r 6 ) ! F ! T ! if E x p r 1 * = < E x p r 2 , E x p r 3 > & E x p r 4 * = < E x p r 5 * , E x p r 8 * > E x p r ^ = nil & E x p r 4 * = nil otherwise Transformation for the invokation of the predicate Print as follows: Ne ( E x p r 1 ( E x p r 4 ) ! = > Print Trans f ormation : Print (<quoteop , L i t > ) ! = > T ! The transformation schema for arithmetic operations is as follows: Arithmetic Transformations ( P r e d = Add , Sub ,Mul ,Div , Rem ): A p p e n d i x C 98 P r e d (<quoteop , L i t > | V a r ) ! = > f T ! w h e r e V&r:=< quote op ,Lit x> if P r e d * ( L i t , L i t i ) l F ! if 3a P r e d * ( L i t , a ) In the case of user defined predicates, invocation of predicates is transformed as follows: Attribution Transformation ( P r e d is def ined t n D e f s ) : P r e d ( E x p r ) ! = > P r o g { V a r : = E x p r } ! assuming the definition of Pred is Pred ( V a r ) i s P r o g Other unconditional schemas of transformation are: Negation Scheduling: ( n o t P r o g ) ! = > n o t ( P r o g !) Conjunction Scheduling: ( P r o g ^ P r o g 2 ) ! = > P r o g j ! ; P r o g 2 ( P r o g l || P r o g 2 ) ! = > P r o g j ! ; P r o g 2 ! Disjunction Scheduling: ( P r o g ! o r P r o g 2 ) ! = > P r o g ! ! o r P r o g 2 ( P r o g j o r P P R O 8 2 ) • = > P r o S i • o r P P R O S 2 ' Truth Table Transf ormations : n o t ( T !) = > F ! n o t ( F !) ==> T ! T !; P r o g = > P r o g ! T ! || P r o g = > P r o g F !; P r o g = > F ! F ! || P r o g = > F ! P r o g || T ! = > P r o g P r o g II F ! = > F ! F ! o r P r o g = > P r o g ! F ! o r p P r o g = > P r o g T ! o r P r o g = > T ! T ! o r p P r o g = > T ! P r o g o r p F ! = > P r o g P r o g o r p T ! = > T ! f i n d V a r i n T ! = > T ! find V a r i n F ! = > F ! Appendix C 9 9 Transformation for if-then-else is as follows: Scheduling o f Decisions: ( i f P r o g ! t h e n P r o g 2 else P r o g 3 ) ! = > i f P r o g j ! t h e n P r o g 2 else P r o g 3 Transformations o f Decisions: i f T ! t h e n P r o g 2 else P r o g 3 = > P r o g 2 ! i f F ! t h e n P r o g 2 else P r o g 3 = > P r o g 3 ! Transformation for the split operation is: Split Transformation: V a r ^ V a ^ not free m E x p r ; E x p r not variable ( find [ V a r ^ V a r o ] : = E x p r i n P r o g )! = > P r o g { V a r ! : = : E x p r i } { V a r 2 : = E x p r 2 } ! if E x p r * = < E x p r j * , E x p r 2 > F ' otherwise Transformation for the find operation is as follows: Search Scheduling: ( f i n d V a r i n P r o g ) ! = > find V a r i n P r o g ! Transformation for the predicate Return is as follows: Return (Expr \ Var ) => bfindss a i n ( V a r : = E x p r ; T ) o r F Transformation for the b f i n d operation when a value needs to be moved back to its corresponding find is as follows: find y i n ( b f i n d a i n (x : = e a n d P r o g ! ) o r P r o S 2 ) = > ( b f i n d a,y i n (x : = e a n d P r o g j ) o r ( f i n d y i n P r o g 2 ) ) find x i n ( b f i n d a i n (x : = e a n d P r o g ^ o r P r o g 2 ) = > ( f i n d a i n P r o g j z : = e } ) o r ( f i n d x i n P r o g 2 ) where P r o g ! == P r o g ! unless a n d = ; . In the latter case, P r o g j == P r o g ! { b f i n d a i n (ar : = e ) a n d P r o g ! ) o r P r o g 2 } o r ! P r o g 3 = > b f i n d a i n {(ar : = e ) a n d P r o g j } o r ( P r o g 2 OTX P r o g 3 ) where o r = o r and P r o g 2 == P r o g 2 unless o r j == o r p . In the latter case Appendix C .. 100 o r = o r p and if o r = o r (sequential or), then P r o g 2 = P r o g 2 !. { ( b f i n d a i n (x :=e) a n d P r o g j ) o r P r o g 2 } a n d ! P r o g 3 = > b f i n d a i n {x:=e) a n d ( P r o g j a n d j P r o g 3 ) } ofl ( P r o g 2 a n d x P r o g 3 ) Some of the bound variables in a must be renamed yielding 3, x, e, and P r o g j should a free variable of P r o g 3 become bound inside b f i n d a. a n d = a n d , o r = o r , P r o g j = P r o g j , and P r o g 2 = P r o g 2 unless a n d j = |[ . In the latter case, a n d = j| and or = o r p . If also a n d = ; , then P r o g ! = Prog l!. Similarly, if o r = o r , then P r o g 2 = P r o g 2 !. Appendix D Correspondence of Abstract Syntax with Logic < trueop ,nil >* = Vx x —x </alseop ,nil >* = 3 i x j£x <attrop ,predop , P r e d , E x p r > * = P r e d * ( E x p r * ) <ifop , P r o g 1 , P r o g 2 , P r o g 3 > * = ( P r o g j * & P r o g 2 * ) V ( - . P r o g l * & P r o g 3 * ) < findop ,varop , V a r , P r o g > * = 3 V a r * P r o g * <.splitop ,varop , V a r ! , v a r o p V a r 2 , E x p r , P r o g > * = 3 V a r , * 3 V a r 2 * ( < V a r i * , V a r 2 * > = E x p r * & P r o g * ) <orsop , P r o g 1 ( P r o g 2 > * = P r o g ! * V P r o g 2 * <orpop , P r o g 1 , P r o g 2 > * = P r o g j * V P r o g 2 * <andsop , P r o g 1 , P r o g 2 > * = P r o g ] * & P r o g 2 * <andpop , P r o g ! , P r o g 2 > * = P r o g j * & P r o g 2 * < notop , P r o g > * = - i P r o g * Appendix E Abstract Syntax of R-Maple Trueop and falseop have the following structure: trueop \ / falseop \ / Quoteop and varop have the following structure: quoteop varop y N u m { / N u m \/ Notop and pairop have the following structure: notop P r o g pairop E x p r , | E x p r 2 Andsop and andpop have the following structure: Appendix E 103 andsop andpop P r ° g < P r o g , P r o S l P r o g ? Orsop and orpop have the following structure: orsop \ y orpop P r o g , P r o g , P r ° g i P r o g o Attrop and findop have the following structure: attrop | , findop predop varop \y N u m | ,\ N u m E x p r P r o g Ifop and splitop have the following structure: Appendix E 104 ifop splitop varop P r ° g i N u m \ , Prog .? I P r o g ; varop N u m , E x p r P r o g Whereop has the following structure: w h e r e XL. a varop N u m E x p r P r o g , I P r o g o
- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- Implementation of a logic programming language : R-Maple...
Open Collections
UBC Theses and Dissertations
Featured Collection
UBC Theses and Dissertations
Implementation of a logic programming language : R-Maple and its extension to include functions Yu, Benjamin 1984
pdf
Page Metadata
Item Metadata
Title | Implementation of a logic programming language : R-Maple and its extension to include functions |
Creator |
Yu, Benjamin |
Publisher | University of British Columbia |
Date Issued | 1984 |
Description | The use of logic as a language for communication with computers has been exploited in various research areas. R-Maple is a logic programming language, designed by Paul Voda, which improves on some of the short-comings of Prolog. The implementation details of R-Maple will be discussed. R-Maple is a relational programming language which has relations as its basic objects. It can be extended to include functions to form a functional and relational programming language. The advantage is to increase readability and efficiency during computation. RF-Maple is such a language which results from combining the features of R-Maple with a functional language F-Maple. The semantics of RF-Maple needs to be defined formally. The currently available methods of formalizing the semantics of a programming language are either too complex or insufficient for the task. The theory of pairs [Voda2 84] can be used in formalizing the semantics of RF-Maple. However, introduction of types to the theory is not straight forward. Hence RF-Maple is modified to become a typeless language and its semantics is defined using the theory of pairs. |
Genre |
Thesis/Dissertation |
Type |
Text |
Language | eng |
Date Available | 2010-05-17 |
Provider | Vancouver : University of British Columbia Library |
Rights | For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use. |
IsShownAt | 10.14288/1.0051884 |
URI | http://hdl.handle.net/2429/24798 |
Degree |
Master of Science - MSc |
Program |
Computer Science |
Affiliation |
Science, Faculty of Computer Science, Department of |
Degree Grantor | University of British Columbia |
Campus |
UBCV |
Scholarly Level | Graduate |
AggregatedSourceRepository | DSpace |
Download
- Media
- 831-UBC_1984_A6_7 Y9.pdf [ 4.87MB ]
- Metadata
- JSON: 831-1.0051884.json
- JSON-LD: 831-1.0051884-ld.json
- RDF/XML (Pretty): 831-1.0051884-rdf.xml
- RDF/JSON: 831-1.0051884-rdf.json
- Turtle: 831-1.0051884-turtle.txt
- N-Triples: 831-1.0051884-rdf-ntriples.txt
- Original Record: 831-1.0051884-source.json
- Full Text
- 831-1.0051884-fulltext.txt
- Citation
- 831-1.0051884.ris
Full Text
Cite
Citation Scheme:
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>
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-0051884/manifest