Equational Theories and Validity for Logically Constrained Term Rewriting (Full Version)

TL;DR

This paper explores the semantics of logically constrained term rewriting by defining constrained equations, establishing validity, and providing an algebraic semantics to determine validity and invalidity within constrained theories.

Contribution

It introduces a semantic framework for logically constrained term rewriting, including validity notions, a sound inference system, and an algebraic semantics for consistency analysis.

Findings

Defined constrained equations and validity based on constrained theories

Constructed a sound inference system for validity proof

Developed an algebraic semantics for invalidity and consistency

Abstract

Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity analysis and confluence analysis for logically constrained term rewriting, these works solely focus on the syntactic side of the formalism lacking detailed investigations on semantics. In this paper, we investigate a semantic side of logically constrained term rewriting. To this end, we first define constrained equations, constrained equational theories and validity of the former based on the latter. After presenting the relationship of validity and conversion of rewriting, we then construct a sound inference system to prove validity of constrained equations in constrained equational theories. Finally, we give an algebraic semantics, which enables one to establish invalidity of constrained equations in constrained equational theories. This algebraic semantics derive a new notion of consistency for constrained equational theories.