원시재순환기능

Primitive recursive functional

수학 논리학에서 원시 재귀함수는 원시 재귀함수를 상위형 이론으로 일반화한 것이다.그것들은 모든 순수한 유한 형태의 함수의 집합으로 구성된다.

원시적인 재귀 함수들은 증명 이론과 건설적인 수학에서 중요하다.그것들은 쿠르트 괴델이 개발한 직관적 산술의 방언시카 해석의 중심 부분이다.

재귀 이론에서 원시 재귀 함수는 튜링 계산성의 예시인 만큼 원시 재귀 함수는 더 높은 유형의 연산성의 예다.

배경

모든 원시 재귀 기능에는 어떤 종류의 입력을 사용하고 어떤 종류의 출력을 생산하는지 알려주는 유형이 있다.유형 0의 물체는 단순히 자연수일 뿐이며, 입력도 하지 않고 자연수의 집합 N에서 출력을 반환하는 상수함수로도 볼 수 있다.

어떤 두 가지 타입의 σ과 τ에 대해서, σ→τ는 타입 σ의 입력을 취하여 타입 τ의 출력을 반환하는 함수를 나타낸다.따라서 함수 f(n) = n+1은 유형 0→0이다.(0→0)→0→0→(0→0)이 서로 다르며, 관례상 표기법 0→0→0을 가리킨다.유형론의 전문용어에서는 유형 0→0의 객체를 함수라고 하고, 유형 0 이외의 입력물을 취하는 객체를 함수라고 한다.

어떤 두 종류의 σ과 τ에 대해서도 σ×τ형은 순서쌍을 나타내며, 그 중 첫 번째 원소는 σ형을, 두 번째 원소는 τ형을 가지고 있다.예를 들어, 기능 A가 N에서 N까지의 함수 f와 자연수 n을 입력하여 f(n)를 반환한다고 가정해 보자.그러면 A형은 (0 × (0→0)→0형이다.이 형식은 커리어를 사용해 0→(0→0)→0으로 표기할 수도 있다.

(순수)유한형의 집합은 0을 포함하는 유형의 최소 집합이며, ×와 →의 연산에 따라 폐쇄된다.위첨자는 변수 x가τ 특정 유형 τ을 갖는 것으로 가정한다는 것을 나타내기 위해 사용된다. 위첨자는 형식이 맥락에서 명확할 때 생략할 수 있다.

정의

원시 재귀함수는 다음과 같이 유한한 유형의 물체 중에서 가장 작은 집합이다.

  • 상수함수 f(n) = 0은 원시 재귀함수다.
  • 후속 함수 g(n) = n + 1은 원시 재귀 함수다.
  • 모든 타입 type××에 대해 기능 K(xσ, yτ) = x는 원시 재귀 기능이다.
  • 모든 유형 ρ, σ, τ에 대해, 기능
    S(rρ→σ→τ,sρ→σ,tρ) = (r(t))(s)(t)
    원시적 재귀적 기능이다.
  • 어떤 타입의 τ과 f, 그리고 타입 0→τ→τ의 어떤 g에 대해서, 기능 R(f,0→τg)은 다음과 같이 재귀적으로 정의했다.
    R(f,g)(0) = f,
    R(f,g)(n+1) = g(n,R(f,g)(n))
    원시적 재귀적 기능이다.

참고 항목

참조

  • Jeremy Avigad and Solomon Feferman (1999). Gödel's functional ("Dialectica") interpretation (PDF). in S. Buss ed., The Handbook of Proof Theory, North-Holland. pp. 337–405.