Proving and Computing: The Infinite Pigeonhole Principle and Countable Choice

이 논문은 스테파노 베르디 (Stefano Berardi) 의 64 세 생일을 기념하여 헌정된 'Logics and Type Theory'집에 수록된 것으로, Zena M. Ariola, Paul Downen, Hugo Herbelin 에 의해 작성되었습니다. 이 논문은 **구조적 코재귀 (structural corecursion)**와 **고전적 논리 (classical reasoning)**를 결합하여 무한한 데이터 스트림을 처리하는 새로운 방식을 제시하며, 특히 **무한 비둘기집 원리 (Infinite Pigeonhole Principle)**와 **가산 선택 공리 (Axiom of Countable Choice)**의 계산적 내용을 증명하고 구현하는 데 중점을 둡니다.

다음은 논문의 상세한 기술적 요약입니다.

1. 문제 제기 (Problem)

• 구조적 재귀 vs 구조적 코재귀: 현대 프로그래밍에서 구조적 재귀 (structural recursion) 는 입력 데이터의 구조에 따라 재귀 호출을 제한하여 종료성을 보장하는 표준 기법입니다. 반면, 그 쌍대인 **구조적 코재귀 (structural corecursion)**는 무한한 데이터 (스트림 등) 를 생성하는 데 사용되며, Haskell, Rocq (Coq), Agda 등의 언어에서 지원됩니다.
• 한계: 기존 코재귀는 순수 함수형 프로그래밍 맥락에서 주로 연구되었으며, 고전 논리 (예: 배중률, callcc) 와 결합된 상황에서의 표현력이나 계산적 의미는 충분히 탐구되지 않았습니다.
• 목표: 고전적 논리 (특히 callcc 제어 연산자) 와 결합된 다양한 코재귀 패턴 (코이테레이션, 최소 코재귀, 고전적 코재귀) 의 표현력을 분석하고, 이를 통해 무한 비둘기집 원리와 가산 선택 공리를 계산적으로 구현하는 프로그램을 개발하는 것입니다.

2. 방법론 (Methodology)

저자들은 Rocq (Coq 의 후속 버전) 증명 보조기를 사용하여 다음과 같은 방법론을 적용했습니다.

• 스트림 정의 및 지연 평가: Rocq 의 CoInductive 타입을 사용하여 스트림을 정의하되, OCaml 과 같은 호출-값 (call-by-value) 언어로 추출 (extraction) 시 발생하는 비효율적인 꼬리 (tail) 강제 평가를 방지하기 위해 tail 을 unit -> stream 형태로 지연 (lazy) 시키는 방식을 채택했습니다.
• 코재귀 패턴의 계층화:
  1. 코이테레이션 (Coiteration/Anamorphism): 상태 (seed) 를 업데이트하며 무한히 스트림을 생성하는 기본 패턴.
  2. 최소 코재귀 (Minimal Corecursion/Apomorphism): 코재귀를 중간에 종료하고 미리 정의된 스트림을 반환할 수 있는 패턴.
  3. 고전적 코재귀 (Classical Corecursion): callcc (call-with-current-continuation) 를 사용하여 코재귀 루프를 일시 중단 (pause) 하고 나중에 재개 (resume) 할 수 있는 패턴. 이는 sum type 대신 continuation 을 사용하여 제어 흐름을 조작합니다.
• 증명 및 추출: 논리적 명제를 Rocq 에서 증명하고, 그 증명 과정을 제거하여 (erasure) 실제 실행 가능한 OCaml 코드를 추출하는 '프로그램 추출 (program extraction)' 기법을 사용했습니다.

3. 주요 기여 (Key Contributions)

A. 무한 비둘기집 원리의 계산적 증명

• 문제: 임의의 무한한 불리언 (true/false) 스트림에서, 동일한 값을 가지는 무한한 부분열 (constant subsequence) 의 인덱스 스트림을 찾는 것.
• 해결: infinite_bool 함수를 구현했습니다. 이 함수는 callcc 를 사용하여 "현재 헤드가 무한히 반복될 것"이라고 가정하고 스트림을 생성합니다. 만약 다른 값이 발견되면, 제어 흐름을 과거의 체크포인트로 되돌려 (backtracking) 가정을 변경하고 다른 값을 기준으로 검색을 계속합니다.
• 특징: 이 알고리즘은 고전적 코재귀를 사용하여, 프로그램이 실행되는 동안 관찰된 유한한 요소에 기반하여 동적으로 답을 수정하면서도 일관된 결과를 보장합니다.

B. Escardó 및 Oliva 의 증명과의 비교

• Escardó 와 Oliva 는 Agda 에서 이중 부정 (double-negation) 변환을 통해 비동기적 (indirect) 인 증명을 제시했습니다.
• 본 논문은 **직접적 (direct style)**인 증명 방식을 제시하며, 스트림이 함수와 달리 파라미터를 전달받아 이전 상태에 의존할 수 있다는 점을 활용했습니다. 이는 Escardó 와 Oliva 의 증명보다 더 유연한 스트림 생성을 가능하게 합니다.

C. 가산 선택 공리 (Countable Choice) 의 구현

• 문제: 가산 도메인 위의 총관계 (total relation) 에서 각 입력에 대한Witness 를 선택하는 함수를 추출하는 것.
• 기존 접근: Spector 나 Berardi 등의 기존 연구는 일반 재귀 (general recursion) 를 사용하며, 그 종료성은 외부적으로 가정 (Bar Induction 등) 했습니다.
• 본 논문의 접근: 고전적 논리를 callcc 로 직접 구현하고, 코이테레이션 (coiteration) 만으로 종료성을 정당화하는 새로운 방식을 제시했습니다. 이는 Double-Negation Shift 원리를 스트림의 분배법칙으로 해석하여, 제어 연산자와 코인덕션의 결합을 통해 선택 공리를 내부적으로 정당화합니다.

4. 결과 (Results)

• OCaml 추출 및 실행: Rocq 에서 작성된 증명 코드가 OCaml 로 추출되어 실행되었습니다. delimcc 라이브러리를 사용하여 callcc 를 구현한 결과, 무한 비둘기집 원리 프로그램이 다양한 입력 스트림에 대해 올바르게 작동함을 확인했습니다.
  • 예: 스트림이 false, true, false, true, true...일 때, 처음 3 개의 인덱스를 요청하면 false 를 찾지만, 5 개를 요청하면 true 가 더 많으므로 true 를 찾는 인덱스로 자동 조정됩니다.
• 일관성: 프로그램은 실행 중 관찰된 정보에 따라 답을 동적으로 수정할 수 있지만, 한 번 호출된 스트림은 전체 수명 동안 일관된 결과를 제공합니다.
• 코드 가용성: 모든 Rocq 코드 및 추출된 OCaml/Scheme 코드는 infinite-pigeonhole 저장소에서 공개되었습니다.

5. 의의 및 중요성 (Significance)

• 고전 논리와 코재귀의 융합: 고전적 논리 (제어 연산자) 와 코재귀를 결합함으로써, 순수 함수형 언어에서는 불가능했던 복잡한 제어 흐름 (백트래킹, 상태 재개) 을 가진 무한 스트림 처리 알고리즘을 설계할 수 있음을 보였습니다.
• 종료성 정당화의 혁신: 가산 선택 공리와 같은 강력한 논리 명제를 구현할 때, 외부적으로 종료성을 가정하는 일반 재귀 대신, 코이테레이션과 제어 연산자만으로 종료성을 정당화하는 새로운 패러다임을 제시했습니다.
• 스테고파노 베르디의 업적 계승: 고전 논리 계산, 가산 선택 공리 계산, 증명으로부터의 프로그램 추출이라는 베르디의 세 가지 주요 기여 분야를 아우르는 통합적인 연구를 수행했습니다.
• 형식적 검증의 확장: Rocq(또는 Coq) 환경에서 고전적 논리를 포함한 복잡한 알고리즘의 정합성을 검증하고, 이를 실제 실행 가능한 코드로 변환하는 방법론을 정립했습니다.

요약하자면, 이 논문은 구조적 코재귀에 고전적 제어 연산자를 도입하여 무한 데이터 처리의 한계를 극복하고, 무한 비둘기집 원리와 가산 선택 공리에 대한 계산적으로 검증 가능한 직접적인 구현을 제시함으로써, 형식적 방법론과 프로그래밍 언어 이론 간의 간극을 좁히는 중요한 성과를 거두었습니다.