Solvable terms

A term M of the untyped \lambda-calculus is solvable just if there exist closed terms T_1, \ldots, T_n such that

M T_1 \ldots T_n = \mathbf{I}

where \mathbf{I} \triangleq \lambda x. x.

We can also use any other \beta-normal form instead of \mathbf{I} here too (this yields an equivalent definition).

Relationship to head normal forms

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

The "standard theory" of the untyped \lambda-calculus arises when we equate all unsolvable terms.

See Theory H.

References

@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}
}