齐次F5算法的简单终止性证明

摘要

Since the F5 algorithm is proposed, a bunch of signature-based Gröbner basis algorithms appear. They use different selection strategies to get the basis gradually and use different criteria to discard redundant polynomials as many as possible. The strategies and criteria should satisfy some general rules for correct termination. Based on these rules, a framework which include many algorithms as instances is proposed. Using the property of rewrite basis, a simple proof of the correct termination of the framework is obtained. For the simple proof of the F5 algorithm, the reduction process is simplified. In particular, for homogeneous F5 algorithm, its complicated selection strategy is proved equivalent to selecting polynomials with respect to module order. In this way, the F5 algorithm can be seen as an instance of the framework and has a rather short proof.%自从F5算法提出以来，出现了一批基于标签的Gröbner基算法，它们使用了不同的选择策略且减少冗余多项式的准则也各不相同。为了满足正确终止性，这些算法的策略和准则必须满足一些一般的规律。根据这些规律，该文提出了一个框架，使大多数算法成为该框架的实例。随后，利用重写基的性质，得到了框架的简单正确终止证明。为了得到F5算法的简单证明，该文对F5算法的约化操作进行合理的化简。特别地，对于齐次F5算法，证明了其复杂的选择策略等价于按模序选择。这样，齐次F5算法就能看成框架的一个特例，从而得到了F5算法的简单证明。