Gödel a staticky typované jazyky

[BaldSlattery]

Právě jsem tu "validnost" chtěl zjednodušit na něco konkrétního a definovat co to ten typový systém vlastně je.

To by byl dobrý začátek

[Reklama]

[BaldSlattery]

zabývat tím, jestli existuje takový algoritmus/systém, že pro každý program, který pro všechny validní vstupy skončí, existuje důkaz.

To bohužel neplatí, důkaz lze zaručeně najít pouze pro primitivně rekurzivní funkce.

[rkapl]

zabývat tím, jestli existuje takový algoritmus/systém, že pro každý program, který pro všechny validní vstupy skončí, existuje důkaz.

To bohužel neplatí, důkaz lze zaručeně najít pouze pro primitivně rekurzivní funkce.

Tak pro primitivně rekurzivní funkce to platí vždy, takže vlastně ani důkaz (otypování) nemusíme ověřovat. Ale proč to neplatí pro obecné programy?

[Mirek Prýmek]

zabývat tím, jestli existuje takový algoritmus/systém, že pro každý program, který pro všechny validní vstupy skončí, existuje důkaz.

To bohužel neplatí, důkaz lze zaručeně najít pouze pro primitivně rekurzivní funkce.

Tak pro primitivně rekurzivní funkce to platí vždy, takže vlastně ani důkaz (otypování) nemusíme ověřovat. Ale proč to neplatí pro obecné programy?

Mám trochu pocit, že na to jdete moc rychle a zbytečně zužujete počet lidí, kteří vám budou rozumět. Nešlo by začít tím, že to trochu zpřehledníte např. vymezením pojmů? Např.: Čemu říkám "důkaz"? Jakými prostředky je veden? V rámci jakého systému? Atd. Tohle vaše povídání je fakt srozumitelné asi jenom tomu, kdo víceméně už zná výsledek

[.]

ostatne Godel se z toho posleze zblaznil

Ne Důkazy vět o neúplnosti publikoval v roce 1931, ve svých 25 letech. Psychické problémy měl až daleko později, zemřel v 71 letech.

Než se pustíte dál, taková malá odbočka.
Jde o to tvé jednoznačné Ne v odpovědi. Výrok Godel se posleze zbláznil v odpovědi nepopíráš, takže se asi shodneme, že je to výrok pravdivý (pomiňme teď definici zbláznění). Vše se teda točí kolem slovíčka z toho. Řekl bych, že nemáme dost informací na to, aby se dalo jednoznačně říct, že se jedná o nepravdivý výrok. Za prvé není úplně jasné, co přesně znamená to "z toho" a za druhé asi úplně nevíme, z čeho konkrétně se Godel zbláznil a zda na to "to" nemohlo mít nějaký vliv.

[Reklama]

[Mirek Prýmek]

Než se pustíte dál, taková malá odbočka.
Jde o to tvé jednoznačné Ne v odpovědi. Výrok Godel se posleze zbláznil v odpovědi nepopíráš, takže se asi shodneme, že je to výrok pravdivý (pomiňme teď definici zbláznění). Vše se teda točí kolem slovíčka z toho. Řekl bych, že nemáme dost informací na to, aby se dalo jednoznačně říct, že se jedná o nepravdivý výrok. Za prvé není úplně jasné, co přesně znamená to "z toho" a za druhé asi úplně nevíme, z čeho konkrétně se Godel zbláznil a zda na to "to" nemohlo mít nějaký vliv.

Krása! Konečně někdo, kdo mluví jazykem mého kmene! Jdu do toho!

Souhlasím, že "asi úplně nevíme, z čeho se G zbláznil". Respektive přesněji: já to nevím a předpokládám, že ty taky ne, protože bys tím zřejmě argumentoval.

Jestliže to jistě nevíme, můžeme se to buď pokusit najít v literatuře (to se mi nechce) nebo zkusit najít nějaká vodítka, která by hypotéze "zbláznil se ze svých vět o neúplnosti" dávala nějakou pravděpodobnost. To udělám.

1. po publikování vět o neúplnosti G ještě relativně dlouho pracoval a to i na veřejně exponovaných místech (přednášky apod.) a složitých problémech

2. předpokládám, že kdyby už v té době nemocí trpěl, tak by se to vědělo (i já bych to věděl). Z toho vyvozuju (s nějakou pravděpodobností), že nemocí začal trpět až později, na sklonku života.

3. Pokud vím, G trpěl především (sorry za laičtinu) "stihomamem", konkrétně strachem z toho, že ho někdo chce otrávit. Prověřme pravděpodobnost, že by zrovna objevy ohledně neúplnosti toto způsobily.

Na samém začátku druhé sv. války G emigroval z Německa do USA. V USA se spřátelil s Einsteinem, pracoval v Institute for Advanced Study a začal se věnovat i fyzice. V té době v USA probíhal výzkum jaderného štěpení, o čemž nacisti věděli.

Z toho mi vychází jako daleko pravděpodobnější, že G měl strach z toho, že bude zavražděn nacistickými agenty, možná v souvislosti s výzkumem štěpení, a tento strach se vyvinul v psychické onemocnění.

Možnost, že by mu srovnatelnou úzkost způsobovaly objevy ohledně neúplnosti, mi přijde málo pravděpodobná. Z toho důvodu se kloním spíš k tomu, že teze "zbláznil se z toho" je nepravdivá.

Zároveň přiznávám, že moje znalosti psychiatrie jsou prakticky nulové, takže předpoklad "patologický stihomam se může vyvinout z relativně opodstatněné obavy" může být chybný. Možná že existence opodstatněných obav nemá na pravděpodobnost vývinu "onemocnění stihomamem" žádný vliv. Potom by argumentace v bodu 3 byla chybná.

[Mirek Prýmek]

Ještě teda by se asi slušelo dodat:

Na kategorické "Ne" striktně vztao nemám nárok, v tom se shodneme. Zaznělo to ale v kontextu neformální debaty o vágním tématu a indicie jsou (podle mě) natolik silné, že jsem v daném kontextu měl oprávnění "pravděpodobně ne" zkrátit do "ne". "Pravděpodobně ne" by podle mě bylo v daném kontextu příliš slabé a mohlo by ve čtenáři vyvolat dojem mé větší nejistoty než jaká skutečně je, což by debatě nepomohlo.

[Kit]

Jedinec s tímto duševním postižením se může chovat relativně normálně, pouze na veřejnosti nebude nic konzumovat. Při přednáškách se to neprojeví, ale domů nikoho nepustí. Takto může žít a pracovat i desítky let - ostatní ho budou brát jen jako podivína. Výraz "z toho" je dle mého názoru mylný. Možná by se za společný jmenovatel dala označit jeho touha po preciznosti.

Pouze je mi záhadou, proč si sám neuvařil, ale místo toho hladověl.

[JS]

Jak uz jsem napsal v puvodnim vlakne - Godel je v praxi irelevantni, v praxi se smirime s neuplnosti (v lepsim pripade, pokud se vubec nekdo obtezuje s korektnosti, treba typove systemy Javy a stare Scaly jsou nekorektni a nikdo z toho nema tezkou hlavu) a kde to nestaci, prida se dodatecny axiom.

[Mirek Prýmek]

treba typove systemy Javy a stare Scaly jsou nekorektni

Pořád ještě jsme si neřekli, co by to ta korektnost (a (ne)dokazatelnost) u typového systému měla být, takže tvrdit, že nějaký typový systém je nekorektní, je předčasné.

[JS]

treba typove systemy Javy a stare Scaly jsou nekorektni

Pořád ještě jsme si neřekli, co by to ta korektnost (a (ne)dokazatelnost) u typového systému měla být, takže tvrdit, že nějaký typový systém je nekorektní, je předčasné.

Vzdyt to bylo receno v tom odkazu, co posilal OP. Ze typovy system neni korektni znamena, ze existuje program, ktery mel byt zavrzen jako nekorektni, protoze v nem nesedi typy, a pritom ho ten system nejak otypuje (tedy prohlasi za spravny). Naopak neuplnost znamena, ze bude existovat spravne otypovatelny program, ale typovy system ho nebude schopen otypovat na zaklade pravidel, ktere ma.

Jinak viz https://dl.acm.org/citation.cfm?id=2984004.

[BaldSlattery]

treba typove systemy Javy a stare Scaly jsou nekorektni

Pořád ještě jsme si neřekli, co by to ta korektnost (a (ne)dokazatelnost) u typového systému měla být, takže tvrdit, že nějaký typový systém je nekorektní, je předčasné.

Vzdyt to bylo receno v tom odkazu, co posilal OP. Ze typovy system neni korektni znamena, ze existuje program, ktery mel byt zavrzen jako nekorektni, protoze v nem nesedi typy, a pritom ho ten system nejak otypuje (tedy prohlasi za spravny). Naopak neuplnost znamena, ze bude existovat spravne otypovatelny program, ale typovy system ho nebude schopen otypovat na zaklade pravidel, ktere ma.

Jinak viz https://dl.acm.org/citation.cfm?id=2984004.

Předchozí výtka byla, co že to je typový systém. Navrhuji vzít Simple theory of types (aka typovaný λ počet).

[JS]

treba typove systemy Javy a stare Scaly jsou nekorektni

Pořád ještě jsme si neřekli, co by to ta korektnost (a (ne)dokazatelnost) u typového systému měla být, takže tvrdit, že nějaký typový systém je nekorektní, je předčasné.

Vzdyt to bylo receno v tom odkazu, co posilal OP. Ze typovy system neni korektni znamena, ze existuje program, ktery mel byt zavrzen jako nekorektni, protoze v nem nesedi typy, a pritom ho ten system nejak otypuje (tedy prohlasi za spravny). Naopak neuplnost znamena, ze bude existovat spravne otypovatelny program, ale typovy system ho nebude schopen otypovat na zaklade pravidel, ktere ma.

Jinak viz https://dl.acm.org/citation.cfm?id=2984004.

Předchozí výtka byla, co že to je typový systém. Navrhuji vzít Simple theory of types (aka typovaný λ počet).

A co s nim? Pokud vim, tak jednoduse typovany lambda kalkulus neumi rekurzi a pro nej tedy Godelova veta o neuplnosti neplati. A jako typovy system je to tudiz dost neprakticke.

[BaldSlattery]

treba typove systemy Javy a stare Scaly jsou nekorektni

Pořád ještě jsme si neřekli, co by to ta korektnost (a (ne)dokazatelnost) u typového systému měla být, takže tvrdit, že nějaký typový systém je nekorektní, je předčasné.

Vzdyt to bylo receno v tom odkazu, co posilal OP. Ze typovy system neni korektni znamena, ze existuje program, ktery mel byt zavrzen jako nekorektni, protoze v nem nesedi typy, a pritom ho ten system nejak otypuje (tedy prohlasi za spravny). Naopak neuplnost znamena, ze bude existovat spravne otypovatelny program, ale typovy system ho nebude schopen otypovat na zaklade pravidel, ktere ma.

Jinak viz https://dl.acm.org/citation.cfm?id=2984004.

Předchozí výtka byla, co že to je typový systém. Navrhuji vzít Simple theory of types (aka typovaný λ počet).

A co s nim? Pokud vim, tak jednoduse typovany lambda kalkulus neumi rekurzi a pro nej tedy Godelova veta o neuplnosti neplati. A jako typovy system je to tudiz dost neprakticke.

Umí rekurzi. Ostatně existují na něm založené, normálně používané jazyky. Už sem přestaňte (pl.) psát nesmysly.

[JS]

treba typove systemy Javy a stare Scaly jsou nekorektni

Pořád ještě jsme si neřekli, co by to ta korektnost (a (ne)dokazatelnost) u typového systému měla být, takže tvrdit, že nějaký typový systém je nekorektní, je předčasné.

Vzdyt to bylo receno v tom odkazu, co posilal OP. Ze typovy system neni korektni znamena, ze existuje program, ktery mel byt zavrzen jako nekorektni, protoze v nem nesedi typy, a pritom ho ten system nejak otypuje (tedy prohlasi za spravny). Naopak neuplnost znamena, ze bude existovat spravne otypovatelny program, ale typovy system ho nebude schopen otypovat na zaklade pravidel, ktere ma.

Jinak viz https://dl.acm.org/citation.cfm?id=2984004.

Předchozí výtka byla, co že to je typový systém. Navrhuji vzít Simple theory of types (aka typovaný λ počet).

A co s nim? Pokud vim, tak jednoduse typovany lambda kalkulus neumi rekurzi a pro nej tedy Godelova veta o neuplnosti neplati. A jako typovy system je to tudiz dost neprakticke.

Umí rekurzi. Ostatně existují na něm založené, normálně používané jazyky. Už sem přestaňte (pl.) psát nesmysly.

Nevim, co tim chces rict - ja jak to chapu tak ne, viz https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus. Nedaji se v nem otypovat funkce, ktere maji libovolne mnozstvi rekurzivnich volani (v zavislosti na termech). Pokud existuji na nem zalozene jazyky, pak nepotrebuji typovat funkce (treba jako C).