Skrivet lambdakalkyl

Den maskinskrivna lambdakalkylen  är en version av lambdakalkylen som tilldelar speciella syntaktiska etiketter som kallas typer till lambdatermer. Olika uppsättningar regler för att konstruera och tilldela sådana etiketter är tillåtna, och de ger upphov till olika typsystem.

Typkalkyler är grundläggande primitiva programmeringsspråk som utgör grunden för typbaserade funktionella programmeringsspråk  - applikativa språk - bland dem ML och Haskell , såväl som generiska imperativa programmeringsspråk.

-kalkyl med typer är språket i den kartesiska stängda kategorin , som etablerar en direkt koppling till en sådan beräkningsmodell som den kategoriska abstrakta maskinen . Ur en synvinkel kan typ -calculi betraktas som specialiseringar av otypade -calculi, och ur en annan synvinkel, tvärtom, kan maskinskrivna språk betraktas som mer grundläggande, från vilka otypade språk erhålls som specialfall. En analys av detta fenomen ges av D. Scotts teori om beräkning [1] .

-kalkyl med typer fungerar som grunden för utvecklingen av nya typsystem för programmeringsspråk, eftersom det är med hjälp av typer och beroenden mellan dem som programmens önskade egenskaper uttrycks.

Inom programmering motsvarar oberoende beräkningsblock (funktioner, procedurer, metoder) för programmeringsspråk med stark typning typ -uttryck.

Se även

• lambdakub
• curry
• Helt enkelt maskinskriven lambdakalkyl
• Polymorf lambdaanalys

Anteckningar

1. ↑ 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.

Litteratur

• Friedman H. Jämlikhet mellan funktionaler. LogicColl. '73, sid 22-37, LNM 453, 1975.
• Barendregt H. Lambda Calculi with Types , Handbook of Logic in Computer Science, Volym II, Oxford University Press.