¿Es posible demostrar la indecidibilidad del problema de detención en Coq?

23

Estaba viendo las " Cinco etapas de aceptar las matemáticas constructivas " de Andrej Bauer y dice que hay dos tipos de prueba por contradicción (o dos cosas que los matemáticos llaman prueba por contradicción):

  1. Suponga que es falso ... bla, bla, bla, contradicción. Por lo tanto, es cierto.PPAGSPAGS
  2. Suponga que es cierto ... bla, bla, bla, contradicción. Por lo tanto, es falso.PAGSPAGS

El primero es equivalente a la Ley del Medio Excluido (LEM) y el segundo es cómo demostrar la negación.

La prueba de la indecidibilidad del Problema de detención (HP) es una prueba por contradicción: suponga que hay una máquina que puede decidir el HP ... bla, bla, bla, contradicción. Por lo tanto, no existe.rere

Entonces, que sea ​​" existe y puede decidir el HP". Suponga que es cierto ... bla, bla, bla, contradicción. Por lo tanto, es falso.PAGSrePAGSPAGS

Este parece ser el segundo tipo de prueba por contradicción, ¿entonces es posible demostrar la indecidibilidad del problema de detención en Coq (sin asumir LEM)?

EDITAR: Me gustaría ver algunos puntos sobre probar esto usando la contradicción. Sé que esto también se puede probar utilizando la diagonalización.

Rafael Castro
fuente
2
@cody ¿Por qué una declaración negativa requiere contradicción? ¿O estás restringiendo a Coq?
David Richerby
3
@DavidRicherby En realidad estoy exagerando un poco, ya que eso solo es cierto en ausencia de axiomas. En ese caso, el primer paso (el más bajo) de una prueba (sin cortes) debe ser Not-Intro en la deducción intuitiva natural. En el caso de que haya axiomas / hipótesis, nunca está de más aplicar este paso primero, ya que es invertible, pero a veces se puede evitar.
cody
2
¿Conoces el papel con el mismo título? (Creo que allí declaro explícitamente que la prueba habitual de la inexistencia del Oráculo detenido es constructiva).
Andrej Bauer
1
@AndrejBauer, no lo sé. Acabo de encontrarlo. Sí, usted afirma que "La prueba habitual de la inexistencia del oráculo de detención es otro ejemplo más de una prueba constructiva de negación".
Rafael Castro
1
@RafaelCastro: como estudiante universitario estás haciendo buenas preguntas. Solo te animo a que valientemente vayas a donde ningún estudiante universitario (o al menos no muchos) haya ido antes.
Andrej Bauer

Respuestas:

20

Tiene toda la razón en que el problema de detención es un ejemplo del segundo tipo de "prueba por contradicción": en realidad es solo una afirmación negativa.

Supongamos que decides_halt(M)es un predicado que dice que la máquina Mdecide si su entrada es una máquina que se detiene (es decir, Mes un programa que para alguna máquina my entrada i, decide si se mdetiene en la entrada i).

Olvidando por un momento cómo probarlo, el problema de detención es la afirmación de que no hay máquina que decida el problema de detención. Podríamos decir esto en Coq como (exists M, decides_halt M) -> False, o tal vez preferimos decir que cualquier máquina no resuelve el problema de detención forall M, decides_halt M -> False. Resulta que sin ningún axioma estas dos formalizaciones son equivalentes en Coq. (He explicado la prueba para que pueda ver cómo funciona, ¡pero firstorderlo hará todo!)

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.

Creo que cualquiera de las afirmaciones no es demasiado difícil de demostrar como un argumento de diagonalización, aunque formalizar máquinas, la computabilidad y la detención probablemente sea un desafío razonable. Para un ejemplo más simple, no es demasiado difícil de demostrar el teorema de diagonalización de Cantor (ver https://github.com/bmsherman/finite/blob/master/Iso.v#L277-L291 para una prueba de que nat -> naty natno son isomorfos).

La diagonalización anterior da un ejemplo de cómo se podría derivar una contradicción de un isomorfismo entre nat -> naty nat. Aquí está la esencia de esa prueba en línea como un ejemplo autónomo:

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.

Incluso sin mirar los detalles, podemos ver en la declaración que esta prueba toma la mera existencia de una biyección y demuestra que es imposible. Primero le damos a los dos lados de la biyección los nombres seqy index. La clave es que el comportamiento de la biyección en la secuencia especial f := fun n => S (seq n n)y su índice index fes contradictorio. La prueba del problema de detención derivaría una contradicción de una manera similar, instanciando su hipótesis sobre una máquina que resuelve el problema de detención con una máquina cuidadosamente elegida (y en particular una que realmente depende de la máquina supuesta).

Tej Chajed
fuente
Bienvenido al sitio! Espero que te quedes, quizás quieras hacer nuestro breve recorrido para ver más sobre cómo funciona Stack Exchange.
David Richerby
2
Olvidé que este problema también se prueba mediante un argumento de diagonalización. Su respuesta es interesante, pero me gustaría ver algunos puntos sobre si es posible probar el HM utilizando una contradicción en Coq. Dejaré esto más claro en la pregunta.
Rafael Castro