(^f g x. f x (g x))(^x y. x)(^x y. x)
with ^ being lambda.
The result should be ^x. x
What I have tried so far and got to a result:
-do an alfa reduction for the 2 x's at the end with z = (^z y. z)
-replace f with (^z y. z) and I get this: (^g x. ((^z y. z)) x (g x))(^z y. z)
-the I replace g with (^z y. z) and get: (^x. ((^z y. z)) x ((^z y. z) x))
-now I replace both z's with x and get: (^x. (^y. x) (^y. x))
-now since I do not have a y in the first (^y. x) I can get rid of the second (^y. x) and get finally: ^x. x
I got the right answer but I am not 100% sure it's OK how I did it. If anyone could point out if there are any errors I would appreciate it.
The second one which I can't seem to get is this:
(^y. x (^x. x))[(^y. y x)/x]
Here I am supposed to substitute x with (^y. y x). The book states that in cases like this I should rename some variables so they do not affect the expression. But I'm really confused and don't know which one. I would go for the y first because if I would substitute the first x with the expression after it that y would become bound.
If anyone could explain this example a bit that would be great.