3
$\begingroup$

I'm reading Type Theory and Formal Proof by Nederpelt and Geuvers. Chapter 3 is about $\lambda 2$ and $\Pi$-Types (aka System F, I think?) and the derivation rule for 2nd order abstraction seems to forbid "shadowing" of the type variable; i.e. in context $\Gamma \equiv \alpha : *$ it is not possible to derive a term of type $\Pi \alpha : * . \alpha \rightarrow \alpha$. This is because the premise of $abst_2$ in Figure 3.1 page 76 has context $\Gamma, \alpha : *$ and definition 3.4.4 of $\lambda 2$ context at page 75 explicitly says that $\Gamma, \alpha : * \equiv \alpha : *, \alpha : *$ wouldn't be a valid context. First obvious question is: did I understand correctly? If yes, then the second question is why? Even in C++ I can do it...

struct alpha {};

template <typename alpha>
alpha id(alpha x) { return x; }

Edit

I just realised that someone who doesn't have the book might struggle to follow my question. So here's more context. The derivation rule for 2nd order abstraction says:

$$ \frac {\Gamma, \alpha : * \vdash M : \sigma} {\Gamma \vdash \lambda \alpha : * . M : \Pi \alpha : * . \sigma}; $$

a valid $\lambda 2$ context is also recursively defined as:

  1. the empty context $\emptyset$ with an empty domain, i.e. $\texttt{dom}(\emptyset)=()$;
  2. if $\Gamma$ is a valid context, and $\alpha$ is a type variable (i.e $\alpha \in \mathbb{V}$) such that $\alpha \notin \texttt{dom($\Gamma$)}$, then $\Gamma, \alpha : *$ is a valid context with $\texttt{dom}(\Gamma, \alpha : *) = (\texttt{dom}(\Gamma), \alpha)$;
  3. if $\Gamma$ is a valid context, $\rho$ is a type (i.e. $\rho \in \mathbb{T}$) such that $\alpha \in \texttt{dom}(\Gamma)$ for all free type variables $\alpha$ occurring in $\rho$, and if $x \notin \texttt{dom}(\Gamma)$, then $\Gamma, x: \rho$ is a valid context with $\texttt{dom}(\Gamma, x: \rho) = (\texttt{dom}(\Gamma), x)$.

So if my goal is to derive some $M : \Pi \alpha : * . \sigma$ and my current context is $\Gamma \equiv \alpha : *$ then the premise of the 2nd order abstraction rule would be $\alpha : *, \alpha : *$ which is not a valid context according to the definition of context just given.

$\endgroup$
2
  • $\begingroup$ Clearly $\Pi \alpha : * . \alpha \rightarrow \alpha =_\alpha \Pi \beta : * . \beta \rightarrow \beta$ so I can change my problem to search for an alpha-equivalent term and now I can do it, but this feels like a hack. $\endgroup$ Apr 17, 2023 at 22:18
  • 1
    $\begingroup$ It's relatively common to define things in a way that shadowing is not allowed, so that it isn't necessary to spell out the details of operations in the presence of shadowing. This shortens the exposition of the mechanical details in texts that aren't about said details. However, it's equivalent to allowing shadowing, so long as the details are filled in appropriately. Working (roughly) this way is sometimes called "the Barendregt convention." It is a pedagogical tool, though. Not an essential property of the system being defined (usually). $\endgroup$
    – Dan Doel
    Apr 18, 2023 at 16:31

1 Answer 1

3
$\begingroup$

Just because two variables have the same name doesn't mean they're the same variable. Shadowing happens when two variables have the same name in overlapping contexts. It's potentially confusing so we try to avoid that. Fortunately, given a term with shadowing, we can always construct an alpha-equivalent term that has no shadowing. Except when studying variable binding itself, we only ever study terms up to alpha equivalence.

Clearly $\Pi \alpha : \ast. \alpha \rightarrow \alpha =_\alpha \Pi \beta : \ast. \beta \rightarrow \beta $ so I can change my problem to search for an alpha-equivalent term and now I can do it, but this feels like a hack.

It's not a hack, it's the normal thing to do. Systematically renaming variables (i.e. performing an alpha conversion) so that no shadowing occurs is called the (weak) Barendregt convention. In fact, the true Barendregt convention (from Barendregt's treatise on the lambda calculus) is a bit stronger: in a given term, you never use the same name for two different variables (even with non-overlapping contexts such as $(\lambda x. x)(\lambda x. x)$, which does not obey the strong Barendregt convention).

See also Free variables as defined in TAPL seems wrong and Substitution lemma for types.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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