page 1  (17 pages)
2to next section

Label-Selective >=-Calculus

Syntax and Confluencey

Hassan A??t-Kaci1 and Jacques Garrigue2

1 Digital Equipment Corporation, Paris Research Laboratory
85 Avenue Victor Hugo, 92500 Rueil-Malmaison, France
2 Department of Information Science, The University of Tokyo
7-3-1 Hongo, Bunkyo-ku, Tokyo 113, Japan

Abstract. We introduce an extension of >=-calculus, called label-selective >=- calculus, in which arguments of functions are selected by labels. The set of labels includes numeric positions as well as symbolic keywords. While the latter enjoy free commutation, the former must comply with relative precedence in order to preserve currying. This extension of >=-calculus is conservative in the sense that when the set of labels is the singleton f1g, it coincides with >=-calculus. The main result of this paper is that the label-selective >=-calculus is confluent. In other words, argument selection and reduction commute.

Keywords. >=-Calculus, record calculus, concurrency, communication.

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 [16, 12, 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). Even if currying is supported and the situation reduced to numeric positions, it is allowed strictly in a 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.

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 ss1 and ss2 were

y This is a short version of [2]. We have systematically omitted all proofs. Please refer there for details of all the proofs.

used explicitly instead of the implicit 1st and 2nd of the ? notation, then instead of A?B we would write ss1 )A? ss2 )B. Thus, allowing this explicit product expression makes Cartesian product commutative explicitly, as opposed to up to isomorphism." Indeed, it becomes obvious that:3 ss1 )A? ss2 )B ' ss2 )B? ss1 )A; and thus that: ss1 )A ! (ss2 )B ! C) ' ss2 )B ! (ss1 )A ! C):