Est-il possible de prouver l'indécidabilité du problème d'arrêt à Coq?

23

Je regardais les " Cinq étapes de l'acceptation des mathématiques constructives " d'Andrej Bauer et il dit qu'il y a deux types de preuves par contradiction (ou deux choses que les mathématiciens appellent preuve par contradiction):

  1. Supposons que est faux ... bla bla bla, contradiction. Par conséquent, est vrai.PP
  2. Supposons que soit vrai ... bla bla bla, contradiction. Par conséquent, est faux.PP

La première équivaut à la loi du milieu exclu (LEM) et la seconde consiste à prouver la négation.

La preuve de l'indécidabilité du problème de l'arrêt (HP) est une preuve par contradiction: supposons qu'il existe une machine qui puisse décider du HP ... bla bla bla, contradiction. Par conséquent, n'existe pas.

Donc, que soit " existe et peut décider du HP". Supposons que soit vrai ... bla bla bla, contradiction. Par conséquent, est faux.PPP

Cela ressemble au deuxième type de preuve par contradiction, est-il donc possible de prouver l'indécidabilité du problème d'arrêt dans Coq (sans supposer LEM)?

EDIT: Je voudrais voir quelques points sur la preuve de cela en utilisant la contradiction. Je sais que cela peut également être prouvé en utilisant la diagonalisation.

Rafael Castro
la source
2
@cody Pourquoi une déclaration négative nécessite-t-elle une contradiction? Ou vous limitez-vous à Coq?
David Richerby
3
@DavidRicherby J'exagère en fait un peu, car cela n'est vrai qu'en l'absence d'axiomes. Dans ce cas, la première étape (la plus basse) d'une preuve (sans coupure) doit être Not-Intro dans la déduction naturelle intuitionniste. Dans le cas où il y a des axiomes / hypothèses, alors cela ne fait jamais de mal d'appliquer d'abord cette étape, car elle est inversible, mais parfois elle peut être évitée.
cody
2
Vous connaissez le journal du même titre? (Je pense que là-dedans, je déclare explicitement que la preuve habituelle de la non-existence de l'Oracle stoppant est constructive.)
Andrej Bauer
1
@AndrejBauer, je ne sais pas. Je viens de le trouver. Oui, vous dites que "la preuve habituelle de non-existence de l'oracle Halting est encore un autre exemple de preuve constructive de négation".
Rafael Castro
1
@RafaelCastro: en tant qu'étudiant de premier cycle, vous posez de bonnes questions. Je vous encourage simplement à aller hardiment là où aucun étudiant de premier cycle (ou du moins pas très nombreux) n'est allé auparavant.
Andrej Bauer

Réponses:

20

Vous avez tout à fait raison de dire que le problème de l'arrêt est un exemple du deuxième type de «preuve par contradiction» - ce n'est vraiment qu'une déclaration négative.

Supposons decides_halt(M)qu'un prédicat indique que la machine Mdécide si son entrée est une machine qui s'arrête (c'est-à-dire, Mun programme qui, pour une machine met une entrée i, décide si elle ms'arrête en entrée i).

Oubliant un instant comment le prouver, le problème d'arrêt est la déclaration selon laquelle il n'y a pas de machine qui décide du problème d'arrêt. Nous pourrions déclarer cela dans Coq comme (exists M, decides_halt M) -> False, ou peut-être préférons-nous dire qu'une machine donnée ne résout pas le problème d'arrêt forall M, decides_halt M -> False. Il s'avère que sans aucun axiome ces deux formalisations sont équivalentes en Coq. (J'ai énoncé la preuve pour que vous puissiez voir comment cela fonctionne, mais vous firstorderferez tout cela!)

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.

Je pense que l'une ou l'autre de ces affirmations n'est pas trop difficile à prouver comme argument de diagonalisation, bien que formaliser les machines, la calculabilité et l'arrêt soit probablement assez difficile. Pour un exemple plus simple, il est pas trop difficile de prouver le théorème de diagonalisation de Cantor (voir https://github.com/bmsherman/finite/blob/master/Iso.v#L277-L291 pour une preuve nat -> natet natne sont pas isomorphes).

La diagonalisation ci-dessus donne un exemple de la façon dont vous pourriez procéder pour dériver une contradiction d'un isomorphisme entre nat -> natet nat. Voici l'essence de cette preuve présentée comme un exemple autonome:

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.

Même sans regarder les détails, nous pouvons voir dans la déclaration que cette preuve prend la simple existence d'une bijection et démontre qu'elle est impossible. Nous donnons d'abord les deux côtés de la bijection les noms seqet index. La clé est que le comportement de la bijection à la séquence spéciale f := fun n => S (seq n n)et son indice index fsont contradictoires. La preuve du problème d'arrêt dériverait d'une contradiction de manière similaire, instanciant son hypothèse sur une machine qui résout le problème d'arrêt avec une machine soigneusement choisie (et en particulier une qui dépend en fait de la machine supposée).

Tej Chajed
la source
Bienvenue sur le site! J'espère que vous resterez - vous aimerez peut-être faire notre très brève visite pour en savoir plus sur le fonctionnement de Stack Exchange.
David Richerby
2
J'ai oublié que ce problème est également prouvé par un argument de diagonalisation. Votre réponse est intéressante mais j'aimerais voir quelques points sur la possibilité de prouver le HM en utilisant une contradiction dans Coq. Je vais préciser cela dans la question.
Rafael Castro