Fórum Root.cz
Hlavní témata => Vývoj => Téma založeno: Mirek Prýmek 06. 01. 2019, 00:32:01
-
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!
-
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
-
nekdo ve vlaknu OOP odkazoval na
http://logan.tw/posts/2014/11/12/soundness-and-completeness-of-the-type-system/ (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 ?)
-
nekdo ve vlaknu OOP odkazoval na
http://logan.tw/posts/2014/11/12/soundness-and-completeness-of-the-type-system/ (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.
-
Ty voe, tady to je skoro jako číst Cimrmany...
-
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...
-
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.
-
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?
-
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.
-
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.
-
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.
-
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í.
-
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.
-
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?
-
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.
-
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 :)
-
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.
-
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?
-
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.
-
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á.
-
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.
:)
-
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.
-
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.
-
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é.
-
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 (https://dl.acm.org/citation.cfm?id=2984004).
-
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 (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).
-
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 (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.
-
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 (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.
-
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 (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 (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).
-
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 (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 (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).
Má rekurzi takovou, která neomezuje silnou normalizovatelnost. Počet rekurzivních volání samozřejmě libovolný je, pokud stačí, že jich je konečně mnoho - což by mělo. Čili návrat k tématu - vezměme STλC jako typový systém.
-
treba typove systemy Javy a stare Scaly jsou nekorektni
tvrdit, že nějaký typový systém je nekorektní, je předčasné.
A kromě toho nemožné, typový systém může být zároveň korektní i nekorektní. Proto jsem navrhoval vzít STλC, to lidi poberou a jde na tom vše kolem typů krásně vysvětlit, včetně metalogických důkazů (ne)korektnosti/úplnosti. A jde v tom přímo programovat za účelem názornosti.
-
A kromě toho nemožné, typový systém může být zároveň korektní i nekorektní. Proto jsem navrhoval vzít STλC, to lidi poberou a jde na tom vše kolem typů krásně vysvětlit, včetně metalogických důkazů (ne)korektnosti/úplnosti. A jde v tom přímo programovat za účelem názornosti.
Každopádně Blbec se vypařil, takže nám svoje tvrzení nedoloží na ničem :)
-
treba typove systemy Javy a stare Scaly jsou nekorektni
tvrdit, že nějaký typový systém je nekorektní, je předčasné.
A kromě toho nemožné, typový systém může být zároveň korektní i nekorektní. Proto jsem navrhoval vzít STλC, to lidi poberou a jde na tom vše kolem typů krásně vysvětlit, včetně metalogických důkazů (ne)korektnosti/úplnosti. A jde v tom přímo programovat za účelem názornosti.
No, ukaz mi, jak v STλC otypujes treba faktorial.. Jaky priradis typ tomu rekurzivnimu volani? Ja STλC chapu tak, ze vzdy muzes otypovat jen funkce nad termy, jejichz typ uz nejak z predtim znas.
-
treba typove systemy Javy a stare Scaly jsou nekorektni
tvrdit, že nějaký typový systém je nekorektní, je předčasné.
A kromě toho nemožné, typový systém může být zároveň korektní i nekorektní. Proto jsem navrhoval vzít STλC, to lidi poberou a jde na tom vše kolem typů krásně vysvětlit, včetně metalogických důkazů (ne)korektnosti/úplnosti. A jde v tom přímo programovat za účelem názornosti.
No, ukaz mi, jak v STλC otypujes treba faktorial.. Jaky priradis typ tomu rekurzivnimu volani? Ja STλC chapu tak, ze vzdy muzes otypovat jen funkce nad termy, jejichz typ uz nejak z predtim znas.
Nějak se v tom motáš, zopakuj si pro začátek, co je λ kalkulus. Zrovna faktoriál bývá první funkcí ve výukových textech pro freshmeny. Normálně je typu ωω, to by asi člověk čekal. Dokud nebudeš chtít psát Ackermannovu funkci a podobně užitečné ptákoviny, STλC bohatě stačí.
-
treba typove systemy Javy a stare Scaly jsou nekorektni
tvrdit, že nějaký typový systém je nekorektní, je předčasné.
A kromě toho nemožné, typový systém může být zároveň korektní i nekorektní. Proto jsem navrhoval vzít STλC, to lidi poberou a jde na tom vše kolem typů krásně vysvětlit, včetně metalogických důkazů (ne)korektnosti/úplnosti. A jde v tom přímo programovat za účelem názornosti.
No, ukaz mi, jak v STλC otypujes treba faktorial.. Jaky priradis typ tomu rekurzivnimu volani? Ja STλC chapu tak, ze vzdy muzes otypovat jen funkce nad termy, jejichz typ uz nejak z predtim znas.
Nějak se v tom motáš, zopakuj si pro začátek, co je λ kalkulus. Zrovna faktoriál bývá první funkcí ve výukových textech pro freshmeny. Normálně je typu ωω, to by asi člověk čekal. Dokud nebudeš chtít psát Ackermannovu funkci a podobně užitečné ptákoviny, STλC bohatě stačí.
Nevim, co tim chces rict, ze ma neco "typ ωω". Primo na Wikipedii se pise:
"This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term Ω = ( λ x . x x ) ( λ x . x x ) {\displaystyle \Omega =(\lambda x.~x~x)(\lambda x.~x~x)} \Omega =(\lambda x.~x~x)(\lambda x.~x~x). Recursion can be added to the language by either having a special operator f i x α {\displaystyle {\mathtt {fix}}_{\alpha }} {\mathtt {fix}}_{\alpha }of type ( α → α ) → α {\displaystyle (\alpha \to \alpha )\to \alpha } (\alpha \to \alpha )\to \alpha or adding general recursive types, though both eliminate strong normalization."
-
treba typove systemy Javy a stare Scaly jsou nekorektni
tvrdit, že nějaký typový systém je nekorektní, je předčasné.
A kromě toho nemožné, typový systém může být zároveň korektní i nekorektní. Proto jsem navrhoval vzít STλC, to lidi poberou a jde na tom vše kolem typů krásně vysvětlit, včetně metalogických důkazů (ne)korektnosti/úplnosti. A jde v tom přímo programovat za účelem názornosti.
No, ukaz mi, jak v STλC otypujes treba faktorial.. Jaky priradis typ tomu rekurzivnimu volani? Ja STλC chapu tak, ze vzdy muzes otypovat jen funkce nad termy, jejichz typ uz nejak z predtim znas.
Nějak se v tom motáš, zopakuj si pro začátek, co je λ kalkulus. Zrovna faktoriál bývá první funkcí ve výukových textech pro freshmeny. Normálně je typu ωω, to by asi člověk čekal. Dokud nebudeš chtít psát Ackermannovu funkci a podobně užitečné ptákoviny, STλC bohatě stačí.
Nevim, co tim chces rict, ze ma neco "typ ωω". Primo na Wikipedii se pise:
"This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term Ω = ( λ x . x x ) ( λ x . x x ) {\displaystyle \Omega =(\lambda x.~x~x)(\lambda x.~x~x)} \Omega =(\lambda x.~x~x)(\lambda x.~x~x). Recursion can be added to the language by either having a special operator f i x α {\displaystyle {\mathtt {fix}}_{\alpha }} {\mathtt {fix}}_{\alpha }of type ( α → α ) → α {\displaystyle (\alpha \to \alpha )\to \alpha } (\alpha \to \alpha )\to \alpha or adding general recursive types, though both eliminate strong normalization."
Jenže tady se celou dobu bavíme o primitivní rekurzi, ne o samodružných bodech ;) Pustý teoretik se může vrtat v Ackermannovi, ale ve vlákně snad jde o *praktické* použití typů ::) Takže rewind (opět) - stačí-li nám faktoriál (a ostatní primitivně rekurzivní funkce, jiné se v praxi stejně nepoužívají), je STλC ideální kandidát na typový systém.
-
treba typove systemy Javy a stare Scaly jsou nekorektni
tvrdit, že nějaký typový systém je nekorektní, je předčasné.
A kromě toho nemožné, typový systém může být zároveň korektní i nekorektní. Proto jsem navrhoval vzít STλC, to lidi poberou a jde na tom vše kolem typů krásně vysvětlit, včetně metalogických důkazů (ne)korektnosti/úplnosti. A jde v tom přímo programovat za účelem názornosti.
No, ukaz mi, jak v STλC otypujes treba faktorial.. Jaky priradis typ tomu rekurzivnimu volani? Ja STλC chapu tak, ze vzdy muzes otypovat jen funkce nad termy, jejichz typ uz nejak z predtim znas.
Nějak se v tom motáš, zopakuj si pro začátek, co je λ kalkulus. Zrovna faktoriál bývá první funkcí ve výukových textech pro freshmeny. Normálně je typu ωω, to by asi člověk čekal. Dokud nebudeš chtít psát Ackermannovu funkci a podobně užitečné ptákoviny, STλC bohatě stačí.
Nevim, co tim chces rict, ze ma neco "typ ωω".
K tomu se na škole ještě dostanete. Nebo se můžeš předběžně dovzdělat a přečíst si něco o STλC, ideálně původní Churchův článek.
-
treba typove systemy Javy a stare Scaly jsou nekorektni
tvrdit, že nějaký typový systém je nekorektní, je předčasné.
A kromě toho nemožné, typový systém může být zároveň korektní i nekorektní. Proto jsem navrhoval vzít STλC, to lidi poberou a jde na tom vše kolem typů krásně vysvětlit, včetně metalogických důkazů (ne)korektnosti/úplnosti. A jde v tom přímo programovat za účelem názornosti.
No, ukaz mi, jak v STλC otypujes treba faktorial.. Jaky priradis typ tomu rekurzivnimu volani? Ja STλC chapu tak, ze vzdy muzes otypovat jen funkce nad termy, jejichz typ uz nejak z predtim znas.
Nějak se v tom motáš, zopakuj si pro začátek, co je λ kalkulus. Zrovna faktoriál bývá první funkcí ve výukových textech pro freshmeny. Normálně je typu ωω, to by asi člověk čekal. Dokud nebudeš chtít psát Ackermannovu funkci a podobně užitečné ptákoviny, STλC bohatě stačí.
Nevim, co tim chces rict, ze ma neco "typ ωω". Primo na Wikipedii se pise:
"This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term Ω = ( λ x . x x ) ( λ x . x x ) {\displaystyle \Omega =(\lambda x.~x~x)(\lambda x.~x~x)} \Omega =(\lambda x.~x~x)(\lambda x.~x~x). Recursion can be added to the language by either having a special operator f i x α {\displaystyle {\mathtt {fix}}_{\alpha }} {\mathtt {fix}}_{\alpha }of type ( α → α ) → α {\displaystyle (\alpha \to \alpha )\to \alpha } (\alpha \to \alpha )\to \alpha or adding general recursive types, though both eliminate strong normalization."
jestli to dobře chápu tak STT rekurzi (let,Y nebo tak) nemá, ale dá se v ní implementovat primitive recursive function: https://stackoverflow.com/questions/46820404/non-recursive-lambda-calculus-factorial-function
-
treba typove systemy Javy a stare Scaly jsou nekorektni
tvrdit, že nějaký typový systém je nekorektní, je předčasné.
A kromě toho nemožné, typový systém může být zároveň korektní i nekorektní. Proto jsem navrhoval vzít STλC, to lidi poberou a jde na tom vše kolem typů krásně vysvětlit, včetně metalogických důkazů (ne)korektnosti/úplnosti. A jde v tom přímo programovat za účelem názornosti.
No, ukaz mi, jak v STλC otypujes treba faktorial.. Jaky priradis typ tomu rekurzivnimu volani? Ja STλC chapu tak, ze vzdy muzes otypovat jen funkce nad termy, jejichz typ uz nejak z predtim znas.
Nějak se v tom motáš, zopakuj si pro začátek, co je λ kalkulus. Zrovna faktoriál bývá první funkcí ve výukových textech pro freshmeny. Normálně je typu ωω, to by asi člověk čekal. Dokud nebudeš chtít psát Ackermannovu funkci a podobně užitečné ptákoviny, STλC bohatě stačí.
Nevim, co tim chces rict, ze ma neco "typ ωω". Primo na Wikipedii se pise:
"This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term Ω = ( λ x . x x ) ( λ x . x x ) {\displaystyle \Omega =(\lambda x.~x~x)(\lambda x.~x~x)} \Omega =(\lambda x.~x~x)(\lambda x.~x~x). Recursion can be added to the language by either having a special operator f i x α {\displaystyle {\mathtt {fix}}_{\alpha }} {\mathtt {fix}}_{\alpha }of type ( α → α ) → α {\displaystyle (\alpha \to \alpha )\to \alpha } (\alpha \to \alpha )\to \alpha or adding general recursive types, though both eliminate strong normalization."
jestli to dobře chápu tak STT rekurzi (let,Y nebo tak) nemá, ale dá se v ní implementovat primitive recursive function: https://stackoverflow.com/questions/46820404/non-recursive-lambda-calculus-factorial-function
Ano, o tom se tu celou dobu bavíme.
-
No, ukaz mi, jak v STλC otypujes treba faktorial.. Jaky priradis typ tomu rekurzivnimu volani? Ja STλC chapu tak, ze vzdy muzes otypovat jen funkce nad termy, jejichz typ uz nejak z predtim znas.
Nějak se v tom motáš, zopakuj si pro začátek, co je λ kalkulus. Zrovna faktoriál bývá první funkcí ve výukových textech pro freshmeny. Normálně je typu ωω, to by asi člověk čekal. Dokud nebudeš chtít psát Ackermannovu funkci a podobně užitečné ptákoviny, STλC bohatě stačí.
Nevim, co tim chces rict, ze ma neco "typ ωω". Primo na Wikipedii se pise:
"This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term Ω = ( λ x . x x ) ( λ x . x x ) {\displaystyle \Omega =(\lambda x.~x~x)(\lambda x.~x~x)} \Omega =(\lambda x.~x~x)(\lambda x.~x~x). Recursion can be added to the language by either having a special operator f i x α {\displaystyle {\mathtt {fix}}_{\alpha }} {\mathtt {fix}}_{\alpha }of type ( α → α ) → α {\displaystyle (\alpha \to \alpha )\to \alpha } (\alpha \to \alpha )\to \alpha or adding general recursive types, though both eliminate strong normalization."
jestli to dobře chápu tak STT rekurzi (let,Y nebo tak) nemá, ale dá se v ní implementovat primitive recursive function: https://stackoverflow.com/questions/46820404/non-recursive-lambda-calculus-factorial-function
Asi to tak muzes udelat, ale pak mi prijde, ze budes mit ruzna prirozena cisla jako ruzne typy. Coz asi v praxi nechces. To co bychom asi chteli je, aby vsechny termy odpovidajici volani faktorialu s nejakou hodnotou mely stejny typ. A to prave v STT nejde (aniz by se pridal dodatecny axiom, treba ten o otypovani kombinatoru pevneho bodu), protoze tam lze z typovych pravidel odvodit typ aplikace jednoho termu na druhy (tj. volani funkce s nejakym parametrem) jen pokud uz zname jejich typy.
Ale mozna opravdu neco chapu spatne. BaldSlattery sice napsal, ze je snadne to vysvetlit, ale nevysvetlil to.
-
Pustý teoretik se může vrtat v Ackermannovi, ale ve vlákně snad jde o *praktické* použití typů ::) Takže rewind (opět) - stačí-li nám faktoriál (a ostatní primitivně rekurzivní funkce, jiné se v praxi stejně nepoužívají), je STλC ideální kandidát na typový systém.
Jinak tady v podstate rikas to same co ja na zacatku - pokud se spokojis s par dodatecnymi axiomy (treba prave moznosti otypovat primitivni rekurzi), tak te Godelovy vety nemusi trapit. V praxi si vyberes neuplnost (existenci termu, ktere nelze otypovat z typovych pravidel) a nikoli nekorektnost.
-
No, ukaz mi, jak v STλC otypujes treba faktorial.. Jaky priradis typ tomu rekurzivnimu volani? Ja STλC chapu tak, ze vzdy muzes otypovat jen funkce nad termy, jejichz typ uz nejak z predtim znas.
Nějak se v tom motáš, zopakuj si pro začátek, co je λ kalkulus. Zrovna faktoriál bývá první funkcí ve výukových textech pro freshmeny. Normálně je typu ωω, to by asi člověk čekal. Dokud nebudeš chtít psát Ackermannovu funkci a podobně užitečné ptákoviny, STλC bohatě stačí.
Nevim, co tim chces rict, ze ma neco "typ ωω". Primo na Wikipedii se pise:
"This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term Ω = ( λ x . x x ) ( λ x . x x ) {\displaystyle \Omega =(\lambda x.~x~x)(\lambda x.~x~x)} \Omega =(\lambda x.~x~x)(\lambda x.~x~x). Recursion can be added to the language by either having a special operator f i x α {\displaystyle {\mathtt {fix}}_{\alpha }} {\mathtt {fix}}_{\alpha }of type ( α → α ) → α {\displaystyle (\alpha \to \alpha )\to \alpha } (\alpha \to \alpha )\to \alpha or adding general recursive types, though both eliminate strong normalization."
jestli to dobře chápu tak STT rekurzi (let,Y nebo tak) nemá, ale dá se v ní implementovat primitive recursive function: https://stackoverflow.com/questions/46820404/non-recursive-lambda-calculus-factorial-function
Asi to tak muzes udelat, ale pak mi prijde, ze budes mit ruzna prirozena cisla jako ruzne typy. Coz asi v praxi nechces. To co bychom asi chteli je, aby vsechny termy odpovidajici volani faktorialu s nejakou hodnotou mely stejny typ. A to prave v STT nejde (aniz by se pridal dodatecny axiom, treba ten o otypovani kombinatoru pevneho bodu), protoze tam lze z typovych pravidel odvodit typ aplikace jednoho termu na druhy (tj. volani funkce s nejakym parametrem) jen pokud uz zname jejich typy.
Ale mozna opravdu neco chapu spatne. BaldSlattery sice napsal, ze je snadne to vysvetlit, ale nevysvetlil to.
pochopil jsem to tak, že to využívá Church numbers, to by měl být jeden typ pro všechna čísla viz https://en.wikipedia.org/wiki/Church_encoding
-
Pustý teoretik se může vrtat v Ackermannovi, ale ve vlákně snad jde o *praktické* použití typů ::) Takže rewind (opět) - stačí-li nám faktoriál (a ostatní primitivně rekurzivní funkce, jiné se v praxi stejně nepoužívají), je STλC ideální kandidát na typový systém.
Jinak tady v podstate rikas to same co ja na zacatku - pokud se spokojis s par dodatecnymi axiomy (treba prave moznosti otypovat primitivni rekurzi), tak te Godelovy vety nemusi trapit. V praxi si vyberes neuplnost (existenci termu, ktere nelze otypovat z typovych pravidel) a nikoli nekorektnost.
STλC s primitivní rekurzí je úplný. Problémem je jen ten Y kombinátor nebo něco stejně mocného.
-
Pustý teoretik se může vrtat v Ackermannovi, ale ve vlákně snad jde o *praktické* použití typů ::) Takže rewind (opět) - stačí-li nám faktoriál (a ostatní primitivně rekurzivní funkce, jiné se v praxi stejně nepoužívají), je STλC ideální kandidát na typový systém.
Jinak tady v podstate rikas to same co ja na zacatku - pokud se spokojis s par dodatecnymi axiomy (treba prave moznosti otypovat primitivni rekurzi), tak te Godelovy vety nemusi trapit. V praxi si vyberes neuplnost (existenci termu, ktere nelze otypovat z typovych pravidel) a nikoli nekorektnost.
STλC s primitivní rekurzí je úplný. Problémem je jen ten Y kombinátor nebo něco stejně mocného.
P.S. Funkce pro rekurzi potřebná například pro ten faktoriál nad ω je typu α(ααω)αω (klasika). Je to standardní a tedy úplný STλC. Víc k tomu už asi dodat nejde.
-
Pustý teoretik se může vrtat v Ackermannovi, ale ve vlákně snad jde o *praktické* použití typů ::) Takže rewind (opět) - stačí-li nám faktoriál (a ostatní primitivně rekurzivní funkce, jiné se v praxi stejně nepoužívají), je STλC ideální kandidát na typový systém.
Jinak tady v podstate rikas to same co ja na zacatku - pokud se spokojis s par dodatecnymi axiomy (treba prave moznosti otypovat primitivni rekurzi), tak te Godelovy vety nemusi trapit. V praxi si vyberes neuplnost (existenci termu, ktere nelze otypovat z typovych pravidel) a nikoli nekorektnost.
STλC s primitivní rekurzí je úplný. Problémem je jen ten Y kombinátor nebo něco stejně mocného.
P.S. Funkce pro rekurzi potřebná například pro ten faktoriál nad ω je typu α(ααω)αω (klasika). Je to standardní a tedy úplný STλC. Víc k tomu už asi dodat nejde.
P.P.S. Kdyby to ještě pořád někdo neviděl, tak prim. rekurze nad ω je (v pseudozápisu) ρ->λn.λb.λs.n=0?b:s(n,ρ(n-1,b,s)), čili zřejmě výraz se (silně) normalizující.
-
P.S. Funkce pro rekurzi potřebná například pro ten faktoriál nad ω je typu α(ααω)αω (klasika). Je to standardní a tedy úplný STλC. Víc k tomu už asi dodat nejde.
P.P.S. Kdyby to ještě pořád někdo neviděl, tak prim. rekurze nad ω je (v pseudozápisu) ρ->λn.λb.λs.n=0?b:s(n,ρ(n-1,b,s)), čili zřejmě výraz se (silně) normalizující.
Hm, premyslel jsem nad tim a nejak se mi to nezda. Uznavam, ze muzes pro kazde zvolene n (v tom Churchove kodovani) otypovat to ρ(n); ale jak pak z toho vyplyva (pres typova pravidla), ze ρ ma typ ω->ω, to mi tedy jasne neni.
-
P.S. Funkce pro rekurzi potřebná například pro ten faktoriál nad ω je typu α(ααω)αω (klasika). Je to standardní a tedy úplný STλC. Víc k tomu už asi dodat nejde.
P.P.S. Kdyby to ještě pořád někdo neviděl, tak prim. rekurze nad ω je (v pseudozápisu) ρ->λn.λb.λs.n=0?b:s(n,ρ(n-1,b,s)), čili zřejmě výraz se (silně) normalizující.
Hm, premyslel jsem nad tim a nejak se mi to nezda. Uznavam, ze muzes pro kazde zvolene n (v tom Churchove kodovani) otypovat to ρ(n); ale jak pak z toho vyplyva (pres typova pravidla), ze ρ ma typ ω->ω, to mi tedy jasne neni.
Ale to ρ má pochopitelně jen jeden typ, je to operátor. V STT je ostatně operátorů (zavedených Churchem) hodně, ale logických (nad τ, tj. de facto boolean). Podle mě v tom hledáš přílišnou složitost. Typ toho ρ je prostě α(ααω)αω (tyto výrazy jsou asociativní doleva) a pro faktoriál (kde α je ω) akorát dodám druhý a třetí argument (báze a krok). Fakt to je jednodušší, než to vypadá.
-
Hm, premyslel jsem nad tim a nejak se mi to nezda. Uznavam, ze muzes pro kazde zvolene n (v tom Churchove kodovani) otypovat to ρ(n); ale jak pak z toho vyplyva (pres typova pravidla), ze ρ ma typ ω->ω, to mi tedy jasne neni.
Ale to ρ má pochopitelně jen jeden typ, je to operátor. V STT je ostatně operátorů (zavedených Churchem) hodně, ale logických (nad τ, tj. de facto boolean). Podle mě v tom hledáš přílišnou složitost. Typ toho ρ je prostě α(ααω)αω (tyto výrazy jsou asociativní doleva) a pro faktoriál (kde α je ω) akorát dodám druhý a třetí argument (báze a krok). Fakt to je jednodušší, než to vypadá.
Asi jsem spatne pochopil, co myslis tim ρ. Pouzivas notaci, ktera mi neni znama. Muzes to napsat v notaci ktera odpovida te, co se pouziva na Wikipedii?
To s tim mavanim rukou kolem operatoru mi prijde trochu divne. Pokud ma byt ten typovy system skutecne uplny, musi byt prece typy vsech termu odvoditelne na zaklade typovych pravidel.
-
Hm, premyslel jsem nad tim a nejak se mi to nezda. Uznavam, ze muzes pro kazde zvolene n (v tom Churchove kodovani) otypovat to ρ(n); ale jak pak z toho vyplyva (pres typova pravidla), ze ρ ma typ ω->ω, to mi tedy jasne neni.
Ale to ρ má pochopitelně jen jeden typ, je to operátor. V STT je ostatně operátorů (zavedených Churchem) hodně, ale logických (nad τ, tj. de facto boolean). Podle mě v tom hledáš přílišnou složitost. Typ toho ρ je prostě α(ααω)αω (tyto výrazy jsou asociativní doleva) a pro faktoriál (kde α je ω) akorát dodám druhý a třetí argument (báze a krok). Fakt to je jednodušší, než to vypadá.
Asi jsem spatne pochopil, co myslis tim ρ. Pouzivas notaci, ktera mi neni znama. Muzes to napsat v notaci ktera odpovida te, co se pouziva na Wikipedii?
Jaký wiki článek? Ten k STT toho moc nemá. Používám notaci z https://plato.stanford.edu/entries/type-theory-church/
-
Hm, premyslel jsem nad tim a nejak se mi to nezda. Uznavam, ze muzes pro kazde zvolene n (v tom Churchove kodovani) otypovat to ρ(n); ale jak pak z toho vyplyva (pres typova pravidla), ze ρ ma typ ω->ω, to mi tedy jasne neni.
Ale to ρ má pochopitelně jen jeden typ, je to operátor. V STT je ostatně operátorů (zavedených Churchem) hodně, ale logických (nad τ, tj. de facto boolean). Podle mě v tom hledáš přílišnou složitost. Typ toho ρ je prostě α(ααω)αω (tyto výrazy jsou asociativní doleva) a pro faktoriál (kde α je ω) akorát dodám druhý a třetí argument (báze a krok). Fakt to je jednodušší, než to vypadá.
To s tim mavanim rukou kolem operatoru mi prijde trochu divne. Pokud ma byt ten typovy system skutecne uplny, musi byt prece typy vsech termu odvoditelne na zaklade typovych pravidel.
To nechápu. STT má jeden typový operátor, konkatenaci, ty jiné operátory jsou na hodnotách. Úplnost znamená, že každá bezesporná teorie má model, což pro STT platí. Jinak typy všech výrazů samozřejmě odvoditelné jsou, ale to ještě neimplikuje úplnost.
K tomu ρ ještě, to je jen funkce, v STT něco jako “makro” (jako ty Churchovy operátory pro predikátovou logiku), lepší je si to představit jako přepisovací pravidlo (=redukce výrazů).
-
Hm, premyslel jsem nad tim a nejak se mi to nezda. Uznavam, ze muzes pro kazde zvolene n (v tom Churchove kodovani) otypovat to ρ(n); ale jak pak z toho vyplyva (pres typova pravidla), ze ρ ma typ ω->ω, to mi tedy jasne neni.
Ale to ρ má pochopitelně jen jeden typ, je to operátor. V STT je ostatně operátorů (zavedených Churchem) hodně, ale logických (nad τ, tj. de facto boolean). Podle mě v tom hledáš přílišnou složitost. Typ toho ρ je prostě α(ααω)αω (tyto výrazy jsou asociativní doleva) a pro faktoriál (kde α je ω) akorát dodám druhý a třetí argument (báze a krok). Fakt to je jednodušší, než to vypadá.
Asi jsem spatne pochopil, co myslis tim ρ. Pouzivas notaci, ktera mi neni znama. Muzes to napsat v notaci ktera odpovida te, co se pouziva na Wikipedii?
To s tim mavanim rukou kolem operatoru mi prijde trochu divne. Pokud ma byt ten typovy system skutecne uplny, musi byt prece typy vsech termu odvoditelne na zaklade typovych pravidel.
Jinak jen dodatečné doplnění, vycházím přímo z https://www.jstor.org/stable/2266170
-
Asi jsem spatne pochopil, co myslis tim ρ. Pouzivas notaci, ktera mi neni znama. Muzes to napsat v notaci ktera odpovida te, co se pouziva na Wikipedii?
Ja jsem taky zvykly spis na pouzivani vyrazu typu "primitivni typy" a explicitni ->. A sam jsem si take intuitivni myslel, ze ten church v ST LC otypovat nepujde. Dole jsem skusil priklad v Haskellu, ktery IMHO je omezeny na ST LC (zadna typova rekurze, pouze typove ->). Nejsem si jisty, co ovsem lze s takto definovanymi typy vs ST LC delat.
type Base = Bool
type Church = (Base -> Base) -> Base -> Base
churchZero:: Church
churchZero _ b = b
churchSucc:: Church -> Church
churchSucc x = \f b -> f (x f b)
isOdd:: Church -> Bool
isOdd x = x not False
main = do
print (isOdd (churchZero))
print (isOdd (churchSucc churchZero))
print (isOdd (churchSucc (churchSucc churchZero)))
Normalne by v Haskellu bylo type Church = (a -> a) -> a -> a, ale to my nemuzeme, musime si tedy ten zakladni typ urcit dopredu.
-
Normalne by v Haskellu bylo type Church = (a -> a) -> a -> a, ale to my nemuzeme, musime si tedy ten zakladni typ urcit dopredu.
já myslím, že se to může
-
Normalne by v Haskellu bylo type Church = (a -> a) -> a -> a, ale to my nemuzeme, musime si tedy ten zakladni typ urcit dopredu.
já myslím, že se to může
Oprava type Church a = (a -> a) -> a -> a (polymorfni typ).
-
Hm, premyslel jsem nad tim a nejak se mi to nezda. Uznavam, ze muzes pro kazde zvolene n (v tom Churchove kodovani) otypovat to ρ(n); ale jak pak z toho vyplyva (pres typova pravidla), ze ρ ma typ ω->ω, to mi tedy jasne neni.
Ale to ρ má pochopitelně jen jeden typ, je to operátor. V STT je ostatně operátorů (zavedených Churchem) hodně, ale logických (nad τ, tj. de facto boolean). Podle mě v tom hledáš přílišnou složitost. Typ toho ρ je prostě α(ααω)αω (tyto výrazy jsou asociativní doleva) a pro faktoriál (kde α je ω) akorát dodám druhý a třetí argument (báze a krok). Fakt to je jednodušší, než to vypadá.
Asi jsem spatne pochopil, co myslis tim ρ. Pouzivas notaci, ktera mi neni znama. Muzes to napsat v notaci ktera odpovida te, co se pouziva na Wikipedii?
Jaký wiki článek? Ten k STT toho moc nemá. Používám notaci z https://plato.stanford.edu/entries/type-theory-church/
All entities have types, and if α and β are types, the type of functions from elements of type β to elements of type α is written as (αβ). (This notation was introduced by Church, but some authors write (β → α) instead of (αβ).
si troufám tvrdit, že dneska je častější notace some authors (určitě se s ní setkávám častěji)
-
Hm, premyslel jsem nad tim a nejak se mi to nezda. Uznavam, ze muzes pro kazde zvolene n (v tom Churchove kodovani) otypovat to ρ(n); ale jak pak z toho vyplyva (pres typova pravidla), ze ρ ma typ ω->ω, to mi tedy jasne neni.
Ale to ρ má pochopitelně jen jeden typ, je to operátor. V STT je ostatně operátorů (zavedených Churchem) hodně, ale logických (nad τ, tj. de facto boolean). Podle mě v tom hledáš přílišnou složitost. Typ toho ρ je prostě α(ααω)αω (tyto výrazy jsou asociativní doleva) a pro faktoriál (kde α je ω) akorát dodám druhý a třetí argument (báze a krok). Fakt to je jednodušší, než to vypadá.
Asi jsem spatne pochopil, co myslis tim ρ. Pouzivas notaci, ktera mi neni znama. Muzes to napsat v notaci ktera odpovida te, co se pouziva na Wikipedii?
Jaký wiki článek? Ten k STT toho moc nemá. Používám notaci z https://plato.stanford.edu/entries/type-theory-church/
All entities have types, and if α and β are types, the type of functions from elements of type β to elements of type α is written as (αβ). (This notation was introduced by Church, but some authors write (β → α) instead of (αβ).
si troufám tvrdit, že dneska je častější notace some authors (určitě se s ní setkávám častěji)
Nebo αβ
-
To s tim mavanim rukou kolem operatoru mi prijde trochu divne. Pokud ma byt ten typovy system skutecne uplny, musi byt prece typy vsech termu odvoditelne na zaklade typovych pravidel.
Jinak jen dodatečné doplnění, vycházím přímo z https://www.jstor.org/stable/2266170
Toho jsem se trochu bal.. Coz o to, nekdy v budoucnu si to chci precist, ale ta budoucnost jeste nenastala, ted me spis zajimaji jine veci. (A obecne mam radsi moderni syntezy nez klasiky, ono oboji ma svoje, ale v tomto pripade se mi moc nechce ucit nejaka obskurni notace a navic nejsem prilis silny v logice.)
si troufám tvrdit, že dneska je častější notace some authors (určitě se s ní setkávám častěji)
Taky si to myslim (asi to budou najednou vsichni ti Haskellisti, co zacali houfem studovat lambda kalkul), ale v zasade OK, nejak jsem tomu porozumel. To Churchovo spis pripomina zapis kombinatoricke logiky, takze proto se od toho mozna ustoupilo, je to trochu zavadejici - neni jasne, zda se bavime o termech nebo typech.
A sam jsem si take intuitivni myslel, ze ten church v ST LC otypovat nepujde. Dole jsem skusil priklad v Haskellu, ktery IMHO je omezeny na ST LC (zadna typova rekurze, pouze typove ->). Nejsem si jisty, co ovsem lze s takto definovanymi typy vs ST LC delat.
Takhle, ja jsem byl puvodne skepticky k tem Churchovym literalum, ale nakonec (nez jsem psal svuj posledni prispevek vcera) jsem si to take rozmyslel (na zaklade definice na Wikipedii, ktera je beztypova) a vyslo mi to.
Takze to, s cim ted mam problem je, jak se v ST LC otypuje ten samotny faktorial (nebo jina rekurzivni funkce na cislech). Aplikace toho faktorialu na konkretni prirozene cislo (jako Churchuv literal) otypovat jde, to mi je jasne, a vyjde prirozene cislo. Ale cely faktorial jako funkce? Podle me ST LC tohle prave neumoznuje (z typovych pravidel), a tudiz musime doplnit nejake dalsi odvozovaci pravidlo, napriklad operator pevneho bodu, nebo nejaky jeho (klidne i omezenejsi) analog.
To nechápu. STT má jeden typový operátor, konkatenaci, ty jiné operátory jsou na hodnotách.
No ale nepotrebujes ke kazdemu operatoru na hodnotach, ktery pridavas v podstate jako axiom, i odpovidajici pravidlo pro otypovani? Pokud to muzes otypovat bez nej, pak ten operator nepotrebujes.. Ale mozna ti jen nerozumim, co myslis tim operatorem.
Hezky je to videt na te Wikipedii, tam je ST LC zaveden pomoci ctyr pravidel, a kazde z nich soucasne odvozuje hodnotu i typ.
Úplnost znamená, že každá bezesporná teorie má model, což pro STT platí. Jinak typy všech výrazů samozřejmě odvoditelné jsou, ale to ještě neimplikuje úplnost.
A mam pocit, ze pridanim toho operatoru ten ST LC zneuplnime - coz chapu tak, ze budou existovat vyrazy, ke kterym muzeme najit "spravne" otypovani, ale nepujdou zkonstruovat na zaklade typovych pravidel (mluvim o uplnosti typoveho systemu). Myslim si to proto, ze (spravne otypovane) rekurzivni funkce se nedaji podle me v tom ST LC ani zkonstruovat. Pokud nejak dovolime jejich konstrukci, otevirame tim dvere i jejich pouziti v parametrech, a tim se bohuzel (IMHO) dostavame mimo primitivni rekurzi.
Jinak je to zajimava diskuse - podle me je dobre si to ujasnit.
Nebo αβ
To je zverstvo - na to aby si clovek koupil diagonalni papir.
-
To s tim mavanim rukou kolem operatoru mi prijde trochu divne. Pokud ma byt ten typovy system skutecne uplny, musi byt prece typy vsech termu odvoditelne na zaklade typovych pravidel.
Jinak jen dodatečné doplnění, vycházím přímo z https://www.jstor.org/stable/2266170
Toho jsem se trochu bal.. Coz o to, nekdy v budoucnu si to chci precist, ale ta budoucnost jeste nenastala, ted me spis zajimaji jine veci. (A obecne mam radsi moderni syntezy nez klasiky, ono oboji ma svoje, ale v tomto pripade se mi moc nechce ucit nejaka obskurni notace a navic nejsem prilis silny v logice.)
si troufám tvrdit, že dneska je častější notace some authors (určitě se s ní setkávám častěji)
Taky si to myslim (asi to budou najednou vsichni ti Haskellisti, co zacali houfem studovat lambda kalkul), ale v zasade OK, nejak jsem tomu porozumel. To Churchovo spis pripomina zapis kombinatoricke logiky, takze proto se od toho mozna ustoupilo, je to trochu zavadejici - neni jasne, zda se bavime o termech nebo typech.
A sam jsem si take intuitivni myslel, ze ten church v ST LC otypovat nepujde. Dole jsem skusil priklad v Haskellu, ktery IMHO je omezeny na ST LC (zadna typova rekurze, pouze typove ->). Nejsem si jisty, co ovsem lze s takto definovanymi typy vs ST LC delat.
Takhle, ja jsem byl puvodne skepticky k tem Churchovym literalum, ale nakonec (nez jsem psal svuj posledni prispevek vcera) jsem si to take rozmyslel (na zaklade definice na Wikipedii, ktera je beztypova) a vyslo mi to.
Takze to, s cim ted mam problem je, jak se v ST LC otypuje ten samotny faktorial (nebo jina rekurzivni funkce na cislech). Aplikace toho faktorialu na konkretni prirozene cislo (jako Churchuv literal) otypovat jde, to mi je jasne, a vyjde prirozene cislo. Ale cely faktorial jako funkce? Podle me ST LC tohle prave neumoznuje (z typovych pravidel), a tudiz musime doplnit nejake dalsi odvozovaci pravidlo, napriklad operator pevneho bodu, nebo nejaky jeho (klidne i omezenejsi) analog.
To nechápu. STT má jeden typový operátor, konkatenaci, ty jiné operátory jsou na hodnotách.
No ale nepotrebujes ke kazdemu operatoru na hodnotach, ktery pridavas v podstate jako axiom, i odpovidajici pravidlo pro otypovani? Pokud to muzes otypovat bez nej, pak ten operator nepotrebujes.. Ale mozna ti jen nerozumim, co myslis tim operatorem.
Hezky je to videt na te Wikipedii, tam je ST LC zaveden pomoci ctyr pravidel, a kazde z nich soucasne odvozuje hodnotu i typ.
Úplnost znamená, že každá bezesporná teorie má model, což pro STT platí. Jinak typy všech výrazů samozřejmě odvoditelné jsou, ale to ještě neimplikuje úplnost.
A mam pocit, ze pridanim toho operatoru ten ST LC zneuplnime - coz chapu tak, ze budou existovat vyrazy, ke kterym muzeme najit "spravne" otypovani, ale nepujdou zkonstruovat na zaklade typovych pravidel (mluvim o uplnosti typoveho systemu). Myslim si to proto, ze (spravne otypovane) rekurzivni funkce se nedaji podle me v tom ST LC ani zkonstruovat. Pokud nejak dovolime jejich konstrukci, otevirame tim dvere i jejich pouziti v parametrech, a tim se bohuzel (IMHO) dostavame mimo primitivni rekurzi.
Jinak je to zajimava diskuse - podle me je dobre si to ujasnit.
Nebo αβ
To je zverstvo - na to aby si clovek koupil diagonalni papir.
Není mi bohužel jasné, proč to pořád ještě není jasné. Možná jsem měl prohodit parametry u toho operátoru pro rekurzi, aby šel faktoriál vyjádřit curryingem, napsal jsem to konvenčně. Pak tedy faktoriál bude λnω.ρ 1 (λmω.λkω.m*k) n a jeho typ (podle těch typovacích pravidel na Wikipedii) ω→ω. To ρ je úplně to samé jako Churchova negace a disjunkce (a jiné jeho tzv. primitivní symboly, viz jeho původní článek o STT) s úplně normálním typem, nijak formální sílu STT neovlivňuje. Viz ten článek na té encyklopedii filozofie, asi nemá smysl, abych tady nějak obhajoval tvrzení, které tam je formálně dokázané, kdo chce, přečte si ten důkaz tam. (A k té úplnosti, když mám nějakou bezespornou teorii s ρ, tak k ní vždy můžu sestrojit model, takže úplnost STT s ρ nijak neutrpí.)
-
Není mi bohužel jasné, proč to pořád ještě není jasné. Možná jsem měl prohodit parametry u toho operátoru pro rekurzi, aby šel faktoriál vyjádřit curryingem, napsal jsem to konvenčně. Pak tedy faktoriál bude λnω.ρ 1 (λmω.λkω.m*k) n a jeho typ (podle těch typovacích pravidel na Wikipedii) ω→ω. To ρ je úplně to samé jako Churchova negace a disjunkce (a jiné jeho tzv. primitivní symboly, viz jeho původní článek o STT) s úplně normálním typem, nijak formální sílu STT neovlivňuje. Viz ten článek na té encyklopedii filozofie, asi nemá smysl, abych tady nějak obhajoval tvrzení, které tam je formálně dokázané, kdo chce, přečte si ten důkaz tam. (A k té úplnosti, když mám nějakou bezespornou teorii s ρ, tak k ní vždy můžu sestrojit model, takže úplnost STT s ρ nijak neutrpí.)
OK, rozmyslim si to. Takhle na prvni pohled mi neni jasne, kam ti z toho faktorialu zmizelo to odecitani o 1.
-
Není mi bohužel jasné, proč to pořád ještě není jasné. Možná jsem měl prohodit parametry u toho operátoru pro rekurzi, aby šel faktoriál vyjádřit curryingem, napsal jsem to konvenčně. Pak tedy faktoriál bude λnω.ρ 1 (λmω.λkω.m*k) n a jeho typ (podle těch typovacích pravidel na Wikipedii) ω→ω. To ρ je úplně to samé jako Churchova negace a disjunkce (a jiné jeho tzv. primitivní symboly, viz jeho původní článek o STT) s úplně normálním typem, nijak formální sílu STT neovlivňuje. Viz ten článek na té encyklopedii filozofie, asi nemá smysl, abych tady nějak obhajoval tvrzení, které tam je formálně dokázané, kdo chce, přečte si ten důkaz tam. (A k té úplnosti, když mám nějakou bezespornou teorii s ρ, tak k ní vždy můžu sestrojit model, takže úplnost STT s ρ nijak neutrpí.)
OK, rozmyslim si to. Takhle na prvni pohled mi neni jasne, kam ti z toho faktorialu zmizelo to odecitani o 1.
To dělá to ρ, kterýžto operátor se “přepíše” na volání té předané funkce, které dá výsledek volání sebe sama na n-1. To je ostatně to jádro pudla (resp. primitivní rekurze) a důvod, proč to zůstane sémanticky úplné (všechna vyhodnocení zůstanou silně normalizující).
-
OK, rozmyslim si to. Takhle na prvni pohled mi neni jasne, kam ti z toho faktorialu zmizelo to odecitani o 1.
To dělá to ρ, kterýžto operátor se “přepíše” na volání té předané funkce, které dá výsledek volání sebe sama na n-1. To je ostatně to jádro pudla (resp. primitivní rekurze) a důvod, proč to zůstane sémanticky úplné (všechna vyhodnocení zůstanou silně normalizující).
OK, odkud jsi vzal definici toho ρ? Ani v jednom z tech dvou odkazu jsem to nenasel.
-
OK, rozmyslim si to. Takhle na prvni pohled mi neni jasne, kam ti z toho faktorialu zmizelo to odecitani o 1.
To dělá to ρ, kterýžto operátor se “přepíše” na volání té předané funkce, které dá výsledek volání sebe sama na n-1. To je ostatně to jádro pudla (resp. primitivní rekurze) a důvod, proč to zůstane sémanticky úplné (všechna vyhodnocení zůstanou silně normalizující).
odkud jsi vzal definici toho ρ?
To je přeci standardní definice primitivní rekurze, ne? Teď jsem jen na mobilu, ale na wiki v příslušném článku určitě bude (v obecnější podobě). Fakt v tom nehledej nic složitého, je to prostě uzavřená formule λ kalkulu (otypovaná), která se aplikuje na tři parametry, čímž se zredukuje (“vyhodnotí”).
Jinak polopatický popis je také na nlabu, možná pomůže.
-
To je přeci standardní definice primitivní rekurze, ne? Teď jsem jen na mobilu, ale na wiki v příslušném článku určitě bude (v obecnější podobě). Fakt v tom nehledej nic složitého, je to prostě uzavřená formule λ kalkulu (otypovaná), která se aplikuje na tři parametry, čímž se zredukuje (“vyhodnotí”).
Jinak polopatický popis je také na nlabu, možná pomůže.
No zkus tu definici najit, jestli muzes. Ja to co delas znam na urovni netypoveho lambda kalkulu, napriklad z https://www.microsoft.com/en-us/research/uploads/prod/1987/01/slpj-book-1987-r90.pdf (https://www.microsoft.com/en-us/research/uploads/prod/1987/01/slpj-book-1987-r90.pdf) (cetl jsem jen prvnich par kapitol), a tam hned sahnou po tom Y kombinatoru. Operator "primitivni rekurze" jsem v lambda kalkulu neznal, a rad bych videl, jak se da otypovat v ST LC (prijde mi, ze musi nejak "rozbalit" ten typ Churchovych literalu, ale to nejde, pokud maji vsechny stejny typ). Proto me to prekvapilo.
-
To je přeci standardní definice primitivní rekurze, ne? Teď jsem jen na mobilu, ale na wiki v příslušném článku určitě bude (v obecnější podobě). Fakt v tom nehledej nic složitého, je to prostě uzavřená formule λ kalkulu (otypovaná), která se aplikuje na tři parametry, čímž se zredukuje (“vyhodnotí”).
Jinak polopatický popis je také na nlabu, možná pomůže.
No zkus tu definici najit, jestli muzes. Ja to co delas znam na urovni netypoveho lambda kalkulu, napriklad z https://www.microsoft.com/en-us/research/uploads/prod/1987/01/slpj-book-1987-r90.pdf (https://www.microsoft.com/en-us/research/uploads/prod/1987/01/slpj-book-1987-r90.pdf) (cetl jsem jen prvnich par kapitol), a tam hned sahnou po tom Y kombinatoru. Operator "primitivni rekurze" jsem v lambda kalkulu neznal, a rad bych videl, jak se da otypovat v ST LC (prijde mi, ze musi nejak "rozbalit" ten typ Churchovych literalu, ale to nejde, pokud maji vsechny stejny typ). Proto me to prekvapilo.
Pokusím se. Prozatím bych ještě doporučil toto: https://en.m.wikipedia.org/wiki/%CE%9C_operator#Example_%231:_The_bounded_%CE%BC-operator_is_a_primitive_recursive_function Konkrétně: “The bounded μ-operator is a primitive recursive function.” Je teď už jasnější, proč je to ρ úplně normální neproblematická funkce? Možná jsem měl zdůraznit to “unbounded”.