# What does $\text{dom}(\Gamma)$ mean in the context of an inference rule?

In the wikipedia page on pure type systems, it gives the following inference rule:

$$\frac{\Gamma \vdash A : s \quad x \notin \text{dom}(\Gamma)}{\Gamma, x : A \vdash x : A }\quad \text{(start)}$$

What does $$\text{dom}(\Gamma)$$ mean here? These are string rewriting systems, so $$\Gamma$$ is supposed to be a string of symbols, a purely syntactic object. I'm not sure what a "domain of a string" is.

• $\Gamma$ here is interpreted as a function from a set of variable names to the set of types. $x \notin \mathrm{dom}(\Gamma)$ means that $x$ is a fresh variable name, not in context. Mar 2, 2021 at 6:02
• @varkor, thank you. Just to check that I understand what you're saying: I was thinking of it as a string of typing statements $t_1:T_1,...,t_n:T_n$, where $t_i$ is a term variable and $T_i$ a specific type (not a type variable). Instead, you're saying, interpret this as a function $\Gamma$ defined by $\Gamma(t_i)=T_i$ for all $i\in \{1,...,n\}$? Mar 2, 2021 at 6:41
• Yes, that's right. (You might see other ways of defining contexts in other sources, e.g. as lists of types.) Mar 2, 2021 at 7:01
• @varkor, Thanks. If you set this as an answer, I'll accept it. Mar 2, 2021 at 8:37

There are various ways to define contexts in type theories. In this style, we assume there is some infinite set of variable names $$V$$ and define the context $$\Gamma : V \rightharpoonup S$$ as a partial function from the set of variable names to the set of types. $$\mathrm{dom}(\Gamma)$$ is then the subset of $$V$$ on which $$\Gamma$$ is defined, i.e. the variables in the context $$\Gamma$$. To require that $$x \notin \mathrm{dom}(\Gamma)$$ is asking for $$x$$ to be a fresh variable for the context $$\Gamma$$.