Reduction System for Extensional Lambda-mu Calculus

ABSTRACT. The Lambda-mu-calculus is an extension of Parigot’s lambda-mu-calculus, the untyped variant of which is proved by Saurin to satisfy some fundamental properties such as the standardization and the separation theorem. For the untyped Lambda-mu-calculus, Nakazawa and Katsumata gave extensional models, called stream models, which is a simple extension of the lambda models, and in which terms are represented as functions on streams. However, we cannot construct a term model from the Lambda-mu-calculus. This paper introduces an extension of the Lambda-mu-calculus, called Lambda-mu-cons, on which we can construct a term model as a stream model, and its reduction system satisfying confluence, subject reduction, and strong normalization.