Программирование основ вычислительной алгебры на языке с зависимыми типами
Автор: Мешвелиани Сергей Давидович
Журнал: Программные системы: теория и приложения @programmnye-sistemy
Рубрика: Искусственный интеллект, интеллектуальные системы, нейронные сети
Статья в выпуске: 4 (27) т.6, 2015 года.
Бесплатный доступ
В статье описываются главные черты разработанной автором на основе доказательного программирования библиотеки вычислительной алгебры. Обсуждается опыт доказательного программирования некоторых классических категорий вычислительной алгебры («группа», «кольцо» и так далее) на основе подхода конструктивизма, применения языка с зависимыми типами, построения машинно-проверяемых доказательств (dependent types, proof carrying code). Выявляются проблемы, связанные с этим подходом, и отмечаются дополнительные возможности, даваемые применением аппарата зависимых типов. В качестве инструмента используется функциональный язык Agda. Статья является продолжением вводной статьи автора в данном журнале за 2014 год
Алгебра, конструктивная математика, зависимые типы, функциональное программирование
Короткий адрес: https://sciup.org/14336171
IDR: 14336171
Список литературы Программирование основ вычислительной алгебры на языке с зависимыми типами
- С. Д. Мешвелиани. 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¨ oef. 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.
- А. И. Кострикин. Введение в алгебру. Основы алгебры, Наука. Физматлит, М., 1994.
- Дж. Коллинз, Р. Лоос. Компьютерная алгебра. Символьные и алгебраические вычисления, ред. Б. Бухбергер, Мир, М., 1986.
- Дж. Давенпорт, И. Сирэ, Э. Турнье. Компьютерная алгебра, Мир, М., 1991.
- S. D. Mechveliani. Computer algebra with Haskell: applying functionalcategorial-‘lazy’ programming//International Workshop CAAP-2001 (Dubna, Russia, 2001). P. 203-211, URL: http://compalg.jinr.ru/Confs/CAAP_2001/Final/proceedings/proceed.pdf.
