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

Abstract : 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.
Complete list of metadatas

https://hal.inria.fr/hal-01191693
Contributor : Frédéric Blanqui <>
Submitted on : Wednesday, September 2, 2015 - 1:04:57 PM
Last modification on : Friday, April 12, 2019 - 10:18:09 AM
Long-term archiving on : Wednesday, April 26, 2017 - 2:10:32 PM

Files

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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

Share

Metrics

Record views

403

Files downloads

240