Parenthèses après l'environnement de saisie

Question

J'ai lu récemment sur System F Omega et je continue de tomber sur une construction dans les règles de saisie pour laquelle je ne trouve pas d'explication : Γ(x) = k.Par exemple, dans Une brève introduction aux systèmes F et F Omega:

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

Je vois la même construction dans Substitution héréditaire pour le système stratifié F.Je comprends bien la partie inférieure.Cela donnerait quelque chose comme :"Dans le contexte Γ, a a du genre k".Je n'ai pas pu trouver d'explication sur la partie supérieure, et les sources auxquelles j'ai fait référence supposent toutes deux qu'elles sont familières avec cette construction.Si je devais deviner, je soupçonne que cela signifie quelque chose comme « Dans le contexte a, exécutant un algorithme de vérification de type sur a te donne du gentil k comme résultat".Est-ce exact ?Quelles ressources en ligne décrivent cette construction ?

Answer 1

$\Gamma$ voici une notation surchargée.Le sens de l'expression $\Gamma(x) = au$ au-dessus de la ligne d'inférence est donné ici sous le "Tapez les règles." section de Une brève introduction aux systèmes F et F Omega à la page 5.Dans ce cadre, $\Gamma$ est une fonction définie de manière inductive envoyant des variables (en $\Gamma$ considéré comme un contexte, c'est-à-direune liste de variables) à leurs types.

Une manière plus illustrative et syntaxique d'écrire la règle que vous donnez pourrait être : $\frac{}{\Gamma,\x : au\ \vdash x : au}$, où $\Gamma$ varie librement selon les contextes.Notez que l'ordre des variables dans un contexte n'a pas d'importance ici, cette règle nous permet donc de projeter n'importe quelle variable dans un contexte en tant que terme.

Answer 2

Pour ajouter à la réponse de Varkor :

Un contexte est juste une fonction envoyant (certaines) variables à leurs types.

La règle dit donc :"Si $\Gamma$ attribue le type $ au$ à variable $x$, alors on peut en déduire $\Gamma \vdash x : au$."