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>.}}
{{Определение|definition=Множество '''чистых термов''' определяется грамматикой <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>) {{---}} это рекурсивно определённый чистый терм:
* <tex>\left|x\right| = x</tex>;
* <tex>\left|\left(tt'\right)\right| = \left(\left|t\right|\left|t'\right|\right) </tex>;
* <tex>\left|\lambda x : U . t\right| = \lambda x . \left|t\right|</tex>.}}
{{Определение|definition=Чистый терм <tex>t</tex> называется '''типизируемым''' в контексте <tex>\Gamma</tex>, если существует терм <tex>t'</tex>, типизируемый в неком <tex>\Gamma\Delta</tex>, являющимся расширением <tex>\Gamma</tex>, что <tex>t'</tex> является объектом в <tex>\Gamma\Delta</tex> и <tex>t=\left|t'\right|</tex>.}}
Типизация чистого терма в контексте <tex>\Gamma</tex> это присвоение типов связанным переменным и некоторым свободным переменным, типов которых нет в <tex>\Gamma</tex>. Если же контекст <tex>\Gamma</tex> пустой, то типизация терма в нём будет являться присваиванием типов и связанным и свободным переменным.
{{Утверждение|statement=Задача вывода типов в пустом контексте разрешима в <tex>\lambda\Pi</tex>-исчислении.|proof=Типизируемые в пустом контексте чистые термы <tex>\lambda\Pi</tex> исчисления совпадают с типизируемыми выражениями просто типизированного <tex>\lambda</tex>-исчисления, а задача вывода типов в просто типизированном <tex>\lambda</tex>-исчислении разрешима.}}
