D IAGRAMMES A. C. R EEVES Towards a sketch based model of self-interpreters Diagrammes, tome 33 (1995), p. I -178 © Université Paris 7, UER math., 1995, tous droits réservés. L’accès aux archives de la revue « Diagrammes » implique l’accord avec les conditions générales d’utilisation (http://www.numdam.org/legal.php). Toute utilisation commerciale ou impression systématique est constitutive d’une infraction pénale. Toute copie ou impression de ce fichier doit contenir la présente mention de copyright. Article numérisé dans le cadre du programme Numérisation de documents anciens mathématiques http://www.numdam.org/ DIAGRAMMES VOLUME 33 ,1995 TOWARDS A SKETCH BASED MODEL OF SELF-INTERPRETERS A. C. Reeves Abstract There has been a steady stream of research into compiler génération Systems since the late 1960's most of which has involved some sort of approach where the user spécifies the source language, the target language and the source —> target relationship. This spécification of the source —• target relationship is, in effect, a spécification of the compiler and the correctness of the generated compiler dépends on the correetness of this relationship. In this thesis we propose an approach, based on partial évaluation, which does not involve the spécification of the source -• target relationship. Correetness of the generated compflers therefore dépends solely on the spécification of source and target languages and upon the soundness of the theory underlying the technique. The method requires the automatic dérivation of both a target partial evaluator and a source interpréter, expressed as a target program. We attempt the development of a technique to calculate a self-interpreter, an £ interpréter which is itself an C program, for an arbitrary language, £, as this represents a significant step towards the goal of the automatic dérivation of both partial evaluators and interpreters. Initially we examine an algebraic model of language which allows us to specify the function which an interpréter for the language £ computes, solely in terms of the algebraic spécification of the language £. The interpréter is described as the composition of a pair of functions, learn : Semantics -* Syntax which forms part of the algebraic spécification of £, and eval : Syntax —• Semantics which arises naturally from the language spécification due to the properties of the category of algebras over a common signature. Using the algebraic model of language the composition learn o eval, which is the £ interpréter function, does not lie within the semantics of £ and therefore cannot easily be used to construct the £ self-interpreter. For this reason a category theoretic model of language based on finite limit sketches is developed. This model is similar to the algebraic model above and shares many of its properties but has the advantage that learn is expressed as an indexed family of arrows from SET, the category of sets, and that eval is a natural transformation whose components also lie within S E T . As a resuit of this the components of learn o eval can be brought within the semantics of £. We can then use the structure of the natural transformation eval to construct an implementation of learn o eval as an £ program. For Charles and Isobel. Nobody could hâve better friends, I am extremely lucky to hâve you as parents. m Acknowledgements Over the course of the last five years I hâve received help and encouragement from numerous people both inside the Computing departments at Stirling and Keele Universities and outside them. This support, not always with the technical problems in this work, has been of indescribable value to me and I would like to thank you ail. Several people deserve spécial mention. First and foremost Charles Rattray, my friend and supervisor, whose support and encouragement, not to mention his, to my mind, irrational belief in me has not only kept me sane but has helped to make this work something it could not otherwise hâve become, completed. Teodor Rus deserves spécial mention for taking the time to discuss both his own work in the context of mine and my work in the context of his. As do Christian Lair and Laurent Coppey, whose boundless enthusiasm and penetrating questions helped to keep alive my interest in this work. I would like to thank David Budgen both for making it possible for me to attend "Journées esquisses et types de structures" in Paris and for his encouragement over the time I hâve been at Keele. Thanks should also go to Jim Cowie, whose encouragement and comments on the initial drafts finally got me to admit that I could actually start writing this document, and to Mike Johnson who explained Kan extensions to me in a way I could understand. The discussions I had with Samuel Kortas, Simon Jones, John Launchbury, Richard Quatrain, and Peter Sestoft helped no end in improving my understanding of the problems I was trying to solve. Sam Nelson and Graham Cochrane deserve my thanks both for the excellent Computing facilities and support and for being prepared to explain those facilities to me and listen to my explanations of this work with a patience that I will never understand. The office cricket club: Dave Harrison, Andrew Sinclair, and Paul Williamson not only helped me to survive the trials and tribulations of life as a Ph.D. student but also provided useful feed-back via many discussions. iv On a personal note I would also like to thank my friends Maria Shaw, Bill Stewart, Sarah Willis-Culpitt, Tony Douglas, Andy Poxon. Anne Tweed, the other irregulars, and Aunty Eleanor for being there when I needed them and for understanding when I was too busy. Without you this thesis would never hâve reached (been battered into) submission! Contents Contents vi 1 A Brief Introduction and Guided Tour 1 2 Compiler Génération: A Science Fiction Story 4 2.1 The factual basis of the story 6 2.2 3 2.1.1 Syntax directed compiler generators 6 2.1.2 Semantics directed compiler generators 7 2.1.3 Algebraic directed compiler generators 9 2.1.4 Compiler génération by partial évaluation 10 A true compiler génération System 16 2.3 Fiction to fact: the requirements 18 An Algebraic Approach to a Self-Interpreter 20 3.1 An algebraic model of language 20 3.1.1 The spécification basis 21 3.1.2 The semantics algebra 21 vi 3.2 4 22 3.1.4 The learn and eval functions 23 3.1.5 Example: a language of numbers and additfon 24 The interpréter function 27 32 4.1 Définitions 32 4.2 Example: lists 37 4.2.1 The sketch of lists 38 4.2.2 The semantics of List 41 Sketch morphisms and induced functors 45 A Categorical Model of Language 50 5.1 Using sketches to model language syntax 50 5.2 Using sketches to model language semantics 56 5.3 A categorical model of language 59 5.3.1 A categorical spécification of language 59 5.3.2 The language of natural numbers and addition 60 5.4 6 The syntax algebra Sketches 4.3 5 3.1.3 Describing language features using the model 66 5.4.1 A simple type scheme 66 5.4.2 The semantics 71 A Categorical Approach to a Self-Interpreter vii 72 7 6.1 Construction of the self-interpreter 72 6.2 Moving into the semantics 75 6.3 The self-interpreter 77 Concluding Discussion 87 7.1 Summary 87 7.1.1 The model of language 88 7.1.2 The self-interpreter construction technique 91 7.2 7.3 Partial evaluators and interpreters 93 7.2.1 Partial evaluators 94 7.2.2 Interpreters 95 7.2.3 The true compiler generator 96 7.2.4 Open questions 99 More science fiction: a better model of language? 102 Bibliography 104 A Example: A Toy Self-interpreter 113 A.l The syntax of Toy 113 A.1.1 A sketch of the Toy syntax — Toysyn 115 A.1.2 The initial model ISyn : ToySyn 117 A.2 The semantics of Toy -> SET 119 A.2.1 The sketch ToySem 119 viii A.2.2 The initial model ISem : ToySem — SET A.3 The eval and learn transformations 145 156 A.3.1 The sketch morphism E : ToySyn —• Sem 157 A.3.2 The model Em{IStm) 158 A.3.3 The eval natural transformation 163 A.3.4 The learn transformation 164 A.4 A Toy datatype to represent Toy programs 164 A.5 The Toy self-interpreter 167 A.5.1 The interpréter function 167 A.5.2 The rep.interpréter function 170 A.6 The self-interpreter program 175 IX Chapter 1 A Brief Introduction and Guided Tour This dissertation describes a method for calculating self-interpreters for arbitrary programming languages, i.e. an interpréter for the language C which is an C program. On the face of it an C self-interpreter, C-self-int, is a singularly useless program, it cannot provide an implementation of the language C because an implementation of C is required before C-self-int can be run. Even then C-self-int can only make C programs run slower by adding an extra layer of unnecessary interprétation to the implementation. So what is the purpose of an C self-interpreter? The calculation of C-self-int is a step towards the ability to calculate an interpréter, int, for C as a program in the arbitrary language T. Calculation of C-self-int is also a reasonable starting point if we wish to calculate the partial evaluator mix [Ersh82, Jone88] for the language £. Given the ability to calculate int and mix for arbitrary languages we can construct a compiler génération System which requires no user input other than the spécifications of the source and target languages. In chapter 2 we set the scène by outlining the development of compiler-compilers and make the distinction between a compiler spécification language which requires the user to specify the relationship between the source language S and the target language T, and a true compiler génération System which requires no such spécification of the S —> T relationship. We attempt to show that a true compiler génération system can be constructed based on partial évaluation and the ability to calculate the appropriate int and mix programs for the languages S and T. The main purpose of chapter 2 is to motivate the subséquent chapters which deal with the calculation of C-self-int. The algebraic model of language developed by Rus [HaRu76, Rus76, RuHe84, Rus85, Rus87, Rus90, Rus92] is discussed in chapter 3. Using this model of language it is possible to describe the function computed by C-self-int in terms of the spécification of C. The function interpréter, computed by C-self-int is described as the composition of certain functions which form part of Rus' algebraic model. There is no obvious way to turn the interpréter function into an C program because the functions used to describe it are not within the semantics of C. In spite of this the algebraic approach is not a complète blind alley, it provides a gentle introduction to the category theoretic approach used subsequently. In chapter 4 we describe aspects of the theory of sketches [Ehre68] which are used in chapter 5 to construct a categorical model of language which has similar properties to Rus' algebraic model of language. For reasons of space we hâve assumed that the reader is familiar with basic category theory, an understanding of (at least) the concepts of category, functor, natural transformation, and adjunction are required before reading further. Readers unfamiliar with category theory are referred to [BaWe90, Gold84, Macl71, RyBu88]. We describe a categorical model of language based on sketches in chapter 5 and discuss some of its implications for the way in which we specify certain language constructs. Chapter 6 concerns the dérivation of a self-interpreter. Using the categorical model of language the function computed by C-self-int is described as the pointwise composition of a pair of indexed collections of arrows in the category of sets and functions. Thèse collections can be calculated from the sketch spécification of the language C. This version of the interpréter function also lies outside the semantics of C but, because it is structured as a collection of arrows in SET, we can construct an analogue of each component arrow of the interpréter function which acts on a représentation of the syntax of C and is within the semantics of C. This allows us not only to convert the interpréter function into an C program but also, at least partially, to formalise the notion of expressive power required for C to express C-self-int We do not attempt to dérive a représentation of the syntax of £ as an £ datatype as this is a relatively trivial problem. The final chapter, chapter 7, re-examines the method used to calculate the self-interpreter, points out some of its shortcomings, and suggests possible extensions to allow the calculation of partial evaluators and interpreters. Finally appendix A contains an example of the calculation of a self-interpreter. Chapter 2 Compiler Génération: A Science Fiction Story The compiler génération system described in this chapter is a work of fiction but, in common with many other science fiction stories, its roots are firmly planted in science fact. Since the birth of formai language spécification attempts hâve been made to produce Systems which generate compilers from formai descriptions of the source and target languages. A conventional compiler génération system requires the user to specify the relationship between the source and target languages h addition to the source and target languages themselves, see figure 2.1. user specified S-+T relationship source language spécification (S) Compiler- Compiler S —• T compiler target language spécification (T) Figure 2.1: A conventional compiler spécification system Given this fact, conventional compiler génération Systems could perhaps be more correctly described as compiler spécification languages. The major drawbacks of the approach are: 1. the spécification of the S —> T relationship requires a great deal of time and effort. 2. If the user incorrectly spécifies the S —• T relationship, the compiler-compiler will usually generate an incorrect compiler. As a resuit if the user wishes to guarantee the correetness of the generated compiler they must prove the correetness of their S —> T relationship [BuLa69, Morr73, ThWW80, Wand80, C0II86]. This proof is likely to be rather involved and just as prone to errors as the original spécification of the S —* T relationship. The process could perhaps be improved somewhat by providing machine assistance for the correetness proof. but even then the process of compiler spécification is still a long and involved task. A true compiler génération system, in the opinion of the author, should require no user input other than the spécifications of the source and target languages. source language spécification (S) Compiler- Generator S —• T compiler target language spécification (T) Figure 2.2: A True Compiler Generator If such a system had a sound basis in mathematics it would not only provide considérable savings both in user time and effort but would also generate compilers which could be guaranteed correct by construction. The remainder of this chapter attempts to answer the question, uHow could a true compiler génération system operate?" 2.1 The factual basis of the story Before attempting to answer the question above we should examine the main approaches to the implementation of compiler spécification languages which are currently available. 2.1.1 Syntax directed compiler generators Probably the simplest form of compiler spécification system is the syntax directed compiler generator. Using this technique the source language is specified as a context free grammar. A semantic action is associated with each production rule of the source grammar and the compiler is produced by generating a parser for the source language. The parser is constructed in such a way that it exécutes the semantic action associated with a production rule whenever it recognises a phrase generated using that production rule. One of the first attempts to produce a syntax directed compiler generator was the STAGE2 system [Wait70]. Other examples of syntax directed compiler generators include YACC [John78], DELTA [Lorh82], and SYNTAX [Boul80]. Of thèse YACC is probably the most generally available as it is distributed as part of the UNIX1 operating system. The most obvious shortcoming of the syntax directed technique is that the semantic action associated with a production rule does not describe either the semantics of the source language phrase, or the target language construct used to implement the source language phrase. In fact the target language of the generated compiler is not specified at ail using the syntax directed approach. What the semantic action actually spécifies is the action to be taken by the generated compiler on recognising the source phrase associated with each action. This effectively obscures the S —• T relationship by hiding it within the implementation détails of the compiler, making its construction and correetness proof much harder. Since the only objects which are formally specified are the source syntax and (in some cases) the meta-language used to express the compiler spécification, the correetness proof requires a great deal of additional information: i.e. source semantics, target syntax, and target semantics. The requirement for additional information also makes the correetness proof much more difficult. It could be argued that the requirement for additional information makes the ! UNIX is a trademark of AT & T Bell Laboratories syntax directed compiler spécification technique a semi-formal compiler spécification method rather than a formai one. 2.1.2 Semantics directed compiler generators A second approach to compiler spécification is the semantics directed compiler génération technique. Compiler writing using this approach is based on a formai description of the source language as input data, and the target language as output data. Usually the source language is described as a context free grammar where each source phrase has an associated target language construction which describes its semantics. The détails of compiler spécification vary from system to system but, in gênerai, aJl semantics directed compiler spécification Systems conform to one or other of the approaches given in [Moss76]. "Choose a fcuniversaT object code with a well defined semantics. Then to generate a compiler from a given denotational semantics for some programming language. find code séquences which simulate the abstract meanings of the phrases of the language. and construct a compiler which produces thèse code séquences" or "Take a more abstract view of compiling: instead of Compiler : progs —* code consider Compiler : progs —>input-output-fns. Thus an abstract compiler does not transform an (abstract) program text into an (abstract) séquence of instructions; rather it transforms it into the abstract input-output-fn represented by those instructions. The concrète version of such an abstract compiler produces denotations (i.e. représentations) of input-outputfns from denotations of programs — it is just an implementation of a denotational semantics." Although Mosses was referring specifically to semantics directed compiler spécification Systems based on denotational semantics the same thing applies to Systems based on attribute grammars [Boch78] or on algebraic semantics [Desc82]. Most commonly semantics directed compiler generators are based on the denotational approach to programming language semantics [ScSt71, Stoy77, Schm86], and there is a great deal of literature dealing with this type of semantics directed compiler spécification system, for example: [Ganz79, Moss79, RaTu79, JoSc80, Schm85, Wand85, Roye86, Vick86]. Of thèse [Roye86] is of particular interest because it attempts to dérive a target semantics from a source denotational semantics in, "the most constructive way possible." The technique described by Royer is still a compiler spécification technique rather than a true compiler génération system because the user has to supply the S —• T relationship in the form of a collection of target domains which are used to implement the source domains, together with a congruence relation for thèse domains. In [Schm85] Schmidt also constructs a semantics directed compiler directly from the standard denotational semantics of a programming language rather than a continuation style denotational semantics as is more usual. This has the advantage that the semantics used to specify the programming language is at a much higher level. The approach used is to transform the semantics so that operational properties of the semantics become clearer. The transformations used are focussed on the operational properties of the particular réduction strategy used to implement an interpréter for the denotational semantics définition. Using this technique the implementor has to supply rather more information about the S —> T relationship than is the case if a continuation semantics were used. This may in fact be an advantage because the user can use implementation "tricks" to produce a much more optimal implementation, however; it also moves further away from the goal of this chapter. The compiler spécification system described in [JoSc80] consists of a back end compiler

Semantics associa- tion is specified by the function learn : Sem(E) — 5yn(E) and by the initiality of 5yn(E), which gives rise to an homomorphism eval : Syn(E) —• 5em(E). If S is a programming language specified over Ei and T is specified over E2 then a compiler C : S —• T is specified as a pair of homomorphisms, compile and encode, such that the équations both hold in figure 2.3. encode = era/2 o compile o learn\ compile = eval\ o encode o /earri2 ,^ v 5yn(Ex) learn\ compile £ eval\ 5em(El) * Syn(E 2 ) learn2 l^de evalo " 5em^2) Figure 2.3: The algebraic directed view of a compiler In the T.I.C.S. System the S -* T spécification takes the form of a set of parameterised macro expressions, one for each opération in Ei. Each macro expression is the target code to be used to implement the source opération. Compilation begins by identifying patterns in the source string which correspond to the generators of Syn(H{) and replacing them by their target représentations. On the subséquent passes through the source string the compiler attempts to identify source opérations whose arguments hâve already been replaced by their target représentations. When the compiler recognises such a source opération it uses the embedded target représentations to parameterise the associated macro opération and replaces the source opération by the resuit of the macro expansion. Compilation is complète when there are no source opérations left to translate. In [Reev87] Reeves attempts to show the relationship between this approach and the semantics directed approach by using a tree of partially expanded macro expressions as the intermediate language of a semantics directed compiler spécification system. The algebraic basis of the T.LC.S. System makes the spécification of T.I.C.S. generated compilers particularly amenable to the usual methods for proving the correetness of the S —• T relationship. 2.1.4 Compiler génération b y partial évaluation Partial évaluation [Futa71, Ersh77] or mixed computation can be described informally as the process of "doing as much évaluation as possible with, possibly, incomplète input." If p is a program whose input can be divided into two classes: S - static i.e. input which is fixed at a particular value, and D - dynamic i.e. input which is not fixed and may vary over ail possible 10 values of the correct type, the program p can be evaluated fully only if it is given both S and a particular value of D. If only S is available the process of partial évaluation can be applied to p. The part of the computation of p which dépends only on S is performed. The resuit of this process is a new specialised version of p whose input is the dynamic part of the input of p, D, and which, when it is applied to D, produces the same output as p applied to both S and D. p(S,D) = ps(D) This specialised function ps is known as a residual program. For example consider the function power power x n = = 1, if n = 0 x * power x (n — 1), otherwise This function raises x to the power of n. Suppose the value of n is fixed at 3 but the value of x is dynamic. Spécialisation of power to its static input n = 3 produces the residual program power' x = x *x *x * 1 because ail computation except multiplication by x, which is dynamic, can be performed at partial évaluation time. Beckmann et al [BHOS76] and Futamura [Futa82] describe some of the potential applications of partial évaluation. Thèse include: • Automatic theorem proving. It is possible to use a partial evaluator to produce a spécifie theorem prover by specialising a gênerai theorem prover to a spécifie set of axioms [Futa82]. • Construction of small specialised utility programs from more gênerai routines [BHOS76]. • Construction of spécifie parsers from gênerai parsing routines [Futa82]. If there is a gênerai parsing algorithm P : BNF-grammar 11 x text -» parseJree, and S is the BNF grammar of the language S. A spécifie S parser P$ can be produced by specialising P to S by partial évaluation. • Compilation and compiler génération. This use of partial évaluation is discussed in détail below. In gênerai partial évaluation is a useful technique where there is a need to construct a fast, spécifie, algorithm to do a particular job and a slower more gênerai, data driven, algorithm already exists. Partial évaluation and compilation The use of partial évaluation as a compiler construction technique is described in [Futa71, Ersh77, Ersh82, Futa82, JoSS85, JoSS89]. A brief overview of the technique is shown below. Suppose that mix is a self-applicable partial evaluator for the target language T , i.e. mix is a T program which implements a partial evaluator for the language T. Because mix is a partial evaluator the following équation holds for ail T programs t with static input istatic and dynamic input idynamic tfcstatic, idynamicl = (wïiartt^M^toticDPdynomicl where mix[[*]][[i5taticl is the residual program produced from t and i3tatic Now assume int is an interpréter for the programming language S and is written in the target language C. If s is an S program which takes i as its input and produces o as its output then 4*1 = o represents running the program s on an S machine with input t. The same output can be produced using a T machine by running int and giving it s and î as its input. int^s* i]] = o 12 Since int is a T program and s is some of its input we can use mix to produce a specialised version of int which can only interpret the program 5 by setting s as static input for int and : as dynamic input. int9 = mix[[tnf]][[s]] Now using ints and a T machine we hâve intsrJl = o furthermore ail the computation in int which applies only to the analysis of the program s is done at partial évaluation time and does not hâve to be done when int3 is executed. The T program int3 has the same input/output relation as the S program s and is, in fact, a compiled version of s. Since mtx|[int]|[[$] is a compiled version of s and mix is a T program, an S to T compiler can be produced using mix and int by regarding int as static input for mix and leaving s as dynamic input. comp = fnix[[mîx]]|[in*]] This is easy to verify because: compW = (rotzJmixl[tnt])|[sD = inta lf we remember that the basic function of a partial evaluator is to eliminate redundancy from a partially bound T program it is easy to understand how thèse results arise. By définition an S interpréter, int, must contain the T expressions necessary to exécute any S program with any input data in addition to the T expressions necessary to parse an S program and exécute its static semantics. If the program argument of an interpréter is bound to a particular S program, q, it is possible to exécute the parsing and static semantics components of the 13 interpréter as they only dépend on the S program text. The code segments of the interpréter which actually simulate the run time behaviour of q dépend on the input data for q as well as the program text and therefore become part of the residual program intq. This reasoning extends to the construction of mixint in the obvious manner. Partial évaluation Systems There is a large, and growing, body of literature on the subject of partial évaluation as a compiler génération technique. In [MaBe85] partial évaluation is used to dérive a compiler and an object interpréter from an operational semantics given using the V.D.L. spécification language. However the approach used needs to place several restrictions on the style of V.D.L. spécification and does not appear to généralise to the automatic génération of compiler generators in any obvious manner. The first working version of a fully self-applicable mix was produced by Jones et al [JoSS85, Sest85, JoSS87, JoSS89]. This project identified the process of binding time analysis as critical to the effective opération of a partial evaluator. To spécialise the power function given above to some fixed value of n the partial evaluator need only unfold recursive calls of power until the value of n falls to 0. Now consider the spécialisation of power to some fixed value of x (say 5) rather than n. The obvious spécialisation is power" n = = 1, if n = 0 5 * power"(n - 1), otherwise but this spécialisation cannot be produced by repeated unfolding of recursive calls because the value of n is dynamic and therefore never falls to 0. Spécialisation by repeated unfolding will actually cause non-termination of the partial evaluator as it attempts to produce the infinité residual program shown below. 14 power"1 n = 1, if n = 0 = 5*1, if n - 1 = 0 = 5*5*1, if n - 1 - 1 = 0 = 5* - * 5 * 1 , otherwise The problem arises because the expression power 5 n where n is dynamic is itself dynamic and must not be unfolded at partial évaluation time. To overcome this problem a partial évaluation system must perform a process of binding time analysis on the program to be specialised to détermine which sub-expressions in its body are static (reducible) and which are dynamic (irreducible) at partial évaluation time. In [JoSS85] the binding time analysis is done "by hand", but in later versions the process is automated, ail be it in a fairly ad hoc manner. The treatment of binding time analysis given by Launchbury [Laun88, Laun89, Laun90] using a domain theoretic construction of dépendent sums which allows aspects of binding time analysis to be expressed as domain projections is particularly interesting but for reasons of space cannot be discussed hère. Another interesting example of partial évaluation is the work of Turchin et al [Turc80, TuNT82, Turc85, Turc86] on the supercompiler concept. A supercompiler is a generalised from of partial evaluator. Supercompilation consists of a process called driving in which a T program, p, is run in a generalised form (with unknown values for some of the variables of p) to produce a graph of states and state transitions of the possible configurations of the Computing system specified by p. To keep this driving finite the supercompiler examines the configurations of p and généralises them until a set of generalised configurations are produced which are capable of describing the whole of the Computing system, p. This généralisation process replaces the binding time analysis of the more traditional partial évaluation system. Because the driving and généralisation process has access to more information than a simple partial evaluator a supercompiler can carry out transformations to the program p which are not possible using partial évaluation alone. On the other hand self-application is much harder to achieve because of the increased complexity of a supercompiler. Other work on partial évaluation includes: compilation of pattern matching [Bond88. Jorg90] 15 by partial évaluation. The extension of partial évaluation to lazy functional languages [Bond90b] and partial évaluation of higher order languages [Goma89, Bond90a, Cons90]. Compiler génération by partial évaluation is included as an example of a compiler spécification system where the S —• T relationship is specified as an «S interpréter expressed in the language T. To be a fully formai compiler spécification technique we require formai spécifications of the S and T languages and a formai description of the process of partial évaluation, in order to prove the correetness of mix. In reality the technique is much more powerful than simple compiler génération, it is probably better described as a program transformation technique but in its guise as a compiler spécification system it provides the inspiration for the fictional true compiler generator described below. 2.2 A true compiler génération system By making two, rather large, assumptions we can now take a look inside the "compiler generator" box in figure 2.2 and speculate about its internai workings, based on a partial evaluator. Assumption 1. there is a technique which allows us to examine the spécification of a computer language, T, and from this spécification, calculate a T program which implements mix for the language T. Assumption 2. given the spécifications of two languages, S, and T, it is possible to dérive an implementation of S in the form of an interpréter expressed as a T program. By allowing assumption 1 only, we could implement a compiler spécification language in the following way: 1. examine the target language spécification, T, and compute the implementation of mix for this language. 2. Accept a source interpréter, int, written as a target program and compute the value mix\mix,int\ 16 3. Output the value mix^mix, int^ as the generated compiler. This system is still a compiler spécification system rather than a compiler génération system because the user has to supply the S —• T relationship in the form of the source interpréter, int If we also allow assumption 2 we can implement a true compiler generator system by calculating the source interpréter from the spécifications of S and T, rather than accepting it as input. The proposed overall structure of the "compiler generator" box in figure 2.2 is shown in figure 2.4. source language spécification (S) int calculate int S-+T compiler compute target language spécification (T) calculate mix mix§mix,int§ mix Figure 2.4: The anatomy of a true compiler generator The boxes labelled "calculate mix" and "calculate int" are implementations of assumptions 1 and 2 respectively. The last box, labelled "compute mix^mix,intY is a parameterised Simulator which accepts the following inputs: 1. a language spécification T. 2. A T program which implements mix for the language T. 3. A T program, int, which is a programming language interpréter. When given the spécification of the language T the "compute mix\mix,intY component becomes a T interpréter and computes the value mix^mix,inï§ which it constructs from its 17 remaining inputs. This last component is relatively trivial to construct as it is basically an interpréter for the meta-language used to specify T. 2.3 Fiction to fact: the requirements How unreasonable are the assumptions in section 2.2? The short answer to this question is currently very unreasonable. Taking each assumption in turn, for assumption 1 to be reasonable we need to be able to: 1. construct a représentation of the syntax of an arbitrary language T as a data type of the language T. This is required because mix must hâve some way of representing the T programs it processes. 2. Construct a binding time analysis phase from the spécification of the semantics of an arbitrary language T. 3. Construct the function spécialisation phase for an arbitrary language T. This is probably the easiest of the three requirements necessary to justify assumption 1. The function spécialisation phase of a T partial evaluator is very closely related to the évaluation function of the programming language T and is basically a T program which reduces other T programs to their canonical form with respect to the static input and binding time analysis. The requirements necessary to justify assumption 2 are: 1. given arbitrary programming languages S and T we must be able to construct a T data type which represents the syntax of S. Hère again this is required because the interpréter, int, must be able to represent any S program to process it. 2. The ability to dérive an S interpréter, int, as a T program. To dérive an S interpréter as a T program we must be able to implement the S évaluation function as a T program. We will concentrate on the development of a technique which allows us to calculate a selfinterpreter for the arbitrary language T, i.e. an interpréter for the language T which is itself 18 a T program. The reason for this is that the calculation of a self-interpreter is a reasonable step on the road to both the calculation of an S interpréter as a T program. and toward the calculation of a function spécialisation phase for the language T. The problem of constructing a T data structure to represent the S programs can be reduted to the problem of implementing binary trees in T, since any tree structure can be transformed into a binary tree and any S program can be represented as its dérivation tree. A less efficient but more straightforward représentation technique could be constructed by implementing nary trees in T, where n is the largest number of subtrees possible for a node in the dérivation tree of an S program. From this point on wre will assume that one or other of thèse techniques is used to construct a représentation of S programs as a data type in the arbitrary language T. This will be required for the construction of a self-interpreter, (both S and X are the same language for a self-interpreter). 19 Chapter 3 An Algebraic Approach to a Self-interpreter The algebraic model of language developed by Rus [HaRu76, Rus76, RuHe84, Rus85, Rus87, Rus90, Rus92] can be used to specify a programming language as a triple C = (Sera, Syn, learn : Sem —• Syn) where Sem and Syn are algebraic structures over a common signature and learn is function which associâtes an expression in Syn with eath meaning in Sem. There is an associated homomorphism eval : Syn -• Sem which defines the évaluation of expressions in Syn. The model is described in section 3.1 and in section 3.2 we show how the properties of the model can be used to construct the function computed by a self-interpreter. 3.1 An algebraic model of language Rus describes an algebraic model of language based on two properties of many sorted algebra. Given the category of E algebras C(E): 1. the word algebra W is unique up to isomorphism and coïncides with the initial algebra in C(E). 20 2. Any function defined on the generators of W returning values in the carrier of a similar algebra A extends to an unique homomorphism £ : W —• A. The construction of the model is shown below. 3.1.1 T h e s p é c i f i c a t i o n basis The three components of the spécification basis are: 1. a set of names of the abstract objects specified in the language, denoted by /. 2. A finite set of reserved words denoted by S. 3. A finite set of opération schemes E. The opération schemes, a £ E specify opérations on families of sets (indexed by / ) and are denoted by a triple. a = (n,s0si ...sn,ii...ini) The components of the triple are: • n > 0, the arity of the opération. • The opération symbol SQSI .. .sn, Sj 6 S. • The operand sorts i\.. .in, ij € / and resuit sort of the opération i 6 / . A proof that every context free grammar générâtes a basis B and every finite basis B générâtes a context free grammar is given in [Rus87]. 3.1.2 T h e s e m a n t i c s algebra The semantics of a programming language is given as an algebra specified by some basis B over a family of sets A = { J 4 I , J 4 2 , . . . } . The family A represents the collection of abstract objects which are denotable within the language semantics. Sem(B,A) = (Sem(I), Sem(S), 5cm(E)) is constructed as follows: 21 The algebra 1. Sem(ik) = Ak.ik € / . Sem(I) is then a family of sets chosen from A and indexed by /, allowing Sem{B,A) to be constructed as a many sorted algebra. 2. Sem(S) = 5. The purpose of this set is to fix the symbols used to express constructions over Sem(I). 3. The set of opérations on Sem(I) is denoted by Sem(E) and Va G E,<7 = (n, so^i - - - ^ , i l . . .in*)> Sem(a) is an opération Sem(a) : Sera(z'i) x . . . x Sem(i n ) -• Sem(i) The tuple (s 0 ,si, -. -,sn) is used as the opération symbol and for a* € Sem(ik), k = 1,...,71 Sem(a) applied to appropriate a* is denoted 5 0 ai5ia 2 .. .sn-\ansn and is of sort i. This construction of Sem(B,A) as a many sorted algebra with opération symbols which distribute over their operands provides a very natural association between the semantics algebra and the phrases of a context free grammar. 3.1.3 T h e syntax algebra The set W(X, E) = {W{(X, E), i G / } is the family of well formed expressions freely generated from the family of finite symbol sets X = {Xi, i € / } by the signature E. Détails of this construction are given in [Higg63, Rus90]. The algebra Syn(B,W) = (Syn(I),Syn(S),Syn(T,)) is constructed as follows: 1. Syn(I) = { W i ( X , E ) , i € J } . 2. Syn(S) = 5. 3. The set of opérations on Syn(I) is denoted by 5yn(E) and Va € E,cr = (n, s0si il.. .ini), Syn(a) is an opération Syn(a) = Syn(ii) x . . . x Syn(in) — Syn(i) defined by the rules for well formed expressions in Wi(X,T,) as 22 ...sn, VÎT, G W t j ( X , E ) , j = l,...n,Syn( (Exp) -* (Exp)*(Exp) (2, e'+'e, ExpExpExp) Note that the opération symbol for the third opération scheme contains two occurrences of the empty string e. The spécification basis B is the triple: 24 5 = ( / = {Exp},S = {0,succ(,),+}, E= {(0,iO\Exp),(l,is\iccC)\ExpExp),(2,e^€,ExpExpExp)) Semantics algebra To specify the semantics algebra Sem(B, A) we must first define the family of abstract objects A. The only object required for the semantics is the set of natural numbers, Nat, constructed by the signature below: the family A is therefore A {Sem(Exp)} = = {AExP} = {Nat}, We can now construct Sera(E). {Sem(a),a zéro : -• Nat suce : Nat —> Nat {Nat}. The construction of Sem(I) and Sem(S) is constructed as Sem(S) is Sem(I) = = {0,succ(,),+}. The set of opérations of the algebra Sem(B,A), i.e. G E } , is constructed by the assignment shown in the table below. opération opération signature Sem((W,Exp)) —• Sem(Exp) zéro Sem^UsMCcV'YExpExp)) Sem(Exp) -> Sem(Exp) suce Sem((2, c'+V. ExpExpExp)) Sem(Exp) x Sem(Exp) -• Sem(Exp) / where the opération / : Nat x Nat —• iVa/ is defined as addition on natural numbers. f(zero,x) = f(succ(x),y) = x succ(f(x,y)) Using this assignment the set Sem(E) is defined as Sem(E) = {zéro,suce,/}, this complètes the définition of Sem(B, A). Syntax algebra Since the expression language is generated by a context free grammar, the family W(X, E) for the syntax algebra is freely generated from the family of symbol sets X = {0} by the 25 signature E. Following the rules for the construction of W(X, E) in [Rus90] we obtain an unchanged set S ( X i s the family of empty sets). The set WEXP(X, WExpo(X.Z) = HWX.S) = S) is described below. {0} WExPn_1(X,2)U{siicctwy.w€WEXPn_1(X,'Z)} U{e«;1 + w2e : (w1,w2) € ^ ^ . , ( ^ , 2 ) x WE^^X WExp(X,Z) So W(X,X) = \JWExPn(X,Z),ne = {WExP{X,i:)}. ,Z)} {0,1,2,...} The family Syn(I) is defined as {WExp(X,?,)} and the set Syn(S) is {0,succ(,),+}. The éléments of the set 5j/n(£) are described in the table below. opération signature Syn((0SO\Exp)) opération —• Syn(Exp) 0 5î/n((l, succ(") ,£xp£xp)) Syn(Exp) —• Syn(Exp) 9 Syn((2, e'+'e, Syn(Exp) x Syn(Exp) h t , ExpExpExp)) The opérations g :WExp(X,Z)-+WExp(X,Z) —> Syn(Exp) and /i : WExp(X,X) x W^* P (*,E) -. WExp(X, E) are defined as: g(w) = succ(ttf) h(wi,W2) = CU?I+W2É 5yn(E) is therefore defined as 5yn(E) = {0,5,/1} and the définition of the algebra of words Syn(B,W(X, E)) is complète. The learn and eva/ functions The function learno : Sem0(B,A) -+ Syno(B,W(X,T,)) is defined as: learn0(zero) This function can be extended through the signature E as follows: learn(zero) = zéro learn(succ(a)) = suce (learn(a)) learn(f(ai,a2)) = elearn(ai) + 26 learnfa)*- = zéro. Since the value /(ai,02) is constructed by the opérations zéro and suce for ail values ai,02 G 5em(i4) this définition simplifies to: learn(zero) = zéro learn(succ(a)) = succ(/earn(a)). We can now define the eval homomorphism as follows: 1. define eval0 : Syn0(B,W(X, E)) - • Sem0(B, A) as: eva/ 0 (zero) = zéro. 2. Extend eva/o homomorphically to eval. 3.2 eval(zero) = zéro eval(succ(w)) = succ(era/(tu)) et;a/(eit;i • W2t) = f(eval(w\),eval(w2)) The interpréter function The conventional définition of an C interpréter is a program which, when given an C program / and input i for the C program as its input, produces the same output as / produces when given input i. If the interpréter is itself an C program it is called an C self-interpreter. For the purposes of the algebraic model above this définition must be made a little more précise. Définition: An C self-interpreter. An C self-interpreter is a term int such that: 1. eval(int) is a function interpréter :Q -+ Q, where W(X, E) Ç Q. 2. For every term w G W(X, E), eval(w) = eval(interpreter(w)) and no further réduction of interpreter(w) is possible. O In other words an C self-interpreter is an C program which takes C syntactic terms as input and delivers maximally reduced C syntactic terms as output while preserving the meaning of thèse terms during the réduction process. 27 The algebraic model of language outlined above can be used to describe the interpréter function. Proposition 3.2.1 If C is a programming language: C = (Sem{B, A), Syn(B, W(X, E)), learn : Sem(B, A) — Syn(B, W(X, E))) with évaluation homomorphism: eval : Syn(B, W(X, E)) - Sem(B, A). The interpréter functions for C is defined as interpréter = learn o eval Proof: The eval homomorphism defines an équivalence relation on Syn(B,W(X, E)). Vwi,u;2 G Syn(B, W(X, E)) : ui = u>2 ^ eva/(u;i) = eval(u2) This relation can be used to construct a quotient algebra Syn(B, W(X, E))/= where each élément of Syn(B,W(X,T,))/= is not an C program but the complète collection of ail £ programs which hâve a given meaning. For example, in the expression language above, the équivalence class which contains the term esucc(O) + suce (suce (0))c will also contain the term succ(succ(succ(0))), and ail other terms which evaluate to succ(succ(succ(zero))). This suggests a mechanism for the Computing the interpréter function. 1. Identify the équivalence class containing the term to be specialised. 2. Select a pre-determined term from this équivalence class and use it as the resuit term. There is an isomorphism between Syn(B,W(X,Y,))/= Syn(B,W(X, and Sem(B.A) so if a term w G E)) can be uniquely identified as the preferred syntactic représentation of each 28 élément of Sem(B,A) the interpréter function can be described using the eval homomor- phism. The learn function from the définition of C performs exactly this task and so the function computed by a self-interpreter can be described as: interpréter = learn o eval. • The effect of proposition 3.2.1 is to define a family of functions Fa on the syntax algebra which correspond to the opérations Sem(a) of the semantics algebra, for each a G E. Theorem 3.2.1 For each opération scheme o = (n,s0Si. ..sn,ii. Fa : Syn(ii) x ...x ..ini) G E the function Syn(in) - • Syn(i) defined as Fa = interpréter o Syn[a) has the same behaviour on syntactic objects as Sem(a) : Sem(ii) x . . . x Sem(in) —• Sem(i) has on semantic objects. Proof: Fa is defined as: Fa(wi, ...,wn) for each a = (n,sQsi ...sn,i'i.. = (learn o eval)(Syn(a)(wi,..., wn)) = learn(eval(Syn(a)(wi,..., wn))) = learn(Sem(o)(eval(wi),. ..,eval(wn))) .ini) G E, n > 0. Fa is defined as: Fa = (learn o eval)(w) D for each a = (0, w, i) G E. Returning to the example from section 3.1.5 the interpréter function can be defined as: interpréter = learn o eval. Using theorem 3.2.1, this définition can be expanded as: 29 as indexed collections of arrows whose components can be brought within the semantics of the specified language. 31 interpreter(zero) = (learn o era/)(zero) = learn(zero) = zéro interpreter(succ(w)) interpreter(ewi • W2O = (learn o eva/)(succ(tr)) = learn(succ(eval(w)) = succ((/earn o eva/)(tr)) = s\icc(interpreter(w)) = (learn o ei;a/)(eu;i • u^c) = learn(f(eval(wi), = r eval(w2))) i (2,^e,£:xpErpExp>(^^rPr^er(it;i),interpr6 Syn(Exp) given by theorem 3.2.1 is the syntactic équivalent of the semantic opération / : JVaJ x Nat —• iVa* and is defined in figure 3.1. F(wi, W2) = learn(f(eval(w{), F(zero, it;) = it? .F( suce (wi ),w2) = succC^it?!,^)) eval(w2))) Figure 3.1: The opération F(2,c+c,ExpExpExp) Although the interpréter function is completely described in terms of the définition of the programming language C it is not a description of a self-interpreter for the simple reason that it is not an C program. In fact the interpréter function is not actually an élément of the algebra Sem(B, A) and so there is no guarantee that an C program to compute the interpréter function actually exists. The following chapters describe a categorical model of language based on finite limit sketches [BaWe85]. The categorical model of language exploits the fact that finite limit sketches modelled in the category of sets and functions (SET) exceed the expressive power of many sorted algebraic théories and hâve ail the properties used above. Using finite limit sketches we can therefore construct analogues of the learn and eval functions 30 Chapter 4 Sketches The concept of a sketch originates with Ehresmann and is described in [BaEh68]. Sketches hâve been studied extensively by several groups Worldwide, mainly in France and Canada, and a gênerai introduction to the work can be found in [Ehre68, BaEh68, Lair75, GuLa80, CoLa84, BaWe85, Gray87, \VeBa87, Ba\Ve90]; this list of références is by no means complète. The formalism used hère most closely follows that of Barr and Wells [BaWe85, BaWe90, WeBa87] as thèse are more widely distributed than the majority of the other références. 4.1 Définitions Sketches provide a formai spécification technique based on graphs and, "as such are the intrinsically categorical way of providing a finite spécification of a possibly infinité mathematical object or class of models" [BaWe90] (ppl61). The définition used in [WeBa87] is given below. Définition: Directed Graph. A directed graph, G, is a pair of sets Go — nodes, and Gi — edges, together with two functions: src : Gi —• Go, which returns the source node of a given edge, and function trg : Gi —> Go maps the edges to their target nodes. For example: 32 D • • b c with Go, G i , src, and trg defined as: G 0 = {a,6,c} Gi = {f,g,h} src(f) = a trg(f) = 6 src(g) = b trg(g) = c src(h) = c trg(h) = c. The définition of a sketch requires the définition of a diagram. To define a diagram we must first define a graph homomorphism. Définition: Graph Homomorphism. A graph homomorphism H : G —» E is defined as a pair of functions Hi : G,- —» £,, t = 0,1 such that the following properties hold: Ve G Gi : H0(src(e)) = src(Hi(e)) Ve G Gi : H0(trg(e)) = trg(Hi(e)). That is to say /7 préserves the connectivity of the graph G. D A diagram can now be defined. Définition: Diagram. If d and G are graphs, a diagram of shape d in G is defined as a graph homomorphism D:d-+G. D r n d = G = 9 u 33 D:d-G = (DQ,Di) where D0 and Di are defined as D0(w) = D0(xj - p D0(y) = D0(z) = q Di(f) = Di(j) = s Di(g) = r £1(/1) = t A directed graph and a set of distinguished diagrams in that graph form two of the components of a sketch. The remaining two components are a set of cônes and a set of cocones, defined below. Définition: Cône. A cône in a graph G consists of: 1. a diagram of shape d in G, D : d -• G. This diagram is called the base of the cône. 2. A node v of G, called the vertex of the cône. 3. A family of projection edges p = {p,; : v — D(i)} indexed by the nodes of d. A cône with vertex v and base D is referred to as a cône from v to D or as cône p:v Any cône p:v -> D can be indicated by a diagram of the form 34 -^ D. • In the category C, a cône p : v —• D is a limit cône if it has two additional properties: 1. for every arrow a : i —• j of d, D(a) opi = pj where o is the composition operator of C. A cône with this property is called a commutative cône. 2. If ç : s —• I? is a différent commutative cône there is a unique arrow w : 5 —• v such that Pi o u = qi for ail nodes t of d. In the category of commutative cônes over diagram D, the limit cône is the terminal object. A limit cône over a discrète diagram, in any category, is called a product cône and its vertex is known as the product of the objects in its base. In SET, the category of sets, for example, the vertex of a limit cône over a discrète diagram is the cartesian product of the sets in its base. A cocone is defined to be the dual of a cône. Définition: Cocone. A cocone in a graph G consists of: 1. a diagram of shape dm G, D : d —• G. This diagram is called the base. 2. A node v of G, called the vertex. 3. A family of injections in = {ini ' D(i) -» v} indexed by the nodes of d. D The colimit cocone over diagram D in the category G is defined as the initial object in the category of commutative cocones over diagram D. That is to say, if j : D —• v is the colimit cocone over diagram D : d -+ G and k : D —• s is another commutative cocone over D there is a unique arrow u : v —• s such that fc, = u o j t . In any category the colimit cocone over a discrète diagram is the sum (coproduct) of the objects in its base. In S E T , for example, the vertex of the colimit cocone is the disjoint union of the sets in its base. Thèse définitions of directed graph, diagram, cône, and cocone are combined to give the définition of a sketch. 35 Définition: Sketch. A sketch is a 4-tuple (G, Di,C,Co) consisting of a graph G, a set Di of diagrams on G, a se: C of cônes on G, and a set Co of cocones on G. C Définition: FP Sketch. A sketch is called an FP (finite product) sketch if it contains no cocones and ail cônes are over finite discrète diagrams. C Définition: FL Sketch. A sketch is called an FL (finite limit) sketch if it contains no cocones and ail cônes are over finite diagrams. Clearly every FP sketch is also an FL sketch. C Définition: Sketch Morphism. If Si = (Gi,2)ti,Gi,Coi) and 52 = (G2,£*2,C2,Co2) are sketches then a sketch morphism F : Si —• 52 is a graph homomorphism such that: 1. for each diagram D : d —• Gi in Dii, F 0 D : d —• G2 is a diagram in Di'2. 2. For each cône p : v —• D in Ci, the cône F(p) : F(v) -* F o D belongs to C2. 3. For each cocone j : D —• v oiCoi, the cocone F(j) : F 0 D —» F(v) is a cocone belonging to Co2. C That is to say that F : Si —* 52 takes the diagrams of 5i to diagrams of 52, the cônes of 5i to cônes of 52, and cocones of 5i to cocones of 52Given any category C, there is a sketch underlying C defined as (G, Di, C, Co) where G is the underlying graph of C, Di is the set of ail commutative diagrams of C, C is the set of ail limit cônes of C, and Co is the set of ail colimit cocones. This leads to the final définition in this section. Définition: Model of a sketch. A model of a sketch, S, is a sketch morphism M : 5 -» \V\ where \V\ is the sketch underlying some category V (typically SET). It follows that the diagrams of S will be taken to commutative diagrams of V, and the cônes (cocones) of S will be taken to limit cônes (colimit cocones) of V. C 36 Although M : S -* \V\ is actually a graph homomorphism, it is sometimes convenient to regard it as a functor M : S —• V where S is the free category generated by the sketch 5. The models of a sketch 5 in category V, M : S —• V also form a category denoted M o d p ( 5 ) . The objects of this category are the models M and the arrows are natural transformations. The category M o d p ( 5 ) is a full reflective subcategory of the functor category [5,2?]. The category of models of 5 in SET is denoted by M o d ( 5 ) . 4.2 Example: lists Currently, interest is growing in the use of sketches as a tool for the spécification of abstract data types. Sketches offer a spécification tool wThich is far more powerful than any which is currently available. Two reasons for this are: 1. the diagrams of a sketch contain no variables and become commuting diagrams (équations) when the sketch is modelled in any category, î>; equational reasoning is therefore greatly simplified for the model of a sketch. 2. The existence of a set of cocones in a sketch allows the user to specify sorts as sums, this can drastically reduce the complexity of a sketch. To quote from Wells and Barr [WeBa87]. "Having the ability to form disjoint unions makes it easy to define opérations .. .which are undefined on part of the datatype. We don't need to give it some artificial value such as 'error' — we just don't define it on the embarrassing part of the datatype, and in any model it is then not defined there and thus gives no trouble." Gray [Gray87] shows how sketches of simple datatypes may be combined to form more complex datatypes such as: SETofNAT, and SETofSETofNAT, and is currently developing a technique for implementing sketches using the computer algebra package Mathematica [Gray?]. A simple example, a sketch of lists of natural numbers with a distinguished error number, is included hère to give a flavour of the use of sketches in the spécification of abstract data 37 types. The sketch of the abstract data type List has seven opérations: empty —• List cons Data x List —* List head List —• Data tail List —» List. which operate on lists and zéro —• Data error -> Data suce .Data — Z)ata The opérations empty and cons are constructors, /iead : List —• .Data and tai/ : Zt$* -* List are described by the functions below. head(empty) = error head(cons(d,l)) = (f tail(empty) = empty tail(cons(d,l)) = / For the sake of simplicity the tail function is defined so that the tail of an empty list is the empty list rather than an error. Defining tail in this manner is done to avoid the need include cocones in the sketch. To force the Data sort to contain a unique error élément we also require: succ(error) = error. 4.2.1 T h e sketch of lists The sketch List comprises a graph G with four nodes, and nine edges. There are two cônes and five diagrams. 38 Graph - G The graph of the sketch of lists contains a node for each sort and an edge corresponding to each opération mentioned in the signature above. The nodes of the graph are: Data, List, T, Datax List and the edges are empty : T —> List, cons : Data x List —• List, head : List —• Data, and tail : List —• List. In addition to the edges above the graph of the sketch also contains edges: error : T —• Data, zéro : T —> Data, and suce : Data —• Data. The complète graph is represented pictorially below. JData x List cons//prLi*% tail Q List PrData head Data j suce empty The construction of the objects T, and Data x List, and arrows prnst and prData is described below. The set of cônes - C The cônes for the sketch List are: the cône over the empty diagram. For any model, M, in category C, M(T) will be the vertex of the limit cône over the empty diagram, so M ( T ) must be the terminal object of C. The second cône is used to specify the object Data x List as a product. 39 Data x List ^PrList PrData, Data List Any model. M, in category C, will take this cône to the product cône M(Data x List) M(prData)/ \M(prList) M(Data) M (List) so the présence of this cône spécifies that M (Data x List) = M (Data) x M (List) with the arrows M(prnst) and M(prj^ata) as the coordinate projections. It should be emphasised that the node Data x List in the graph G is not a product, in spite of its name, it is merely a node of the graph. The set of diagrams - D The sketch of lists requires five diagrams: two to specify the behaviour oîhead : List — Data, and two to specify tail : List —• List. List head Data x List Data JPTData cons A empty error List head Data W («) Together thèse diagrams specify the behaviour of head since any model, M, will force the diagrams (a) and (6) to commute. By (c) we obtain the équation M(head) o M(empty) M (error) and (b) gives rise to the équation M (head) o M(cons) = M(prData). 40 = The diagrams List tail Data x List List ^PrList empty" empty List tail List (d) (<0 specify the behaviour of tail. Again because any model, M, forces (c) and (d) to commute, we obtain the équations M(tail) M(tail) o M(cons) = M(prn5t), o M(empty) = M(empty), from (c), and from diagram (d). One final diagram is required to specify the behaviour of the suce opération: Data suce Data error error (e) which gives rise to the équation M (suce) o M (error) = M(error). This diagram will be used to force the Data sort to contain a unique error value. The sketch contains no other diagrams. Since the sketch List is an FP sketch it contains no cocones and is fully described as the 4-tuple List = (G, Z?,C,0). 4.2.2 The semantics of List A set valued model of an FP sketch S is called a term model if it is the initial object in the category Mod(5). FP sketches always hâve a term model [Barr86] as do FL sketches. To 41 provide a semantics for the sketch List we take its term model. / : List - • SET. To do this we must first define a congruence relation. Définition: Congruence relation. A congruence relation ~ is an équivalence relation on the arrows of a category C such that: 1. if / ~ ff, then / a n d g hâve the same source and target. 2. In the diagram: *ft \C -D if / ~ 05 then f ° h ~ g o h and k o f ~ k o g. The congruence class containing the arrow / i s denoted [/]. D In [BaWe90] Barr and Wells give a set of rules for the construction of the term model J : S -» SET for the FP sketch S = (G,D,C,Q). The terms are constructed as congruence classes of strings of tuples of composable arrows from the graph G and the rules recursively construct terms from an alphabet which consists of: the arrows of G, and ail finite length tuples of thèse arrows. For each cône c € C of the form: 1. If / : a -> b is an arrow of G and [x] € I(a), then [fx] € I(b) and I(f)[x] = [fx]. 2. If ( / i , - . - , / m ) and (gu.. .,gn) are paths, a -> + b, in a diagram d € D and [x] € / ( a ) , then ( / ( / 0 o . . . o I(fm))[x] in /(6). 42 = (/(Si) o . . . o I(gn))[x] 3. If for i = 1 , . . . , n, [xt] € I(ai), then [c(xx,..., xn)] G I(q) is a congruence class of strings consisting of the cône, c, followed by a tuple of arrows, so if n = 0 there is only one élément [c()] for the empty product. 4. If for i = l , . . . , n , [xi],[yi] € /(a,-) and [x,] = [y,-], then c ( x ! , . . . . x n ) = c(y a ,.. .,j/ n ). 5. For i = l , . . . , n , [p,c(xi,.. .,x n )] = [x,]. By rules 1 and 2 each / ( / ) : I(a) -* 7(6) is forced to be a function which respects the diagrams D. From rule 3 the vertex I(q) of a cône is forced to contain an élément corresponding to each tuple ( / ( a i ) , . . . , I(an)). Rule 5 forces I(pi), i = 1 , . . . , n to be the coordinate projections and from rules 1 and 5 we obtain I(pi)[c(xi,...,xn)] = [x,-],V* = l , . . . , n . Rule 4 extends the congruence relation to cover tuples. We can now construct the term model, I : List —• SET. The alphabet is constructed as: Ai = {empty, zéro, error, suce, cons,prust, pra>ata, tail, head} An = A1} = {(ai,...,an) A = LMn,n€{l,2,...}. : a,; G Ai,i = 1,.. .,n} Together rules 1, 3 and 5 define I(Data x List) as the set I(Data) x I(List), and I(prList), I(PrData) are the coordinate projections giving I(List) and I(Data) respectively. The functions I(prnst) and I(prData) cannot construct any éléments of I(List) and I(Data) and will be ignored below, except where they form part of a diagram. By rule 3, / ( T ) is a singleton set, I(empty) is an élément of 1(List) which we shall naine nil, while I(zero) and I(error) are éléments of I(Data) which we name 0 and err respectively. From rule 1, the set I(Data) is inductively defined as: 43 I(Data)0 = {0,err} I{Data)n = {succ(x) : x € I(Data)n-!} U {head(x) : x <= I(List)} I(Data) = [JI(Data)n,nÇ: {0.1,2,...}. Notice that from rule 2 and diagrams (a) and (b) we obtain: I(head) o I(empty) = I(error) and I(head) o I(cons) = /(pr0 ota ) so the set {/iead(x),x € /(lis*)} adds no new éléments to I(Data)n and can be ignored. Similarly, by rule 2 and diagram (e), I(succ) o I(error) = /(error) so I(Data) = {O,succ(0),succ(succ(0)),...} U {err}, i.e the set of natural numbers with a distinguished error élément. By rule 1, the set I(List) is constructed as: I(List)0 = {nil} I{List)n = /(XwO»-iU {cons(x,y) : (x,y) G I{Data) x Z(/is*)n-i} U {tai/(x) : x € Z(Iist)„_i} /(li«0 = U / ( M n , n £ {0,1,2,...}. From rule 2 and diagram (c), we obtain /(toi/) o I(empty) = I{empty), therefore tail{nil) = nil. Similarly rule 2 and diagram (d) produce I(tail) o I(cons) = I(prLiat), {tail(x),x € I(List)n-i} so the set adds no new éléments to I(List)n. The description of I(List) can therefore be simplified to I(List)0 - {nil} I(List)n = J(List)n-i U {cons(x, y) : (x, y) € I(Data) x /(Ii50„-i} I(List) = U/(£*«*)n,n€ {0,1,2,...} the set of séquences of éléments of I(Daia) terminated by the value nil, i.e. Lists of natural numbers with a distinguished error number. The opération I{head : List -* Data) is specified by the équations generated by diagrams (a) and (b) as: 44 (a) I(head)(nil) = err (b) I{head)(I(cons)(x,y)) = x, V(x,y) € I{Data) x I{List) and I(tail : List - • List) is specified by (c) and (d) as: (c) I(tail)(nil) = ni/ (d) /(*a«7)(J(cons)(x,y)) = y, V(x, y) € J(Z?a*a) x / ( I M * ) - In other words, the expected head and tail opérations. 4.3 Sketch morphisms and induced functors In this section we examine some of the properties of sketches and their models. The construction of the categorical model of language in chapter 5 is based on thèse properties. Property 4.3.1 IfhiS -+T isa sketch morphism it induces a functor between the catégories of models ofS and T, h' : M o d ( T ) -* M o d ( S ) . Proof: h* : Mod(T) — M o d ( S ) is defined as h'(M) h*(f:M-+N) = M oh = fh:h'(M)^h'(N) We can use property 4.3.1 to construct models of a sketch, S, which play the rôle of datatypes with hidden sorts and opérations. Proposition 4.3.1 Let S = (G,I>,C,0) be an FL sketch, T = (G', £>', C , Co') be a sketch, andhxS^Tbea sketch morphism. For each model, M :T — S E T , of T, the datatype h*(M) : S -* SET has the saine behaviour as M except that each object n' € G'0 which is not the image in h of some object n € Go becomes a hidden sort ofh"{M) and each edge e' € G\ which is not the image in h of some edge e € G\ becomes a hidden opération. 45 Proof: If n € Go then h(n) € G'0 and from property 4.3.1 h*(M)(n) = M(h(n)) are the same sort. If n1 6 G'0 and there is no n 6 Go such that h(n) = n' then hu(M)(n) is undefined so the sort M(n') is hidden. Similarly if e € Gi then h(e) 6 G[ and from property 4.3.1 hm(M)(e) = M(h(e)) are the same opération. If e' 6 G^ and there is no e G Gi such that /i(e) = e' then /i*(M)(e) is undefined a and the opération M(e') is hidden. A second property allows us to map the initial model of S to the model h*(M). Property 4.3.2 If S is an FL sketch then for any sketch, T, and sketch morphism h : S -+ T we hâve a unique natural transformation, e : /5 -A h*(M), where Is : S -> S E T is the initial model of S and M :T -+ SET is any model of T. Proof: IS:S - SET is initial in M o d ( S ) . D For FL sketches S and T and sketch morphism h : S -> T the construction in Mod(5) is shown in figure 4.1 \ \ Figure 4.1: The category Mod(S) where Is : S — S E T is the initial raodel of 5, M : T - • S E T is a model of T, and hm : Mod(T) -> Mod(5) is given by h : S -• T and property 4.3.1. The natural transformation e : /5 A h*(M) is given by property 4.3.2. Our intention is to use Mod(5) to construct a model of language where /5 models language syntax, hm(M) models language semantics and e : Is -^ h*(M) models the évaluation of programs. 46 To construct this model of language with properties similar to Rus' model of language we need to establish: 1. that Is can be used to model a language syntax. 2. That h*(M) can model a language semantics and 3. the conditions under which we can construct an arrow learn : h*(M) —• / 5 . We will leave 1 and 2 for the next chapter and concentrate hère on 3, the construction of learn. To discuss the conditions sufficient to allow the construction of learn we must first define what sort of object learn is. In order to impose as few conditions on S,T, and h : S —• T as possible we define learn as a transformation [Copp80]. Définition: Transformation. Let F : C - • V and G : C - • V be functors. A transformation t : F - • G is defined as any collection of arrows / c : F(c) -+ G(c) indexed by the objects, c, of C. D This définition is simply a much weaker form of the définition of natural transformation where the naturality condition has been completely removed. The composition of transformations we require is the horizontal composition given in [Copp80] and is defined below. Définition: Composition of transformations. Let F, G, H : C — V be functors and s : F — G, t : G — H be transformations. The composition of t and s is defined as the transformation t 0 s : F - • H given by the collection of arrows tcosc: F(c) -+ H (c) indexed by the nodes, c, of C. D If learn : hm(M) -+ /5 is a transformation then to construct and analogue of Rus' learning function we require that e o learn = 1&»(M)- TO ^ e a ^ e t o construct learn we require a relationship between S and T which is illustrated in figure 4.2 In the situation where the arrow g e T is not the image in h of an arrow from S it must be the case that the arrow M(g) adds no new éléments to the set M(h(y)). Additionally we also require that the set M(h(y)) contains no éléments which are not constructed by some arrow 47 -^- y h(f) -=> ^ h(y) h(x) T g Figure 4.2: Generalised arrows in sketches S and T. M(p) where p is a path in 7\ i.e. we can ensure this by insisting the M : T -> SET is the initial model IT - T —• SET of T. When the sketches S and T hâve the relationship described above we will say that S is learnable from T. That is to say we can construct the sketch S by deleting parts of T without removing éléments from the sets constructed by models of T from objects of T which are common to both S and T. We can now describe the construction of the transformation learn : h*(Ij) —• Is- Proposition 4.3.2 If S and T be an FL sketches and h : S -+T is a sketch morphism such that S is learnable from T. We can construct a transformation learn : hm(Ij) -+ Is where Is : S -> SET and IT -T -+ SET are the initial models of S and T respectively. The natural transformation e : Is + h*(Ij) given by property 4.3.1 defines an équivalence = s on the set Is(s) for each node s e S. Vx.y e Is(s) :x=sy& es(x) = e3(y) We can therefore construct a quotient set /5(5)=, where each élément [x] £ Is(s)=, is the class of terms t G /5(5) which are équivalent under = , . Since S is learnable from T there is an isomorphism between the sets /5(5)=, and h*(IT)(s) so to construct an arrow l5 : h*(IT)(s) -» Is(s), set ls(x) = y for each x G h*(IT)(s) where y is a member of the équivalence class, [y] such that es(y) = x. The arrows /5 form the transformation learn : h*(Ir) -+ / s - 48 D Obviously the arrows la are not unique as we can choose an arbitrary y from [y] but regardless of the choice of y we know, by construction, that e3 o ls = lh*(iT)(s) and therefore e o learn = l/i*(/ r )- We now hâve ail the components necessary to construct a categorical model of language with similar properties to the algebraic model of language discussed in chapter 3. 49 Chapter 5 A Categorical Model of Language The categorical model of language described in this chapter is a development of the model discussed in [ReRa89], and is used to construct a category Mod(S), where Sis an FL sketch describing the syntax of a programming language. The category, Mod(S), is generated by an FL sketch and, as a resuit, has properties similar to those of the category of E-algebras, C(S). The category of E-algebras is actually équivalent to the models of FP sketches, so by using the FL class of sketches (which includes ail FP sketches) we can increase the power of the model of language. The model of language described therefore has similar properties to Rus' algebraic model of language discussed in chapter 3 while having a greater expressive power. 5.1 Using sketches to model language syntax To model the syntax of a programming language, C, we construct a sketch which describes the abstract syntax trees of C programs. To define the abstract syntax trees of C we will assume that the syntax of C is described by a context free grammar, CFG. Définition: Context Free Grammar. A context free grammar, CFG, is defined as a 4-tupie \N,T, P,S) where: 50 1. the set N, called the set of nonterminal symbols, is a set of names used to name the types of phrases of the language, L(CFG), described by the context free grammar. 2. The set T, of terminal symbols, is the set of symbols which may appear in a sentence of the language, L. The set of strings of terminal symbols is denoted by T + . 3. P, called the set of production rules, is a non-symmetric, non-transitive binary relation, P : N -*RHS, where RHS is the set of strings which can be constructed from the set NuT. 4. The start symbol S G N is a distinguished nonterminal symbol such that: Vs G T + : s is a sentence in L & S —>+ s where —•+ is the transitive closure of P. The set, L(CFG) = {x : x G T + A S -++ x}, describes the language generated by the context D free grammar, CFG. Using this définition of context free grammar the abstract syntax trees generated by CFG are defined below. Définition: Abstract syntax tree. An abstract syntax tree is a labelled, ordered, rooted tree such that: Abs-1. if tis a string in T + and there is a production rule, p : N —> t, then t is an abstract syntax tree describing a phrase belonging to type N. Abs-2. Let p : N —• Co . . . cx, x > 0, be a production rule such that, c t , . . . , c*,..., Cj, 0 < i < k < j < x,is the séquence of nonterminals from the string co.. .c x . If ti is the abstract syntax tree of a phrase of type c,, tk is the abstract syntax tree of a phrase of type c&, and tj is the abstract syntax tree of a phrase of type Cj, an abstract syntax tree, t, rooted by p is constructed by setting U,..., tk,..., t:; in order as the children of node p. The abstract syntax tree, t, describes a phrase of type N. 51 Abs-3. Nothing else is an abstract syntax tree. D Theorem 5.1.1 shows that we can construct an FP sketch, S, which describes the abstract syntax trees of the language generated by the arbitrary context free grammar, CFG. Theorem 5.1.1 For every context free grammar, CFG, there is an FP sketch. S, such that each node, n, which is not the vertex of a cône, is mapped to the set phrases of type n G N of L(CFG) by the initial model, Is : S — SET, in Mod(S). Proof: The FP sketch, S, describing the abstract syntax trees of L(CFG) is constructed as: 1. set S = (G,0, C,0) where G is the graph containing exactly one node, T , and no edges, and Cis the set of cônes containing just the cône over the empty diagram. e : T —• G. 2. For each nonterminal symbol, n G N, add a node n to the set of nodes, Go3. For each production rule, p : n — t,t G T + add an edge, p : T —> n, to the set of edges, Gi. 4. For each production rule, p : n — c o . . . c x , where c t , . . . , c*,..., c:, 0 < i < k < j < x is the séquence of nonterminals from co .. . c r : (a) if i ^ j , add a node named. c, x . . . x c* x . . . x Cj, to Go(b) If i ^ j , add a cône pr : c t x . . . x c* x . . . x Cj —• D over the discrète diagram Ci ... Ck ... Cj to the set of cônes, C. (c) If i = j , add the edge p : c, —• n to G\. If i ^ j add the edge, p : c, x . . . x c* x . . . x Cj —• n to Gi. 5. Nothing else belongs to S. We must now show that each set Is(n), n G Go, where n is not the vertex of a cône is the set of phrases of type n G AT of L(CFG). 52 From Abs-1 we know that each phrase of type n, t, which has no subtrees is generated by a rule of the form p : n —> t. Rules 1, 2, and 3 above ensure that the sketch, S, has an edge p : T —• n corresponding to each production rule p : n —• t. Since S contains no diagrams we know that the arrow Is(p) - / s ( T ) —> /s(n) uniquely identifies a term in Is(n), corresponding to the phrase, t. From rule Abs-2 we know that each phrase, t, with subtrees U,..., tk,..., by a production rule p : n —> CQ...CX t3 is constructed where c,-,.. .,c*,.. ,,Cj, 0 < i < k < j < x are nonterminal symbols such that: U is a phrase belonging to type c t , tk is a phrase belonging to type c*, and tj is a phrase belonging to type Cj. Rule 2 ensures that the sketch, S, contains a node, n, while rules 4a, and 4b ensure that Is(ci,.. . , c * , . . .,Cj) is the product Is(ct) x . . . x Is(ck) x . . . x Is(cj)- By rule 4c we obtain an edge in G, p : a x . . . x Ck x ... x Cj —• n, corresponding to each production rule p : n -+ CQ .. .cx. Since, 5, contains no diagrams the arrow Is(p) : Is(ci) x . . . x Is(ck) x . . . x Is(cj) -+ /s(^) constructs terms such that for each y = (U,...,tk,...,tj) G /5(^1) x . . . x Is(ck) x . . . x Is(cj), Is(p)(y) is uniquely identified as a term in Is(n) and has subterms, in order, / , - , . . . , ^ , . . . , tj. The term Is(p)(y) corresponds to the phrase, t. From rule 5 we know that each Is(n) contains no other terms. The simple expression language in chapter 3 with syntax: (Exp) — 0 (Exp) —• succ((Exp)) (Exp) — (Exp)+(Exp) has the abstract syntax trees shown. exp-treeso = {0} exp-treesn = {succ(x): x €exp-treeSn-i}\J {+(x,y): exp-trees = (x,y) eexp-treesn-iXexp-treesn-i} \Jexp-treesn. n G {0,1,...} 53 • The sketch, Exp, which describes this set of abstract syntax trees has 3 nodes, T, exp, and, exp x exp. and 5 edges: 0 T—• exp suce exp —* exp pr\ exp x exp —• exp pr2 exp x exp -» exp + exp x exp —• exp The edge, 0 : T -* exp arises from the production rule (Exp) —• 0, because of rule 3. The production rules (Exp) -» succ((£xp)). and (Exp) —• (Exp)+(Exp), together with rule 4 force the existence of the edges suce : exp —» exp and + : exp x exp —* exp respectively. The edges pri : exp x exp —• exp and pr2 : exp x exp —• exp arise solely because of rule 4b, as they are the projection edges of a cône. There are just 2 cônes: the cône over the empty diagram, and exp x exp which is forced to exist by rules 4a and 4b and, when modelled in SET, forces M(exp x exp) to be the product M(exp) x M(exp). The sketch is represented pictorially below. prx succ\ •exp — + pr2 54 •exp x exp The sketch, Exp contains only one node which is not the vertex of a cône, namely exp. Using rules for constructing the term model, Ï£zv : Exp — SET, of Exp given in section 4.2.2 we obtain the set, ÏExP(exp), shown below. IExp(exp)o = {W°)(0)} lExp(exp)n = {IEXP(SUCC)(X) :x€ lExP(exp)n-i}U {lExP(pri)(x) : x £ lExp{exp)n-i}\J {lExp{pr2){x) •• x € lExP(exp)n-i}U {lExP(+)(Xny) : (x,y) € lExP(exp)n-i lExP(exp) = x \JlExP{exp)n, n € { 0 , 1 , . . . } The sketch contains no diagrams and so lExp{0)jExp(succ),IExp{+) in IExp(exp). lExP(exp)n-i} uniquely construct terms The arrows Isxpipri) and Isxpipri) are forced to be the coordinate projections of the product lExp(e*P x exp) and as a conséquence do not construct terms in /£ x p (eip). The description of iExp(exp) can therefore be simplifled to: lExp(exp)0 = {0} lExp(exp)n = {succ(a:):z G/£xP(earp)n-i}U {+(x,y): (x,y) € lExp(exp)n-i lExP(exp) = x lExP(exp)n-i} {JlExp(exp)n, n € { 0 , 1 , . . . } and so lExp(exp) S cxp-trees. In section 5.4 we will show that by using FL rather than FP sketches to model language syntax we can simplify the process of language spécification by capturing the static semantics of a programming language within the spécification of the syntax. 55 5.2 Using sketches to model language semantics In this section we show how a sketch can be used to construct the semantics of a programming language. To describe the senantics of a programming language we must actually describe the computational uni verse in which the language exists. To describe this uni verse we simply view it as a complex abstract data type and construct an FL sketch, Sem, which has this datatype as its initial model. The semantics of the simple expression language is given by an FP sketch, Nat, which describes the natural numbers with an addition opération. This sketch has nodes, T, nat, and natxnat, and edges: 0 : T— nat dispose : nat -• T suce : nat —• nat pr\ : nat x nat —> nat pr2 : nat x nat —• nat + : nat x nat -+ nat : nat —• nat idnat : nat —> nat (ï.idnat) : nat —• nat x nat SUCC X idnat : nat x nat —• nat x nat. There are two cônes: and nat x nat nat 56 Thèse cônes force the objects, M(T), and M (nat x nat) to be the sets, {0}, and M (nat) x M(nat) respectively. The graph of the sketch is shown below. (z, idnat) s+ suce dispose SUCC X idnat -nat x nat —nat* idnai [3 a We require six diagrams to complète the spécification of the semantics. nat nat dispose idnat nat (b) From diagram (a) we obtain the équation M(z) = M (0) o M (dispose) For the initial model of Nat, I^at : Nat —• SET, this équation forces //Vot(^) to be the function, x -+ lNat(0)(lNat(T)), 1 i.e. x -* 0. Diagram (6) forces lNat(idnat) to be the function /Nat(noO' nat (2, idnat) pri nat x nat (c) 57 — — nat The équations: M(pri)oM((z,idnat)) = M(z) M(pr2) o M((z, idnat)) = M(idnat) are obtained from diagram (c). Together, thèse équations force lNat((z, idnat)) to be the function: x -+ (lNat(z)(x),INat(idnat)(x)). PT\ nat -* PT2 nat x nat -nat id< nat SUCC X idnat suce nat- pri nat x nat • pT2 •nat (d) From diagram (d) we obtain the équations: M(pri) o M (suce x idnat) = M (suce) o M(pri) M(pr2) o M(succ x idnat) = M(idnat) o M(pr2) so lNat(succ x idnat) is the function, (x,y) -> (lNat(succ)(x), A (*,idnat) nat . nat x nat •- nat + nat -nat SUCC X idnat suce nat x nat • (e) nat (/) The final two diagrams (e), and (/) provide the équations: 58 lNat(idnat)(y)). which force Ixat(+) M( + )oM((z,idnat)) = M(idnat) Àf(+) o M(succ x idnat) = M(succ) o M(+) to be addition on natural numbers. The sketch, Nat, is discussed in greater détail in [BaWe90], chapter 7, and Ijsjat describes the semantics of the simple expression language of natural numbers and addition. In section 5.3 below we show how to combine the sketches Exp and Nat to produce a complète description of this language. 5.3 A categorical model of language 5.3.1 A categorical spécification of language Recall that Rus' algebraic model of language spécifies a language as a triple (Sem, Syn, learn : Sem —• Syn) where Syn is the initial algebra over signature E and Sem is a similar algebra. The function learn : Sem —• Syn is defined on the carrier sets of Sem and Syn such that, if eval : Syn —• Sem is an homomorphism given by the initiality of Syn then evalolearn = l 5 e m . To construct a categorical model of language with properties similar to Rus' algebraic model we specify it as a 4-tuple (Sem, Syn, E : Syn - • Sem, learn : E*(Msem) - • Isyn) where Sem and Syn are FL sketches, and E : Syn —• Sem is a sketch morphism such that Syn is learnable from Sem. The transformation learn : E*(Isem)(Sem) —• Isyn(Syn) is constructed by following the procédure given in the proof of proposition 4.3.2 and is described in greater détail below. By theorem 5.1.1 we know that for every context free grammar, CFG, we can construct an FL sketch (actually an FP sketch but the extra power of FL sketches can be used to describe the static semantics) whose initial model in SET describes the abstract syntax trees of the 59 language, L(CFG). The sketch, Syn, is just such a sketch and we take its initial model in SET, Isyn • Syn -• S E T to be the abstract syntax of the language, The semantics of L(CFG) L(CFG). is specified by the sketch, Sem. but we do not regard the initial model, Isem • Sem —> SET, as the semantics because there is no obvious way to describe the évaluation of programs if Isem is the semantics. tics of L(CFG) we use property 4.3.1. duces a functor E* : Mod(Sem) The sketch morphism E : Syn —• Sem in- —• Mod(Syn), E*(Istm) • Syn -+ S E T e Mod(Syn) To construct the seman- and so by proposition 4.3.1 the model spécifies a datatype which is équivalent to Isem hidden sorts. We use the model Em(IsCm) € Mod(Syn) as the semantics of The évaluation function, eval : ISyn -^ E*(Isem), with L(CFG). is the natural transformation which is known to exist because of property 4.3.2. To complète the spécification of L(CFG) we specify learn : E*(Isem) -> Isyn as a transformation such that, eval o learn = l£*(/ Sem ), w ^ e r e ° *s composition of transformations. Since Syn, Sem, and E : Syn — Sem are such that Syn is learnable from Sem proposition 4.3.2 guarantees the existence of learn. The 4-tuple (Sem,Syn, E : Syn —• Sem, learn : Em(Isem) —• Isyn) therefore completely spécifies the syntax, semantics and syntax *•* semantics the language, 5.3.2 association of L(CFG). The language of natural numbers and addition We hâve already constructed sketches, Exp, and Nat, which we will use to specify the syntax and semantics of the simple expression language from section 3.1.5. To complète the spécification we must: 1. construct a sketch morphism E : Syn -+ Sem such that Exp is learnable from Nat. 2. Construct the transformation learn : E*(Isat) - 4 lExp- 60 The construction of E : Syn —• Sem follows a fairly simple procédure. We simply map éléments from the syntax (the sketch Exp) to the corresponding éléments from the semantics (the sketch Nat) which we wish to use to express the meanings of the syntactic objects. In this way we can construct E : Syn —> Sem as: E(T) = T E(exp) = nat E(exp x exp) = nat x nat E(0 : T — exp) 0 : T -* nat E(succ : exp —• exp) suce : nat -* nat E(pri : exp x exp —> exp) pri : nat x nat —• nat E(pr2 : exp x exp -+ exp) pr2 : nat x nat —* nat E(+ : exp x exp —• exp) + : nat x nat —• nat. This leaves us with the following edges of Nat which are not the images in E of edges of Exp. dispose nat-* T z nat —* nat idnat nat —• nat (Z, idnat) SUCC X idnat nat —• nat x nat nat x nat —* nat x nat To show that Exp is learnable from Nat we need to show that none of thèse arrows construct éléments of the sets /Not(T), iNat(^at), or lNat(^at x nat). We know that except for dispose : nat —* T, the model I^at maps each of the above edges to functions which are defined in terms of /;vot(0), iNat(succ), and l/Nat(naQ- ^ s a resuit none of thèse functions produce éléments of /^at(T), iNat(nat), or Itfat(nat x nat) which are not constructed by some combination of lsat(0) and Isat(succ). Since we also know that //Vat(T) is terminal we know that I^at(dispose) : iNat(nat) —> -^Not(T) can only be the function x —• 0 so it cannot construct éléments either. We therefore know that Exp is learnable from Nat. We must now construct the transformation learn : Em(Ijsrat) -* lExp- 61 The component arrows of learn are constructed so that they are right inverses of the eval natural transformation. Obviously to specify learn we must first calculate eval. The eval natural transformation From property 4.3.2 we know that eval is the unique natural transformation eval : IEXP - • Em(ljvat) given by the initiality of IEXP- We therefore know that the diagrams below commute. WT)" hrP(0) - lExp(exp) eval,exp evalrç E*(lNat)(T) E"(lsat)(0) E*(INat)(exp) (a) From the définitions of IEXP and Iffat we know that IEXP(T) = £*(/)v a t)(T) = {0} and so evalf = 1{0} From diagram (a) we obtain the équation evalexp o IEXP(0 < = E*(lNat)(0) o eval?. We know from the définitions of IEXP, and Isat that IEXP(0)(9) = 0 where 0 is a syntactic term, and E*(lriat)(0)(to) - 0, i.e. the number 0, so from the équation above we obtain evalexp o IET7(0) = (0 •-» 0) o 1{ 0 } eval^ o (0 — 0) = 0 -* 0. From this final équation we can partially define evalexp as: eva/ eip (0) = 0. 62 IEXP(MCC) iExp(exp) * ÏExpiexp) eval exp eval,exp E*(INat)(exp) Em(INat)(exp) — E*(INat)(sUCC) (b) From diagram (b) we obtain eval^ o IEXP(SUCC) = Em(I^at)(succ) o evalexp By the définitions of IEXP and ^Nat we know that IEXP(SUCC), and Em(lNat)(succ) tively the functions x —• s u c c ( x ) and x —• z + 1. From this we obtain: evaltxpo(x - • s u c c ( x ) ) = (x — x + l ) o which allows us to partially define evalexp as: ei?a/ e x p (succ(x)) = evalexp(x) I r , x lExP(exp x exp) ExP(pri) - lExp(exp) eval eval exp x exp E'(INat)(exp eval^p x exp) E —* (lNat)(pri) exp E'(INat)(exp) (c) The commutativity of diagram (c) gives us the équation: eval^p o iExp(pri) = Em(lNat)(pr\) 63 o evalcxpxexP + 1. are respec- while commutativity of diagram (d) gives us: evalexp o IEXP(P^2) w „ , x el?) = E*(Itfat)(pr2) ° evalexpxexP. W£!î> . WMF) eval exp eva/,exp x exp Em(Isat)(exp - x exp) Em(INat)(exp) E'(lNat)(pr2) (d) Since lExP{pr\) and IEXP(P^2) are the co-ordinate projections for iExp(exp) x iExp(exp) and Em(Ixat)(pri) and Em(Isat)(pT2) are the co-ordinate projections for iNat(nat) diagrams (c) and (d) define evalexpxtaep: lExP(exp x exp)- evaltxpxexP(z,y) W+) iNat(nat), = (evaWx)>evaWîO)- - /£xp(e*p) eva/.exp evalexpxexp E"(lNat)(exp x x exp) E'(Isat){exp) — £•(/*.«)(+) (e) This final diagram adds one last équation which allows us to complète the définition of evalexp- evalexp o J E * P ( + ) = Em(INat)(+) From the définition of J ^ p we know that IEXP(+) o evalexpxexp- is the function (x, y) -* +(x , y ) which con- s t r u i s syntactic expressions involving the plus operator from pairs of expressions. Similarly 64 we know from I^at that E*(Iwat)(+) is addition on natural numbers. Using diagram (e) we can dérive the équation evalexp(+(x>y)) = evalexp(x) + evalcxp(y). By collecting the various parts of the définition of the eval natural transformation together we construct the following: evalf = 0 i—• 0 evalexp = / evalexpxexp = where /(0) = 0 /(succ(x)) = /(x) + l /(•<*, y » = f(x) + f(y) (x, y) — (evalexp( x), evalcxp(y)) Having calculated the eval natural transformation we can now specify learn : Em(Isat) -* lExp so that Vn € Exp : evaln o learnn = l£'(/ Nût )n- The components of learn : Eu(Iwat) —* ^Exp are specified as: learnj^ = 0 i—• 0 learnexp = l where learneXpxexp = 1(0) = 0 /(x+1) = succ(/(x)) (*, y) - • (/earn cxp (x), learnexp(y)). The language of natural numbers and addition is therefore completely specified by the 4-tuple: (Nat, Exp, E, learn) 65 where Nat is the sketch from section 5.2, Exp is the FP sketch given in section 5.1, E : Syn — Sem and learn : E*(Ijvat) -> lExp are, respectively, the sketch morphism and transformation shown above. In the remainder of this chapter we discuss some of the implications the sketch based model of language has for the way in which we specify certain language features while in chapter 6 we will discuss the process by which we arrive at a self-interpreter for the arbitrary language C specified using this model. 5.4 Describing language features using the model The categorical model of language described above allows the language spécifier to use limits which are not simple products in a language spécification. The use of such constructs can drastically simplify the spécification of certain types of language construct. In [KoQu92] Kortas and Quatrain use the categorical model of language described above to specify a subset of the pascal programming language. The spécification that they provide is interesting because it uses thèse features to construct a spécification which is both clear and less complex than can be achieved using conventional methods. In this section we show how the model of language can be used to construct a spécification of the type scheme for a simple FP [Back78] like language. The spécification that we construct demonstrates some of the extra power which is available within the categorical model of language, and shows that while the model has a great deal in common with Rus' algebraic model it is significantly more powerful. 5.4.1 A simple type scheme The language we describe hère constructs programs as the composition of functions. The language has two basic types: nurn and char and two basic opérations: 1. ord which returns the ordinal number of a given character. 66 2. chr which will return the character with the ordinal number of its argument. We also hâve one structured type constructor, list, which allows us to construct lists of any depth. The function map takes a function f of type f : * —> ** and constructs a function of type map f : * list —• ** list. Functions are composed using the o operator. This operator is a partial operator since the composition f o g is only defined if the source type of the function f is equal to the target type of the function g. We can describe this aspect of the semantics of our language using a very simple sketch whose graph contains only 4 nodes: T, exp, type, and exp x exp. we require 12 edges: ord T -• exp chr T -* exp map exp —• exp o exp x exp -» exp num T — type char T — type list type -+ type src exp —• type trg exp —• type pri exp x exp —• exp pr2 exp x exp -H- type pr 3 exp x exp -» exp to produce the graph shown pictorially as: 67 Pn • exp x exp P?3 pr2 We require four diagrams to describe the src arrow: src src type (a) (b) which give us the équations: M (src) o M (ord) = M (char) M(src) o M(chr) = M(num) In other words the source type of the function ord is char and the source type of the function chr is num. From diagram (c) 68 map exp x exp src src exp pr$ src exp src type (d) (c) we obtain the équation: M(src) o M(map) = M(list) o M(src). This tells us that the source type of the expression map f is * list where * is the source type of f, while diagram (d) gives us the équation: M(src) o M(o) = M(src) o M(pr^) which states that the source of the composition f o g is equal to the source of g. Four similar diagrams are needed to describe trg. We now hâve only the partial nature of the o operator left to describe. This is done using the cônes. There are two cônes. Firstly the cône over the empty diagram and secondly the cône exp x exp exp exp When this cône is modelled we obtain an équation 69 M(src) o M(pri) = M(pr2) = M(trg) o M(pr3) and the cône becomes a new kind of limit known as a pullback. In SET the vertex of this cône is a restricted form of product containing only those pairs which conform to certain properties. In this case the restricting property is given by the commutativity of the cône so we know that the set M (exp x exp) is {(x, y) : (x, y) £ M(exp) x M(exp) A M(src)(x) = M(trg)(y)}. This allows us to specify o as a total operator since the only members of the set M (exp x exp) are those pairs of functions whose types make them composable. Contrast this with a spécification given using FP sketches or using Rus' algebraic model. In the case of an FP sketch the node exp x exp would be defined by the cône exp x exp exp exp and so M (exp x exp) would contain very many pairs of non-composable functions. We would need to add several diagrams to the sketch to describe the behaviour of o when applied to thèse pairs, which would need to be mapped to a new expression value type-error. We would then need to add a new arrow type-error: T -* exp and several more diagrams to describe the behaviour of src, trg, and map applied to this value. We would also need to add another arrow error-type: T —• type so that we could define the source and target type of the expression type-error. The resuit is a sketch (or an algebraic spécification) which is drastically more complicated than the one given above and in which the simplicity of the type scheme we are trying to specify is consequently obscured. The inclusion of a cône which is modelled as a pullback allows us simply to ignore incorrectly typed programs because our syntax cannot contain them. 70 5.4.2 The semantics The simple language described hère is a higher order language which présents us with something of a problem since we cannot use any type of sketch directly to describe a higher order construct. We can, however, still describe the semantics of our language indirectly by describing the effect of applying programs to data objects. To explain: we construct a node, data, whose model Isem(data) contains ail well formed (i.e. type correct) data objects which can be processed in our language. We also define an edge typ : data — type with appropriate diagrams so that the function Iscm(typ) returns the type of any élément of Isem(data) to which it is applied. Using the data node and the typ : data —•> type edge we can construct the cône exp x data ex P — 1 Ï T ^ 'w* ~tjiï— data whose vertex Isem(exp x data) contains ail pairs of programs and the data objects to which they can be applied. If we now add an edge run : exp x data —• data we can construct diagrams which describe the effect of applying programs to data objects and thus describe the semantics of the language. The resulting sketch is, however, rather complex and there is little to be gained by showing it hère. 71 Chapter 6 A Categorical Approach to a Self-interpreter So far we hâve constructed a model of language based on FL sketches which while it has many properties in common with Rus' algebraic model of language is, as we demonstrated in section 5.4, significantly more powerful. In this chapter we use the properties which our sketch based model of language shares with Rus' model to construct a self-interpreter. 6.1 Construction of the self-interpreter It was shown in section 3.2 that using Rus' algebraic model of language, the function computed by the interpréter for the programming language C = (Syn(B, W(X, E)), Sem(B, A), learn : Sem(B, A) - Syn(B, W(X, E))) is defined as interpréter = learn o eval. This is also true for the categorical model of language. 72 Proposition 6.1.1 If C is specified using sketches C = (Sem, Syn, E : Syn -• Sem, learn : E*(Isem) -* hyn) the interpréter function is described as interpréter = learn o eval. Proof: Since Sem, Syn, and E : Syn —• Sem are such that Syn is learnable from Sem we know that for each object S G Syn there is a quotient set Isyn(S)=s Isyn(S)=s = Em(Isem)(S). m e E*(Isem)(S), defined by eval s and that From the construction of learns we know that for each meaning m 2 [x], where evals(x) = m, learns(m) 6 [x] is the preferred syntactic représentation of m. The function interpréter = learn o eval therefore maps programs to their preferred syntactic form (whilst preserving their meaning) and is an C interpréter. • Proposition 6.1.1 is an exact analogue of proposition 3.2.1 stated in section 3.2. We also obtain an analogue of theorem 3.2.1 shown below Theorem 6.1.1 For each edge, f :a -+ b, from the graph of the sketch Syn, the function, Ff:a^b : ISyn(a) -> ISyn(b) in SET, defined as Fj:a-+b = interpréter o hyn(f) has the same behaviour on syntactic objects as Em(Isem)(f) '• Em(Isem)(a>) -> Em(Isem)(b) has on semantic objects. Proof: Fj:a-*b is defined as: Ff-.a-*b = interpréter o ISyn (f) = learnb o evah o hyn(f) = learnb o E*(Isem ) ( / ) ° evala 73 This theorem can in fact be generalised to include ail arrows g : E(a) -• E(b) from the graph of Sem where E : Syn —• Sem is the sketch morphism, given in the language spécification, and defines Em. F9:E(a)^E(b) = l arn ^ b ° Em(IScm)(g) o evala This généralisation allows us to construct arrows which correspond to the hidden opérations defined on the objects of E*(IScm)(Syn). ° In the example language given in chapter 5 the interpréter function for the language: C = (Nat, Exp,E: Exp — Nat, learn : Em(INat) -> IErp) is therefore specified as: interpréter^ interpréterexp interpréterexpXexP = learn^ o eval^ = 0.-0 = learneXp ° evalexp = / where f(0) = 0 /(succ(x)) = succ(/(x) f(+(x>y)) = i r +:expxcxp-cxp(^ ? î/) = lea>rnexpxexp ° evalexpxexp = learneXpxexp ° (*> y) -+ (et>aJexp(s), evaleXp(y)) = (x, y) — ((/ear7icxp o eva/^pXx), (learnexp o evalexp)(y)) = (*, y) — (mterpreter^x), interpréterexp(y)) The function, F+:cxpxc*p-e*p : /syn(exp) x Jsyn(exp) — /syn(esp), used in the définition of interpréter exp above is given by theorem 6.1.1 and is defined exactly as in figure 3.1. F+:expxexp-*exp = k<*™exp ° + ° F+:expXcxp—*exp(Qiy) = S r = SUCC(i r +:C xpxcxp^cxp(^i î/)) i +:cxpXcxp-cxp(sUCC(x),î/) 74 evaleXpxexp As with the algebraic description of a self-interpreter in section 3.2 the components of the interpréter function above lie outside the semantics of the language C. The remainder of this chapter deals with the process by which the interpréter transformation is converted into an C program. 6.2 Moving into the semantics The first step in the process of converting interpréter into an C program is to construct a datatype which exists within the semantics of C and is capable of representing the abstract syntax trees of C programs. Although the construction of this représentation is not addressed in this thesis we still need to provide a définition of such a représentation since we require certain properties for the construction of the self-interpreter. Définition: A représentation of syntax. Given a language spécification C = (Sem, Syn, E : Syn — Syn, learn : E*(Isem) -* Isyn) a représentation of the syntax of C is defined as a pair of transformations encode : ISyn - • E*(IStm) décode : Em(Istm) -+ hyn such that décode o encode = l/ 5 y n . D Each object, Isyn(t), of the syntax must be taken to an object, rept, of the semantics. The objects reps and rept need not be distinct if they represent différent objects from the syntax. The only restriction required is that where a semantics object represents more than one syntax object the représentations form disjoint subsets. In this way the syntax of C is represented in the semantics of £ with no loss of information. The choice of thèse arrows is dépendent on the exact représentation chosen for the syntax of £ and is outside the scope of this discussion. An example représentation may be found in appendix A.4. 75 Once the représentation of the syntax has been constructed the interpréter function can be moved within the semantics of £ by composing it with the encode and décode transformations. rep-interpréter = encode o interpréter o décode For each function Fj:a-+b ' Isyn(a) —> Isyn(b) we can also construct the function repJFf:a-+b by composition with encode and décode. rep J7/^—6 = encode^ o Fj:a-+b ° decodea We can now formalise a notion of a language with sufficient power to express its self interpréter. The language £ is powerful enough to express its self-interpreter if the following holds: V* G GsynO ' rep-interpréter t 6 E*(Isem)(Syn). Less formally, the language £ can express its self-interpreter if its semantics contains the arrow rep-interpréter t for every node, t, from the graph of Syn. We should note that rep-interpréter is defined in terms of the rep-Ff:a-*b functions so if the semantics of £ contains the arrows rep-interpréter t for each node t it will also contain the arrow rep-F/:a—b for every arrow / : a -> b of Syn. The predicate above is really too abstract to tell us much about the nature of the language £ because it does not relate to any language features. We would, however, expect £ to provide methods of constructing: Binary trees: Which are necessary to represent £ programs as data objects. Conditional: We require some form of conditional in order to be able to sélect the correct code segments to simulate a particular syntactic construct in an £ program. Recursive functions: Thèse are necessary to enable us to form the code segments necessary to simulate the behaviour of the syntactic constructs of the language £. 76 Thèse requirements may be met directly by £, as is the case for the Toy language defined in appendix A, or indirectly as would be the case if £ were, say, an assembler language. In this second case £ does not provide either binary trees or recursive functions but is sufficiently powerful to be used to construct implementations of both. 6.3 The self-interpreter For a suitable language, £ = (Sem, Syn,E : Syn -> Sem, learn : Em(Isem) —• Isyn), the category Em(Isem)(Syn) contains the arrows, {rep-interprétert : t £ Gsemo}, which are the functions the £ self-interpreter, C-self-int, computes. To complète the construction of C-self-int we must convert thèse functions into an £ program. To perform this conversion we require an algorithm which générâtes an £ program, C-selfint, such that eval(C-self-int) = rep -interpréter 9, where s is the node of Syn which dénotes complète £ programs. Provided we make the, not unreasonable, assumption that the notation used to represent the rep -interpréter function has a fixed syntax and semantics, this algorithm is, in fact, a parameterised compiler. The extra pièces of information which we must supply as parameters of the compiler are: 1. the syntactic construct which £ uses to define functions. 2. The £ syntactic construct corresponding to a function call. 3. The form of conditional used by £. Thèse parameters are required because the rep-interpréter function is structured as a set of functions which perform re-writes of the encoding of the syntax of £. We therefore need to be able to: 1. define functions in C-self-int which perform thèse re-writes. 2. Generate calls of thèse re-writing functions. 3. Generate conditionals to décide which re-writing function to call in a given situation. In appendix A we define Toy, a simple, typeless, first order functional language. Functions in Toy can only be defined at the top level and hâve one implicit argument, named arg in the body of the function. The only data objects in Toy are natural numbers and binary trees. We can test natural numbers for equality using the = operator and construct and destruct binary trees using the (.,_) and f s t , snd operators respectively. The function which our Toy self-interpreter computes is shown in appendix A.5.2. Below we outline the final stage of the construction of the self-interpreter. Note that for the sake of clarity we hâve used arabic mimerais and meaningful identifiers rather than the Toy syntactic constructs. The node of the sketch ToySyn which corresponds to complète Toy programs is named prg. We can use this information to index the component of repJnt corresponding to the top level of the self-interpreter. rep.intVTg = ( 1 0 , ( 9 , ( e , d ) ) ) - rep-Fwhm:expxdecs^prg(e,d) This allows us to construct the top level of the self-interpreter as a call to the function *where. •where(arg) where We now use the définition given by theorem 6.1.1 of rep-F whtTt.txpxdtC5_prg rep-Fwkere:tx?xdecs_prg(e,d) = (10 AS Arep-F apply:expxdecs^tTp(x, shown below y) 9 (3 9(090))))) to add the définition of *where to the self-interpreter. •where(arg) where *where * ( 1 0 , ( 9 , ( * a p p l y ( a r g ) , ( 3 , ( 0 , 0 ) ) ) ) ; Since rep-F^ereicxpxdecs-*prg is defined in terms of rep-Favpiv.txpxdecs-^prg, we must use its définition 78 rep-Fapply:txpxdecs^exp(^^090)).d) = (4,(0,0)) nep.Fapp/y:cXpXrfccJ^cxp((4,(0,l)),d) = (4,(0.1)) reP-Fapply:expxdec3-+exp(U>(l>rihd) = ( 4 . ( 1 , II)) ™P-Fapply.expxdecs^exp( = rep-Ffst:txV-+tTV{reP-F}apply'.expxdecs-.exp(ei = ™P-F snd:txp_exp(rep ( 4 , ( 2 , e ) ) , d) re P-Fapply:expxdec3-+exp((4>(3 reP-Fapply:expxdec3-+exp( »€^ ^) rep-Fapply:txpxdecs^exp(C4» where d), rep-Fapply,expxdecs^txp(y, d )) d)) ) ) ( 4 , ( 5 , ( 5 , ( x , y ) ) ) ) , d) (6> ( 6 , ( x , (y,z))))),d) apply:expxdec3—*exp\reP-* if:expXeTpXcxp-+cTp\reP-*i reP-Fapply:expxdecs^exp( = -Fapply:expxdec3-+exp(€i ^P^=:expxexp^tJn>(^P^apply:expxdec3^exp(x^d),repJpapp^^^ = = rep-t )) ( 4 , ( 4 , ( 5 , ( x , y ) ) ) ) , d) = ( 4 , ( 4 , (rep-Fapply:expxdecs^cxp(x, ™P-Fapply:expxdecs-*exp{ d apply:expxdecs->exp\xf ")» !/> 2 j , a J ( 4 , ( 7 , ( t , e ) ) ) , d) repJrapp/y:CxpX(fCC5->Cxp(^ tody = rep-Ffetch:idenixdecs^txp(i, d) to construct the définition of *apply which we then add to the self-interpreter. •apply = if f s t ( f s t ( a r g ) ) = 4 then if f s t ( s n d ( f s t ( a r g ) ) ) = 0 then fst(arg) else if f s t ( s n d ( f s t ( a r g ) ) ) - 1 then f s t ( a r g ) else if f s t ( s n d ( f s t ( a r g ) ) ) = 2 then •fst(•apply((snd(fst(arg)),snd(arg))) else if f s t ( s n d ( f s t ( a r g ) ) ) • 3 then *snd(*apply((snd(fst(arg)),snd(arg))) else if f s t ( s n d ( f s t ( a r g ) ) ) * 4 then (4,(4,(*apply((fst(snd(snd(snd(fst(arg))))),snd(arg))), •apply((snd(snd(snd(snd(fst(arg))))),snd(arg) ) ) ) ) ) else i f f s t ( s n d ( f s t ( a r g ) ) ) = 5 then *=(*apply((fst(snd(snd(snd(fst(arg))))).snd(arg))), *apply((snd(snd(snd(snd(fst(arg))))).snd(arg)))) else if fst(snd(fst(arg))) = 6 then •apply ( (*if ( (•apply ( (f st (snd(snd(snd(f st (arg) ) ) ) ) , snd(arg) ) ) , (fst(snd(snd(snd(snd(fst(arg)))))), 79 snd(snd(snd(snd(snd(fst(arg))))))))), snd(arg))) e l s e if f s t ( s n d ( f s t ( a r g ) ) ) = 7 then •apply((+replace((+fetch(fst(snd(snd(fst(arg))))),snd(arg))), •apply((snd(snd(snd(fst(arg)))),snd(arg))))) e l s e error e l s e error; Each clause of the définition of rep-Fapply,txpxdecs-+exp a d d s a conditional branch to +apply and to complète the définition of this function we must construct implementations of the functions: rep-Fjst:exp-+exp, rep-Frotact^xcrp-cxp, rep-Fsnd:txv^txv, rep-F =:crpX crp—crp, rep-Fif-.cxpxexpxcxp^cxp, reP-Ffetch:idcntxdCcs-.cxp- Thèse functions implement the language opérations: fst, snd, = , if, and call, where call is actually implemented using apply, replace, and fetch. rep-Ff3t:exp_exp(x) = (4,(0,1)), x = (4,(0,1)) = x, x=(4,(l,y)) = a, x = (4,(4,(5,(a,6)))) = (4,(2,x)), otherwise This function gives us the définition of +f st. • f s t = i f fst(arg) « 4 then i f fst(snd(arg)) = 0 then if snd(snd(arg)) = 1 then (4,(0,1)) else error else if fst(snd(arg)) = 1 then arg else if fst(snd(arg)) * 4 then fst(snd(snd(snd(arg)))) else (4,(2,arg)) else (4,(2,arg)); 80 rep-Fênd:exp^exp(x) = (4,(0,1)), x = (4,(0,1)) = x, x = (4,(1,y)) = 6, x = (4,(4,(5,(a,6)))) = (4,(3,x)), otherwise The function TepJFsnd:exp_^txp provides the implementation of •snd shown. •snd = if f s t ( a r g ) = 4 then if f s t ( s n d ( a r g ) ) * 0 then if snd(snd(arg)) = 1 then ( 4 , ( 0 , 1 ) ) else error e l s e if f s t ( s n d ( a r g ) ) = 1 then arg e l s e if f s t ( s n d ( a r g ) ) = 4 then s n d ( s n d ( s n d ( s n d ( a r g ) ) ) ) else (4,(3,arg)) else (4,(3,arg)); The function repJ r = : c r j , x c r p _ e r ? ) is defined as reP-^=:«pxerp-Crp (*>!/) = (4,(l,rep.e 9 tia/(a,6))), x = (4,(1,a)) A y = (4,(1,6)) = (4,(0,1)), x = (4,(4,a)) V y = (4,(4,6)) V x = (4,(0,1)) V y = (4,(0,1)) = where (4,(5,(x,y))), otherwise rep-equal( ( 2 , 0 ) , ( 2 , 0 ) ) = (2,0) rep.e9iia/((2,x = (2,1) rep.eçtia/((2,0),(2,x+l)) = (2,1) rep.eçtia/((2,x + l ) , ( 2 , y + D ) = rep.equal(x,y) + 1),(2,0)) and adds •* to the self-interpreter. •= * if • a n d ( ( f s t ( f s t ( a r g ) ) * 4 , f s t ( s n d ( a r g ) ) * 4 ) ) then i f • a n d ( ( f s t ( s n d ( f s t ( a r g ) ) ) - l , f s t ( s n d ( s n d ( a r g ) ) ) - l ) ) then (4,(1,•rep.equal((snd(snd(fst(arg))),snd(snd(snd(arg))))))) else if •or((^and((fst(snd(fst(arg)))*4,fst(snd(snd(arg)))=4)), 81 •and((•and((fst(snd(fst(arg)))=0, snd(snd(fst(arg)))=D), •and((fst(snd(snd(arg)))=0, snd(snd(snd(arg)))=l)))))) then (4,(0,1)) else (4,(5,arg)) else error; Since the définition of rep-F=:expxtxp—ix? is given in terms of the function rep-equal we must also construct •rep-equal. In addition, for the sake of readability, we hâve defined the functions +and and •or. • r e p . e q u a l = if • a n d ( ( f s t ( f s t ( a r g ) ) = 2 , f s t ( s n d ( a r g ) ) = 2 ) ) then (2,snd(fst(arg))=snd(snd(arg))) else error; •and = if f s t ( a r g ) then snd(arg) e l s e f s t ( a r g ) ; •or = if f s t ( a r g ) then f s t ( a r g ) e l s e s n d ( a r g ) ; The définition of rep-Fif:exTXexvXtrp-.esP shown below requires no auxiliary functions. re P'Fif:expXexpXexp^exp(x,y,z) = (4,(0,1)), x =(4,(0,1)) = y, x =(4,(1,0)) = 2, x = ( 4 , ( l , y + D ) Vx = (4,(4,a)) = (4, ( 6 , ( 6 , (x, ( y , 2 ) ) ) ) ) . otherwise We therefore only need to add • i f to the self-interpreter to implement it. • i f = if f s t ( f s t ( a r g ) ) = 4 then i f • a n d ( ( f s t ( s n d ( f s t ( a r g ) ) ) « 0 , s n d ( s n d ( f s t ( a r g ) ) ) = D ) then (4,(0,1)) e l s e i f • a n d ( ( f s t ( s n d ( f s t ( a r g ) ) ) = l , s n d ( s n d ( f s t ( a r g ) ) ) = 0 ) ) then 82 fst(snd(arg)) else if *or((fst(snd(fst(arg)))=l,fst(snd(fst(arg)))=4)) then snd(snd(arg)) else (4,(6,(6,(fst(arg),(fst(snd(arg)),snd(snd(arg))))))) else (4,(6,(6,(fst(arg),(fst(snd(arg)),snd(snd(arg))))))); The opération rep-Fnpuee:ezfXtxp->exp also becomes a single Toy function in the implementa- tion. ^P-Frtvhcf.trvx « , - e * , ( W . < ° . 0 » » r ) = r rep-FTepUct:txJ,xtxp^erj,(^AO,l)),r) = (4,(0.1)) rep-F„p/ace:MJ)XeIJ,_eip((4,(l,n)),r) = (4,(l,n)) rep-Frej),ace:MÏ, x e r p _ e x p ( ( 4 , ( 2 , e) ) , r) r€ P-Fjst:ezp->exp\reP-Frtplacc:expXtxp-~ezp{eir)) reP-Fnplacc:expXcTp^cTp(^.^,€)),r) TZP-Ï sndiexpXcrp—teTpK^P-* replace : exp x exp —• exp Ie'? r)) reP-Frtplacc-.txpxtTp-expite'te'te'tX'ymhr) = rep_.T _ . e r j , X e r j ) _ e l j , ( r e p _ r TepUct:txpxtxp-*txp\xiT)i *' replace:expxexp—>exp{yi T)) «P-F,rep/««:exPxexP-.erP((4,(4,(5,(l,y)))),r) = trep_T rep/ace:expxexp-*erp(.a'' T)>reP-*' nP-Frcplacf.expx r )' « ? - « ? ( ( 4 . ( 6 » ( 6 . ( x , (y , * ) ) ) ) ) . r) = where Ttplact:txpxtxp — txp\.yi x' = repJrreplace:expXexp^exp(x,r) y' = rep-Freplace:expXexp^exp(y,r) Z = reP-T TCP-* \]itxpxexpxexp—>exp\x lit iz ) replacc:txpxtxp-*exp\z'>r) rep-Freplaee:txpXtXT^tx?((4A7A7>(i,e)))),r) = (4,(7,(7,(i,nep^rc7,/acc:erpxcr7>^CX7,(e,r))))) •replace * if fst(fst(arg)) * 4 then if fst(snd(fst(arg))) = 0 then if snd(snd(fst(arg))) = 0 then snd(arg) else (4,(0,1)) e l s e i f f s t ( s n d ( f s t ( a r g ) ) ) • 1 then f s t ( a r g ) 83 else if fst(snd(fst(arg))) = 2 then •fst(+replace((snd(snd(fst(arg))),snd(arg)))) else if fst(snd(fst(arg))) = 3 then •snd(+replace((snd(snd(fst(arg))),snd(arg)))) else if fst(snd(fst(arg))) = 5 then •=((+replace((fst(snd(snd(snd(fst(arg))))),snd(arg))), •replace((snd(snd(snd(snd(fst(arg))))),snd(arg))))) else if fst(snd(fst(arg))) = 4 then (•replace((fst(snd(snd(snd(fst(arg))))),snd(arg))), •replace((snd(snd(snd(snd(fst(arg))))),snd(arg)))) else if fst(snd(fst(arg))) = 6 then •if((•replace((fst(snd(snd(snd(fst(arg))))),snd(arg))), (•replace((fst(snd(snd(snd(snd(fst(arg)))))), snd(arg))), •replace((snd(snd(snd(snd(snd(fst(arg)))))), snd(arg)))))) else if fst(snd(fst(arg))) = 7 then (4,(7,(7,(fst(snd(snd(snd(fst(arg))))), •replace((snd(snd(snd(snd(fst(arg))))), snd(arg))))))); In the définition of repJFreplaeeîexpxexp^txp we only encounter one function for which we do not already hâve a Toy implementation, namely rep-Ffetch:identxdec8-+exp reP-Ffetck:identxdecs^exp(*,te>(°>0») = (4,(0,1)) nep.F / c ^ : ^ c n < x ^ C J ^ c r p (x,(3,(l,(8,(y,(e,d)))))) = rep-Fget:identxnumxtxpxdecs-*txp\xi l^P-ï 8amc:identxident-mum\x) We implement this function as +f etch. •fetch = if fst(snd(arg)) = 3 then if fst(snd(snd(arg))) = 0 then (4,(0,1)) else if fst(snd(snd(arg))) = 1 then •get((fst(arg), 84 V)) ei **) (•same((fst(arg),fst(snd(snd(snd(snd(arg))))))), (fst(snd(snd(snd(snd(snd(arg)))))), snd (snd(snd(snd(snd(snd(arg)))))))))) else error; else error; The rep-F}tuh'.identxdec8-+expfonctionis defined in terms of two new functions ™P-F 9eUidentxnumXexpxdecs-+txp{xM >Q) ,C,d) = reP-E getiidentxnumxexpxdeca-* « r p ( x > ( l , fl + D > * , d ) = e re P-Ffetch:identxdec8-+exp{X'>d) and »«P-^Mme:We» Sem, learn : E*(Isem) -• Isyn). Sem and Syn are FL sketches, and E : Syn —• Sem is a sketch morphism such that Syn is learnable from Sem. The syntax and semantics of £ are both constructed as models of Syn, where the syntax is constructed as the initial model: Isyn ' Syn -» S E T . We use property 4.3.1 to construct the semantics of C as the model E*(ISem):Syn-+ SET where Isem • Sem —• SET is the initial model of Sem in S E T . The construction of eval as the natural transformation eval :Isyn -^ Em(IStm) arises from property 4.3.2. Since Sem, Syn, and E : Syn —• Sem are such that Syn is learnable from Sem we can use proposition 4.3.2 to construct the components of the learn transformation learn : E*(Isem) - • h.yn such that eval o learn = l£»(/ 5em ) and the language C is fully specified. The extremely abstract nature of the language spécification enables very gênerai properties of languages and classes of languages to be studied and understood. 88 Since the category Mod(Syn) is a full reflexive sub-category of [Syn, SET] we can obtain a great deal of information about any class of languages without ever having to consider the détails of an individual language, simply by studying what is known about the category [Syn, SET]. An example language spécification using the sketch based model of language is given in appendix A. The sketch describing the semantics of Toy is an extremely large and complex object, much more so than, say, a domain theoretic semantics for the same language. The complexity arises in a number of way s. Firstly it is due to the fact that every object used in a sketch must be described explicitly from a few basic constants and opérations, we cannot for example simply assume the existence of a particular product, we must construct that product. To paraphrase Barr and Wells [BaWe90] pp 172, "when ail the girders and braces are exposed the true complexity of an object is revealed." This may be no bad thing as it forces the language spécifier to consider exactly what properties he or she requires of each "girder", and certainly it is what allows us to define models of a sketch in an arbitrary category. Secondly the model of language based on sketches is essentially context free and programming languages are not. To explain, the meaning of the expression x + 1, where x is an identifier, dépends on exactly what value x is bound to when it is evaluated. In other words, in différent context s or environments, x + 1 will hâve différent meanings and so the language has a context sensitive1 aspect. Since the categorical model of language describes the évaluation function of a programming language as a natural transformation we know that the diagram below commutes. ISyniA) - eval/L E'{IStm)(A) ISyn(B) evals E.{Isen)U) ' EVstm){B) The fact that eval A is a function, combined with the commutativity of the diagram above forces eval&(x), where x € Isyn(A), to hâve a constant value even when the term x is 1 This use of the term context sensitive refers to the semantics of the language and should not be confused with the term context sensitive as used to describe a language whose grammar falls into type 1 of the Chomsky hierarchy. 89 embedded in the larger term Isyn(f)(x)- This forces x to hâve the same meaning regardless of its context and thus forces the model to be essentially context free. To overcome this problem we hâve to introduce more cônes and auxiliary opérations to put terms like x into a correct context and then détermine the value of this context, rather than just the value of x. This can add a great deal of complexity to the sketch as illustrated by the semantics of Toy in appendix section A.2. We shall return to this problem in section 7.3. As it stands at the moment the model of language is unrealistic as it does not constrain the évaluation order of the language. In appendix A, for example, the semantics of Toy does not state whether Toy uses call-by-value or call-by-need semantics. This is a serious deficiency in any language spécification method, but is potentially disastrous if the spécification method is used to specify the semantics of a functional language like Toy. This information is missing because we use SET to model the sketch specifying the semantics of a programming language. Since we can construct our categorical model of language in any category we could rectify this omission by constructing a sketch of the semantics of Toy to be modelled in DOM, the category of domains and continuous functions. In moving to DOM we would, however, add to the complexity of the sketch without gaining any new insight into the technique for the construction of the self-interpreter. For this reason the work in this thesis has centred on models in SET only. A third criticism of the model of language concerns the nature of the learn transformation. Since learn lacks any form of naturality condition its usefulness is strictly limited. There hâve been a number of attempts to weaken the naturality condition from the définition of natural transformation. Several such weaker conditions are contained in [Copp80] and thèse should certainly be explored. In spite of thèse disadvantages the model of language we hâve constructed is not without merit. As we illustrated in section 5.4 we can include limits which are more complex than simple product s. Thèse limits can be included in both the syntax and the semantics, allowing us to capture the static semantics of a language in the spécification of its syntax if we wish. This is a considérable enhancement over the algebraic model developed by Rus. At the cost of moving away from initial models of the semantics we could also include colimits in the models of programming language semantics and further simplify the spécification of language semantics as Kortas and Quatrain demonstrate in [KoQu92]. 90 Finally, in [BaWe90], pp 171, Barr and Wells state: "A deeper différence is that there are no distinguished nodes or opérations in a sketch. The graph of the sketch for semigroups, for example, has three nodes, no one singled out, whereas in the usual définition of semigroup, the underlying set S ... is singled out and other things are defined in terms of it. Similarly in the graph there are various arrows; c is just one of them." In other words, "ail the objects and opérations specified by a sketch hâve equal status." This can cause a problem if we hâve something complex to specify. Just as it can be useful to hâve hidden sorts and opérations in an algebraic spécification it can also be useful to conceal parts of the inner structure of a sketch, either to specify the interface to a data sort or to formally draw attention to spécifie parts of a spécification. Although Barr and Wells are quite correct when they state that there are no distinguished nodes (or opérations) in a single sketch, proposition 4.3.1 which is used hère to specify the semantics of a programming language, in effect, provide a mechanism by which any nodes or edges of a sketch can be distinguished from the remaining parts of the sketch. To explain, when we construct the sketch morphism E : Syn -» Sem what we are actually doing is picking out some of the nodes and edges of Sem as being of spécial interest. Formally, because E : Syn -» Sem allows us to use property 4.3.1 to construct the functor E* : Mod(Sem) -> Mod(5yn) we can use E* to construct a model of Syn. From proposition 4.3.1 we know that this model of Syn, Em(Isem) - Syn —• SET has the properties of the given model of Sem, Isem ' Sem -+ SET, and can be used to specify the external interface of an abstract data type. We can therefore use proposition 4.3.1 to provide a mechanism to distinguish éléments of a sketch as being of spécial interest. 7.1.2 The self-interpreter construction technique Suppose we hâve a language C = (Sem, Syn,E : Syn - • Sem, learn : E*(Isem) - • Isyn) 91 specified using the categorical model of language above. We can describe the function which an interpréter for this language computes using the expression interpréter = learn o eval where eval is the évaluation natural transformation eval :Isyn -^ E*(ISem) used in the construction of learn. If we then take a pair of transformations encode : ISyn — E*(ISem) décode : Em(ISem) — hyn which describe an encoding of the syntax of C within the semantics of C we can construct a family of arrows rep-interpréter = encode o learn o eval o décode which may also lie inside the semantics of C, if C is powerful enough to describe its own interpréter. It is then a fairly simple matter to use the structure of rep-interpreter and theorem 6.1.1 to construct an C program, C-self-int, which computes the function rep -interpréter s, where Sis the start symbol of the grammar of C. The program C-self-int is the self-interpreter for the language C. This is the case because the spécification of a programming language, however given, must in some sensé be the description of an interpréter for that language. In the case of our categorical model of language this description is relatively clear as it exists in the form of the eval and learn transformations. As a resuit of this we hâve a fairly straightforward, if time consuming, process of symbol manipulation by which we can produce the function rep-interpreter. To transform the description of repJnterpreter into a self-interpreter is still, 92 unfortunately, something of an art form. We rely on a programmera intuition for the last step in the dérivation of the self-interpreter. As shown in section 6.3 the programmer is needed to supply the C syntactic forms of function définition, function application, and conditional. This is because there are simply too many différent ways of providing thèse constructs in a programming language. For example, conditional can be realised as: if .. .then, if .. .then .. .else, case, pattern matching, computed goto, etc. Thèse constructs ail generate significantly différent structures within the semantics of a programming language. To make matters worse there are very many différent mechanisms that the language spécifier may use within Sem to specify the semantics of any single one of thèse constructs, particularly if we allow the spécifier to work with models of Sem in catégories other than S E T . This makes the construction of a gênerai analysis procédure to recognise the structure of conditional at least extremely difficult. It may even make it impossible. This begs the question: " of what value is the self-interpreter construction technique described hère?" In my view it is not likely to lead to a completely automatic process, but it still has value because it does produce a complète description of the C self-interpreter as a function within the semantics of C. Even if we cannot use the self-interpreter dérivation process to construct the actual program code we can still use it to construct a design of this code which is so highly detailed that any programmer who knows how to define and call functions and express conditionals in C can write the code for C-self-int with little need for extra intellectual effort. 7.2 Partial evaluators and interpreters The true compiler generator system discussed in section 2.2 dépends on a pair of assumptions, re-stated below. Assumption 1. there is a technique which allows us to examine the spécification of a computer language, T , and from this spécification, calculate a T program which implements mix for the language T. 93 Assumption 2. given the spécifications of two languages, S, and T , it is possible to dérive an implementation of S in the form of an interpréter expressed as a T program. The self-interpreter calculation technique was originally proposed as a useful first step towards justifying thèse assumptions. In sections 7.2.1 and 7.2.2 we discuss exactly how large this first step is. 7.2.1 Partial evaluators There are two distinct problems which need to be solved before a technique for deriving a self-interpreter can be converted into a technique for deriving a partial evaluator. Firstly, we must develop a method which allows us to dérive the binding time analysis phase of the partial evaluator. The work of Launchbury [Laun90] using dépendent sums to factorise domains into their static and dynamic values offers a promising starting point as it is a significant step towards the formalisation of the process of binding time analysis. It is, however, not at ail clear how to incorporate this work into the categorical method developed hère. The second problem is the transformation of a self-interpreter into the function spécialisation phase of a partial evaluator. In principle it should be possible to modify both the syntax and semantics of C by adding éléments to represent dynamic values. Since dynamic values are not reduced by the function spécialisation phase of a partial evaluator we would not need to alter the diagrams in the sketch describing the semantics of C. The process used to dérive the self-interpreter with the original semantics should now construct a function spécialiser when applied to the altered semantics. This is because a function spécialiser behaves exactly like an interpréter when it is working with static values, and suspends évaluation when it encounters a dynamic value. The original diagrams of the sketch of the semantics are therefore sufficient to deal with static values, and since dynamic values are not reduced, no new diagrams are required to describe their réduction. Unfortunately, without a complète description of the binding time analysis phase, we cannot begin to solve this second problem because we would hâve no clear idea of where a dynamic value could occur and so do not know where we need to add new values to the syntax and semantics of C. 94 Clearly, there is still a very long way to go before the automatic dérivation of a partial evaluator is a practical proposition. This is not the case with the second assumption as we explain below. 7.2.2 Interpreters The fact that Assumption 2 fairs rather better than Assumption 1 is almost certainly due to the fact that the généralisation from self-interpreter to interpréter is much smaller than that from self-interpreter to partial evaluator. Because of the close relationship between an interpréter and a self-interpreter the techniques used hère to calculate a self-interpreter for language S can also be used to calculate an S interpréter in language T given sketch spécifications of both S and T. The extra generality of the technique arises because the composition of learn and eval spécifies the function to be computed by an S interpréter, not the S interpréter itself. To get from the function to the actual interpréter we need to construct a représentation of the syntax of «S as a data object within the semantics of S. The interpréter is then produced by implementing the function rep-interpreter. To recap: to represent the syntax of S within the semantics of S we require a pair of transformations encode : I§,n ^ décode : E'(I§em) - E'(llJ /|,n with the property that décode o encode = 1 is . The interpréter function is then embedded Syn within this représentation as interpret = encode o learn o eval o décode to move it within the semantics of S. To construct an S interpréter in the programming language T we can replace the représentation functions encode and décode by a pair of transformations which represent the syntax 95 of «S as a datatype within the semantics of the arbitrary language T: encodeT: / f , B - > £ - ( J j m ) décoder :E'(IU -+/*„. This allows us to move the S interpréter function into the semantics of T: interpret = encodej o learn o eval o decodej provided that T is sufïiciently powerful to express the interpréter for the language S. The remainder of the interpréter calculation process then proceeds exactly as before. The only extra requirement necessary to use the technique for the calculation of a gênerai S interpréter is that we can construct a représentation of the S syntax within the semantics of T. 7.2.3 The true compiler generator The true compiler generator system discussed in section 2.2 is it seems still a long way off. We are still unable to dérive the actual program code of mix for the target language and we cannot dérive the code for int, the source interpréter, either. So hâve we actually advanced towards this goal at ail? The answer to this question is, I believe, yes! While we cannot, as yet, dérive a C self-interpreter we can at least dérive a définition of the function which an C self-interpreter computes. In section 7.2.2 above we indicated that we can even généralise this dérivation process to dérive the interpréter function for an S interpréter as a T program. To construct a true compiler generator of sorts we need only accomplish one more task. We need to be able to dérive the binding time analysis for the language T. If we can achieve this we can construct a true compiler generator because we can at least dérive the two functions below. 1. repjmix the function which a T partial evaluator computes. 2. rep-int the function which a T implementation of an S interpréter computes. 96 Provided we use a standard language, TZ, to describe thèse functions we can construct the compiler generator shown in figure 7.1. user specified TZ-+T compiler source language spécification (S) Compiler- Generator S —• T compiler target language spécification (T) Figure 7.1: A différent true compiler generator system This system accepts as input: the spécification of the source language S, the spécification of the target language T, and a compiler which translates from the internai représentation 71 to the target language T. The process discussed in the preceding chapters can then be used to dérive the TZ représentations of rep-mix and rep-int. The given 71 —• T compiler is used to generate mix and int as T programs. We can then realise the S —> T compiler as mix^mix, int\ While this is not the compiler génération system envisagea in chapter 2 is is still an improvement over the current situation because we do not need to specify the S —• T relationship. The burden of proof on the compiler writer is therefore reduced since they only need to prove the TZ —• T compiler correct rather than having to prove a différent S -+ T relationship for each language S. Even without the ability to calculate the binding time analysis for the language T we can construct a compiler generator (shown in figure 7.2) which does not require the user to define the S —• T relationship. The opération of this system is similar to the system shown in figure 7.1 except that mix is supplied by the user rather than calculated as part of the génération process. With this last system the compiler writer's proof obligations are again increased as they must now prove mix correct in addition to the TZ —• T compiler, but once again thèse proofs need only be 97 user specified 7Z-+T compiler source language spécification (S) S —* T compiler Compiler- Generator target language spécification (T) user specified T implementation of mix Figure 7.2: A final true compiler generator carried out once for each target language T. There is an interesting parallel between the approach that both compiler génération Systems above use to construct the S —• T relationship (encoded in the program int) and the usual construction of a semantics directed compiler. Typically a semantics directed compiler is factorised into a front end which translates source language sentences into some universal intermediate language and a back end which translates from the intermediate language to the targetlanguage. Source Language front end Intermediate Language back end Target Language With the compiler génération Systems outlined in this section we factorise the construction of the S —• T relationship into a front and back end. The back end of this process is the 7Z-+T compiler provided by the user. We use a universal intermediate language TZ to describe the S —> T relationship. The front end is the process for calculating the rep-int function described in this thesis. Source Language _ Spécification S front end Description of rep-int in TZ 98 TZ —p T compiler Description of int in T In spite of thèse similarities there are two striking différences between the approach we propose and that of a semantics directed compiler. Firstly a semantics directed compiler factorises the actual process of translating individual sentences from S into T. Our approach opérâtes as a higher level and factorises the construction of the S —• T relationship. Secondly, with a semantics directed compiler the front end is spécifie to a particular source programming language S. In our approach the front end is universal. 7.2.4 Open questions Hère we examine some open questions about the true compiler génération technique. With the exception of question 4, ail the questions below are related to the single question, "Do we really want compilers which are produced without human intervention?" 1. How much static computation is there in mix(mix,int) when both mix and int are machine generated? This is a very important question since the power of partial évaluation dépends on the ability to eliminate static computation. Consider the function /(x,y) = x+ l +y Partial évaluation of the expression / ( 4 , y), where y is dynamic, produces the function A(y) = 5 + y because the expression x + 1 is static if x is static. If, on the other hand, / i s expressed as /(x,y) = x+ y+ 1 then there is no static computation because x + y is dynamic, unless both x and y are static, and so partial évaluation gives no improvement in the cost of Computing / 4 . In other words, the improvement gained by partial évaluation of a program dépends on 99 the style in which that program is written. We currently do not know whether the style of a machine generated int and mix will be "partial évaluation friendly" or not. The problem of transforming "partial évaluation unfriendly" functions into "friendly" ones is addressed in [HoHu90] where the technique of obtaining "free theorems" from a functions polymorphic type, developed by Wadler [Wadl89], is used to dérive transformation rules. This technique is still in its infancy but seems like a good starting point for the related problem of synthesising "partial évaluation friendly" implementations of int and mix from language spécifications expressed as sketches. 2. Can we ensure that a machine generated compiler will generate good quality object code? In some respects this question is related to the previous one. The more static computation contained in the expression mix(mix,int) the better the object code generated by the compiler is likely to be. This, however, is not the only issue in the efïiciency of the generated target code, for example, a compiler generated from an interpréter written using labels and "goto" to express its control flow is likely to generate better target code than the code generated if the interpréter uses recursion exclusively. This issue will need to be examined in détail before the proposed true compiler génération technique becomes viable for the génération of "industrial quality" compilers. 3. Is the technique applicable to imperative languages? The assumption that we are dealing with functional languages has been implicit throughout the preceding chapters. Although the categorical model of language is capable of specifying an imperative language in theory, this has not been done yet. In [KoQu92] Kortas and Quatrain give a spécification of a subset of the pascal language, however the subset that they use avoids having to specify the store. It is in the spécification of the store (and of assignment) that the most serious problems are to be encountered so whilst this work provides a useful insight into this use of sketches it leaves several questions unanswered. Any problems encountered in the synthesis of mix and int for a functional language are likely to be at least an order of magnitude worse for an imperative language. This question cannot be answered without a great deal more work. 4. Can sketches be implemented on a computer? 100 By using the techniques for constructing implementations of categorical constructs given in [RyBu88] we can certainly construct implementations of graph, diagram, cône, cocone, and model (functor) which would allow us to implement a spécifie sketch. This, however, is not what we mean by implementation of sketches on a computer because for each sketch we would need to construct its implementation by hand. When we ask "can sketches be implemented on a computer" we mean: can we construct an computer program which will, given an arbitrary sketch, automatically generate an implementation of the datatype specified by that sketch? The answer to this question has to be a qualified no. Work has been undertaken in this area, for example Gray's work using Mathematica [Gray?], and the work of Yusop [Yuso91] using prolog. There are some quite serious problems with implementing sketches because, as with algebraic spécifications, it is possible to use sketches to specify objects which are simply unimplementable on a computer, or to write sketches in a style which is non-constructive therefore not directly implementable on a computer. The problems above are fairly gênerai problems with the implementation of formai spécifications. Of the problems spécifie to the implementation of sketches the most obvious ones are caused by the fact that sketches can be modelled in an arbitrary category and do not always hâve an initial model. This problem even arises in SET. It is true that every FL sketch has a term model but this is not the case for every class of sketch. Thèse problems will hâve to be addressed before a useful technique for the implementation of sketches can be developed. As a starting point we suggest the technique of dynamic évaluation developed by Duval and Raynaud [DuRa91] which provides an interesting and promising approach to this problem. 5. Do we really want compilers which are produced without human intervention? This question is basically impossible to answer. In [Schm85] Schmidt briefly argues that a compiler génération system which requires more décisions from the implementor than is normal can be an advantage as the extra freedom of choice allows the implementor to orient the implementation towards the spécifie hardware and software available. It is indubitably true that when the user has to provide the implementation relationship such orientation is possible; what is less clear is that such orientation is not possible when the implementation relationship is automatically produced from the spécifications of the source and target languages. Sketches would seem to be an idéal method of representing 101 the source and target languages in this context since, by their very nature, every détail in a language spécification must be stated explicitly and is therefore readily available to any software for calculating an implementation relationship. Due to the categorical nature of sketches this software could also hâve some extremely powerful analytical tools available to it. To the best of my knowledge nobody has examined thèse issues in any détail. 7.3 More science fiction: a better model of language? There is one fundamental problem with the categorical model of language discussed above. The language spécifications developed using this technique are far too large and unwieldy. The resuit of this is that a language spécification using sketches is almost impossible to work with. The reasons for this complexity are illustrated in section 5.4.2, explained in section 7.1.1 and can be summarised in one sentence. Sketches cannot be used to specify functions as objects. If we could describe higher order objects using sketches, or some related tool, we could drastically reduce the complexity of the sketch describing the semantics of a programming language. A function is an extremely natural way to describe context sensitivity within a formai system. The context sensitive object becomes a function and its context can be passed into it as its argument. It is using this technique that a denotational semantics typically handles context sensitivity, the typical évaluation function for an expression looking something like S : Expression —> Environment —• Value. So the meaning of an expression, exp, is the function £(exp) : Environment —• Value which expects its context (the environment) and will only produce an actual value when given this context. 102 There are a number of extensions to the concept of a sketch which could possibly be used to solve this problem. The first of thèse extensions is the form which is described by Wells in [Well90]. A form is essentially a sketch but we hâve the additional ability to require diagrams to become instances of any essentially algebraic categorical construction when modelled. Although there is insufïicient space to describe the approach in any détail hère the basic idea is to provide a uniform method for defining the primitive types and opérations on which the constructors specified within a sketch can operate. This allows the introduction of objects other than limits and colimits within the model of a sketch, in particular function objects can be specified for forms modelled in a cartesian closed category. Using this technique Wells hopes to be able to specify functional programming languages using sketches. A second extension to the concept of sketch which may allow function objects to be introduced is the <*rame> described by Lair in [Lair87b]. The model of language developed in this thesis exists within an extremely gênerai framework and is, as a resuit, easy to extend. The model is not tied to any spécifie procédure for the calculation of models of Sem so we can easily incorporate developments like dynamic évaluation [DuRa91] to increase the power of the model by allowing the sketch Sem to be modelled in new ways. We can even replace the sketch Sem, describing the semantics of a programming language by any graph theoretic structure, X, containing cônes and diagrams. This is because the key components on which the model of language is based are property 4.3.1 and the notion of learnability. Provided we can define a graph homomorphism E : Syn —• X which préserves diagrams and cônes we know both that property 4.3.1 holds and that the notion of learnability is still applicable. Extension of the model of language to use either forms or -CJrames» is as a resuit not likely to présent too many problems. Finally, sketches themselves should not be dismissed. We hâve been able to construct a model of language which exceeds the power of Rus9 algebraic model of language, which is itself a powerful language spécification tool with an impressive compiler technology of its own. This technology is now available for study in a categorical universe. There are likely to be many useful discoveries still to be made. This dissertation has only scratched the surface. 103 Bibliography [Back78] Backus J.; Can programming be liberated from the von Neuman Style? A functional style and its algebra of progmms, Communications of the A.CM., Vol 20, No 8, 1978, pp 613-641. [Barr86] Barr M.; Models of sketches, Cahiers de Topologie Géomértie Différentielle Catégorique 27, 1986, pp 93-107. [BaWe85] Barr M., Wells C; Toposes, triples and théories, Springer-Verlag, 1985. [BaWe90] Barr M., Wells C; Category theory for Computing science, Prentice Hall International Séries in Computer Science, Ed C. A. R. Hoare, 1990. [BaEh68] Bastiani A., Ehresmann C ; Catégories of sketched structures, Cahiers de Topologie Géomértie Différentielle 10, pp 104-213, 1968. [BH0S76] Beckman L., Haraldson A., Oskarsson, O., Sandewall E.; A partial evaluator, and its use as a programming tool, Artificial Intelligence, Vol 7, No 4, pp 319357, 1976. [BJEJ88] Bjorner D., Ershov A.P., Jones N.D. (Eds); Partial évaluation and mixed computation, Proceedings IFEP TC2 Workshop, Gammel Avernaes, Denmark, October 1987, North-Holland, 1988. [Boch78] Bochmann G. V.; Compiler writing System for attribute grammars, Computing Journal Vol 21, No 2, pp 144-148, 1978. [Bond88] Bondorf A.; Pattern matching in a self-applicable partial evaluator, Unpublished draft, DIKU, University of Copenhagen, 1988. 104 [Bond90a] Bondorf A.; Automatic autoprojection of higher order recursive équations, ES0P '90, Copenhagen, Denmark, LNCS 432, pp 70-87, Jones (Ed), SpringerVerlag. [Bond90b] Bondorf A.; Compiling laziness by partial évaluation, Functional Programming: Proceedings of the 1990 Glasgow Workshop, pp 11-21. 13-15th August 1990, Ullapool, Scotland, Peyton Jones S.L., Hutton G., Holst C.K. (Eds.), Springer Workshops in Computing, Springer-Verlag. [BoDa80] Borceaux F., Day B.; Universal algebra in closed catégories, Journal of pure and applied algebra 16, 1980, pp 133-147. [Boul80] Boullier P.; Génération automatique d'analysers syntaxiques avec rattrapage d'errors, Journées Francophone sur la Production Assistée de Logiciel, Geneva, 1980. [Burr70] Burroni A.; Esquisse des catégories à limites et des quasi-topologies, Esquisse Math. 5, 1970. [BuLa69] Burstall R. M., Landin P. J.; Programs and their proofs: an algebraic approach, Machine Intelligence 4, 1969. [C0II86] Collier P. D.; Simple compiler correetness - a tutorial on the algebraic approach, The Australian Computer Journal, Vol 18, No 3, ppl2S-135, 1986. [Cons90] Consel C ; Binding time analysis for higher order untyped functional languages, ACM Conférence on Lisp and Functional Languages, Nice, France, pp 264-272, June 1990. [Copp80] Coppey L.; Quelques problèmes typiques concernant les graphes multiplicatifs, Diagrammes, Vol 3, pp C1-C46. [CoLa84] Coppey C , Lair C ; Leçons de théorie des esquisses (I), Diagrammes, Vol 12, 1984. [CoLa85] Coppey C , Lair C ; Algébricité, monadicité, esquissabilité et non algébricité, Diagrammes 13, 1985. 105 [Desc82] Deschamp Ph.; PERLUETTE: a compiler producing system using abstract data types, Proceedings of International Symposium on Programming, Turin, April 1982. [DuRa91] Duval D., Raynaud J-C; Sketches and computation, Rapport De Recherche RR 871-MMAG-123 LIFIA, LIFIA-IMAG, Institut National Polytechnique de Grenoble, 1991. [Ehre67] Ehresmann C; Sur les structures algébriques, CRAS, tome 264, pp 840-843, 1967. [Ehre68] Ehresmann C. Esquisses et types de structures algébriques, Bull. Instit. Polit. XIV, pp 1-14, 1968. [Ersh77] Ershov A.P.; On the partial computation principle, Information processing letters, Vol 6, No 2, 1977, pp 38-41. [Ersh82] Ershov A.P.; Mixed computation: potential applications and problems for study, Theoretical computer science, Vol 18, No 1, 1982, pp 41-67. [Folt69] Foltz F.; Sur la catégorie des fondeurs dominés, Cahiers de Topologie Géomértie Diff-érentielle 9, 2, 1969 [Futa71] Futamura Y.; Partial évaluation of computation process - an approach to a compiler-compiler, Systems, Computers, Controls, Vol 2, No 5, 1971, pp 45-50. [Futa82] Futamura Y,; Partial computation of programs, Proc: RIMS Symposia on software science and engineering, Kyoto 1982, LNCS 147, pp 1-34, Springer-Verlag. [Ganz79] Ganzinger H.; Some principles for the development of compiler descriptions from denotational language définitions, Techuical University of Munich, Technical Report, 1979. [Gold84] Goldblatt R.; Topoi, the categorical analysis oflogic, Revised édition, Studies in logic and the foundations of mat hématies, Vol 98, Eds: J. Barwise, D. Kaplan, H.J. Keisler, P. Suppes, A.S. Troelstra, 1984, North-Holland. [Goma89] Gomard C.K.; Higher order partial évaluation - HOPE for the lambda calculus, Masters Thesis, DIKU, Department of Computer Science, University of Copenhagen, 1989. 106 [Gray87] Gray J.W.; Categorical aspects of data type constructors, Theoretical computer science, Vol 50, No 2, 1987, pp 103-135. [Gray?] Gray J.W.; Exécutable spécifications for data-type constructors, in préparation. [GuLa80] Guitart R., Lair C ; Calcul syntaxique des modèles et calcul des formules internes, Diagrammes 4, (1980). [HaRu76] Hatcher W. S., Rus T.; Context-free algebras, Journal of Cybernetics 6:2-3, 1976, pp 65-77. [Higg63] Higgins P. J.; Algebra with a scheme of opérations, Mathematische Nachrichten 27,1963/64, pp 115-132. [HoHu90] Holst C.K., Hughes J.; Towards a binding-time analysis improvement for free, Functional Programming: Proceedings of the 1990 Glasgow Workshop, pp 1121, 13-15th August 1990, Ullapool, Scotland, Peyton Jones S.L., Hutton G., Holst C.K. (Eds,), Springer Workshops in Computing, Springer-Verlag. [John78] Johnson S.C.; Yacc: Yet another compiler compiler, in the UNIX programmeras manual, Vol 2B, 1978. [Jone88] Jones N.D.; Automatic program specialization: A re-examination from basic principles, In [BJEJ88], pp 225-282, 1988. [JoSc80] Jones N.D., Schmidt D.A.; Compiler génération from denotational semantics, Semantics Directed Compiler Génération, Proceedings of a workshop Aarhus, January 1980, LNCS 94, pp 70-93, Springer-Verlag. [JoSS85] Jones N.D., Sestoft P., Sondergaard H.; An experiment in partial évaluation: the génération of a compiler generator, Rewriting techniques and applications, J.P. Jouannaud (Ed), 1985, LNCS 202, pp 124-140, Springer-Verlag. [JoSS87] Jones N.D., Sestoft P., Sondergaard H.; Mix: A self-applicable partial evaluator for experiments in compiler génération, Mathematical foundations of programming language semantics, Proceedings: 3rd workshop, Tulane University, New Orléans, Louisiana, 1987, LNCS 298, pp 386-413, Springer-Verlag. 107 [JoSS89] Jones N.D., Sestoft P., Sondergaard H.; Mix: A self-applicable partial evaluator for experiments in compiler génération, Lisp and Symbolic Computation, Vol 2, No 1, 1989. [Jorg90] Jorgensen J.; Generating a pattern matching compiler by partial évaluation, Functional Programming: Proceedings of the 1990 Glasgow Workshop, pp 1121, 13-15th August 1990, Ullapool, Scotland, Peyton Jones S.L., Hutton G., Holst C.K. (Eds.), Springer Workshops in Computing, Springer-Verlag. [KoQu92] Kortas S., Quatrain R.; Modélisation de la syntaxe et la sémantique d'un language informatique par les esquisses, Rapport du Séminaire d'Initiation a la Recherche (1991/1992), Ecols Centrale de Paris, Laboratoire de Mathématiques Appliquées, Muîtigraphie, Paris 1992. [Lair75] Lair C ; Etude générale de la Catégorie des esquisses, Esquisses Mathématiques 23, pp 1-62, 1975. [Lair87] Lair C ; Categorrie qualifiables et catégories esquissables, Diagrammes 17,1987. [Lair87b] Lair C ; Trames et sémantiques catégoriques des systèmes trames, Diagrammes 18, 1987. [Laun88] Launchbury J.; Projections for spécialisation, University of Glasgow Department of Computing Science, Technical Report 88/R8, 1988. [Laun89] Launchbury J.; Dépendent sums express séparation of binding times, Functional Programming: Proceedings of the 1989 Glasgow Workshop, pp 238-253, 2123 August 1989, Fraserburgh, Scotland, Davis K, Hughes J (Eds), Springer Workshops in Computing, Springer-Verlag. [Laun90] Launchbury J.; Projection factorisations in partial évaluation, Ph.D. Thesis, Department of Computing Science, University of Glasgow, CSC 90/R2, 1990. [Lorh82] Lorho B.; The system DELTA and its derivatives, Tools and Notions for Program Construction, D. Neel (Ed), Cambridge University Press, pp 306-317, 1982. [Macl71] Mac Lane S.; Catégories for the working mathematician, 1971, Springer-Verlag. 108 [MaBe85] Mazaher S., Berry D.M.; Deriving a compiler from an operational semantics written in V.D.L., Computer Languages, Vol 10, No 2, pp 147-164, 1985. [Morr73] Morris F.L; Advice on structuring compilers andproving them correct, Proceedings ACM Symposium on Principles of Programming Languages, Boston, 1973, pp 144-152. [Moss76] Mosses P.D.; Compiler génération using denotational semantics, Mathematical foundations of Computer Science, 1976, LNCS 45, pp 463-441, Springer-Verlag. [Moss79] Mosses P.D.; A constructive approach to compiler correetness, DAIMI IR-16, University of Aarhus, 1979. [RaTu79] Raskovsky M., Turner R.; Compiler génération and denotational semantics, Fundamentals of Computation Theory, 1979. [Reev87] Reeves A.C.; An algebraic directed compiler generator using denotational semantics, University of Stirling Department of Computing Science, Honours Project, May 1987. [ReRa89] Reeves A.C., Rattray C; Sketching a constructive définition of 'mix\ Functional Programming: Proceedings of the 1989 Glasgow Workshop, pp 118-132, 21-23 August 1989, Fraserburgh, Scotland, Davis K, Hughes J (Eds), Springer Workshops in Computing, Springer-Verlag. [Roye86] Royer V.; Transformations of denotational semantics in semantics directed compiler génération, Proceedings of the SIGPLAN '86 Symposium on Compiler Construction, Palo Alto, USA, In: SIGPLAN Notices (USA), Vol 12, No 7, pp 68-73,1986. [Rus76] Rus T.; Context-free algebra: a mathematical device for compiler spécification, Mathematical foundations of Computer Science, 1976, LNCS 45, pp 488-494, Springer-Verlag. [Rus83] Rus T.; T.I.C.S. System: a compiler generator, University of Iowa Department of Computer Science technical report 83-08,1983. [RuHe84] Rus T., Herr F.B.; An algebraic directed compiler generator, University of Iowa Department of Computer Science, Technical Report 84-02, 1984. 109 [Rus85] Rus T.; An inductive approach for program évaluation, University of Iowa Department of Computer Science, Technical Report 85-02, 1985. [Rus86] Rus T.; An alternative to CF. grammar for language spécification, Proceedings of IEEE conférence on computer languages, Oct 27-30, 1986, Miami beach, Florida. [Rus87] Rus T.; An algebraic model for programming languages, Computer Languages, Vol 12, No 3/4, ppl73-195, 1987. [Rus90] Rus T.; Algebraic construction of a compiler, University of Iowa Department of Computing Science, Technical Report 90-01,1990. [Rus92] Rus T.; Algebraic construction of compilers, The Unified Computation Laboratory, Rattray C.M.I. Clark R.G. (Eds), The Institute of Mathematics and its Applications, Oxford University Press, 1992. [RyBu88] Rydeheard D.E., Burstall R.M.; Computational category theory, Prentice Hall international séries in computer science, Ed: C.A.R. Hoare, 1988. [ScSt71] Scott D.S., Strachey C ; Toward a mathematical semantics for computer languages, Oxford University Computing Laboratory, Programming Research Group, Technical Monograph PRG-6, 1971. [Sest85] Sestoft P.; The structure of a self-applicable partial evaluator, Programs as data objects, Proceedings of a workshop, Denmark, 1985, LNCS 217, pp 236-256, Springer-Verlag. [Stoy77] Stoy J.E.; Denotational semantics, MIT press, Cambridge, Mass., 1977. [Schm85] Schmidt D.A.; An implementation from a direct semantics définition, Programs as data objects, Proceedings of a workshop, Denmark, 1985, LNCS 217, pp 222235, Springer-Verlag. [Schm86] Schmidt D.A.; Denotational semantics - A methodology for language development, Allyn and Bacon, 1986. [ThWW80] Thatcher J.W., Wagner E.G., Wright J.B.; More advice on structuring compilers and proving them correct, Semantics Directed Compiler Génération, Pro110 ceedings of a workshop Aarhus, January 1980, LNCS 94, pp 165-188, SpringerVerlag. [Turc80] Turchin V.F.; Semantic définitions in REFAL and automatic production of compilers, Semantics Directed Compiler Génération, Proceedings of a workshop Aarhus, January 1980, LNCS 94, pp 441-474, Springer-Verlag. [TuNT82] Turchin V.F., Nirenberg R.M., Turchin D.V.; Experiments with a supercompiler, ACM Symposium on Lisp and Functional Programming, Pittsburgh Pennsylvania, pp 47-55, 1982. [Turc85] Turchin V.F.; Program transformation by supercompilation. Programs as data objects, Proceedings of a workshop, Denmark, 1985, LNCS 217, pp 257-281, Springer-Verlag. [Turc86] Turchin V.F.; The concept of a supercompiler, ACM-TOPLAS, Vol 8, No 3, 1986, pp 292-325. [Vick86] Vickers T.N.; Quokka: A translator generator using denotational semantics, The Australian Computer Journal, Vol 18, No 1, pp 9-17, 1986. [Wadl89] Wadler P.; Theorems for free!, Proceedings FPCA' 89, Fourth International Conférence on Functional Programming Languages and Computer Architecture, London, September 1989, pp 347-359, Addison Wesley. [Wait70] Waite W. M.; The mobile programming system: STAGE2, Communications of the A.C.M., Vol 13, No 7, pp 415-421, 1970. [Wand80] Wand M.; Différent advice on structuring compilers and proving them correct, Indiana University Department of Computer Science, Technical Report No 95, 1980. [Wand85] Wand M.; From interpréter to compiler: a representational dérivation, Programs as data objects, Proceedings of a workshop, Denmark, 1985, LNCS 217, pp 306-324, Springer-Verlag. [WeBa87] Wells C , Barr M.; The formai description of data types using sketches, Mathematical foundations of programming language semantics, Proceedings: 3rd 111 workshop, Tulane University, New Orléans, Louisiana, 1987, LNCS 298, pp 386-413, Springer-Verlag. [Well90] Wells C; A généralisation of the concept of sketch. Theoretical Computer Science, Vol 20, No 1, 1990, pp 159-178. [Yuso91] Yusop N.I.; Generating exécutable sketches in prolog, MSc IT dissertation, Department of Computing Science, University of Stirling, 1991. 112 Appendix A Example: A Toy Self-interpreter Toy is a typeless first order functional language. Functions can only be declared at the top level and hâve one implicit argument, named arg within the body of the function. Function names are therefore the only type of identifier which can exist in a Toy program. The only data objects which can be processed by a Toy program are natural numbers and binary trees. Natural numbers can be tested for equality using the = operator. Binary trees may be constructed using the (_,-) constructor and dismantled using the f s t and snd operators. This restricted language is specified because it is amongst the simplest languages which are capable of expressing a self-interpreter. A.l The syntax of Toy Using conventional methods the syntax of the Toy programming language is described by the following set of production rules: (ident) -* x (ident) -+ x(ident) (num) —• 0 (num) -• suce ((num)) 113 (decs) —> £ (decs) —• (ident) s (exp) ; (decs) (exp) -• arg (exp) —• error (exp) —• (num) (exp) —• f s t ((exp)) (exp) —> snd ((exp)) (exp) -• ((exp), (exp)) (exp) —• (exp) s (exp) (exp) —• i f (exp) then (exp) e l s e (exp) (exp) —• c a l l (iden/)(exp) (p^) —• (c^p) where (decs) The corresponding sketch Toysyn, which describes the phrases of the Toy language is shown below. 114 A.1.1 A sketch of t h e Toy s y n t a x — Toysyn Graph — G syn ident ident x exp j exp x decs if where iL i - -prg exp x exp x exp empty ident x exp x decs decs Note: projection arrows omitted for clarity. Cônes — Csy* The six cônes shown below are required in the sketch Toysynconstruct the production rules: (ident) — x (num) —• 0 (decs) -> £ 115 Thèse cônes are required to (exp) -• arg (exp) —• error (exp) -+ ((exp), (exp)) (exp) —• (exp) = (exp) (exp) —• if (exp) then (exp) e l s e (exp) (exp) —• c a l l (ident) (exp) (decs) —• (iden/) « (exp) ; (decs) (prg) —• (exp) where (decs) exp x exp exp iden* x exp x decs exp x exp x exp Pr14 exp \PrI5 pr27j / ident exp pr 2 s \pr 29 exp decs tdent x exp exp x decs ident exp Diagrams — Ds,yn Since the sketch Toysyn describes the syntax of a programming language and does not attempt to capture its static semantics the set of diagrams, Dsyn, is empty. Ds^ = 0- 116 A. 1.2 The initial model Isyn ' Toysyn —• SET /Syn(T) = {0} IsVn(num) = {jIsyn(num)n,nÇ: where Isyn(nu™)o = {0} IsVn(num)n = {succ(x): x G ISyn(ident) where = Isyn(num)n-i} \JISyn(ident)n,n G {0,1,2,...} Isyn(ident)0 = {x} Isyn(ident)n = {xy : y € /syn(*'den*)n_;L} / 5 y n (exp) where {0,1,2,...} = / 5 y n (exp) 0 = Isyn(exp)n = UJsyn(e*p)n,ne { 0 , 1 , 2 , . . . } {arg,error} U {isjium(x): x € Isyn(num)} {f s t ( x ) : x G /5yn(exp) n _i} U {snd(x): x G /syn(ezp)n-i}U { ( x , y ) : (x,y) 6 /syn(exp) n _i x Jsyn(e*p)n-i}U { « ( x , y ) : (x,y) € Isyn(exp)n-i { i f ( x , y , 2 ) : (x,y,z) * /syn(e*p)n-i}U G /s y n(exp) n -i x /syn(exp) n _i x { c a l l ( x , y ) : x € Isyn(ident),y G Jsyn^xp)*-!} Isyn(ident x exp) = Isyn(ident) ISyn(exp x exp) = Isyni^p) / 5 y n (exp x exp x exp) = /5yn(exp) x /5 yn (exp) x /s y n (exp) ISyn(decs) = U^5yn(^ecs)n,nG {0,1,2,...} where /5yn(decs)0 = /5yn(d€Cs)n = Isyn(exp)n-i}U x J 5yn (exp) x / 5 y n (exp) {empty} { b i n d ( x , y , z ) : x G Isyn(ident),y G /s y n(exp),z G Js y n(decs) n _i} Isyn(exp x decs) = Isyn(exp) x Isyn(decs) Isyn(ident x exp x decs) = Isyn(ident) Isyn(prg) = {where(x,y): (x,y) G /syn(e:rp) x J Syn (decs)} x Isyn(exp) x Isyn(decs) /syn(0 : T -+ num) = 0^0 Isyn(succ : num - • num) = x -+ succ(x) 117 ISyn(x:T - ident) = 0 = y -+ xy Isyn{x- • ident — ident) Isyn(arg : T — exp) 0 i-* arg ISyn(error 0 i-+ error : T -* exp) Isyn(is-num x —• is-iium(x) : num ->• exp) hyn{call : t'den* x exp — exp) (x,y)-> c a l l ( x . y ) ISynifst : exp -+ exp) x -• fst(x) Isyn(snd : exp — exp) x —• snd(x) /Syn(*7 : e a r P X e x P X eX P " (x,y,z) — i f ( x , y , z ) eX ÏÏ ISyn{=- exp x exp — exp) ( x , y ) - » =(x,y) /sVn((,):expx e x p - e x p ) (x,y) — (x,y) /Syn(P»"ll : exP X e x P "* eXP) /s V n(pr 12 : exp x exp — exp) hynipru (*' ») "* x = (x, y) - y : exp x exp x exp — exp) = (x, Isynipru : exp x exp x exp — exp) = (x, y, z) -<• y /5yn(pri5 : exp x exp x exp — exp) - (x, y, z) — 2 ISyn(empty y,z)-+x : T — tdent) = (x, y,z)-* J Svn (pr 2 8 : *'dcn* x exp x decs -+ exp) = (x, y, 2) -» y / 5yn (pr 2 9 : tdent x exp x decs -»• decs) = (x, y,z)-> hyn{pTA7 '> exp x decs — exp) hyniprvi : exp x decs - • decs) ISyn(Pr3 '• ident Isyn(pu x ex P ~* 118 = ident : ident x exp -* exp) = ) (x, y) — x (x, y)-* y (x,y)^x (x,y)^y x z Isyn(where : exp x decs -+ prg) A.2 The semantics of Toy A.2.1 The sketch = (x,y) —• where(x,y) ToySem Graph — Gsem The graph Gsem needed to describe the semantics of Toy is an extremely large and complex object. A pictorial représentation of this graph is not practical so the graph is represented in tabular from below. Nodes T ident num decs ident x exp x decs ident x ident num x num exp ident x decs ident x T exp x exp ident x exp exp x exp x exp exp x T T x exp num x exp ident x exp x exp exp x exp x exp x exp num x exp x exp iden* x num x exp x decs tden* x ident x exp x decs T x decs num x decs exp x decs exp x exp x decs exp x exp x exp x decs prg Edges x : T —* ident x . : iden* —• ident xo : ident -> ident idident ' ident -*• ident dispose ideni : ident —> T 119 empty : T —• decs =; : ident x exp x decs —> decs iddeca ^ ^cs —> decs pr27 : tden/ x exp x decs —• tdenJ pr28 : tden* x exp x decs —• exp pr29 : zden* x exp x decs —• decs (call o (pr27,P^28)^P^29) : ident x exp x decs — exp x decs (/e*c/i o (pr27,pr2g), apply o (pr 28 ,pr 29 ),pr 29 ) : ident x exp x decs -* exp x exp x decs (pr27, pr2g) : ident x exp x decs —• ident x exp (pr27,pr2g) : ident x exp x decs —• idenJ x decs (Pr28,P^29) : tden* x exp x decs —• exp x decs prx : ident x iden* —• zden* pr2 : ident x ident —• ident (x,x) : T —• ident X ident x. x XQ : ident x ident -* ident x tdeni xo x x . : ident x ident —• ident x tden£ x. x x . : ident x ident -> tdeni x ident disposeidentxident : ident x iden/ —• T same : ident x ident —• num 0 : T -> num suce : num —> num zéro : num -* num îdnum ^ ntim —• n u m dispose num : num —• T 120 pr$ : num x num —* num prio : num x num —» num (0,0) : T —» num x num suce x zéro : num x num —• num x num zéro x suce : num x num —> num x num suce x suce : num x num —• num x num equal : num x num —• num an/ : T —• exp unde/ : T -» exp is-num : num -» exp /st : exp —• exp snd : exp —• exp id cxp : exp -* exp dispose txv : exp —^ T (, ) : exp x exp —• exp =: exp x exp -+ exp i/ : exp x exp x exp —• exp ca/Z : ident x exp —• exp isjnum x isjnum : num x num —• exp x exp is : exp —* prg pr7 : ident x decs —• ident pr& : ident x decs —• decs pr5 : ident x T -> ident pr 6 : ident x T - ^ T id crp x empty : ident x T -+ ident x decs dispose ident xT '• ^ent x T -• T 121 pru : exp x exp -» exp p r i 2 : exp x exp —* exp /st x idcxp : exp x exp —• exp x exp snd x i d c r p : exp x exp —• exp x exp replace : exp x exp —• exp pf3 : ident x exp —• ident pr 4 : ident x exp —• exp pri3 : exp x exp x exp —» exp pri4 : exp x exp x exp —• exp pris : exp x exp x exp —• exp dispose c r p x c r p x c r p : exp x exp x exp — T ((, ) o ( p r 1 3 , p r 1 4 ) , p r i 5 ) : exp x exp x exp -> exp x exp (P r i3, (, ) ° (pri4,pr 1 5 )) : exp x exp x exp — exp x exp (= o(pr 13,pr 1 4 ),pr! 5 ) : exp x exp x exp -> exp x exp U x i d c r p x id c r p : exp x exp x exp —• exp x exp x exp (P r i3>pri4) : exp x exp x exp —• exp x exp ( p ^ i P ^ i s ) • exp x exp x exp —• exp x exp ( p r i 4 , p r i 5 ) : exp x exp x exp —• exp x exp (replace 0 ( p r i 3 , p r 1 5 ) , rep/ace 0 ( p r 1 4 , p r i 5 ) ) : exp x exp x exp -> exp x exp p r 4 i : exp x T -> exp pr42 : exp x T - ^ T Werp x unde/ : exp x T - • exp x exp disposetx?xi : exp x T - * T p r 3 4 : T x exp -» T pr3s - T x exp - • exp dispose^xexT : T x exp - • T ary x t d c r p : T x exp —• exp x exp unde/ x i d ^ : T x exp -> exp x exp 122 p7*36 • num x exp —• num pr37 : num x exp —• exp is.num x id c r p : num x exp —* exp x exp pr 3 8 : ident x exp x exp —* ident pr39 : ident x exp x exp —> exp pr 4 0 : ident x exp x exp —• exp (caZZ o (pr 3 8,pr 3 9),pr 4 o) : ident x exp x exp - • exp x exp (Pr38?P^39) • ident x exp x exp —• ident x exp (Pr39?P^4o) '• ident x exp x exp -> ident x exp (P^38, replace o (pr 3 9 ,pr 4 0 )) : ident x exp x exp —• ident x exp prig : exp x exp x exp x exp — exp pr 2 0 : exp x exp x exp x exp -* exp pr 2 1 : exp x exp x exp x exp —> exp pr 2 2 : exp x exp x exp x exp — exp (if o (pr*i9,pr 2 o,pr 21 ),pr 22 ) : exp x exp x exp x exp —• exp x exp ((, ) o (pri9,pr 2 0 ),pr 2 1 ,pr 2 2 ) : exp x exp x exp x exp —• exp x exp (P r i9,P r 2o) • exp x exp x exp x exp —• exp x exp (Pri9,P^22) • exp x exp x exp x exp —• exp x exp (pr 2 o,pr 22 ) : exp x exp x exp x exp -> exp x exp (Pr2i9P^22) : exp x exp x exp x exp -> exp x exp (P r i9,pr20>P r 2i) : exp x exp x exp x exp - • exp x exp x exp (replace o (pr^,pr22), replace o (pr2o,pr22), replace o (pr 2 1 ,pr 2 2 )) : exp x exp x exp x exp —• exp x exp x exp pr!6 : num x exp x exp - • num pri7 : num x exp x exp —• exp pr 1 8 : num x exp x exp —• exp is.num o zéro x idexp x idcxp : num x exp x exp -> exp x exp x exp is-num o suce x id c r p x id^ : num x exp x exp -> exp x exp x exp 123 pr3o : ident x num x exp x decs —> ident pr3! : ident x num x exp x decs —• num pr32 : ident x num x exp x decs —• exp pr33 : ident x num x exp x decs —• decs idutnt x -ero x idtxv x id^CC3 : ident x num x exp x decs —> ident x num x exp x decs idutnt x succ x idex? x irf^,.^ : ident x num x exp x decs —• ident x num x exp x decs (P^30,P^33) : ident x num x exp x decs —• ident x decs /etcA : ident x decs —• exp get : ident x num x exp x decs —> exp pr^ : ident x ident x exp x decs -* ident pr24 : ident x ident x exp x decs -> ident pr25 : ident x ident x exp x decs -» exp pr26 : ident x ident x exp x decs —• decs (pr24>pf"25,pr26) : ident x ident x exp x decs -> ident x exp x decs (Pr23, =;o(pr24>pr25,pr26)) : wfen* x ident x exp x decs ~> ident x exp x decs (Pr23?P^24) : ident x ident x exp x decs —• ident x ident same o (pr23,pr24) : ident x ident x exp x decs —• num (Pr23>sameo (pr 23 ,pr 24 ),pr 25 ,pr 26 ) : ident x ident x exp x decs —• ident x num x exp x decs pr43 : T x decs - • T pr44 : T x decs - • decs dispose? xdecs : T x decs ™» T arg x id^ecj : T x decs —• exp x decs undef x idiCC5 : T x decs —• exp x decs pr+z : num x decs -+ num pr46 : num x decs —• decs is-num x id exp x decs (= o(pr49,pr50),P^5i) : exp x exp x exp — exp x decs (apply o (pr49,pr5i), appZy o (pr50,pr5i)) : exp x exp x decs -> exp x exp (replace o (pr49,pr5o),pr5i) : exp x exp x decs -+ exp x decs (p^49,pr5o) : exp x exp x decs -> exp x exp (pr49?P7'5i) : C Z P x exp x decs -+ exp x decs (pr50,prsi) : exp x exp x decs -> exp x decs (appZy o (pr49,pr5i), apply o (pr50,pr5i)) : exp x exp x decs -* exp x exp pr 52 : exp x exp x exp x decs —• exp pr53 : exp x exp x exp x decs —• exp pr54 : exp x exp x exp x decs —> exp pr$$ : exp x exp x exp x decs —• decs (if o (pr52,pr53,pr54),pr55) : exp x exp x decs -> exp x decs (appZy o (pr52,pr55),pr53,pr54,pr55):C *P x €XP x e x P x dec5 "* exP x e x P x exP x d e c 5 (p^52,P^539P^54) : exp x exp x exp x decs -+ exp x exp x exp (p^52iPr55) : exP X exp x exp x decs —• exp x decs (appZy o (pr52,pr55),pr53,P^54,P^55) : exp x exp x exp x decs -> exp x exp x exp x decs where : exp x decs —• pn/ is"1 : pnj —• exp Cônes — Csem The twenty two cônes required in the définition of the semantics of Toy are shown below. 125 ident x ident ident ident ident x T ident ident ident x decs num x num decs ident num num exp x exp x exp exp x exp P r i4 exp exp exp x exp x exp x exp num x exp x exp pri7 \pri8 exp num ident x exp x decs ident x ident x exp x decs /^27, ident \pri5 ident exp ident decs 126 P^28 exp \P^29 decs T x exp ident x num x exp x decs ident exp num decs exp ident x exp x exp num x exp P^39 ident exp num \P^40 exp exp exp x T decs exp num x decs decs decs num exp x exp x exp x decs exp x exp x decs P^50 \pr51 PÏ-53 exp exp decs exp exp exp decs Diagrams — Dsem The 10 diagrams below are used to describe the opération same : ident x ident —• num. This opération is used to specify equality of identifiers. 127 fydident ident ident ident dispose ideni pr2 pr <* ident {dent —^ Xo ident • pr-i pr\ -ident x ident — pr2 ident x ident ident • pri vri ident —-- pr2 ident » ident x. x x 0 X. - ident Xo x X- XQ ident ident* ident x ident £o -ident x ident—zzr—'ident pr2 pr2 ident x ident * ident x . x x. ident - pr\ -ident x ident- ident x x x (x x) —— - ident x ident ident x ident T num x. x x dispOSeidentxiient * ident x ident same -*• num- suce • • n u m X-X X- ident x ident ident x ident aident x ident same num — num- SUCC •+-num Since the sets IScm(ident) - dispose ident X ident same ident x ident pr2 and /sem(num) are, to ail intents and purposes the same we require a similar set of 10 diagrams to describe the equality opération on numbers, equal : num x num —• num. 128 num num «• num x num P^9 dispose T num- num zéro num x num pr 9 num x num pno 9 zéro -num x num- pr\o -num prg num x num Prio -num SUCC X SUCC suce num*- prg SUCC -num x num- pr\o — num zéro x suce -num x num num x num equal dispose num x num num x num equal — num- SUCC — num num suce x zéro » num x num dispose num x num succ -num suce x zéro num — pr num x num •num num*- P^9 -num x num- pr\o — num suce num* Prio zéro x suce zéro num num- P^9 -num pr\o num x num suce x suce •* num x num \equal num — num- SUCC— num The next collection of diagrams describe the opération =: exp x exp —• exp. This is the Toy language equality operator. Notice that 0 is the True value and that 1 is the False value. 129 equal num x num ts.num x » num isjnum xs.num exp x exp • — exp pr 9 prio num- num x num is num » num ts.num x ts.num ts.num I eip " P x exP " p n T ^ e x p ' prn (pri3,pri4) exp x exp » exp x exp x exp (.) v.Pr15 <(,)°(P r 13,Pn4>,Pn5> exp •*- «?*«*> pr 11 exp x exp x exp exp •*- P^n (pru,pri5) {pris,(,)° PT13y -exp x exp pru (,) — exp pri2 exp x exp x exp P^12 •• exp exp -• P^12 pni (pri3,(,)°(pri4,pri5)) exp x exp x exp *exp x exp ((,)0(pn3,pn4),pn5) exp x exp x exp —exp x exp dispose exp xexpx exp dispose exp X exp X exp undef exp * exp x exp (pru,pris)) exp x exp x exp JWll ' — exp undef 130 — exp idexj> x undef exp x T undef x idtXp *• exp x exp T x exp exp x exp dispose^ xexp di*PO**expxT exp undef exp undef pr42 ,exp x T -T PUï exp^ idexp x undef undef prn *exp x exp . T x exp- — exp PH2 przA pr*K exp^ pr\jT undef x id exp *exp x exp undef — -exp In total 6 diagrams describe the behaviour of the Toy opérations fst : exp —• exp and snd : exp —* exp. Note that both fst and snd behave as identity when applied to a number. undef ts-num num undef •* exp num ts-num is.num 131 ts-num *• exp snd (O exp x exp (0 »• exp exp x exp *• exp We require 9 diagrams to specify the behaviour of if. thèse diagrams are shown below. Note that the True value is 0 and the false value is any non zéro value including a pair constructed U x idtXp x idcrj, •exp x exp x exp exp x exp x exp dispose expxexpxexp if undef •exp is.num o zéro x idexj) x idcr7, exp x exp x exp exp x exp x exp exp x exp x exp is.num o suce x idCXJ> x i d ^ — exp x exp x exp exp x exp x exp x exp (d ) ° (pri9,pr2o),pr2i,pr22) *• exp x exp x exp if pr22 exp 132 exp— pri3 -exp x exp x e x p ^ \ P r i 5 I dispose^ U x id c x p x idexp I T unde/l exp—— exp pri3 prie P^13 ex P exp pri4 ' - num x exp x exp v ^ P r i 8 is.num o suce x idea7> x id e x p is.num^ exp-— prj^ exp x exp x exp i>*" pr 1 5 succj num pr^ — num x exp x exp ^ v v P r i 8 I is.num o zéro x ideXD x idexv P P i num is.num^ exp— exp Pr14 exp x exp x expC^ prie num* zeroj pr^ pr i7^ exp pri4 exp -exp x exp x exp £ ^ pr^ exp x exp x exp x exp exp** exp x exp- pr n (prX9,pr20) exp x exp pri2 exp x exp x exp x exp\^>P r 22 I ( ( 0 ° (P^19,P^20),P^21,P^22) I exp— P^13 — exp Pr21 ^ exp Pr14y exp exp x exp x exp £ ^ pri 5 Below are the diagrams necessary to describe the opération apply : exp x decs —• exp and its auxiliary functions. The purpose of this opération is to specify function application. Its opération is as follows. 1. When a function call exists as a sub-expression it is replaced by the function body bound to the function in the decs part of its argument. This is the purpose of the fetch opération described below. 133 2. Ail occurrences of the sub-expression arg within the body of the function found at 1 above are replaced by the function argument from the call of the function in 1 above. 3. Together steps 1 and 2 produce an expression whose évaluation is described by the remaining diagrams of the sketch. arg xiddecs T x decs •* exp x decs dispose *£ x de apply — exp arg undef xiddecs T x decs »• exp x decs dispose f x de apply -exp undef num x decs is.num xiddecs —— exp x decs apply prAS num- — exp ts.num exp x decs snd xiddecs apply exp x decs M xiddecs apply apply exp- fst *• exp x decs apply *> exp- exp x exp x decs snd exp (= o (jW49,pr5o),pr5i) (apply °(pr 49, pr si), apply o(pr 50 ,pr 5 i)) •* exp x decs apply exp exp x exp 134 exp x decs exp ((i)0(Pr49,pr5o),pr5i) exp x exp x decs exp x decs (app/yo(pr49,pr51}, apply o(pr50,pr51)> apply exp exp x exp (,) exp x exp x exp x decs (apply o (pr52,pr55),pr53,pr54,pr55) {if ° (pr52,pr53,pr54),prss) >- exp x decs apply (if ° (pr52,pr53,pr54),pr55) exp x exp x exp ident x exp x decs (fetcho(pr27,pr29), apply 0 (pr28,pr29), 1 . exp x decs (callo(pr27,pr28),pr29) appZy + exp *• exp x decs pr2d) exp x exp x decs apply (replace o (pr49,pr5o),pr5i) exp x decs pr43 decs PT45 num - pr4i snd 47 fst exp x decs 'PU* , PU7 exp x decs 'pr4% . fst X idde (= o (pr49,pr5o),P^5i) 135 PU7 \pr4S decs exp x decs 'PUs (PU9, pr so) exp x expexp x exp x exp — r v P 44 decs exp x decs exp — PU7 decs exp x decs 'PU8 exp — pr T x decs undef x idde exp - decs exp x decs \nr4s snd x idde Pr43 Pr47 num x decs « JUe pr47 exp exp- , is.num x idde exp- undef exp x decs 'PUs exp — pr47 ts.num T « T x decs r44 arg x idde arg — exp apply decs^pr decs exp x decs 'pr48 (pr 4 9 ,pr 5 o) exp x expexp x exp x (,) {{,)° decs^pr51 decs (pr49,prso),prsi) exp- exp x decs 'pr48 pr47 exp x exp x decs exp** pr exp x exp pr ii pr 12 exp s- exp x exp x exp x decs prsî\ exp (pr 52 ,pr53,pr 5 4) pru exp x exp x exp prïT- (pr52 * pr53, pr54) exp x exp x exp exp x exp x exp x decs \pr55 decs (*/ 0 (pr52,P^53,P^54),P^55) if exp — exp x decs PU7 'pr48 exp x exp x exp x decs l \ r (pr52,P 55) i exp — Pf47 exp x decs • (prs2,prss) exp x exp** apply exp - decs , exp x exp x exp x decs (aPPly°(Pr^Pr™)> prs3, prs4, prss) — pr 4 s \xp \xp /rpr53 yfprbA exp x exp x exp x decs 136 \ecs yrpr55 ident x exp x decs ident x exp x decs -decs exp — exp x decs pr47 pr48 ident x exp x decs (Pr2B- Pr29) I ident x exp (pr 27, pr 28) tdent x exp- (call o call exp — exp — PU7 PU — exp ident x exp x decsKpr29 decs (pr27.pr2$),pr29) exp x decs ' P pr47 48 exp x exp x decs exp x exp x decs (pr 49, pr si) (pr so, pr si) i i -exp x decs- exp x decs PUs (Pr49, Pr'51 ) exp x decs « , (P^50,P^5l) exp x exp x decs » exp x decs {apply o (pr49,pr51).apply o {prS0,prSi)) apply exp — exp x exp pr n ^^ (pr27,pr29) 1 pr 29 > PU9 , {prM,prM) - exp x decs apply /m exp x exp x decs 137 "exp prii ident x decs tdent x exp x decs (fetch o (pr27, p»^) - \ V \ P r 2 9 apply o (pr2s, pr-n), decs fetch exp — apply prso exp PUs exp x exp x decs exp** pr n pr 12 (PU9, prso) exp x exp exp x exp x decsKpr51 decs (replace o (pr49,pr5o),pr5i) replace exp — exp x decs 'P?48 pr47 Thèse diagrams describe the behaviour of fetch : ident x decs - • exp whose purpose is described above. iàent _ ^ L _ id€nt id^cnt x PT T « T *rfiien< x empty ident- ident x decs • P^7 ident x T empty decs prs idident x empty - tdent x decs fetch dispose ident xT\ ! t T exp undef (P^23,=;°(P^24,P^25,P^26)) ident x ident x exp x decs (pr23,same o -tdent x decs fetch (pr23,pr24),pr2s,pr26) ident x num x exp x decs get , ident x tdent x exp x decs P^25\ ident^ {pr24,pr 25, pr 2e) pr™ pr2 ident x exp x decs 138 —exp P 23^^ ident (P r 24,pr25,pr 2 6) — . , , . , , , tdent x tdent x exp x decs T ., A . * ident x exp x decs (pr23, =; o(pr 2 4 ,pr 2 5 ,pr 2 6 )) ^ r 7 ^ " ^ ident x decs -+decs prs ident x ident x exp x decs (Pr23,pr24) tdent x tdent x exp x decs same o - tdent x tdent (pr2$,pr24) same num ident x ident x exp x exp P^26 same o (pr2$, pr24) exp (pr23^ same o ( p r 2 3 , pr2i), pr25, pr26)\ num exp pr32 ident x num x exp x exp pr3i num- ident zéro num+. ident x num x exp x decs idident X zéro x idexp X iddecs ident x num x exp x decs PT31 pr32 ident x num x exp x decs idident X zéro x idtxv x idde — exp get ident x num x exp x decs 139 pr3i • ident x num x exp x decs num — pr30/ ident SUCC idident x suce x idexv x iddecs ident x num x exp x decs num + pr3i ident x num x exp x decs (pr30,pr33) -ident ident x num x exp x decs idident x X SUCC X idtrp x decs fetch idde t ident x num x exp x decs -exp get This collection of diagrams are used to describe the replace : exp x exp - pr34 / r / P 12 exp x exp exp — pru o r3 6 mP num num pr^A exp — prn x exp s^r37 T x exp \ p r 3 5 exp undef x idtrp undef exp arg x ideXp arg T — T x exp v p f 3 5 exp opération. exp pr a 'pri2 exp x exp exp x exp \ ^ r i 2 \ xsjnum exp — pr n exp snd exp is-num x id{axp prn exp x exp /prn fst x id{exp exp — pr n (pri3,pri4) exp x exp snd x id{exp exp — prn fst exp x exp \pn2 exp x exp r pri2 exp x exp exp x exp x exp exp 140 ^n prn ex P x \prl5 exp ( = o(pr 1 3 ,pr 1 4 ),pr 1 5 ) exp /pri2 exp ex P /pri2 (pri3,pru) exp x exp exp x exp x exp G) ( ( , ) 0 ( p r i 3 , p r i 4 ) , p r i 5 ) exp- p n 9 ^ exp~ exp exp x exp pr u ex P x exP x exP x ex \prï5 /prx2 P pr2o\^ (pri9,pr 2 0 ,pr 2 1 ) priT exp x exp x exp (pr 1 9 ,pr 2 0 ,pr 2 i) exp x exp x exp exp x exp x exp x exp v p r 2 2 if (*/ o (pri9,pr 2 0 ,pr 2 i),pr 2 2 ) exp- ,e*P exp x exp ^ 1 2 P^n ident x exp x exp •-exp tdent x exp** call (P^38,P^39) ., A tdent x exp x exp exp x exp pr n prn /pr 1 2 exp x exp x exp exp x exp x exp exp** r exp (caZZo (pr38,pr39),P^4o) exp — \r>r40 pr 12 - exp exp *+ pr n 141 exp x exp prn — exp (pri3.pris) exp x exp - (pri4,pris) •• exp x exp exp x exp x exp (replace o (pr^P^is), replace(prï4,pri5)) replace exp** \ exp x exp prn - ^ prn exp x exp pr n -exp exp x exp x exp x exp exp x exp x exp x exp exp replace pr 12 — exp exp ** prn pri2 exp x exp x exp x exp exp** exp x exp replace pr 12 prn (pri9,pr22) exp x exp x exp x exp ( P ^ ' P 7 * 2 2 / — * exp x exp (pr20,pr22) exp x exp replacel exp- (replace o (prx9,pr22), replace o (pr20,pr22), replace o (pr 2 i,pr 2 2 )) P7"14 _ ^ exp x exp x exp replace exp pris P^13 ident x exp x exp exp •* pr$*^ ident pri2 prn -exp (PT39,PT40) % dent x exp x exp* • exp x exp replace (pr38, replace o (pr 39 , puo)) P r 3 ^ ^ ^ ident x exp exp pr4 142 replace undef x idexp T x exp » exp x exp dispose^ xexp replace —*-exp undef is.num xidtexp exp x exp num x exp replace P^36 —+ exp num- ts.num exp x exp fst xidexp *• exp x exp replace replace ezp — exp x exp -*. exp fst snd xid.exp — exp x exp replace exp- ident x exp x exp replace snd (call o (pr38,pr39),pr4o) *• exp x exp (pr38. replace o (pr39,pr40)) ident x exp exp call 143 replace exp exp x exp x exp (= o (pr 13 ,pri 4 ),pr 15 ) (replace o (pr13,pr15), replace o (pr 14 ,pri 5 )) - exp x exp replace exp exp x exp exp x exp x exp (G)°(P r i3,pri4),pri5) (repZaceo (pr 13 ,pri 5 ), replace o (pri 4 ,pr 15 )) replace exp x exp exp x exp x exp x exp (replace o (pri9,pr22), replace o (pr20,pr22)), replace o (pr2i,pr22)) ,, exp x exp x exp * exp x exp exp (0 ( if ° (Pr19, Pr20, P^21 ), P^22) •" exp x exp replace if —*. exp Finally we describe the opération wAere : exp x decs -* pnp. This opération is used to place an expression within a context, (i.e. an environment) and thus allow the évaluation of function calls. The opérations is : exp -+ prg and is'1 : prg -> exp are used to force an isomorphism between the sets ISem(exp) and Isem(prg). ts exp-. is-1 ~prg 144 A.2.2 SET The initial model Isem ' Toyse /Sem(T) = w Isemiident) = {0,1,2,...} Isem(num) = {0,1,2,...} ISem(decs) = \JIsem(decs)n,ne where Isem(decs)0 = {empty} /sem(<*ecs)n = Iscmidecs^-! {0,1,2,...} U {*;(x,y,z): (x,y, z) Ç Isem(ident) x ISem(exp) x /sem(decs)„_i} Isem(ident x exp x decs) = ISem(tdent) x Jsem(exp) x Isem(ident x t'denf) = ISem{ident) x Isem(num x num) = Iscm(num) x /sem(nu"*) ISem(exp) = U/sem(exp) n ,ne {0,1,2,...} where ISem{decs) ISem{ident) Isem(exp)0 = {undef,arg} U { is_num(x) : x € Isem(num)} ISem(exp)n = /SemCexp^U { f s t ( x ) : x € {î/ : y € /sem(exp)n-i A ->p(u)}}U { snd(x) : x € {y : y € /sem(exp)„_i A ->p(y)}}U { (x,y) : (x,y) € /s e m(exp)„_i x Is e m(exp) n _i}U { =(x,j/), =(j/,x) : (x,y) G {z : z € /sem(exp) n _i A ->p(«)}x /Sem(exp) n _i}U { i f ( x . y . x ) : (x,y,z) e{a:a£ Js e m(exp) n _i A -ip(a)}x /5em(exp)n_i X ISem(exp)n.-i}U { calKt'.e) : (i,e) € ISem{ident) p(arg) = False p(snd(x)) = False p( undef) = True p(call(i,e)) = Fa/se p(isjium(x)) = True p(=(x,î/)) = False p((x,y)) = True p(if(x,j/,2)) = Fa/se p(fst(x)) = False 145 x /sem(exp) n _i} = hem(ident) x ISem{decs) hem{ident) X hem(T) hem ident x decs) ISem ident x T) hem1 exp x exp) = hem(exp) hem ident x exp) = hem(ident) hem exp x exp x exp) = hem(exp) X hem(exp) *Sem exp x T) = hem(exp) X *Sem T x exp) = hem(T) + Sem num x exp) = hem(num) x ISem ident x exp x exp) = hem(ident) x hem(exp) *Sem exp x exp x exp x exp) = hem(exp) X hem(exp) X hem(exp) = hem(num) X hem(exp) X hem{ident) x hem(num) x hem(exp) x hem(decs) hem(ident) x IS(im(ident) x hem{exp) x ISem(decs) hem(decs) + Sem num x exp x exp) •LSem1 ident x num x exp x hem{exp) x X hem{exp) X hem(exp) hem(T) hem(exp) hem(exp) x hem(exp) X hem(exp) hem(exp) decs) = ISem X ident x ident x exp x decs) *Sem T x decs) = hem{T) X + Sem num x decs) = hem(num) x hem(decs) hem exp x decs) = hem(exp) X hem{decs) hem exp x exp x decs) = hem{exp) X hem(exp) X *Sem exp x exp x exp x decs) = hem(exp) X hem(exp) X hem(exp) hem(decs) X hem{decs) hem(exp) *Sem prg) IScm(x : T hem{z-: x —x+ 1 ident —• ident) hem(xo ' ident - • x-+0 ident) hem(idident : ident — ident) x —* X hem(disposeideni x-*0 hem(empty hem(=; 0~O ident) : ident — T ) : T - • decs) ' ident x exp x decs -+ decs) hem(iddecs ' decs -» decs) 146 = ¢ ^ empty = (x,y,z) = x-> x - • =; ( x , y , x ) hem(pr27 • ident x exp x decs -> ident) = (x, y, z) -+ x hem(pr28 - ident x exp x decs -• exp) = (x, y,z)-+ hem(pr29 ' ident x exp x decs -* decs) = (x, y, z) -* x hem((callo (pr27,pr2S),pr29) : ident x exp x decs -+ exp x decs) = hem((fetch o (pr27,pr29), y (x, y, z) — (hem(call)(x, y), z) apply o (pr 28 .pr 29 ),pr 29 ) : ident x exp x decs - • exp x exp x decs) = (x,y, z) -> (hem(fetch)(x, y), hem(apply)(y, z), z) hem((pr27,pr28) ' ident x exp x decs — ident x exp) = (x, y, z) -• (x, y) hem((pr27,pr29) ' ident x exp x decs — ident x decs) = (x, y, z) -+ (x, z) hem{(pr28,pr29) '- «dent x exp x decs — exp x decs) = (x, y, z) -> (y, x) hem(pri : ident x ident —> ident) = (x,y) —• x hem(pr2 : «dent x ident -+ ident) = (x,j/) -• y / S c m ((x,x) : T -> ident x ident) = 0 •-> (0,0) hem(z- X zo ^ Wewt x ident — ident x ident) = (x, y) -• (x + 1,0) hem(xo x X. : ident x ident — ident x ident) = (x, y) -> (0, y + 1) hem{x- x x- : «dent x ident — ident x ident) = (x, y) -+ (x + 1, y + 1) Isem(di8po8elitnixiieni = (x, y) -+ 0 = / : ident x ident - T) hem(same : ident x ident — num) where /(0,0) = 0 / ( * + l,0) = 1 /(0,x+l) = 1 / ( x + 1,2,+ 1) = f(x,y) hem(0 : T - • num) = 0^0 hem{succ : num —> num) = x —• x + 1 hem(zero : num — num) = x —• 0 /scm(Wnum : num — num) = x -> x J 5cm (dispose nmm : num -> T) = x —0 147 Isemiprç • num x num -* num) = (x,y) -»• x J Sem (prio : num x num -» num) = (x,y) ->• y /sem«0,0) : T -• num x num) = 0-+(0,0) ISem(succ x zéro : num x num — num x num) = (x,t/) -»• (x + 1,0) ISem{zero x suce : num x num -* num x num) = (x, y) ->• (0, y + 1) •Tsem(succ x succ : num x num -> num x num) = (x, y) -* (x + 1, y + 1) Is«n(di8pose%%mXn%m : num x num - T) = (x, y) - 0 ISem(equal : num x num —• num) = / where /(0,0) = 0 / ( Ï + 1,0) = 1 / ( 0 , x + l) = 1 /(x + l , y + l ) = f(x,y) 148 hem(arg : T — exp) = 0 >- arg Jscm(unde/:T-* exp) = 0 ^ undef hem(is~num : num — exp) = x —* is_num(x) hemifst : exp -> exp) = / = / hem(idexP • exp — exp) = X — X hem(disposetxv : exp -* T) = x^0 /sem((,): expx exp — exp) = (x,y) — ( x , y ) /sem(=: exp x exp — exp) = / where where /(x) = undef, x = undef = x, x = is-num(y) = a, x = (a,6) = fst(x), otherwise hem(snd : exp -+ exp) where /(x) f(x,y) = undef, x = undef = x, x - is-num(y) = 6, x = (a, h) = snd ( x ) , ot her wise = is-num( Jscm(eçuaZ)(a, 6)), x = is-num(a) A y = is-num(6) = undef, x = (a,6) V y = (c,d) V x = undef V y = undef = otherwise =(x,y), hem(if : exp x exp x exp -+ exp) where f(x,y,z) = / = undef, x = undef = î/, x = is-num(O) = 2:, x = is-num(n + 1) V x = (a,6) x = is-num(x + 1) V x = (a,6) = if(x,y,z), otherwise hem{eall : ident x exp -> exp) = (i,x) -• c a l l ( i , x ) hem(is-num x isjnum : num x num —> exp x exp) = /5em(«5 : exp -• prg) (s, y) —• (is-num(x),isjiuiii(y)) = 149 x —x IsemipTi • ident x decs —• ident) = (I.J)-»Î Isem(pr& : ident x decs — decs) = (x. y) — y /sem(/»-5 : "fent x T -• ideni) (x,y)->x /5em(pr6 : ident x T - T) (x,y)-*î/ /sem(dt'sposeI exp x exp) = ( x , y , * ) — (/sem((,))(x,y),^) /Sem((pri3, (, ) ° ,P»-i5) : «xp x exp x exp -• exp x exp) (x,y,2r)^(/Sem(=)(x,y),z) /Sem( i/ x idtrp x id e i p : exp x exp x exp - • exp x exp x exp) = (x,y,z)-* (undef, y, z) /s e m((pri3,pri4) : exp x exp x exp — exp x exp) = (a, 6, c) -» (a, 6) /Sem((pri3,pris) : exp x exp x exp — exp x exp) = (a, 6, c) — (a, c) •Tsem((pri4,pri5) : exp x exp x exp -» exp x exp) = (a, b, c) -* (b, c) Isem({replace o (pr 13 ,pr 15 ), replace o (pr14,pr15)) : exp x exp x exp - • exp x exp) = (x,y,z) - • (7s e m(rep/ace)(x,r),/sem('«p/ace)(y,z)) Isem(pr4i : exp x T — exp) x,y) — x /5em(pr42 : exp x T - T) x,y) — y Isem(disposeetpxT x,y) — 0 : exp x T -* T) Isemiidtxp x unde/ : exp x T -» exp x exp) x,y) —* (x,undef) /Sem(pr34 : T x exp ^ T) x,y)-*x Isemiprss : T x exp -» exp) x,y)-> y »5em(disposeTxer}, : T x exp -* T) x,y)-+ Isem(arg x »'d«, : T x exp -» exp x exp) x,y)^(arg,y) Isem(undef x tde*p : T x exp - • exp x exp) x, y) - • (undef, y) 0 •Tsem(p»"36 : "«"* x exp - • num) x,y)->x i5em(pr37 : num x exp - • exp) x,y)-*y Isem{is.num x,y) - • (is_num(x),y) x t'dez7 : num x exp —• exp x exp) 151 -Tsem(pr38 : ident x exp x exp — ident) = (x, y, z) -* x hem(pr39 • ident x exp x exp — exp) = (x, y,z)^ Isem(pr4o - ident x exp x exp - • exp) = (x, y, z) — 2 /s e m((«i// o ident x exp) J5ern((pr39,pr4o) : ident x exp X exp -» ident x exp) = = y y), z) (x, y, 2) - • (x, y) (x, y, z) -* (y, z) Isemdprx, replace o (pr39,pr4o)) : ident x exp x exp -• ident x exp) = (x, y, z) — (x, Isem(replace)(y, / Sem (pri9 : exp x exp x exp x exp -» exp) = (o, b, c,d)^> a Isem(pr20 : exp x exp x exp x exp — exp) = (a, b, Isem(pr2i : exp x exp x exp x exp - • exp) = (a,b,c,d)-*c / Sem (pr 2 2 : exp x exp x exp x exp -» exp) = (a,b,c,d)^d z)) c,d)->b Isem((if ° (pn», ^20,^21),^22) : exp x exp x exp x exp — exp x exp) = M,C,d)-+(Jsem(«/)KM,d) /s e m(((,)o (pr19,pr2o),pr2i,pr22) : exp x exp x exp x exp - • exp x exp) = (a, &,C,d)-+(/Sem((, ))(<*, &),C,d) /5«n(Oww,prao) : exp x exp x exp x exp -* exp x exp) = (a, 6, c,d) -• (a, 6) /sem((pn9,pr22) : exp x exp x exp x exp -• exp x exp) = (a, 6, c, d) — (a, d) Isem{(pr20,pr22> : exp x exp x exp x exp -* exp x exp) /sem«P»-2i,pr22) : exp x exp x exp x exp — exp x exp) = (a, 6, c,d) -f (6, d) = (a, 6, c, d) -» (c, d) /sem((pri9,pr20,pr2i) : exp x exp x exp x exp - exp x exp x exp) = (a,6,c,d)-+(a,6,c) Isem({replace o (pr 19 ,pr2 2 ), rep/ace o (pr2o,pr22), replace o (pr2i,pr32)) : exp x exp x exp x exp -*• exp x exp x exp) = (a, b, c, d) - • ( Jstm(rep/«*)(«> d), /Sem(rep/ace)(6, d), /Sern(repface)(c, d)) 152 hem(pri6 : rium x exp X exp -» num) = (x, y, z) -> x hem{pri7 : num x exp x exp — exp) = (x, y,z)-> y hem{pri8 ' num x exp x exp — exp) = (x, y,z)-* z hem(is-num ° zero x ideXp x idexp : num x exp x exp —• exp x exp x exp) = (z, y, z) — (7sCm(is-num)( J 5cm (2:ero)(x)), y, z) /5 em (t*-num o suce x idtXp x *dcrp : num x exp x exp —> exp x exp x exp) = (x, y, 2) — (/5cm(^-num)(/5 cm (succ)(x)), y, 2) hem(pr3o ' ident x num x exp x decs —• ident) = (a,b,c,d) —• a hem(pr3i : ident x num x exp x decs —• num) = (a,6,c, d) —> 6 hem{prz2 • «dent x num x exp x decs —> exp) = (a, 6, c, d) -* c hem(prz3 : ident x num x exp x decs —• decs) = (a,6,c,d) —• d hem(idident x ^ro x id crp x idrfCCj : ident x num x exp x decs —• ident x num x exp x decs) = (a,6,c,d) — (a,0,c,d) hem(idident x suce x ideXp x id decs : ident x num x exp x decs —> ident x num x exp x decs) = (a, 6, c, d) -+ (a, 6 + 1, c, d) Jsem( (1^30^33) - ident x num x exp x decs —• ident x decs) hemifetch : ident x decs —• exp) where ( a , 6 , c , d ) ^ (a,d) = / /(x,empty) = undef f(x,= ; ( y , e , d ) ) = hem(get)(x, hem(same)(x, y), e, d) hem(get : ident x num x exp x decs —• exp) where = /(x,0,e,d) = / ( x , x + l,e,d) = e hem{fetch)(x,d) 153 = / /Sem(P'"23 : ident x ident x exp x decs —> ident) = (a,6,c,d) ->• a Isem{Pr24 '• ident x ident x exp x decs -+ ident) = (a,b,c,d) -* b ISem(pr25 • ident x ident x exp x decs -+ exp) = (a,6,c,d) -»• c / S e m (pr 2 6 : ident x ident x exp x decs -+ decs) = (a,6,c,d)-* d IsemiiP*,24,P',25,pr26) : «dent x ident x exp x decs -> ident x exp x decs) = (a,6,c,d)-> (6,c,d) /5em((P',23,=;0(PT'24,pr25,pr26)) : ident x ident x exp x decs -• ident x exp x decs) = (a,6,c,d)-*(a,= ;(6,c,d)) /sem«P'"23,P',24) : ident x ident x exp x decs - • ident x ident) = (a,b,c,d) - • (0,6) /sem(*<"ne ° (P r 23,P r 2 4 ) : «dent x ident x exp x decs -»• num) = Isem((pr23,same (a, 6, c,d) - • Isem{same)(a, b) o (pr 2 3,pr2 4 ),pr 25 ,pr 26 ) : ident x ident x exp x decs — ident x num x exp x decs) = (a,6,c,d)-> (a,Isem(same)(a,b),c,d) /sem(pr 43 : T x decs ^ T) = (x,y)-x Isem(pr44 • T x decs -» decs) = (x, y) - • y / S e m (dispose T x ( i e „ : T x decs - T) = (x, y) - 0 Isemiarg x idi eM : T x decs -f exp x decs) = (x, y) — (arg, y) J S e m (unde/ x W^e. : T x decs -» exp x decs) = (x, y) -» (undef, y) ISem(PUS ' num x <* C C 5 —" " « m ) = (x,y) —• X / 5 e m (pr 4 6 : num x decs -»• decs) = (x, y)-> y ISem(is-numx = (x,y) -+ (is_num(x),y) idiec, : num x decs -* exp x decs) 154 hem{pU7 : exp x decs -+ exp) = (x, y) - • x hem(pr48 ' exp x decs -> decs) = (x, y) - • y hemifst x iddecs'•num x decs -* exp x decs) = (x,y) — hem{snd x iddecs - rxum x decs -• exp x decs) = (x,y) -• (/sem(srcd)(x),y) hem(apply : exp x decs -+ exp) = / where (hem(fst)(x),y) /(arg. d) = arg /(undef, d) = undef /(is-num(x),d) = isjium(x) /(fst(x),d) = / S e m (/st)(/(x,d)) /(snd(x),d) = ISem(snd)(f(x,d)) /((x,y),d) = /sem((,))(/(x,d),/(y,d)) /(«(x,y),d) = /sem(=)(/(x,d),/(y,d)) / ( i f ( x , y,z),d) = f(ISem(if)(f(x,d),y,z).d) / ( c a l l (i,e),d) = f(ISem(replace)(ISem{fetch)(i,d),f(e,d)),d) Isem(pr49 '• exp x exp x decs —• exp) = (x. y.z) -* x Isem{prso : exp x exp x decs -+ exp) = (x. y.z)-+ y /s e m (pr 5 i : exp x exp x decs —• decs) = (x,y.z)-* z Isem{{(,)° (pr49,pr5o),pr5i) : exp x exp x exp -+ exp x decs) = (x,y.2)^(JSem((,))(x,y),z) Isem((= ° {pr 49, Prso)*pr 51) : exp x exp x exp - • exp x decs) = (x,y,z)^(/5em(=)(x,y),2) Isem((apply o (pr 4 9.pr 5 i), appty o (p^scP^si)) : exp x exp x decs -> exp x exp) = (x, y, 2) -<• (Isem(apply)(x, z), Isem(apply){y, *)) Isemdreplace o (pr49,pr5o),pr5i) : exp x exp x decs -»• exp x decs) = (x,y,z) — (Isem{replace)(x,y),z) Isem((pr49,prw) : exp x exp x decs - • exp x exp) = (x, y, z) -* (x, y) /sem((p»"495pr5i) : exp x exp x decs -* exp x decs) = (x, y, 2) -+ (x, z) Isem{{prso,prs\) : exp x exp x decs -> exp x decs) = (x, y, 2) - • (y, 2) Isem((apply o (pr 4 9,prsi), app/y © (pr5o,pr5i)) : exp x exp x decs -> exp x exp) = (x,y,z) -» 155 (Isem(apply)(x,z),ISem(apply)(y,z)) hem(prs2 : exp x exp x exp x decs -> exp) = (a. 6. c,d) — a /sCm(p^53 : exp x exp x exp x decs -• exp) = (a. 6. c,d) -> 6 hemipr54 - exp x exp x exp x decs -+ exp) = (a. 6. c, d) -+ c hem(pr55 ' exp x exp x exp x decs -• decs) = (a,6,c,d)-+ d hem{(if ° (pr52,pr53,pr54),pr55) : exp x exp x decs — exp x decs) = hem((apply o (prb2,prb5),pr53,pr54,pr55) (a,6,c,d)-(/5cT„(i/)(a,6,c),d) : exp x exp x exp x decs -» exp x exp x exp x decs) = (a, 6, c, d) - • (he-i(apply)(a, hem((pr52,pr53,pr54) : exp x exp x exp x decs — exp x exp x exp) hem((pr52,pr55) > exp x exp x exp x decs -> exp x decs) d), b, c, d) = (a,6,c,d) — (a,b,c) = (a, 6.c,d) — (a,d) hem{(apply 0 (pr52,pr55),pr53,pr54,pr55) : exp x exp x exp x decs -+ exp x exp x exp x decs) = A.3 (a,b,c,d)-+ hem(where : exp x decs -+ prg) = hemiis'1 = : prg ^ exp) {he-XaPPly){a->d),b,c,d) hem(is){htm{apph)) x —x The eva/ and Zearn transformations We begin by specifying the sketch morphism E : ToySyn -* Tby 5cn which allows us to specify the functor E* : Mod(ToySem) -> Mod{ToySyn). Using this functor we are able to define the model E*(hem) - ToySyn - • SET and the transformations eval : hyn learn : E*(hem) -» hyn- 156 A Em(hem) and À.3.1 T h e sketch m o r p h i s m E : ToySyn -> Sem E(T) = T JE'(num) = num E(ident) = ident E(exp) = exp E(ident x exp) = ident x exp E(exp x exp) — exp x exp E(exp x exp x exp) = exp x exp x exp E(decs) = decs E(exp x decs) = exp x decs E(exp x ident x decs) = ident x exp x decs E(prg) = prg E(0 : T -> num) = 0 E(succ : num —• num) = suce i:(x : T -+ ident) = x £ ( x . : ident —• ident) = x. £(an7 : T —• exp) = arg E(error : T —• exp) = unde/ E(isjnum : num —• exp) = is_num E(call : ident x exp —• exp) = ca// £(/st : exp —• exp) = /st E(snd : exp —• exp) = snd £ ( t / : exp x exp x exp —• exp) = t/ £ ( = : exp x exp -* exp) = = E((, ) : exp x exp —• exp) = (, ) £"(Prii : exp x exp -» exp) E(pri2 : exp x exp —* exp) 157 = prn = pri2 A.3.2 E(pri3 : exp x exp x exp - • exp) = prX3 E(pru : exp x exp x exp -> exp) = prl4 E(pris : exp x exp x exp — exp) = prXh E(empty : T — decs) = empty £ ( = ; : ident x exp x decs -* decs) = =; E(pr27 : ident x exp x decs —> ident) = pr27 E(pr2S : ident x exp x decs -+ ident) = pr28 E(pr29 : ident x exp x decs -* ident) = pr29 E(pr47 : exp x decs —•exp) = pr47 E(pr4S : exp x decs —•exp) = pr48 The model E(pr3 : ident x exp — ident) = pr3 E(pr4 : ident x exp — ident) = pr4 E (where. : exp x decs -+ prg) = where E*(hem) The functor Em : Mod( ToySem) — Mod(7by 5 y n ) is defined below. £*(M : Toy sem - SET) = M oE E*(f:M = f : E*(M) + E*(N) + N) From this we obtain the following définition of Em(hem) • ToySyn -> SET. 158 E'(ISem)(T) = W E'(ISem)(ident) = {0,1,2,...} E'(ISem)(num) = {0,1,2,...} E*(ISem)(decs) = UIsem(decs) n ,ne { 0 , 1 , 2 , . . . } where Isem(decs)0 = {empty} Isem(decs)n = /5em(decs)n_iU{=;(x,y,2):(x,y,2)€ ISem(ident) X Isem(exp) X /Sem(decs) n _i} E"(ISem)(ident x exp x decs) E'(ISem )(exp) where = ISem(ident) x Isem(exp) x ISem(decs) = U hem(exp)n, n € {0, 1, 2,. . .} Isem(exp)0 = {undef,arg} U { isjium(x) : x € /5 e m (num)} /Sem(exp)n = /sem(exp) n _ 1 U { f s t ( x ) : x € {y : y € Istm(exp)n-i A -'p(y)}}U { snd(x) : x £ {y : y € /semtexp),,-! A ->p(y)}}U { (x,y) : (x,y) € /5em(exp)„_i x /semtexpjn-iju { = ( x , y ) , =(y,x) : (x,y) € {2 : 2 € Isem(exp)n.i A ->p(2)}x /Sem(exp)n_1}U { i f ( x . y . x ) : (x,y,2) Ç {a : a £ Isem(exp)n-i A ->p(a)}x ISem{exp)n-i X /sem(exp) n _i}U { call(i.e) : (i,e) € Is*n(ident) P(arg) Fa/se p(snd(x)) = False p(undef) True p(call(i,e)) = False p(is_num(x)) = True p(=(x,y)) = False p((.x,y)) = True p(if(x,y,2)) = False p(fst(x)) = False x /sem(exp)n_1} E'(ISem)(exp x exp) = Isem(exp) X Isem(exp) -EVsemXident x exp) = /sem ( «dent ) x ISem ( exp) E*(ISem)(exp = ISem(exp) X Isemiexp) X Isem(exp) £*(/s e m)(expx decs) = ISem ( exp) X /Sem ( decs) EVsem)(prg) = /Sem(exp) x exp x exp) ^*(/5em)(x : T -> ident) 0f-O •E*(-fsem)(x-: ident -* ident) x -*• x + 1 159 E'(ISem)(empty : T - decs) £*(Jsem)(=;: ident x exp x decs - • decs) = 0 ~ empty = (x,y,x)-• »;(x,y,x) £"(/sem)0w"27 : ident x exp x decs -» ident) = (x, y, 2) -» x £"(/sem)(p»"28 : ident x exp x decs - • exp) = (x, E'(Isem)(pr29 • ident x exp x decs -> decs) = (x, y,z)-> E'(ISem)(0:T->num) = 0~O E*{Jsem)(succ : num -> num) = i-»i + l 160 y,z)-^y z Em(hem)(arg:T-+exp) = 0- Em(hem)(error = 0 -» undef = x —• isjium(x) = / : T -+ exp) Em(hem)(is-num : num —• exp) Em{hem)(fst : exp — exp) where = undef, x = undef = x, x = is-num(y) = a, x = (a,6) = fst(x), otherwise £*(/sCm)(s™* : exp — exp) = where /(x) /(x) undef, x = undef = x, x = is-num(y) = 6, x = (a,6) = snd(x), otherwise exp-* exp) -E*(/sem)(=: exp x exp -> exp) where /(x,y) / = E*(hem)((,)'-expx arg = (x,y)-+ (x,y) = / = is-num(/sem(eçua/)(a,6)), x = is-num(a) A y = isjium(6) = undef, x = (a,6) V y = (c,d) V x = undef V y = undef = Em{hem)(if where =(x,y), otherwise • exp x exp x exp-+exp) f(x,y,z) = / = undef, x = undef = y, x = i s Jium(O) = z, x = is-num(n + 1) V x = (a,6) x = is-num(x + 1) V x = (a,6) = if(x,y,z), Em{hem){call : ident x exp - • exp) Em(hem)(prn otherwise = (i,x) -* c a l l ( i , x ) : exp x exp - exp) = (x,y) -> x £*(/5em)(pr12 : exp x exp - exp) = (x, y) ^ y E*(hem)(pr3 ' ident x exp -• ident) = (x,y) -> x £*(/s C m)(pr 4 : W c n * x e x ? -* e x P) = (*' ?) ~> » 161 E'(Isem)(pri3 : erp x exp x exp ~» exp) = (x,y,z)-+ x E'{Isem)(pri4 : exp x exp x exp -* exp) = (x,y, 2) — y •EVsemXpris : exp x exp x exp - • exp) = (x,j/,z)-t2 £*(/semXJW47 : exp x decs -» exp) = (x, y) -* x E*(Isem)(pr4& • exp x decs -» decs) = (x, y) -* y E*(Isem)(where : exp x decs - • prg) 162 = /sem(is)(/sem(appty)) A.3.3 T h e eval natural t r a n s f o r m a t i o n evali = U evalident = evalnum eval exp = = / where / where / where /(x) = 0 /(xy) = l + /(y) /(0) = 0 /(succ(y)) = l + /(y) /(arg) = arg /(error) = undef /(is_num(n)) = is_num(eva/Bttm(n)) /(fst(x)) = ISem(fst)(f(x)) /(snd(x)) = ISem(snd)(f(x)) /((x,y)) = (/(x)./(y)) /(=(x,y)) = /sem(=)(/(x),/(y)) /(if(x,y,2)) = /Sem(t/)(/(x),/(y),/(2)) /(call(i.e)) = call(et;a/ i < i e n < (i),/(e)) eval exp X exp = eval exp X exp x exp = (x,y,2)-» (era/ exp (x),et;a/ er p(y),eva/ eX p(2)) evalidentx exp = (x, y) -* (et;fl/^eii«(x), evalexp(y)) (x,y)-*(evalexp(x),evalcxp(y)) eval idtntxtxpx decs = (x,y,z)-~ evalit / = where eval expx decs = evalprg = (evalident(x), evalexp(y), evalitcs(z)) /(empty) = empty /(s;(x,y,2)) = -;(evalident(x), evaleXT(y), eval decs(z)) {x,y)-+(evalexp(x),evalexp(y)) / where /(where(x.y)) 163 = ISem(apply)(evalexp(x),evaldecs(y)) A.3.4 T h e learn transformation learni = 1(} learnutnt = / learnnum = learntxp = where /(°) / ( 1 + y) = x = x/(y) /(0) = 0 / ( 1 + y) = succ(/(y)) / where / where /(arg) = arg /(undef) = error /(is_num(n)) = is_num(/earn„„m(n)) /(fst(x)) = fst(/(x)) /(snd(x)) = snd(/(x)) /((x.y)) = (/(x)J(y)) /(=(x.y)) = =(/(x).f(y)) /(if(x,y,2)) = if(/(x),/(y),/(2)) /(call(i.e)) = call(/earn^ e n < (i),/(e)) learnexpxexp = (x,y) ^ (learnesp(x), learntxpXexpXeXp = (x,y,z)-^ learnidentxezv = (x, y)-+(learniàerJx), learnuentxerpxdecs = learn decs where (leam^x^learn^y^learn^z)) (x,y,z)- learnap(y)) (learnueni(x),leamtxp(y),leamitc>(z)) — f /(empty) = empty /(*;(x,y,2)) = =lUearnideni(x), learntxpxdecs = (x,y)-^ learnprg = f where A.4 learnexp(y)) learntxp(y), learn*«.(*)) {learn^x^leam^y)) /(x) = where(/ecrn erp (x),empty) A Toy datatype to represent Toy programs The datatype is described as a pair of transformations: encode : /syn -•• E*(Isem) décode : E"(Isem) -* ISyn 164 such that décode o encode = l / s . encode? = 0 *-+ (0,0) encode^cnt = y -> (1 •/(»)) where /(x) = 0 /(xy) = l + /(y) encodenum where = /(0) = 0 /(succ(y)) = l + /(y) encodedees where = d—>(3,/(d)) /(empty) = (0,0) /(=;(i,e,d)) = (l,encode t ^ n , x c r p x ,f c c ,(i,e,d)) encodeexp where y-» (2,/(y)) = z — (4,/(x)) /(arg) = (0,0) /(error) = (0,1) /(is_num(n)) = (l,encode nUTn (n)) /(fst(x)) = (2,encode crp (x)) /(snd(x)) = (3,6ncode crp (x)) /((*.!/)) = (4,encode c x p x e r p (x,y)) /(=(*,y)) = (5,encode crpxCi7> (x,y)) /(if(x,y,z)) = (6,encode c r p x c r p x c x p (x,y,z)) /(call(i,e)) = (7 ,encodeidentxexp{i,e)) encodeexpxexp = (*,»)-+ (5, (encode^(x), encode crp (y))) encode exp x exp x exp encodeidentxexp = = (^»î/^)-* (6,(encade &rp (x), (encocfecxp(y), encode tXp(z)))) (*,») — (7,(encodef-,*en,(x), encode crp (y))) encode identx exp X decs = (x,y,*)-» (8,(encode,^ n t(x), (encode crp (y), encode^ cs (z)))) encode «xy xdec* = ( * , » ) - • (9,(encode e x p (x), encode decs (y))) encodeprg = (where(e,d)) -• (10,encode ^x decs (e,d)) 165 décode? = ((0,0))^-0 decodeident = ( C l . y ) ) — f(y) where /(0) = x / ( 1 + y) = x/(y) decodenum where = ((2,y))-»/(y) /(0) = 0 / ( 1 + y) = succ(/(y)) décode decs = ((3,d))-/(d) where /((0,0)) = empty /((l,x)) = =;(i,e,d) where {i,e,d) decodetXp where = décodeidentx exp x decs (x) = (4,x) - - / ( x ) /((0,0)) = arg /((0,1)) = error /((l,n)) = is-num(decode n t m (n)) /((2,x)) = f s t (décode /((3,x)) = snd(decode c r p (x)) /((4,x)) = (a,6) where /((5,x)) = = = (a, b) = décode txpxcxp{x) = décode exp x exp X exp = (a, 6) = décode tXpx exp xcxp{*) = décode ident xcxp(x) call(i,e) where décode exp x exp décode c r p x grp (x) if(a,6,c) where /((7,¾) = =(a,6) where /((6,x)) (a, 6) txv{x)) (i,e) ((5,(x,y)))-^(decode C x ï ,(a:),decodeex,>(y)) ((6,(x,y,z)))-^(decodecrp(x),decodecip(y),decodecrp(z)) deCOde identx exp = ((7,(x,y)))-^(decodelicnt(x),decodeexp(y)) decodeuemxexpxdecs = ( ( 8 , ( x , (y ,2:) ) ) ) — (decodet ¥here(e,d) where (e,d) = décode exp x decs (*) 166 décode itcs{z)) A.5 The Toy self-interpreter A.5.1 T h e interpréter function This function interpréter : Isyn —• Isyn is defined as interpréter = learn o eval. This définition expands to the one shown below. interpréter^ = 1Q interpréterident = lrSyn(ident) interpréter num = 1/Syn(„„m) interpréter txp = / where /(arg) = arg /(error) = error /(is_num(n)) = is_num(n) /(fst(e)) = Ff3t..exp-.exp(f(e)) /(snd(e)) = Fsnd:exT^exV(f(e)) /((x.y)) = (f(x)J(y)) /(*(x,y)) = F=:eïpxerp.-erp(/(x),/(y)) /(if(x,y,2)) = /(call(i.e)) = call(i,/(e)) interpréterexpxexp = (x, y)-* (interprétertxp(x), interpréter exfXtxpXexp = Fij:exJ)Xexpxexp^exp(f(x),f(y),f(z)) (x, y, 2) — (in«erpre*ereip(x), interprétertxp(y), interpréter iitnixtXf = interpréter iientxexpx decs - (x, y) -* (interpréteriient(x), interprétertxp(y)) interpréterez)) interprétertxp(y)) (x,y, 2) -» ( interpréterl(fen< (x), in«erpreïer erp (y), i n t e r p r e t e r ^ x ) ) interpréter dees = f where /(empty) = Feroj,») ~> (interpréter^(x), interpréterpry = (where(e.d)) - • Fu,Aere:erj.xprg(x;y) = error, x = error = = y z, x •=•- isjuum(0) = if(s,y,z), otherwise = x = is.num(succ(y)) V x = (a,6) ^^^Favvîy,txpxdecs^exp{x, 168 y), empty) Fapply:expxdecs-+exp(zrg,d) Fapply:expxdec3^exp(^T0T, d) FaPply:expxdecs-^exp(iS-nUto(n) = arg = error , d) = is-iium(n) = Ff3t:exp-*exp\Fapply:expxdcc3-+exp\e, d)) Fapply:expxdec3—*exp{811d\ej,d) = F3nd:exp —• exp(*app/y:expxdecs-*exp\e, a)) Fapply:expxdec3-+exp{(x = (-fapp/y:expxdec5-»exp(£* d) $ -r app/y :expX(feca—exp(î/> d)) Fapply\expxdecs-+exp\îs^'{e) ,d) » î/) , d) Fapply:expxdec3—*exp\s{x>y', ") = F=:exp x cxp->cxp{Fapply:expxdec3-+exp{x, Fapply:expxdec3->exp(îf \X 9y d), ^ apply iexp X decs—>exp[y, <*)) 9ZJ,d) = Fapply:expxdec3^exp\*if:expXcxpxcxp—*cxp\-rapply:expxdec3--+exp\x, Fapply:expxdec3-+exp ( c a l l &), V, z), &) (ife),d) = Fapply:expxdcc3-*cxp{Frep lace: exp x exp-+exp (vOdy, r apply:expx decs-• exp \e, a)), Where ftody = a) FfeUh:identxdccs-+exp(i,d) •Treplace:expx exp-+exp\ttg,T) = T irrCp/acC:CrPxCrp-Crp(error,r) = error Frcpiace:cxpxexp-+cxp(isjriymU) ,r) = is-aum(n) Freplacc:expxcxp-+exp\î S t ( e ) , r) — T fst: exp—* exp \f replace : exp X exp—* exp \e, •*replace :expx exp-• exp(SD.d(e) , r) = r snd: exp x exp —*> cxp\*replace -.exp x exp —»• exp V e , f replace : exp X exp-* exp \~\x = iV' Frcplacc'.cxpxexp-+cxp\tt\x T ), -^ rep la ce : exp x exp-* exp (V, r)) *y),r) = Where ,r) F=:expxcxp-+cxp\Freplace:expXcxp—>cxp\x, * rep la ce: exp x exp—*exp\ *x r)) \Freplacc:expxexp->cxp\x, »y »Z',T) = Fi}=ltxpxcxp X; = Frtplace:expXexp^exp{x,r) V = r rep lace : exp X exp-* exp \V, T) Z = + replace : exp X exp—> exp Freplace\expXexp—*cxp\t^-±{l*ej,r) = T J ** rep lace: exp x exp-* exp \V, r)J x exp-*exp\x , V , z ) \z,r) C a l l Q t » J4 replace: exp x exp—* exp (e, 169 r)) r )) Fjetchudent x decs-*exp ( x , e m p t y ) Fjetch:idcntxdecs-+ exp(x,= l = = error (y,e,d)) * gct:\dcntx num x exp X decs—* exp \x, * sameiident x idcnt-+num\x, * getiidcntxnum x exp x decs—>cxp\x,Q, e, d) = * geUidentx num x exp X decs-* exp \x,SUCC ( n ) , €, d) A.5.2 e = Ffetch:identx decs-* exp (x, d) F3amc:idcntxident-+num\Q,Q) = 0 FSamc:idcntxidcnt-+num(sUCc(x),0) = SUCC(O) F3ame:ident X ident-^num (0,SUCC ( x ) ) = SUCC ( 0 ) FSame:ident X ident-* nttm(sUCc(x), SUCC ( y ) ) = T h e rep-interpréter y), e, d) Fsame:identxident-*num(x,y) function We now define the function repJnt : Em(Isem) -* £*(/sem)- This function is defined using the functions: interpréter, décode, and encode as rep.Ànt = encode o interpréter o décode. This définition expands to the one shown below. 170 rep.int^ - (0,0) *-• (0,0) rep.intidtnt = (1.x) - * ( l , x ) rep.intnum = (2,x) ->(2,x) rep.intexp = (4,x) — / ( x ) where /((0,0)) = (0,0) /((0,1)) = (0,1) /((l,n)) = (l.n) /((2,x)) = rep_F/,<:erp_„J)(rep-in^zp(x)) /((3.x)) = rep-F,nd:exp-.exp(rep.intexp(x)) /((4,(5,(x,y)))) = (4,(5,(rep_in* exj ,(x),rep_ini erj) (y)))) /((5.(5,(¾. y)))) = rep.F = : e „, x e r j > _ e x p (x,y) / ( ( 6 , ( 6 , ( 1 , (y, 2))))) = rep-F,/:expXerj)Xeip_eirp(x,y,2) / ( ( 7 , (7. ( i . e ) ) ) ) = (7,(7,(i,rep.in* e r p (e)))) rep-int^x^ rep.int txpXexpx = txp ( ( 5 , ( x , y ) ) ) -+ (5,(rep.in( e i p (x), rep.intexp(y))) = ( ( 6 , ( x , ( y , 2 ) ) ) ) - > (6,(rep_in« eip (x),(rep.int exp (y),rep-inf erp (2)))) reP-*^.,fendtntxeipxdccs-+decs = (0,0) ~ (3.(0,0)) (i,e,d) - • ( 3 , ( 1 , ( 8 , ( i , ( e . r f ) ) ) ) ) 171 rep_Ff,Ucxp^exp(x) rep-F^^^x) = (4,(0,1)), x = (4,(0,1)) = x, x=(4,(l,y)) = o, x = (4,(4,(5,(0,6)))) = (4,(2,x)), otherwise = (4,(0,1)), x = (4,(0,1)) = x, x=(4,(l,y)) = 6, * = (4,(4,(5.(0,6)))) = (4,(3,x)), otherwise repS=xtxpXtxp^txp(x,y) = (4,(l,rep.eguo/(o,6))), x = (4,(1,o)) A y = (4,(1,6)) = (4,(0,1)), x = (4,(4,0)) V y = (4,(4,6)) V x = (4,(0,1)) V y = (4,(0,1)) = (4,(5,(x,y))), where rep.eguo/( ( 2 , 0 ) , ( 2 , 0 ) ) otherwise = (2,0) rep.eguo/((2,x+ 1),(2,0)) = (2,1) rep.eguo/((2,0),(2,x + l ) ) = (2,1) rep_eguo/((2,x+ = rep.eguo/(x, y) 1),(2,y+1)) reP-FiJ.expx exp x eij>—exp (x> Vi z) = (4.(0,1)), x =(4.(0,1)) = y, X =(4.(1,0)) = z, x = ( 4 , ( 1 , y + D ) V x = (4,(4,0)) = (4,(6,(6,(x,(y,2))))), otherwise repJ^ ere: e*px<<«,-We,<*) = (10.(9,(rep_F4pp/,:expxiec,_«p(x,y),(3,(0.0))))) 172 rep-FBppfr:«px&«-«*p((4. (0.0) ), d) = (4,(0,0)) repJ^ o p p / y : e x p x r f e M - e x p ((4,(0,l)),d) = (4,(0,1)) repJ^ a p p , y : e x p x r f e c J - e x p ((4,(l,n)),d) = (4,(l,n)) rep-Fapply.expxdec3^exp((4,(2,e)),d) = repJ r / ,, : e r p - e r p (repJ r o p p / y : „ p x d e c ,_ > e x p (e,d)) r = r e p - F , n J : e r p - e r p ( r e p _ F o p p , y : e x p x d e c J _ e x p ( e , d)) ep-FappiV:exPxdeu-*exp( r ( 4 , (3 , e ) ) , d) F eP- op P / v: «pxexp(X, "), y, 2), «) ™P-F*pplviezpxdeu-*ezp( ( 4 . ( 7 , ( i , e ) ) ) , d) = rep_T opp / y:expx< ( ec4 _ >exp (rep_/' Ttplace:ezpxexp-*exp("0dy'>reP-^ apply:expxdecs-*exp\e,d)),a) where 6ody = rep.FJtUh:idenixdec3^exp(i,d) 173 re P-f,rep/a«:erpxex7,-exp((4. rep-Fnplact:txpx ( 0 , 0 ) ) , r) = r ^-^,((4,(0,1)),0 = (4,(0,1)) = (4,(l,n)) rep-Fr^c^rpx^-exp^.a.n))^) rep-Fnplace:expx «,-e«p((4.(2.e)),r) r eP-Ffst;txp-~czp(reP-Frephce:exp X «p-erp ( e , 0 ) rep-F«p/ace:erpXexp_exp((4,(3,e)),r) reP-T ind-.cxpxexp—cxpKTep-ï replacc:erpXerp-+crp\ei r)) rep-F„p/ace:erpXexp_erp((4,(5,(5,(x,y)))),r) = repJ? _. e x p x e x p _ > e x p (rep_r rep/aee:expXerp^erp(X»0» *«p'«ee:expXe*p-»erp(y»r)) r ep-F„p,aee:expxexp_erp((4,(4,(5,(x,y)))),r) = (rep.r rep/ace:erpxexp—"•exp(X,r),rep_r r e p / a c e : e x p x erp—•erpli'' r ) ' r ep-Frep/a«:expxerp_e;rp((4,(6,(6,(x,(y,2))))),r) = where x' = rep_F rep , Bce:expxexp ^ eX| ,(x,r) » = reP-*1 replace:exp x exp•~>cxp\y,>T) Z = ^P—^ rep/ace:erpxexp—•expl'2'r) rep-Frep,ace:expxexp_exF((4,(7,(7,(i,e)))),r) rep_Fi/:expXexpxexp^erp(x',y',2') = (4,(7,(7,(i,rep_F„p/ace:expxexp_exp(e,r))))) rep-F/e n t t m (x,yj,e,a) reP-Fgef.identxnnmxcxpxdccs—e*p(x»(l . 0 ) , e, d) = re = F P- jet:i(^exp(x,d) = (1,0) »«pJ'..m.:««.«xM«.«-...m((l.* + l ) . C l . < » ) ~ U»l> « p J , . « m e : « e . t x W « H - . « . m ( ( 1 . 0 ) . < l . * + 1 >) = C1»1) «P-fj.meM.'eiHxMeiU—a.roU1»1 + 1 ) , ( 1 , y + D ) = repJ? tamt.idtnt 174 x jtf en *-n«m (x, y) A.6 The self-interpreter program The rep .interpréter function is implemented in Toy by the program shown below. Note that we shall use numerical characters to represent numbers rather than the Toy représentation using suce and 0. For the sake of readability we also use meaningful identifiers rather than strings of x as the Toy syntax spécifies. •where(arg) where •where - (10,(9,(•apply(arg),(3,(0,0))))); •apply = i f f s t ( f s t (arg)) • 4 then i f f s t ( s n d ( f s t ( a r g ) ) ) * 0 then f s t (arg) else i f f s t ( s n d ( f s t ( a r g ) ) ) = 1 then f s t (arg) else i f f s t ( s n d ( f s t ( a r g ) ) ) = 2 then *fst(*apply((snd(fst(arg)),snd(arg))) else i f f s t ( s n d ( f s t ( a r g ) ) ) * 3 then *snd(*apply((snd(fst(arg)),snd(arg))) else i f f s t ( s n d ( f s t ( a r g ) ) ) = 4 then (4,(4,(*apply((fst(snd(snd(snd(fst(arg))))),snd(arg))), *apply((snd(snd(snd(snd(fst(arg))))),snd(arg)))))) else i f f s t ( s n d ( f s t ( a r g ) ) ) = 5 then *=(*apply((fst(snd(snd(snd(fst(arg))))),snd(arg))), •apply((snd(snd(snd(snd(fst(arg))))),snd(arg)))) else i f f s t ( s n d ( f s t ( a r g ) ) ) « 6 then •apply((^if((•apply((fst(snd(snd(snd(fst(arg))))),snd(arg))), (fst(snd(snd(snd(snd(fst(arg)))))), snd(snd(snd(snd(snd(fst(arg))))))))), snd(arg))) else i f f s t ( s n d ( f s t ( a r g ) ) ) * 7 then •apply((•replace((•fetch(fst(snd(snd(fst(arg))))),snd(arg))), •apply((snd(snd(snd(fst(arg)))),snd(arg))))) else error e l s e error; 175 *fst = if fst(arg) = 4 then if fst(snd(arg)) = 0 then if sdn(snd(arg)) = 1 then (4,(0,1)) else error else if fst(snd(arg)) * 1 then arg else if fst(snd(arg)) = 4 then fst(snd(snd(snd(arg)))) else (4,(2,arg)) else (4,(2,arg)); •snd = if fst(arg) • 4 then if fst(snd(arg)) = 0 then if sdn(snd(arg)) • 1 then (4,(0,1)) else error else if fst(snd(arg)) « 1 then arg else if fst(snd(arg)) • 4 then snd(snd(snd(snd(arg)))) else (4,(3,arg)) else (4,(3,arg)); *= = if *and((fst(fst(arg))=4,fst(snd(arg))*4)) then if *and((fst(snd(fst(arg)))*l,fst(snd(snd(arg)))=1)) then (4,(l,*rep.equal((snd(snd(fst(arg))),snd(snd(snd(arg))))))) else if *or((*and((fst(snd(fst(arg)))*4.fat(snd(snd(arg)))=4)), *and((*aud((fst(snd(fst(arg)))-0, snd(snd(fst(arg)))*l)), «•and((fst(snd(snd(arg)))-0, snd(snd(snd(arg)))=l)))))) then (4.(0.1)) else (4,(5,arg)) else error; •rep.equal « if »and((fst(fst(arg))=2,fst(snd(arg))=2)) then (2,snd(fst(arg))»snd(snd(arg))) 176 else error; •if = if fst(fst(arg)) = 4 then if •and((fst(snd(fst(arg)))=0,snd(snd(fst(arg)))=l)) then (4,(0,1)) else if •and((fst(snd(fst(arg)))=l,snd(snd(fst(arg)))=0)) then fst(snd(arg)) else if •or((fst(snd(fst(arg)))=1,fst(snd(fst(arg)))=4)) then snd(snd(arg)) else (4,(6,(6,(fst(arg),(fst(snd(arg)),snd(snd(arg))))))) else (4,(6,(6,(fst(arg),(fst(snd(arg)),snd(snd(arg))))))); •replace = if fst(fst(arg)) = 4 then if fst(snd(fst(arg))) = 0 then if snd(snd(fst(arg))) = 0 then snd(arg) else (4,(0,1)) else if fst(snd(fst(arg))) = 1 then fst (arg) else if fst(snd(fst(arg))) = 2 then •fst(•replace((snd(snd(fst(arg))),snd(arg)))) else if fst(snd(fst(arg))) = 3 then •snd(•replace((snd(snd(fst(arg))),snd(arg)))) else if fst(snd(fst(arg))) = 5 then •=((•replace((fst(snd(snd(snd(fst(arg))))),snd(arg))), •replace((snd(snd(snd(snd(fst(arg))))),snd(arg))))) else if fst(snd(fst(arg))) = 4 then (•replace((fst(snd(snd(snd(fst(arg))))),snd(arg))), •replace((snd(snd(snd(snd(fst(arg))))),snd(arg)))) else if fst(snd(fst(arg))) = 6 then •if((•replace((fst(snd(snd(snd(fst(arg))))),snd(arg))), (•replace((fst(snd(snd(snd(snd(fst(arg)))))), snd(arg))), •replace((snd(snd(snd(snd(snd(fst(arg)))))), snd(arg)))))) 177 else if fst(snd(fst(arg))) = 7 theD (4,(7,(7,(fst(snd(snd(snd(fst(arg))))), •replace((snd(snd(snd(snd(fst(arg))))), snd(arg))))))); •fetch = if fst(snd(arg)) = 3 then if fst(snd(snd(arg))) = 0 then (4,(0,1)) else if fst(snd(snd(arg))) = 1 then •get((fst(arg), (•same((fst(arg),fst(snd(snd(snd(snd(arg))))))), (fst(snd(snd(snd(snd(snd(arg)))))), snd(snd(snd(snd(snd(snd(arg)))))))))) else error; else error; •get = if fst(fst(snd(arg))) = 1 then if snd(fst(snd(srg))) = 0 then fst(snd(snd(arg))) else •fetch((fst(arg),snd(snd(snd(arg))))) else error; •same = if •and((fst(fst(arg))=l,fst(snd(arg))=D) then (l,snd(fst(arg))=snd(snd(arg))) else error; •and = if fst(arg) then snd(arg) else fst(arg); •or = if fst(arg) then fst(arg) else snd(arg); 178