Reduction system for extensional lambda-mu calculus. (English) Zbl 1417.03133

Nakazawa, Koji; Nagai, Tomoharu

Dowek, Gilles (ed.), Rewriting and typed lambda calculi. Joint international conference, RTA-TLCA 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8560, 349-363 (2014).

Summary: The \(\Lambda \mu \)-calculus is an extension of Parigot’s \(\lambda \mu \)-calculus. For the untyped \(\Lambda \mu \)-calculus, Saurin proved some fundamental properties such as the standardization and the separation theorem. Nakazawa and Katsumata gave extensional models, called stream models, in which terms are represented as functions on streams. This paper introduces a conservative extension of the \(\Lambda \mu \)-calculus, called \(\Lambda \mu _\mathsf{cons }\), from which the open term model is straightforwardly constructed as a stream model, and for which we can define a reduction system satisfying several fundamental properties such as confluence, subject reduction, and strong normalization.
For the entire collection see [Zbl 1291.68017].

MSC:

03B40	Combinatory logic and lambda calculus
68Q05	Models of computation (Turing machines, etc.) (MSC2010)