Carryless Pairing: Additive Pairing in the Fibonacci Basis

기술적 요약: 피보나치 기저에서의 자리옮김 없는 쌍 만들기

문제 제기
본 논문은 제크endorf(피보나치) 기저의 덧셈적 제약 조건 내에서 엄격하게 작동하는 쌍 만들기 함수 $\pi: \mathbb{N}^2 \to \mathbb{N}$의 구성을 다룹니다. 전통적인 쌍 만들기 방식들은 종종 위치 기반의 자리수 교차 (예: Z-순서/모orton 코드) 나 곱셈과 소인수분해를 포함한 산술 연산 (예: 괴델 번호 매기기, 칸토어 쌍 만들기) 에 의존합니다. 저자는 곱셈, 지수 연산, 그리고 데이터 결합 중 '자리옮김 (carry)' 전파나 정규화 단계의 필요성을 피하면서, 쌍 $(x, y)$의 인코딩과 디코딩이 오직 지지 집합 추출과 덧셈 연산에만 의존하는 메커니즘을 모색합니다. 이는 곱셈이 가정되지 않거나 비용이 큰 약한 산술 기저 (예: $I\Delta_0$) 에서 불완전성 논증과 증명론적 조사를 지원하려는 동기에 기인합니다.

방법론
제안된 솔루션인 자리옮김 없는 쌍 만들기($\pi_{CL}$) 는 제크endorf 지지 집합에 기반하여 두 자연수를 피보나치 인덱스의 서로 다른 '대역'으로 인코딩합니다.

1. 제크endorf 표현: 모든 자연수 $n$은 $k \ge 2$인 연속되지 않는 피보나치 수 $F_k$들의 합으로 유일하게 표현됩니다. 인덱스 집합은 $Z(n)$으로 표기합니다.
2. 구분자 구성: 쌍 $(x, y)$에 대해, 알고리즘은 먼저 $F_{r(x)} > x$를 만족하는 가장 작은 인덱스로 정의된 순위 $r(x)$를 계산합니다. 구분자 $B(x)$는 $2r(x)$로 설정됩니다.
3. 대역 분리:
   • 짝수 대역 ($x$용): $x$의 지지 집합 $Z(x)$의 인덱스는 $e \mapsto 2e$를 통해 짝수 인덱스로 매핑됩니다. 이들은 범위 $[4, 2r(x))$에 배치됩니다.
   • 홀수 대역 ($y$용): $y$의 지지 집합 $Z(y)$의 인덱스는 $j \mapsto B(x) + (2j - 1)$을 통해 홀수 인덱스로 매핑됩니다. 이들은 구분자 $B(x)$보다 엄격히 위에 배치됩니다.
4. 자리옮김 없는 불변성: $Z(x)$는 연속된 정수를 포함하지 않으므로, 매핑된 짝수 인덱스 사이에는 최소 4 의 간격이 존재합니다. 마찬가지로 매핑된 홀수 인덱스 사이에도 최소 4 의 간격이 존재합니다. 중요하게도, 구분자 $B(x)$는 $x$가 사용하는 가장 높은 짝수 인덱스가 $y$가 사용하는 가장 낮은 홀수 인덱스보다 엄격히 작음을 보장합니다. 결과적으로, 이러한 두 인덱스 집합의 합집합은 연속된 정수를 포함하지 않습니다.
5. 인코딩: 인코딩된 값은 이러한 인덱스들의 합집합에 대응하는 피보나치 수들의 합입니다. 지지 집합이 연속된 인덱스를 포함하지 않으므로, 결과는 자동으로 제크endorf 정규 형태가 됩니다. 자리옮김 전파가 필요하지 않습니다.

주요 기여

• 완전한 덧셈 장치: 논문은 제크endorf 지지 집합에 덧셈과 유계 스캔만을 사용하여 작동하는 쌍 만들기 사상 $\pi_{CL}$과 역 사상 unpair를 정의합니다. 곱셈이나 소인수분해는 사용되지 않습니다.
• 단사성과 결정 가능성: 해당 사상은 단사적임이 증명되었습니다. 전사는 아니지만, 이미지 소속 여부는 '고정점 테스트'를 통해 결정 가능합니다: 자연수 $n$이 이미지에 속할 필요충분조건은 $\pi_{CL}(\text{unpair}(n)) = n$인 것입니다.
• 한 단계 정규화: 논문은 정규화 함수 $can(n) = \pi_{CL}(\text{unpair}(n))$을 도입합니다. 이 함수는 임의의 자연수를 $\pi_{CL}$의 이미지 내 유일한 대표자로 한 단계에 매핑합니다.
• 안정성 보조정리: 논문은 $x$가 고정된 상태에서 두 번째 좌표 $y$를 수정 (지지 집합에서 인덱스 추가 또는 제거) 하는 것이 인코딩된 값에 지역적 변화 (특정 피보나치 수의 추가 또는 차감) 를 초래함을 확립합니다.
• 기계화: 모든 핵심 정확성 정리 (역 사상과 단사성) 는 갈리나 (Gallina) 명세 언어를 사용하여 Rocq(이전 Coq) 에서 기계화되었습니다. 형식화에는 지지 집합의 존재성과 유일성에 대한 증명이 포함되어 있어, 쌍 만들기 장치가 지지 인터페이스에 관한 증명되지 않은 공리에 의존하지 않도록 보장합니다.

결과

• 정확성: 정리 6.0.1 은 unpair $\circ$ $\pi_{CL}$이 $\mathbb{N}^2$에서 항등 함수임을 증명합니다.
• 비전사성: 해당 사상은 전사가 아닙니다. 많은 자연수 (예: 6) 는 제크endorf 지지 집합이 특정 패리티와 구분자 제약 조건과 일치하지 않기 때문에 이 방식 하에서 유효한 쌍에 대응하지 않습니다.
• 복잡도: 쌍 만들기와 역쌍 만들기의 비용은 지지 집합 추출 단계 (일반적으로 탐욕적 스캔에 대해 $O(r(n))$) 에 의해 지배됩니다. 논문은 이러한 것들이 인증된 복잡도 정리라기보다는 비공식적 관찰임을 명시합니다.
• 비교: 괴델 번호 매기기 (소인수분해 필요) 나 칸토어 쌍 만들기 (곱셈과 제곱근 필요) 와 달리, $\pi_{CL}$은 순수하게 덧셈적으로 작동합니다. Z-순서 (고정된 이진 위치를 교차) 와 달리, $\pi_{CL}$은 첫 번째 피연산자의 순위에 기반하여 두 번째 피연산자의 위치를 이동시켜 동적 구분자를 생성합니다.

의의와 주장
본 논문은 이 구성을 역수학과 약한 산술 기저 연구의 도구로 위치시킵니다. 곱셈을 피하는 쌍 만들기 함수를 제공함으로써, 저자는 곱셈이 사용 불가능하거나 제한된 시스템에서의 일관성 논증과 증명 가능성 조사를 위해 유용할 수 있음을 시사합니다 (Buss, 1997; Friedman, 1976 참조).

저자는 더 넓은 함의에 대해 겸손함을 명시적으로 밝힙니다:

• 논문은 덧셈 전용 원칙으로부터 제크endorf 지지 집합 인터페이스 자체를 유도한다고 주장하지 않으며, 그러한 유도가 존재하지 않을 수 있다고 추측합니다.
• $\pi_{CL}$의 이미지에 대한 간단한 폐쇄형 특징화를 주장하지 않습니다; 결정 절차는 지지 기반 고정점 테스트입니다.
• 주요 기여는 '자리옮김 없는' 장치의 명시적 구성과 그 속성 검증이며, 이를 통해 이미지와 그 기하학적 구조가 이론적 분석을 위해 직접 검사 가능하게 만듭니다.

이 작업은 일반적인 컴퓨팅을 위한 실용적 자료 구조라기보다는 기초 산술 장치로 제시되며, 논리와 증명 이론에서의 이론적 유용성을 강조합니다.