Realizability, Covers, and Sheaves I. Application to the Simply-Typed Lambda-Calculus

We present a general method for proving properties of typed λ-terms. This method is obtained by introducing a semantic notion of realizability which uses the notion of a cover algebra (as in abstract sheaf theory, a cover algebra being a Grothendieck topology in the case of a preorder). For this, we introduce a new class of semantic structures equipped with preorders, called pre-applicative structures. These structures need not be extensional. In this framework, a general realizability theorem can be shown. Kleene's recursive realizability and a variant of Kreisel's modified realizability both fit into this framework. Applying this theorem to the special case of the term model, yields a general theorem for proving properties of typed λ-terms, in particular, strong normalization and confluence. This approach clarifies the reducibility method by showing that the closure conditions on candidates of reducibility can be viewed as sheaf conditions. Part I of this paper applies the above approach to the simply-typed λ-calculus (with types →, ×, +, and ⊥). Part II of this paper deals with the second-order (polymorphic) λ-calculus (with types → and ∀).