Calcul lambda tipizat

Calculul lambda tipizat este o versiune a calculului lambda care atribuie etichete sintactice speciale numite tipuri termenilor lambda. Sunt permise seturi diferite de reguli pentru construirea și atribuirea unor astfel de etichete și dau naștere la diferite sisteme de tip.

Calculele de tip sunt limbaje de programare primitive fundamentale care oferă baza pentru limbaje de programare funcționale bazate pe tipuri - limbaje aplicative - printre ele ML și Haskell , precum și limbaje de programare imperative generice. $\lambda$

$\lambda$ -calculul cu tipuri este limbajul categoriei cartezian-închise , care stabilește o legătură directă cu un astfel de model de calcul precum mașina abstractă categorială . Dintr-un punct de vedere, tipul -calculi pot fi considerate ca specializări ale netipizate -calculi, iar din alt punct de vedere, dimpotrivă, limbile tipizate pot fi considerate mai fundamentale, din care cele netipizate se obțin ca cazuri speciale. O analiză a acestui fenomen este dată de teoria calculului a lui D. Scott [1] . $\lambda$ $\lambda$

$\lambda$ -calculul cu tipuri servește drept bază pentru dezvoltarea de noi sisteme de tastare pentru limbaje de programare, deoarece prin intermediul tipurilor și dependențelor dintre ele sunt exprimate proprietățile dorite ale programelor.

În programare, blocurile de calcul independente (funcții, proceduri, metode) ale limbajelor de programare cu tastare puternică corespund expresiilor de tip . $\lambda$

Vezi și

Note

↑ Scott DS The lattice of flow diagrams.- Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.- Berlin, Heidelberg, New York: Springer-Verlag, 1971, pp. 311-372.

Literatură

Friedman H. Egalitatea între funcționale. LogicColl. '73, paginile 22-37, LNM 453, 1975.
Barendregt H. Lambda Calculi cu tipuri , Manual de logică în informatică, volumul II, Oxford University Press.