2.1. Input Language

Our input language is a first-order functional language shown in Figure 1. A program is a function definition which can be self-recursive. A function definition is composed of a function name and alternatives and each alternative is composed of a formal parameter pattern and a function body. In the function body, labels are attached to all subexpressions and variable patterns for identification.

Figure 1: Syntax of Input Language

In functional languages, data collections are declared using algebraic data types which have recursive structures. In this paper, we restrict them as follows.

$$\begin{array}{lcl} {\tt d}{\tt atatype}~{\mathit rtype} &... ...hit rtype}^{1} * \ldots * {\mathit rtype}^{r_m} \\ \end{array}$$

$C_i$'s are data constructors, which build new values belonging to the new data type ${\mathit rtype}$. ${\mathit rtype}$ is recursive because its data constructors use arguments of ${\mathit rtype}$. In this paper, we assume that a data constructor $C_i$ uses one non-recursive argument of $t_i$ type and $r_i$ recursive arguments($0 \le r_i$). This is not a real limitation because $t_i$ can be a tuple type. Given a value $C_i(v,rv_1,\ldots,rv_{r_i})$ of ${\mathit rtype}$, we will refer $v$ as non-recursive field and $rv_j$ as recursive field.