이 장에서 배우는 것🔗

• 추상 구문(abstract syntax) — 언어를 문자열이 아니라 트리로 정의하는 것, 그리고 그때 필요한 세 조건

• 표시적 의미론(denotational semantics) — 구문의 각 절에 뜻을 주는 구문 지향 방정식

• 타당성과 추론 — 뜻으로 정의한 참과 규칙으로 유도한 참, 그리고 둘을 잇는 건전성(soundness)

• 결합과 치환 — 양화사(quantifier)가 들어오면서 생기는 자유 변수(free variable)와 속박 변수(bound variable)의 구분, 그리고 변수 포획(capture)

특히 §1.4에서는 정의가 타입에 맞는 것만으로 충분하지 않다. 자유 변수를 빠뜨리거나 치환에서 포획을 허용하면 함수는 실행되지만 일치 정리와 치환 정리가 깨진다. 이 저장소는 정의의 타당성을 그 정리와 반례로 확인한다.