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