Gödel a staticky typované jazyky

BaldSlattery

Re:Gödel a staticky typované jazyky
« Odpověď #45 kdy: 08. 01. 2019, 15:08:50 »
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í.


JS

Re:Gödel a staticky typované jazyky
« Odpověď #46 kdy: 08. 01. 2019, 20:23:12 »
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.

BaldSlattery

Re:Gödel a staticky typované jazyky
« Odpověď #47 kdy: 08. 01. 2019, 20:31:02 »
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á.

JS

Re:Gödel a staticky typované jazyky
« Odpověď #48 kdy: 08. 01. 2019, 21:38:49 »
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.

BaldSlattery

Re:Gödel a staticky typované jazyky
« Odpověď #49 kdy: 08. 01. 2019, 22:21:42 »
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/


BaldSlattery

Re:Gödel a staticky typované jazyky
« Odpověď #50 kdy: 08. 01. 2019, 22:35:02 »
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ů).

BaldSlattery

Re:Gödel a staticky typované jazyky
« Odpověď #51 kdy: 08. 01. 2019, 22:39:03 »
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

rkapl

Re:Gödel a staticky typované jazyky
« Odpověď #52 kdy: 08. 01. 2019, 22:45:58 »
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.

Kód: [Vybrat]
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.

v

Re:Gödel a staticky typované jazyky
« Odpověď #53 kdy: 08. 01. 2019, 22:54:31 »
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

rkapl

Re:Gödel a staticky typované jazyky
« Odpověď #54 kdy: 08. 01. 2019, 22:57:17 »
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).

v

Re:Gödel a staticky typované jazyky
« Odpověď #55 kdy: 08. 01. 2019, 22:57:51 »
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/

Citace
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)

BaldSlattery

Re:Gödel a staticky typované jazyky
« Odpověď #56 kdy: 09. 01. 2019, 00:23:46 »
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/

Citace
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 αβ

JS

Re:Gödel a staticky typované jazyky
« Odpověď #57 kdy: 09. 01. 2019, 09:19:59 »
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.)

Citace
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.

Citace
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.

Citace
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.

Citace
Ú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.

Citace
Nebo αβ

To je zverstvo - na to aby si clovek koupil diagonalni papir.

BaldSlattery

Re:Gödel a staticky typované jazyky
« Odpověď #58 kdy: 09. 01. 2019, 10:10:09 »
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.)

Citace
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.

Citace
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.

Citace
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.

Citace
Ú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.

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

JS

Re:Gödel a staticky typované jazyky
« Odpověď #59 kdy: 09. 01. 2019, 12:19:51 »
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.