Линейная логика I

Линейная логика вспомнилась мне, когда я разбирался с rvalue-ссылками в C++11. Не то чтобы новый тип ссылок имеет много общего с линейной логикой, но некоторые аспекты схожи. Добавление rvalue-ссылок - это попытка разграничить в языке значения долгоживущие и временные, а также предоставить способ поглощать значения временные, используя их внутреннюю структуру для новых значений. 

Для программистов на C++ эффективная работа с временными значениями нужна, во-первых, потому что эффективность работы программы ставится во главу угла разработчиками языка, во-вторых, потому что это позволяет писать код естественным образом - так, чтобы результат операции был выражен её возвращаемым значением, даже если это вектор с кучей значений внутри - теперь такой естественный стиль является также эффективным, что приятно. 

Люди, которые разрабатывали rvalue-ссылки, правда, немного намудрили с дизайном - и теперь даже для того чтобы разобраться, где собственно rvalue-ссылка, а где нет, нужен некоторый навык. Но это у них так принято.

Что же общего у линейной логики и нового C++? Формальная логика обычно представляется системой оперирующей высказываниями, для которых мы можем установить их истинность (или ложность). Как правило, речь идет о высказываниях, для которых истинность может быть установлена раз и навсегда. Это величина константная и вечная. Высказывание нельзя потратить, израсходовать. Но для линейной логики это не совсем так. Она имеет дело как с высказываниями, так и с командами/действиями. Единожды совершённое действие не обязательно можно повторить. Таким образом, в линейной логике наличествуют величины расходуемые, временные.

На C++ линейная логика, по всей видимости, не оказала влияния. Но некоторые языки программирования, вышедшие из академической среды, явно или неявно используют концепции, вдохновлённые линейной логикой. Считается, что для самих логиков эта формальная система не столь важна, как для computer science.

Я постараюсь рассказать о линейной логике и её моделях в разных областях математики и не только. Но начать нужно издалека. Прежде чем говорить о линейной логике, имеет смысл рассказать о логике интуиционистской (ИЛ) и её отличиях от классической логики (КЛ), и о связи логики и программирования. В некотором смысле это будет историческим подходом - линейная логика была обнаружена при попытке построить простые модели ИЛ, и её открытие дало систему, в которой можно примирить две логики и прояснить их различия.

Пишу я во многом для того, чтобы разобраться самому. Вероятно, у меня будут встречаться ошибки и неточности - я постараюсь их избежать, но отсутствие гарантировать не могу.