VŠ z trochu jiného úhlu

[Mirek Prýmek]

A mimochodem, nejjednodušší automat, pro který je obecný problém zastavení nerozhodnutelný, je "counter automaton" (nevím, jak se tomu říká česky, asi automat s čítačem). Stačí jediná paměťová buňka, schopná držet neomezené přirozené číslo.

Proč?

No protože držet "neomezené přirozené číslo" vyžaduje mít k dispozici neomezené množství paměti - a z toho právě plyne neomezené množství stavů a tímpádem ta nerozhodnutelnost.

Čili "teoretická nerozhodnutelnost" je čistý jednorožec. V praxi hraje a vždycky bude hrát roli jenom "praktická nerozhodnutelnost".

[Reklama]

[Zz]

No tak pokud celým smyslem debaty bylo ukázat Zz-ovi, k čemu je potřeba znát TS a důkazy s ním spojené, tak to jsme se teda pochlapili

Celým smyslem debaty bylo uvědomit si, že TS v praxi nepoužijete Já to tuším už mnoho let, teorii TS mám za sebou.
A pokud má TS pouze sloužit k trénování mozku, platí můj nápad že si ho lze stejně dobře trénovat na věcech více souvisejících s IT.

[Zz]

Stačí jediná paměťová buňka, schopná držet neomezené přirozené číslo.

Za tohle jsem chtěl jít vyučujícího na přednášce zmlátit, naštěstí mě překecali ať jdu radši na pivo.

[Mirek Prýmek]

Celým smyslem debaty bylo uvědomit si, že TS v praxi nepoužijete

V tomhle se musím matematiků trochu zastat. Pokud dokážeš, že nějaká úloha nejde řešit Turingovým strojem, víš naprosto jistě, že nepůjde řešit ani skutečným strojem. Nebo ještě jinak: víš, že řešení té úlohy není závislé na paměti - i kdybys jí měl nekonečně mnoho, stejně to nevyřešíš. Potud to aspoň v bujné představivosti nějaký smysl má.

Blbý je to s opačným problémem - dokázat, že něco na normálním počítači řešit půjde. To už pomocí TS prostě dokázat nejde, protože TS má (reálně, prakticky) větší výpočetní sílu než jakýkoli počítač, který kdy bude sestrojen.

Co se týče praktičnosti, tak jsou na tom o něco líp LBA, tam už je podobnost se skutečným HW docela slušná. Paměť je sice pořád potenciálně nekonečná, ale aspoň je svázaná s délkou vstupu, takže můžeme říct něco ve stylu "ke zpracování obrázku velkého 1MB potřebujeme 1GB paměti", což je už docela prakticky použitelné.

[Zz]

V tomhle se musím matematiků trochu zastat. Pokud dokážeš, že nějaká úloha nejde řešit Turingovým strojem, víš naprosto jistě, že nepůjde řešit ani skutečným strojem. Nebo ještě jinak: víš, že řešení té úlohy není závislé na paměti - i kdybys jí měl nekonečně mnoho, stejně to nevyřešíš. Potud to aspoň v bujné představivosti nějaký smysl má.

To nepochybuji, jenže kolik takových úloh v praxi potkáš. Za 1000 příspěvků jsem viděl pouze HP který se v praxi neřeší, Haskel TS nepoužívá prokazatelně a další případ je nejistý.
Čili dokud nebudu mít jasno takovým způsobem, že například bez TS nebudu umět program na podvojné účetnictví, tak je to slabota.

[Reklama]

[Mirek Prýmek]

To nepochybuji, jenže kolik takových úloh v praxi potkáš.

Žádnou. V praxi se obvykle snažíš řešit to, co je intuitivně jasně řešitelné.

Čili dokud nebudu mít jasno takovým způsobem, že například bez TS nebudu umět program na podvojné účetnictví, tak je to slabota.

No tak on TS je formální nástroj pro dokazování, nic jiného. Takže se musíš ptát, jestli je nějaká běžná úloha, pro jejíž naprogramování nutně potřebuješ vědět nějaký důkaz. To asi není. Respektive jestli je, tak je to nějaká obskurnost v nějakém obskurním jazyce (a takové úlohy mají řešit teoretici, proti tomu snad nikdo nic nenamítá).

V běžném životě na nic takového nenarazíš... Daleko pravděpodobnější by bylo, že bys v praxi narazil na úlohu, která pomocí TS řešitelná je, ale prakticky není - ale to poznáš velmi rychle, protože v tom algoritmu prostě budeš podezřele často (a bezmezně) alokovat paměť.

Pro praktické věci se daleko víc hodí ty FSM nebo LBA, tam si dovedu praktické použití představit docela lehko. Nebo se třeba hodí vědět, že PDA se dvěma zásobníky má stejnou výpočetní sílu jako TM, to se taky může hodit, když třeba chceš zkonstruovat nějaký jednoduchý VM nebo tak něco...

[Zz]

No tak on TS je formální nástroj pro dokazování, nic jiného. Takže se musíš ptát, jestli je nějaká běžná úloha, pro jejíž naprogramování nutně potřebuješ vědět nějaký důkaz. To asi není.

Tak to se shodneme.

[poiu]

Psal jsem tady 3x, že v praxi se HP neřeší, tak počtvrté: V praxi se problém HP neřeší, nemáme nekonečnou pásku.

Automatické odstřelení zacykleného programu má dneska vyřešen každý mikrokontrolér za 1 USD a to watchdogem, na to Turinga netřeba. Dokonce máš po resetu od watchdogu zachován obsah RAM, takže se můžeš podívat co se stalo, přijdeš jenom o obsah registrů.
Na vyšší úrovni to takhle lze hravě emulovat, zabití procesu po timeoutu je triviální, vyčtení dat před zabitím je jenom mírný kus práce.

Ale ten watchdog ti niekedy odstrelí aj nezacyklenú aplikáciu, nie? U niektorých programov sa predpokladá dlhá doba výpočtu a tam je zistenie zložitejšie / nemožné a o takých programov nám ide.

[Zz]

Ale ten watchdog ti niekedy odstrelí aj nezacyklenú aplikáciu, nie? U niektorých programov sa predpokladá dlhá doba výpočtu a tam je zistenie zložitejšie / nemožné a o takých programov nám ide.

Ano a je mi to úplně jedno, nepotřebuji zjišťovat proč se tak stalo, bohatě mě stačí zjištění že štěstí že se tak stalo. Psal jsem tady už dříve, že algoritmus který neskončí do příštího pondělí letí ze skály tak jako tak.

Riziko že se budu marně pokoušet implementovat neimplementovatelný algoritmus si uvědomuji, jenže jediný takový problém který místní osazenstvo předvedlo je problém HP, ten se v praxi neřeší a teoretici to ani prakticky řešit neumí a žádný další předveden nebyl.

[Jakub Galgonek]

a žádný další předveden nebyl

A co ta ekvivalence programů?

[Radek Miček]

Riziko že se budu marně pokoušet implementovat neimplementovatelný algoritmus si uvědomuji, jenže jediný takový problém který místní osazenstvo předvedlo je problém HP, ten se v praxi neřeší a teoretici to ani prakticky řešit neumí a žádný další předveden nebyl.

Praktická úloha je automatické dokazování v logice prvního řádu - dokazovače jsou navíc psány tak, že mohou běžet neomezeně dlouho.

[Jakub Galgonek]

a žádný další předveden nebyl

Další algoritmicky nerozhodnutelný problém je třeba, zda dvě bezkontextové gramatiky generují stejný jazyk, anebo zda je bezkontextová gramatika nejednoznačná.

[poiu]

Ano a je mi to úplně jedno, nepotřebuji zjišťovat proč se tak stalo, bohatě mě stačí zjištění že štěstí že se tak stalo. Psal jsem tady už dříve, že algoritmus který neskončí do příštího pondělí letí ze skály tak jako tak.

Ale stratíš týždeň. A sú firmy, kde sa bežne niečo robí aj mesiac - keďže sa nastavujú externé zariadenia, na ktorých sa trávi drvivá väčšina času a teda sa toto nedá rozumne urýchliť. A keď sa to nevhodným spôsobom zacyklí na začiatku (možno), tak sa to zle ladí, lebo zväčša vývojárom všetko funguje a užívateľom niekedy nie. Zvlášť keď je bug v niečom triviálnom ako že pre vhodné floaty a,b a b>0 platí a + b = a. To sa niekedy vyskytne, niekedy nie - a externe zistiť takéto chyby je ťažké - prevádzka zacykleného stroja ti berie čas (peniaze), elektrinu (zase peniaze) a možno budeš musieť platiť ešte pokutu za to, že niečo nestihneš (veľké peniaze).

[Zz]

A co ta ekvivalence programů?

Máš to naimplementováno ? Kde se to dá stáhnout nebo koupit ?

[Zz]

Praktická úloha je automatické dokazování v logice prvního řádu - dokazovače jsou navíc psány tak, že mohou běžet neomezeně dlouho.

To je pořád dokola, nic nemůže běžet neomezeně dlouho.