Termination of rewrite relations on λ-terms based on Girard's notion of reducibility. F. Blanqui. TCS 611, 37 pages, 2016.

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.

Erratum

p. 53, l. 25 (stable subterm). After "FV(t)⊆FV(u)", add: " and no bound variable of u belongs to FV(t)".

p. 56, l. -12. Replace "Sat: Tait' set of saturated sets [Tai75]" by "Sat: Mitchell' set of type sets relative to SN [Mit86] (called saturated in [Gal90])", with [Mit86] J. Mitchell. A type-inference approach to reduction properties and semantics of polymorphic expressions (summary). In the proceedings of the ACM Symposium on Lisp and Fonctional Programming, 1986.

p. 58, l. -15. Replace "Πx∈ABx = P(Σx∈ABx)" by "Πx∈ABx ⊆ P(Σx∈ABx)".


Statcounter W3C Validator Last updated on 16 May 2018. Come back to main page.