A term of the untyped -calculus is solvable just if there exist closed terms such that
where .
We can also use any other -normal form instead of here too (this yields an equivalent definition).
Solvable terms are intimately related to head normal forms, in that
Lemma. A term is solvable if and only if it has a head normal form.
The "standard theory" of the untyped -calculus arises when we equate all unsolvable terms.
See Theory H.
Barendregt, Henk. 1984. Lambda Calculus: Its Syntax and Semantics. Amsterdam: North-Holland. [link]
@book{barendregt_1984,
address = {Amsterdam},
title = {Lambda {Calculus}: {Its} {Syntax} and {Semantics}},
isbn = {978-0-444-87508-2},
publisher = {North-Holland},
author = {Barendregt, Henk},
year = {1984}
}