January 27, 1995 1

Compilation of Id^{−}: A Subset of Id ^{∗}

Zena M. Ariola Aiken Computational Laboratory Harvard University

Arvind Laboratory for Computer Science Massachusetts Institute of Technology

January 27, 1995

Abstract

Compilation of Id, a higher-order non-strict functional language augmented with Istructures, is described in terms of two languages. The first language is called Kid, which is a Kernel language for Id. Kid is further translated into a language where all Kid data structures and functions are represented using only one data structure. This second language is called P-TAC for Parallel Three Address Code. The operational semantics of both Kid and P-TAC are presented in terms of two contextual reduction systems. Formalization of many commonly known optimizations is also presented in the contextual reduction framework.

Keywords and phrases: Term Rewriting Systems, Contextual Reduction Systems, Dataflow, Functional Languages, I-structures, Compiler Optimizations.

∗This technical report is created by merging CGS memo 315 (dated November 1 1990) and CSG memo 322 (dated December 10 1990)

1 Introduction

Figure 1: Compilation scheme

We describe the compilation of Id^{−}, a subset of the Id language, in terms of successive translations into different languages. Each of the successive languages has a precise operational semantics, which is given in terms of rewrite rules. The compilation scheme is shown in Figure 1. Id^{−} does not contain the following features of Id:

abstract types and algebraic types except lists;

overloading;

mutable structures.

Id^{−} is first parsed into de-sugared Id^{−}, where enough parentheses are inserted to make operator associativity and precedence irrelevant. Desugared Id^{−} also does not contain patterns in function definitions. During the de-sugaring phase list-comprehensions and array-comprehensions are transformed into nested loops. We will informally describe this phase in the next Section.

In the next phase de-sugared Id^{−} is translated into Kid, the Kernel language for Id. Kid is a subset of Id except for the notion of multiple values which have been inspired by dataflow graphs. Essentially a Kid program contains only primitive patterns and simple expressions. The Kid syntax and operational semantics are given in Section 3. The translation from de-sugared Id^{−} to Kid, including the compilation of complex patterns into primitive patterns, is described in Section 4.

Kid serves several purposes. Since Id is too complex to be given direct operational semantics, it is preferable first to give a translation of Id into a smaller language such as Kid. Thus, Id is defined indirectly in terms of the rewrite rule semantics of Kid. Kid is also the intermediate language in which a large number of architecture independent compiler optimizations are performed. These optimizations are described in Section 7.1. We think that many other types of analyses such as Milner style type checking, or abstract interpretation for storage reclamation should be performed at the Kid level. These analyses are not described in this document.

An implementation method that is preferred by many researchers eliminates explicit environments containing the value of free variables of a function. This requires applying a program transformation known as lambda-lifting. Lambda-lifting involves two steps: first, all nested function definitions (λ-expressions) of a Kid program are “closed” by turning their free variables into parameters. In the second step, all closed definitions are lifted to the top level. Lambda-lifting should be done after optimizations have been performed on Kid programs. There are many algorithms for doing lambda-lifting and we do not describe any of them in this document. Interested reader is referred to Johnsson’s paper [14].

The next step is to translate a lambda-lifted Kid program into P-TAC [1], which is a much smaller language than Kid. This translation calls for choosing a machine representation for each type of Kid value and thus, involves many low level efficiency issues. P-TAC and its operational semantics are given in Section 8.1. A translation from Kid into P-TAC is given in Section 9. We end the document by showing in Section 10 how a P-TAC program is extended with Signals [7] which are needed to detect termination and for resource management.

Our compiling approach allows the formalization of questions related to correctness [1]. For example, it will make sense to talk about the correctness of lambda-lifting, or the correctness of the translation from Kid to P-TAC. Moreover, since there exists an independent operational semantics of Id^{−} in terms of a even smaller subset of kernel Id [12], it may be possible to prove the correctness of the translation between de-sugared Id^{−} and Kid. Another advantage of our approach is that we are able to delay the introduction of concepts tied to specific machines or even to the dataflow computation model until we actually generate machine code. However, in this document we do not go below the P-TAC level.

2 Desugared Id^{−}

The syntax of de-sugared Id^{−} is described in Figure 2. As can be seen from the grammar, de-sugared Id is fully parenthesized and thus has no operator precedence. Thus, an Id expression like

            (f x) : map f xs

becomes

            ((f x):((map f) xs))

Id has curried versions of infix binary operators which are written by enclosing the operator in parenthesis. Thus, (+) represents the curried +, and it makes sense to write ((+) 2) in Id. In de-sugared Id^{−} we treat the curried version of an operator as a constant, which has a standard function definition associated with it. For the sake of symmetry we have also included curried versions of all unary operators in de-sugared Id^{−}.

During the de-sugaring phase multi-clause functions, are turned into equivalent case expressions, as shown in the example below

UOP ∈ Unary Operator
BOP ∈ Binary Operator
E  ∈ Expression
P  ∈ Pattern
V ariable ::= x | y | z | ⋯ | a | b | ⋯ | f | ⋯ | x_{1} | ⋯ | F | G | ⋯
Constant ::= Integer | Boolean | () | Nil | (Not) | ⋯ | (+) | (−) | ⋯ | Make nD array
UOP  ::= Negate | Not | nD Bounds | I nD array | Open cons
BOP  ::= + | − | ∗ | ⋯ | == | Eq? | < | ⋯ | And | :
E  ::= V ariable | Next V ariable | Constant

| (UOP E) | (E BOP E) | (E E) | E[E] | E.cons 1 | E.cons 2

| (E, E) | (E, E, E) | ⋯

| (If E then E else E) | {Case E of Clause [ | Clause]^{∗} }

| {While E do [Statement; ]^{∗} Finally E}

| {For V ariable ← E to E step E do [Statement; ]^{∗} Finally E} | \{Fun [V ariables]^{∗} = E\} | \{\underline{Fun} [V ariables]^{∗} = E\}

| Block
Block  ::= {[Statement; ]^{∗} In E}
Statement ::= Binding | Command
Binding ::= P = E
Command ::= E[E] = E | E.cons 1 = E | E.cons 2 = E
Clause  ::= P = E
P  ::= Nil | V ariable | Next V ariable | (P, P) | (P, P, P) | ⋯ | (P : P)
P rogram ::= Block

Figure 2: Grammar of de-sugared Id^{−}

           Def map f Nil  = Nil
            |  map f x:xs = (f x) : map f xs;

becomes

           Def map  t1 t2 = { Case (t1, t2)   of
                                |  (f,  Nil)  = Nil
                                |  (f,  x:xs) = (f x) : map f xs }

where t1 and t2 are new variables. Furthermore, all function definitions are turned into λ - expressions.

          map =  { Fun t1 t2 = { Case (t1, t2)   of
                                   |  (f,  Nil)  = Nil
                                   |  (f,  x:xs) = (f x) : map f xs } }

If the Id function is defined as substitutable (Defsubst) then the corresponding λ-expression (\underline{Fun}) is underlined. The “underlined” λ-expressions are then expanded in line during optimizations (see Section 7.1 ).

The most complex part of the de-sugaring phase is the transformation of comprehensions into loops. This is described in detail in [9]. Here we only illustrate the idea using the following example:

           {: e || x <- xs ; y <- ys}

A typical translation of this list-comprehension is given in terms of nested map-list operations followed by a list flattening operation [13]. In Id we make use of “open lists”, a type of I-structure, to generate a tail recursive program. Basically, in the following program, a open list (signified by h in the inner loop) is generated for each element of xs and then these open lists are “glued” together in the outer loop.

           { h1  =  Open_cons ();
             hn  = { For x <- xs do
                      Next h1 =
                         { Case ys of
                            | Nil = h1
                            | y:yss =
                                 { h =  Open_cons ();
                                   h1.cons_2 = h.cons_2;
                                  In { For y <- ys do
                                         t  = Open_cons ();
                                         t.cons_1 = e;
                                         h.cons_2 = t;
                                         Next h = t;
                                      Finally h }}};
                     Finally h1 };
             hn.cons_2 = Nil;
            In h1.cons_2 }

The above translation is correct if we treat open lists and lists as the same type. However, there are several subtle issues regarding type checking that are still not resolved.

3 Kid : The Kernel Id Language

Id is a high level functional language [10] augmented with a novel data structuring facility known as I-structures [3]. Id, like most modern functional languages, is non-strict, and has higher-order functions and a Milner-style type system. It also has a fairly large syntax to express currying, loops, list and array comprehensions, and pattern matching for all algebraic types. We have found it difficult to give direct operational semantics of Id because of its syntactic complexities. Kid, a kernel language for Id, has been developed to give precise (though indirect) operational semantics of Id. Kid has also proved to be an extremely useful intermediate language for the Id compiler [2]. Within the compiler,

MV  ∈ Multiple Variable
SE  ∈ Simple Expression
PF i_{m}  ∈ Primitive Function with i arguments and m outputs
Ap E_{m}  ∈ Applicative Expression with m outputs
Case E_{m} ∈ Case Expression with m outputs
Loop E_{m} ∈ Loop Expression with m outputs
lambda E ∈ Lambda Expression
E m  ∈ Expression with m outputs

V ariable ::= x | y | z | ⋯ | a | b | ⋯ | f | ⋯ | x_{1} | ⋯
MV_{m}  ::= \underbrace{V ariable, ⋯, V ariable}_{m}
Constant ::= Integer | Boolean | () | (Not) | ⋯ | (+) | (−) | ⋯

| Nil | Make nD array | Error | ⊤

SE  ::= V ariable | Constant
SE_{m}  ::= \underbrace{SE, ⋯, SE}_{m} | SE, SE_{m−1} | SE, SE, SE_{m−2} | ⋯
PF 1_{1}  ::= Negate | Not | nD Bounds | I nD array | Open cons | Cons 1 | Cons 2
PF 1_{m}  ::= Detuplem
PF 2_{1}  ::= + | − | ∗ | ⋯ | Equal? | Eq? | < | ⋯ | And | Cons | Apply

| P nD select | Make tuple2

PF N_{1}  ::= Make tuplen | Applyn−2
Ap E_{m}  ::= Apn,m (SE_{n+1})
Case E_{m} ::= Bool casem (SE, E_{m}, E_{m}) | List casem (SE, E_{m}, E_{m})
Loop E_{m} ::= WLoopm (SE_{m+3}) | FLoopm (SE_{m+4})
lambda E ::= λn,m (MV_{n}) . (E_{m}) | \underline{λn,m} (MV_{n}) . (E_{m})
E_{1}  ::= SE_{1} | PF 1_{1} (SE) | PF 2_{1} (SE_{2}) | PF N_{1} (SE_{n}) | Ap E_{1}

| Case E_{1} | Loop E_{1} | lambda E | Block_{1}

E_{m}  ::= SE_{m} | P F 1_{m} (SE) | Ap E_{m} | Case E_{m} | Loop E_{m} | Block_{m}
Block_{m}  ::= {m [Statement; ]^{∗} In SE_{m}}
Statement ::= Binding | Command
Binding ::= MV_{m} = E_{m}
Command ::= P nD store (SE, SE, SE) | Cons store 1 (SE, SE)

| Cons store 2 (SE, SE) | Store error | ⊤_{s}

P rogram ::= Block_{1}

Figure 3: Grammar of Kid 9 all machine independent optimizations are expressed as source-to-source program transformations on Kid. We believe I-structures are an essential feature of Kid, and are needed to express the semantics of the purely functional subset of Id.

Kid has only uncurried operators and no complex expressions. A major subset of Kid is simply the λ-calculus with constants and let-blocks. However, unlike other functional languages, let-blocks play a fundamental role, that is, they can not be eliminated by systematic substitution of variables. The syntax of Kid is given in Figure 3. Every expression, except a block or λ-expression, consists of a function symbol followed by the corresponding number of arguments. The ordering of statements within a block is irrelevant.

An important feature of Kid is the concept of multiple values. The expression

x, y = {_{2} a = ⋯; b = ⋯; In a, b}

is a well-formed-expression, where “x, y” indicates multiple variables, not to be confused with a 2-tuple in Id [10]. The 2 after the curly brace indicates that two values are to be returned by this block expression. Multiple values avoid packaging values in a data structure, and are useful in expressing some optimizations. Thus, in Kid a binding has the form MV = E, where MV stands for multiple variables. Suppose we have m variables on the left-hand-side, then the expression E on the right-hand-side must return m values. In the sequel we capture the number of values that an expression produces by subscripting the corresponding syntactic category. Thus, to express the above binding we will write MV_{m} = E_{m}. Note that the function symbol Apply appears as a PF 2_{1} in the grammar because we assume that all user-defined procedures return only one result. We also use subscripted function symbols to express a family of functions. For example, Make tuplen stands for Make tuple2, Make tuple3, etc. . Subscripts in a function symbol do not necessarily represent the number of values to be returned by the application of the function. By convention, we drop the subscript when its value is one.

Kid also contains While-loops and For-loops because these play a significant role in program transformations. These constructs also play a major role when Kid is further translated into P-TAC.

4 Translating Desugared Id^{−} into Kid

4.1 Simplification of Expressions

We give the translation in terms of the following functions:

Translate Expression, TE : Id^{−} Expression ⟶ Kid Expression
Translate Statement, TS : Id^{−} Statement ⟶ list (Kid Statement)
Translate Binding,  TB : Id^{−} Binding  ⟶ list (Kid Binding)
Translate Operator, TO : Id^{−} Operator ⟶ Kid Operator
Pattern Matching,  PM : Case expression ⟶ Kid Expression

The exact syntax of Case expression is given in Section 4.3.

We will write TE[[E_{1}]] = E_{2}, where the expression enclosed in double brackets represents an Id^{−} expression and E_{2} is the corresponding Kid expression. The whole translation is given in terms of syntactic categories. The proper way of reading a translation function

such as “TE[[(UOP E_{1})]] = {t_{1} = TE[[E_{1}]]; t = TO[[UOP]] (t_{1}); In t} ” is that “TE” when applied

to a unary expression in Id^{−} produces the Kid expression on the right-hand-side.

Throughout, the emphasis is on clarity of Id^{−} to Kid translation rather than its efficiency. We will use the same conventions introduced in Section 6, with the addition of meta-variable P_{i} that ranges over Patterns. As before X_{n}^{→} indicates multiple metavariables. The lower case variables, such as t_{i}, x_{i}, that appear in the translated expression represent new Kid variables. The translation procedure given below does not require lexical scope analysis for variables. However, after the translation is complete a procedure to make all bound variables unique has to be applied before any rewriting can be done.

A common situation in the translation procedure is the need to replace variable X by a new variable t in some Id expression E. This idea can be expressed by addding another block around E as in { X = t; t′ = E; In t′ }. To avoid clutter, we will write E [t/X]_{B} as a shortand for { X = t; t′ = E; In t′ }. (As an aside, it should be noted that since we do not assume unicity of variables during translation, we can not use the notion for naive substitution. Conversely, the use of E [X_{n}^{→} / Z_{n}^{→}]_{B} in the application rewrite rule, given earlier, would have been incorrect, because it could lead to duplication of bound variables Z_{n}^{→}, while expanding two different applications of the same function).

TE: Id^{−} Expression ⟶ Kid Expression

TE[[X]] = X

TE[[Next X]] = next(X)

Where “next” is a function on identifiers that keeps the association between a variable and its corresponding nextified version during the loop translation phase. After the translation is complete, next(X) is treated like an ordinary identifier which is different from X.

TE[[C]] = C

TE[[(UOP E)]] = \{ \begin{matrix}t_{1} & = & TE[[E]]; \\ t & = & TO[[UOP]] (t_{1}) \\ & In t\} \end{matrix}

TE[[(E_{1} BOP E_{2})]] = \{ \begin{matrix}t_{1} & = & TE[[E_{1}]]; \\ t_{2} & = & TE[[E_{2}]]; \\ t & = & TO[[BOP]] (t_{1}, t_{2}) \\ & In t\} \end{matrix}

TE[[(E_{1} E_{2})]] = \{ \begin{matrix}t_{1} & = & TE[[E_{1}]]; \\ t_{2} & = & TE[[E_{2}]]; \\ t & = & Apply (t_{1}, t_{2}) \\ & In t\} \end{matrix}

TE[[E_{1}[E_{2}]]] = \{ \begin{matrix}t_{1} & = & TE[[E_{1}]]; \\ t_{2} & = & TE[[E_{2}]]; \\ t & = & Ap2 (Select, t_{1}, t_{2}) \\ & In t\} \end{matrix}

where Select is a standard function definition in Kid (see Section 4.2).

TE[[E.cons 1]] = \{ \begin{matrix}t_{1} & = & TE[[E]]; \\ t & = & List case (t_{1}, Error, Cons 1 (t_{1})) \\ & In t\} \end{matrix}

Similarly for E.cons 2.

TE[[(E_{1}, ⋯, E_{n})]] = { t_{1} = TE[[E_{1}]]; ⋮ t_{n} = TE[[E_{n}]]; t = Make tuplen (t_{n}^{→}) In t}

TE[[(If E_{1} then E_{2} else E_{3})]] = \{ \begin{matrix}t_{1} & = & TE[[E_{1}]]; \\ t & = & Bool case (t_{1}, TE[[E_{2}]], TE[[E_{3}]]) \\ & In t\} \end{matrix}

TE[[\{ Case E of ; | P_{1} = E_{1} ; ⋮ ; | P_{n} = E_{n} \}]] = \{ \begin{matrix}t_{1} & = & TE[[E]]; \\ t & = & PM[[\{ Case (t_{1}) of | P_{1} = TE[[E_{1}]] ⋮ | P_{n} = TE[[E_{n}]] \}]] \\ & In t\} \end{matrix}

Where PM is described in the Section 4.3.

TE[[{ While E do S_{1}; ⋮ S_{n}; Finally E_{f} }]] = TSLE[[{ While TE[[E]] do TS[[S_{1}]]; ⋮ TS[[S_{n}]]; Finally TE[[E_{f}]] }]]

Note that TE uses an auxiliary function TSLE which stands for “Translate simple loop expression”. However this is only done for clarity of exposition. In fact, we are slightly abusing our notation because the expression inside TSLE[[ ]] is a mixture of Id^{−} and Kid syntax.

TSLE[[\{ While E do next(X_{1}) = E_{1}; ⋮ next(X_{n}) = E_{n}; Y_{1} = E_{y_{1}}; ⋮ Finally E_{f} \}]] = \{ \begin{matrix}p & = & \underline{λ_{n}} (X_{n}^{→}) . (E); \\ b & = & \underline{λ_{n,n}} (X_{n}^{→}) . (\{n next(X_{1}) = E_{1}; ; ⋮ ; next(X_{n}) = E_{n}; ; Y_{1} = E_{y_{1}}; ; ⋮ ; In next(X_{1}), ⋯, next(X_{n}) \}); \\ t_{p} & = & Apn (p, X_{n}^{→}); \\ t_{n}^{→} & = & WLoopn (p, b, X_{n}^{→}, t_{p}); \\ t_{f} & = & E_{f} [t_{n}^{→} / X_{n}^{→}]_{B} \\ & In t_{f}\} \end{matrix}

Notice that the correspondence between the formal parameters of the procedure “b” and the multiple value returned is not accidental. It will be wrong to have (X_{1}, ⋯, X_{n}) as input and (next(X_{n}), ⋯, next(X_{1})) as output, because the values of the nextified variables come either from the surrounding scope or from the previous iteration. The λ-expressions corresponding to the predicate and loop body are underlined indicating the fact that they can be inlined at compile time.

TE[[{ For X ← E_{i} to E_{b} step Es do S_{1}; ⋮ S_{n}; Finally E_{f} }]] = TSLE[[{ For X ← TE[[E_{i}]] to TE[[E_{b}]] step TE[[E_{s}]] do TS[[S_{1}]]; ⋮ TS[[S_{n}]]; Finally TE[[E_{f}]] }]]

TSLE[[ \{For X_{1} ← E_{i} to E_{b} step E_{s} do next(X_{2}) = E_{2}; ⋮ next(X_{n}) = E_{n}; Y_{1} = E_{y_{1}}; ⋮ Finally E_{f} \}]] = \{ \begin{matrix}b & = & \begin{matrix}\underline{λ_{n,n−1}} (X_{n}^{→}) . \\ (\{n−1 next(X_{2}) = E_{2}; ; ⋮ ; next(X_{n}) = E_{n}; ; Y_{1} = E_{y_{1}}; ; ⋮ ; In next(X_{2}), ⋯, next(X_{n}) \}); \end{matrix} \\ t_{i} & = & E_{i}; \\ t_{b} & = & E_{b}; \\ t_{s} & = & E_{s}; \\ t_{p} & = & ≤ (t_{i}, t_{b}); \\ t_{n}^{→} & = & FLoopn (t_{b}, t_{s}, b, t_{i}, X_{2,n}^{→}, t_{p}); \\ t_{f} & = & E_{f} [t_{n}^{→} / X_{n}^{→}]_{B} \\ & In t_{f}\} \end{matrix}

TE[[{Fun X_{n}^{→} = E}]] = λn (X_{n}^{→}) . (TE[[E]])
TE[[\{\underline{Fun} X_{n}^{→} = E\}]] = \underline{λn} (X_{n}^{→}) . (TE[[E]])

TE[[{S_{1}; ⋯ S_{n}; In E}]] = { TS[[S_{1}]];
⋮
TS[[S_{n}]];
t = TE[[E]]
In t }

TS: Id^{−} Statement ⟶ list (Kid Statement)

Often an Id^{−} statement translates into a group of Kid statements. We will enclose the translated statement or statements within parenthesis even though parenthesis are not part of Kid syntax. These parenthesis do not introduce a new lexical scope.

TS[[P = E]] = (t = TE[[E]]; TB[[P = t]])
TS[[E_{1}[E_{2}] = E_{3}]] = ( \begin{matrix}t_{1} & = & TE[[E_{1}]]; \\ t_{2} & = & TE[[E_{2}]]; \\ t_{3} & = & TE[[E_{3}]]; \\ t & = & Ap3 (Store, t_{1}, t_{2}, t_{3})) \end{matrix}

where Store is a standard function defined in Kid (see Section 4.2 ).

TS[[E_{1}.cons 1 = E_{2}]] = ( \begin{matrix}t_{1} & = & TE[[E_{1}]]; \\ t_{2} & = & TE[[E_{2}]]; \\ t & = & List case (t_{1}, \{ Store error In ()\}, \{ Cons store 1 (t_{1}, t_{2}) In () \} ) ) \end{matrix}

Similarly for cons 2.

TB: Id^{−} Bindings ⟶ list (Kid Binding)

TB[[(P_{1}, ⋯, P_{n}) = X]] = (t_{n}^{→}= Detuplen (X);
TB[[P_{1} = t_{1}]];
⋮
TB[[P_{n} = t_{n}]] )

TB[[(P_{1} : P_{2}) = X]] = (t_{1}, t_{2} = List case2 (X, ( Error, Error ), (Cons 1 (X), Cons 2 (X)) );
TB[[P_{1} = t_{1}]];
TB[[P_{2} = t_{2}]])

TB[[Y = X]] = (Y = X)

TB[[Next Y = X]] = (next(Y) = X)

TO: Id^{−} Operator ⟶ Kid Operator

TO[[UOP]] = the corresponding Kid PF 1

TO[[BOP]] = the corresponding Kid PF 2

The Kid operator corresponding to Id^{−} “:” is Cons and for “==” is Equal?.

4.2 Definition of Standard Functions

In our translation from Id^{−} to Kid we have introduced two new functions Select and Store. These are not primitive operators in Kid, therefore we give their definitions. Similarly we give a definition for Make 1D array. For the sake of brevity we give these definitions in Id^{−}. These definitions and Make 1D array can be written as follows

      Make_1D_array = { Fun b f = { (l,u) = b ;
                                     a = I_array b;
                                     i = l;
                                     d = { While i ≤ u  do
                                            a[i] = f i;
                                            Next i = i+1
                                           Finally () }
                                     In a } }

Like lists we are treating I-arrays and functional arrays as the same type. However, functional arrays have a different degree of polymorphism than I nD array. We are ignoring these subtle issues in the above translation.

      Select = { Fun x i = { (l,u) =  1D_Bounds x;
                             In
                               If (i > u Or i < l)  then
                                                 Error
                                                    else
                                                 P_1D_select x i } }
      Store = { Fun x i y = { (l,u) =  1D_Bounds x;
                               In
                                 If (i > u Or i < l)  then
                                                 { Store_error In () }
                                                      else
                                                 { P_1D_store x i y In () } } }

The above Id^{−} definitions can be translated into Kid by adding the following rules:

TE[[P nD select x i]] = P nD select (x, i)

TS[[P nD store x i y]] = P nD store (x, i, y)

TE[[Error]] = Error

TE[[Store error]] = Store error

4.3 Pattern Matching: Elimination of Complex Patterns

Pattern matching in Id follows a different philosophy than other functional languages such as Miranda and Haskell. In both these languages clauses in patterns are examined from top to bottom and patterns in a clause are examined from left to right. Within the limitations of the above rule, pattern matching does not force the evaluation of a pattern whose type is irrefutable (tuples are examples of irrefutable patterns) [13]. Miranda in addition allows repeated occurrences of a variable in a clause.

Id pattern matching is designed to be order-insensitive and is maximally non-strict for sequential implementations. In Id, patterns must not overlap to allow order-insensitivity.

Id also does not permit repeated variables.

Determination of which variables are necessary to evaluate to resolve patterns is quite tricky as illustrated by the following example (due to Lennart Augustsson):

       { Case (x, y, z) of
          |   (1, 0, w) = 1
          |   (0, w, 1) = 2
          |   (w, 1, 0) = 3 }

First of all notice that the patterns are non-overlapping, i.e., only one can be true for a given x, y and z. Second, notice that top-to-bottom and left-to-right rule will evaluate x and then evaluate y or z depending upon the value of x. Thus, if x does not terminate no answer will ever be produced. Notice if y = 1 and z = 0 one could demand the answer 3 regardless of the x. Traversal of patterns in a different order will force evaluation of different variable.

Id pattern matching rules will force the evaluation of all three variables in this example because no unique sequential order exists. (In Miranda and Haskell, all three variables will be evaluated only if y turns out to be 1 or z turns out to be 0).

Now we informally describe a simplified version of the pattern matching algorithm used by the Id compiler [11]. For Id^{−} we take into consideration lists and tuples only. In the following we describe various cases that arise during pattern matching.

The signature of the pattern matching function is

PM : Case expression ⟶ Kid Expression

where Case-expression is defined as follows

Case expression ::= {Case SE of [ | Clause]^{∗}}
Clause  ::= P = Kid Expression
P  ::= Nil | Variable | () | (P, P) | (P, P, P) | ⋯ | (P : P)
SE  ::= () | (Variable, ⋯, Variable )

If the pattern is a variable, say “X”, then “X” is equivalent to “(X)”.

As was stated earlier, no scope analysis of variable names is required for the translation from Id to Kid. Thus, we will not assume that all bound variable names are unique in the Kid program that is generated by the translation process.

Variable rule

The column of patterns corresponding to a case variable consists only of variables.

PM[[ {Case (X_{1,i−1}^{→}, X_{i}, X_{i+1,n}^{→}) of ; | (P 1_{1,i−1}^{→}, Y_{1}, P 1_{i+1,n}^{→}) = E_{1} ; ⋮ ; | (P m_{1,i−1}^{→}, Y_{m}, P m_{i+1,n}^{→}) = E_{m}}]] =

\{ \begin{matrix}t = X_{i}; \\ t_{f} = PM[[ \{Case (X_{1,i−1}^{→}, X_{i+1,n}^{→}) of ; | (P 1_{1,i−1}^{→}, P 1_{i+1,n}^{→}) = E_{1}[t/Y_{1}]_{B} ; ⋮ ; | (P m_{1,i−1}^{→}, P m_{i+1,n}^{→}) = E_{m}[t/Y_{m}]_{B}\}]] \\ In t_{f} \} \end{matrix}

Note that meta-variables Y_{1} ⋯ Y_{m} may be distinct.

Irrefutable pattern rule

The column of patterns corresponding to a case variable consists of at least one tuple and zero or more variables. Without loss of generality in the following rule we assume the tuple to be a 2-tuple.

PM[[ {Case (X_{1,i−1}^{→} , X_{i} ,  X_{i+1,n}^{→}) of ; | (P 1_{1,i−1}^{→} , Y_{1} ,  P 1_{i+1,n}^{→}) = E_{1} ; ⋮ ; | (P k_{1,i−1}^{→} , Y_{k} ,  P k_{i+1,n}^{→}) = E_{k} ; | (P l_{l,i−1}^{→} , (Y l_{1} , Y l_{2}) ,  P l_{i+1,n}^{→}) = E_{l} ; ⋮ ; | (P m_{1,i−1}^{→} , (Y m_{1} , Y m_{2}) , P m_{i+1,n}^{→}) = E_{m}}]] =

{t_{1}, t_{2} = Detuple2 (X_{i});
t  = X_{i};
t_{f}  = PM[[ {Case (X_{1,i−1}^{→} , t_{1} ,  t_{2} ,  X_{i+1,n}^{→}) of ; | (P 1_{1,i−1}^{→} , t_{1,1} , t_{1,2} , P 1_{i+1,n}^{→}) = E_{1}[t/Y_{1}]_{B} ; ⋮ ; | (P k_{1,i−1}^{→} , t_{k,1} , t_{k,2} , P k_{i+1,n}^{→}) = E_{k}[t/Y_{k}]_{B} ; | (P l_{l,i−1}^{→} , Y l_{1} , Y l_{2} , P l_{i+1,n}^{→}) = E_{l} ; ⋮ ; | (P m_{1,i−1}^{→} , Y m_{1} , Y m_{2} , P m_{i+1,n}^{→}) = E_{m}}]]

In t_{f}}

Refutable pattern rule

The column of patterns corresponding to a case variable consists of only Nil’s and (Y_{1} : Y_{2})’s.

PM[[ {Case (X_{1,i−1}^{→} , X_{i} ,  X_{i+1,n}^{→}) of | (P 1_{1,i−1}^{→} , Nil ,  P 1_{i+1,n}^{→}) = E_{1} ⋮ | (P k_{1,i−1}^{→} , Nil ,  P k_{i+1,n}^{→}) = E_{k} | (P l_{l,i−1}^{→} , Y l_{1} : Y l_{2} ,  P l_{i+1,n}^{→}) = E_{l} ⋮ | (P m_{1,i−1}^{→} , Y m_{1} : Y m_{2} , P m_{i+1,n}^{→}) = E_{m}}]] =

List case (X_{i},

PM[[ {Case (X_{1,i−1}^{→} , X_{i+1,n}^{→}) of ; | (P 1_{1,i−1}^{→} , P 1_{i+1,n}^{→}) = E_{1} ; ⋮ ; | (P k_{1,i−1}^{→} , P k_{i+1,n}^{→}) = E_{k}}]],

\{ \begin{matrix}t_{h}, t_{t} = Cons 1 (X_{i}), Cons 2 (X_{i}); \\ t_{f} = PM[[ \{Case (t_{h} ,  t_{t} ,  X_{1,i−1}^{→} , X_{i+1,n}^{→}) of ; | (Y l_{1} , Y l_{2} , P l_{1,i−1}^{→} , P l_{i+1,n}^{→}) = E_{l} ; ⋮ ; | (Y m_{1} , Y m_{2} , P m_{1,i−1}^{→} , P m_{i+1,n}^{→}) = E_{m}\}]] \\ In t_{f}\} ) \end{matrix}

Note that if the case expression is not exhaustive then an alternative that will raise a run-time error is generated. As, for example:

PM[[ \begin{matrix}\{Case & X & of \\ | & Y_{1} : Y_{2} & = E\}]] \end{matrix} = PM[[ \begin{matrix}\{Case & X & of \\ | & Y_{1} : Y_{2} & = E \\ | & Nil & = Error\}]] \end{matrix}

PM[[ \begin{matrix}\{Case & X & of \\ | & Nil & = E\}]] \end{matrix} = PM[[ \begin{matrix}\{Case & X & of \\ | & Nil & = E \\ | & t_{1} : t_{2} & = Error\}]] \end{matrix}

Mixed variable-refutable patterns

The column of patterns corresponding to a case variable consists of at least one refutable pattern. In such a case each variable is replaced by all the possible alternatives, as shown below:

PM[[ \begin{matrix}\{Case & (X_{1}, & X_{2}, & X_{3} & ) & of \\ | & (Nil , & Y_{1,1} : Y_{1,2} , & Y_{1} & ) & = E_{1} \\ | & (Y_{2,1} : Y_{2,2} , & Y_{2} , & Nil & ) & = E_{2} \\ | & (Y_{3} , & Nil , & Y_{3,1} : Y_{3,2} & ) & = E_{3}\}]] = \end{matrix}

\{ \begin{matrix}t_{3}^{→} & = & X_{3}^{→}; \\ t_{f} & = & PM[[ \begin{matrix}\{Case & (X_{1}, & X_{2}, & X_{3} & ) & of \\ | & (Nil , & Y_{1,1} : Y_{1,2} , & Nil & ) & = E_{1}[t_{3}/Y_{1}]_{B} \\ | & (Nil , & Y_{1,1} : Y_{1,2} , & t_{1,1} : t_{1,2} & ) & = E_{1}[t_{3}/Y_{1}]_{B} \\ | & (Y_{2,1} : Y_{2,2} , & Nil , & Nil & ) & = E_{2}[t_{2}/Y_{2}]_{B} \\ | & (Y_{2,1} : Y_{2,2} , & t_{2,1} : t_{2,2} , & Nil & ) & = E_{2}[t_{2}/Y_{2}]_{B} \\ | & (Nil , & Nil , & Y_{3,1} : Y_{3,2} & ) & = E_{3}[t_{1}/Y_{3}]_{B} \\ | & (t_{3,1} : t_{3,2} , & Nil , & Y_{3,1} : Y_{3,2} & ) & = E_{3}[t_{1}/Y_{3}]_{B}\}]] \end{matrix} \\ In t_{f}\} \end{matrix}

This rule can be applied only after checking that none of other rules apply. It should be noted that patterns can be tested in many different orders, each giving rise to a correct program though non necessarily the same program. The above rules cover all legal cases. If we ever get tuple and list patterns in one column, the compiler will flag it as a type violation.

Empty variable rule

PM[[ {Case () of ; | () = E_{1} ; ⋮ ; | () = E_{m}}]] = Compiler Error “overlapping patterns”

PM[[ \begin{matrix}\{Case & () & of \\ | & () & = E\}]] \end{matrix} = E

5 Contextual Reduction Systems

A Contextual Reduction System is a pair (A(F, S), R) , where A is a set of terms, and R is a set of context sensitive rules. F includes at least the Apn,m primitive. The saliant syntactic features of the terms in A can be seen by the grammar given in Figure 4. This grammar can be related to the Kid grammar by defining F to be +, Apply, WLoop_{m}, P select, etc. and S to be P store, Cons store, etc. respectively.

5.1 Basic Definitions

The applicability of a context sensitive rule depends upon both the structure of the term and a precondition on the context in which the term occurs. For example, the context sensitive rule corresponding to the well known rule “ Cons 1 (Cons X_{1} X_{2}) − ; − ; → X_{1}” is

\frac{X = Cons (X_{1}, X_{2})}{Cons 1 (X) − ; − ; → X_{1}}

where the binding X = Cons (X_{1}, X_{2}) over the line denotes a precondition, and X, X_{1}, and X_{2} denote meta-variables. A way of reading the above rule is that Cons 1 (X) can be rewritten to X_{1} if the binding X = Cons (X_{1}, X_{2}) occurs in the context of Cons 1 (X).

A context is a term with an arbitrary number of □_{E}, expression holes, and □_{S}, statement holes. Formally contexts are terms generated by the grammar of Figure 4, where □_{E} and □_{S} are added to SE and Statement categories, respectively. Thus, given a context

SE ∈ Simple Expression
E_{m} ∈ Expression with m outputs
Fn,m ∈ Primitive Function of n arguments and m outputs
Sn ∈ Primitive command of n arguments
SE  ::= V ariable | F_{0}
SE_{m}  ::= \underbrace{SE, ⋯, SE}_{m}
MV_{m}  ::= \underbrace{V ariable, ⋯, V ariable}_{m}
lambda E ::= λn,m (MV_{n}) . (E_{m})
E_{m}  ::= SE_{m} | Fn,m (SE_{n}) | lambda E | Block_{m}
Block_{m}  ::= { [Statement; ]^{∗} In SE_{m}}
Statement ::= Binding | Command
Binding ::= MV_{m} = E_{m}
Command ::= S_{n} (SE_{n})
T erm  ::= Block

Figure 4: Syntax of terms of a CRS C[□_{S}, □_{E}], and a substitution, σ, for the meta-variables X, X_{1} and X_{2} such that

C[(X = Cons (X_{1}, X_{2}))^{σ}, (Cons 1 (X))^{σ}]

is a term, we say

C[(X = Cons (X_{1}, X_{2}))^{σ}, (Cons 1 (X))^{σ}] − ; − ; → C[(X = Cons (X_{1}, X_{2}))^{σ}, X_{1}^{σ}] (1)

where ⟶ stands for “rewrites to”. From (1) we can observe that the precondition of the rule is not affected by the rewriting, however, the precondition usually affects the outcome of the rewriting.

Definition 5.1 (Context sensitive rule) A rule is an ordered set of preconditions, P_{1} ⋯ P_{n}, and a left-hand-side, l, and a right-hand-side, r, and is written as

\frac{P_{1} | ⋯ | P_{n}}{l − ; − ; → r}

where P_{i} is a statement and l and r are expressions.

Definition 5.2 (Redex) Given a rule \frac{P_{1} | ⋯ | P_{n}}{l − ; − ; → r} and a term M ≡ C[S_{1}, ⋯, S_{n}, E],

E is said to be a redex iff (1) E ≡ l^{σ} ;

(2) S_{j} ≡ P_{j}^{σ} ∀ j, 1 ≤ j ≤ n; where σ is a substitution.

Definition 5.3 (Reduction Relations) Given terms M, N ∈ A and a rule τ ∈ R, M reduces to N in one step (M − ; − ; →_{τ} N), iff M ≡ C[P_{1}^{σ}, ⋯, P_{n}^{σ}, l^{σ}], and N ≡ C[P_{1}^{σ}, ⋯, P_{n}^{σ}, r^{σ}]. The one-step rewriting relation − ; − ; →_{R} = ⋃_{τ ∈R}(− ; − ; →_{τ}). The transitive reflexive closure of − ; − ; →_{R} is written as − ; → ; →_{R}.

5.2 Basic Rules of Contextual Reduction System’s (RCRS)

One has to deal with the problem of free-variable capture in any formal system with bound variables. In the λ-calculus, the problem is usually solved either by making some variable convention, as for example, assuming that all free variables are different from the bound variables, or by adopting a variable-free notation such as that of DeBruijn [6]. According to the variable convention given in [4], the term (λx.xx)(λx.xx) is a legal term, while the term (λy.(λx.+(x, y))x is not a legal term, because the variable x appears both free and bound. The convention allows one to express application in terms of a naive form of substitution, which does not require α-renaming at execution time. In a system with let-blocks, in order to avoid the free-variable capture as well as a to allow naive substitution, we have to adopt a even more stringent convention: all bound variables in an expression must be unique and different from variables free in the whole program. In order to maintain this invariant we will occasionally rename all bound variables of a subterm to completely new variables explicitly, by applying the function RB to the subterm. For example,

RB [[{x = + (a, 1) In x}]] = {x′ = + (a, 1) In x′}

An example of the use of RB function arises in the use of the application rule (see Section 6.1) as shown below

\frac{F = λn,m (Z_{n}^{→}) . (E)}{Apn,m (F, X_{n}^{→}) − ; − ; → (RB[[E]]) [X_{n}^{→} / Z_{n}^{→}]}

All contextual reduction systems have the following rules, named R_{CRS}.

Substitution rules

\frac{X = Y}{X − ; − ; → Y} ; \frac{X = C}{X − ; − ; → C}

where meta-variable C stands for a constant, and X and Y stand for distinct variables.

Block Flattening rule

{m X_{n}^{→} = {n SS_{1}; SS_{2}; ⋯  {m X_{n}^{→} = Y_{n}^{→};
In Y_{n}^{→}} − ; − ; → SS_{1}; SS_{2}; ⋯
S_{1}; ⋯ S_{n}  S_{1}; ⋯ S_{n}
In Z_{m}^{→}}  In Z_{m}^{→}}

Multivariable rule

X_{n}^{→} = Y_{n}^{→} − ; − ; → (X_{1} = Y_{1}; ⋯ X_{n} = Y_{n})

Lemma 5.4 RCRS is Strongly Normalizing and Confluent. Proof: Since there are only a finite number of blocks and occurrences of a variable in a term M, R_{CRS} is strongly normalizing. It is easy to see that the block flattening rules are locally confluent. Since variable substitution rules within a flattened block are also locally confluent, the uniqueness of the normal form of M follows trivially from Newman’s Lemma [4].

5.3 Canonical Forms of terms in a CRS

The notion of α-equivalence between terms as defined in the λ-calculus, makes too fine a distinction in a CRS calculus, for example, the following two Kid terms have apparently different syntactic structure.

{x = 8; t′ = {y = x; t = x + y In t} In t′} and {x = 8; y = x; t = x + y In t}

However, we consider the difference between the above two terms merely “syntactic noise”. Eliminating this syntactic noise is the motivation behind the following definitions.

Definition 5.5 (Canonical form) Let N be the normal form of a term M with respect to RCRS. \overline{M}, the canonical form of M, is the term obtained by deleting from N all bindings of the form x = y (where x and y are distinct variables) or x = v ( where v is a constant).

Definition 5.6 (α-equivalence) Two terms M and N are said to be α-equivalent, if \overline{M} and \overline{N} can be transformed into each other by a consistent renaming of bound variables.

Lemma 5.7 Each term has a unique canonical form.

6 Contextual Reduction System of Kid

We now present a set of rewrite rules, R_{Kid}, which give an intuitive understanding of how Kid terms may get evaluated. If we call A the set of Kid terms generated by the grammar of Figure 3, then the structure ⟨A, R_{Kid}⟩ is a Contextual Reduction System. We assume that a primitive function is applied only to arguments of appropriate types, i.e., the type checking has been done statically.

All the variables that appear on the left-hand-side of the rules are meta-variables that range over appropriate syntactic categories. By convention, we use capital letters for meta-variables and small letters for Kid variables. All variables that appear on the righthand-side of the rules are either meta-variables or “new” Kid variables. We will make use of the following convention regarding meta-variables:

X_{i}, Z_{i}, Y_{i}, F_{i}, P, B, U, D ∈ Variable and Constant
C  ∈ Constant
S_{i}, SS_{i}, S′  ∈ Statement
E_{i}  ∈ Expression

The notation E [Y/X] means the substitution of Y for X in E. Due to our assumptions E [Y/X] will simply indicate naive substitution, that is, substitution where no danger of free-variable-capture exists and where X can be replaced by Y without regards to scope. Moreover, we will use the notation X_{n,m}^{→} to stand for (X_{n}, ⋯, X_{m}), X_{m}^{→} for X_{1,m}^{→}, and E [Y_{n}^{→}

/ X_{n}^{→}] for E [Y_{1}/X_{1}, ⋯, Y_{n}/X_{n}], which is the same as (⋯ ((E [Y_{1}/X_{1}]) [Y_{2}/X_{2}]) ⋯) [Y_{n}/X_{n}]).

In the following, \underline{n} represents a numeral.

6.1 Kid Rewrite Rules

δ rules

+ (\underline{m}, \underline{n})  − ; − ; →_{δ} \underline{+(m, n)}
⋮
Equal? (\underline{n}, \underline{n}) − ; − ; →_{δ} True
Equal? (\underline{m}, \underline{n}) − ; − ; →_{δ} False  (if m ≠ n)

Case rules

Bool casem (True, E_{1}, E_{2}) − ; − ; → E_{1}
Bool casem (False, E_{1}, E_{2}) − ; − ; → E_{2}
List casem (Nil, E_{1}, E_{2})  − ; − ; → E_{1}

\frac{X = Open cons ()}{List casem (X, E_{1}, E_{2}) − ; − ; → E_{2}}

Arity Detection rule

\frac{F = λ(Z).E}{Apply (F, X) − ; − ; → Ap (F, X)}

\frac{F = λ_{n}(Z_{n}^{→}).E}{Apply (F, X) − ; − ; → Apply1 (F, \underline{n}, X)} n > 1

Similar rules apply for \underline{λ_{n}}.

\frac{F_{i} = Applyi (F, \underline{n}, X_{i}^{→})}{Apply (F_{i}, X) − ; − ; → Applyi+1 (F, \underline{n}, X_{i+1}^{→})} i < (n−1)
\frac{F_{i} = Applyi (F, \underline{n}, X_{i}^{→})}{Apply (F_{i}, X) − ; − ; → Apn (F, X_{n}^{→})}  i = (n−1)

Application rule

\frac{F = λn,m (Z_{n}^{→}) . (E)}{Apn,m (F, X_{n}^{→}) − ; − ; → (RB[[E]]) [X_{n}^{→} / Z_{n}^{→}]}

A similar rule applies for \underline{λ_{n,m}}. Loop rules

WLoopn (P, B, X_{n}^{→}, True) − ; − ; → {n t_{n}^{→} = Apn,n (B, X_{n}^{→}); t_{p} = Apn (P, t_{n}^{→}); t′_{n}^{→} = WLoopn (P, B, t_{n}^{→}, t_{p}) In t′_{n}^{→}}
WLoopn (P, B, X_{n}^{→}, False) − ; − ; → X_{n}^{→}

In the following two rules we assume that the index variable is the first variable in X_{n}^{→}.

FLoopn (U, D, B, X_{n}^{→}, True) − ; − ; → {n t_{2,n}^{→} = Apn,n−1 (B, X_{n}^{→}); t_{1} = + (X_{1}, D); t_{p} = < (t_{1}, U); t′_{n}^{→} = FLoopn (U, D, B, t_{n}^{→}, t_{p}) In t′_{n}^{→}}

FLoopn (U, D, B, X_{n}^{→}, False) − ; − ; → X_{n}^{→}

Tuple rule

\frac{X = Make tuplen (X_{n}^{→})}{Detuplen (X) − ; − ; → X_{n}^{→}}

List rules

Cons (X, Y) − ; − ; → \{ \begin{matrix}t & = & Open cons (); \\ Cons store 1 (t, X); \\ Cons store 2 (t, Y) \\ In t\} \end{matrix}

\frac{Cons store 1 (X, Y)}{Cons 1 (X) − ; − ; → Y}

\frac{Cons store 2 (X, Y)}{Cons 2 (X) − ; − ; → Y}

\frac{Cons store 1 (X, Y)}{Cons store 1 (X, Y′) − ; − ; → ⊤_{s}}

\frac{Cons store 2 (X, Y)}{Cons store 2 (X, Y′) − ; − ; → ⊤_{s}}

Array rules

\frac{X = I array (X_{b})}{Bounds (X) − ; − ; → X_{b}}

\frac{P store (X, Y, Z)}{P select (X, Y) − ; − ; → Z}

\frac{P store (X, Y, Z)}{P store (X, Y, Z′) − ; − ; → ⊤_{s}}

Propagation of ⊤

\begin{matrix}\{m X = ⊤; S_{1}; ⋯ S_{n} In Z_{m}^{→} \} & − ; − ; → & ⊤ \\ \{m ⊤_{s}; S_{1}; ⋯ S_{n} In Z_{m}^{→} \} & − ; − ; → & ⊤ \end{matrix}

The rules for propagating ⊤ were motivated by a discussion with Vinod Kathail. Theorem 6.1 Kid is Confluent upto α-renaming on canonical terms. Proof: See [1].

6.2 Printable Values and Answer of a Kid Term

We now define the printable information associated with a term. The grammar for printable values for Kid is given in Figure 5. A precise notion of printable values is essential to develop an interpreter for Kid as well as to discuss the correctness of optimizations (see Sections 6.3 and 7.3, respectively).

Atoms ::= Integers | Booleans | Error | “Function” | Ω
List  ::= ⟨List P V List⟩ | Nil
T uple ::= ⟨2 Tuple P V P V ⟩ | ⟨3 Tuple P V P V P V ⟩ | ⋯
Array ::= ⟨n Array T uple P V ⋯ P V ⟩
P V  ::= Atoms | List | T uple | Array | ⊤

Figure 5: Grammar of Printable Values

The following procedure, P, produces the printable value associated with a term. ρ and σ represent, respectively, the list of bindings that have as RHS either a λ-expression or an allocator, i.e. Make tuple, I array, Open cons, and the list of store commands, i.e. the I-structure store. The procedure L is used to lookup the value of a variable or a location in ρ and σ, respectively. Given a program, i.e. a closed term, M, the Print procedure is invoked as follows:

Print (M) = P [[M]] Nil Nil

where P is:

P[[{S_{s}; A_{s}; B_{s} In X}]] ρ σ = P[[X]] (A_{s} : ρ) (S_{s} : σ) P[[\underline{n}]] ρ σ = \underline{n} P[[True]] ρ σ = True P[[False]] ρ σ = False P[[⊤]] ρ σ = ⊤ P[[Nil]] ρ σ = Nil

P[[X]] ρ σ = \{ \begin{matrix}⟨n Tuple (P[[X_{1}]] ρ σ) ⋯ (P[[X_{n}]] ρ σ)]]⟩ & if L(X, ρ) = Make tuplen(X_{1}, ⋯, X_{n}) \\ ⟨List (P[[X.1]] ρ σ) (P[[X.2]] ρ σ)]]⟩ & if L(X, ρ) = Open cons() \\ ⟨Array ⟨2 Tuple \underline{l} \underline{u}⟩ (P[[X.\underline{l}]] ρ σ) ⋯ (P[[X.\underline{u}]] ρ σ)]]⟩ & if L(X, ρ) = I array(Y) \\ & and L(Y, ρ) = Make tuple (\underline{l}, \underline{u}) \\ “Function” & if L(X, ρ) = λ X_{n}^{→} . (E) or \\ & if L(X, ρ) = Applyi (F, \underline{n}, X_{i}^{→}) ∧ i < (n−1) \\ Ω & Otherwise \end{matrix}

P[[X.i]] ρ σ = \{ \begin{matrix}P[[Y]] ρ σ & if L(X.i, σ) = Y \\ Ω & if L(X.i, σ) = not found \end{matrix}

Notice that the printable value of a finite term can be an infinite tree. For example, the Print of :

{x = Open cons (); Cons store 1 (x, 1); Cons store 2 (x, x); In x}

is ⟨ List 1 ⟨ List 1 ⟨⋯⟩ ⋯⟩ ⟩, that is, an infinite list of 1’s.

We want to define the answer associated with a term in terms of printable values. Furthermore, we want to describe the answer independently of any interpreter, i.e. method of computing it. We need to define an ordering on printable values.

Definition 6.2 (Partial Order on Printable Values) Let a and b be Printable Values; a ⊑ b iff

(i) a = Ω; or

(ii) b = ⊤; or

(iii) both a and b are Atoms and a = b; or

(iv) a = ⟨n Tuple a_{1} ⋯ a_{n}⟩ and b = ⟨n Tuple b_{1} ⋯ b_{n}⟩ and a_{i} ⊑ b_{i} ∀ 1 ≤ i ≤ n; or

(v) a = ⟨List a_{1} a_{2}⟩ and b = ⟨List b_{1} b_{2}⟩ and a_{1} ⊑ b_{1} and a_{2} ⊑ b_{2}; or

(vi) a = ⟨n Array abounds a_{1} ⋯ a_{n}⟩ and b = ⟨n Tuple bbounds b_{1} ⋯ b_{n}⟩ and abounds = bbounds and a_{i} ⊑ b_{i} ∀ 1 ≤ i ≤ n.

Theorem 6.3 P V is a complete partial order with respect to ⊑.

For the proof see [5]. Lemma 6.4 Given a term M, M − ; − ; → N ⟹ Print (M) ⊑ Print (N). Pictorially:

\begin{matrix}M & − ; − ; → & M_{1} & − ; − ; → & M_{2} & ⋯ \\ Print(M) & ⊑ & Print(M_{1}) & ⊑ & Print(M_{2}) & ⋯ \end{matrix}

Intuitevely, the answer of a term may be defined as the limit of this chain, that is, the answer is the maximum printable value that can be obtained by reducing a term. We need the following definitions to give a precise definition of “Answer”.

Definition 6.5 (Reduction Graph of a term) Given a term M, the reduction graph of M, G(M), is defined as

{N | M − ; → ; → N}.

Definition 6.6 (Printable Reduction Graph of a term) Given a term M, the printable reduction graph of M, PG(M), is defined as

{Print (N) | M − ; → ; → N}.

Definition 6.7 (Answer) Given a term M, the Answer of M, Print^{∗}(M), is defined as

⊔ PG(M).

In order for the above definition to make sense we need to show that the limit of the printable reduction graph exists and is unique.

Theorem 6.8 ∀ M, PG(M) is directed. Proof: Given a, b ∈ PG(M), we have:

∃M_{1}, M_{2} such that a = Print(M_{1}), M − ; → ; → M_{1} ∧ b = Print(M_{2}), M − ; → ; → M_{2}.

By confluence, ∃ M_{3} such that

M_{1} − ; → ; → M_{3} ∧ M_{2} − ; → ; → M_{3}

By lemma 6.4,

a ⊑ c ∧ b ⊑ c, c = Print(M_{3})

Since PG(M) ⊆ P V is directed, by theorem 6.3 we know that the limit exists and is unique.

6.3 An Interpreter to Compute the Answer of a Kid term

The set of rewrite rules given in Section 6 per se do not define the operational semantics of Kid, they define a calculus to prove properties of programs. From a computational point of view we need to specify a strategy to apply these rules. Furthermore, the reduction strategy should be normalizing with respect to the definition of the answer. Intuitevely the interpreter should stop when it is known that no more printable information can be gotten by further reductions.

The strategy consists in evaluating the outermost redexes first, and in case of a block, evaluating all the right-hand-side redexes in parallel. We will represent a block

as {Ss; As; Bs In X} , where

Ss represents a set of store commands in the block
As represents a set of λ-bindings and allocator bindings in the block
Bs represents a set of bindings, excluding λ-binding and allocators, in the block

The interpreter E keeps track of store commands it encounters in σ, an I-structure store. It also keeps track of λ-bindings and allocator bindings encountered in ρ. At the start of the evaluation, both ρ and σ are considered to be empty.

The rules for propagating ⊤ imply that whenever new store commands are added to the store a check has to be made for inconsistencies, that is, multiple writes into the same location. We will assume this function is performed by CC. Thus, CC (ρ ∪ Ss) returns either a new consistent store or ⊤_{s}. While evaluating a block, we need to substitute variables and constants and eliminate the corresponding binding. We also need to flatten blocks. Though all nested blocks can be flattened in one go, we need to merge in one step only the block expressions on the RHS of bindings in the top-level block. Any substitution or block flattening can create new redexes on the RHS of bindings in a block. According to the ⊤ propagation rules, if a binding of the form x = ⊤ exists in any block then that block goes to ⊤. This can also be done during the substitution process. We will assume a function F&S (for flatten and substitute) that accomplishes all this. In addition to the new block, it returns a flag showing if any substitutions or flattening was done. Thus,

F&S[[{X = 1; Y = {P store (W, I, Z); Z = X + 3 In Z} In Y }]]
= {P store (W, I, Z); Z = 1 + 3; In Z}, True

We will also assume the existence of a function ERHS which is only applied to a block expression. It may be described informally as

\begin{matrix}ERHS[[\{Ss; As; X_{1} = E_{1}; ⋯ X_{n} = E_{n} In X_{i}\}]] ρ σ = \\ \{Ss; As; X_{1} = E[[E_{1}]] ρ σ; ⋯ X_{n} = E[[E_{n}]] ρ σ In X_{i}\} \end{matrix}

Given a program M, the E procedure is invoked as follows:

Eval [[M]] = E[[M]] Nil Nil

The Interpreter:

E[[+ (\underline{m}, \underline{n})]] ρ σ = \underline{+(m, n)} E[[Equal? (\underline{n}, \underline{n})]] ρ σ = True E[[Equal? (\underline{n}, \underline{m})]] ρ σ = False E[[Bool casem (True, E_{1}, E_{2})]] ρ σ = E[[E_{1}]] ρ σ E[[Bool casem (False, E_{1}, E_{2})]] ρ σ = E[[E_{2}]] ρ σ E[[List casem (Nil, E_{1}, E_{2})]] ρ σ = E[[E_{1}]] ρ σ E[[List casem (X, E_{1}, E_{2})]] ρ σ = E[[E_{2}]] ρ σ if L (X, ρ) = Open cons ()

E [[Apply (F, X)]] ρ σ = \{ \begin{matrix}E[[Ap (F, X)]] ρ σ & if L (F, ρ) = λZ . (E) \\ Apply1 (F, \underline{n}, X) & if L (F, ρ) = λ_{n}(Z_{n}^{→}).(E) ∧ n > 1 \\ Applyi+1 (F, \underline{n}, X_{i+1}^{→}) & if L (F, ρ) = Applyi (F, \underline{n}, X_{i}^{→}) ∧ i < (n−1) \\ E[[Apn (F, X_{n}^{→})]] ρ σ & if L (F, ρ) = Applyi (F, \underline{n}, X_{i}^{→}) ∧ i = (n−1) \end{matrix}

E[[Apn,m (F, X_{n}^{→})]] ρ σ = E[[(RB [[E]]) [X_{n}^{→} / Z_{n}^{→}]]] ρ σ where L (F, ρ) = λ_{n,m}(Z_{n}^{→}).E

E[[WLoopn (P, B, X_{n}^{→}, True)]] ρ σ = E[[{n t_{n}^{→} = Apn,n (B, X_{n}^{→}); t_{p} = Apn (P, t_{n}^{→}); t′_{n}^{→} = WLoopn (P, B, t_{n}^{→}, t_{p}) In t′_{n}^{→}}]] ρ σ

E[[WLoopn (P, B, X_{n}^{→}, False)]] ρ σ =X_{n}^{→} E [[Detuplen (X)]] ρ σ =X_{n}^{→} if L (X, ρ) = Make tuple X_{n}^{→} E [[Cons (X, Y)]] ρ σ = E[[{t = Open cons (); Cons store 1 (t, X); Cons store 2 (t, Y) In t}]] ρ σ

E [[Cons 1 (X)]] ρ σ = Y if L (X, σ) = Cons store 1 (X, Y) E [[Cons 2 (X)]] ρ σ = Y if L (X, σ) = Cons store 2 (X, Y) E[[Bounds (X)]] ρ σ = X_{b} if L (X, ρ) = I array (X_{b}) E[[P select (X, Y)]] ρ σ = Z if L (X, σ) = P store (X, Y, Z)

E[[{Ss; As; Bs In X}]] ρ σ = e

where e is obtained by the execution of the following program written in pseudo-Id

\{ \begin{matrix}blk, − = F&S(\{Ss; As; Bs In X\}); \\ flag = True; \\ In If blk = ⊤ then ⊤ \\ else & \{While flag do Suppose blk is \{Ss; As; Bs In X\} is = CC(σ ∪ Ss); fs = ρ ∪ As; next blk, next flag = If is = ⊤s then (⊤, False) else F&S(E RHS(blk, is, fs)) finally blk\}\} \end{matrix}

If none of the above clauses apply, then

E[[E]] ρ σ = E

Theorem 6.9 (Soundness) Given a term M,

Eval[[M]] = N ⟹ Print^{∗}(M) = Print(N)

Theorem 6.10 (Normalization Theorem) Given a term M,

Print^{∗}(M) is finite ⟹ Print(E[[M]]) = Print^{∗}(M).

7 Optimizations of Kid Programs

7.1 Optimizations as Rewrite rules (R_{opt})

Following is a partial list of optimization rules or source-to-source transformations that can be expressed as rules in the CRS for Kid. Optimizations should be performed after type checking and after all bound variables have been assigned unique names. A strategy for applying optimizations is discussed in the next section. Applicability of certain rules requires some semantic check such as “\underline{n} > 1”. We write such semantic predicates above the line but following an “&”.

R_{opt} is as follows:

R_{opt} = R_{Kid} ∪ R_{oi} ∪ R_{io} − {Ap_{n,m} − rule, Cons − rule}

where R_{oi} and R_{io} are defined below.

R_{Kid}

All Kid rewrite rules, except the Cons-rule, can be applied at compile time. However, care needs to be excercised in applying some rules such as the Application rule, because these can cause non-termination. A similar problem exists with WLoop and FLoop. We will assume that the user will annotate the program to indicate when these rules are safely applicable.

R_{oi} :

R_{oi} rules are applied “outside in”, as will be shown in the next section.

Inline Substitution

\frac{F = \underline{λn,m} (Z_{n}^{→}) . (E)}{Apn,m (F, X_{n}^{→}) − ; − ; → (RB [[E]]) [X_{n}^{→} / Z_{n}^{→}]}

An underlined λ corresponds to the Defsubst annotation in Id. It indicates that the function is substitutable at compiler time. Notice, if the user underlines a recursive procedure, the above rule will cause non-termination. This mechanism of underlining is often used in term rewriting systems to turn a set of rules into an equivalent strongly normalizing set of rules [8]. This mechanism also allows us to control the applicability of the loop rules. If the λ’s corresponding to predicate (P) and loop body (B) of a loop expression are not underlined, then the loop rule can not be applicable more than once. If the user wants to unfold loops more than once at compiler time then, he must annotate the loop to indicate this. When a loop in Id is annotated to be unfolded, then the translation from Id to Kid will generate underlined λ’s for P and B.

Partial Evaluation

\frac{F = λn,m (Z_{n}^{→}) . (E)}{Apply_{pe} (F, X) − ; − ; → \begin{matrix}\{f = λn−1,m (z_{n−1}^{→}) . ((RB [[E]]) [z_{n−1}^{→} / Z_{2,n}^{→}, X/Z_{1}]) \\ In f\} \end{matrix}}

\frac{F_{i} = Applyi (F, \underline{n}, X_{i}^{→}) ∧ F = λn,m (Z_{n}^{→}) . (E)}{Apply_{pe} (F_{i}, X) − ; − ; → \begin{matrix}\{f = λn−i−1,m (z_{n−i−1}^{→}) . ((RB [[E]]) [z_{n−i−1}^{→} / Z_{i+2,n}^{→}, X_{i+1}^{→} / Z_{i+1}^{→}]) \\ In f\} \end{matrix}}

A similar rule applies for \underline{λ_{n,m}}. Apply_{pe} indicates an Apply which the user has annotated for partial evaluation. Notice the difference with the previous rule. Instead of underlining the λ, the information is associated with the application. The rational being that we want to avoid the generation of too many specialized functions. This rule can also cause non termination, if an application in a recursive definition is annotated for partial evaluation. A more sophisticated strategy, that we have not explored yet, would try to compute some fixpoint in case of such an annotation.

Fetch Elimination

\frac{X = Cons (X_{1}, X_{2})}{Cons 1 (X) − ; − ; → X_{1}}

\frac{X = Cons (X_{1}, X_{2})}{Cons 2 (X) − ; − ; → X_{2}}

\frac{X = Cons (X_{1}, X_{2})}{List case (X, E_{1}, E_{2}) − ; − ; → E_{2}}

The above rules are useful because we do not reduce Cons (X_{1}, X_{2}) into Open cons at compile time.

Algebraic Identities

Alg_{1}
And (True, X) − ; − ; → X
Or (False, X) − ; − ; → X
+ (X, 0)  − ; − ; → X
∗ (X, 1)  − ; − ; → X
⋮

Alg_{2}
And (False, X) − ; − ; → False
Or (True, X) − ; − ; → True
∗ (X, 0)  − ; − ; → 0
− (X, X)  − ; − ; → 0
Equal? (X, X) − ; − ; → True
⋮

Alg_{3}

\frac{X = + (X_{1}, \underline{m}) & \underline{m} > 0}{Less (X_{1}, X) − ; − ; → True}

\frac{X = + (X_{1}, \underline{m}) & \underline{m} > 0}{Less (X, X_{1}) − ; − ; → False}

\frac{X = + (X_{1}, \underline{m}) & \underline{m} > 0}{Greater (X_{1}, X) − ; − ; → False}

\frac{X = + (X_{1}, \underline{m}) & \underline{m} > 0}{Equal? (X_{1}, X) − ; − ; → False}

⋮

Eliminating Circulating Variables

Suppose in the Id loop body of an Id program there exists an expression like “Next x = x ” , then the variable x can be made into a free variable of the loop and its circulation can be avoided. Without loss of generality we assume that the nextified variable to be eliminated is the last one.

\frac{\begin{matrix}P = λn (X_{n}^{→}) . (E) & | \\ B = λn,n (X′_{n}^{→}) . (\{n S In Z_{n−1}^{→}, X′_{n}\}) \end{matrix}}{WLoopn (P, B, Y_{n}^{→}, Y_{p}) − ; − ; → \{ \begin{matrix}p = λn−1 (x_{n−1}^{→}) . (RB[[E]] [x_{n−1}^{→} / X_{n−1}^{→}, Y_{n}/X_{n}]); \\ b = λ_{n−1,n−1} (x′_{n−1}^{→}) . (RB[[\{n−1 S In Z_{n−1}^{→}\}]] [x′_{n−1}^{→} / X_{n−1}^{→}, Y_{n}/X′_{n}]); \\ t_{n−1}^{→}= WLoopn−1 (p, b, Y_{n−1}^{→}, Y_{p}) \\ In t_{n−1}^{→}, Y_{n}\} \end{matrix}}

A similar optimization applies to for-loops.

Eliminating Circulating Constants

Suppose in the loop body there exists an expression like “Next x = t ”, where the variable t is a free variable of the loop body then its circulation can be avoided. Such situations may arise as a consequence of lifting invariants from a loop. The following example illustrates this transformation:

          { While (p x y) do
              Next x = t;
              Next y = f x y;
            Finally  y}

This may be transformed as follows:

        If (p x y) then
                { y1 = f x y;
                 In
                   { While (p t y1) do
                       Next y1 = f t y1;
                     Finally  y1} }
                    else
                 y

Notice that it is only after the first iteration that the value of “x” is t. Thus, to avoid the circulation of the nextified variable “x”, the loop has to be peeled once. This rule can be expressed as follows. Please note that we could have also written Z_{n} instead of t_{n} on the right-hand-side.

\frac{\begin{matrix}P = λn (X_{n}^{→}) . (E) & | \\ B = \underbrace{λn,n (X′_{n}^{→}) . (\{n S In Z_{n}^{→}\})}_{ρ} & F E(Z_{n}, ρ) \end{matrix}}{WLoopn (P, B, Y_{n}^{→}, Y_{p}) − ; − ; → Bool casen (Y_{p}, \{n p  = λn−1 (x_{n−1}^{→}) . (RB[[E]] [x_{n−1}^{→} / X_{n−1}^{→}, t_{n}/X_{n}]); b  = λn−1,n (x′_{n−1}^{→}) . (RB[[\{n−1 S In Z_{n−1}^{→}\}]] [x′_{n−1}^{→} / X′_{n−1}^{→}, t_{n}/X′_{n}]); t_{n}^{→} = Apn,n (B, Y_{n}^{→}); t_{p}  = Apn−1 (p, t_{n−1}^{→}); t′_{n−1}^{→} = WLoopn−1 (p, b, t_{n−1}^{→}, t_{p}); In t′_{n−1}^{→}, t_{n}\}, Y_{n}^{→})}

Peeling the Loop

FLoopn (U, D, B, X_{n}^{→}, X) − ; − ; → Bool casen (X, {n t_{2,n}^{→} = Apn,n−1 (B, X_{n}^{→}); t_{1} = + (X_{1}, D); t_{p} = < (t_{1}, U); t′_{n}^{→} = FLoopn (U, D, B, t_{n}^{→}, t_{p}) In t′_{n}^{→}},

X_{n}^{→})

Notice that the above rule is again applicable to the Floop generated on the RHS. To avoid unbounded number of applications of this rule the user will have to indicate how many times the loop peeling should be performed.

Loop Body Unrolling K times

\frac{& remainder ((U −X_{1})/D, \underline{k}) = 0}{FLoopn (U, D, B, X_{n}^{→}, X_{p}) − ; − ; → \{n b = λn,n−1(x_{n}^{→}) . (\{n−1 t_{2,n}^{1}^{→} = Apn,n−1 (B, x_{n}^{→}); t_{1}^{1} = + (X_{1}, D); t_{2,n}^{2}^{→} = Apn,n−1 (B, t_{n}^{1}^{→}); t_{1}^{2} = + (t_{1}^{1}, D); ⋮ t_{2,n}^{k}^{→} = Apn,n−1 (B, t_{n}^{k−1}^{→}) In t_{2,n}^{k}^{→}\} ); t_{n}^{→} = FLoopn (U, D, b, X_{n}^{→}, X_{p}); In t_{n}^{→}\}}

Suppose r = remainder((U − X_{1})/D, \underline{k}) , and r is not zero. We can still apply the above transformation by first peeling the loop r times. Notice, k has to be supplied by the user.

Rio :

These optimizations need to be applied “inside-out”, because that way bigger and bigger common expressions or expressions to be lifted can be formed. Furthermore these optimizations are only applied to side-effect-free expressions (sef’s) defined below:

Definition 7.1 (Side-effect-free expression) (1) Variables and constants are sef; (2) all PF_{n,m} (X_{n}^{→}) , except I array, Open cons, Apply, WLoop and FLoop, are sef;

(3) Bool Casem (X, E_{1}, E_{2}) is sef if E_{1} and E_{2} are sef; similarly for List Case.

(4) λ_{n,m}x.E is sef if E is sef;

(5) Ap_{n,m} (F, X_{n}^{→}) is sef if F is bound to a sef λ-abstraction and X_{n}^{→} are bound to sef’s;

(6) WLoop_{m} (P, B, X_{n}^{→}, Y) is sef if P and B are bound to sef λ-abstractions; similarly for FLoop;

(7) Blocks ..........

Common Subexpression Elimination

\frac{Y_{m}^{→}= PFN_{m} (X_{n}^{→})}{P F N_{m} (X_{n}^{→}) − ; − ; → Y_{m}^{→}}

Lift Free Expressions

\frac{& FE(E, λn,m (Z_{n}^{→}) . (\{m Y = E; S In X_{m}^{→} \}))}{λn,m (Z_{n}^{→}) . (\{m Y = E; S In X_{m}^{→} \}) − ; − ; → \{m \begin{aligned}t_{1} & = & E; \\ t & = & λn,m (Z_{n}^{→}) . (\{m Y = t_{1}; S In X_{m}^{→} \}) \\ & In t \} \end{aligned}}

Where FE(e, e′) return true if the expression e is free in e′. This optimization allows us to deal with loop invariants, that is, expressions that do not depend on the nextified variables. A similar rule applies for \underline{λ_{n,m}}. This rule in conjunction with the loop rules will cause loop invariants to be lifted from loops.

Hoisting Code out of a Conditional

\frac{& FE(E, (Bool casen (X, \{n Y = E; S In X_{n}^{→} \}, \{n Y′ = E; S′ In X′_{n}^{→} \})))}{Bool casen (X, \{n Y = E; S In X_{n}^{→} \}, \{n Y′ = E; S′ In X′_{n}^{→} \}) − ; − ; → \{n t_{1} = E; t_{n}^{→} = Bool casen (X, \{n Y = t_{1}; S In X_{n}^{→} \}, \{n Y′ = t_{1}; S′ In X′_{n}^{→}\}) In t_{n}^{→} \}}

7.2 A Partial Evaluator for Kid

Applying R_{kid} rules and R_{oi} rules is like partial evaluation of a Kid program. In the following we present an efficient strategy for applying R_{kid} and R_{oi} rules using the function EV.

However, space does not permit us to give a full interpreter. Therefore, we illustrate our strategy using a few carefully chosen rule, i.e. R_{CRS} ∪ {δ rules, Case rules for booleans, P select rule }. The extension of EV to other rules of R_{kid} and R_{oi} is straightforward. As usual, initially ρ and σ would be empty.

EV[[+ (\underline{m}, \underline{n})]] ρ σ = \underline{+(m, n)} EV[[Bool casem (True, E_{1}, E_{2})]] ρ σ = EV[[E_{1}]] ρ σ EV[[Bool casem (False, E_{1}, E_{2})]] ρ σ = EV[[E_{2}]] ρ σ EV[[Bool casem (X, E_{1}, E_{2})]] ρ σ = Bool casem (X, (EV[[E_{1}]] ρ σ), (EV[[E_{2}] ρ σ)])

EV[[P select (X, Y)]] ρ σ = Z if (L (X, σ)) = P store (X, Y, Z) EV[[{Ss; As; Bs In X}]] ρ σ = e

where e is obtained by the execution of the following program written in pseudo-Id

\{ \begin{matrix}blk, − = F&S(\{Ss; As; Bs In X\}); \\ flag = True; \\ If blk = ⊤ then ⊤ \\ else \\ \{ blk = \{ \begin{matrix}While flag do \\ Suppose blk is \{Ss; As; Bs In X\} \\ is = CC(σ ∪ Ss); \\ fs = ρ ∪ As; \\ next blk, next flag = If is = ⊤s then (⊤, False) else F&S(EV′ RHS(blk, is, fs)) \\ finally blk\} \end{matrix} \\ Suppose blk’ is \{Ss′; As;′ Bs′ In X′\} \\ is = CC(σ ∪ Ss); \\ fs = ρ ∪ As; \\ blk′′ = If is = ⊤s then (⊤, False) \\ else (EV RHS(blk′′, is, fs)) \\ In blk′′\}\} \end{matrix}

where

EV′ RHS([[Ss; As; X_{1} = E_{1}; ⋯ X_{n} = E_{n} In X_{i}]] ρ σ =

{Ss; As; X_{1} = EV′(E_{1}, ρ σ); ⋯ X_{n} = EV′(E_{n}, ρ σ) In X_{i}}

and the function EV′ given below unlike EV does not go inside encapsulators.

EV′[[+ (\underline{m}, \underline{n})]] ρ σ = \underline{+(m, n)}

EV′[[Bool casem (True, E_{1}, E_{2})]] ρ σ = E_{1} EV′[[Bool casem (False, E_{1}, E_{2})]] ρ σ = E_{2} EV′[[P select (X, Y)]] ρ σ = Z, True if (L ( X, σ)) = P store (X, Y, Z) else EV′[[E]] ρ σ = E

\begin{matrix}else \\ EV[[E]] ρ σ = E \end{matrix}

Theorem 7.2 (Normalization Theorem) Given terms M and N, and let R= R_{CRS} ∪ R_{kid} ∪ R_{oi}

M − ; → ; →_{R} N ⟹ EV[[M]] Nil Nil = N.

We do not describe the strategy for R_{io} rules because it requires choosing a data structure for Kid programs. These rules should be applied from inside out. Unfortunately R_{io} rules can trigger some R_{oi} optimizations. For example, the cse-rule may trigger an algebraic rule, such as, the equality rule.

Briefly the overall strategy for optimizations is as follows:

(1) apply R_{Kid} ∪ R_{oi} - {Ap_{n,m} − rule, Cons − rule }, from outside in, as explained in Section 7.2;

(2) apply R_{io} rules from inside out;

(3) if there is any change in the expression in step (2) go to step (1), else stop. We beleive that the above strategy is normalizing with respect to R_{opt}.

An other interesting question about optimizations is whether R_{opt} is confluent. We have shown in [1] that Alg_{3} rules cause R_{opt} to be non confluent. However, this is not a serious drawback because the cases where the confluence is lost are the ones where the unoptimized program would have produced no information .

7.3 Correctness of Optimizations

Definition 7.3 (Observational Equivalence) Given two terms M and N, M and N are said to be Observationally Equivalent iff

Print^{∗} (M) ≡ Print^{∗} (N).

For correctness, observational equivalence is not enough. It has to be shown that no context can distinguish between optimized and unoptimized term.

Definition 7.4 (Observational Congruence) Given two terms M and N, M and N are said to be Observationally Congruent iff

∀ C[□], Print^{∗} (C[M]) ≡ Print^{∗} (C[N]) .

Definition 7.5 (Correctness) An optimizer (A,R_{opt}) of (A,R) is correct iff

∀ M ∈ A, M − ; → ; →_{R_{opt}} N ⟹ \begin{matrix}(i) Print^{∗}(M) ⊑ Print^{∗}(N) and \\ (ii) Print^{∗}(N) = ⊤ ⟹ Print^{∗}(M) = ⊤. \end{matrix}

Notice that condition (ii) is needed because ⊤ is higher than all print values and we do not want the optimizer to take all programs to ⊤.

It is believed that all optimizations presented in Section 7.1 preserve correctness, though this has been proven for only a small subset of them so far [1]. In general, correctness of an optimization is difficult to prove. However, some optimizations can be proven correct easily because they are derived rules.

Definition 7.6 (Derived rule) A rule r is said to be derived in R iff

M − ; − ; →^{r} M_{1} ⟹ ∃ M_{2}, M − ; → ; →_{R} M_{2} ∧ M_{1} − ; → ; →_{R} M_{2}

Corollary 7.7 Given an optimizer (A,R_{opt}) of (A,R),

∀ r ∈ R_{opt}, r is derived ⟹ (A, R_{opt}) is correct .

Lemma 7.8 All R_{Kid} rules, Inline Substitution and Fetch Elimination are derived rules, and hence correct.

Unfortunately, it is not always possible to mimic inside R_{Kid} what an optimizations does. Therefore, we introduce a notion of graph equivalence, which is useful for proving the correctness of cse-like rules. The terms of a graph may be described by the grammar of Figure 3 by changing the definition of the SE syntactic category with SE = E. Graphs for a Kid term can be generated by applying a new substitution rule, called the E substitution rule.

E substitution rule

\frac{X = E}{X − ; − ; → E}

where E can be any side-effect free expression.

Suppose RCRS^{′} be {E substitution rule, Block flattening rule, Multivariable rule}.

Definition 7.9 (Unravelled form) Let N be the normal form of a term M with respect to RCRS^{′}. U(M), the unravelling form of a term M, is the term obtained by deleting from N all bindings of the form X = E (where E is a side-effect free expression).

Notice that the unravelled version of a term is not necessarily a tree.

Definition 7.10 (graph-equivalence ≡_{g}) Two terms M and N are said to be graphequivalent, if

U(M) ≡_{α} U(N).

Corollary 7.11 Given an optimizer (A,R_{opt}) of (A,R),

∀ M, N ∈ A, [M − ; − ; →_{opt} N ⟹ M ≡_{g} N] ⟹ (A, R_{opt}) is correct .

Lemma 7.12 Let R be the set {Common subexpression elimination rule, lift free expressions rule, Hoisting code out of a conditional rule }.

M − ; − ; →_{R} N ⟹ M ≡_{g} N.

Hence cse-like rules are correct.

8 P-TAC: Parallel Three Address Code

8.1 P-TAC

The syntax of P-TAC is given in Figure 6. In P-TAC, I-structure Storage is modelled in greater detail which requires the notion of Labels. All composite objects, that is, data structures and closures are stored in I-structure store and assigned unique labels, which are treated as constants that can be substituted freely.

8.2 Rewrite rules of P-TAC

In the following V stands for a ground value.

δ rules

+ (\underline{m}, \underline{n}) − ; − ; →_{δ} \underline{+(m, n)} ; ⋮

Conditional rule

Dispatchn,m (\underline{i}, E_{i−1}^{→}, E_{i}, E_{i+1,n}^{→}) − ; − ; → E_{i}

UDF ∈ User Defined Function
GV ∈ Ground Value
Integer  ::= 1 | 2 | ⋯ | \underline{n} | ⋯
Boolean ::= True | False
V ariable ::= x | y | z | ⋯ | a | b | ⋯ | f | ⋯ | x_{1} | x_{2} | ⋯
MV_{m}  ::= \underbrace{V ariable, ⋯, V ariable}
Label  ::= L | L1 | ⋯ | L′ | ⋯
PF 1  ::= Negate | Not | Allocate
PF 2  ::= + | − | ∗ | ⋯ | Less | Equal? | P select
PF 3  ::= Ack store
UDF  ::= F | G | ⋯
SE  ::= V ariable | UDF | GV
SE_{m}  ::= \underbrace{SE, ⋯, SE}_{m}
GV  ::= Integer | Boolean | () | Label | Error | ⊤
E_{1}  ::= SE | PF 1 (SE) | PF 2 (SE_{2}) | PF 3 (SE_{3}) | Apn (SE_{n+1})

| Dispatchn (SE, \underbrace{E, ⋯, E}_{n}) | WLoop1 (SE_{4}) | FLoop1 (SE_{5}) | Block

E_{m}  ::= SE_{m} | Apn,m (SE_{n+1}) | Dispatchn,m (SE, \underbrace{E_{m}, ⋯, E_{m}}_{n})

| WLoopm (SE_{m+3}) | FLoopm (SE_{m+4}) | Block_{m}

Block_{m}  ::= {m [Statement; ]^{∗} In SE_{m}}
Statement ::= Binding | Command | Store Error
Command ::= P store (SE_{3}) | ⊤_{s}
Binding ::= MV_{m} = E_{m}

Figure 6: Grammar of P-TAC

I structure rules

Allocate (\underline{n}) − ; − ; → L

where L is a brand new label.

\frac{P store (L, \underline{i}, V)}{P select (L, \underline{i}) − ; − ; → V}

\frac{P store (L, \underline{i}, V)}{P store (L, \underline{i}, V′) − ; − ; → ⊤s}

where V is either an Integer or a Boolean or a Label or Error. The following rules are the same as the corresponding rules in Kid.

Application rule

\frac{F = λn,m (Z_{n}^{→}) . (E)}{Apn,m (F, X_{n}^{→}) − ; − ; → (RB[[E]]) [X_{n}^{→} / Z_{n}^{→}]}

A similar rule applies for \underline{λ_{n,m}}.

Loop rules

WLoopn (P, B, X_{n}^{→}, True) − ; − ; → {n t_{n}^{→} = Apn,n (B, X_{n}^{→}); t_{p} = Apn (P, t_{n}^{→}); t′_{n}^{→} = WLoopn (P, B, t_{n}^{→}, t_{p}) In t′_{n}^{→}}
WLoopn (P, B, X_{n}^{→}, False) − ; − ; → X_{n}^{→}

FLoopn (U, D, B, X_{n}^{→}, True) − ; − ; → {n t_{2,n}^{→} = Apn,n−1 (B, X_{n}^{→}); t_{1} = + (X_{1}, D); t_{p} = < (t_{1}, U); t′_{n}^{→} = FLoopn (U, D, B, t_{n}^{→}, t_{p}) In t′_{n}^{→}}
FLoopn (U, D, B, X_{n}^{→}, False) − ; − ; → X_{n}^{→}

Multivariable rule

X_{n}^{→} = Y_{n}^{→} − ; − ; → (X_{1} = Y_{1}; ⋯ X_{n} = Y_{n})

Substitution rules

\frac{X = Y}{X − ; − ; → Y} ; \frac{X = V}{X − ; − ; → V}

where V is either an Integer or a Boolean or a Label or Error.

Block Flattening rule

{m X_{n}^{→} = {n SS_{1}; SS_{2}; ⋯  {m X_{n}^{→} = Y_{n}^{→};
In Y_{n}^{→}} − ; − ; → SS_{1}; SS_{2}; ⋯
S_{1}; ⋯ S_{n}  S_{1}; ⋯ S_{n}
In Z_{m}^{→}}  In Z_{m}^{→}}

Propagation of ⊤

\begin{matrix}\{m X = ⊤; S_{1}; ⋯ S_{n} In Z_{m}^{→} \} & − ; − ; → & ⊤ \\ \{m ⊤_{s}; S_{1}; ⋯ S_{n} In Z_{m}^{→} \} & − ; − ; → & ⊤ \end{matrix}

9 Translation of Kid into P-TAC

Prior to translating Kid to P-TAC, λ-lifting is performed. A Kid program after λ -lifting only contains closed λ-expressions. The translator, given a Kid program, produces the corresponding P-TAC program and a set, “D” , of definitions. The set D is initialized with constants that are introduced by the translator.

9.1 Simple Kid Expressions

TE[[X]] = X

TE[[C]] = C

where C ranges over Integers and Booleans.

TE[[Negate (X)]] = Negate (X)

The same holds for Not.

TE[[+ (X, Y)]] = + (X, Y)
TE[[WLoopm (P, B, X_{m}^{→}, X_{b})]] = WLoopm (P, B, X_{m}^{→}, X_{b})

The same holds for FLoop.

TE[[Bool casem (X, E_{1}, E_{2})]] = {m t = BooltoInt (X); t_{m}^{→} = Dispatch2,m (t, E_{1}, E_{2}); In t_{m}^{→}}

BooltoInt is a coercion function which converts True to 0 and False to 1.

TE[[{m X_{1} = E_{1}; ⋯ X_{n} = E_{n}; S_{1}; ⋯ S_{m} In Y_{m}^{→} }]] = {m X_{1} = TE[[E_{1}]]; ⋮ X_{n} = TE[[E_{n}]]; TS[[S_{1}]]; ⋮ TS[[S_{m}]]; In Y_{m}^{→} }

9.2 Data Structure Representations

There are usually several reasonable ways to represent each data structure in terms of a P-TAC array. For each type we present one representation, though not necessarily the most efficient one. We have included a “type” tag field for all composite objects, even though it is not needed by the P-TAC interpreter since Id is a statically typed language. We might need types information for other reasons, such as, garbage collection, and printing values in a partially executed program.

Tuples

All n-tuple data types may be represented as follows:

TE[[Make tuplen (X_{n}^{→})]] = \{t = Allocate (\underline{n + 1});

P store (t, Type, “n tuple”);

P store (t, 1, X_{1});

⋮

P store (t, \underline{n}, X_{n});

In t}

TE[[Detuplem (X)]] = \{m t_{1} = P select (X, 1); ⋮ t_{m} = P select (X, \underline{m}); In t_{m}^{→}\}

1D-Arrays

1D-arrays “Array (l, u)” may be represented as follows:

The constant definition Headersize = 2 should be included in the set “D”.

TE[[nD Bounds (X)]] = P select (X, Bounds)

TE[[I array (X)]] = \{ \begin{matrix}l & = & P select (X, Lower); \\ u & = & P select (X, Upper); \\ s & = & − (u, l); \\ size & = & + (s, 3); \\ t & = & Allocate (size); \\ P store (t, Type, “Array”); \\ P store (t, Bounds, X); \\ In t\} \end{matrix}

TE[[P 1D select (X_{1}, X_{2})]] = \{ \begin{matrix}t_{b} & = & P select (X_{1}, Bounds); \\ l & = & P select (t_{b}, Lower); \\ t_{1} & = & − (X_{2}, l); \\ t_{2} & = & + (t_{1}, Headersize); \\ t & = & P select (X_{1}, t_{2}) \\ & In t\} \end{matrix}

TE[[P 1D store (X_{1}, X_{2}, X_{3})]] = \{ \begin{matrix}t_{b} & = & P select (X_{1}, Bounds); \\ l & = & P select (t_{b}, Lower); \\ t_{1} & = & − (X_{2}, l); \\ t_{2} & = & + (t_{1}, Headersize); \\ t & = & P store (X_{1}, t_{2}, X_{3}) \\ & In t\} \end{matrix}

A representation that will be more efficient for computing the slot address may want to store l and u values redundantly in two additional fields.

2D-Arrays

The translation given below assumes that the matrix is stored in the row major order. The following constant definitions should be included in the set “D”.

First dim = 1 Second dim = 2
First index = 1 Second index = 2
TE[[I 2D array (X)]] = \{ \begin{matrix}d_{1} & = & P select (X, First dim); \\ d_{2} & = & P select (X, Second dim); \\ l_{1} & = & P select (d_{1}, Lower); \\ u_{1} & = & P select (d_{1}, Upper); \\ l_{2} & = & P select (d_{2}, Lower); \\ u_{2} & = & P select (d_{2}, Upper); \\ s_{1} & = & − (u_{1}, l_{1}); \\ s_{2} & = & − (u_{2}, l_{2}); \\ s′_{1} & = & + (s_{1}, 1); \\ s′_{2} & = & + (s_{2}, 1); \\ s & = & ∗ (s′_{1}, s′_{2}); \\ size & = & + (s, Headersize); \\ t & = & Allocate (size); \\ P store (t, Type, “Array”); \\ P store (t, Bounds, X); \\ In t\} \end{matrix}

Translation for I nD array can be given in a similar fashion.

TE[[P 2D select (X_{1}, X_{2})]] = \{ \begin{matrix}b & = & P select (X_{1}, Bounds); \\ d_{1} & = & P select (b, First dim); \\ d_{2} & = & P select (b, Second dim); \\ l_{1} & = & P select (d_{1}, Lower); \\ u_{1} & = & P select (d_{1}, Upper); \\ l_{2} & = & P select (d_{2}, Lower); \\ u_{2} & = & P select (d_{2}, Upper); \\ r & = & − (u_{2}, l_{2}); \\ r′ & = & + (r, 1); \\ i & = & P select (X_{2}, First index); \\ j & = & P select (X_{2}, Second index); \\ i′ & = & − (i, l_{1}); \\ j′ & = & − (j, l_{2}); \\ o & = & ∗ (i′, r′); \\ o′ & = & + (o, 1); \\ ad & = & + (o, j′); \\ ad′ & = & + (ad, Headersize); \\ t & = & P select (X_{1}, ad′) \\ In t\} \end{matrix}

A similar rule applies for P 2D store, and higher dimensional arrays.

Lists

The list data type can be represented as follows:

It is often possible to store niladic constructors using much less space by combining them with pointers. We won’t discuss such machine dependent representations in this paper.

The following constant definitions should be included in the set “D”.

Nil size = 2
Cons size = 4
Nil Tag = 0
Cons Tag = 1

TE[[Nil]] = {t = Allocate (Nilsize); P store (t, Type, “List”); P store (t, Tag, Nil Tag); In t}

TE[[Open cons ()]] = \{ \begin{matrix}t = Allocate (Cons size); \\ P store (t, Type, “List”); \\ P store (t, Tag, Cons Tag); \\ In t\} \end{matrix}

TE[[Cons 1 (X)]] = P select (X, Hd)
TE[[Cons 2 (X)]] = P select (X, Tl)

TE[[Cons (X_{1}, X_{2})]] = \{ \begin{matrix}t = Allocate (Cons size); \\ P store (t, Type, “List”); \\ P store (t, Tag, Cons Tag); \\ P store (t, Hd, X_{1}); \\ P store (t, Tl, X_{2}); \\ In t\} \end{matrix}

TS[[Cons store 1 (X_{1}, X_{2})]] = P store (X_{1}, Hd, X_{2});
TS[[Cons store 2 (X_{1}, X_{2})]] = P store (X_{1}, Tl, X_{2});
TE[[List casem (X, E_{1}, E_{2})]] = {m t = P select (X, Tag); t_{m}^{→} = Dispatch2,m (t, E_{1}, E_{2}); In t_{m}^{→}}

9.3 Function Calls and Closures

At the machine level, the apply operator checks if the arity of the function has been satisfied or not, and in case the arity has not been satisfied, it stores the argument in a data stucture called a closure. There is great choice in representing closures and associated function calling conventions. In fact, a function can be compiled using several different calling conventions and the compiler can pick up the most appropriate one for a given application. As an illustration we chose the following representation for the closure data type:

The constant definition Closure size = 5 should be included in the set “D”.

We begin by describing a procedure that builds a closure given an old closure and an argument.

Make closure = \underline{λ} (cl, X) . (\{ \begin{matrix}f & = & P select (cl, Funcname); \\ f_{fc} & = & P select (cl, Fastcallname); \\ n & = & P select (cl, Arity); \\ ch & = & P select (cl, Chain); \\ cl′ & = & Allocate (Closure size); \\ P store (cl′, Type, “Closure”); \\ P store (cl′, Functionname, f); \\ P store (cl′, Fastcallname, f_{fc}); \\ P store (cl′, Arity, n′); \\ P store (cl′, Chain, ch′); \\ n′ & = & − (n, 1); \\ ch′ & = & Ap2 (Arg chain, X, ch); \\ In cl′\} ) \end{matrix}

where the function to build argument chains is defined as follows:

Arg chain = \underline{λ} (X, Xs) . ( \begin{matrix}\{xs′ = Allocate (2); \\ P store (xs′, Arg, X); \\ P store (xs′, Rest, Xs); \\ In xs′\} ) \end{matrix}

The argument chain can be destructured using the following function:

Argsn = \underline{λ} (X) . (\{n t_{1}  = P select (X, Chain); a_{n} = P select (t_{1}, Arg); t_{2}  = P select (t_{1}, Rest); a_{n−1} = P select (t_{2}, Arg); t_{3}  = P select (t_{2}, Rest); ⋮ a_{1}  = P select (t_{n−1}, Arg); In a_{n}^{→}\} )

These three definitions must be included in the “D” set.

Now we can give the translation for the apply operator. As stated earlier, the apply basically checks to see if the arity is satisfied and either makes a new closure or calls Ap.

TE[[Apply (F, X)]] = \{ \begin{matrix}n & = & P select (F, Arity); \\ fire_{b} & = & Equal? (n, 1); \\ fire_{i} & = & BooltoInt(fire_{b}); \\ res & = & Dispatch2,2 (fire_{i}, \\ & \{ \begin{matrix}fun & = & P select (F, Functioname); \\ as & = & P select (F, Chain); \\ as′ & = & Ap2 (Arg chain, X, as); \\ res′ & = & Ap (fun, as′); \\ In res′\}, \end{matrix} \\ & Ap2 (Make closure, F, X)) \\ In res\} \end{matrix}

TE[[Apn,m (F, X^{→})]] = {m f′ = P select (F, Fastcallname); t_{m}^{→} = Apn,m (f′, X^{→}); In t_{m}^{→} }

The only thing that remains to be described is the creation of the first closure for a function. It is built as a consequence of translating a λ-expression.

TE[[λn (X_{n}^{→}) . (E)]] = {cl = Allocate (Closure size); P store (cl, Type, “Closure”);

P store (cl, Functioname, ‘T_{c});
P store (cl, Fastcallname, ‘T_{fc});
P store (cl, Arity, \underline{n});
P store (cl, Chain, “End”);
In cl}

The following two function definitions are included in the set D.

T_{c} = λ1 (Xs) . \{ \begin{matrix}X_{n}^{→} & = & Ap1,n (Argsn, Xs); \\ t & = & TE[[E]]; \\ In t\} \end{matrix}

T_{fc} = λn (X_{n}^{→}) . TE[[E]]

‘T_{c} indicates the name T_{c} and not the value associated to T_{c}. Note that TE[[E]] can be computed once and shared between the curried aabd the fastcall version of the function. The same translation rule applies for \underline{λn}.

10 Signals

Before introducing signals, the P-TAC program is canonicalized, that is, all blocks are flattened and variables and values are substituted. Furthermore, dead code should be eliminated. We add signals only to non-strict combinators, and to combinators that produce side-effect, such as P store. The output of a strict operator can be interpreted as the signal that the instruction has indeed fired. We give the signal transformation using the translation functions S, SE and SC. The transformation is applied also to each constant definition in “D” .

S[[λn,m (X_{n}^{→}).{m Y_{1}  = Se_{1} ; ⋮ ; Y_{n}  = Se_{n} ; Y_{n+1} = Nse_{1} ; ⋮ ; Y_{n+m} = Nse_{m} ; C_{1} ; ⋮ ; C_{k} ; In R_{m}^{→}}]] = λn,m+1 (X_{n}^{→}) . ({m+1 Y_{1}  = Se_{1} ⋮ Y_{n}  = Se_{n} Y_{n+1}, S_{1} = SE[[Nse_{1}]] ⋮ Y_{n+m}, S_{m} = SE[[Nse_{m}]] S_{m+1}  = SC[[C_{1}]]; ⋮ S_{m+k}  = SC[[C_{k}]]; S′  = Syncm+k+i (Deadvariables, S_{m+k}^{→}) In R_{m}^{→}, S′})

Where Se_{i} stands for an expression involving strict operators, whilst Nse_{i} stands for either an applicative or a loop expression. Deadvariables are the parameters that are not being used in the body of the function.

SE[[WLoopn (P, B, Y_{n}^{→}, Y)]] = WLoopn^{′} (P, B, Y_{n}^{→}, S_{p}, Y)

Where S_{p} is the signal associated with the invocation of the predicate.

SE[[Apn,m (F, X_{n}^{→})]] = Apn,m+1 (F, X_{n}^{→}) SC[[P store (X, I Z)]] = Ack store (X, I Z)

Where Ack store is a new P-TAC function symbol of arity 3, which generates a Signal when the store actually takes place. The new rewrite rules are:

WLoopn^{′} (P, B, X_{n}^{→}, S, True) − ; − ; → {n+1 t_{n}^{→}, S_{b} = Apn,n+1 (B, X_{n}^{→}); t_{p}, S_{p} = Apn,2 (P, t_{n}^{→}); S′  = Sync3 (S, S_{b}, S_{p}); t′_{n}^{→}, S_{l} = WLoopn^{′} (P, B, t_{n}^{→}, S′, t_{p}) In t′_{n}^{→}, S_{l}}

WLoopn^{′} (P, B, X_{n}^{→}, S, False) − ; − ; → X_{n}^{→}, S
Ack store (L, \underline{i}, V)

− ; − ; →
{t = Signal;
P store (L, \underline{i}, V);
In t}
Syncn (V_{n}^{→}) − ; − ; → ()

Sync produces a void value when all the signals are received.

11 Conclusions

Kid goes a long way towards expressing many machine independent implementation concerns. Since Kid has a proper calculus associated with it, correctness issues can be handled at an abstract level. Kid is central to the current restructuring of the Id compiler which is already being used by at least 4 or 5 groups to generate code for their machines by just changing back end of the compiler. The major deficiency of Kid is the inability to express storage reuse. We believe a language with a proper calculus which does not obscure parallelism and which can express storage reuse would be extremely useful in practical compilers for functional and other declarative languages.

Some of the important optimizations that we currently perform in the Id compiler but have not included in R_{opt} are dead code elimination, loop variable induction to hoist array bound checking, and array subscript analyses. These optimizations do not fit in the CRS model very well. A better formalization of these optimizations would be very useful.

Acknowledgments

We would like to thank Shail Aditya for reading several earlier drafts of this paper and suggesting changes for better readability. This paper has benefitted a lot by informal discussions with the members of Computation Structures Group.

References

[1] Z. M. Ariola and Arvind. P-TAC: A parallel intermediate language. In Proc. ACM Conference on Functional Programming Languages and Computer Architecture, London, 1989. Also: CSG Memo 295, MIT Laboratory for Computer Science, 545 Technology Square, Cambridge, MA 02139, USA.

[2] Z. M. Ariola and Arvind. Compilation of Id^{−}: a subset of Id. Technical Report CSG Memo 315, MIT Laboratory for Computer Science, 545 Technology Square, Cambridge, MA 02139, USA, July 1990. Revised 1 November.

[3] Arvind, R. S. Nikhil, and K. K. Pingali. I-Structures: Data Structures for Parallel Computing. ACM Transactions on Programming Languages and Systems, 11(4), October 1989. An earlier version appeared in Proceedings of the Workshop on Graph Reduction, Santa Fe, New Mexico, USA, September/October 1986, Springer-Verlag LNCS 279, pages 336-369.

[4] H. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, 1984.

[5] B. Courcelle. Fundamentals Properties of Infinite Trees. D. Reidel Publishing Company, 1982.

[6] N. de Bruijn. Lambda calculus notation with nameless dummies: A tool for automatic formula manipulation, with application to the church-rosser theorem. In Koninkijke Nederlandse Akademie van Wetenschappen, Series A, Mathematical Sciences, 1972.

[7] T. Kenneth R. A Compiler for the MIT Tagged-Token Dataflow Architecture. Technical Report LCS TR-370, MIT Laboratory for Computer Science, 545 Technology Square, Cambridge, MA 02139, August 1986.

[8] J. Klop. Term rewriting systems. Course Notes, Summer course organized by Corrado Boehm, Ustica,Italy, September 1985.

[9] R. S. Nikhil. Notes on Translating List Comprehensions in Id. Technical report, MIT Laboratory for Computer Science, 545 Technology Square, Cambridge, MA 02139, USA, January 1988.

[10] R. S. Nikhil. Id (Version 90.0) Reference Manual. Technical Report CSG Memo 284-a, MIT Laboratory for Computer Science, 545 Technology Square, Cambridge, MA 02139, USA, July 1990.

[11] R. S. Nikhil and Arvind. Notes on Pattern Matching Algorithm. Technical report, MIT Laboratory for Computer Science, 545 Technology Square, Cambridge, MA 02139, USA, February 1988.

[12] R. S. Nikhil and Arvind. Programming in Id: a parallel programming language. 1990. (book in preparation).

[13] P. J. Simon L. The implementation of Functional Programming Languages. Prentice-Hall International, Englewood Cliffs, N.J., 1987.

[14] J. Thomas. Lambda lifting: Transforming programs to recursive equations. In Springer-Verlag LNCS 201 (Proc. Functional Programming Languages and Computer Architecture, Nancy, France), September 1985.

Contents

1 Introduction 3

2 Desugared Id^{−} 5

3 Kid : The Kernel Id Language 8

4 Translating Desugared Id^{−} into Kid 11 4.1 Simplification of Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . 11 4.2 Definition of Standard Functions . . . . . . . . . . . . . . . . . . . . . . . 17 4.3 Pattern Matching: Elimination of Complex Patterns . . . . . . . . . . . . . 18

5 Contextual Reduction Systems 24 5.1 Basic Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 5.2 Basic Rules of Contextual Reduction System’s (RCRS) . . . . . . . . . . . 26 5.3 Canonical Forms of terms in a CRS . . . . . . . . . . . . . . . . . . . . . . 28

6 Contextual Reduction System of Kid 29 6.1 Kid Rewrite Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 6.2 Printable Values and Answer of a Kid Term . . . . . . . . . . . . . . . . . 33 6.3 An Interpreter to Compute the Answer of a Kid term . . . . . . . . . . . . 36

7 Optimizations of Kid Programs 39 7.1 Optimizations as Rewrite rules (R_{opt}) . . . . . . . . . . . . . . . . . . . . 39 7.2 A Partial Evaluator for Kid . . . . . . . . . . . . . . . . . . . . . . . . . . 45 7.3 Correctness of Optimizations . . . . . . . . . . . . . . . . . . . . . . . . . . 48

8 P-TAC: Parallel Three Address Code 50 8.1 P-TAC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 8.2 Rewrite rules of P-TAC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50

9 Translation of Kid into P-TAC 54 9.1 Simple Kid Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 9.2 Data Structure Representations . . . . . . . . . . . . . . . . . . . . . . . . 55

9.3 Function Calls and Closures . . . . . . . . . . . . . . . . . . . . . . . . . . 61 10 Signals 64 11 Conclusions 66