Свята Трійця

Християнське вчення про Трійцю — це уявлення про єдиного Бога, що виступає в іпостасі Бога-Отця, Бога-Сина і Святого Духа. Доктрина обчислювального тринітаризму полягає в тому, що обчислення представляється у трьох формах: доказах висловлювань, програмах деякого типу і відображень між структурами. Кожен з цих аспектів є об'єкт поклоніння одній з трьох деномінацій: логіки, утверджує верховенство доказів і висловлювань, теорії мов програмування, що звертається в першу чергу до програм і типів, і теорії категорій, віддає першість відображенням і структурам. Основний догмат обчислювального тринітаризму свідчить, що логіки, мови програмування і категорії — всього лише маніфестації єдиного божественного поняття обчислення. Не існує найкращого шляху до просвітління, кожен з аспектів дає можливість розуміння того, що в нашому житті являє собою досвід обчислення.


Обчислювальний тринітаризм має наслідком, що будь-яка концепція, що виникла в рамках одного з трьох підходів, повинна також мати значення з точки зору двох інших. Якщо ж отриманий результат, істотний і для логіки, і для теорії типів, і для теорії категорій, то можна бути впевненим, що вдалося прояснити деяку суттєву сторону поняття обчислення, а значить, скоєно справжнє наукове відкриття. Успіхи в нашому розумінні обчислення можуть відбуватися з результатів, отриманих різними шляхами (будь-які дані корисні і доречні), а істинність результатів не залежить від їх популярності.

Логіка говорить про те, які висловлювання існують (які види думок ми хочемо вміти висловити) і що являє собою доказ (як ми можемо повідомляти наші думки інших). Мови (в тому сенсі слова, який прийнятий в інформатиці) повідомляють, які існують типи (які обчислювальні явища ми хочемо вміти висловити) і що являє собою програма (яким чином ці явища можливо здійснити). Категорії говорять про те, які існують структури (з якими математичними моделями нам доведеться працювати) і що являє собою відображення між ними (як вони ставляться один до одного). У цьому сенсі всі три підходи наказують, чому бути, а не описують те, що дано заздалегідь. І в тому ж сенсі вони являють собою підстави. Якщо припустити, що вони мають лише описової силою, питання про походження заздалегідь даних концепцій залишиться без відповіді, що знову вимагатиме звернення до проблеми підстав. Тут я хочу обговорити саме підстави, оскільки це допоможе, як я сподіваюся, виправити деякі поширені помилки щодо понять висловлювання, типу і структури. Особливо цікаво тут те, що в рамках розглянутої концепції система типів не являє собою довільний набір обмежень, що накладаються на даний заздалегідь поняття програми (незалежно від того, чи використовуються при її записі горизонтальні лінії чи ні). Швидше, система типів — це спосіб говорити про те, що в першу чергу являють собою програми і яким чином їх можна інтерпретувати як докази і відображення.

Далі я опишу основні відповідності між логікою, мовами програмування і категоріями на основі їх структурних властивостей (і поки обмежуся цим).

Центральна концепція логіки — слідування, записується у вигляді виражає виводимість . Такий запис говорить, що може бути отримана у відповідності з правилами логіки, якщо дані в якості аксіом. На відміну від структурного прямування (яке тут обговорюватися не буде), ця форма прямування не висловлює імплікації! Зокрема, слідування з пустого набору аксіом неможливо. Дотримання володіє щонайменше двома ключовими структурними властивостями, які дозволяють розглядати його як відносини предпорядка:


Крім того, часто вводяться такі додаткові структурні властивості:



Вони говорять про те, що «додаткові» аксіоми не впливають на виводимість, «зміна» аксіом не грає ролі, «подвоєння» аксіом не грає ролі. Ці умови видаються неминучими, але у так званих субструктурних логиках будь-які з цих аксіом можуть не мати місця.

В теорії мов програмування базова концепція — судження про типізації, записується як і затверджує, що є вираз типу , містить змінні типу . Судження про типізації має задовольняти наступним основним структурним властивостям:



Можна думати про змінних як про імена «бібліотек», при цьому перша властивість говорить про те, що може використовуватися будь-яка бібліотека, а друге — про замкнутості щодо компонування (як у програмі ld в Unix і аналогічних), де є результат компонування x з бібліотекою M у вираженні N. Зазвичай ми очікуємо, що аналоги аксіом «доповнення», «переупорядковування» і «подвоєння» будуть виконуватися і тут, хоча це не обов'язково. Їх формулювання залишається читачеві в якості вправи.

В теорії категорій основна концепція — концепція відображення між структурами X Y. Найпростішими прикладами є, ймовірно, множини та функції між ними, однак частіше розглядаються, наприклад, топологічні простору і неперервні відображення між ними. Відображення задовольняє аналогічним структурним властивостям:



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

Обчислювальний тринітаризм полонить мене своєю красою! Уявіть собі світ, в якому логіка, програмування і математика єдині, в якому будь-якого доказу відповідає програма, будь програмі — відображення, будь відображення — доказ! Уявіть собі світ, в якому код — це математика, де немає поділу на міркування і здійснення, немає відмінності між мовою математики і мовою обчислень. Тринітаризм — це центральний організуючий принцип теорії обчислень, інтегруючий, об'єднує і збагачує мову логіки, програмування і математики. Він дає кошти відкриття та аналізу обчислювальних явищ. Нововведення в одній області зобов'язано мати наслідки для інших. Хороша ідея хороша незалежно від того, в якій формі вона була вперше сформульована. Якщо ж якась ідея не має сенсу одночасно з логічної, теоретико-категорной і теоретико-типової точки зору — вона не може бути проявом божественного.

Джерело: Хабрахабр

0 коментарів

Тільки зареєстровані та авторизовані користувачі можуть залишати коментарі.