index.pug

include header

html
    head
        meta(property='og:title'       content='AXIO/1')
        meta(property='og:description' content='FORMAL MATHEMATICS')
        meta(property='og:url'         content='https://groupoid.github.io/axio/')

block title
    title AXIO/1

block content
    +header('', 'AXIO/1', 'Формальне середовище виконання, система вищих мов та базові бібліотеки для програмування, доведення теорем і формальної філософії')
    article.main
        .om
            section
                h1 АНОТАЦІЯ

            aside Дисертація на здобуття ступеня <br> доктора філософії <br> Максима Сохацького
                time 1 Вересня 2021

            p(style="font-size: 14px;").
                Дисертація присвячена розробці першої формальної системи AXIO/1,
                яка встановлює новаторський підхід до математичної верифікації та
                створює уніфіковану систему формальних мов для програмування, математик та філософій.
                У процесі створення цієї системи автор проаналізував синтаксис і семантику понад 50 мов програмування
                з промислових та академічних доменів, реалізувавши 8 власних мов.
                Робота презентує концептуальну модель уніфікованої мовної системи, що складається з 8 математичних мов,
                та демонструє їхні імплементації. Основна мета — синтез універсальної платформи для механічної
                верифікації теорем, що охоплює класичні та синтетичні математики в обчислювально перевірюваному формалізмі.

            p(style="font-size: 14px;").
                Перша формальна система AXIO/1 визначає формальний підхід до математичної
                верифікації та описує спробу автора у цій парадигмі побудувати
                уніфіковану систему формальних мов для програмування,
                математики та філософії. В процесі розробки моделі такої
                системи автору довелося апробувати підхід та практики
                для головних функціональних формальних академічних мов.

            section
                h1 СТРУКТУРА РОБОТИ
            p.
                Мови розглядаються як моноїдальні категорії,
                де об’єкти — простори програм, а морфізми — правила верифікації та компіляції.
                Система розкладається на спектральну послідовність мов, індексовану натуральними числами.
            p.
                Як результат дослідження пропонується унікальна відкрита система, яка інтегрує:
                1) системне програмне забезпечення: модального середовища виконання разом з інтерпретатором написаним на формальній мові;
                2) бібліотеки: для прикладного програмування в середовищах виконання;
                3) прикладне програмне забезпечення: системи вищих формальних мов з різними ефективними моделями для різних математик та їх імплементаціями;
                4) математичні бібліотеки: механізовані теореми для верифікації.
            p.
                Робота черпає натхнення з LISP-машин, APL-систем, ранніх систем доведення теорем (як AUTOMATH),
                віртуальних машин для паралельної обробки (як BEAM) та кубічних систем (HTS).

        h2 Середовище виконання

        p Середовища виконання — зерна.

        .index
            .index__col
                h2 Зерна
                ul
                    li: a(href='https://alonzo.groupoid.space/') ДЗК-інтерпретатор
                    li: a(href='https://yves.groupoid.space/') СМК-інтерпретатор
            .index__col
                h2 Бібліотека
                ul
                    li: a(href='https://anders.groupoid.space/foundations/modal/process/') Процеси
                    li: a(href='https://groupoid.space/runtime/effects/') Ефекти
                    li: a(href='https://anders.groupoid.space/foundations/mltt/io/') IO
                    li: a(href='https://anders.groupoid.space/foundations/mltt/ioi/') IOI

        h2 Мови програмування

        p Мови програмування — паростки.

        .index
            .index__col
                h2 Паростки
                ul
                    li: a(href='https://henk.groupoid.space') Ядро розшарування
                    li: a(href='https://per.groupoid.space') Ядро локальних ДЗК
                    li: a(href='https://christine.groupoid.space') Індуктивне ядро
                    li: a(href='https://anders.groupoid.space/') Гомотопічне ядро
                    li: a(href='https://laurent.groupoid.space') Ядро аналізу
                    li: a(href='https://dan.groupoid.space') Сімліціальне ядро
                    li: a(href='https://jack.groupoid.space') K-теоретичне ядро
                    li: a(href='https://urs.groupoid.space') Супергеометричне ядро
            .index__col
                h2 Бібліотеки
                ul
                    li: a(href='https://groupoid.space/misc/library/') Математичні компоненти
                    li: a(href='https://groupoid.space/institute/КМ-111/10-Гомотопічна-теорія-типів/') Курс по теорії типів
                    li: a(href='https://groupoid.space/misc/internship/') Інтернатура
                    li: a(href='https://anders.groupoid.space/mathematics/homotopy/hopf/') Розшарування хопфа
                    li: a(href='https://groupoid.space/') Групоїд Інфініті

        h2 Формалізація математик

        p Математичні теорії — дерева, математики — їх ліси.

        .index
            .index__col
                h2 <b>ANALYSIS</b>
                ul
                    li: <a href='https://anders.groupoid.space/mathematics/analysis/topology/'>TOPOLOGY</a>
                    li: <a href='https://anders.groupoid.space/mathematics/analysis/set/'>SET</a>
                    li: <a href='https://anders.groupoid.space/mathematics/analysis/rational/'>ℚ</a>, <a href='https://anders.groupoid.space/mathematics/analysis/real/'>ℝ</a>, <a href='https://anders.groupoid.space/mathematics/analysis/complex/'>ℂ</a>, <a href='https://anders.groupoid.space/mathematics/analysis/quatro/'>ℍ</a>, <a href='https://anders.groupoid.space/mathematics/analysis/octo/'>𝕆</a>
            .index__col
                h2 <b>ALGEBRA</b>
                ul
                    li: a(href='https://anders.groupoid.space/mathematics/algebra/group/') GROUP
                    li: a(href='https://anders.groupoid.space/mathematics/algebra/algebra/') ALGEBRA
                    li: a(href='https://anders.groupoid.space/mathematics/algebra/homology/') HOMOLOGY
            .index__col
                h2 <b>GEOMETRY</b>
                ul
                    li: a(href='https://anders.groupoid.space/mathematics/geometry/etale/') ETALE
                    li: a(href='https://anders.groupoid.space/mathematics/geometry/bundle/') BUNDLE
                    li: a(href='https://anders.groupoid.space/mathematics/geometry/manifold/') MANIFOLD
                    li: a(href='https://anders.groupoid.space/mathematics/geometry/derham/') DE RHAM

            .index__col
                h2 <b>HOMOTOPY</b>
                ul
                    li: a(href='https://anders.groupoid.space/mathematics/homotopy/coequalizer/') COEQUALIZER
                    li: a(href='https://anders.groupoid.space/mathematics/homotopy/pushout/') PUSHOUT
                    li: a(href='https://anders.groupoid.space/mathematics/homotopy/pullback/') PULLBACK
                    li: a(href='https://anders.groupoid.space/mathematics/homotopy/hopf/') HOPF
                    li: a(href='https://anders.groupoid.space/mathematics/homotopy/cw/') CW

            .index__col
                h2 <b>CATEGORIES</b>
                ul
                    li: a(href='https://anders.groupoid.space/mathematics/categories/category/') CATEGORY
                    li: a(href='https://anders.groupoid.space/mathematics/categories/functor/') FUNCTOR
                    li: a(href='https://anders.groupoid.space/mathematics/categories/groupoid/') GROUPOID
                    li: a(href='https://anders.groupoid.space/mathematics/categories/topos/') TOPOS
                    li: a(href='https://anders.groupoid.space/mathematics/categories/presheaf/') PRESHEAF

        .om
            section
                h1 Середовище виконання

            p.
                Розділ присвячений загальній таксономії мов програмування. Виявляється, що
                всі мови програмування так чи інакше є внутрішніми мовами категорій, що містять структуру
                декартово-замкнених або симетричних моноїдальних категорій. Кінцева мета — створення
                <a href="https://groupoid.github.io/languages/">енциклопедії мов програмування</a> і
                <a href="https://o83.github.io/platform.rs/">прототипу обчислювального середовища</a>.

            +tex.
                $\mathbf{Alonzo}$ — мінімальна мова для послідовних обчислень в декартово-замкнених категоріях.
            +tex.
                $\mathbf{Yves}$ — мінімальна мова для паралельних обчислень в симетричних моноїдальних категоріях.
            p.
                Повний перелік інтерпретаторів і асемблерів, як цілей компіляцій, представлений в роботі:
                1) інтерпретатор MinCaml написаний на MinCaml;
                2) авторський лінивий лямбда інтерпретатор з паралельним середовищем виконанням без надлишкового копіювання,
                   AVX-512 векторизацією і чергах на CAS-курсорах на мові програмування Rust;
                3) віртуальна машина BEAM мови програмування Erlang від Ericsson (LING).
                4) Intel асемблер як ціль компіляції для MinCaml;
                5) ARM64 асемблер як ціль компіляції для MinCaml.

            +tex.
                $\mathbf{Joe}$ — українська віртуальна машина Джо Армстронга.
            +tex.
                $\mathbf{Leslie}$ — верифікатор TLA+ протоколів Леслі Лампорта.
            +tex.
                $\mathbf{Tim}$ — компілятор STG Тіма Олсона з синтаксисом Miranda.
            +tex.
                $\mathbf{Eijiro}$ — компілятор Ейджиро Сумії з синтаксисом MiniCaml.
            +tex.
                $\mathbf{Robin}$ — мова Робіна Мілнера для BLAS 3 на основі Standard ML.

            section
                h1 Мови програмування
            p.
                Розділ присвячений таксономії мов програмування для доведення теорем — від
                <a href="https://henk.groupoid.space">найпростіших</a> з квантором узагальнення до
                <a href="https://anders.groupoid.space">гомотопічних систем</a> з двома рівностями.
                Кінцева мета — створення прототипів верифікаторів для <a href="https://laurent.groupoid.space">функціонального аналізу</a>
                і <a href="https://urs.groupoid.space">квантової супергеометрії</a>.
            +tex.
                $\mathbf{Henk}$ — чиста система з всвесвітами.
            +tex.
                $\mathbf{Frank}$ — мінімальна індуктивна система.
            +tex.
                $\mathbf{Christine}$ — тактична система доведення теорем.
            +tex.
                $\mathbf{Per}$ — внутрішня мова локальних ДЗК.
            +tex.
                $\mathbf{Anders}$ — гомотопічна система з двома рівностями.

            p.
                Повний перелік теорій типів, представлений в роботі:
                1) Теорія типів Генка Барендрегта для чистого залежного лямбда-числення;
                2) Теорія типів Пера Мартіна-Льофа для фібріційного контексту та індуктивних типів;
                3) Теорія типів Андерса Мьортберга для початкового завантаження CCHM/CHM/HTS;
                4) Симпліціальна гомотопічна теорія типів Дана Кана;
                5) Теорія типів Джека Морави для хроматичної гомотопічної теорії та K-теорії;
                6) Теорія типів Урса Шрайбера для еквіваріантної супeргеометрії;
                7) Теорія типів Фаб’єна Мореля для A¹-гомотопічної теорії;
                8) Теорія типів Лорана Шварца для функціонального аналізу та теорії розподілів;
                9) Теорія типів Ернста Цермело для ZFC з законом виключеного третього;
                10) Теорія типів Пола Коена для системи кардиналів, що включає великі кардинали та форсинг.

            +tex.
                $\mathbf{Laurent}$ — система типів функціонального аналізу.
            +tex.
                $\mathbf{Dan}$ — сімпліціальна теорія інфініті-категорій.
            +tex.
                $\mathbf{Jack}$ — синтетична К-теорія.
            +tex.
                $\mathbf{Fabien}$ — $\mathbb{A}^1$-теорія гомотопій.
            +tex.
                $\mathbf{Urs}$ — еквіваріантна система типів супергеометрії.

            section
                h1 Формалізація математик
            p.
                Розділ присвячений механічній верифікації
                математичних теорем, від класичного аналізу до сучасних теорій множин і гомотопій.
                Система синтезує синтетичну гомотопію, стабільні гомотопічні спектри, когезивну геометрію,
                дійсний аналіз і теорію множин у єдиному формалізмі.
            +tex.
                $\mathbf{Analysis}$ — теорія розподілів Лорана Шварца.
            +tex.
                $\mathbf{Algebra}$ — гомологічна алгебра.
            +tex.
                $\mathbf{Homotopy}$ — теорія гомотопій.
            +tex.
                $\mathbf{Geometry}$ — диференціальна геометрія.
            +tex.
                $\mathbf{Topos}$ — теорія топосів.
            p.
                Перелік теорем для самоверифікації: 1) Теорія чисел: Теорема про прості числа;
                2) Фундаментальна теорема числення (аналіз);
                3) Аналіз: Теорема про збіжність Лебега;
                4) Топологія: Гіпотеза Пуанкаре (3D);
                5) Алгебра: Класифікація скінченних простих груп;
                6) Теорія множин: Незалежність гіпотези континууму (CH);
                7) Теорія категорій: Теорема про спряжені функтори;
                8) Гомотопічна теорія: Кон’юктура Адамса (через K-теорію);
                9) Консистентність ZFC з великими кардиналами;
                10) Остання теорема Ферма;
                11) Теорема про великі кардинали: Максимум Мартіна.
            p.
                Це не вичерпне, але оглядове бачення її здатності охоплювати алгебраїчні,
                аналітичні, топологічні та фундаментальні домени. AXIO/1 є кандидатом на
                універсальну механізовану математичну платформу, що конкурує з такими системами,
                як кубічна теорія типів (Agda), чи індуктивна теорія типів з фактор-просторами (Lean),
                розширюючи їхній обсяг примітивів.

        .om
            section
                h1 Висновки
            p.
                Система AXIO/1 об’єднує синтетичні і класичні математики в механічно перевірюваній структурі.
                Її категорні моделі охоплюють симпліціальні ∞-категорії, стабільні спектри,
                когезивні модальності, ZFC, великі кардинали та форсинг, забезпечуючи повне
                покриття математичних доменів станом на 2025 рік. Спектральна категорія мов
                дозволяє працювати у внутрішніх мовах відповідних категорій і транспортувати
                моделі за необхіодності у інші топоси для найефективніших обчислень, що робить систему
                унікальною платформою для формалізації математик.

        .om
            section
                h1 Публікації

                div(style="padding-top: 8px;")
                    img(src="https://anders.groupoid.space/images/pdf.jpg", width="35")
                    a(href="https://groupoid.space/books/vol5/vol5.pdf") &nbsp; AXIO.PDF
                    |  Формальні Математики

                div(style="padding-top: 8px;")
                    img(src="https://anders.groupoid.space/images/pdf.jpg", width="35")
                    a(href="https://groupoid.space/books/vol3/henk.pdf") &nbsp; HENK.PDF
                    |  Хенк Барендрегт

                div(style="padding-top: 8px;")
                    img(src="https://anders.groupoid.space/images/pdf.jpg", width="35")
                    a(href="https://groupoid.space/books/vol1/mltt.pdf") &nbsp; MLTT.PDF
                    |  Пер Мартін-Льоф

                div(style="padding-top: 8px;")
                    img(src="https://anders.groupoid.space/images/pdf.jpg", width="35")
                    a(href="https://groupoid.space/books/vol3/anders.pdf") &nbsp; ANDERS.PDF
                    |  Андерс Мортберг

                div(style="padding-top: 8px;")
                    img(src="https://anders.groupoid.space/images/pdf.jpg", width="35")
                    a(href="https://groupoid.space/books/vol3/anders.pdf") &nbsp; LAURENT.PDF
                    |  Лоран Шварц

                div(style="padding-top: 8px;")
                    img(src="https://anders.groupoid.space/images/pdf.jpg", width="35")
                    a(href="https://groupoid.space/books/vol3/urs.pdf") &nbsp; URS.PDF
                    |  Урс Шрайбер

include footer