Theorem. Adequacy (充分性定理) [math-CFN7]

If $M$ is closed term of ground type and $\mathcal{C}\llbracket M \rrbracket = \mathcal{C}\llbracket V \rrbracket$ for a value $V$, then $M \Downarrow V$.

對一個形式系統來說，需要證明一個假定的 model 確實能表現系統的特徵，所以才需要證明這個定理。參考 computational adequacy