Вычислительное триличие 2.0
Введение
Перед вами очередная попытка осмыслить статью Харпера The Holy Trinity.
Ключевая идея статьи в том, что логика, языки и категории суть ипостаси вычисления. В рамках каждой из ипостасей существует фундаментальная концепция (fundamental concept). В логике — логическое следствие (entailment). В языках — суждение о типизации (typing judgment). В категориях — отображение¹ (mapping).
И, вроде бы, всё хорошо, но что-то смущает… В первой части статьи утверждается, что высказывание соответствует типу и структуре, а доказательство — программе и отображению. Но во второй части логическое следствие сопоставляется с суждением о типизации и… отображением! Таким образом с одной стороны может показаться, что отображение соответствует логическому следствию и суждению о типизации, а с другой — доказательству и программе. Попытаемся объяснить идею Харпера в терминах понятных обычному программному инженеру.
Суждение
Назовём форму, описывающую фундаментальную концепцию, суждением (judgment). Всё, что слева от символа турникета (turnstile) называется контекстом (context). Контекст — это всё, что есть у агента (опыт, знания, ресурсы, способности и т.д. и т.п.). Таким образом любое суждение всегда фиксируется в контексте некоторого агента.
Логика
Начнём с логики. В логике фундаментальной концепцией является логическое следствие, которое фиксирует осуществимость (derivability) некоторого высказывания (proposition). Небольшая проблема заключается в том, что в логической нотации нет средств, которые позволили бы явно показать осуществимость и доказательство. Всё это как бы спрятано в правой части логического следствия.
Языки
В языках фундаментальной концепцией является суждение о типизации, которое фиксирует выразимость² (expressibility) некоторого типа (type). Тут уже нотация гораздо богаче и позволяет увидеть всё в полном объёме. В оригинальной статье нет понятия аналогичного выразимости, но оно необходимо для полноценного соответствия между ипостасями.
Категории
В категориях фундаментальной концепцией является суждение об отображении, которое фиксирует отобразимость³ (mappability) некоторой структуры (structure). В оригинальной статье нет понятий аналогичных суждению об отображении и отобразимости, но они необходимы для полноценного соответствия между ипостасями.
Соответствия
Таким образом ипостаси соотносятся⁴ следующим образом:
UPD1:
- Более чётко сформулирована проблема исходной статьи.
- Доказуемость заменена на осуществимость.
TODO:
- Добавить про вычислимость.
[1]: Далее в статье вводится понятие суждения об отображении.
[2]: Считаем, что выразимость и программируемость — синонимы. То же самое относится к выражениям и программам.
[3]: Считаем, что отображение и морфизм — синонимы. Понятие отобразимости чуть лучше передает следующий смысл:
A central theme in category theory is the study of structures and structure-preserving maps. A map f : X → Y is a kind of observation of object X via a specified relationship it has with another object, Y. For example, think of X as the subject of an experiment and Y as a meter connected to X, which allows us to extract certain features of X by looking at the reaction of Y.
Brendan Fong, David I Spivak https://arxiv.org/abs/1803.05316
[4]: Подробнее о соотношении https://ncatlab.org/nlab/show/computational+trinitarianism
