# What does "lambda terms modulo convertibility" mean?

In "The Lambda Calculus - Its Syntax and Semantics" by H.P. Barendregt (WorldCat) is this statement, the first sentence of chapter 2 after the introduction chapter, so in a way this sets the tone of the book and is useful to understand.

The principal object of study in the λ-calculus is the set of lambda terms modulo convertibility. (p. 22)

Then a few paragraphs later is found convertibility. (p. 23)

The basic equivalence relation of λ-terms is that of convertibility. This relation will be generated by axioms. In order to formulate these axioms, a substitution operator is needed. M[x := N] denotes that the result of substituting N for x in M. ...

Then for 2.1.4 Definition ...

Provability in λ of an equation is denoted by λ ⊢ M = N or often just by M = N. If λ ⊢ M = N, then M and N are called convertible.

What does "lambda terms modulo convertibility" mean?

Based on a comment for this question it seems a different synonym for modulo would clear things up.

In reading TAPL (Types and Programming Languages) by Benjamin C. Pierce (WorldCat) one can get an understanding of axiom with regards to λ-calculus so no need to explain that.

Formally speaking, this means that you're actually studying equivalence classes for the given equivalence relation. In this case, the equivalence relation is the existence of a chain of alpha-conversions (variable renamings) and beta-conversions (replacing a function call by the result of applying the function) between terms. So whenever Barendregt writes e.g. $$\lambda x.(\lambda y.y)x$$, what it really means is “the set of lambda terms that are $$\beta$$-equivalent to $$\lambda x.(\lambda y.y)x$$”, i.e. the infinite set $$\{\lambda x.x, \lambda y.x, (\lambda x.x)(\lambda y.y), \lambda x.(\lambda y.y)x, \lambda u.((\lambda x.x)((\lambda y.y)u)), \ldots \}$$. And when $$M$$ and $$N$$ are two lambda terms, $$M = N$$ means that $$M$$ and $$N$$ are members of the same equivalence class.