В 1934 году Генцен ввёл исчисления секвенций для классической (LK) и интуиционистской (LJ) логики.

Секвенция или «условное суждение» состоит из суждения Σ и контекста Г, в котором оно верно. Записываются секвенции вот так:

Г ⊢ Σ

В интуиционистском исчислении LJ суждениями Σ являются просто формулы логики первого порядка, а контекстами Г конечные списки таких формул. То есть в конечном итоге секвенции LJ имеют следующий вид:

A, B,.., C ⊢ R

Тут подразумевается, что формула R доказуема (интуиционисткая логика отражает доказуемость), если доказуемы формулы A, B, ... и C. Пустой контекст тоже допустим: ⊢ R означает, что формула R доказуема без каких либо дополнительных условий.

В исчислении LK (классическая логика отражает истинность) cеквенции симметричные, там суждение (то есть то, что стоит справа от ⊢, иногда эту часть ещё называют коконтекстом) — не одна формула, а список формул, как и контекст. Там подразумевается, что вывод может быть недетерминистским:

A, B ⊢ X, Y 

означает, что из истинности A и B следует истинность X или Y (или и того, и другого). В LK допустим не только пустой контекст, но и пустое суждение: Г ⊢ контекст противоречив, т.е. содержит противоречащие друг другу утверждения, или внутренне противоречивые (“тавтологически ложные”) утверждения.

Основное содержание исчисления секвенций — правила вывода. Правило вывода образует конечный набор секвенций-посылок, которые пишутся над чертой, и секвенцию-результат под чертой. Примеры:

 Г ⊢ A    Г ⊢ B
————————————————
   Г ⊢ (A ∧ B)

   Γ, A ⊢ B
——————————————
 Γ ⊢ (А -> B)
 
———————
 A ⊢ A
 
 Г ⊢ A   A ⊢ Σ
———————————————
     Г ⊢ Σ

Дерево, построенное из правил вывода называется деревом вывода. В исчислении секвентов именно дерево вывода служит доказательством.

Для системы LJ существует, однако, другой способ трактовать контексты и суждения, а именно — как типы переменных (со стороны контекста) и выражений (со стороны суждения), а правила вывода — это правила построения выражений. Теперь контект в LJ это список элементов вида “x : T”, читающихся как “пусть x переменная типа T” или “пусть x доказательство формулы T”, а суждения имеют вид expr : T и читаются ”тогда можно построить выражение expr типа T” или “тогда выражение expr доказательство формулы T”. В этой системе не нужно таскать за собой дерева вывода — выражение уже хранит в себе дерево собственного вывода с точностью до эквивалентности деревьев.

Рассмотрим, как будут трактоваться приведённые согласно этому подходу:

———————————————
 a : A ⊢ a : A
 
 Словами: в контексте, состоящем из переменной
 a типа A можно построить выражение a типа A.

 Г ⊢ a : A    Г ⊢ a : B
—————————————————————————
   Г ⊢ (a, b) : (A ∧ B)

Словами: Пара (a, b) доказательств a утверждения A и b
утверждения B является доказательством утверждения A ∧ B.

      Γ, x : A ⊢ expr(x) : B
——————————————————————————————————
 Γ ⊢ (x̲ : A) ↦ expr(x) : (А -> B)
 
 
 Словами: если в контексте, содержащем переменную x типа A
 можно построить выражение expr, содержащее переменную x,
 типа B, то в том же контексте без переменной x можно
 построить выражение `(x̲ : A) ↦ expr(x)` типа `A -> B`.
 
  Г ⊢ x : A   x : A ⊢ y : B
————————————————————————————
       Г ⊢ y(x) : B
       
Словами: в выражение с переменной типа A можно подставить
выражение типа A.

Получившаяся система называется просто-типизированным лямба-исчислением. Если начать допускать в качестве типов переменных и выражений не только утверждения, но и ещё что-нибудь (например, точки на эвклидовой плоскости, полуплоскости и окружности) то при помощи выражения смогут выражать не только доказательства, но и другие типы построений (например, геометрические построения). Если же в качестве дополнения к базовым типам разрешить конечные множества, натуральные числа, а также пары, списки и деревья таковых, получатся типизированные в сильном смысле* функциональные языки программирования.

(* Всякое выражение имеющее тип имеет нормальную форму, т.е. типизированные вычисления не имеют права “зависнуть”.)

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

a : A, b : B ⊢ expr₁ : X, expr₂ : Y 

как “в указанном контексте можно построить два параллельных (возможно коммуницирующих друг с другом) вычислительных потока, возвращающие объекты типов X и Y соответственно”. Обратите внимание на использование слова “объект” вместо “значение” — дело в том, что при переходе к многопоточности возникают объекты, которые в отличие от значений не могут быть “клонированы”:

• В лямбда-исчислениях выражения типа X -> Y самодостаточны, в частности по этому они называются во многих языках программирования «замыканиями». Внутри них не происходит никакого “взаимодействия со внешним миром”, результат полностью детерминирован вводом, и никаких побочных эффектов вычисление не имеет, так что функции f : X -> Y могут рассматриваться как значения, и совершенно не важно сколько раз переменная такого типа была задействована.
• В многопоточном случае выражение “p : X -> Y” может коммуницировать с другими параллельными вычислительными потоками. В частности, для любого типа X мы можем вывести

⊢ p₁ : X, p₂ : (X -> Unit)

где через Unit мы обозначем тип значений с единственным значением (). Тут параллельно запущены два потока p₁ и p₂. Если рассматривать, как если бы они были замкнутыми вычислениями, выходило бы что p₁ не весть откуда наколдовывает значение типа X, а p₂ принимает аргумент типа X, но это совершенно не важно, потому что результат вычисления не зависит от аргумента — это в любом случае будет (), потому что других значений типа Unit не бывает. На самом же деле, у p₂ просто есть побочный эффект — он передаёт аргумент потоку p₁, который в свою очередь возвращает его в качестве значения. Если мы рассматриваем всю систему в целом, её поведение детерминистично и не имеет побочных эффектов, однако если рассматривать фрагмент, возникают побочные эффекты и недетерминизм. Чтобы создать аналог лямбда-исчисления, поддерживающий коммуницирующие вычислительные потоки, нам понадобится сперва развить вариант LK исчисления, поддерживающий помимо типов значений ещё и типы объектов и, соответственно, переменные, которые могут быть использованы вычислительно лишь один раз.

К счастью, такое исчисление секвенций уже разработал J.Y. Girard, и называется оно линейная логика. На в процессе развития системы естественной дедукции для этого исчисления секвенций мы выясним и то, каким образом типизировать части системы так, как будто бы они были автономны, но с побочными эффектами (“коммуникационным протоколом со внешним миром”) и недетерминизмом. Такая типизация позволит нам моделировать интерактивные программы, где роль внешнего мира играет пользователь или неизвестная third party-система.

Удивительным образом, эта же система может быть без больших усилий расширена для моделирования квантовых явлений: в квантовой механике так же при рассмотрении замнутой системы целиком не возникает недетерминизма, однако при выделении наблюдаемой подсистемы возникает истинный недетерминизм. Согласно текущим представлениях о космологии и квантовой теории поля, если мы рассматриваем не изолированную лабораторную систему в ящике, а систему погруженную в окружающий мир, мы имманентно имеем дело с наблюдаемой подсистемой, т.к. из-за расширения вселенной, горизонт наблюдаемой вселенной конечен и за этот горизонт постоянно утекает “часть системы”. Более того, по этой же причине в каждой точке вселенной заряженные частицы в небольшой мере сцеплены с “изотермическим фоном инфрачастиц” — фотонов столь низкой энергии, что из-за конечности диаметра наблюдаемой вселенной, они не смогут быть измерены никогда в принципе. Добавив логическое исчисление такой “бесоконечный термический резервуар” (своего рода заземление для энтропии), можно получить квантовое лямбда-исчисление — язык программирования, на котором можно записывать не только обыкновенные, но и квантовые вычисления.

Рассмотрим правило вывода лямбда-выражений:

      Γ, x : X ⊢ y(x) : Y
——————————————————————————————————
 Γ ⊢ (x̲ : X) ↦ y : (А -> B)

В симметричном исчислении нам нужно учитывать, что справа ещё может быть ещё коконтекст Σ, а вместо стрелки в линейной логике используется значок “⊸”, так что правило выглядит вот так:

      Γ, x : X ⊢ y(x) : Y, Σ
——————————————————————————————————
 Γ ⊢ (x̲ : X) ↦ y(y) : (А ⊸ B), Σ

Отметим, что мы подразумеваем, что внутри Σ переменная x не используется. Но так как в линейной логике всякая переменная может и должна использоваться ровно один раз, мы можем это не уточнять.

Авторы λ⅋-исчисления F. Aschieri и др. [1], совершили любопытное наблюдение, что линейный формализм допускает вариант, чтобы переменная как раз использовалась в коконтексте Σ, но не использовалась выражении y, получилась вот такая конструкция:

      Γ, x : X ⊢ y : Y, Σ(x)
——————————————————————————————————
 Γ ⊢ (x̅ : X; y) : (А ⊸ B), Σ(x)

Т.е. выражение (x̅ : X; y) вводит в оборот коммуникационный канал под названием x, который может (и должен) быть единожды использован в одном из параллельных потоков. Применение выражения такого вида к объекту o сперва посылает аргумент в тот параллельный поток, где x используется, а затем продолжает выполнение y.

Теперь мы можем построить пример коммуницирующих процессов, приведённый в предыдущем разделе:

 ———————————————      —————————————
  x : X ⊢ x : X        ⊢ () : Unit
—————————————————————————————————————
     x : X ⊢ x : X, () : Unit
 ——————————————————————————————————
  ⊢ x : X, (x̅ : X; ()) : X ⊸ Unit