Modified realizability toposes and strong normalization proofs

Abstract

This paper is motivated by the discovery that an appropriate quotient SN. of the strongly normalising untyped λ*-terms (where * is just a formal constant) forms a partial applicative structure with the inherent application operation. The quotient structure satisfies all but one of the axioms of a partial combinatory algebra (PCA). We call snell partial applicative structures condstwnally partial combmalory algebras (C-PCA). Kemarkably, an arbitrary right-absorplive C-PCA gives rise to a lripos provided the underlying intuitionistic predicate logic is given an interpretation in the style of Kreisel’s modified realizabdilg, as opposed to the standard Kleene-style realizability. Starting from an arbitrary right-absorptive C-PCA U, the tripos-to-topos construction due to Hyland et al. can then be carried out to build a modified realizabilily lopos TOPm(U) of non-standard sets equipped with an equality predicate. Church’s Thesis is internally valid in TOPm(K1) (where the PCA K1 is “Kleene’s first model” of natural numbers) but not Markov’s Principle. There is a topos inclusion of SET -the “classical” topos of sets - into TOPm(U); the image of the inclusion is just sheaves for the -topology. Separated objects of the -topology are characterized. We identify the appropriate notion of PERS (partial equivalence relations) in the modified realizahility setting and state its completeness properties. The topos TOPm(U) has enough completeness property to provide a category-theoretic semantics for a family of higher type theories which include Girard’s System F and the Calculus of Constructions due to Coquand and Huet. As an important application, by interpreting type theories in the topos TOPm(SN*), a clean semantic explanation of the Tail-Girard style strong normalization argmnent is obtained. We illustrate how a strong normalization proof for an impredicative and dependent type theory may be assembled from two general “stripping arguments” in the framework of the topos TOPm(SN*). This opens up the possibility of a “generic” strong normalization argument for an interesting class of type theories.