Problemo de halto
Problemo de halto estas tasko de teorio de nombrigebleco, kiu povas esti neformale donita jene:
- Se vi konas fontkodon de programo kaj ties eniron, decidu, ĉu la programo haltos aŭ ĉu ĝi funkcios por ĉiam sen halto.
En la jaro 1936 Alan Turing pruvis, ke ĝenerala algoritmo, kiu solvus la problemon de halto por ĉiuj eniroj de ĉiuj programoj, ne ekzistas. La problemo de halto tial estas markata kiel algoritme nedecidebla problemo.
Skizo de la pruvo
[redakti | redakti fonton]La nedecideblecon de la problemo de halto eblas pruvi per disputo.
- Komenca supozo: Ni supozu, ke la problemon de halto eblas decidi. Tio signifas, ke ekzistas ia programo Haltu(programon, eniron), kiu estas universala solvo de la problemo de halto.
Tiu funkcias tiel, ke se la vokado programo(eniro) post fina kvanto de paŝoj finiĝos, poste ĝi Haltu(programon, eniron) revenigos la valoron JES, en mala kazo (se la vokado programo(eniro) encikliĝus) revenigos la valoron NE. - Ni konstruu programon Paradokso(x), kiu intence encikliĝos, se la vokado de programo Haltu(x x) revenigos JES, kaj ĝi haltos, se la vokado de programo Haltu(x x) revenigos NE.
- Nun ni demandu, kio estas la rezulto de la vokado Paradokso(Paradokso).
- Ni supozu por momento, ke Haltu(Paradokson, Paradokson) revenigas JES. Sed laŭ la difino de la programo Haltu validas, ke se Paradokso(Paradokso) encikliĝos, poste la Haltu(Paradokson, Paradokson) devas revenigi NE. Ni venis al disputo.
- Ni supozu aliflanke por momento, ke la Haltu(Paradokson, Paradokson) revenigas NE. El la difino de la programo Paradokso ni poste scias, ke la Paradokso(Paradokso) haltos. Sed laŭ la difino de la programo Haltu validas, ke se la Paradokso(Paradokso) haltos, poste la Haltu(Paradokson, Paradokson) devas revenigi JES. Denove ni venis al disputo.
- Ĉar ni elĉerpis ĉiujn eblecojn kaj ĉiam ni venis al disputo, la komenca supozo devas esti malvera. El tio rezultas, ke la programo Haltu(programon, eniron), tiel kiel ĝi estis difinita, ne ekzistas.