Towards Weak Stratification for Logics of Definitions

기술 요약: 정의의 논리를 위한 약한 계층화(Weak Stratification)를 향하여

문제 정의
정의의 논리(logic of definitions)는 추론 규칙에 의해 명시된 판단을 인코딩하고 추론하기 위해 사용되는 일련의 논리들로, 원자적 술어가 자기 자신에 의존할 수 있는 논리식과 연관된 술어들을 다룬다. 이러한 정의에 내재된 외견상의 순환성을 해결하기 위해, 표준적인 접근 방식들은 정의가 단조적인 고정점 연산자(monotone fixed-point operators)로 취급되도록 보장하는 *계층화 조건(stratification condition)*을 부과한다. 이 조건은 술어가 자신의 정의 내부에서 부정적으로(함의의 왼쪽에) 나타나는 것을 방지한다.

그러나 논리적 관계(logical relations)를 포함하여 프로그래밍 언어의 성질을 증명하는 데 유용한 많은 명세들은 술어가 부정적으로 나타나는 정의를 필요로 한다. Abella 증명 보조기의 기초가 되는 논리 $\mathcal{G}$에서는 이러한 정의들이 허용되지 않는다. Tiu [19]는 이전에 계층화 조건을 *약한 계층화(weak stratification)*로 완화하여(헤드의 레벨이 부정적 출현의 레벨보다 엄격히 큰 경우 부정적 출현을 허용함) $\mathcal{LD}$라는 논리를 도입했으나, $\mathcal{LD}$는 핵심 파편(core fragment)에 국한되어 있었다. $\mathcal{LD}$는 이름(names)과 신선도(freshness)를 다루기 위해 노미널 상수(nominal constants)를 사용하는 데 필수적인 *나블라 양화사($\nabla$)*와 자연수 귀납법을 넘어의 일반적인 *귀납적 정의(inductive definitions)*에 대한 지원이 부족했다. 본 연구에서 다루는 과제는 $\nabla$와 일반적인 귀납적 정의가 존재하는 상황에서도 일관성을 유지하면서, 정의의 논리를 약한 계층화를 포함하도록 확장하는 것이다.

방법론
본 논문은 Tiu의 $\mathcal{LD}$를 나블라 양화와 일반적인 귀납적 정의로 확장한 새로운 논리 $\mathcal{LD}\mu\nabla$를 정의한다. 방법론은 세 가지 주요 단계로 진행된다:

1. $\mathcal{LD}\mu\nabla$의 구문 및 의미론:
   논리는 정의 집합 $\mathcal{D}$와 귀납적 정의 집합 $\mathcal{I}$를 갖는 1차 시퀀트 계산(first-order sequent calculus)의 확장으로 정식화된다.

• 약한 계층화: 정의 집합 $\mathcal{D}$가 약하게 계층화되어 있다는 것은 모든 절(clause) $H \triangleq_X B$와 그라운딩 대입(grounding substitution) $\rho$에 대하여, $\text{lvl}(H\rho) \ge \text{lvl}(B\rho)$임을 의미한다. 결정적으로, 이는 헤드의 레벨이 부정적 출현의 레벨보다 엄격히 크다면 정의된 술어가 부정적으로 나타나는 것을 허용한다.
• 귀납을 위한 엄격한 계층화: 본 논문은 귀납적 정의 $\mathcal{I}$에 대해 더 엄격한 조건인 엄격한 계층화를 부과한다(그라운드 원자 술어의 레벨이 그 인자들에 독립적이어야 함). 이 제한은 귀납과 약한 계층화를 결합할 때 발생할 수 있는 불일치를 방당하기 위해 필요하다.
• 나블라 양화사: 논리는 노미널 상수와 신선도를 처리하기 위해 이름의 일반적인 인스턴스와 특정 인스턴스를 구분하는 $\nabla$ 양화사를 포함한다.

2. 그라운드 논리 및 해석:
   일관성을 증명하기 위해, 저자들은 모든 공식이 그라운드 형태인(고유 변수가 없는) 논리의 그라운드 버전인 $\mathcal{LD}\mu\nabla_\infty$를 구축한다.

• 그라운딩 보조 정리(Grounding Lemma): 핵심적인 기술적 단계는 $\mathcal{LD}\mu\nabla$에서의 모든 유도가 그라운딩 대입을 통해 $\mathcal{LD}\mu\nabla_\infty$에서의 유도로 해석될 수 있음을 증명하는 것이다. 이는 전체 논리의 일관성 문제를 그라운드 논리의 일관성 문제로 환원시킨다.
• 무한 규칙(Infinitary Rules): $\mathcal{LD}\mu\nabla_\infty$에서 표준적인 $\forall R$ 및 $\exists L$ 규칙은 모든 그라운드 항(term)에 대해 양화하는 무한 규칙으로 대체되며, 귀납을 위한 $\mu L$ 규칙 역시 모든 그라운드 인스턴스를 다루도록 확장된다.

3. 컷 제거(Cut Elimination):
   일관성 증명의 핵심은 $\mathcal{LD}\mu\nabla_\infty$에서 컷 규칙(구체적으로 멀티컷 규칙)을 제거하는 것이다.

• 축약 관계(Reduction Relation): 컷을 위로 밀어 올리거나 제거하는 방법을 명시하는 축약 관계가 유도(derivation) 위에 정의된다.
• 가적성(Reducibility): McDowell와 Miller가 적응시킨 Tait-Martin-Löf 기법을 따라, 저자들은 유도에 대한 가적성(및 정규화 가능성) 개념을 정의한다. 저자들은 $\mathcal{LD}\mu\nabla_\infty$의 모든 유도가 가적임을 증명한다.
• 귀납적 사례 처리: 증명의 결정적인 측면은 약한 계층화와 귀납의 상호작용을 다루는 것이다. 저자들은 일반적인 정의에는 약한 계층화가 충분하지만, 귀납적 정의는 일관성을 유지하기 위해 엄격하게 계층화되어야 함을 보여준다. 저자들은 약한 계층화된 귀듭적 정의를 허용하는 것이 논리적 불일치로 이어진다는 반례(섹션 3.3)를 제공한다.

주요 기여

• $\mathcal{LD}\mu\nabla$의 정의: 본 논문은 약한 계층화, 나블라 양화, 그리고 일반적인 귀납적 정의를 결합한 논리를 공식적으로 정의한다.
• 일관성 증명: 주요 기여는 $\mathcal{LD}\mu\nabla$가 일관적임을 증명하는 것이다. 이는 $\mathcal{LD}\mu\nabla_\infty$에 대한 컷 제거를 증명하고 그라운딩 해석을 확립함으로써 달성된다.
• 계층화 제약: 본 연구는 허용 가능한 정의와 허용되지 않는 정의 사이의 경계를 명확히 한다. 이는 일반적인 정의에는 약한 계층화가 충분하지만(논리적 관계를 가능하게 함), 귀납적 정의는 일관성을 보존하기 위해 엄격한 계층화가 필요함을 입증한다.
• 반례: 본 논문은 귀납적 정의에 대한 계층화 조건을 완화하는 것이 논리적 불일치를 초래한다는 구체적인 반례를 제공하여, $\mathcal{I}$에 부과된 제한의 정당성을 부여한다.

결과

• 일관성: $\mathcal{LD}\mu\nabla$의 일관성이 증명되었다. 결과적으로, $\mathcal{LD}\mu\nabla_\infty$는 모든 증명 가능한 시퀀트에 대해 컷이 없는 유도를 허용한다.
• 역전 성질(Inversion Properties): 본 논문은 $\mathcal{LD}\mu\nabla_\infty$에 대한 다양한 도입 규칙의 역전성(예: $\wedge R, \vee L, \nabla R$의 역전성)과 문맥이 비어 있을 때 $\vee R, \exists R$, 그리고 정의 규칙($\Delta R$)의 특수한 부분 역전성을 확립한다. 이러한 성질들은 증명 탐색 절차에 매우 중요하다.
• 한계: 컷 제거 정리는 그라운드 논리 $\mathcal{LD}\mu\nabla_\infty$에 대해서만 확립되었다. 저자들은 이 결과를 고유 변수가 있는 전체 논리 $\mathcal{LD}\mu\nabla$로 확장하는 것이 여전히 미해결 과제로 남아 있다고 언급한다.

의의
본 연구의 의의는 Abella 증명 보조기의 능력을 확장할 수 있는 잠재력에 있다. Abella는 현재 정의가 엄격하게 계층화되도록 제한하는 논리 $\mathcal{G}$를 기반으로 한다. 약한 계층화된 정의의 포함을 정당화함으로써, 본 연구는 Abella가 프로그래밍 언어의 의미론적 성질(예: 타입 안전성 및 컴파일러 정확성)을 증명하는 데 근본적인 기술인 논리적 관계를 네이티브로 지원할 수 있는 길을 열어준다.

본 논문은 이 작업을 $\mathcal{G}$의 더 넓은 확장을 위한 기초적인 단계로 위치시킨다. 현재의 결과는 $\nabla$와 귀납을 포함한 약한 계층화를 다루지만, 저자들은 Abella를 위한 완전한 정당화를 위해서는 코-귀납(co-induction)과 노미널 추상화(nominal abstraction)를 포함하는 추가적인 확장이 필요하다고 언급한다. 또한 본 연구는 약한 계층화를 귀납과 혼합할 때 발생할 수 있는 불일치를 방지하기 위해, 귀납적 정의에 대해 엄격한 계층화를 유지해야 할 필요성을 강조한다.