113
правок
Изменения
<tex> вместо <math>
=<math tex dpi = "180">\lambda\Pi</mathtex>-исчисление=
Множество ''термов'' рекурсивно определяется следующей грамматикой:
<mathtex>\displaystyle T ::= \mathrm{Type} \mid \mathrm{Kind} \mid x \mid \left(T T\right) \mid \lambda x : T . T \mid \Pi x : T . T</mathtex>.
Термы <mathtex>\mathrm{Type}</mathtex> и <mathtex>\mathrm{Kind}</mathtex> называются ''сортами'', <mathtex>x</mathtex> {{---}} ''переменными'', <mathtex>(t t')</mathtex> {{---}} ''применениями'', <mathtex>\lambda x : t . t'</mathtex> {{---}} ''абстракциями'', <mathtex>\Pi x : t . t'</mathtex> {{---}} произведениями. Обозначение <mathtex>t \rightarrow t'</mathtex> используется вместо <mathtex>\Pi x : t . t'</mathtex>, если <mathtex>x</mathtex> не входит свободно в <mathtex>t'</mathtex>.
Пусть есть термы <mathtex>t</mathtex> и <mathtex>t'</mathtex> и переменная <mathtex>x</mathtex>. Записью <mathtex>t\left[x \leftarrow t'\right]</mathtex> обозначается терм, полученный заменой <mathtex>t'</mathtex> на <mathtex>t</mathtex> в <mathtex>x</mathtex>. Запись <mathtex>t =_\beta t'</mathtex> означает, что термы <mathtex>t</mathtex> и <mathtex>t'</mathtex> <mathtex>\beta</mathtex>-эквивалентны.
''Контекст'' это список пар <mathtex>x : T</mathtex>, где <mathtex>x</mathtex> {{---}} переменная, <mathtex>T</mathtex> {{---}} терм.
Правила вывода для нашего исчисления:
<mathtex>
\displaystyle
\frac{}{\left[ \right] \text{ well-formed}} \text{,} \vspace{3mm} \\
\frac{\Gamma \vdash t : \Pi x : T . T' \qquad \Gamma \vdash t' : T}{\Gamma \vdash \left(t t'\right) : T'\left[x \leftarrow t'\right]} \text{,} \vspace{3mm} \\
\frac{\Gamma \vdash T : s \qquad \Gamma \vdash T' : s \qquad \Gamma \vdash t : T \qquad T =_\beta T'}{\Gamma \vdash t : T'} \text{;}
</mathtex>
где <mathtex>s ::= \mathrm{Type} \mid \mathrm{Kind}</mathtex>.
Терм <mathtex>t</mathtex> ''типизируется'' в контексте <mathtex>\Gamma</mathtex>, если существует такой терм <mathtex>T</mathtex>, что <mathtex>\Gamma \vdash t : T</mathtex>.
Отношение редуцируемости на типизируемых термах сильно нормализуемо и обладает ромбовидным свойством. Каждый типизируемый терм имеет единственную нормальную форму, два терма эквивалентны, если у них одинаковая нормальная форма.
Типизируемый в контексте <mathtex>\Gamma</mathtex> терм <mathtex>t</mathtex> имеет единственный тип с точностью до эквивалентности.
Нормальный терм <mathtex>t</mathtex>, типизируемый в контекте <mathtex>\Gamma</mathtex>, имеет либо вид
<mathtex>\displaystyle t = \lambda x_1 : T_1 \ldots \lambda x_n : T_n . \left(x c_1 \ldots c_n\right)</mathtex>,
где <mathtex>x</mathtex> это переменная или сорт, либо вид
<mathtex>\displaystyle t = \lambda x_1 : T_1 \ldots \lambda x_n : T_n . \Pi x : P . Q\text{.}</mathtex>
Согласимся ''первым символом'' <mathtex>t</mathtex> называть <mathtex>x</mathtex> в первом случае, и <mathtex>\Pi</mathtex> во втором. ''Первыми переменными'' <mathtex>t</mathtex> будем называть переменные <mathtex>x_1, \ldots, x_n</mathtex>.
