Two common ways of formulating operational semantics for programming languages based on lambda-calculus are big-step and small-step semantics.
- In a big step semantics, you give a relation $e \Downarrow v$ which directly relates an expression to the value it computes.
- In a small-step semantics, you give a transition relation $e \mapsto e'$ which does one step of evaluation, and you get to a value by iterating the transition relation. $e \mapsto^{*} v$.
These two relations are equivalent, in the sense that $e \Downarrow v$ if and only if $e \mapsto^{*} v$.
However, some things are easier to define one way or another. For example, we can say that a set of terms $R \subseteq \mathrm{Exp}$ is closed under expansion if it satisfies the property that: $$\forall e \in R, e' \in \mathrm{Exp}.\;e' \mapsto e \;\mathrm{implies}\; e' \in R$$
Likewise, a set $R$ is closed under reduction if if satisfies:
$$\forall e \in R, e' \in \mathrm{Exp}.\;e \mapsto e' \;\mathrm{implies}\; e' \in R$$
It's not immediately obvious to me how to formulate expansion or contraction in terms of a big-step semantics. Does anyone know how?