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.