Теоретико-типовая экспликация математического аппарата родов структур

Олег Анатольевич Доманов

doi:10.47850/RL.2025.6.3.40-58

Авторы

Олег Анатольевич Доманов Институт философии и права СО РАН (г. Новосибирск)

DOI:

https://doi.org/10.47850/RL.2025.6.3.40-58

Ключевые слова:

теория типов, концептуальное проектирование, роды структур, Бурбаки, Никаноров

Аннотация

Методология концептуального проектирования (С. П. Никаноров и др.) опирается на теорию родов структур Н. Бурбаки. Она использует классическую теорию множеств и логику предикатов. Вместе с тем, в последнее время в математике успешно применяются системы работы с доказательствами, основанные на интуиционистской теории типов (Coq, Agda, Lean и пр.) и обладающие большими возможностями в части вычисления, проверки доказательств и пр. Совмещение родоструктурного и теоретико-типового подходов может быть полезным и для того, и для другого. В статье представлена формализация теории родов структур в терминах теории типов (Cubical Agda, вариант гомотопической теории типов). Рассмотрено общее понятие рода структуры, ступени, M-графа, а также операции над термами ступеней и родами структур. На основе формализации сделаны два основных вывода: 1) несмотря на различие философских оснований и используемых концепций множества
оба подхода имеют сходную формальную структуру и связаны через каррирование и декаррирование; 2) теория
родов структур может служить метатеорией по отношению к теории типов. Оба подхода можно рассматривать
как взаимодополнительные. Если первый описывает общую архитектуру теорий, их взаимодействие и генезис,
то второй добавляет вычислительные и доказательственные возможности/

Биография автора

Олег Анатольевич Доманов, Институт философии и права СО РАН (г. Новосибирск)

кандидат философских наук, старший научный сотрудник

Библиографические ссылки

Бурбаки, Н. (1965). Теория множеств. М.: Мир. 455 с.

Bourbaki, N. (1965). Set Theory. Moscow. 455 p.

Кононенко, А. А., Кучкаров, 3. А., Никаноров, С. П., Никитина, Н. К. (2008). Технология концептуального проектирования. Никаноров, С. П. (ред.). М.: Концепт. 580 с.

Kononenko, A. A., Kouchkarov, Z. A., Nikanorov, S. P., Nikitina, N. K. (2008). Technology of Conceptual Design. Nikanorov, S. P. (ed.). Moscow. 580 p.

Никаноров, С. (2013). Введение в аппарат ступеней множеств. М.: Концепт. 350 с.

Nikanorov, S. P. (2013). Introduction to the Apparatus of Set Levels. Moscow. 350 p.

Пономарёв, И. Н. (2007). Введение в математическую логику и роды структур: Учебное пособие. М.: МФТИ. 244 с.

Ponomarev, I. N. (2007). Introduction to Mathematical Logic and Species of Structures: Textbook. Moscow. 244 p.

Erwig, M. (2001). Inductive graphs and functional graph algorithms. Journal of Functional Programming. Vol. 11. No. 5. Pp. 467-492.

Martin-Löf, P. (1984). An Intuitionistic Type Theory. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980. Napoli. Bibliopolis. 91 p.

Martin-Löf, P. (1987). Truth of a Proposition, Evidence of a Judgement, Validity of a Proof. Synthese. Vol. 73. Pp. 407-420. DOI: 10.1007/BF00484985.

Univalent Foundations Program (2013). Homotopy Type Theory. Univalent Foundations of Mathematics. Institute for Advanced Study. 589 p. Available at: http://homotopytypetheory.org/book.

Vezzosi, A., Mörtberg, A., Abel, A. (2021). Cubical Agda: A dependently typed programming language with univalence and higher inductive types. Journal of Functional Programming. Vol. 31. P. e8. DOI: 10.1017/S0956796821000034.