Skrivregel

I typteorin är en typningsregel en inferensregel som beskriver hur ett typsystem tilldelar en typ till en syntaktisk konstruktion. Dessa regler kan tillämpas av typsystemet för att avgöra om ett program är välskrivet och vilka typuttryck som har. Ett prototypiskt exempel på användningen av skrivregler är att definiera typinferens i den enkelt skrivna lambdakalkylen, som är det interna språket för kartesiska slutna kategorier .

Notation

Skrivregler anger strukturen för en skrivrelation som relaterar syntaktiska termer till deras typer. Syntaktiskt betecknas typningsrelationen vanligtvis med ett kolon, så till exempel $e\!:\!\tau$ anger att ett uttryck $e$ har typen $\tau$ . Reglerna i sig specificeras vanligtvis med beteckningen naturlig deduktion . Till exempel anger följande skrivregler skrivrelationen för ett enkelt språk med booleska språk :

{\frac {}{{\mathsf {true}}:{\mathsf {Bool}}}}\qquad {\frac {}{{\mathsf {false}}:{\mathsf {Bool} }}}\qquad {\frac {e_{1}:{\mathsf {Bool}}\quad \;e_{2}:\tau \quad \;e_{3}:\tau }{\mathbf {if} \ e_{1}\ \mathbf {då} \ e_{2}\ \mathbf {else} \ e_{3}:\tau }}

Varje regel anger att slutsatsen under linjen kan härledas från premisserna ovanför linjen. De två första reglerna har inga premisser ovanför linjen, så de är axiom . Den tredje regeln har premisser ovanför linjen (specifikt tre premisser), så det är en slutledningsregel .

I programmeringsspråk beror typen av variabel på var den är bunden , vilket kräver kontextkänsliga skrivregler. Dessa regler ges av en skrivbedömning \ , vanligtvis skriven ${\displaystyle \Gamma \vdash e:\tau } ,$ som anger att ett uttryck $displaystyle e}$ har typen $\tau$ under en skrivkontext $\Gamma$ som relaterar variabler till deras typer. Denna notation kan användas för att ge skrivregler för variabelreferenser och lambdaabstraktion i den enkelt skrivna lambdakalkylen :

{:\} tau \in \Gamma }{\Gamma \vdash x:\tau }}\qquad {\frac {\Gamma ,x{:}\tau _{1}\vdash e:\tau _{2}}{\Gamma \vdash (\lambda x{:}\tau _{1}.\,e):\tau _{1}\högerpil \tau _{2}}}

På liknande sätt beskriver följande skrivregel $\mathbf {let}$ -konstruktionen av Standard ML :

{\frac {\Gamma{ \vdash 1}:\tau _{1}\qquad \Gamma ,x{:}\tau _{1}\vdash e:\tau _{2}}{\Gamma \vdash \mathbf {let} \ x=e_{ 1}\ \mathbf {in} \ e_{2}\ \mathbf {end} :\tau _{2}}}

Inte alla system med skrivregler anger direkt en typkontrollalgoritm . Till exempel kräver skrivregeln för att applicera en parametriskt polymorf funktion i Hindley-Milner-typsystemet " gissa" den lämpliga typen vid vilken funktionen ska instansieras. Att anpassa ett deklarativt regelsystem till en avgörbar algoritm kräver produktion av ett separat, algoritmiskt system som kan bevisas specificera samma typningsrelation.

Se även

Vidare läsning

Cardelli, Luca (mars 1996). "Typ system" (PDF) . ACM Computing Surveys . 28 (1): 263–264. doi : 10.1145/234313.234418 . S2CID 227408784 .