Даже если понимать под типизацией не определение principle type (наиболее общего типа), а указание какого-то из допустимых, то
Проблема всегда в том, что значит "имеет тип". Если тип неявен и выводится из структуры терма по определенным правилам - это типизация по Карри, в этом случае данный артефакт имеется. А при типизации по Черчу, где каждый подтерм изучаемого терма явно типизирован (тип явно приписан любому терму), всё OK и есть лемма уникальности типов.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2008-03-29 12:56 pm (UTC)Проблема всегда в том, что значит "имеет тип". Если тип неявен и выводится из структуры терма по определенным правилам - это типизация по Карри, в этом случае данный артефакт имеется. А при типизации по Черчу, где каждый подтерм изучаемого терма явно типизирован (тип явно приписан любому терму), всё OK и есть лемма уникальности типов.