QuickChecking Convergence of Rewriting Systems (Functional Pearl)
TL;DR
A QuickCheck testing method based on generating and shrinking random execution traces based on checking if the first and last terms of a generated trace share the same deterministic normal form that efficiently finds counterexamples and enables fast, robust shrinking.
Abstract
Term rewriting systems are a common tool in automated reasoning and semantics of programming languages, and many practical applications require these systems to be convergent. While automated tools and theory exist to establish convergence, this paper is concerned with a practical method for testing it to quickly find useful counterexamples. Standard property-based testing approaches struggle here: exhaustively computing all normal forms is fundamentally flawed and too slow, while generating random normal forms makes counterexample minimization (shrinking) fragile due to dependencies on earlier generated test data. To solve this, we introduce a QuickCheck testing method based on generating and shrinking random execution traces. By checking if the first and last terms of a generated trace share the same deterministic normal form, we remove the data dependency between generators. This approach yields a property that efficiently finds counterexamples and enables fast, robust shrinking. We demonstrate the effectiveness of this method on various examples, ranging from group theory equations to distributed process calculus.