Bounded Rewriting Induction for LCSTRSs

TL;DR

This paper introduces Bounded Rewriting Induction, an adaptation of Rewriting Induction for Logically Constrained Simply-typed Term Rewriting Systems that reduces termination constraints, enhancing its practical proof capabilities.

Contribution

The paper proposes Bounded RI, a novel method that minimizes termination requirements in rewriting induction for LCSTRSs, improving proof efficiency and applicability.

Findings

Reduces strong termination requirements in RI

Enhances proof capacity for LCSTRSs

Improves practical program verification

Abstract

Rewriting Induction (RI) is a method to prove inductive theorems, originating from equational reasoning. By using Logically Constrained Simply-typed Term Rewriting Systems (LCSTRSs) as an intermediate language, rewriting induction becomes a tool for program verification, with inductive theorems taking the role of equivalence predicates. Soundness of RI depends on well-founded induction, and one of the core obstacles for obtaining a practically useful proof system is to find suitable well-founded orderings automatically. Using naive approaches, all induction hypotheses must be oriented within the well-founded ordering, which leads to very strong termination requirements. This, in turn, severely limits the proof capacity of RI. Here, we introduce Bounded RI: an adaption of RI for LCSTRSs where such termination requirements are minimized.