VŠ z trochu jiného úhlu

[Mirek Prýmek]

Neshodli jsme se tu na tom, že HP v praxi řešitelný je, ale navržené řešení je v praxi nepoužitelné ?

Ne. Shodli jsme se (doufam) na tom, ze k reseni konkretniho zastaveni konkretniho algoritmu "narocnosti" N je potreba algoritmus "narocnosti" nejake f(N). Prakticka pouzitelnost nebo nepouzitelnost pak je dana porovnanim velikosti f(N) s tim, co mam realne k dispozici k reseni naseho realneho problemu.

Cili pokud ded kennedy rika:

Prisel nejaky idiot, ktery neni tak chytry jako ja, a navrhl, abysme tenhle problem resili zpusobem X. Ovsem neuvedomil si (protoze je nedouk), ze X je vlastne HP. A tak jsem nastoupil ja a rikam mu: ty jsi takovy idiot, ze mi pripominas jednoho vrchniho! Tohle je prece HP a ten je neresitelny. Takze takhle to resit nejde.

- tak to proste NENI PRAVDA, d.k. nepochopil, co vlastne skutecne HP nad TM je, a cosi, co slysel ve skole CHYBNE APLIKOVAL. Nejspis proto, ze misto toho, aby se ve skole aplikacemi zabyvali, zabyvali se dukazy.

Na tomhle proste trvam a nemuzu jinak, klidne at me mistni honorace upali, neodvolam!

[Reklama]

[Mirek Prýmek]

P.S. nehlede na to, ze i kdyby to bylo tak, jak pises ty, tak by porad d.k. nemel pravdu, protoze neproveditelnost toho "idiotskeho reseni" nema s Turingem nic spolecneho.

[Jakub Galgonek]

Neshodli jsme se tu na tom, že HP v praxi řešitelný je, ale navržené řešení je v praxi nepoužitelné ?

Ne. Shodli jsme se (doufam) na tom, ze k reseni konkretniho zastaveni konkretniho algoritmu "narocnosti" N je potreba algoritmus "narocnosti" nejake f(N). Prakticka pouzitelnost nebo nepouzitelnost pak je dana porovnanim velikosti f(N) s tim, co mam realne k dispozici k reseni naseho realneho problemu.

Hlavně to (obecně) nelze ověřit na tom samém stroji.

[Mirek Prýmek]

Hlavně to (obecně) nelze ověřit na tom samém stroji.

Jasne, ale pak si taky musime rict, co znamena slovo "obecne". To znamena "bez dalsich omezujicich podminek". A takove problemy proste v realu resit nepotrebujes.

V realu by to vypadalo asi takhle: mame tady algoritmus, o kterem vime, ze muze pouzivat maximalne 1GB RAM. Potrebujeme overit, jestli se zastavi pro vsechny mozne vstupy. Zaver: ok, ale musime to proverit pomoci pocitace, ktery ma aspon 12GB RAM!

...a to jeste vubec nemluvim o tom, ze obvykle v realu mame daleko silnejsi omezujici podminku: overovany algoritmus neni "jakykoli", ale ma nejakou strukturu. A ta struktura mi umoznuje pouzit nejakou fikanou heuristiku - napr. si vytvorit strom volani, najit kruznice, v kazde kruznici najit nejakou podminku, za ktere zarucene skonci a potom dokazat, ze ke splneni podminky zarucene dojde. Cili nic, co by pro *realne* algoritmy neslo udelat.

Ale to je celkem jedno, to je jenom tak na okraj. Dulezite je, ze to nema vubec nic spolecneho s Turingovym strojem a znalost TS nam k reseni tohodle problemu vubec nepomuze, je naprosto irelevantni a zbytecna.

[Radek Miček]

dead kenedy se tady ohani neresitelnosti halting problemu a vubec mu nedoslo, ze V PRAXI h.p. resitelny JE. A jde i naprosto trivialne dokazat, ze resitelny je.

Třeba při verifikaci programů v Coqu potřebujete garantovat totálnost funkcí - tj. potřebujete provést důkaz terminace. Tam HP řešitelný není.

[Reklama]

[Mirek Prýmek]

Třeba při verifikaci programů v Coqu potřebujete garantovat totálnost funkcí - tj. potřebujete provést důkaz terminace. Tam HP řešitelný není.

Jeste jednou: pokud mam abstraktni program pro abstraktni, nicim neomezeny stroj, tak HP ani teoreticky resitelny neni. Pokud mam realny program pro realny stroj, tak HP teoreticky resitelny je. Vzdy a dokazatelne. Jak je to prakticky, to uz je jina otazka.

[Rax]

Třeba při verifikaci programů v Coqu potřebujete garantovat totálnost funkcí - tj. potřebujete provést důkaz terminace. Tam HP řešitelný není.

To rozhodně nepotřebujeme. My potřebujeme vědět zda program na mašině i7-3770K s 16 GB RAM skončí do příštího pondělí, jinak zákazník nedostane výsledky včas a nezaplatí fakturu.

[Radek Miček]

pokud mam abstraktni program pro abstraktni, nicim neomezeny stroj, tak HP ani teoreticky resitelny neni. Pokud mam realny program pro realny stroj, tak HP teoreticky resitelny je. Vzdy a dokazatelne. Jak je to prakticky, to uz je jina otazka.

Jenže při verifikaci v Coqu potřebujete totálnost nad všemi vstupy - tj. řešit HP pro daný program na ničím neomezeném stroji. Netotální funkce vám totiž do logického systému Coqu vnáší spor a celá verifikace je k ničemu.

[Mirek Prýmek]

Jenže při verifikaci v Coqu potřebujete totálnost nad všemi vstupy - tj. řešit HP pro daný program na ničím neomezeném stroji. Netotální funkce vám totiž do logického systému Coqu vnáší spor a celá verifikace je k ničemu.

Coq neznam, takze konkretne nemuzu rict, ale obecne u takovychto problemu jde o to, ze jsou to prave problemy zadane tak, ze nejsou nicim omezene. A ta neresitelnost primo plyne prave z te neomezenosti.

Overit totalnost funkce nad nejakou konecnou strukturou je trivialita. Overit totalnost nad nekonecnou strukturou samozrejme bez nejake heuristiky obecne nejde, na tom neni nic prekvapiveho.

Je to zhruba tak stejne, jako byt strasne prekvapeny, ze realny pocitac neumi secist dve libovolne velka cela cisla - jednou mu proste dojde pamet no. To ale nic nemeni na tom, ze D.K. tady machruje, jak ho skola vybavila a opak je pravdou.

[JurIT]

este vas to stale bavi? co tak radsej si precitat knizku, pozriet film alebo skocit von?

[Radek Miček]

To rozhodně nepotřebujeme. My potřebujeme vědět zda program na mašině i7-3770K s 16 GB RAM skončí do příštího pondělí, jinak zákazník nedostane výsledky včas a nezaplatí fakturu

Pro část programu, jenž se spouští, je samozřejmě důležitá i složitost (a nikde netvrdím opak). Ale pro část programu, jenž se nespouští (například důkaz některých vlastností), stačí pouze totálnost.

Idea je: typy jsou tvrzení a funkce jsou jejich konstruktivní důkazy - bez totálnosti funkcí bych mohl dokázat cokoliv, neboť např. funkce, jenž nikdy nic nevrátí (cyklí), může mít libovolný typ (dokazuje libovolné tvrzení).

[Mirek Prýmek]

Idea je: typy jsou tvrzení a funkce jsou jejich konstruktivní důkazy - bez totálnosti funkcí bych mohl dokázat cokoliv, neboť např. funkce, jenž nikdy nic nevrátí (cyklí), může mít libovolný typ (dokazuje libovolné tvrzení).

No a co se tim snazis rict? Ze si umime vymyslet problemy, ktere nejsou ani teoreticky resitelne? To ale vsichni vime a nikdo to nerozporuje. Jenom to jaksi vubec nesouvisi s tim, o cem psal DK, a od ceho se tahle nova iterace stare debaty odpichla...

[JurIT]

pani, ak vas zaujima formalna verifikacia a validacia, odporucim vas na na FIT VUT je tam vedecka skupina pod nazvom VeriFIT, mozte sa realizovat, su tam velmi kvalifikovani ludia na vysokej urovni co sa tohoto tyka.

[Jakub Galgonek]

pani, ak vas zaujima formalna verifikacia a validacia, odporucim vas na na FIT VUT je tam vedecka skupina pod nazvom VeriFIT, mozte sa realizovat, su tam velmi kvalifikovani ludia na vysokej urovni co sa tohoto tyka.

Taková skupina je i na MFF UK.

[Mirek Prýmek]

Taková skupina je i na MFF UK.

Tak at nejsem pozadu: i na FI MU: http://www.fi.muni.cz/research/formal-methods/verification.xhtml.cs