Centrala begrepp
원시 재귀 함수는 Martin-Löf 타입 이론(MLTT)에서 Π-타입을 포함하지 않는 유니버스 내에서 정의된 모든 함수로 표현될 수 있다.
Sammanfattning
이 논문은 원시 재귀 함수의 개념을 일반 타입으로 확장하는 것을 보여준다.
주요 내용은 다음과 같다:
-
Primitive Recursive Dependent Type Theory(PRTT)라는 이론을 정의한다. PRTT는 MLTT의 하위 이론으로, 두 개의 유니버스 U0와 U1을 가지며, U0는 Π-타입을 포함하지 않는다.
-
PRTT에서 정의되는 모든 함수 n: N ⊢ f(n) : N은 원시 재귀 함수라는 것을 증명한다. 이를 위해 원시 재귀 함수의 해석을 가지는 sheaf 토포스에 대한 해석을 구성한다.
-
PRTT는 원시 재귀 산술(PRA)에 대한 보수적 확장이다. 따라서 PRTT는 역수학이나 형식 메타이론 분야에서 PRA를 대체할 수 있는 더 표현력 있는 시스템이 될 수 있다.
-
PRTT의 확장으로 유한 귀납 타입, 원시 재귀 구성의 내부 유니버스, 다항식 시간 계산 등을 다룬다.
Statistik
원시 재귀 함수는 유한한 for-loop만을 사용하여 계산할 수 있는 수치 알고리즘이다.
원시 재귀 함수는 모든 계산 가능 함수의 하위 클래스이다.
Martin-Löf 타입 이론(MLTT)은 수학의 기초로 사용될 수 있는 종속 타입 이론이다.
Citat
"We show that restricting the elimination principle of the natural numbers type in Martin-Löf Type Theory (MLTT) to a universe of types not containing Π-types ensures that all definable functions are primitive recursive."
"Our work aims to alleviate this problem by giving a subsystem of MLTT (which is itself the basis for many proof assistants, including Agda, Rocq (née Coq), and Lean), which is conservative over PRA, but is much more expressive (requiring fewer encodings), and which is directly amenable for mechanization."