1장에서 2장으로 넘어가는 한 줄🔗

1장의 의미 함수는 구문 구조를 그대로 따라가면 끝났다. while b do c의 뜻을 같은 방식으로 쓰면 우변에 while b do c의 뜻이 다시 나타난다.

⟦while b do c⟧ σ
  = if ⟦b⟧ σ then Flat.bind (⟦c⟧ σ) ⟦while b do c⟧ else Flat.some σ

이 식은 반복문의 뜻이 만족해야 할 조건은 말하지만, 구문 트리의 더 작은 부분으로 내려가는 재귀 정의는 아니다. 실제로 이 조건을 만족하는 함수가 둘 이상 생긴다. 2장의 §2.2~§2.4는 그 비유일성에서 출발해, 정보 순서를 만들고, 유한 근사의 극한을 택해, 실행 가능한 해석기와 같은 종료 결과를 내는 뜻을 얻는 과정이다.