λβ theory

The \lambda\beta theory of the untyped \lambda-calculus is the theory induced by a single axiom, which is known as \beta:

(\lambda x. M)N = M[N/x]

The theory is then closed under the usual rules that make equality an equivalence relation (reflexivity, symmetry, transitivity) and a congruence (i.e. respecting every constructor - in this case just abstraction and application).

The theory is the main subject of study of Barendregt's seminal book Barendregt 1984.

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