3622
правки
Изменения
→Выписать систему уравнений типизации
==Выписать систему уравнений типизации==
(λ a . a a) (λ b c . c)
=== Решение ===
Сначала надо дать типы всем термам и подтермам, раздавая каждый раз новые буквы новым переменным и термам. А потом связать эти буквы по следующим правилам:
* если у нас абстракция (λ x . M) :: T0, x :: T1, M :: T2, то добавляем в систему T0 = T1 -> T2,
* если имеет аппликацию (M N) :: T0, M :: T1, N :: T2, то добавляем T1 = T2 -> T0
* если у нас переменная в теле абстракции встречается несколько раз и мы раздаём каждый раз ей новые буквы, то надо будет потом приравнять типы в аргументе абстракции и внутри её тела.
Итого:
(λ a . a a) (λ b c . c) :: A
(λ a . a a) :: B, (λ b c . c) :: C
a :: D, (a a) :: E
первая и вторая буквы "a" в E {{---}} a :: F, a :: G
Можем сразу расписать часть системы уравнений:
B = C -> A
B = D -> E
F = G -> E
D = F
D = G
Теперь расписываем терм с типом C (раскрыв сокращения для начала): (λ b . (λ c . c)) :: С
b :: H, (λ c . c) :: I
c :: J, c :: K
И добавляем уравнения:
C = H -> I
I = J -> K
J = K
==Кодирование по Чёрчу==
