이 장에서 배우는 것🔗

• 부분 함수(partial function) — 끝나지 않을 수 있는 명령을 State V → Flat (State V)라는 전함수로 표현하는 방법

• 풀기 방정식(unwinding equation) — 반복문을 한 번 펼친 방정식과, 그 방정식만으로는 뜻이 유일해지지 않는 이유

• 도메인 이론(domain theory) — 계산의 유한 근사를 정보 순서로 비교하고 사슬의 극한으로 합치는 방법

• 최소 고정점(least fixed point) — 여러 방정식의 해 중 유한 근사에서 시작하는 해를 고르는 원리

• 적합성(adequacy) — 증명용 표시적 의미 Comm.eval과 실행용 연료 해석기 Comm.run이 같은 종료 결과를 낸다는 정리

이 용어들은 서로 따로 놓인 정의가 아니다. while의 뜻을 정하려다 생긴 한 문제를 차례로 풀면서 필요해진다.