정의 선택과 정리의 성립🔗

여기까지는 정의가 주어지고 그 정의에 대한 정리를 증명해 왔다. 그러면 "이 정의가 맞다"를 받아들이고 시작하게 된다. 그런데 Reynolds가 §1.4에서 공들이는 것은 정리 증명이 아니라 정의를 고르는 일 이다. 포획 회피가 왜 필요한지, 자유 변수 함수가 뜻에 영향을 줄 가능성이 있는 변수를 빠뜨리지 않는지가 그 절의 내용이다. 그 집합이 항상 최소인 것은 아니다. x - x에는 x가 자유롭게 나타나지만 값은 어느 상태에서나 0이다.

Design.lean은 방향을 뒤집어, 그럴듯하지만 틀린 정의 셋을 주고 각각이 무엇을 깨뜨리는지 증명하게 한다.

• 자유 변수에서 이항 논리 연산의 오른쪽을 빠뜨리면 — 일치 정리 가 깨진다

• 의미에서 양화사가 상태를 갱신하지 않으면 — 일치 정리 가 깨진다

• 치환에서 결합 변수를 그대로 두면 — 치환 정리 가 깨진다

앞의 둘은 같은 정리를 깨뜨리지만 이유는 반대다. 하나는 fv가 너무 작고, 다른 하나는 의미가 묶인 변수에 여전히 의존한다. 두 반례를 나란히 보면 일치 정리가 무엇을 주장하는지가 분명해진다 — fv와 eval이 서로 맞물려야 하고, 어느 쪽을 건드려도 맞물림이 풀린다.

세 번째가 §1.4의 본론이다. ∃y. x < y는 "x보다 큰 수가 있다"이므로 어떤 상태에서도 참인데, 포획을 막지 않은 치환으로 x를 y로 바꾸면 ∃y. y < y가 되어 어떤 상태에서도 거짓이 된다. 들어온 y가 자유 변수여야 하는데 양화사에 잡힌 것이다.

한 가지는 이 방식으로 바로 보이기 어렵다. 동시 치환을 기본으로 두는 이유다. 한 변수씩 치환하는 직접 방정식은 양화사 절에서 구조적 재귀가 아니므로 Lean이 그대로는 받아들이지 않는다. 구의 크기가 줄어든다는 보조정리와 정초 재귀(well-founded recursion)를 쓰면 정의할 수 있지만, 동시 치환은 그 추가 장치 없이 진부분항에 대한 구조적 재귀로 끝난다. Design.lean 마지막 절에 산문으로 적어 두었다.