113
правок
Изменения
→\lambda\Pi-исчисление: English terms
=<tex dpi = "180">\lambda\Pi</tex>-исчисление=
{{Определение|definition=Множество '''термов''' (англ. ''term'') рекурсивно определяется следующей грамматикой:
<tex>\displaystyle T ::= \mathrm{Type} \mid \mathrm{Kind} \mid x \mid \left(T\ T\right) \mid \lambda x : T . T \mid \Pi x : T . T</tex>.
* Термы <tex>\mathrm{Type}</tex> и <tex>\mathrm{Kind}</tex> называются '''сортами'''(англ. ''sorts''), * <tex>x</tex> {{---}} '''переменными'''(англ. ''variables''), * <tex>(t\ t')</tex> {{---}} '''применениями'''(англ. ''applications''), * <tex>\lambda x : t . t'</tex> {{---}} '''абстракциями'''(англ. ''abstractions''), * <tex>\Pi x : t . t'</tex> {{---}} '''произведениями'''(англ. ''products''). Обозначение <tex>t \rightarrow t'</tex> используется вместо <tex>\Pi x : t . t'</tex>, если <tex>x</tex> не входит свободно в <tex>t'</tex>.}}
Пусть есть термы <tex>t</tex> и <tex>t'</tex> и переменная <tex>x</tex>. Записью <tex>t\left[x \leftarrow t'\right]</tex> обозначается терм, полученный заменой <tex>t'</tex> на <tex>t</tex> в <tex>x</tex>. Запись <tex>t =_\beta t'</tex> означает, что термы <tex>t</tex> и <tex>t'</tex> <tex>\beta</tex>-эквивалентны.
{{Определение|definition='''Контекст''' (англ. ''context'') это список пар <tex>x : T</tex>, где <tex>x</tex> {{---}} переменная, <tex>T</tex> {{---}} терм.}}
{{Определение|definition=Правила вывода для нашего исчисления:
где <tex>s ::= \mathrm{Type} \mid \mathrm{Kind}</tex>, а <tex>\mathrm{WF}</tex> {{---}} множество корректных грамматик.
Терм <tex>t</tex> '''типизируется''' (англ. ''well-typed'') в контексте <tex>\Gamma</tex>, если существует такой терм <tex>T</tex>, что <tex>\Gamma \vdash t : T</tex>.}}
Отношение редуцируемости на типизируемых термах сильно нормализуемо и обладает ромбовидным свойством. Каждый типизируемый терм имеет единственную нормальную форму, два терма эквивалентны, если у них одинаковая нормальная форма.
<tex>\displaystyle t = \lambda x_1 : T_1 \ldots \lambda x_n : T_n . \Pi x : P . Q\text{.}</tex>
Согласимся '''первым символом''' (англ. ''head symbol'') <tex>t</tex> называть <tex>x</tex> в первом случае, и <tex>\Pi</tex> во втором. '''Первыми переменными''' (англ. ''top variables'') <tex>t</tex> будем называть переменные <tex>x_1, \ldots, x_n</tex>.}}
=Задача вывода типов в <tex dpi = "180">\lambda\Pi</tex>-исчислении=
