A lambda term is solvable if its closure by lambda abstractions over its free variables can be applied to finitely many closed lambda terms to obtain in beta equivalence. This is equivalent to having a head normal form. A head variable in a head normal form can be replaced by a projection returning ; conversely standardization theorem for beta reduction traces any successful head computation back to a head variable of the original term.
New to topics? Read the docs here!