Indtastet lambdaregning

Den indtastede lambdaregning er en version af lambdaregningen , der tildeler specielle syntaktiske etiketter kaldet typer til lambda-udtryk. Forskellige sæt regler for konstruktion og tildeling af sådanne etiketter er tilladt, og de giver anledning til forskellige typesystemer.

Type -calculuses er grundlæggende primitive programmeringssprog, der danner grundlaget for typebaserede funktionelle programmeringssprog - applikative sprog - heriblandt ML og Haskell , såvel som generiske imperative programmeringssprog. $\lambda$

$\lambda$ -calculus med typer er sproget i den kartesisk-lukkede kategori , som etablerer en direkte forbindelse med en sådan beregningsmodel som den kategoriske abstrakte maskine . Fra et synspunkt kan type -calculi betragtes som specialiseringer af utypede -calculi, og fra et andet synspunkt kan maskinskrevne sprog tværtimod betragtes som mere grundlæggende, hvorfra utypede sprog opnås som særlige tilfælde. En analyse af dette fænomen er givet af D. Scotts teori om beregning [1] . $\lambda$ $\lambda$

$\lambda$ -calculus med typer tjener som grundlag for udviklingen af nye skrivesystemer til programmeringssprog, da det er ved hjælp af typer og afhængigheder mellem dem, at programmers ønskede egenskaber kommer til udtryk.

I programmering svarer uafhængige computerblokke (funktioner, procedurer, metoder) af programmeringssprog med stærk skrivning til type- udtryk. $\lambda$

Se også

Noter

↑ 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. Ligestilling mellem funktionaler. LogicColl. '73, side 22-37, LNM 453, 1975.
Barendregt H. Lambda Calculi with Types , Handbook of Logic in Computer Science, bind II, Oxford University Press.