<pre>
char *halting_problem (..)
{
struct sandbox A, B;
struct prog P;
int ff = 0;
read_prog (&P, stdin);
init_sandbox (&A, &P);
init_sandbox (&B, &P);
while (! is_halted (&A)) {
step_next (&A);
if (is_equal (&A, &B))
return "program se zacykli a neskonci";
if (ff ^= 1)
step_next (&B);
}
return "program se zastavi";
}
Jen dodam, kdyby to nekomu nahodou nebylo jasne na prvni pohled. Program je simulovan v sandboxu, coz je jakysi simulacni model pocitace, na kterem program pobezi. Nejprve nactu program, a poslu ho do DVOU sandboxu. Stacil by i jeden, ale detekce zacykleni by byla slozitejsi, musel bych uchovavat historii vsech stavu. Pak se program zacne soubezne provadet v obou sandboxech, v tom prvnim 2x rychleji. Ze smycky se vypadne bud kdyz program skonci ve stavu oznacenem jako konecny (is_halted vrati true), nebo zjistim ze okamzita konfigurace obou sandboxu je stejna (tj stejny algoritmus se po provedeni 2N kroku ocitne ve stavu kde byl po N krocich, je tedy zjevne ze ve stejnem stavu bude i po K*N krocich, a K muzeme poslat do nekonecna.
Muj program proto A) spravne reportuje kdyz program skonci B) spravne pozna kdyz se program zacykli. Vazne nevim co ti vedatori resi. :)
Je treba si uvedomit, ze simulovany program muze alokovat nekonecne mnozstvi pameti (nad konecnou pameti ma uloha zastaveni samozrejme reseni). Tzn program je schopny generovat stale nove a nove stavy az do nekonecna (lze si napr. prestavit, ze treba pocitam hodnotu pi). Tvuj program da odpoved v pripade, ze se program _necykli_, na tuto odpoved ale neni treba psat nejaky specialni kod, proste zkoumany program spustim.
P.S. Ad Milan Sorm, rad bych ctenare teto diskuse ubezpecil, ze _vyznamna_vetsina_ absoloventu FI MUNI chape rozdil mezi problemy ze tridy NP a problemem zastaveni.
K čemu je dobrý program, který alokuje nekonečně mnoho paměti? A hlavně kde ho chcete spouštět? Program který nelze spustit nemá smysl analyzovat, nemyslíte? Jde o teoretický konstrukt (čti výmysl) a přemýšlet nad ním je zhruba stejně zbytečné jako soutěž v čurání do dálky.
Tak specialne pro absolventy a studenty FIT VUT: Predstavte si program, ktery pricita jednicku k promenne x, kterazto nemuze pretect, protoze prostor tohoto cisla je alokovan dynamicky. (Pro ilustraci treba podobne jako v bc.) Toto je jenom vylepsena verze "alokatoru pameti", ktery ji ale alokuje jenom logaritmicky rychle (teda spis pomalu). Jinymi slovy uz na par megabajtech vypocet predstavje nekolik dob existence slunecni soustavy, tudiz sandbox je uplne na ... (Informatikovi normalne staci predstava "rychleho" alokatoru pameti na nekonecnem datovem, holt pro VUT je to vysvetlovani trochu pomalejsi.)
No a jadro psa je, ze by se docela hodilo, kdybych dokazal zjistit, zda se muj vypocet ubira stejnou cestou, jako "pomaly alokator pameti", tj. nikdy neskonci, nebo zda bude nekdy koncit. No a to se nikdy nedovime, protoze problem zastaveni. No a dobre je to k tomu, ze se uz nemusim snazit napsat obecny detektor zastaveni, protoze to nejde, nebo to muzu dat nejakemu VUTakovi abych se ho na par dni zbavil. :P
Znam spoustu kvalitnich absolventu a studentu VUTu, (a nekvalitnich studentu a absolventu FI, jejichz perly lze nalezt i v teto diskusi :) ale bez takove vulgarni generalizace by nikdy nemohl vzniknout poradny flame. A kde jinde si muze clovek zaflamovat, nez prave ve foru k podobnemu clanku?
$ bc
bc 1.06
Copyright 1991-1994, 1997, 1998, 2000 Free Software Foundation, Inc.
This is free software with ABSOLUTELY NO WARRANTY.
For details type `warranty'.
2^2^2^2^2^2^2^2^2^2^2
Runtime error (func=(main), adr=38): exponent too large in raise
Hmm, asi pouzivate jiny BC, zejo? Matfyzaci si asi vydupali neco extra :-) :-)
> 2^2^2^2^2^2^2^2^2^2^2
> Runtime error (func=(main), adr=38): exponent too large in raise
Nevim co jste snazil timhle demonstrovat. BC vskutku alokuje pamet dynamicky, dokud ovsem zbyva co alokovat. Cislo 2^n pro n>ULONG_MAX se proste do pameti nevejde, a je jiste uzitecnejsi ohlasit rovnou "exponent too large", nez pocitat a pocitat a pocitat a nakonec zhynout na nedostatek VM.
Vašek tvrdil že předpokládat "nepřetečitelný" counter je zcela legitimní a rozumný předpoklad, a uvedl BC jako příklad. To jestli BC chcípne hned nebo až později je jedno, důležité je že chcípne, tedy nepřetečitelný counter neumí, stejně jako jej nikdy nebude umět žádný počítač. Proto je abstrakce konečného automatu zcela adekvátní pro libovolný myslitelný počítací stroj.
Tohle muze rici nejspis jen clovek, ktery si nevidi dal nez na spicku nosu. Nebo je to frustraci ze zjisteni, ze i ta nejnabusenejsi masina, kterou lze sehnat, je v principu jen konecny automat?
Kdyby uz nic jineho, tak teorie vycislitelnosti prinasi jeden velice prakticky dusledek halting problemu: nelze automaticky verifikovat software (snad kazdy rozumny clovek bude souhlasit s tim, ze rici, co dany program dela, je tezsi nez zjistit, zda vubec konci). Mimochodem halting problem souvisi s mnoha jinymi problemy, nekdy i zdanlive zcela nesouvisejicimi, napr. z teorie cisel... Jak se rika: vse souvisi se vsim. Tvrzeni, ze zabyvat se teorii, ktera na prvni pohled nema prime prakticke pouziti, bych od studenta nebo dokonce absolventa VS rozhodne necekal :-(
To se pletete, software verifikovat jde, dokonce je to velky byznys, a formalni verifikace jsou docela v kursu. Chtel jste asi napsat ze nejde verifikovat KAZDY program- ale to nikdo nepotrebuje. Staci ze jde automatizovane testovat ze dany kod bude dodrzovat urcite invarianty, a dokazat ze nejaka tvrzeni o vztahu mezi vstupem a vystupem budou pravdiva pro libovolny vstup.
Ano, to je pravda, tak jsem to myslel - nelze verifikovat libovolny program.
Navic i pri psani programu se musi pocitat s tim, ze ho nekdo bude chtit verifikovat, ze treba existuje nejaka formalni specifikace atd. Jiste nejste schopen zverifikovat kdejaky zdrojak vam kdo podstrci a bude se ptat, co to dela, ci zda to dela to, co si mysli, ze to dela.
Myslím, že to dokázat lze, nicméně důkaz nejsem schopen napsat ;-(.
Vycházím z toho, že v mnoha ohledech je it. fce použitá pro výpočet Mandelbrotovy množiny podobná bifurkacím a tam opravdu nemůžete rozhodnout stav systému v budoucnosti. Jediná možnost je projít si postupně všechny stavy až do místa, které Vás zajímá.
To bych opravdu rád věděl jak to vyřešíte v konečném počtu kroků.
Ta otázka o typu dat je mimo (počítám v reálných číslech, konkrétní implementace na procesoru to samozřejmě převede na diskrétní hodnoty), dejme tomu že v long doublech. Tj. můžete si samozřejmě zkusit projít celý stavový prostor, ale na to zas nemáte dostatek paměti.
Jistě, že po nějakém počtu kroků můžete říct: už to diverguje (|z|>2), nebo možná zjistit cyklus (zase ne všechny), popř. pevné body, ale to je tak asi vše.
Jak například po 1000000 krocích zjistíte, že se jedná o cyklus o periodě 20000000?
OK
a ako toto riesenie obide problem spominany na zaciatku clanku?
void Q(void) {
if (halting_problem(Q))
while(1) { }
}
Tak co, zastavi sa funkcia Q alebo nie?
ZAKLADNY problem je, ze ak sa ta funkcia da naprogramovat, vznikne paradox a preto sa NEDA naprogramovat (neda sa naprogramovat tak aby riesila problem zastavenia pre vsetky mozne programy, co tvoja funkcia nerobi).