재작성 규칙

재작성 규칙 (Rewriting)

재작성 규칙(rewrite rules)은 Agda의 평가 관계를 새로운 계산 규칙으로 확장할 수 있게 해줘요.

규칙은 --confluence-check가 활성화되어 있으면 Agda.Builtin.Equality와 함께 사용해도 안전해요. 정합(합류)적이지만 종료하지 않는 재작성 규칙은, 종료하지 않는 함수와 달리 무정합성(consistency)을 깨뜨리지 않아요. 이러한 결과는 Cockx, Tabareau, Winterhalter가 증명했는데, 그 진술은 해당 논문의 3절을 참조하세요.

참고: 이 페이지는 --rewriting 옵션과 관련된 REWRITE 빌트인에 관한 내용이에요. 대신 rewrite 구문에 대한 문서를 찾고 있다면, with 추상화 페이지의 Rewrite 섹션을 참조하세요.

예제로 보는 재작성 규칙 (Rewrite rules by example)

재작성 규칙을 활성화하려면 --rewriting 플래그로 Agda를 실행하고 모듈 Agda.Builtin.Equality와 Agda.Builtin.Equality.Rewrite를 임포트해야 해요:

{-# OPTIONS --rewriting #-}

module language.rewriting where

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

겹치는 패턴 매칭 (Overlapping pattern matching)

재작성 규칙이 Agda를 처음 접하는 거의 모든 사람이 겪는 문제를 해결할 수 있는 예부터 보자. 이 문제는 보통 0 + m은 m으로 계산되지만 m + 0은 그렇지 않은 이유(비슷하게 (suc m) + n은 suc (m + n)으로 계산되지만 m + (suc n)은 그렇지 않은 이유)에 대한 질문으로 나타나. 이 문제는 예를 들어 _+_의 교환법칙을 증명하려 할 때 그대로 드러나:

+comm : m + n ≡ n + m
+comm {m = zero}  = refl
+comm {m = suc m} = cong suc (+comm {m = m})

여기서 Agda는 n != n + zero of type Nat이라며 불평해. 이 문제를 푸는 일반적인 방법은 방정식 m + 0 ≡ m과 m + (suc n) ≡ suc (m + n)을 증명하고 주 증명에서 명시적 rewrite 문장을 사용하는 것이야 (참고: Agda의 rewrite 키워드는 REWRITE 프래그마로 추가하는 재작성 규칙과 혼동해서는 안 돼).

재작성 규칙을 사용하면 우리 논문의 해법을 시뮬레이션할 수 있어. 먼저, 우리가 원하는 방정식이 명제적 동등성으로 성립함을 증명해야 해:

+zero : m + zero ≡ m
+zero {m = zero}  = refl
+zero {m = suc m} = cong suc +zero

+suc : m + (suc n) ≡ suc (m + n)
+suc {m = zero}  = refl
+suc {m = suc m} = cong suc +suc

다음으로 REWRITE 프래그마로 그 동등성들을 재작성 규칙으로 표시해:

{-# REWRITE +zero +suc #-}

이제 교환법칙 증명이 우리가 앞서 쓴 것과 정확히 같이 작동해:

+comm : m + n ≡ n + m
+comm {m = zero}  = refl
+comm {m = suc m} = cong suc (+comm {m = m})

재작성 규칙 없이는 이 증명을 끝낼 방법이 없다는 점에 주목해: _+_가 첫 번째와 두 번째 인자 모두에 대해 계산되는 것이 본질적으로 필요하지만, Agda의 일반적인 패턴 매칭으로는 _+_를 그런 방식으로 정의할 방법이 없어.

더 많은 예제 (Additional examples)

추가적인 재작성 규칙 사용 예는 Jesper Cockx의 블로그 글에서 찾을 수 있어.

primRewriteNoMatch로 재작성 규칙 매칭 제어하기 (Controlling rewrite rule matching with primRewriteNoMatch)

재작성 규칙 매칭은 패턴 매칭 정의를 축약(reduce)하지 않아. 이 때문에 겉보기에 무해한 재작성 규칙이 비-합류적(non-confluent)일 수 있어.

예를 들어, 벡터 연결의 결합법칙(그 자체가 덧셈의 결합법칙에 의존함)에 대한 재작성 규칙을 생각해 보자:

_++_ : Vec A n → Vec A m → Vec A (n + m)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

++-assoc : {xs : Vec A n} {ys : Vec A m} {zs : Vec A l}
         → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc {xs = []}     = refl
++-assoc {xs = x ∷ xs} = cong (x ∷_) (++-assoc {xs = xs})

불행히도 첫 번째 벡터의 길이를 0으로 특수화하면 ++-assoc 재작성 규칙이 올바르게 적용되지 않아.

{-# REWRITE ++-assoc #-}

++-assoc-fail : {xs : Vec A zero} {ys : Vec A m} {zs : Vec A l}
              → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc-fail = refl -- error: [UnequalTerms]
                     -- The terms
                     --   _++_ {n = m} (xs ++ ys) zs
                     -- and
                     --   _++_ {n = zero} xs (ys ++ zs)
                     -- are not equal at type Vec A (m + l)

문제는 ++-assoc의 좌변에 있는 바깥쪽 _++_가 암시적 길이 인자 {n = n + m}을 받는데, 우리의 특수한 경우에 n은 0이라서 그 암시적 인자가 그냥 {n = m}으로 축약된다는 것이야. Agda는 재작성 규칙 매칭 중에 패턴 매칭 정의를 축약하지 않으므로, m을 n + m에 매칭하는 데 실패하고 재작성이 적용되지 않아.

primRewriteNoMatch 원시(primitive, Agda.Builtin.Equality.Rewrite로 내보내짐)는 이 제한을 수동으로 우회할 수 있게 해줘. 재작성 규칙 좌변의 부분식을 이 원시로 감싸면, Agda에게 그 부분식에 대해서는 엄격하게 매칭하지 말라고(재작성 규칙 LHS의 나머지를 매칭하는 데 성공한 뒤에만 변환(conversion)을 확인하라고) 지시하는 거야.

primRewriteNoMatch로 감싼 부분식에 자유롭게 나타나는 모든 변수는 좌변의 다른 어딘가에 바인딩되어야 해.

벡터 연결 결합법칙 재작성 규칙의 좌변에 있는 바깥쪽 _++_의 암시적 길이 인자를 primRewriteNoMatch로 감싸면 재작성 규칙이 올바르게 작동한다는 것을 알 수 있어:

++-assoc' : {xs : Vec A n} {ys : Vec A m} {zs : Vec A l}
          → _++_ {n = primRewriteNoMatch (n + m)} (xs ++ ys) zs
          ≡ xs ++ (ys ++ zs)
++-assoc' {xs = xs} = ++-assoc {xs = xs}

{-# REWRITE ++-assoc' #-}

++-assoc-succeed : {xs : Vec A zero} {ys : Vec A m} {zs : Vec A l}
                 → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc-succeed = refl

정의적 싱글턴과 주제 축약 (Definitional singletons and subject reduction)

일부 유용한 재작성 규칙은 정의적 싱글턴(단위 타입 ⊤ 같은 것)이 있을 때 주제 축약(subject reduction)을 깨뜨려. 예를 들어 원(circle)을 고차 귀납 타입으로 공리화한 다음을 생각해 보자:

IdOver : (P : A → Set) → x ≡ y → P x → P y → Set
IdOver P refl x y = x ≡ y

syntax IdOver P p x y = x ≡[ P ↓ p ]≡ y

dcong : ∀ {B : A → Set} (f : (x : A) → B x) (p : x ≡ y) → f x ≡[ B ↓ p ]≡ f y
dcong f refl = refl

postulate
  Circle : Set
  base   : Circle
  loop   : base ≡ base

  circle-elim : ∀ (P : Circle → Set) (baseP : P base)
              → baseP ≡[ P ↓ loop ]≡ baseP
              → ∀ x → P x

  circle-elim-base : ∀ (P : Circle → Set) (baseP : P base)
                       (loopP : baseP ≡[ P ↓ loop ]≡ baseP)
                   → circle-elim P baseP loopP base ≡ baseP
  {-# REWRITE circle-elim-base #-}

  circle-elim-loop : ∀ (P : Circle → Set) (baseP : P base)
                       (loopP : baseP ≡[ P ↓ loop ]≡ baseP)
                   → dcong (circle-elim P baseP loopP) loop ≡ loopP

이상적으로는 경로 생성자 loop에 적용된 circle-elim에 대한 계산 규칙(circle-elim-loop)도 재작성 규칙으로 만들고 싶을 거야:

{-# REWRITE circle-elim-loop #-}

불행히도 이것은 ⊤로 소거(eliminate)할 때 주제 축약 문제를 일으켜. η-동등성에 의해, 두 항등 증명 p와 q에 대해 circle-elim (λ _ → ⊤) tt p = circle-elim (λ _ → ⊤) tt q가 정의적으로 성립한다는 점을 기억해:

open import Agda.Builtin.Unit

circle-elim-pq : ∀ {p q}
               → circle-elim (λ _ → ⊤) tt p
               ≡ circle-elim (λ _ → ⊤) tt q
circle-elim-pq = refl

계산 규칙 circle-elim-loop는 따라서 p ≡ q도 정의적으로 함의해야 하는데, 귀납 항등 타입(id)은 그런 η 규칙을 만족하지 않아.

Agda는 이러한 문제성 재작성 규칙을 탐지하려 시도하고, 재작성이 안전하다고 확신할 수 없으면 RewriteVariablesBoundInSingleton 경고를 던져. 재작성 규칙이 실제로 안전하다고 확신하거나, 정의적 싱글턴을 사용하지 않는다는 것을 알거나, 단순히 이상하게 행동하는 정의적 동등성에 대해 걱정하지 않는다면, -WnoRewriteVariablesBoundInSingleton으로 경고를 끄고 재작성 규칙에 계속 의존할 수 있어.

재작성 규칙의 일반적인 형태 (General shape of rewrite rules)

일반적으로, 동등성 증명 eq는 다음 요구 사항이 충족되면 {-# REWRITE eq #-} 프래그마로 재작성 규칙으로 등록될 수 있어:

  • eq의 타입이 eq : (x₁ : A₁) ... (xₖ : Aₖ) → f p₁ ... pₙ ≡ v 형태일 것
  • f가 추정(포스툴레이트), 정의된 함수 기호, 또는 완전히 일반적인 매개변수에 적용된 생성자(즉 매개변수가 서로 다른 변수여야 함)일 것
  • 각 변수 x₁, …, xₖ가 p₁ ... pₙ의 패턴 위치에서 적어도 한 번 나타날 것 (패턴 위치의 정의는 아래 참조)
  • 좌변 f p₁ ... pₙ은 중립(neutral)이어야 함, 즉 축약되지 않아야 함

다음 패턴들이 지원돼:

  • x y₁ ... yₙ — 여기서 x는 패턴 변수이고 y₁, …, yₙ은 패턴 안에서 지역적으로 바인딩된 서로 다른 변수들
  • f p₁ ... pₙ — 여기서 f는 추정, 정의된 함수, 생성자, 또는 데이터/레코드 타입이고, p₁, …, pₙ은 다시 패턴들
  • λ x → p — 여기서 p는 다시 패턴
  • (x : P) → Q — 여기서 P와 Q는 다시 패턴들
  • y p₁ ... pₙ — 여기서 y는 패턴 안에서 지역적으로 바인딩된 변수이고 p₁, …, pₙ은 다시 패턴들
  • Set p 또는 Prop p — 여기서 p는 다시 패턴
  • 그 외의 용어 v (여기서 v의 변수들은 패턴 위치에 있다고 간주되지 않음)

재작성 규칙이 추가되면 Agda는 축약 중에 좌변의 모든 인스턴스를 대응하는 우변 인스턴스로 자동으로 재작성해. 더 정확히는, (정의적으로) f p₁σ ... pₙσ와 같은 용어가 vσ로 재작성되며, 여기서 σ는 패턴 변수 x₁, …, xₖ에 대한 어떤 치환이야.

재작성은 정상 축약 후에 일어나므로, 재작성 규칙은 달리 중립이었을 용어에만 적용돼.

합류 검사 (Confluence checking)

Agda는 --confluence-check 플래그를 활성화하면 재작성 규칙의 합류성을 선택적으로 검사할 수 있어. 구체적으로 다음 두 속성을 강제해:

  • 재작성 규칙의 두 좌변이 (근(root) 위치나 부분식에서) 겹치면, 두 좌변의 가장 일반적인 통일자인다시 재작성 규칙의 좌변이어야 한다. 예를 들어 suc m + n = suc (m + n)과 m + suc n = suc (m + n) 두 규칙이 있으면 suc m + suc n = suc (suc (m + n)) 규칙도 있어야 한다.
  • 각 재작성 규칙은 삼각형 성질(triangle property)을 만족해야 한다: 어떤 재작성 규칙 u = w와 u => v의 단일 단계 병렬 펼침에 대해, v => w의 다른 단일 단계 병렬 펼침이 있어야 한다.

--local-confluence-check 플래그도 있는데, 덜 제한적이면서 재작성 규칙의 지역 합류성만 검사해. 재작성 규칙이 종료한다면(현재는 검사되지 않음) 이 두 속성은 동등해.

고급 사용 (Advanced usage)

Agda.Builtin.Equality.Rewrite를 임포트하는 대신, 그것을 REWRITE 빌트인으로 등록하면 다른 타입을 재작성 관계로 선택할 수 있어. 예를 들어 {-# BUILTIN REWRITE _~_ #-} 프래그마는 _~_ 타입을 재작성 관계로 등록해. 재작성 관계가 되기 위해서는 타입이 최소한 두 개의 인자를 받아야 하고, 마지막 두 인자는 가시적(visible)이어야 해.

재작성 규칙 임포트 (Importing rewrite rules)

import M으로 모듈 M의 모든 재작성 규칙은 M의 전역에서든 부분모듈 안에서든 상관없이 임포트돼. 또한 M이 임포트한 모든 재작성 규칙도 전이적으로 임포트돼.

즉, 모듈 M0이 어떤 재작성 규칙을 선언하거나 임포트하고, M1이 M0을 임포트하면, M2가 M1을 임포트할 때 M2가 M0을 직접 임포트하지 않더라도 그 재작성 규칙들을 임포트하게 돼.

이 전이적 임포트 동작의 이유는 주제 축약(타입 보존이라고도 함) 속성을 보장하기 위해서야. M0이 타입 A와 A를 Nat으로 재작성하는 규칙을 내보내면, M1은 타입 A의 상수 a = zero를 선언할 수 있어. M2가 M1에서 A와 a를 임포트하지만 A에 대한 재작성 규칙은 임포트할 수 없다면, M2의 맥락에서 a에서 zero로의 축약이 그 타입을 A에서 Nat으로 바꾸는데, 재작성 규칙이 없으면 이것은 A와 같지 않아. 따라서 축약 하의 타입 보존이 실패하게 돼.

요약하면, 재작성 규칙의 범위 규칙은 Haskell 2010에서 인스턴스의 범위 규칙과 같아.

더 알아보기 (Learn more)