Про принцип Маркова, Verse Calculus и их связь с линейной логикой
Принцип Маркова это невыводимое в интуиционистской логике предикатов утверждение, которое тем не менее выполняется в вычислительной/конструктивной интерпретации оной.
Пусть у нас есть
- P(n) разрешимый предикат на натуральных числах, т.е. ∀(n : ℕ) P(n) ∨ ¬P(n) и
- доказательство, что ¬∀(n : N) P(n), то есть что этот предикат выполянется не для всех n.
Тогда мы можем начать пробовать последовательно все натуральные числа одно за другим на то, выполняется ли
это для них P(n), и заведомо найдём в какой-то момент такое, для которого ¬P(n). То есть при наших вводных, выводимо конструктивное существование
∃∀(n : ℕ) ¬P(n)
С точки зрения функционального прораммирования, фильтруя натуральные числа на предмет того, чтобы для них выполнялось ¬P(n), мы получаем ленивую последовательность всех таких чисел, а принцип Маркова гарантирует нам, что она непуста. Если мы вместо натуральных чисел возьмём произвольное непустое перечислимое множество (т.е. такое множество T, что есть сюрьекция ℕ ↠ T, а чтобы включить пустые, нужно требовать сюрьекции ℕ ↠ 1 + T), то мы тоже можем получить такую гарантированно непустую ленивую последовательность всех таких чисел, вот только порядок в ней зависит от способа нумерации.
И вот verse calculus дают нам способ работать с такими possibly infinite choice sequences (мне нравится название junctions), при которой вычисление зависит от порядка нумерации, результат в правильном смысле инвариантен относительно этого порядка. Но verse calculus не типизирован, а предположим мы сделали для него (инспирированную аффинной логикой) типизацию, где есть монада ‽T, которая делает для из любого непустого перечислимого типа T делает тип непустых junctions его значений.
В обычных зависимо-типизированных языках у нас есть тип зависимых пар (x : X, y : Y(x)) также обозначаемый Σ(x : X) Y(x). Тут нам понадобится расширить это определение для случая, когда левая переменная многозначная - тогда правая переменная тоже должна быть многозначной, сцепленной с ней, и в сценарии, где x : ?X имеет конкретное значение t, будет иметь конкретное значение типа Y(x).
Такой тип мы будем обозначать ⅋(x : ?X) Y(x).
На этом языке принцим Маркова говорит нам, что для непустого перечислимого типа T и разрешимого утверждения P(x)
q : ¬∀(n : T) P(n)
--------------
e : ⅋(n : ?T) ¬P(n)
или
q : ¬∀(n : T) P(n)
---------------
e : ?Σ(n : T) ¬P(x)
* * *
Как выясняется, мы можем отказаться от требований к типу T и предикату P (теперь не нужна ни перечислимость первого, ни разрешимость второго), если устрожим требования к доказательству q и ослабим возможности использования недетерминистской переменной e. Сейчас я постепенно объясню, как сформулировать такое утверждение (будем называть его формальным принципом Маркова).
Ещё в 1970ых [citation needed] заметил, что если запретить использование одной и той же переменной более одного раза (на самом деле, не обязательно запретить, а ограничить строгими правилами), то использование наивного правила формирования множеств не приводит к парадоксу Кантора: сформировать множество, содержащие все множества кроме самого себя, становется невозможно синтаксически. {x | x ∉ x} требует использования одной и той же переменной x дважды в такой форме. Такой контроль также позволяет амнистировать некоторые “неконструктивные доказательства” - при детальном анализе выясняется, что замкнутые доказательства от противного, где контропозитивная гипотеза используется в точности один раз, оказываются конструктивными.
В функциональном языке программирования/исчислении построений (я сейчас о Verse Calculus и Lean/Coq/Agda/Arend одновременно) можно допустить наряду с обыкновенными переменными ещё и переменные одноразовые, и тогда оказывается, что вселенную утверждений Prop можно значительно обогатить!
Наряду с интуиционистскими утверждениями (их proof-terms можно использовать сколько угодно раз в доказательствах) там добавляются ещё недекартовы утверждения. В доказательствах недекартовых утверждений, констатации/опровержения других недекартовых утверждений можно использовать лишь один раз, подробности можно почитать вот тут: https://arxiv.org/pdf/1805.07518.pdf
Я сейчас не предлагаю это читать, а расскажу оттуда некий минимум, нужный чтобы понимать о чём я говорю дальше.
Во-первых, у нас появляется на утверждениях операция -P, такая что -(-P) = P. Загвоздка в том, что для обычного декартового утверждения P его обратное утверждение -P недекартово: это оказывается как бы наше обычное ¬P := P → 𝟘, но только одноразовое. Помните я выше писал, что если в замкнутом доказательстве от противного использовать контрапозитивную гипотезу в точности один раз, то оно получается конструктивным? Вот это и даёт нам идемпотентность такого отрицания, --P = P. При этом надо понимать, что никакого волшебства тут нет - просто далеко не всякое (интуиционистское) доказательство ¬P приводимо к форме -P. Утверждение -P это более сильное утверждение, его сложнее доказать. Но зато, если получилось, то это идемпотентное отрицание.
Сейчас я опишу ещё две операции, при помощи которых формируются недекартовы типы (пока мы не добавили в язык одноразовых переменных, эти операции нам недоступны):
Пусть T некий тип значений, а P(x) предикат на нём, тогда существуют одноразовые обратимые типы
⊓(x : T) P(x) where -⊓(x : T) P(x) := ⊔(x : T) -P(x)
and
⊔(x : T) P(x) where -⊔(x : T) P(x) := ⊓(x : T) -P(x)
Они называются аддитивной (или биконструктивной) конъюнкцией и дизьюнкцией соответственно.
Использование в качестве типа X типа из двух значений позволяет получить бинарные коньюнкцию и дизьюнкцию соответственно, а использование в качестве X пустого типа - нейтральные элементы этих операций.
Биконструктивными они назваются потому что из доказательства или опровержения утверждения с таким квантором впереди всегда извлекается пример/контрпример или прямое доказательство всеобщности. Но за всё приходится платить:
Во-первых доказать ⊓/⊔(x : T) P(x) гораздо сложнее чем ∀/∃(x : T) P(x) - такое доказательство требует вот этой вот недекартовой формы с одноразовым использованием всего, и часто бывает, что ∀/∃(x : T) P(x) доказуемо, а ⊓/⊔(x : T) P(x) нет.
Во-вторых биконструктивности является одноразовость - посылку такого типа в последующем доказательстве недекартового утверждения можно применить лишь один раз.
Есть у нас и оператор !_, превращающая недекартово утверждение Q в декартово !Q с частичной потерей конструктивности:
Для декартовых предикатов P(x) (но не произвольных зависимых типов!) верно
!⊔(x : T) P(x) = ∃(x : T) P(x) ≠ -!⊓(x : T) -P(x)
и
!⊓(x : T) P(x) = ∀(x : T) P(x) ≠ -!⊔(x : T) -P(x)
[Первые равенства также выполняются, если P(x) декартов предикат, но не в случае произвольного зависимого типа P(x)]
Модальность !_ имеет структуру комонады. Есть у него и двойственный оператор, который мы уже видели - монада ?_, сопоставляющая каждому типу значений T junction type ?T всех его значений, мы правда не упомянули что тип ?T вообще говоря недекартов, и поэтому правильнее его называть не junction type, а spectral type.
На данный момент в указанной работе Майка Шульмана, на которую я выше сослался, для типов утверждений (propositional types) выводится вариант аффинной логики, но я полагаю, что такой логике подчиняются только propositional types в univalent dependently-typed verse calculus, а для включения в неё обыкновенных типов (value types) и typed junctions нам потребуется ослабить систему до bi-intuitionistic linear logic.
Теперь вернёмся к принципу Маркова, напомню как он выглядел:
q : ¬∀(n : T) P(n)
---------------
e : ?Σ(n : T) ¬P(x)
Если мы усилим требования сверху до недекартового ¬⊓(x : T) P(x), и ослабим результат снизу до недекартового ?⊔(x : T) -P(x), то безо всяких ограничений на предикат P мы получим линейно-логическое тождество
p : ¬⊓(x : T) P(x)
===============
εᵖ : ?⊔(x : T) -P(x)
Чтобы продемонстрировать его, нам понадобятся мультипликативные кванторы - уже знакомый нам
⅋(n : ?T) P(n) и более простой для понимания ⊗(n : !T) ¬P(n).
Впрочем, для демонстрации идеи давайте обойдёмся их бинарными версиями, прекрасно описанными в литературе мультипликативной конъюнкцией и дизьюнкцией, естественным образом возникающими если в качестве типа T подставить булев тип 𝔹 := {tt, ff} с ровно двумя значениями:
X ⅋ Y = ⅋(c : ?𝔹) (if c then X else Y)
X ⊗ Y = ⊗(c : 𝔹) (if c then X else Y)
Теперь давайте выведем “формальный принцип Маркова”:
¬(P ⊓ Q)
========
-!(P ⊓ Q)
=========
-(!P ⊗ !Q)
=========
-!P ⅋ -!Q
=========
?-P ⅋ ?-Q
=========
?(-P ⊔ -Q)
А теперь давайте ещё посмотрим на двойное интуиционистское отрицание ¬¬P. По законам линейной логики ¬¬P = -!(-!P) = ?(-(-!P)) = ?!P. Если посмотреть на правила поведения этого двойного оператора, получается что это propositional lax modality, давайте обозначим её через ⁰P, широко известно что эта модальность вкладывает классическую логику с исключённым третьим в линейную логику. Но это ещё не всё.
Рассмотрим тип значений T. Пользуясь уже описанными выше эквивалентностями,
!⊔(x : T) 𝟙 = ∃(x : T) 𝟙 = |T|, где знаком модуля мы обозначаем propositional truncation. Таким образом с точностью до одноразовости, получаем
p : ⁰P
======
εᵖ : ?|T|
Ой! То есть модальность ⁰_ даёт не просто классическую логику, но ещё и совместимый с унивалентностью оператор выбора эпсилон, у всякого непустого типа есть формальный (недетерминистский и одноразовый) элемент ε. Это даёт нам в точности ту неконструктивную модальность, о которой я писал в предыдущем посте, и которая позволяет внутри унивалентного и в полном смысле конструктивного (decidable typechecking, normalization, canonicity) исчисления построений иметь загончик, в котором можно заниматься классической теорией множеств с аксиомой выбора, более того оно консервативное расширение теории множеств с аксиомой выбора и соответствующим количеством вселенных.
* * *
Я предполагаю, что типизировав verse calculus, и обогатив его всеми фичами HOTT (Higher Observable Type Theory), мы получим квазивычислительную интерпретацию для би-интуиционистской линейной (или аффинной) логики. Для типов вроде натуральных чисел ℕ и булеанов 𝔹 (hereditarily-pure quotient-inductive-inductive type families) там будет выполняться честная skew-canonicity, так что это будет честная вычислительная интерпретация, а для утверждений оно даст как минимум Krivine-type realizability semantics, а в идеале, quantum game semantics.
В 1958 году великий Курт Гёдель стремясь получить убедительное доказательство непротиворечивости арифметики, придумал вычислительную интерпретацию арифметики первого порядка - Dialectica Interpretation.
Отец-основатель линейной логики Jean-Yves Girard начал свою большую карьеру с того, что развил работу Гёделя и разработал вычислительную интерпретацию для арифметики второго порядка (арифметика второго порядка достаточно выразительна, чтобы описывать и вещественный анализ).
Его линейная и аффинная логика это конечно же о том, чтобы завершить эту программу и получить вычислительную интерпретацию для “всей математики” в смысле ZFC and beyond. И сейчас уже реально виден берег.
Пусть у нас есть
- P(n) разрешимый предикат на натуральных числах, т.е. ∀(n : ℕ) P(n) ∨ ¬P(n) и
- доказательство, что ¬∀(n : N) P(n), то есть что этот предикат выполянется не для всех n.
Тогда мы можем начать пробовать последовательно все натуральные числа одно за другим на то, выполняется ли
это для них P(n), и заведомо найдём в какой-то момент такое, для которого ¬P(n). То есть при наших вводных, выводимо конструктивное существование
∃∀(n : ℕ) ¬P(n)
С точки зрения функционального прораммирования, фильтруя натуральные числа на предмет того, чтобы для них выполнялось ¬P(n), мы получаем ленивую последовательность всех таких чисел, а принцип Маркова гарантирует нам, что она непуста. Если мы вместо натуральных чисел возьмём произвольное непустое перечислимое множество (т.е. такое множество T, что есть сюрьекция ℕ ↠ T, а чтобы включить пустые, нужно требовать сюрьекции ℕ ↠ 1 + T), то мы тоже можем получить такую гарантированно непустую ленивую последовательность всех таких чисел, вот только порядок в ней зависит от способа нумерации.
И вот verse calculus дают нам способ работать с такими possibly infinite choice sequences (мне нравится название junctions), при которой вычисление зависит от порядка нумерации, результат в правильном смысле инвариантен относительно этого порядка. Но verse calculus не типизирован, а предположим мы сделали для него (инспирированную аффинной логикой) типизацию, где есть монада ‽T, которая делает для из любого непустого перечислимого типа T делает тип непустых junctions его значений.
В обычных зависимо-типизированных языках у нас есть тип зависимых пар (x : X, y : Y(x)) также обозначаемый Σ(x : X) Y(x). Тут нам понадобится расширить это определение для случая, когда левая переменная многозначная - тогда правая переменная тоже должна быть многозначной, сцепленной с ней, и в сценарии, где x : ?X имеет конкретное значение t, будет иметь конкретное значение типа Y(x).
Такой тип мы будем обозначать ⅋(x : ?X) Y(x).
На этом языке принцим Маркова говорит нам, что для непустого перечислимого типа T и разрешимого утверждения P(x)
q : ¬∀(n : T) P(n)
--------------
e : ⅋(n : ?T) ¬P(n)
или
q : ¬∀(n : T) P(n)
---------------
e : ?Σ(n : T) ¬P(x)
* * *
Как выясняется, мы можем отказаться от требований к типу T и предикату P (теперь не нужна ни перечислимость первого, ни разрешимость второго), если устрожим требования к доказательству q и ослабим возможности использования недетерминистской переменной e. Сейчас я постепенно объясню, как сформулировать такое утверждение (будем называть его формальным принципом Маркова).
Ещё в 1970ых [citation needed] заметил, что если запретить использование одной и той же переменной более одного раза (на самом деле, не обязательно запретить, а ограничить строгими правилами), то использование наивного правила формирования множеств не приводит к парадоксу Кантора: сформировать множество, содержащие все множества кроме самого себя, становется невозможно синтаксически. {x | x ∉ x} требует использования одной и той же переменной x дважды в такой форме. Такой контроль также позволяет амнистировать некоторые “неконструктивные доказательства” - при детальном анализе выясняется, что замкнутые доказательства от противного, где контропозитивная гипотеза используется в точности один раз, оказываются конструктивными.
В функциональном языке программирования/исчислении построений (я сейчас о Verse Calculus и Lean/Coq/Agda/Arend одновременно) можно допустить наряду с обыкновенными переменными ещё и переменные одноразовые, и тогда оказывается, что вселенную утверждений Prop можно значительно обогатить!
Наряду с интуиционистскими утверждениями (их proof-terms можно использовать сколько угодно раз в доказательствах) там добавляются ещё недекартовы утверждения. В доказательствах недекартовых утверждений, констатации/опровержения других недекартовых утверждений можно использовать лишь один раз, подробности можно почитать вот тут: https://arxiv.org/pdf/1805.07518.pdf
Я сейчас не предлагаю это читать, а расскажу оттуда некий минимум, нужный чтобы понимать о чём я говорю дальше.
Во-первых, у нас появляется на утверждениях операция -P, такая что -(-P) = P. Загвоздка в том, что для обычного декартового утверждения P его обратное утверждение -P недекартово: это оказывается как бы наше обычное ¬P := P → 𝟘, но только одноразовое. Помните я выше писал, что если в замкнутом доказательстве от противного использовать контрапозитивную гипотезу в точности один раз, то оно получается конструктивным? Вот это и даёт нам идемпотентность такого отрицания, --P = P. При этом надо понимать, что никакого волшебства тут нет - просто далеко не всякое (интуиционистское) доказательство ¬P приводимо к форме -P. Утверждение -P это более сильное утверждение, его сложнее доказать. Но зато, если получилось, то это идемпотентное отрицание.
Сейчас я опишу ещё две операции, при помощи которых формируются недекартовы типы (пока мы не добавили в язык одноразовых переменных, эти операции нам недоступны):
Пусть T некий тип значений, а P(x) предикат на нём, тогда существуют одноразовые обратимые типы
⊓(x : T) P(x) where -⊓(x : T) P(x) := ⊔(x : T) -P(x)
and
⊔(x : T) P(x) where -⊔(x : T) P(x) := ⊓(x : T) -P(x)
Они называются аддитивной (или биконструктивной) конъюнкцией и дизьюнкцией соответственно.
Использование в качестве типа X типа из двух значений позволяет получить бинарные коньюнкцию и дизьюнкцию соответственно, а использование в качестве X пустого типа - нейтральные элементы этих операций.
Биконструктивными они назваются потому что из доказательства или опровержения утверждения с таким квантором впереди всегда извлекается пример/контрпример или прямое доказательство всеобщности. Но за всё приходится платить:
Во-первых доказать ⊓/⊔(x : T) P(x) гораздо сложнее чем ∀/∃(x : T) P(x) - такое доказательство требует вот этой вот недекартовой формы с одноразовым использованием всего, и часто бывает, что ∀/∃(x : T) P(x) доказуемо, а ⊓/⊔(x : T) P(x) нет.
Во-вторых биконструктивности является одноразовость - посылку такого типа в последующем доказательстве недекартового утверждения можно применить лишь один раз.
Есть у нас и оператор !_, превращающая недекартово утверждение Q в декартово !Q с частичной потерей конструктивности:
Для декартовых предикатов P(x) (но не произвольных зависимых типов!) верно
!⊔(x : T) P(x) = ∃(x : T) P(x) ≠ -!⊓(x : T) -P(x)
и
!⊓(x : T) P(x) = ∀(x : T) P(x) ≠ -!⊔(x : T) -P(x)
[Первые равенства также выполняются, если P(x) декартов предикат, но не в случае произвольного зависимого типа P(x)]
Модальность !_ имеет структуру комонады. Есть у него и двойственный оператор, который мы уже видели - монада ?_, сопоставляющая каждому типу значений T junction type ?T всех его значений, мы правда не упомянули что тип ?T вообще говоря недекартов, и поэтому правильнее его называть не junction type, а spectral type.
На данный момент в указанной работе Майка Шульмана, на которую я выше сослался, для типов утверждений (propositional types) выводится вариант аффинной логики, но я полагаю, что такой логике подчиняются только propositional types в univalent dependently-typed verse calculus, а для включения в неё обыкновенных типов (value types) и typed junctions нам потребуется ослабить систему до bi-intuitionistic linear logic.
Теперь вернёмся к принципу Маркова, напомню как он выглядел:
q : ¬∀(n : T) P(n)
---------------
e : ?Σ(n : T) ¬P(x)
Если мы усилим требования сверху до недекартового ¬⊓(x : T) P(x), и ослабим результат снизу до недекартового ?⊔(x : T) -P(x), то безо всяких ограничений на предикат P мы получим линейно-логическое тождество
p : ¬⊓(x : T) P(x)
===============
εᵖ : ?⊔(x : T) -P(x)
Чтобы продемонстрировать его, нам понадобятся мультипликативные кванторы - уже знакомый нам
⅋(n : ?T) P(n) и более простой для понимания ⊗(n : !T) ¬P(n).
Впрочем, для демонстрации идеи давайте обойдёмся их бинарными версиями, прекрасно описанными в литературе мультипликативной конъюнкцией и дизьюнкцией, естественным образом возникающими если в качестве типа T подставить булев тип 𝔹 := {tt, ff} с ровно двумя значениями:
X ⅋ Y = ⅋(c : ?𝔹) (if c then X else Y)
X ⊗ Y = ⊗(c : 𝔹) (if c then X else Y)
Теперь давайте выведем “формальный принцип Маркова”:
¬(P ⊓ Q)
========
-!(P ⊓ Q)
=========
-(!P ⊗ !Q)
=========
-!P ⅋ -!Q
=========
?-P ⅋ ?-Q
=========
?(-P ⊔ -Q)
А теперь давайте ещё посмотрим на двойное интуиционистское отрицание ¬¬P. По законам линейной логики ¬¬P = -!(-!P) = ?(-(-!P)) = ?!P. Если посмотреть на правила поведения этого двойного оператора, получается что это propositional lax modality, давайте обозначим её через ⁰P, широко известно что эта модальность вкладывает классическую логику с исключённым третьим в линейную логику. Но это ещё не всё.
Рассмотрим тип значений T. Пользуясь уже описанными выше эквивалентностями,
!⊔(x : T) 𝟙 = ∃(x : T) 𝟙 = |T|, где знаком модуля мы обозначаем propositional truncation. Таким образом с точностью до одноразовости, получаем
p : ⁰P
======
εᵖ : ?|T|
Ой! То есть модальность ⁰_ даёт не просто классическую логику, но ещё и совместимый с унивалентностью оператор выбора эпсилон, у всякого непустого типа есть формальный (недетерминистский и одноразовый) элемент ε. Это даёт нам в точности ту неконструктивную модальность, о которой я писал в предыдущем посте, и которая позволяет внутри унивалентного и в полном смысле конструктивного (decidable typechecking, normalization, canonicity) исчисления построений иметь загончик, в котором можно заниматься классической теорией множеств с аксиомой выбора, более того оно консервативное расширение теории множеств с аксиомой выбора и соответствующим количеством вселенных.
* * *
Я предполагаю, что типизировав verse calculus, и обогатив его всеми фичами HOTT (Higher Observable Type Theory), мы получим квазивычислительную интерпретацию для би-интуиционистской линейной (или аффинной) логики. Для типов вроде натуральных чисел ℕ и булеанов 𝔹 (hereditarily-pure quotient-inductive-inductive type families) там будет выполняться честная skew-canonicity, так что это будет честная вычислительная интерпретация, а для утверждений оно даст как минимум Krivine-type realizability semantics, а в идеале, quantum game semantics.
В 1958 году великий Курт Гёдель стремясь получить убедительное доказательство непротиворечивости арифметики, придумал вычислительную интерпретацию арифметики первого порядка - Dialectica Interpretation.
Отец-основатель линейной логики Jean-Yves Girard начал свою большую карьеру с того, что развил работу Гёделя и разработал вычислительную интерпретацию для арифметики второго порядка (арифметика второго порядка достаточно выразительна, чтобы описывать и вещественный анализ).
Его линейная и аффинная логика это конечно же о том, чтобы завершить эту программу и получить вычислительную интерпретацию для “всей математики” в смысле ZFC and beyond. И сейчас уже реально виден берег.