Inductive Logic Program Synthesis

{... other generalities about *Isabelle* ...}

The remainder of this paper is now organised as follows. In Section
2, the language used to communicate specifications to the *Isabelle*
technique is presented, and, in Section 3, the language used by *Isabelle*
to express the synthesised algorithms is introduced. Section 4 is about
the synthesis technique proper, and I illustrate *Isabelle* at work
by means of a sample synthesis in Section 5. Next, in Section 6, a critical
evaluation of *Isabelle* is given by relating it to other state of
the art techniques. I then propose, in Section 7, some directions for future
work around *Isabelle*, and develop one of them in detail. Finally,
Section 8 concludes.

{... other details about the specification language ...}

This language is [a subset of first / second-order] logic / algebraic / ... . The axioms / examples / ... are written in relational / functional form, which means that {...}. Recursive axioms / ... are [not] allowed / needed, because {...}.

This specification language is [in]expressive / [un]readable / with[out] implementation bias, because {...}. Using this language, it is [im]possible to write specifications that are totally correct / partially correct / complete with respect to the intentions, and that are minimal / internally consistent / unambiguous / non-redundant, because {...}. The assumption for synthesis is that a submitted specification is {...}, because {...}.

{... other details about the target language ...}

Such expressions can be seen as algorithms, rather than [logic] programs,
because {...}. *Isabelle* itself provides [no] support for implementing
such algorithms into programs (written in {...}). By the way, the *Isabelle*
system is itself written in {...}, and [but] it has [not] been used to
synthesise [parts of] itself [Reddy 94].

{... other details of the synthesis technique,

preferably illustrated by a "small" and "easy" example ...}

This synthesis technique is [not] proven to be sound, that is to {...} [Reddy 94]. Moreover, it is [non]deterministic, because {...}. It is [semi-]automatic, because {...}. The combinatorial explosion of the search space is tackled by {...}.

The synthesised algorithms / programs reflect a divide-and-conquer / generate-and-test / ... strategy, because {...}. Algorithms / Programs that are a composition of algorithms / programs of different strategies can[not] be synthesised, because {...}.

{In case it is a divide-and-conquer strategy:} The induction parameter
is selected by {...}. Compound induction parameters (i.e. induction parameters
that {...}) can[not] be handled, because {...}. The minimal forms of the
induction parameter (that is the values of the induction parameter where
{...}) are determined by {...}. There can / must thus be an arbitrary /
constant (namely *m*) number of minimal forms. The non-minimal forms
of the induction parameter (that is the values of the induction parameter
where {...}) are determined by {...}. There can / must thus be an arbitrary
/ constant (namely *n*) number of non-minimal forms. The induction
parameter can be decomposed intrinsically (in a way reflecting {...}),
because {...}. The induction parameter can also / cannot be decomposed
extrinsically (in a way reflecting {...}), because {...}. Minimal cases
(cases where the induction parameter is of a minimal form) and non-minimal
cases (cases where the induction parameter is of a non-minimal form) can[not]
be further split into sub-cases, because {...}. Discrimination between
such sub-cases is then achieved by {...}. Useless recursion in non-minimal
cases is [not] detected, because {...}. Auxiliary parameters (parameters
that {...}) are detected / declared via {...}. Algorithms / Programs for
appearing auxiliary problems are designed by re-use and/or re-invocation
of the synthesiser, namely {...}.

{In case it is a divide-and-conquer strategy:} The synthesised algorithms / programs may thus feature intrinsic [as well as extrinsic] decomposition of the induction parameter, complete [as well as incomplete] traversal of the induction parameter, and single loops [as well as multiple nested loops]. The synthesised algorithms / programs may be deterministic / fully deterministic / non-deterministic / finite / infinite, given ground values of the induction parameter and of the auxiliary parameter(s), because {...}. Structural manipulation problems (problems where {...}) [as well as semantic manipulation problems (problems where {...})] may be handled, because {...}.

{... specification of the *compress*/2 problem ...}

The synthesis of an algorithm / program from this formal specification
is a piece of cake for *Isabelle*, and goes as follows:

{... details of the synthesis ...}

Finally, the synthesised algorithm / program is as follows:

{... algorithm / program for the *compress*/2 problem ...}

This algorithm / program features {... use the vocabulary defined in Section 4 ...}. Alternative algorithms / programs can be obtained by {...}. The chosen sample problem turns out [in]significant, because {...}.

Synthesis is [not] knowledge-based. Indeed, algorithm design knowledge (knowledge about {...}) is {...}. Efficiency / complexity knowledge (knowledge about {...}) is {...}. Domain knowledge (knowledge about {...}) is {...}. Meta-knowledge (knowledge about {...}) is {...}.

There is [no] support for evolving intentions and specifications, because {... history mechanism ... re-play ...}.

Compared to *Periwinkle* / *Cypress* / *KIDS* {respectively:
*DIALOGS*
/ *SMART* / *Progol*}, the *Isabelle* approach {...}.

{... details about my brilliant ideas about what to do with *Isabelle*
...}

The *Isabelle* system is actually much larger in scope than what
has been examined in this paper, as it also provides support for specification
elaboration / specification validation / specification maintenance / algorithm
transformation / algorithm implementation (into *Prolog* / ... programs)
/ program optimisation.

I believe the *Isabelle* technique is a[n] [in]significant contribution
to the state of the art in program synthesis, because {...}. *Isabelle*
has [not yet] reached the break-even point, where {...}, because {...}.
{... my other conclusions ...}.

Pierre Flener.

[Reddy 93]

R.U. Reddy. Isabelle: A semi-automatic logic program synthesis technique.

[Reddy 94]

R.U. Reddy.

[Rich and Waters 88]

Charles Rich and Richard C. Waters. Automatic programming: Myths and prospects.