Label-Selective λ-Calculus Syntax and Confluence

Hassan Aït-Kaci  Jacques Garrigue

December 5, 1994

Abstract

We introduce an extension of λ-calculus, called label-selective λ-calculus, in which arguments of functions are selected by labels. The set of labels combines symbolic keywords with numeric positions. While the former enjoy free commutation, the latter and relative renumbering are needed to extend commutation to conflictuous names, and allow full currying. This extension of λ-calculus is conservative, in the sense that when we restrict ourselves to using only one label, it coincides with λ-calculus. The main result of this paper is the proof that the label-selective λ-calculus is confluent. In other words, argument selection and reduction commute.

Keywords λ-Calculus, Record Calculus, Concurrency, Communication.

Acknowledgements

The authors wish to thank Kathleen Milsted, Atsushi Ohori, Mitsuhiro Okada, and Andreas Podelski for their comments and suggestions. Also, we are grateful to Patrick Baudelaire and Jean-Christophe Patat for kindly and thoroughly proofreading our manuscript.

1 Synopsis

Many modern programming languages allow specifying arguments of functions and procedures by symbolic keywords as well as using the traditional and natural numeric positions [21, 17, 4]. Symbolic keywords are usually handled as syntactic sugar and “compiled away” as numeric positions. This is made easy if the language does not support currying (like Common LISP or ADA).

On the other hand, when currying is supported, the situation has to be reduced to numeric positions alone, which are handled in an absolute left-to-right order, so that the first argument is “consumed” before the second. In general, if a function f is defined on two arguments and it is desired that the second be consumed before the first, one must resort to using an explicit closure of form λx.λy.f(y, x) and curry that one. However, the cost incurred (the closure construction and ensuing weight of handling in terms of depth of stack, etc.) is undue since out-of-order currying simply amounts to commutation of stack offsets.

A short version of this article appeared in the Proceedings of the 13th International Conference on Foundations of Software Technology and Theoretical Computer Science, Bombay, India, December 1993.

The authors may be contacted at the following addresses:

Hassan Aït-Kaci  Jacques Garrigue School of Computing Science  Research Institute for Mathematical Sciences Simon Fraser University  Kyoto University Burnaby, British Columbia  Kitashirakawa-Oiwakecho, Sakyo-ku V5A 1S6, Canada  Kyoto 606-01, Japan hak@cs.sfu.ca                          garrigue@kurims.kyoto-u.ac.jp

More precisely, currying is possible thanks to the following natural isomorphism:

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

for any set A, B and C. However, there is another obvious natural isomorphism that could also be useful; namely, A × B ≃ B × A. Hence we should be able to exploit this directly in the form:

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

One way to do that is to use a style of Cartesian product more of a category-theoretic, as opposed to set-theoretic, flavor. By this we mean that if projections π_{1} and π_{2} were used explicitly instead of the implicit 1st and 2nd of the × notation, then instead of A × B we would write π_{1} ⇒ A × π_{2} ⇒ B. Thus, allowing this explicit product expression makes Cartesian product commutative explicitly, as opposed to “up to isomorphism.” Indeed, it becomes obvious that:^{1}

π_{1} ⇒A × π_{2} ⇒B ≃ π_{2} ⇒B × π_{1} ⇒A,

as one uses for records, and thus that:

π_{1} ⇒A → (π_{2} ⇒B → C) ≃ π_{2} ⇒B → (π_{1} ⇒A → C).

The advantage of explicit projections is clear: one can account directly for symbolic keywords since these play precisely the role of projections. The other benefit is the aforementioned permutativity of currying which allows out-of-order partial application of function to its arguments. For example, an out-of-order application like f(2⇒a) can be readily used when there is a need to consume the second argument before the first, as opposed to the more complex and costly (λx.λy.f(y, x))(a).

The drawback of explicit projections, however, is also obvious: implicit argument positions as numeric offset is lost, and the notation is more cumbersome. It is indeed much easier to write f(x, y) instead of f(1⇒x, 2⇒y) every time we need to apply f to two arguments.

So the question is: can we allow freely mixing implicit and explicit argument selectors safely? In other words, can we allow the notation f(x, y) to be syntactic sugar for explicitly selecting f(1⇒x, 2⇒y)? If we do, the least we should require is that the “all-functions-are-unary” paradigm of λ-calculus be retained. This means that the equation f(x, y) = f(x)(y) should hold for any such expression. However, the syntactic sugaring gives, on one hand, f(x, y) = f(1 ⇒ x, 2 ⇒ y), and on the other hand, f(x)(y) = f(1 ⇒ x)(1 ⇒ y). Therefore the free syntax should guarantee that f(1 ⇒ x, 2 ⇒ y) = f(1 ⇒ x)(1 ⇒ y). In other words, stack offset permutation must be built into the rule of application at numeric positions. This is essentially what is performed in the extension of λ-calculus that we propose here.

1.1 Relation to other work

There is an intuitive relation between our calculus and the notation with offsets introduced by de Bruijn [6] and used for the compilation of λ-calculus in the style of the SECD machine [16]. These offsets are used to denote the “physical” (topological) relation between a variable and its binder. Our labels denote associations between abstractions and applications. The same kind of shifting mechanic is used to keep the links during reductions. However those two kinds of indexes work on two independent levels: variables and arguments. That means that we cannot easily encode selective λ-calculus into the calculus of explicit substitutions [1] for instance. The opposite is possible, thanks to the two-level structure of our calculus. Another connection is the possibility to combine them, obtaining two levels of indices. We have already adapted the calculus of explicit substitutions, and are currently working on a compiling scheme for label-selective λ-calculus based on it.

Another potential connection, albeit from an opposite viewpoint, is with the work of Ohori in compiling extensible records for functional programming [20]. Indeed, records are essentially labeled Cartesian products. Since that style of records allows extensions and outof-order labels, it is possible to use them in a way similar to ours for passing arguments. The techniques used to compile them, like index abstraction, may then be extended to our system. At this time, the connection is not formalized and begs for deeper study.

1Parse the following with ‘⇒’ binding tighter than ‘×’ or ‘→’.

An intuitive, but accurate, explanation of label-selective λ-calculus can be given as extracting implicit concurrency from λ-calculus. It is well-known that λ-calculus is a sequential calculus and for a clear reason: function application is not commutative. This inherent sequentiality is exacerbated all the more by the strict syntactic left-associativity of application adopted by λ-calculus. Hence, our idea is to reveal the inherent concurrency lost in λ-calculus; namely, commutation of arguments in applications. The syntax and operational semantics that we propose are precisely meant to expose, explicate, and exploit this implicit concurrency. This concurrency is inherent in λ-calculus in the sense that it does not interfere with the confluence of the calculus. This would not be the case with a fully concurrent extension of λ-calculus using parallel composition, a commutative monoid. Thus does our calculus differ from the known calculi for communication of concurrent processes [5, 19, 18].

In [5], Gérard Boudol proposes γ-calculus, an extension of λ-calculus based on realizing that β-reduction is communication between a receiving λ-abstraction and a sending operand along one single channel called λ. Thus, the argument of a β-redex is implicitly prefixed with λ̄. This idea is taken to its full extent by Robin Milner in [19] where, rather than λ alone, there are (countably) many channel names. In both Milner’s and Boudol’s calculi, parallel composition is used to achieve full concurrency and thus, naturally, confluence is lost. By contrast, label-selective λ-calculus is not a fully concurrent calculus. Indeed, our calculus is a confluent one. It explicates the fine interaction between functional application as process communication along channel names that are identified, not as λ’s as in [19, 5], but as explicit position names. This is a wholly different insight. In addition, the availability of numeric indexes on channels and their laws of relative commutation allows also to speak of relatively numbered channels, as opposed to absolutely named channels only.

We are also developing, and will report later [3], our label-selective calculus as a true calculus of communication and concurrency. We plan to extend the calculus along the lines of Robin Milner’s π-calculus, adding, for example, process operators, such as parallel composition and non-deterministic choice, as well as exploring other directions, for example, by allowing computable channel names. One of the gains expected is that λ-calculus will need not be encoded as in [18], but directly embedded as syntactic identity.

More recently, we became aware of the work of Laurent Dami [8, 9]. In his work, Dami develops a complex calculus of record objects with a part dealing with functions with named arguments. At a first glance, because it allows named arguments and out-of-order application, Dami’s calculus looks reminiscent of the part of our calculus dealing with symbolic positions. It is in fact fundamentally different. In Dami’s calculus, a functional abstraction is seen as a pair consisting of a name and an expression (its body)—the name (the “inlet” [sic]) designates the result of applying the function to arguments. Arguments are identified as the “unprotected” [sic] (ie. , free) names in the expression. To avoid confusion in name references, a “protection” level in the form of a string of backslashes may prefix a name’s occurrence—if a name’s occurrence is prefixed with n backslashes in an expression, that reference occurs nested n levels deep from its free scope.^{2} Accordingly, an application is also a pair made of a name and an expression. The name designates the unprotected reference (the “outlet” [sic]) in the applied function’s body to substitute for the expression. Hence, Dami’s application is really instantiation through a first-order substitution that associates expressions to names.^{3} Clearly, this view allows out-of-order argument consumption. In fact, Dami’s functions are one-fielded records from which to extract the result (by field-name selection). Complex records are contructed by two operations—a product (called combination) and a coproduct (called alternation)—and are objects behaving like function products and sums, respectively. Besides its intriguing back-to-front view of functions, an essential difference between Dami’s calculus and ours is that his calculus does not distinguish variable names and position names—the two are confused. Although quite original and interesting, his calculus departs, unlike ours, in some rather basic way from λ-calculus.^{4}

2In other words, the number of slashes is the reference’s de Bruijn index.

3In a sense, plugging these expressions into the free “outlets!”

In summary, what we recount in this paper, has not, to our knowledge, been studied as such.

1.2 Organization of paper

We have organized this paper as follows. In Section 2 we introduce our language of selective λ-terms, and define various selective λ-calculi based on them. In Section 3 we define the selective λ-calculus, including all of them. We add some variations to its syntax, and present some reflections about their meaning. The core of the paper lies in Section 4 where we give the proof of confluence of selective λ-calculus. Finally, we close the paper with some conclusion and a brief discussion of further work to follow this idea in Section 5.

2 Introducing selective λ-calculi

2.1 Generic syntax

Selective λ-terms are formed by variables taken from a set V, and two labeled constructions: abstraction and application. The labeling is done with labels taken from a set of position labels L.

We will denote variables by x, y, labels in L by p, q, and λ-expressions by capitals.

We can define the syntax of λ-terms as:

M ::= x  (variables),
| λ_{p}x.M (abstractions),
| M _{p} M (applications).

We will say of a term λ_{p}x.M that it “abstracts x at p in M,”, and of the term M _{p} N, that it “applies M to N through p.”

It will often be convenient to break the atomicity of an abstraction or an application. In the abstraction λ_{p}x.M, the part λ_{p}x will be called its abstractor, and M its body. In the application M _{p} N, the part _{p} N will be called the applicator. By entity, we will mean either an abstractor or an applicator.

2.2 Relative and absolute positions

Before we look at different selective λ-calculi, let us give some intuition to justify this syntax, thinking of two possible sets of labels, symbolic and numeric ones.

Symbolic labels are what we referred to as “keywords” in the introduction. A useful way of thinking of these symbols is to see them as channel names used for process communication [19]. Here, a process is a λ-term, where sending is performed by applicators and receiving by abstractors. If an application is performed (“sends arguments”) through two different channels p and q, then clearly there cannot be any ambiguity as far as which abstractor will “receive” them. Hence, these reductions (“communications”) may be done in any order, with the same end result. However, if that situation arises with p = q, then clearly the order in which they are performed will matter. In this case, the rules will insure that reduction will respect the order specified syntactically. In other words, several arguments sent through the same channel are “buffered” in sequence.^{5}

If numeric labels are always kept explicit, then the above view applies to them as well. Indeed, recall from the introduction that the free syntax of function application to several arguments at a time uses their positions as Cartesian projections; eg. , f(a_{1}, …, a_{n}) may be seen as the more explicit f(1⇒a_{1}, …, n⇒a_{n}). However, numeric labels do not quite behave like symbolic labels in that a number is always implicitly seen as the first position relatively to the form on its left. More precisely, currying works by seeing each argument as the first one relatively to the form on its left. This has the benefit of simplifying the rule of functional reduction to be a local rule never needing to consider more than a single argument at a time. So, clearly, we do want to allow using relative argument positions.

4Quoting Dami’s own words: “an abstraction (...) is somewhat similar to a λ-abstraction (...). However, there are perhaps more differences than similarities.” Indeed!

5In fact, we are also considering a possible variation of our calculus where this sequential buffering is not guaranteed. Rather, several arguments received on a given channel are chosen non-deterministically. This interesting twist yields essentially the functionality of asynchronous process communication, at the expense, of course, of confluence. That work is the object of our current study and will be reported later [3].

Nevertheless, it is more natural to use absolute positions “packaged” as labeled Cartesian tuples. For instance, it is easier to write (λ(1 ⇒ x, 2 ⇒ y, 4 ⇒ z).M) (1 ⇒ a, 4 ⇒ b) rather than (λ_{1}x.λ_{1}y.λ_{2}z.M) _{1} a _{3} b. However, the latter fully curried form is needed to express reduction with local rules. Fortunately, translation from the notation with absolute labels to a fully curried one with relative labels is in fact systematic: one need simply subtract from each numeric label the number of numeric-labeled components, smaller than it, and appearing to its left in the labeled Cartesian product. Namely,

\begin{matrix}M (n_{1} ⇒N_{1}, …, n_{k} ⇒N_{k}) = M _{n′_{1}} N_{1} … _{n′_{k}} N_{k} \\ where n′_{k} = n_{k} − |\{i | i < k, n_{i} < n_{k}\}|. \end{matrix}

Conversely, one may go back from relative syntax to the absolute one by inserting iteratively entities in an abstraction or application tuple. That is,

(M _{m} N) (n_{1} ⇒N_{1}, …, n_{k} ⇒N_{k}) = M (m⇒N, n′_{1} ⇒N_{1}, …, n′_{k} ⇒N_{k})

where n′_{i} = \{ \begin{matrix}n_{i} & if n_{i} < m \\ n_{i} + 1 & if n_{i} ≥ m \end{matrix}

These two rules apply directly for abstractions too, and one may verify that they just do opposite work.

For the absolute and relative notations to be effectively coherent, we will expect M (n_{1} ⇒ N_{1}, …, n_{k} ⇒N_{k}) and M (n_{σ(1)} ⇒N_{σ(1)}, …, n_{σ(k)} ⇒N_{σ(k)}) to be convertible terms for any permutation σ of IN_{k}, that is, the order of the pairs in a record should be semantically irrelevant.

With this, we are justified to limit our syntax to that of relative-labeling lending itself to simpler local reduction rules, while still keeping the freedom of a flexible surface syntax with Cartesian tuples using absolute position labeling.

Now, a reasonable question that one may have is whether we could not also treat symbolic labels as we do numeric labels. That is, we could envisage using a function associating each symbol to its predecessor in the linear order of symbols, thus doing away with names altogether.^{6} This, however, would be possible only if the order on symbols were not dense. Since, in practice, symbols are the free monoid, generated by a subset of the ASCII alphabet, and is densely ordered by lexicographic ordering, this is ruled out. Hence, symbolic labels always designate absolute positions of arguments. In other words, packaging symbolic-labeled arguments in labeled Cartesian tuples is always safe since they are not concerned with relative positioning. In fact, the ordering on symbols is only necessary as a trick to avert nontermination so that rules may perform well-founded label commutation.

Reciprocally one could think of getting rid of numeric labels. However, simply forgetting about numeric labels, just because they are a little cumbersome, would reduce the generality of the calculus. With only symbolic labels we can directly send values to abstractions as long as they have different labels. An abstraction can still be hidden by another abstraction with same label. However, with symbolic labels, we have this property in all cases. This is certainly useful if you want, for instance, to construct a model of this calculus: intuitively all curried functions become flat, while they would still be partly hierarchized in an only keyword calculus.

2.3 A lambda-calculus with multiple channels

This is the first possibility, using keywords as label. We define an extension of the lambda calculus, the symbolic selective λ-calculus, with symbolic labels.

6This would amount to “compiling them away” as alluded to in the introduction.

β − reduction

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

Reordering

(1) λ_{a}x.λ_{b}y.M → λ_{b}y.λ_{a}x.M  a > b
(2) M _{a} N_{1} _{b} N_{2} → M _{b} N_{2} _{a} N_{1} a > b
(3) (λ_{a}x.M) _{b} N → λ_{a}x.(M _{b} N) a ≠ b, x ∉ F V (N)

Figure 1: Reduction rules for symbolic selective λ-calculus

Following the above syntax, we take our labels from a totally ordered set of symbols S. We will denote these labels by a, b.

To keep compatibility with the classical λ-calculus, we have a default label, 1, such that an unlabeled abstraction or application is interpreted as being labeled by 1.

The reduction rules for this calculus are given in Figure 1. β-reduction only happens on abstractor-applicator pairs with the same label. Otherwise they commute by rule (3). Rules (1) and (2) normalize the order of abstractors and applicators. The condition x ∉ F V (N) in rule (3) can always be satisfied through α-conversion.

Definition 1 We call symbolic selective λ-calculus the free combination of rules in Figure 1.

This calculus is meaningful, in that it is confluent.

Corollary 1 The symbolic selective λ-calculus is confluent.

PROOF Consequence of the proof for selective λ-calculus. □

Example 2.1 We suppose that a < b < c < d, (For keywords the notations λ(a⇒x, …) and M(a⇒N, …) are only shorthands.)

(λ(a⇒x, b⇒y, c⇒z).M) (c⇒N_{1}, d⇒N_{2}, a⇒N_{3})
= (λ_{a}x.λ_{b}y.λ_{c}z.M) _{c} N_{1} _{d}N_{2} _{a} N_{3}
→_{3} (λ_{a}x.((λ_{b}y.λ_{c}y.M) _{c} N_{1})) _{d}N_{2} _{a} N_{3}
→_{2} (λ_{a}x.((λ_{b}y.λ_{c}y.M) _{c} N_{1})) _{a} N_{3} _{d}N_{2}
→_{β} (λ_{b}y.λ_{c}z.[N_{3}/x]M) _{c} N_{1} _{d}N_{2}
→_{3} (λ_{b}y.((λ_{c}z.[N_{3}/x]M) _{c} N_{1})) _{d}N_{2}
→_{β} (λ_{b}y.([N_{3}/x][N_{1}/z]M)) _{d}N_{2})
→_{3} λ_{b}y.([N_{3}/x][N_{1}/z]M _{d}N_{2})

2.4 A lambda-calculus with moving indexes

In this calculus we can selectively apply a function on any of its arguments, according to its apparent position.

For an unlabeled expression, the apparent position of an abstractor is intuitively defined as the number of times we have to apply this expression in order to have the abstractor applied to the desired argument. For instance, in λx.λy.λz.M, the apparent position of the abstractor of z is 3, but in λx.(λy.λz.M)N it is 2. As a consequence, apparent positions do not change when we reduce an expression. When we add labels, we want to keep this property.

Definition 2 Numerical selective λ-calculus takes its labels from N = IN − {0}. Reduction rules on terms modulo α-conversion are given in Figure 2.

Definition 3 The apparent position of an abstractor in a term M is n such that M _{n} N associates this abstractor and N (makes them to be β-reduced together eventually).

β − reduction

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

Reordering

(1) λ_{m}x.λ_{n}y.M → λ_{n}y.λ_{m−1}x.M  m > n
(2) M _{m} N_{1} _{n} N_{2} → M _{n} N_{2} _{m−1} N_{1} m > n
(3) (λ_{m}x.M) _{n} N → λ_{m−1}x.(M _{n} N) m > n, x ∉ F V (N)
(4) (λ_{m}x.M) _{n} N → λ_{m}x.(M _{n−1} N) m < n, x ∉ F V (N)

Figure 2: Reduction rules for numerical selective λ-calculus

Well-definedness of apparent positions is guaranteed by confluence. Of course, if an abstractor is already linked with an applicator in the term, or appears in the right-hand of an application, it has no apparent position.

Corollary 2 The numerical selective λ-calculus is confluent.

PROOF Consequence of the proof for selective λ-calculus. □

We can now relate apparent positions to the absolute positions of our relative vs. absolute dichotomy. The idea is that when we apply M to the tuple (n_{1} ⇒N_{1}, …, n_{k} ⇒N_{k}), the n_{i}’s, which are absolute positions in the above definition, are the apparent positions in M of the abstractors they aim at. Similarly, in λ(n_{1} ⇒ x_{1}, …, n_{k} ⇒ x_{k}).M, x_{i} has apparent position n_{i}. As a result, we have

(λ(n_{1} ⇒x_{1}, …, n_{k} ⇒x_{k}).M) (n_{1} ⇒N_{1}, …, n_{k} ⇒N_{k}) →^{∗} [N_{i}/x_{i}]_{i=1}^{k}M

and the order of bindings in records is free, as one would expect.

Example 2.2 Numerical indexes

(λ(2⇒x, 1⇒y, 4⇒z).M) (4⇒N_{1}, 6⇒N_{2}, 2⇒N_{3})
= (λ_{2}x.λ_{1}y.λ_{2}z.M) _{4} N_{1} _{5} N_{2} _{2} N_{3}
→_{4} (λ_{1}y.λ_{1}x.λ_{2}z.M) _{4} N_{1} _{5} N_{2} _{2} N_{3}
→_{7} (λ_{1}y.((λ_{1}x.λ_{2}z.M) _{3} N_{1})) _{5} N_{2} _{2} n_{3}
→_{5} (λ_{1}y.((λ_{1}x.λ_{2}z.M) _{3} N_{1})) _{2} N_{3} _{4} N_{2}
→_{7} (λ_{1}y.λ_{1}x.((λ_{2}z.M) _{2} N_{1})) _{2} N_{3} _{4} N_{2}
→_{β} (λ_{1}y.λ_{1}x.[N_{1}/z]M) _{2} N_{3} _{4} N_{2}
→_{7} (λ_{1}y.((λ_{1}x.[N_{1}/z]M) _{1} N_{3})) _{4} N_{2}
→_{β} (λ_{1}y.[N_{3}/x][N_{1}/z]M) _{4} N_{2}
→_{7} λ_{1}y.([N_{3}/x][N_{1}/z]M _{3} N_{2})

2.5 A first way to combine these two systems

Intuitively it would be interesting to get in one calculus both the power of symbolic and numeric selective λ-calculi.

For this we take L to be the disjoint union of the two sets N of numeric, and S of symbolic labels. Namely, N is ordered with the natural number ordering, that we shall write <_{N}; S is ordered with a linear order that we write <_{S}; and, L is ordered by the order <_{L} such that <_{L} = <_{N} on N, <_{L} = <_{S} on S, and ∀(n, p) ∈ N × S, n <_{L} p. In other words, all numeric labels are less than all symbolic labels.

Our set of rule is the union of numeric (Fig. 2) and symbolic (Fig. 1) rules applied to their respective sets of labels, and the three following rules, which just generalize symbolic ones to handle conflicts with numeric labels, in conformity with our new order.

(1′) λ_{a}x.λ_{n}y.M → λ_{n}y.λ_{a}x.M
(2′) M _{a} N_{1} _{n} N_{2} → M _{n} N_{2} _{a} N_{1}
(3′) (λ_{a}x.M) _{n} N → λ_{a}x.(M _{n} N) x ∉ F V (N)

We call this system flat selective λ-calculus. Again it is confluent.

Corollary 3 The flat selective λ-calculus is confluent.

PROOF Consequence of the proof for selective λ-calculus. □

We considered for a long time the flat calculus as the best balanced of these calculi, since it includes both symbolic and numeric calculi in a coherent way. Indeed most of the terms one would write can be expressed in it. However it appears that a stronger one includes it conservatively, and we will rather chose that one as “fundamental” calculus.

3 The selective λ-calculus

3.1 Definition

3.1.1 Syntax

Selective λ-calculus combines orthogonally symbolic and numerical selective λ-calculi. Its set of labels is L = S × N. ^{7} The order induced on labels is the lexicographical one: a <_{S} b ⇒ am <_{L} bn and m <_{N} n ⇒ am <_{L} an.

M ::= x | λ_{an}x.M | M _{an} M′

The set of selective λ-terms (considered modulo α-conversion) is Λ. We use a, b for symbols (or channels), m, n for numbers (or indexes), and p, q for labels formed of a couple (channel,index).

3.1.2 Substitutions

Substitution of variables by λ-expressions needs the same precautions as in λ-calculus and obeys exactly the same rules. As usual, we use the equal sign (=) to mean syntactic equality modulo α-conversion, defining α-conversion as for classical λ-calculus.

Let FV(M) be the set of free variables in M, defined as usual in lambda calculus. The expression [N/x]M denotes the term obtained by replacing all the free occurrences of a variable x by N in (an appropriate α-renaming of) M. That is,

[N/x]x  = N
[N/x]y = y if y ∈ V, y ≠ x
[N/x](M_{1} _{p} M_{2}) = ([N/x]M_{1}) _{p} ([N/x]M_{2})
[N/x](λ_{p}x.M)  = λ_{p}x.M
[N/x](λ_{p}y.M)  = λ_{p}y.[N/x]M
if y ≠ x and y ∉ FV(N)
[N/x](λ_{p}y.M)  = λ_{p}z.[N/x][z/y]M
if y ≠ x and y ∈ FV(N),
and z ∉ FV(N)∪ FV(M).

3.1.3 Reductions

The reduction system is the combination in Figure 3. We call weak reordering the system excepting β-reduction. It may look complex, but one may see reordering rules as structural equalities, and then we have β-reduction as unique reduction rule. One might wonder about why then we do not adopt this view, and separate completely reordering from β-reduction. The answer is that to define from the beginning reordering as a structural equivalence, we would need a good understanding of what is a term modulo reordering. As a matter of fact, we can define it, using a monoid of records. But it would be as complex, and term structure harder to grasp. So, it is probably more convincing to first verify the confluence on a simple structure, and then trivially extend it to the equational one.

7In [2] this was defined as a product system, and selective λ-calculus as the sum system L = S ∪ N.

Properties of the two systems being similar, we work here on the most general one.

β − reduction

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

Symbolic reordering

(1) λ_{am}x.λ_{bn}y.M → λ_{bn}y.λ_{am}x.M  a > b
(2) M _{am} N_{1} _{bn} N_{2} → M _{bn} N_{2} _{am} N_{1}  a > b
(3) (λ_{am}x.M) _{bn} N → λ_{am}x.(M _{bn} N)  a ≠ b, x ∉ F V (N)

Numeric reordering

(4) λ_{am}x.λ_{an}y.M → λ_{an}y.λ_{am−1}x.M  m > n
(5) M _{am} N_{1} _{an} N_{2} → M _{an} N_{2} _{am−1} N_{1} m > n
(6) (λ_{am}x.M) _{an} N → λ_{am−1}x.(M _{an} N) m > n, x ∉ F V (N)
(7) (λ_{am}x.M) _{an} N → λ_{am}x.(M _{an−1} N) m < n, x ∉ F V (N)

Figure 3: Reduction rules for selective λ-calculus

Since the combination is orthogonal (symbolic and numeric labels work on two independent levels), confluence is inherited from the two previous systems.

Theorem 1 The selective λ-calculus is confluent.

PROOF in Section 4. □

To let this system include the symbolic and numerical sub-calculi, we will identify a symbol a with the label (a, 1) and an index n with the label (1, n) (this 1 being the default channel of the symbolic calculus). Remark that the default label 1, used to interpret the classical λ-calculus, will result into (1,1) by both rules.

3.2 Entity syntax

To emphasize the similarity between abstraction and application we define a new notation for the first.

λ_{p}x.M = M ∨ p x

for any p ∈ L, x ∈ V, M ∈ Λ.

As a result, β-reduction becomes:

M ∨ p x ∧ p N →_{β} M[x\N],

where it is natural to write substitutions on the right side of terms.

We can redefine more clearly the notions we introduced for the generic syntax, and introduce some new ones.

Definition 4 An entity (in Γ), either an applicator or an abstractor, is a pair of an operator (∧ p or ∨ p for some p ∈ L) and a term for applications, a variable for abstractions.

We chose here the term abstractor rather than the usual binder to emphasize on the presence of a label. Then we can call binder the variable of an abstractor, that is the x in ∨ p x.

Definition 5 We distinguish in a term its head and its spine. Any selective λ-term can be written

x ⊙ P = (… (x e_{1}) …)e_{n}

where the head x is a variable and the spine P an entity sequence (e_{1}, …, e_{n}) ∈ Γ^{∗}. ι_{P} (e_{k}) = n − k is the position of e_{n} in P (counting from the right).

• For any entity sequence P in Γ^{∗} we define BV (P), the set of variables bounded by P, that is the set of variables abstracted by the roots of the entities forming P. For any M in Λ, any occurrence of a variable of BV (P) in M is bound in M ⊙ P.

• We note P · Q the concatenation of two entity sequences, and have M ⊙ (P · Q) = (M ⊙ P) ⊙ Q.

Example 3.1 In the term x ∧ p z ∨ q x ∨ q y, x is the head and P =∧ p y ∨ q x ∨ q y the spine. BV (P) is {x, y} and F V (P) is {z}.

This notation will simplify many proofs. We will use indifferently the two notations in the following.

3.3 Towards a transformation calculus

Before going on to the proof of confluence, we will just give here some hints about the future developments of selective λ-calculus. We will base ourselves on the new notation introduced above, and explain in what way this notation suggests another extension.

The intuition behind selective λ-calculus is no longer functions but functions over labeled arguments which behave like communicating processes through named and (relatively) indexed channels. Application corresponds to process communication. What we called entities are seen as actions: abstractors correspond to receiving and applicators to sending. But what about composition? It is easily defined for functions as f ∘ g = λx.f(gx) in the classical calculus. But in the selective λ-calculus we would have to parameterize this composition with three labels! That is f ∘^{p,q,r} g = f ∧ p (g ∧ q x) ∨ r x, the function taking its input on r, giving it to g on q, and feeding the result to f on p. This is complex, and this is rather weak. Particularly when we think of the powerful out-of-order currying power of our system.

Rather, we will just use syntactic juxtapostion ⊙, as defined above. Then we can obtain a more interesting composition with M ∘ P = M ⊙ P, where we do not specify anything about labels, and may have created more than one connection at once. Here again P is a sequence of actions, and we would like to manipulate them as such. This lets us define a transformation calculus [11], able to describe notions like state in a lambda calculus framework. More immediately, the potential of this notation is such that it simplifies considerably many proofs. For instance we could prove easily Böhm’s expansion theorem using it. Since our extension is conservative, our proof is valid for classical λ-calculus as well.

Of course, all this starts to be strongly reminiscent of a calculus for process communication [19], although still a direct and conservative extension of classical λ-calculus, and particularly still confluent, thanks to our indexes. We believe that this is not coincidental. This idea is the object of our current research and we are actively exploring the deep connections with the various existing communication calculi. But, we shall say no more on this for now.

4 Proof of confluence

4.1 Pseudo-reduction

4.1.1 Rules

Pseudo-reduction rules are intended to make reordering systems confluent in the absence of β-reduction. They promote the formation of new reordering redexes by commutation over β-redexes. The idea is that, without β-reduction, β-redexes just sit there, presenting “obstacles” to the formation of reordering redexes. Hence, we need pseudo-reduction rules to simulate the promotion of reordering redexes that would appear if the β-reduction had been performed. We simulate that effect by having a labeled entity “jump” into, or out of, the body of the abstraction part of a β-redex through its “λ-membrane” and seek reordering on the other side of that membrane. There are two cases: (a) one corresponding to having an applicator jump “into” the body of the abstraction part of a β-redex, and (b) the other corresponding to having an abstractor jump “out of” it. Namely,

\begin{matrix}(a) & M ∨ p x ∧ p N_{1} ∧ q N_{2} → M ∧ q N_{2} ∨ p x ∧ p N_{1} & x ∉ F V (N_{2}) \\ (b) & M ∨ q y ∨ p x ∧ p N → M ∨ p x ∧ p N ∨ q y & y ∉ F V (N) \end{matrix}

Example 4.1 If we use only reordering rules, (λ_{1}x.λ_{2}y.x ∧ 1 y) ∧ 2 a ∧ 1 b can be reduced by Rules (7) and (6) yielding A = (λ_{1}x.λ_{1}y.x ∧ 1 y ∧ 1 a) ∧ 1 b. It can also be reduced by Rule (5) to B = (λ_{1}x.λ_{2}y.x ∧ 1 y) ∧ 1 b ∧ 1 a. Both terms A and B are normal forms with respect to reordering. We need pseudo-reduction to recover confluence. Namely, applying Rule (a) to B promotes the appearance of a redex for Rule (6), which yields A.

4.1.2 Pseudo-reduced form equivalence (PRF)

Since some critical pairs appear between reordering rules, we introduce an equivalence relation that unifies their results. Confluence of the reordering part of the system can only be considered under this equivalence.

Definition 6 If x ∉ F V (N_{1}) and y ∉ F V (N_{2}) then

M ∨ q y ∧ q N_{1} ∨ p x ∧ p N_{2} ↔ M ∨ p x ∧ p N_{2} ∨ q y ∧ q N_{1}

For any M, x, N,

M {∨ \atop am} x {∧ \atop am} N ↔ M {∨ \atop an} x {∧ \atop an} N

Example 4.2 Consider the term A = M ∨ 1 x ∨ 2 y ∧ 2 N ∧ 1 N′. If we exclude β-reduction, we can still apply either rule (4) or (5), yielding to B = M ∨ 1 y ∨ 1 x ∧ 2 N ∧ 1 N′ or C = M ∨ 1 x ∨ 2 y ∧ 1 N′ ∧ 1 N, which by (7) and (6) give B′ = M ∨ 1 y ∧ 1 N ∨ 1 x ∧ 1 N′ and C′ = M ∨ 1 x ∧ 1 N′ ∨ 1 y ∧ 1 N. No reordering rule can recover confluence between B′ and C′, but they are PRF equivalent.

The necessity for the second equation is more subtle, but is linked to the use of pseudoreductions.

Combining these two we can see that PRF equivalence makes both order and symbolic part of labels irrelevant for locally associated pairs (cf. Def. 8), as long as variable dependencies are satisfied.

4.2 Combined systems and restricted reductions

We will first distinguish reordering rules, and prove properties of those alone. To do this we have to add some rules to preserve confluence: pseudo-reductions (a) and (b). So the system we are really interested in is weak reordering combined with pseudo-reduction. We will call it the reordering system.

An order normal form is a normal form for the reordering system.

A stable reordering is a reordering where pseudo-reduction is prefered to weak reordering for critical pairs.

Intermediate statements will be done on the system called β-reordering. It is β-reduction on order normal forms, where the result of each step is normalized by the reordering system.

A last system, the label-parallel system, which makes the link between selective λ-calculus and β-reordering, is the combination of all rules, and the stable label-parallel system includes the same restriction as stable reordering.

For each of these reduction systems, we shall use the symbol → to indicate a single reduction step using any of system’s rules, and →_{r} if the rule uses Rule (r). When unconcerned by termination, we shall accept the step (M → M) in this relation. As usual, →^{∗} is the reflexive and transitive closure, also possibly subscripted. Given a reduction strategy ϱ, we will use the symbol ▷_{ϱ} to denote the subrelation of →^{∗} using only ϱ-reduction steps. For example, ▷_{stb} for stable reorderings, ▷_{mcd} for minimal complete developments, etc…

For many of these systems confluence will be considered modulo pseudo-reduced form equivalence. Here is the definition, as given in [15].

Definition 7 We say that the relation → is confluent modulo ∼ iff

(∀xyx′y′) x ∼ y ∧ x →^{∗} x′ ∧ y →^{∗} y′ ⇒ (∃\overline{x}\overline{y}) x′ →^{∗} \overline{x} ∧ y′ →^{∗} \overline{y} ∧ \overline{x} ∼ \overline{y}.

4.3 Confluence of the reordering system

Before going on it may be good to have an idea of what an order normal form looks like, but first we need a basic definition.

Definition 8 An abstractor and an applicator are said to be locally associated when they match β-reduction, namely ∨ p x and ∧ p N in M ∨ p x ∧ p N. They are locally free if they do not. They are associated if a reordering can bring them to this state, free otherwise.

Proposition 1 The general structure of an order normal form is:

x {∧ \atop p_{1}} N_{1} … {∧ \atop p_{j}} N_{j} {∨ \atop q_{k}} y_{k} {∧ \atop q_{k}} K_{k} … {∨ \atop q_{1}} y_{1} {∧ \atop q_{1}} K_{1} {∨ \atop r_{l}} x_{l} … {∨ \atop r_{1}} x_{1}
where p_{i} ≤ p_{i+1}, r_{i} ≤ r_{i+1}, N_{i}’s and K_{i}’s are in order normal form.

PROOF Thanks to rules (3),(6),(7) and pseudo-reductions, in each spine, all locally free applicators (resp. abstractors) have to be on the left of all absractors (resp. on the right of all applicators).

By rules (1) and (4) free abstractors must have decreasing labels; and by rules (2) and (5) free applicators must have growing ones.

Locally associated abstractors and applicators stay by pair with the same label. □

Then next lemma is essential, since it allows us to consider reordering as a reduction on independent spines rather than terms.

Lemma 1 (Stability of entities) The reordering rules (1)–(7),(a), (b) do not produce any labeled entities nor do they destroy any. Moreover, a labeled entity stays on the same spine after any reordering rule application, and only the numeric part of its label may change.

PROOF A quick look at the rules shows that none moves an entity from a spine in the set of spines of a term to another one. Moreover, it is even possible to track entities through the transformations, considering that those entities corresponding to the same label occurrence on the two sides of the rule are in fact identical up to variable renaming details (by “same label occurrence” we include m and m − 1, n and n − 1). □

Now we can give a new, and more general definition of the notion of apparent position. We base it on shifting.

Definition 9 To each spine P we associate a shifting function ϕ(P) defined as follows. It corresponds to pushing right {∨ \atop am} x through P, using reordering rules bidirectionally.

ϕ()(am)  = am
ϕ({∨ \atop bk} y · P)(am) = ϕ(P)(am)  a ≠ b
ϕ({∧ \atop bk} N · P)(am) = ϕ(P)(am)  a ≠ b
ϕ({∨ \atop an} y · P)(am) = ϕ(P)(am)  m < n
ϕ({∨ \atop an} y · P)(am) = ϕ(P)(am + 1) m ≥ n
ϕ({∧ \atop an} N · P)(am) = ϕ(P)(am)  m < n
ϕ({∧ \atop an} N · P)(am) = ϕ(P)(am − 1) m > n

ϕ(P)(am) is undefined iff our abstractor bumps into an applicator with same label in P. Similarly ϕ^{−1}(P)(am) is uniquely defined and corresponds to pushing left {∧ \atop am} N through P; it is undefined iff our applicator bumps into an abstractor with same label.

Proposition 2 (shifting) a. ϕ is compositional: ϕ(P · Q) = ϕ(Q) ∘ ϕ(P). b. ϕ^{−1}(P) = ϕ(\overline{P}) where \overline{P} is the dual of P.

\begin{aligned}\overline{P · Q} & = & \overline{Q} · \overline{P} \\ \overline{{∨ \atop an} x} & = & {∧ \atop an} x \\ \overline{{∧ \atop an} N} & = & {∨ \atop an} x_{N} \end{aligned}

PROOF

a. by the recursivity of the definition.

b. by verifying cases 5 and 7 of the definition exchange correctly, and by compositionality of ϕ.

□

Definition 10 The apparent position of {∨ \atop an} x in P = P_{1}· {∨ \atop an} x · P_{2} is π_{P} ({∨ \atop an} x) = ϕ(P_{2})(an). That of {∧ \atop an} N is P = P_{1}· {∧ \atop an} N · P_{2} is π_{P} ({∧ \atop an} N) = ϕ^{−1}(P_{1})(an).

We will have to verify that this new definition matches the precedent. This is in fact equivalent to having the following static association match previous association.

Definition 11 An abstractor {∨ \atop am} x and an applicator {∧ \atop an} N are said to be statically associated when they belong to the same spine P · {∨ \atop am} x · Q· {∧ \atop an} N · R and ϕ(Q)(an) = am.

What intuitionally this definition does is using ϕ to simulate a reordering moving {∨ \atop am} x outwards. If this simulation succeeds in meeting {∧ \atop an} N with an abstractor {∨ \atop an} x, then they are statically associated.

The following lemma is the most important of this subsection. It proves all at once that apparent positions are invariant, static association too, and that it is association.

Lemma 2 Apparent positions are conserved by reordering.

PROOF We only study the case for an abstractor, since we can extend to applicators by duality (Proposition 2b, all reordering rules being symmetrical w.r.t. abstractors and applicators).

In P · {∨ \atop am} x · Q, we have three possible positions of the reordering redex:

1. either the redex is included in P, and has no effect on the apparent position,

2. either it is included in Q = Q_{1} · R · Q_{2}, with R the redex, and we need to prove that ϕ(R′) = ϕ(R), since ϕ(Q) = ϕ(Q_{2}) ∘ ϕ(R) ∘ ϕ(Q_{1}),

3. either it contains {∨ \atop am} x.

We first prove that for any reordering redex R, ϕ(R′)(ck) = ϕ(R)(ck). We proceed by case on the rules:

• Symbolic rules. We only detail the first one: {∨ \atop bn} y {∨ \atop am} x →{∨ \atop am} x {∨ \atop bn} y. If c ≠ a and c ≠ b then ϕ(R′)(ck) = ϕ(R)(ck) = ck. If c = a then ϕ(R′)(ak) = ϕ(R)(ak) = ϕ({∨ \atop am} x)(ak). Resp. for c = b.

Others use the same argument (one interference in maximum, and invariant).

• Numeric rules. If c ≠ a then there is no interference: ϕ(R′)(ck) = ϕ(R)(ck) = ck. Otherwise we calculate the interference case by case.

(4)  ϕ({∨ \atop an} y {∨ \atop am} x)(ak)  ϕ({∨ \atop am−1} x {∨ \atop an} y)(ak)
k ≥ m − 1 ≥ n ϕ({∨ \atop am} x)(ak + 1)  = ak + 2 = ϕ({∨ \atop an} y)(ak + 1)
m − 1 > k ≥ n ϕ({∨ \atop am} x)(ak + 1)  = ak + 1 = ϕ({∨ \atop an} y)(ak)
m − 1 ≥ n > k ϕ({∨ \atop am} x)(ak)  = ak = ϕ({∨ \atop an} y)(ak)
(5)  ϕ({∧ \atop am} N_{1} {∧ \atop an} N_{2})(ak)  ϕ({∧ \atop an} N_{2} {∧ \atop am−1} N_{1})(ak)
k > m > n  ϕ({∧ \atop an} N_{2})(ak − 1)  = ak − 2 = ϕ({∧ \atop am−1} N_{1})(ak − 1)
m > k > n  ϕ({∧ \atop an} N_{2})(ak)  = ak − 1 = ϕ({∧ \atop am−1} N_{1})(ak − 1)
m > n > k  ϕ({∧ \atop an} N_{2})(ak)  = ak = ϕ({∧ \atop am−1} N_{1})(ak)
(6)  ϕ({∨ \atop am} x {∧ \atop an} N)(ak)  ϕ({∧ \atop an} N {∨ \atop am−1} x)(ak)
k ≥ m > n  ϕ({∧ \atop an} N)(ak + 1)  = ak = ϕ({∨ \atop am−1} x)(ak − 1)
m > k > n  ϕ({∧ \atop an} N)(ak)  = ak − 1 = ϕ({∨ \atop am−1} x)(ak − 1)
m > n > k  ϕ({∧ \atop an} N)(ak)  = ak = ϕ({∨ \atop m−1} x)(ak)
(7)  ϕ({∨ \atop am} x {∧ \atop an} N)(ak)  ϕ({∧ \atop an−1} N {∨ \atop am} x)(ak)
k > n − 1 ≥ m ϕ({∧ \atop an} N)(ak + 1)  = ak = ϕ({∨ \atop am} x)(ak − 1)
n − 1 > k ≥ m ϕ({∧ \atop an} N)(ak + 1)  = ak + 1 = ϕ({∨ \atop am−1} x)(ak)
n > m > k  ϕ({∧ \atop an} N)(ak)  = ak = ϕ({∨ \atop m−1} x)(ak)

• Pseudo-reductions. For any pair P ={∨ \atop an} x {∧ \atop an} N, ϕ(P) = Id: this is clear for a label with a different symbolic part. Otherwise, either m < n, and ϕ(P)(am) = ϕ({∧ \atop an} N)(am) = am, or m ≥ n, and ϕ(P)(am) = ϕ({∧ \atop an} N)(am + 1) = am.

As a result, since pseudo-reductions do not change indexes, ϕ(R′) = ϕ(R) = ϕ(∧ q N_{2}) (resp. ϕ(∨ q y)).

When the reordering redex contains {∨ \atop am} x, we verify that they stay associated. Pseudoreductions and symbolic reordering are clearly not a problem, since the former moves a locally assocated pair, with no effect on ϕ, and the later move an entity with a different symbolic part.

For the numeric rules we just remark that ϕ simulates a reduction moving {∨ \atop am} x outwards, using the rules bidirectionally. As such all steps are either the actual simulated step (outward) or its opposite (inward), and naturally static association is conserved. □

Corollary 4 Static associations are conserved by reordering. Static association is association.

PROOF The spine is P · {∨ \atop am} x · Q· {∧ \atop an} N · R.

When the reordering redex contains both {∨ \atop am} x and {∧ \atop an} N, this is a pseudo-reduction, and they stay locally associated, which is statically associated.

When the reordering redex is contained in P · {∨ \atop am} x · Q, we apply Lemma 2 on it. Otherwise we apply the lemma on Q· {∧ \atop an} N · R. Moreover, by Proposition 1, in an order normal form all entities are either free or locally

associated. So, statically associated entities associated.

Reciprocally, since statically free entities have an apparent position out of the spine, they cannot be associated. As such all associated entities are statically associated. □

With these lemma and corollary we easily prove the confluence of reordering modulo PRF equivalence, once we have termination.

Proposition 3 The reordering system in Noetherian.

PROOF We define a mesure on spines by the following ordered pair (remember that positions (ι_{P}) in a spine start from the right):

μ(P) = (|{(e, e′) ∈ P | e abstractor, e′ applicator, ι_{P} (e) > ι_{P} (e′)}|,
|{(e, e′) ∈ P | e, e′ abstractors, ι_{P} (e) > ι_{P} (e′), π_{P [e,e′]}(e) < π_{P [e,e′]}(e′)}|

+|{(e, e′) ∈ P | e, e′ applicators, ι_{P} (e) > ι_{P} (e′), π_{P [e,e′]}(e) > π_{P [e,e′]}(e′)}|)

where P [e, e′] is the sub-spine extracted from P between e an e′ (included). When one of the π’s is not defined, the inequality is considered false.

Now we must prove that this mesure, as lexicographical ordering, decreases.

For the first term this is easy: only rules (3),(6),(7) and pseudo-reductions may change it, and they reduce it.

For the second one we must be more careful, because of the changing sub-spine in π. But we remark that ϕ(P) is strictly monotonous for any P, and by compositionality we can extend our sub-spine to the totality of the redex and get the same order. However, a special case arises when this is a pseudo-reduction implying e or e′ as locally associated. We can no longer use ϕ. Actually, this may increase the term. However since the first term increased, this does not matter.

Moreover, as needed, rules (1),(4) and (2),(5) decrease respectively the left and right side of the sum, while clearly not changing the other.

Since all rules decrease that mesure, which is well-founded, reordering terminates. □

Theorem 2 The reordering system is confluent modulo PRF equivalence.

PROOF We prove this property spine by spine, since reordering keeps entities on the same spine (cf. Lemma 1).

Since by Proposition 3 we know that reordering terminates, we just have to prove that for any spine taken modulo PRF equivalence, its order normal form is unique modulo PRF equivalence.

By Lemma 2 and Corrolary 4, we know that both apparent positions for free entities, and associations for associated ones, are invariant by reordering. We verify easily that they are invariant by PRF equivalence too.

Moreover Proposition 1 gives us the structure of order normal forms. First free abstractor and free applicator parts are entirely specified by there apparent positions, and the ordering on labels. Then PRF equivalence says that the order of locally associated pairs is irrelevant, and the numeric part of their labels too. Since we know by Lemma 1 that the symbolic part does not change, that specifies the associated part modulo PRF equivalence. Since all reordering rules respect variable dependencies, they are kept.

As a result order normal forms are completely specified, modulo PRF equivalence, by the original term. □

4.4 Confluence of β-reordering

Definition 12 (β-Reordering) A β-reordering step is a β-reduction step immediately followed by a stable reordering to order normal form.

Since stable reordering can reduce every time reordering reduces, and reordering is Noetherian and confluent modulo PRF-equivalence, this completely defines a reduction rule on the quotient of order-normal λ-terms modulo PRF-equivalence. The one-step β-reordering relation is denoted as →_{β↓}.

Not to worry about renaming problems during reordering, we will assume that all free variables and abstraction variables have distinct names.

For Definition 12 to stand we have to prove that PRF-equivalent order-normal expressions are still equivalent after β-reordering. This is immediate, since PRF-equivalence and β-reduction are orthogonal: β-reduction do not separate any association pair, and PRFequivalence do not separate any β-redex, nor change variable scoping.

This justifies us in the rest of this subsection, to consider no longer terms, but their equivalence classes modulo PRF equivalence.

From here on, the proof of β-reordering confluence follows the Martin-Löf-Tait scheme as in [14]. By contracting a β-redex, we mean applying the corresponding step of β-reduction.

Still, the definition of β-redex has to be changed to let us work with equivalence classes: with the classical one, two redexes could be different and mutually included in one another.

Definition 13 (β-redex) In (λ_{p}x.(z ⊙ P)) _{p} only are included in the β-redex the associated pair, z and the entitities of P selected by the following process.

1. We start with V_{0} = {x}, and parse from the right.

2. If the n^{th} entity is an applicator _{q} N, and F V (N) contains variables in V_{n−1}, then we select it. Otherwise it is not part of the redex.

3. If the n^{th} entity is an abstractor ∨ q y, if it is associated in P with a selected applicator, then we select it and V_{n} = V_{n−1} ∪ {y}. Otherwise it is not part of the redex, and V_{n} = V_{n−1} \ {y}.

With this definition we get out of the redex all entities which could escape by a reordering (for abstractors), or be inserted by a reordering (for applicators).

As a result, this definition allows us to use any selective λ-term as a representative for the equivalence class of its order normal form modulo PRF equivalence: reordering does not modify such β-redexes.

We note M ↓ this equivalence class for a selective λ-term M. However we will abbreviate it in simply M for the rest of this subsection (except Lemma 3, Corollary 5 and Proposition 4 ), and work modulo reordering, proving in Lemmas 3,4,6 and Corollary 5 that this does not give us wrong intuitions on the structure of reductions: Lemmas 3 and Corollary 5 proves that substitution and β-reordering commute with full reordering, Lemma 4 that we can still induce on the structure of terms before reordering, and Lemma 6, enunciated later, a property about postponment of reductions.

Lemma 3 (Substitution) Reordering before or after a substitution does not change the result.

[N/x]M = [N/x]M ↓

PROOF We shall only consider whether heads of spines will be substituted or not. In each spine where it is substituted, we can conclude by confluence of reordering (reordering the outer part of the spine and then introducing the end is equivalent to reordering directly the whole spine). In spines where it is not, there is no problem since they are left unmodified. □

Lemma 4 (Induction)  \begin{matrix}M →_{β↓} & M′ ⇒ & λ_{p}x.M →_{β↓} & λ_{p}x.M′ \\ M →_{β↓} & M′ ⇒ & M _{p} N →_{β↓} & M′ _{p} N \\ N →_{β↓} & N′ ⇒ & M _{p} N →_{β↓} & M _{p} N′ \end{matrix}

PROOF

1. M = λ_{p_{1}}x_{1} … λ_{p_{n}}x_{n}.M_{1}, with M_{1} an order-normal form starting with an abstraction and p_{i} ≤ p_{i+1}. So that M′ = λ_{p_{1}}x_{1} … λ_{p_{n}}x_{n}.M′_{1}, with M′_{1} any order-normal expression, and M_{1} →_{β↓} M′_{1}. Hence

λ_{p}x.M =  λ_{p_{1}}x_{1} … λ_{p′}x … λ_{p_{n}}x_{n}.M_{1}
→_{β↓} λ_{p_{1}}x_{1} … λ_{p′}x … λ_{p_{n}}x_{n}.M′_{1}
=  λ_{p}x.M′

2. If _{p} N is associated then

M _{p} N =  (λ_{p_{1}}x_{1} … λ_{p′}x … λ_{p_{n}}x_{n}.M_{1}) _{p} N M_{1} as before, p_{i} ≤ p_{i+1}
=  λ_{p_{1}}x_{1} … λ_{p_{n}}x_{n}.((λ_{p′}x.M_{1}) _{p′} N) (order normal form)
→_{β↓} λ_{p_{1}}x_{1} … λ_{p_{n}}x_{n}.((λ_{p′}x.M′_{1}) _{p′} N)
=  (λ_{p_{1}}x_{1} … λ_{p′}x … λ_{p_{n}}x_{n}.M′_{1}) _{p} N
=  M′ _{p} N

If _{p} N is not associated then

M _{p} N =  (λ_{p_{1}}x_{1} … λ_{p_{n}}x_{n}.(z _{q_{1}} N … _{q_{m}} N_{m} ⊙ A)) _{p} N
=  λ_{p_{1}}x_{1} … λ_{p′_{n}}x_{n}.(z _{q_{1}} N … _{p′} N _{q′_{m}} N_{m} ⊙ A)
→_{β↓} λ_{p_{1}}x_{1} … λ_{p′_{n}}x_{n}.(Z′ _{q_{1}} N′_{1} … _{p′} N … _{q′_{m}} N′_{m} ⊙ A′)
=  (λ_{p_{1}}x_{1} … λ_{p_{n}}x_{n}.(Z′ _{q_{1}} N′_{1} … _{q_{m}} N′_{m} ⊙ A′)) _{p} N
=  M′ _{p} N

where A is the entity associations, A′ the reduced associations, and N is unchanged because all its variables are free.

3. By independence of spines.

□

Corollary 5 (β-reduction) Reordering before β-reduction does not change the order-normal form modulo PRF quivalence.

M →_{R} N ∧ M ↓→_{R} N′ ⇒ N ↓ = N′ ↓

where R is the redex reduced in →_{R}.

PROOF Let M_{\R} be the context M without R, that is M_{\R}[R] = M. By Lemma 4, R →_{β} R′ implies M_{\R}[R] ↓→_{β↓} M_{\R}[R′] ↓. But M_{\R}[R′] = N and M_{\R}[R′] ↓= N′ ↓, so the equality stands. □

Definition 14 (Residuals) Let R, S be β-redexes in a selective λ-term P. When R is contracted, let P change to P’. The residuals of S with respect to R are redexes in P’, defined as follows:

• R, S are non-overlapping parts of P. Then contracting R leaves S unchanged. This unchanged S in P′ is called the residual of S.

• R = S. Then contracting R is the same as contracting S. We say S has no residual in P′.

• R is part of S and R ≠ S. Then S has form (λ_{p}x.M) _{p} N and R is in M or in N. Contracting R changes M to M′ or N to N′, and S to (λ_{p}x.M′) _{p} N or (λ_{p}x.M) _{p} N′; this is the residual of S.

• S is part of R and S ≠ R. Then R has form (λ_{p}x.M) _{p} N and S is in M or in N. If S is in M, then S′ = [x/N]S. If S is in N, then there are as many residuals S′ of S as there were occurences of x in M, and S′ = S.

This case will not happen in our proof.

• R ≠ S, but R is not part of S and S is not part of R. We can handle this as R part of S and R in M, by PRF equivalence.

We can read this definition in two ways. If we are working with only β-reduction, without PRF equivalence nor reordering, then we adopt the usual definition of β-redex and do not need the last case.

Otherwise, we read all terms as non order-normal representatives of order-normal equivalence classes, and use the new definition of β-redex.

Note that anyway, in the first three cases (and the last too, since this is the third) S has at most one residual.

Before going on with our proof about β-reordering, we enunciate finite developments for β alone.

Proposition 4 (finite developments) Let R be a set of β-redexes in M. Then reducing, in any order, of all residuals of redexes in R terminates and converges to the same M′.

PROOF Since we use only β-reduction, finite developments for classical lambda calculus does apply. □

Now we are back to our proof about β-reordering.

Let R_{1}, …, R_{n} (n ≥ 0) be redexes in a term P. An R_{i} is called minimal iff it properly contains no other R_{j} (using our new definition of β-redex).

A minimal complete development (MCD) of {R_{1}, …, R_{n}} in P is a sequence of contractions on P performed as follows:

• First, contract any minimal R_{i} (say i = 1 for convenience). This leaves at most n − 1 residuals R′_{2}, …, R′_{n}, of R_{2}, …, R_{n}.

• Then, contract any minimal R′_{j}. This leaves at most n − 2 residuals.

• Repeat the above two steps until no residuals are left.

Note that this process is non-deterministic, and thus there are more than one such sequence of contractions.

Definition 15 (MCD) Let P be a term as above, and Q a term. We write P ▷_{mcd} Q iff Q is obtained from P by minimal complete development of the set {R_{1}, …, R_{n}}.

Note that if M ▷_{mcd} M′ and N ▷_{mcd} N′, then M _{p} N ▷_{mcd} M′ _{p} N′. (cf. , Lemma 4)

Lemma 5 If M ▷_{mcd} M′ and N ▷_{mcd} N′, then

[N/x]M ▷_{mcd} [N′/x]M′.

PROOF We proceed by induction on M. Let R_{1}, …, R_{n} be the redexes developed in the given MCD of M.

1. M = x. Then n=0 and M′ = x, so

[N/x]M = N ▷_{mcd} N′ = [N′/x]M′.

2. x ∉ FV(M). Then x ∉ FV(M′), so

[N/x]M = M ▷_{mcd} M′ = [N′/x]M′.

3. M = λ_{p}y.M_{1}. Then each β-redex in M is in M_{1}, so M′ has form λ_{p}y.M′_{1} where M_{1} ▷_{mcd} M′_{1}. Hence

[N/x]M =  [N/x](λ_{p}y.M_{1}) Lemma 3
=  λ_{p}y.[N/x]M_{1} since y ∉ FV(xN)
▷_{mcd} λ_{p}y.[N′/x]M′_{1} by induction hypothesis
=  [N′/x]M′  since y ∉ FV(xN′)

4. M = M_{1} _{p} M_{2} and each R_{i} is in M_{1} or M_{2}. Then M′ has form M′_{1} _{p} M′_{2} where M_{j} ▷_{mcd} M′_{j} for j = 1, 2. Hence

[N/x]M =  ([N/x]M_{1}) _{p} ([N/x]M_{2}) Lemma 3
▷_{mcd} ([N′/x]M′_{1}) _{p} ([N′/x]M′_{2}) by ind. and note above
=  [N′/x]M′.

5. M = (λ_{p}y.L) _{p} Q and one R_{i}, say R_{1}, is M itself and is contracted last, and the others are in L or Q. (If it is not contracted last then we have M = (λ_{q}z.K) _{q} O too, and this one is contracted last). Hence the MCD has form

M = (λ_{p}y.L) _{p} Q ▷_{mcd} (λ_{p}y.L′) _{p} Q′ (L ▷_{mcd} L′, Q ▷_{mcd} Q′)
→_{β↓} [Q′/y]L′
=  M′.

By induction hypothesis we have MCD’s of [N/x]L and [N/x]Q. Hence

[N/x]M =  (λ_{p}y.[N/x]L) _{p} ([N/x]Q)  since y ∉ FV(xN)
▷_{mcd} (λ_{p}y.[N′/x]L′) _{p} ([N′/x]Q′) induction
→_{β↓} [([N′/x]Q′)/y][N′/x]L′
=  [N′/x][Q′/y]L′
=  [N′/x]M′.

This reduction is an MCD, as required.

□

The following lemma is necessary because we are working on order normal forms: it is unclear wether (λ_{p}x.M) _{p} N will still be most external after reordering, but thanks to our definition of redex, it cannot be included in any other, so can be reduced last.

Lemma 6 (Proof induction) If there is an MCD

P = (λ_{p}x.M) _{p} N →^{∗}_{β↓} (λ_{p}x.M′) _{p} N′
→_{β↓} [N′/x]M′  = Q
→^{∗}_{β↓} Q′

then there is an MCD

\begin{aligned}P = & (λ_{p}x.M) _{p} N & →^{∗}_{β↓} & (λ_{p}x.M′′) _{p} N′′ \\ & & →_{β↓} & [N′′/x]M′′ & = Q′ \end{aligned}

That is, reduction of a potentially most external redex may be done last.

PROOF Since this is an MCD, new reductions do not apply on redexes created in the substitution, and Q′ has form [N′′/x]M′′.

We should then just show that there are MCD’s M ▷_{mcd} M′′ and N ▷_{mcd} N′′, which proves that (λ_{p}x.M) _{p} N ▷_{mcd} [N′′/x]M, by Lemma 5.

Each step of the original MCD after [N′/x]M′ only modifies either N′ or M′ at a time. So that we can write M′ →_{β↓} M_{1} →_{β↓} … →_{β↓} M′′, and since it is an MCD, M′ ▷_{mcd} M′′. Similarly N′ ▷_{mcd} N′′. And all the reductions performed are on the external level, that is permutable with our reduction on p in an MCD. So that M ▷_{mcd} M′′ and N ▷_{mcd} N′′. □

Lemma 7 (confluence of MCD) If P ▷_{mcd} A and P ▷_{mcd} B, then there exists T such that A ▷_{mcd} T and B ▷_{mcd} T.

PROOF By induction on P.

1. P = x. Then A = B = P. Choose T = P.

2. P = λ_{p}x.P_{1}. Then all β-redexes in P are in P_{1}, and

A = λ_{p}x.A_{1}, B = λ_{p}x.B_{1},

where P_{1} ▷_{mcd} A_{1} and P_{1} ▷_{mcd} B_{1}. By induction hypothesis there is a T_{1} such that

A_{1} ▷_{mcd} T_{1}, B_{1} ▷_{mcd} T_{1}.

Choose T = λ_{p}x.T_{1}.

3. P = P_{1} _{p} P_{2} and all the redexes developed in the MCD’s are in P_{1}, P_{2}. Then the induction hypothesis gives us T_{1}, T_{2}, and we choose T_{1} _{p} T_{2}.

4. P = (λ_{p}x.M) _{p} N and just one of the given MCD’s involves contracting P ’s residual; say it is P ▷_{mcd} A. Then, by Lemma 6, there is an MCD with form

P =  (λ_{p}x.M) _{p} N
▷_{mcd} (λ_{p}x.M′) _{p} N′ (M ▷_{mcd} M′, N ▷_{mcd} N′)
→_{β↓} [N′/x]M′
=  A.

And the other MCD has form

P =  (λ_{p}x.M) _{p} N
▷_{mcd} (λ_{p}x.M′′) _{p} N′′ (M ▷_{mcd} M′′, N ▷_{mcd} N′′)
=  B.

The induction hypothesis applied to M, N gives us M^{+}, N^{+} such that

\begin{matrix}M′ ▷_{mcd} M^{+}, & M′′ ▷_{mcd} M^{+}; \\ N′ ▷_{mcd} N^{+}, & N′′ ▷_{mcd} N^{+}. \end{matrix}

Choose T = [N^{+}/x]M^{+}. Then there is an MCD from A to T, thus, by Lemma 5

A = [N′/x]M′ ▷_{mcd} [N^{+}/x]M^{+}.

And for B,

B =  (λ_{p}x.M′′) _{p} N′′
▷_{mcd} (λ_{p}x.M^{+}) _{p} N^{+}
→_{β↓} [N^{+}/x]M^{+}

5. P = (λ_{p}x.M) _{p} N and both the given MCD’s contract P ’s residual. Then (Lemma 6) we can give these MCD’s form

P =  (λ_{p}x.M) _{p} N  P =  (λ_{p}x.M) _{p} N
▷_{mcd} (λ_{p}x.M′) _{p} N′  ▷_{mcd} (λ_{p}x.M′′) _{p} N′′
→_{β↓} [N′/x]M′  →_{β↓} [N′′/x]M′′
=  A,  =  B.

Apply the induction hypothesis to M and N in case 4, and choose T = [N^{+}/x]M^{+}. Then Lemma 5 gives the result, as above.

□

Theorem 3 β-reordering is confluent modulo PRF equivalence.

P →^{∗}_{β↓} M, P →^{∗}_{β↓} N ⇒ (∃T) M →^{∗}_{β↓} T, N →^{∗}_{β↓} T.

PROOF By induction on the length of the reduction from P to M, it is enough to prove

P →_{β↓}, P →^{∗}_{β↓} N ⇒ (∃T) M →^{∗}_{β↓} T, N →^{∗}_{β↓} T.

Since a single β-reordering step is an MCD, it is sufficient to have

P ▷_{mcd} M, P →^{∗}_{β↓} N ⇒ (∃T) M →^{∗}_{β↓} T, N ▷_{mcd} T.

which is shown by an induction on the number of β-steps from P to N. □

4.5 Confluence of selective λ-calculus

In this section, → (or →_{λ}) denotes the union of β-reduction and ordering rules (label-selective λ-calculus), and →_{ω} is the union of all rules (label-parallel system). We will now no longer consider terms modulo PRF equivalence, except in the β-reordering diamond of Figure 4.

Definition 16 (Normalized reduction) For each label-parallel reduction M_{0} →_{ω} M_{1} →_{ω} … →_{ω} M_{n} we define its normalized reduction N_{0} →_{β↓} N →_{β↓} … →_{β↓} N_{n} by taking for each N_{i} the order-normal form M_{i} ↓.

Proposition 5 Normalized reduction is a β-reordering.

PROOF We should verify that we really obtain a β-reordering by this process.

We can first remark that, since we have Corollary 4, all β-redexes in M_{i} are still β-redexes in N_{i}.

If M_{i} → M_{i+1} is a reordering step, then N_{i} = N_{i+1}. Else, M_{i} → M_{i+1} is a β-step, and we should show N_{i} →_{β↓} N_{i+1}. From our remark, we have N_{i} →_{β↓} N′_{i}, reducing the same redex. We will in fact construct two parallel reorderings of M_{i} and M_{i+1}. First, a stable reordering of M_{i}, from M_{i}^{0} = M_{i} to M_{i}^{k} = N_{i}. With such a reordering, we have at each step M_{i}^{j} → M_{i}^{′j} by a β-step. Then we define a reordering of M_{i+1} going through all M_{i}^{′j}’s. By definition M_{i}^{j} → M_{i}^{j+1} does not separate two locally associated entities. There are four cases to consider:

1. If it is external to the reduced redex, then we can do the same reduction M_{i}^{′j} →_{c} M_{i}^{′j+1}.

2. If it is internal, the β-reduction may only substitute some variables, but the reduction can still be applied. M_{i}^{′j} →_{c} M_{i}^{′j+1}.

3. If it was an (a) or (b) reordering step over the redex, then it is superfluous after reduction, M_{i}^{′j} = M_{i}^{′j+1}.

Finally we can go from M_{i}^{′k} to N′_{i} by a stable reordering. By confluence it gives N′_{i} = N_{i+1}, and the normalized reduction is correctly constructed. □

Theorem 4 (Confluence of label-parallel reduction) The label-parallel system is confluent. Moreover, the converging reductions are stable,

P →^{∗}_{ω} M, P →^{∗}_{ω} N ⇒ (∃T) M ▷_{ωstb} T, N ▷_{ωstb} T.

PROOF We have

\begin{aligned}P & →_{ω} M_{1} & →_{ω} … →_{ω} M_{m} & = M, \\ P & →_{ω} N_{1} & →_{ω} … →_{ω} N_{n} & = N. \end{aligned}

So that we obtain normalized reductions

\begin{aligned}P′ →_{β↓} M′_{1} & →_{β↓} … →_{β↓} M′_{m}, \\ P′ →_{β↓} N′_{1} & →_{β↓} … →_{β↓} N′_{n}. \end{aligned}

And by confluence of β-reordering modulo PRF-equivalence,

\begin{aligned}M′_{m} & = R_{0} & →_{β↓} R_{1} & →_{β↓} … →_{β↓} R_{r} & = T, \\ N′_{n} & = S_{0} & →_{β↓} S_{1} & →_{β↓} … →_{β↓} S_{s} & = T′. \end{aligned}

with T and T′ PRF-equivalent.

Since normalized (β-reordering) reductions are confluent, and all steps used here are in the stable label-parallel system, the label-parallel system is confluent modulo PRF equivalence, using stable reductions.

We can then reduce all the β-redexes present in the resulting term, thanks to Proposition 4, and obtain full confluence. All differences masked by PRF equivalence are contained in the redexes, and since in this last stage we do not use pseudo-reduction, we do not create new differences. □

[figure: T; M; N; T; β; β; β; β; β; β; P; P’; N; N’; M; M’; T’; T; β ↓; β ↓; β ↓; β ↓; λ; λ; β; ↓; ↓; ↓; λ; λ; λ; λ; β; β; R’; S’]

Figure 4: Schematic confluence of label-selective λ-calculus

Theorem 1 (Confluence of label-selective λ-calculus) The label-selective λ-calculus is confluent. That is,

P →^{∗} M, P →^{∗} N ⇒ (∃T) M →^{∗} T, N →^{∗} T.

PROOF By Theorem 4,

\begin{aligned}M & = R_{0} & →_{ωstb} R_{1} & →_{ωstb} … →_{ωstb} R_{r} & = T′, \\ N & = S_{0} & →_{ωstb} S_{1} & →_{ωstb} … →_{ωstb} S_{s} & = T′. \end{aligned}

But the absence of pseudo-reduction rules makes it impossible to follow these paths. Each time we have a (a) or (b) reduction, we should have a β-reduction in place.

We first define the set B_{k} of all residuals of β-redexes which where implied in an (a) or (b) pseudo-reduction. That is B_{0} = ∅, B_{k+1} = {residuals of B_{k} in R_{k} → R_{k+1}} if this was not a pseudo-reduction, B_{k+1} = {residuals of B_{k} in R_{k} → R_{k+1}} ∪ {the skipped β-redex} if it was. Since reductions are stable, residuals do not disappear.

Then we define R′_{k} as R_{k} where all redexes in B_{k} were reduced; Proposition 4 makes this definition correct. We have R′_{k} →^{∗} R′_{k+1} where → is either the original R_{k} → R_{k+1} step applied on all its residuals, either →_{β} applied on B_{k+1} \ B_{k} if it was a pseudo-reduction.

We define similarly S′_{k}.

We will finally have two expressions, coming from T′ by β-reduction only. The number of β-reductions done may differ, but reducing all the redexes which were present in T′ is enough, since the B_{k}’s contain only residuals of β-redexes. That is,

\begin{matrix}M & →^{∗} R′_{0} & →^{∗} R′_{1} & →^{∗} … →^{∗} R′_{r} & →^{∗}_{β} T, \\ N & →^{∗} S′_{0} & →^{∗} S′_{1} & →^{∗} … →^{∗} S′_{s} & →^{∗}_{β} T. \end{matrix}

So that finally, M →^{∗} T and N →^{∗} T. □

Figure 4 shows a schematic diagram of the process.

Corollary 1,2,3 Symbolic, numeric and flat selective λ-calculi are confluent.

PROOF For the numerical case, just take S with only one element.

For symbols, you just add the index 1 to all of them. No rule increases the index, and since all index are equal, no rule recreases them. As a consquence any reduction on a symbolic selective λ-term in selective λ-calculus uses only steps of the symbolic calculus, and we get confluence by injection.

For the flat case, take S′ = S ˙∪{ϵ}, and define ϵ to be the least element of S′. On the S part we can apply the argument for symbols, and get indexes on the extra symbol ϵ. Rules (1’), (2’), (3’) are ensured by the extended order. □

5 Conclusion and further work

Label-selective λ-calculus offers the advantage of realizing directly a more complete isomorphism of Cartesian products and function applications. An immediate consequence is a more convenient notation, and a more efficient, indeed concurrent, manner to extract arguments out of order.

Beyond the bare calculus, we have started studying a typed version of our calculus [13]. There, we propose a simply typed version of this calculus, and show that it extends to second order and polymorphic typing. For this last one there exists a most generic type, and we give the algorithm to find it.

A topic for further work along this idea is, of course compilation. As mentioned in the first section, we plan to extend the stack-based model of execution of λ-calculus with our label-selection scheme to realize efficient access to arguments regardless of position label. We have already adapted the calculus of explicit substitutions [1], as are currently working on a compiling scheme for label-selective λ-calculus based on it.

Also, we plan to study the work of Ohori [20] to elucidate the gains that this may have in the compilation of records. As for semantics, we have initiated work on a typed version of label-selective λ-calculus and a framework of models for it.

Based on our remarks of Section 3.3, we have formulated and are studying several concurrent calculi extending label-selective λ-calculus towards full concurrency [3], including the provision for computable channel names. One of the gains expected is that λ-calculus will need not be encoded as in [18], but directly embedded as syntactic identity.

Another application of this insight, in a pure confluent calculus, is studied as a new approach to state handling in the lambda calculus [10, 11]. In a composition-based system, similar in this respect to Categorical Combinatory Logic [7], we use labels as a way to select or modify directly the part of the state we are interested in. Some even stronger extension of the notion of currying towards binary relations can be done on this basis, with a symmetric calculus of transformations [12].

Finally, the real goal that has motivated our working out this calculus has been to use it for a useful generalization of object-oriented style of message passing. Method invocation based on the type of the first argument of a call can be elegantly explained by seeing a method definition in a class as a curried form with respect to the object instance of the class. Labelselective currying can thus reinstate the lost symmetry by distributing one partially-applied form for each arguments of the class of a method. As a result, message-passing can be used on any argument of a call, making labels act as channels. Our confluence result guarantees that the choice of channel does not matter. We plan to pursue this insight and investigate all its ramifications.

References

[1] Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. Journal of Functional Programming, Vol. 1, No. 4, pp. 375–416, October 1991.

[2] 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, pp. 24–40, Bombay, India, 1993. Springer-Verlag LNCS 761.

[3] Hassan Aït-Kaci and Kathleen Milsted. Concurrent label-selective λ-calculus. PRL research report, Digital Equipment Corporation, Paris Research Laboratory, Rueil-Malmaison, France, forthcoming.

[4] Hassan Aït-Kaci and Andreas Podelski. Towards a meaning of LIFE. Journal of Logic Programming, Vol. 16, No. 3&4, pp. 195–234, July-August 1993.

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

[6] N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation. Indag. Math., Vol. 34, pp. 381–392, 1972.

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

[8] Laurent Dami. HOP: Hierarchical objects with ports. In D. Tsichritzis, editor, Object Frameworks. Technical report, University of Geneva, 1992.

[9] Laurent Dami. Software Composition: Towards an Integration of Functional and Object-Oriented Approaches. PhD thesis, Université de Genève, Faculté des Sciences Économiques et Sociales, Switzerland, 1994.

[10] Jacques Garrigue. Transformation calculus and its typing. In Proc. of the workshop on Type Theory and its Applications to Computer Systems, pp. 34–45. Kyoto University RIMS Lecture Notes 851, August 1993.

[11] Jacques Garrigue. The transformation calculus. Technical Report 94-09, University of Tokyo, Department of Information Science, April 1994.

[12] Jacques Garrigue. Label-Selective Lambda-Calculi and Transformation Calculi. PhD thesis, University of Tokyo, Department of Information Science, March 1995.

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

[14] J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators and λ-Calculus, volume 1 of London Mathematical Society Student Texts. Cambridge University Press, 1986.

[15] Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, Vol. 27, No. 4, pp. 797–821, October 1980.

[16] Peter J. Landin. The mechanical evaluation of expressions. Computer Journal, Vol. 6, No. 4, pp. 308–320, 1964.

[17] Henry Ledgard. ADA : An Introduction, Ada Reference Manual (July 1980). Springer-Verlag, 1981.

[18] Robin Milner. Functions as processes. Rapport de Recherche 1154, INRIA, Rocquencourt, France, February 1990.

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

[20] Atsushi Ohori. A compilation method for ML-style polymorphic records. In Proc. ACM Symposium on Principles of Programming Languages, pp. 154–165, 1992.

[21] Guy L. Steele. Common LISP : The Language. Digital Press, 1984.