Genetic Programming \(\varvec{+}\) Proof Search \(\varvec{=}\) Automatic Improvement

There is growing interest in automatic programming techniques for software maintenance and evolution. In addition to the work described in the previous section, one noted success has been a 70-fold improvement in runtime performance [14] for a 50,000 line C++ program in widespread use. In general, the optimisation criteria can include a variety of functional and non-functional properties [15]. This suggests that exploring the space of data types is likely to be useful, since this allows (for example) memory to be traded for execution speed. In GP in general, programs are typically represented as expressions trees, stack- or register-machines. In GI, the tendency is to use Abstract Syntax Trees (AST) or e.g. delta-edit sequences of ASTs [16]. The type system of a program can contain useful semantic information, which is of particularly value in a functional (referentially-transparent) context. In particular, types can give information about what a program calculates, i.e. a denotational semantics [17]. For example, for \(f{:}\, List \rightarrow {\mathbb {N}}\), it can be determined from the type of f (via the mechanism of ‘free theorems’) that f is a function of the length of the list [18]. More expressive languages (e.g. Agda [19]) allow even stronger inference of the underlying semantics. For example, each of the 3 terms in the following expression are types, and the two numbers \(a,b \in {\mathbb {N}}\) returned by the function

when given an argument \(c \in {\mathbb {N}}\) are always guaranteed to satisfy the predicate \(a * b == c\):In subsequent sections, we describe a method of program transformation that operates on algebraic data types (ADTs) and which can be considered as a semantics-preserving mutation operator. Although algebraic data types share an acronym with abstract data types, they should not be confused with the latter notion. ADTs are ubiquitous in functional programming (indeed, they are the only data types in the Haskell language, for example) and with the increasing trend for incorporating aspects of functional programming into mainstream languages, it might be expected that ADTs will become more widely known. Although our implementation uses Scala, the technique is applicable to any language which can express ADTs, whether explicitly or by convention—in principle this could even be achieved in more traditional imperative languages such as C, but the idiosyncrasies of the type system and the lack of sophisticated reflection facilities would make the implementation a daunting prospect.

As described in more detail subsequently, ADTs are inductively-defined in terms of multiple type-constructors via choice, tupling and higher-order functions [20]. A simple example of an ADT is the singly-linked list, having two constructors,

for the empty list and

for combining an element with a pre-existing list to create a new list. In Scala this is expressed as

as shown in Listing 1. For those unfamiliar with Scala, a

can be considered as equivalent to a Java™ interface and the

keyword ensures that the only subclasses which can exist are those given in the listing (the latter is necessary in order to guarantee the validity of the equational derivation described in Sect. 3). A

denotes a value (as opposed to reference) type that can appear in pattern-matching expressions.

The term ‘algebraic data type’ arises from the fact that ADTs have an ‘equational’ representation, viz. the notion of ‘choice of constructor’ corresponds to ‘\(+\)’, tupling of types corresponds to ‘\(\times \)’ and functions are denoted by exponentiation.

The transformation process is achieved via a search for a semantics-preserving mapping which replaces a designated source type with some alternative (but functionally compatible) target type. As detailed subsequently, the equational representations for source and target types can be automatically derived from the type declaration and then used to guide the search process. The search method is that of deterministic proof search [13], resulting in a proof that the source can be transformed into the target. This proof can then be turned into a program fragment which performs the required mapping via the Curry–Howard isomorphism (see [13], Ch. 3). Such a mapping is desirable for two reasons:Case studies for both of these applications appear in Sect. 6. The former application is novel and the latter provides further detail to that given in [21]. The remainder of this article is as follows: Sect. 2 describes related work in both GI and formal methods of program synthesis, together with some of the open issues in GI. We describe the transformation process in Sects. 3 and 3.3 and detail the two case studies above in Sect. 6. Section 7 gives conclusions and avenues for future work.

As discussed above, GI is the application of Genetic Programming techniques [3] to (typically human-engineered) source or object code. Although in relative infancy, GI has been used to improve performance [14]; obtain multi-objective trade-offs between non-functional properties [22] and fix bugs [2]. Two prevalent examples of GI systems are the GISMOE system of Langdon and Harman [14] and GenProg by Le Goues et al. [2]. The GISMOE system is used to improve the performance of the 50,000 lines of C++ code of the widely-used DNA sequencing system Bowtie2. In [2], Le Goues et al. describe the latest version of their GenProg GI software for bug repair in ‘C’ programs. GenProg employs negative test cases for encoding the bug and a set of positive test cases describing behavioural invariants. In order to conserve memory, program variants are represented as a sequence of edit operations (‘patches’).

As might be expected of an emerging research topic, there are some issues with GI. The most notable issue is loss of correctness: it is common practice in GI to validate against a test suite (if one exists) and/or treat the seed program as an Oracle. This approach is of course subject to the caveat that “program testing can be used very effectively to show the presence of bugs but never to show their absence” [23]. Indeed, some results from more popular GI systems have recently been called into question. In a study by Qi et al. [24] of the validity of repairs generated by GenProg and the RSRepair [25] and AE [26] systems, it was determined that these systems actually failed to produce valid repairs on at least half of their own validation suite.

Even aside from obvious issues this raises for safety-critical systems, the potential for loss of correctness might reasonably be expected to hinder the adoption of GI in many application areas. For these reasons, it was suggested by White [27] that some variant of formal model-checking be integrated into the optimization procedure.

Another significant issue is that GI often requires a degree of ‘human-in-the-loop’. One recent approach which has the potential to reduce human intervention is the ‘grow and graft’ (termed GGGI) of Harman et al. [11], in which base functionality is evolved via GP (the ‘growing’ phase) and then transplanted (‘grafting’) into a pre-existing host program. Essentially, the ‘grafting‘ consists of replacing a node of the syntax tree with a function call. A case study is given which grows an invocation of the Google Translate API and grafts it into the Pidgin instant messaging system, the latter being a 200 KLoC C/C++ program.

Any attendant necessity for human validation also robs GI of some of the automation that initially motivated it. It might be hoped that GI would be easier for the untrained end-user to apply “off the shelf” than GP, since function and terminal sets could in principle be obtained from the host program. In current practice, a higher degree of human intervention is typically required: e.g. in Langdon and Harman [14], it was necessary to provide ‘match templates’ and perform profiling in order to constrain the space of possible mutations. Since the methods presented here are constrained by the type system, no such configuration activity is necessary.

A third issue (somewhat shared with plain GP) is the trade-off between modularity, expressiveness and readability. It is well-known that GP tends to suffer from bloat and also poor module induction [3]. Insofar as these properties are inherited by GI, there is clearly the potential to degrade the readability of the source program. This effect can be addressed at the potential expense of expressiveness by limiting the permissible mutation operators and/or the scope within which variables can be referenced [14, 28]. By contrast, the technique we describe in this article is intrinsically modular: a direct mapping (a wrapper or adaptor function) is generated between types, which is always representable as a subroutine call. As such, our technique improves upon the state of the art by providing a more adaptable ‘grafting’ phase for ‘grow and graft’ GI, which nonetheless leads to human-readable end results.

There is of course a very large body of pre-existing work on formal approaches to program synthesis. Building on work by Summers [29], there has been much research under the umbrella term of inductive programming [30]. Initial approaches essentially performed symbolic regression and avoided search (stochastic or otherwise) via inductive inference followed by a semantics-preserving construction. This was made possible by two means: a judiciously-chosen set of input–output pairs and a restricted space of programs. More recently, Jha et al. [31] give a method (which they term ‘Iterative Synthesis’) for the construction of loop-free programs from input–output pairs, driven by a SMT solver. The PROSPECTOR system of Mandelin et al. [32] performs type conversion via a collection of operations obtained from existing source code. Perelman et al. [33] and Givero et al. [34] both provide code-completion assistants via type-assisted ranking of API calls for the completion of partial code fragments. In terms of hybridizations between formal and generative techniques, the IGOR II system of Katayama [35] employs an approach termed ‘analytically-generate-and-test’, in order to synthesise programs from input–output pairs.

Of greatest relevance to this article is Djinn [36], which uses a decision procedure to automatically construct functions that map between ADTs in the Haskell language. Since this decision procedure is based on proof search in the intuitionistic propositional calculus [37], Djinn will always find such a function if one exists, or else terminate after constructing an implicit proof of non-existence. However, Djinn does not work with recursive types, since there is no termination guarantee in this case. In the following section, we present our algorithm, which extends Djinn’s approach to deal with a family of recursive types. As a result, our approach is able to generate proofs that Djinn cannot, as described in detail in the following section and illustrated in detail in Sect. 3 and in the case study of Sect. 6, where it is used to synthesize a mapping between two recursively-defined list variants.

Two types are said to be isomorphic iff. they contain the same information, that is, a pair of mutually inverse conversion functions can be defined between them. Considering types up to isomorphism allows us to ignore superfluous details in data representation. For example, functions that solely disagree in their argument order have isomorphic types.

Describing when two types are isomorphic (and witnessing the isomorphism with conversion functions) is an active research area. An important technique is to associate an equational theory to the types of the language such that the equality \(A = B\) follows from the axioms of the theory precisely when the types A and B are isomorphic. Since recursive types can be characterized as fixed-points of equations, a similar association will prove useful in Sect. 3.2. Bruce and Longo [38] showed that the simply typed lambda calculus admits such theories with a single axiom. The result was subsequently extended to the lambda calculus with surjective pairing [39], and later to several different combinations of type constructors.

Among programming languages, ML’s type system has been the main subject of research. Type isomorphism algorithms have found important applications in API search engines. The idea of using types as keys in a database was first proposed by Rittri [40]. Di Cosmo [41] gave an efficient algorithm for deciding type isomorphism in ML-style polymorphic type assignment frameworks, and applied it to API search engines.

On the logic side, type isomorphism corresponds to the existence of proofs \(A \vdash B\) and \(B \vdash A\) that reduce to the axiom rule when cut against each other. Finding such proofs is possible using the Proof Search paradigm presented in the article. One should note, however, that some of our grow-and-graft applications are not direct instances of the type isomorphism problem. For example, many types used in the case studies of Sect. 6 fail to be isomorphic, yet one can still derive useful injections and partial inverses between them.

We now describe our approach, the concrete implementation of which we call PolyFunic. First of all, we associate an algebraic equation to each type. The latter stages of our algorithm (the so-called Proof Search phase) will operate directly on this algebraic representation. In the following, we distinguish between data types and function types (exponentials). Each data type is associated with a finite set of constructors, and the constructor arguments can be accessed positionally during pattern matching. There are three fundamental constructions for defining new types based on existing ones S and T:With this notational convention, any data type can equivalently be characterized using an algebraic equation given in terms of its constructors. Let S be a data type with two constructors, \(c_1{:}\,A_1 \times A_2 \rightarrow T\) and \(c_2{:}\,A_3 \rightarrow T\). Then the corresponding algebraic equation isGenerally: take a data type T and denote its set of constructors by \(C_T\). For \(c \in C_T\), let the list of arguments of c be given by \(A_c\) (the arguments themselves may be function types as well). The algebraic equation for the type T is then given byConstructors without any arguments are traditionally denoted by 1 in the algebraic equation, since such constructors arise from the vacuous product. To illustrate this, first consider a data type describing a

: two constructors,

which takes no arguments, and

which takes two arguments, the colour and the plate number. The Scala declaration of this type can be seen on Listing 2. The corresponding algebraic equation is simply

Now consider the data type of natural numbers. In Scala, this can be described as per the

data type of Listing 3. The type has two constructors, i.e.

, and the

constructor which gives the successor of its argument, another

. The argument of the constructor

is another

. The associated algebraic equation is therefore

Unlike Eq. 2, Eq. 3 is “recursive” since the term \({\text {Nat}}\) occurs on both sides. Normally, the Proof Search is non-terminating in the presence of such self-reference. Fortunately, in many cases, it is possible to eliminate the self-reference using a technique from category theory.

To explain the elimination of self-reference, it is necessary to briefly introduce some category-theoretic notions. We will attempt to convey the essential concepts without undue technical detail. Category theory has served as a formidably-powerful unifying mechanism in mathematics, but also has widespread applications in software engineering [42], where it provides principled constructions for many kinds of software artifacts. The reader who desires a more in-depth introduction is referred to Pierce [43] or Bird and de Moor [20].

Formally, a category is formed by a collection of objects, and an associated collection of morphisms, mapping objects to objects. It is required that there is an identity morphism, i.e. \(id{:}\,X \rightarrow X\) for all objects X and that morphisms compose, i.e. for objects A, B, C, given morphisms \(f{:}\,A \rightarrow B\) and \(g{:}\,B \rightarrow C\), a composite morphism \(g \circ f{:}\,A \rightarrow C\) can be constructed. The most well-known category is the category having all sets as objects and all functions as morphisms. Up to technical considerations, it is possible to consider a category having Scala types as objects, and Scala functions as morphisms.

A functor F is a mapping between categories: it associates to every object A of the source category an image object F[A] of the target category, and to every morphism \(m{:}\,A\rightarrow B\) in the source category an image morphism \(map_F[m]\) in the target category. The image of an identity morphism is required to be an identity morphism.

Intuitively, we can imagine a functor F as a generic container.¹ The notation F[T] denotes a container F parametrised by the type variable T. The container F can be then instantiated with any of a family of types, e.g. the

data type is a functor, which can be instantiated as a list of integers

, a list of strings

and so on.

Functors must provide a structure-preserving map operation which, when provided with F[T] and a means of conversion between the type T and the type U, yields an isomorphic container of type F[U]. For example, the map operation of the

functor preserves the order of the elements:The concepts of strong typing and type constructors are of course entirely familiar within the formal methods community. The GP community has become familiar with the use of types to constrain the search space of programs [44] and the notion of a type constructor has also become a familiar concept via its incorporation into object-oriented languages. The same holds for parametric polymorphism, known as “generic types”, or sometimes simply “generics” in the object-oriented context. In terms of foundational computer science, many typed programming languages (e.g. the simply-typed lambda-calculus [45] or intuitionistic type theory [46]) give rise to corresponding categories: the objects are types and morphisms are functions between types.

The following steps (see Bird and de Moor [20] for further detail) allow us to eliminate self-reference from a recursive type T when our goal is to find a mapping to another type R:Unless certain technical conditions apply [20], the base functor for T can be obtained from the right-hand side of the algebraic equation of T by replacing the recursive occurrences of type constructors with an additional type parameter R. For example, in the case of Nat, the base functor is defined by the equation

The ultimate goal of PolyFunic is transforming a given ADT T (or a set of ADTs \(\varGamma \)) to some other ADT U. Equipped with the base functor and the cata function, we can reduce the associated proof search for \(T \vdash U\) to a search for a proof of \(B_{T}[U] \vdash U\). Notice that this latter sequent does not contain the recursive data type T, and is thus amenable to Djinn-style proof search.

This simplification is made possible by virtue of the fact that the fixed point of the functor \(B_{{\text {T}}}\) is isomorphic to the type

. Naturally, the fixed point X of a functor F is defined by the property³ \(F[X] = X\). The Scala code corresponding to these constructions can be seen in Listing 4. In general, the code for \(B_{T}[R]\) can be synthesized from the data type definition of T (e.g. as obtained by Scala’s reflection mechanism [47]). The

function can be derived for any data type by the trivial bijection between the constructors of T and \(B_{T}[R]\). The version of cata given is a specific case of the general parametric cata function, which can operate on any base functor.

A sequent is of the form \(\varGamma \vdash \varDelta \), where \(\varGamma \) and \(\varDelta \) are comma-separated lists of Scala ADTs.⁴ The intended reading of the sequent is that “given instances of all types in \(\varGamma \), we can construct an instance of some type in \(\varDelta \)”. Therefore, commas on the left of the \(\vdash \) symbol correspond to products, on the right of the \(\vdash \) to sums. Many readers will be familiar with the concept of pattern matching in functional languages, which is essentially an ordered sequence of condition-action rules mapping from patterns (as described by type constructors) to executable code.

In our proof search, the types are manipulated using left and right rules of inference derived mechanically from the definition of the corresponding data types. The search starts from the root of the tree (i.e. the rules are meant to be read from bottom to top): it is sufficient to prove the sequents above the horizontal line to conclude the sequent below the horizontal line. Left rules corresponds to pattern-matching on the type, while right rules corresponds to invocations of a constructor of the type. The left rule for a general ADT T can be seen below: every branch corresponds to a constructor c of T, and \(A_c\) is the corresponding set of constructor arguments. A single branch corresponds to one possible result of pattern matching.

The right rule for a general ADT T is similarly derived. In this case, branches correspond to elements P of the Cartesian product \(\prod _{c \in C} A_c\), thus accounting for all the possible ways of supplying arguments to the constructors:

There are separate left and right rules for dealing with function types, given below:

In order to preserve termination in the case of recursive types, the application of left rules has to be forbidden. Instead of left rules, the synthetic rule seen below must be used. This synthetic rule is derived from the catamorphic substitution technique explained in Sect. 3.2, and corresponds to an invocation of the parametric

function presented there.

By repeated applications of these rules of inference, a branching proof tree is constructed. A branch of the search is terminated when reaching an axiom (a sequent such that \(\varGamma \cap \varDelta \) is non-empty), or when no further rules are applicable. A proof tree is valid if and only if all the branches terminate in axioms. A sequent with a valid proof tree is said to be proven, the corresponding proof tree being the proof.

As described in the previous section, proofs in the sequent calculus are constructed in a bottom-up fashion, starting from the conclusion and repeatedly applying inference rules until axioms are reached. At every stage of the search, only finitely-many rules are available. PolyFunic uses a simple deterministic search procedure with backtracking, which is able to exhaust all possible proofs of a given sequent. An overview of the usual techniques of proof search is given in Paulson [48]. Using a proof of the sequent \(A \vdash B\), one can derive Scala functions of signature \(f{:}\,A \rightarrow B\). A single proof always corresponds to a single⁵ such function and the correspondence between left rules/pattern matching and right rules/constructor invocations can be used to procedurally generate the corresponding transformation. Having factored out recursion as described above, the generating procedure is precisely that implemented by Djinn [36].

For these types, the general construction outlined above gives the following left and right rules of inference:

Clearly, an instance of the class

can be extracted from an instance of the class

in two ways: one can extract either the

or the

. However, it is not possible to extract an

instance from an

instance: one would need to create either the

or the

(neither of which are ADTs) from scratch. These results are easily established via Proof Search. We try to prove the sequents \(IaS \vdash IoS\) and \(IoS \vdash IaS\) respectively. In the first case, the resulting proof will generate the code for the two possible extraction functions. In the second case, the search will fail when the pool of possible rules is exhausted. The search for \(IaS \vdash IoS\) yields the following proof (the LaTeX code for the proof trees was generated by PolyFunic):

There are two Scala functions corresponding to this proof, one for each type that occurs on both sides of the axiom, as follows:

Here is an invalid proof tree, corresponding to a failed search for a proof of the false implication \(IoS \vdash IaS\):

The algorithm presented above is a simple extension of Proof Search in the LJT calculus to deal with recursively defined types. While every valid proof tree of conclusion \(A \vdash B\) corresponds to a Scala function of type \(A \rightarrow B\), it should be clear that the converse fails in the presence of recursive types. Finding an explicit counterexample is left as an exercise to the reader. As such, implementing some of the type isomorphism approaches presented in Sect. 1 could be a useful—if somewhat ad-hoc—way to further increase the capabilities of the algorithm.

Notice also that the FAILED branches correspond to the cases where either an

or a

would have to be generated from scratch, which suggests an opportunity for hybridization with some kind of generative technique, e.g. traditional GP. In the following sections, we present two case studies that reveal how the Proof Search algorithm can be used in the ‘grafting’ phase of ‘grow and graft’ GI.

PolyFunic ignores data types that do not confirm to the following rules:These rules are required because algebraic data types (and by extension, the emitted code) have to support pattern matching. If the conditions are violated, pattern matching could fail to work in the expected manner. In fact, the Scala compiler statically forbids pattern matching unless Rule 2 is satisfied, although it allows partial pattern matches that may result in runtime errors if Rule 2 is satisfied but the other rules are violated.

The restriction is harmless in Scala, but it may cause problems once PolyFunic is extended to work with other languages. For example, Java has no analogues of the

or

keywords, so new ways of detecting suitable data types will have to be devised. In the worst case, one could always fall back to manual hints and annotations.

PolyFunic is designed to be used as a library, integrated with other tools into some GGGP toolchain. The three phases (extraction and grafting, proof search and code generation) are implemented separately and independently. At the time of writing, two code generators are available: one emits executable Scala code based on a proof tree, the other emits LaTeX for pretty-printing proof trees.⁶ Once the input and output modules are designated, the three phases can be executed without human intervention. The implementation achieves good performance by using a functional variant of backtracking: the proof search produces a lazily-evaluated stream of proof trees until the caller finds one acceptable and terminates the process.

As noted above, the current PolyFunic implementation uses runtime reflection. Compile time reflection (macros) [49] would allow finer-grained inspection of class declarations, and interfacing with the compiler would allow us to treat extraction, grafting and code generation in a simple, uniform manner. Indeed, the macro approach proved to be extremely versatile in another application of Proof Search to Software Engineering, the Proofbox Dependency Injection container.⁷ As such, it is anticipated that PolyFunic will be extended to use macro-based reflection in the future.

As a concrete instance of this problem, take the two ways of building linked-lists as ADTs: the constructors correspond either to prepending or appending an element, yielding what are traditionally called

and

respectively and are given in Listing 7. The two types are, of course, isomorphic, and PolyFunic is able to derive conversion functions between them.

When asked to prove \(ConsList \vdash SnocList\), PolyFunic returns the following proof tree (among others). For reasons of space,

and

are abbreviated by S and C respectively in the proof below.

This proof corresponds to the obvious conversion function between

and

—in the specific case of lists, the

function corresponds to the ubiquitous higher-order fold function, which turns iteration over the list into recursion. In the case of

, fold acts on the constructors by replacing

with a value

and

with a binary operation

. Hence, for the list [1, 2] given by

, fold yields op(1, op(2, initialValue)). The conversion function derived by PolyFunic is equivalent to a fold with

and

. In the program of Listing 8, the initialValue and the op correspond to the branches of the pattern matching.

As discussed above, the naïve application of GI suffers from a lack of guarantees: most notably of correctness, but also of efficiency. Even when the latter is an explicit objective, it is typically the case that this objective is obtained on some training set, in anticipation that this will generalize to the scenario of end-use. In closing, we describe a transformation that is not only semantics-preserving, but which also leads to an asymptotic improvement in efficiency.

Many immutable data structures, such as

above, or regular Java™’s

class, have poor asymptotic performance on common functionality such as repeated concatenation or even the

function (for a broader discussion of this phenomenon the reader is referred to [51]). This motivates alternative data representations, such as the infamous

s, and the difference lists presented below.

A difference list is a functional data structure introduced by Hughes [51], which supports constant-time concatenation operations.¹¹ Every difference list f represents an underlying linked list \(L_f\). The difference list itself is implemented as a function \(f{:}\,ConsList[A] \rightarrow ConsList[A]\) which works by prepending \(L_f\) to its argument. As such, only some functions with that signature represent linked lists, i.e. the types

and

are not isomorphic. The Scala declaration for a difference list ADT is the following:

Concatenation of difference lists is simply composition of their associated functions. As such, a grown code fragment which uses difference lists for a function that requires many concatenation operations will be asymptotically superior to one that works directly on linked lists. Such operations are required even for relatively common functionality such as reverse, see [51]. As discussed at the beginning of this section, there is a need for grown functionality to use types that achieve good asymptotic performance, but this is problematic since the data structures of the host program are fixed. The grafting phase must therefore accommodate this type discrepancy. Given the declaration of

above, PolyFunic’s proof search is able to derive the proof for converting between the

and

data structures, which allows the grown functionality to work on the latter ADT, even though the host program uses the former, thus allowing for asymptotically superior performance.