Карри-Говард и программы из неконструктивных доказательств

Это дополнительный вопрос к

В чем разница между доказательствами и программами (или между предложениями и типами)?

Какая программа будет соответствовать неконструктивному (классическому) доказательству вида ? (Предположим, что является интересным разрешимым отношением, например, тая TM не останавливается за шагов.) $\forall k \ T(e,k) \lor \lnot \forall k \ T(e,k)$ $T$ $e$ $k$

(ps: я публикую этот вопрос отчасти потому, что мне интересно узнать больше о том, что Нил подразумевает под « переводом Годеля-Генцена - трансформация продолжения» в его комментарии .)

lo.logic pl.programming-languages proof-theory Кава
источник

Частичный ответ на странице 2 этих конспектов . Это немного загадочно; Я постараюсь откопать что-нибудь более полное.

Дейв Кларк,

Написание моего ответа занимает немного больше времени, чем планировалось, поскольку я допустил ошибку, решив доказать то, что я знал, а не просто утверждать их. :)

Нил Кришнасвами

У последней JSL была эта статья . Суть в том, что вычислительное содержание классических доказательств может сильно зависеть от того, как вы решили его извлечь. Я действительно еще не переварила это, но я думала, что брошу это туда.

Марк Рейтблатт

Но вы указали, что T является разрешимым отношением, поэтому из этого следует, что существуют конструктивные доказательства вашего предложения. Классическая логика является подмножеством интуиционистской логики, и вы указали, что T принадлежит этому подмножеству, назвав его разрешимым.

Рен Романо

Рен, это то, что я тоже думал сначала! Но предложение P в примере P \ / ~ P в вопросе, является ли оно фактически количественным по всем k, и это количественное определение T не обязательно разрешимо.

Jbapple

Ответы:

Это интересный вопрос. Очевидно, нельзя ожидать наличия программы, которая решает для каждого , выполняется ли или нет, так как это решило бы проблему остановки. Как уже упоминалось, существует несколько способов вычислительной интерпретации доказательств: расширения Карри-Ховарда, реализуемость, диалектика и так далее. Но все они вычислили бы теорему, которую вы упомянули, более или менее следующим образом. $e$ $\forall k T(e, k)$

Для простоты рассмотрим эквивалентную классическую теорему

(1) $\exists i \forall j (\neg T(e, j) \to \neg T(e, i))$

Это (конструктивно) эквивалентно упомянутому, потому что, учитывая мы можем решить, выполняется ли или нет, просто проверив значение . Если выполнено, то и, следовательно, . Если, с другой стороны, не выполняется, то в силу (1) имеем что влечет . $i$ $\forall k T(e, k)$ $\neg T(e, i)$ $\neg T(e, i)$ $\exists i \neg T(e, i)$ $\neg \forall i T(e, i)$ $\neg T(e, i)$ $\forall j (\neg T(e, j) \to \bot)$ $\forall j T(e, j)$

Теперь снова мы не можем вычислить в (1) для каждого заданного потому что мы снова решили бы проблему остановки. То, что сделали бы все упомянутые выше интерпретации, это посмотреть на эквивалентную теорему $i$ $e$

(2) $\forall f \exists i' (\neg T(e, f(i')) \to \neg T(e, i'))$

Функция называется функцией Хербранда. Он пытается вычислить контрпример для каждого данного потенциального свидетеля . Ясно, что (1) и (2) эквивалентны. Слева направо это конструктивно, просто возьмите в (2), где - предполагаемое свидетельство (1). Справа налево нужно рассуждать классически. Предположим, (1) не было правдой. Затем, $f$ $j$ $i$ $i' = i$ $i$

(3) $\forall i \exists j \neg (\neg T(e, j) \to \neg T(e, i))$

Пусть будет функцией, свидетельствующей об этом, т.е. $f'$

(4) $\forall i \neg (\neg T(e, f'(i)) \to \neg T(e, i))$

Теперь возьмем в (2) и получим для некоторого . Но, взяв в (4), мы получим отрицание этого противоречия. Отсюда (2) влечет (1). $f = f'$ $(\neg T(e, f'(i')) \to \neg T(e, i'))$ $i'$ $i = i'$

Итак, мы имеем, что (1) и (2) классически эквивалентны. Но интересно то, что (2) теперь имеет очень простое конструктивное свидетельство. Просто возьмите если не выполняется, потому что тогда вывод (2) верен; или же возьмите если выполняется , потому что тогда не выполняется, и предпосылка (2) ложна, что делает его снова верным. $i' = f(0)$ $T(e, f(0))$ $i' = 0$ $T(e, f(0))$ $\neg T(e, f(0))$

Следовательно, способ вычислительной интерпретации классической теоремы, подобной (1), состоит в том, чтобы посмотреть на (классически) эквивалентную формулировку, которая может быть конструктивно доказана в нашем случае (2).

Упомянутые выше различные интерпретации расходятся только в том, как всплывает функция . В случае реализуемости и интерпретации диалектики это явно дается интерпретацией в сочетании с некоторой формой отрицательного перевода (например, Геделя-Генцена). В случае расширений Curry-Howard с операторами call-cc и продолжением функция возникает из-за того, что программе разрешено «знать», как будет использоваться определенное значение (в нашем случае ), поэтому является продолжением программы около точки, где вычисляется. $f$ $f$ $i$ $f$ $i$

Другим важным моментом является то, что вы хотите, чтобы переход от (1) к (2) был «модульным», т. Е. Если (1) используется для доказательства (1 '), то его интерпретация (2) должна использоваться аналогичным образом. чтобы доказать толкование (1 '), скажите (2'). Все упомянутые выше интерпретации делают это, включая отрицательный перевод Геделя-Генцена.

Пауло
источник

Добро пожаловать! Приятно видеть здесь эксперта-теоретика доказательств.

Нил Кришнасвами

Спасибо, Пауло, ваш ответ прояснил часть картины в связанной проблеме, над которой я работаю.

Каве

Хорошо известно, что классическая и интуиционистская арифметика равнозначны.

Одним из способов показать это является «негативное вложение» классической логики в интуиционистскую логику. Итак, пусть - формулы классической арифметики первого порядка. Теперь мы можем определить формулу интуиционистской логики следующим образом: $\phi$

\begin{array}{lcl} G (⊤) & = & \neg \neg ⊤ \\ G (ϕ \land ψ) & = & \neg \neg (G (ϕ) \land G (ψ)) \\ G (⊥) & = & \neg ⊤ \\ G (\neg ϕ) & = & \neg G (ϕ) \\ G (ϕ \lor ψ) & = & \neg (\neg G (ϕ) \land \neg G (ψ)) \\ G (\forall x . ϕ) & = & \forall x . \neg \neg G (ϕ) \\ G (\exists x . ϕ) & = & \neg \forall x . \neg (G (ϕ)) \\ G (P) & = & \neg \neg P \end{array}

$\begin{array}{lcl} G(\top) & = & \lnot\lnot\top \\ G(\phi \land \psi) & = & \lnot\lnot(G(\phi) \land G(\psi)) \\ G(\bot) & = & \lnot\top \\ G(\lnot\phi) & = & \lnot G(\phi) \\ G(\phi \vee \psi) & = & \lnot(\lnot G(\phi) \land \lnot G(\psi)) \\ G(\forall x.\;\phi) & = & \forall x.\; \lnot\lnot G(\phi) \\ G(\exists x.\;\phi) & = & \lnot \forall x.\; \lnot(G(\phi)) \\ G(P) & = & \lnot\lnot P \\ \end{array}$

Заметьте, что - это, в основном, гомоморфизм, который вставляется в дополнительные не-не-везде, за исключением того, что при дизъюнкциях и экзистенциалах он использует дуальность де Моргана, чтобы превратить их в союзы и универсалии. (Я совершенно уверен, что это не точный перевод Геделя-Генцена, поскольку я подготовил его для этого ответа - в основном все, что вы пишете с использованием двойного отрицания + двойственности де Моргана, будет работать. Это разнообразие на самом деле оказывается важным для вычислительные интерпретации классической логики; см. ниже.) $G(\phi)$

Во-первых: очевидно, что этот перевод сохраняет классическую истину, так что истинно тогда и только тогда, когда - классически. $G(\phi)$ $\phi$

Во-вторых, это менее очевидно, но все же имеет место, что для формул в фрагмент, доказуемость в интуиционистской и классической логике совпадает. Способ доказать это - сначала взглянуть на формулы, взятые из этой грамматики: $\forall, \implies, \land, \lnot$

\begin{array}{lcl} A, B & ::= & \forall x . A (x) | A ⟹ B | A \land B | \neg A | \neg \neg P \end{array}

$\newcommand{\bnfalt}{\;\;|\;\;} \begin{array}{lcl} A,B & ::= & \forall x.\;A(x) \bnfalt A \implies B \bnfalt A \land B \bnfalt \lnot A \bnfalt \lnot\lnot P \end{array}$

И тогда мы можем доказать в качестве леммы (индукцией по ), что выводимо интуитивистски. Итак, теперь мы можем показать эквивалентность отрицательных формул, выполнив индукцию по структуре доказательства (скажем, в последовательном исчислении) и использовать предыдущую лемму для моделирования закона исключенной середины. $A$ $G(A) \implies A$

Итак, как вы должны думать об этом интуитивно?

Во-первых, теоретико-доказательственный взгляд. Если вы посмотрите на правила последовательного исчисления, вы увидите, что единственное место, где классическая и интуиционистская логика серьезно отличаются, - это правила дизъюнкции и экзистенциалов. Таким образом, мы используем этот факт, чтобы показать, что доказательства в одной логике этих формул могут быть переведены в доказательства в другой. Это показывает, как думать о конструктивной логике как о расширении классической логики с двумя новыми связями: « и . То, что мы называем «классическим существованием» и «классическим дизъюнкцией», были просто аббревиатурами, включающими , конъюнкт и отрицание, и поэтому, чтобы говорить о реальном существовании, нам нужно было ввести новые связки. $\exists$ $\vee$ $\forall$
Во-вторых, есть топологический вид. Теперь модель классической логики (как семейства множеств) представляет собой булеву алгебру (т. Е. Семейство подмножеств, замкнутых относительно произвольных объединений, пересечений и дополнений). Оказывается, что модель интуиционистской логики представляет собой топологическое пространство , а предложения интерпретируются как открытые множества. Их интерпретация отрицания является внутренней частью дополнения, и тогда легко показать, что , что означает, что двойное отрицание отправляет нас в наименьший колпан, покрывающий каждое открытое --- и Clopens образуют булеву алгебру. $\lnot\lnot\lnot P = \lnot P$

Теперь, благодаря Карри-Говарду, мы знаем, как интерпретировать доказательства в интуиционистской логике как функциональные программы. Итак, один возможный ответ (но не единственный) на вопрос «каково конструктивное содержание классического доказательства?» является следующим:

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

Итак, давайте посмотрим на перевод . Таким образом, это говорит о том, что конструктивное содержание исключенной середины - это то же самое, что сказать, что дело не в том, что и выполняются, то есть не противоречат. Так что в этом смысле на самом деле не так много вычислительного содержания для закона исключенной середины. $G(A \vee \lnot A) = \lnot(\lnot G(A) \land \lnot\lnot G(A))$ $\lnot P$ $\lnot\lnot P$

Чтобы увидеть, что это конкретно, вспомним, что конструктивно отрицание определяется как . Таким образом, эта формула . Следующий фрагмент кода Ocaml будет иллюстрировать: $\lnot A == A \implies \bot$ $((G(A) \implies \bot) \land ((G(A) \implies \bot) \implies \bot)) \implies \bot$

type bot = Void of bot
type 'a not = 'a -> bot

let excluded_middle : ('a not * 'a not not) not = fun (u, k) -> k u

То есть, если вы получаете не-А и не-не-А, вы можете просто передать первое отрицание второму, чтобы получить противоречие, которое вы хотите.

Теперь, что является продолжением преобразования в стиле передачи?

Продолжение типа является то , что принимает значение типа и вычисляет окончательный ответ от него. $\tau$ $\tau$
Продолжения используются для моделирования контекста программы. То есть у нас может быть член оцениваемый как часть гораздо более крупной программы . Вся эта штука вокруг этого возьмет результат вычисления и вычислит окончательный ответ. $3+5$ $C[3+5]$ $3 + 5$
Таким образом, вы можете думать о продолжении типа как функции , где - это любой тип ответа. $\tau$ $\tau \to \alpha$ $\alpha$
Так что если у вас есть программа типа , мы можем "CPS-преобразовать" ее, найдя термин типа , который в конечном итоге будет передавать все, что вычислило бы для его продолжение. (По сути, это просто делает поток управления явным.) $e$ $\tau$ $(\tau \to \alpha) \to \alpha$ $e$
Но мы должны делать это по наследству, чтобы каждая часть программы дала явное продолжение.

В настоящее время,

Отрицательный перевод в основном наследственно посылает к . $\phi$ $\lnot\lnot\phi$
Однако, хотя в нашем переводе используется отрицание, оно фактически не устраняет ложное суждение, поэтому в этом предложении перевод работает параметрически.
В частности, мы можем заменить любым типом ответа . $\bot$ $\alpha$
Таким образом, мы наследственно заменяем на . $\phi$ $(\phi \to \alpha) \to \alpha$
Это преобразование CPS.

Я видел «a» преобразование CPS, поскольку, как я упоминал ранее, существует много отрицательных переводов, которые позволяют вам доказать эту теорему, и каждый из них соответствует разной трансформации CPS. В операционном плане каждое преобразование соответствует другому порядку оценки . Таким образом, не существует уникальной вычислительной интерпретации классической логики, поскольку у вас есть выбор, и выбор различий имеет очень разные эксплуатационные характеристики.

Нил Кришнасвами
источник

Это отличный ответ. Это напомнило мне статью Вадлера «Call-by-value двойственна call-by-name»: homepages.inf.ed.ac.uk/wadler/topics/call-by-need.html , в который включен очень запоминающийся анекдот в разделе 4, чтобы объяснить взаимосвязь между callCC и исключенной серединой.

sclv

Есть целые конференции на тему неконструктивных доказательств как программ , и я не специалист по этому вопросу. Выше Нил Кришнасвами сослался на более длинный ответ, который он готовит, что, судя по его работе здесь, будет превосходным. Это просто вкус ответа.

Оказывается, тип продолжения звонка с током соответствует предложению, известному как закон Пирса , который можно использовать для доказательства закона исключенного среднего ( ). Программа LEM может быть написана с использованием callcc. В Coq: $\forall P, P \lor \lnot P$

Set Implicit Arguments.

Axiom callcc : forall (A B : Set), ((A -> B) -> A) -> A.

Lemma lem : forall (A B:Set), sum A (A -> B).
Proof.
  intros.
  eapply callcc.
  intros H.
  right.
  intros.
  apply H.
  left.
  assumption.
Defined.

Recursive Extraction lem.

дает код O'Caml:

type ('a, 'b) sum =
  | Inl of 'a
  | Inr of 'b

(** val callcc : (('a1 -> 'a2) -> 'a1) -> 'a1 **)

let callcc =
  failwith "AXIOM TO BE REALIZED"

(** val lem : ('a1, 'a1 -> no) sum **)

let lem =
    callcc (fun h -> Inr (fun h0 -> h (Inl h0)))

Самое чистое введение в это я видел в книге Тима Гриффина «Формула понятия контроля» .

jbapple
источник

Вы должны попытаться извлечь в Схему и сказать, что процедура извлечения должна извлечь callccв Схему callcc. Тогда вы действительно можете попробовать.

Андрей Бауэр