Is it possible to reduce a lambda expression to it's smallest equivalent form?

Question

In the Untyped Lambda Calculus, is it possible to reduce any arbitrary expression to it's smallest equivalent form? (defined as an expression with the smallest number of lambda terms) If so, is there an algorithm already defined for this, and what is it's computational complexity? Via the Curry–Howard correspondence, a similar result in logic (first-order logic?) would also be helpful, but not ideal.

Answer 1

If "smallest" is a complet order, then it is not possible. Otherwise you could decide equivalence of two terms by checking that their "smallest form" is the same. It is the same reason why you cannot convert a Turing Machine to the smallest equivalent Turing Machine.

In fact even if there are several "smallest" equivalent formula, it is still not possible, because of Rice theorem. (I switch to TM because it is easier to think of for me, but $\lambda$-calculus should be the same) This is because you could then decide the size of the samllest TM for a language, which is impossible by Rice's theorem.