1. На главную
  2. Электронные версии
  3. Программирование
  4. № 4, 2023

Программирование, 2023, № 4, стр. 3-20

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

С. Д. Мешвелиани 1, *

a Институт программных систем им. А.К. Айламазяна РАН
152021 Ярославская обл., Переславский р-н, с. Веськово, ул. Петра Первого, 4 “а”, Россия

* E-mail: mechvel@scico.botik.ru

Поступила в редакцию 23.09.2022
После доработки 12.11.2022
Принята к публикации 14.11.2022

Аннотация

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

Ключевые слова: компьютерная алгебра, многочлены, допустимое упорядочение мономов, конструктивное доказательство, лемма Диксона

Список литературы

  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.

Дополнительные материалы отсутствуют.

Инструменты

следующая статья выпуска содержание выпуска

Программирование

Архивы выпусков Информация о журнале Отправить рукопись в журнал