Unsolvable lambda term
= Unsolvable lambda term
An unsolvable <lambda term> has no <head normal form>, equivalently it is not a <solvable lambda term>. <Capture-avoiding substitution> and <lambda application> preserve unsolvability: until a head variable appears, head contractions proceed within the original term and cannot inspect the supplied terms.