The Transformation Calculus

Jacques Garrigue

Research Institute for Mathematical Sciences Kyoto University, Kitashirakawa-Oiwakecho Sakyo-ku, Kyoto 606-01 JAPAN

                   E-mail garrigue@kurims.kyoto-u.ac.jp

October 23, 1995

Abstract

The lambda-calculus, by its ability to express any computable function, is theoretically able to represent any algorithm. However, notwithstanding their equivalence in expressiveness, it is not so easy to find a natural translation for algorithms described in an imperative way.

The transformation calculus, which only extends the notion of currying in lambdacalculus, appears to be able to correct this flaw, letting one implicitly manipulate a state through computations.

This calculus remains very close to lambda-calculus, and keeps most of its properties. We prove here confluence, strong-normalization in presence of a typing system, and present a model of the typed calculus.

Topics input/output models and state transformers, lambda calculus (formal aspects), formal semantics.

1 Introduction

Currying is as old as lambda calculus. For the simple reason that, in raw lambda calculus —without pairing or similar built-in constructs—, this is the only way to represent multiargument functions. This just means that we will write

λx.λy.M[x, y]

in place of

(x, y) ↦ M[x, y].

At this stage appears a first asymmetry: while in the pair (x, y) the two variables play symmetrical roles, in λx.λy.M they don’t. An implicit order was introduced. Materially this means that we can partially apply our function directly on x but not on y.

We now look at types. There, currying can be seen as isomorphism of types [BCL90]:

(A × B) → C ≃ A → B → C.

Here comes another asymmetry: why don’t we get any similar isomorphism for A → (B × C).

The calculus we will present here generalizes currying to these two kinds of symmetries: between arguments, and between input and output. For the first one, we are just taking over the mechanism of label-selective currying developed previously [AKG93, GAK94].

For the second one we develop a new notion of composition, which, contrary to the usual one, is compatible with currying.

The resulting system, transformation calculus, is a conservative extension of lambda calculus. Why such a name? Because this essentially syntactic extension —semantics remain very similar— provides us with a new way of representing state transformations, i.e. state being represented by labeled input parameters, that may get returned by our term. Handling state as a supplementary parameter that gets returned with the result is not new. But by extending currying we get more flexibility, in two ways. First, since a part of the state is no more than a labeled parameter, we can dynamically extend it by simply adding a new parameter at some point in our term. Second, selective currying lets a transformation ignore parts of the state it doesn’t need. They will just be left unmodified.

To demonstrate our point, we introduce scope-free variables, which are trivially encoded in the transformation calculus, and can be used in place of usual scoped mutable variables, in the Algol tradition. Since they have no syntactic scope, scope-free variables respect dynamic binding rather than static binding; but they are more flexible than Algol variables, while simulating blocks and stack discipline.

The rest of this paper is composed as follows. In Section 2 we introduce progressively the different features which form the transformation calculus. In this process we are brought to define streams, which are formalized in Section 3. Section 4 is devoted to the formal definition of the transformation calculus. Sections 5, 6 and 7 respectively define and give the fundamental properties of scope-free variables, a simply typed transformation calculus, and semantics for this calculus. Related works are presented in Section 8. Finally, Section 9 concludes. Proofs are given in appendix.

2 Composition and streams

We first introduce informally and progressively the features of our calculus. We start from the classical pure lambda-calculus, that is^{1}

M ::= x | λx.M | (M).M

with β-reduction

(N).λx.M →_{β} [N/x]M

and where terms are considered modulo α-conversion (renaming of bound variables).

2.1 Implicit currying

Currying is the fundamental transformation by which multi-argument functions are encoded in the lambda-calculus. It can appear in abstractions as well as applications. For instance f(a, b) will be encoded as (b).(a).f, and λ(x, y).M becomes λx.λy.M.

1Application, denoted by a dot, is written postfix, and is left associative.

This operation does not modify the nature of calculations, since clearly (a, b).λ(x, y).M and (b).(a).λx.λy.M reduce to the same [a/x, b/y]M (provided x and y are distinct variables). Currying can be extended to an arbitrary number of arguments, i.e. λ(x_{1}, …, x_{n}).M is encoded as λx_{1}. · · · .λx_{n}.M. As long as we encode similarly applications and abstractions, no problem should appear.

By implicit currying, we mean that we will write curried and uncurried versions of terms indifferently, always supposing that we reduce curried ones. Of course we work in the pure lambda-calculus without pairing, so that no confusion is possible. The new syntax becomes

M ::= x | λ(x, …).M | (M, …).M

where abstracted variables under the same λ should be distinct. Implicit currying is expressed by the two structural equivalences:

If all x_{i}’s are distinct then

λ(x_{1}, …, x_{n}).M ≡_{λ} λ(x_{1}, …, x_{k}).λ(x_{k+1}, …, x_{n}).M
(N_{1}, …, N_{n}).M ≡_{.} (N_{k+1}, …, N_{n}).(N_{1}, …, N_{k}).M

≡ is defined as the reflexive, symmetric and transitive closure of ≡_{ς}’s.

β-reduction applying on the implicitly curried form, a reduction step only binds one variable.

(a, b).(λ(x, y).M) →_{β} (b).(λ(y).[a/x]M) →_{β} [a/x, b/y]M

In fact, if we remember the habit many have of writing (λxy.M) a b for the above term, we have done absolutely nothing new. However this syntax lets us emphasize some natural groupings of values. For instance the encoding of pairs in lambda-calculus can be written as λ(x, y).λf.(x, y).f.

2.2 Composition

The next step is to introduce a binary composition operator (“;”)^{2} and a transformation constructor (“↓”).

M ::= … | ↓ | M; M

A transformation is a term such that, provided enough input, it gets a transformation constructor at its head position.

Together we add a new reduction rule, and a new structural equivalence, to eliminate compositions. Some other equivalences are introduced in the actual calculus, to enable earlier flattening of terms, but we leave them for later.

\begin{aligned}↓; M & →_{↓} & M \\ (N_{1}, …, N_{k}).(M_{1}; M_{2}) & ≡_{.;} & (N_{1}, …, N_{k}).M_{1}; M_{2} \end{aligned}

We can see the sequencing role of composed pairs as follows: when we apply (M_{1}; M_{2}) to a sufficient input tuple of arguments, we first apply M_{1} to this tuple, get (hopefully) a tuple-term (term of form (N_{1}, …, N_{k}).↓) as result of its reduction, and apply M_{2} to this result tuple.

2Both the dots of abstraction and application bind tighter than composition.

It just looks like if we added a stack machine into the lambda-calculus. For instance, we can write the transformation that switches two terms on top of a stack as sw = λ(x, y).(y, x).↓, and can apply it to an input tuple of any size:

(a, b, c) .λ(x, y).(y, x).↓
→_{β} (b, c) .λ(y).(y, a).↓
→_{β}  (c) .(b, a).↓
≡_{.} (b, a, c) .↓

Composed with another term, it plays the same role as the C = λfxy.fyx combinator; but in a postfix way.

(c) .(a, b).(sw; K)
≡_{.} (a, b, c) .(sw; K)
≡_{.;} (a, b, c) .sw; K
→^{∗} (b, a, c) .↓; K
≡_{.;} (b, a, c) .(↓; K)
→_{↓} (b, a, c) .K.x
→^{∗}  (c) .b

Since we are in the lambda-calculus, we can define the fix-point operator Y. We just define then loops in terms of this operator. The functional for a while-do loop can be defined as

while = Y (λwhl.

λ(end, do).(end;

λb.if b then do; (end, do).whl else ↓)

)

The end-condition is a transformation that adds to its input a boolean b, false to end, true to go on, leaving the rest in position. do may change the values from the input, but not their number. Such a functional works on a state of any size.

An imperative version of Euclid’s algorithm for the greatest common divisor can then be written

(λ(x).(x ≠ 0, x).↓,
λ(x, y).(y mod x, x).↓).while;
λ(x, y).y

We notice here an important difference between this “while” functional and something equivalent written using pairing. Here our end-condition only uses x, whereas a functional using pairing would have required it to receive the whole state even though y is not needed. This remark will become even more important when we will add to our calculus the power of selective currying.

2.3 Selective currying

Combining lambda-calculus and a stack machine should be enough to express algorithms both in their functional and imperative form. However, in chosing a reduction system rather than an equational theory to express our calculus, we are interested in giving some meaning to the reductions themselves. We can think of various meanings, like complexity, sequentiality constraints, etc... If we do such an analysis, then we see that, with simple implicit currying, we need much more reduction steps than should be necessary. That is, when we want to access the 5^{th} element of a tuple we have to extract successively all the elements before it, and put them back:

λ(x_{1}, x_{2}, x_{3}, x_{4}, x_{5}).(x_{5}, x_{1}, x_{2}, x_{3}, x_{4}).↓

Even more than the number of reductions, we should be preoccupied by the fact we have accessed four unrelated values to move only one. And this in an asymmetrical way, values after the fifth element being left untouched.

2.3.1 Indexed streams

The answer to this problem comes from the canonical injection of tuples into records, as it can be found functional languages like Standard ML or LIFE. That is

(x_{1}, …, x_{n}) ≡ {1⇒x_{1}, …, n⇒x_{n}}

We will just consider tuples as a particular case of streams (the name we give to these numerically indexed records). We use streams to access directly the arguments we are interested in. For instance we write the previous transformation

λ{5⇒x}.{1⇒x}.↓

We extract the 5^{th} element from the input, and put it in first position.

By symmetry we can use such incomplete streams in applications as well as abstractions. The transformation {5 ⇒ a}.↓ inserts a before the fifth argument of its input, pushing up all its followers by one.

(b_{1}, b_{2}, b_{3}, b_{4}, b_{5}, b_{6}).{5⇒a}.↓ →_{β} (b_{1}, b_{2}, b_{3}, b_{4}, a, b_{5}, b_{6}).↓

The stream we apply our transformation to can be incomplete too, like in the following case.

{2⇒a, 5⇒b, 7⇒c}.{5⇒d}.↓ →_{β} {2⇒a, 5⇒d, 6⇒b, 8⇒c}.↓

Generally, we must define a concatenation operation on streams, compatible with the partial isomorphism between streams and tuple. This is done by shifting indexes in the inserted stream according to those present in the original one. The algorithm doing that will be detailed in the next section. The important point is that we have a reciprocal operation, sub-stream extraction, which we can use to separate a stream into two parts, forming it back by concatenation.

{1⇒a, 2⇒b, 3⇒c, 5⇒d, 7⇒e}.λ{2⇒x, 3⇒y}.M
≡ {1⇒a, 3⇒d, 5⇒e}.{2⇒b, 3⇒c}.λ{2⇒x, 3⇒y}.M
→^{∗} {1⇒a, 3⇒d, 5⇒e}.[b/x, c/y]M

This operation can be applied to the abstraction part too:

{2⇒a, 4⇒b}.λ{2⇒x, 3⇒y}.M
≡ {3⇒b}.{2⇒a}.λ{2⇒x}.λ{2⇒y}.M
→_{β} {3⇒b}.λ{2⇒y}.[a/x]M
≡_{.λ} λ{2⇒y}.{2⇒b}.[a/x]M

In the second line we decompose both abstraction and application to permit β-reduction in the third one. The ≡_{λ} equivalence in the last line is there to switch unrelated abstractions and applications, and let the reduction progress smoothly. We will argue later its coherence with the rest of the system.

Thanks to these streams we can now write algorithms using the power of something quite close to a direct-access stack machine. It is slightly different since reading a position in the stream destroys this position, but writing resulting in a symmetrical insertion this is not a problem. Here is a transformation incrementing the fifth position in a stream.

(a, b, c, d, e) .λ{5⇒x}.{5⇒x + 1}.↓
≡  (a, b, c, d) .{5⇒e}.λ{5⇒x}.{5⇒x + 1}.↓
→_{β}  (a, b, c, d) .{5⇒e + 1}.↓
≡ (a, b, c, d, e + 1) .↓

2.3.2 Naming positions

The problem of such a system is that since the indexes in the stream may change with each transformation we apply to it, we have no uniform way to address a defined position in it. This increments the fifth position by the first (which is destroyed):

λ{1⇒x, 5⇒y}.{4⇒x + y}.↓

The position we addressed as 5^{th} before the transformation must become the 4^{th} after it, since we do not distinguish arguments (x) from mutable variables (y).

This possibility of mixing is good, since it means that we can see everything with a functional insight. However we would like to have a more uniform way to handle a position. Going on with our analogy between streams and records, we will accept to have named fields in our streams. So that we can write the previous incrementer as

λ{1⇒x, i⇒y}.{i⇒x + y}.↓

Since i is a named position its index is not modified by the extraction of the first one.

A problem may appear when we concatenate two streams containing the same named position. On records this operation has two definitions. Either we just refuse to do it (symmetrical concatenation), either we accept, take for this field the value in one operand, and just forget the value in the other (asymmetrical concatenation). Since concatenation is already asymmetrical on numerical indexes, there is no point in refusing to do such a thing. However we cannot erase a value since we would lose confluence: {i ⇒ b}.{i ⇒

a}.λ{i ⇒ x}.λ{i ⇒ y}.M →_{β}^{2} [a/x, b/y]M but {i ⇒ b}.λ{i ⇒ x}.λ{i ⇒ y}.M doesn’t. So

we just add a numerical index to our position name. That is, we view both numerical and name positions as their injections into their product, the set of labels. We have a default name ϵ such that the index n is in fact ϵn, and we add 1 to names so that p is p1. With that we define easily

{p⇒b}.{p⇒a}.M ≡ {p1⇒a, p2⇒b}.M

This works right with the above example, which becomes {i1 ⇒ a, i2 ⇒ b}.λ{i1 ⇒ x, i2 ⇒ y}.M.

Going on with our comparison with stacks, we have now as many stacks as we have names, each of them handled through indexed extraction and insertion.

We see here a new version of Euclid’s algorithm, using labels for both the function and the while functional.

while = λ{end⇒end, do⇒do}.
end; λ{ok ⇒ok}.
if ok then do; {end⇒end, do⇒do}.while else ↓
gcd = λ(x, y).{m⇒x, n⇒y}.↓;
{end⇒λ{m⇒m}.{ok ⇒m ≠ 0, m⇒m}.↓,
do⇒λ{m⇒m, n⇒n}.{m⇒n mod m, n⇒m}.↓}.while;
λ{m⇒m, n⇒n}.n

On such an example the addition of labels may look as pure verbosity, but what we obtain here is very close to what we would write as an imperative algorithm. We only have to add trivial abstractions of the form λ{m⇒m} in order to transform an assignment-like syntax into functions.

2.4 Stream behavior

The examples we presented above worked all right, but what happens with “incorrect” terms, that are not well-behaved?

We had already such terms in classical lambda-calculus. For instance, if we encode an if-then-else by a pair λs.(s t e), where s is expected to be an encoded boolean, and t and e the two cases, we expect in most cases t and e to be well-behaved, that is if t encodes a pair, then e should also encode a pair. Otherwise, we will have unexpected behavior trying to apply a projection on it.

This problem of behavior is even more pernicious with the transformation calculus. Again in an if-then-else we expect the two branches to have similar behavior. But even if the second one gives back a stream with more labels than the first, it may well not appear, as long as we only use transformations that only access labels present in the first stream. This is still an incoherence.

So, by well-behaved, we will mean here that for any acceptable input with same stream structure, a transformation should give back a stream with same labels. That is, its stream-behavior, the stream structure of the result with respect to the stream structure of the input, should not be dependent on encoded values in the input.

For instance,

λb.if b then {l ⇒M}.↓ else ↓

is not well behaved since it returns either a stream with label l or an empty stream, depending on the value of b.

This is difficult to give a precise definition of well-behaved terms in an untyped framework, since it depends on what encodings we use. In a typed framework that amounts to subject reduction, and we give in Section 6 a simply typed transformation calculus that satisfies it (i.e. all typable terms are well-behaved).

2.5 Scope-free variables

Up to this point we have progressively enriched the lambda-calculus with new constructs. The transformation calculus is approximately the result of this process. We have insisted on how this calculus was a potential basis for an integration of imperative and functional styles in the design of algorithms. Here we introduce a general method to directly map the imperative notion of variable into the transformation calculus.

In fact, what we mean by scope-free variable is slightly stronger than a mutable variable. We call it scope-free, since it is not syntactically scoped like in structured programming, neither is it global. We can say that it is local to a sequence of transformations, composed together.

A scope free variable is essentially a name v whose use in labels is exclusively reserved in the concerned sequence of transformations. This sequence is delimited by the creation of the variable with value a, encoded {v ⇒ a}.↓, and its destruction by an abstraction, λ{v ⇒ x}.↓. Between these, all transformations using or modifying this variable should once take it (through abstraction) and then put it back (by application), identical or modified. Typically a modification can be written λ{v ⇒ x}.{v ⇒ M}.↓. That is, the sequence has form:

{v ⇒a}.↓; …; λ{v ⇒x}.{v ⇒M}.↓; …; λ{v ⇒x}.M

Since some transformations may be functionals, the recognition of such a structure is not immediate, but for instance m and n in the last version of Euclid’s algorithm are scope-free variables.

The most interesting property of scope-free variables is that, like scoped variables, they have no effect outside of the sequence they are used in. That is, we can use the same label v outside of the sequence our scope-free variable is local to, without interference. A scope-free variable may even be used in a subsequence of another scope-free variable using the same label:

\{v ⇒a\}.↓; …; \underline{\{v ⇒b\}.↓; …; λ\{v ⇒x\}.↓}; …; λ\{v ⇒x\}.↓

In the underlined subsequence the external scope-free variable is identifiable by the label v + 1 but comes back to v after.

Still, we must be careful that scope-free variables are not variables in the meaning of lambda-calculus: they appear on a completely different level, that of labels. Nor are they pervasive like would be references. We do not add side-effects to functions, but just provide some implicit way to manipulate a “stream” of arguments. That means that a function that is not called directly on this stream (through composition) will not access the scopefree variables it contains, and as such cannot have any imperative behavior with respect to this stream. This is this limitation which permits us to assimilate scope-free variables with arguments, and still be a conservative extension of lambda-calculus.

We give two examples of the use of scope-free variables. The first one is a simple encoding of an imperative programming language à la Algol. The second one shows how scope-free variable are stronger than scoped ones.

Here is the program and its translation.

          begin
            var x=5, y=10;
            x := x+y;
            begin
              var x=3;
              y := x+y
            end
            x := x-y;
            return(x)
          end

{x⇒5, y ⇒10}.↓; λ{x⇒x, y ⇒y}.{x⇒x + y, y ⇒y}.↓; {x⇒3}.↓; λ{x⇒x, y ⇒y}.{x⇒x, y ⇒x + y}.↓; λ{x⇒x}.↓; λ{x⇒x, y ⇒y}.{x⇒x − y, y ⇒y}.↓; λ{x⇒x, y ⇒y}.x

We expect this program to evaluate to 5 + 10 − (3 + 10) = 2.

{x⇒5, y ⇒10}.↓; …

{x⇒5, y ⇒10} .λ · · · .{x⇒x + y, y ⇒y}.↓; …
{x⇒15, y ⇒10} .{x⇒3}.↓; …
{x1⇒3, x2⇒15, y ⇒10} .λ · · · .{x⇒x, y ⇒x + y}.↓; …
{x1⇒3, x2⇒15, y ⇒13} .λ{x⇒x} ↓; …
{x⇒15, y ⇒13} .λ · · · .{x⇒x − y, y ⇒y}.↓; …
{x⇒2, y ⇒13} .λ{x⇒x, y ⇒y}.x

2

Note here that since we encode dynamic binding^{3} for scope-free variables, we would get the same result even if the central part was a call to the same piece of code defined elsewere: with scope-free variable, even Basic’s subprograms, which have no variable passing, would be a nice feature, since we can create a scope-free variable before the call to pass a parameter, and destroy it after.

The translation we propose here is a general one. By defining variables at the beginning of blocks and destroying them by abstractions at the end, we can translate any Algol-like program (with dynamic binding for mutable variables), even containing procedures and functions.

The above example still respects a scoping discipline: variables are created and destroyed in opposite order. To show the specificity of scope-free variables, we must disobey it.

Not respecting a scoping discipline seems quite dangerous for variables, and of little use in purely computing programs. However, if we think of IO’s, then the situation is different. Consider a program with structure

\overline{A;}\underline{\overline{B}; C}

in which we want the console to be redirected in part A; B, and the screen to be changed in B; C. We suppose that we have mutable variables con and scr to indicate respectively which console and which screen should be used. Moreover we do not know which were the console and screen before entering A.

A dirty method is to use temporary variables c and s, to store the old values:

                       c:=con; con:=newc; A; s:=scr;
                       scr:=news; B; con:=c; C; scr:=s

3Dynamic binding is generally considered as bad, because destroying referential transparency. However, if we distinguish between static (defined only once, like λ-variables) and mutable variables, the notion of referential transparency for the last is not so clear. Since they are already not referentially transparent w.r.t. their values, the simpler modeling offered by dynamic binding can be seen as an advantage.

The problem is that these temporary variables may be modified by error in A, B or C. So a better solution is to use static variables, only set once:

                       let c = !con in
                         con:=newc; A ;
                         let s = !scr in
                           scr:=newc; B ; con:=c; C ; scr:=s
                       end end

However, because of the scope discipline, c is still defined in C, whereas we do not need it anymore. We can see here an inconsistency between the scope of c, which is A; B; C, and its expected area of use, A; B.

We think that the scope-free variable way to do it is cleaner:

\begin{matrix}\{con⇒newc\}.↓; A; \{scr ⇒news\}.↓; B; \\ λ\{con⇒c\}.↓; C; λ\{scr ⇒s\}.↓ \end{matrix}

We didn’t define any new variable, but did just temporarily hide the original value by the redirected one. And there are no “dangling” definitions (variables still defined out of their area of use).

3 Stream monoid

The transformation calculus is essentially defined in terms of operations on streams. We give one definition for their set here, but transformation calculus can be defined on any “reversible” monoid: the monoid operation, or concatenation, gives us uncurrying, while its inverse, or extraction, gives us currying.

We will note the concatenation on streams by a simple dot “·”, and the monoid of streams is (S, ·).

Preliminaries • L_{s} is an ordered set of names, N = IN \ {0}.

• L = L_{s} × N is the set of labels, lexicographically ordered.

• l will always represent an element of L; p, q elements of L_{s}; m, n elements of N.

Definition 1 (stream) The set S(L, A) of streams on a domain A is the set of finite partial functions from L to A.

S(L, A) = {s ∈ A^{L} | |s| ∈ IN}

Notations • D_{s} is the definition domain of a stream s.

• {} is the function defined nowhere (D_{{}} = ∅).

• We note labels pn, and defining pairs {pn⇒a} with a ∈ A.

• The following equivalences of notation are admitted for labels and streams:

- n denotes ϵn, p denotes p1

- if l = pn then l + m = p(n + m)

- (a_{1}, …, a_{n}) = {1⇒a_{1}, …, n⇒a_{n}}

Example 1 (stream monoid) The simplest instanciation of S is the monoid of tuples: L_{s} = {ϵ} (a singleton) and S = ⋃_{n≥0} A[[1, n]]. Then concatenation is

(a_{1}, …, a_{m}) · (b_{1}, …, b_{n}) = (a_{1}, …, a_{m}, b_{1}, …, b_{n}),

and is reversible.

This example gives our first calculus, omiting selective currying. In the general case, we need a more complex definition, permitting label operations. It is based on a notion of n^{th} free position in a stream, which, while intuitively clear —just imagine that undefined labels point to free positions—, looks a little complex once formalized.

Definition 2 (free position) 1. The n^{th} position on p in a stream r is said to be occupied if pn ∈ D_{r}. It is free otherwise, and F_{r} = L \ D_{r} is the set of these free positions.

2. The n^{th} free position for p in r is the n^{th} element of {i | pi ∈ F_{r}}.

Namely ϕ_{r,p}(n) = min{m | |{pi ∈ F_{r} | i ≤ m} = n}.

3. The relative index of pn in r is the number of free positions preceding n on p plus one. Namely ψ_{r,p}(n) = |{pi ∈ F_{r} | i < n}| + 1.

One notices immediately the inversion relation between free positions, used for concatenation, and relative indexes, used for extraction.

ϕ_{r,p}(n) = min{m | |{pi ∈ F_{r} | i ≤ n}| = n}
= max{m | |{pi ∈ F_{r} | i < n}| = n − 1}
= max ψ_{r,p}^{−1}(n)

We extend both ϕ and ψ to streams by ϕ_{r}({p_{i}n_{i} ⇒a_{i}}_{i=1}^{k}) = {p_{i}ϕ_{r,p_{i}}(n_{i})⇒a_{i}}_{i=1}^{k} (resp. for ψ).

Example 2 (free positions) In {p1 ⇒ a, p3 ⇒ b, p5 ⇒ c, q2 ⇒ d}, relative indexes are respectively 2 for p4 and q3, and 3 for p5 and q4. Free positions are {2, 4, 6, 7, …} on p, and {1, 3, 4, …} on q. As a result, the second free position on p is 4, and on q this is 3.

Proposition 1 (reversibility) ϕ_{r} is a bijection from S to {s ∈ S | D_{r} ∩ D_{s} = ∅}. ψ_{r} ∘ ϕ_{r} = id_{S}.

Definition 3 (concatenation and extraction)

1. Stream concatenation is defined as r · s = r ⊎ ϕ_{r}(s) where “⊎” denotes union of (set represented) functions on disjoint domains.

2. Sub-stream extraction is defined as r⊎s = r·ψ_{r}(s), where r is the extracted sub-stream and ψ_{r}(s) is the rest after extraction.

Proposition 2 (monoid) Concatenation as in Definition 3 is an associative application S × S → S, accepting {} as neutral element.

l ::= pn  p ∈ L_{s}, n ∈ N
M ::= x  variable
| ↓  transformation constructor
| λ{l ⇒x, …}.M abstraction
| {l ⇒M, …}.M application
| M; M  composition

Figure 1: Syntax of the transformation calculus

S.R.M ≡_{.} (R · S).M
λR.λS.M ≡_{λ} λ(S · R).M  V (R) ∩̸ V (S)
R.λS.M ≡_{.λ} λψ_{R}(S).ψ_{S}(R).M F V (R) ∩̸ V (S), D_{R} ∩̸ D_{S}
(R.M_{1}); M_{2} ≡_{.;} R.(M_{1}; M_{2})
(λR.M_{1}); M_{2} ≡_{λ;} λR.(M_{1}; M_{2})  V (R) ∩̸ F V (M_{2})
(M_{1}; M_{2}); M_{3} ≡_{;} M_{1}; (M_{2}; M_{3})

Figure 2: Structural equivalences

The intuition behind these definitions is that when we do r ·s we insert elements of s at free positions in r: for each name p we insert the element whose index is n in s at the n^{th} free position for p in r. ϕ_{r} is the function which does this shifting. Reciprocally, extraction uses ψ_{r} to shift back positions in the rest to their relative indexes w.r.t r.

Example 3 (stream concatenation)

{2⇒a} · (b, c) · {p⇒d} · {q ⇒e} · {p⇒f}
= (b, a, c) · {p⇒d} · {p⇒f} · {q ⇒e}
= {ϵ1⇒b, ϵ2⇒a, ϵ3⇒c, p1⇒d, p2⇒f, q1⇒e}.
{p1⇒a, p3⇒b, r1⇒c} · {p1⇒d, q_{2} ⇒e}
= {p1⇒a, p3⇒b} · {p1⇒d} · {q2⇒e} · {r1⇒c}
= {p1⇒a, p2⇒d, p3⇒b, q2⇒e, r1⇒c}

4 Syntax of transformation calculus

In this section we define the untyped transformation calculus, and the selective λ-calculus as a subsystem of it.

The definition is done in two steps. 1) We give a syntactic definition of terms in the transformation calculus, and add a structural equivalence on these terms^{4}. 2) Then we define reduction rules for these equivalence classes.

Notations In the following definitions we will use the abbreviations A ∩̸ B for A ∩ B = ∅, F V (M) for the free variables of M, and V (R) for the values contained in the stream R.

4We could use all equivalences as directed reduction rules. This would result in a slightly more complicated system (cf. [AKG93] for selective λ-calculus)

Definition 4 Terms of the transformation calculus, or Λ_{T}, are those generated by M in the grammar of figure 1, where variables should be distinct in abstractions, and labels distinct in streams. Composition has lower priority than dots.

They are considered modulo ≡, the minimal equivalence relation defined by the closure of the equalities in figure 2.

The selective λ-calculus Λ_{S} is the subset formed by those terms which do not contain ; nor ↓.

Equalities ≡_{.} and ≡_{λ} are derived from the monoidal structure. ≡_{.;}, ≡_{λ;} and ≡_{;} are intuitive.

Equality ≡_{.λ} is the “symmetrical” of β-reduction. It comes from the need to close the equality

(R′ ⊎ S′).λ(R ⊎ S).N ≡_{.} ψ_{R}(S′).R′.λS.λψ_{S}(R).N,

with D_{R′} = D_{R}, D_{S′} = D_{S} and V (S) ∩̸ V (R). If we take M = λϕ_{S}^{−1}(R).N, and apply R′.λS.M to ψ_{R}(S′), then ≡_{.λ} preserves confluence: it gives

(R′ ⊎ S′).λ(R ⊎ S).N ≡ ψ_{R}(S′).λψ_{R}(S).ψ_{S}(R′).λψ_{S}(R).N.

Substitutions are done in the same way as for lambda-calculus, composition not interacting with variable binding. Terms will always be considered modulo α-conversion. That is λ{l ⇒x}.M ≡ λ{l ⇒y}.[y/x]M when y ∉ F V (M).

Definition 5 “→” is defined on transformation calculus terms by β-reduction and ↓- elimination^{5}.

\begin{aligned}\{l ⇒N\}.λ\{l ⇒x\}.M & →_{β} & [N/x].M \\ ↓; M & →_{↓} & M \end{aligned}

→^{∗} is the reflexive and transitive closure of →.

Selective λ-terms and β-reduction define the selective λ-calculus.

Theorem 1 Selective λ-calculus is confluent.

Theorem 2 Transformation calculus is confluent.

The proofs are given in appendix A. Confluence of transformation calculus is obtained from selective λ-calculus through a translation into it.

Proposition 3 Normal terms are generated by N in the following grammar, where streams and anti-streams may be empty.

\begin{aligned}H & ::= & x | ↓ \\ F & ::= & \{l ⇒N, …\}.x | F; λ\{l ⇒x, …\}.F \\ N & ::= & λ\{l ⇒x, …\}.\{l ⇒N, …\}.H | λ\{l ⇒x, …\}.(F; N) \end{aligned}

This formalizes our intuition that, in a normal form, a composition only subsists when its left side cannot be reduced to a transformation.

5We chose to make ↓-elimination a reduction rule rather than a structural equality because it reduces the size of terms, while the structural equalities of Definition 4 do not change it.

5 Scope-free variable encoding

We cannot expect to give a precise definition of scope-free variable in the transformation calculus, where it is only encoded. It appears as an intuitive notion of a variable whose locality is not syntactical but operational. We will define it outside of the calculus.

For this we use a framework in which a program is a sequence of operations. Operations can themselves contain programs, but these are independent, and may not have side-effects on the external sequence.

Definition 6 A scope-free variable is some way to create, modify and destroy a value such that:

1. these operations may appear in different syntactic entities, which may be used independently.

2. a closed use of this variable is obtained when a creator, some modifiers, and a destructor result in a modification sequence.

3. its closed use in a modification sequence has no side-effect outside it.

A consequence of this definition is the hiding property we insisted on. The same variable may have several independent closed uses, with modification sequences included in one another, and there is no problem as long as we do not try to modify the value from one use inside another’s modification sequence.

As we introduced in Section 2, elementary creators, modifiers and destructors in transformation calculus are respectively {v ⇒M}.↓, λ{v ⇒x}.{v ⇒M}.↓ and λ{v ⇒x}.↓. But we can think of more complex ones, acting simultaneously on multiple variables, taking arguments, or returning results. For instance, in

λ{1⇒x}.{a⇒2, b⇒x}.↓;
λ{a⇒x, b⇒y}.{a⇒x × y, b⇒x − y}.↓;
λ{a⇒x, b⇒y}.(x + y)

a and b are two scope-free variables, but their creator, modifier and destructor are joint.

To ensure that we have a correct scope-free variable encoding here, we must verify the third point of the definition, which says that it has no effect outside the sequence it is used in.

Proposition 4 The scope-free variable encoding into the transformation calculus ensures locality to the modification sequence.

As we have seen, thanks to this property, scope-free variables are not only more flexible than classical scoped variables, but can replace them in most of their uses. Particularly, in functional language they can replace “disciplined” references (which do not go out of their scope), without the need of a specific evaluation strategy. Their only limitation is that —in the transformation calculus— one cannot export them like references, since they are linked to an explicit name. However, this is a limitation of the label system we use, and not of scope-free variable in themselves: one can add a syntactical scope to scope-free variables [Garar]. The real point about them is that the use of a (now scoped) scope-free variable is not restricted by that syntactical scope^{6} (which is only a problem of naming), like with the stack discipline, but by its life area, or modification sequence (its real operational scope).

6This is true with references too, but their operational scope is only defined by garbage collection.

6 Simply typed transformation calculus

To obtain a simply typed form of transformation calculus, we annotate variables with some type in abstractions, just the same way it is done in lambda calculus. But first we must define what are these types.

The two most important novelties are that, first, stream types are introduced, and second, that function type are not from any type to any other, but only from stream types to stream or base types. This last particularity “flattens” types, but still contains as a subset all simple types of lambda-calculus.

Definition 7 Simple types in the transformation calculus are generated by t in the following grammar.

u ::= u_{1} | …  base types
r ::= {l ⇒t, …} stream types
w ::= u | r  return types
t ::= r → w  types

The same label may not appear more than once in the same stream type; stream types are equal up to different orders, and ({} → τ) = τ, for short.

These last restrictions make a stream type a stream of types as defined in Section 3. This means that we can use stream composition on these types, as we will do for typing rules.

Definition 8 A term in the simply typed transformation calculus is constructed according to the following syntax.

M ::= x | ↓ | λ{l ⇒x:t, …}.M | {l ⇒M, …}.M | M; M

with the same constraints on labels and variables as before.

Finally the relation between terms and types is given in the following definition.

Definition 9 A type judgement, written Γ ⊢ M : τ, expresses that the term M has type τ in the context Γ. Induction rules for type judgements are given in figure 3.

Rules (I,II,III) are the traditional ones for typed lambda calculus, simply extended to streams. We can go back to it by limiting labels in streams to sequences of integers starting from 1 (that is, in the above rules, having only l = ϵ1).

Rule (IV) types the constant ↓. However it will most often need the cooperation of rule (VI), transformation subtyping, which expresses that any transformation may be applied to labels it is not concerned with: they will simply be rejected to the result. For instance, it gives to ↓ any symmetrical type (r → r). Rule (V) types composition: M is applied to the result stream of N, and re-abstracted by its abstraction part. Here again, we need the collaboration of rule (VI) to extend the types of either M or N.

Proposition 5 (subject reduction) If Γ ⊢ M : τ and M → N then Γ ⊢ N : τ.

Proposition 6 (strong normalization) If Γ ⊢ M : τ then there is no infinite reduction sequence starting from M.

This last property is interesting, since it is general belief that introducing mutables suppresses strong normalization: we keep it here, because all values used by a term appear in its type.

Γ[x ↦ τ] ⊢ x : τ  (I)
\frac{Γ[x ↦ θ] ⊢ M : r → w}{Γ ⊢ λ\{l ⇒x:θ\}.M : (\{l ⇒θ\} · r) → w}  (II)
\frac{Γ ⊢ M : (\{l ⇒θ\} · r) → w Γ ⊢ N : θ}{Γ ⊢ \{l ⇒N\}.M : r → w}  (III)
Γ ⊢ ↓ : {}  (IV)
\frac{Γ ⊢ M : r_{1} → r_{2} Γ ⊢ N : r_{2} → w}{Γ ⊢ M; N : r_{1} → w}  (V)
\frac{Γ ⊢ M : r_{1} → r_{2}}{Γ ⊢ M : (r_{1} · r) → (r_{2} · r)}  (VI)

Figure 3: Typing rules for simply typed transformation calculus

7 Denotational semantics

In this section we give a model of the transformation calculus. However, to avoid technical problems specific to untyped models, and to get simple semantics, we base ourselves on the simply typed version of the calculus.

Definition 10 A model of the transformation calculus is a pair (A, [[ ]] ) with A a set of values, and (M, ρ) ↦ [[M]]_{ρ} : Λ_{T} × A^{V} → A a translation from a simply typed term M and an environment ρ (F V (M) ⊂ D_{ρ}) into our model satisfying the axioms

\begin{aligned}M ≡ N & ⇒ & [[M]]_{ρ} = [[N]]_{ρ}, \\ M → N & ⇒ & [[M]]_{ρ} = [[N]]_{ρ}, \\ ρ(x) = a & ⇒ & [[x]]_{ρ} = a. \end{aligned}

We define our model A = ⋃_{τ∈T} A^{τ} by closure of the following procedure.

1. For u ∈ T_{0} (base type), A^{u} is given. A_{0} = ⋃_{u∈T_{0}} A^{u}.

2. Streams values of level n are in S_{n} = ⋃_{r∈S(T_{n})} A^{r}, where

A^{{l_{i}⇒τ_{i}}_{i=1}^{m}} = ⋃_{a_{1}∈A^{τ_{1}}} … ⋃_{a_{m}∈A^{τm}}{l_{1} ⇒a_{1}, …, l_{m} ⇒a_{m}}

3. Types of level n + 1 are defined by

T_{n+1} = T_{n} ∪ {r → w | r ∈ S(T_{n}), w ∈ S(T_{n}) ∪ T_{0}}

4. Values of level n + 1 are defined by A_{n+1} = ⋃_{τ∈T_{n+1}} A^{τ} where

A^{r→w} = A^{r} → A^{w}

5. A = lim_{n→∞} A_{n} A is well-defined, since for any τ there exists n such that τ ∈ T_{n} and then A^{τ} ⊂ A_{n}. Note that, like we did with types, we are identifying the streams of A^{r} with the functions

of A^{{}→r} = A^{{}} → A^{r}.

Once we have defined the values of the model, we must define operations on them. Out of concatenation, already defined on streams, we have two: extension and composition.

Extension is the operation by which a value in A^{r_{1}→r_{2}} gets canonically extended into a value of A^{(r_{1}·r)→(r_{2}·r)}. If f is in A^{r_{1}→r_{2}} then f ∗ r, the r-extension of f is defined as:

\begin{matrix}f ∗ r : A^{r_{1}·r} & → & A^{r_{2}·r} \\ \{l ⇒x_{l}\}_{l∈D_{r_{1}·r}} & ↦ & (f\{l ⇒x_{l}\}_{l∈D_{r_{1}}}) · (\{l ⇒x_{ϕ_{r_{1}}(l)}\}_{l∈D_{r}}) \end{matrix}

Composition is just the mathematical one; if f is in A^{r_{1}→r_{2}} and g in A^{(r_{2}·r)→w}, then f; g is defined as:

\begin{aligned}f; g : & A^{r_{1}} & → & A^{w} \\ & s & ↦ & g(f(s)) \end{aligned}

However the above definitions will not work as model: with the subtyping introduced on transformations in the calculus, we expect that the same value may actually be contained in several A^{τ} sets. That is why we will consider the above definition modulo extension.

More precisely, we introduce the following equivalence f =_{∗} f ∗ r, closed by symmetry and transitivity (it is already reflexive). Since extension only applies on members of A^{r_{1}→r_{2}}, equivalent terms are transformations. Moreover we remark that, modulo this equivalence, A^{s_{1}→s_{2}} now includes all A^{r_{1}→r_{2}} such that for some r, r_{1} · r = s_{1} and r_{2} · r = s_{2}.

We define A_{∗} as A_{/=_{∗}}, and A_{∗}^{τ} as the sets of all classes containing an element of A^{τ}. We show easily that composition is coherent with this equivalence: if f ∈ A^{r_{1}→r_{2}} and

g ∈ A^{r_{2}→r_{3}} (for extension to be possible, both f and g must be transformations), then f ∗ r ∈ A^{(r_{1}·r)→(r_{2}·r)}, g ∗ r ∈ A^{(r_{2}·r)→(r_{3}·r)}, and

(f ∗ r; g ∗ r){l ⇒x_{l}}_{l∈D_{r_{1}·r}}
= (g ∗ r)((f{l ⇒x_{l}}_{l∈D_{r_{1}}}) · ({l ⇒x_{ϕ_{r_{1}}(l)}}_{l∈D_{r}}))
= (g(f{l ⇒x_{l}}_{l∈D_{r_{1}}})) · ({l ⇒x_{ϕ_{r_{1}}(l)}}_{l∈D_{r}}))
= ((f; g) ∗ r){l ⇒x_{l}}_{l∈D_{r_{1}·r}}

Finally we define the translation (M, ρ) ↦ [[M]]_{ρ} : Λ_{T} × A_{∗}^{V} → A_{∗}, from a simply typed term M and an environment ρ (F V (M) ⊂ D_{ρ}) into our model^{7} in figure 4.

Proposition 7 (A_{∗}, [[ ]] ) is a model of the simply typed transformation calculus.

8 Related works

Since transformation calculus only happens to be able to represent state, its origin is not to be found in the field of semantics of stateful languages. It is rather based on two independent threads of work. The first one is the Categorical Combinatory Logic [Cur93], in which composition and currying play a central role. The direction seems opposed: one encodes lambda-calculus into CCL (or its abstract machine version, the CAM [CCM87]), while

7Since terms are statically typed, we could construct a model based on tuples and type information, which would avoid the extra structure for streams, and compile away labels. Only extension would have to be modified. We based ourselves on streams here for the sake of simplicity of the equivalence relation.

[[x]]_{ρ}  = ρ(x)
[[↓]]_{ρ}  = {}
[[λ{l_{0} ⇒x:τ}.M]]_{ρ} = (when [[M]]_{ρ[a^{τ} /x]} ∈ A^{r→w})

\begin{matrix}A^{\{l_{0}⇒τ\}·r} & → & w \\ \{l ⇒x_{l}\}_{l∈\{l_{0}\}∪D_{r}} & ↦ & [[M]]_{ρ[x_{l_{0}}/x]}\{l ⇒x_{l}\}_{l∈D_{r}} \end{matrix}

[[{l ⇒N}.M]]_{ρ}  = {l ⇒[[N]]_{ρ}}; [[M]]_{ρ}
[[M; N]]_{ρ}  = [[M]]_{ρ}; [[N]]_{ρ}

Figure 4: Semantic function of the simply typed transformation calculus

transformation calculus extends lambda-calculus. But the intuition that algorithmicity can be found in the structures of the lambda-calculus itself is the same.

The second one is process calculi. Their use of names for communication is similar to the principle of the transformation calculus. In [Bou89], Boudol proposes the γ-calculus. The base is lambda-calculus, but applications express emissions of messages and abstractions their reception, while multiple terms can be evaluated simultaneously. Milner’s π-calculus [Mil92] proceeds alike, and by labeling with names applications and abstractions, it allows the use of multiple channels. The fundamental difference with our calculus is that nondeterminism of the receptor of a message make these calculi divergent, while our terms are syntactically sequenced in order to keep determinism.

A third might be Lamping’s Unified Parameterization System [Lam88], which tries like us to encode state modifications into the parameter passing system. However his systems departs essentially from lambda-calculus, so that this last has to be encoded; and destructive overriding makes impossible to limit the effect of modifying variables like we do.

After these somewhat different directions, our claims makes necessary to look at the larger literature concerning modeling of mutables in Algol, Lisp, and modern functional programming languages. Algol is the closest to our system, since scope-free variables cannot be used out of their life area, like with Algol’s stack discipline, where a variable cannot be exported out of its scope.

This subject starts with Landin’s encoding of Algol 60 into the lambda calculus [Lan65]. Or rather, nothing starts, since the problem remains unsolved: “The semantics of applicative expressions can be specified formally without the recourse to a machine. […] With imperative applicative expressions on the other hand it appears impossible to avoid specifying semantics in terms of a machine”.

Later, to encompass the stack discipline, marked store models were developped [Gor79, MS76] but they had two problems: a lack of abstraction, and the existence of some pathological cases, described in [MS88], where equivalences in Algol are not provable in the model.

A first answer to this was Oles and Reynolds category-theoretic models [Ole85, Rey81]. The essential idea is to define blocks as functions that can be applied to a range of states with various shapes, but do not change their shapes. However, inside the block, state is temporarily extended with local variables. Thus, they do not appear in its meaning. Our approach shares a lot with this view, since we syntactically “expand” and “shrink” our state when we create and delete a scope-free variable.

Another one is the Halpern-Meyer-Trakhtenbrot Store Model [HMT84, THM84], later refined by Meyer and Sieber [MS88], still based on stores, but using locally complete partial orders. It comes at last very close to full-abstraction, but fails in a 7^{th} example. Aknowledging the depth of the problem, Mason and Talcott even proposed an Operational Framework [MT92b, MT92a] to solve it out of denotational semantics.

Apart from this problem, there is interesting remark about the Orthogonality of assignments and procedures in Algol [WF93]. A theorem is enunciated, proving that normalization of an Algol program can be done in two phase, one using β and copy rules, and the other a simple stack machine. We do not obtain such a result, since we do not explicitly distinguish between imperative and functional features in the transformation calculus, but we can see the same kind of behaviour, first reducing higher order functions and eliminating composition, and then reducing β-redexes of ground types.

If we go out of the Algol tradition, we can forget about the stack discipline. As a result, most systems give a formalization of references. So does the λ_{v}-S-calculus [FF87, FF89] for Scheme, and a call-by-value reduction strategy. With effect inference [GL86, LG88, TJ92], restrictions on the reduction strategy can be reduced, and, for instance, parallelism can be introduced.

Still, we feel more concerned by systems going the other way, starting without a specific reduction strategy. There are a number of them, which enforce single-threadedness of variables by various typing disciplines [GH90, PW93, SRI91, Wad90a, Wad90b]. We can see an intuitive relation between the way scope-free variables are used and linear types, but still we are not relying to typing for single-threadedness.

We actually do it in a syntactical way. In that we are very close to λ_{var} [ORH93, CO94]. In fact, even the structures of the calculus have similarities: like us, they use the linear structure of spines to ensure single-threadedness. They have rules to propagate the values of mutable variables along the spine of a term, like does our structural equivalences for labeled arguments, and their return-elimination rule ((return N) ▷ λx.M → (λx.M)N, cf. [ORH93]) can be seen as a variant of ↓-elimination (↓; M → M) including value-passing. The essential difference is that, since we use the same mechanism for scope-free variables and value-passing, we obtain a more unified calculus. In particular, the fact they are encoding references means that they must do some kind of garbage collection (their pure construct) to convert a value obtained using mutable variables into a purely functional one. In the transformation calculus, since we explicitely delete variables, we do not need such an “impure” purifier.

9 Conclusion

We proposed the transformation calculus as an extension of currying in the lambda-calculus permitting both functional and imperative encoding of algorithms.

We think this gives interesting answers to the two sides of the relation function/algorithm: as a demonstration of the relation between lambda-calculus and algorithms, and as a basis for functional languages handling states and sequentiality problems.

Still there are many topics left to explore. Typing is one of them. If we are to write program in this calculus, it is even unavoidable, since we must be able to verify that scopefree variables are correctly used. We presented here a simply typed system. We propose in [Gar95] a polymorphic version of it, extending that for selective λ-calculus [GAK94]. This could be completed by the introduction of linear types [Wad90b]: in the transformation calculus, variables are single threaded (operations on them are sequenced), but there is no restriction to their duplication. This is particularly a problem with IO: we can semantically create fictious worlds, but there is no way to implement them. Moreover, using linear types within the transformations calculus relieves the programmer of most of the grudge of the linear style, since sending back an argument is easy.

Compilation, which is easy with stores, is complex here. The final goal would be to eliminate label information, but the possibility to compose a term with a variable makes impossible to reach it in the general case. As we remarked about the model, there is no problem if we use non-polymorphic typing, but the polymorphic case is still open.

One strength of the transformation calculus is its system of labels. We may be interested in extending it. For instance, the possibility to generate new label names would give unique identifiers for scope-free variable, and avoid the hiding of a label in those sub-sequences which create new variables on this label. A more structured label space could even enable the use of object-based techniques, and solve the restrictions of dynamic binding.

Last, the similarities between this calculus and process calculi suggest that it might be used to express some forms of parallelism. If one looks at the way data flows in our terms, lots of reminiscences of the dataflow model may be seen. A topic like compilation of the calculus into this model looks interesting.

A Applicative translation and confluence

The idea of applicative continuation semantics was developed in [JD88] for a framework of stores and partial continuations. A partial continuation is a function from a state to a new state, but we can translate it into a function prefixing a continuation, that is a function from a continuation to a new continuation doing intended operations before calling the old continuation. In fact transformations look very much like partial continuations on streams, and this idea provides us with a translation from transformation calculus to selective λcalculus.

Definition 11 T r is the applicative translation from Λ_{T} (L_{s}) (without the associativity of composition (M_{1}; M_{2}); M_{3} ≡ M_{1}; (M_{2}; M_{3})) to Λ_{S}(L_{s} ∪ {cont}).

\begin{aligned}T r(↓) & = & λ\{cont⇒x\}.x \\ T r(M; N) & = & \{cont⇒T r(N)\}.M \\ T r(x) & = & x \\ T r(λR.M) & = & λR.T r(M) \\ T r(R.M) & = & T r(R).T r(M) \end{aligned}

The well-definedness of this translation is proved in Lemma 1.

The image of Λ_{T} is T r(Λ_{T}) = Λ_{S}^{∗}.

“cont” in the above definition stands for continuation. We translate composition into an application of its right-hand side to its left-hand side, seen as a continuation. Since cont is a new name, the continuation is received by the λ{cont ⇒ x}.x head of the right-hand side, and operational semantics of the calculus are preserved.

We will use this translation to prove the confluence of transformation calculus, based on that of selective λ-calculus.

Theorem 1 Selective λ-calculus is confluent.

∀M, P, Q (M →^{∗} P ∧ M →^{∗} Q) ⇒ (∃T P →^{∗} T ∧ Q →^{∗} T)

PROOF As one may expect, the proof is complex, and can be found for a variant of this calculus in [AKG93]. We have to modify two points. First, in its original definition selective λ-calculus use sum labels (L = N ∪ L_{s}) whereas we use a product system here (L = L_{s} × N). Names and indexes being independent, the modification of the proof is immediate. The modified proof appears in [AKGar]. Next, structural equivalences were defined in terms of reordering rules included in the calculus. Once proved the confluence of the calculus including them, we can transform these rules into equivalences and keep confluence. □

Lemma 1 T r is coherent w.r.t. ≡ (without associativity of composition), and reduction paths coincide. T r is a bijection from Λ_{T} to Λ_{S}^{∗}.

PROOF For coherence, we just verify that all equivalences in Λ_{T} are mapped to equivalences in Λ_{S}. For ≡_{.}, ≡_{λ} and ≡_{.λ} this is immediate, since the same equivalence applies in the translation. ≡_{.;} and ≡_{λ;} are mapped respectively to ≡_{.} and ≡_{.λ}:

T r((R.M_{1}); M_{2}) = {cont⇒T r(M_{2})}.T r(R).T r(M_{1})
≡ T r(R).{cont⇒T r(M_{2})}.T r(M_{1})
= T r(R.(M_{1}; M_{2}))
T r((λR.M_{1}); M_{2}) = {cont⇒T r(M_{2})}.λR.T r(M_{1})
≡ λR.{cont⇒T r(M_{2})}.T r(M_{1})
= T r(λR.(M_{1}; M_{2}))

For reduction steps, both →_{β} and →_{↓} are mapped to β-reduction:

T r(↓; M) = {cont⇒T r(M)}.λ{cont⇒x}.x

We define T r^{−1} by reversing each case in the definition of T_{r}. It is well-defined on raw terms of Λ_{S}^{∗}, and coherent by reversing cases above. This makes T r a bijection. □

The above lemma lets us translate reduction of the transformation calculus into selective λ-calculus ones. We need another lemma to get reductions starting in Λ_{S}^{∗} back into Λ_{T}.

Lemma 2 If M ∈ Λ_{S}^{∗} and M → N then N ∈ Λ_{S}^{∗}.

PROOF Terms of Λ_{S}^{∗} are characterized by the fact all abstractions using cont only appear in the form λ{cont⇒x}.x.

If the reduction step is not on cont1, then it do not create any abstraction on cont, nor modify λ{cont⇒x}.x’s.

If this is on cont1, then the λ{cont⇒x}.x concerned disappears.

In the two cases, the resulting term is still in Λ_{S}^{∗}. □

Theorem 2 Transformation calculus is confluent.

\begin{aligned}∀M, P, Q ∈ Λ_{T} & (M →^{∗} P ∧ M →^{∗} Q) \\ & ⇒ (∃T ∈ Λ_{T} P →^{∗} T ∧ Q →^{∗} T) \end{aligned}

PROOF By Lemma 1, we get T r(M) →^{∗} T r(P) and T r(M) →^{∗} T r(Q). By confluence of selective λ-calculus, we have T′ such that T r(P) →^{∗} T′ and T r(Q) →^{∗} T′. But by Lemma 2 these reductions are in Λ_{S}^{∗}, so that T = T r^{−1}(T′) is a solution. □

B Proofs of propositions

Proposition 1 (reversibility) ϕ_{r} is a bijection from S to {s ∈ S | D_{r} ∩ D_{s} = ∅}. ψ_{r} ∘ ϕ_{r} = id_{S}.

PROOF For each label pn, by definition of ϕ we have,

ψ_{r,p}(ϕ_{r,p}(n)) = ψ_{r,p}(max{i | ψ_{r,p}(i) = n}) = n.

Moreover, since ψ_{r,p} is an increasing surjection, we have,

(∃m) ϕ_{r,p}(m) = n
⇔ ψ_{r,p}(n) < ψ_{r,p}(n + 1), by definition of ϕ_{r,p}
⇔ |{pi ∈ F_{r} | i < n}| < |{pi ∈ F_{r} | i < n + 1}|
⇔ pn ∈ F_{r}
⇔ pn ∉ D_{r},

and we can conclude that ϕ_{r,p}(N) = {n ∈ N | pn ∉ D_{r}}, to obtain ϕ_{r}(S) = {s ∈ S | D_{r} ∩ D_{s} = ∅} by extension. □

Proposition 2 (monoid) Concatenation as in definition 2 is an associative application S × S → S, accepting {} as neutral element.

PROOF Associativity comes from the equality ϕ_{r} ∘ ϕ_{s} = ϕ_{r⊎ϕ_{r}(s)}. For this we reason on inverses, pn being a free position of r · s:

ψ_{s,p}(ψ_{r,p}(n))
= 1 + |{pi ∈ F_{s} | i < ψ_{r,p}(n)}|
= 1 + |{pi ∈ F_{s} | ϕ_{r,p}(i) < ϕ_{r,p}(ψ_{r,p}(n))}|,

since ϕ_{r,p} is strictly growing

= 1 + |{pi ∈ ϕ_{r}(F_{s}) | i < ϕ_{r,p}(ψ_{r,p}(n))}|,

since ϕ_{r} is an injection

= 1 + |{pi ∈ ϕ_{r}(F_{s}) | i < n}|,

since pn is a free position of r

= 1 + |{pi ∈ F_{r} ∩ F_{ϕ_{r}(s)} | i < n}|
= 1 + |{pi ∈ F_{r·s} | i < n}|
= ψ_{r·s,p}(n)

We then have r·(s·t) = r⊎ϕ_{r}(s⊎ϕ_{s}(t)) = r⊎ϕ_{r}(s)⊎ϕ_{r}(ϕ_{s}(t)) = r⊎ϕ_{r}(s)⊎ϕ_{r⊎ϕ_{r}(s)}(t) = (r · s) · t.

r · {} = r = {} · r is immediate (ϕ_{{}} = id). □

Proposition 4 The scope-free variable encoding into the transformation calculus ensures locality to the modification sequence.

PROOF If our variable is encoded on a label whose name is unique, there is no problem since it does not modify indexes of other arguments and variables, and its label appears only between its creation and destruction.

Otherwise, labels with the same name may appear with a different index in the sequence. But since each time they meet an abstraction or an application on our variable their indexes go alternately up and down, and the number of abstraction is equal to the number of applications, their index is the same on each side of the sequence. Moreover modifiers do not modify the value they support, since index changes avoid overloading of the same label. □

Proposition 5 (strong normalization) If Γ ⊢ M : τ in the simply typed transformation calculus, then there is no infinite reduction sequence starting from M.

PROOF We base ourselves on a translation into a simply typed λ-calculus with streams (we use matching rather than projections). This calculus, clearly equivalent to simply typed λ-calculus with pairing, is strongly normalizing.

We translate a proof Π of Γ ⊢ M : τ into a proof Π′ of Γ ⊢ M′ : τ in simply typed λcalculus with streams, where types are identical to those of the simply typed transformation calculus. This translation is very similar to that used for our simply typed model.

Rules get translated into (I does not change):

\frac{Γ[x ↦ θ] ⊢ M′ : r → w}{\begin{matrix}Γ ⊢ λ^{∗}\{k ⇒y_{k}\}_{k∈\{l\}·D_{r}}:\{l ⇒θ\} · r.(λx:θ. \\ M′ \{k ⇒y_{ϕ_{\{l\}}(k)}\}_{k∈D_{r}}) y_{l} : \{l ⇒θ\} · r → w \end{matrix}}  (II’)

\frac{Γ ⊢ M′ : \{l ⇒θ\} · r → w Γ ⊢ N′ : θ}{Γ ⊢ λ^{∗}y:r.M(\{l ⇒N\} · y) : r → w}  (III’)
Γ ⊢ λy:{}.y : {} → {}  (IV’)
\frac{Γ ⊢ M′ : r_{1} → r_{2} Γ ⊢ N : r_{2} → w}{Γ ⊢ λ^{∗}y:r_{1}.N′(M′ y) : r_{1} → w}  (V’)
\frac{Γ ⊢ M′ : r_{1} → r_{2}}{\begin{matrix}Γ ⊢ λ^{∗}\{l ⇒y_{l}\}_{l∈D_{r_{1}·r}}:r_{1} · r.((M′\{l ⇒y_{l}\}_{l∈D_{r_{1}}}) \\ ·\{l ⇒y_{ϕ_{r_{1}}(l)}\}_{l∈D_{r}}) : r_{1} · r → r_{2} · r \end{matrix}}  (VI’)

We sketch the rest of the proof.

We have marked some abstractions with * in this translation. This means that they have only a structural role. We will just ignore them, and write \overline{M′} for M′ where all ∗- marked redexes were reduced (thanks to strong normalization). All other redexes are kept, since ∗-marked abstractions are linear, and their reduction do not change inclusion relation between redexes. This gives us unicity of \overline{M′}. Moreover, in \overline{M′} all potential redexes of M (using ≡) appear. Particularly, associativity of transformation composition maps to associativity of λ-function composition.

One can verify that if we have Γ ⊢ M → N : τ in the simply typed transformation calculus, then, for M′ and N′ translations of M and N (the proof of Γ ⊢ N : τ chosen to be similar to that of Γ ⊢ M : τ), we have Γ ⊢ \overline{M′} →→^{∗} \overline{N′} : τ in the simply typed λ-calculus with streams (we may need more steps than in the orginal, because of marked redexes).

As a result, strong normalization extends to simply typed transformation calculus. □

Proposition 6 (A_{∗}, [[ ]] ) is a model of the simply typed transformation calculus.

PROOF We must prove that our three axioms are verified.

• ≡: the proof is direct for each basic equivalence.

• →_{↓}: just notice that all extensions of [[↓]] are the identity.

• →_{β}: [[{l ⇒N}.λ{l ⇒x}.M]]_{ρ} = [[M]]_{ρ[[[N]]_{ρ}/x]} = [[[N/x]M]]_{ρ}.

□

References

[AKG93] Hassan Aït-Kaci and Jacques Garrigue. Label-selective λ-calculus: Syntax and confluence. In Proc. of the Conference on Foundations of Software Technology and Theoretical Computer Science, pages 24–40, Bombay, India, 1993. Springer-Verlag LNCS 761.

[AKGar] Hassan Aït-Kaci and Jacques Garrigue. Label-selective λ-calculus: Syntax and confluence. Theoretical Computer Science, to appear.

[BCL90] Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Technical Report LIENS-90-14, LIENS, July 1990.

[Bou89] Gérard Boudol. Towards a lambda-calculus for concurrent and communicating systems. In Proceedings of TAPSOFT ’89, pages 149–161, Berlin, Germany, 1989. Springer-Verlag, LNCS 351.

[CCM87] Guy Cousineau, Pierre-Louis Curien, and Michel Mauny. The categorical abstract machine. Science of Computer Programming, 8, 1987.

[CO94] Kung Chen and Martin Odersky. A type system for a lambda calculus with assignments. In Proc. of the International Conference on Theoretical Aspects of Computer Software, pages 347–363, 1994.

[Cur93] Pierre-Louis Curien. Categorical Combinators, Sequential Algorithms, and Functional Programming. Progress in Theoretical Computer Science. Birkhäuser, Boston, 1993. First edition by Pitman, 1986.

[FF87] Mathias Felleisen and Daniel P. Friedman. A calculus for assignments in higherorder languages. In Proc. ACM Symposium on Principles of Programming Languages, pages 314–325, 1987.

[FF89] M. Felleisen and D.P. Friedman. A syntactic theory of sequential state. Theoretical Computer Science, 69:243–287, 1989.

[GAK94] Jacques Garrigue and Hassan Aït-Kaci. The typed polymorphic label-selective λ-calculus. In Proc. ACM Symposium on Principles of Programming Languages, pages 35–47, 1994.

[Gar95] Jacques Garrigue. Label-Selective Lambda-Calculi and Transformation Calculi. PhD thesis, University of Tokyo, Department of Information Science, March [Garar] Jacques Garrigue. Dynamic binding and lexical binding in a transformation

calculus. In Proc. of the Fuji International Workshop on Functional and Logic Programming. World Scientific, Singapore, to appear.

[GH90] J.C. Guzmán and P. Hudak. Single threaded polymorphic calculus. In Proc. IEEE Symposium on Logic in Computer Science, pages 333–343, 1990.

[GL86] David K. Gifford and John M. Lucassen. Integrating functional and imperative programming. In Proc. ACM Conference on LISP and Functional Programming, pages 28–38, 1986.

[Gor79] M. J. C. Gordon. The Denotational Description of Programming Languages. Springer-Verlag, 1979.

[HMT84] J.Y. Halpern, A. R. Meyer, and B. A. Trakhtenbrot. The semantics of local storage, or what makes the free-list free? In Proc. ACM Symposium on Principles of Programming Languages, pages 245–257, 1984.

[JD88] Gregory F. Johnson and Dominic Duggan. Stores and partial continuations as first-class objects in a language and its environment. In Proc. ACM Symposium on Principles of Programming Languages, pages 158–168, 1988.

[Lam88] John Lamping. A unified system of parameterization for programming languages. In Proc. ACM Conference on LISP and Functional Programming, pages 316–326, 1988.

[Lan65] P. J. Landin. A correspondence between ALGOL 60 and Church’s lambda notation. Communications of the ACM, 8(2-3):89–101 and 158–165, February 1965.

[LG88] John M. Lucassen and David K. Gifford. Polymorphic effect systems. In Proc. ACM Symposium on Principles of Programming Languages, pages 47–57, San Diego, California, 1988.

[Mil92] Robin Milner. The polyadic π-calculus: A tutorial. In Logic and Algebra of Specification, pages 203–246. NATO ASI Series, Springer Verlag, 1992.

[MS76] R. Milne and C. Strachey. A Theory of Programming Language Semantics. Chapman and Hall, 1976.

[MS88] Albert R. Meyer and Kurt Sieber. Toward fully abstract semantics for local variables. In Proc. ACM Symposium on Principles of Programming Languages, pages 191–203, 1988.

[MT92a] Ian A. Mason and Carolyn L. Talcott. Inferring the equivalence of functional programs that mutate data. Theoretical Computer Science, 105(2), 1992.

[MT92b] Ian A. Mason and Carolyn L. Talcott. References, local variables and operational reasoning. In Proc. IEEE Symposium on Logic in Computer Science, pages 186– 197, 1992.

[Ole85] F.J. Oles. Type algebras, functor categories, and block strcutures. In N. Nivat and J.C. Reynolds, editors, Algebraic Methods in Semantics, chapter 15, pages 543–573. Cambridge University Press, 1985.

[ORH93] Martin Odersky, Dan Rabin, and Paul Hudak. Call by name, assignment, and the lambda calculus. In Proc. ACM Symposium on Principles of Programming Languages, pages 43–56, 1993.

[PW93] Simon L. Peyton Jones and Philip Wadler. Imperative functional programming. In Proc. ACM Symposium on Principles of Programming Languages, pages 71– 84, 1993.

[Rey81] John C. Reynolds. The essence of ALGOL. In de Bakker and van Vliet, editors, Proc. of the International Symposium on Algorithmic Languages, pages 345–372. North Holland, 1981.

[SRI91] Vipin Swarup, Uday S. Reddy, and Evan Ireland. Assignments for applicative languages. In John Hugues, editor, Proc. ACM Symposium on Functional Programming and Computer Architectures, pages 192–214. Springer Verlag, 1991. LNCS 523.

[THM84] B. A. Trakhtenbrot, Joseph Y. Halpern, and Albert R. Meyer. From denotational to operational and axiomatic semantics for ALGOL-like languages: An overview. In E. CLarke and D. Kozen, editors, Logic of Programs, pages 474–500, Berlin, 1984. LNCS 164, Springer-Verlag.

[TJ92] Jean-Pierre Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245–271, July 1992.

[Wad90a] Philip Wadler. Comprehending monads. In Proc. ACM Conference on LISP and Functional Programming, pages 61–78, 1990.

[Wad90b] Philip Wadler. Linear types can change the world! In M. Broy and C. B. Jones, editors, Programming Concepts and Methods. North Holland, 1990.

[WF93] S. Weeks and M. Felleisen. On the orthogonality of assignments and procedures in Algol. In Proc. ACM Symposium on Principles of Programming Languages, pages 61–78, January 1993.