ДОПУСТИМЫЙ ПОРЯДОК НА МОНОМАХ ВПОЛНЕ ЗАДАН. КОНСТРУКТИВНОЕ ДОКАЗАТЕЛЬСТВО

Обсуждаются конструктивное доказательство завершаемости алгоритма NF построения нормальной формы для многочленов нескольких переменных и связанное с ним понятие допустимого упорядочения \({{ < }_{e}}\) на показателях мономов. В классической математике свойство обрыва убывающей цепи (well-quasiorder) отношения \({{ < }_{e}}\) выводится из леммы Диксона, и этого достаточно для обоснования завершаемости алгоритма NF. В доказательном программировании на основе конструктивной теории типов (Coq, Agda) требуется более сильное (в конструктивной математике) свойство: свойство вполне-заданности отношения порядка (соответствует понятию well-founded – в конструктивном определении, как подобие свойства фундированности). Предлагается конструктивное доказательство этой теоремы (T) для \({{ < }_{e}}\), основанное на некотором известном методе, который здесь назовем “метод образцов”. Эта теорема о вполне-заданности произвольного допустимого упорядочения важна и сама по себе, независимо от алгоритма NF. Нам не известны другие работы, в которых (конструктивно) доказана эта теорема. Оказывается, она не очень сложно следует из результатов, достигнутых другими исследователями еще в 2003-м году. Доказательство запрограммировано автором на языке Agda в виде библиотеки AdmissiblePPO-wellFounded доказательных программ вычислительной алгебры, разработанной автором. Разработка включает в себя применение этой теоремы к доказательному программированию алгоритма NF. Поэтому библиотека также содержит часть доказательных программ алгебры многочленов, которая по объему значительно больше того, что нужно для доказательства теоремы T.