The Isabelle Approach to
Inductive Logic Program Synthesis

I.M. Good
Uppsala University, S-751 05 Uppsala, Sweden
Email: img@uu.se Voice: +46/18/266-4000

Abstract

In this overview paper, I present Reddy's Isabelle inductive synthesis technique, and illustrate it by means of a sample synthesis. I then critically evaluate it by comparing it to the state of the art in program synthesis, and outline an extension that greatly enhances the appeal of Isabelle.

1   Introduction

The Isabelle technique (Inductive Synthesis of Algorithms By Excellent use of Logic in LEarning) [Reddy 93] interactively synthesises algorithms (expressed in a subset of first-order logic) from examples of their intentions.

{... 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.

2   The Specification Language

The language used to give specifications to the Isabelle technique is a [non]formal language, because {...}.

{... 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 {...}.

3   The Target Language

The language used by Isabelle to express its synthesised algorithms / programs is a functional / relational / ... language. Such a language is suitable for the synthesis task, 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].

4   The Synthesis Technique

The synthesis technique of Isabelle performs transformational / constructive / schema-guided deductive synthesis {respectively: trace-based / model-based inductive synthesis} [Flener 95], because {...}.

{... 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 {...}.

5   A Sample Synthesis

I now illustrate Isabelle at work by means of a sample synthesis. Let us start with the intentions. Informally speaking, a plateau is a non-empty list of identical elements. A compact list is a list of couples, where the first term of a couple, called the value of the couple, is different in two consecutive couples, and the second term of a couple, called the counter of the couple, is a positive integer. Let us now informally describe the intentions of a list compression problem: In Isabelle's specification language (see Section 2), these intentions can be expressed as follows:

{... 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 {...}.

6   Evaluation and Related Work

The Isabelle technique belongs to the expert-specifier / narrow-domain / software assistant trend [Rich and Waters 88] of automatic programming, 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 {...}.

7   Future Work

There are many directions for future work around Isabelle: I here develop one of them in some detail.

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


 

8   Conclusion

In this overview paper, I have {...}.

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 ...}.

Acknowledgments

I hereby express my gratitude to Prof. Frank Lee Stund (Tampere University of Technology), for his constructive comments on an earlier draft of this paper, and to my office-mate Spal Ing Czecka, for his careful proof-reading.

References

[Flener 95]
          Pierre Flener. Logic Program Synthesis from Incomplete Information. Kluwer, 1995.
[Reddy 93]
          R.U. Reddy. Isabelle: A semi-automatic logic program synthesis technique.
          IEEE Transactions on Software Engineering 19(5):225-275, May 1993.
[Reddy 94]
          R.U. Reddy. Logic Program Synthesis with Isabelle. Ultimate Books, 1994.
[Rich and Waters 88]
          Charles Rich and Richard C. Waters. Automatic programming: Myths and prospects.
          IEEE Computer 21(8):40-51, August 1988.