3622
правки
Изменения
м
→Решение
Сначала надо дать типы всем термам и подтермам, раздавая каждый раз новые буквы новым переменным и термам. А потом связать эти буквы по следующим правилам:
* если у нас абстракция (λ x . M) :: T0, x :: T1, M :: T2, то добавляем в систему T0 = T1 -> T2,
* если имеет имеем аппликацию (M N) :: T0, M :: T1, N :: T2, то добавляем T1 = T2 -> T0
* если у нас переменная в теле абстракции встречается несколько раз и мы раздаём каждый раз ей новые буквы, то надо будет потом приравнять типы в аргументе абстракции и внутри её тела.
