Every countable poset is embeddable in the poset of unsolvable terms (Q1098834)

A combinator (or closed \(\lambda\)-term) M is solvable if for any combinator N there exists a sequence of combinators \(M_ 1,...,M_ k\) such that \(MM_ 1,...,M_ k=_{\beta}N\) (M is solvable iff M has head normal form.) Most models of \(\lambda\)-calculus do not distinguish between unsolvable combinators. The author uses the structure of the quotient poset to shed some light on their computational behaviour. For combinators M and N, M is said to be more solvable than N (N\(\leq M)\) if there exist combinators \(N_ 1,...,N_ n\) such that \(MN_ 1,...,N_ n=_{\beta}N\). \(\leq\) is a quasiordering of combinators and yields a quotient poset \({\mathcal U}\). \({\mathcal U}\) has a bottom element consisting of all solvable terms and some maximal elements, however its structure is complex. The main result of the paper shows that every countable poset can be isomorphically embedded in \({\mathcal U}\).