Dw:03642 RR266

<figure><img src="image_1.png" /></figure>

laboria

laboratoire de recherche
en informatique
et automatique

PROVING AND APPLYING
PROGRAM TRANSFORMATIONS
EXPRESSED WITH
SECOND-ORDER PATTERNS

Gérard HUET
Bernard LANG

Rapport de Recherche N° 266

Novembre 1977

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
B. P. 105 78150 - Le Chesnay
France
Tél.: 954 90 20
PROVING AND APPLYING PROGRAM TRANSFORMATIONS
EXPRESSED WITH SECOND-ORDER PATTERNS

Gérard Huet, Bernard Lang

IRIA/LABORIA

Résumé :

Nous proposons une technique de transformations de programmes basées sur la réécriture de schémas de second ordre. Un algorithme de reconnaissance complète est défini. On montre comment valider formellement les transformations, en utilisant des méthodes de preuve basées sur une sémantique dénotationnelle. La méthode est illustrée sur des exemples concernant la transformation de récursions en itérations.

Abstract :

We propose a program transformation technique based on rewriting second-order schemas. A complete matching algorithm is given, and the correctness of the method is proved, using denotational semantics. The method is illustrated with recursion removal examples.
## Introduction

There is a huge gap between practical software certification techniques and the theoretical tools defined for formal proofs of programs. One way to close this gap is to write interactive systems that will help the programmer to design, debug, run and ultimately validate his programs.

A desirable feature of such a system is the ability to manipulate programs into various forms, while preserving their meaning.

Such a "program massaging" facility has been advocated by many people [3], [4], [7], [15], [24].

As a systematic approach to high-level optimization for programs, it is the natural complement to structured programming development techniques, which tend to sacrifice program efficiency to clarity and good organization.

One of the most promising techniques is due to Darlington and Burstall. Program transformations are defined as schematic rewriting systems, together with constraints on the instances of the schemas that must be met in order for the transformation to be valid.

We shall here formalize this method, using a second order term language to represent program schemas. We give a uniform matching algorithm to apply the transformations to parts of a program. We show how one can formally validate the transformations, using denotational semantics. Finally we discuss the problems related to organizing a system of schematic transformations.
# 1. Inducing transformation templates from program transformations

Let us first give an example of the schematic transformation method on an example in recursion removal.

Let us suppose we are interested in replacing recursions by iterations. Over the integers, the problem has a well-known but trivial solution : every partial recursive function may be computed with a flowchart using only three registers. However we are not interested in such "Turing machine monster", and we want to favor transformations based on control structure equivalences, as opposed to data encodings. This is why we are more interested in transformations expressed by schemes (programs computing over arbitrary interpretations).

On program schemes it is possible to express the fact that recursion is more powerful than iteration : Paterson and Hewitt [22] showed that the following program scheme may not be computed by a flowchart :

```pascal
f(x) <= if p(x) then a(x) else h(f(h(x)), f(c(x))).
```
(of course we do not allow storage stacks !).

Actually, few recursion schemes are translatable into iterations at the schematic level [25], [28].

Darlington and Burstall proposed in [3] to consider program transformations in the class of all the interpretations that satisfy some axioms concerning the data manipulated by the program.

For instance, consider the factorial program :

```pascal
P : fact(x) <= if x = 0 then 1 else x * fact(x-1)
```
which computes fact(n) as : $n * ((n-1) * (\cdots * (2 * (1*1))\cdots))$ ; Rearranging this expression as :

```pascal
(((\cdots(n * (n-1)) * \cdots) * 2) * 1) * 1
```
suggests using a different computation sequence, which corresponds to the following iterative program, written in ALCOI-like style :
P' : function fact(x) ;
    if x=0 then fact := 1 else
        begin
            fact := x ;
            x := x-1 ;
            while x <> 0 do
                begin
                    fact := fact * x ;
                    x := x-1 ;
                end ;
            [fact := fact * 1]
        end

The equality of the two computation expressions above depends solely
on the associativity of the operator *. We keep the useless statement at the
end of P', which corresponds to the last "1" in the second sequence, because
we do not want to use the additional property that 1 is a right identity for *.

Let us now "abstract" the corresponding schemas. We get :

Σ : f(x) <= if a(x) then b(x) else h(d(x), f(e(x))).

and :

Σ' : function f'(x) ;
    if a(x) then f':= b(x) else
        begin
            f':= d(x) ;
            x := e(x) ;
            while not a(x) do
                begin
                    f':= h(f', d(x)) ;
                    x := e(x) ;
                end ;
            f':= h(f', b(x)) ;
        end

Our conjecture at this point is that the two schemas compute the same
function, in every interpretation that satisfies the axiom :

$$X_1 : \forall xyz h(h(x,y),z) = h(x,h(y,z)).$$

If the statement between brackets in P' had been suppressed, we would get a more restrictive condition, i.e. we would have to add an axiom $\forall xy a(y) \supset h(x,b(y)) = x$, which is not relevant to the recursion removal and would reduce the applicability of the transformation.

Let us call *transformation template* a triple such as $<\Sigma, \Sigma', \{X_1\}>$. There are now four problems to be solved :

1) How do we discover such templates ?

2) How do we validate them ?

3) How do we recognize a template is applicable to a given program ?

4) How do we organize a system applying automatically such templates ?

Problem 1 may be considered as one of the basic problems of communicating knowledge about programming. Although it is the focus of much research at this time, surprisingly few different program transformations are known. For instance, on the topic of recursion removal, Darlington's thesis [2] contains only 10 templates, that we were actually able to generalize to only 6. In the appendix, we list these and a few others. We have not attempted to list all known recursion removal techniques ; in particular we have not considered transformations requiring counters or stacks. Other recursion removal transformations that could be represented by templates may be found in [28,36,37,...]. Templates pertaining to more general transformations may be found in Loveman [15], Gerhart [6] and Standish [23].

Our paper is mainly concerned with problems 2 and 3. We shall see in the next section a uniform matching algorithm, complete over a wide class of schemas, which answers problem 3. Then section 3 shows how to formally validate transformations templates, using program proving techniques based on denotational semantics. It is our thesis that formal proof techniques, although rightly criticized as being difficult to apply to non-trivial programs, can be put to practical use for the rigorous validation of program transformation systems. We have completely proved all the templates presented in the appendix and in the process discovered missing assumptions in transformations given in [3]. For instance, we shall see in section 3 that in order to validate the template above, we need a supplementary axiom $X_2$.
## 2. Matching programs to schemes

### 2.1. Example

Our problem here is to consider our program schemes as second-order patterns. For instance, P above may be considered as an instance of the schema Σ, where a,b,h,d and e are now treated as second-order variables. We have P = σΣ, with σ being the second-order substitution :

$$ 
\begin{aligned}
a & \leftarrow \lambda x \cdot x = 0 \\
b & \leftarrow \lambda x \cdot 1 \\
h & \leftarrow \lambda xy \cdot x \cdot y \\
d & \leftarrow \lambda x \cdot x \\
e & \leftarrow \lambda x \cdot x - 1
\end{aligned}
 $$

Such second-order patterns are a powerful way of expressing a wide class of programs. Let us give a few programs that are instances of Σ :

- program reversing a list

reverse(x) <= if Null(x) then x else Append(reverse(Cdr(x)), Cons(Car(x),Nil))

using the substitution

$$ 
\begin{aligned}
a & \leftarrow \lambda x \cdot \text{Null}(x) \\
b & \leftarrow \lambda x \cdot \text{Nil} \\
e & \leftarrow \lambda x \cdot \text{Cdr}(x) \\
h & \leftarrow \lambda xy \cdot \text{Append}(y,x) \\
d & \leftarrow \lambda x \cdot \text{Cons}(\text{Car}(x), \text{Nil})
\end{aligned}
 $$

- program computing if a number is perfect :

perfect(y) <= y = f(y-1) where
f(y) <= if x=1 then 1 else f(x-1) + if Div(x,y) then x else 0.

Here the inner recursive function is an instance of Σ, using the substitution :

$$ 
\begin{aligned}
a & \leftarrow \lambda x \cdot x = 1 \\
b & \leftarrow \lambda x \cdot 1 \\
h & \leftarrow \lambda xy \cdot y + x \\
e & \leftarrow \lambda x \cdot x - 1 \\
d & \leftarrow \lambda x \cdot \text{if Div}(x,y) \text{ then } x \text{ else } 0 \text{ (note : y is free here)}
\end{aligned}
 $$
For these examples, it is easy to check the associativity of the function substituted to h. Note that, for the last example, the last statement of the iterative translation $σΣ'$ is necessary.

## 2.2. A second-order term language.

Since programs denote functions, it is natural to treat them as second-order objects. Our formalism will therefore represent programs, and schemas denoting families of programs, by terms in a second-order logic.

We assume first that our programming language is defined by an abstract syntax. With every operator or construct of the language is associated a typed operator of fixed arity. For instance, if we have the types "variable", "expression" and "instruction", the assignment operator would have type (variable x expression → instruction).

### a) Types

We assume there is a finite set $T_0$ of elementary types, and the set $T$ of types is the smallest superset of $T_0$ closed by the operation :

$$ α_1, α_2, \dots, α_n \in T \quad & \& \quad β \in T_0 \quad \Rightarrow \quad (α_1 xα_2 x\dots xα_n \to β) \in T. $$

We define the order of type $τ$ recursively by :

$$ \begin{array}{l} \text{if } τ \in T_0 \quad 0(τ) = 1 \\ \text{if } τ = (α_1 xα_2 x\dots xα_n \to β) \quad 0(τ) = \max\{0(α_i) \mid 1 \le i \le n\} + 1. \\ \text{if } τ = (α_1 x\dots xα_n \to β), (α \to τ) \quad \text{stands for} \quad (α xα_1 x\dots xα_n \to β). \end{array} $$

### b) Terms

The set $T$ of terms is built as follows.

We first define the set of atoms $A = Cu'$, where :

- $C$ is a set of constant symbols

- $V$ is a set of variable symbols

- $C_nV = \emptyset$

- every $φ$ in $A$ is given a type $τ(φ) \in T$

- for every $α$ in $T$, there is a denumerable subset $V_α$ of $V$ of variables of type $α$.

The set of terms is built from :

#### Atomic terms

If $t \in A$ and $τ(t) \in T_0$, then $t \in T$. (+)

<footnote>(+) Atoms of non-elementary type are ruled out as terms for technical convenience; equivalent terms may be built through explicit abstraction. This permits us to avoid n-conversion problems.</footnote>
## Applications

If $\phi \in A$, and $t_1, t_2, \dots, t_n \in T$, with $\tau(\phi) = (\alpha_1 x \alpha_2 x \dots x \alpha_n \to \beta)$ and $\tau(t_i) = \alpha_i$, then $t = \phi(t_1, \dots, t_n) \in T$, with $\tau(t) = \beta$.

By convention, $\phi(t_1, \dots, t_i)$, with $i<n$, stands for

$$ \lambda u_{i+1} \cdots u_n \cdot \phi(t_1, \cdots, t_i, u_{i+1}, \cdots, u_n). $$

## Abstractions

If $t \in T$, with $\tau(t) \in T_0$, and $u_1, u_2, \dots, u_n \in V$, then $t' = \lambda u_1 u_2 \cdots u_n \cdot t \in T$, with $\tau(t') = (\tau(u_1) x \cdots x \tau(u_n) \to \tau(t))$.

We note $t = t'$ iff $t$ and $t'$ are identical up to a one-one renaming of their bound variables ($\alpha$-conversion).

### Example :

Let $T_0 = \{B, I\}$. The program schema $\Sigma$ given in section 1 could be represented as the term :

$$ \lambda u \cdot Y(\lambda f x \cdot C(a(x), b(x), h(d(x), f(e(x))), u) $$

$$ \text{with} \quad C = \{C, Y\} \quad (\text{conditional and fixpoint operators}) \\ V = \{x, f, a, b, h, d, e\} $$

$$ \text{and } \tau(x) = I, \tau(a) = (I \to B), \tau(b) = \tau(d) = \tau(e) = \tau(f) = (I \to I), \\ \tau(h) = (I \times I \to I), \tau(C) = (B \times I \to I), \tau(Y) = (((I \to I) \times I \to I) \times I \to I). $$

(I stands for integers, B for booleans).

### c) Type constraints

In order to restrict ourselves to second order terms, we assume that the variable symbols in the set $V$ have their types restricted to be :

- either in $T_0$ (first-order variables)

- or of the form $(\alpha_1 x \cdots x \alpha_n \to \beta)$ with $\tau(\alpha_i) \in T_0$ (function variables).

### d) Substitutions

Let us first introduce a notation. If $t \in T$, $x_1, x_2, \dots, x_n$ are first-order variables, and $t_1, \dots, t_n$ are terms in $T$ such that $\tau(t_i) = \tau(x_i) \in T_0$, we denote by $t[x_i/t_i, 1 \le i \le n]$ the term $t$, in which every free occurrence of $x_i$ is replaced by $t_i$. (As usual, a free occurrence of $x$ is an occurrence which is not inside the scope of some $\lambda \cdots x \cdots$). It should be clear that $t[\cdots]$ is a term of the same type as $t$.

We define a *substitution pair* as a pair $\langle\phi, t\rangle$ where $\phi \in V$ and $t \in T$, in which $\tau(t) = \tau(\phi)$.
A *substitution* $\sigma$ is now defined as a finite set of substitution pairs, pertaining to a set $D(\sigma)$ of distinct variables. For every $t \in T$, we define inductively $\sigma t \in T$ by :

* if $t \in A$ : if $\exists <t, t' > \in \sigma$ then $\sigma t = t'$, otherwise $\sigma t = t$.

* if $t = \phi(t_1, \dots, t_n)$ :
  - if $\exists <\phi, \lambda x_1 \dots x_n \cdot t' > \in \sigma$ then $\sigma t = t' [x_i \setminus \sigma t_i, 1 \le i \le n]$,
  - otherwise $\sigma t = \phi(\sigma t_1, \dots, \sigma t_n)$.

* if $t = \lambda u_1 \dots u_n \cdot t'$ then $\sigma t = \lambda u_1 \dots u_n \cdot \sigma t'$

(We ignore here $\alpha$-conversion problems, and assume $u_i$ does not appear in $\sigma$).

**Example :**

If $t = f(f(x))$

and $\sigma = \{<x,A>, <f, \lambda x \cdot G(x,x)>\}$,

then we compute $\sigma t$ inside out :

$$\sigma x = A$$

$$\sigma f(x) = G(x,x) \quad [x/A] = G(A,A)$$

$$\sigma t = \sigma f(f(x)) = G(x,x) \quad [x/G(A,A)] = G(G(A,A),G(A,A)).$$

## 2.3. Program constructs expressed by second-order patterns

A program pattern is going to be a second-order term of the language $T$ defined in 2.2. Let us see some specific uses of this notation.

### a) program composition

We can readily express "black boxes" of a flowchart as functions variables of the corresponding schema, and composition of these boxes corresponds to application. For instance, the pattern $f(A(g(B)),C)$ where $A,B$ and $C$ are constants, $f$ and $g$ are function variables, matches the program while $C$ do $A(B)$ according to (among others) the substitution

`{<f,lambda·while v do u>,<g,lambda·u>}`.

### b) contexts

If we want to express as a pattern a condition such as : " a while statement containing in its body an assignment to variable $x$", then the term while $p$ do $f(x:=e)$ will not do. We want to restrict the terms substituted to
variable f to be of the form $\lambda u \cdot t$, where t contains one and only one occurrence of u. We shall introduce a new kind of variable, called a *context variable*, and use square brackets rather than parentheses: *while p do f[x:=e]*. This expresses that variable f is restricted as indicated above. The notation generalizes immediately to contexts with several arguments.

### c) scope restrictions

Block structure and scope restrictions can be expressed with the corresponding variable abstraction. For instance, we shall represent a system of recursive equations of the form:

$$ \begin{cases} f_1(x_1^1, \dots, x_{n_1}^1) & \Leftarrow t_1 \\ \vdots & \\ f_p(x_1^p, \dots, x_{n_p}^p) & \Leftarrow t_p \end{cases} $$

by the term:

$Y(\lambda f_1 \dots f_p \left< \lambda x_1^1 \dots x_n^1 \right. \left. \left< \lambda x_1^p \dots x_n^p \right. \left. t_1, \dots, t_p \right> \right)$, where Y and < > are two constants of the appropriate type, denoting respectively the fixpoint operator and cartesian product Y and < > are generic constants, whose types are determined by the context. In the following, we shall use also $\perp$ and $=$ as generic constants.

### d) segment variables for lists and associative operators

Let us indicate briefly how the associativity of the composition of monadic functions may be used to model associativity of certain operators, or to build in lists.

Given a type $\tau$, we can add a new elementary type $\bar{\tau}$, and a new constant $C^T$ of type $(\tau \bar{x} \tau \bar{\tau})$. We now represent a list $a_1, \dots, a_n$ of objects of type $\tau$ as the term of type $(\bar{\tau} \to \bar{\tau})$: $\lambda u \cdot C^T(a_1, C^T(a_2, \dots, C^T(a_n, u) \dots))$.

Note that appending lists is denoted by functional composition. We can now represent the set of lists containing the constant A as the pattern $<z_1 \dots A \dots z_2>$, where $z_1$ and $z_2$ are (segment) variables of type $(\bar{\tau} \to \bar{\tau})$. This pattern is an abbreviation for the term:

$$ \lambda u \cdot z_1 (C^T(A, z_2(u))) $$

This pattern matches the list $<A, A, B>$ in two ways:

$$ \sigma_1 \begin{cases} <z_1, \lambda u \cdot u> & \text{(the empty list< >)} \\ <z_2, \lambda u \cdot C^T(A, C^T(B, u))> & \text{(the list <A, B>)} \end{cases} $$

$$ \sigma_2 \begin{cases} <z_1, \lambda u \cdot C^T(A, u)> & \text{(the singleton list <A>)} \\ <z_2, \lambda u \cdot C^T(B, u)> & \text{(the singleton list <B>)} \end{cases} $$
e) Finally, program features such as arrays and data structures are basically functional in nature, and indexing (respectively field accessing) may be represented by function application. But the authors have not used so far this idea for representing transformations of programs manipulating structured data.

## 2.4. A complete matching algorithm for second-order terms

### a) The match preorder ≤

Let t, t' be two terms of the same type. We say that t matches t', and we note $t \le t'$, iff there exists a substitution $\sigma$ such that $t' = \sigma t$.

Let us define in the usual way the composition of two substitutions $\sigma$ and $\sigma'$:

$$ \sigma'\sigma = \{<x, \sigma' t>|<x, t>\in\sigma\} \cup \{<x, t>\in\sigma'|x \notin D(\sigma')\}. $$

We can extend the preorder $\le$ to substitutions by defining:

$$ \sigma \le \sigma' \text{ iff } \exists \rho \quad \sigma' = \rho \sigma. $$

Properties of this preorder for various logical languages are given in [8].

For t, t' terms of the same type, we define:

S is a complete set of minimal matches of $<t, t'>$ iff:

a) $\forall \sigma \in S \quad t' = \sigma t \quad \text{consistence}$

b) $\forall \sigma' \ t' = \sigma' t \Rightarrow \exists \sigma \in S \ \sigma \le \sigma' \quad \text{completeness}$

c) $\forall \sigma, \sigma' \in S \quad \sigma \neq \sigma' \Rightarrow \sigma \neq \sigma' \quad \text{minimality}$

**Example:** Let $t = f(x)$, $t' = A$. Then $\{\sigma_1, \sigma_2\}$ is a complete set of minimal matches of $<t, t>$, with:

$$ \begin{cases} \sigma_1 = \{<f, \lambda u \cdot A>\} \\ \sigma_2 = \{<f, \lambda u \cdot u>, <x, A>\} \end{cases} $$

Some other matches:

$$ \sigma_3 = \{<f, \lambda u \cdot A>, <x, B>\} $$

$$ \sigma_4 = \{<f, \lambda u \cdot A>, <y, B>\}. $$

### b) Matching trees

We shall now show how to construct a complete set $S$ of minimal matches of terms $t$ and $t'$. The method is an adaptation to second-order of a unification
algorithm for type theory described in [9].

We define trees, called matching trees, whose nodes are finite sets of pairs of terms `<t,t'>` of the same type, or the special tokens `S` for success and `F` for failure.

We first define a procedure SIMPL(N) that simplifies a node N, by recognizing common constant initial subterms :

SIMPL(N)

Loop

If N = ∅ then replace N by `S` and exit.

If N = $\overline{N}U\{<\lambda x_1...x_n \cdot \phi(t_1,...,t_p), \lambda x'_1...x'_n \cdot \phi'(t'_1,...,t'_p)>\}

with $\phi \in Cu\{x_1,...,x_n\}$ then :

i) if $\phi' = \begin{cases} \phi & \text{if } \phi \in C \\ x_i' & \text{if } \phi = x_i \end{cases}$ then
N = \overline{N}U\{<\lambda x_1...x_n \cdot t_i, \lambda x'_1...x'_n \cdot t'_i>|1 \le i \le p\}

ii) otherwise replace N by `F` and exit.

Repeat

End of SIMPL.

Matching trees for `<t,t>` are grown as follows.

1) The root node is $N_0 = SIMPL(\{<t,t>'\})$. We shall assume that $N_0$ is such that all constants appearing in it are of a type of order at most 3. That means that we authorize constants of order higher than 4 in t and t' only in a common outer context. This will be the case for our schemas, where the fourth-order constant Y appears only at the top-level.

2) Nodes `S` and `F` are leaves.

3) To grow the successors of node N, select in N an arbitrary pair : `<t₁,t₂>`. The function MATCH `<t₁,t₂>` given below returns a finite set of substitution pairs $(\sigma_1, ..., \sigma_k)$. For each of these pairs $\sigma_i$, grow an arc labeled with $\sigma_i$ from N to its successor SIMPL($\sigma_i$N). (If $k=0$, replace N by `F`).

Let us now define the algorithm MATCH :
### MATCH<t₁, t₂>.

There are two cases, according to the order of the head variable of $t_1$:

1. Order 1 : $t_1 = \lambda u_1 \cdots u_n \cdot x \quad \tau(x) \in T_0$.

Let $t_2 = \lambda v_1 \cdots v_n \cdot t'_2$. Then:

- if one of the v's appear free in $t'_2$, then $k=0$, no solutions

- otherwise $k=1$, return the unique solution $\langle x, t'_2 \rangle$.

2. Order 2 : $t_1 = \lambda u_1 \cdots u_n \cdot f(t_1^1, \dots, t_1^p)$
$t_2 = \lambda v_1 \cdots v_n \cdot \phi(t_2^1, \dots, t_2^q)$.

Remark that $\phi \in C\{v_1, \dots, v_n\}$.

We generate $k \le p+1$ solutions as follows:

a) in the case $\phi \in C$, one imitation : $\langle f, \lambda x_1 \cdots x_p \cdot \phi(\hat{t}_1, \dots, \hat{t}_q) \rangle$
where $\hat{t}_i$ is constructed as :

- if $\tau(t_2^i) \in T_0$ then $\hat{t}_i = h_i(x_1, \dots, x_p)$

- if $\tau(t_2^i) = (\alpha_1, \dots, \alpha_s \to \beta)$ then $\hat{t}_i = \lambda w_1 \cdots w_s \cdot h_i(x_1, \dots, x_p, w_1, \dots, w_s)$
  with $\tau(w_j) = \alpha_j, 1 \le j \le s$

where the $h_i$'s are new distinct variables of the appropriate type. Note that since $\phi$ is of order at most 3, $t_2^i$ is of order at most 2, whence $\alpha_j \in T_0$, and therefore the $h_i$'s are second-order variables.

b) all the projections $\langle f, \lambda x_1 \cdots x_p \cdot x_j \rangle$ that are type compatible, i.e. such that $\tau(f) = (\gamma_1 x \cdots x \gamma_p \to \delta)$ with $\delta=\gamma_j$.
end of MATCH.

**Lemma** : For all t and t', the construction of a matching tree always terminates.

**Proof** : By double induction on $\lambda+\omega\lambda'$, where

$$ \lambda = \sum \{ |t_1| \mid \langle t_1, t_2 \rangle \in N \} $$

$$ \text{and } \lambda' = \sum \{ |t_2| \mid \langle t_1, t_2 \rangle \in N \}, $$

$$ \text{with } \left\{ \begin{array}{l} |\lambda u_1 \cdots u_n \cdot \phi(t_1, \dots, t_p)| = 1 + \sum_{i=1}^n |t_i| \\ |x| = 1. \end{array} \right. $$
### c) Correctness of the method

**Definition:**

Let MT be a matching tree constructed for t and t' as defined above. We call set of solutions of MT the set $S(MT)$, of all substitutions $\sigma = \sigma_n \circ \sigma_{n-1} \circ \cdots \circ \sigma_1$ such that $\sigma_1, \sigma_2, \cdots, \sigma_n$ label a branch of MT terminated in $S$. The domain of $\sigma$ is restricted to those variables appearing free in t.

**Theorem:** For all t and t' terms of the same type built on variables of order at most 2 and constants of order at most 3 (except possibly in a common outer context), for all MT matching trees for t and t', $S(MT)$ is a complete set of minimal matches of t and t'.

**Proof:** Given in Huet [8], where various examples of matching trees are given.

Note that this proves the existence of such complete sets, which can be shown to be unique up to an isomorphism.

**Example:** Let us go back to our example template, where $\Sigma$ is represented by the term :

$$t = \lambda u \cdot Y(\lambda f x \cdot C(a(x), h(x), h(d(x), f(e(x))), u).$$

Suppose we are trying to recognize as an instance of $\Sigma$ the "reverse" program, represented by the term :

$$t' = \lambda u \cdot Y(\lambda rev x \cdot C(\text{Null}(u), \text{Nil}, \text{Append}(\text{rev}(\text{Cdr}(x)), \text{Cons}(\text{Car}(x), \text{Nil})), u).$$

Any matching tree constructed for t and t' will give us three solutions :

$$\begin{array}{l}
\rho u \sigma_1, \rho u \sigma_2 \text{ and } \rho u \sigma_3 \text{ where} \\
\rho = \{\langle a, \lambda u \cdot \text{Null}(u) \rangle, \langle h, \lambda u \cdot \text{Nil} \rangle, \langle e, \lambda u \cdot \text{Cdr}(u) \rangle\} \\
\sigma_1 = \{\langle h, \lambda xy \cdot \text{Append}(y, x) \rangle, \langle d, \lambda u \cdot \text{Cons}(\text{Car}(u), \text{Nil}) \rangle\} \\
\text{and} \\
\sigma_2 = \{\langle h, \lambda xy \cdot \text{Append}(y, \text{Cons}(x, \text{Nil})) \rangle, \langle d, \lambda u \cdot \text{Car}(u) \rangle\} \\
\sigma_3 = \{\langle h, \lambda xy \cdot \text{Append}(y, \text{Cons}(\text{Car}(x), \text{Nil})) \rangle, \langle d, \lambda u \cdot u \rangle\}
\end{array}$$

Of these, only $\rho u \sigma_1$ satisfies $\Sigma_1$; this is precisely the match we considered in section 2.1.

**Remarks:**

In the algorithm above we have supposed that the second order variables were unrestricted. For instance if we suppose $f$ to be a *context variable*,
then we accept $\sigma$ as a solution only if $f = \lambda x \cdot t$, where $x$ appears free in $t$ in just one occurrence.

The algorithm given here is general and rather efficient. However one should formulate the schemas with care to as not to get redundant solutions, for instance by using unnecessary compositions of free variables.

In certain special cases the algorithm can be speeded up. For instance, in the case of monadic functions, it may be a good idea to first check length conditions.

## 2.5. Applying transformation templates

Let $<\Sigma, \Sigma', X>$ by a transformation template, and let $P^t$ be a program which contains as a subterm. We say the template is *applicable* in $P$ at $t$ iff there exists a substitution $\sigma$ for the free variables of $\Sigma$ and $\Sigma'$ such that:

1) $t = \sigma\Sigma$

2) $M \models \sigma X$ i.e. axioms $X$ instantiated by $\sigma$ are valid in the programming language semantics $M$ (we shall make this more precise in the next section). When these two conditions are met, we say we apply the template in $P$ at $t$ by replacing in $P$ the subterm $t$ by the term $\sigma\Sigma' : P[\sigma\Sigma']$.

Let $V(\Sigma)$ be the set of free variables appearing in $\Sigma$, same for $V(\Sigma')$ and $V(X)$. We have of course $V(X) \subset V(\Sigma) \cup V(\Sigma')$.

The general method for applying a template to a program part proceeds as follows:

a) Apply the matching algorithm given in the previous section to terms $\Sigma$ and $t$. This gives a finite set of candidates of $\sigma$. However such $\sigma$'s only fix the values of the variables in $\Sigma$.

b) Complete $\sigma$ to the variables in $V(X) - V(\Sigma)$

c) Prove $\sigma X$ as explained in the next section.

d) If this succeeds, replace in the program $t$ by $\sigma\Sigma'$.

In simple examples of transformation templates such as our standard example, step b is missing since $V(X) \subset V(\Sigma)$. However in more complicated examples step b can be a bit tricky. This problem is in fact very similar to program synthesis. Let us give an example of the kind of difficulty involved.
One of the templates given in the appendix is the following :

$$ \Sigma_2 = f(x) \iff \text{if } a(x) \text{ then } b \text{ else } h(x, f(e(x))) $$

$$ \Sigma_2' = \begin{cases} f'(x) & \leftarrow g'(x,b) \\ g'(x,y) & \leftarrow \text{if } a(x) \text{ then } y \text{ else } g'(e(x),h'(y,x)) \end{cases} $$

$$ X_2 = \begin{cases} \forall x h(x,h) = h'(h,x) \\ \forall xyz h(x,h'(y,z)) = h'(h(x,y),z) \\ \forall x h(x,\perp) = \perp \end{cases} $$

It is possible for instance to recognize as an instance of $\Sigma_2$ the reverse program :

```
rev(x) <=> if Null(x) then Nil else Append(rev(Cdr(x)), Cons(Car(x),Nil)),
by using the match :
```

$$ \sigma \quad \left\{ \begin{array}{l} h' \leftarrow \lambda xy \cdot \text{Append}(y, \text{Cons}(\text{Car}(x), \text{Nil})) \\ a \leftarrow \lambda x \cdot \text{Null}(x) \\ b \leftarrow \text{Nil} \\ e \leftarrow \lambda x \cdot \text{Cdr}(x) \end{array} \right. $$

But now one must find the match for $h'$ (which does not appear in $\Sigma_2$) that will validate $X_2$. One way of doing that is to use $\sigma_{X_2}$ as match equations, using our algorithm above. For instance, using the first axiom, one wants to match $\lambda x \cdot h'(\text{Nil},x)$ with $\lambda x \cdot \text{Append}(\text{Nil},\text{Cons}(\text{Car}(x),\text{Nil}))$. One of the matches is $h' \leftarrow \lambda xy \cdot \text{Append}(\text{Nil},\text{Cons}(\text{Car}(y),x))$.

It is now easy to prove the other axioms, knowing the recursive definition of Append :

a) Append(Nil, x) = x

b) Append(Cons(x, y), z) = Cons(x, Append(y, z))

and the fact that Append is strict in its second argument.

A better way would be first to apply a) as a simplification on $X_{2,1}$, then match $h'$ in $X_{2,1}$ by: $h' \leftarrow \lambda uv \cdot \text{Cons}(\text{Car}(y),x)$, then validate $X_{2,2}$ as an instance of $h$).

One can then rewrite $\Sigma'$ in an iterative reverse program :

$$ \text{rev}(x) \iff \text{revl}(x, \text{Nil}) $$

where $\text{revl}(x,y) \iff \text{if } \text{Null}(x) \text{ then } y \text{ else } \text{revl}(\text{Cdr}(x), \text{Cons}(\text{Car}(x),y))$.
# 3. Proving transformation templates

## 3.1. Semantics of program schemes

In this section, we shall now regard a program pattern as a program schema, denoting the family of programs obtained by fixing the interpretation of the atoms appearing in it.

Our general formalism to express the semantics of such program schemas is usually known as denotational semantics (as opposed to operational semantics, which describes the deductive aspects of the programming language considered as a formal system). The foundations of this method were first investigated by the Scott-Strachey group. It is now generally recognized that this type of semantic definition is the most rigorous framework in which one can prove formally properties of programs (including termination). The formal system known as LCF [19] (Logic for Computable Functions) is an implementation of this method for typed languages, which is directly suitable for our purpose. We shall here assume an underlying proof system similar to LCF.

Let $T$ be the second-order term language over $V$ and $C$, as defined in section 2, in which we represent programs and schemas. An interpretation domain $D$ of $T$ is determined by a set of complete partial orders $D_\alpha$, one for each elementary type $\alpha$ in $T_0$. For $\alpha = (\alpha_1 \times \alpha_2 \times \cdots \times \alpha_n \to \beta)$, we define $D_\alpha$ as the set of continuous functions in $D_{\alpha_1} \times D_{\alpha_2} \times \cdots \times D_{\alpha_n} \to D_\beta$.

We then define an interpretation over $D$ as a mapping $I: A \to \bigcup_{\alpha \in T} D_\alpha$ preserving types : $I(\phi) \in D_{T(\phi)}$. The interpretation $I$ is then extended to the set $T$ of terms as a morphism. For more details, see Milner [20].

A programming language over $T$ is defined by a set $M$, (the models of the language) of interpretations. We shall here assume that $M$ is the set of interpretations that satisfy a set of LCF axioms.

In practice, these axioms express the meaning of the control structure part of the programming language, and things such as "$\perp_\alpha$ is the least element of $D_\alpha$", and so on. If $p$ is an LCF statement, then we use $M \models p$ to express the fact that $p$ is derivable in LCF from the programming language axioms. For instance, $M \models P_1 = P_2$ means that program schemes $P_1$ and $P_2$ are strongly equivalent
in any interpretation in the class M. For more information about constructing
programming language axioms, see the excellent survey by Tennent [26].

Let <Σ,Σ',X> be a transformation template. We say this template is
valid if M,X ⊑ Σ=Σ' i.e. iff in every interpretation in M that satisfies all
the axioms in X, Σ and Σ' denote the same function.

If a template is valid, then the correctness of program transformations obtained with it is easy to show :

Let P[t] be a program containing as a subterm a term t maching Σ :
t = σΣ, with σ such that M ⊢ σX. Let M' = {I|σ|IεM}. We have M'⊂M, since the
programming language axioms are supposed to be closed, i.e. do not pertain to the
free variables in the templates. Thus M' ⊑ X, and by validity of the template :

$M' \models \Sigma = \Sigma', \text{ i.e. } M \models \sigma\Sigma = \sigma\Sigma'.$

If we now assume that our semantic equivalence = is a congruence relatively to
the programming construct, i.e. if

$M \models t = t' \supset P[t] = P[t'], (*)$

which is usually the case, then we may infer

$M = P[t] = P[t'], \text{ with } t' = \sigma\Sigma';$

i.e. our schematic transformation has preserved strong equivalence.

This finishes the formal justification of the method. Our plan now
is to prove valid every transformation template before adding it to our library
of schematic transformations. These proofs can be carried out mechanically, for
instance on the LCF system implemented in Edinburgh [33]. However, it should be
stressed that this is not a trivial task : these proofs can be fairly tedious,
depending on the peculiarities of the programming language. In the next section,
we shall show the complete proof of the validity of the template given in
section 1.

For the simplicity of the exposition, we shall not prove directly
the equivalence of Σ and Σ', since in order to do that we should axiomatize the
iterative constructs used in Σ'. Rather, we shall prove the equivalence of Σ
and the recursive schema Σ'' obtained by applying McCarthy's transform on Σ'
[17].
### 3.2. A worked example

We now attempt to prove the validity of the template <Σ, Σ", X>
where :
Σ : f(x) ⇐⇒ if a(x) then b(x) else h(d(x), f(e(x))).
and Σ" is the recursive schema obtained from the iterative Σ' given in
section 1 by application of McCarthy's transformation [17] :

$$ \Sigma'' : \begin{cases} f''(x) & \Leftarrow \text{if } a(x) \text{ then } b(x) \text{ else } g''(e(x), d(x)) \\ g''(x,y) & \Leftarrow \text{if } a(x) \text{ then } h(y, b(x)) \text{ else } g''(e(x), h(y, d(x))) \end{cases} $$

The set of axioms X contains the associativity axiom for h, as expected,
but also an axiom stating that h is strict in its second argument :

$$ \begin{cases} X_a : \forall x, y, z \ h(x, h(y, z)) = h(h(x, y), z) \\ X_b : \forall x \ h(x, \bot) = \bot \end{cases} $$

(As noted before, $\bot$ is a constant always interpreted as the least element of the appropriate domain $\mathcal{D}$).

We now prove that $M, X \models \Sigma = \Sigma''$, assuming for M the usual fixpoint semantics of recursive equations [16]. Let us recall two properties that will be needed in the proof :

#### (1) (parallel) computation induction rule

Let P be a proposition, $\phi_i$ be a variable of type $\tau_i$, $F_i = \lambda f_i \cdot t_i$ be a term of type $(\tau_i \to \tau_i)$, $\bot_i$ be the least element of type $\tau_i$, and $Y_i$ be the fixpoint operator of type $((\tau_i \to \tau_i) \to \tau_i)$, for $i \le n$.

We let : $\sigma_i = \{<f_i, \phi_i>\}, \sigma_\bot = \{<f_i, \bot_i> | i \le n\}$,

$\sigma_F = \{<f_i, \sigma_i t_i> | i \le n\}$ and $\sigma_Y = \{<f_i, Y_i(F_i)> | i \le n\}$.

Our induction rule is :

$$ \frac{\sigma_{\bot} P, P \supset \sigma_{F} P}{\sigma_{Y} P} $$

For the conditions of validity of this rule (P must be an admissible pro-
position) see [16]. In the following we use the rule with n=2. Recall that we
use $\bot$ and $Y$ as generic constants, whose types are determined by the context.

(2) The "if axiom" $\forall \phi \in A, \forall n, \forall i \le n \ \forall t, t_1, \dots, t_n, t_i' \text{ of the appropriate types } t = \bot \Rightarrow \phi(t_1, \dots, t_{i-1}, \bot, t_{i+1}, \dots, t_n) = \bot \vdash \phi(t_1, \dots, t_{i-1}, \text{ if } t \text{ then } t_i \text{ else } t_i', t_{i+1}, \dots, t_n) = \text{ if } t \text{ then } \phi(\dots, t_i, \dots) \text{ else } \phi(\dots, t_i', \dots).$
Let $f = Y(F)$, where

$$F = \lambda f x. \text{ if } a(x) \text{ then } h(x) \text{ else } h(d(x), f(e(x))),$$

confusing the variable $f$ with the name of the smallest fixpoint $Y(F)$.

Similarly $g'' = Y(G'')$, with

$$G'' = \lambda g'' x y. \text{ if } a(x) \text{ then } h(y, h(x)) \text{ else } g''(e(x), h(y, d(x)))$$

and we introduce a new function $g = Y(G)$, with

$$G = \lambda g x y. \text{ if } a(x) \text{ then } h(y, h(x)) \text{ else } h(y, g(e(x), d(x))).$$

**Lemma 1 :** $\forall x,y h(x,f(y)) = g(y,x)$

*Proof:* We use computation induction in parallel on $f$ and $g$.

- base step : $h(x, \perp) = \perp$ using $X_h$

- induction step :

Assuming the lemma true for $\phi$ and $\Psi$, we prove it for $F(\phi)$ and $G(\Psi)$.

$$h(x, F(\phi)(y)) = h(x, \text{ if } a(y) \text{ then } b(y) \text{ else } h(d(y), \phi(e(y)))))$$

$$= \text{ if } a(y) \text{ then } h(x, h(y)) \text{ else } h(x, h(d(y), \phi(e(y)))))$$

using the "if axiom" and $X_h$

$$= \text{ if } a(y) \text{ then } h(x, h(y)) \text{ else } h(x, \Psi(e(y), d(y)))))$$

using the induction hypothesis

$$= G(\Psi)(y,x). \quad \Box$$

**Lemma 2 :** $\forall x,y,z h(x,g(y,z)) = g''(y,h(x,z))$

*Proof:* We use again computation induction on $g$ and $g''$

- base step : $h(x, \perp) = \perp$ using $X_h$

- induction step : we assume the lemma true for $\phi$ and $\phi''$.

$$h(x, G(\phi)(y,z)) = h(x, \text{ if } a(y) \text{ then } h(z, h(y)) \text{ else } h(z, \phi(e(y), d(y)))))$$

$$= \text{ if } a(y) \text{ then } h(x, h(z, h(y))) \text{ else } h(x, h(z, \phi(e(y), d(y)))))$$

using the "if axiom" and $X_h$.

$$= \text{ if } a(y) \text{ then } h(h(x,z), h(y)) \text{ else } h(h(x,z), \phi(e(y), d(y)))))$$

using $X_a$ twice.

$$= \text{ if } a(y) \text{ then } h(h(x,z), h(y)) \text{ else } \phi''(e(y), h(h(x,z), d(y)))))$$

using the induction hypothesis.

$$= G''(\phi'')(y, h(x,z)). \quad \Box$$
**Lemma 3 :** $\forall x, y \quad g(x,y) = g''(x,y)$

**Proof :**
$$
\begin{align*}
g(x,y) &= \mathit{if} \ a(x) \ \mathit{then} \ h(y,b(x)) \ \mathit{else} \ h(y,g(e(x),d(x))) \\
&= \mathit{if} \ a(x) \ \mathit{then} \ h(y,b(x)) \ \mathit{else} \ g''(e(x),h(y,d(x))) \\
&\qquad \text{using lemma 2.} \\
&= g''(x,y). \quad \Box
\end{align*}
$$

**Lemma 4 :** $\forall x \quad f(x) = f''(x)$

**Proof :**
$$
\begin{align*}
f(x) &= \mathit{if} \ a(x) \ \mathit{then} \ b(x) \ \mathit{else} \ h(d(x),f(e(x))) \\
&= \mathit{if} \ a(x) \ \mathit{then} \ b(x) \ \mathit{else} \ g(e(x),d(x)) \\
&\qquad \text{using lemma 1.} \\
&= \mathit{if} \ a(x) \ \mathit{then} \ b(x) \ \mathit{else} \ g''(e(x),d(x)) \\
&\qquad \text{using lemma 3.} \\
&= f''(x). \quad \Box
\end{align*}
$$

**Remark :** validity of Mc Carthy's transformation

We have now proven that $\Sigma=\Sigma''$. The validity of the template <Σ,Σ',X>
will thus be established, provided Mc Carthy's transformation preserves strong
correctness. Unfortunately this is not quite the case, since we assumed for
our recursive equations a least fixpoint semantics, whereas the usual proof of
the validity of Mc Carthy's transform [25] uses an operational semantics (in-
nermost evaluation of recursive call) which may lead to functions less defined
than by using the least-fixpoint semantics.

For instance, consider the following interpretation :

$$
\left\{
\begin{array}{l}
h = \lambda x y.y \\
a(X) = \text{false} \\
a(e(X)) = \text{true} \\
d(X) = \bot
\end{array}
\right.
\qquad \text{for some value } X
$$
then $f(X) = b(e(X)) = f''(X)$

whereas $f'(X) = \bot$ with $f'$ computed by the iterative $\Sigma'$ in section 1.

Thus, with the above method, we would only prove that Σ' [Σ" = Σ,
and therefore Σ' [Σ. (Where [ is the "less defined than" partial ordering). One
solution to this problem is to add new validity conditions, such as ∀x d(x) ≠ ⊥
in the above example, in order to preserve termination. Another solution would
be to define the semantics of iterative and recursive schemes so that McCarthy's
transformation is strongly correct. We shall not do it here for lack of space.
Some conditions on those semantics that guarantee strong correctness of the
transformation are investigated in [14].

This discussion emphasizes the necessity of presenting the semantic
definition of the language used, and the validation proof, together with
any proposed transformation template.

### 3.3. Finding and checking transformation templates

Even for the simple transformation template validated in the previous
section, the proof is rather long. Furthermore, although simple enough to
prove, the intermediate lemmas are not always easy to find. Thus we have found
convenient to have some other techniques to check ("debug") transformation
templates before attempting to prove formally their validity. It appears from
our experience that these techniques might be developed to help discovering
new templates.

The first is the "fold-unfold" method described in [17]. Let us apply
it to check the template <Σ,Σ",X>.

We have :

$$f(x) \Leftarrow \text{if } a(x) \text{ then } b(x) \text{ else } h(d(x), f(e(x)))$$

and we define ("eureka"!):

$$g''(x,y) \Leftarrow h(y,f(x))$$

So, by unfolding :

$$g''(x,y) \Leftarrow h(y, \text{if } a(x) \text{ then } b(x) \text{ else } h(d(x),f(e(x)))))$$

$$\Leftarrow \text{if } a(x) \text{ then } h(y,b(x)) \text{ else } h(y,h(d(x),f(e(x)))))$$

by the "if axiom" and $X_h$.

$$\Leftarrow \text{if } a(x) \text{ then } h(y,b(x)) \text{ else } h(h(y,d(x)),f(e(x)))$$

by axiom $X_a$.

$$\Leftarrow \text{if } a(x) \text{ then } h(y,b(x)) \text{ else } g''(e(x),h(y,d(x)))$$

by folding.

We define :

$$f''(x) \Leftarrow \text{if } a(x) \text{ then } b(x) \text{ else } g''(e(x),d(x))$$

$$\Leftarrow \text{if } a(x) \text{ then } h(x) \text{ else } h(d(x),f(e(x)))$$

by unfolding of $g''$.

$$\Leftarrow f(x) \text{ by folding of } f.$$
If this checking is carried out with computer assistance, the matching algorithm used to apply transformations to programs may be used here to perform the fold operation.

Note that this type of program manipulation, possibly guided by an analysis of the program [30], can be used to discover new transformations.

Similar program manipulations (e.g. loop unraveling) are possible for iterative languages.

The second method, best used with computer assistance, is to symbolically evaluate the two program patterns of the transformation template. Of course, equivalent arbitrary (but consistent) assumptions on the value of boolean expressions must be made for both patterns when conditionals are encountered. Then we can use the axioms of the transformation template to check the equivalence of the two symbolic expressions computed.

Applying this to our example, let us assume that for some integer n (to be chosen) we have

$$ \forall i<n \quad ae^i(x) = \text{false} \quad \text{and} \quad ae^n(x) = \text{true} $$

The term computed by $Σ$ is then

$$ E = h(d(x), h(de(x), \dots, h(de^{n-1}(x), he^n(x)), \dots)) $$

while $Σ'$ or $Σ''$ computes :

$$ E' = h(h(\dots h(d(x), de(x)), \dots, de^{n-1}(x)), he^n(x)) $$

It is easy to see that $E$ and $E'$ are equivalent, provided that $h$ is associative.

Again it should be possible to use this approach to guide the discovery of new transformations, for example along the line outlined for factorial in §1.

A close examination of the terms computed symbolically by two program schemes may give clues about the kind of induction necessary to prove their equivalence. This approach is close to the theorem proving technique used by Boyer and Moore in [0].
We have presented here 3 various methods to check and ultimately formally prove the validity of a transformation template <Σ, Σ', X>. Applying such a template in a program context P[] has been explained in 2.5. However we stress that the validity of the transformation requires our semantics to be congruent with respect to program contexts (condition (*) in 3.1). When this condition is not met, context preconditions must be added to the templates. We shall not further develop this idea in the present paper.

Let us now turn to the problem of organizing together a set of transformation templates.

# 4. Organizing transformation templates

## 4.1 Matching several templates simultaneously

Let us suppose that two templates <Σ₁, Σ'₁, X₁> and <Σ₂, Σ'₂, X₂> are such that Σ'₁ and Σ₂ are similar. It may be a good idea to try to factorize the common part of Σ₁ and Σ₂ into a term Σ, and to search first for occurrences of Σ.

This problem has a well-known solution in first-order logic : Σ is the least generalisation (i.e. glb for the preorder ≤) of the terms Σ₁ and Σ₂. Unfortunately, such a glb does not always exist in second-order logic, even for monadic terms, as shown in [8]. We would have therefore to content ourselves with some lower bound of Σ₁ and Σ₂ (in general of a set of Σ'₁'s).

Another problem occurs when in a certain context two distinct transformations are available, leading to two different programs. Then either the user of the system is asked to validate transformations one by one, and he chooses the one he prefers, or some preference ordering is used.

More generally, the application of a transformation at some point may prevent some other transformation in an inside or outside context. The effect of a set of transformation templates may therefore differ whether one adopts an outside-in or an inside-out search. These are well known problems for rewriting systems. In some cases it will be possible to prove nice properties of our sets of templates such as confluence (or Church-Rosser property). Non-confluent systems may be made confluent by trying to apply closure algorithms, along the lines of the Knuth-Bendix superposition algorithm. Although
Define $\sigma_1 = \sigma_{2\circ T}$; since $T_1 \le T_2$ we have also
$$ \begin{cases} t = \sigma_1 \sigma_1 \\ t' = \sigma_1 \sigma_1' \end{cases} $$

Let $M' = \{I \circ \sigma_2 | I \in M\}$

$M' \models X_2$, but since $M' \not\models M$ (see §3.1)

$$M' \models X_2 \supset \tau X_1$$

so $M' \models \tau X_1$, i.e. $M' \models (\sigma_{2\circ T})X_1$ or $M' \not\models \sigma_1 X_1$

Therefore $t' \in T_1(t)$. $\square$

### c) Application to template library organization

We can apply the proposition above to the cleaning-up of a template library. If the library contains $T_1$ and $T_2$ such that $T_1 \le T_2$, we can eliminate $T_2$ because it does not add any extra transformational power.

Such redundancy is easily detected in practice by applying to $T_2$, and with the library minus $T_2$, the same matching algorithm that we use to transform programs.

In fact, since transformations can often be composed (i.e. applied in succession), we can detect with this method the subsumption of a transformation by the composition of some others.

As an example, we will establish that the template $T_{3.3}$ is redundant with another one $T_{1.2}$ (the indexes refers to the template organization in [2]).

$T_{1.2} = \langle \Sigma_{1.2}, \sigma_1', \Sigma_{1.2}', \chi_{1.2} \rangle$ where

$\Sigma_{1.2} : f(x) \iff \text{if } a(x) \text{ then } b \text{ else } h(d(x), f(e(x)))$

$\Sigma_{1.2} : \text{function } f(x) ;$

```
begin
```

```
f:=b;
```

```
while not a(x) do
```

```
begin
```

```
f:=h(d(x),f);
```

```
x:=e(x);
```

```
end;
```

```
end;
```
$$ X_{1.2} : \begin{cases} X_{1.2,a} : \forall x,y,z h(x,h(y,z)) = h(y,h(x,z)) \\ X_{1.2,b} : \forall x h(x,\perp) = \perp \end{cases} $$

and

$$ T_{3.3} = <\Sigma_{3.3}, \Sigma'_{3.3}, \chi_{3.3}> \quad \text{where} $$

$$ \Sigma_{3.3} : f(x) \iff \begin{array}{l} \text{if } a(x) \text{ then } h \text{ else } h(f(d(x)), f(d(x))) \\ \text{function } f(x); \\ \text{begin} \\ f:=b; \\ \text{while not } a(x) \text{ do} \\ \quad \text{begin} \\ \quad \quad f:=h(f,f); \\ \quad \quad x:=d(x); \\ \quad \quad \text{end}; \\ \text{end} \\ \end{array} $$

$$ X_{3.3} : \begin{cases} X_{3.3,a} : h(\perp,\perp) = \perp \\ X_{3.3,b} : h(\perp,\perp) = \perp \end{cases} $$

We leave it to the reader to show that the substitution $\sigma$ below is such that $T_{1.2} \le T_{3.3}$:

$$ \sigma = \{ \langle h, \lambda u \cdot h(v,v) \rangle, \langle e, \lambda u \cdot d(u) \rangle \} $$

Therefore, $T_{3.3}$ can be removed from the template library. In fact, four templates out of the ten presented in [2] can be removed in the same way.

We should however emphasize that it is only because our matching is complete that we can eliminate redundant templates. Going back to the proof of the underlying proposition $b$), we see that it is only the completeness of the matching algorithm that guarantees that, if it finds the match $t = \sigma_2 \Sigma_2$, it can also find the match $t = (\sigma_2 \sigma \tau) \Sigma_1$.

### d) Application to template simplification

Let us consider again the template $T_2 = <\Sigma_2, \Sigma'_2, \chi_2>$ mentioned in 2.5. Actually, the template that was originally discovered was the slightly more
complicated $\hat{T}_2 = \langle \hat{\Sigma}_2, \hat{\Sigma}'_2, \hat{X}_2 \rangle$ where :

$\hat{\Sigma}_2 : f(x) \Leftarrow if a(x) then b else h(d(x), f(e(x)))$

$\hat{\Sigma}'_2 : \begin{cases} f'(x) & \Leftarrow g'(x, b) \\ g'(x, y) & \Leftarrow if a(x) then b else g'(e(x), h'(y, d(x))) \end{cases}$

$\hat{X}_2 : \begin{cases} \hat{X}_{2,a} : \forall x h(x,b) = h'(b,x) \\ \hat{X}_{2,b} : \forall x, y, z h(x,h'(y,z)) = h'(h(x,y),z) \\ \hat{X}_{2,c} : \forall x h(x,\perp) = \perp \end{cases}$

The reader can easily check that $T_2 \le \hat{T}_2$ and $\hat{T}_2 \le T_2$ where $\sigma = \{ \langle h, \lambda x \cdot h(d(x), y) \rangle, \langle h', \lambda x \cdot h'(x, d(y)) \rangle \}$

and $\tau = \{ \langle d, \lambda x \cdot x \rangle \}$.

The two templates $T_2$ and $\hat{T}_2$ being equivalent as to their effect, we should choose on some other criterion the one we will keep. This criterion will be simplicity of application.

Let us try to apply $T_2$ and $\hat{T}_2$ to the same program defining the list reversal function :

$\text{rev}(x) \Leftarrow if \ \text{Null}(x) \ \text{then} \ \text{Nil} \ \text{else} \ \text{Append}(\text{rev}(\text{Cdr}(x)), \text{Cons}(\text{Car}(x), \text{Nil})).$

A match with $\Sigma_2$ gives the unique substitution

$\sigma = \{ \langle a, \lambda x \cdot \text{Null}(x) \rangle, \langle b, \text{Nil} \rangle, \langle e, \lambda x \cdot \text{Cdr}(x) \rangle, \langle h, \lambda xy \cdot \text{Append}(y, \text{Cons}(\text{Car}(x), \text{Nil})) \rangle \}$

which will eventually lead to a transformation (see 2.5).

A match with $\hat{\Sigma}_2$ gives three solutions (see 2.4) :

$\tau \cup \tau_1, \tau \cup \tau_2$ and $\tau \cup \tau_3$ where

$\tau = \{ \langle \bar{a}, \lambda x \cdot \text{Null}(x) \rangle, \langle \bar{b}, \text{Nil} \rangle, \langle \bar{e}, \lambda x \cdot \text{Cdr}(x) \rangle \}$

$\tau_1 = \{ \langle h, \lambda xy \cdot \text{Append}(y, x) \rangle, \langle d, \lambda x \cdot \text{Cons}(\text{Car}(x), \text{Nil}) \rangle \}$

$\tau_2 = \{ \langle h, \lambda xy \cdot \text{Append}(y, \text{Cons}(x, \text{Nil})) \rangle, \langle d, \lambda x \cdot \text{Car}(x) \rangle \}$

$\tau_3 = \{ \langle h, \lambda xy \cdot \text{Append}(y, \text{Cons}(\text{Car}(x), \text{Nil})) \rangle, \langle d, \lambda x \cdot x \rangle \}$

All three matches satisfy $\hat{X}_2$, with a proper choice of $h'$, and thus lead to a solution.

Since $T_2 \le \hat{T}_2$, the solution has to be the same unique one given by $T_2$ for all three matches of $\hat{T}_2$.
Without going into details, we can note that the matching algorithm
will have more computation to perform to find 3 substitutions instead of one.
Furthermore, if our transformation algorithm tries all possible transforma-
tions rather than stopping after the first success, $\hat{T}_2$ will cause it to do
three times as much work as $T_2$, for the same result.

In short, the (apparently) increased degree of freedom brought in
the template by the extra free variable $d$ will cause greater non determinism
(more choices), thus more inefficiency, in the computations without giving
better results.

Given two equivalent templates, it seems to be a good rule to keep
in the template library the one having the smallest number of free variables,
e.g. $T_2$ in our example.

It is worth noting that this situation arises fairly often since one
way of generalizing an already validated template is by trying to introduce
new free variables without increasing (too much) the axiomatic constraints.

### 4.3. Focusing on interesting parts of a program

In general, one will want to use program transformations in order
to achieve specific goals, such as optimization of computing time.

A system for applying program transformations should therefore as-
sociate with the templates some indication on their effects on various cost
parameters. It is also desirable to analyse the program under consideration to
identify the critical parameters associated with a given program context. The
system will then try to apply the templates that improve those parameters. For
instance, it will try time-saving transformations to innermost loops, and
space saving ones to the least used program segments.

We shall not deal with this kind of problems here, and we refer the
interested reader to [12], [21], [29].
## 5. More general program transformations

It is possible to generalize the program transformation method presented above in several ways. First, it may be possible to enrich the schema language, and still have a complete match algorithm. However, it is known for instance, that it is not possible to find a complete finite set of matches for arbitrary third-order terms [8].

Another interesting extension would be to use information given in the axioms to help the match algorithm. For instance, if we know that some operator is associative, we know how to do the match modulo associativity of this operator. Some specialized match algorithms exist already in pattern-matching oriented programming languages for artificial intelligence [31], [32].

More generally, one may imagine specialized match algorithms that recognize specific families of program constructs. This is the approach we are currently investigating in the MENTOR project at IRIA. The idea is to use as a programming language the command language of a structured editor [5], and to write specialized programs to match complex schemes, and in case of success to effect the corresponding transformation. For instance, we implemented with this technique the recursion removal technique that consists in removing terminal recursions (i.e. doing the inverse of McCarthy's transformation).
As an illustration, we show the effect of this transformation on a (real) Pascal program :

procedure RECSAVE(CP:SPTRG);
begin
  if F11nil then
  begin
    with P1 do
    begin
      SAUVEFILED(11,01:45);
      Care A11T1Y nil
    end; beg11
    C1011 nil
  end; end;
  SAUECOM(CP);
  end .CAS 02;
1: begin
  if F11nil then # else #
    PUT(SAUVEFILE);
    SAUECOM(CP);
    RECSAVE(CP);
    end .CAS 1%
2: begin
if F21nil then # else #;
if F22nil then #;
PUT(SAUVEFILE);
SAVECON(P);
RECSAVE(F21);
RECSAVE(F22);
end %CAS 2%;
3: begin
if F31nil then # else #;
if F32nil then #;
if F33nil then #;
PUT(SAUVEFILE);
SAVECON(P);
RECSAVE(F31);
RECSAVE(F32);
RECSAVE(F33);
end %CAS 3%;
end %ARTIT%;
end %WITH%;
end %P#HIL%;
end %RECSAVE%

The symbols '#' are standard abbreviation signs in our system (the
full procedure would be two pages long). After the transformation is performed
here is the resulting program :

procedure RECSAVE(P:SPTR): label
1;
begin
1: if Pnil then
  begin
  with P do
  begin
    SAUVEFILE(S,01):=5;
    case ART: 0 not
    of
      G: begin
        G := G;
        # nil # nil # nil
      end;
      U: LAST 5%;
      S/P/M/P:
      end; (CAS 0%)
    end;
    begin
      if F11nil then # else #;
      PUT(SAUVEFILE);
      SAVECON(P);
      G:=F11;
      goto 1;
    end %CAS 1%;
  end
end
2: begin
   of F21=Nil then # else #;
   if F22#nil then #;
   PUT(SAUVEFILE);
   SAVECOM(P);
   RECSAVE(F21);
   P:=F22;
   goto 1;
end %CAS 2%

3: begin
   if F31=Nil then # else #;
   if F32#nil then #;
   if F33#nil then #;
   PUT(SAUVEFILE);
   SAVECOM(P);
   RECSAVE(F31);
   RECSAVE(F32);
   P:=F33;
   goto 1;
end %CAS 3%;
end %ARITY%;
end %WITH%;
end %WITHU%;
end %RECSAVE%;

This technique is very general and more powerful than schematic rewriting. We believe that it may be used for instance to implement Cohen's recursion removal transformations [39]. However the formal proof of correctness of such transformations is a much harder problem than correctness of schematic rewritings.
## Conclusion

We have presented in this paper a program transformation technique based on rewriting program schemas written in a 2nd order term language. We have given a complete matching algorithm for this language and have shown how to formally validate such transformations, using denotational semantics.

This technique can be completely automated, and made part of the "program massagers" or "assistant programmers" that are now under development in various places [3], [15], [24]. The MENTOR project at IRJA [10] is part of this effort. These systems, in which knowledge about programming is organized in various ways, seem to be among the most promising applications of artificial intelligence techniques.
# Appendix

## A library of recursion removal templates

We now present a small library of recursion removal templates. However, to keep them short we have expressed the second patterns of those templates as recursive equations with only "tail-recursion", i.e. readily transformable into iterative patterns by a straightforward application of the reverse Mc Carthy transformation (see [17]).

All these templates have been proved valid, but because of space limitations the proofs will be published later [13]. Proof of weak correctness for some of these templates may be found in [35].

These patterns have varied origins. Some were taken in [2], and sometimes generalized. Some were obtained by abstracting patterns from examples of known equivalent programs. Some were useful intermediary steps appearing in the validation proof of other templates.

- $T_1 = <\Sigma_1, \Sigma'_1 X_1>$ where

$$ \Sigma_1 : f(x) \iff \text{if } a(x) \text{ then } b(x) \text{ else } h(d(x), f(e(x))) $$

$$ \Sigma'_1 : \begin{cases} f'(x) & \iff \text{if } a(x) \text{ then } b(x) \text{ else } g'(e(x), d(x)) \\ g'(x,y) & \iff \text{if } a(x) \text{ then } h(y, b(x)) \text{ else } g'(e(x), h'(y, d(x))) \end{cases} $$

$$ X_1 : \begin{cases} \forall x, y, z & h(x, h(y, z)) = h(h'(x, y), z) \\ \forall x & h(x, \perp) = \perp \end{cases} $$

- $T_2 = <\Sigma_2, \Sigma'_2, X_2>$ where

$$ \Sigma_2 : f(x) \iff \text{if } a(x) \text{ then } b \text{ else } h(x, f(e(x))) $$

$$ \Sigma'_2 : \begin{cases} f'(x) & \iff g'(x, \perp) \\ g'(x, y) & \iff \text{if } a(x) \text{ then } y \text{ else } g'(e(x), h'(y, x)) \end{cases} $$

$$ X_2 : \begin{cases} \forall x & h(x, b) = h'(b, x) \\ \forall x, y, z & h(x, h'(y, z)) = h'(h(x, y), z) \\ \forall x & h(x, \perp) = \perp \end{cases} $$
$$- T_3 = <\Sigma_3, \Sigma'_3, X_3> \text{ where}$$

$$\Sigma_3 : f(x) \iff \text{if } a(x) \text{ then } b(x) \text{ else } h(x, f(e(x)))$$

$$\Sigma'_3 : \begin{cases} f'(x) \iff g'(a, b, x) \\ g'(x, y, z) \iff \text{if } x=z \text{ then } y \text{ else } g'(e'(x), h(e'(x), y), z) \end{cases}$$

$$X_3 : \begin{cases} \forall x \ e'(e(x)) = x \land e(e'(x)) = x \\ \forall x \ h(x, \perp) = \perp \end{cases}$$

$$- T_4 = <\Sigma_4, \Sigma'_4, X_4> \text{ where}$$

$$\Sigma_4 : f(x) \iff \begin{cases} \text{if } a(x) \text{ then } h(x) \text{ else } h(f(d(x)), f(d(x))). \\ \text{(the "Fibonacci scheme")} \end{cases}$$

$$\Sigma'_4 : \begin{cases} f'(x) \iff g'(x, b, b) \\ g'(x, y, z) \iff \text{if } a(x) \text{ then } y \text{ else } g(d(x), h(z, y), y) \end{cases}$$

$$X_4 : \begin{cases} \forall x (\neg a(x) \land a(d(x))) \lor a(d(d(x))) \\ \forall x \ h(x, \perp) = \perp \end{cases}$$

$$- T_5 = <\Sigma_5, \Sigma'_5, X_5> \text{ where}$$

$$\Sigma_5 : f(x, y) \iff \text{if } a(x) \text{ then } h(x, y) \text{ else } h(y, f(c(x), d(x)))$$

$$\Sigma'_5 : f'(x, y) \iff \text{if } a(x) \text{ then } h(x, y) \text{ else } f'(c(x), h'(y, d(x)))$$

$$X_5 : \begin{cases} \forall x, y, z \ h(x, h(y, z)) = h(h'(x, y), z) \\ \forall x, y, z \ h(x, b(y, z)) = h(y, h'(x, z)) \\ \forall x \ h(x, \perp) = \perp \end{cases}$$

$$- T_6 = <\Sigma_6, \Sigma'_6, X_6> \text{ where}$$

$$\Sigma_6 : f(x, y) \iff \text{if } a(x) \text{ then } h(x, y) \text{ else } h(x, f(e(x), y))$$

$$\Sigma'_6 : f'(x, y) \iff \text{if } a(x) \text{ then } h(x, y) \text{ else } f'(e(x), h'(x, y))$$

$$X_6 : \begin{cases} \forall x, y, z \ h(x, h(y, z)) = h(y, h(x, z)) \\ \forall x, y, z \ h(x, h(y, z)) = h(y, h'(x, z)) \\ \forall x \ h(x, \perp) = \perp \end{cases} (+)$$

<footnote>(+) It is also possible to replace this axiom with the corresponding one for $h'$.</footnote>
References :

[0] B. Boyer, J. Moore "Proving theorems about LISP functions" JACM 22,1 Jan 75, pp 129-144.

[1] R. Burstall, J. Darlington "Some Transformations for Developing Recursive Programs". Proceedings International Conference on Reliable Software. Los Angeles, California, 1975. Also JACM 24,1 Jan. 77.

[2] J. Darlington, *A Semantic Approach to Automatic Program Improvement*, Ph.D. Thesis, Dept. of Machine Intelligence, University of Edinburgh, (1972).

[3] J. Darlington & R. Burstall, "A System which Automatically Improves Programs", Proceeding of the third International Joint Conference on Artificial Intelligence, (1973), Stanford, Cal. pp. 479-484. Also Acta Informatica, 1976.

[4] N. Dershowitz & Z. Manna "The evolution of programs : a system for automatic program modification". Proceedings of 4th POPL Conference, Los Angeles 1977.

[5] V. Donzeau-Gouge et al. "A structure-oriented program editor : a first step towards computer assisted programming". Proceedings of ICS 75, Antibes, France.

[6] S. Gerhart. "Correctness preserving program transformations". Proceedings of 2nd POPL Conference, Palo Alto 1975.

[7] S. Gerhart. "Knowledge about programs : a model and case study". Proc of Intern. Conf. on Reliable Software, Los Angeles 75.

[8] G. Huet, "Résolution d'Equations dans des Langages d'ordre 1,2,...,ω" Thèse d'Etat, 1976.

[9] G. Huet "A unification algorithm for typed λ-calculus" Theoretical Computer Science 1,1 June 1975 pp.27-58.

[10] G. Huet, G. Kahn et al. "The MENTOR program transformation system" Rapport Laboria, in preparation.

[11] D. Knuth & P. Bendix "Simple word problems in universal algebras" in Computational problems in abstract algebra. Ed. by J. Leech, Pergamon Press 1969.

[12] D. Knuth & P. Stevenson"Optimal measurement points for program frequency counts". BIT 13(1973) pp.313-322.

[13] B. Lang, "Quelques transformations éliminant la récursion et leur preuve" Rapport Laboria, in preparation.
[14] B. Lang, "Threshold Evaluation and the Semantics of Call by Name, Assignment and Generic Procedures", Proceeding of Fourth Conf. on Principles of Prog. Lang., Los Angeles, 77.

[15] D.B. Loveman, "Program Improvement by source-to-source transformation", JACM, 24,1 (Jan. 77), pp.121-145.

[16] Z. Manna, S. Ness, J. Vuillemin, "Inductive Methods for Proving Properties of Programs". Comm. ACM, Vol 15,n°7, 1972.

[17] J. McCarthy, "Recursive functions of symbolic expressions and their computation by machine" Part I, CACM Vol3 (1960) pp.184-204.

[18] R.E. Milne & C. Strachey, "A theory of Programming language semantics". Chapman & Hall, London.; Wiley, New-York, 1976.

[19] R. Milner, "Implementation and Applications of Scott's Logic for Computable Functions", Proc. ACM Conference on Proving Assertions about Programs, Les Cruces, New-Mexico, 1972.

[20] R. Milner, "Models of LCF". Stanford Artificial Intelligence Laboratory Memo AIM-186, January 73.

[21] B. Mont-Reynault: Forthcoming Ph.D. thesis, Stanford University.

[22] M. Paterson, C. Hewitt, "Comparative Schematology", Record of Project MAC Conference on Concurrent Systems and Parallel Computations, ACM, New Jersey, 1970, p.119-128.

[23] T.A. Standish, D.C. Harriman, D.F. Kibler and J.M. Neighbors. "The Irvine program transformation catalogue". Dept. Inform. and Computer Science, U. Of California at Irvine, Irvine, Calif., Jan. 1976.

[24] T.A. Standish, D.C. Harriman, D.F. Kibler, and J.M. Neighbors. "Improving and refining programs by program manipulation". Proc. 1976 ACM Annual Conf., Oct. 20-22 1976, pp-509-516.

[25] R. Strong, "Translating Recursion Equations into Flow Charts", Journal of Computer and System Sciences, vol. 5, n°3, (June 1971).

[26] R.D. Tennent, "The denotational semantics of programming languages", CACM 19,8 Aug 76, pp. 437-453.

[27] J. Vuillemin, "Syntacte, Sémantique et Automatique d'un langage de Prograngement simple". These de Doctorat ès-sciences Mathematiques Université de Paris VI, Paris, (1974).

[28] S.A. Walker and H.P. Strong, "Characterizations of Flowchartable Recursions", Journal of Computer and System Sciences, Vol 7, pp.404-447, (1973).
[29] B. Wegbreit, "Mechanical program analysis", CACM 18,9 (Sept. 75) pp. 528-539.

[30] B. Wegbreit, "Goal-directed program transformation": IEEE, Trans on Software Frg. 2,2 (June 76) pp 69-80.

[31] R. Roboh & E. Sacerdoti, Q.LISP Reference manual. Technical Note 81, SPI, Aug 73.

[32] M. Stickel, Forthcoming Ph.D. thesis, Carnegie Mellon University.

[33] M. Gordon, R. Milner & C. Wadsworth
Edinburgh LCF
private communication.

[34] G. Huet
Confluent reductions : abstract properties and
application to term rewriting systems
FOCS conference 1977.

[35] D.C. Cooper, "The equivalence of certain computations",
Computer Journal 9 (1966) pp.45-52.

[36] R. Steinbrüggen, "Equivalent recursive definitions of certain
number theoretical functions". Technical Report INFO-7714
(June 77), Technische Universität Munchen.

[37] A.K. Chandra, "Efficient compilation of linear recursive programs".
Res.Rep CS-72-282, Stanford University, 1972.

[38] R.S. Bird, "Notes of recursion elimination",
CACM 20 (1977) pp. 434-439.

[39] N.H. Cohen, "Mechanical analysis and restructuring of recursive
programs", Internal report,
Harvard University (May 1976).