The Global Orientation Barrier in Step-Duplicating Recursors: Impossibility, Modular Escape, and a Certified Witness

이 논문은 스텝-복제 재귀자를 갖는 1 차원 재작성 시스템에서 직접적 구성적 측정의 불가능성을 기계적으로 검증하고, 투영 기반 방법이 이를 우회하는 방식을 규명하며, 안전한 부분 집합에 대해 기계화된 종료성 증명과 인증 체인을 제시합니다.

핵심

이 논문은 **"복잡한 계산 시스템이 왜 멈추는지 (종료성), 그리고 왜 어떤 방법은 그걸 증명할 수 없는지"**에 대한 흥미로운 발견을 담고 있습니다.

비유하자면, 이 논문은 **"무한히 반복되는 미로에서 탈출하는 방법"**을 연구한 것입니다. 연구자들은 "왜 어떤 나침반은 미로에서 길을 잃게 만들고, 다른 나침반은 성공적으로 탈출하게 하는지"를 증명했습니다.

핵심 내용을 일상적인 언어와 비유로 설명해 드릴게요.

---

1. 상황 설정: "복제되는 미로" (KO7 시스템)

연구자들은 아주 작은 규칙으로 이루어진 가상의 세계, **'KO7'**이라는 시스템을 만들었습니다. 이 세계에는 다음과 같은 특징이 있습니다.

• 규칙: 어떤 물건을 처리하면, 그 물건이 두 개로 복제되어 다시 처리됩니다.
  • 예: "사과를 반으로 자르면, 사과 2 개가 나오고 그중 하나는 다시 자른다."
• 문제: 이 복제 과정이 계속되면 물건이 기하급수적으로 늘어날 것 같아, 시스템이 영원히 멈추지 않을 것 같습니다. 하지만 실제로는 언젠가 반드시 멈춥니다.

2. 장애물: "전체적인 시야의 함정" (Global Orientation Barrier)

연구자들은 "이 시스템이 왜 멈추는지"를 증명하려는 두 가지 방법을 시도했습니다.

• 방법 A: 전체 무게 재기 (직접적/전체적 측정)

  • 비유: 시스템의 모든 물건을 한 바구니에 담고 무게를 재는 것입니다.
  • 실패 이유: 규칙상 물건이 '두 개'로 복제되는데, 바구니의 무게는 당연히 늘어납니다. "무게가 줄어들어야 멈춘다"는 논리에서, 무게가 늘어난 순간 증명 실패가 됩니다.
  • 논문 결론: "물건이 두 개로 복제되는 규칙이 있는 한, 무게를 재는 방식으로는 절대 멈춤을 증명할 수 없다"는 것을 컴퓨터로 엄밀하게 증명했습니다. (이것이 '불가능성 정리'입니다.)

• 방법 B: 핵심만 쏙 빼기 (모듈형/프로젝션 측정)

  • 비유: 바구니 전체 무게를 재는 대신, "가장 중요한 숫자 (카운터)"만 눈여겨보는 것입니다.
  • 성공 이유: 복제되는 물건들 사이에는 '중요한 숫자'가 하나씩 들어있습니다. 규칙이 적용될 때마다 이 숫자는 반드시 1 씩 줄어듭니다.
  • 핵심: 복제된 나머지 물건들은 '쓰레기'처럼 무시하고, 숫자만 보면 "아, 숫자가 줄어들고 있으니 언젠가 0 이 되어 멈추겠구나!"라고 증명할 수 있습니다.
  • 논문 결론: "복제된 물건을 무시하고 핵심 숫자만 추적하는 방법은 이 미로를 성공적으로 탈출합니다."

3. 주요 발견: "왜 다른 방법은 실패하는가?"

논문은 이 두 방법 사이의 경계를 명확히 그렸습니다.

• 왜 '무게 재기'는 실패할까?
  • 복제된 물건들이 시스템의 '함정 (App Trap)'에 걸려 있습니다. 복제된 물건은 실제로는 아무 일도 하지 않지만 (무용지물), 무게를 재는 나침반은 그걸 진짜로 중요한 것처럼 착각합니다. 그래서 무게가 늘어난다고 착각하게 됩니다.
• 왜 '핵심 쏙 빼기'는 성공할까?
  • 이 방법은 복제된 가짜 물건들을 아예 무시하고, 진짜로 줄어들고 있는 '숫자'만 봅니다. 그래서 함정에 걸리지 않고 정답을 찾습니다.

4. 실증 실험: "TTT2 라는 로봇의 검증"

연구자들은 이 이론을 검증하기 위해 TTT2라는 자동 증명 로봇에게 문제를 던졌습니다.

• 로봇의 반응:
  • "무게를 재는 방식 (다항식 해석 등)"으로 해결하려 했더니: **"모르겠어요 (MAYBE)"**라고 답했습니다. (증명 실패)
  • "핵심 숫자만 보는 방식 (의존 쌍, DP)"으로 해결하려 했더니: **"네, 멈춥니다 (YES)"**라고 확신 있게 답했습니다.
• 이는 연구자의 이론이 실제로도 작동함을 보여줍니다.

5. 안전한 미로 만들기 (Certified Normalizer)

전체 시스템은 멈추지만, 가끔은 "어디로 갈지 두 갈래로 갈라지는" (충돌) 문제가 생길 수 있습니다.

• 연구자들은 **안전한 규칙 (SafeStep)**만 골라낸 작은 미로를 만들었습니다.
• 이 작은 미로에서는 반드시 멈추고, 모든 길이 하나로 합쳐지며 (결합성), 정확한 답을 주는 기계를 직접 만들어 증명했습니다.
• 이 기계는 Lean 4 라는 프로그래밍 언어로 작성되어, 수학적으로 100% 오류가 없음을 컴퓨터가 검증했습니다.

---

📝 요약: 이 논문이 우리에게 주는 메시지

1. 복제는 함정이다: 어떤 시스템에서 물건이 두 개로 복제되면, "전체적인 크기나 무게"를 재는 방식으로는 그 시스템이 멈춘다는 것을 증명할 수 없습니다. (이론적 한계)
2. 핵심은 단순하다: 대신 복제된 쓰레기를 무시하고, **실제로 줄어들고 있는 핵심 요소 (숫자)**만 추적하면 증명할 수 있습니다.
3. 증명은 확실하다: 이 이론은 컴퓨터로 엄밀하게 증명되었으며, 실제 자동 증명 도구로도 검증되었습니다.

한 줄 요약:

"복제되는 미로에서 길을 잃지 않으려면, 복제된 가짜 물건들을 무시하고, 진짜로 줄어드는 숫자만 쫓으세요."

이 연구는 컴퓨터 과학에서 복잡한 시스템이 왜 멈추는지, 그리고 어떤 증명 방법이 실패하는지에 대한 정밀한 지도를 제공한 셈입니다.

기술 요약

1. 연구 배경 및 문제 정의 (Problem)

이 논문은 **1 차원 항 재작성 시스템 (First-Order Rewrite Systems)**에서 **단계 복제 (Step-Duplicating)**를 수행하는 재귀자 (Recursor) 를 다룰 때 발생하는 **전역 지향 장벽 (Global Orientation Barrier)**을 규명합니다.

• 핵심 문제: 재귀 규칙에서 단계 인자 (step argument) 가 복제되어 오른쪽 항 (RHS) 에 두 번 나타나는 경우 (예: $rec(b, s, \delta(n)) \to app(s, rec(b, s, n))$), 기존의 직접적 구성적 측정 (Direct Compositional Measures) 방법론이 시스템의 종결성 (Termination) 을 증명하는 데 실패하는 경계를 발견했습니다.
• 구체적 상황:
  • KO7 계산: 7 개의 생성자 (constructors) 와 8 개의 규칙으로 구성된 최소한의Witness 계산기를 제안했습니다.
  • 조건: 바인딩 연산자 없음, 외부 메모리 (공유) 없음, 객체 수준 공리 없음, 무제한 단계 복제 재귀자가 포함된 시스템.
  • 문제점: 복제된 인자가 app (적용) 생성자 아래에 갇혀 있어 (App Trap), 이 인자는 실제 재귀 카운터로 작용하지 못하지만, 전역 측정 함수는 이 복제된 질량을 모두 합산해야 하므로 측정값이 감소하지 않거나 오히려 증가하는 모순이 발생합니다.

2. 방법론 (Methodology)

저자는 Lean 4를 이용한 기계 검증 (Machine-checked formalization) 과 외부 도구 TTT2를 결합하여 이중 접근 방식을 취했습니다.

1. 기계 검증 (Lean 4, 약 7,000 줄):

   • 불가능성 증명: 두 가지 범주 (Tier 1: 가법적 측정, Tier 2: 추상적 구성 측정) 에 속하는 모든 전역 측정 함수가 복제 재귀 규칙을 엄격하게 지향 (strictly orient) 할 수 없음을 증명했습니다.
   • 안전한 부분집합 (SafeStep) 분석: 전체 시스템의 종결성을 보장하기 위해 가드 (guard) 가 추가된 SafeStep 부분 관계를 정의하고, 이를 위한 **계산 가능한 3 중 사전식 측정 (Triple-lexicographic measure)**을 구성했습니다.
   • 정합성 (Confluence) 및 정규화: 뉴먼의 보조정리 (Newman's Lemma) 를 적용하여 국소적 조인 (local-join) 가 증명된 후 전역 정합성을 확보하고, 총체적 (total) 이며 정합적인 (sound) 정규화 함수를 추출했습니다.
   • 순서형 보정 (Ordinal Calibration): 측정 함수의 상한을 $\epsilon_0$ 미만의 순서형 (구체적으로 $\omega^\omega$) 으로 보정하고, 하한에 대한 surjectivity 를 증명했습니다.

2. 외부 검증 (TTT2/CeTA):

   • 전체 커널 규칙 (가드 없음) 에 대해 TTT2 도구를 사용하여 종결성을 검증했습니다.
   • 비교 실험: 의존 쌍 (Dependency Pairs, DP) 프레임워크와 전역/구성적 방법 (다항식 해석, KBO, 행렬 해석 등) 을 모두 적용하여 결과를 비교했습니다.

3. 주요 기여 (Key Contributions)

1. 전역 지향 장벽의 불가능성 정리 (Impossibility Theorem):

   • Theorem 9.1: 정의된 두 가지 구성적 측정 클래스 (Tier 1, Tier 2) 내의 어떤 측정 함수도 무제한 단계 복제 재귀자를 모든 항 인스턴스에 대해 엄격하게 지향할 수 없음을 기계적으로 증명했습니다.
   • 이는 단순한 실패가 아니라, 복제된 질량을 전역적으로 집계하는 방식의 구조적 한계임을 보여줍니다.

2. 모듈형 탈출구 (Modular Escape) 의 규명:

   • Theorem 9.2: 의존 쌍 (DP) 프레임워크와 **부분항 기준 (Subterm Criterion)**이 이 장벽을 어떻게 우회하는지 증명했습니다.
   • 메커니즘: DP 는 app 생성자를 무시하고 재귀 카운터 (3 번째 인자) 로만 투영 (projection) 합니다. 복제된 단계 인자 $s$는 app 아래에 갇혀 있어 재귀 체인에 참여하지 않으므로, DP 는 이를 "보이지 않는" 것으로 처리하고 재귀 카운터의 감소만 확인하여 종결성을 증명합니다.

3. 인증된 Witness 시스템 (KO7) 및 정규화기:

   • SafeStep: 종결성, 정합성, 정규화기가 모두 기계적으로 검증된 가드된 부분 관계를 제공합니다.
   • 측정 함수: $(\delta\text{-flag}, \kappa_M, \tau)$로 구성된 3 중 사전식 측정 함수를 사용하여 모든 규칙에 대한 감소 증명을 수행했습니다.
   • 정규화기: normalizeSafe 함수는 총체적이고 정합적임이 증명되었습니다.

4. 실험적 검증 및 장벽의 원인 규명:

   • TTT2 테스트 결과, **DP 기반 방법 (YES)**과 **LPO (YES)**는 성공했으나, **다항식 해석, KBO, 행렬 해석 등 전역적 방법 (MAYBE)**은 실패했습니다. 이는 기계 검증된 불가능성 정리와 일치합니다.
   • Ablation Study: 복제를 제거한 선형 재귀자 (Linear Recursor) 에서는 단순한 가법적 측정으로도 종결성이 증명됨을 보여, **복제 (Duplication)**가 장벽의 유일한 원인임을 확인했습니다.

4. 결과 (Results)

• 이론적 결과:
  • 전역적/구성적 측정 방법론은 단계 복제 재귀자가 있는 시스템에서 실패할 수밖에 없음을 증명했습니다.
  • 모듈적 방법 (DP + 부분항 기준) 은 이 장벽을 우회할 수 있음을 보였습니다.
  • KO7 시스템의 전체 종결성은 외부 도구 TTT2 를 통해 확인되었으며, Lean 내에서는 가드된 부분집합 (SafeStep) 에 대해 완전히 검증되었습니다.
• 실용적 결과:
  • Lean 4 로 작성된 7,000 줄 이상의 형식화 코드와 TTT2/CeTA 인증 파일이 공개되었습니다.
  • 모든 규칙에 대한 감소 증명, 뉴먼의 보조정리를 통한 정합성 증명, 정규화기의 총체성/정합성 증명이 sorry 없이 완료되었습니다.
  • 순서형 상한이 $\epsilon_0$ 미만임을 보정하여, 시스템의 복잡도가 매우 낮음을 입증했습니다.

5. 의의 및 중요성 (Significance)

1. 종결성 증명 방법론의 한계 명확화:

   • 기존의 전역적 측정 (Global Aggregation) 방법론이 왜 특정 구조 (복제) 에서 실패하는지에 대한 **정밀한 경계 (Boundary)**를 제시했습니다. 이는 단순한 도구의 한계가 아니라, 측정 함수의 수학적 구조적 제약에서 기인함을 보여줍니다.

2. 모듈형 접근법의 우월성 입증:

   • 복잡한 재귀 시스템에서 **의존 쌍 (Dependency Pairs)**과 부분항 투영이 왜 효과적인지, 그리고 그것이 어떻게 "불필요한 복제 질량"을 제거하여 문제를 단순화하는지를 이론적으로 정립했습니다.

3. 형식 검증의 새로운 표준:

   • 종결성, 정합성, 정규화기, 순서형 보정 등 여러 핵심 속성을 하나의 작은 계산기 (KO7) 에 대해 완전히 기계 검증된 형태로 제공함으로써, 형식적 방법론의 신뢰성을 높였습니다.

4. 복잡도 이론적 통찰:

   • 이 장벽은 절대적인 불완전성 (Gödel의 불완전성 정리 등) 과는 다르며, 방법론적 (Methodological) 한계임을 지적했습니다. 즉, 시스템 자체는 종결되지만, 특정 측정 도구로는 이를 볼 수 없다는 점을 명확히 했습니다.

결론적으로, 이 논문은 단계 복제 재귀자를 가진 시스템에서 전역적 측정 방법론의 근본적인 실패를 증명하고, 모듈형 방법론 (DP) 이 이를 어떻게 해결하는지 기계 검증된 Witness 를 통해 입증한 중요한 연구입니다.