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