2.3 계산 가능성 — 계산할 수 없는 문제와 분석 도구의 한계

"아직 좋은 알고리즘을 못 찾은 문제"와 "어떤 알고리즘도 존재할 수 없는 문제"는 다르다. 이 문서는 튜링 기계로 계산 가능성의 최소 모델을 세우고, 정지 문제를 대각선 논증으로 직접 구성한 뒤, Rice의 정리가 왜 정적 분석기·안티바이러스·리팩터링 검증 도구 모두가 건전성·완전성·항상 종료 중 하나를 포기해야 하는지 설명한다.

학습 목표

• 결정 가능(decidable), 인식 가능(recognizable), 결정 불가능을 각각 정의하고 항상 종료하는 판정기와 종료하지 않을 수 있는 인식기의 차이를 설명한다.
• 정지 문제가 결정 불가능함을 대각선 논증으로 직접 구성하고, 환원으로 다른 문제의 결정 불가능성을 이끌어 내는 방법을 설명한다.
• Rice의 정리가 규정하는 "비자명한 의미적 속성"의 범위를 밝히고, 문법적 속성과 의미적 속성을 구분한다.
• 정지 문제를 근거로 "모든 정적 분석은 무의미하다"고 일반화하는 오류를 제한된 문제의 반례로 반박한다.
• step budget을 둔 인터프리터로 "정지 확인됨"과 "모름"을 구분하고, budget 초과가 비종료의 증명이 아님을 설명한다.

배경: 왜 이것이 존재하는가

1936년, 힐베르트가 제기한 결정 문제(Entscheidungsproblem) — "모든 수학적 명제가 참인지 거짓인지 판정하는 기계적 절차가 존재하는가" — 에 답하기 위해 튜링과 처치가 각자 다른 모델로 "효과적으로 계산 가능하다"는 개념을 정식화했다. 튜링은 테이프와 헤드로 구성된 추상 기계(튜링 기계)를, 처치는 함수 정의와 치환 규칙으로 구성된 람다 계산법을 제안했다. 두 모델은 표기가 전혀 다른데도 정확히 같은 함수 집합을 계산할 수 있다는 것이 곧 증명됐고, 이후 괴델의 일반 재귀 함수 등 독립적으로 제안된 다른 형식화들도 전부 같은 집합으로 수렴했다. 서로 무관하게 출발한 여러 형식화가 하나로 모인다는 사실이 "계산 가능하다"는 직관적 개념을 이 모델들이 정확히 포착했다는 확신의 근거가 됐다 — 이를 처치-튜링 논제라 부른다.

이 챕터의 2.2가 유한 오토마타로 정규 언어의 인식 능력을 세웠다면, 2.3은 그 계층의 맨 위(촘스키 계층의 Type 0, 제약 없는 문법)에 대응하는 가장 강력한 계산 모델 자체의 한계를 다룬다. 질문이 "이 언어를 인식하는 더 강한 기계가 있는가"에서 "가장 강력한 기계로도 원리적으로 답할 수 없는 질문이 있는가"로 바뀌는 지점이다.

핵심 개념

결정 문제, 결정 가능, 인식 가능

결정 문제(decision problem)는 예/아니오로 답하는 질문이다 — 형식적으로는 "이 문자열이 언어 L에 속하는가?"로 통일해 쓸 수 있다. 이 질문에 답하는 절차의 강도는 두 단계로 나뉜다.

• 결정 가능(decidable): 모든 입력에 대해 항상 멈추고 옳게 예/아니오를 답하는 튜링 기계(판정기, decider)가 존재한다.
• 인식 가능(recognizable, recursively enumerable): 입력이 L에 속하면 멈추고 "예"를 답하지만, 속하지 않으면 영원히 멈추지 않을 수도 있는 튜링 기계(인식기, recognizer)가 존재한다.

이 구분이 실무적으로 중요한 이유는, 인식기가 아직 "아니오"를 답하지 못했다는 사실이 "예"가 아니라는 증거가 되지 못하기 때문이다. 아직 계산 중인 것과 영원히 끝나지 않을 것을 실행 중에는 구분할 방법이 없다 — 이 문서의 미니 실험이 이 상황을 직접 재현한다. (참고로 L과 L의 여집합이 둘 다 인식 가능하면 L은 결정 가능하다는 것이 알려져 있다 — 양쪽에서 동시에 실행해 먼저 멈추는 쪽의 답을 취하면 되기 때문이다. 하지만 이 조건이 항상 성립하지는 않는다.)

튜링 기계 — 프로그램을 데이터로 다루는 최소 모델

튜링 기계는 무한히 늘어나는 테이프, 그 위를 움직이는 헤드, 유한한 상태 집합, 그리고 "지금 상태와 헤드 아래 기호"에서 "다음 상태, 쓸 기호, 헤드 이동 방향"을 정하는 전이 함수로 구성된다. 이 챕터에서 전이표를 직접 설계하는 연습 자체는 다루지 않는다 — 중요한 것은 세부 구현이 아니라 이 모델이 증명한 한 가지 사실이다: 튜링 기계의 설명(전이 규칙)도 유한한 문자열로 인코딩할 수 있고, 그 인코딩을 다른 튜링 기계의 입력으로 줄 수 있다. 이렇게 "프로그램 하나의 설명과 입력을 받아 그 프로그램을 시뮬레이션하는" 튜링 기계를 보편 튜링 기계(universal Turing machine)라 부른다. 프로그램을 데이터처럼 다룰 수 있다는 이 성질이 저장 프로그램 방식 컴퓨터의 이론적 원형이며, 아래의 정지 문제 논증이 성립하는 근거이기도 하다 — H라는 프로그램에게 "다른 프로그램 P(와 입력 I)"를 입력으로 줄 수 있다는 것, 그리고 P 자신을 자신의 입력으로 줄 수도 있다는 것이 대각선 논증의 재료가 된다.

처치-튜링 논제 — 정리가 아니라 논제

여기서 "논제"(thesis)라는 단어를 신중하게 쓴다. 처치-튜링 논제는 수학 정리처럼 공리에서 증명된 것이 아니다. "효과적으로 계산 가능하다"는 것은 원래 사람이 유한한 절차를 손으로 실행할 수 있다는 직관적 개념이었고, 튜링 기계는 그 직관을 정식화한 하나의 수학적 모델이다. 직관적 개념과 수학적 모델이 정확히 일치한다는 주장은 증명 대상이 아니라 — 여러 독립적 형식화가 같은 결론에 수렴한다는 정황 증거로 뒷받침되는 논제다. 실무에서 중요한 결론은 이렇다: 어떤 새로운 계산 모델(양자 컴퓨터 포함)도 지금까지 계산 가능한 함수의 범위 자체를 넓히지 못했다 — 양자 컴퓨터는 특정 문제를 더 빨리 풀 수 있지만, 튜링 기계가 원리적으로 계산할 수 없던 것을 계산 가능하게 만들지는 않는다. 이 챕터가 다루는 결정 불가능성은 계산 모델을 바꾼다고 사라지는 종류의 한계가 아니다.

정지 문제 — 자기 참조로 모순을 만든다

정지 문제(halting problem)는 이렇게 정의된다: 프로그램 P와 입력 I가 주어졌을 때, P가 I에서 실행을 멈추는지(halt) 판정하라. 이 문제가 결정 불가능하다는 것을 튜링이 보인 방법은 존재를 가정한 뒤 모순을 끌어내는 대각선 논증(diagonalization)이다.

H(P, I)가 이 문제를 항상 정확히, 항상 멈추면서 판정하는 프로그램이 존재한다고 가정하자. 이제 다음과 같은 새 프로그램 D를 만든다.

D(P):
  if H(P, P) == "halts":
    loop forever
  else:
    halt

D는 어떤 프로그램 P를 받아, "P가 자기 자신을 입력으로 받았을 때 멈추는가"를 H로 확인하고 정반대로 행동한다. 이제 D 자신에게 D를 입력으로 주면 어떻게 되는지 보자.

• D(D)가 멈춘다고 하자. D의 정의에 따르면 이는 H(D, D)가 "멈추지 않는다"고 답했을 때만 일어난다. 그런데 H가 정확하다고 가정했으므로 H(D, D)가 "멈추지 않는다"고 답했다는 것은 실제로 D(D)가 멈추지 않는다는 뜻이다. D(D)가 멈추면서 동시에 멈추지 않는다 — 모순이다.
• D(D)가 멈추지 않는다고 하자. D의 정의에 따르면 이는 H(D, D)가 "멈춘다"고 답했을 때만 일어난다(그 분기가 무한 루프다). H가 정확하다면 이는 실제로 D(D)가 멈춘다는 뜻이다. 다시 모순이다.

두 경우 모두 모순이므로, 처음 가정 — "H가 존재한다" — 이 틀렸다. 따라서 정지 문제를 항상 정확히 판정하는 프로그램은 존재할 수 없다. 이 논증에서 결정적인 재료는 D가 자기 자신을 입력으로 받을 수 있다는 것(자기 참조)과, H의 답을 보고 그것과 반대로 행동하도록 D를 프로그램으로서 구성할 수 있다는 것(프로그램=데이터)이다.

환원 — 이미 불가능한 문제로 새 문제를 무너뜨린다

정지 문제 하나를 대각선 논증으로 힘들게 증명한 뒤에는, 다른 문제의 결정 불가능성을 매번 같은 논증으로 다시 증명할 필요가 없다. **환원(reduction)**은 "문제 A가 결정 불가능하다는 것을 알고 있을 때, A를 문제 B의 판정기로 풀 수 있음을 보여서 B도 결정 불가능함을 전달하는" 방법이다. 논리는 대우다 — B가 결정 가능하다면 그것으로 A도 풀 수 있는데 A는 결정 불가능하다고 알려져 있으므로, B도 결정 불가능해야 한다.

예를 들어 "프로그램 P가 입력 없이 실행했을 때 멈추는가"(HALT_ε라 하자, 정지 문제의 특수한 경우처럼 보인다)가 결정 불가능함을 보이자. 임의의 정지 문제 인스턴스 (P, I)가 주어졌다고 하자. 다음과 같은 새 프로그램 P'를 구성한다.

P'():
  P를 입력 I로 실행한다   // P'는 자신의 (없는) 입력을 무시하고 I를 하드코딩해서 쓴다

P'는 입력을 받지 않고, P(I)를 그대로 실행할 뿐이다. P'가 입력 없이 멈춘다는 것은 정확히 P가 I에서 멈춘다는 것과 같다. 만약 HALT_ε를 항상 정확히 판정하는 프로그램이 있다면, 임의의 (P, I)에 대해 위 방식으로 P'를 만들어 HALT_ε(P')를 물어보는 것으로 원래 정지 문제 HALT(P, I)를 풀 수 있다. 정지 문제는 결정 불가능하다고 이미 알고 있으므로, HALT_ε도 결정 불가능하다.

이 환원 기법이 실무적으로 중요한 이유는, "이 새로운 분석 문제가 결정 불가능한가"를 매번 대각선 논증으로 손수 증명할 필요 없이, 이미 알려진 결정 불가능한 문제를 그 문제로 표현할 수 있는지만 확인하면 된다는 것이다. 아래 Rice의 정리도, 그리고 2.4에서 NP-완전성이 퍼져 나가는 방식(다항 시간 환원)도 같은 논리 구조를 쓴다.

Rice의 정리 — 의미 있는 질문은 대개 결정 불가능하다

Rice의 정리(1953)는 이 환원 기법을 극단까지 밀어붙인 결과다.

프로그램이 계산하는 함수의 비자명한 의미적 속성은 일반적으로 결정 불가능하다.

두 단어를 정확히 풀어야 한다.

• 의미적(semantic): 프로그램의 소스 코드 모양이 아니라, 그 프로그램이 계산하는 함수 자체에 대한 속성이다. "이 프로그램은 항상 종료하는가", "이 함수는 항등 함수와 같은 함수를 계산하는가", "이 프로그램은 특정 입력에서 예외를 던지는가"는 모두 의미적 속성이다.
• 비자명(non-trivial): 모든 프로그램이 그 속성을 갖는 것도 아니고, 어떤 프로그램도 갖지 않는 것도 아니다 — 즉 그 속성이 프로그램 공간을 실제로 둘로 가른다.

결정적으로, Rice의 정리는 문법적(syntactic) 속성에는 적용되지 않는다. "이 함수의 이름에 deprecated가 포함되어 있는가", "이 소스 코드는 100줄을 넘는가", "이 함수는 for 루프를 포함하는가"는 소스 코드의 겉모습에 대한 질문이고, 소스 코드를 그냥 읽으면(파싱하고 문자열을 검사하면) 항상 멈추고 정확히 답할 수 있다 — 결정 가능하다. Rice의 정리가 막는 것은 "실행했을 때 실제로 어떤 함수를 계산하는가"에 대한 질문이지, "코드가 어떻게 생겼는가"에 대한 질문이 아니다.

실무 관점

정적 분석기는 셋 중 하나를 반드시 포기한다

"이 함수가 항상 종료하는가", "이 값은 절대 null이 될 수 없는가", "이 코드 경로는 도달 불가능한가"는 전부 프로그램이 계산하는 함수에 대한 비자명한 의미적 속성이다. Rice의 정리에 따라 이런 질문에 항상 종료하면서, 항상 정확히(건전하고 완전하게) 답하는 알고리즘은 일반적으로 존재하지 않는다. 그래서 실제 정적 분석기는 다음 중 하나를 의도적으로 포기한다.

• 완전성을 포기(over-approximation): 확신할 수 없으면 "위험"으로 보고한다. 실제로는 안전한데 경고하는 false positive가 생기지만, 놓치는 것(false negative)은 없다 — 건전하다.
• 건전성을 포기(under-approximation): 확신할 수 있는 것만 보고한다. 놓치는 것(false negative)이 생기지만, 보고한 것은 항상 진짜다 — 완전하다.
• 항상 종료를 포기: 시간·탐색 깊이 제한 없이 정확한 답을 찾을 때까지 계속 계산한다. 이론적으로 언젠가 답을 낼 수도 있지만 실행 중에 "얼마나 더 기다려야 하는지" 알 수 없다.

세 선택 모두를 동시에 만족하는 정적 분석기는 없다. 챕터 5의 정적 분석이 이 트레이드오프를 도구의 정책(어느 쪽 오류를 얼마나 허용하는지)으로 읽는 방법을 다루는데, 이 문서가 보인 것은 그 정책이 선택이 아니라 강제된 필연이라는 점이다 — Rice의 정리 때문에 셋을 동시에 가질 수 없으므로, 만든 사람이 의식했든 아니든 모든 도구는 이미 어느 하나를 포기한 상태다.

"완벽한 판정기"라는 요구사항을 검토한다

같은 논리가 다른 요구사항에도 적용된다. "리팩터링 전후 프로그램의 동작이 완전히 같음을 자동으로 완벽하게 검증해 달라"(프로그램 동등성), "이 함수가 어떤 입력에서도 예외를 던지지 않음을 증명해 달라"(전역 안전성), "이 프로그램이 악성 행위를 하는지 항상 정확히 판정해 달라"(안티바이러스의 이상형)는 모두 비자명한 의미적 속성이고, 일반적인 프로그램 전체를 대상으로 한다면 결정 불가능하다. 이런 요구사항을 마주하면 "어떤 도구를 더 찾아야 하는가"가 아니라 "이 요구사항 자체가 원리적으로 불가능한 것을 묻고 있지는 않은가"를 먼저 물어야 한다.

"불가능하다"는 결론이 전부 같은 이유에서 나오는 것은 아니라는 점도 짚어 둘 필요가 있다. 이 문서의 불가능성은 "항상 종료하며 항상 정확한 알고리즘 자체가 존재하지 않는다"는 것이었다. 분산 시스템에는 성격이 다른 불가능성 결과도 있다 — 챕터 10의 FLP 불가능성은 알고리즘이 원리적으로 존재할 수 없다는 것이 아니라, 비동기 네트워크에서 메시지 지연의 상한을 알 수 없다는 전제 아래 "고장 노드가 하나라도 있으면 항상 종료하는 합의 알고리즘은 없다"는, 계산 모델의 통신 가정에서 비롯된 다른 종류의 한계다. 두 결과 모두 "불가능하다"는 말을 쓰지만 원인과 우회 방법(전자는 근사·시간제한, 후자는 타임아웃 기반 장애 감지나 부분 동기 가정)이 다르므로 섞어 쓰면 안 된다.

현실적 타협이 포기하는 것을 명시한다

시간 제한, 추상화(근사), 탐색 깊이 제한, 사용자 annotation은 모두 이 불가능성을 우회하는 실무적 타협이다. 각각이 무엇을 포기하는지 명시하는 것이 설계의 핵심이다.

• 시간·step 제한: 항상 종료하게 만들지만, 제한에 도달하면 "모름"을 반환해야 한다 — 이 문서의 미니 실험이 보이는 것이 정확히 이것이다.
• 추상화(과잉 근사): 건전성을 지키되 완전성(정밀도)을 낮춘다 — 실제 실행보다 넓은 근사 세계에서 판정하므로 false positive가 생긴다.
• 사용자 annotation(@NonNull, contract 명세 등): 도구가 스스로 증명하지 못하는 부분을 사람이 대신 확언해, 그 부분만큼은 결정 불가능성의 영향권 밖으로 빼낸다. 사람의 확언이 틀리면 도구의 보장도 함께 무너진다.

더 깊이: Rice의 정리도 환원으로 증명된다

Rice의 정리 자체도 앞서 본 환원 기법으로 증명된다(전체 증명은 이 챕터의 범위를 넘지만 구조만 스케치한다). 어떤 비자명한 의미적 속성 Prop이 있다고 하자 — 어떤 프로그램은 Prop을 갖고 어떤 프로그램은 갖지 않는다. 정지 문제 HALT(P, I)의 임의의 인스턴스가 주어지면, 다음과 같은 새 프로그램 P'를 만든다.

P'(x):
  P를 입력 I로 실행한다(끝날 때까지 기다린다)
  그 다음, x에 대해 Prop을 갖지 않는 것으로 알려진 어떤 고정 프로그램처럼 행동한다

P가 I에서 멈추지 않으면 P'는 첫 줄에서 영원히 멈추지 않으므로 P'가 계산하는 함수는 "아무 입력에도 답하지 않는" 함수가 된다. P가 I에서 멈추면 P'는 이후 고정된 동작으로 넘어가 특정 속성을 갖거나 갖지 않는 함수가 된다. Prop이 비자명하다는 가정 덕분에 이 두 경우를 구별하도록 P'를 구성할 수 있고, 따라서 "P'가 Prop을 갖는가"를 판정할 수 있다면 "P가 I에서 멈추는가"도 판정할 수 있게 된다 — 정지 문제의 결정 불가능성과 모순이다. 이 스케치가 보여 주려는 것은, Rice의 정리가 별도의 새로운 마법이 아니라 정지 문제의 결정 불가능성을 임의의 비자명한 의미적 속성으로 확산시키는 환원의 결과물이라는 점이다.

미니 실험: step budget으로 halted와 unknown을 구분한다

아주 작은 명령어 집합(set, dec, inc, jz, jmp, halt)을 가진 인터프리터에 step budget을 두고, 그 예산 안에서 정지하면 halted, 예산을 다 쓰면 unknown을 반환한다. 서로 다른 두 프로그램에 같은 budget을 주면 똑같이 unknown이 나오지만, budget을 늘렸을 때 한쪽만 halted로 바뀐다는 것을 직접 확인한다.

// step-budget-interpreter.ts — node step-budget-interpreter.ts 로 실행

type Instr =
  | { op: "set"; reg: string; value: number }
  | { op: "dec"; reg: string } // reg -= 1 (0 미만으로는 내려가지 않는다)
  | { op: "inc"; reg: string }
  | { op: "jz"; reg: string; target: number } // reg === 0 이면 target으로 점프
  | { op: "jmp"; target: number }
  | { op: "halt" };

type Status = "halted" | "unknown";
interface RunResult { status: Status; stepsUsed: number; registers: Record<string, number>; }

// 최소 인터프리터. "halts(program, input)"을 일반적으로 구현할 수 없다는 것이
// 이 문서의 정지 문제 논증인데, 여기서는 budget 안에서 관찰 가능한 근사만 만든다.
function run(program: Instr[], maxSteps: number): RunResult {
  const registers: Record<string, number> = {};
  let pc = 0, steps = 0;
  while (steps < maxSteps) {
    if (pc < 0 || pc >= program.length) return { status: "halted", stepsUsed: steps, registers };
    const instr = program[pc];
    steps++;
    switch (instr.op) {
      case "set": registers[instr.reg] = instr.value; pc++; break;
      case "dec": registers[instr.reg] = Math.max(0, (registers[instr.reg] ?? 0) - 1); pc++; break;
      case "inc": registers[instr.reg] = (registers[instr.reg] ?? 0) + 1; pc++; break;
      case "jz": pc = (registers[instr.reg] ?? 0) === 0 ? instr.target : pc + 1; break;
      case "jmp": pc = instr.target; break;
      case "halt": return { status: "halted", stepsUsed: steps, registers };
    }
  }
  // 예산을 다 썼다. 이것이 halt=false를 뜻하지 않는다 — "모른다"가 정확한 답이다.
  return { status: "unknown", stepsUsed: steps, registers };
}

// 프로그램 A: n부터 0까지 감소시키고 정지한다. 항상 halt한다.
function countdownProgram(n: number): Instr[] {
  return [
    { op: "set", reg: "n", value: n },   // 0
    { op: "jz", reg: "n", target: 4 },   // 1: n==0이면 탈출
    { op: "dec", reg: "n" },             // 2
    { op: "jmp", target: 1 },            // 3
    { op: "halt" },                      // 4
  ];
}
// 프로그램 C: 무조건 자기 자신으로 되돌아가는 무한 루프. 어떤 budget을 줘도 halt하지 않는다.
const trueInfiniteLoop: Instr[] = [{ op: "jmp", target: 0 }];

console.log("A(짧은 countdown, n=5):", run(countdownProgram(5), 100));

const longCountdown = countdownProgram(1_000_000);
console.log("B(긴 countdown, budget=1000):", run(longCountdown, 1000));
console.log("B(같은 프로그램, budget=5,000,000):", run(longCountdown, 5_000_000));

console.log("C(무한 루프, budget=1000):", run(trueInfiniteLoop, 1000));
console.log("C(같은 프로그램, budget=5,000,000):", run(trueInfiniteLoop, 5_000_000));

Node.js v24.14.0, Apple M5 Pro, macOS 26.6.2에서 실행한 결과다.

A(짧은 countdown, n=5): { status: 'halted', stepsUsed: 18, registers: { n: 0 } }
B(긴 countdown, budget=1000): { status: 'unknown', stepsUsed: 1000, registers: { n: 999667 } }
B(같은 프로그램, budget=5,000,000): { status: 'halted', stepsUsed: 3000003, registers: { n: 0 } }
C(무한 루프, budget=1000): { status: 'unknown', stepsUsed: 1000, registers: {} }
C(같은 프로그램, budget=5,000,000): { status: 'unknown', stepsUsed: 5000000, registers: {} }

budget=1000에서 프로그램 B(결국 종료하지만 오래 걸리는 카운트다운)와 프로그램 C(진짜 무한 루프)는 { status: 'unknown', stepsUsed: 1000 }으로 완전히 같은 결과를 낸다. budget을 늘려 보기 전에는 이 인터프리터의 출력만으로 둘을 구분할 방법이 없다. budget을 5,000,000으로 늘리자 B는 halted로 판명됐지만, C는 아무리 budget을 늘려도 결코 halted가 되지 않는다 — 정의상 한 번도 정지하지 않기 때문이다. "아직 정지 안 함"과 "영원히 정지 안 함"은 겉보기 관찰이 아니라 무한한 시간에 대한 주장이라는 점에서 근본적으로 다른 종류의 명제이고, 유한한 시간 안에 실행해 보는 것만으로는 후자를 확인할 수 없다. 실제 정적 분석기가 "타임아웃"을 "버그"가 아니라 정직한 세 번째 답("unknown")으로 다뤄야 하는 이유가 여기에 있다.

정리

• 결정 가능은 항상 멈추고 정확히 답하는 판정기의 존재를, 인식 가능은 "예"인 경우에만 멈추는 것으로 충분한 인식기의 존재를 뜻한다. 인식기가 멈추지 않는 것은 실행 중에는 "아직 계산 중"과 구분되지 않는다.
• 처치-튜링 논제는 증명된 정리가 아니라, 독립적으로 형식화된 여러 계산 모델이 같은 함수 집합으로 수렴한다는 정황에 근거한 논제다.
• 정지 문제는 판정기가 존재한다고 가정한 뒤 자기 자신을 입력으로 받는 프로그램을 구성해 모순을 끌어내는 대각선 논증으로 결정 불가능함이 증명된다.
• 환원은 이미 결정 불가능하다고 알려진 문제를 새 문제의 판정기로 풀 수 있음을 보여 새 문제의 결정 불가능성을 전달하는 방법이다.
• Rice의 정리는 프로그램이 계산하는 함수의 비자명한 의미적 속성이 일반적으로 결정 불가능하다는 것이다. 소스 코드의 겉모습에 대한 문법적 속성은 이 정리의 대상이 아니며 대개 결정 가능하다.
• 정적 분석기는 건전성, 완전성, 항상 종료 중 하나를 반드시 포기해야 하며, 이것은 도구의 미숙함이 아니라 Rice의 정리가 강제하는 필연이다.
• 특정 언어 조각, 유한 상태 시스템, 제한된 입력 크기에서는 결정 가능할 수 있다. 결정 불가능성은 일반적이고 제한 없는 경우에 대한 주장이며, "모든 정적 분석이 무의미하다"로 확대하는 것은 오류다.

확인 문제

1. 어떤 팀이 "이 정적 분석 도구는 '함수 이름이 Deprecated로 끝나는가'를 항상 정확하고 빠르게 판정하는데, 이게 Rice의 정리와 모순되지 않는가?"라고 묻는다. 모순이 아닌 이유를 설명하라.

정답과 해설

Rice의 정리는 프로그램이 계산하는 함수에 대한 비자명한 의미적 속성에 적용된다. "함수 이름이 Deprecated로 끝나는가"는 소스 코드의 표면적 표기(식별자 문자열)에 대한 질문이지, 그 함수가 어떤 입력에 대해 어떤 값을 계산하는지와는 무관한 문법적 속성이다. 문법적 속성은 소스 코드를 파싱해서 그냥 읽으면 항상 멈추고 정확히 답할 수 있으므로 결정 가능하고, Rice의 정리의 적용 대상이 아니다.

2. 다음 주장을 평가하라: "우리 서비스는 사용자가 입력한 정규식을 실행하는 기능이 있는데, ReDoS 방지를 위해 '이 정규식이 특정 악성 입력에서 무한정 느려질 수 있는가'를 사전에 완벽히 판정하는 정적 분석기를 만들면 된다." 이 요구사항이 일반적으로 왜 실현 불가능한지, 그리고 실현 가능한 축소된 버전이 있다면 무엇인지 설명하라.

정답과 해설

"임의의 정규식과 임의의 엔진 구현에 대해, 어떤 입력에서든 특정 시간 이상 걸리는지"를 일반적인 튜링 완전 프로그램 취급으로 판정하는 것은 실행 시간이라는 의미적 속성에 대한 비자명한 질문이므로 일반적으로는 결정 불가능한 문제로 귀착될 수 있다. 그러나 이 챕터가 강조하듯 이것은 "제한 없는 일반적인 경우"에 대한 주장이다. 실제로 정규식은 임의의 튜링 완전 프로그램이 아니라 유한한 문법(2.2에서 다룬 정규 언어와 그 확장)으로 제한된 대상이고, 특정 실행 전략(NFA 구조에서 모호한 반복과 겹치는 분기를 탐지하는 것)에 한정하면 실제로 위험 패턴을 판정하는 정적 도구(예: 정규식 린터)가 존재하고 실무에서 쓰인다. "일반적으로 결정 불가능하다"와 "이 좁은 문법과 한정된 실행 모델 안에서 결정 가능한 부분 문제가 있다"를 구분해야 하며, 완벽을 요구하지 않고 알려진 위험 패턴 클래스를 탐지하는 것으로 요구사항을 축소하는 것이 현실적이다.

3. 배포 파이프라인에서 "정적 분석이 30초 안에 끝나지 않으면 무한 루프가 있다고 간주해 빌드를 실패시킨다"는 정책을 쓰고 있다. 이 문서의 미니 실험과 연결해 이 정책의 어떤 전제가 틀렸는지 지적하고, 더 정확한 정책 문구를 제안하라.

정답과 해설

"30초 안에 끝나지 않으면 무한 루프다"는 "budget 초과 = 비종료의 증명"이라고 가정하는데, 미니 실험이 보였듯 이는 참이 아니다 — budget을 초과한 프로그램은 결국 종료할 예정이었지만 그저 느린 프로그램(B)일 수도 있고, 실제로 무한 루프인 프로그램(C)일 수도 있으며, 30초 시점의 관찰만으로는 둘을 구분할 수 없다. 정확한 정책 문구는 "정적 분석이 30초 안에 결론을 내지 못하면 결과를 unknown으로 취급하고, 그 경우 빌드를 실패시킬지 경고만 하고 통과시킬지는 별도의 위험 허용 정책으로 정한다"처럼, 초과를 무한 루프의 증거가 아니라 "판정 실패"로 명시해야 한다. 실제로 무한 루프인지 확인하려면 별도의 수동 검토나 다른 방식의 증거(예: 반복 횟수 상한을 코드에 명시)가 필요하다.

참고 자료

• Alan Turing, "On Computable Numbers, with an Application to the Entscheidungsproblem" (Proceedings of the London Mathematical Society, 1936) — 튜링 기계와 정지 문제의 결정 불가능성을 정식화한 원 논문.
• Alonzo Church, "An Unsolvable Problem of Elementary Number Theory" (American Journal of Mathematics, 1936) — 람다 계산법으로 독립적으로 계산 가능성을 정식화하고 결정 불가능성을 보인 원 논문.
• Henry Gordon Rice, "Classes of Recursively Enumerable Sets and Their Decision Problems" (Transactions of the American Mathematical Society, 1953) — Rice의 정리 원 논문.
• Michael Sipser, Introduction to the Theory of Computation 3rd ed. (Cengage, 2012) — 정지 문제의 대각선 논증, 환원 기법, Rice의 정리 증명을 표준 표기로 다루는 교재. 이 문서의 증명 스케치가 따르는 전개 방식이다.
• 챕터 5의 정적 분석 — 건전성·완전성 트레이드오프를 실제 도구(TypeScript, 보안 스캐너)의 정책으로 확인한다. 이 문서가 세운 "왜 그 트레이드오프가 강제되는가"의 실무 적용이다.