...если у вас во время путешествия по Франции вдруг появится лишний денек, возьмите напрокат авто и поезжайте в город Руан. Всего полтора-два часа на северо-запад от Парижа. Это надо сделать всего ради двух вещей: снять шляпу перед великой дочерью Франции, и съесть утку по-руански в ресторане «Корона». Ни того ни другого вы больше нигде в мире сделать не сможете.
Я уже не раз говорил, что есть некоторые вещи, которые надо обязательно попробовать хоть раз в жизни. Утка по-руански в ресторане «Корона» относится к их числу. Я скажу кощунственную вещь, но я немного благодарен англосаксам, которые лишили Руан его исторической самобытности. Не случись этого, Руан непременно стал бы туристическим городом, а ресторан «Корона» — туристическим аттракционом. И вы никогда не смогли бы попробовать настоящую утку по-руански за 34 евро на две персоны.
"Номер один", Андрей Шипилов
Одной из естественных интерпретаций линейной логики является логика ресурсов. То есть, мы отказываемся от взгляда, что логические формулы обязаны описывать высказывания, и считаем, что линейная логика оперирует ресурсами. Опишем такую интерпретацию подробно.
p — может описывать наличие некоего ресурса или же запрос на ресурс p⊥
A ⊗ B — A и B одновременно в наличии (в том случае, если A и B представляют собой ресурсы, а не нужду в них, в противном случае мы нуждаемся и в A⊥ и в B⊥)
A ⊕ B — в наличии или A или B. Когда нам предлагают A ⊕ B, то согласившись мы получаем одно из них, но выбор между ними делается за нас.
A & B — можно получить A или B, но следует выбрать что именно, ресурсов хватит только на одно A или на одно B.
A ℘ B — эту связку сложно описать в ресурсной интерпретации. Легче всего её трактовать через линейную импликацию как A⊥ ⊸ B или B⊥ ⊸ A. То есть, A ℘ B не позволяет получить A и B одновременно, но этот ресурс можно пустить на создание A (при наличии B⊥) или создание B (при наличии A⊥).
A ⊸ B — из одного ресурса A можно получить один B.
!A — возобновляемый ресурс A, доступный в неограниченном количестве, мы можем запрашивать столько сколько нам нужно (в том числе, не запрашивать совсем).
?A — возможно (но не гарантируется) наличие A, если такой ресурс имеется, мы можем использовать его столько сколько нам надо.
1 — мультипликативная истина (A ⊗ 1 эквивалентно A), ресурс, который не требует других ресурсов, чтобы его произвести.
⊥ — мультипликативная ложь (A ℘ ⊥ эквивалентно A), невозможный ресурс, нет ресурсов, которые его производят.
⊤ — аддитивная истина (A & ⊤ эквивалентно A), ⊤ поглощает любое количество ресурсов. При этом !⊤ эквивалентно 1.
0 — аддитивная ложь (A ⊕ 0 эквивалентно A), 0 производит любое количество ресурсов. ?0 эквивалентно ⊥, так что 0 тоже невозможно произвести, и получив A ⊕ 0, мы можем быть уверены, что там именно A, а не 0.
В качестве примера такой интерпретации обычно приводят ресторанное меню. Не будем использовать меню руанского ресторана «Корона», который в этом году отмечает 670 лет со дня основания. Возьмём что-нибудь попроще. Положим у нас есть такое предложение:
A ⊸ B — из одного ресурса A можно получить один B.
!A — возобновляемый ресурс A, доступный в неограниченном количестве, мы можем запрашивать столько сколько нам нужно (в том числе, не запрашивать совсем).
?A — возможно (но не гарантируется) наличие A, если такой ресурс имеется, мы можем использовать его столько сколько нам надо.
1 — мультипликативная истина (A ⊗ 1 эквивалентно A), ресурс, который не требует других ресурсов, чтобы его произвести.
⊥ — мультипликативная ложь (A ℘ ⊥ эквивалентно A), невозможный ресурс, нет ресурсов, которые его производят.
⊤ — аддитивная истина (A & ⊤ эквивалентно A), ⊤ поглощает любое количество ресурсов. При этом !⊤ эквивалентно 1.
0 — аддитивная ложь (A ⊕ 0 эквивалентно A), 0 производит любое количество ресурсов. ?0 эквивалентно ⊥, так что 0 тоже невозможно произвести, и получив A ⊕ 0, мы можем быть уверены, что там именно A, а не 0.
В качестве примера такой интерпретации обычно приводят ресторанное меню. Не будем использовать меню руанского ресторана «Корона», который в этом году отмечает 670 лет со дня основания. Возьмём что-нибудь попроще. Положим у нас есть такое предложение:
Суп или салат на выбор
Основное блюдо: пицца или паста
На десерт: мороженное или сорбет
(в зависимости от наличия)
Кофе или чай (неограниченно)
Стоимость: 50 гривен
Его можно представить в виде следующей формулы:
50 грн. ⊸ (суп & салат) ⊗ (пицца & паста) ⊗ (мороженное ⊕ сорбет) ⊗ !(кофе & чай)
Можно заметить, что «или» в «суп или салат» представлено как &, поскольку выбор совершает клиент (а заведение должно иметь возможность приготовить и то и другое), но «мороженное или сорбет» использует ⊕, так как здесь выбор осуществляет заведение. Формулу можно переписать с использованием ℘:
(50 грн.)⊥ ℘ ((суп & салат) ⊗ (пицца & паста) ⊗ (мороженное ⊕ сорбет) ⊗ !(кофе & чай))
Таким образом, «мультипликативное или» можно трактовать как дилемму, которая задана извне. В такой ситуации мы можем потратить 50 гривен на обед или же просто заключить, что нам нужно 50 гривен, чтоб не остаться голодными, какое-либо разрешение этой дилеммы затрагивает обе части формулы (другим примером аналогичной дилеммы может служить «жизнь или кошелёк»).
В ресурсной интерпретации логики, заметно, что часть логических связок отвечает за наличие ресурсов прямо сейчас, а другая, скорее, связана с возможностью их получения. Также заметно, что формулы линейной логики описывают взаимодействие между двумя сторонами: между клиентом и рестораном, между доказывающим и его оппонентом, между программой и её окружением. Причём одни логические связки (⊗, ⊕, !) естественно связывать с одной стороной взаимодействия, а другие (&, ℘, ?) с противоположной. Такой феномен носит называние полярности. Мы его ещё будем обсуждать подробно, но прежде мы попытаемся ответить на вопрос, который должен был возникнуть у читателя: что, собственно, линейного в линейной логике?
Комментариев нет:
Отправить комментарий