Toward a General Rewriting-Based Framework for Reducibility
Colin Riba, Inria Sophia, Antipolis Médeterranée · HAL (Le Centre pour la Communication Scientifique Directe) · 2008
Reducibility is a powerful proof method which applies to various properties of typed terms in different type systems. For strong normalization, different variants are known, such as Girard’s reducibility candidates, Tait’s saturated sets and biorthogonals. They differ by the closure conditions imposed to types interpretations, called here reducibility families. This paper is about the computational and observational properties underlying untyped reducibility. Our starting point is the comparison of reducibility families w.r.t. their ability to handle rewriting, for which their possible stability by union plays an important role. Indeed, usual saturated sets are generally stable by union, but with rewriting it can be difficult to define a uniform notion of saturated sets. On the other hand, rewriting is more naturally taken into account by reducibility candidates, but they are not always stable by union. It seems that for a given rewrite relation, the stability by union of reducibility candidates should imply the ability to naturally define corresponding saturated sets. In this paper, we seek to devise a general framework in which the above claim can be substantiated. In particular,