A Guide to Specialising Gödel Programs with the Partial Evaluator
Contents
1. lt FormulaVariables goal vars amp AnswerString1 vars program module answer string PREDICATE AnswerString1 List Term Program String TermSubst String String AnswerString1 _ _ _ _ AnswerString1 varlrest program module answer comma string rest string lt ApplySubstToTerm var answer var_answer amp BindingToString var var answer program module comma commal string amp AnswerString1 rest program module answer commal rest string PREDICATE BindingToString Term Term Program String String String String BindingToString var var answer program module comma commal string lt IF var var_answer THEN commai comma amp string ELSE ProgramTermToString program module var var_string amp ProgramTermToString program module var_answer answer_string amp commai amp string comma var_string answer_string 22 5 SPECIALISING GODEL META PROGRAMS 23 PREDICATE Go 1 String String Go_1 goal_string answer string lt StringToProgramFormula lt Append gt Append goal_string goal amp MySucceed 1 goal var _ Empty _ EmptyTermSubst answer 4 FormulaVariables goal vars amp AnswerString1 1 vars answer answer string PREDICATE AnswerString1_1 List Term TermSubst String String AnswerString1_1 _ _ lt AnswerString1_1 var rest answer comma str2. Compute partial evaluations of safe selectable atoms in goal and covering atoms 6 Construct residual script e Optimise partially evaluated atoms e Remove superfluous code e Construct new predicate declarations e Insert specialised declarations and code 7 Write residual script to file Write log to screen and file 3 2 Running SAGE In this section we provide a manual for using SAGE and an example of its execution 3 2 1 Loading and Invoking SAGE SAGE is comprised of four modules SAGE PE Assemble and Analyse It is loaded by loading the top level module SAGE Once loaded SAGE is invoked by the proposition RunPE 3 2 2 User Inputs Strings are input to SAGE without quotes and are terminated by a carriage return Full stops are not required to terminate a string Non selectable predicates are input individually as atoms The end of a list of them is denoted by inputting a carriage return to the prompt When specialising a meta program that is any program which imports the system module Syntax the user is prompted whether they want to mark the WA M like predicates as non selectable The relevance of these predicates is discussed in Section 5 1 The file extensions for the object program and specialised script that is prm and scr respec tively are appended automatically by SAGE So if your program s main module is Main then SAGE will write the residual script to the file Main scr This process will overwrite existing fi
3. Then 1 lt R A Else 2 lt R B 4 3 Pruning While there is a strong argument in favour of allowing pruning within logic programs it is well established that the cut operator of Prolog is unsound Hill et al 6 propose an alternative pruning operator for logic programming the commit which while naturally affecting completeness is proved to be sound The commit operator is supplied by G del to allow pruning and has three forms The most general form of the Godel pruning operator has the form _n of which two special cases have the form and We refer to the most general form as the full commit It is also shown in 6 that provided two conditions are met the computational equivalence of a program and its partial evaluation wrt a given goal that is 7 theorem 4 3 can be extended to encompass programs containing commits These conditions are restrictions on the structure of the SLDNF trees used to obtain the partial evaluation and are referred to as the freeness and regularity conditions A detailed description of the commit operator and proof of its soundness would unfortunately be far too long for a paper of this form Suffice it to say that it is shown in 4 that while the freeness condition is acceptable the regularity condition imposes restrictions on the computation of partial evaluations which are both expensive to enforce and lead to a significant reduction in the amount of specialisation that may be per
4. an atom whose predicate or proposition symbol is declared in a closed module it interprets the execution of a call to this atom wrt the program being partially evaluated as long as this atom matches any delay declaration for the relevant predicate or proposition Thus an atom such as Member x 1 2 3 whose predicate is defined in the system module Lists will be executed by SAGE during a partial evaluation An atom such as Member x y however will not be executed as it does not match the delay declaration in the system module Lists for this predicate DELAY Member _ y UNTIL NONVAR x Any such atom which is not executed by SAGE will be left as a residual atom in the partial evaluation 2 2 2 G del Scripts When partially evaluating a Godel program a process we refer to as flattening occurs The details of this flattening process are not relevant here but we remark that because of this process any partial evaluator must construct the results of a partial evaluation as a G del script A script is essentially a G del program from which all module structure has been removed G del supports the representation of partially evaluated programs as scripts and a file Program scr containing the representation of a script may be compiled into executable code by calling the script compile command sc Program from the G del environment Removing the module structure of a program by constructing its partial evaluation as a script is not as drastic a m
5. manner in which Resolve implements it means that the WAM does not have an equivalent to the UnifyFunction instruction 5 SPECIALISING GODEL META PROGRAMS 20 Promoting Symbols from the Ground Representation When performing the partial evaluation of a meta program we recommend that SAGE be permitted to unfold any of the data type predicates EmptyTermSubst And Or Not etc The unfolding of such predicates in the definition of Solve for example will cause the symbols used by G del s ground representation to be promoted into the heads of the three statements as can be seen in Figure 5 This would permit the Bristol G del to perform first argument indexing on the specialised definition of this predicate and thus make the execution of this specialised code more efficient An important point to note is that the Bristol Godel only performs indexing on the first argument of the head of a statement Therefore it is most important to ensure that the argument on which the user of SAGE would wish the specialised version of a meta program to perform indexing will be the first argument in the specialised meta program In the unspecialised meta interpreter SLD the desired argument is in fact the second argument in the heads of the statements defining Solve However as the first argument to the specialised call is instantiated to a term which will be discarded in the specialised program that is the representation of the object program which SLD is s
6. nbi amp AndWithEmpty nb1 r nb amp Select nb new answer program 11 si r1 amp MySucceed s1 program new var vari 11 ri new answer answer PREDICATE MyStatementMatchAtom Program Formula Formula MyStatementMatchAtom program atom statement s PredicateAtom atom pred V PropositionAtom atom pred amp DefinitionInProgram program _ pred defn amp Member statement defn PREDICATE Select Formula TermSubst Program Formula Formula Formula Select formula _ _ formula formula formula lt EmptyFormula formula Select formula subst program left selected right lt And 1 r formula IF SOME 11 si ri Select 1 subst program 11 si r1 THEN 5 SPECIALISING GODEL META PROGRAMS 25 left 11 amp selected s1 4 AndWithEmpty r1 r right ELSE Select r subst program 11 selected right amp AndWithEmpty 1 11 left Select formula subst program empty formula empty lt Atom formula EmptyFormula empty amp CanRunAtom program formula subst PREDICATE CanRunAtom Program Formula TermSubst CanRunAtom program atom sss s PredicateAtom atom predicate _ amp ProgramPredicateName program module _ _ predicate amp IF SOME heads conditions n ControlInProgram program module predicate heads conditions amp Length heads n amp n gt 0 THEN GetDelay heads conditions atom sss PREDICATE GetDelay List
7. specialisation of this predicate If we wish to both specialise a predicate and prevent unwanted unfoldings of calls with this predicate we have two further options The first option is to ensure that the relevant predicate will be marked unsafe by SAGE This will happen whenever this predicate is recursive and insufficiently instantiated at the time of partial evaluation This strategy of SAGE s will often work successfully for recursive predicates in meta programs as examples in Section 5 demonstrate However for some predicates particularly non recursive predicates such as Filter above this is not sufficient A second option for preventing unwanted unfoldings makes use of SAGE s technique for specialising conditional formulas in G del programs This technique is described in Section 4 2 and is guided primarily by a test of whether the condition of a conditional is sufficiently instantiated at the time of partial evaluation for SAGE to be able to determine whether or not it will succeed when the specialised program is executed H the condition of a conditional is sufficiently instantiated at partial evaluation time then it will be unfolded together with the then part or else part as appropriate If the condition is not sufficiently instantiated at partial evaluation time then the conditional will still be specialised but the residual code will remain as a single conditional formula For example we might modify the above definition of the p
8. subst subst lt EmptyFormula goal Solve program goal v_in v_out subst_in subst_out lt And left right goal amp Solve program left v_in new_v subst_in new_subst amp Solve program right new_v v_out new_subst subst out Solve program goal v in v out subst_in subst out lt Atom goal amp MyStatementMatchAtom program goal statement amp Resolve goal statement v in new v subst in new subst new goal amp Solve program new goal new v v out new subst subst out PREDICATE MyStatementMatchAtom Program x Formula Formula MyStatementMatchAtom program atom statement lt PredicateAtom atom pred _ PropositionAtom atom pred amp DefinitionInProgram program _ pred defn amp Member statement defn Solve program goal v_in v_out subst_in subst_out lt Or left right goal amp Solve program left v_in v_out subst_in subst out Solve program right v_in v out subst in subst out Solve program goal v v subst subst lt Not goal1 goal amp Solve program goall v _ subst _ Figure 4 Extension to the Definition of Solve 5 SPECIALISING GODEL META PROGRAMS 18 DefinitionInProgram versus StatementMatchAtom In the third statement in the definition of the predicate Solve we have used the user defined predicate MyStatementMatchAtom where one might have expected to use the system predicate StatementMatchAtom The reasoning behind
9. the Solve predicate SAGE has made three optimisations 1 the calls to Resolve have been specialised wrt the two statements in the object program to 5 SPECIALISING GODEL META PROGRAMS 21 produce the third and fourth statements respectively in the new predicate Solve 1 2 symbols such as Empty and amp which are ordinarily hidden by G del s implementation of the ground representation as an abstract data type have been promoted into the specialised program 3 the representation of the object program Append which is now redundant has been removed by replacing the predicate Solve 6 by the new predicate Solve_1 5 5 2 The Interpreter Coroutine The second meta interpreter we consider is while still a relatively small meta program significantly more complex than SLD and serves to illustrate more sophisticated meta programming techniques such as the explicit manipulation of substitutions and implementation of a selection rule 5 2 1 Using SAGE on the Module Coroutine The module Coroutine loc is the main module for this interpreter and performs the same I O and pre and post processing functions that were performed by the module SLD in the previous section The two main differences between this module and the SLD module are that this module 1 calls MySucceed where the SLD module calls Solve 2 produces a more sophisticated presentation of the answer substitution The first of these two points merely emphasises that the int
10. this choice concerns the delay declarations for the two system predicates StatementMatchAtom and DefinitionInProgram and the fact that during partial evaluation of the program SLD the object program will be known but the object goal will be unknown StatementMatchAtom and DefinitionInProgram are both defined in the closed system module Programs and have the following declarations PREDICATE StatementMatchAtom Program Representation of a program String Name of an open module in this program Formula Representation of an atom in the flat language of this program Formula Representation of a statement in this module whose proposition or predicate in the head is the same as the proposition or predicate in this atom DELAY StatementMatchAtom x _ z _ UNTIL GROUND x amp GROUND z PREDICATE DefinitionInProgram Program Representation of a program String Name of an open module in this program Name Representation of the flat name of a proposition or predicate declared in this module List Formula List in a definite order of representations of statements in the definition of this proposition or predicate x x DELAY DefinitionInProgram x _ _ _ UNTIL GROUND x As the object program is known during partial evaluation we would expect that SAGE would encounter calls to these predicates for which the first argument and only the first argument were instantiated Examining the above delay
11. user can comprehend Performing Pre and Post Processing of Interpretations The module SLD imports the module Solve which defines the predicate Solve This predicate performs the actual interpretation of the object goal wrt the object program and is called by the Demo predicate Before it is called Demo will call the predicates StandardiseFormula and EmptyTermSubstitution to initialise the variables in the object goal and to get the representation of an empty term substitution Demo then calls Solve which performs the interpretation returning the representation of the answer substitution To enable this answer substitution to be converted into a string which may be re turned to the user Demo will apply the substitution to the interpreted goal by using the predicate ApplySubstToFormula This formula is then converted to a string as described above Specialising the Module SLD Examining the specialisation of the module SLD allows us to illustrate the difference in SAGE s hand ling of open and closed code Let us assume that we wish to specialise the program SLD wrt a known object program Append for example and an unknown goal We can see that we would wish to partially evaluate SLD wrt the goal lt Demo Append g a We shall consider first what will happen when SAGE unfolds the I O predicates called by Demo In the Bristol G del these I O predicates are all defined in closed modules and have the delay declarations given in Figure 2 Th
12. A Guide to Specialising Godel Programs with the Partial Evaluator SAGE C A Gurr Human Communication Research Centre University of Edinburgh 2 Buccluech Place Edinburgh EH8 9LW Scotland April 1994 Abstract This document provides a description of the partial evaluator SAGE a partial evaluator written in the logic programming language G del which specialises G del programs Although capable of specialising any G del program SAGE was developed primarily to specialise meta programs which use a ground representation To assist users of SAGE this document gives an overview of SAGE a manual for its use and a guide to writing G del programs particularly meta programs in a style which makes them amenable to specialisation 1 Introduction Godel is a declarative general purpose logic programming language which provides a number of higher level programming features including extensive support for meta programming with a ground repre sentation The Godel language is documented in 5 and we refer here to the current implementation of G del as The Bristol G del This document provides a description of the partial evaluator SAGE Self Applicable G del partial Evaluator a manual for its use and a guide to writing G del programs in a style which makes them amenable to specialisation by SAGE A full description of the techniques employed by SAGE is given in 4 A summary of that document is given in 3 SAGE was originally implement
13. Bis handled simply by transforming them to the forms A B A Band A amp B A amp B respectively Disjunctions may be unfol ded to produce two resultants one for each of the disjuncts For example the disjunction in the re sultant H lt Ak B C amp D can be unfolded to produce the two new resultants H lt A amp B amp D andH lt A amp C amp D During SAGE s partial evaluations existentially quantified variables are renamed so as to have names different from all other variables in the formula Consequently SAGE may generally ignore existential quantifiers as the names of the quantified variables are guaranteed not to occur outside the scope of the quantifier The cases where we are interested in knowing whether variables are free or quantified in negated formulas for example are dealt with by the unfolding strategy for those particular cases 4 SPECIALISING GODEL PROGRAMS 12 Universally quantified formulas such as ALL x P x y are transformed to the form SOME x P x y 4 2 Constructive Negation and Conditional Formulas For negated formulas in G del programs we have extended the definition of partial evaluation in 7 to include the concept of constructive negation 1 Constructive negation may be described as follows First a partial evaluation of the formula that has been negated is computed If there are no residual resultants for this partial evaluation then the formula has failed finitel
14. For each unsafe predicate SAGE will compute a generalisation of every atom in the partial evaluation which has this predicate This generalisation is referred to as a covering atom for this predicate A partial evaluation of each of the covering atoms is then computed 2 3 4 Selection Strategy The current implementation of SAGE relies upon a depth first leftmost safe selectable literal selection strategy That is to say when selecting a literal for unfolding from a formula SAGE will always select the leftmost literal whose predicate symbol is both selectable and safe Note that by not selecting literals with unsafe predicates and computing partial evaluations of the unsafe atoms in which unsafe literals are not selected SAGE produces specialised recursive definitions for unsafe predicates 2 3 5 Post Partial Evaluation Optimisations Having performed the partial evaluation SAGE performs a post processing optimisation which involves the deletion of redundant terms from the partially evaluated atoms For example if P A x y B is an atom which is partially evaluated by SAGE then a new predicate P_1 binary in this case will be defined and every instance of this partially evaluated atom will be replaced by an equivalent instance of the atom P_1 x y The definition of P will be replaced with the definition of this new predicate P_1 in the specialised program When constructing the specialised program SAGE will delete all redundant selectable pred
15. Formula List Condition Formula TermSubst GetDelay head condition _ atom subst lt Instance0fHead head atom subst sss amp ConditionSatisfied condition sss GetDelay Irh _lrc atom sss lt GetDelay rh rc atom sss PREDICATE InstanceOfHead Formula Formula TermSubst List Bind Instance0fHead head atom subst bind lt PredicateAtom head name head_args amp PredicateAtom atom name args amp Instance0fHead2 head_args args subst bind PREDICATE InstanceOfHead1 Term Term List Bind List Bind Instance0fHeadi1 head arg arg b head_arg arglb lt Variable head_arg InstanceO0fHeadi head_arg arg subst subst lt ConstantTerm head_arg name ConstantTerm arg name InstanceOfHeadi head_arg arg subst new_subst lt FunctionTerm head_arg name head_args FunctionTerm arg name args amp InstanceOfHead3 head_args args subst new_subst PREDICATE Instance0fHead2 List Term List Term TermSubst List Bind List Bind REFERENCES 26 Instance0fHead2 _ subst subst Instance0fHead2 head_arg head_args arglargs sss subst new_subst lt ApplySubstToTerm arg sss arg1 amp InstanceOfHeadi head_arg argi subst substi amp InstanceO0fHead2 head_args args sss substi new_subst PREDICATE Instance0fHead3 List Term List Term List Bind List Bind Instance0fHead3 subst subst I
16. artial evaluation of P wrt lt P x we lastly replace the definition of the predicate P in P with this new definition 2 2 Partial Evaluation of G del Programs G del provides a module system for programming and has a large library of system modules 20 in the Bristol G del In this section we describe two aspects of this module system which affect and are affected by partial evaluation 2 2 1 Open and Closed Code in Godel Programs Modules in G del programs may be of one of two kinds The first kind of modules are those which have been written by some G del user and are referred to as user defined modules The second kind of modules are those which are provided by the G del system and these are referred to as system modules The majority of system modules are what we refer to as closed modules A module is closed if its export part uses the module keyword Closed instead of the keyword Export Any module which is not closed is an open module In the Bristol G del only system modules may be closed modules and all system modules are closed other than the Syntax module All code in a G del program falls into one of two categories which we refer to as open and closed We define the open code of a G del program to be that code which is either defined in a user defined module of the program or which is defined in an open system module We define all code that is defined in a closed G del system module as being closed code When SAGE encounters
17. ator which was developed primarily to specialise G del meta programs which use the ground representation Therefore it is fitting that we devote a section of this guide to illustra ting with examples the features of G del s ground representation which allow suitable meta programs to be effectively specialised by SAGE 5 1 The Interpreter SLD We first present the meta interpreter SLD which is analogous to the well known vanilla or solve meta interpreter of languages such as Prolog The difference between SLD and a vanilla interpreter is that SLD uses a ground representation and a vanilla interpreter uses a non ground representation The meta interpreter SLD is the most simple ground meta interpreter which could be written and we use it here to illustrate the basis issues involved in specialising G del meta programs with SAGE 5 1 1 Using SAGE on the Module SLD The module SLD 1loc is the main module for this interpreter and illustrates two things 1 A potential approach to I O for for meta programs 2 The pre and post interpretation instructions MODULE SLD IMPORT Solve ProgramsI0 PREDICATE Demo String String String Demo program_string goal_string answer_string lt FindInput program_string t prm Inis amp GetProgram is program amp MainModuleInProgram program module amp StringToProgramFormula program module goal_string goal amp StandardiseFormula goal 0 var goal1 amp EmptyTermSubst emp
18. declarations we see that this would mean that calls to DefinitionInProgram would be executed by SAGE and that calls to StatementMatchAtom would be left as residual For this reason we provide the user defined predicate MyStatementMatchAtom The declarative meaning of this predicate is equivalent to that of StatementMatchAtom the difference being that when specialising the program SLD wrt a known object program SAGE may unfold the call to MyStatementMatchAtom and thereby deduce the representations of all open statements in the object program The Partial Evaluation of Resolve It is in the third statement in the definition the predicate Solve that we see a call to the predicate which is possibly the most important meta programming predicate of all of those provided by G del the predicate Resolve The atom Resolve atom st v v1 s s1 body is called to perform the resolution of the atom atom with the statement st The integers v and v1 are used to rename the statement with v being the 5 SPECIALISING GODEL META PROGRAMS 19 integer value used in renaming before the resolution step is performed and v1 being the corresponding value after the resolution step has been performed The representations of term substitutions s and s1 represent respectively the answer substitution before and after the resolution step The last argument body is the representation of the body of the renamed statement The predicate Resolve has been designed to meet the needs of
19. easure as it may seem if we assume that the module structure is provided primarily 2 AN OVERVIEW OF PARTIAL EVALUATION 4 for software engineering purposes Here the module structure is a useful aid to the programmer when writing and debugging the original program It seems safe to assume that a program will only be partially evaluated once it is complete and hopefully bug free In this case the user needs only to be certain that the answers computed by the partially evaluated program are correct with respect to the original program and he she is unlikely to be concerned with the module structure of the specialised program In fact taking the widely accepted view that partial evaluation may be considered as a part of the compilation process for a program the above argument is perfectly acceptable All that programmers will generally require from the compilation of their programs is that the compiled version of a program should be correct with respect to the original program 2 3 SAGE s Implementation of Partial Evaluation In this section we give an overview of SAGE s strategy for partially evaluating Godel programs 2 3 1 Non Selectable Predicates When requesting SAGE to perform a partial evaluation of some program the user may denote certain of the predicates in the program to be non selectable A predicate is selectable if it is not non selectable Non selectable predicates are never selected for unfolding by SAGE thus they can be used
20. ed lt load Append Loading module Append Append lt type Append_1 PREDICATE Append 1 List Integer List Integer Append lt Append_1 x y x y 1 2 3 x 1 y 2 3 Yes Append lt quit unix 3 3 Viewing Residual Scripts The Bristol G del does not currently provide a script viewer so the means of viewing the residual code produced by SAGE are somewhat limited at the moment Support for viewing scripts is currently provided by the program View This program consists of the single module View and once loaded may be invoked with the atom ViewScript lt script_name gt where lt script_name gt is the name a string of the top level module of the program that has been specialised For example the specialised code for the Append program given above which is stored in the file Append scr may be viewed via the call ViewScript Append 3 4 Some Tips on Writing Programs to be Specialised Recall that atoms which are selectable and not unsafe are always unfolded by SAGE It must be stressed that this unfortunately is not always a good thing as the following example illustrates Let P be the following program FilterList FilterList xlrest list lt Filter x list listi1 amp FilterList rest listi Filter A list list Filter x x list list lt x A which we are specialising wrt the goal lt FilterList x y z list If the predicat
21. ed to test techniques developed during research into the self application of a declarative partial evaluator written in a logic programming language As such SAGE was and is designed primarily for the specialisation of G del meta programs which use a ground representation G del meta programs which use a ground representation suffer from a computational expense that this incurs which is in addition to the so called interpretation overhead that is recognised in all meta programs However these extra overheads may be almost entirely removed by partial evaluation We refer to this as specialising the ground representation and a summary of the techniques used to perform this is given by 2 These techniques may be applied to supplement techniques used to remove the more familiar interpretation overheads The layout of this guide is as follows In the following section we give a brief overview of partial evaluation as it is defined for SAGE In Section 3 we provide a user manual for SAGE and give some email corin cogsci ed ac uk 2 AN OVERVIEW OF PARTIAL EVALUATION 2 pointers on good programming style for writing Godel programs which are intended to be specialised by SAGE Finally in Sections 4 and 5 we describe with examples SAGE s strategy for unfolding general G del programs and G del meta programs respectively 2 An Overview of Partial Evaluation SAGE is a partial evaluator based mainly on finite unfolding Partial evalua
22. equality atoms will be unfolded This conditional will be replaced by a specialised version which will appear in the definition of the specialised AnswerString1 predicate To illustrate these specialisations Figure 6 shows the partial evaluation of the Coroutine module wrt the object program Append As comparatively little specialisation of the predicates AnswerString1 and BindingToString may actually be performed it is possible that a user of SAGE might prefer simply to mark either AnswerString or AnswerString1 as non selectable thus leaving the residual definitions of these pre dicates the same as their original definitions A selection of more effective specialisations of conditionals is illustrated by the partial evaluation of the module Conc 5 SPECIALISING GODEL META PROGRAMS MODULE Coroutine IMPORT Conc ProgramsI0 PREDICATE Go String String String Go program_string goal_string answer_string lt FindInput program_string t prm Inis amp GetProgram is program amp MainModuleInProgram program module amp StringToProgramFormula program module goal_string goal amp FormulaMaxVarIndex goal var amp EmptyTermSubst empty amp EmptyFormula e amp MySucceed goal program var _ e e empty answer amp AnswerString program module goal answer answer_string PREDICATE AnswerString Program String Formula TermSubst String AnswerString program module goal answer string
23. erefore SAGE will execute calls which match these declarations and DELAY FindInput x _ UNTIL GROUND x DELAY GetProgram x _ UNTIL GROUND x DELAY MainModuleInProgram x _ UNTIL GROUND x DELAY StringToProgramFormula x y z _ UNTIL GROUND x amp GROUND y amp GROUND z DELAY ProgramFormulaToString x y z _ UNTIL GROUND x amp GROUND y amp GROUND z Figure 2 Delay Declarations for I O Predicates leave as residual those calls which fail to match these declarations As the string giving the name of the object program is known we see that the call FindInput will be executed and that therefore the calls GetProgram and MainModuleInProgram will also be executed In this way SAGE is able to deduce the representation of the object program that SLD is to be specialised wrt However the string giving the representation of the object goal is unknown and therefore the call StringToProgramFormula will not be executed as the third argument is not ground 5 SPECIALISING GODEL META PROGRAMS 16 Similarly as a ter the partial evaluation of the interpretation the object goal and answer substitution will still be unknown the call ProgramFormulaToString will also be left as residual We now consider the partial evaluation of the pre and post processing instructions It is essential to note that in the Bristol G del the system module Syntax is an open module and that therefore the definitions of the predicates called during pre and pos
24. erpretation performed by Coroutine is different to that of SLD We shall examine this in more detail below The second point a more sophi sticated presentation of the answer substitution is illustrative of certain aspects of the manipulation of substitutions in meta programs and the specialisation of conditionals We consider this next Partial Evaluation of the Predicate AnswerString Suppose that we permit SAGE to unfold any of the predicates appearing in the definitions for AnswerString AnswerString1 and BindingToString When specialising the initial call to AnswerString the representation of the object program and main module name that is the first two arguments will be known but the other arguments will be unknown It is apparent therefore that SAGE will mark the predicate AnswerString1 as being unsafe in this partial evaluation When performing the partial evaluation SAGE will therefore unfold the call to AnswerString in Go but not the call to AnswerString1 Instead a separate call to AnswerString1 with the first two arguments instantiated will be specialised to produce a new recursive definition of this predicate in which the call to BindingToString will have been unfolded The condition of the conditional in the definition of BindingToString will not be unfolded as it not sufficiently instantiated to be executed without binding any free variables Examining the formulas in the then part and else part of this conditional we see that only the
25. es FilterList and Filter were both marked selectable and safe then SAGE would produce the following specialised definition for FilterList FilterList A A A D FilterList A A x x lt x A FilterList A x A l x lt x A 3 A GUIDE TO USING SAGE 10 FilterList A x y x y lt x A amp y A FilterList x A A x lt x A FilterList x A y x y lt x A amp y A FilterList x y A x y lt x A amp y A FilterList x y z x y z lt x A amp y A amp z A The above new definition while highly specialised is probably not ideal as we have introduced a large element of non determinism which makes this residual code less efficient than it might be The problem is caused by the fact that we have unfolded the call to Filter when we probably would have preferred not to To solve this problem we must find a means of preventing such unfoldings from being made There are three ways in which this may be achieved the first of which is that we mark a predicate such as Filter as being non selectable For the program and goal above such a partial evaluation would lead to the following specialised code FilterList x y z list lt Filter x list listi1 amp Filter y listi list2 amp Filter z list2 Filter A list list Filter x xllist list lt x A However marking a predicate non selectable means that SAGE will not be able to perform any
26. formed In 4 a technique for partially evaluating programs containing commit operators is presented which allows us to strengthen the partial evaluation theorem for such programs 6 theorem 3 2 by entirely removing the regularity condition While techniques have been developed that enable a partial evaluator to perform unfolding with out respecting the regularity condition the full commit is necessary to implement these techniques Unfortunately the Bristol Godel does not currently support the full commit and therefore the version of SAGE documented here cannot implement these techniques In view of the restrictive nature of unfolding while respecting the regularity condition we have decided that the best approach under the circumstances is that the current implementation of SAGE should remove all commits in any program statements which it specialises This approach will not affect the soundness of the partial evaluation although it does imply that a partially evaluated program may return more answers than the unspe cialised program for certain queries as pruning is effectively disabled for all selectable predicates 4 4 Set Terms and the Sets Module Note The current implementation of SAGE does not support programs which import the Sets module therefore the correctness of partially evaluated programs which import Sets cannot be guaranteed 5 SPECIALISING GODEL META PROGRAMS 14 5 Specialising Godel Meta Programs SAGE is a partial evalu
27. gives this specialised PREDICATE Demo 1 String String Demo_1 goal_string answer_string lt StringToProgramFormula lt Append gt Append goal_string goal amp StandardiseFormula goal 0 var goal1 amp Solve 1 goal var _ EmptyTermSubst answer amp ApplySubstToFormula goal1 answer answer goal amp ProgramFormulaToString lt Append gt Append answer goal answer string Figure 3 Specialised Version of Module SLD definition for Demo in which we have denoted the representation of the object program Append by lt Append gt In addition we have replaced calls to the predicates Demo and Solve by calls to the new predicates Demo_1 and Solve 1 This is a post processing optimisation performed by SAGE to remove redundant terms We shall explain it in more detail when we consider the partial evaluation of the module Solve 5 1 2 Using SAGE on the Module Solve In this section we illustrate the specialisation of the ground representation by an examination of the partial evaluation of the module Solve We first comment that while the definition for the predicate Solve only covers empty formulas atoms and conjunctive formulas extending the definition of this predicate to cover other kinds of formulas would be very straightforward As an example Figure 4 gives one possible extension covering disjunctive formulas and negated formulas 5 SPECIALISING G DEL META PROGRAMS 17 LOCAL Solve Solve program goal v v
28. icates A predicate is redundant if it is not relied upon by any predicate appearing in some literal in the partial evaluations computed by SAGE 3 A Guide to Using SAGE In this section we give an outline of SAGE s main algorithm and describe how it is used We note that SAGE s strategy for computing partial evaluations is a relatively simple one and therefore we conclude this section with some pointers on how to write Godel programs which may be optimally specialised by SAGE 3 1 Algorithm for SAGE When invoked SAGE will prompt the user to input the name of the object program the object goal this program is to be specialised wrt and the list of non selectable predicates Once SAGE has 3 A GUIDE TO USING SAGE 6 constructed the partial evaluation of this program and written the resulting script into a file it will output a message describing the partial evaluation which has been computed We refer to this message as the log of the partial evaluation and a copy of this log is also written to a file The following list describes the main points of SAGE s operation 1 User inputs object program object goal and list of non selectable predicates 2 Extract selectable atoms from goal 3 Compute predicate dependency graph to determine recursive selectable predicates which atoms to be partially evaluated depend upon 4 Compute static analysis to determine which recursive predicates are unsafe and construct cover ing atoms for them 5
29. ing string1 lt ApplySubstToTerm var answer var_answer amp IF Test O var var answer THEN Then_1 comma commal string ELSE Else_2 var var answer comma commal string amp AnswerString1 rest answer commal stringi PREDICATE Test O Term xt Term Test_O var var PREDICATE Then_1 String String String Then 1 comma comma PREDICATE Else_2 Term Term String String String Else_2 var var_answer comma comma var_string answer_string lt ProgramTermToString lt Append gt Append var var string amp ProgramTermToString lt Append gt Append var answer answer string Figure 6 Specialised Version of Module Coroutine 5 SPECIALISING GODEL META PROGRAMS 24 5 2 2 Using SAGE on the Module Conc Note This section of the guide has yet to be completed EXPORT Conc PREDICATE MySucceed Formula Program Integer Integer Formula Formula TermSubst TermSubst LOCAL Conc IMPORT Programs BASE Bind FUNCTION xFx 200 Term Term gt Bind MySucceed formula _ var var _ _ answer answer lt EmptyFormula formula MySucceed formula program var vari 1 r answer_so_far answer lt Atom formula MyStatementMatchAtom program formula clause amp Resolve formula clause var new_var answer_so_far new_answer new_body amp IF EmptyFormula new body THEN AndWithEmpty 1 r nb ELSE AndWithEmpty 1 new body
30. ithout the risk of an infinite unfolding The static analysis is based upon an analysis of ground arguments in atoms If it may be determined that each occurrence of an atom with some recursive selectable predicate has a particular argument which will always be ground and that this can guarantee the finite unfolding of this atom then this predicate is marked safe Any recursive selectable predicate which is not marked safe will be marked unsafe by the static analysis For example consider the following definition of the standard Member predicate Member x xI_ Member x _ list lt Member x list 3 A GUIDE TO USING SAGE 5 This predicate is recursive If we may determine that every atom with this predicate which is encoun tered in some partial evaluation will have a ground term in the second argument then it is obvious that such an atom may be unfolded in a finite number of unfolding steps and thus this predicate would be marked safe by the static analysis If we were unable to determine that every atom with this predicate in some partial evaluation had a ground term in its second argument then the static analysis would mark this predicate as being unsafe 2 3 3 Partially Evaluated Atoms Having performed the static analysis SAGE will identify all safe selectable atoms in the goal to be partially evaluated and compute the partial evaluation of these atoms In addition SAGE will identify all instances of atoms with unsafe predicates
31. les of that name so if you have such a file we suggest that a copy with a different name is made before the partial evaluation is initiated 3 A GUIDE TO USING SAGE 7 3 2 3 SAGE Specialisation Logs Upon completion SAGE prints out the specialisation log describing the specialisation it has just performed A copy of this log is also written to the file Main new where Main is the name of the main module of the specialised program 3 2 4 An Example Run Specialising the Program Append The module Append 1loc is a G del program which gives a user defined version of the standard Append predicate This program defines MyAppend an open code version of the closed predicate Append which is defined in the system module Lists MODULE Append IMPORT Lists PREDICATE MyAppend List a List a List a MyAppend x x MyAppend alx y alz lt MyAppend x y z We show below the listing of a sample run of SAGE in which the Append program is specialised wrt the goal MyAppend x y 1 2 3 unix goedel Goedel 1 3 Type h for help lt load SAGE Loading module SAGE Loading module PE Loading module Assemble Loading module Analyse SAGE lt RunPE SAGE Partial Evaluator Object Program Name Append Loading program done Object goal MyAppend x y 1 2 3 Non Selectable Atoms Input non selectable predicates as atoms terminating with empty string Next atom 3 A GUIDE TO USING SAGE Construc
32. nstance0fHead3 head_arglhead_args arglargs subst new subst lt InstanceOfHeadi head_arg arg subst substi amp InstanceO0fHead3 head_args args substi new subst PREDICATE ConditionSatisfied Condition List Bind ConditionSatisfied cond subst lt GroundCondition var cond Member var term subst amp GroundTerm term ConditionSatisfied cond subst lt OrCondition cond1 cond2 cond OrConditionSatisfied condi cond2 subst ConditionSatisfied cond subst lt AndCondition cond1 cond2 cond ConditionSatisfied cond1 subst amp ConditionSatisfied cond2 subst ConditionSatisfied cond subst lt NonVarCondition var cond Member var term subst amp NonVariable term ConditionSatisfied cond subst lt TrueCondition cond PREDICATE OrConditionSatisfied Condition Condition List Bind OrConditionSatisfied cond _ subst lt ConditionSatisfied cond subst OrConditionSatisfied _ cond subst lt ConditionSatisfied cond subst References 1 D Chan and M Wallace A treatment of negation during partial evaluation In H D Abramson and M H Rogers editors Meta Programming in Logic Programming Proceedings of the Meta88 Workshop June 1988 pages 299 318 MIT Press 1989 REFERENCES 27 2 C A Gurr Specialising the Ground Representation in the Logic Programming Language G del In Proceedings of the Third International Workshop on Logic Program Synthesi
33. olve SAGE will unfold the call to MyStatementMatchAtom in the third statement for Solve In this manner SAGE may then specialise Resolve with respect to each statement in the object program Specialising a call to Resolve with respect to a known statement will remove the vast majority of the expense of the ground representation When a call to Resolve is specialised wrt a known object statement the specialised code is gua ranteed to be a single possible empty conjunction of atoms provided that the user has specified that the WAM like predicates were to be marked non selectable The predicates of these atoms will each be one of UnifyTerms GetConstant GetFunction UnifyValue UnifyVariable UnifyConstant or UnifyFunction These predicates perform highly specialised unification operations and together form a crucial part of the implementation of Resolve The above seven predicates we refer to as the WAM like predicates as they are analogous to emulators for the WAM instructions Get Value in the case of UnifyTerms GetConstant GetFunction Unify Value Unify Variable and UnifyConstant after which they are named As such these operations could be implemented by G del at a very low level leading to a computation time for the specialised form of a meta program which would be comparable to that of the object program itself Note that a subtle difference in the manner in which the WAM implements the unification of nested function terms and the
34. pecialised wrt then we can see that this second argument in the unspecialised definition of Solve will be the first argument of the specialised definition of Solve as we would wish Specialising the Module Solve Figure 5 illustrates the result of specialising the call Solve lt Append gt g v v1 s s1 where lt Append gt Object program MyAppend x x MyAppend alx y alz lt MyAppend x y z Specialised interpreter Solve 1 Empty v v subst subst Solve 1 left amp right v in v_out subst in subst out lt Solve 1 left v in new v subst in new subst amp Solve 1 right new v v out new subst subst out Solve 1 MyAppend arg1 arg2 arg3 v in v_out subst in subst out lt GetConstant arg1 Nil subst in s1 amp GetValue arg2 arg3 s1 new subst amp Solve 1 Empty v in V out new subst subst out Solve 1 MyAppend arg1 arg2 arg3 v in v_out subst in subst out lt GetFunction arg1 sub11 sub12 mode subst in s1 amp UnifyVariable mode subi1 var vin v1 amp UnifyVariable mode subi12 al vi v2 amp GetFunction arg3 sub21 sub22 model s1 s2 amp UnifyValue model var sub21 s2 new subst 4 UnifyVariable model sub22 a2 v2 new v amp Solve 1 MyAppend a1 arg2 a2 new v v out new subst subst out Figure 5 Specialisation of Solve wrt Append is the representation of the Append program In this specialised definition of
35. practically any G del meta program which performs logical inference steps To achieve this the implementation of this predicate handles the following operations e Renaming the statement to ensure that the variables in the renamed statement are different from all other variables in the current goal e Applying the current answer substitution to the atom to ensure that any variables bound in the current answer substitution are correctly instantiated e Unifying the atom with the head of the renamed statement e Composing the mgu of the atom and the head of the statement with the current answer substi tution to return the new answer substitution Each of these four operations is potentially very expensive when we are dealing with the explicit representation of substitutions therefore it is vital that they are handled in as efficient manner as possible The implementation of Resolve is designed to meet this need by being both as efficient as possible and capable of being highly specialised by SAGE In the previous section we demonstrated how the module SLD would be specialised wrt an ob ject program such as Append In the specialisation of this module assuming that the predicate Solve were marked as unsafe we see that SAGE would determine that a specialisation of the atom Solve lt Append gt g v vi s s1 should be performed where lt Append gt is the representation of the object program Append As the object program is known in the call to S
36. redicate FilterList to replace the call to Filter with a conditional formula as follows FilterList D FilterList x rest list lt IF xzA THEN FilterList rest list ELSE list x listi amp FilterList rest listi or alternatively as follows 4 SPECIALISING GODEL PROGRAMS 11 FilterList FilterList x rest list lt IF x A THEN list listi ELSE list xllist1 amp FilterList rest listi Of these two alternatives we comment that the second is preferable as the recursive call to FilterList only appears once in the second statement A general rule of thumb is that the then_part and else_part of conditionals used in this way should be kept simple wherever possible When this second alternative definition is specialised wrt the goal lt FilterList x y z list SAGE will produce the following new definition FilterList x y z list lt IF xrA THEN list listi ELSE list xllist1 amp IF y A THEN listi list2 ELSE listi yllist2 a IF z A THEN list2 ELSE list2 z is 4 Specialising Godel Programs In this section we give an overview of the extensions to the definition of partial evaluation in 7 which permit the specialisation of G del programs containing logical connectives in addition to amp conditional formulas commit operators and set terms 4 1 Quantifiers and Connectives Unfolding formulas of the form A lt B A gt B and A lt gt
37. s and Transformation Springer Verlag July 1993 C A Gurr A Self Applicable Partial Evaluator for the Logic Programming Language Goedel Extended Abstract Technical Report Draft Human Communication Research Centre University of Edinburgh 1994 CA Gurr A Self Applicable Partial Evaluator for the Logic Programming Language Godel PhD thesis Department of Computer Science University of Bristol January 1994 P M Hill and J W Lloyd The G del Programming Language Technical Report CSTR 92 27 Department of Computer Science University of Bristol 1992 Revised May 1993 To be published by MIT Press P M Hill J W Lloyd and J C Shepherdson Properties of a pruning operator Journal of Logic and Computation 1 1 99 143 1990 J W Lloyd and J C Shepherdson Partial evaluation in logic programming Journal of Logic Programming 11 217 242 1991
38. t processing consist of open code The system module Syntax being the only open system module in the Bristol G del deserves particular care when specialised Much of the code in Syntax is already as efficient as we would wish and should not be specialised Those predicates we would wish to specialised are Resolve ResolveAll and the data type predicates EmptyTermSubst And Or Not and so on The approach taken in the current implementation of SAGE is to treat Syntax as a closed module for all predicates other than Resolve and ResolveAll This approach means that the predicates EmptyTermSubst And Or Not will always be unfolded as they have no delay declarations When a user wishes to specialise a meta program SAGE will ask if the WAM like predicates are to be marked non selectable In general the user should answer yes to this question as this assists SAGE in specialising the ground representation by specialising calls to Resolve This specialisation is described in more detail below for the module Solve Of the two pre processing calls and the single post processing call we see that SAGE will unfold the call EmptyTermSubst but not the calls StandardiseFormula and ApplySubstToFormula as these latter two calls do not match their delay declarations To end our illustration of the partial evaluation of the module SLD we give the specialised definition of the predicate Demo specialised wrt the object program Append Figure 3
39. ting predicate dependency graph done Performing static analysis done Performing partial evaluation done Optimising residual code done Writing script in file Append scr done Script Append scr Partial evaluation of program Append wrt goal MyAppend x y 1 2 3 The following atoms were partially evaluated MyAppend x y 1 2 3 No predicates were marked non selectable No predicates were marked unsafe The following new predicates have been defined Predicate MyAppend 3 defined in module Append has been replaced by PREDICATE MyAppend 1 List Integer List Integer as if re defined by the statement MyAppend v v_1 1 2 3 lt MyAppend_1 v v_1 These changes have been recorded in the file Append new Do you wish SAGE to perform another partial evaluation Y N n Goodbye Yes SAGE lt quit unix Figure 1 gives the specialised code produced by SAGE following this run MyAppend 1 1 2 3D MyAppend_1 1 2 3 MyAppend_1 1 2 3 MyAppend_1 1 2 3 Figure 1 Specialised Code for Predicate MyAppend The specialised version of the Append program has been written to the file Append scr This file may be compiled into executable code using the sc command script compile in the G del environment as the following listing demonstrates unix goedel Goedel 1 3 Type h for help 3 A GUIDE TO USING SAGE lt sc Append Compiling script Append Module Append compil
40. tion by unfolding was put on a firm theoretical footing by Lloyd and Shepherdson in 7 and we refer to that paper for a formal definition of partial evaluation as used by SAGE In this section we give first a brief outline of the concept of partial evaluation by finite unfolding and then describe some issues in the application of this technique which relate to the G del language and to the SAGE partial evaluator in particular 2 1 Partial Evaluation by Finite Unfolding In the context of 7 the basic technique for partially evaluating a program P wrt a goal G is to construct partial search trees for P with suitably chosen atoms from G as goals and then extract the specialised program P from the definitions associated with the leaves of these trees For example let P be the following partial program P x lt Q x y amp ROY P x lt S x Q x A lt T x Q x B lt T F x R A R B and lt P x the goal we wish to partially evaluate P wrt We would therefore construct a partial SLDNF tree for this program wrt the singleton set P x The following is one possible such tree lt P x lt Q x y amp ROY lt S x lt Q x A lt Q x B lt T x lt T F x We next extract new statements for the predicate P from the leaf nodes of this tree giving us the new 2 AN OVERVIEW OF PARTIAL EVALUATION 3 definition P x lt T x P x lt T F x P x lt S x To construct the p
41. to mask off parts of the object program which a user would prefer not to be specialised When specifying the set of non selectable predicates it is necessary to ensure that any predicate which a non selectable predicate depends upon is also non selectable A set of non selectable predicates for which this property holds is said to be well structured In general it is not necessary to mark all predicates which non selectable predicates depend upon as also being non selectable If a particular predicate is depended upon by some non selectable predicate in the program to be partially evaluated we need only mark this particular predicate as non selectable if it is also depended upon by some selectable predicate Note The current implementation of SAGE does not check for well structuredness of the non selectable predicates This property is currently the responsibility of the user 2 3 2 Unsafe Predicates Prior to computing the partial evaluation of an object program and goal SAGE will construct a predicate dependency graph for that goal to identify the recursive selectable predicates which the goal depends upon and then perform a static analysis of the goal wrt the object program The static analysis detects those atoms with recursive predicates which will be encountered in the subsequent partial evaluation The purpose of this analysis is to determine which of these atoms are sufficiently instantiated for them to be unfolded during partial evaluation w
42. ty_substitution amp Solve program goall var _ empty_substitution answer amp ApplySubstToFormula goal1 answer answer goal amp ProgramFormulaToString program module answer goal answer string This module declares the top level predicate Demo for this interpreter Demo has three arguments each of type list which give the name of the object program the body of the object goal and the interpreted answer respectively Using I O predicates in Meta Programs Demo calls the system predicates FindInput GetProgram and MainModuleInProgram to deduce from the string giving the name of an object program the representation of the object program and the name 5 SPECIALISING GODEL META PROGRAMS 15 of its main module Demo then uses this information to deduce the representation of the object goal by using the system predicate StringToProgramFormula Once this goal has been interpreted wrt the object program to return a formula containing the answer substitution Demo converts this formula into a string which may be displayed to the user by calling the system predicate ProgramFormulaToString we shall demonstrate a somewhat more sophisticated way to display an answer substitution with the program Coroutine in Section 5 2 Together these calls perform the I O operations necessary to translate the users choice of object program and goal into the ground representation and to translate the interpreters computed answer back into a string which the
43. ubsequently be specialised further Alternatively the specialised version of Condition will be the disjunction of all the residual resultant bodies of this partial evaluation and the bindings they compute If any of these disjuncts is an empty formula then in at least one case Condition has terminated successfully and bound no free variables In this case we may replace the conditional with the conjunction of the specialised Condition and Formula1 which may subsequently be specialised further Otherwise the specialisation of Condition has not indicated whether Condition will succeed or fail and so Formulal and Formula2 are both par tially evaluated and a new conditional is constructed in which Condition Formulal and Formula are replaced by their specialised versions As for negated formulas these specialised versions of Condition Formula1 and Formula2 are represented in the specialised conditional as calls to new predicates For example suppose that the predicate P was defined as in the above example R x was in all cases the partial evaluation of the atom Q x y and the definition of the predicate S was S x y z lt IF P x THEN Q y z ELSE Q z y 4 SPECIALISING GODEL PROGRAMS 13 then the specialisations of the formulas S A A B S C A B and S x A B would be R A R B and IF Test_0 x THEN Then 1 ELSE Else_2 respectively where the new predicate Test 0 and new propositions Then_1 and Else_2 are defined as Test_O A Test 0 B
44. y and the negation has therefore succeeded If at least one of residual resultants has an empty body and has not bound any variables in the original formula then the negation fails safely otherwise the negations of these resultant bodies and the bindings they compute are conjoined to produce a specialised version of the negation This specialised version of the negation is recorded in the residual script as the definition of a new predicate For example let P be the program P x lt Q x QCA Q B where A B and C are constants The partial evaluations of the formulas P C P A and P x would be the sets True and x A x B respectively where True is the truth proposition The spe cialisations of the formulas P C P A and P x would therefore be True False and Not 0 x respectively where False True and the definition of the new predicate Not O is Not O A Not O B G del also provides a conditional operator of the form IF Condition THEN Formulal ELSE Formula2 which is defined to mean Condition amp Formula1 Condition amp Formula2 and is used to avoid the need to compute the formula Condition twice We use constructive negation in the specialisation of this operator in the following manner First a partial evaluation of Condition is computed If there are no residual resultants for this partial evaluation then Condition has failed finitely and the conditional is replaced by Formula2 which may s
Download Pdf Manuals
Related Search