- Код статьи
- 10.31857/S0132347423040106-1
- DOI
- 10.31857/S0132347423040106
- Тип публикации
- Статус публикации
- Опубликовано
- Авторы
- Том/ Выпуск
- Том / Номер выпуска 4
- Страницы
- 3-20
- Аннотация
- Обсуждаются конструктивное доказательство завершаемости алгоритма NF построения нормальной формы для многочленов нескольких переменных и связанное с ним понятие допустимого упорядочения \({{ < }_{e}}\) на показателях мономов. В классической математике свойство обрыва убывающей цепи (well-quasiorder) отношения \({{ < }_{e}}\) выводится из леммы Диксона, и этого достаточно для обоснования завершаемости алгоритма NF. В доказательном программировании на основе конструктивной теории типов (Coq, Agda) требуется более сильное (в конструктивной математике) свойство: свойство вполне-заданности отношения порядка (соответствует понятию well-founded – в конструктивном определении, как подобие свойства фундированности). Предлагается конструктивное доказательство этой теоремы (T) для \({{ < }_{e}}\), основанное на некотором известном методе, который здесь назовем “метод образцов”. Эта теорема о вполне-заданности произвольного допустимого упорядочения важна и сама по себе, независимо от алгоритма NF. Нам не известны другие работы, в которых (конструктивно) доказана эта теорема. Оказывается, она не очень сложно следует из результатов, достигнутых другими исследователями еще в 2003-м году. Доказательство запрограммировано автором на языке Agda в виде библиотеки AdmissiblePPO-wellFounded доказательных программ вычислительной алгебры, разработанной автором. Разработка включает в себя применение этой теоремы к доказательному программированию алгоритма NF. Поэтому библиотека также содержит часть доказательных программ алгебры многочленов, которая по объему значительно больше того, что нужно для доказательства теоремы T.
- Ключевые слова
- компьютерная алгебра многочлены допустимое упорядочение мономов конструктивное доказательство лемма Диксона
- Дата публикации
- 17.09.2025
- Год выхода
- 2025
- Всего подписок
- 0
- Всего просмотров
- 18
Библиография
- 1. Гаранина Н.О. Общие знания в хорошо структурированных системах с абсолютной памятью // Модел. и анализ информ. Систем. 2013. Т. 20. № 6. С. 10–21.
- 2. Ершов Ю.Л., Палютин Е.А. Математическая логика. 6-e изд., испр. М.: ФИЗМАТЛИТ, 2011. 356 с. ISBN 978-5-9221-1301-4.
- 3. Мешвелиани С.Д. O зависимых типах и интуиционизме в программировании математики // В электронном журнале Программные системы: теория и приложения. 2014. Т. 5. Вып. 3. С. 27–50. http://psta.psiras.ru/read/psta2014_3_27-50.pdf
- 4. Мешвелиани С.Д. AdmissiblePPO-wellFounded – программа на языке Agda формального конструктивного доказательства леммы Диксона и теоремы о вполне-заданности допустимого упорядочения на мономах многочленов. Институт программных систем РАН, Переславль-Залесский, 2022, www.botik.ru/pub/local/Mechveliani/inAgda/admissiblePPO-wellFounded.zip
- 5. Martin-Mateos F.J., Alonso J.A., Hidalgo M.J., Ruiz-Reina J.L. A Formal Proof of Dickson’s Lemma in ACL2. M.Y. Vardi and A. Voronkov (Eds.): LPAR 2003, LNAI 2850. 2003. P. 49–58.
- 6. Agda. A proof assistant. A dependently typed functional programming language and its system. http://wiki.portal.chalmers.se/agda/pmwiki.php.
- 7. Norell U. Dependently Typed Programming in Agda. AFP 2008: Advanced Functional Programming, Lecture Notes in Computer Science, vol. 5832, Springer, Berlin–Heidelberg, 2008. P. 230–266.
- 8. Бухбергер Б. Базисы Грёбнера. Алгоритмический метод в теории полиномиальных идеалов. В сборнике “Компьютерная алгебра”, редакторы Б. Бухбергер, Дж. Коллинз, Р. Лоос. Перевод с английского. Москва, МИР, 1986. С. 331–372.
- 9. Coquand Th. and Persson H. Gröbner Bases in Type Theory. 1998. 13 p. https://www.researchgate.net/publication/221186683_Grobner_Bases_in_Type_Theory
- 10. Théry L. A Machine-Checked Implementation of Buchberger’s Algorithm // Journal of Automated Reasoning. 2001. V. 26. P. 107–137.
- 11. Romanenko S.A. Proof of Higman’s Lemma (for two letters) Formalized in Agda. In Russian. Июль 2017. https://pat.keldysh.ru/roman/doc/talks/2017_Romanenko__Higman’s_lemma_for_2_letters_in_Agda_ru__slides.pdf Agda program for the proof: https://github.com/sergei-romanenko/agda-Higman-lemma, in the folder Berghofer.
- 12. Robbiano L. Term orderings on the polynomial ring. Proc. EUROCAL ’85 European Conference on Computer Algebra. Linz 1985, Springer Leer. Notes Comp. Sei. 1986. V. 204. P. 513–517.
- 13. Curry H.B., Feys R. Combinatory Logic, vol I. Amsterdam, North-Holland, 1958. 417 p.
- 14. Howard W.A. The formulae-as-types notion of construction. To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Boston, Academic Press, 1980. P. 479–490.
- 15. Марков А.А. О конструктивной математике. Проблемы конструктивного направления в математике. 2. Конструктивный математический анализ, Сборник работ, Тр. МИАН СССР, 67, Изд-во АН СССР, М.–Л., 1962. С. 8–14.
- 16. Per Martin-Loef. Intuitionistic type theory. Bibliopolis, ISBN 88-7088-105-9. 1984. 91 p.
- 17. Stricland Neil P. Euclid’s theorem. An annotated proof in Agda that there are infinitely many primes. https://nextjournal.com/agda/euclid-theorem
- 18. Vytiniotis D., Coquand Th., Wahlstedt D. Stop When You Are Almost Full. Adventures in Constructive Termination // ITP 2012: Interactive Theorem Proving. 2012. P. 250–265.
