VŠ z trochu jiného úhlu

[Radek Miček]

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.

Snažím se říct to, že při programování v určitých programovacích jazycích potřebujete dokázat, že funkce je totální pro všechny vstupy a nestačí to jen pro některé (což mj. znamená, že musíte dokázat, že na každém vstupu zastaví).

[Reklama]

[Mirek Prýmek]

Snažím se říct to, že při programování v určitých programovacích jazycích potřebujete dokázat, že funkce je totální pro všechny vstupy a nestačí to jen pro některé (což mj. znamená, že musíte dokázat, že na každém vstupu zastaví).

Hm, to jsme radi, ze to vime. A jak to souvisi s tematem?

[Rax]

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.

Část programu která se nespouští patří z projektu vyhodit preventivně.
U části programu která se spouští potřebuji znát jenom míru složitosti s ohledem na příští pondělí. Informace že jistojistě by to bylo příštího Silvestra nebo to neskončí nikdy jsou mi platné jako mrtvému zimník

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í).

To nepotřebuji, nekonečné smyčky odhaluji jinými prostředky.

[Radek Miček]

Hm, to jsme radi, ze to vime. A jak to souvisi s tematem?

Pokud připustíte, že programování v jazyce Coq (nebo jiném podobném jazyce - např. Isabelle) je součást praxe, tak to odporuje vašemu tvrzení:

V PRAXI h.p. resitelny JE. A jde i naprosto trivialne dokazat, ze resitelny je.

[Radek Miček]

Část programu která se nespouští patří z projektu vyhodit preventivně.

Pak se může stát, že ten program ani nepřeložíte.

[Reklama]

[Mirek Prýmek]

.

Pokud připustíte, že programování v jazyce Coq (nebo jiném podobném jazyce - např. Isabelle) je součást praxe, tak to odporuje vašemu tvrzení:

V PRAXI h.p. resitelny JE. A jde i naprosto trivialne dokazat, ze resitelny je.

Mluvil jsem samozrejme o problemu zastaveni realneho (cili omezeneho) pocitace. Cili napriklad problem zastaveni i386 s 1GB RAM. Myslel jsem, ze to je z kontextu dostatecne jasne.

To, o cem pisete vy, je JINY problem, o kterem jsem nemluvil.

[Jakub Galgonek]

tak to odporuje vašemu tvrzení:

V čem přesně má být ten rozpor?

[Radek Miček]

V čem přesně má být ten rozpor?

I v praxi je třeba řešit terminaci pro všechny vstupy, tudíž i v praxi se vyskytuje obecný HP.

[Mirek Prýmek]

I v praxi je třeba řešit terminaci pro všechny vstupy, tudíž i v praxi se vyskytuje obecný HP.

To je naprosto nesmyslna argumentace.

To je asi tak jako bych rekl, ze filosof X resi problem, kolik andelu se vejde na spicku jehly -> resi se to v praxi -> je to prakticky problem.

[Radek Miček]

To je asi tak jako bych rekl, ze filosof X resi problem, kolik andelu se vejde na spicku jehly -> resi se to v praxi -> je to prakticky problem.

Takže nechcete připustit, že to je v praxi?

[Jakub Galgonek]

Takže nechcete připustit, že to je v praxi?

Jde o to, že v praxi tam nekonečně mnoho různých vstupů stejně rvát nemůžeš.

[Radek Miček]

Jde o to, že v praxi tam nekonečně mnoho různých vstupů stejně rvát nemůžeš.

Jde o existenci totální funkce s daným typem (viz Curry–Howard correspondence) - ta funkce je důkaz a až si ho kompilátor ověří, tak tu funkci může zahodit. Ta funkce se vůbec nemusí vyhodnocovat.

[student]

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.

Ked myslis nepresne povedane len u "beznych programov", tak to plati (programatori sa snazia programovat tak, aby ich program skoncil a bolo to vidiet).

Ale ukaz mi ten trivialny dokaz v PRAXI v dobe, ked mozeme menit disky, mame siet a naviac vyrobcovia stale produkuju dalsie a stale vacsie zaznamove media. Podla mna sa neda jednoducho obmedzit stavovy priestor niecim ako 2^(#"pamatovych buniek" v PC), lebo ak to pritiahneme za vlasy, tak si algoritmus moze lubovolne pytat dalsiu kapacitu a my sme schopni mu ju nejak v rozumnom case dodat (=>prakticky nekonecny stavovy priestor).
Keby islo napriklad aj pri kompilacii Linuxu o blackbox, ktory bud da vysledok "OK" a binarku alebo zahlasi chybu, tak by som naozaj nebol schopny rozhodnut, ci si gcc v nekonecnom cykle len alokuje disk, vytazuje CPU a potom napise "no space left on device" alebo naozaj nieco kompiluje a "no space left on device" je len znamka toho, ze potrebuje vacsi disk, na ktorom uz skonci.
Potom si mozeme nahradit hlasku "no space left on device" cyklom cakajucim na volne miesto a mame "ten teoreticky" HP (ak sa teda nemylim).

V praxi sa to riesi obmedzenim niecoho "nekonecneho" - tj. dam kompilacii napr. 5GB a na zaklade toho usudim, ze Linux nejde skompilovat a vzdy zahlasi "no space left on device". Alebo dobu stravenu kompilaciou. V principe to ale neriesi HP.

Jeze ty prvocisla sou knicemu , dostal si zcela praktickou odpoved. Stejne tak je pro 99% lidi k nicemu trebas Huble ... jsou z toho pekny obrazky a to je tak vsechno.

Povedat, ze su "k nicomu" je asi dost silne, kedze ich (aspon nevedome) pouzivaju ludia pri prihlasovani sa k internet bankingu alebo mozno aj k svojmu emailu.
Ale inak by sme mohli postupovat aj tvojim smerom - ta elektrina vlastne k nicomu 99% ludom nie je - 99% ludi nevlastni elektrarne, nie su elektrikari, ktorym to prinasa zisk a ani nevedia skoro nic o tom, ako to funguje.

Tvoje názory a řešení nikoho nebudou zajímat, drtivá většina věcí v IT je dávno vyřešena, jsou na to vyzkoušené a zavedené postupy a ty je budeš jenom aplikovat. Potrvá dlouhé roky než tě někdo možná pustí něco skutečně řešit.

Ak ide len o aplikaciu postupov, tak na to sprav program - mozes ho predavat ako programatora na mojej urovni, ktory nebude robit chyby (vzdy bude spravne aplikovat postupy). Ak by si takeho "virtualneho programatora" predaval za 1000€ hodinu - totiz pocitac zvlada aplikovanie postupov radovo rychlejsie ako clovek, tak mas pri 1000 takto predanych programatoroch isty zarobok na zaciatku nieco ako 1M€/h; neskor aj viac. To podla mna za pokus stoji.
Alebo to nie je len o aplikovani postupov?

[Mirek Prýmek]

lebo ak to pritiahneme za vlasy, tak si algoritmus moze lubovolne pytat dalsiu kapacitu a my sme schopni mu ju nejak v rozumnom case dodat (=>prakticky nekonecny stavovy priestor).

Zaprve to neni pravda. Moznosti kazdeho stroje jsou celkem jasne omezene. Stavovy prostor kazdeho stroje je a vzdy bude omezeny.

Zadruhe to je hloupy predpoklad, protoze pokud se bavime o skutecne realnych problemech ve skutecne realnych podminkach, tak vzdy mame ramcovou predstavu o narocnosti algoritmu. Spravne to rika Rax: pokud soucet dvou 32bitovych cisel bude trvat deset let, tak nas proste uz vysledek nezajima.

[Mirek Prýmek]

Jde o existenci totální funkce s daným typem (viz Curry–Howard correspondence) - ta funkce je důkaz a až si ho kompilátor ověří, tak tu funkci může zahodit. Ta funkce se vůbec nemusí vyhodnocovat.

Jazkovanoho ale to je prece uplne jedno, o co jde. Dulezite je, ze jediny zpusob, jak zajistit strojovou nedokazatelnost neceho nad nejakou strukturou (a je uplne jedno o jakou strukturu se jedna) je to, ze ten stroj prochazi stale novymi a novymi stavy. Opakuju: je uplne jedno, o co se jedna: muze to byt ten tvuj solver, kde "se nic nespousti, jenom overuje", nebo to muze byt pocitac, to je proste jedno. Dulezite je, ze jakysi vypocet ma moznost nabyvat stale novych a novych stavu, cimzpadem ma moznost se nikdy nezastavit, cimzpadem se nikdy nedovime vysledek takoveho vypoctu.

Jenze to je ciste teoreticky (matematicky) koncept. realne nikdy nemuze existovat jakykoli stroj/mechanismus/robot/cokoli... co by mohlo nabyvat stale nove a nove stavy. A jelikoz pocet stavu je nejak shora omezeny, tak proste k tehle TEORETICKE neresitelnosti nikdy nedojde.

Jeste jednou, naposledy a uplne polopaticky: zjistovani vlastnosti* nicim neomezeneho stroje, je ciste jenom teoreticky problem, protoze nicim neomezeny stroj neexistuje a nikdy existovat nebude. Vsechny stroje, ktere mame ted, ktere budeme mit zitra a az do skonani veku, jsou a vzdy budou omezene a proto i jejich zastaveni je teoreticky resitelne.

* napr. za jakych okolnosti se zastavi nebo nezastavi