Some Rules For The Automatic Synthesis Of Programs
Proceedings of the Fourth International Joint Conference on Artificial Intelligence. Learning Debugging And Automatic Programming. Pages 232-238.
© 1975 International Joint Conferences on Artificial Intelligence
Abstract
A set of rules (or facts) about program synthesis is presented. The rules are about the process of programming, and are sufficient for the synthesis of an insertion sort program. The use of the rules to write a short LISP program is described. Taken together, the rules are an embodiment of a detailed theory which explains one small part of the programming process. The size of the set of rules suggests the complexity of the process of writing programs and indicates that much work will be required to codify significant amounts of programming knowledge as a step toward the development of program-understanding systems.
- Green, Cordell, and Barstow, David. A Hypothetical Dialogue Exhibiting a Knowledge Base for a Program- Understanding System, presented at the NATO Advanced Study Institute on Machine Representations of Knowledge, Santa Cruz, California, July 1975.
References were extracted automatically from the PDF and may contain errors.
Full text extracted automatically from the PDF; figures, tables and equations may differ. The PDF is the version of record.
SOME RULES FOR THE AUTOMATIC SYNTHESIS OF PROGRAMS
Cordell Green and David Barstow Stanford Artificial Intelligence laboratory Stanford, California USA
mind. We hope to correct these omiss1ons by expanding this rule set in the future. A real likelihood with this "skeletal" approach is that the framework provided by this initial set of rules may well need remodeling to accommodate further pro~ramming knowledge. The only overall framework presented in this paper, that of an iterative transfer program, will perhaps not be the reader's (or the eventual user's) favorite way to view the synthesis of a sort proeram. OlhP.r weaknesses are that the rules do not allow enough "planning" activity (resulting in a rather rigid sequence that rnusl be followed), and .that · a few rules probably have too much specialized knowled~;e. It is also important to note that the rules are currently designed for s-vnrl.nis and would require modification (or else a different set of rules) in order to anai."Ft or modify existing programs. Our omission of conventional inference ability is intentional, since we feel that the stale of the art in the area is well ahead of the stale of any theory about the process of programming. However, it is clear that in a more general program-underslanaing system inference plays a part in selecting applicable rules and in putting the pieces of a program together in any non-preconceived order.
OVERVIEW
To provide a context within which the rules can be easily understood, we present here a short desctiption of the tarect insertion sort program. The complete program produced by our rules appears in the section giving an example application of the rules, and the reader may wish to refer to it now.
tr;msfer pro&ram: initializer: initiali:e th.e generator and the output list; body: repe.:it until finished; termination test: if there are no elements left in the input list then finished; so lector: gen e r~te the next element; increment the state of the generator; con~tructor: position-finder: find the position in the output list for the generated element; element-adder: add the generated element in the po s i lion founcl;
rrpca t.
The program is basically a loop with three parts: a termination test which tests whether all of the elements in the input list have been generated; a selector which generates the next element in a first to last order and saves its computational state; and a constructor which finds the position in the output list for the element and then adds it at that position. Thus, the program takes each of the elements from the input list (in first to last order) and builds up the output list by inserting these (one at a time) into their appropriate places.
Note that the program is basically iterative rather than recursive. This is primarily a reflection of our feeling that significant aspects of the algorithm are hidden by a recursive call. In many real applications, programmers must deal with the notion of generating elements sequentially, and of saving the state of a computation, so we have chosen to look at these explicitly.
ABSTRACT
A set of rules (or facts) about program synthesis is presented. The rules are about the process of programming, and are sufficient for the synthesis of an insertion sort program. The use of the rules to write a short LISP program is described. Taken together, the rules are an embodiment of a detailed theory which explains one small part of the programming process. The size of the set of rules suggests the complexity of the process of writing programs and indicates that much work will be required to codify significant amounts of programming knowledge as a step toward the development of program-understanding systems.
INTRODUCTION
This paper may be viewed as a sequel to an earlier paper [I), in which we tried to exhibit the knowledge required by a computer system in order to synthesize a simple insertion. sort program. In this paper, we present the results of an attempt to codify that knowledge in the form of an (Xf'licit system of rules. Although there are other ways in which this knowledge might be available to a computer system (e.g., derivable through some kind of inference applied to more general knowledge), the rules presented here seem to express the information used in the process of writing one simple program. As such, the rules constitute one detailed part of a thtory of programming. A more complete theory could provide the basis for a knowledge-based program-understanding system
The rules presented here are about the proem of programming, rather than about program semantics. Thus one of the rules states that one method of generating all elements in a stored set is to first select a method for saving the state of the generator, then write the body, then . the initializer, and so on. Additional rules elaborate how to achieve each subgoal. The subjects of this set of rules include the synthesis of transfer programs (in which the elements of one ordered set are transferred and possibly re-ordered into a new ordered set), generators of elements and positions in ordered sets, constructors of sets, search strategies, tests for correctness of a position, etc. Also included are the lower-level programming rules (for the LISP language) that are necessary to actually code the program. The complete set of rules has in fact been used to synthesize the intended program in an implementation which is basically a rule-testing system. This implementation is described at the end of the paper.
It may seem strange that so many rules are used for one simple program. The number and complexity of these rules has resulted from a desire to adequately reflect the amount of knowledge needed for this particular synthesis and from an effort to minimize the amount of remodeling required to add more knowledge.
Despite our desires and intentions, however, there are several shortcomings of the rules and we would like to make some disclaimers. The most obvious limitation is the amount of higher-level programming knowledge which is not included,,e.g., more complex search strategies (such as binary chop), other state-saving schemes (such as the overwriting of elements), and other knowledge necessary for more efficient sort programs. The reader will usually find only one method explicated when many more come to We will now give an overview of how these rules would be used to synthesize this program.
- O: As stated in the introduction, we will assume that the system has already decided to use a transja t·rngram as the basic paradigm. A transfer program consists of two parts, the sdrctor, which enumerates elements from the input set, and the constrrtctor, which places these elements in the output set. This transfer program is an instance of a gnwatr and process par;~rliem, in which the selector is the generator and the constructor is the process.
- 1: The system decides to write a insertion sort rather than an ;elution sou program. (An insertion sort removes the clements from the input in first to last order and inserts each into its correct place in the output such that after each step the output set is ordered; by contrast, a selection sort removes the largest element from the input and adds it onto the front of the output; the rules presented here only consider the case of insertion sort programs.)
- 2: The selector for the transfer program is written .. First a pointer into the input list is chosen as the method for saving the state of the selector between calls to it . Then the sdtctor body (consisting of code to generate the element and code to increment the pointer) is synthesized. Finally the selector inilialiur and the sduror J·rc-tt'St (a test which the transfer program can apply to determine whether there are any more elements to be generated) are written.
- 3: Work on the output conslruelor is begun. First it is decided that the new set will be built up by list inwtion. Then, noticing that the elements arrive not necessarily in increasing (or decreasing) order, the system decides that it needs a somewhat complex constructor that must search for the position to insert each element. It chooses a pair of pointers into the list to represent that position.
- 4: Now the position finda is synthesized. This requires choosing a search stratrgy for finding the correct position, and a method for representing the state of the search. Once these have been chosen, the loop which finds the correct position is written: this includes writing an initia/iur, a position tester, and an ino nnrntrr.
- 5: Now the element inserter is written. It requires a special case for inserting at the front of the list. The position finder and element inserter together constitute the constructor body.
- 6: To complete the output constructor, the system writes the constructor initialiw which initializes the output set to the empty list.
THE RULE SYSTEMS
As an aid in understanding the rules, let us point out that they are grouped into structured systems of rules, each system dealing with a different aspect of the process of writing a transfer program. As will become apparent, there is a simple hierarchical structure to the rule systems. This, we feel, is a reflection of the nature of the task: some goals require other goals to be satisfied, hence some rules call others as sub-rules. However, a strict hierarchy is certainly unnecessary.for example, in the process of writing a non-linear generator, the generator rule is called again, in order to write the code to generate the elements linearly for use in the comparison.
We wish to point out that, in the rules presented here, wherever a choice is indicated, only one alternative is actually provided. When we have extended the rules to enable the synthesis of a large class of programs, most of these rules will contain several options. Choices between them could be made either by using additional rules dealing with efficiency or by leaving such choices up to the user. But the important point here is that the notion of "understanding" seems to carry with it an awareness of possible alternatives.
The Rule system for Transfer Program
There is one transfer program rule:
TI: In order to write a transfer program, the following four sub-tasks must be achieved:
- ( 1) select a transfer rt-ordtring
- write a stltetor, which will include a body, initializer, and pre-test;
- write a constructor, which will include a body, and an initializer .
- put the selector and constructor together into a gn1natf and proem paradigm with the selector pre-test used as the termination lest and applied just before the call to the selector body
The meanings of most parts of this rule are relatively obvious, and we shall delay the detailed explanation of each of its sub-tasks until we discuss the rules for achieving those sub-task.
The first choice which must be made in the process of writing a transfer program is to choose the pattern of re ordering to be used by the program. The input to the transfer program we will call the soww and the output we will call the rargtt. As part of the transfer process, there will be some overall re-ordering from the positional ordering of the source (initial order) to the positional ordering of the target (final order). There is also an intermediate ordering: the temporal ordering of the elements as they are transferred (transja ordtr). Corresponding to these three orderings, there are relationships between them. We shall discuss these relationships as functions from one order to the next order, i.e. rc-ordaings or permutations. The orderings and re orderings are shown in the diagram The transfa re-c·rdrring is the main re-ordering_ accomplished by the transfer program. This re-ordering is part of the top-level specification of the program, presumably furnished by the user or a higher-level program. An example of a transfer re-ordering specification for a "reverse" program is "final order is converse of initial order". In our paradigm, we factor this re-ordering into two re-orderings, the selection re-ordering and the constntction rt-ordering. Accordingly the transfer program is also factored into two sub-programs, the seltctor and the constmctor which perform these re-orderings.

The rules consider four possible re-ordering operations:
- SAME: makes a copy with the identical ordering.
- CONVERSE: reverses an ordered set.
- BASED ON COMPARISON PREDICATE: the re-ordered set
- is such that one element precedes another if and only if the comparison predicate (supplied by the user) applied to these elements is true. The order of the re-ordered set is independent of the initial order (except in the case where two elements have equal keys).
- BASED ON EVALUATION FUNCTION: the re-ordered set is such that one element precedes another if and only if the value of the first element is less than the the value of the second, where the values are the results of applying the evaluation function (supplied by the user). The order of the re-ordered set is independent of the initial order. (Although this is actually a special case of 3, we include it since people seem to use it frequently.)
It is convenient to classify the first two re-orderings as lintar since the programs to accomplish these are simple and are treated as special cases.
In addition to the transfer program rule given above, there is a set of transfer re-ordering rules which guide the choice of selection re-orderings and construction re orderings. Their effect is to constrain the choices for the two re-orderings to be such that their composition will yield the transfer re-ordering. An example of such a rule is: if we are writing a "reverse" program and the selection re-ordering is SAME, then the construction re-ordering must be CONVERSE. The normal case in a sort program is that either !he selector or the constructor will do the bulk of the work of the total re-ordering, and that the other will perform only a simple (linear) re-ordering (either SAME or CONVERSE). The transfer re-ordering rules are straightforward but lengthy, so we shall not present them here.
The Rule system for Selector
In considering the rule system for a stlcaor, we first observe that a selector is a special kind of grnrrc1tor. That is, a selector is required to generate exactly the elements of the source set, once and only once, and in a particular order <the order discussed earlier as the transfer order). Perhaps the most important aspect of any generator is that, relative to the program which uses it, it is essentially a process or co-routine; that is, between calls to it, it must somehow "remember" which elements have been generated and which have not, in order to guarantee generating all elements one time each. This "remembering" must be part of what is performed by the body of the generator, in addition to "generating" the next element.
Also, there must be some way of determining when the generator is finished, that is, when each element in the source !Jet has been generated and none remain. In the generators for which our rules are intended, this will be done by using a f>r(-(rst which the calling program guarantees to apply before each call to the generator (for example, a test whether a pointer points to the empty list.) This is the test which the transfer program will use to decide when to stop transferring. Finally, there must be some way of initializing the generator prior to its first call. From this discussion, we can see that the rule system for the selector (generator) must produce three separate sections of code: the main body, the pre-test, and the initializer.
It is also worth noting that the generator must know the manner in which the generated element should be given to the caller. In the case of our. rules, we consider only the case of setting some global variable to a particular value, either the element itself or a pointer to the sublist beginning with that element.
- s 1: In order to write a selector, one of the following sub-tasks must be achieved:
- (I) write a gtnrrator with the productiOll order the same as the selection re-ordering, and constrain the generator to be TOTAL
- 52: In order to write a generator, the following four sub-tasks must be achieved:
- ( 1) select a state-saving scheme tor the generator
- write the generator body, based on the state saving scheme
- write the generator initialiur, based on the state saving scheme
- ( 4) write the gmerator pre-test, based on the state saving scheme
Note that the first sub-task of this rule is the selection of a state-saving scheme for the generator. This state saving scheme will be essentially a specification of some plan about how to do the "remembering" discussed above. There are many possible schemes which will perform adequately (e.g., bit strings, property list marks, hash table entries), but there are certain common characteristics. Each scheme includes some way of looking at a particular description of the state of the generator and knowing (or deducing) which elements of the set have been generated. Additionally, each scheme includes some way of incrementing the state after the appropriate element has been produced. Also implicit in any such scheme must be some way of determining (from a state description) whether any elements remain to be generated.
The choice of state-saving scheme depends upon the representation of the set, the order of enumeration, and whether destructive operations are allowed. For the case we are considering, the enumeration of the elements in a list requires only one variable, which points into the list. In this standard enumeration scheme, the pointer always points to the sublist beginning with the next element to be generated and is bumped by one more list cell each time a new element is required. We will refer to this scheme as POINTER INTO SOURCE and to the pointer as POINTER. The rule may be written as:
GSI: In order to select a state-saving scheme for a generator:
(I) if a non-destructive state-saving scheme is desired, the source-set is represented as a linked list, and the production re-ordering is SAME, then use POINTER INTO SOURCE
For a simple linked-list, forward scanning generator, the part of the program that finds the next element and the part of the program that increments the state communicate very simply through one pointer, the pointer used for the state representation. With more complex state-saving schemes, additional variables may be required to communicate between these two subprograms. For example, with a destructive, element-deleting scheme, the !>late is represented by one pointer to the front of the list, but in addition another pointer (indicating which element is to be deleted) must be passed from the element finder (which finds the element) to the state incrementer (which deletes that element). The following rule is thus a minor simplification.
- 53: In order to write the generator body, the following three 5ub-tasks must be achieved:
- (I) write the part of the body which produces the element to be generated
- write the part of the body which increments the state of the generator
- put these two parts together into a sequential block
Two ways in which a generator can report an element to its caller are (I) by a pointer to the sublist beginning with that element and (2) by a pointer to the element it self. These two rlcmrnr rrprncnrarions we call SUBLIST and ITEM respectively. (Actually, the transfer program rule, TJ, needed to specify the ITEM representation, so that the selector and constructor could communicate.)
- 54: In order to write the part of the body which produces the element to be generated, the following two sub-tasks must be achieved:
- (I) write an expression which has as its value the element to be generated
- write a statement which assigns this value to the variable which should hold the element to be generated
- 55: In order to write an expression which has as its value the element to be generated:
- (I) if the generator slate-saving scheme is POINTER INTO SOURCE, then write an expression which has as its value the element representation of the first element in the list pointed to by POINTER
- 56: In order to write an expression which has as its value the element representation of the first element in a list:
- (I) if the element representation is ITEM, then write an expression which has as its value the first element of the list pointed to by POINTER
Note that 55 considers which element to produce and 56 considers how to represent it.
- 57: In order to write the part of the body which increments the state of the generator:
- (I) if the generator state-saving scheme is POINTER INTO SOURCE, then write a statement which increments POINTER
- 58: In order to write the generator initializer:
- (I) if the generator is constrained to be TOTAL, then write code which initializes · the state to the entire source
- 59: In order to write code which initializes the state of the g.enerator to the entire source:
- (I) if the generator state-saving scheme is POINTER INTO SOURCE, then write a statement which assigns the source to POINTER
- s 1 O: In order to write the generator pre-lest:
- (I) if the generator is constrained to be TOTAL, then write a statement which tests whether all of the elements have been generated
- Sll: In order to write a statement which tests whether all of the elements have been generated:
- (I) if the generator state-saving scheme is POINTER INTO SOURCE, then write a statement which tests whether POINTER points to the end of a list
The Rule !,;ystem fo1· Constl·uotol'
A consrr uaor builds a new ordered set in accordance with the construction re-ordering. The constructor rules given here synthesize a constructor which operates inductively; that is, the new set is initially empty and after each element has been added, the resulting subset satisfies the re-ordering relation. The constructor has a <'MlSir rtrror initia/iu r, which makes the new set initially empty, and a consrrurr"'· body. The main body first finds the correct position for the new element and then inserts the element.
- Cl: In order to write a constructor, one of the following sub-tasks must be achieved:
- (I) write an iruluctiz'r constwctor with the construction orda the same as the construction re-ordering; the target should be INITIAllY EMPTY
- C2: In order to write an inductive constructor, the following three -!lub-tasks must be achieved:
- (I) select a constntction method for the constructor
- ( 2) write the constructor body, based on the construction method
- write the constructor initia/izer, based on the construction method
The rule for selecting a construction method is very simple:
CMI: In order to select a construction method:
- (I) if the set being constructed is represented as a linked list, then use LIST INSERTION
Although there are several ways to do this operation, our use of the term "list insertion" refers to the commonly used method in which the "cdr" of the list cell preceding the desired position is destructively modified to point to a newly created cell which is in turn linked back to the rest of the list. Note that this technique requires saving a pointer to the list cell preceding the position and it also requires special treatment at the front of the list.
We will classify list insertion as being indrprndrnt, meaning that the code which finds the position where the new element belongs and the code which adds the new element at that position are independent and may be written as separate pieces of code. [If the construction method were, say, array shifting, then this independence would no longer hold.)
C3: In order to write the constructor body:
- (I) if the construction method has the property "independent", then achieve all of the following sub tasks:
- ( 1.1) select a method for representing the desired position
- ( 1.2) write the part of the body which finds the position in which the new element belongs
- ( 1.3) write the part of the body which adds the new element at this position
- (I .4) put these two parts together into a sequential block
The position finder and the element adder both require that a method be specified for representing the position at which the new element will be added. For example, in an array, the index of the correct position is an adequate representation. For lists, one or two pointers into the list are convenient position representations.
The rule we shall use for selecting a position representation is:
PRI: In order to select a position representation:
- (I) if the set being constructed is represented as a linked list and the construction method is LIST INSERTION, then use TWO POINTERS (which will point to the list cells before and after the point where the new cell will be added)
Pictorially, this position representation looks like this:

This representation has a special case for the front of a list: the "before" pointer will have as its value a unique string constant, say, "FRONT". For the end of the list, the "after" pointer will point to NIL. We will refer to the two variables involved as BEFORE and AFTER.
Note that this position representation is more than adequate for the list insertion method used, since it maintains not only a pointer to the previous cell in the list, but also a pointer to the succeeding cell in the list. The second pointer will be used by the correctness test. This representation leads to a relatively simple algorithm.
The selection of this rule and the corresponding construction method is pretty obviously a cheat, since the rules should first do some planning, i.e., notice that later parts of the program would have profited from the two pointer representation. An alternative to a planning technique would have been some later simplification or Optimization of the program.
C4: In order to write the part of the body which finds the position in which the new element belongs:
- (I) if the construction order is not "linear", then write a position _firrdn which guarantees success (discussed later before rule PI); it must find the desired position according to the construction order, and specify it according to the position representation
In a similar manner to the selector, a linear construction re-ordering would mean that the position is already implicit in the state, say an index moving linearly through an array, and need not be recomputed. In the remaining rules, rather than saying "an ordered set represented as a linked list· we will use the term "list". '
CS: In order to write the part of the body which adds the element at the position:
- ( 1) if the posit.ion representation has a special case for the front of the list and the construction method has a special case for the front of the list, then achieve all of the following sub-tasks:
- ( 1.1) write a statement which tests whether the position (which has already been found) occurs at the front of the list
- ( 1.2) write a statement which adds the element onto the front of the list
- ( 1.3) write a statement which inserts the element into the list at the position specified (assuming the position is not at the front)
- ( 1.4) put these three pieces together into a conditional expression C6: In order to write a statement which tests whether the position is at the front of the list:
- ( 1) if the position representation is TWO POINTERS, then write a statement which tests whether BEFORE is equal to the special string constant "FRONT"
- C7: In order to write a statement which adds the element onto the front of the list:
- ( 1) if the construction method is LIST INSERTION then write a statement which destructively add~ the element onto the front of the list
- C8: In order to write a statement which inserts the element into the middle of the list:
- (I)· if the construction method is LIST INSERTION then write a statement which destructively insert~ the element into the middle of the list
- C9: In order to write a statement which destructively inserts the element into the middle of the list:
- (I) if the position representation is TWO POINTERS then write a statement which destructively inserts th~ element between two pointers
- CIO: In order to write the constructor initializer:
- (I) if the target is specified to be INITIALLY EMPTY, then write code which initializes the target to an · empty list
Cll: In order to write code which initializes the target to an empty list:
- ( 1) if the construction method is LIST INSERTION, then write a statement which assigns the empty list to the target
The Rule system for Position Finder
The J·Mition firrda looks through the available positions in the set being constructed and finds the correct position at which to insert the new element. The position finder can be thought of as a total generator that generates each position and tests whether the position is correct. A srarch stmtcgy is required to determine the order of enumeration of positions. A srarch-statt saving schemt is used to remember the state of the search. A con-cctnrss ttst is synthesized to test whether the proposed position results in an ordered set. Each position must be represented according to the earlier specified position representation, so some code may be required to translate from the search state representation into the position representation.
The reader may wonder why the position finder rules do not call the high level generator rules discussed in the selector section. Instead a slightly different type of generator is effectively entailed by these position finder rules. In other versions we have the position finder call the existing generator rules. For clarity we present separate rules here for the position finder, although we feel that it is conceptually better to combine the two into a unifying paradigm.
The position finder was constrained by the constructor to be one that guarantees success, i.e., it must find a correct position or else the inductive constructor won't work. Structurally, this means there is no failure branch for the position finder.
PI: In order to write a position finder that guarantees success, the following five sub-tasks must be achieved:
- (I) select a mnch stratrgy that guarantees success
- select a uarcl>-statt sat,ing schtmt tor the position finder, based on the search strategy
- write the positiorr fi~~<lrr body, based on the search strategy and the search-state saving scheme
- write the J·ositiorr fintlcr initia/i;:a, based on the search strategy and the search-state saving scheme
- put the last two together into a sequential block
The selection of a search strategy that guarantees success consists of lots of checking followed by the selection of a simple forward linear scan.
- SSI: To choose a search strategy that guarantees success, one technique is:
- (I) check that a correct position exists
- select a total search strategy
- SS2: To check that a correct position exists, one technique is to check these conditions:
- (I) if the correctness criteria is based on a comparison predicate (an ordering relation):
- (1 .1) the ordering relation is transitive
- ( 1.2) the set being scanned is ordered
- SS3: To select a total search strategy:
- (I) if the search list is represented as a linked list, then use FORWARD LINEAR SCAN for the search strategy
We will speak of this search strategy as being indt'f·nl<ifnr, meaning that the part which finds the position and the part which tests it for correctness are independent of each other [as opposed to the case with a binary chop).
The search for a position requires a slate-saving mechanism, just as did the earlier kind of generator. The slate-saving scheme given by our rule will be TWO POINTERS, pointing respectively before and after the current position. Recall that this is the same as the position representation. The rule first checks some conditions to see if a two pointer scheme is adequate. Next it notes that since the position representation and the search stale representation are the same, they will be combined and the stale representation will be said to mbJWitt the position representation. Finally, the variables used for the position representation become the variables used for the search state representation.
sss 1: To select a position finder search-state sa vine scheme:
- (I) if a non-destructive scheme is all right, a "linear" strategy is being used, and the search list is represented as a linked list, then:
- (I . I) a two pointer stale representation will work
- (I .2) note that the position representation is subsumed by the search state representation
- (I .3) if the position representation includes a "before" pointer, then that is superceded by the stale's "before" pointer
- (I .4) if the position representation includes an "after" pointer, then that is superceded by the stale's "after" pointer
We note that this rule ·is something of a cheat in that again, some planning should be required to select such ~ good and optimizing state representation. This rule is a good example of trying to embody knowledge in a form too specific to a particular slate or position representation. More reasonable would be a general rule giving a preference for using one variable instead of two when they would perform similar functions.
P2: In order to write the position finder body:
- (I) if the search strategy is "independent", then achieve all of the following sub-tasks:
- ().1) write the part of the body which translates from the representation of the stale of the search into the representation of the current position
- (I .2) write the part of the body which tests whether the determined position is correct according to the criteria for acceptance
- ( 1.3) write the pari of the body which increments the slate of the search
- ( 1.4) write the part of the body which tests whether there are no positions left, thus indicating failure to find the desired position
- (I .5) put the pieces together into a loop
The fact that the position representation is subsumed by the search state means that at any point in the search, the next position to be tested is completely specified by the search-state representation, i.e., absolutely no work must be done in order to specify the position to be tested, given the stale of the search. This is reflected in the next rule.
P3: In order to write the part of the body which translates from the representation of the slate of the search into the current position:
- (I) if the position representation is subsumed by the search-slate scheme, then there is nothing left to do to determine the position to be tested
The next five rules, P4 through P8, represent a chain of simplifications of the test that the position is correct, i.e., the new set is ordered. The chain proceeds from testing the new clement against each other element to checking against only one. This situation may occur frequently enough that one special case rule should be used.
P4: In order to write the part of the body which tests whether the determined position is correct according to the criteria for acceptance:
- (I) if the criteria is based upon a comparison predicate, then achieve all of the following sub-tasks:
- ( 1.1) write a statement which tests the new element against all of the elements preceding the determined position
- ( 1.2) write a statement which tests the new element against all of the elements following the determined position
- ( 1.3) if either statement is vacuous, then return only the other; otherwise, combine the two tests into a conjunction
- P5: In order to write a statement which tests an element against all of the elements preceding the determined position:
- (I) if the comparison predicate is transitive, and the search strategy is FORWARD LINEAR SCAN, then there is nothing left to do to test the element against all of the elements preceding the determined position
- P6: In order to write a statement which tests an element against all of the elements following the determined position, the following three sub-tasks must be achieved:
- (I) write a statement which tests whether there are no more elements after the determined position
- write a statement which tests the new element against all of the elements following the determined position, assuming there is at least one such element
- combine these two tests into an ordered disjunction
- P7 : In order to write a statement which tests whether there are no more elements after a position:
- (I) if the position representation is TWO POINTERS, then write a statement which tests whether AFTER points to the end of a list
- P8: In order to write a statement which tests an element against all of the elements following a position, assuming there is at least one:
- (I) if the comparison predicate is transitive and the search list is ordered, then write a statement which tests the clement against the immediately following element
The rest of the rules are more or less self-explanatory. P9: In order to write a statement which tests an element against the immediately following element, the following two sub-tasks must be achieved:
- (I) write an expression which has as its value the first element after the position
- write a statement which applies the comparison predicate to the new element and the expression just written
- PIO: In order to write a statement which has as its value the first element after a position:
- (I) if the position representation is TWO POINTERS, then write a statement which has as its value the first element of the list pointed to by AFTER
- PII: In order to write the part of the body which increments the state of the search:
- (I) if the search strategy is FORWARD LINEAR SCAN, then write a statement which increments the search state to the next following position
Pl2: In order to write a statement which increments the search state to the next following position:
- (I) if the search-state saving scheme is TWO POINTERS, then achieve all of the following sub-tasks:
- ( 1.1) write a statement which assigns to BEFORE the value of AFTER
- ( 1.2) write a statement which increments AFTER
- ( 1.3) combine these two into a sequential block
Note that this incrementing technique works both for the special case where BEFORE has the special value "FRONT" and for the general case where BEFORE points into the output list.
P13: In order to write the part of the body which tests whether there are no positions left:
- (I) if the position finder guarantees success, then this part is unnecessary
Pl4: In order to write the position finder initializer:
(1) if the search strategy is FORWARD LINEAR SCAN, then write a statement which initializes the search state to the first position in the search list
PIS: In order to write a statement which initializes the search state to the first position in a list:
- if the search representation is TWO POINTERS, then achieve all of the following sub-tasks:
- ( 1.1) write a statement which assigns to BEFORE the string constant "FRONT"
- ( 1.2) write a statement which assigns to AFTER the search list
- ( 1.3) combine these into a sequential block
The Rules for LISP Statements
The rules given here are included only for completeness. They embody the LISP knowledge necessary for the insertion sort program.
Ll: In order to write an expression which has as its value the first element of a list, return the list: <CAR [1 ist name))
L2: In order to write a statement which assigns a value to a variable, return the list:
<SETQ [va r 1 able name] [value) l
L3: In order to write a statement which increments a pointer, return the list:
(SETQ [pointer name) <CDR [pointer name]))
L4: In order to write a statement which tests whether a pointer points to the end of a list, return the list: C'4ULI. [pointer name)>
L5: In order to write a statement which tests whether a variable is equal to a string constant, return the list: (EQUAL [variable name) [string constant) l L6: In order to write a statement which destructively adds an element onto the front of a list, return the list:
<SETQ [1 ist name) cco~s [element name) !list name)))
L7: In order to write a statement which destructively inserts an element between two pointers, return the list:
<RrLACD ["before" pointer name) <COi\S [element name) ("after" pointer name)))
L8: In order to write a statement which assigns the empty list to a variable, return the list:
<SETQ [variable name) 1\IL)
L9: In order to combine two tests into an ordered disjunction, return the list:
<OR [first test) [second test])
uo: In order to apply a function to a list of arguments, return the list:
<[function name) ··· arguments ··· )
AN EXAMPLE
We now present an example of the use of the rules. We will look in detail at steps I and 2 of the overview presented earlier.
Let INPUT be the name of the source list and let OUTPUT be the name of the target list. Let ELEMENT be the variabl0. name chosen to do the communicating between the selector and constructor. We will suppose that the final order is BASED ON COMPARISON PREDICATE, with GREATERP as the comparison predicate. We assume that the system has already dccide>d to write a transfer program. That is, rule T 1 has been invoked.
Step 1 involved the choice of an insertion sort rather than a selection sort . If we consider what the possible lcoitimutc combinations of selection re-orderin~ and co~struction re-ordering are, we note that using SAME for the Gelection re-ordering implies that the constructor must do the bulk of the work (i.e., an insertion sort). In fact, the construction re- ordering must then be the same as the final order: BASED ON COMPARISON PREDICATE.
Step 2 involved writing the selector for the · transfer program. That is, rule Sl is invoked by Tl . This. will result in each of the other selector rules being invoked at the appropriate times. The accompanying chart gives a structural diagram of the various ·rule invocations.

In the interests of brevity, we do not go into any further dctnil for the other steps of the overview, except to notP. thnt ~teps 3 through 6 are essentially the results of using the constructor rule system, with 4 being an invocation of the position finder rules. After all of the rules have be·en invoked, the parts of the generate and process paradigm have been filled in. The result is the followine proernm:
(PROG NIL (SETQ REST INPUT) (SETQ OUTPUT NIL) L3 (COND ((NULL REST) (.GO L4))) ultctor initializtr constructor initializtr ulector pre-test (S ETQ ELEMENT <CAR REST) )I stltctor body (SETQ REST (CDR REST)) (SETQ BEFORE "FRONT") (SETQ AFTER OUTPUT) Ll (COND ((OR (NULL AFTER) constructor body (GREATERP ELEMENT (CAR AFTER))) (GO L2))) (SETQ BEFORE AFTER) (SETQ AFTER <CDR AFTER)) (GO L 1) L2 (COND ((EQUAL BEFORE "FRONT") (SETQ OUTPUT (CONS ELEMENT OUTPUT))) (T <RPLACD BEFORE <CONS ELEMENT AFTER)))) (GO L3) L4 (RETURN NIL))
Note that J: EST, ['.EFOI\E and AFTER were chosen as new variClble names; nothing in our rules deals with the selection of "reasonable" variable names. Our rules also have no knowledge about the scope of variables.
AN IMPLEMENTATION
The rules given in this paper are an abstraction of some of the rules now operational in a system being developed. We have endeavored to separate out those aspects of the rules which are implementation independent from those aspects which are the results of idiosyncrasies in the implementation. Thus, the rules presented here are not precisely in correspondence to our implementation. We include here a short discussion of our implementation for those who may be curious about it.
The basic mode of operation is to invoke rules by name. Each rule is responsible for determining which rules to invoke to accomplish its sub-goals. The user may be queried for a preference when alternative sub-goals are possible. The invocation by name has two major implications for the system. First, addition of knowledge is not strictly incremental, although the addition of "systems" of rules is generally fairly simple. Second, the system has no sophisticated abilities above and beyond those stemming from the knowlec::lge represented by the rules. In particular, the system has no inference capabilities apart from those implicit in the rules. As the system is primarily a rule-testing device, rather than a sophisticated user oriented system, these defects do not seem critical.
REMARI{S
Having looked at these rules, it is natural to wonder what they can do for us. In regard to their "understanding" ability, it seem!l that they can quite adequately .·xj·lnin the program that they produce. One need merely look at the rule path which produced any part of the final program to underGtand the relationship of that part to the entire program. On the other hand, the rules are clearly unable to anal-,·;-,· or "'(ldif.y the program. It seems plausible that they could be extended to do some rudimentary analysis through Gornc kind of parsing technique. Since the rules presented here are incomplete, in the sense that they do not present various alternatives, they cannot be expected to allow modification. When they have been extended to a broader clnss of prograrns, different specifications will yield different prograrns, and modification would seem to require only slight extensions. This is, however, rnere speculation; further experimentation is required before anything definite can be determined.
One of our original intentions was to determine a set of rules with a wide applicability. We feel that we have done this. We are now in the process of extending these rules into a larger set, capable of synthesizing an entire class of Gorl progrums. If we are successful, then we will have an indication that these rules do indeed have some generality. But more than that, we expect the rules to be useful in many other programming tasks. Set operations (such as intersection and union) seem to involve many of the concepts with which our rules already deal (e.g., generating elements from an ordered set). Another area of potential usefulness seems to be in various kinds of searching and table look-up operations. Obviously the entire set of rules will not be applicable in any one situation, but it seems that for each situation some subset of these rules will be useful.
In regard to such generality, it seems to us that some of the rules may be overly specific to the one particular target progrom, in the ~ense that such rules (or equivalent knowledge) could be derived or inferred from more general principles during synthesis of the program. The choice between these two modes of operation seems to be largely a computational issue: some kind of trade-off between space and time considerations.
At this point it is far too early to prefer one mode to any other, but having explicated the knowledge in some form, we may gauge the requirements of future knowledge-ban~d program-understanding systems. We have seen that i:lbout 50 "rules" are needed for a system to "understand" what is involved in writing even one simple sort program. If we are to design kn~wlrdgr-based j·r~gmm·lilldo si<Piding systo·1s, with the abilities of synthesis, analysis, and modification, applicable to many different kinds of programs, then the body of programming knowledge which will be required is quite large. Our current work indicates that well over a hundred rules will be required to enable the synthesis of a large class of sort programs. It is still too early to estimate the size of the body of programming knowledge which will be necessary for the establishment of reasonable knowledge-based program-understanding systems, but we can at least see that the task of codifying this knowledge is likely to be a long one.
ACKNOWLEDGEMENTS
The <tuthor5 gratefully acknowledee the diligence with which Avra Cohn read the drafts of this paper, and the generosity with which the Artificial lntellicence Center of the Stanford Research Institute provided machine time for the research upon which this paper is based.
@inproceedings{ijcai1975p36,
title = {Some Rules For The Automatic Synthesis Of Programs},
author = {Green, C. Cordell and Barstow, David R.},
booktitle = {Proceedings of the Fourth International Joint Conference on
Artificial Intelligence, {IJCAI-75}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Patrick Winston and Carl Hewitt},
pages = {232--238},
year = {1975},
note = {Learning Debugging And Automatic Programming},
url = {https://ijcai.org/proceedings/1975/36},
}
TY - CPAPER TI - Some Rules For The Automatic Synthesis Of Programs AU - Green, C. Cordell AU - Barstow, David R. T2 - Proceedings of the Fourth International Joint Conference on Artificial Intelligence, IJCAI-75 PB - International Joint Conferences on Artificial Intelligence PY - 1975 SP - 232 EP - 238 UR - https://ijcai.org/proceedings/1975/36 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
Welcome
Future Conferences
AI Journal Division
IJCAI Proceedings
About IJCAI
IJCAI Awards