영역 이론: 스콧과 재귀의 의미(Domain theory)

팩토리얼⁠(factorial)⁠은 흔히 이렇게 정의합니다. fact(n)은 n = 0이면 1, 아니면 n · fact(n − 1). 식의 양쪽에 fact가 있으니 이것은 정의라기보다 방정식입니다. 재귀를 처음 배울 때는 '같은 모양의 더 작은 문제로 줄인다'고 이해하고 넘어가지만, 방정식이라면 물어야 할 것이 있습니다. 해가 있는가, 하나뿐인가? 다른 재귀 정의를 보면 걱정이 현실이 됩니다. f(n) = f(n + 1)은 모든 상수 함수가 만족합니다. f(n) = f(n)은 모든 함수가 만족합니다. 그런데 이 두 정의를 프로그램으로 돌리면 어떤 수를 넣어도 끝나지 않습니다. 컴퓨터는 수많은 해 가운데 무엇을 계산하는 걸까요? 1969–70년 미국 논리학자 데이나 스콧이 세운 영역 이론은 '가장 적게 아는 해'라고 답합니다.

먼저 방정식을 고정점⁠(fixed point)⁠ 문제로 바꿉니다. 함수 g를 받아 새 함수를 돌려주는 변환 F를 'F(g)(n)은 n = 0이면 1, 아니면 n · g(n − 1)'로 정의하면, 팩토리얼의 정의는 fact = F(fact)가 됩니다. 다시 말해 fact는 F의 고정점입니다. 고정점이 여럿일 수 있으니 고를 기준이 필요합니다. 끝나지 않는 계산의 결과를 ⊥('바닥'이라 읽습니다. 정보 없음)로 적습니다. 그러면 프로그램이 계산하는 함수는 어떤 입력에서는 값을 정하지 않아도 되는 함수가 됩니다. 이런 함수를 부분 함수라 합니다. 정수⁠(integer)⁠ 위의 부분 함수⁠(partial function)⁠들 사이에 $g \sqsubseteq h$를 'g가 값을 정한 곳에서는 h도 같은 값을 정한다'로 정의하고, 'g는 h보다 덜 안다(또는 같다)'로 읽습니다. 예를 들어 0에서만 1을 정한 함수는 0에서 1, 1에서 1을 정한 함수보다 덜 압니다. h는 g보다 더 많이 알 뿐 g와 어긋나지 않습니다. 어디서도 값을 정하지 않은 함수 ⊥가 가장 작습니다. 이것은 크기의 순서가 아니라 정보의 순서입니다. 자연수⁠(natural number)⁠에 ⊥를 더한 $\mathbb N_\bot$에서 $\bot \sqsubseteq 3$이지만 3과 4는 서로 비교되지 않습니다. 둘 다 완전한 정보이고, 서로 다를 뿐입니다.

이제 ⊥에서 출발해 F를 되풀이해 씌웁니다. F(⊥)는 0에서만 값 1을 정합니다. 0이 아닌 n에서는 ⊥(n − 1)이 필요한데 그것이 ⊥이기 때문입니다. F²(⊥)는 0과 1에서, F³(⊥)는 0, 1, 2에서 값을 정합니다. Fⁿ(⊥)는 '재귀 호출을 n − 1번까지만 허락한 팩토리얼'입니다. 한 단계씩 넘겨 보세요. 재귀 정의:

표의 각 줄은 윗줄을 그대로 품고 몇 칸을 더 채웁니다. 한 번 정해진 값은 바뀌지 않습니다. $\bot \sqsubseteq F(\bot) \sqsubseteq F^2(\bot) \sqsubseteq \cdots$. 이렇게 늘어나는 사슬에서 모든 줄이 정한 값을 모은 함수가 사슬의 상한 $\bigsqcup_n F^n(\bot)$이고, 팩토리얼에서는 모든 n에서 n!을 정하는 함수입니다. 두 번째 정의를 고르면 홀수 칸이 끝까지 ⊥로 남습니다. 홀수에서 2씩 빼면 0을 건너뛰고 음수로 끝없이 내려가니, 실제 프로그램도 홀수에서 끝나지 않습니다. 이 방정식에는 홀수에서도 값을 채운 해가 얼마든지 있지만(예: 2m + 1에서 m + 7), 최소 고정점은 프로그램이 실제로 하는 일과 정확히 같습니다. 존 매카시가 프로그램 검증의 시험 문제로 만든 91 함수는 재귀 호출 안에 재귀 호출이 들어 있어 무엇을 계산하는지 한눈에 보이지 않는데, 근삿값을 쌓아 보면 보이는 칸 88–100이 F¹²(⊥)에서 모두 91로 채워집니다. 실제로 100 이하의 모든 정수 n에서 값은 91입니다. 마지막 정의 f(n) = f(n + 1)은 몇 번을 씌워도 ⊥입니다. 상수 함수들도 고정점이지만, 가장 작은 고정점은 어디서도 끝나지 않는 ⊥이고, 이것이 프로그램의 실제 행동입니다.

이 관찰을 정리로 적으려면 낱말 셋이 필요합니다. 첫째, 가장 작은 원소⁠(element)⁠ ⊥가 있고 늘어나는 사슬마다 상한이 있는 순서 집합⁠(set)⁠을 완비 부분 순서(cpo)라 합니다. 부분 함수들의 정보 순서가 그 예입니다. 둘째, $x \sqsubseteq y$이면 $F(x) \sqsubseteq F(y)$인 F, 다시 말해 순서를 지키는 F를 단조라 합니다. 셋째, F가 늘어나는 사슬의 상한을 보존하면 F를 스콧 연속⁠(Scott continuous)⁠이라 합니다. 식으로는 $F(\bigsqcup_n x_n) = \bigsqcup_n F(x_n)$입니다. 말로 하면 '사슬을 끝까지 쌓은 뒤 F를 씌운 것'과 '줄마다 F를 씌운 뒤 쌓은 것'이 같다는 뜻입니다. 스콧 연속인 F는 늘 단조입니다.

이제 정리입니다. 흔히 클리니 고정점 정리라 부릅니다. cpo에서 F가 스콧 연속이면 $\bigsqcup_n F^n(\bot)$은 F의 고정점이고, 다른 모든 고정점 아래에(⊑) 있다. 증명은 세 줄입니다. (1) 사슬: ⊥가 가장 작으니 $\bot \sqsubseteq F(\bot)$이고, F는 단조이므로 양쪽에 F를 씌우면 $F(\bot) \sqsubseteq F^2(\bot)$, 이것을 되풀이하면 사슬 전체가 나옵니다. 수학적 귀납법⁠(mathematical induction)⁠입니다. (2) 고정점: 상한을 $x^*$라 하면

$$F(x^*) \;=\; F\Big(\bigsqcup_{n} F^{n}(\bot)\Big) \;=\; \bigsqcup_{n} F^{n+1}(\bot) \;=\; x^*.$$

가운데 등호가 연속성⁠(continuity)⁠이고, 마지막 등호는 사슬의 맨 앞 ⊥를 빼도 상한이 그대로라는 사실입니다. (3) 최소: y = F(y)인 아무 y에 대해 $\bot \sqsubseteq y$이고, 양쪽에 F를 n번 씌우면 $F^n(\bot) \sqsubseteq F^n(y) = y$. 모든 n에서 그러니 상한 $x^*$도 y 아래에 있습니다. 같은 모양으로 최소 고정점에 대한 성질을 증명하는 방법도 나옵니다. 성질 P가 ⊥에서 참이고, P(x)이면 P(F(x))이며, 늘어나는 사슬의 상한으로 넘어가도 유지되면 P는 fix(F)에서 참입니다. 스콧 귀납법⁠(Scott induction)⁠이라 부르며, 수학적 귀납법을 사슬의 상한까지 늘인 것입니다.

스콧 연속의 식 $F(\bigsqcup_n x_n) = \bigsqcup_n F(x_n)$은 연속 함수가 수열의 극한⁠(limit)⁠을 보존하는 것, $f(\lim x_n) = \lim f(x_n)$과 같은 모양입니다. 위의 (2)는 고정점 페이지의 논증 'f가 연속이면 $x_{n+1} = f(x_n)$이 다가가는 곳은 고정점'과 한 줄씩 같습니다. 거리가 줄어드는 대신 정보가 늘어날 뿐입니다.

연속성이 빠지면 무엇이 무너지는지 작은 예가 있습니다. 자연수 0, 1, 2, …를 크기 순서로 늘어놓고, 그 위에 모든 자연수보다 위에 있는 새 원소 ω(오메가)를 하나 놓고, 다시 그 위에 ω + 1을 하나 더 놓은 순서 $0 \sqsubseteq 1 \sqsubseteq 2 \sqsubseteq \cdots \sqsubseteq \omega \sqsubseteq \omega + 1$을 생각합니다. 이 순서에서 F(n) = n + 1, F(ω) = ω + 1, F(ω + 1) = ω + 1이라 합시다. F는 순서를 지키지만, 가장 작은 원소 0에서 되풀이하면 0, 1, 2, …의 상한 ω에 닿고, F(ω) = ω + 1 ≠ ω이라 ω는 고정점이 아닙니다. 최소 고정점 ω + 1에는 '무한 번 되풀이한 뒤 한 번 더'가 있어야 닿습니다. $F(\bigsqcup_n n) = \omega + 1$인데 $\bigsqcup_n F(n) = \omega$이니, 연속성이 깨진 바로 그 자리입니다.

프로그램에 연속성을 요구하는 것은 억지 제약이 아니라 사실의 기술입니다. 이런 영역에서 연속성은 '출력의 유한한 조각은 입력의 유한한 조각에만 기댄다'는 뜻이기 때문입니다. 함수 g를 받는 프로그램이 유한한 시간 안에 답을 내려면 g를 유한 번만 불러 볼 수 있습니다. 그러니 답은 g의 어떤 유한한 근삿값에서 이미 정해집니다. 반대로 'g가 모든 n에서 끝나면 1'처럼 무한히 많은 값을 봐야 하는 변환은 연속이 아니고, 프로그램으로 쓸 수도 없습니다. 정지 문제⁠(halting problem)⁠의 벽도 같은 모양으로 보입니다. 정지 문제 자체는 프로그램의 코드를 입력으로 받는 문제라 아래 논증과 같은 정리는 아니지만, 이유가 닮았습니다. $\mathbb N_\bot$에서 참·거짓(과 ⊥)으로 가는 함수 h가 h(⊥) = 참, h(3) = 거짓이라면, $\bot \sqsubseteq 3$인데 참과 거짓은 서로 비교되지 않으므로 h는 순서를 지키지 못합니다. 순서를 지키면서 h(⊥) = 참이면 모든 입력에서 참일 수밖에 없습니다. 값이 ⊥인지 보고 답하는 함수, 곧 '끝나지 않음을 알아내는' 함수는 정보의 순서를 거스르므로 이 세계에 없습니다.

스콧이 이 이론을 만든 동기는 람다 계산⁠(lambda calculus)⁠이었습니다. 람다 계산은 함수를 만들고 함수에 인자를 넣는 규칙만으로 계산을 적는 언어이고, 그 식 하나하나를 항이라 합니다. 스콧이 찾던 것은 이 언어의 모형, 다시 말해 항마다 값을 하나씩 붙여 주는 수학적 세계였습니다. 타입⁠(type)⁠ 없는 람다 계산에서는 모든 항이 함수이면서 동시에 다른 함수의 인자도 됩니다. 그러니 값들의 집합 D는 'D에서 D로 가는 함수들의 집합'과 원소를 빠짐없이 하나씩 짝지을 수 있어야(동형⁠(isomorphism)⁠이어야) 합니다. 그런데 칸토어의 대각선 논법⁠(Cantor's diagonal argument)⁠에 따르면, 원소가 둘 이상인 D에서 D로 가는 함수 전체는 D보다 엄격히 많습니다. 스콧은 처음에 이 때문에 타입 없는 람다 계산에는 수학적 모형이 없다고 보고 타입이 있는 논리를 제안했는데, 1969년 가을 연속 함수만 모으면 된다는 것을 깨달았습니다. 연속 함수는 유한한 근삿값들로 정해지므로 함수 전체보다 훨씬 적습니다.

스콧은 작은 영역 $D_0$에서 시작해, 한 단계마다 앞 단계에서 자기 자신으로 가는 연속 함수들을 모아 다음 영역 $D_{n+1} = [D_n \to D_n]$을 쌓았습니다. 이 사슬의 극한으로 지은 영역 $D_\infty$는 자기 자신에서 자기 자신으로 가는 연속 함수들의 영역과 짝이 맞습니다. 식으로 $D_\infty \cong [D_\infty \to D_\infty]$이고, ≅는 '동형'이라 읽습니다. 이 세계에서는 모든 연속 함수에 최소 고정점이 있고, 람다 계산에서 재귀를 만들어 주는 항인 Y 조합자⁠(Y combinator)⁠가 정확히 그것을 계산합니다. 데카르트 닫힌 범주⁠(cartesian closed category)⁠ 페이지에서 말한 D ≅ D^D가 이것입니다.

영국 컴퓨터 과학자 크리스토퍼 스트레이치와 스콧은 1971년, 프로그램마다 이런 영역의 원소 하나를 그 프로그램의 '뜻'으로 붙이는 방법을 내놓았습니다. 이것을 표시적 의미론⁠(denotational semantics)⁠이라 합니다. 반복문 while b do C(b가 참인 동안 C를 되풀이하라)의 뜻도 최소 고정점으로, '0번 돌고 끝나는 경우, 1번 돌고 끝나는 경우, …'를 쌓아 올린 상한입니다. 데이크스트라가 1975년에 내놓은 최약 전조건⁠(weakest precondition)⁠도 같은 방식으로 계산됩니다. 최약 전조건은 '반복문이 끝나고, 끝난 뒤 원하는 조건이 성립한다'를 보장하는 시작 조건 가운데 가장 느슨한 것이고, 호어 논리⁠(Hoare logic)⁠와 함께 쓰는 계산법입니다.

1977년 고든 플롯킨은 재귀를 위한 상수 fix를 가진 작은 언어 PCF에서, 영역 모형이 프로그램보다 조금 더 많은 것을 담는다는 것을 보였습니다. 예가 '병렬 또는'입니다. 두 인자 가운데 하나라도 참이면, 다른 쪽이 끝나지 않아도 참을 돌려주는 함수입니다. 이 함수는 연속이라서 모형에는 있지만, 인자를 하나씩 차례로 계산하는 PCF로는 쓸 수 없습니다. 첫 인자가 끝나지 않으면 둘째 인자를 볼 차례가 오지 않기 때문입니다. 그래서 모형과 언어가 정확히 맞는 모형을 찾는 문제가 생겼습니다. 이런 모형을 완전 추상 모형이라 합니다. 같은 1977년 로빈 밀너가 그런 모형이 있음을 보였지만, 그의 모형은 프로그램의 문법으로부터 지은 것이었습니다. 문법을 빌리지 않고 수학적으로 지은 완전 추상 모형은 1990년대 중반 무렵 게임 의미론⁠(game semantics)⁠이 내놓을 때까지 이 분야의 큰 문제로 남았습니다. 게임 의미론은 프로그램을 '환경이 묻고 프로그램이 답하는' 질문과 답의 주고받기로 보는 모형입니다.

같은 1977년 파트리크 쿠소와 라디아 쿠소는 추상 해석⁠(abstract interpretation)⁠을 내놓았습니다. 프로그램을 실제 값으로 돌리는 대신 '음수·0·양수' 같은 요약으로 계산해, 프로그램을 실행하지 않고도 그 성질을 미리 알아내는 방법입니다. 계산은 격자 위의 최소 고정점으로 합니다. 격자는 어느 두 원소에도 상한(둘 다의 위에 있는 것 가운데 가장 작은 것)과 하한(둘 다의 아래에 있는 것 가운데 가장 큰 것)이 있는 순서입니다. 실제 값의 격자와 요약의 격자를 갈루아 연결⁠(Galois connection)⁠로 잇는 것이 핵심이며, 오늘날 컴파일러⁠(compiler)⁠와 정적 분석 도구의 이론적 바탕입니다.

연속성 없이 쓰는 고정점 정리⁠(fixed-point theorem)⁠도 있습니다. 두 원소뿐 아니라 모든 부분집합⁠(subset)⁠에 상한과 하한⁠(lower bound)⁠이 있는 순서를 완비 격자라 합니다. 완비 격자⁠(complete lattice)⁠에서는 순서를 지키는 모든 F에 최소 고정점이 있고, 그것은 $F(x) \sqsubseteq x$인 x들의 하한입니다. 이것이 크나스터–타르스키 정리입니다. 1928년 크나스터와 타르스키가 한 집합의 부분집합 전체(멱집합⁠, power set⁠)에 대해 증명했고, 1955년 타르스키가 모든 완비 격자로 넓혔습니다. 다만 이 정리는 있다는 것만 말할 뿐, ⊥에서 몇 걸음 만에 닿는지는 말하지 않습니다. 위의 ω + 1처럼 무한 번을 넘는 되풀이가 필요할 수 있습니다. 범주론⁠(category theory)⁠에서는 같은 생각이 함자⁠(functor)⁠의 고정점으로 올라갑니다. 자연수나 리스트 같은 재귀적 자료형은 함자의 가장 작은 고정점이고(이것을 시작 대수라 합니다), 람베크의 보조정리⁠(lemma)⁠가 그것이 정말 고정점임을 말해 줍니다. 재귀 함수⁠(recursive function)⁠의 최소 고정점과 재귀 타입의 시작 대수는 같은 원리의 두 층입니다.

흔한 오해 둘. 첫째, ⊥는 프로그램이 돌려주는 특별한 값(null이나 오류 코드)이 아닙니다. 돌려주는 값이 없다는 사실을 수학 안에 적는 자리입니다. 위의 h처럼, 프로그램은 ⊥인지 검사할 수 없습니다. 둘째, '최소'는 가장 작은 수가 아니라 가장 적게 아는 것입니다. f(n) = f(n + 1)의 최소 고정점은 상수 0이 아니라 모든 n에서 ⊥인 함수입니다.

이어지는 곳.

• 고정점: 되풀이해 다가간 곳이 고정점이 되는 논증의 원형입니다. 여기서는 거리 대신 정보의 순서가 그 역할을 합니다.
• 재귀와 람다 계산: 재귀로 정의한 함수와 Y 조합자가 무엇을 뜻하는지가 이 이론의 첫 질문이었습니다.
• 단순 타입 람다 계산⁠(simply typed lambda calculus)⁠과 커리–하워드 대응⁠(Curry–Howard correspondence)⁠: 타입이 있는 언어에 fix를 더하면 끝남과 논리의 무모순성⁠(consistency)⁠을 함께 잃는다는 이야기입니다.
• 정지 문제: 끝나지 않음을 검사할 수 없다는 관찰을 순서의 언어로 다시 본 것이 이 페이지의 h입니다.
• 갈루아 연결: 두 순서 사이의 짝으로 근삿값을 계산하는 도구입니다.
• 시작 대수: 재귀 타입을 함자의 가장 작은 고정점으로 봅니다.
• 호어 논리: 반복문의 뜻을 최소 고정점으로 계산하는 일이 최약 전조건에서 다시 나옵니다.
• 연속과 극한: 스콧 연속성은 극한의 보존입니다. 실제로 스콧 연속 함수는 '스콧 위상⁠(Scott topology)⁠'이라는 위상(topology)에서의 연속 함수와 정확히 같습니다.