Difference between revisions of "Ce tip are Y - combinatorul paradoxal ?"
m |
|||
| Line 1: | Line 1: | ||
[[Category:Ro]] |
[[Category:Ro]] |
||
| − | Intrebarea este daca in lambda calculul tipizat (adica lambda calculul acompaniat cu tipuri) exista UN ANUME tip care sa poata fi atribuit lui [[Y]] - combinatorul paradoxal cu ajutorul caruia se exprima recursia. In practica acest lucru este evident dificil. O parte din problema consta in faptul ca la o aplicare x x (citeste: "x aplicat lui x") ar trebui sa fie indeplinite doua conditii: |
+ | Intrebarea este daca in lambda calculul tipizat (adica lambda calculul acompaniat cu tipuri) exista UN ANUME tip care sa poata fi atribuit lui [[Y]] - combinatorul paradoxal cu ajutorul caruia se exprima recursia. In practica acest lucru este evident dificil. O parte din problema consta in faptul ca la o aplicare x x (citeste: "x aplicat lui x") ar trebui sa fie indeplinite doua conditii: <br> |
| − | 1) primul x sa aiba tipul ''a -> b '' |
+ | 1) primul x sa aiba tipul ''a -> b '' <br> |
| − | 2) al doilea x sa aiba tipul ''a'' |
+ | 2) al doilea x sa aiba tipul ''a'' <br> |
din cauza regulii care spune ca la aplicarea unei expresii (in esenta aplicarea unei functii) tipul ei este t1 -> t2 iar al argumentului este t1. |
din cauza regulii care spune ca la aplicarea unei expresii (in esenta aplicarea unei functii) tipul ei este t1 -> t2 iar al argumentului este t1. |
||
| − | Din nefericire este vorba de acelasi x, ceea ce explica dificultatea de a scrie |
+ | Din nefericire este vorba de acelasi x, ceea ce explica dificultatea de a-l scrie pe [[Y]] in lambda calculul cu tipuri. |
| − | pe [[Y]] cu tipuri. |
||
Teorie: S-a demonstrat ca in lambda calculul pur tipizat nu exista operatori / combinatori de punct fix. |
Teorie: S-a demonstrat ca in lambda calculul pur tipizat nu exista operatori / combinatori de punct fix. |
||
Revision as of 18:44, 10 February 2008
Intrebarea este daca in lambda calculul tipizat (adica lambda calculul acompaniat cu tipuri) exista UN ANUME tip care sa poata fi atribuit lui Y - combinatorul paradoxal cu ajutorul caruia se exprima recursia. In practica acest lucru este evident dificil. O parte din problema consta in faptul ca la o aplicare x x (citeste: "x aplicat lui x") ar trebui sa fie indeplinite doua conditii:
1) primul x sa aiba tipul a -> b
2) al doilea x sa aiba tipul a
din cauza regulii care spune ca la aplicarea unei expresii (in esenta aplicarea unei functii) tipul ei este t1 -> t2 iar al argumentului este t1.
Din nefericire este vorba de acelasi x, ceea ce explica dificultatea de a-l scrie pe Y in lambda calculul cu tipuri.
Teorie: S-a demonstrat ca in lambda calculul pur tipizat nu exista operatori / combinatori de punct fix.
Bibliografie:
Cititi primele paragrafe din prima coloana de la pagina 376 (acesta este numarul tiparit pe pagina) din lucrarea:
Hudak Paul, Conception, Evolution and, Application of Functional Programming Languages ACM Computing Surveys, vol 21, no 3 , Sept 1989 - care ar trebui sa fie disponibila in format pdf aici.
Pagina indexata la indexul Categories:Ro
<= Inapoi la pagina principala Ro/Haskell.
<- Inapoi la inceputul paginii 'Intrebarile incepatorului Ro/Haskell'.