Gépelt lambda kalkulus

A típusos lambda-számítás a lambda-számítás egy olyan változata , amely speciális szintaktikai címkéket, úgynevezett típusokat rendel a lambda-kifejezésekhez. Az ilyen címkék létrehozásához és hozzárendeléséhez különböző szabályok megengedettek, és ezek különböző típusú rendszereket eredményeznek.

A típusszámítások alapvető primitív programozási nyelvek , amelyek a típusalapú funkcionális programozási nyelvek – az aplikatív nyelvek – alapját képezik, köztük az ML és a Haskell , valamint az általános kötelező programozási nyelvek. $\lambda$

$\lambda$ A -calculus típusokkal a Descartes-zárt kategória nyelve , amely közvetlen kapcsolatot létesít egy olyan számítási modellel, mint a kategorikus absztrakt gép . A típus-kalculi egy szempontból a típusolatlan -kalculi specializációinak tekinthetők , más szempontból pedig a tipizált nyelvek tekinthetők alapvetőbbnek, ahonnan speciális esetekként kapják a típusolatlanokat. Ennek a jelenségnek az elemzését D. Scott számítási elmélete adja [1] . $\lambda$ $\lambda$

$\lambda$ A -calculus a típusokkal alapjául szolgál a programozási nyelvek új tipizálási rendszereinek kidolgozásához, mivel a típusok és a köztük lévő függőségek segítségével fejeződnek ki a programok kívánt tulajdonságai.

A programozásban a programozási nyelvek független számítási blokkjai (függvények, eljárások, módszerek) erős gépeléssel megfelelnek a típuskifejezéseknek. $\lambda$

Lásd még

Jegyzetek

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

Irodalom

Friedman H. Egyenlőség a funkcionálisok között. LogicColl. '73, 22-37. oldal, LNM 453, 1975.
Barendregt H. Lambda Calculi with Types , Handbook of Logic in Computer Science, II. kötet, Oxford University Press.