Technical Reports

The ICICS/CS Reading Room

UBC CS TR-83-03 Summary

Numeration Models of $\lambda$-Calculus, April 1983 K and Akira a

Models of $\lambda$-calculus have been studied by Church [2] and Scott [7]. In these studies, finding solutions to the isomorphic equations \(S \approx [S \rightarrow S] \) where \( [S \rightarrow S] \) is a certain set of functions from $S$ to $S$ is the main issue. In this paper, we present an example of such solutions which fails to be a model of $\lambda$-calculus. This example indicates the necessity of careful consideration of the syntax of $\lambda$-calculus, especially for the study of constructive models of $\lambda$-calculus. Taking this into account, we axiomatically show when a numeration of Er\u{s}ov [3] forms a model of $\lambda$-calculus. This serves as a general framework for countable models of $\lambda$-calculus. Various examples of such numerations are studied. An algebraic characterization of this class of numerations is also given.

If you have any questions or comments regarding this page please send mail to