원시 재귀 함수

Primitive recursive function

계산 가능성 이론에서 원시 재귀 함수(primitive recursive function)는 대략적으로 말하면, 모든 루프"for" 루프컴퓨터 프로그램에 의해 계산될 수 있는 함수입니다(즉, 루프에 들어가기 전에 모든 루프의 반복 횟수의 상한이 결정될 수 있습니다). 원시 재귀 함수는 전체 함수일반 재귀 함수의 엄격한 부분 집합을 형성합니다.

원시 재귀 함수의 중요성은 수론(그리고 더 일반적으로 수학에서)에서 연구되는 대부분의 계산 가능한 함수가 원시 재귀적이라는 사실에 있습니다. 예를 들어 덧셈나눗셈, 계승지수 함수, n번째 소수를 반환하는 함수는 모두 원시 재귀적입니다.[1] 실제로 계산 가능한 함수가 원시 재귀적임을 보여주기 위해서는 시간 복잡도가 입력 크기의 원시 재귀적 함수에 의해 위로 제한된다는 것을 보여주기에 충분합니다.[2] 따라서 원시 재귀적이 아닌 계산 가능한 함수를 고안하는 것은 특별히 쉬운 일이 아닙니다. 몇 가지 예는 아래 § 제한 섹션에 나와 있습니다.

원시 재귀 함수의 집합은 계산 복잡도 이론에서 PR로 알려져 있습니다.

정의.

원시 재귀 함수는 고정된 수의 인수(음성이 아닌 정수: {0, 1, 2, ...})를 사용하고 자연수를 반환합니다. n개의 인수가 필요한 경우 n-ary라고 합니다.

기본적인 원시 재귀 함수는 다음과 같은 공리에 의해 제공됩니다.

  1. 상수 함수 C: 각 자연수 n과 모든 k에 대해 k = =}}\로 정의되는 k-ary 상수 함수는 원시 재귀적입니다.
  2. 후계 함수: 인수의 계승자를 반환하는 1차 계승자 함수 S, 즉 = f + 1 } {=}\ 는 원시 재귀적입니다.
  3. Projection function : For all natural numbers such that , the k-ary function defined by }\ 은(는) 원시 재귀적입니다.

더 복잡한 원시 재귀 함수는 다음과 같은 공리에 의해 주어진 연산을 적용함으로써 얻을 수 있습니다.

  1. 연산자 \circ \,}(대체 연산자라고도 함): m-ary 함수 1 mk-ary 함수 1 x k
  2. 기본 재귀 연산자 ρ: k-arygx,…,x k) g({1x_{k})\,} 및 (k + 2)-ary h, ,…,x k) h(z,{1x_k})\,}:

    해석:

    함수는 0에서 첫 번째 인수의 값까지 for-loop 역할을 합니다. 여기1 x, ..., xk 함께 표시된 f에 대한 나머지 인수는 계산 중에 for-loop에 사용될 수 있지만 for-loop에 의해 불변인 초기 조건의 집합입니다. f를 정의하는 방정식의 오른쪽에 있는 함수 gh는 계산을 수행하는 루프의 몸체를 나타냅니다. 함수 g는 초기 계산을 수행하는 데 한 번만 사용됩니다. 루프의 다음 단계에 대한 계산은 h에 의해 수행됩니다. his의 첫 번째 매개 변수는 for-loop의 인덱스의 "현재" 값을 공급합니다. his의 두 번째 매개 변수는 이전 단계에서 for-loop의 이전 계산 결과를 제공합니다. h에 대한 나머지 매개변수는 앞서 언급한 for-loop의 불변 초기 조건입니다. 계산을 수행하는 데 h에 의해 사용될 수 있지만 h에 의해 자체적으로 변경되지는 않습니다.

원시 재귀 함수는 기본 함수와 이러한 연산을 유한한 횟수로 적용하여 기본 함수에서 얻은 함수입니다.

  • 은(는) 할 때마다 0 0을(는) 반환하는 1진 함수입니다. C )= 입니다
  • 은(는) 입력할 때마다 을(는) 반환하는 1진 함수입니다. 1 ) )= 입니다
  • 은 0진 함수입니다. 즉 상수: 3 = 입니다
  • 1 은(는 자연수의 ID 함수입니다. 1 ) x )=
  • and is the left and right projection on natural number pairs, respectively: and .
  • S S\circ S}는에 2를 추가하는 1진 입니다.∘ S ) ( ) x + 2 (S\ x = x + 2}
  • C 0 10}^{1}}은 ∘ C 0 1) S ( 0 1( C_{0}^{)=S(C_{0}^0)=1}입니다. 즉, C 0 1 0}^{}} C 1 1 {\1}^{1}}은(는) 기능입니다 C S\circ } = C_{1}^{1}}. 비슷한 방식으로, 모든 C 의 구성으로 표현할 수 있습니다

추가

2진 함수 의 정의는 인수의 합을 계산하기 위해 기본 재귀 연산자ρrho}를 사용하여 얻을 수 있습니다. 이를 위해 잘 알려진 방정식들을

"원시적 재귀 함수 용어로 다시 표현"됩니다. ρ(g h) {\gh))}의 정의에서 첫 번째 방정식은 g= 1 1 {\ g =P_1}^{1}}를 하여 ( y) = (y) = y {\Add(0),; the second equation suggests to choose to obtain . 따라서 덧셈 함수는 =ρ(1 , ∘ P 2 3) {\= (1)},circ P_{2}^{3}}로 정의할 수 있습니다. 계산 예로서,

더블링

Given , the 1-ary function doubles its argument, .

곱셈

또한 곱셈은 =ρ 0 P 23 P )) {\=\2}^{3 P_{3}^{3})}로 정의할 수 있습니다. 이렇게 하면 잘 알려진 곱셈 방정식이 재현됩니다.

그리고.

선대

이전 함수는 후속 함수의 "opposite" 역할을 하며 ( = 0{\) =0} 및 (= {\)) =}에 의해 재귀적으로 정의됩니다 원시 재귀적 정의는 =ρC 0 0, =\ 연산 예로서,

절사

제한된 뺄셈 함수("monus"라고도 하며 는 이전 함수에서 정의할 수 있습니다. 방정식을 만족합니다.

재귀는 두 번째 인수에 대해 실행되므로 역 뺄셈의 원시 재귀적 정의인 ) = -. ) = x 그런 다음 재귀는 첫 번째 인수에 대해 실행되므로, =ρ , ∘ P 23) {\=circ P_{2}^{3}}와 같이 원시 재귀 정의를 얻을 수 있습니다. 반대되는 인수 하려면 = ∘(P 2, 연산 예로서,

술어를 숫자 함수로 변환

일부 설정에서는 숫자와 진리 값을 혼합하는 입력 튜플(true는 t, f는 false) 또는 진리 값을 출력으로 생성하는 원시 재귀 함수를 고려하는 것이 자연스럽습니다.[3] 이것은 임의의 고정된 방식으로 숫자로 진리 값을 식별함으로써 달성될 수 있습니다. 예를 들어, 진리값 t는 숫자 1로, 진리값 f는 숫자 0으로 식별하는 것이 일반적입니다. 이 식별이 이루어지면 항상 1 또는 0을 반환하는 집합 A특성 함수는 집합 A에 숫자가 있는지 여부를 알려주는 술어로 볼 수 있습니다. 숫자 기능을 가진 술어의 이러한 식별은 이 글의 나머지 부분에서 가정할 것입니다.

술어 "IS 0"

원시 재귀 술어의 예로, 1차 함수 는 x = x = 인 경우 = 이고 그렇지 않은 경우 = 0 ) = 이 되도록 정의되어야 합니다. =ρ C) {\= C_02}}을(를) 정의함으로써 달성할 수 있습니다. 다음 =ρ C 2)(0) = 0) = 1 0)} =}^{2}(0)=C_}^{0}()=1} 입니다. .

술어 "Less or equal"

x ⟺ x - .= 0 xstackrel {.2진 는) Leq {\ IsZero\Sub}로 정의할 수 있습니다. x 인 경우 ( = y) = 이고 그렇지 않은 경우 ( = y) = 입니다. 계산 예로,

술어 "더 크거나 같음"

의 정의가 얻어지면 반대 술어는 = P ) {\=12})}로 정의할 수 있습니다. 다음 ≥ y {\) = Geq(x) = Leq(y,가 true(더 정확하게는 값이 1)인 경우에만 해당됩니다.

그 때가 아니면

프로그래밍 언어에서 알려진 3-ary if-then else 연산자는 =ρ (22 P ) {\textit {} =2 P_{3}^{4})}로 정의할 수 있습니다. 그런 다음 임의 에 대해

그리고.

즉, z )} {\x y, z(가) 반환되면if-part 가) true이고 그렇지 않으면 다른-part z 이(가) 반환됩니다.

교차점

함수를 기반으로 논리적 접합부를 쉽게 정의할 수 있습니다. For example, defining , one obtains , that is, is true if, 가 모두 참인 경우에만 해당됩니다(x{\x} y{\y}의 logical 결합).

마찬가지로 = C P ) {\=}), 2}^{}} = ∘ C0 1, C 1) {\=1}^{1}}, C_{0}^{1},은(는) 적절한 불일치 및 부정의 정의로 이어집니다. (y ( y )} = {\ = ( 0 ) = {\

등식 술어

위의 함수 를) 사용하여 정의 = ) {\ = AndLeq,Geq)}이 등식 술어를 구현합니다. = ( = 는 x 가 같은 경우에만 참입니다

마찬가지로, = {\ = circ Geq} 정의는 술어 ""을 구현하고, = ∘ Leq {\ = Not\circ Leq} 는 "greater-than"을 구현합니다.

기타 자연수 연산

지수화원시성 테스트는 원시 재귀적입니다. 원시 재귀 함수 e, f, g h가 주어지면 e≤f일g의 값을 반환하고 그렇지 않으면 h의 값이 원시 재귀적인 함수입니다.

정수와 유리수에 대한 연산

괴델 수를 사용하면 원시 재귀 함수를 정수 및 유리수와 같은 다른 개체에서 작동하도록 확장할 수 있습니다. 정수가 괴델 수에 의해 표준적인 방식으로 부호화된다면 덧셈, 뺄셈, 곱셈을 포함한 산술 연산은 모두 원시 재귀적인 것입니다. 마찬가지로 유리수가 괴델 수로 표현되면 필드 연산은 모두 원시 재귀적입니다.

몇 가지 일반적인 원시 재귀 함수

다음 예시와 정의는 Kleene (1952) pp. 223–231. 많은 사람들이 증명과 함께 나타납니다. 대부분은 증명 또는 예로서 유사한 이름으로 불로스-부르제-제프리 2002 pp. 63–70에서 나타나는데, 정확한 도출에 따라 로그 lo(x, y) 또는 lg(x, y)를 추가합니다.

다음에서 "", 예를 들어 "a"는 "후계자"를 의미하는 원시 표식으로, 일반적으로 "+1"로 간주됩니다. 예를 들어 "a +1 = a"입니다. 함수 16-20과 #G는 원시 재귀 술어를 괴델 수로 표현되는 "수학적" 형태로 변환하고 이를 추출하는 것과 관련하여 특히 중요합니다.

  1. 덧셈: a+b
  2. 곱셈: axb
  3. 지수화b: a
  4. 요인 a! : 0! = 1, a'! = a!xa'
  5. pred(a): (전치 또는 감소): a > 0이면 a-1 아니면 0
  6. 적절한 뺄셈 a ∸ b: 만약 a ≥ b이면 a-belse 0
  7. 최소값(a1, ...an)
  8. 최대값(a1, ...an)
  9. 절대차: a-b = (a ∸ b) + (b ∸ a)
  10. ~sg(a):NOT[signum(a)]: a=0이면 1이 아니면 0
  11. sg(a): signum(a): a = 0이면 0 아니면 1
  12. b: (a divides b): 만약 어떤 k에 대하여 b=k×a이면 0이 아니면 1
  13. 나머지(a, b): b가 "짝수"를 나누지 않는 경우 남은 것. MOD(a, b)라고도 함
  14. a = b: sg a - b (클라인의 관례는 true를 0으로, false를 1로 표현하는 것이었습니다; 현재, 특히 컴퓨터에서, 가장 일반적인 관례는 그 반대입니다. 즉, true를 1로, false를 0으로 표현하는 것으로, 이것은 sg를 여기와 다음 항목에서 ~sg로 바꾸는 것에 해당합니다.)
  15. a < b: sg( a' ∸ b )
  16. Pr(a): a는 소수 Pr(a) = a>1 & NOT(존재하는 c) [ca]
  17. pi: i+1번째 소수
  18. (a):i pini a의 지수 : paix & NOT(paix')가 되는 고유 x
  19. lh(a): a의 "길이" 또는 사라지지 않는 지수의 수
  20. lo(a, b): (기저 b에 대한 a의 logar): 만약 a, b > 1이면 b가x 0이 되는 가장 큰 x
다음에서 약어 x = x, ... xn; 의미가 필요한 경우 첨자가 적용될 수 있습니다.
  • #A: 함수 ψ 및 상수 q, ... q는 ψ에서 원시 재귀적입니다.
  • #B: 유한합 σ ψ(x, y) 및 곱 π ψ(x, y)는 ψ적으로 원시 재귀적입니다.
  • #C: 술어 Q의 각 변수에 대한 함수 χ,..., χ, Q를 대입한 술어 P는 χ,..., χ, Q에서 원시 재귀적입니다.
  • #D: Q와 R에서 원시 재귀적으로 사용되는 술어는 다음과 같습니다.
  • NOT_Q(x).
  • Q OR R: Q(x) V R(x),
  • Q AND R: Q(x) & R(x),
  • Q IMPLIES R: Q(x) → R(x)
  • Q is equivalent to R: Q(x) ≡ R(x)
  • #E: 다음 술어들은 술어 R에서 원시 재귀적입니다.
  • (Ey)y<z R(x, y) 여기서 (Ey)y<z는 "z보다 작은 y가 적어도 하나 존재하여 그러한 것"을 나타냅니다.
  • (y)y<zRy<z(x, y) 여기서 (y)y<z는 "z보다 작은 모든 것에 대해 그것은 사실이다"를 나타냅니다.
  • μyy<z R(x, y). 연산자 μyy<z R(x, y)는 소위 최소화 연산자 또는 mu 연산자의 유계 형태입니다. "R(x, y)가 참이 되도록 z보다 작은 y 값 또는 그러한 값이 없는 경우 z"로 정의됩니다.
  • #F: 사례별 정의: 따라서 정의된 함수는 Q, ..., Q가 상호 배타적 술어(또는 "ψ(x))는 φ, ..., Q, ... Q에서 원시 재귀적입니다.
φ(x) =
  • φ1(x) if Q1(x) is true,
  • . . . . . . . . . . . . . . . . . . .
  • φm(x) if Qm(x) is true
  • φ(x) 그렇지 않으면
  • #G: φ이 다음 식을 만족하는 경우:
φ(y,x) = χ(y, COURSE-φ(y; x2, ... xn ), x2, ... x 그러면 φ는 χ에서 원시 재귀적입니다. Course-of-value 함수의 Course- φ(y; x) 값은 원래 함수의 φ(0,x), ..., φ(y-1,x) 의 시퀀스를 인코딩합니다.

재귀 함수와의 관계

부분 재귀 함수의 광범위한 클래스는 무제한 검색 연산자를 도입하여 정의됩니다. 이 연산자를 사용하면 부분 함수, 즉 각 인수에 대해 최대 하나의 값을 갖는 관계가 발생할 수 있지만 반드시 모든 인수에 대해 을 갖는 것은 아닙니다(도메인 참조). 동등한 정의는 부분 재귀 함수가 튜링 기계에 의해 계산될 수 있는 함수라는 것입니다. 전체 재귀 함수는 모든 입력에 대해 정의되는 부분 재귀 함수입니다.

모든 원시 재귀 함수는 완전 재귀 함수이지만 모든 전체 재귀 함수가 원시 재귀 함수인 것은 아닙니다. 아커만 함수 A(m,n)는 원시 재귀적이 아닌 총 재귀적 함수(사실은 증명 가능한 총합)의 잘 알려진 예입니다. 애커만 함수를 사용하여 전체 재귀 함수의 부분 집합으로 원시 재귀 함수의 특성이 있습니다. 이 특성화는 함수가 항상 A(m,n) 이하의 단계 내에서 중단되는 튜링 기계에 의해 계산될 수 있는 자연수 m이 있는 경우에만 함수가 원시 재귀적이라는 것을 나타냅니다. 여기서 n은 원시 재귀적 함수의 인수의 합입니다.[4]

원시 재귀 함수의 중요한 속성은 모든 전체 재귀 함수 집합의 재귀적으로 열거 가능한 부분 집합이라는 것입니다(자체적으로 재귀적으로 열거 가능하지 않음). 즉, 원시 재귀 함수를 열거하는 단일 계산 가능 함수 f(m,n)가 있음을 의미합니다.

  • 모든 원시 재귀 함수 g에 대하여, 모든 n에 대하여 g(n) = f(m,n)인 m이 존재하며,
  • 모든 m에 대하여 함수 h(n) = f(m,n)는 원시 재귀적입니다.

f는 원시 재귀 함수를 만드는 가능한 모든 방법을 반복적으로 반복함으로써 명시적으로 구성할 수 있습니다. 따라서, 그것은 증명할 수 있는 완전한 것입니다. 대각선화 인수를 사용하여 f가 그 자체로 재귀적 원시가 아님을 보여줄 수 있습니다. 만약 그렇다면 h(n) = f(n,n)+1도 마찬가지일 것입니다. 그러나 이것이 어떤 원시 재귀 함수와 같다면, 모든 n에 대해 h(n) = f(m,n), 그리고 h(m) = f(m,m)가 되어 모순을 초래하는 m이 있습니다.

그러나 원시 재귀 함수의 집합은 모든 전체 재귀 함수의 집합에서 가장 큰 재귀적으로 열거 가능한 부분 집합이 아닙니다. 예를 들어, 이론의 모든 증명을 열거할 수 있기 때문에 (페아노 산술의) 증명 가능한 총 함수 집합도 재귀적으로 열거할 수 있습니다. 모든 원시 재귀 함수는 총합을 증명할 수 있지만 그 반대는 사실이 아닙니다.

한계

원시 재귀 함수는 계산 가능한 함수가 무엇이어야 하는지에 대한 우리의 직관과 매우 밀접하게 일치하는 경향이 있습니다. 확실히 초기 함수는 직관적으로 계산할 수 있으며(매우 간단합니다), 새로운 원시 재귀 함수를 생성할 수 있는 두 가지 연산도 매우 간단합니다. 그러나 원시 재귀 함수의 집합이 모든 가능한 총 계산 가능 함수를 포함하는 것은 아닙니다. 이는 칸토어의 대각 논법의 변형에서 볼 수 있습니다. 이 인수는 원시 재귀적이 아닌 전체 계산 가능 함수를 제공합니다. 증명의 스케치는 다음과 같습니다.

하나의 인수의 원시 재귀 함수(즉, 단항 함수)는 계산 가능하게 열거될 수 있습니다. 이 열거는 원시 재귀 함수(구성 및 원시 재귀 연산을 연산자로 하는 표현과 기본 원시 재귀 함수를 원자로 하는 표현)의 정의를 사용하며, 모든 정의를 한 번 포함하는 것으로 가정할 수 있습니다. 동일한 함수가 목록에서 여러 번 발생하더라도 (많은 정의가 동일한 함수를 정의하기 때문에; 실제로 단순히 항등 함수에 의해 구성되는 것은 하나의 원시 재귀 함수에 대해 무한히 많은 정의를 생성합니다. 이는 이 열거에서 원시 재귀 함수의 n번째 정의가 n으로부터 효과적으로 결정될 수 있음을 의미합니다. 실제로 어떤 사람이 괴델 번호를 사용하여 정의를 숫자로 인코딩하면 목록에서 이 n번째 정의는 n의 원시 재귀 함수에 의해 계산됩니다. 이 정의에 의해 주어지는 일항 원시 재귀 함수를 f라고n 하자.

이제 ev(i,j) = f(j)로 두 개의 인수로 "evaluator 함수" ev를 정의합니다. fi 정의를 효과적으로 결정할 수 있기 때문에 ev는 분명히 전체적이고 계산 가능하며 원시 재귀 함수 fi 그 자체로 전체적이고 계산 가능하므로 f(j)i 항상 정의되고 효과적으로 계산 가능합니다. 그러나 대각선 인수는 두 인수의 함수 ev가 원시 재귀적이 아님을 보여줍니다.

ev가 원시 재귀적이라면, g(i) = S(ev(i,i))에 의해 정의되는 단항 함수 g도 후계 함수와 ev의 합성에 의해 정의되는 것처럼 원시 재귀적일 것입니다. 그러나 g는 열거에서 발생하므로 g = f와 같은 숫자 n이 있습니다. But now g(n) = S(ev(n,n)) = S(fn(n)) = S(g(n)) gives a contradiction.

인수는 항상 중단되는 Machine 기사에 설명되어 있듯이 이러한 방식으로 열거할 수 있는 모든 계산 가능(총) 함수 클래스에 적용할 수 있습니다. 그러나 부분 계산 가능 함수(모든 인수에 대해 정의할 필요가 없는 함수)는 예를 들어 튜링 기계 인코딩을 열거함으로써 명시적으로 열거할 수 있습니다.

원시 재귀 함수가 아닌 전체 재귀 함수의 다른 예는 알려져 있습니다.

변종

상수 함수

정의에서는 대신 0진 영함수 C 만 항상 0을 반환하는 원시 함수로 사용하고 영함수, 후계 함수 및 합성 연산자로부터 상수 함수를 구축합니다.

약한 원시 재귀

1자리 이전 함수는 원시 재귀적입니다. 섹션 #이전을 참조하십시오. Fischer, Fischer & Beigel[5] 은 암묵적인 이전 규칙을 재귀 규칙에서 제거하고 약한 규칙으로 대체했습니다.

그들은 이전 함수가 여전히 정의될 수 있다는 것을 증명했고, 따라서 "약한" 원시 재귀도 원시 재귀 함수를 정의한다는 것을 증명했습니다.

반복 함수

rity k+1의 h 을(를) 사용하여 를 h 의 인수에서 완전히 제거하면 반복 규칙을 얻을 수 있습니다.

반복 함수의 클래스는 이 약한 규칙을 제외하고 원시 재귀 함수의 클래스와 동일하게 정의됩니다. 이들은 원시 재귀 함수의 적절한 하위 집합으로 추측됩니다.[5]

추가 원시 재귀적 형태

일부 추가적인 재귀 형태는 사실상 원시 재귀적인 함수를 정의하기도 합니다. 이러한 형태의 정의는 읽기 또는 쓰기에 더 쉽게 찾을 수 있거나 더 자연스러울 수 있습니다. 의 코스 재귀는 원시 재귀 함수를 정의합니다. 상호 재귀의 일부 형태는 원시 재귀 함수를 정의하기도 합니다.

LOOP 프로그래밍 언어로 프로그래밍할 수 있는 함수는 정확히 원시 재귀 함수입니다. 이것은 이러한 기능의 힘에 대한 다른 특성을 제공합니다. 튜링-완전 언어와 비교하여 LOOP 언어의 주요 한계는 루프가 실행되기 전에 각 루프가 실행될 횟수가 LOOP 언어에서 지정된다는 것입니다.

컴퓨터 언어 정의

원시 재귀 프로그래밍 언어의 예로는 기본 연산자(예: + 및 - 또는 ADD 및 SUBT), 조건 및 비교(IF-THEN, EQUERS, LESS-THAN), 경계 루프(예: 모든 루프에 알려진 또는 계산 가능한 상한이 있는 경우)가 있습니다. 루프 바디에 의해 변경할 수도 없고 변경할 수도 없습니다. 루프나 IF-THEN + GOTO와 같이 더 일반적인 제어 구조는 원시 재귀 언어로 허용되지 않습니다.

1967년 알버트 알의 논문에서 소개된 루프 언어. 마이어데니스 M. 리치,[6] 그런 언어예요. 컴퓨팅 성능은 원시 재귀 함수와 일치합니다. LOOP 언어의 변형은 괴델, 에셔, 바흐에 있는 더글러스 호프스태터BloP입니다. 무한 루프(WHILE, GOTO)를 추가하면 모든 실제 컴퓨터 프로그래밍 언어와 마찬가지로 언어가 일반적으로 재귀적이고 튜링이 완전합니다.

원시 재귀 함수의 정의는 모든 입력(한정된 수의 단계 후)에서 계산이 중단된다는 것을 의미합니다. 반면, 일반적인 재귀 함수의 경우 정지 문제결정할 수 없습니다.

유한성과 일관성 결과

원시 재귀 함수는 수학적 유한성과 밀접한 관련이 있으며 특히 건설적인 시스템이 필요한 수학 논리의 여러 맥락에서 사용됩니다. 자연수와 그 위의 원시 재귀 함수에 대한 형식적 공리 체계인 원시 재귀 산술(PRA)은 종종 이 목적을 위해 사용됩니다.

PRA는 유한 체계가 아닌 페아노 산술보다 훨씬 약합니다. 그럼에도 불구하고이론증명 이론에서 많은 결과를 PRA에서 증명할 수 있습니다. 예를 들어, 괴델의 불완전성 정리는 PRA로 공식화되어 다음과 같은 정리를 제공할 수 있습니다.

T가 괴델 문장 G와 함께 특정 가설을 만족하는 산술 이론이라면 PRA는 Con(T)→G라는 함의를 증명합니다.

마찬가지로, 증명 이론의 많은 구문 결과는 PRA에서 증명될 수 있으며, 이는 증명의 해당 구문 변환을 수행하는 원시 재귀 함수가 있음을 의미합니다.

증명론과 집합론에서는 유한적 일관성 증명, 즉 그 자체가 유한적으로 허용 가능하다는 일관성 증명에 관심이 있습니다. 그러한 증명은 S의 불일치에 대한 모든 증명을 T의 불일치에 대한 증명으로 변환할 수 있는 원시 재귀 함수를 생성함으로써 이론 T의 일관성을 의미한다는 것을 확립합니다. 일관성 증명이 유한하기 위한 한 가지 충분한 조건은 PRA에서 공식화할 수 있는 능력입니다. 예를 들어, 강제로 얻은 집합 이론의 많은 일관성 결과는 PRA에서 공식화할 수 있는 구문 증명으로 재구성될 수 있습니다.

역사

재귀적 정의는 이전에 수학에서 다소 형식적으로 사용되었지만 원시 재귀의 구성은 리처드 데데킨드의 그의 "신드와 솔렌 다이 자흘렌?"(1888) 정리 126으로 거슬러 올라갑니다. 이 연구는 특정 재귀적 구조가 고유 함수를 정의한다는 증거를 최초로 제시한 것입니다.[7][8][9]

원시 재귀 산술은 1923년 토랄 스콜렘[10] 의해 처음으로 제안되었습니다.

현재의 용어는 1928년 아커만이 오늘날 그의 이름을 딴 함수가 원시 재귀 함수가 아니라는 것을 증명한 후 Rózsa Péter (1934)에 의해 만들어졌으며, 이 사건으로 인해 그때까지 단순히 재귀 함수라고 불렸던 것의 이름을 바꾸어야 했습니다.[8][9]

참고 항목

메모들

  1. ^ 브레이너드 앤드 랜드베버(Brainerd and Landweber, 1974)
  2. ^ 하트매니스, 1989
  3. ^ Kleene [1952 pp. 226–227]
  4. ^ 이것은 이 형태의 함수가 가장 빠르게 성장하는 원시 재귀 함수이며, 함수가 시간 복잡도가 원시 재귀 함수에 의해 제한되는 경우에만 원시 재귀 함수라는 사실에서 비롯됩니다. 전자의 경우 참조 Linz, Peter (2011), An Introduction to Formal Languages and Automata, Jones & Bartlett Publishers, p. 332, ISBN 9781449615529후자의 Linz, Peter (2011), An Introduction to Formal Languages and Automata, Jones & Bartlett Publishers, p. 332, ISBN 9781449615529경우 참조
  5. ^ a b Fischer, Fischer & Beigel 1989.
  6. ^ Meyer, Albert R.; Ritchie, Dennis M. (1967). The complexity of loop programs. ACM '67: Proceedings of the 1967 22nd national conference. doi:10.1145/800196.806014.
  7. ^ Peter Smith (2013). An Introduction to Gödel's Theorems (2nd ed.). Cambridge University Press. pp. 98–99. ISBN 978-1-107-02284-3.
  8. ^ a b George Tourlakis (2003). Lectures in Logic and Set Theory: Volume 1, Mathematical Logic. Cambridge University Press. p. 129. ISBN 978-1-139-43942-8.
  9. ^ a b Rod Downey, ed. (2014). Turing's Legacy: Developments from Turing's Ideas in Logic. Cambridge University Press. p. 474. ISBN 978-1-107-04348-0.
  10. ^ 소랄프 스콜렘 (1923) 장 반 하이에노르트의 "초등 산술의 기초", 번역가와 편집. (1967) 프레게에서 괴델까지: 수학 논리학의 원천 책, 1879-1931. 하버드 대학교 누름: 302-33.

참고문헌