Simpelthen indtastet lambdaregning

Simpelt indtastet lambdaregning ( simpelt indtastet lambdaregning , lambdaregning med simple typer , system $\lambda ^{\højrepil }$ ) er et system med maskinskrevet lambdaregning , hvor en speciel "pil"-type er tildelt en lambdaabstraktion. Dette system blev foreslået af Alonzo Church i 1940 [1] . For formalismen af kombinatorisk logik tæt på lambda-regningen blev et lignende system overvejet af Haskell Curry i 1934 [2] .

Formel beskrivelse

Syntaks af typer og termer

I den grundlæggende version af systemet er typer konstrueret ud fra et sæt variabler ved hjælp af en enkelt binær infix-konstruktør . Traditionelt bruges græske bogstaver til typevariable, og operatoren betragtes som højreassociativ, det vil sige, at den er en forkortelse for . Bogstaver fra anden halvdel af det græske alfabet ( , , osv.) bruges ofte til at betegne vilkårlige typer, ikke kun typevariable. $\lambda ^{\højrepil }$ $\højre pil$ $\højre pil$ $\alpha \rightarrow \beta \til \gamma$ $\alpha \rightarrow (\beta \to \gamma )$ $\sigma$ $\tau$

Der er to versioner af det enkelt indtastede system. Hvis de samme termer bruges som termer som i den utypede lambdaregning , så kaldes systemet implicit indtastet eller Curry -type . Hvis variablerne i lambda-abstraktionen er annoteret med typer, kaldes systemet eksplicit typet eller kirketype . Som et eksempel er her en identisk curry-stil-funktion: , og kirke-stil: . $\lambda x.~x$ $\lambda x\!:\!\alpha .~x$

Reduktionsregler

Reglerne for reduktion adskiller sig ikke fra reglerne for utypebestemt lambdaregning . -reduktion defineres gennem substitution $\beta$

(\lambda x\!:\!\sigma .~M)~N\ \to _{{\beta }}\ M[x:=N]

$\eta$ -reduktion er defineret som følger

\lambda x\!:\!\sigma .~M~x\ \to _({\eta }}\ M

-reduktionen kræver, at variablen ikke er fri i termen . $\eta$ $x$ $M$

Skrivekontekster og typepåstande

En kontekst er et sæt kommaseparerede variable skrivesætninger, f.eks.

f\!:\!(\beta \to \gamma ),g\!:\!(\alpha \to \beta ),x\!:\!\alpha

Kontekster er normalt angivet med store græske bogstaver: . Du kan tilføje en variabel "frisk" for denne kontekst til konteksten: hvis er en gyldig kontekst, der ikke indeholder variablen , så er det også en gyldig kontekst. $\Gamma ,\Delta$ $\Gamma$ $x$ $\Gamma ,x\!:\!\alfa$

Den generelle form for en skriveerklæring er:

\Gamma \vdash M\!:\!\sigma

Dette lyder som følger: i kontekst har et udtryk typen . $\Gamma$ $M$ $\sigma$

Indskrivningsregler (ifølge Kirken)

I den enkelt indtastede lambdaregning sker tildelingen af typer til termer efter reglerne nedenfor.

Aksiom. Hvis en variabel er tildelt en type i en kontekst , så har den en type i den kontekst . I form af en slutningsregel: $x$ $\sigma$ $x$ $\sigma$

{{x\!:\!\sigma \in \Gamma } \over {\Gamma \vdash x\!:\!\sigma ))

Introduktionsregel . $\højre pil$ Hvis udtrykket i en eller anden sammenhæng, udvidet med udsagnet, der har type , har type , så har lambda-abstraktionen i den nævnte kontekst (uden ) type . I form af en slutningsregel: $x$ $\sigma$ $M$ $\tau$ $x$ $\lambda x\!:\!\sigma .~M$ $\sigma \to \tau$

{{\Gamma ,x\!:\!\sigma \vdash M\!:\!\tau } \over {\Gamma \vdash (\lambda x\!:\!\sigma .~M)\!:\ !(\sigma \to \tau )}}

slette regel . $\højre pil$ Hvis et udtryk i en eller anden sammenhæng er af typen , og et udtryk er af typen , så er applikationen af typen . I form af en slutningsregel: $M$ $\sigma \to \tau$ $N$ $\sigma$ $M~N$ $\tau$

{{\Gamma \vdash M\!:\!(\sigma \to \tau )\quad \Gamma \vdash N\!:\!\sigma } \over {\Gamma \vdash (M~N)\!: \!\tau}}

Den første regel giver dig mulighed for at tildele en type til frie variabler ved at specificere dem i konteksten. Den anden regel giver dig mulighed for at skrive lambda-abstraktionen med en piletype, og fjerner variablen bundet af denne abstraktion fra konteksten. Den tredje regel giver dig mulighed for at skrive ansøgningen (ansøgningen), forudsat at den venstre ansøger har en passende piltype.

Eksempler på skrivepåstande i kirkelig stil:

x\!:\!\alpha \vdash x\!:\!\alpha

(aksiom)

\vdash (\lambda x\!:\!\alpha .~x)\!:\!(\alpha \to \alpha )

(introduktion )

\højre pil

f\!:\!(\beta \to \gamma \to \delta ),y\!:\!\beta \vdash (f~y)\!:\!(\gamma \to \delta )

(fjernelse )

\højre pil

Egenskaber

Et enkelt indtastet system har egenskaben af typesikkerhed: under-reduktioner, typen af lambda-udtrykket forbliver uændret, og selve indtastningen forstyrrer ikke beregningernes fremskridt. $\beta$
I 1967 beviste William Tait [3] at -reduktion for et simpelt indtastet system har den stærke normaliseringsegenskab: enhver tilladt term kan reduceres til en unik normalform efter et endeligt antal -reduktioner. Som en konsekvens viser det sig, at termernes ækvivalens kan afgøres i dette system. $\beta$ $\beta$ $\beta \eta$
Curry-Howard isomorfisme forbinder den enkelt indtastede lambda-regning med den såkaldte "minimallogik" (et fragment af intuitionistisk propositionel logik , der kun inkluderer implikation ): de befolkede typer er nøjagtigt tautologier af denne logik, og termerne svarer til beviser skrevet i form af et naturligt fradrag.

Noter

↑ A. Kirke. En formulering af den simple typeteori // J. Symbolsk Logik. - 1940. - S. 56-68 .
↑ HB Karry. Funktionalitet i kombinatorisk logik // Proc Natl Acad Sci USA. - 1934. - S. 584-590 .
↑ W. W. Tait. Intentionelle fortolkninger af funktionaler af endelig type I // J. Symbolsk logik. - 1967. - T. 32 (2) .

Litteratur

Pierce, Benjamin C. Typer og programmeringssprog. - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Oversættelse til russisk: Pierce B. Skriver på programmeringssprog. - Dobrosvet , 2012. - 680 s. — ISBN 978-5-7913-0082-9 .
Barendregt, Henk. Lambda Calculi med typer // Handbook of Logic in Computer Science. - Oxford University Press, 1992. - Vol. II . - S. 117-309 .