Computation

Abstractions represent functions, which can be applied to arguments. The main computation rule is $\beta$-reduction, which indivates how to find the result of the function for a given argument.

A redex is a term of the form $(\lambda x.M)N$, it reduces to the term $M\{x\mapsto N\}$ where $M\{x\mapsto N\}$ is the term obtained when we substitute $x$ by $N$ taking into account bound variables.