[TYPES] Strong Normalization for Dependent Typed Calculus

[Anitha Gollamudi]

Hi,

Looking for some help in understanding the strong normalization (SN) proofs
for LF.

Chapter 13 from the book "Lectures on Curry-Howard Isomorphism" by Sorensen
and Urzyczyn, translates LF (actually \lambda P) to STLC using contracting
maps. I am trying to understand the invariant(s) of the translation.

The first attempt at translation (Definition 13.3.1 on p.334)  uses a
contracting map, b,  that is not strong enough to prove SN. Even then, I am
puzzled by the definition for the case of the constructor variable \alpha
(shown below)

b(\alpa) = p_\alpha

where \alpha is a constructor variable and p_\alpha is a fresh
propositional variable.

However, the translation of the typing context uses a different definition
for translating \alpha.

b(\G) = {x_\alpha : b(k) | (\alpha : k) \in \G  } \cup ...

where x_\alpha is a fresh term variable.

The discrepancy between type and typing context translation  threw me off a
bit for a few  reasons.

1. p_\alpha is a type variable; clearly STLC has no type variables. So, the
translated type does not belong to STLC types.
2. Related to the above point. How to translate a term (x: \alpha) under \G
that has a suitable kind for \alpha?
3. The translation of \G introduces fresh variables x_\alpha that are not
used in the translated terms. So why bother?

Appreciate any pointer/explanation.

Best
Anitha