Divide-and-conquer schema

The Cypress system [Smith 85] is based on a divide-and-conquer schema. Specifications of sub-problems are derived from the adaptation of a schema to the top-level specification, and recursively so on, until primitive problems are reached. This top-down problem reduction is then followed by a bottom-up composition of the synthesized sub-algorithms into the top-level algorithm, according to the schema. The system is interactive, yields totally correct algorithms, and is even able to cope with partial specifications. 

In the area of manual or computer-aided program construction (for experts), [Deville and Burnay 89] and [Deville 87,90] suggest a divide-and-conquer schema. They also discuss interesting transformation schemas, based on (structural or computational) generalization. 

Heuristic synthesis from examples is performed by the systems of [Hardy 75], [Shaw et al. 75], [Siklossy and Sykes 75], and [Biggerstaff 84], in the sense that they fill in the place-holders of a LISP divide-and-conquer schema (see Chapter 8) in a plausible way according to the given examples. 

Second, as we already have hinted when stopping the incremental inference of different versions of a divide-and-conquer schema, version 4 of that schema is far from covering all possible divide-and-conquer logic algorithms. 

In the sub-area of synthesis from incomplete specifications, schemas are often implicitly or explicitly present to guide the synthesis. Early systems based on divide-and-conquer schemas are described by [Shaw et al. 75], [Hardy 75], [Summers 77], and [Biermann and Smith 79]. 

As a conclusion of this survey, it must be observed that almost all of the research has gone into investigating divide-and-conquer schemas. This is not a bad thing, as the covered class of algorithms is very interesting and large. But these published schemas tend to be extremely simplified ones, namely often at best the equivalents of our version 2. In order to be really useful, we think that more sophisticated versions should also be supported. 

The divide-and-conquer strategy was presented as an attractive strategy in Section 8.2, because of its diverse applicability, efficient results, and simplicity of application. The chosen approach for developing a synthesis mechanism is thus stepwise synthesis guided by a divide-and-conquer schema. 

First, regarding the schema underlying the mechanism, we retain version 3 of the divide-and-conquer schema for the theoretical presentation ... 

The objective at Step 2 is to instantiate the predicate-variables Minimal and NonMinimal of the divide-and-conquer schema. This amounts to transforming LA ir) into LA2 r) such that it is covered by the following schema ... 

Heuristic 13-3 From the used divide-and-conquer schema, we know that the parameters of the discriminate are HX, TX, and T, so we should project [Pettorossi and Proietti 89] the discriminants upon these parameters. 

How to discover compound induction parameters Due to our restriction to version 3 of the divide-and-conquer schema. Task A only considers simple induction parameters. Meeting this challenge is thus considered future research. According to what well-founded relation to decompose the induction parameter Step 3 (Synthesis of Decompose) does this non-deterministically by considering all predefined decomposition operators (which each reflect some well-founded relation) of a typed database, and possibly by listening to the specifier s hints. 

Is the mechanism able to design the whole family of possible logic algorithms for a given problem This ability is in theory achieved for the family of algorithms that are covered by version 3 of the divide-and-conquer schema. In practice, everything depends on the completeness of the databases used by Steps 2 and 3. How many structural forms are there Due to our restriction to version 3 of the divide-and-conquer schema. Task C of Step 2 only considers the distinction between two structural forms, namely one minimal form and one non-minimal form. A generalization of this task is considered future research. 

How to detect that recursion is useless in some non-minimal sub-cases Step 4 (Syntactic introduction of the recursive atoms) creates a non-recursive case if at least one example Ej leads to a non-admissible procComp(,,yp atom. Howto invent or re-use appropriate predicates How to implement invented predicates The predicate invention problem is tackled at four points during the synthesis. At Steps 2 and 3, the Database Method re-uses predefined predicates this amounts to using domain knowledge. At Step 6, the Synthesis Method (see Section 14.2.4 below) invents new composition operators. As of now, there is no method yet of re-using common composition operators. At Step 7, the PaP Method synthesizes discriminants that are in terms of predicates other than rfn. How to discover which parameters are auxiliary parameters Due to our restriction to version 3 of the divide-and-conquer schema, auxiliary parameters are not taken into account. See Section 14.2.2 below on how to achieve this. 

The support of any number of minimal or non-minimal forms and of compound induction parameters is considered future research, as considerable extensions to the already defined tasks need to be developed. Note however that Section 5.2.2 shows that single minimal forms and non-minimal forms are more frequent than one might believe at first sight. As outlined in Section 8.4, there is still a lot of space for designing even more sophisticated divide-and-conquer schemas. 

However, version 3 of the divide-and-conquer schema is hardwired into our synthesis mechanism. This results from a hardwired sequence of instantiations of predicate-variables of that schema, as well as from a hardwired mapping between these predicate-variables and the methods of the developed tool-box. Parameterizing the synthesis mechanism on algorithm schemas and tool-boxes would thus be a first step towards supporting schemas reflecting design strategies other than divide-and-conquer. 

In defense of our hardwiring the divide-and-conquer schema, we should however make the following two remarks. First, the hardwired sequence of predicate-variable instantiations is justifiable by our arguing (see Section 11.3 and Section 12.3.2) that this sequence is probably the only one in the context of logic programming. Second, the hardwired mapping between the predicate-variables and the methods of the toolbox is justifiable by pure common sense. 

A possible solution is to automatically infer a property set of the intended relation and then to use an entire synthesis mechanism (such as the one described in the two previous chapters) in order to infer a logic algorithm that is complete wrt the given examples and inferred properties. We here describe such a method, called the Synthesis Method, which is specific to the synthesis of the Processj and Composej predicate-variables of the divide-and-conquer schema. 

The Synthesis Method is currently too closely entangled with the divide-and-conquer schema, with the synthesis mechanism described in the two previous chapters, and with the objective of Step 6 of that mechanism. In order to make it a full-fledged stand-alone method that can be added to a more general tool-box, some future research is needed to make it schema-independent. It might still rely on the MSG Method for the inference of an example set. But the inference of a property set could probably be made predicate-variable-independent and schema-independent by some theorem-proving task that exploits the integrity constraints of a schema. 

The architecture of SYNAPSE is very obvious from the technical details of the underlying synthesis mechanism (see Chapters 12 and 13) synthesis is achieved by a sequence of 7 non-deterministic procedures, each implementing one of the 7 synthesis steps. The implementation is actually based on version 4 of the divide-and-conquer schema, unlike the presentation in this book, which is restricted to version 3. This means that arbitrary A2-ary predicates can be handled, rather than only binary ones. 

Schema-variables of (version 3 of) the divide-and-conquer schema c the number of sub-cases of the non-minimal case c = v + w...

The central methodology is to assume the target program can be created by instantiating a particular schema and to concentrate resources on finding how to fill in the associated fields. In this work, a divide-and-conquer schema is used which can be instantiated to do a wide variety of computations. Once the schema is selected, one can provide a number of specialized strategies for instantiating its parts and the associated costs can be kept under control. All of these ideas and many more are incorporated into the Hener system and covered here. 

---