자유 변수가 둘로 갈라진다🔗

FV(c)는 명령이 읽거나 쓰는 변수 전부이고, FA(c)는 대입하는 변수다.

FA ⊆ FV가 성립한다. 대입하는 변수는 당연히 관여하는 변수이기 때문이다.

구분이 값을 하는 자리는 명제 2.6(b)다. "이 명령은 그 변수를 안 건드린다"를 문장으로 만들려면 읽기와 쓰기를 갈라야 한다. §2.6의 for 제약도, §2.8의 별칭 이야기도 이 구분 위에 선다.

결합이 있는 절은 newvar 하나다. newvar v := e in c에서 v는 c에서만 묶이고 초기값 e는 범위 밖이라, e의 자유 변수는 지우지 않는다.

비종료가 있는 "같다"🔗

1장의 일치 정리는 "자유 변수 위에서 같으면 뜻이 같다" 한 줄이었다. 여기서는 결과가 Σ⊥라서 "같다"를 두 경우로 나눠 말해야 한다.

둘 다 ⊥이거나, 둘 다 상태이고 그 상태들이 다시 자유 변수 위에서 같거나. 하나만 ⊥인 경우는 거짓이다.

명제 2.6의 증명에는 두 가지 새 도구가 든다.

진술 강화

FV(c) 위에서의 일치만으로는 seq 절이 돌지 않는다. c₀를 지난 상태들은 FV(c₀) 위에서만 일치한다고 알게 되는데, c₁은 그 밖의 변수도 읽기 때문이다. 진술을 "임의의 S ⊇ FV(c) 위에서"로 올리면 그 간극이 사라진다. 1장에서 상태를 ∀로 묶어야 했던 것과 같은 종류의 일반화이고, 이번에는 집합을 묶는다.

Scott 귀납법

while 절은 fix에 대한 주장이므로 성질이 극한을 통과해야 한다. AgreeOn이 허용 가능하다는 것은 Σ⊥의 평평함에서 나온다. 두 극한이 각각 어느 단계에서 이미 결정되어 있으므로, 극한끼리의 주장이 한 단계끼리의 주장으로 내려온다.

코드에서는 Comm.coincidence_general이 명제 2.6(a)이고 Comm.eval_agree_outside_fa가 2.6(b)다.

명령의 치환은 변수를 변수로만 보낸다🔗

1장의 치환 사상은 ⟨var⟩ → ⟨intexp⟩였다. 변수 자리에 임의의 식을 넣을 수 있었다. 명령에서는 그것이 불가능하다. x := e의 왼쪽과 newvar v := e in c의 결합자는 변수 자리라서, x를 x + 1로 보내는 치환은 구문에 없는 것을 만들어 낸다.

형식화에서는 이 제약이 저절로 지켜진다. 타입이 V → V라서 변수 아닌 것을 넣는 치환은 아예 적을 수 없다.

newvar 절은 1장의 양화사 절과 같은 수법이다. 결합자를 새 이름으로 바꾸고, 치환 사상 쪽에서도 그 변수를 새 이름으로 보내도록 고친다.

치환 정리에 단사 가정이 붙는다🔗

원래 프로그램의 w를 치환된 프로그램의 δ w와 비교해야 하므로, 사상을 사이에 둔 일치 관계가 필요하다.

명제 2.7(Comm.substitution_general)에는 가정이 둘 붙는다.

S ⊇ FV(c)인 변수 집합

책의 명제 2.7도 이 범위로 진술한다(p. 43). 여기서는 유한 집합으로 표현한다. seq 절에서 c₀의 귀납 가설이 주는 일치가 FV(c₀) 위뿐이면 c₁이 읽는 나머지를 잇지 못한다. 반대로 모든 변수에서의 단사만 다루면, newvar에서 갱신한 치환이 전체 변수 집합에서 단사라는 보장이 없다. 책 p. 44는 이 두 특수 경우를 직접 귀납으로 증명할 수 없는 이유를 설명한다.

S 위에서의 단사

1장에는 없던 가정이다. 서로 다른 두 변수가 같은 변수로 가면 원래 프로그램에서 서로 다른 저장 공간이던 것이 치환 후에는 같은 공간이 된다.

while 절은 명제 2.6(a)보다 한 단계 어렵다. 왼쪽과 오른쪽이 서로 다른 연산자의 최소 고정점이라 Scott 귀납법 하나로는 안 되고, 두 반복 사슬을 나란히 세워 단계별로 관계를 증명한 뒤 극한에 올린다.

별칭이 정리를 깨뜨린다🔗

단사 가정이 장식이 아님을 확인한다. 임시 변수를 거쳐 두 변수를 맞바꾸는 프로그램을 놓고 본다.

여기에 t와 y를 같은 변수로 보내는 이름 바꾸기를 걸면 맞바꾸기가 망가진다.