Theory of Linear Equations Applied to Program Transformation

I Introduction

Since the pioneering work of [Darlington 1976, Burstall 1977], program transformation has come to be widely recognized as a program development tool. In this paper, we are interested in the application of program transformation to develop iterative programs from recursive programs. A generalized calculus for such transformations called unfold-fold method was given in [Burstall 1977]. Given a recursive equation to compute a function{, one finds another function f ', such that

1. there exists a recursive equation for f' that is in iterative form, and
2. f can be defined in terms off ' without using recursion.

Once such a function f' is found, the unfold-fold method can be used to systematically develop the recursive equation for f ' from that for f. The main problem with the use of this method is to find the target recursive function f '.

We submit that the cause of the problem is that the unfold­ fold method attempts to transform one recursive equation into another without regard to what the functions defined by these equations are. If we can find the solution of the given recursive equation, the function {, it may be possible to systematically develop the function f ' for which an iterative equation exists. But, unfortunately, it is not known how to express the solution of an arbitrary recursive equation. Even though the solution of any recursive equation can be specified as the limit of a

Theory of Linear Equations Applied to Program Transformation

Uday S.Reddy

University of Utah, Salt Lake City Barat Jayaraman

University of North Carolina at Chapel Hill

monotonically increasing sequence of functions [Scott 1970, Manna 1972], the limit itself is, in general, not "expressible", i.e., cannot be specified using a closed form expression involving other functions. Backus [1978] initiated the development of notation and theory to formally derive and express the solutions of certain classes of recursive equations. Further developments of this approach can be found in [Backus 1979, Backus 1981, Williams 1982].

In this paper, we shall consider the class of linear equations as defined in [Backus 1981]. The solutions of these equations can always be expressed using a construct called abstract sequence [Reddy 1982a]. Further, the solutions fall into a class of abstract sequence programs called right-associative sequence programs. We will identify another class called left-associative sequence programs which are equivalent to iterative programs. We will then present examples of transformation rules to transform right-associative sequence programs into left-associative ones, based on the "algebra of functional programs" introduced in [Backus 1978].

II Notation

We shall use the FP system given in [Backus 1978] as the language for presenting the transformations . An object in an FP system is either the undefined object (l_), or an atom or a sequence of objects. The atoms include boolean values (T, F) and numbers. Sequences are enclosed in angular brackets ( ... ) and the empty sequence is denoted by 0 . A sequence containing l_ is equal to l_. All functions accept a single object as argument and yield a single object as result, either or both of which can be sequences. The application of a function on an object is denoted by the operator":". All functions yield l_ when applied to l_ (i.e. they are strict). Unlike other functional languages, in an FP system, only first-order functions are defined. Using a sma ll set of higher order functions called functional forms, functions can be defined without using A.-abstraction. Such definitions are called function- level definitions in contrast to the object- level definitions of the X.--ealculus style.

Appendix I contains a list of Backus's functions and functional forms which we shall use in this paper. Some new functional forms that will be used are given below.

Abstract Sequence

Insert from left

Insert from right

Cumulate from left

Cumulate from right

Example 1: The factorial function can be defined in FP using these functional forms as

factorial = (insertr x) o [(seq pred eq1), ]]

The application of this function to 3, for instance, yields

D

For the sake of convenience, we shall use some purely syntactic extensions to the FP notation. Firstly, we shall use object-level definitions as in >.-calculus based languages. Such definitions can be translated into pure FP definitions in much the same way as extended definitions discussed in [Backus 1981). Another notational extension we shall find useful is infix notation for binary functions. We shall write f(x,y) as x f y using infix notation. Prefix applications of functions have precedence over infix applications.

The seq functional form was introduced in [Reddy 1982a] where a sequence yielded by the seq functional form was called an abstract sequence. As they play a pivotal role in our manipulations, we shall introduce informal notation to denote abstract sequences. In this notation,

denotes (seq r p:t:x). The symbols n, i , and xi are all formal parameters in this notation. It is implicitly understood that p:xi does not hold for all i<n . Using these syntactic extensions, the definition of factorial in example 1 can be written as

The functions tl, tlr, distl, distr, all g, curnl h preserve abstract sequences, i.e., applying any of them on an abstract sequence produces another abstract sequence that can be expressed using the functional form seq. Therefore, we shall use liberalized abstrace sequence nota tion to denote the expressions in which the above functions are applied on other abstract sequences. For instance,

Ill Linear Functionals and Canonical Linear Forms

Definition: A functional of arity n is a higher-order function , that maps every tuple of n functions into a function. D

A functional is an abstract object. A representation of a functional that can be defined in FP is called a form.

Definition: [Backus 1981) Let V = {! 1 ... fn} be a set of (function) variables. Then we shall say that Ef1 ... fn is a form , or E is a form in V, if exactly one of the following holds:

1. Ef 1 ... fn = r for some function r , or
2. Ef1 ... fn = f; for some i, or
3. There are forms E1 ... Ek in V and a primitive form (functional form) r with k parameters such that Ef1 .. . fn = r(E1, ... , Ek).

Consider a recursive equation of the form

where p and q are functions and H is a functional. Using the approach of [Kleene 1952], the solution of such an equation is the limit of the sequence of functions:

Finding the limit of such a sequence of functions is a nontrivial exercise owing to the nesting of the functional H in the approximating functions. If there exists another functional Ht such that

then, each of the approximating functions can be simplified to

The limit of this sequence of functions can be easily found.

Definition: [Backus 1981] A functional Hf is linear if there exists another functional HI called its predicate transformer, so that

1. for all objects x, if Hlx oF= L then for all functions a, H,a:x = T

A form that represents a linear functional is a linear form . D

Example 2: The following recursive equation for factorial

D

It has been proved by [Backus 1981] that, whenever H is a linear functional , the recursive equation

for any p and q, has as its solution, the linear expansion,

Backus then goes on to characterize some of the forms that can be constructed in FP as linear. In the following, we shall give a much simpler characterization of linear functionals, which is essentially the same as that of linear recursive schema of [Walker 1973].

Definition: A form of the kind

is called a canonical linear form. D

It can be verified that a canonical linear form represents a linear functional with the predicate transformer, Hf = f"r.

Theorem 111.1: [Reddy 1983] A functional is linear if and only if there exists a canonical linear form that represents it. D

Using this theorem, we can also formulate a simple operational test to check if a form is linear.

Corollary 111.2: [Reddy 1983] A form H is linear if and only if for all functions b and objects x, either the computation of Hb:x involves a b-application on at most one distinct value, or Hb:x = l_. D

Example 3: The form used in the factorial equation of Example 2 is a canonical linear form. As a more complex example, consider the one given in [Backus 1981].

Note that the computation of Hfx for any x would involve only one {-application, either on b:x or on g:x.

Even though the test given in corollary Ill.2, cannot be performed by an algorithm, it is possible to mechanically identify most useful linear forms and also to transform them to canonical linear forms.

IV Solutions of Linear Equations

A linear equation is a recursive equation of the form

where His a linear form. Using theorem Ill.1, we can see that every such equation can be rewritten in the form

We shall call the function r, the reduction function of this equation, because it reduces the problem of computing fx to that of computing fr:x. As shown in [Backus 1978], this equation has as its solution, the infinite expansion:

lfwe define

qi = lh o apndr 0 [tlr, Q 0 1r] 0 R ; = insertr h 0 [tlr, q 0 1r] 0 R i q = lh o apndr o [tlr, Q 0 1r] oRo= insertr h o [tlr, q 0 1r] oR 0 The sequences yielded by R ; are called reduction sequences. We can now rewrite the solution using the reduction sequences as:

The infinite conditional in the parentheses is itself the solution of the linear equation

R = p - > [id]; apndl 0 [id, Wr]

Using the functional form seq defined as

seq r p = p - > [id]; apndl o [id, (seq r p) 0 r]

we can express R without recursion.

Theorem IV.1: [Backus 1978] The solution of the linear equation

Example 4: The definition of factorial in example 1 is nothing but the solution of the factorial equation given in example 2. D

V Left-associative and Right-associative Sequence Programs

Dt:finition: A right-associative (sequence) program is one of the two forms

fx = insertr h : (seq r p:x, { 0 :x)

Similarly, a left-associative (sequence) program is one of the two forms

Note that an abstract sequence can be transformed into both a right-associative program and a left-associative program. So can a program in which a right selector, such as 1r, which is applied on an abstract sequence. For instance:

Every left-associative program can also be trivially transformed into a right-associative one.

The solution of a linear recursive equation is a right­ associative program and vice versa. On the other hand, every left-associative sequence program can be transformed into an iterative (tail-recursive) equation. Suppose

The iterative equation for f ' is

If { 0 :x is defined by another left--associative program, it can be redefined using another iterative equation. All iterative equations can also be trivially transformed into left--associative programs.

Thus, we have a kind of strong equivalence between linear equations and right--associative programs, on the one hand, and between iterative equations and left--associative programs, on the other. The problem of transforming a linear equation into an iterative one is therefore reduced to the problem of transforming a right--associative program into a left--associative program.

Example 5: We have seen that the solution of the following factorial equation of example 2 is the right--associative program given in example 1. This can be directly transformed to the following left--associative program using the fact that x is associative and commutative:

This, in turn, can be transformed into an iterative program.

factorial :n = fact: (1,n)

fact:(p,n) = n eq 1 - > p x 1; fact:(p x n, n-1 )

0

VI Right-associative-To-Left-associative Transformations

There are basically three methods to transform a right-- associative sequence program into a left-associative one:

1. Using a stack
2. Reduction inversion
3. Associative Duals

Using a stack, all right-associative programs can be transformed into left-associative ones. This is not surprising since all recursive equations can be transformed into iterative ones using a stack. We shall concentrate on the latter two methods.

A. Reduction Inversion

If {is defined by the right-associative program

fx = insertr h: (R:x, { 0 :x)

R:x is the reduction sequence of the corresponding linear equation and is defined as an abstract sequence. If rev:R:x can be defined as an abstract sequence revR:x, then fx can be defined by the left--associative program

This is the simplest technique to use when the reduction function has an inverse. Suppose

and the reduction function has an inverse g so that

r:g:x = x whenever p:x = F

If the last element of the reduction sequence (xO>···.Xn) is t:x, then,

wherey0 = t:x; yi+I = g:yi; Yneqt

The function t:x can, in turn, be defined using the left­ associative program

t:x = 1r : seq r p : x

However, it is not desirable to have two abstract sequences in the transformed program. So, this transformation should not normally be used unless t:x can be defined without using an abstract sequence.

Example 6: Consider the very common reduction sequence

The inverted sequence is

It is sometimes possible to use reduction inversion, even if the reduction function does not have an inverse, but has several right--inverses.

Example 7: Consider the more interesting reduction sequence

where n0 = n; ni +l = ni div 2; nk eq 0 The halve function has two right--inverses: double:n = 2 x n doubleadd:n = 2 x n + 1

Let

ceilingpower:n = the smallest l such that n < 2k

This is nothing but one plus the length of the reduction sequence and can be defined by a left-associative program. The reversed reduction sequence can be defined using the two right--inverses.

0

B. Associative Duals

The method of reduction inversion has only limited applicability. The use of associative duals has much wider applicability and forms the main core of our transformation technique. Consider, again, the right-associative program

We may be able to find a function h', so that

Definition: If, for all sequences s,

insertr h: (z,s) = insertl h' : (s,z)

then the functions (h', h) are said to be associative duals with respect to z. h' is called the left associative dual of h with respect to z, and his called the right associative dual of h' respect to z. 0

Theorem Vl.1: [Reddy 1982b] If(h', h) are duals with respect to z, then (h 0 swap, h' 0 swap) are duals with respect to z. 0

The concept of associative duals was introduced by [Kieburtz 1981]. But, their definition differs from ours. We can show that their definition is a sufficient condition for ours.

satisfy the following conditions, for some z E B,

then (h', h) are duals with respect to z. 0

Example 8: The functions (apndr, apndl) are duals with respect to the empty sequence, 0, because

a apndl ((s 1 , . .. ,sn) apndr c) = (a apndl (s 1 ... ,s ~) apndr c

The function rev, for reversing a sequence can be defined by the linear equation

Its right associative solution is

Since (apndr, apndl) are duals with respect to 0 , the functions (apndloswap, apndroswap) are also duals with respect to 0, by theorem Vl.l. Hence,

A special case of duals occurs when an operation h is associative. If it has an identity I, then h is its own dual with respect to I. If it is associative as well as commutative, then it is its own dual with respect to any value. The functions such as +, -, min, and max are examples of such functions .

Theorem VI.3: [Reddy 1982b) If (h' ,h) are duals with respect to z then (h' 0 [l,k 0 2}, h 0 [k 0 1,2}) are duals with respect to z, for any function k. 0

If a powerful set of properties of associative duals, such as the one of theorem VI.3 , is found then the use of duals may be a viable tool in transformations. But, currently we do not know enough useful properties of them. Therefore, instead of directly looking for the associative dual of the function used with insertr, we would like to transform the given right-associative program into another right-associative program, so that the technique of duals can be used with the latter.

VII Right-associative-To-Right-associative Transformations

For most programs, the function h used with insertr functional form, is too complicated to have an associative dual. We then transform it into another right-associative program in which a simpler function h' is used with insertr. The transformations that are possible for a specific function h are highly sensitive to the form of h and the properties that it satisfies. The following rules identify certain widely applicable. forms and properties of h. But there may indeed be several others. The proofs of these rules can be found in [Reddy 1982b).

1. If the function h satisfies the property

a h (b h c) = (a h' b) h c

for some function h'

The h' may have a dual or may be simpler than h. For example, consider

where exp is the exponentiation function.

a h (b h c) = a h (c exp b) = (c exp b) exp a

0

1. This rule is a generalization of 2 and 3 above. Suppose h is of the form

and k is distributive over h ' in the second variable position, i .e.,

Further, let k be associative and have an identity I. Then

insertr h: ((s 1 , ... , sn), z)

• = insertr h' : ((s' 1 , ... , s'n), z') where z' = k:0k:(b:s 1 , ... ,b:~, z)

The function x is associative and commutative, whereas h is neither.

1. If h is of the form

Example 9: Consider the following linear program from [Arsac 1981).

The right associative solution is

Since the n mod b part does not depend on y, we can simplify the function h, using rule 2.

0 1 insertr + :((tlO :(n 0 mod b), ... ,tlif :(np- 1 ,b)),O) Now, the function + used with insertr is associative and commutative. So, f can be defined by fhe left--associative program (it is not exactly a program yet)

The tlOi factors can be handled by introducing another parameter c . in the elements of the sequence, so that tlOi·x = c .xx' . '

f(n,b) =

This can now be rewritten using an iterative equation.

1. This is a variant of rule 4. Suppose h is of the form h: (x,y) = k: (b:x, h ':(a:x,y))

k is distributive over h'.

h:(x,y) = h' : (k:(b:x,a :x), k: (b:x,y))

Further, assume that k is associative. It need not have an identity.

6. If h is a conditional of the form

h: (x,y) = p:x - > y; h':(x,y)

and h' has a left-identity I,

then, we can redefine h as

1. This is a generalization of rule 6. Suppose his of the form h: (x,y) = p:x - > h, :(x,y); h 2 :(x,y) Suppose

ku .ki2 ····.kip Let us call them the embedded sequence of functions in hi . There will be a similar sequence for h 2 .

k2I .k22 . ... . k2q We need to find a sequence that generalizes these two sequences, so that,

• a . by substituting some of the functions in the generalized sequence by the identity function (id 0 2) we can obtain each of the original'sequences, and
• each of the functions that need to be substituted has a left identity.

We can then construct a function with the generalized embedded sequence using the left identities of the embedded functions, so that this function equals the conditional h. We can extend this method for any number of conditional branches. This scheme of generalization has been used with unfold-fold method by [Arsac 1982].

Examp~e 10: Consider the linear equation

mult:(a,b) = b eq 0 - > 0;

even:b - > 2 X (mult:(a, b div 2));

Its right-associative solution is

h:((a,b),y) = even:b-> 2 x y; a+y

The embedded sequences for the conditional branches are x and + respectively. The generalized embedded sequence can be either +. x or x .+ . Let us choose the former. We can redefine the function h to have this generalized embedded sequence.

Since x distributes over + we can use the rule 4.

mult:(a,b)

= insert! + :(0, (c 0 x l:(a,b 0 ), ... ,C n- f t:(a,b nJ))

Note that each of the coefficients ci is a power of 2. Using a "shift left" operation

it can be rewritten as

mult:(a,b) =

It is also possible to obtain a program without the shift left operation, by noting that x commutes with t. See [Reddy 1982b]. 0

VIII Discussion

An automatic transformation system can be designed based on the techniques described here. Such a system would have three stages.

1. Rewrite the linear equation using a canonical linear form and solve it.
2. If the reduction sequence can be inverted, then use it to produce a left-associative program. Otherwise, apply right-associative-to-right-associative transformations, until the right-associative function is sufficiently simple to have a dual.
3. Transform the left-associative sequence program into an iterative equation or equivalently a loop. ,

The stages 1 and 3 can be done algorithmically, whereas the stage 2 handles a hard problem. We envisage the best approach for stage 2 to be a user-directed transformation system such as that of [Feather 1982].

The main advantage of our transformation scheme over the unfold-fold scheme [Burstall 1977] is that the target recursive function is not guessed (by the sCH:alled eureka steps) but results automatically from the transformation of the solution of the source recursive equation. However, Arsac and Kodratoff [1982] have recently suggested a generalization strategy which can be used to guess the target recursive equation based on the form of the source recursive equation. Even though their strategy is radically different from ours, the effects achieved by them are surprisingly close to ours. More investigation to find any possible relationship of our strategy with theirs is worthwhile.

The main drawback of our transformation scheme is that the algebraic properties of the right-associative function h have to be restated in a form applicable to sequences, so they can be used in right-associative-to-right-associative transformations. The rules given in section VII are such restatements. It is not always clear how the properties can be so restated. The unfold-fold method, on the other hand, directly uses the algebraic properties of the functions involved. Further development of FP algebra may alleviate this problem.

The right-associative-to-right-associative transformations are proved using an inductive proof similar to the unfold-fold method. The rules used in such proofs are 1 and 2 or 1 and 3 of the following.

1. insertr h : (0 ,z) = z 2. insertr h : (s apndr a, z) = insertr h : (s, a h z)

1. insertr h : (a apndl s, z) = a h (insertr h : (s,z))

This suggests that it may be possible to apply these transformations directly on a recursive equation using unfold­ fold, in effect mimicking the transformation of the sequence programs (because every right-associative sequence program is equivalent to a linear equation and vice versa). Such a strategy would eliminate the need to restate the algebraic properties of functions in sequence form, and also integrate our technique with the unfold-fold method which is a much more general technique applicable to any recursive transformation.

If our techniques have to be used for equations other than linear equations, methods to express the solutions of those equations must be found. [Williams 1982) was a step in that direction. Further investigation of recursive equation solutions would facilitate the development of transformation techniques for nonlinear equations.

Acknowledgements

We would like to thank Don Stanat, Manton Matthews and Gyula Mago for several discussions and suggestions.

Appendix I

This appendix contains informal definitions of some FP functions and functional forms that are used in this paper.

Basic functions

identity id:x = x

Basic functional forms

constant c:x = c c:l_ = l_ I is therefore the everywhere-undefined function composition r g : X = f"g:x construction [f 1 , . . . ,fn] : x = (f 1 :x, ... ,fn:x) condition (p - > f; g):x = if p:x = T then f:x else if p:x = F then g:x else l_

Functions on sequences

Functional forms on sequences