1장 술어 논리🔗

Reynolds 1장은 익숙한 술어 논리(predicate logic)를 작은 프로그래밍 언어처럼 다룬다. 구문을 데이터로 만들고, 각 생성자에 의미 방정식을 주고, 그 정의에서 성질을 증명한다. 2장 이후에도 대상 언어는 바뀌지만 이 작업 순서는 계속 남는다.

이 장 문서는 소스 파일의 순서를 따라가되, 코드만으로는 드러나지 않는 경계도 함께 적는다. 표준 정수 해석의 완전성과 일차 논리의 완전성은 무엇이 다른지, 결합 변수의 표현을 바꾸면 복잡성이 어디로 이동하는지, 동적 결합에서는 왜 이름 바꾸기가 안전하지 않은지가 그 예다.

1. 이 장에서 배우는 것
2. 읽는 순서
3. §1.1 추상 구문
4. §1.2 표시적 의미론
5. §1.3 타당성과 추론
6. §1.4 자유 변수와 일치 정리
7. §1.4 치환
8. 정의 선택과 정리의 성립
9. 연습 1.5 · 1.6 — 정수 식의 결합자
10. 직접 해 보기
11. 연습 1.1–1.3 — 단언과 구문 세계 만들기
12. 연습 1.4 — 치환 결과를 직접 쓰기
13. 연습문제
14. 선택 심화: 책 식 (1.2) — 깊이별 구성
15. 선택 심화: 초기성이 구조적 귀납을 돌려준다
16. 선택 심화: 초기성이 Lambek 보조정리를 돌려준다
17. 선택 심화: 정수 식과 단언을 함께 접기
18. 선택 심화: 의미와 자유 변수는 어떤 접기인가
19. 선택 심화: 같은 초기성을 Mathlib으로 읽기
20. 선택 심화: 합성성과 합동
21. 선택 심화: 치환 모나드와 α-동치
22. 더 읽을거리