gistfile1.txt

Загальна картина: Чи може одна мова керувати всією математикою?
Уявіть, що вам доручено створити єдину мову програмування для кодування всього Всесвіту. Вона має обчислювати планетарні орбіти, писати прості програми, описувати квантову механіку та доводити кожну математичну теорему, коли-небудь задуману.

Десятиліттями математики та вчені-інформатики намагалися знайти цю «єдину універсальну мову».

Дехто вважав, що відповіддю є теорія множин. Інші вважали, що відповіддю є теорія гомотопічних типів (мова, заснована на геометрії).

У цій статті «Архітектура математики» робиться сміливе твердження: жодна окрема мова не може зробити все. Спроба створити монолітну мову — це як спроба створити швейцарський армійський ніж, який також є газонокосаркою, калькулятором і космічним кораблем. Він стає занадто важким і ламається під власною вагою.

Натомість у статті пропонується «Решітка мов» — мережа менших, вузькоспеціалізованих мов, які з'єднані автоматичними перекладачами (так званими «функторами»).

Три гілки (хребти) мережі
Замість однієї драбини, де одна мова «краща» за іншу, автори розподіляють свої мови на три основні гілки (хребти), залежно від того, в чому вони найкраще розбираються:

1. Хребет I: Хребет логіки та обчислення (Френк Крістін Лоран)
Для чого він призначений: Традиційна математика, комп'ютерне програмування, обчислення та реальні числа.
Як це працює: Починається з базової логіки та переходить до роботи зі складними речами, такими як границі, інтеграли та дійсні числа (обчислення). Якщо ви хочете довести теореми про стандартне шкільне обчислення, ви використовуєте цю гілку.

2. Хребет II: Хребет форми та фізики (Хенк Пер Андерс Урс)
Для чого він призначений: Геометрія, простори, фізика та квантова механіка.
Як це працює: Замість того, щоб розглядати математику як жорсткі рівняння, ця гілка розглядає математичні твердження як геометричні фігури.
У звичайній математиці, якщо $A = B$, це простий варіант «так/ні».
У цій гілці рівність розглядається як безперервний шлях (лінія), що з'єднує точку $A$ з точкою $B$. Якщо існує кілька способів дістатися від $A$ до $B$, ці шляхи самі можуть мати шляхи між собою! Це критично важливо для фізики (наприклад, теорії струн або квантових обчислень), де частинки рухаються вздовж шляхів у просторі.
3. Spine III: The Relationship Spine (Dan $\to$ Mike $\to$ Ulrik)
Для чого він призначений: Категорії, напрямки та операції.
Як він працює: Цей spine моделює відносини. Він вводить «спрямовані шляхи» — це означає, що ви можете перейти від $A$ до $B$, але не обов'язково повернутися назад. Це корисно для моделювання процесів, які протікають лише в одному напрямку (наприклад, час або виконання комп'ютером).
«Космічний куб» (Тривимірна координатна сітка)
Щоб упорядкувати всі ці мови, у статті їх зображено на тривимірній сітці під назвою Космічний куб.

Так само, як ви можете знайти будь-яку точку в кімнаті, використовуючи висоту, ширину та глибину, ви можете класифікувати будь-яку математичну мову за допомогою трьох координат:

Строгість (чи трактує мова речі як статичні дані, чи як плинні форми?)
Групоїдальність (чи є рівність простою так/ні, чи це мережа шляхів?)
Стабільність (чи є логіка стандартною, чи вона квантова/ресурсозалежна, де ви не можете дублювати код?)
Частина, що піднімає розум: Розгляд коду як геометричної фігури
Найкреативніша частина статті — це те, де автори застосовують топологію (вивчення геометричних фігур, які можна розтягувати або скручувати, як-от пончики та кавові чашки) до синтаксису мов програмування.

Вони визначають синтаксичний CW-комплекс. Ось як його можна візуалізувати:

0-Виміри (Точки): Основні ключові слова мови (такі як змінна, функція, якщо/інакше).
1-Вимір (Лінії): Правила, які дозволяють переписувати або запускати код (з'єднуючи один стан коду з іншим).

2-виміри (поверхні): рівняння, що показують, що два різні шляхи виконання коду дають однаковий результат.
Вищі виміри: складні правила, які гарантують, що різні частини мови не суперечать одна одній.
Розглядаючи граматику та правила мови програмування як фізичну, багатовимірну форму, математики можуть використовувати передові інструменти (так звані когомології та спектральні послідовності) для обчислення «глобальної форми» та структурної складності всієї мережі мов.

Чому це важливо?
Зараз, якщо ви хочете, щоб комп'ютер перевірив математичний доказ (щоб ми були на 100% впевнені, що в ньому немає помилок), ви повинні перевести цей доказ у код.

Створюючи цю мережу спеціалізованих мов та показуючи, як саме вони перетворюються одна в одну, ця стаття надає структурний план майбутнього комп'ютерно-верифікованої математики, квантової фізики та наднадійного проектування програмного забезпечення.