Termination of rewrite relations on λ-terms based on Girard's notion of reducibility

Frédéric Blanqui (1)

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique

In this paper, we show how to extend the notion of reducibility 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.

Mots clés: types; rewriting; λ-calculus; termination; Girard's reducibility; rewriting modulo; matching modulo βη; patterns a la Miller

Domaines: Logique en informatique [cs.LO]; Logique [math.LO]

Frédéric Blanqui. Termination of rewrite relations on λ-terms based on Girard's notion of reducibility. Theoretical Computer Science, 2015, 611 (50-86), pp.37. ⟨10.1016/j.tcs.2015.07.045⟩. ⟨hal-01191693⟩