一句话：提出基于随机执行迹生成与收缩的 QuickCheck 方法，测试项重写系统的收敛性并高效发现反例。
项重写系统广泛用于自动推理与编程语言语义，许多应用要求系统收敛（合流且终止）。现有工具与理论可判定收敛性，但本文关注一种实用的测试方法，以快速发现有用的反例。标准基于性质的测试在此面临困难：穷举计算所有范式本质上有缺陷且过慢；随机生成范式则因依赖先前生成的数据，使反例收缩变得脆弱。作者提出基于随机执行迹的生成与收缩的 QuickCheck 方法：检查迹的首项与末项是否共享同一确定性范式，从而消除生成器间的数据依赖，得到高效发现反例、并支持快速稳健收缩的性质。作者在群论方程到分布式进程演算等多个例子上展示了方法有效性。
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.