$$\renewcommand{\fv}{\operatorname{FV}}
\renewcommand{\unit}{\textsf{unit}}
\renewcommand{\t}{\tau}
\renewcommand\proves\vdash
\renewcommand{\Var}{\textbf{Var}}
\renewcommand{\Type}{\textbf{Type}}
\renewcommand{\nat}{\mathbb N}
\renewcommand{\Add}{\mathsf{add}}
\renewcommand{\Succ}{\mathsf{succ}}
$$
1. Pure $\lambda$-calculus
Definition. we know that pure $\lambda$-calculus formally defined as follows
$$e:= x\mid \lambda x. e\mid e_1\ e_2
$$
Definition. A $\lambda$ term $e$ is called closed if $\fv (e)=\emptyset$
2. Evaluation Contexts
2.1. Call by Value
In CBV $\lambda$-calculus, a value is defined as
$$v:=\lambda x.e
$$
The small step-operational semantics of CBV $\lambda$-calculus is defines as
$$\frac{}{(\lambda x.e)v\to e[x\mapsto v]}\\
\frac{e_1\to e_1'}{e_1\ e_2\to e_1'\ e_2}\\
\frac{e_2\to e_2'}{v\ e_2\to v\ e_2'}
$$
2.2. Call by Name
2.3. Evaluation Context
We have seen three different semantics (normal order, CBV applicative order, CBN applicative order) for $\lambda$-calculus, and they all have a similar structure: one rule that defines $\beta$-reduction, and other rules simply specify the order in which the $\beta$-reductions can be performed. Small-step operational semantics always have this distinction, and in fact we can split rules into two classes,
- reduction rule, which describe the actual computational steps; and
- evaluation order rules, which constrain the choice of reductions that can be performed next.