Termination of rewrite relations on λ-terms based on Girard's notion of reducibility. F. Blanqui. To appear in Theoretical Computer Science, 47 pages, 2015.

In this paper, we show how to extend the notion of reducibility or computability introduced by Girard for proving the termination of β-reduction in the polymorphic λ-calculus, to prove the termination of various kinds of rewrite relations on λ-terms, including rewriting modulo some equational theory and rewriting with matching modulo βη, by using the notion of computability closure. This provides a powerful termination criterion for various higher-order rewriting frameworks, including Klop's Combinatory Reductions Systems with simple types and Nipkow's Higher-order Rewrite Systems.