Программирование вычислительной алгебры на основе конструктивной математики. Области с разложением на простые множители
Автор: Мешвелиани Сергей Давидович
Журнал: Программные системы: теория и приложения @programmnye-sistemy
Рубрика: Математические основы программирования
Статья в выпуске: 1 (32) т.8, 2017 года.
Бесплатный доступ
Статья продолжает публикации автора о подходе к использованию конструктивной математики и применении языка с зависимыми типами для доказуемого программирования вычислительной алгебры. Получено конструктивное выражение понятия области с разложением на простые множители для моноидa и кольца с некоторыми дополнительными свойствами. Описан способ построения машинно-проверяемых доказательств для теорем, связывающих понятия разложения на простые множители в областях различного вида. Все описываемые построения и доказательства воплощены полностью в виде программы на функциональном языке Agda
ID: 14336113 Короткий адрес: https://sciup.org/14336113
Список литературы Программирование вычислительной алгебры на основе конструктивной математики. Области с разложением на простые множители
- С. Д. Мешвелиани. O зависимых типах и интуиционизме в программировании математики//Программные системы: теория и приложения, Т. 5, № 3(21). 2014. С. 27-50, URL: http://psta.psiras.ru/read/psta2014_3_27-50.pdf
- А. А. Марков. О конструктивной математике//Проблемы конструктивного направления в математике, Сборник работ. Т. 2: Конструктивный математический анализ, Тр. МИАН СССР, т. 67, Изд-во АН СССР, М.-Л., 1962. С. 8-14.
- P. Martin-Löef. Intuitionistic Type Theory, Bibliopolis, 1984.
- U. Norell, J. Chapman. Dependently Typed Programming in Agda, URL: http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
- Agda. A dependently typed functional programming language and its system, Homepage of Agda, URL: http://wiki.portal.chalmers.se/agda/pmwiki.php
- С. Д. Мешвелиани. Программирование основ вычислительной алгебры на языке с зависимыми типами//Программные системы: теория и приложения, Т. 6, № 4(27). 2015. С. 313-340, URL: http://psta.psiras.ru/read/psta2015_4_313-340.pdf
- А. И. Кострикин. Введение в алгебру. Основы алгебры, Наука. Физматлит, М., 1994.
- Дж. Коллинз, Р. Лоос. Компьютерная алгебра. Символьные и алгебраические вычисления, ред. Б. Бухбергер, Мир, М., 1986.
- Дж. Давенпорт, И. Сирэ, Э. Турнье. Компьютерная алгебра, Мир, М., 1991.
- С. Ленг. Алгебра, Мир, М., 1968.
- N. Jacobson. Basic Algebra I, W. H. Freeman and Company, New York, 1985.
- S. D. Mechveliani. Computer algebra with Haskell: applying functionalcategorial-’lazy’ programming//International Workshop CAAP-2001 (Dubna, Russia, 2001). С. 203-211, URL: http://compalg.jinr.ru/Confs/CAAP_2001/Final/proceedings/proceed.pdf
- S. Watt, et al.. Aldor Compiler User Guide, IBM Thomas J. Watson Research Center, URL: http://www.aldor.org
- The Coq Proof Assistant, Homepage of the Coq system, URL: http://coq.inria.fr
- A. Mahboubi. "The Rooster and the Butterflies", Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 7961, Springer-Verlag, Berlin-Heidelberg, 2013. P. 1-18.
- S. Meshveliani. "Provable programming of algebra: particular points, examples", Polynomial Computer Algebra 2016, Collection of theses (Eulers’ International Mathematical Institute, Sankt-Petersburg, 2016), VVM Publishing, SPb.. P. 61-64.
- С. Д. Мешвелиани. DoCon-A, библиотека доказательных программ для построителя алгебраических областей, выпуск 0.04.1. Руководство (на английском языке) и исходный код (Переславль-Залесский, 2016), URL: http://www.botik.ru/pub/local/Mechveliani/docon-A/
