In lambda calculus, how would I write a function that returns true when its input is the identity function?

Question

In lambda calculus, how would I write a function that returns true when its input is the identity function?

Assume true is some church encoded value of true.

It seems like this should be an easy function to write. But for every test I think of, a tricky input can outsmart it. Is it impossible?

Answer 1

I := λx.x
0 := λf.λx.x
1 := λf.λx.f x
TRUE := λx.λy.x
FALSE := λx.λy.y
PRED := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
ISZERO := λn.n (λx.FALSE) TRUE

The identity function λx.x is Eta equivalent to church numeral 1 λf.λx.f x. The Fn below will return FALSE for any function that does not evaluate to a church numeral zero (λf.λx.x) after being passed through the predicate function.

λx.(ISZERO (PRED x)) TRUE FALSE

There may exist a function BAD that behaves as such:

λx.(ISZERO (PRED x)) TRUE FALSE BAD := TRUE
BAD != I