原始F5算法的终止性

Faugère提出的原始F5算法是针对任意齐次多项式集输入而设计的。对于任何使算法终止的输入，其输出的正确性已被证明，但终止性本身仅对输入为正则多项式序列的情形得到证明。本文证明该算法对任意齐次输入都能正确终止，无需任何正则性假设。该证明包含两步：首先证明如果算法不终止，则最终会生成两个多项式，其中第一个是第二个的约化子。但第一步并未表明该约化被F5中引入的准则所允许。第二步证明如果存在这样的对，则存在另一对使得该约化被所有准则允许。这样的对的存在导致矛盾。v3版本修正了参考文献。