2
$\begingroup$

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.

$\endgroup$
4
  • 1
    $\begingroup$ $\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. $\endgroup$ – varkor Mar 2 at 6:02
  • $\begingroup$ @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\}$? $\endgroup$ – user56834 Mar 2 at 6:41
  • $\begingroup$ Yes, that's right. (You might see other ways of defining contexts in other sources, e.g. as lists of types.) $\endgroup$ – varkor Mar 2 at 7:01
  • $\begingroup$ @varkor, Thanks. If you set this as an answer, I'll accept it. $\endgroup$ – user56834 Mar 2 at 8:37
2
$\begingroup$

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$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.