Short version appeared in Proc. of the Conference on Foundations of Software Technology and Theoretical Computer Science, pages 24-40, Bombay, India, 1993. Springer-Verlag LNCS 761.
Abstract. We introduce an extension of lambda-calculus, called label-selective lambda-calculus, in which arguments of functions are selected by labels. The set of labels includes numeric postions 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 lambda-calculus is conservative in the sense that when the set of labels is the singleton {1}, it coincides with lambda-calculus. The main result of this paper is that the label-selective lambda-calculus is confluent. In other words, argument selection and reduction commute.
Keywords. Lambda-calculus, record calculus, concurrency, communication.
JG 2024.3.13