Function subscript notation in Types and Programming Language

74 Views Asked by At

In Pierce, Types and Programming Languages, Chapter 6, the reader is asked to define a function $removenames_\Gamma(t)$ where $\Gamma$ is a naming context and $t$ is a term with some number of free variables less than $dom(\Gamma)$ and the function yields a nameless term using de Bruijn indices.

The answer provided in case $t = \lambda.t_1$ is $\lambda.removenames_{\Gamma,x}(t_1)$.

What does the subscript $\Gamma,x$ mean in the answer? I think I understand that the naming context here should be smaller since the abstraction is binding one of the free variables, but if I'm correct (am I?), I'm still not sure how to read the notation.

1

There are 1 best solutions below

0
On

There's a typo in the question: the case you're asking about should be

$removenames_\Gamma (\lambda x. t_1) = \lambda. removenames_{\Gamma, x}(t_1)$

The notation $\Gamma, x$ means $x$ appended to the (right of) list $\Gamma$. The dual of the rule above is

$removenames_\Gamma(x) = \text{the index of the rightmost x in $\Gamma$}$


An example:

$removenames_{[]}(\lambda x . x) = \lambda . removenames_{[x]} (x) = \lambda . 0$