Inversion of Applicative Programs

1. Introduction

This paper describes ongoing research on the problem of automatically inverting applicative programs. The motivation for this work is to achieve a better understanding of the transformation of computer programs. Inversion is an important program manipulation problem. In addition, program inversion may prove to be a fruitful special case. for studying the general transformation problem. The domain of purely applicative programs is chosen because the absence of side effects results in much cleaner program manipulation.

The program inversion problem was originally addressed by McCarthy [3] in the context of Turing machines. Sickel [6] provides an algorithm for determining the invertibility of logic programs. Dijkstra [2] presents a manual derivation of the inverse of an imperative program. A rule for inverting the cons construct in applicative programs is described by Scherlis [5]. Wadler [7] .has implemented a limited inversion facility as part of the interpreter for his What? language. Darlington's[1] program transformation system handles inversion by the folding and unfolding of recursion equations. However, his system requires the user to specify the different input cases for the inverse program. Neither Wadler nor Darlington address the issue of the generality of their mechanisms.

Given a program P, we define the inverse of Pas p· 1 such that P" 1 (P(x)) = x for all x in the domain of P. Our problem is to automatically derive p· 1 from P. In other words. starting with an Computer Sciences Department and IBM Thomas J, Watson Research Center Yorktown Heights, N.Y. 10598

This research was sponsored by the Defense Advanced Research Projects Agency (DOD), ARPA order No. 3597, monitored by the Air Force Avionics Laboratory under contract F33615·78·C·1551. The views and conclusions contained in thos document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the U.S. Government.

equation of the form y = F(x) , we want an equation in the form F' 1 (y) = x. The contribution of this paper is a new method for attacking this problem. It involves successively stripping off the outermost function on the right-hand side and adding the corresponding inverse function to the left-hand side. Each primitive construct in the language requires a separate rule and an additional rule is required to handle recursive and auxiliary function calls. Constructs without a unique inverse are inverted by the introduction of new variables. The values of these variables are determined by solving the simultaneous equations generated by this process. The language chosen is a minimal subset of pure LISP, including car, cdr. cons. con d. and equal.

2. The transformation rules

This section describes the transformation rules required to invert programs written in the above LISP subset. For clarity of exposition, the syntax is based on the meta language of McCarthy, et. al. [4]. For example, if

then taking the car of both sides we get

Similarly, i~ we take the cdr of both sides, the result is

Thus. we can replace the first equation by these two derived equations, without loss of information. This rule is quite simple because cons is an invertible function.

However, car and cdr are not invertible functions since we cannot uniquely determine a list given only its car or its cdr . These functions are inverted by the introduction of new variables. liz · car(x) . then x mustbeoftheform cons(z,a).where a is the as yet undetermined cdr of x. Thus.

is replaced by

Similarly, the equation

can be rewritten as

where a is the undetermined car of x. The values of the variables are later determined by solving simultaneous equations (see example below) .

We also require a rule lor inverting the conditional function. A conditional equation of the form

and is transformed into

This rule allows us to invert conditional clauses independently. However, if P(G- 1 (y)) and -P(W 1 (y)) and Q(H- 1 (y)) are all true, then the function is not invertible in general. The generalization of the conditional rule to more than two clauses is straightforward.

Finally, if the outermost function on the right -hand side of the current equation is a recursive call to the function we are trying to invert, then we generate a recursive call to the inverse function on the left-hand side. In other words, if F(x) is the original function, and the current equation is of the form

we can replace it with

where F- 1 is the name of the inverse function.

This same rule applies when the outermost function on the right-hand side is a user-defined auxiliary function. It is replaced by its own inverse on the left-hand side and the equation defining the function must then be inverted. Note that if a function has two arguments, its inverse consists of two separate functions, one to produce the first argument and one to produce the second argument. These are distinguished by subscripts in the example below.

3. Example: reverse of a list

As an example of the application of this technique, we invert a program which computes the reverse of a list. Reverse (abbreviated R) takes a list and reverses the order of its top-level elements. It uses an auxiliary function, tailcons (abbreviated C), which appends an element to the end of a list. Note that our goal is to express the argument z as a function of R ( z) or s . The derivation is shown ~n figure 1.

The resulting program removes the last element of the list and adds it to the beginning of the reverse of the rest of the list. c. - 1 is one of the inverses of tailcons, and returns the front of the list excluding the last element. Similarly, c 1 - 1 is the other inverse, and returns the last element of the list. What remains is to derive these two inverses from C ( x, y) . This is done in figure 2.

4. Observations and current research

An obvious question at this point is how do we know that all the indeterminate variables can be solved for. If a function has a unique inverse, or in other words is one-to-one, then the equations that result from applying our rules will have a unique solution. However, our ability to solve those equations will ultimately limit the power of this method.

II a function is not one-to-one, then this technique produces a partial inverse in the sense of inverting what can be inverted and indicating exactly what information is missing. For example, consider inverting a program which swaps the elements of a two-element list:

This is a partial inverse because the variable a remains indeterminate. The reason is that we neglected to specify that the list contains exactly two elements (i.e. cdr (cdr (.x) ) · n 11 ).

Another observation is that the program for the inverse of reverse is not the same as the original program. Even though the inverse of the reverse function is the same function, the inverse of the reverse program is in fact the program derived in the example. Inverting the inverse of a program should yield the original program, and it does in the case of reverse.

Current research on this problem is focused on extending this technique to more complex inversion problems. In addition, I hope to prove the correctness of the method for as wide a class of programs as possible. In particular, since the inversion algorithm implements a one·to·one function, it should be possible for the algorithm to invert itself.

Acknowledgments

I would like to thank Allen Newell, Bill Scherlis, and Herbert Simon for several helpful discussions concerning this research. In addition, Merrick Furst, Michael Horowitz, Greg Korf, Bruce Lucas, and Mark Stehlik read and provided constructive comments on drafts of this paper.