Solve recursive equation in lambda calculus

256 Views Asked by At

I need to find such F, so that for any M $FM = MF$. I can't figure out, how to bring this equation to the form like this: $F = TF$, so that I could just apply Y combinator

1

There are 1 best solutions below

1
On

Try setting

$$T = \lambda FM.MF$$

So

$$F = (\lambda FM. MF)F$$

Or

$$F = Y(\lambda FM. MF)$$

We can verify that this is correct using the definition of $Y$:

$$ \begin {align} Fa &= (\lambda f.(\lambda x.f(xx))(\lambda x.f(xx)))(\lambda FM.MF)a \\ &= (\lambda x.(\lambda FM.MF)(xx))(\lambda x.(\lambda FM.MF)(xx))a \\ &= (\lambda xM. M(xx))(\lambda xM. M(xx))a \\ &= a (\lambda xM. M(xx))(\lambda xM. M(xx)) \end {align} $$