Eta-reduction is the process of removing redundant lambda abstractions from a term. For example, the term λx. f x can be eta-reduced to f but only if
x is not free in f
f is pure expression
A term is pure if it does not contain any side effects, such as Error, Force or saturated builtin applications.
Error is not pure because it halts the computation.
Force is not pure because it can halt the evaluation if the argument is not a Delayed term or a builtin that must be forced.
a saturated builtin application is not pure because it can halt the evaluation in some cases. For example, DivideInteger(1, 0) will halt the evaluation.
A builtin application is saturated if it has all its arguments applied. For example, AddInteger(1, 2) is saturated but AddInteger(1) is not.