= Solvable lambda term
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 $I=\lambda x.x$ 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 $I$; conversely <standardization theorem for beta reduction> traces any successful head computation back to a head variable of the original term.
Back to article page
