기술적 요약: 대수적 비정합 증명: 재귀성과 GTC

문제 제기

순환 증명을 포함한 비정합 증명 체계는 모달 $\mu$-계산과 고차 고정점 논리와 같은 (공)귀납을 포함하는 논리에 필수적입니다. 유한한 유도 트리를 갖는 유한 증명과 달리, 이러한 체계는 무한 유도 트리를 허용합니다. 따라서 건전성 (soundness) 은 트리 깊이에 대한 표준 구조적 귀납을 통해 확립될 수 없습니다. 대신, 이러한 체계는 건전성을 보장하기 위해 유도 트리 내의 무한 경로에 대한 제약 조건인 **전역 추적 조건 (Global Trace Condition, GTC)**을 부과합니다.

순환 증명을 위한 다양한 범주론적 접근 (예: $\mu$-양완 범주, 추적 범주) 이 있음에도 불구하고, 건전성을 보장하는 GTC 의 범주론적 특성화를 제공하는 것은 여전히 중요한 과제입니다. 주요 어려움은 다음과 같습니다:

1. 전역 대 국소: GTC 는 전체 유도 트리에 제약을 부과하므로, 표준 범주론적 추론의 국소적이고 구성적인 성격과 충돌합니다.
2. 무한 구조: 비정합 증명은 무한할 수 있어, 의미론적 사상을 구성하기 위해 표준 구조적 귀납을 사용할 수 없습니다.
3. 재귀적 대수 이론의 간극: 재귀적이고 정합적인 대수는 유일한 해 (의미론적 해석) 를 보장하지만, 비정합 증명의 유도 트리는 종종 비정합 대수를 생성합니다. 기존 이론들은 특정 비정합 사례 (예: Capretta 와 Jeannin 등의 "하강 수열" 예시) 에서 왜 유일한 해가 존재하는지를 명확히 설명하지 못합니다.

방법론

본 논문은 유도 트리를 대수로 모델링하고 GTC 를 이러한 대수의 그래프에 대한 조건으로 형식화함으로써 비정합 증명 체계를 위한 대수적 프레임워크를 개발합니다.

1. 프레시브 (Presheaves) 위의 가족적 함자 (Familial Functors) 의 대수

저자들은 유도 트리를 $c: C \to FC$ 형태의 대수로 모델링하며, 여기서 $F$는 프레시브 범주 $\widehat{\mathcal{J}}$ 위의 가족적 함자입니다.

• 가족적 함자: 이들은 특정 피브레이션 속성을 가진 범주 다이어그램인 다항식을 통해 정의된 다항 함자의 일반화입니다. 이들은 노드가 판단 (judgements) 으로 레이블링되고 분기 구조가 추론 규칙에 의해 결정되도록 하여, 매개변수와 문맥을 자연스럽게 수용합니다.
• 대수의 그래프: 대수의 그래프 개념을 바탕으로, 본 논문은 $\mathbf{Set}$ 위의 엔도함자에 대한 대수의 정합성과 해당 그래프 내 무한 경로의 부재 사이의 동치 관계를 프레시브 위의 엔도함자로 확장합니다 (정리 1.9).

2. 쌍대성과 재귀적 이미지

증명의 비정합적 성격을 해결하기 위해, 이 프레임워크는 쌍대성 (adjunctions) 을 따른 대수-대수 사상 간의 대응을 활용합니다.

• 전략: 원래 대수 $c$가 재귀적이어야 한다는 요구 대신, 본 논문은 적절한 왼쪽 쌍대자 (left adjoint) $L$ (구체적으로, 순서수 주석에 의해 유도된 기저 변경 함자) 하에서의 $c$의 이미지가 재귀적인지 여부를 조사합니다.
• 메커니즘: 만약 $Coalg(L)(c)$가 재귀적이고, 대상 의미론 대수$a$가 오른쪽 쌍대자$R$의 이미지에 속한다면 (즉,$a \cong Alg(R)(a')$),$c$에 대해 유일한 대수-대수 사상이 존재합니다 (명제 2.4).
• 직관: 이는 쌍대성을 따라 당겨오기 (pulling back) 로 얻은 순서수 주석과 같은 추가 차원으로 유도 그래프를 풍부하게 하는 것에 해당합니다. 이러한 확장은 원래 그래프가 비정합적일지라도 그래프를 정합적으로 만들 수 있습니다.

3. 추적 구조와 GTC

GTC 는 추적 구조 $(pfml, prog)$를 사용하여 형식화됩니다:

• 추적 구조: VPoly 범주 (다항식 범주) 의 사상으로, 에지를 따라 공식 (또는 표시된 공식) 을 추적하며, 일반적으로 고정점 풀림에 해당하는 "진행하는" 에지의 부분집합과 결합됩니다.
• GTC 정의: 전증명 (pre-proof) 이 GTC 를 만족한다는 것은 레이블이 지정된 그래프의 모든 무한 경로가 접미사를 따라 무한히 진행하는 추적을 허용함을 의미합니다.
• 순서수 주석: 이 프레임워크는 순서수로 주석이 달린 판단을 갖는 추상 증명 시스템 $P^\gamma$를 구성합니다. 망각 함자 $u_\gamma: \mathcal{J}dg^\gamma \to \mathcal{J}dg$는 필요한 쌍대성을 유도합니다.

주요 기여 및 결과

1. 프레시브로의 그래프 이론 확장

본 논문은 $\mathbf{Set}$ 위의 엔도함자에 대한 그래프의 정합성과 대수의 재귀성 사이의 동치 관계를 프레시브 범주 위의 엔도함자로 확장합니다 (정리 1.9). 이는 가족적 함자에 대한 대수의 그래프를 정의하고, 함자가 교차와 역상을 보존함을 증명함으로써 달성됩니다.

2. 재귀적 이미지를 통한 건전성

본 논문은 **건전성 정리 (Theorem 4.13)**를 확립합니다: 전증명 $c$가 GTC 를 만족하면, $a$가 순서수 주석을 통한 리프트된 대수의 이미지에 속하는 한, $c$에서 임의의 의미론 대수 $a$로 가는 유일한 대수-대수 사상이 존재합니다.

• 이는 표준적인 의미에서 재귀적이지 않지만 유일한 해를 허용하는 비정합 사례 (예: 하강 수열) 에 대한 대수적 설명을 제공합니다.
• GTC 가 (순서수 주석을 포함한) "확장된" 대수를 재귀적으로 만든다는 것을 보여줍니다.

3. GTC 와 재귀성의 특성화

본 논문은 GTC 와 재귀성 사이의 양방향 특성화를 확립합니다:

• GTC $\implies$ 재귀성: 전증명이 GTC 를 만족할 필요충분조건은 순서수 주석 함자 하에서의 그 이미지가 재귀적인 것입니다 (정리 4.17).
• 재귀성 $\implies$ GTC: 전증명이 모든 추적 구조에 대해 GTC 를 만족할 필요충분조건은 재귀적인 것입니다 (명제 4.14).
• 이는 GTC 가 본질적으로 적절한 쌍대성을 따라 이동한 후 관련 대수가 재귀적이 되도록 보장하는 조건임을 명확히 합니다.

4. 구체적인 구현

이 프레임워크는 세 가지 증명 시스템을 통해 시연됩니다:

1. 모달 $\mu$-계산: GTC 가 최대 고정점의 무한 풀림에 해당하는 $\nu$-스레드의 존재에 대응되는 비정합 증명 체계입니다. 순서수 주석은 최대 고정점에 대한 표준 근사치에 해당합니다.
2. 고차 고정점 논리 (HFLN): $\mu$ 및 $\nu$ 추적을 모두 추적해야 하는 시스템으로, 복잡한 추적 구조를 처리할 수 있는 프레임워크의 능력을 보여줍니다.
3. $\mu$-양완 범주: Santocanale 의 순환 증명 시스템의 비정합 변형으로, 판단이 변수 할당에 따라 함자적으로 변하는 비이산 범주를 처리할 수 있는 프레임워크의 능력을 보여줍니다.

중요성 및 주장

본 논문은 건전성을 성공적으로 보장하는 비정합 증명의 범주론적 추상화가 주요 기여라고 주장합니다.

• 개념적 통찰: GTC 는 단순한 운영적 점검이 아니라, 적절한 쌍대성 (구체적으로 순서수 의미론에 의해 안내된 쌍대성) 의 렌즈를 통해 볼 때 대수가 재귀적이 되도록 보장하는 구조적 속성입니다.
• 통합: 이 프레임워크는 가족적 함자와 쌍대성을 포함하는 단일 대수 메커니즘 하에서 다양한 비정합 증명 체계의 건전성 처리를 통합합니다.
• 이론적 간극 메우기: 이는 쌍대성을 따라 의미론을 "리프트"함으로써 비정합 대수에 대해 유일한 해가 존재할 수 있는 방식을 설명함으로써 기존 재귀적 대수 이론의 간극을 메웁니다.

저자들은 이 프레임워크가 건전성을 확립하지만, 향후 작업에서 이 대수적 설정 내에서 완전성, 절제 (cut-elimination), 그리고 리셋 조건이나 튕기는 스레드 (bouncing threads) 와 같은 다른 건전성 조건들을 다루는 것이 필요하다고 지적합니다.