3
$\begingroup$

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.

Improve this question
$\endgroup$
2

2 Answers 2

Reset to default
4
$\begingroup$

Saying that you consider ⟨objects⟩ modulo ⟨equivalence⟩ means that you treat equivalent objects as equal. This implies that the only properties of the objects that you're interested in are the ones that are invariant under this equivalence, the only functions you're interested in are the ones that turn equivalent objects into equivalent ones, etc.

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.

Improve this answer
$\endgroup$
0
2
$\begingroup$

"lambda terms modulo convertibility" is an informal phrase that means "lambda terms, but we don't make any distinction between any two lambda terms that are convertible".

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.