Computation by infinite descent made explicit

문제 및 동기
$\mu$-calculus의 맥락에서 유래한 비정형적(non-wellfounded) 증명 이론은 유도적(inductive) 및 공유도적(co-inductive) 추론을 표현하기 위해 무한한 증명 트리를 허용한다. 이 분야의 핵심 과제는 유효한 증명과 유효하지 않은 유도 트리를 구별하는 정당성 기준을 정의하는 것이다. '트레이스(trace)' 또는 '진행 스레드(progressing thread)' 조건과 같은 전통적인 기준들은, 모든 무한 브랜치가 최소 고정점(least fixpoint)이 왼쪽에서 무한히 언폴딩(unfolding)되거나 최대 고정점(greatest fixpoint)이 오른쪽에서 무한히 언폴딩되는 특정 공식의 시퀀스를 포함할 것을 요구한다.

그러나 최근 Baelde 등의 연구[BDKS22]는 트레이스 기반 조건의 한계, 특히 합성성(compositionality)과 관련된 문제를 식별했다. 그들은 컷(cut)이 트레이스를 단절시키는 경우를 처리하기 위해 '바운싱 스레드(bouncing threads)'를 도입했으나, 이 조건이 결정 불가능(undecidable)하며 증명 체계의 구조적 규칙들과 상호작용이 좋지 않다는 점을 언급했다. 나아가, 커리-하워드 대응(Curry-Howard correspondence)이 증명을 프로그램으로 간주한다는 점을 고려할 때, 복잡한 유효성 조건 하에서 비정형적 증명이 계산 가능한 함수(정규화)를 나타낸다는 것을 입증하는 것은 쉽지 않은 일이다.

본 논문은 명시적 서수 변수(explicit ordinal variables)를 갖춘 증명 체계를 탐구함으로써 비정형적 증명의 합성성과 계산적 내용에 관한 문제를 다룬다. Dam, Gurov, 그리고 Sprenger [DG02, SD03a]가 개척한 이 접근 방식은 서수 근사치를 나타내는 서수 변수로 고정점 공식을 주석 처리한다. 본 논문은 이 프레임워크가 표준 트레이스 조건을 놓칠 수 있는 증명들을 포착하면서도 결정 가능한, 더 투명한 정당성 기준을 제공하고 견고한 커리-하워드 해석을 지원할 수 있는지 조사한다.

방법론
저자 Sebastian Enqvist는 유도적($\mu$) 및 공유도적($\nu$) 정의가 확장된 직관주의 명제 논리를 위한 비정형적 증명 체계를 개발한다. 핵심 방법론은 다음과 같다:

1. 구문 확장(Syntax Extension): 언어는 명시적 서수 변수와 제약 조건을 포함하도록 확장된다. $\mu X. A$와 같은 공식은 $\mu_\alpha X. A$로 주석이 달릴 수 있으며, 여기서 $\alpha$는 서수 항(서수 변수 $a, b, \dots$ 또는 상수 $\infty$)이다. 시퀀트는 이러한 서수 항들 사이의 부등식을 나타내는 제약 트리 $O$를 포함한다.
2. 유효성 기준(Validity Criterion): 유도는 모든 무한 브랜치에 대해, 해당 브랜치에서 결국 성립하는 서수 변수의 무한 감소 사슬($a_0 > a_1 > a_2 > \dots$)이 존재할 때 **유효(valid)**하다고 정의된다. 이는 유도적 추론의 건전성의 핵심인 "무한 감소(infinite descent)" 논증을 구문에 명시적으로 드러낸다.
3. 계산 가능성 의미론(Computability Semantics): 본 논문은 닫힌 유도(closed derivations)에 대한 계산 가능성(computability) 개념을 정의한다. 증명은 논리 연결사와 고정점에 대응하는 특정 귀납적 절들을 만족하는 정규형(normal form)으로 축소될 때 계산 가능하다고 간주된다. 예를 들어, 최소 고정점 $\mu_\infty X. A$의 증명은 어떤 $\xi$에 대하여 근사치 $\mu_\xi X. A$의 증명으로 축소될 때 계산 가능하다.
4. 컷 축소(Cut Reductions): 증명의 계산적 동작을 정의하기 위해 일련의 재작성 규칙(컷 축소 및 순열 규칙)이 도입된다. 이 체계는 이러한 특정 규칙들 하에서 결합성(confluence)을 갖도록 설계되어, 잘 정의된 정규화 개념을 허용한다.
5. 범주적 모델링(Categorical Modeling): 닫힌 공식들이 객체이고 증명의 동치류가 화살표인 증명 범주를 구성한다. 저자는 이 범주가 각각의 고정점 공식에 대한 초기 대수(initial algebras)와 최종 코대수(final coalgebras)의 구조를 지원함을 입증한다.

주요 기여 및 결과

• 유효한 증명의 계산 가능성: 주요 결과(정리 4.9)는 모든 유효한 증명(무한 감소 사슬 조건을 만족하는 증명)이 계산 가능함을 확립한다. 이는 만약 증명이 계산 불가능하다면, 서수의 감소 사슬이 없는 무한 브랜치를 구성할 수 있게 되어 유효성 조건을 모순하게 된다는 것을 보여줌으로써 증명된다.
• 유한 공식의 정규화: 이 계산 가능성 결과의 결과로서, 본 논문은 "유한 공식"( $\top, \land, \lor, \mu$로부터 구축되었으며 $\nu$는 포함하지 않는 공식)의 증명이 항상 유일한 정규형으로 정규화됨을 증명한다(정리 4.11).
• 함수의 표현: 본 체계는 $N, \dots, N \vdash N$ 형태의 시퀀스(여기서 $N$은 자연수를 나타냄)에 대한 증명의 정규화 결과를 제공한다. 이러한 증명들은 자연수 상의 유일한 전사 함수(total functions)를 나타낸다(정리 4.12).
• "바운싱(Bouncing)" 사례 처리: 본 논문은 서수 변수 프레임워크가 표준 진행 스레드 조건을 통과하지 못하지만 "바운싱 스레드" 조건 하에서는 유효한 증명들을 포착할 수 있음을 보여준다. 컷이 표준 트레이스를 방해하지만, 컷 공식 내의 명시적 서수 변수가 감소 논증을 보존하여 증명을 유효하게 만드는 예시가 제공된다.
• 범주적 의미론: 본 논문은 최소 고정점이 초기 대수에 해당하고 최대 고정점이 최종 코대수에 해당하는 범주적 모델을 구축한다(섹션 5.2 및 5.3). 이는 계산 가능성 의미론이 유도 및 공유도적 타입에 대한 표준적인 범주적 해석과 일치함을 확인시켜 준다.
• 결정 가능성: 바운싱 스레드 조건과 달리, 서수 변수에 기반한 유효성 기준은 결정 가능하다[SD03a].

의의 및 주장
본 논문은 표준 트레이스 조건을 넘어선 자연스러운 비정형적 증명 유효성 기준을 찾고자 하는 Baelde 등의 프로젝트[BDKS22]에 기여하는 파일럿 연구로서 자신을 위치시킨다. 저자는 명시적 서수 변수를 사용하는 Dam-Gurov-Sprenger 프레임워크가 이 목적을 위한 적절한 후보라고 주장한다.

그 의의는 두 가지 주요 관찰에 있다:

1. 표현력: 유효성 조건은 표준 진행 스레드 조건에 의해 유효하다고 인식되지 않는 증명들(특히 "바운싱" 동작을 가진 증명들)을 포착한다.
2. 계산적 의미: 계산 가능성 의미론을 제공함으로써, 본 논문은 이 체계의 모든 유효한 증명이 잘 정의된 계산 가능한 프로그램을 나타낸다는 것을 입증한다. 이는 구문적 유효성 조건과 종료/계산 가능성이라는 의미론적 요구 사이의 간극을 메운다.

저자는 본 논문이 논리 전체에 대한 완전한 컷 제거 정리(추가적인 순열 규칙이 필요함)를 제공하거나, 서수 변수 체계가 바운싱 스레드 조건과 동일한 능력을 갖는지에 대한 확정적인 증명을 제공하지 않는다는 점을 겸허히 언급한다. 대신, 모든 바운싱 스레드 유효 증명이 서수 변수를 사용하여 표현될 수 있는지에 대한 문제는 향후 연구를 위한 열린 문제로 남겨둔다. 이 연구는 커리-하워드 관점에서 서수 변수에 대한 추가적인 탐구를 촉발하는 역할을 한다.