F5(F5类)算法正确性的一个新证明
符号计算
2010-07-01 v4
摘要
著名的用于计算Gröbner基的F5算法由Faugère于2002年提出，但未给出其正确性的完整证明。当前作者已将原始F5算法简化为Buchberger风格的F5算法(F5B算法)，该算法等价于原始F5算法，并可推导出一些F5类版本。本文简要回顾了F5B算法，并提出了一个关于F5B算法正确性的新完整证明。该新证明不限于齐次系统，且不依赖于选择关键对(即决定先计算哪个关键对的策略)的策略，因此F5B(F5)算法中可采用任何策略。从这个新证明中，我们发现特殊的约化过程(F5-约化)是F5算法的关键，因此保持这种特殊约化，各种变体算法成为可能。本文还提出并证明了一种F5算法的自然变体，该变体将原始F5算法转化为非增量算法。该自然变体已在布尔环上实现。该自然变体中的两个修订准则也能拒绝几乎所有不必要的计算，并且在大多数例子中很少有多项式约化为0。
引用
@article{arxiv.1004.0084,
title = {A New Proof for the Correctness of F5 (F5-Like) Algorithm},
author = {Yao Sun and Dingkang Wang},
journal= {arXiv preprint arXiv:1004.0084},
year = {2010}
}