VŠ z trochu jiného úhlu

Jakub Galgonek

Re:VŠ z trochu jiného úhlu
« Odpověď #735 kdy: 17. 10. 2012, 13:18:16 »
pokud se to do hodiny nezastaví, tak předpokládám, že se to nezataví už nikdy.

Tomuhle přístupu se občas říká inženýrská indukce  ;)


Radek Miček

Re:VŠ z trochu jiného úhlu
« Odpověď #736 kdy: 17. 10. 2012, 13:18:56 »
Citace
Ž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

Třeba konstrukce deterministického konečného automatu derivováním regulárního výrazu.

Re:VŠ z trochu jiného úhlu
« Odpověď #737 kdy: 17. 10. 2012, 13:19:13 »
Potom se ale musím logicky ptát, jestli nehledáš (vhodná) omezení právě proto, že víš, že obecně to řešit nelze ;)?
Moc hezká a správná argumentace!

Ovšem tím se dostáváme k tomu, co už jsem tady taky psal: že běžnému programátorovi bohatě stačí vědět, že obecný problém zastavení je neřešitelný. Víc se v tom rýpat pro něj imho nepřináší žádnou reálnou přidanu hodnotu, opravdu stačí jenom tahle jedna věta + její vyvětlení, asi tak na dvacet minut - a přesně o tom přece píšu: pro lidi, co ví, že půjdou do praxe, zhustit teorii jenom do toho, co se jim opravdu bude hodit vědět a zbytek hodit přes palubu ve prospěch něčeho jiného.

Re:VŠ z trochu jiného úhlu
« Odpověď #738 kdy: 17. 10. 2012, 13:20:30 »
Třeba konstrukce deterministického konečného automatu derivováním regulárního výrazu.
Což je typický reálný problém, který bude řešit víc než polovina absolventů :)

JS

Re:VŠ z trochu jiného úhlu
« Odpověď #739 kdy: 17. 10. 2012, 13:24:25 »
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í.

To neni tak uplne pravda, smysluplne analyzy dela kazdy lepsi kompilator. A netrva to moc dlouho. Problem je opravdu v tom, ze nektere analyzy udelat nemuzeme, protoze nevime, jak dlouho to bude trvat a zda to skonci.

Ž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ě.

Obecne resitelny je, protoze prostor reseni je konecny. Ale nezname lepsi zpusob, jak nalezt presne reseni, nez vyzkouset vsechna po jednom.

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)

To je nepochopeni. Nerozhodnutelne problemy se prave v praxi vyskytuji az prilis casto. To ze o nejake jejich podtride neco lze dokazat jeste neznamena, ze na to existuje obecny algoritmus - je to asi jako rozdil mezi normalni a stejnomernou konvergenci.


Radek Miček

Re:VŠ z trochu jiného úhlu
« Odpověď #740 kdy: 17. 10. 2012, 13:25:35 »
Citace
Což je typický reálný problém, který bude řešit víc než polovina absolventů :)

To sice ne, ale napadl mě jako první :-)

Re:VŠ z trochu jiného úhlu
« Odpověď #741 kdy: 17. 10. 2012, 13:28:38 »
To sice ne, ale napadl mě jako první :-)
No to je sice hezký, ale úplně mimo téma :)

Re:VŠ z trochu jiného úhlu
« Odpověď #742 kdy: 17. 10. 2012, 13:29:17 »
Tomuhle přístupu se občas říká inženýrská indukce  ;)
Jo. A v praxi se přesně tohle používá v 99.9% případů :)

JS

Re:VŠ z trochu jiného úhlu
« Odpověď #743 kdy: 17. 10. 2012, 13:29:40 »
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...

To neni tak uplne pravda - napriklad starsi verze CICSu formalne verifikovana byla. A to byl (a jeste nekde je) v praxi casto nasazovany operacni system.

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.

Ano, a to je minimalne prave to, co by si mel absolvent odnest z prednasky o Turingovych strojich (nebo vycislitelnosti) - totiz ten zakladni trik, redukci problemu na halting problem. Aby se pak zbytecne nesnazil resit obecny problem a uvedomil si, ze musi nejakym zpusobem prave zredukovat to zadani.

Re:VŠ z trochu jiného úhlu
« Odpověď #744 kdy: 17. 10. 2012, 13:33:16 »
To neni tak uplne pravda - napriklad starsi verze CICSu formalne verifikovana byla. A to byl (a jeste nekde je) v praxi casto nasazovany operacni system.
A to je příklad technologie, se kterou se setká víc než 50% absolventů? Pokud ne, je to úplně mimo mísu - opět argument proti ničemu z toho, co zaznělo.

Ano, a to je minimalne prave to, co by si mel absolvent odnest z prednasky o Turingovych strojich (nebo vycislitelnosti) - totiz ten zakladni trik, redukci problemu na halting problem. Aby se pak zbytecne nesnazil resit obecny problem a uvedomil si, ze musi nejakym zpusobem prave zredukovat to zadani.
Pořád mi nějak chybí příklad reálného problému, se kterým by se setkala většina absolventů, a který by vyžadoval umět dokazovat něco o TS.

Že by absolvent měl znt fakt "problém zastavení je obecně neřešitelný", to nezpochybňuju.

Radek Miček

Re:VŠ z trochu jiného úhlu
« Odpověď #745 kdy: 17. 10. 2012, 13:36:01 »
Ale nezname lepsi zpusob, jak nalezt presne reseni, nez vyzkouset vsechna po jednom.

Přesněji: neznáme polynomiální algoritmus.

Radek Miček

Re:VŠ z trochu jiného úhlu
« Odpověď #746 kdy: 17. 10. 2012, 13:37:21 »
Citace
A to je příklad technologie, se kterou se setká víc než 50% absolventů?

S čím vším se vlastně setká více než 50% absolventů?

Re:VŠ z trochu jiného úhlu
« Odpověď #747 kdy: 17. 10. 2012, 13:49:06 »
S čím vším se vlastně setká více než 50% absolventů?
Např. s cyklem while :)

Jakub Galgonek

Re:VŠ z trochu jiného úhlu
« Odpověď #748 kdy: 17. 10. 2012, 13:57:55 »
S čím vším se vlastně setká více než 50% absolventů?
Např. s cyklem while :)

S čím vším se vlastně setká více než 50% absolventů a bežně/povinně se to neučí?

JS

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

Dobre, ale jeste zbyva dokazat, ze operacni system prislusnou ulohu skutecne vzdy zastavi.  :P (A to neni jen teoreticka otazka - na cele rade operacnich systemu se mi parkrat prihodilo, ze k tomu nedoslo.)