VŠ z trochu jiného úhlu

[Mirek Prýmek]

Jenže tohle obecně nefunguje, když neznáte velikost té pásky (co když uživatel přidá paměť?).

Stejně tohle nemá vůbec smysl řešit, takové věci se prostě v praxi obvykle nedějí.

Obvyklý program když běží dlouho, tak nejspíš provádí nějaké iterace s cílem něčeho dosáhnout. Nějproblematičtější jsou možná stochastické algoritmy typu neuronek. Ale tam se to afaik opět řeší úplně stupidně "inženýrsky" - sleduje se, jestli dochází ke konvergenci a když ne, tak se prostě předpokládá, že lepší už to nebude. A spadla klec!

[Reklama]

[Jakub Galgonek]

Hraje to nějakou roli u té dříve zmiňované nemožnosti (obecně) zjistit, zda dva programy dělají totéž?

To řekněte vy teoretici - a dokažte

Já nejsem teoretický informatik

Ale viděl bych to asi nějak takto:

Mějme algoritmus a, který se vždy zastaví (tj. vždy potřebuje jen konečnou pásku). Tento algoritmus tedy vyčísluje nějakou obecně rekurzivní funkci f. Uvažujme množinu A všech algoritmů, které vyčíslují f. Pak já tvrdím, že A není rekurzivní. Tedy nejde rozhodnout, zda nějaké x náleží do A (a dělá tedy totéž co a) anebo ne.

Pro spor předpokládejme, že A rekurzivní je. Pak zle zkontruovat obecně rekurzivní funkci g takovou, že:
g(t) = k iff k not in A
     = l iff k in A
Kde k je libovolný prvek z A a l je libovolný prvek z doplňku A.

Z věty o rekurzi plyne, že existuje n takové, že algoritmus n dělá totéž co algoritmus g(n). Což je spor, neboť g(n) vždy dělá něco jiného než n.

[Jakub Galgonek]

Omlouvám se, má to být:

g(t) = k iff t not in A
     = l iff t in A

[Radek Miček]

Ano, počítač má konečnou paměť, kde lze HP rozhodovat triviálně (alespoň teoreticky). Jenže prakticky je počet možných stavů příliš velký, takže je triviální řešení nepoužitelné (proto GHC používá praktické řešení, kdy má zásobník s kontexty omezenu maximální velikost - standardně 201).

Teď jsem se nějak ztratil. Takže i když tvůrci GHC měli k dispozici aktuální výtisk Turinga, tak jim v praxi moc nepomoh a museli vzít za vděk pekelnou praxí kontrolou stack overflow, tedy jak by to dělali kdyby o žádném Turingovi nevěděli ?

Právě věděli, že by kompilátor nemusel skončit, tak tam dali nějaké omezení. Stejně tak díky oné teorii ví, že typová inference je pro polymorfismus vyšších řádů nerozhodnutelná, a proto tam GHC Haskell a jiné programovací jazyky vynucují typové anotace.

[Zz]

Za predpokladu konečnej abecedy (čo je v PC zrejmé) si myslím, že ano - konečná páska => konečný počet stavov počítača => stačí zistiť ekvivalenciu konečných automatov a to vieme => vieme zistiť, či 2 programy robia to isté.
Mám tam niekde chybu?

Teoreticky nevím.
V praxi jsou dva programy nade vší pochybnost ekvivalentní pouze tehdy, když se přeloží na identický strojový kód.

[Reklama]

[Radek Miček]

Za predpokladu konečnej abecedy (čo je v PC zrejmé) si myslím, že ano - konečná páska => konečný počet stavov počítača => stačí zistiť ekvivalenciu konečných automatov a to vieme => vieme zistiť, či 2 programy robia to isté.
Mám tam niekde chybu?

V praxi jsou dva programy nade vší pochybnost ekvivalentní pouze tehdy, když se přeloží na identický strojový kód.

Ano, máte pravdu. Kolegové mají na mysli, zda programy počítají ekvivalentní funkci.

[poiu]

Mějme algoritmus a, který se vždy zastaví (tj. vždy potřebuje jen konečnou pásku). (...)

Pozor - toto sa mi nepáči. My chceme niečo dokazovať z konečnej pásky, teda Má Konečnú Pásku (MKP) => .. => vieme zistiť, či 2 programy Robia To Isté (RTI).

Vy ste ale použili
Vždy zastaví => MKP
pričom
Vždy zastaví => .... => RTI
je spor

To ale nehovorí nič o MKP => RTI - alebo sa mýlim?

Implikácia "MKP => Vždy zastaví" zrejme neplatí - stačí si nájsť TS, ktorý sa bude stále skákať L a R medzi 2 poľami.

[Zz]

Právě věděli, že by kompilátor nemusel skončit, tak tam dali nějaké omezení.

Omezení je tam tak nějak samo od sebe Buď to vyhnije na protection fault nebo na VirtualAlloc.
Já to vidím tak, že na to nedošli z Turinga, ale že když začali kompilovat složitější programy tak to začalo takto uhnívat a aby se uživatelé nelekali, tak to trochu učesali a dali tam mravoučné hlášky
Ale to je samozřejmě čirá spekulace.

[poiu]

Za predpokladu konečnej abecedy (čo je v PC zrejmé) si myslím, že ano - konečná páska => konečný počet stavov počítača => stačí zistiť ekvivalenciu konečných automatov a to vieme => vieme zistiť, či 2 programy robia to isté.

Mám tam niekde chybu?

Jenže tohle obecně nefunguje, když neznáte velikost té pásky (co když uživatel přidá paměť?).

Keď je užívateľ obmedzený max. veľkosťou pamäte, tak sme tam kde sme boli.
A keď nie je obmedzený a môže si pridávať ako sa mu páči, tak to je presne "potenciálne nekonečno" pamäti a teda neplatí predpoklad o konečnej páske a nemá zmysel sa baviť o dôsledkoch. Alebo to bolo myslené inak?

[Jakub Galgonek]

Mějme algoritmus a, který se vždy zastaví (tj. vždy potřebuje jen konečnou pásku). (...)

Pozor - toto sa mi nepáči.

Pokud si to změníte na "nepotřebuje více jak x políček pásky", tak by to snad nemělo nic změnit.

[Mirek Prýmek]

Pokud si to změníte na "nepotřebuje více jak x políček pásky", tak by to snad nemělo nic změnit.

Nejsem si jistej, jestli je ten důkaz korektní.

Když si vezmu třeba hloupé sčítání s neomezenou přesností - neexistuje žádné x takové, aby mi páska délky x stačila. Mám algoritmus, který se zaručeně zastaví, a přitom potřebuju (potenciálně) nekonečnou pásku.

[poiu]

Mějme algoritmus a, který se vždy zastaví (tj. vždy potřebuje jen konečnou pásku). (...)

Pozor - toto sa mi nepáči.

Pokud si to změníte na "nepotřebuje více jak x políček pásky", tak by to snad nemělo nic změnit.

To máte pravdu, to skoro nič nezmení - stále mi tam chýba implikácia vychádzajúca z prvého kroku do ďalšieho kroku.  Akurát teraz beriem ako prvý krok "nepotřebuje více jak x políček pásky".

[Mirek Prýmek]

Když si vezmu třeba hloupé sčítání s neomezenou přesností - neexistuje žádné x takové, aby mi páska délky x stačila. Mám algoritmus, který se zaručeně zastaví, a přitom potřebuju (potenciálně) nekonečnou pásku.

- přijde mi, že to docela koresponduje s intuitivní představou: mám-li konečné množství stavů, potom musí být nutně možnost porovnání výpočtu hrubou silou. Ten problém, co tam zdánlivě nastává, je v tom, že při té tvé úvaze nemám konečné množství stavů, protože vstupů je nekonečně a nemám nijak garantováno, že dva různé vstupy způsobí stejný stav.

(asi to píšu kostrbatě, ale snad je jasný, co mám tak asi namysli)

[Jakub Galgonek]

Když si vezmu třeba hloupé sčítání s neomezenou přesností - neexistuje žádné x takové, aby mi páska délky x stačila. Mám algoritmus, který se zaručeně zastaví, a přitom potřebuju (potenciálně) nekonečnou pásku.

V tom pro tebe oplatí první varianta důkazu.

[Jakub Galgonek]

To máte pravdu, to skoro nič nezmení - stále mi tam chýba implikácia vychádzajúca z prvého kroku do ďalšieho kroku.

Co přesně ti tam chybí?