функции едят констант - мультифильмы

[bntr]

fst (E1,E2) = E1



mul 2 3 = 6




учитывая
T ≡ (\x y -> x)
fst ≡ (\p -> p T)
(E1,E2) ≡ (\f -> f E1 E2)
mul ≡ (\m n f x -> m (n f) x)
5 ≡ (\f x -> f (f (f (f (f x)))))

fst (E1,E2)
= (\p -> p (\x y -> x)) (\f -> f E1 E2)
= (\f -> f E1 E2) (\x y -> x)
= (\x y -> x) E1 E2
= (\y -> E1) E2
= E1

mul 2 3
= (\m n f x -> m (n f) x) (\f x -> f (f x)) (\f x -> f (f (f x)))
...
= (\f x -> f (f (f (f (f (f x))))))
= 6