Jan Hoffmann, Big-Step Operational Semantics and Divergence
In its classic formulation, big-step operational semantics does not
formalize evaluations that diverge. This is problematic if one
intends to proof statements for both terminating and non-terminating
evaluations of programs.
We present three different big-step semantics for the lambda
calculus to illustrate how big-step semantics can be used to
formalize diverging computations. The first (following Cousot et
al.) uses additional coinductive rules, the second (following Leroy)
interprets the usual rules coinductively, and the third adds
additional inductive rules.
To motivate the inductive approach we discuss the soundness proof of a
static analysis that computes resource bounds for functional programs.