Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.01246

Augmenting Rewrite Rule Sets via Knuth-Bendix Completion

Michael Schifferer·Marcel Ullrich·Sebastian Hack
View original source ↗Read source document ↗Export metadata ↓

Abstract

Equality Saturation (EqSat) is a powerful technique for program optimization, systematically exploring the search space of candidate programs to overcome the phase ordering problem. However, the feasibility and performance of EqSat rely heavily on the specific rewrite rules used to derive equivalent programs. These rule sets are typically handcrafted, requiring extensive domain expertise and carrying the risk of missing valuable transformations. In this work, we evaluate Knuth-Bendix Completion (KBC) as a method for automatically generating and augmenting rewrite rules for EqSat. Our experiments show faster optimization as well as reaching better terms with previously missed optimizations.

Explore related subjects

cs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Michael Schifferer, Marcel Ullrich, Sebastian Hack. 2026-10-01. Augmenting Rewrite Rule Sets via Knuth-Bendix Completion. https://arxiv.org/abs/2610.01246

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Associativity and Commutativity in Equality Saturation

Equality saturation is a promising technique for program optimization which sidesteps the phase ordering problem. However, current e-graph implementations grow exponentially large, even for simple examples. Many practical applications involve associative and commutative (AC) operators. We present an extension of relational e-matching that handles AC operators natively by storing terms as multisets. Preliminary results show that equality saturation modulo AC uses asymptotically less memory in certain cases.

cs.PL↗
arXiv2026

Freely Generated Categorical Structures and Automatic Differentiation, PhD Thesis (Introduction and Conclusion)

This version contains the introduction and conclusion of my PhD thesis, "Freely Generated Categorical Structures and Automatic Differentiation", together with its English and Dutch summaries. The full thesis consists of an introductory chapter, six joint research papers, and a concluding chapter, developed during my PhD studies at Utrecht University under the supervision of Gabriele Keller and Matthijs Vákár. The research papers are available separately and are not reproduced here. The introduction presents the scope of the thesis, explains the contributions of the six papers and their connections, and introduces the categorical foundations of our approach. The guiding idea is that programming languages, viewed as freely generated categorical structures, provide a principled setting for constructing structure-preserving program transformations and proving their correctness. Automatic differentiation supplies the central application: we study forward- and reverse-mode differentiation for expressive typed languages, including higher-order functions, recursive types, iteration and partiality. The semantic requirements of these transformations also motivate independent mathematical results on free distributive and extensive categories, cartesian closedness, and Grothendieck constructions. The conclusion brings these contributions together, discusses their limitations, and outlines further directions. Throughout, the thesis develops a dialogue between theory and practice: categorical semantics guides the construction of reliable and practically useful program transformations, while the demands of computation lead to new categorical structures and results.

cs.PL↗
arXiv2026

Automatically Building Machine-Checked Assurance Cases from C Codebases to Requirements

Large language models (LLMs) have shown promise in automating interactive theorem proving, yet verification of real-world C codebases requires more than discharging individual proof goals. The task involves jointly constructing expressive function specifications and their proofs, and ensuring that library interfaces compose along intended call sequences even without a designated client. This paper presents CCV, an LLM-assisted framework for building machine-checked assurance cases: structured, auditable artifacts supporting the claim that a C codebase meets its intended requirements. To model intended cross-interface use in open libraries, CCV constructs an interface protocol that exposes permitted call sequences and resource assumptions for review, with a conditional safety guarantee under verified contracts and caller obligations. CCV coordinates two complementary phases: (i) requirement-guided analysis and bottom-up construction of candidate specifications and protocols; and (ii) modular proof construction with feedback that revises the specifications and proofs. Implemented using VST in Rocq, CCV verifies memory safety and leak freedom for all 299 function definitions across six C benchmarks, including industrial cryptographic components, with less than one person-day of reported human effort per benchmark. The guarantees depend on disclosed contracts and assumptions; human review supplies the conformance judgments connecting the formal artifacts to the intended requirements.

cs.PL↗