Details

Autor(en) / Beteiligte

• Aït-Kaci, Hassan
• Garrigue, Jacques

Titel

Label-selective λ-calculus syntax and confluence

Ist Teil von

• Theoretical computer science, 1995-11, Vol.151 (2), p.353-383

Ort / Verlag

Amsterdam: Elsevier B.V

Erscheinungsjahr

1995

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• 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 λ-caculus is confluent. In other words, argument selection and reduction commute.