Numeration Models of λ-Calculus

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.