Work-in-Progress: A Tactic for Pattern Matching in Autosubst

기술 요약: Autosubst에서의 패턴 매칭을 위한 전술(Tactic)

문제 정의
본 논문은 de Bruijn term과 $\sigma$-calculus를 통한 치환(substitution)에 대한 추론을 자동화하는 Rocq(구 Coq) 기반의 코드 생성기인 Autosubst 프레임워크의 특정 한계를 다룹니다. Autosubst는 asimpl 전술을 통해 가정이 없는 목표(assumption-free goals)에 대한 동등성 검사(equality checking)는 성공적으로 자동화하지만, 사용자가 표준 전술인 apply나 eapply를 사용하여 가정(예: 타이핑 규칙 또는 보조 정리)을 목표에 적용하려고 할 때 실패합니다.

이러한 시나리오에서 사용자는 $\sigma$-동등성(modulo $\sigma$-equivalence)을 기준으로 목표와 가정을 통일(unify)해야 합니다. 그러나 Autosubst의 자동화는 가정을 대상으로 하는 매칭을 위해 설계되지 않았습니다. 결과적으로 사용자는 다음과 같은 번거로운 우회 방법을 사용해야만 합니다:

• 규칙을 간접적인 형태(직접적인 치환 항 대신 신선한 메타 변수를 사용)로 공식화하기.
• 목표와 가정 사이의 간극을 메우기 위해 보조 정리(auxiliary lemmas)를 도입하기.
• 증명 과정에서 목표를 수동으로 변형하거나 존재 변수(existential variables)를 명시적으로 인스턴스화하기.

핵심적인 어려움은 $\sigma$-매칭($\sigma$-동등성을 고려한 매칭)이 유일하지 않다는 점에 있습니다. 즉, 단일 매칭 문제는 여러 해를 가질 수 있으며, 그 해들이 모두 컨텍스트의 전제 조건(premises)을 만족하는 것은 아닙니다. 또한, 전체 $\lambda\sigma$-calculus에 대한 2차 매칭(second-order matching)은 결정 불가능(undecidable)하며, $\beta$-축약(reduction)이 없는 경우에도 해가 반드시 유일한 것은 아닙니다.

방법론
저자들은 $\sigma$-동등성을 기준으로 패턴 매칭을 자동화하기 위해, Rocq의 Ltac 언어로 구현된 **as_apply**라는 이름의 작업 진행 중(work-in-progress) 휴리스틱 전술을 제안합니다. 이 전술은 크게 두 가지 주요 단계로 작동합니다:

1. 전처리(Preprocessing):

   • 목표(goal)와 대상 가정의 결론(conclusion) 모두를 기존의 asimpl 전술을 사용하여 $\sigma$-calculus에 대해 정규화(normalize)합니다.
   • 가정 내의 양화된 변수들을 존재 변수(evars)로 대체합니다.
   • 가정의 전제 조건들을 매칭 단계 이후에 해결해야 할 하위 목표(subgoals)로 변환합니다.
   • substify와 renamify를 사용하여 명시적 이름 변경 연산(예: $s\langle\xi\rangle$)과 인스턴스화 연산($s[\xi]$) 간의 변환을 처리합니다.

2. 매칭 단계(Matching Phase):

   • 전술은 목표 항과 인스턴스화된 가정 항 사이의 매칭 방정식 집합 $M = \{s_i =_\sigma t_i\}$를 구성합니다.
   • 부분 절차인 $\sigma_{min}$을 사용하여 방정식을 왼쪽에서 오른쪽으로 처리합니다 ($\sigma_{min}$은 인스턴스화와 합성성을 특징짓는 $\sigma$-규칙의 부분집합입니다).
   • 휴리스틱(Heuristics): 만약 $\sigma_{min}$이 매치를 찾는 데 실패하면, 전술은 형식적 개발에서 흔히 나타나는 패턴을 포착하는 일련의 휴리스틱을 적용합니다. 여기에는 다음이 포함됩니다:
     • $s[t \cdot \sigma] =_\sigma ?s[t \cdot id]$ 형태의 방정식을 처리하여, 미지의 값을 리프팅된 치환(lifted substitution)으로 인스턴스화하는 경우 ($?s \mapsto s[\Uparrow\sigma]$).
     • 항등 치환(identity substitutions) 또는 특정 변수 구조를 포함하는 경우를 처리하는 것.
   • 치환을 적용한 후, 전술은 가정을 다시 정규화합니다. 목표와 가정이 구문론적으로 동일해지면 성공으로 간정합니다.

이 전술은 다중 상호 유도 정렬(multiple mutually inductive sorts), 벡터 치환, 그리고 일급 이름 변경(first-class renamings)을 포함하여 Autosubst 컴파일러가 지원하는 전체 입력 언어를 지원하도록 일반화되었습니다.

주요 기여

1. as_apply의 도입: Autosubst 기반 개발에서 apply/eapply를 대체하기 위해 설계된 휴리스틱 전술로, 가정이 존재하는 상황에서 $\sigma$-동등성을 기준으로 매칭을 가능하게 합니다.
2. 일반화: 복잡한 바인더(binders)와 이름 변경 연산을 포함하여 Autosubst가 지원하는 전체 구문을 커버하도록 매칭 로직을 확장했습니다.
3. 경험적 평가: 표준 벤치마크, 특히 POPLMark 및 POPLMark Reloaded 챌린지에 이 전술을 적용했습니다.

결과
저자들은 POPLMark (642행) 및 POPLMark Reloaded (683행) 챌린지 솔루션에 대해 as_apply를 평가했습니다.

• 사용 빈도: as_apply는 POPLMark B 솔루션에서 15회, POPLMark Reloaded 솔루션에서 10회 사용되었습니다.
• 효과성: 테스트된 모든 사례에서 as-apply는 의도된 목표를 성공적으로 해결했습니다.
• 단순화: 이 전술의 사용은 이전 솔루션들의 특징이었던 간접적 규칙 공식화, 보조 정리, 그리고 수동 목표 변형의 필요성을 제거했습니다.
• 한계점: 저자들은 as_apply가 $\sigma$-완전(complete)하지 않으며 결정기(decider)가 아님을 인정합니다. $\sigma$-매칭은 여러 해를 가질 수 있으므로, 휴리스틱 성격의 전술이기 때문에 올바른 해가 존재하더라도 이론적으로는 잘못된 해를 선택할 가능성이 있지만, 사례 연구에서는 그러한 실패가 관찰되지 않았습니다.

의의 및 주장
본 논문은 $\sigma$-매칭의 이론적 문제가 본질적으로 어렵지만(비유일한 해, 전체 $\lambda\sigma$에서의 결정 불가능성), 실용적인 휴리스틱 접근 방식이 실제 환경에서 높은 수준의 자동화를 회복할 수 있다고 주장합니다. 이 연구의 의의는 de Bruijn 구문을 사용하는 사용자들이 증명 보조기의 한계에 맞춘 간접적인 형태가 아니라, 직접적이고 자연스러운 형태로 타이핑 규칙과 보조 정리를 기술할 수 있게 하여 수동 부담을 줄여준다는 데 있습니다.

저자들은 현재 작업의 상태를 "작업 진행 중(Work-in-Progress)"이라고 명시하며 겸허한 태도를 유지하고 있습니다. 그들은 현재의 전술이 무한하거나 다수의 해가 발생할 가능성 때문에 휴리스틱에 의존하고 있음을 언급했습니다. 향 \후 연구는 유일성 기준이 성립하는 가장 큰 파편 $\sigma'$를 식별하여, 잠재적으로 검증된 보장을 갖는 매칭 전술을 만드는 것을 목표로 합니다.