Программирование вычислительной алгебры на основе конструктивной математики. Области с разложением на простые множители
Автор: Мешвелиани Сергей Давидович
Журнал: Программные системы: теория и приложения @programmnye-sistemy
Рубрика: Математические основы программирования
Статья в выпуске: 1 (32) т.8, 2017 года.
Бесплатный доступ
Статья продолжает публикации автора о подходе к использованию конструктивной математики и применении языка с зависимыми типами для доказуемого программирования вычислительной алгебры. Получено конструктивное выражение понятия области с разложением на простые множители для моноидa и кольца с некоторыми дополнительными свойствами. Описан способ построения машинно-проверяемых доказательств для теорем, связывающих понятия разложения на простые множители в областях различного вида. Все описываемые построения и доказательства воплощены полностью в виде программы на функциональном языке Agda
ID: 14336113 Короткий адрес: https://sciup.org/14336113
