In the past couple of lectures we covered the Reduction Semantics for the lambda calculus and understood its coherence by studying the Church-Rosser Theorem. We hereby present a new kind of semantics, namely the natural or structure operational semantics (SoS). There are advantages to either of these semantics: the reduction semantics is easier to implement whereas the natural semantics is easier to reason about.
We will start by presenting the natural semantics for lazy or normal evaluation, followed by an example. We also note that evaluation of lambda terms can be viewed as a relation between them, i.e. a predicate, and that there exists a finite derivation tree to be used in inductive proofs. Finally, we present a theorem which essentially says that both natural and reduction semantics are equivalent.