Big-Step Semantics

The goal is to define a binary relation between configurations, which associates a configuration with its corresponding terminal one if it exists. That is, define by induction the binary relation $⟨P,s⟩{\to }^{\ast }⟨P^{\prime },s^{\prime }⟩$ such that $⟨P^{\prime },s^{\prime }⟩$ is terminal.

The usual notation for this is $⟨P,s⟩\Downarrow ⟨P^{\prime },s^{\prime }⟩$. In other words: $⟨P,s⟩\Downarrow ⟨P^{\prime },s^{\prime }⟩\text{ if }⟨P,s⟩{\to }^{\ast }⟨P^{\prime },s^{\prime }⟩$ where $⟨P^{\prime },s^{\prime }⟩$ is terminal.