(A mistake above: it should be "we see it's nothing other than (\x, f (x x)) (\x, f (x x))")
While we're here, another cool application is that quines exist. I'll give a way that misuses the theorem (though in a correctable way) to derive a quine. Consider the meta-function quote : L -> L that takes a lambda expression and produces a representation of it (like the representation used by the self-interpreter two comments up). I say meta-function because this isn't implemented by a lambda expression itself. Applying the fixed-point theorem to the same I : L -> (L -> L) with quote, if it were an actual lambda expression, we'd get a lambda expression s with s = quote s. That is, the expression s would evaluate to its own representation!
The fixed point is purportedly (\x, quote (x x)) (\x, quote (x x)), which doesn't make sense since quote is not a function. However, suppose q is a lambda expression that takes representations of lambda expressions and quotes those, so it satisfies the equation q (quote x) = quote (quote x) for all lambda expressions x. Also, let app : L -> L -> L be the constructor for application. Then (\x, q (app x (q x))) (quote (\x, q (app x (q x)))) fixes the problems and is a quine:
(\x, q (app x (q x))) (quote (\x, q (app x (q x))))
= q (app (quote (\x, q (app x (q x))))
(q (quote (\x, q (app x (q x))))))
= quote ((\x, q (app x (q x)))
(quote (\x, q (app x (q x)))))
(A way to do this all above board is to use the self-interpreter and somehow use q in the thing we're trying to find a fixed point of.)
While we're here, another cool application is that quines exist. I'll give a way that misuses the theorem (though in a correctable way) to derive a quine. Consider the meta-function quote : L -> L that takes a lambda expression and produces a representation of it (like the representation used by the self-interpreter two comments up). I say meta-function because this isn't implemented by a lambda expression itself. Applying the fixed-point theorem to the same I : L -> (L -> L) with quote, if it were an actual lambda expression, we'd get a lambda expression s with s = quote s. That is, the expression s would evaluate to its own representation!
The fixed point is purportedly (\x, quote (x x)) (\x, quote (x x)), which doesn't make sense since quote is not a function. However, suppose q is a lambda expression that takes representations of lambda expressions and quotes those, so it satisfies the equation q (quote x) = quote (quote x) for all lambda expressions x. Also, let app : L -> L -> L be the constructor for application. Then (\x, q (app x (q x))) (quote (\x, q (app x (q x)))) fixes the problems and is a quine:
(A way to do this all above board is to use the self-interpreter and somehow use q in the thing we're trying to find a fixed point of.)