Towards an HRS Category in TermCOMP

기술 요약: TermCOMP 내 HRS 카테고리 구축을 향하여

문제 정의
연례 종료 경진대회(TermCOMP)에는 고차 재작성(higher-order rewriting)을 위한 카테고리가 포함되어 있다. 역사적으로 이 카테고리는 일반 매칭(plain matching)과 명시적인 $\beta$-축약 규칙에 의존하는 대수적 함수 시스템(Algebraic Functional Systems, AFSs)의 의미론을 활용해 왔다. Nipkow의 고차 재작성 시스템(HRSs)은 $\beta\eta$ 모듈로 재작성을 수행하며 일반적으로 Miller의 패턴(PRSs)이나 최근의 결정론적 고차 패턴 재작성 시스템(DPRSs)을 사용하지만, 이는 잘 확립된 형식주의임에도 불구하고 TermCOMP의 경쟁 프레임워크에 완전히 통합되지 못했다. 과제는 HRS의 의미론($\beta\eta$ 모듈로 재작성)을 기존 TermCOMP 프레임워크(AFSs 및 메타 치환 기반)와 조화시켜, HRS를 대상으로 하는 도구들이 AFS를 대상으로 하는 도구들과 직접 경쟁할 수 있도록 하는 데 있다.

방법론
저자들은 HRS와 현재의 TermCOMP 고차 의미론(단순 유형 메타 치환 재작성 시스템, STMRSs로 정의됨) 사이의 공식적인 가교를 제안한다. 방법론은 세 가지 주요 단계로 구성된다:

1. 패턴의 일반화: 저자들은 PRS와 DPRSs를 모두 일반화하는 **확장 패턴 재작성 시스템(Extended Pattern Rewrite Systems, EPRSs)**을 도입한다. EPRSs는 "확장 패턴(Extended Patterns, EPATs)"을 사용하는데, 이는 DPRSs의 결정론적 매칭 제약을 완화하면서도 자유 변수가 추상화되지 않은 인자에 적용되는 구조를 유지한다. 이 클래스는 독립적인 실용 도구로서가 아니라 이론적 증명을 용이하게 하기 위해 주로 정의되었다.
2. STMRS 의미론의 확장: 저자들은 STMRS 규칙(현재 TermCOMP 표준)의 정의를 확장하여, 좌변(left-hand sides)이 표준 패턴이 아닌 EPAT가 될 수 있도록 한다. 저자들은 well-behaved(잘 작동하는) 및 quasi-well-behaved(준-잘 작동하는) 항(term)의 개념을 도입한다. 이러한 구문적 제한은 메타 치환이 적용될 때, 결과물인 항이 추가적인 축약 단계를 요구하는 새로운 $\beta$-redex를 생성하지 않고 $\beta$-정규형(구체적으로 $\beta\eta$-long normal form)을 유지하도록 보장한다.
3. 정규화된 재작성을 통한 구현: 핵심 기술적 기여는 well-behaved STMRS에서의 재작성이 그에 대응하는 EPRS에서의 재작성을 시뮬레이션한다는 것을 입증하는 것이다. 저자들은 일반 치환(EPRSs에서 사용됨)과 메타 치환(STMRSs에서 사용됨) 사이의 번역을 정의하여 두 시스템이 종료성에 관해 동등함을 증명한다.

주요 기여

• EPRSs의 정의: DPRSs를 일반화하여 더 넓은 범위의 벤치마크를 수용하면서도 관리 가능한 매칭 특성을 유지하는 새로운 HRS의 구문적 하위 클래스.
• 동등성을 위한 구문적 제한: "well-behaved" STMRS 규칙의 도입. 이 규칙들은 좌변이 well-behaved이고 우변이 quasi-well-behaved가 되도록 제한한다. 이는 메타 치환의 적용이 $\beta$-redex를 생성하지 않도록 하여, 항의 $\beta$-정규형을 보존한다.
• 공식 동등성 정리: well-behaved STMRS $R$과 항 $s$가 $\beta\eta$-long normal form일 때, EPRS 의미론에서의 재작성 단계($s \to_R t$)가 발생하는 것은 STMRS 의미론을 따른 후 $\beta$-정규화가 발생하는 것($s \Rightarrow_R \cdot \Rightarrow!_\beta t$)과 동치임을 증명한다.

결과
주요 결과는 well-behaved STMRSs와 그에 대응하는 EPRSs의 재작성 관계를 확립하는 **정리 15(Theorem 15)**이다. 구체적으로:

• $s \Rightarrow_R \cdot \Rightarrow!_\beta t$ 일 필요충분조건은 $s \to_R t$ 이다 ($R$을 EPRS로 볼 때).
• 이는 **따름정리 20(Corollary 20)**으로 이어지며, well-behaved STMRS에서 "재작성 후 $\beta$-정규화" 전략의 종료성은 대응하는 EPRS의 보편적 종료성과 일치함을 명시한다.

저자들은 이 동등성이 $\beta\eta$-long normal form에 있는 항들에 대해 성립함을 보여준다. 저자들은 2차 STMRS의 경우, 메타 치환이 해당 문맥에서 $\beta$-redex를 생성할 수 없기 때문에 대응 관계가 더욱 강력하며, 단계 간의 일대일 매핑을 제공한다고 언급한다.

의의
본 논문은 TermCOMP 내에 HRS (하위) 카테고리를 위한 공식적 토대를 마련했다고 주장한다. 기존 TPDB 형식을 사용하여 구문적으로 검사 가능한 벤치마크의 부분 집합(well-behaved STMRSs)을 정의함으로써, 저자들은 다음을 가능하게 한다:

1. 직접 경쟁: HRS를 위해 설계된 도구($\beta\eta$-재작성 사용)가 이제 동일한 카테고리 내에서 AFS를 대상으로 하는 도구들과 직접 경쟁할 수 있다. 이는 그들의 종료성이 제안된 의미론 하에서 일치함이 증명되었기 때문이다.
2. 더 넓은 도구 지원: 구현 결과는 단순한 전역적 종료성뿐만 아니라 단계별 대응에 기반한 시뮬레이션을 바탕으로 하므로, 종료성 이상의 속성을 비교할 수 있게 한다.
3. 기존 연구의 정교화: 이 결과는 AFSM에서의 PRS 구현(Kop)과 조합 시스템(combinatory systems)에서의 구현(van Oostrom 및 van Raamsdonk)을 더 일반적인 클래스의 HRS(EPRSs)로 확장하고, 정규화된 재작성과 고차 재작성의 동등성에 대한 엄격한 증명을 제공함으로써 기존 연구를 강화한다.

저자들은 메타 치환이 전체 고차 치환보다 엄격히 덜 강력하기 때문에, 이 결과가 모든 HRS를 다루지는 않는다는 점을 인정하며 연구 범위를 겸허하게 설정하였다. 그러나 정의된 하위 클래스가 기존 벤치마크의 상당 부분과 이전 연구에서 소개된 특정 DPRSs를 수용하기에 충분하다고 주장한다.