Программирование основ вычислительной алгебры на языке с зависимыми типами
Автор: Мешвелиани Сергей Давидович
Журнал: Программные системы: теория и приложения @programmnye-sistemy
Рубрика: Искусственный интеллект, интеллектуальные системы, нейронные сети
Статья в выпуске: 4 (27) т.6, 2015 года.
Бесплатный доступ
В статье описываются главные черты разработанной автором на основе доказательного программирования библиотеки вычислительной алгебры. Обсуждается опыт доказательного программирования некоторых классических категорий вычислительной алгебры («группа», «кольцо» и так далее) на основе подхода конструктивизма, применения языка с зависимыми типами, построения машинно-проверяемых доказательств (dependent types, proof carrying code). Выявляются проблемы, связанные с этим подходом, и отмечаются дополнительные возможности, даваемые применением аппарата зависимых типов. В качестве инструмента используется функциональный язык Agda. Статья является продолжением вводной статьи автора в данном журнале за 2014 год
Алгебра, конструктивная математика, зависимые типы, функциональное программирование
Короткий адрес: https://sciup.org/14336171
IDR: 14336171
Programming basic computer algebra in a language with dependent types
The article describes the main features of the computational algebra library developed by the author on the basis of proving programming. The experience of demonstrative programming of some classical categories of computational algebra ("group", "ring" and so on) is discussed on the basis of the constructivist approach, the use of language with dependent types, the construction of machine-verified proofs (dependent types, proof carrying code). The problems associated with this approach are identified, and additional possibilities are indicated, given by the use of a device of dependent types. The instrument is the functional language Agda. The article is a continuation of the introductory article of the author in this magazine for 2014
Список литературы Программирование основ вычислительной алгебры на языке с зависимыми типами
- С. Д. Мешвелиани. 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.
