113
правок
Изменения
→Задача вывода типов в \lambda\Pi-исчислении: More english
=Задача вывода типов в <tex dpi = "180">\lambda\Pi</tex>-исчислении=
{{Определение|definition=Терм <tex>t</tex> типа <tex>T</tex> в контексте <tex>G</tex> называется '''объектом''' (англ. ''object'') в <tex>\Gamma</tex>, если <tex>\Gamma \vdash T : \mathrm{Type}</tex>.}}
{{Утверждение|statement=Если терм <tex>t</tex> является объёктом в контексте <tex>\Gamma</tex>, то он является либо переменной, либо применением, либо абстракцией. Если он является применением <tex>t=(u\ v)</tex>, тогда оба терма <tex>u</tex> и <tex>v</tex> являются объектами в <tex>\Gamma</tex>, если он является абстракцией <tex>t=\lambda x : U . u</tex>, то тогда терм <tex>u</tex> является объектом в контексте <tex>\Gamma\left[x : U\right]</tex>.}}
{{Определение|definition=Множество '''чистых термов''' (англ. ''pure terms'') определяется грамматикой <tex>T ::= x \mid \left(T\ T\right) \mid \lambda x . T</tex>.}}
{{Определение|definition=Пусть <tex>t</tex> {{---}} объект в контексте <tex>\Gamma</tex>. '''Содержимое''' <tex>t</tex> (<tex>\left|t\right|</tex>) {{---}} это рекурсивно определённый чистый терм:
