Extensional Models of Untyped Lambda-mu Calculus

TL;DR

This paper introduces novel mathematical models for the untyped Lambda-mu calculus, including stream models and stream combinatory algebras, establishing their properties and equivalences.

Contribution

It presents the first stream models and stream combinatory algebras for Lambda-mu calculus, along with a new combinatory calculus SCL.

Findings

Stream models extend lambda models to interpret terms as functions from streams.

Stream combinatory algebras characterize extensional equality in Lambda-mu calculus.

Stream models are algebraically characterized as a specific class of stream combinatory algebras.

Abstract

This paper proposes new mathematical models of the untyped Lambda-mu calculus. One is called the stream model, which is an extension of the lambda model, in which each term is interpreted as a function from streams to individual data. The other is called the stream combinatory algebra, which is an extension of the combinatory algebra, and it is proved that the extensional equality of the Lambda-mu calculus is equivalent to equality in stream combinatory algebras. In order to define the stream combinatory algebra, we introduce a combinatory calculus SCL, which is an abstraction-free system corresponding to the Lambda-mu calculus. Moreover, it is shown that stream models are algebraically characterized as a particular class of stream combinatory algebras.