The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (Full Version)

기술 요약: 베타-에타-노멀 고차 재작성(Beta-Eta-Normal Higher-Order Rewriting)을 위한 계산 가능성 경로 순서(Computability Path Order)

문제 정의
고차 재작성(higher-order rewriting)은 다양한 형식을 포함한다. 구체적으로는 "일반적인(plain)" 고차 재작성(구문론적 매칭을 사용하고 $\beta$-축약을 재작성 규칙으로 취급함)과 "노멀(normal)" 고차 재작성(매칭을 $\beta\eta$ 모듈로 수행하고 항을 $\beta\eta$-노멀 폼으로 간주함)이 있다. 일반적인 고차 재작성을 위한 CPO(Computability Path Order)와 같은 강력한 종료 방법들이 존재하지만, 이를 노멀 고차 재작성(특히 Nipkow 식의 Higher-Order Rewrite Systems, HRS)에 적용하는 데는 상당한 어려움이 따른다.

NHORPO와 같은 기존의 HRS 방식들은 코어 순서가 실패하는 시스템을 처리하기 위해 "중립화(neutralization)"라는 변환 기법에 의존하는 경우가 많다. 그러나 중립화는 자동화를 복잡하게 만든다. 또한, 표준 경로 순서는 노멀 재작성에서 어려움을 겪는데, 그 이유는 $\beta\eta$와 호환되는 정칙 순서(well-founded order)가 전통적인 의미에서의 단조성(context에 대해 닫혀 있음)이나 안정성(substitution에 대해 닫혀 있음)을 갖지 못하는 경우가 많기 때문이다. 예를 들어, 어떤 순서가 $\beta\eta$와 호환되고 컨텍스트에 대해 닫혀 있다면, $c > c$와 같은 모순을 초래하여 정칙성을 위반할 수 있다.

방법론
저자들은 일반적인 고차 재작성을 위해 원래 정의되었던 CPO를 $\beta\eta$-노멀 고차 재작성 환경으로 격상시키는 것을 제안한다. 이렇게 생성된 순서를 **$\beta\eta$-노멀 계산 가능성 경로 순서(NCPO)**라고 부른다.

이 방법론은 다음과 같은 핵심 구성 요소에 기반한다:

1. 축약 순서 쌍(Reduction Order Pair): Jouannaud와 Rubio의 접근 방식을 따라, 저자들은 주 순서(primary order)인 NCPO와 "일반적인" 변형인 CPO로 이루어진 순서 쌍 $(>, \sqsupset)$를 정의한다. 이 쌍은 $\beta\eta$-노멀 안정성을 만족한다: 즉, $s > t$이면 모든 치환 $\sigma$에 대해 $s\sigma\downarrow \sqsupset^+ t\sigma\downarrow$를 만족하며, 여기서 $\downarrow$는 $\beta\eta$-정규화(normalization)를 의미한다. 이를 통해 종료 증명이 일반 CPO 구성 요소의 정칙성과 단조성에 의존할 수 있도록 한다.
2. 비범용 항(Nonversatile Terms): 핵심적인 기술적 혁신은 순서의 적용 대상을 비범용 항으로 제한하는 것이다. 비범용 항이란 치환과 그에 따른 $\beta\eta$-정규화가 오직 해당 항의 진정한 부분항(proper subterms)에만 영향을 미치는 항을 말한다. 저자들은 이전 연구에 비해 개선된 비범용성 충분 조건(Lemma 1)을 제공하며, 이는 순서의 안정성을 증명하는 데 필수적이다.
3. CPO로부터의 확장: NCPO는 원래의 CPO로부터 두 가지 주요 확장을 포함한다:
   • 접근 가능한 부분항(Accessible Subterms): 이는 타입 위치(양의/음의 베이스 타입 위치)에 의해 결정되는 특정 경우에 대해 재귀적 비교가 엄격한 타입 감소를 우회할 수 있도록 한다.
   • 작은 심볼(Small Symbols): 이 기능은 특정 함수 심볼을 "작은" 것으로 취급할 수 있게 하여, 표준 재귀적 경로 순서가 실패하는 시스템(예: 리스트 처리 함수)의 종료 증명을 가능하게 한다.
4. 규칙 세트: 순서는 함수 심볼(big 및 small), 적용(application), 추상화(abstraction)를 다루는 일련의 규칙(Figure 1)을 통해 귀납적으로 정의된다. 주목할 점은, 순서가 노멀 폼에서 직접 작동하므로 $\beta$ 및 $\eta$ 축약을 방향 지우는(orienting) 규칙이 제거되었다는 것이다. 또한, 접근 가능한 부분항의 문맥 내에서 $\eta$-확장을 다루기 위해 새로운 규칙 $\langle \lambda\triangleright\eta \rangle$가 도입되었다.

주요 기여

• NCPO의 정의: 본 논문은 접근 가능한 부분항과 작은 심볼을 통합하여 $\beta\eta$-노멀 고차 재작성을 위해 특별히 설계된 최초의 계산 가능성 경로 순서인 NCPO를 공식적으로 정의한다.
• 정당성 증명: 저자들은 쌍 $(>_\tau, \sqsupset_\tau)$가 유효한 $\beta\eta$-노멀 고차 축약 순서임을 증명하여(Theorem 2), 이와 호환되는 모든 HRS의 종료를 보장한다.
• 개선된 비범용성 조건: 본 논문은 NHORPO에서 제공된 것보다 더 강력한 비범용성 충분 조건을 제시한다.
• SAT/SMT를 통한 자동화: 저자들은 NCPO가 중립화를 사용하는 NHORPO보다 자동화에 더 용이하다고 주장한다. 중립화는 심볼릭 파라미터에 의존하는 변환된 항의 복잡한 구문 분석을 요구하여 SMT 인코딩을 어렵게 만드는 반면, NCPO의 파라미터(우선순위, 타입 순서, 상태)는 더 직관적으로 인코딩될 수 있다.

결과
저자들은 NCPO의 프로토타입을 Haskell로 구현하였으며, Hasmtlib 패키지를 사용하여 종료 문제를 SMT-LIB 2 형식으로 인코딩하고 Z3 솔버를 사용하여 해결하였다. 실험 결과(Table 1)는 NCPO를 중립화가 있는 경우와 없는 경우의 NHORPO, 그리고 WANDA 및 CSI$^{ho}$의 HORPO 구현과 비교한다.

• NHORPO 대비 우월성: NCPO는 NHOR포(중립화 포함)가 실패하는 여러 시스템의 종료를 성공적으로 증명한다. 구체적으로:
  • 예제 8 (리스트 증가): NCPO는 NHORPO에는 없는 기능인 '작은 심볼'을 사용하여 종료를 증명한다.
  • 예제 7 (부정 표준형): NCPO는 '접근 가능한 부분항'을 사용하여 종료를 증명하는 반면, 중립화가 포함된 NHORPO는 비교 과정에서 범용 항을 다룰 수 없어 규칙의 방향을 정하지 못해 실패한다.
• 비교 불가능한 능력: 연구는 neutr.p와 같이 NHORPO(중립화 포함)는 성공하지만 NCPO는 실패하는 사례를 식별하여, 두 접근 방식의 능력이 서로 비교 불가능함을 보여준다.
• 효율성: NCPO의 파라미터 탐색은 계산적으로 효율적이며, 종종 NHORPO 탐색과 유사한 시간을 소요하는 반면, 중립화 파라미터 탐색은 복잡성이 폭발할 수 있음을 보여준다.

의의 및 주장
본 논문은 NCPO가 NHORPO와 중립화의 조합에 대한 강력하고 가벼운 대안을 제공한다고 주장한다. 저자들은 중립화를 사용하는 NHORPO가 강력한 경쟁자이긴 하지만, 중립화 기법의 자동화 복잡성을 고려할 때 NCPO가 노멀 고차 재작성의 자동 종료 증명을 위한 더 실용적인 선택임을 강조한다.

저자들은 NCPO의 이행성(transitivity)이 여전히 미해결 과제로 남아 있다고 겸허히 언급한다. 이는 밑바탕이 되는 plain order에 $\beta$-축약이 포함되어 있어 CPO와 NHORPO의 비이행성을 정당화하기 때문이며, NCPO의 구체적인 속성에 대해서는 추가 조사가 필요하다. 또한, NC고차 재작위의 의존 쌍(dependency pair) 기법에 NCPO를 통합하는 것이 논리적인 다음 단계라고 제안한다. 결론적으로, 저자들은 NHORPO의 특정 예제를 해결할 수 있다는 잘못된 주장과 같은 기존 문헌의 오류를 피하기 위해 고차 종료 방법론의 정형화가 필요함을 강조하며 논문을 마친다.