Synopsis
The system we will talk about today is called small-step semantics, also called transition semantics, or even operational semantics. The idea with this semantics is that we model what one step of computation looks like, and use that to describe the meaning of a program.
One very important concept that comes up with this form is the Church-Rosser theorem.