§1.4 치환🔗

정의가 길어지는 곳은 여기 하나다. 앞의 의미 함수들은 절마다 한 줄이었는데, 치환은 양화사 절에서 새 이름을 골라야 한다.

/--
`p /ₛ δ` — 단언에 대한 동시 치환.

양화사 절만 특별하다.

```
(∀v. p) /ₛ δ = ∀ vnew. (p /ₛ δ[v := var vnew])
```

`v`를 새 이름 `vnew`로 바꾸고, 치환 사상 쪽에서도 `v`를 `var vnew`로 보내도록 고친다.
`vnew`는 `newBinder`가 골라 주므로, 실제로 본문에 자유롭게 나타나 치환되는
`w ∈ p.fv.erase v`에 대해 `δ w`의 자유 변수와 겹치지 않는다.

이 정의가 내놓는 것은 신선한 이름 선택까지 기록한 원시 이름 구문이다. 따라서 서로 다른
신선 이름 선택은 구문 등식으로 같지 않을 수 있지만, 명제 1.5가 그 이름 차이가 의미를
바꾸지 않음을 보인다.

**정지성**: 재귀 호출이 `p` 라는 진부분항에 대해 일어나므로 구조적 재귀다.
"먼저 이름을 바꾸고 다시 치환한다"는 이름 있는 단일 치환의 직접 정의에는 별도의 정지성
증명이 필요하다. Reynolds의 동시 치환 정의는 그 추가 증명 없이 구조적 재귀로 받아들여진다.
-/
def Assert.subst [HasFresh V] : Assert V → Subst V → Assert V
  | .tru,          _ => .tru
  | .fls,          _ => .fls
  | .cmp c e₀ e₁,  δ => .cmp c (e₀ /ₑ δ) (e₁ /ₑ δ)
  | .not p,        δ => .not (p.subst δ)
  | .bin op p q,   δ => .bin op (p.subst δ) (q.subst δ)
  | .quant q v p,  δ =>
      .quant q (newBinder p v δ) (p.subst (Function.update δ v (.var (newBinder p v δ))))

양화사 절만 특별하다. δ가 데려오는 자유 변수가 v에 잡히면(포획, capture) 뜻이 달라지므로, 결합 변수를 안전한 이름으로 미리 바꾼다.

이 정의 위에서 명제 1.2부터 1.5까지가 이어진다. 치환 정리(명제 1.3)가 그중 중심이고, 치환한 구문을 평가한 결과와 치환 항들의 값을 상태에 넣은 뒤 원래 구문을 평가한 결과가 같다는 것을 말한다.

범주론 렌즈 — 치환은 모나드의 bind다🔗

p /ₛ δ를 변수 타입을 바꾸는 쪽으로 일반화하면(Depth/TermMonad.lean의 IntExp.bind) 모나드의 bind가 된다. 연습 1.7이 묻는 치환 두 번의 합성은 그 결합법칙이고, 결합자가 없는 정수 식에서는 등식으로 성립한다(Subst.kleisli). ∀v가 있는 단언에서는 포획을 피하려고 고르는 새 이름이 매번 달라질 수 있어서, 등식 대신 α-동치(=α)까지만 성립한다. 선택 심화: 치환 모나드와 α-동치에서 그 반례와 =α를 본다.

곁가지 — 이름을 어떻게 다룰 것인가🔗

Reynolds는 §1.4 끝에서 결합 변수 이름을 구체 표현의 일부로 보내고, α-동치인 표기들을 하나의 추상 구를 나타내는 표현으로 보는 방향을 고차 추상 구문(higher-order abstract syntax)과 연결한다. 현대 용례에서 HOAS는 보통 메타언어의 함수로 객체언어의 결합을 표현하는 구체적인 기법을 가리킨다. 이름 차이를 추상 구문의 동일성에서 제외한다는 원칙과 그 원칙을 구현하는 특정 표현법을 구분해서 읽어야 한다.

대표적인 표현법은 다음과 같다. 어느 방법도 결합의 증명 부담을 없애지는 않고, 부담이 나타나는 정의와 보조정리를 바꾼다.

이름 있는(named) — 우리가 고른 방식: 결합 변수를 이름 그대로 둔다. 치환할 때 포획을 피해야 하며, Substitution.lean의 captureSet과 newBinder가 그 일을 맡는다.
de Bruijn 색인: 결합 변수를 번호로 바꾼다. 항을 다른 자리로 옮길 때마다 번호를 미는 연산(shifting)이 필요하다.
locally nameless: 묶인 변수는 번호로, 자유로운 변수는 이름으로 둔다. 두 표현 사이를 여닫는 연산이 필요하다.
HOAS: 묶인 변수를 메타언어 함수의 인자로 표현한다. α-변환과 포획 회피 치환 일부를 메타언어에 맡길 수 있지만, 임의의 메타언어 함수를 객체 구문으로 받아들이지 않도록 재귀·양성성 원리를 설계해야 한다.

우리가 첫 번째를 고른 것은 Reynolds를 따라간 것이다. 다른 방식을 골랐다면 newBinder가 사라지는 대신 다른 코드가 생긴다.

CSlib 의존성 소스에는 locally nameless 구현이 포함돼 있다.

.lake/packages/cslib/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean

우리의 Assert.subst와 나란히 열어 놓고 "포획 회피가 어디로 갔는지"를 찾아보는 것이 좋은 스터디 토론거리다. 묶인 변수에 이름이 없으므로 결합 변수의 이름을 바꾸다가 생기던 포획 문제는 사라진다. 대신 open과 close가 잘 맞물리는지, 그리고 항에 닫히지 않은 de Bruijn 색인이 없는지, 곧 국소적으로 닫혀 있는지(locally closed) 증명해야 한다.

곁가지 — 이름 바꾸기가 깨지는 언어🔗

명제 1.5 는 결합 변수의 이름이 뜻에 영향을 주지 않는다고 말한다. Reynolds는 바로 뒤에서 이 성질이 잘 작동하는 결합을 가진 모든 언어에 적용되지만, 일부 잘 알려진 언어는 예외라고 덧붙인다. §11.7의 동적 결합(dynamic binding) 예고다.

정적 결합(static binding)에서 자유 변수는 그 변수가 쓰인 자리를 둘러싼 코드에서 뜻을 얻는다. 그래서 결합 변수의 이름을 바꿔도 어느 결합자에 매이는지가 변하지 않는다.

동적 결합에서는 호출한 쪽에서 뜻을 얻는다. 그러면 이름이 실행 시점에 의미를 갖게 되고, 결합 변수를 다른 이름으로 바꾸는 순간 어떤 호출자와 만나는지가 달라진다. 명제 1.5 의 결론이 성립하지 않는다.

이 장에서 예고만 하고 넘어가는 이유는, 그것을 말하려면 프로시저와 호출 규약이 먼저 있어야 하기 때문이다. 1장에는 호출이 없다.

따라서 α-변환의 의미 보존은 모든 이름 붙은 구문에서 자동으로 성립하는 사실이 아니다. 1장의 정적 결합 의미와 포획 회피 치환이 그 정리의 가정을 충족한다.