Czy można udowodnić nierozstrzygalność problemu zatrzymania w Coq?

23

Oglądałem „ Pięć etapów akceptacji konstruktywnej matematyki ” Andreja Bauera i mówi on, że istnieją dwa rodzaje dowodów sprzeczności (lub dwie rzeczy, które matematycy nazywają dowodem sprzeczności):

  1. Załóżmy, że jest fałszywe ... bla bla bla, sprzeczność. Dlatego jest prawdziwe.P.P.
  2. Załóżmy, że jest prawdą ... bla bla bla, sprzeczność. Dlatego P jest fałszem.P.P.

Pierwszy jest równoważny Prawu Wykluczonego Środka (LEM), a drugi - jak udowodnić negację.

Dowód nierozstrzygalności problemu zatrzymania (HP) jest dowodem sprzeczności: załóżmy, że istnieje maszyna która może zadecydować o HP ... bla bla bla, sprzeczność. Dlatego D nie istnieje.rere

Niech więc będzie „ D istnieje i może decydować o HP”. Załóżmy, że P jest prawdą ... bla bla bla, sprzeczność. Dlatego P jest fałszem.P.reP.P.

To wygląda na drugi rodzaj dowodu sprzeczności, więc czy można udowodnić nierozstrzygalność problemu zatrzymania w Coq (bez zakładania LEM)?

EDYCJA: Chciałbym zobaczyć kilka punktów na temat udowodnienia tego za pomocą sprzeczności. Wiem, że można to również udowodnić za pomocą diagonalizacji.

Rafael Castro
źródło
2
@cody Dlaczego oświadczenie negatywne wymaga sprzeczności? A może ograniczasz się do Coq?
David Richerby
3
@DavidRicherby Właściwie trochę przesadzam, ponieważ jest to prawdą tylko przy braku aksjomatów. W takim przypadku pierwszym (najniższym) krokiem (bezciętego) dowodu musi być Intro w intuicyjnej naturalnej dedukcji. W przypadku, gdy istnieją aksjomaty / hipotezy, to nigdy nie zaszkodzi zastosować ten krok jako pierwszy, ponieważ jest on odwracalny, ale czasami można go uniknąć.
cody
2
Wiesz o gazecie o tym samym tytule? (Myślę, że tam wyraźnie stwierdzam, że zwykły dowód braku istnienia Wyroczni Powstrzymującej jest konstruktywny.)
Andrej Bauer
1
@AndrejBauer, nie wiem. Właśnie to znalazłem. Tak, stwierdzasz, że „Zwykły dowód nieistnienia wyroczni Halting jest kolejnym przykładem konstruktywnego dowodu negacji”.
Rafael Castro
1
@RafaelCastro: jako student studiów licencjackich zadajesz dobre pytania. Po prostu zachęcam was, byście śmiało poszli tam, gdzie wcześniej nie byli studenci (a przynajmniej nieliczni).
Andrej Bauer,

Odpowiedzi:

20

Masz całkowitą rację, że problem zatrzymania jest przykładem drugiego rodzaju „dowodu sprzeczności” - to tak naprawdę tylko negatywne stwierdzenie.

Załóżmy, że decides_halt(M)jest predykatem, który mówi, że maszyna Mdecyduje, czy jej wejście jest maszyną, która się zatrzymuje (to znaczy Mjest programem, który dla niektórych maszyn mi danych wejściowych idecyduje, czy mzatrzymuje się na wejściu i).

Zapominając na chwilę o tym, jak to udowodnić, problemem zatrzymania jest stwierdzenie, że nie ma maszyny, która rozstrzygałaby problem zatrzymania. Możemy to stwierdzić w Coq jako (exists M, decides_halt M) -> False, a może wolimy powiedzieć, że dana maszyna nie rozwiązuje problemu zatrzymania forall M, decides_halt M -> False. Okazuje się, że bez żadnych aksjomatów te dwie formalizacje są równoważne w Coq. (Podałem dowód, abyś mógł zobaczyć, jak to działa, ale firstorderzrobi wszystko!)

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.

Myślę, że którekolwiek z tych stwierdzeń nie jest zbyt trudne do udowodnienia jako argument przekątny, chociaż sformalizowanie maszyn, obliczalność i zatrzymanie jest prawdopodobnie dość trudne. Prostszy przykład, nie jest to zbyt trudne do udowodnienia diagonalizacja Twierdzenie Cantora (patrz https://github.com/bmsherman/finite/blob/master/Iso.v#L277-L291 za dowód, że nat -> nati natnie są izomorficzne).

Powyższa diagonalizacja daje przykład, jak możesz dojść do sprzeczności z izomorfizmem pomiędzy nat -> nati nat. Oto istota tego dowodu przedstawiona jako samodzielny przykład:

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.

Nawet bez patrzenia na szczegóły możemy stwierdzić ze stwierdzenia, że ​​dowód ten zakłada jedynie istnienie bijectionu i pokazuje, że jest to niemożliwe. Najpierw nadamy obu stronom bijection nazwy seqi index. Kluczem jest to, że zachowanie bijectionu w specjalnej sekwencji f := fun n => S (seq n n)i jego indeksie index fjest sprzeczne. Dowód problemu zatrzymania mógłby doprowadzić do sprzeczności w podobny sposób, tworząc hipotezę o maszynie, która rozwiązuje problem zatrzymania za pomocą starannie wybranej maszyny (w szczególności takiej, która faktycznie zależy od założonej maszyny).

Tej Chajed
źródło
Witamy na stronie! Mam nadzieję, że zostaniesz w pobliżu - może chcesz wziąć udział w naszej krótkiej prezentacji, aby dowiedzieć się więcej o działaniu Stack Exchange.
David Richerby
2
Zapomniałem, że ten problem dowodzi również argument diagonalizacji. Twoja odpowiedź jest interesująca, ale chciałbym zobaczyć kilka kwestii, czy możliwe jest udowodnienie HM za pomocą sprzeczności w Coq. Wyjaśnię to bardziej w pytaniu.
Rafael Castro,