라이스의 정리

계산 가능성 이론에서 라이스의 정리(Rice's theorem)는 프로그램의 모든 비자명한 의미론적 속성이 판단 불가능하다고 말한다. 의미론적 속성은 프로그램의 동작에 관한 것이다 (예를 들어, "프로그램이 모든 입력에 대해 종료하는가?"), 이는 구문적 속성 (예를 들어, "프로그램에 if-then-else 문이 포함되어 있는가?")과는 다르다. 비자명한 속성은 모든 프로그램에 대해 참이거나 모든 프로그램에 대해 거짓이 아닌 속성이다.

이 정리는 정지 문제의 판단 불가능성을 일반화한다. 이는 프로그램의 정적 분석의 실현 가능성에 광범위한 영향을 미친다. 이는 예를 들어, 주어진 프로그램이 정확한지 또는 오류 없이 실행되는지 확인하는 도구를 구현하는 것이 불가능함을 의미한다 (항상 과대평가하거나 과소평가하는 도구를 구현하는 것은 가능하므로, 실제로는 어떤 것이 덜 문제인지 결정해야 한다).

이 정리는 1951년 시러큐스 대학교 박사 학위 논문에서 이를 증명한 헨리 고든 라이스의 이름을 따서 명명되었다.

서론

라이스의 정리는 어떤 유형의 정적 프로그램 분석을 자동으로 수행할 수 있는지에 대한 이론적 한계를 설정한다. 프로그램의 구문과 의미론을 구별할 수 있다. 구문은 프로그램이 작성되는 방식, 즉 "내포"의 세부 사항이며, 의미론은 프로그램이 실행될 때 어떻게 동작하는지, 즉 "외연"이다. 라이스의 정리는 속성이 자명하지 않은 한 (모든 프로그램에 대해 참이거나 모든 프로그램에 대해 거짓), 구문에 의존하지 않고 의미론에만 의존하는 프로그램의 속성을 결정하는 것이 불가능하다고 주장한다.

라이스의 정리에 따르면, 프로그램과 명세를 입력으로 받아 프로그램이 명세를 만족하는지 확인하여 다른 프로그램에서 버그의 부재를 자동으로 검증하는 프로그램을 작성하는 것은 불가능하다.

이것이 특정 유형의 버그를 방지하는 것이 불가능하다는 것을 의미하지는 않는다. 예를 들어, 라이스의 정리는 튜링 완전한 동적 프로그래밍 언어에서 자료형 오류의 부재를 검증하는 것이 불가능하다는 것을 의미한다. 반면에, 정적 자료형 프로그래밍 언어는 자료형 오류를 정적으로 방지하는 자료형 시스템을 특징으로 한다. 본질적으로, 이것은 해당 언어의 구문(광범위한 의미에서)의 특징으로 이해되어야 한다. 프로그램을 자료형 검사하려면 소스 코드를 검사해야 한다; 이 작업은 프로그램의 가설적인 의미론에만 의존하지 않는다.

일반적인 소프트웨어 검증 측면에서, 이는 주어진 프로그램이 주어진 명세를 만족하는지 알고리즘적으로 확인할 수는 없지만, 프로그램이 정확함을 증명하는 추가 정보로 주석을 달거나, 검증을 가능하게 하는 특정 제한된 형태로 작성되도록 요구하고, 이런 방식으로 검증된 프로그램만 받아들일 수 있음을 의미한다. 자료형 안전성의 경우, 전자는 자료형 주석에 해당하고, 후자는 자료형 추론에 해당한다. 자료형 안전성을 넘어, 이 아이디어는 호어 논리와 같은 증명 주석을 통한 프로그램의 정확성 증명으로 이어진다.

라이스의 정리를 우회하는 또 다른 방법은 완전하지는 않지만 많은 버그를 잡는 방법을 찾는 것이다. 이것이 추상 해석 이론이다.

검증의 또 다른 방향은 모델 검사이며, 이는 튜링 완전 언어에는 적용할 수 없고 유한 상태 프로그램에만 적용할 수 있다.

정의

${\displaystyle \phi }$를 부분 계산 가능한 함수의 허용 가능한 번호 매기기라고 하고, ${\displaystyle P}$를 ${\displaystyle \mathbb {N} }$의 부분 집합이라고 하자. 다음을 가정한다:

1. ${\displaystyle P}$는 비자명하다: ${\displaystyle P}$는 비어 있지도 않고 ${\displaystyle \mathbb {N} }$ 자체도 아니다.
2. ${\displaystyle P}$는 확장적이다: 모든 정수 ${\displaystyle m}$과 ${\displaystyle n}$에 대해, 만약 ${\displaystyle \phi _{m}=\phi _{n}}$이면, ${\displaystyle m\in P\iff n\in P}$이다.

그러면 ${\displaystyle P}$는 판단 불가능하다.

더 간결한 진술은 색인 집합 측면에서 할 수 있다: 유일하게 결정 가능한 색인 집합은 ${\displaystyle \varnothing }$와 ${\displaystyle \mathbb {N} }$이다.

예시

자연수 n을 받아 자연수 P(n)을 반환하는 프로그램 P가 주어졌을 때, 다음 질문들은 판단 불가능하다:

• P는 주어진 n에서 종료하는가? (이것은 정지 문제이다.)
• P는 0에서 종료하는가?
• P는 모든 n에서 종료하는가 (즉, P는 전체인가)?
• P는 종료하고 모든 입력에 대해 0을 반환하는가?
• P는 종료하고 일부 입력에 대해 0을 반환하는가?
• P는 종료하고 모든 입력에 대해 동일한 값을 반환하는가?
• P는 주어진 프로그램 Q와 동등한가?

클레이니 재귀 정리에 의한 증명

${\displaystyle P}$가 자연수의 비자명하고 확장적이며 계산 가능한 집합이라고 모순적으로 가정해 보자. 자연수 ${\displaystyle a\in P}$와 자연수 ${\displaystyle b\notin P}$가 존재한다. ${\displaystyle e\in P}$일 때 ${\displaystyle Q_{e}(x)=\varphi _{b}(x)}$이고 ${\displaystyle e\notin P}$일 때 ${\displaystyle Q_{e}(x)=\varphi _{a}(x)}$로 함수 ${\displaystyle Q}$를 정의한다. 클레이니 재귀 정리에 의해, ${\displaystyle \varphi _{e}=Q_{e}}$인 ${\displaystyle e}$가 존재한다. 그러면, 만약 ${\displaystyle e\in P}$이면, ${\displaystyle \varphi _{e}=\varphi _{b}}$가 되어 ${\displaystyle b\notin P}$이므로 ${\displaystyle P}$의 확장성에 모순되며, 반대로, 만약 ${\displaystyle e\notin P}$이면, ${\displaystyle \varphi _{e}=\varphi _{a}}$가 되어 ${\displaystyle a\in P}$이므로 다시 확장성에 모순된다.

정지 문제로부터의 환원을 통한 증명

증명 스케치

구체적으로, 프로그램 p를 검사하여 p가 정수 d를 받아 d²을 반환하는 제곱 함수의 구현인지 정확하게 판별하는 알고리즘이 있다고 가정해 보자. 이 증명은 프로그램 동작의 다른 비자명한 속성(즉, 의미론적이고 비자명한 속성)을 결정하는 알고리즘이 있는 경우에도 마찬가지로 잘 작동하며, 아래에 일반적인 형태로 제시된다.

주장은 제곱 프로그램을 식별하는 알고리즘을 정지하는 함수를 식별하는 알고리즘으로 변환할 수 있다는 것이다. 우리는 입력 a와 i를 받아 프로그램 a가 입력 i에서 정지하는지 여부를 결정하는 알고리즘을 설명할 것이다.

이를 결정하는 알고리즘은 개념적으로 간단하다: 인자 n을 받는 새 프로그램 t의 (설명)을 구성하는데, 이는 (1) 먼저 입력 i에서 프로그램 a를 실행하고 (a와 i는 모두 t의 정의에 하드코딩된다), (2) 그 다음 n의 제곱을 반환한다. 만약 a(i)가 영원히 실행된다면, t는 n에 관계없이 단계 (2)에 도달하지 못한다. 그러면 분명히, t는 단계 (1)이 종료하는 경우에만 제곱을 계산하는 함수이다. 제곱을 계산하는 프로그램을 정확하게 식별할 수 있다고 가정했으므로, a와 i에 의존하는 t가 그런 프로그램인지 결정할 수 있다; 따라서 우리는 프로그램 a가 입력 i에서 정지하는지 결정하는 프로그램을 얻었다. 우리의 정지 결정 알고리즘은 t를 실행하지 않고, 단지 그 설명을 제곱 식별 프로그램에 전달하며, 이 프로그램은 가정에 따라 항상 종료한다; t의 설명을 구성하는 것 또한 항상 종료하는 방식으로 수행될 수 있으므로, 정지 결정도 정지하지 않을 수 없다.

 halts (a,i) {
   define t(n) {
     a(i)
     return n×n
   }
   return is_a_squaring_function(t)
 }

이 방법은 제곱을 계산하는 함수를 인식할 수 있는지 여부에 특별히 의존하지 않는다; 우리가 인식하려는 것을 어떤 프로그램이 할 수 있는 한, 우리는 a에 대한 호출을 추가하여 t를 얻을 수 있다. 우리는 제곱근을 계산하는 프로그램을 인식하는 방법, 또는 월급을 계산하는 프로그램, 또는 입력 "Abraxas"가 주어졌을 때 정지하는 프로그램을 인식하는 방법을 가질 수 있었다; 각 경우에, 우리는 정지 문제를 유사하게 해결할 수 있었을 것이다.

정식 증명

비자명한 속성을 결정하는 알고리즘이 있다면, 정지 문제를 결정하는 튜링 기계를 구성할 수 있다.

정식 증명을 위해, 알고리즘은 문자열에 대한 부분 함수를 정의하고 스스로 문자열로 표현된다고 가정한다. 문자열 a로 표현되는 알고리즘에 의해 계산되는 부분 함수는 F_a로 표기된다. 이 증명은 귀류법으로 진행된다: 우리는 알고리즘에 의해 결정되는 비자명한 속성이 있다고 가정하고, 그 다음 우리가 정지 문제를 결정할 수 있다는 것을 보여주는데, 이는 불가능하므로 모순이다.

이제 P(a)가 F_a의 비자명한 속성을 결정하는 알고리즘이라고 가정해 보자. 일반성을 잃지 않고 P(no-halt) = "no"라고 가정할 수 있으며, no-halt는 결코 정지하지 않는 알고리즘의 표현이다. 만약 이것이 사실이 아니라면, 속성 P의 부정을 계산하는 알고리즘 P에 대해 이것이 성립한다. 이제 P가 비자명한 속성을 결정하므로, 알고리즘 F_b를 나타내는 문자열 b가 존재하고 P(b) = "yes"이다. 그러면 H(a, i) 알고리즘을 다음과 같이 정의할 수 있다:

1. 알고리즘 T(j)를 나타내는 문자열 t를 구성한다.

• T는 먼저 F_a(i)의 계산을 시뮬레이션하고,
• 그 다음 T는 F_b(j)의 계산을 시뮬레이션하고 그 결과를 반환한다.

2. P(t)를 반환한다.

이제 H가 정지 문제를 결정한다는 것을 보여줄 수 있다:

• 문자열 a로 표현되는 알고리즘이 입력 i에서 정지한다고 가정해 보자. 이 경우 F_t = F_b이고, P(b) = "yes"이며 P(x)의 출력이 F_x에만 의존하므로, P(t) = "yes"이고 따라서 H(a, i) = "yes"이다.
• 문자열 a로 표현되는 알고리즘이 입력 i에서 정지하지 않는다고 가정해 보자. 이 경우 F_t = F_no-halt, 즉 결코 정의되지 않는 부분 함수이다. P(no-halt) = "no"이고 P(x)의 출력이 F_x에만 의존하므로, P(t) = "no"이고 따라서 H(a, i) = "no"이다.

정지 문제는 판단 불가능하다고 알려져 있으므로, 이것은 모순이며, a로 표현되는 함수에 대한 비자명한 속성을 결정하는 알고리즘 P(a)가 존재한다는 가정은 거짓이어야 한다.

같이 보기

• 정지 문제
• 라이스-샤피로 정리 및 크라이젤-라콤베-슈엔필드-체이틴 정리, 라이스의 정리의 일반화
• 스콧-커리 정리, 람다 계산에서의 라이스의 정리의 아날로그
• 튜링의 증명

각주

• Hopcroft, John E.; Ullman, Jeffrey D. (1979), 《Introduction to Automata Theory, Languages, and Computation》, Addison-Wesley, 185–192쪽
• Rice, H. G. (1953), “Classes of recursively enumerable sets and their decision problems”, 《Transactions of the American Mathematical Society》 74 (2): 358–366, doi:10.1090/s0002-9947-1953-0053041-6, JSTOR 1990888
• Rogers, Hartley Jr. (1987), 《Theory of Recursive Functions and Effective Computability》 2판, McGraw-Hill, §14.8