선택 심화: 치환 모나드와 α-동치🔗

범주론 렌즈에서 짚었듯, §1.4의 치환 p /ₛ δ는 변수 타입을 바꾸지 않는 특수한 경우다. Depth/TermMonad.lean은 변수 잎을 다른 변수 타입의 식으로 바꿔 끼우는 일반형 bind를 둔다.

def IntExp.bind {V W : Type u} (e : IntExp V) (f : V → IntExp W) : IntExp W :=
  match e with
  | .num n        => .num n
  | .var v        => f v
  | .neg e        => .neg (e.bind f)
  | .bin op e₀ e₁ => .bin op (e₀.bind f) (e₁.bind f)

좌단위·우단위 법칙 둘이 등식으로 성립한다. 좌단위는 정의를 펼치면 바로 나온다.

/-- 좌단위. `pure v >>= f = f v`. `IntExp.bind`의 `var` 절이 곧 이 등식이다. -/
theorem IntExp.bind_pure_left {V W : Type u} (v : V) (f : V → IntExp W) :
    (IntExp.var v).bind f = f v := rfl

우단위(IntExp.bind_pure_right : e.bind IntExp.var = e)는 Reynolds가 명제 1.2(b)에서 "c_var가 항등 치환으로 작동한다"고 쓴 §1의 결과(subst_pure_right)를 변수 타입을 바꾸는 쪽으로 일반화한 것이다. 증명은 e에 대한 구조적 귀납법으로, bind_pure_left와 같은 모양의 케이스 분석이다.

연습 1.7(a)가 묻는 치환 두 번의 합성은 모나드의 결합법칙이다. δ로 옮기고 다시 δ'로 옮기는 것을 한 번에 하는 합친 치환이 Kleisli 합성(Subst.kleisli, >=>ₑ)이다.

def Subst.kleisli {V W X : Type u} (δ : V → IntExp W) (δ' : W → IntExp X) : V → IntExp X :=
  fun v => (δ v).bind δ'

@[inherit_doc Subst.kleisli] scoped infixr:90 " >=>ₑ " => Subst.kleisli

결합자가 없는 정수 식에서는 이 결합법칙이 등식으로 성립한다. "심화 A2.1"(§1, 변수 타입을 고정한 판)을 먼저 풀어 본 사람은 var 케이스가 rfl인 이유가 여기서도 그대로임을 알아챈다 — 심화 A2.2는 그 결과를 쓰지 않고 독립적으로 다시 증명한다.

@[exercise "심화 A2.2" 2]
theorem IntExp.bind_assoc {V W X : Type u} (e : IntExp V) (δ : V → IntExp W) (δ' : W → IntExp X) :
    (e.bind δ).bind δ' = e.bind (δ >=>ₑ δ')

∀v가 있는 단언에서는 사정이 다르다. 포획을 피하려고 고르는 새 결합 변수가 치환을 어떻게 나누느냐에 따라 달라질 수 있어서, 결합법칙이 구문의 등식으로는 깨진다. 심화 A2.3은 그 구체적인 반례를 만드는 연습이다.

@[exercise "심화 A2.3" 2]
theorem subst_assoc_assert_not_eq :
    ∃ (p : Assert String) (δ δ' : Subst String),
      (p /ₛ δ) /ₛ δ' ≠ p /ₛ (fun w => (δ w) /ₑ δ')

구문으로는 달라도 뜻은 같다 — 결합 변수 이름의 차이만 있을 뿐이다. 그 이름 차이를 무시하는 관계가 α-동치(=α)다. cmp 절은 정수 식 쪽에 결합자가 없으므로 두 비교식이 그대로 같아야 한다고 요구하고, quant 절만 결합 변수 이름 차이를 허용한다.

inductive Assert.AlphaEq [DecidableEq V] [HasFresh V] : Assert V → Assert V → Prop
  | tru : Assert.AlphaEq .tru .tru
  | fls : Assert.AlphaEq .fls .fls
  | cmp (c : Cmp) (e₀ e₁ : IntExp V) : Assert.AlphaEq (.cmp c e₀ e₁) (.cmp c e₀ e₁)
  | not {p p' : Assert V} : Assert.AlphaEq p p' → Assert.AlphaEq (.not p) (.not p')
  | bin (op : LogOp) {p p' q q' : Assert V} :
      Assert.AlphaEq p p' → Assert.AlphaEq q q' → Assert.AlphaEq (.bin op p q) (.bin op p' q')
  | quant (qt : Quant) (v v' : V) (p p' : Assert V) (w : V)
      (hw : w ∉ p.fv.erase v ∪ p'.fv.erase v') :
      Assert.AlphaEq (p /[v := .var w]) (p' /[v' := .var w]) →
      Assert.AlphaEq (.quant qt v p) (.quant qt v' p')

심화 A2.4는 α-동치가 뜻을 보존한다는 것 — 명제 1.5(이름 바꾸기 정리)의 구문적 일반화다. 명제 1.5는 결합 변수 하나를 그 자리에서 새 이름으로 바꾼 결과의 뜻이 같다고 말하고, =α는 그 바꿔치기를 구문의 어느 깊이에서든 몇 번이든 허용한다. 명제 1.5 자체 (renaming_assert)는 그 증명이 치환 정리(Prop 1.3-assert, 채점)를 직접 쓰므로, 연습 독립성을 지키려고 가설 hrename으로 받는다 — 실제로 쓸 때는 renaming_assert를 그 자리에 넘긴다.

@[exercise "심화 A2.4" 3]
theorem Assert.AlphaEq.sound [HasFresh V]
    (hrename : ∀ (qt : Quant) (v₀ vnew : V) (body : Assert V), vnew ∉ body.fv.erase v₀ →
      ∀ σ : State V,
        ⟦Assert.quant qt vnew (body /[v₀ := IntExp.var vnew] )⟧ₐ σ ↔ ⟦Assert.quant qt v₀ body⟧ₐ σ)
    {p p' : Assert V} (h : p =α p') :
    Equivalent p p'

2장의 리프팅 모나드 Σ⊥ = Flat (State V)(Ch02/Semantics.lean의 SigmaBot)도 같은 모양의 구조를 갖는다. pure에 해당하는 것이 Flat.some, Kleisli 확장에 해당하는 것이 liftBot이고, liftBot_eq_bind가 그 liftBot이 정확히 Flat.bind와 같음을 보여 준다. IntExp의 bind/Subst.kleisli와 Σ⊥의 Flat.bind/liftBot은 "항 모나드"와 "리프팅 모나드"라는 서로 다른 계산 효과가 공유하는 같은 뼈대다.