클레이니 재귀 정리

계산 가능성 이론에서 클레이니 재귀 정리()는 계산 가능 함수가 자신에 대한 설명에 적용되는 방식에 대한 근본적인 결과 두 가지이다. 이 정리들은 스티븐 클레이니가 1938년에 처음 증명했으며 1952년 저서 《메타수학 서론》(Introduction to Metamathematics)에 실렸다. 계산 가능 함수의 고정점을 구성하는 관련 정리는 로저스의 정리(Rogers's theorem)로 알려져 있으며 하틀리 로저스 주니어의 업적이다.

재귀 정리는 계산 가능 함수에 대한 특정 연산의 고정점을 구성하고, 콰인을 생성하며, 재귀적 정의를 통해 정의된 함수를 구성하는 데 적용될 수 있다.

 표기법 
정리의 진술은 부분 재귀 함수의 허용 가능한 번호 매기기 를 참조하며, 색인 에 해당하는 함수는 이다.

와 가 자연수에 대한 부분 정의 함수일 때,  표기는 각 n에 대해 과 이 모두 정의되고 같거나, 또는 과 이 모두 정의되지 않았음을 나타낸다.

 로저스의 고정점 정리 
함수 가 주어졌을 때, 의 고정점은 인 색인 이다. 여기서 입력과 출력의 비교는 수치적 값이 아니라 관련 함수에 대한 것임을 유의해야 한다.

로저스는 다음 결과를 클레이니의 (두 번째) 재귀 정리의 "더 간단한 버전"으로 설명한다.

이는 본질적으로 우리가 프로그램에 효율적인 변환(예: 후속, 점프와 같은 명령을 바꾸거나, 줄을 제거하는 등)을 적용한다면, 항상 동작이 변환에 의해 변경되지 않는 프로그램이 존재한다는 것을 의미한다. 따라서 이 정리는 다음과 같이 해석될 수 있다. "프로그램을 변환하는 효과적인 절차가 주어지면, 그 절차에 의해 수정되었을 때 이전에 했던 작업을 정확히 수행하는 프로그램이 항상 존재한다" 또는 "모든 프로그램의 확장적 동작을 변경하는 프로그램을 작성하는 것은 불가능하다".

 고정점 정리의 증명 
증명은 다음과 같이 정의된 특정 전체 계산 가능 함수 를 사용한다. 자연수 가 주어졌을 때, 함수 는 다음 계산을 수행하는 부분 계산 가능 함수의 색인을 출력한다.
입력 가 주어지면, 먼저 를 계산한다. 이 계산이 출력 를 반환하면, 를 계산하고 그 값을 반환한다 (만약 있다면).
따라서 부분 계산 가능 함수의 모든 색인 에 대해, 가 정의되면 이다. 만약 가 정의되지 않았다면, 는 어디에서도 정의되지 않은 함수이다. 함수 는 위에서 설명한 부분 계산 가능 함수 와 s-m-n 정리로부터 구성될 수 있다. 즉, 각 에 대해 는 함수 를 계산하는 프로그램의 색인이다.

증명을 완성하기 위해, 를 임의의 전체 계산 가능 함수로 두고, 위와 같이 를 구성한다. 의 색인을 라고 하자. 이는 전체 계산 가능 함수이다. 그러면 의 정의에 의해 이다.
그러나 가 의 색인이므로 이고, 따라서 이다. 의 전이성에 의해, 이는 를 의미한다. 그러므로 에 대해 이다.

이 증명은 Y 조합자를 구현하는 부분 재귀 함수의 구성이다.

 고정점이 없는 함수 
모든 에 대해 인 함수 를 고정점이 없는 함수라고 한다. 고정점 정리는 어떤 전체 계산 가능 함수도 고정점이 없을 수 없음을 보여주지만, 계산 불가능한 고정점이 없는 함수는 많이 존재한다. 아르슬라노프의 완전성 기준은 고정점이 없는 함수를 계산하는 유일한 재귀적으로 열거 가능한 튜링 차수는 정지 문제의 차수인 0′라고 명시한다.

 클레이니의 두 번째 재귀 정리 
두 번째 재귀 정리는 함수에 두 번째 입력이 있는 로저스의 정리의 일반화이다. 두 번째 재귀 정리의 비공식적인 해석 중 하나는 자기 참조 프로그램을 구성하는 것이 가능하다는 것이다. 아래 "콰인에 대한 적용"을 참조하라.

두 번째 재귀 정리. 어떤 부분 재귀 함수 에 대해서도 인 색인 가 존재한다.

이 정리는 를 와 같은 함수로 두면 로저스의 정리로부터 증명할 수 있다(S-m-n 정리에 의해 설명된 구성). 그런 다음 이 의 고정점이 필요한 색인 임을 확인할 수 있다. 이 정리는 구성적이다. 즉, 고정된 계산 가능 함수가 에 대한 색인을 로 매핑한다.

 로저스 정리와의 비교 
클레이니의 두 번째 재귀 정리와 로저스의 정리는 서로를 통해 비교적 간단하게 증명될 수 있다. 그러나 클레이니 정리의 직접적인 증명은 보편적인 프로그램을 사용하지 않는다. 이는 보편적인 프로그램이 없는 특정 하위 재귀 프로그래밍 시스템에도 이 정리가 적용된다는 것을 의미한다.

 콰인에 대한 적용 
두 번째 재귀 정리를 사용하는 고전적인 예시는 함수 이다. 이 경우 해당하는 색인 는 어떤 값에 적용되든 자신의 색인을 출력하는 계산 가능 함수를 생성한다. 컴퓨터 프로그램으로 표현될 때, 이러한 색인들은 콰인으로 알려져 있다.

다음 Lisp 예시는  함수로부터 따름정리의 가 어떻게 효과적으로 생성될 수 있는지를 보여준다. 코드의 s11 함수는 S-m-n 정리에 의해 생성된 해당 이름의 함수이다.

Q는 임의의 두 인자 함수로 변경될 수 있다.
(setq Q '(lambda (x y) x))
(setq s11 '(lambda (f x) (list 'lambda '(y) (list f x 'y))))
(setq n (list 'lambda '(x y) (list Q (list s11 'x 'x) 'y)))
(setq p (eval (list s11 n n)))

다음 표현식의 결과는 동일해야 한다.  p(nil)
(eval (list p nil))
Q(p, nil)
(eval (list Q p nil))

 재귀의 제거에 대한 적용 
와 가 함수 에 대한 재귀 정의에 사용되는 전체 계산 가능 함수라고 가정해 보자.

두 번째 재귀 정리는 이러한 방정식들이 계산 가능 함수를 정의한다는 것을 보여주는 데 사용될 수 있다. 여기서 계산 가능성의 개념은 우선적으로 재귀 정의를 허용할 필요가 없다(예를 들어, 뮤-재귀나 튜링 기계에 의해 정의될 수 있다). 이 재귀 정의는 재귀를 시뮬레이션하기 위해 가 자신에 대한 색인이라고 가정하는 계산 가능 함수 로 변환될 수 있다.

재귀 정리는 인 계산 가능 함수 의 존재를 확립한다. 따라서 는 주어진 재귀 정의를 만족시킨다.

 반사적 프로그래밍 
반사적(reflective) 프로그래밍은 프로그램에서 자기 참조를 사용하는 것을 의미한다. 존스(Jones)는 반사적 언어를 기반으로 한 두 번째 재귀 정리의 관점을 제시한다.
정의된 반사적 언어가 반사 기능이 없는 언어보다 강력하지 않음이 입증된다(반사적 언어용 인터프리터를 반사 기능을 사용하지 않고 구현할 수 있기 때문). 그런 다음, 반사적 언어에서 재귀 정리가 거의 자명하다는 것이 입증된다.

 첫 번째 재귀 정리 
두 번째 재귀 정리가 계산 가능 함수의 고정점에 관한 것인 반면, 첫 번째 재귀 정리는 열거 연산자에 의해 결정되는 고정점과 관련이 있다. 열거 연산자는 귀납적 정의의 계산 가능 아날로그이다. 열거 연산자는 A가 유한한 수의 집합(코드로 표현됨)이고 n이 단일 자연수인 쌍 (A,n)의 집합이다. 함수가 열거 연산자를 통해 정의될 때, n은 종종 자연수의 순서쌍에 대한 코드로 간주된다. 열거 연산자는 열거 축소성 연구에서 핵심적인 중요성을 갖는다.

각 열거 연산자 Φ는 자연수 집합에서 자연수 집합으로의 함수를 다음과 같이 결정한다.

재귀 연산자는 부분 재귀 함수의 그래프가 주어졌을 때 항상 부분 재귀 함수의 그래프를 반환하는 열거 연산자이다.

열거 연산자 Φ의 고정점은 Φ(F) = F인 집합 F이다. 첫 번째 열거 정리는 열거 연산자 자체가 계산 가능하면 고정점을 효과적으로 얻을 수 있음을 보여준다.

첫 번째 재귀 정리. 다음 진술이 성립한다.
 어떤 계산 가능 열거 연산자 Φ에 대해서도 Φ(F) = F인 재귀적으로 열거 가능한 집합 F가 존재하며, F는 이 속성을 가진 가장 작은 집합이다.
 어떤 재귀 연산자 Ψ에 대해서도 Ψ(φ) = φ인 부분 계산 가능 함수 φ가 존재하며, φ는 이 속성을 가진 가장 작은 부분 계산 가능 함수이다.
첫 번째 재귀 정리는 (재귀 이론의) 고정점 정리라고도 불린다. 또한 다음과 같이 재귀 함수에 적용될 수 있는 정의도 있다.

가 재귀 함수라고 하자. 그러면 는 계산 가능한 최소 고정점 을 갖는다. 즉,

1) 

2) 인 모든 에 대해 가 성립한다.

3) 는 계산 가능하다.

 예시 
두 번째 재귀 정리와 마찬가지로, 첫 번째 재귀 정리는 재귀 방정식 시스템을 만족하는 함수를 얻는 데 사용될 수 있다. 첫 번째 재귀 정리를 적용하려면, 재귀 방정식을 먼저 재귀 연산자로 재구성해야 한다.

계승 함수 f에 대한 재귀 방정식을 고려해 보자.
해당 재귀 연산자 Φ는 이전 값에서 f의 다음 값을 얻는 방법에 대한 정보를 가질 것이다. 그러나 재귀 연산자는 실제로 f의 그래프를 정의할 것이다. 먼저 Φ는 쌍 을 포함할 것이다. 이는 f(0)이 명백히 1이며, 따라서 쌍 (0,1)이 f의 그래프에 있음을 나타낸다.

다음으로, 각 n과 m에 대해 Φ는 쌍 을 포함할 것이다. 이는 f(n)이 m이면 이 이므로, 쌍 이 f의 그래프에 있음을 나타낸다. 기본 경우 와 달리, 재귀 연산자는 의 값을 정의하기 전에 f(n)에 대한 약간의 정보를 필요로 한다.

첫 번째 재귀 정리(특히 1부)는 인 집합 F가 존재한다고 명시한다. 집합 F는 전적으로 자연수의 순서쌍으로 구성되며, 원하는 계승 함수 f의 그래프가 될 것이다.

재귀 방정식을 재귀 연산자로 재구성할 수 있다는 제약은 재귀 방정식이 실제로 최소 고정점을 정의하도록 보장한다. 예를 들어, 다음 재귀 방정식 집합을 고려해 보자.
이러한 방정식을 만족하는 함수 g는 존재하지 않는다. 왜냐하면 g(2) = 1이라는 것과 g(2) = 0이라는 것을 동시에 의미하기 때문이다. 따라서 이러한 재귀 방정식을 만족하는 고정점 g는 존재하지 않는다. 이러한 방정식에 해당하는 열거 연산자를 만들 수는 있지만, 이는 재귀 연산자가 아닐 것이다.

 첫 번째 재귀 정리 증명 개요 
첫 번째 재귀 정리의 1부 증명은 공집합으로 시작하여 열거 연산자 Φ를 반복함으로써 얻어진다. 먼저 에 대해 수열 Fk를 구성한다. F0를 공집합으로 둔다. 귀납적으로 진행하여, 각 k에 대해 Fk + 1을 로 둔다. 마지막으로 F는 로 취한다. 증명의 나머지 부분은 F가 재귀적으로 열거 가능하며 Φ의 최소 고정점임을 확인하는 것으로 구성된다. 이 증명에 사용된 수열 Fk는 클레이니 고정점 정리 증명의 클레이니 사슬에 해당한다.

첫 번째 재귀 정리의 두 번째 부분은 첫 번째 부분으로부터 이어진다. Φ가 재귀 연산자라는 가정은 Φ의 고정점이 부분 함수의 그래프임을 보여주는 데 사용된다. 핵심은 고정점 F가 함수의 그래프가 아니라면, Fk가 함수의 그래프가 아닌 어떤 k가 존재한다는 것이다.

 두 번째 재귀 정리와의 비교 
두 번째 재귀 정리와 비교했을 때, 첫 번째 재귀 정리는 더 강력한 결론을 도출하지만, 더 좁은 가설이 충족될 때만 그렇다. 로저스는 첫 번째 재귀 정리를 약한 재귀 정리로, 두 번째 재귀 정리를 강한 재귀 정리로 부른다.

첫 번째 재귀 정리와 두 번째 재귀 정리의 한 가지 차이점은 첫 번째 재귀 정리에 의해 얻어진 고정점은 최소 고정점임이 보장되는 반면, 두 번째 재귀 정리로부터 얻어진 고정점은 최소 고정점이 아닐 수 있다는 것이다.

두 번째 차이점은 첫 번째 재귀 정리가 재귀 연산자로 재구성될 수 있는 방정식 시스템에만 적용된다는 것이다. 이러한 제약은 순서론의 클레이니 고정점 정리에서 연속 연산자에 대한 제약과 유사하다. 두 번째 재귀 정리는 모든 전체 재귀 함수에 적용될 수 있다.

 일반화된 정리 
예르쇼프는 자신의 번호 매기기 이론의 맥락에서 클레이니의 재귀 정리가 모든 사전완비 번호 매기기에 대해 성립함을 보였다. 괴델 번호 매기기는 계산 가능 함수 집합에 대한 사전완비 번호 매기기이므로, 일반화된 정리는 클레이니 재귀 정리를 특수한 경우로 포함한다.자세한 내용은 영어로 된 개요인 를 참조하라.

사전완비 번호 매기기 가 주어졌을 때, 두 개의 매개변수를 가진 어떤 부분 계산 가능 함수 에 대해서도 하나의 매개변수를 가진 전체 계산 가능 함수 가 존재하여 다음이 성립한다.

 같이 보기 
 표시적 의미론, 여기서 다른 최소 고정점 정리가 첫 번째 재귀 정리와 동일한 목적으로 사용된다.
 고정점 조합자, 람다 대수에서 첫 번째 재귀 정리와 동일한 목적으로 사용된다.
 대각선 보조정리 수학 논리학에서 밀접하게 관련된 결과이다.

 각주 





Footnotes

 더 읽어보기 


 외부 링크 
 .

분류:계산 가능성 이론
분류:수학기초론 정리