Rewriting Induction (RI) is a formal system in term rewriting to establish program equivalence. The recently defined Bounded RI for higher-order Logically Constrained Term Rewriting Systems (LCSTRSs) yields a convenient proof system for analyzing real programming code. A practical challenge in RI is the automatic generation of induction hypotheses, called lemmas. While various lemma generation techniques exist for plain term rewriting, there are much fewer that consider the intricacies brought on by calculations or constraints. Taking advantage of recent developments in higher-order RI, we here present a new approach based on templates, which operates by recognising typical programming constructs as instances of higher-order functions. While templates have been used as a stand-alone method to justify the correctness of program transformations, we here consider their integration in Bounded RI to obtain a complementary lemma generation heuristic. This allows us to prove equivalences that were previously out of reach.

翻译：重写归纳（RI）是项重写中用于建立程序等价性的形式化系统。近期针对高阶逻辑约束项重写系统（LCSTRSs）提出的有界RI为分析实际编程代码提供了便捷的证明系统。RI的一个实际挑战在于自动生成归纳假设（称为引理）。尽管针对简单项重写已存在多种引理生成技术，但能处理计算或约束所带来的复杂性的技术却少得多。利用高阶RI的最新进展，本文提出了一种基于模板的新方法，通过将典型编程结构识别为高阶函数的实例来运作。尽管模板已被用作独立方法来证明程序转换的正确性，但本文考虑将其集成到有界RI中，以获得互补的引理生成启发式策略。这使得我们能够证明此前无法触及的等价性。