Как уменьшить лямбда-исчисление

Я взял на себя смелость переписать его на синтаксис haskell

(\y -> x (\x-> x y))
(\y -> x (\x-> x y)) t

x (\x -> x t)

поскольку y уже привязан к входу \y, все y будут заменены на t.

Изменить: как отмечено в комментарии ниже, если t содержит свободный x, было бы важно переименовать связанный x в этой области на «свежее» имя. Это имя в настоящее время не имеет никакого значения. Если мы скажем

let t = \t -> x t

Тогда правильная замена будет выглядеть так

x (\z -> z (\t -> x t))

Где, как указано в pigworker, некоторый z выбран для свежести в качестве нового идентификатора, чтобы заменить наш связанный x, чтобы предотвратить скрытие свободного x в t.