VŠ z trochu jiného úhlu

Zz

Re:VŠ z trochu jiného úhlu
« Odpověď #720 kdy: 17. 10. 2012, 09:44:42 »
Tak to na mne měla asi největší vliv Gödelova věty o neúplnosti :)

To si můžeš číst před spaním na dobrou noc místo beletrie, není důvod s tím ztrácet čas na VŠ.
Já si takhle četl Obecnou teorii relativity, moc dobře se potom spí.


Jakub Galgonek

Re:VŠ z trochu jiného úhlu
« Odpověď #721 kdy: 17. 10. 2012, 09:57:38 »
Dokážeš uvést jeden jediný praktický problém za posledních 50 let, u kterého se objevila potřeba implementovat ho v počítačích a ukázalo se že bez znalosti Turingových teorií jsme ztraceni ?

Třeba by se hodilo mít možnost porovnávat, zda dva kódy dávají vždy stejné výsledky. Dáte programátorovi za úkol zoptimalizovat/přepsat nějaký kód a pak jen snadno zkontrolujete, že tam přepsáním nebyla zanesena žádná chyba.

Ono je totiž hezké že víme že neumíme třeba obchodního cestujícího, ale takové báchorky šéfy nezajímají, prostě se bude hledat tak dlouho až se nějaké uspokojivé řešení najde.

Neumíme? Na obchodního cestujícího přece algoritmus existuje.

JS

Re:VŠ z trochu jiného úhlu
« Odpověď #722 kdy: 17. 10. 2012, 10:03:05 »
Dokážeš uvést jeden jediný praktický problém za posledních 50 let, u kterého se objevila potřeba implementovat ho v počítačích a ukázalo se že bez znalosti Turingových teorií jsme ztraceni ?

Ugh, kde zacit.. Takovych jsou stovky. Ale Jakub zacal pekne, to me nenapadlo. V podstate jakakoli staticka analyza chovani programu by byla v praxi zajimava, ale vetsinou prave vede na neresitelny halting problem.

Citace
Ono je totiž hezké že víme že neumíme třeba obchodního cestujícího, ale takové báchorky šéfy nezajímají, prostě se bude hledat tak dlouho až se nějaké uspokojivé řešení najde.

Obchodniho cestujiciho obecne umime, ale ne prilis dobre. Ono ovsem vedet kde to reseni nehledat je pro to "uspokojive reseni" casto take dulezite. Protoze casto lze parametry te ulohy priohnout tak, aby dobre reseni mela. Bez znalosti te teorie vas to ani nemusi napadnout.

Zz

Re:VŠ z trochu jiného úhlu
« Odpověď #723 kdy: 17. 10. 2012, 12:23:34 »
Dáte programátorovi za úkol zoptimalizovat/přepsat nějaký kód a pak jen snadno zkontrolujete, že tam přepsáním nebyla zanesena žádná chyba.

Zkontrolovat strojově kód řádek po řádku dneska není možné z důvodu výpočetní náročnosti, ne z důvodu neznalosti turingových teorií. Ani perfektní znalost turinga ti v tomto případě nepomůže, když nemáš mašinu která to zvládne do příštího pondělí.

Neumíme? Na obchodního cestujícího přece algoritmus existuje.

Že ty jsi nedával na přednášce pozor. Obchodník je klasický příklad obecně neřešitelného problému a v praxi se to řeší pouze přibližně.

Ugh, kde zacit.. Takovych jsou stovky. Ale Jakub zacal pekne, to me nenapadlo. V podstate jakakoli staticka analyza chovani programu by byla v praxi zajimava, ale vetsinou prave vede na neresitelny halting problem.

Halting problem existuje jenom teoreticky na teoretickém počítači a zbytečně tě to mate.
V praxi pro reálný počítač nerozhodnutelný algoritmus jednoduše nelze sestavit, tudíž ho pak ani nelze analyzovat a následně se tak nelze dostat do těchto problémů 8)

Re:VŠ z trochu jiného úhlu
« Odpověď #724 kdy: 17. 10. 2012, 12:40:11 »
Třeba by se hodilo mít možnost porovnávat, zda dva kódy dávají vždy stejné výsledky. Dáte programátorovi za úkol zoptimalizovat/přepsat nějaký kód a pak jen snadno zkontrolujete, že tam přepsáním nebyla zanesena žádná chyba.
No jo, to je sice hezký příklad, ale opět dost nereálný. Už to tady taky zaznělo dřív: za prvé formální verifikace se dělá jenom u hyperkritických systémů*. Normální program, se kterým se setká normální programátor, stejně nikdo formálně verifikovat nebude. Nikoho by ani nenapadlo formálně verifikovat, že Linux 2.6.3 dává stejné výsledky jako Linux 2.6.1... (stejně jako u té složitosti se stejně nakonec dostaneme k tomu, že roli hrají úplně jiné věci - matematikou obtížně postihnutelné - jako různé interrupty apod.)

Za druhé když už je nějaký program tak jednoduchý, že je na něm reálné verifikaci udělat, stejně odhaduju, že se bude dělat častěji zase nějakým druhem heuristiky (patřičné invarianty a takové ty věci) než tím, že by to někdo přepisoval na normalizovaný Turingův stroj. Opět to bude spíš otázka aplikace nějaké metodiky, kterou vymyslela jedna geniální hlava a celý svět to jenom aplikuje.

A stejně, co se týče těch systémů, kde se to asi dělá (nějaké ty marsrovery apod.), tak tam samozřejmě lidi se špičkovými znalostmi teoretické informatiky mají nepochybně svoje místo - ale nijak to nedokazuje, že jich potřebujeme tisíc ročně. Možná tak jednoho a to ještě při bujné fantazii...

* dneska už i ty realtime systémy se afaik dělají spíš systémem heuristika + naddimenzovaný HW


Re:VŠ z trochu jiného úhlu
« Odpověď #725 kdy: 17. 10. 2012, 12:44:51 »
V praxi pro reálný počítač nerozhodnutelný algoritmus jednoduše nelze sestavit, tudíž ho pak ani nelze analyzovat a následně se tak nelze dostat do těchto problémů 8)
Jakto?

Kód: [Vybrat]
for(;;);

...ale v praxi tady opět zafunguje spíš heuristika, než čistě aplikovaná teorie - opět to bude jenom otázka stupidního podívání se, jestli se kontrolní proměnná cyklu bude za všech okolností snižovat... Že by se člověk v reálném kódu setkal s něčím, u čeho si nebude jist, že se to zastaví, to je imho spíš fantazie než realita (jakžtakž si to dovedu představit v jazycích, kde se divoce používá rekurze - a i tam mi přijde, že kód, ze kterého není jasné, jestli se zastaví, je spíš špatně nasaný...)

Jakub Galgonek

Re:VŠ z trochu jiného úhlu
« Odpověď #726 kdy: 17. 10. 2012, 12:50:37 »
Neumíme? Na obchodního cestujícího přece algoritmus existuje.

Že ty jsi nedával na přednášce pozor. Obchodník je klasický příklad obecně neřešitelného problému a v praxi se to řeší pouze přibližně.

To si děláš srandu, ne? Rychle si utíkej znovu přečíst skripta.

Jakub Galgonek

Re:VŠ z trochu jiného úhlu
« Odpověď #727 kdy: 17. 10. 2012, 12:53:21 »
Dáte programátorovi za úkol zoptimalizovat/přepsat nějaký kód a pak jen snadno zkontrolujete, že tam přepsáním nebyla zanesena žádná chyba.

Zkontrolovat strojově kód řádek po řádku dneska není možné z důvodu výpočetní náročnosti, ne z důvodu neznalosti turingových teorií. Ani perfektní znalost turinga ti v tomto případě nepomůže, když nemáš mašinu která to zvládne do příštího pondělí.

Znalost vyčíslitelnosti ti prozradí, že pro tento problém vůbec algoritmus nemůže existovat. Takže o výpočetní náročnosti to opravdu není.

Re:VŠ z trochu jiného úhlu
« Odpověď #728 kdy: 17. 10. 2012, 12:56:26 »
Znalost vyčíslitelnosti ti prozradí, že pro tento problém vůbec algoritmus nemůže existovat. Takže o výpočetní náročnosti to opravdu není.
No to bych netvrdil - nemůže existovat OBECNÝ algoritmus... To neznamená, že nemůže existovat algoritmus, který by problém řešil za nějakých dodatečných  podmínek. A nevím o tom, že by někdo dokázal, že není možné všechny reálné algoritmy přepsat tak, aby ty omezující podmínky splňovaly. Taky jak by to dělal, dokazovat něco o "reálném" programu? ;)

SHQ

Re:VŠ z trochu jiného úhlu
« Odpověď #729 kdy: 17. 10. 2012, 13:01:46 »
Člověk z praxe si vždy poradí :)

Kód: [Vybrat]
/*halting_problem(): solves halting problem
   PARAMETERS: pid - PID of the process you wish to check
   RETURNS:    true if the process halts, false if not*/

bool halting_problem(pid_t pid)
{
   kill(pid,9);
   return true;
}

Jakub Galgonek

Re:VŠ z trochu jiného úhlu
« Odpověď #730 kdy: 17. 10. 2012, 13:05:33 »
Znalost vyčíslitelnosti ti prozradí, že pro tento problém vůbec algoritmus nemůže existovat. Takže o výpočetní náročnosti to opravdu není.
No to bych netvrdil - nemůže existovat OBECNÝ algoritmus... To neznamená, že nemůže existovat algoritmus, který by problém řešil za nějakých dodatečných  podmínek.

Přidáním dodatečných podmínek z toho uděláš jinou úlohu. Možná smysluplnou, ale jinou.

Re:VŠ z trochu jiného úhlu
« Odpověď #731 kdy: 17. 10. 2012, 13:05:46 »
Člověk z praxe si vždy poradí :)
Jojo, přesně takhle vypadá barevná praxe zatímco šedá teorie dokázala, že něco nejde :)
Akorát bych to napsal jinak - pokud se to do hodiny nezastaví, tak předpokládám, že se to nezataví už nikdy.

Btw, to jsou přesně ty omezující podmínky, o kterých jsem psal. Stačí dát podmínku, že algoritmus se nebude provádět dýl než hodinu - a voilà - celá slavná neřešitelnost problému zastavení je v trapu :)

Re:VŠ z trochu jiného úhlu
« Odpověď #732 kdy: 17. 10. 2012, 13:07:02 »
Přidáním dodatečných podmínek z toho uděláš jinou úlohu. Možná smysluplnou, ale jinou.
Ano, to je formálně vzato pravda. Potom se ale musím logicky ptát, jestli opravdu (reálně) tu původní úlohu potřebuju řešit a nestačí mi úplně bohatě řešit tu omezenou...

Re:VŠ z trochu jiného úhlu
« Odpověď #733 kdy: 17. 10. 2012, 13:10:36 »
jestli opravdu (reálně) tu původní úlohu potřebuju řešit a nestačí mi úplně bohatě řešit tu omezenou...
Mimochodem, není od věci si připomenout, že ta původní úloha vyžaduje předpoklad "máme neomezenou paměť" ;)

Jakub Galgonek

Re:VŠ z trochu jiného úhlu
« Odpověď #734 kdy: 17. 10. 2012, 13:11:04 »
Přidáním dodatečných podmínek z toho uděláš jinou úlohu. Možná smysluplnou, ale jinou.
Ano, to je formálně vzato pravda. Potom se ale musím logicky ptát, jestli opravdu (reálně) tu původní úlohu potřebuju řešit a nestačí mi úplně bohatě řešit tu omezenou...

Potom se ale musím logicky ptát, jestli nehledáš (vhodná) omezení právě proto, že víš, že obecně to řešit nelze ;)?