Parentheses after Typing Environment

Question

I've been reading about System F Omega lately, and I keep stumbling across a construct in typing rules that I cannot find an explanation of: Γ(x) = k. For example, in A Short Introduction to Systems F and F Omega:

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

I see the same construct in Hereditary Substitution for Stratified System F. I understand the bottom part fine. It would read something like: "In context Γ, a has kind k". I've not been able to find an explanation of the top part, and the sources I referenced both assume familiarity with this construct. If I had to guess, I suspect that it means something like "In context a, running a kind-checking algorithm on a gives you kind k as the result". Is that accurate? What online resources describe this construct?

Answer 1

$\Gamma$ here is overloaded notation. The meaning of the expression $\Gamma(x) = \tau$ above the inference line here is given under the "Type rules." section of A Short Introduction to Systems F and F Omega on page 5. In this setting, $\Gamma$ is an inductively-defined function sending variables (in $\Gamma$ considered as a context, i.e. a list of variables) to their types.

A more illustrative, syntactic way to write the rule you give might be: $\frac{}{\Gamma,\ x : \tau\ \vdash x : \tau}$, where $\Gamma$ ranges freely over contexts. Note that the order of variables in a context here does not matter, so this rule allows us to project any variable in a context as a term.

Answer 2

To add to varkor's answer:

A context is just a function sending (some) variables to their types.

So the rule is saying: "If $\Gamma$ assigns the type $\tau$ to variable $x$, then we can deduce $\Gamma \vdash x : \tau$."