[Комбинаторы, λ-исчисление] Fx = F

[arseniiv]

Нужно найти комбинатор (замкнутый $\lambda$-терм) $F$ такой, что для любого $\lambda$-терма $x$ $Fx = F$.

Не смог вывести ничего интересного, только $F = \lambda x.F$ и $F = YF$. Кто знает, что бы такое применить к $F$ или к чему бы его применить и с чем, чтобы найти его вид?

[Xaositect]

Ну я даже не знаю, что написать, чтобы не написать решения.
$F = \lambda x.F$, значит, $F$ - это неподвижная точка $\lambda y. (\lambda x.y)$, т.е. $K$.
Проверяем. $F = YK$, $Fx = YKx = K(YK)x = YK = F$

[arseniiv]

Понял.

[arseniiv]

А вот ещё задание (все они из книжечки Henk Barendregt и Erik Barendsen «Introduction to Lambda Calculus»):

Найти $F$, если $FI = x$ и $FK = y$.

Моё решение, которое не нравится:
Как мы знаем, $K$ и $K_* = KI$ редуцируются соответственно в первый и второй из двух своих аргументов. Пусть $F = \mathcal F xy$, при том $x, y \notin \mathrm{FV}(\mathcal F)$. Тогда

$$\mathcal F xy = \lambda t . (\mathcal F K K_*) txy,$$

$$\mathcal F = \lambda xyt . \mathcal F K K_* txy,$$

$$\mathcal F = \left( \lambda fxyt . f K K_* txy \right) \mathcal F,$$

$$\mathcal F = Y \left( \lambda fxyt . f K K_* txy \right),$$

т. е. $F = Y (\ldots) xy$.

Действительно равно? (Не хочется проверять «в лоб» — выражения страшные будут…)