2장 단순 명령형 언어
1장에서는 모든 구문의 뜻을 구문 트리에 대한 재귀로 정의할 수 있었다. 2장의 while은
유한한 구문 트리지만 실행은 끝나지 않을 수 있다. 구문의 유한성과 실행의 유한성이 처음으로
갈라지는 자리다.
명령 하나의 뜻은 상태를 새 상태로 보내는 함수다. 다만 항상 새 상태를 얻는 것은 아니므로
결과 타입을 전용 귀납 타입 Flat으로 감싼다. Flat.none은 바닥이고
Flat.some σ는 종료 결과다. 일반 Option의 순서는 그대로 둔다.
State V → Flat (State V)
some σ'는 σ'에서 끝났다는 정보이고 none은 결과 상태를 아직 얻지 못했다는 정보다.
이 장에서는 none을 실행 오류나 비결정적 결과와 섞지 않고 비종료의 근사로만 읽는다.