Понимание доказательства сильной нормализации исчисления конструкций

У меня есть трудности в понимании доказательства строгой нормализации для исчисления конструкций. Я пытаюсь следовать доказательству в работе Германа Гойвера «Краткое и гибкое доказательство строгой нормализации для исчисления конструкций».

Я могу хорошо следовать основной линии рассуждений. Конструкции Geuvers для каждого типа$T$ интерпретация $[\![T]\!]_\xi$ основанный на некоторой оценке переменных типа $\xi(\alpha)$, И тогда он строит некоторую интерпретацию термина$(\!|M|\!)_\rho$ основанный на некоторой оценке переменных термина $\rho(x)$ и доказывает, что для достоверных оценок утверждение $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ для всех $\Gamma\vdash M:T$ держит.

Моя проблема: для простых типов (таких как системные типы F) интерпретация типов $[\![T]\!]_\xi$ это действительно набор терминов, поэтому утверждение $(\!|M|\!)_\rho \in [\![T]\!]_\xi$имеет смысл. Но для более сложных типов интерпретация$[\![T]\!]_\xi$это не набор терминов, а набор функций некоторого подходящего функционального пространства. Я думаю, я почти понимаю конструкцию функциональных пространств, однако она не может придавать никакого значения$(\!|M|\!)_\rho \in [\![T]\!]_\xi$ для более сложных типов $T$,

Кто-нибудь может объяснить или дать ссылки на некоторые более понятные презентации доказательства?

Изменить: Позвольте мне попытаться сделать вопрос яснее. Контекст$\Gamma$ имеет объявления для переменных типа $\alpha:A$и переменные объекта. Оценка типа действительна, если для всех$(\alpha:A) \in \Gamma$ с $\Gamma\vdash A:\square$ тогда $\xi(\alpha) \in \nu(A)$действует. Но$\nu(A)$ может быть элементом $(SAT)^*$ и не только $SAT$, Поэтому нельзя определить действительный срок оценки для$\rho(\alpha)$, $\rho(\alpha)$ должен быть термином, а не некоторой функцией функционального пространства.

Редактировать 2: пример, который не работает

Давайте сделаем следующий корректный вывод:

В последнем контексте допустимая оценка типа должна удовлетворять $\xi(\beta) \in \nu(\Pi \alpha:*.*) = \{f| f:\text{SAT} \to \text{SAT}\}$, Для оценки этого типа нет действительного термина оценки.

К сожалению, я не уверен, что ресурсов для новичков больше, чем аккаунт Geuvers. Вы можете попробовать эту заметку Криса Касингино, которая содержит несколько доказательств в мучительных деталях.

Я не уверен, что понимаю суть вашей путаницы, но я думаю, что одна важная вещь, которую стоит отметить, это следующая лемма (следствие 5.2.14), доказанная в классическом тексте Барендрегта :

Это означает, что в то время как $[\![T]\!]_\xi$ может быть сложной функцией, если $\Gamma \vdash M:T$ держит, то $[\![T]\!]_\xi$ должен быть набор терминов .

Об этом говорится в общих чертах (раздел 3.1), где $(\!|t|\!)_\sigma\in[\![T]\!]_\xi$ только если $\Gamma \vdash t:T :*$, что соответствует нашему ожиданию, а именно, что интерпретация типа должна быть набором терминов, т.е. ${\cal V}(*)\subseteq{\cal P}(\mathrm{Term})$ (верно, ${\cal V}(*)=\mathrm{SAT}$!)

Это распространенная ситуация в теории типов, что, хотя мы заинтересованы только в «базовом виде» (здесь$*$) нам еще предстоит определить семантику для вещей более высокого вида (отсюда и необходимость $\mathrm{SAT}^*$). В конце концов, все получается, потому что только вид, населенный типами,$*$ (а также $\square$, но это не очень важно).