En teoría de tipos, un entorno de escritura (o contexto de escritura ) representa la asociación entre nombres de variables y tipos de datos .
Más formalmente, un entorno es un conjunto o una lista ordenada de pares , generalmente escrito como , donde está una variable y su tipo.![{\displaystyle \Gamma}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle \langle x,\tau \rangle }](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle x:\tau}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle x}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle \tau}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
el juicio
![{\displaystyle \Gamma \vdash e:\tau }](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
se lee como " tiene tipo en contexto ". [1]![{\displaystyle e}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle \tau}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle \Gamma}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
Para cada tipo de cuerpo de función se verifica:
![{\displaystyle \Gamma =\{(f,\tau _{1}\times ...\times \tau _{n}\to \tau _{0})|(f,xs,(\tau _{ 1},...,\tau _{n}),t_{f},\tau _{0})\in e\}}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
Ejemplo de reglas de escritura:![{\displaystyle {\begin{array}{c}\Gamma \vdash b:Bool,\Gamma \vdash t_{1}:\tau ,\Gamma \vdash t_{2}:\tau \\\hline \Gamma \ vdash ({\text{if}}(b)t_{1}{\text{else}}t_{2}):\tau \\\end{array}}}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
En los lenguajes de programación de tipo estático, estos entornos se utilizan y mantienen mediante reglas de escritura para verificar el tipo de un programa o expresión determinado.
Ver también
Referencias
- ^ "Cálculo λ simplemente escrito" (PDF) .