Можно ли доказать неразрешимость проблемы остановки в Coq?

23

Я смотрел « Пять этапов принятия конструктивной математики » Андрея Бауэра, и он говорит, что существует два вида доказательств от противного (или две вещи, которые математики называют доказательством от противного):

  1. Предположим, что является ложным ... бла-бла-бла, противоречие. Следовательно, верно.ПPP
  2. Предположим, что это правда ... бла-бла-бла, противоречие. Следовательно, ложно.ПPP

Первый из них эквивалентен Закону исключенного среднего (LEM), а второй - как доказать отрицание.

Доказательство неразрешимости проблемы остановки (HP) является доказательством от противного: предположим, что существует машина которая может решить HP ... бла-бла-бла, противоречие. Следовательно, не существует.DDD

Итак, пусть будет " существует и может решать HP". Предположим, что это правда ... бла-бла-бла, противоречие. Следовательно, ложно.D P PPDPP

Это похоже на второй тип доказательства от противного, поэтому можно доказать неразрешимость проблемы остановки в Coq (без предположения LEM)?

РЕДАКТИРОВАТЬ: Я хотел бы увидеть некоторые моменты о доказательстве этого с помощью противоречия. Я знаю, что это также можно доказать с помощью диагонализации.

Рафаэль Кастро
источник
2
@cody Почему отрицательное утверждение требует противоречия? Или вы ограничиваете Coq?
Дэвид Ричерби
3
@DavidRicherby Я немного преувеличиваю, так как это верно только при отсутствии аксиом. В этом случае первый (самый низкий) шаг доказательства (без выреза) должен быть не вступительным в интуитивистском естественном выводе. В случае, когда есть аксиомы / гипотезы, тогда никогда не повредит применять этот шаг первым, поскольку он обратим, но иногда его можно избежать.
Коди
2
Вы знаете о бумаге с таким же названием? (Я думаю, что там я прямо заявляю, что обычное доказательство несуществования Остановляющего Оракула конструктивно.)
Андрей Бауэр
1
@AndrejBauer, я не знаю. Просто нашел это. Да, вы утверждаете, что «Обычное доказательство небытия Орала Остановки - это еще один пример конструктивного доказательства отрицания».
Рафаэль Кастро
1
@RafaelCastro: будучи студентом, вы задаете хорошие вопросы. Я просто призываю вас смело идти туда, где до этого не ходили студенты (или, по крайней мере, не очень).
Андрей Бауэр

Ответы:

20

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

Предположим, decides_halt(M)есть предикат, который говорит, что машина Mрешает, является ли ее ввод машиной, которая останавливает (то есть, Mявляется ли программа, которая для некоторой машины mи ввода i, решает, mостанавливается ли ввод i).

Забыв на мгновение о том, как это доказать, проблема остановки - это утверждение, что нет машины, которая решает проблему остановки. Мы можем указать это в Coq как (exists M, decides_halt M) -> False, или, может быть, мы предпочитаем сказать, что любая машина не решает проблему остановки forall M, decides_halt M -> False. Оказывается, что без каких-либо аксиом эти две формализации эквивалентны в Coq. (Я изложил доказательства, чтобы вы могли видеть, как это работает, но firstorderсделаю все это!)

Parameter machine:Type.
Parameter decides_halt : machine -> Prop.

(* Here are two ways to phrase the halting problem: *)

Definition halting_problem : Prop :=
  (exists M, decides_halt M) -> False.

Definition halting_problem' : Prop :=
  forall M, decides_halt M -> False.

Theorem statements_equivalent :
  halting_problem <-> halting_problem'.
Proof.
  unfold halting_problem, halting_problem'; split; intros.
  - exact (H (ex_intro decides_halt M H0)).
  - destruct H0.
    exact (H x H0).
Qed.

Я думаю, что любое утверждение не слишком сложно доказать в качестве аргумента диагонализации, хотя формализация машин, вычислимость и остановка, вероятно, достаточно сложны. Для более простого примера, это не так уж трудно доказать теорему диагонализации Кантора (см https://github.com/bmsherman/finite/blob/master/Iso.v#L277-L291 для доказательства этого nat -> natи natне изоморфны).

Диагонализация, приведенная выше, дает пример того, как вы можете получить противоречие из изоморфизма между nat -> natи nat. Вот суть этого доказательства в виде отдельного примера:

Record bijection A B :=
  {  to   : A -> B
  ; from : B -> A
  ; to_from : forall b, to (from b) = b
  ; from_to : forall a, from (to a) = a
  }.

Theorem cantor :
  bijection nat (nat -> nat) ->
  False.
Proof.
  destruct 1 as [seq index ? ?].
  (* define a function which differs from the nth sequence at the nth index *)
  pose (f := fun n => S (seq n n)).
  (* prove f differs from every sequence *)
  assert (forall n, f <> seq n). {
    unfold not; intros.
    assert (f n = seq n n) by congruence.
    subst f; cbn in H0.
    eapply n_Sn; eauto.
  }
  rewrite <- (to_from0 f) in H.
  apply (H (index f)).
  reflexivity.
Qed.

Даже не глядя на детали, мы можем видеть из утверждения, что это доказательство принимает простое существование биекции и демонстрирует, что это невозможно. Сначала мы даем две стороны биекции имена seqи index. Ключевым является то, что поведение биекции в специальной последовательности f := fun n => S (seq n n)и ее индекс index fпротиворечивы. Доказательство проблемы остановки могло бы привести к противоречию аналогичным образом, создавая свою гипотезу о машине, которая решает проблему остановки с помощью тщательно выбранной машины (и, в частности, той, которая фактически зависит от предполагаемой машины).

Тей Чаджед
источник
Добро пожаловать на сайт! Я надеюсь, что вы останетесь здесь - возможно, вы захотите пройти наш краткий тур, чтобы узнать больше о том, как работает Stack Exchange.
Дэвид Ричерби
2
Я забыл, что эта проблема также доказана аргументом диагонализации. Ваш ответ интересен, но я хотел бы увидеть некоторые моменты о том, можно ли доказать HM, используя противоречие в Coq. Я сделаю это более ясным в вопросе.
Рафаэль Кастро