Natural Semantic

logic

Definition

Natural Semantics

Natural semantics (also known as big-step semantics) describes the overall result of executing a statement in its entirety, rather than the individual steps. A transition is written as:

$$⟨\Pi ,\sigma ⟩\Downarrow {\sigma }^{\prime }$$

This indicates that executing the program fragment $\Pi$ starting in state $\sigma \in \mathcal{S}$ results in the final state ${\sigma }^{\prime }\in \mathcal{S}$.

Characteristics

• Abstraction: Natural semantics ignores intermediate states, focusing solely on the relationship between initial and final values.
• Divergence: It is difficult to distinguish between non-termination and a program being “stuck” (e.g., a type error), as there is no final state ${\sigma }^{\prime }$ to point to in either case.
• Proof Structure: Proofs in big-step semantics typically follow the structure of the syntax tree (induction on the program structure).