Rewriting modulo in Deduction modulo

TL;DR

This paper extends termination results for rewriting in the Calculus of Algebraic Constructions to rewriting modulo equations, ensuring termination under conditions like finiteness, linearity, and syntactic constraints, including common algebraic equations.

Contribution

It generalizes previous termination results to rewriting modulo equations, introducing conditions that handle equations like associativity and commutativity.

Findings

Termination is preserved when equations are finite, linear, and satisfy computable closure.

Includes common algebraic equations like associativity and commutativity.

Provides an original approach to termination modulo equations.

Abstract

We study the termination of rewriting modulo a set of equations in the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. In a previous work, we defined general syntactic conditions based on the notion of computable closure for ensuring the termination of the combination of rewriting and beta-reduction. Here, we show that this result is preserved when considering rewriting modulo a set of equations if the equivalence classes generated by these equations are finite, the equations are linear and satisfy general syntactic conditions also based on the notion of computable closure. This includes equations like associativity and commutativity, and provides an original treatment of termination modulo equations.