Paréntesis después del entorno de escritura

Question

He estado leyendo sobre System F Omega últimamente y sigo tropezando con una construcción al escribir reglas para la que no puedo encontrar una explicación: Γ(x) = k.Por ejemplo, en Una breve introducción a los sistemas F y F Omega:

Γ(a) = k
--------
Γ ⊢ a : k

Veo la misma construcción en Sustitución hereditaria del sistema estratificado F.Entiendo bien la parte de abajo.Se leería algo como:"En contexto Γ, a tiene tipo k".No he podido encontrar una explicación de la parte superior y las fuentes a las que hice referencia asumen estar familiarizados con esta construcción.Si tuviera que adivinar, sospecho que significa algo como "En contexto a, ejecutando un algoritmo de verificación de tipo en a te da amabilidad k como el resultado".¿Es eso exacto?¿Qué recursos en línea describen esta construcción?

Answer 1

$\Gama$ Aquí hay notación sobrecargada.El significado de la expresión. $\Gamma(x) = au$ encima de la línea de inferencia aquí se da debajo de "Escriba reglas." Sección de Una breve introducción a los sistemas F y F Omega en la página 5.En esta configuración, $\Gama$ es una función definida inductivamente que envía variables (en $\Gama$ considerado como un contexto, es deciruna lista de variables) a sus tipos.

Una forma más ilustrativa y sintáctica de escribir la regla que usted proporciona podría ser: $\frac{}{\Gamma,\ x : au\ \vdash x : au}$, dónde $\Gama$ varía libremente según los contextos.Tenga en cuenta que aquí el orden de las variables en un contexto no importa, por lo que esta regla nos permite proyectar cualquier variable en un contexto como un término.

Answer 2

Para agregar a la respuesta de varkor:

Un contexto es solo una función que envía (algunas) variables a sus tipos.

Entonces la regla dice:"Si $\Gama$ asigna el tipo $ au$ a variable $x$, entonces podemos deducir $\Gamma\vdash x : au$."