0

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.

sam256
  • 121

1 Answers1

1

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$

abeln
  • 555