로컬 재작성 규칙
로컬 재작성 규칙 (Local Rewriting)
로컬 재작성 규칙(local rewrite rules)은 모듈을 계산 규칙으로 매개변수화할 수 있게 해주는 실험적 기능이에요. 구체적으로, @rewrite 속성으로 주석을 달아 재작성 관계를 목표로 하는 모듈 매개변수를 로컬 재작성 규칙으로 선언할 수 있게 해줘요. 그 결과:
- 모듈 내부에서 로컬 재작성 규칙은 축약(reduction) 중에 자동으로 적용돼, 전역 재작성처럼 왼쪽 변의 인스턴스를 오른쪽 변으로 재작성해요.
- 모듈 외부에서 로컬 재작성 규칙은 모듈 매개변수의 인스턴스화에 대한 제약으로 작용해요. 예를 들어 모듈을 열 때 Agda는 양쪽 변이 정의적으로 같아야 하는지 확인해요.
이 기능은 Yann Leray와 Théo Winterhalter의 "Encode the Cake and Eat It Too"에서 소개된 로컬 재작성 타입 이론(LRTT)에 기반해요. 그들의 제시와 달리 우리는 "인터페이스 환경"과 "로컬 문맥"을 강한 구문적 구분으로 나누지 않지만, 그럼에도 @rewrite 속성을 모듈 매개변수로 제한함으로써 재작성에 대한 양화는 프리넥스(prenex)만 허용돼요. 예를 들어 정의는 로컬 재작성 규칙을 반환하거나, 로컬 재작성 규칙을 취하는 다른 정의로 매개변수화될 수 없으므로 foo : (n : Nat) → ((@rewrite p : n ≡ 0) → Nat) → Nat는 허용되지 않아요.
의미론적으로 로컬 재작성 규칙은 로컬 재작성 규칙 매개변수를 가진 모듈의 모든 인스턴스화를 인라인함으로써 제거될 수 있어서, Agda 이론의 나머지에 대해 보수적(conservative)이어야 해요.
참고: 이 페이지는
--local-rewriting옵션에 관한 것이에요. 이것은--rewriting옵션을 사용하면서 전역REWRITE규칙에 대한 일종의 합류(confluence) 검사를 활성화하는--local-confluence-check와는 관계가 없어요.그것은 또한 (현재로서는)
rewrite구성체와도 구별돼요. 다만 내부적으로는 로컬 재작성 규칙("smart with")으로 디슈가하는with추상화의 새 버전을 구현할 계획이 있어요.
예제로 보는 로컬 재작성 규칙 (Local rewrite rules by example)
{-# OPTIONS --local-rewriting --rewriting #-}
module language.local-rewriting where
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
로컬 재작성 규칙을 동기 부여하기 위해, Agda의 내장 자연수에 대한 덧셈을 구현하고 결합법칙을 증명하는 다음 코드를 생각해 봐요.
module Addition where
_+_ : Nat → Nat → Nat
zero + m = m
suc n + m = suc (n + m)
+-assoc : ∀ {n m l} → (n + m) + l ≡ n + (m + l)
+-assoc {n = zero} = refl
+-assoc {n = suc n} = cong suc (+-assoc {n = n})
이제 자연수의 다른 인코딩, 예를 들어 단위 값의 리스트를 사용하고 싶다고 상상해 봐요.
Nat' = List ⊤
Nat'에 대해 덧셈을 정의하고 결합법칙을 증명하기 위해 중복 없이, 우리는 덧셈과 결합법칙 정의를 추상 타입의 자연수와 귀납 원리에 대해 매개변수화할 수 있어요.
module ParametricAddition
(Nat : Set) (zero : Nat) (suc : Nat → Nat)
(ind : (P : Nat → Set) → P zero → (∀ n → P n → P (suc n)) → ∀ n → P n)
(ind-zero : ∀ {P z s} → ind P z s zero ≡ z)
(ind-suc : ∀ {P z s n} → ind P z s (suc n) ≡ s n (ind P z s n))
where
_+_ : Nat → Nat → Nat
n + m = ind (λ _ → Nat) m (λ _ → suc) n
+-assoc : ∀ {n m l} → (n + m) + l ≡ n + (m + l)
+-assoc {n = n} {m = m} {l = l}
= ind (λ □ → (□ + m) + l ≡ □ + (m + l))
(trans (cong (_+ l) ind-zero) (sym ind-zero))
(λ _ h → trans (cong (_+ l) ind-suc)
( trans ind-suc
( trans (cong suc h) (sym ind-suc))))
n
우리는 덧셈과 결합법칙의 단일 매개변수 정의를 작성하는 데 성공했지만, 훨씬 더 복잡한 증명을 대가로 치렀어요. 귀납 원리에 대해 매개변수화된 것은 더 이상 zero와 successor에서 자동으로 계산되지 않으므로, ind-zero와 ind-suc를 여러 번 수동으로 호출해야 해요.
로컬 재작성 규칙은 이 지루함을 해결해 줘요. ind-zero와 ind-suc 방정식에 @rewrite로 간단히 주석을 달면, 인코딩 세부사항에 매개변수화된 채로 단순한 결합법칙 증명을 되찾을 수 있어요.
module ParametricAdditionRew
(Nat : Set) (zero : Nat) (suc : Nat → Nat)
(ind : (P : Nat → Set) → P zero → (∀ n → P n → P (suc n)) → ∀ n → P n)
(@rewrite ind-zero : ∀ {P z s} → ind P z s zero ≡ z)
(@rewrite ind-suc : ∀ {P z s n} → ind P z s (suc n) ≡ s n (ind P z s n))
where
_+_ : Nat → Nat → Nat
n + m = ind (λ _ → Nat) m (λ _ → suc) n
+-assoc : ∀ {n m l} → (n + m) + l ≡ n + (m + l)
+-assoc {n = n} {m = m} {l = l}
= ind (λ □ → (□ + m) + l ≡ □ + (m + l)) refl (λ _ h → cong suc h) n
로컬 재작성 규칙이 유용할 수 있는 더 많은 예는 "Encode the Cake and Eat It Too" 논문을 참고하세요.
제한 사항 (Limitations)
합류성과 종료 검사 (Confluence and termination checking)
현재 로컬 재작성 규칙에 대한 합류성 또는 종료 검사의 형태는 구현되어 있지 않아요. 비-합류 또는 비-종료 로컬 재작성 규칙의 결과는 전역 재작성과 유사해요: 비-합류는 주체 축약(subject reduction)을 위태롭게 하고 비-종료는 타입 체커가 루프를 돌게 할 수 있지만, 논리적 건전성(logical soundness)은 결코 위협받지 않아야 해요.
패턴 매칭으로 로컬 재작성 규칙 정제하기 (Refining local rewrite rules with pattern matching)
현재 로컬 재작성 규칙에 발생하는 변수에 대한 접근 불가 패턴 매칭은 허용되지 않아요. 이는 유효하지 않은 재작성 규칙 아래에서의 타입 체킹을 피하기 위해서예요 (재작성 유효성은 치환 아래에서 불안정해요).
module _ (f : Nat → Nat) (@rewrite p : f 1 ≡ 0) where
bad : f ≡ (λ x → x) → Nat
bad refl = {!!} -- 여기서 'f'를 'λ x → x'로 치환하면 로컬 재작성 규칙 'p'가 무효화됨
게다가 로컬 재작성 규칙의 변수에 대한 매칭은 인라인 기반 의미론적 근거를 깨뜨려요.
이런 단점에도 불구하고, 추가 플래그 아래에서 이 제한을 미래에 완화할 계획이 있어요. 패턴 매칭으로 로컬 재작성 규칙을 정제하는 것은 "로컬 동일성 반영(local equality reflection)"의 제한된 형태를 가능하게 하는데, 이는 (가능하면) 더 잘 작동하는 with 추상화 메커니즘을 포함해 많은 흥미로운 응용을 가져요.
--cubical로 로컬 재작성 규칙에 대해 데이터 타입 매개변수화 (Parameterising datatypes over local rewrite rules with --cubical)
큐빅 아그다(Cubical Agda)에는 로컬 재작성 규칙에 대한 추가 제한이 있어요. 로컬 재작성 규칙 매개변수를 가진 모듈 내부에서 데이터 또는 레코드 타입을 선언하려고 하면 CannotGenerateTransportLocalRewrite 오류가 발생해요:
module _ (n : Nat) (@rewrite _ : n ≡ 0) where
data Foo : Set where
mk : Foo
이 제한은 Cubical Agda가 transport와 경로 합성의 데이터 타입에 대해 다양한 프리미티브를 자동으로 정의하는 방식 때문이에요. 이것이 (현재로서는) 로컬 재작성 규칙 매개변수를 가진 데이터 타입에 대해 어떤 모습이어야 하는지는 명확하지 않아요.
이 문제가 발생하면 로컬 재작성 규칙이 있는 모듈 밖에서 데이터 또는 레코드 타입을 정의해 보세요.