Big-step semantics: Defining arithmetic expressions and commands

This lecture focuses on defining a simple programming language and its semantics using big-step semantics. The instructor begins by reviewing the language of arithmetic expressions, which includes constants, variables, and operations such as addition, subtraction, and multiplication. The notation for these expressions is established to simplify the representation of the language. The lecture then transitions to the concept of valuations, which are partial maps from variables to natural numbers, and discusses operations like 'get' and 'set' for managing these valuations. The instructor proves several lemmas related to these operations to build momentum for later proofs. The lecture also introduces a simple imperative language that includes commands for assignment, sequencing, conditionals, and while loops. The instructor emphasizes the differences between this approach and previous methods, particularly in how big-step semantics is modeled. The session concludes with the development of an optimizer for the language, demonstrating how to prove its correctness through structured induction on commands.