113
правок
Изменения
→Задача вывода типов в \lambda\Pi-исчислении
{{Определение|definition=Множество '''чистых термов''' (англ. ''pure terms'') определяется грамматикой <tex>T ::= x \mid \left(T\ T\right) \mid \lambda x . T</tex>.}}
{{Определение|definition=Пусть <tex>t</tex> {{---}} объект в контексте <tex>\Gamma</tex>. '''Содержимое''' (англ. ''content'') <tex>t</tex> (<tex>\left|t\right|</tex>) {{---}} это рекурсивно определённый чистый терм:
* <tex>\left|x\right| = x</tex>;
* <tex>\left|\lambda x : U . t\right| = \lambda x . \left|t\right|</tex>.}}
{{Определение|definition=Чистый терм <tex>t</tex> называется '''типизируемым''' (англ. ''typable'') в контексте <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> пустой, то типизация терма в нём будет являться присваиванием типов и связанным и свободным переменным.
