...Этот способ выйти из затруднения равносилен утверждению, что квантовомеханические уравнения движения перестают быть линейными, а точнее, становятся чрезвычайно нелинейными, когда речь заходит о существах, наделённых сознанием.
"Замечания относительно вопроса о соотношении сознания и тела",
Юджин Вигнер
Юджин Вигнер
Для того чтобы понять, почему линейную логику назвали линейной, рассмотрим аналогию между высказываниями и аналитическими функциями. Напомню, что функция называется аналитической в окрестности какой-то точки x0, если она представима в виде степенного ряда:
f (x) = a0 + a1 (x - x0) + a2 (x - x0)2 + ...
Если будем трактовать x в степени n как использование x n раз, то ключевое для линейной логики требование использования x ровно один раз даст нам функции, задающие прямые линии:
f (x) = с + a x
то есть линейные функции.
Вообще, слово линейный в математике имеет два разных смысла: операционный и алгебраический. Функция является линейной в операционном смысле, если использует аргумент ровно один раз (то есть так, как у нас получилось выше), линейная в алгебраическом смысле функция ‒ это функция, которая сохраняет какую-то операцию, например:
F(A + B) = F(A) + F(B)
Здесь F ‒ линейная по отношению к операции сложения. (Но это не обязательно должно быть сложение, сама операция может иметь разный смысл для A, B и F(A), F(B), это может быть разное сложение). Что замечательно, при рассмотрении разных математических моделей линейной логики, в том числе той, которая привела к открытию линейной логики (в модели когерентных пространств), линейная импликация ставится в соответствие функциям линейным уже в алгебраическом смысле.
В этой модели каждой логической формуле ставится в соответствие так называемое когерентное пространство, которое можно представлять как ненаправленный граф. Вершинами графа служат некие базовые объекты ‒ сведения, атомарные высказывания, ресурсы и т.д. Ребра обозначают совместимость, когерентность двух таких объектов. Конструкции, которые нас интересуют, представляют собой полные подграфы¹ такого графа, то есть множества объектов, которые совместимы друг с другом. Полные подграфы еще называют кликами (название произошло от клики как группы людей). Именно они считаются элементами пространства когерентности.
Логические связки конструируют новые графы на основе существующих. Так A ⊗ B будет графом пар (a, b), две пары когерентны друг другу, только если когерентны компоненты этих пар. A ⊕ B будет размеченным объединением² двух графов, в котором не появляется новых связей. Вообще, мультипликативные связки представлены парами, а аддитивные ‒объединениями. Так, A & B тоже будет размеченным объединением двух графов, в котором дополнительно любой объект из A связан с любым объектом из B. Это следует из правил де Моргана и определения линейного отрицания A⊥. Граф A⊥ совпадает по вершинам с графом A, но в A⊥ два разных объекта связаны друг с другом, когда они не связаны между собой в A.
В такой модели импликация A ⇒ B задаёт набор функций на кликах. Нам, правда, подойдут не все функции, а только обладающие набором хороших свойств. К примеру, если a является подграфом b, то f (a) должна быть подграфом f (b) и тому подобные. Множеству таких функций можно сопоставить когерентное пространство. Линейная импликация A ⊸ B задаёт набор функций, для которых
Заметим, что эта операция объединения в самом формализме линейной логики отсутствует. Её можно трактовать как операцию смешивания двух однотипных ресурсов. При такой трактовке соблазнительно еще учитывать числовую меру ресурсов, их количество. В такой формальной системе можно говорить об операции дифференцирования, то есть об операции поиска линейного приближения A ⊸ B нелинейной функции A ⇒ B. Называется такая система дифференциальной линейной логикой, это направление успешно развивается с начала двухтысячных. Другим применением такого смешивания может быть логика квантовой механики, тогда под количеством ресурса мы подразумеваем вероятность события. Вообще, концепция линейности весьма близка квантовой механике, в которой квантовое состояние невозможно скопировать.
На том же перекрёстке computer science (а после обнаружения соответствия Карри-Ховарда логика неотделима от computer science) и квантовой механики находится дисциплина квантовых вычислений. Вполне логично, что языки программирования, предлагаемые для квантовых вычислений, строятся на различных вариациях линейной логики. Правда, линейная логика может пригодиться и для обычных вычислений. Об этом в следующий раз.
В этой модели каждой логической формуле ставится в соответствие так называемое когерентное пространство, которое можно представлять как ненаправленный граф. Вершинами графа служат некие базовые объекты ‒ сведения, атомарные высказывания, ресурсы и т.д. Ребра обозначают совместимость, когерентность двух таких объектов. Конструкции, которые нас интересуют, представляют собой полные подграфы¹ такого графа, то есть множества объектов, которые совместимы друг с другом. Полные подграфы еще называют кликами (название произошло от клики как группы людей). Именно они считаются элементами пространства когерентности.
Логические связки конструируют новые графы на основе существующих. Так A ⊗ B будет графом пар (a, b), две пары когерентны друг другу, только если когерентны компоненты этих пар. A ⊕ B будет размеченным объединением² двух графов, в котором не появляется новых связей. Вообще, мультипликативные связки представлены парами, а аддитивные ‒объединениями. Так, A & B тоже будет размеченным объединением двух графов, в котором дополнительно любой объект из A связан с любым объектом из B. Это следует из правил де Моргана и определения линейного отрицания A⊥. Граф A⊥ совпадает по вершинам с графом A, но в A⊥ два разных объекта связаны друг с другом, когда они не связаны между собой в A.
 |
| Клика как она есть |
f (a ∪ b) = f (a) ∪ f (b),
то есть линейных относительно операции объединения графов³. Такие функции достаточно задать на одно-элементных подграфах ‒ это полностью определит их поведение.Заметим, что эта операция объединения в самом формализме линейной логики отсутствует. Её можно трактовать как операцию смешивания двух однотипных ресурсов. При такой трактовке соблазнительно еще учитывать числовую меру ресурсов, их количество. В такой формальной системе можно говорить об операции дифференцирования, то есть об операции поиска линейного приближения A ⊸ B нелинейной функции A ⇒ B. Называется такая система дифференциальной линейной логикой, это направление успешно развивается с начала двухтысячных. Другим применением такого смешивания может быть логика квантовой механики, тогда под количеством ресурса мы подразумеваем вероятность события. Вообще, концепция линейности весьма близка квантовой механике, в которой квантовое состояние невозможно скопировать.
На том же перекрёстке computer science (а после обнаружения соответствия Карри-Ховарда логика неотделима от computer science) и квантовой механики находится дисциплина квантовых вычислений. Вполне логично, что языки программирования, предлагаемые для квантовых вычислений, строятся на различных вариациях линейной логики. Правда, линейная логика может пригодиться и для обычных вычислений. Об этом в следующий раз.
¹ То есть графы, у которых все вершины соединены ребрами.
² Объединением, в котором известно происхождение элемента, из левой ли он части или из правой.
² Объединением, в котором известно происхождение элемента, из левой ли он части или из правой.
³ При объединении мы берем все вершины двух графов, и все ребра, которыми эти вершины связаны в базовом графе. Надо учесть, что мы рассматриваем функции на кликах, а объединение двух клик не обязательно будет кликой, так что формула не всегда имеет смысл.
Комментариев нет:
Отправить комментарий