При выполнении бета-сокращения вы заменяете связанную переменную на лямбда-функцию с предоставленным значением. Обозначение для этого [param := value], и вы берете первую переменную, которая дается.
В случае λx . katze(x)(Garfield) -> katze (Garfield) правильное уменьшение. Мы заменили переменную x на Garfield и удалили λx в процессе, оставив только выражение внутри. Вот шаги, которые будут предприняты:
λx . katze(x)(Garfield)
= katze(x)[x := Garfield]
= katze(Garfield)
Однако два других неправильно. Вы забываете, что у вас есть лямбда-функция, где выражение внутри является другой лямбда-функцией. Поскольку у вас есть одиночный вход, вам нужно только уменьшить одну функцию - первую, оставив другую. Вы можете подумать о том, чтобы отделить внешнюю и обнажить внутреннюю.
В случае λP . λx . P(x)(tea) это может быть лучше представлено как (λP . (λx . P(x)))(tea), где теперь каждая лямбда-функция заключена в скобки. Поскольку мы поставляем один вход tea, мы разрешаем внешнюю функцию только с параметром P (оставляя скобки для некоторой ясности):
(λP . (λx . P(x)))(tea)
= (λx . P(x))[P := tea]
= (λx . P(x))
= λx . tea(x)
или без скобок:
λP . λx . P(x)(tea)
= λx . P(x)[P := tea]
= λx . tea(x)
Что касается конечной функции, она по-прежнему имеет ту же проблему, что и удаление обеих функций, когда дается только один вход. Правильные шаги восстановления:
λy . λx . likes(x, y)(Mia)
= λx . likes(x, y)[y := Mia]
= λx . likes(x, Mia)