lection12.tex

\section{Линейные типы}

Все системы типов, которые мы ранее рассматривали, были так или иначе основаны
на интуиционистской логике. В данном разделе мы немного отступим в сторону и
приведем пример системы типов, основанной на логике, существенно отличающейся 
от интуиционистской.

Линейная логика была предложена Жираром в ... Основная ее мотивация - попытка
в логических выражениях учесть стоимость тех или иных утверждений. В самом деле,
традиционная интерпретация интуиционистской логики предполагает, что если 
некоторое утверждение $A$ доказано, то это утверждение может быть использовано
в дальнейшем рассуждении сколько угодно раз без дополнительных затрат. Однако,
поскольку мы живем в реальном мире, такой взгляд на вопрос есть упрощение.

Вспомним традиционную интерпретацию интуиционистской логики --- например,
импликация $A \rightarrow B$ есть метод получения по утверждению $A$ утверждения $B$.
Но, к сожалению, в реальном мире часто превращение объекта $A$ в объект $B$ 
разрушает исходный объект. Линейная логика предлагает способ учесть это в 
логических рассуждениях. 

Рассмотрим выражение $A \multimap B$ (связка $\multimap$ читается как lollipop --- 
леденец): будем говорить, что из $A$ можно получить $B$, если материальный объект 
$A$ можно превратить в материальный объект $B$. Например, утверждение, что 
за $31$ рубль можно получить в кассе метрополитена один жетон на проезд можно
записать как $\texttt{31 рубль}\multimap\texttt{жетон}$. В рамках этой аналогии
утверждение $\texttt{31 рубль}\multimap\texttt{жетон}, \texttt{31 рубль}\vdash\texttt{31 рубль}\varotimes\texttt{жетон}$
не может быть доказано: ведь превратив 31 рубль в жетон, мы не сможем больше этими 31 рублями пользоваться.

%Мы использовали уже еще одну дополнительную связку (&)

Например, мы можем показать, что $\langle !(A \& B) \rangle \vdash !A \varotimes !B$ и
$\langle !A \varotimes !B \rangle \vdash !(A \& B)$.
Поясним первое выражение: если у нас есть неограниченный источник одноразовых автоматов, 
умеющих выдать $A$ или $B$ по нашему выбору, то это то же самое, что иметь два специализированных 
автомата, выдающих неограниченное количество $A$ (первый автомат) и $B$ (второй автомат).

Часто в исчислении рассматривают еще одну (парную к $\&$) связку ($!(A\parr B) = !A\varoplus !B$), 
но содержательно к нашему рассуждению она ничего не добавит, поэтому для простоты мы ее
опустим.

Помимо двуместных связок, имеющих прямые аналогии в интуиционистской логике, мы введем новую
одноместную связку, называемую экспонентой или <<точно>>.

Линейная логика в некотором смысле эквивалентна интуиционистской:
\begin{theorem}
Каково бы ни было выражение $X$ в интуиционистской логике, найдется выражение $X^\circ$
в линейной.
\end{theorem}

В прямую сторону доказательство тривиально --- если стереть все $!$, 
превратить $\varotimes$ и $\&$ в $\cap$, а $\varoplus$ и $\parr$ --- в $\vee$, 
то мы получим аксиомы интуиционистской логики.
Обратное утверждение можно показать с помощью \emph{стандартного} вложения интуиционистской логики
в линейную:

\begin{tabular}{ll}
Интуиционистская связка & Аналог в линейной логике \\
\hline
$A \rightarrow B$ & $!A \multimap B$\\
$A \cap B$ & $A \& B$\\
$A \vee B$ & $!(!A \varoplus !B)$
\end{tabular}

Особую важность в линейной логике играют структурные правила: правило ослабления и правило 
сжатия:

Правило ослабления позволяет уничтожать значения:
$$\infer{\vdash A\rightarrow B}{}$$

Если мы впрямую построим по такой системе типовую систему для лямбда-исчисления, мы
не добьемся нашей цели: ведь мы всегда можем превратить значение из линейного типа
в интуиционистский и наоборот. 
Для этой цели мы запретим превращения и построим две параллельные теории.