113
правок
Изменения
м
→Задача вывода типов в \lambda\Pi-исчислении
=Задача вывода типов в <tex dpi = "180">\lambda\Pi</tex>-исчислении=
{{Определение|definition=Терм <tex>t</tex> типа <tex>T</tex> в контексте <tex>G</tex> называется '''объектом''' в <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>.}}
