4.22 라이스 정리(Rice’s Theorem)와 의미론적 속성의 결정 불가능성

1. 라이스 정리의 진술

라이스 정리(Rice’s Theorem)는 계산 이론에서 가장 일반적인 결정 불가능성 결과 중 하나이다. 이 정리는 부분 재귀 함수의 모든 비자명(Nontrivial) 의미론적 속성(Semantic Property)이 결정 불가능함을 보장한다.

1.1 형식적 진술

$\mathcal{C}$ 를 부분 재귀 함수의 클래스라 하자. $\mathcal{C}$ 가 비자명(Nontrivial)이라 함은 $\mathcal{C} \neq \emptyset$ 이고 $\mathcal{C} \neq \{\text{모든 부분 재귀 함수}\}$ 임을 의미한다. 즉, $\mathcal{C}$ 에 속하는 함수와 $\mathcal{C}$ 에 속하지 않는 함수가 모두 존재한다.

이때, 인덱스 집합 $I_\mathcal{C} = \{e \in \mathbb{N} \mid \varphi_e \in \mathcal{C}\}$ 는 결정 불가능(Undecidable)하다.

즉, 부분 재귀 함수에 관한 모든 비자명 속성에 대해, 주어진 프로그램(인덱스 $e$ )이 해당 속성을 만족하는 함수를 계산하는지를 알고리즘적으로 판별하는 것은 불가능하다.

1.2 의미론적 속성의 의미

**의미론적 속성(Semantic Property)**은 프로그램의 구조(구문)가 아니라, 프로그램이 계산하는 함수의 입출력 행동(의미)에 관한 속성이다. 형식적으로, 의미론적 속성은 인덱스(프로그램 코드)가 아닌 함수(프로그램의 행동)에 의해 결정된다: $\varphi_e = \varphi_f$ 이면 $e \in I_\mathcal{C} \iff f \in I_\mathcal{C}$ .

2. 라이스 정리의 증명

2.1 증명

귀류법으로 증명한다. $I_\mathcal{C}$ 가 결정 가능하다고 가정한다.

공백 함수(Nowhere Defined Function) $\varphi_\emptyset$ (모든 입력에서 정의되지 않는 함수)를 고려한다. 일반성을 잃지 않고 $\varphi_\emptyset \notin \mathcal{C}$ 라 가정한다(만약 $\varphi_\emptyset \in \mathcal{C}$ 이면 $\mathcal{C}$ 를 $\overline{\mathcal{C}}$ 로 대체).

$\mathcal{C}$ 가 비자명이므로, $\varphi_d \in \mathcal{C}$ 인 인덱스 $d$ 가 존재한다.

정지 문제를 $I_\mathcal{C}$ 의 결정으로 환원한다. 임의의 $\langle e, x \rangle$ 에 대해, 다음과 같이 동작하는 튜링 기계 $M_{e,x}$ 를 구성한다:

$M_{e,x}$ 는 입력 $y$ 에 대해:

$\varphi_e(x)$ 를 시뮬레이션한다.
$\varphi_e(x)$ 가 정지하면, $\varphi_d(y)$ 를 계산하여 반환한다.

s-m-n 정리에 의해, $M_{e,x}$ 의 인덱스 $i(e, x)$ 를 $e$ 와 $x$ 로부터 효과적으로 계산할 수 있다.

분석:

$\varphi_e(x)$ 가 정지하면: $\varphi_{i(e,x)} = \varphi_d \in \mathcal{C}$ 이므로 $i(e,x) \in I_\mathcal{C}$ .
$\varphi_e(x)$ 가 정지하지 않으면: $\varphi_{i(e,x)} = \varphi_\emptyset \notin \mathcal{C}$ 이므로 $i(e,x) \notin I_\mathcal{C}$ .

따라서 $I_\mathcal{C}$ 를 결정하는 알고리즘이 있으면 정지 문제를 결정할 수 있다. 정지 문제가 결정 불가능하므로 모순이다. $\blacksquare$

3. 라이스 정리의 구체적 적용

라이스 정리에 의해 다음의 모든 문제가 결정 불가능하다:

3.1 프로그램 종료 관련

“프로그램 $P$ 가 모든 입력에 대해 종료하는가?” (전역성, Totality)
“프로그램 $P$ 가 특정 입력 $x$ 에 대해 종료하는가?” (정지 문제)

3.2 입출력 행동 관련

“프로그램 $P$ 가 상수 함수를 계산하는가?”
“프로그램 $P$ 가 항등 함수를 계산하는가?”
“프로그램 $P$ 가 입력 $x$ 에 대해 값 $v$ 를 출력하는가?”
“두 프로그램 $P$ 와 $Q$ 가 동일한 함수를 계산하는가?” (동치 문제, Equivalence Problem)

3.3 함수적 성질 관련

“프로그램 $P$ 가 단사(Injective) 함수를 계산하는가?”
“프로그램 $P$ 가 전사(Surjective) 함수를 계산하는가?”
“프로그램 $P$ 가 유한 영역(Finite Domain)의 함수를 계산하는가?”

4. 라이스 정리가 적용되지 않는 경우

라이스 정리는 의미론적(Semantic) 속성에만 적용되며, 구문론적(Syntactic) 속성에는 적용되지 않는다.

4.1 결정 가능한 구문론적 속성의 예

“프로그램 $P$ 의 코드 길이가 100 이하인가?”
“프로그램 $P$ 의 코드에 변수 $x$ 가 등장하는가?”
“프로그램 $P$ 가 정확히 5개의 상태를 갖는 튜링 기계인가?”

이들은 프로그램의 코드(구문)를 검사하여 판정 가능하며, 프로그램이 계산하는 함수(의미)에 관한 속성이 아니므로 라이스 정리의 대상이 아니다.

5. 라이스 정리의 소프트웨어 공학적 함의

5.1 완벽한 프로그램 검증의 불가능성

라이스 정리에 의해, 임의의 프로그램이 특정 기능적 명세(Functional Specification)를 만족하는지를 자동으로 판별하는 범용적 도구는 존재하지 않는다. “프로그램이 올바른가?“라는 물음은 의미론적 속성에 관한 것이므로, 일반적으로 결정 불가능하다.

5.2 실용적 우회 전략

라이스 정리의 한계에도 불구하고, 소프트웨어 검증 분야는 다음의 우회 전략을 사용한다:

근사적 분석(Approximate Analysis): 프로그램의 일부 속성에 대해 건전(Sound)하지만 불완전(Incomplete)한 분석을 수행한다. 즉, 오류를 탐지하지 못하는 경우는 있으나, 오류라고 보고하면 실제 오류인 것을 보장한다.
제한된 프로그램 클래스: 특정 프로그래밍 패러다임이나 유형 시스템(Type System)에 의해 프로그램의 클래스를 제한하여, 제한된 클래스 내에서 결정 가능한 속성을 분석한다.
반결정 절차(Semi-Decision Procedure): 속성이 만족되는 경우에만 확인하고, 만족되지 않는 경우는 탐지하지 못하는 절차를 사용한다.

6. 라이스 정리와 인공지능

6.1 AI 체계의 행동 검증

인공지능 체계가 특정 행동적 보장(Behavioral Guarantee)을 만족하는지를 자동으로 검증하는 것은 라이스 정리에 의해 일반적으로 결정 불가능하다. “이 신경망이 항상 안전한 출력을 생성하는가?“라는 물음은 의미론적 속성에 관한 것이므로, 일반적으로 결정 불가능하다.

6.2 AI 안전성(AI Safety)에 대한 함의

라이스 정리는 AI 안전성 연구에 근본적 도전을 제기한다. 완벽한 AI 행동 검증이 원리적으로 불가능하므로, AI 안전성 확보는 형식적 보장이 아닌 경험적 검증, 확률적 보장, 제한된 환경에서의 분석 등 실용적 접근법에 의존해야 한다.

라이스 정리는 프로그램(그리고 이를 확장하여 AI 체계)의 의미론적 속성을 자동 판별하는 것의 근본적 한계를 확정하는 결과이며, 이 한계의 인식이 올바른 검증 전략과 안전성 접근법의 설계에 필수적이다.