읽는 순서🔗

2장 본문은 다음 순서로 읽는다.

1. Syntax.lean — §2.1 불 식과 명령의 추상 구문

2. Notation.lean — §2.1 명령을 Lean 안에서 쓰는 DSL

3. Semantics.lean — §2.2 불 식의 계산과 명령 의미의 명세

4. Domain.lean — §2.3 사슬, 프리도메인, 연속성

5. Domain/Lifting.lean·Domain/LiftingLaws.lean — §2.3 평평한 순서와 리프팅 법칙

6. Domain/FunctionSpace.lean — §2.3 상태 변환 함수들의 점별 순서와 극한

7. Fixpoint.lean — §2.4 반복 사슬과 최소 고정점 정리

8. Eval.lean·Approximation.lean·SumApproximation.lean — §2.4 의미·근사 명령·합산 계산

9. Interpreter.lean — §2.4 연료 해석기와 적합성

10. FreeVars.lean — §2.5 자유 변수 두 종류와 명제 2.6

11. Substitution.lean — §2.5 명령의 치환, 별칭, 지역 변수 이름 바꾸기

12. Sugar.lean — §2.6 for 명령과 세 가지 결함

13. Sugar2.lean — §2.6 판본 3의 정확 반복 정리

14. ArithErrors.lean — §2.7 산술 오류와 0으로 나누기

15. FullAbstraction.lean — §2.8 문맥, 관찰, 완전 추상성

16. FullAbstraction2.lean — §2.8 관찰의 선택과 세 등식

그 뒤로 Ex.lean과 Ex/ 아래에 책 연습 2.1~2.10이 있다.

전부 Reynolds/Answers/Ch02/ 아래에 있고, Reynolds/Exercises/Ch02/에는 같은 선언 순서에서 채울 자리만 sorry로 비어 있다. 이 문서는 2장 본문 전체(§2.1~§2.8)를 다룬다.