선택 심화: 합성성과 합동
범주론 렌즈에서 본 것처럼, 구문 지향적으로 정의한 의미 함수는 자동으로 합성적(compositional)이다. Reynolds §1.2 p.11은 이 귀결을 이렇게 적는다.
"A semantics is said to be compositional when the meaning of each phrase does not depend on any property of its immediate subphrases except the meanings of these subphrases. … It implies that, in any phrase, one can replace an occurrence of a subphrase by another phrase with the same meaning, without changing the meaning of the enclosing phrase."
"바꿔 끼워도 전체 뜻이 바뀌지 않는다"를 문맥마다 따로 보이는 대신, Validity.lean은
단언의 생성자 각각이 Equivalent를 보존한다는 합동(congruence) 보조정리로 한 번에 준다.
부정의 합동이 심화 A1.8 연습이다.
@[exercise "심화 A1.8" 1]
theorem Equivalent.not_congr {p p' : Assert V} (h : Equivalent p p') :
Equivalent (.not p) (.not p')
이항 논리 연산의 합동(bin_congr)도 같은 패턴(Assert.eval을 펼치고 가정을 꽂는다)의
완성본이다. 비교식의 두 자리는 단언이 아니라 정수 식이므로, 합동의 가정도 다른 모양을
받는다 — 합성성이 단언 생성자에만 있는 특별한 성질이 아니라 정수 식과 단언을 넘나드는
경계에서도 같은 모양으로 성립한다는 뜻이다.
theorem Equivalent.cmp_congr {c : Cmp} {e₀ e₀' e₁ e₁' : IntExp V}
(h₀ : ∀ σ, e₀.eval σ = e₀'.eval σ) (h₁ : ∀ σ, e₁.eval σ = e₁'.eval σ) :
Equivalent (.cmp c e₀ e₁) (.cmp c e₀' e₁') := V:Type uinst✝:DecidableEq Vc:Cmpe₀:IntExp Ve₀':IntExp Ve₁:IntExp Ve₁':IntExp Vh₀:∀ (σ : State V), ⟦e₀⟧ₑ σ = ⟦e₀'⟧ₑ σh₁:∀ (σ : State V), ⟦e₁⟧ₑ σ = ⟦e₁'⟧ₑ σ⊢ Equivalent (Assert.cmp c e₀ e₁) (Assert.cmp c e₀' e₁')
V:Type uinst✝:DecidableEq Vc:Cmpe₀:IntExp Ve₀':IntExp Ve₁:IntExp Ve₁':IntExp Vh₀:∀ (σ : State V), ⟦e₀⟧ₑ σ = ⟦e₀'⟧ₑ σh₁:∀ (σ : State V), ⟦e₁⟧ₑ σ = ⟦e₁'⟧ₑ σσ:State V⊢ ⟦Assert.cmp c e₀ e₁⟧ₐ σ ↔ ⟦Assert.cmp c e₀' e₁'⟧ₐ σ; All goals completed! 🐙
양화의 합동은 결합 변수 v를 그대로 두고 본문만 바꾼다.
theorem Equivalent.quant_congr {qt : Quant} (v : V) {p p' : Assert V}
(h : Equivalent p p') : Equivalent (.quant qt v p) (.quant qt v p') := V:Type uinst✝:DecidableEq Vqt:Quantv:Vp:Assert Vp':Assert Vh:Equivalent p p'⊢ Equivalent (Assert.quant qt v p) (Assert.quant qt v p')
V:Type uinst✝:DecidableEq Vqt:Quantv:Vp:Assert Vp':Assert Vh:Equivalent p p'σ:State V⊢ ⟦Assert.quant qt v p⟧ₐ σ ↔ ⟦Assert.quant qt v p'⟧ₐ σ
V:Type uinst✝:DecidableEq Vqt:Quantv:Vp:Assert Vp':Assert Vh:Equivalent p p'σ:State Vkey:∀ (n : ℤ), ⟦p⟧ₐ σ[v := n] ↔ ⟦p'⟧ₐ σ[v := n]⊢ ⟦Assert.quant qt v p⟧ₐ σ ↔ ⟦Assert.quant qt v p'⟧ₐ σ
V:Type uinst✝:DecidableEq Vv:Vp:Assert Vp':Assert Vh:Equivalent p p'σ:State Vkey:∀ (n : ℤ), ⟦p⟧ₐ σ[v := n] ↔ ⟦p'⟧ₐ σ[v := n]⊢ ⟦Assert.quant Quant.all v p⟧ₐ σ ↔ ⟦Assert.quant Quant.all v p'⟧ₐ σV:Type uinst✝:DecidableEq Vv:Vp:Assert Vp':Assert Vh:Equivalent p p'σ:State Vkey:∀ (n : ℤ), ⟦p⟧ₐ σ[v := n] ↔ ⟦p'⟧ₐ σ[v := n]⊢ ⟦Assert.quant Quant.ex v p⟧ₐ σ ↔ ⟦Assert.quant Quant.ex v p'⟧ₐ σ
V:Type uinst✝:DecidableEq Vv:Vp:Assert Vp':Assert Vh:Equivalent p p'σ:State Vkey:∀ (n : ℤ), ⟦p⟧ₐ σ[v := n] ↔ ⟦p'⟧ₐ σ[v := n]⊢ ⟦Assert.quant Quant.all v p⟧ₐ σ ↔ ⟦Assert.quant Quant.all v p'⟧ₐ σ All goals completed! 🐙
V:Type uinst✝:DecidableEq Vv:Vp:Assert Vp':Assert Vh:Equivalent p p'σ:State Vkey:∀ (n : ℤ), ⟦p⟧ₐ σ[v := n] ↔ ⟦p'⟧ₐ σ[v := n]⊢ ⟦Assert.quant Quant.ex v p⟧ₐ σ ↔ ⟦Assert.quant Quant.ex v p'⟧ₐ σ All goals completed! 🐙Reynolds가 §1.4 p.21에서 이름 바꾸기 정리(명제 1.5) 바로 뒤에 다시 꺼내는 문장은 결합 변수 자체를 바꾸는 경우까지 포함한다.
"From this proposition and the compositional nature of our semantics, it is clear that, in any context, one can replace an occurrence of a subphrase of the form ∀v. q by ∀vnew. (q/v → vnew), without changing the meaning of the context."
이름 바꾸기 정리의 renaming_assert는 "그 양화 구 하나"의
뜻이 같다는 것만 준다. "어느 문맥에 넣어도" 쪽은 생성자별 합동(not_congr, bin_congr,
quant_congr)을 문맥의 모양에 대한 귀납으로 이어서 얻는다. α-변환이 임의의 문맥에서
적용된다는 것은 이름 바꾸기 정리와 합동을 조합한 결과다.