Изменения

{{Определение|definition=Множество '''термов''' (англ. ''term'') рекурсивно определяется следующей грамматикой:

Согласимся '''первым символом''' (англ. ''head symbol'') <tex>t</tex> называть <tex>x</tex> в первом случае, и <tex>\Pi</tex> во втором. '''Первыми переменными''' (англ. ''top variables'') <tex>t</tex> будем называть переменные <tex>x_1, \ldots, x_n</tex>.}}

{{Определение|definition=Терм <tex>t</tex> типа <tex>T</tex> в контексте <tex>G</tex> называется '''объектом''' (англ. ''object'') в <tex>\Gamma</tex>, если <tex>\Gamma \vdash T : \mathrm{Type}</tex>.}}

{{Утверждение|statement=Задача вывода типов в пустом контексте разрешима в <tex>\lambda\Pi</tex>-исчислении.|proof=Типизируемые в пустом контексте чистые термы <tex>\lambda\Pi</tex> исчисления совпадают с типизируемыми выражениями просто типизированного <tex>\lambda</tex>-исчисления, а задача вывода типов в просто типизированном <tex>\lambda</tex>-исчислении разрешима.}}

Рассмотрим контекст