|
1
Поступила в редакцию 26.11.2016
Подписана в печать
23.01.2017
44 с.
/r2/pdf.jpg)
PDF |
С. Д.
Мешвелиани
Программирование вычислительной алгебры на основе конструктивной
математики. Области с разложением на простые множители
Статья продолжает публикации автора о подходе к использованию
конструктивной математики и применении языка с зависимыми типами для
доказуемого программирования вычислительной алгебры. Получено
конструктивное выражение понятия области с разложением на простые
множители для моноидa и кольца с некоторыми дополнительными
свойствами. Описан способ построения машинно-проверяемых
доказательств для теорем, связывающих понятия разложения на простые
множители в областях различного вида. Все описываемые построения и
доказательства воплощены полностью в виде программы на
функциональном языке Agda.
Ключевые слова: конструктивная математика, алгебра, факторизация,
зависимые типы, функциональное программирование, Agda. |
/r1/pdf.jpg){kind=small}
.