Gödel a staticky typované jazyky

[BaldSlattery]

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

[Reklama]

[JS]

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.

[BaldSlattery]

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.

[JS]

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

[BaldSlattery]

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

[Reklama]