Gödel a staticky typované jazyky

[Mirek Prýmek]

V diskusi "Co si myslíte o OOP?" mě zaujalo tohle tvrzení:

Existujou validní programy, který statickej jazyk neuzná. Žádnej statickej typovej systém nebude nikdy dostatečně silnej na to, aby uznal všechny validní programy - viz Godelovy věty o nekompletnosti.

Narozdíl od neplodného hádání se o to, jestli je lepší statické nebo dynamické typování, prosvištět si Gödela mi přijde užitečný. Chtěl bych teda poprosit Blbce, jestli by mohl nějak (alespoň polo)formálně svoje tvrzení dokázat - tj. vzít Gödelovy výsledky a vyvodit z nich to, co tvrdí (čistě tady v tomhle tématu - tj. bez odkazů na autority).

Dík!

[Reklama]

[BaldSlattery]

V diskusi "Co si myslíte o OOP?" mě zaujalo tohle tvrzení:

Existujou validní programy, který statickej jazyk neuzná. Žádnej statickej typovej systém nebude nikdy dostatečně silnej na to, aby uznal všechny validní programy - viz Godelovy věty o nekompletnosti.

Narozdíl od neplodného hádání se o to, jestli je lepší statické nebo dynamické typování, prosvištět si Gödela mi přijde užitečný. Chtěl bych teda poprosit Blbce, jestli by mohl nějak (alespoň polo)formálně svoje tvrzení dokázat - tj. vzít Gödelovy výsledky a vyvodit z nich to, co tvrdí (čistě tady v tomhle tématu - tj. bez odkazů na autority).

Dík!

Blbec si popletl pojmy - úplnost teorie vs. úplnost formálně logického systému, pročež je ten canc blbost.

https://cs.wikipedia.org/wiki/%C3%9Apln%C3%A1_teorie

[Lojza]

nekdo ve vlaknu OOP odkazoval na


http://logan.tw/posts/2014/11/12/soundness-and-completeness-of-the-type-system/


jinak ja nemam sanci se k tomu vyjadrit (ostatne Godel se z toho posleze zblaznil) ale nerikaji ty Godelovy vety o neuplnosti v podstate jen to, ze pravdivost ? (uplnost ?) systemu zalozeneho na nejakych axiomech NELZE DOKAZAT, ale vubec nepopira (resp. nevyjadruje se) ze by takovy system nemohl existovat ? cili ze takovy system je mozne mit (jen tam bude ta nejistota ze to nelze dokazat ?)

[BaldSlattery]

nekdo ve vlaknu OOP odkazoval na


http://logan.tw/posts/2014/11/12/soundness-and-completeness-of-the-type-system/


jinak ja nemam sanci se k tomu vyjadrit (ostatne Godel se z toho posleze zblaznil) ale nerikaji ty Godelovy vety o neuplnosti v podstate jen to, ze pravdivost ? (uplnost ?) systemu zalozeneho na nejakych axiomech NELZE DOKAZAT, ale vubec nepopira (resp. nevyjadruje se) ze by takovy system nemohl existovat ? cili ze takovy system je mozne mit (jen tam bude ta nejistota ze to nelze dokazat ?)

V predikátové logice platí, že každou (bezespornou) neúplnou teorii lze rozšířit na úplnou. To dokázal kdysi v (matematickém) pravěku Lindenbaum a přišlo mu to tak triviální, že to nezveřejnil, to za něj udělal Tajtelbaum a lemma připsal původnímu autorovi. Gödelovy věty se týkají jen malinkaté podmnožiny teorií predikátové logiky.

[Fudge]

Ty voe, tady to je skoro jako číst Cimrmany...

[Reklama]

[Mirek Prýmek]

nerikaji ty Godelovy vety o neuplnosti v podstate jen to, ze pravdivost ? (uplnost ?) systemu zalozeneho na nejakych axiomech NELZE DOKAZAT, ale vubec nepopira (resp. nevyjadruje se) ze by takovy system nemohl existovat ? cili ze takovy system je mozne mit (jen tam bude ta nejistota ze to nelze dokazat ?)

Pokud si chceme fakt Goedelovy věty připomenout a popovídat si o tom, co z nich plyne pro programátorskou praxi, tak tomu nepomůžou takhle mlhavé vágní úvahy, spíš naopak.

Právě proto jsem tohle téma založil - nelíbí se mi zdejší nešvar, že se tady teorie zmiňuje jenom stylem mírnixtýrnix plácnutí nějakého "vznešeného" pojmu, aniž by se nějak doložilo, jestli je ten poznatek v daném kontextu vůbec relevantní (typický je "ale to nejde, protože halting problem", to tady na fóru zaznělo už x-krát, skoro vždycky nekorektně, protože se tím argumentovalo pro něco, co z poznatků o halting problem vůbec nevyplývá).

Takže pokud se někdo chce pokusit, bylo by asi dobrý začít tím, že Goedelovy věty mluví o dokazatelnosti v rámci nějakého logického systému, kde mám nějaké axiomy a nějaká odvozovací pravidla. Pokud to chci dát do souvislosti s typovým systémem programovacího jazyka, budu asi muset mezi těmahle dvěma světy najít nějakou korespondenci...

[Mirek Prýmek]

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.

[Mirek Prýmek]

V predikátové logice platí, že každou (bezespornou) neúplnou teorii lze rozšířit na úplnou. To dokázal kdysi v (matematickém) pravěku Lindenbaum a přišlo mu to tak triviální, že to nezveřejnil, to za něj udělal Tajtelbaum a lemma připsal původnímu autorovi. Gödelovy věty se týkají jen malinkaté podmnožiny teorií predikátové logiky.

Tohle je přesně to plácnutí do vody, které ničemu nepomůže - kdo ví, o co jde, ten to slyšet nepotřebuje, a kdo neví, tomu tohle nijak nepomůže.

Pokud chceš přispět k hezké diskusi, můžeš to trochu rozvést a zdůvodnit, proč je to relativní pro to, o čem se bavíme?

[BaldSlattery]

nerikaji ty Godelovy vety o neuplnosti v podstate jen to, ze pravdivost ? (uplnost ?) systemu zalozeneho na nejakych axiomech NELZE DOKAZAT, ale vubec nepopira (resp. nevyjadruje se) ze by takovy system nemohl existovat ? cili ze takovy system je mozne mit (jen tam bude ta nejistota ze to nelze dokazat ?)

Goedelovy věty mluví o dokazatelnosti v rámci nějakého logického systému, kde mám nějaké axiomy a nějaká odvozovací pravidla. Pokud to chci dát do souvislosti s typovým systémem programovacího jazyka, budu asi muset mezi těmahle dvěma světy najít nějakou korespondenci...

Jenže tam žádná přímá souvislost není, Gödel mluví o klasické logice a typové systémy jsou intuicionalistické (kterážto logika má blízko k logice modální). Navíc jak již zaznělo, Blbec si popletl dva odlišné koncepty úplnosti. Nehledě na to, že úplnost nějakého formálního systému není otázkou ano/ne, zvlášť u třířitních logik, jako je ta modální. Sorry, možná to byla upřímná snaha o rozjezd vysoce intelektuální diskuze, ale kromě tebe tady o tom nemáme ani šajnu, takže by to byla jen parodie.

[rkapl]

Jenže tam žádná přímá souvislost není, Gödel mluví o klasické logice a typové systémy jsou intuicionalistické.

Z lehkého Googlení to vypadá, že důkaz Godelových tvrzení nepotřebuje klasickou logiku, intuicionalistická by měla stačit. Ale jinak souhlasím s poznámkou o rozlišování úplnosti dokazovacího systému vs teorie. A taky o tom, že tato diskuze je asi nad naše možnosti, i když to tak ze začátku nevypadá.

A také je třeba se zamyslet jestli směr Curry-Howard -> Godel stačí. Co když existuje nějaký lepší typový systém? (i když si to nemyslím).

V obecnosti to beru tak, že se ptáme, zda existuje algoritmus, který ověří, zda daný program skončí (=validnost), pokud mu dáme nějaký "důkaz" (=otypování programu). Zdá se mi tedy jedno, jeslti budeme operovat na úrovni typového systému, nebo si někdo vybere nějaký logický dokazovací systém.

[BaldSlattery]

Jenže tam žádná přímá souvislost není, Gödel mluví o klasické logice a typové systémy jsou intuicionalistické.

Z lehkého Googlení to vypadá, že důkaz Godelových tvrzení nepotřebuje klasickou logiku, intuicionalistická by měla stačit.

Asi stačí i Heytingova aritmetika, ale já se s tím nikdy blíže nesetkal, takže se k tomu radši nebudu moc vyjadřovat.

[BaldSlattery]

Jenže tam žádná přímá souvislost není, Gödel mluví o klasické logice a typové systémy jsou intuicionalistické.

V obecnosti to beru tak, že se ptáme, zda existuje algoritmus, který ověří, zda daný program skončí (=validnost), pokud mu dáme nějaký "důkaz" (=otypování programu).

To samozřejmě existuje, některé jazyky to mají. Pochopitelně funkcionalní.

[rkapl]

Jenže tam žádná přímá souvislost není, Gödel mluví o klasické logice a typové systémy jsou intuicionalistické.

V obecnosti to beru tak, že se ptáme, zda existuje algoritmus, který ověří, zda daný program skončí (=validnost), pokud mu dáme nějaký "důkaz" (=otypování programu).

To samozřejmě existuje, některé jazyky to mají. Pochopitelně funkcionalní.

Ano, to si uvedomuji, je to vlastně předpoklad pro to C-H. 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. My se tu pak chceme 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.

A ano neřekl jsem, jak určit ty validní vstupy.

[Mirek Prýmek]

pro každý program, který pro všechny validní vstupy skončí

To je zajímavé zúžení. Nechceme od typového systému, aby uměl posoudit i programy, které se potenciálně můžou zacyklit?

[rkapl]

pro každý program, který pro všechny validní vstupy skončí

To je zajímavé zúžení. Nechceme od typového systému, aby uměl posoudit i programy, které se potenciálně můžou zacyklit?

Nemyslím, že je takové zůžení na škodu a je podle mě běžné. Všechny čistě funkcionální programy, které se zacyklí, jsou z black-box pohledu stejné. Prostě se zacyklili. A jak poznamenal "BaldSlattery", takové typové systémy jsou (Agda, Coq, typované lambda kalkuly -- kdyžtak mě opravte). V praxi potom můžeme převést další problémy s "validností" (např. program vyhodí vyjímku) na zacyklení.

Snažil jsem se definovat co vlastně je ten typový systém, abych jsme mohli přimo zvažovat logický důkaz "validnosti" jako otypování programu, bez nutnosti skákat přes Curry-Howard isomorfismus.