선택 심화: 의미와 자유 변수는 어떤 접기인가🔗

Reynolds §1.2 pp.10–11은 생성자마다 주어진 의미 방정식이 정수 식과 단언의 의미를 함께 유일하게 정한다고 설명한다. 앞 절의 추상적인 목표 대수에 실제 해석을 넣어 보자. 정수 식은 상태에서 정수를 얻는 함수로, 단언은 상태에서 명제를 얻는 함수로 옮긴다. 비교 연산은 정수 함수 둘을 받아 명제 함수를 만든다.

def logicEvalAlg (V : Type u) [DecidableEq V] : LogicAlg V where
  E := State V → Int
  A := State V → Prop
  num n := fun _ => n
  var x := fun σ => σ x
  eneg f := fun σ => -f σ
  ebin op f g := fun σ => op.denote (f σ) (g σ)
  tru := fun _ => True
  fls := fun _ => False
  cmp c f g := fun σ => c.denote (f σ) (g σ)
  anot p := fun σ => ¬ p σ
  abin op p q := fun σ => op.denote (p σ) (q σ)
  quant
    | .all, x, p => fun σ => ∀ n : Int, p (σ[x := n])
    | .ex, x, p => fun σ => ∃ n : Int, p (σ[x := n])

양화사의 본문은 여러 갱신 상태에서 해석된다. 따라서 본문을 접은 결과에는 상태 하나의 진릿값 대신 상태 전체를 입력받는 함수가 들어간다. Lean에서는 책의 진릿값을 Prop으로 표현한다. 예를 들어 ∃x. x = 7은 바깥 상태가 x에 어떤 값을 주더라도 참이다.

다음 한 문제는 단언의 구조적 귀납법으로 푼다. 비교 분기에서는 완성된 IntExp.eval_eq_foldE를 사용하고, 양화 분기에서는 본문에 대한 함수 등식을 쓴다. 초기성 문제 A1.3을 먼저 풀 필요는 없다.

@[exercise "심화 A1.4" 2]
theorem Assert.eval_eq_foldA {V : Type u} [DecidableEq V] (p : Assert V) :
    p.eval = (logicEvalAlg V).foldA p := byV:Type uinst✝:DecidableEq Vp:Assert V⊢ ⟦p⟧ₐ = (logicEvalAlg V).foldA p

초기성 정리에 이 목표 대수를 넣으면 의미 방정식을 만족하는 함수 쌍이 기존 해석과 같다는 귀결을 얻는다. 이 유일한 접기를 catamorphism이라고도 부른다. 아래 정리는 초기성을 이용한 제공 자료이며 별도의 채점 문제가 아니다.

theorem logicEval_unique {V : Type u} [DecidableEq V]
    (h : (IntExp V → State V → Int) × (Assert V → State V → Prop))
    (hh : (logicEvalAlg V).IsHom h) : h = (IntExp.eval, Assert.eval) := byV:Type uinst✝:DecidableEq Vh:(IntExp V → State V → ℤ) × (Assert V → State V → Prop)hh:(logicEvalAlg V).IsHom h⊢ h = (IntExp.eval, Assert.eval)

§1.4 pp.15–16의 자유 변수 방정식도 같은 방식으로 읽는다. logicFvAlg는 두 반송자를 모두 Finset V로 두고, 비교와 이항 연산에서 합집합을 취하며, 양화사에서는 결합 이름을 지운다. 이 방정식의 유일한 해석 쌍은 IntExp.fv와 Assert.fv다.

theorem logicFv_unique {V : Type u} [DecidableEq V]
    (h : (IntExp V → Finset V) × (Assert V → Finset V))
    (hh : (logicFvAlg V).IsHom h) : h = (IntExp.fv, Assert.fv) := byV:Type uinst✝:DecidableEq Vh:(IntExp V → Finset V) × (Assert V → Finset V)hh:(logicFvAlg V).IsHom h⊢ h = (IntExp.fv, Assert.fv)

자유 변수 집합은 구문을 따라 계산한다. x - x의 값은 늘 0이지만 자유 변수 집합에는 x가 남는다. 이 선택 보충은 책의 구문 지향 정의를 대수로 연결하며, 의미의 최소 의존 집합이나 α-동치까지 다루지는 않는다.