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

DOI10.1016/J.TCS.2015.07.045MaRDI QIDQ896904zbMATHOpenAlexFDO

Publication date 15 December 2015

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1509.00649

types \(\lambda\)-calculus rewriting termination Girard's reducibility matching modulo \(\beta\eta\)rewriting modulo patterns à la Miller

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

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

l a m b d a

-calculus, to prove the termination of various kinds of rewrite relations on

l a m b d a

-terms, including rewriting modulo some equational theory and rewriting with matching modulo

e t a

, 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.

Recommendations

Cites work

Cited in

(7)

Describes a project that uses

Uses Software

This page was built for publication: Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q896904)