Gödel a staticky typované jazyky

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

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

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.

[Reklama]

[BaldSlattery]

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.

[Mirek Prýmek]

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

[JS]

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.

[BaldSlattery]

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

[Reklama]

[JS]

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

[BaldSlattery]

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.

[BaldSlattery]

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.

[v]

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

[BaldSlattery]

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.

[JS]

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.

[JS]

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.

[v]

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

[BaldSlattery]

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.

[BaldSlattery]

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.