Saltar al contenido
The Lumenary
Sendero del AsombroOpcional · nunca se calificaParte de Repetition and decisions

Can a computer decide?

Esta página todavía no está disponible en Español, por eso se muestra en English.

Ayuda a traducir →
1

La pregunta

Some programs stop and some loop forever. Could someone write one clever program that looks at any program, together with its input, and always correctly says whether it will stop?

Prueba el experimento antes de seguir leyendo. No hay una forma equivocada de explorar.

2

Experimento

La máquina diagonal

Esta es una lista de sucesiones infinitas de ceros y unos (solo podemos mostrar el principio). La sucesión dorada d invierte la diagonal.

s1…
s2…
s3…
s4…
s5…
s6…
d101001????…

Señala una fila (o llega a ella con el tabulador) para ver dónde se diferencia d de ella. Haz clic en cualquier dígito para cambiar la lista.

Añade d a la lista y aparecerá una nueva d que vuelve a ser distinta. Ninguna lista, por larga que sea, puede contener todas las sucesiones.

3

Pistas, si las quieres

    4

    Qué está pasando

    Qué está pasando

    In 1936 Alan Turing proved that no such checker can exist. The argument is short.

    Suppose a program HH could take any program PP and input xx and always answer correctly "PP stops on xx" or "PP runs for ever on xx". Build a new program DD: given a program PP, it asks HH whether PP stops when given its own text as input, and then does the opposite — if HH says "stops", DD loops for ever; if HH says "runs for ever", DD stops.

    Now run DD on its own text. If DD stops, then HH said "DD runs for ever" — wrong. If DD runs for ever, then HH said "DD stops" — wrong again. Either way HH makes a mistake, so the perfect checker HH cannot exist. This is the halting problem, and it is undecidable.

    This is the same diagonal trick Cantor used to show that some infinities are bigger than others, and Gödel used to show that no consistent formal system can prove every true statement about whole numbers. It does not say that we can never tell whether a particular program stops — often we can — only that no single program can do it for all programs. Henry Rice later showed that the same holds for every non-trivial question about what programs compute.

    Analogía, no una construcción formal: The experiment shows Cantor's diagonal argument for 0–1 sequences. The halting proof below uses the same diagonal idea, applied to programs; the experiment is an illustration of the idea, not the halting proof itself.

    Probado computacionalmenteRedactado con IA · pendiente de revisión humana
    5

    Adónde lleva esto