고정점: 극한에 도달하는 것으로서의 추론

📍 현재 위치: 2부 · 계산으로서의 추론 — 7장. 리졸루션과 SLD에서는 기계가 하나의 목표로부터 거꾸로 거슬러 올라가며 그 목표 하나를 증명하는 방법을 보았다. 이제 우리는 방향을 돌려, 한 번의 훑기로는 결코 도달할 수 없는 극한을 향해 앞으로 나아가며 뒤따르는 모든 것을 계산한다.

후방 추론(backward reasoning)은 질문을 던지고 그것을 거슬러 쫓는다. 전방 추론(forward reasoning)은 그 반대다. 가지고 있는 사실들을 받아들여, 적용 가능한 모든 규칙을 발화시키고, 이를 반복해서 알려진 진리의 집합을 키워 나가다가 어느 라운드가 새로운 것을 하나도 더하지 못할 때 멈춘다. 이 "더 이상 새로운 것이 나타나지 않을 때까지"라는 조건은 단순한 프로그래밍상의 편의가 아니다. 이것은 정확한 수학적 대상, 즉 어떤 연산자의 최소 고정점(least fixpoint)이며, 이 시리즈가 계속해서 마주치는 네 가지 것 — 전방 연쇄, 데이터로그 질의 평가, 추이 폐쇄, 그리고 2권에서 다룰 기술 논리 완성 알고리즘 — 밑에 숨어 있는 것과 동일한 대상임이 드러난다. 이 장은 바로 그 하나의 아이디어와, 재귀(recursion)가 정확히 왜 피할 수 없는 지점인지에 관한 것이다.

이 장은 이 아이디어를 아무것도 없는 데서부터 쌓아 올린다. 우리는 "아무것도 바뀌지 않을 때까지 반복한다"를 블랙박스로 취급하지 않을 것이다. 우리는 그 극한이 존재함을 증명하고(크나스터–타르스키), 바닥에서 시작한 등반이 그 극한에 도달하며 유한한 세계에서는 멈춘다는 것을 증명하고(클레이니 구성), 전방 연쇄 뒤에 있는 연산자가 이 정리들이 요구하는 바로 그 성질을 가진다는 것을 증명한 다음, 실행 예제 위에서 그 등반을 손으로 직접 실행하며, 커밋된 코드가 출력하는 정확한 [23, 41, 47, 47] 파동을 따라 사실 집합이 커지는 것을 지켜볼 것이다. 이 장을 마칠 즈음이면 여러분은 거의 모든 기호적 추론기를 읽으면서 그 안에서 하나의 루프가 자신을 바라보고 있음을 알아볼 수 있게 될 것이다.

쉽게 말하면

어느 학과에 소문이 퍼지는 상황을 상상해 보자. 첫째 날, 소문을 처음 낸 사람이 자기 친구들에게 이야기한다. 둘째 날에는 그 사람들이 자기 친구들에게 이야기하는데, 그중에는 첫째 날에는 결코 들을 수 없었던 사람들도 포함된다. 그들은 원천으로부터 두 다리 건너 있기 때문이다. 매일 그 원은 커지고, 결국 아무도 새로 아는 것이 없는 날이 오면 그 소문은 앞으로도 도달할 모든 사람에게 도달한 것이다. 그 마지막 원이 바로 고정점(fixpoint)이다. "친구에게 말하기"라는 단계를 그 원에 적용해도 아무것도 바뀌지 않는다. 하루 만에 그것을 찾아낼 수는 없었을 것이다. 친구의 친구는 친구가 들은 다음에야 듣기 때문이다. 전방 연쇄에 의한 추론은 정확히 이와 같으며, "아는 사람들" 자리에 "규칙이 도출할 수 있는 사실들"이 놓여 있을 뿐이다.

이 장에서 다루는 내용

• 사실 집합의 격자 — 가능한 모든 원자(atom)의 부분집합 전체를, ⊆로 순서를 매기고, 최소원(bottom) ⊥(아무것도 알려지지 않음)와 최대원(top) ⊤(모든 것)를 갖춘 것으로 보고, 이 장 전체가 그 위에서 돌아가는 두 가지 순서 개념(단조 사상, 상승 사슬)을 살펴본다.
• 증명된 크나스터–타르스키 — 완비 격자 위의 단조 연산자는 항상 최소 고정점을 가진다는 것을, 그 연산자가 자기 자신 안으로 사상하는 모든 집합들의 교집합으로서 존재함을 증명한다.
• 증명된 클레이니의 등반 — ⊥에서부터 반복하면 상승 사슬이 만들어지고, 유한한 정의역 위에서는 그 사슬이 반드시 바로 그 최소 고정점에서 멈춘다는 것을 증명한다. 이 증명은 실제 루프의 종료 조건 그 자체다.
• 즉각귀결 연산자(immediate-consequence operator) $T_P$ — 전방 연쇄란 바로 $T_P$를 반복하는 것이다. 우리는 (규칙의 몸체가 양(positive)이기 때문에) 그것이 단조적임을 증명한 다음, forward_chain.py에서 실제로 실행해 본다.
• [23, 41, 47, 47] 파동을 원자 단위로 풀어보기 — 어느 원자가 어느 라운드에 들어오는지, 그리고 왜 person이 researcher보다 한 파동 늦게, 두 홉짜리 인용이 한 홉짜리보다 한 파동 늦게 나타나는지에 대한 전체 추적.
• 재귀가 왜 고정점을 요구하는가 — 일반 규칙들의 사슬은 한정된 횟수의 패스만 필요로 하지만, 재귀는 그 횟수가 데이터에 따라 달라지게 만들기 때문에 정해진 만큼 펼쳐두는 어떤 방법도 안전하지 않다.
• 동일한 루프로서의 추이 폐쇄 — 관계(relation) 위에서 벌어지는 똑같은 "극한까지 반복한다"는 아이디어를, sets_relations.py에서 인용하고 추적한다.
• 되풀이되는 엔진, 그리고 그 최전선 — 기술 논리 완성(2권)과 미분 가능한 고정점 레이어(4권)가 왜 동일한 패턴인지, 그리고 존재 규칙과 체이스가 어떻게 그 등반을 끝없이 이어지게 만들 수 있는지.

사실 집합의 격자: 단조 사상과 커지는 사슬

순서와 격자에서 나온 두 가지 아이디어가 여기서 필요한 도구의 전부이므로, 우리가 실제로 추론하는 대상들 위에서 그것들을 되짚어 보자. 학계 세계가 진술할 수 있는 모든 접지 원자(ground atom)를 하나의 커다란 풀(pool)로 모아 보자: ("professor", "alice") 하나하나, ("citesTransitively", "p3", "p1") 하나하나, 다섯 명의 사람과 세 편의 논문 가운데 어떤 선택에 적용되든 모든 술어(predicate)마다 하나씩의 원자다. 논리학자들은 이 풀을 허브랜드 베이스(Herbrand base)라고 부르며, 이를 $H$라고 쓴다. "현재 무엇이 알려져 있는가"의 한 스냅샷은 $H$의 어떤 부분집합이며, 추론은 부분집합들 사이를 옮겨 다니는 것이다.

이 논증을 지탱하는 것은 두 개의 기호다. 부분집합 관계 $A \subseteq B$("$A$는 $B$의 부분집합이다"라고 읽는다)는 $A$에 있는 모든 원자는 $B$에도 있다는 뜻이며, 따라서 $B$는 적어도 $A$가 아는 모든 것을 안다. 소속 기호 $a \in A$("$a$는 $A$의 원소이다"라고 읽는다)는 원자 $a$가 집합 $A$ 안에 들어 있다는 뜻이다. ⊆로 순서를 매기면, $H$의 부분집합들은 완비 격자(complete lattice)를 이룬다: 그 가운데 어떤 모음이든, 심지어 무한한 모음이라도, 최소상계(least upper bound)와 최대하계(greatest lower bound)를 가진다. 구체적으로, 사실 집합들에 대해 최소상계는 합집합(union) $\bigcup$이고(모든 원자를 한데 모은 것, 즉 그것들을 모두 포함하는 가장 작은 집합), 최대하계는 교집합(intersection) $\bigcap$이다(모두에 공통된 원자만 남긴 것, 즉 각각에 포함되는 가장 큰 집합). 최소원(bottom) ⊥는 공집합 $\varnothing$이며(아직 아무것도 유도되지 않음), 모든 것 가운데 가장 작은 집합이다. 최대원(top) ⊤는 $H$ 그 자체이며(생각할 수 있는 모든 것), 가장 큰 집합이다.

단조 사상(monotone map)이란 이 격자 위에서 순서를 결코 뒤섞지 않는 함수 $F$이다:

$$A \subseteq B \quad\Longrightarrow\quad F(A) \subseteq F(B).$$

화살표 $\Longrightarrow$는 "함의한다(implies)"라고 읽는다. 말로 풀면: 단조 연산자에 더 큰 사실 집합을 먹이면, 그것이 돌려줄 수 있는 결과는 오직 더 큰 것뿐이며, 결코 더 작아지지 않는다. 상승 사슬(ascending chain)이란 오직 커지기만 하는 집합들의 수열이다,

$$X_0 \subseteq X_1 \subseteq X_2 \subseteq \cdots,$$

여기서 아래첨자는 그저 하나의 카운터이며, $X_t$는 "$t$번의 단계 이후"의 집합이다. 추론이란, 알고 보면, 바로 이런 사슬 하나를 쌓아 올리고 그 극한을 읽어 내는 행위다. 아래에 나오는 모든 내용은 이 두 개념을 어느 특정한 연산자에 적용한 것이다.

크나스터–타르스키: 단조 연산자는 항상 정착한다

여기 "아무것도 바뀌지 않을 때까지 반복한다"를 그저 희망 사항이 아니라 정당한 것으로 만들어 주는 정리가 있다. 연산자 $F$의 고정점(fixpoint)이란 $F$가 자기 자신으로 사상하는 집합 $X$, 즉 $F(X) = X$이다: 연산자를 적용해도 아무것도 움직이지 않는다. 크나스터–타르스키 정리(Knaster–Tarski theorem)는 완비 격자 위의 모든 단조 연산자가 고정점을 가지며, 그 가운데 유일하게 가장 작은 것, 즉 $\mathrm{lfp}(F)$라고 쓰는 최소 고정점(least fixpoint)이 다른 모든 고정점 안에 포함되어 있다고 말한다 [1].

대부분의 교재는 이것을 진술하고 넘어간다. 우리는 우리가 의지하는 부분, 즉 최소 고정점이 존재한다는 것을 증명한다. 그 증명은 짧은 세 단계로 이루어져 있으며, 우리가 그것을 계산하기 전에 그 극한이 어디에 사는지를 보여주기 때문이다.

최소 고정점은 존재한다: 증명

$F$를 적용해도 더 높이 밀어 올려지지 않는 집합, 즉 $F(X) \subseteq X$인 집합 $X$를 $F$에 대해 닫혀 있다(closed)고 부르자. 닫힌 집합들을 모두 모아 하나의 모음으로 만들면,

$$\mathcal{C} \;=\; \{\, X \subseteq H : F(X) \subseteq X \,\}.$$

(집합 구성 표기의 중괄호는 "…인 모든 $X$"라고 읽고, 콜론은 "…인"이라고 읽는다.) 이 모음은 비어 있지 않은데, 최대원 ⊤가 닫혀 있기 때문이다: 모든 집합이 최대원의 부분집합이므로 $F(\top) \subseteq \top$은 자동으로 성립한다. 이제 $\mathcal{C}$ 안의 모든 것의 교집합을 만들자,

$$m \;=\; \bigcap \mathcal{C},$$

이는 모든 닫힌 집합에 공통된 원자들이다. 우리는 $m = \mathrm{lfp}(F)$임을 세 단계로 주장한다.

단계 A — $m$ 자체가 닫혀 있다. 임의의 닫힌 집합 $X \in \mathcal{C}$를 고르자. $m$은 $X$를 포함하는 모음의 교집합이므로 $m \subseteq X$이다. 단조성은 이것을 $F(m) \subseteq F(X)$로 바꾸고, $X$가 닫혀 있다는 것은 $F(X) \subseteq X$를 뜻한다. 두 포함관계를 이으면 $F(m) \subseteq X$이다. 이것은 모든 $X \in \mathcal{C}$에 대해 성립하므로, $F(m)$은 모든 닫힌 집합보다 아래에 있고, 따라서 그것들의 교집합보다도 아래에 있다: $F(m) \subseteq \bigcap \mathcal{C} = m$. 그러므로 $m$은 닫혀 있다.

단계 B — $m$은 실제로 고정점이다. 방금 증명한 포함관계에 $F$를 적용하자. 단조성은 $F(F(m)) \subseteq F(m)$을 주는데, 이는 $F(m)$ 역시 닫혀 있다는 뜻이므로 $F(m) \in \mathcal{C}$이다. 그런데 $m$은 $\mathcal{C}$의 하계이며 모든 원소보다 아래에 있으므로 $m \subseteq F(m)$이다. 이제 우리는 $F(m) \subseteq m$(단계 A)과 $m \subseteq F(m)$을 모두 가지고 있다. 부분집합 순서는 반대칭적(antisymmetric)이다 — 순서와 격자에서 보았듯, $A \subseteq B$이고 $B \subseteq A$이면 함께 $A = B$를 강제한다 — 따라서 $F(m) = m$이다. 모든 닫힌 집합의 교집합은 진짜 고정점이다.

단계 C — $m$은 최소 고정점이다. $Y$를 임의의 고정점, 즉 $F(Y) = Y$라고 하자. $F(Y) = Y$이므로 특히 $F(Y) \subseteq Y$이고, 따라서 $Y$는 닫혀 있으며 $Y \in \mathcal{C}$이고, 그러므로 $m = \bigcap\mathcal{C} \subseteq Y$이다. 따라서 $m$은 모든 고정점보다 아래에 있다: 그것이 바로 최소인 것이다. $\;\blacksquare$

이것은 존재 보장이다: 목표(모든 닫힌 집합의 교집합)가 어디에 있는지를 알려주지만, 그곳까지 걸어가는 절차를 건네주지는 않는다. 그것을 위해서는 구성적인 짝이 필요하다.

클레이니의 등반은 그곳에 도달하며, 유한한 세계에서는 멈춘다

최소원 ⊥에서 시작해 $F$를 계속해서 적용해 보자. $F^t$를 "$F$를 $t$번 적용한 것"이라고 쓰면, $F^0(\bot) = \bot$, $F^1(\bot) = F(\bot)$, $F^2(\bot) = F(F(\bot))$, 이런 식으로 이어진다:

$$\bot \;\subseteq\; F(\bot) \;\subseteq\; F(F(\bot)) \;\subseteq\; F(F(F(\bot))) \;\subseteq\; \cdots$$

이것은 상승 사슬이다. 첫 번째 연결고리 $\bot \subseteq F(\bot)$은 공짜로 얻어진다. ⊥가 공집합이고, 공집합은 모든 것의 부분집합이기 때문이다. 이 포함관계를 단조 함수 $F$에 통과시키면 $F(\bot) \subseteq F(F(\bot))$을 얻고, 그것을 다시 $F$에 통과시키면 다음 연결고리를 얻는다. 귀납법에 의해 모든 단은 그 아래 단만큼은 높은 곳에 놓인다. 바닥에서부터 이 사슬을 타고 올라가 그 극한을 취하는 것이 바로 클레이니 고정점 구성(Kleene fixed-point construction)이다 [2].

유한한(finite) 정의역 위에서는 이 등반이 반드시 멈춘다. $|X|$가 $X$의 농도(cardinality), 즉 그 안에 있는 원자의 단순한 개수를 나타낸다고 하자. 사슬을 따라가면 $|X_t|$는 전체 풀의 크기인 $|H|$로 상한이 잡힌, 감소하지 않는 정수다. 각각의 엄격한(strict) 성장 단계 $X_t \subsetneq X_{t+1}$(기호 ⊊는 "부분집합이지만 같지 않다"는 뜻이다)은 적어도 하나의 원자를 더하므로, 그 개수를 적어도 하나 늘린다. 유한하게 시작해서 오직 오르기만 하고 $|H|$를 넘어설 수 없는 개수는 오직 유한하게만 오를 수 있다. 따라서 아무것도 새로 도착하지 않는 첫 번째 지표 $n$, 즉 $F^{n+1}(\bot) = F^{n}(\bot)$인 지표가 존재하며, 그 지표에서 $F$는 그 집합을 자기 자신으로 사상한다: $X_n = F(X_n)$은 고정점이다.

그것이 최소 고정점일까? 그렇다. 그리고 이것이 바로 두 정리를 하나로 묶어 주는 보상이다. 임의의 고정점 $Y$를 잡고, 귀납법으로 모든 $t$에 대해 $F^t(\bot) \subseteq Y$임을 증명해 보자. 기저: $F^0(\bot) = \varnothing \subseteq Y$. 귀납 단계: $F^t(\bot) \subseteq Y$이면, 단조성에 의해 $F^{t+1}(\bot) = F(F^t(\bot)) \subseteq F(Y) = Y$이다. 따라서 사슬 전체가 모든 고정점 안에 들어 있다. 특히 우리가 도달한 고정점 $X_n$도 모든 고정점 안에 들어 있으므로, 그것은 앞의 증명에서 나온 $\mathrm{lfp}(F) = m$ 바로 그것이다. 바닥에서 시작한 등반은 그저 어떤 고정점 하나를 찾는 것이 아니다. 유한한 세계에서는 유한한 단계 만에 최소 고정점을 찾아낸다.

(무한한 격자 위에서도 최소 고정점은 크나스터–타르스키에 의해 여전히 존재하지만, 그 등반이 그곳에 도달하는 것은 오직 $F$가 연속적(continuous)일 때뿐이다 — 즉 사슬 전체의 합집합에 $F$를 적용한 것이 각 단에 $F$를 적용한 것들의 합집합과 같을 때, $F(X_0 \cup X_1 \cup \cdots) = F(X_0) \cup F(X_1) \cup \cdots$일 때다 — 그리고 그럴 때조차 답은 어느 유한한 단계가 아니라 무한한 사슬 전체의 최소상계일 수 있다. 전방 연쇄 뒤에 있는 연산자와 추이 폐쇄는 유한적(finitary)이다: 그것들이 유도하는 각 원자는 오직 유한히 많은 입력 사실만을 읽는데, 규칙 하나의 발화가 한정된 몸체만을 참조하기 때문이다. 유한적 연산자는 자동으로 연속적인데, 무한한 사실들의 합집합으로부터 그것이 만들어 내는 무엇이든 이미 그 합집합의 어떤 유한한 부분에서 나타나기 때문이다. 그러므로 이 등반은 유효하다. 최전선을 다루는 절에서는 그것이 결코 멈추지 않는 경우로 되돌아간다.)

즉각귀결 연산자 T_P

전방 연쇄 뒤에 있는 연산자에는 이름이 있다: 즉각귀결 연산자(immediate-consequence operator)로, $T_P$라고 쓴다("P"는 규칙들의 프로그램(program)을 뜻한다). 그 역할은 한 문장으로 요약된다: 현재 사실들에 의해 몸체가 충족되는 모든 규칙을 발화시키고, 그 결과로 나오는 머리를 모두 더한다. 사실들의 집합에 적용하면, 그 사실들에 더해 단 한 단계로 유도 가능한 모든 것을 돌려준다. forward_chain.py에서 이것은 다섯 줄짜리 함수이며(독스트링을 포함하면 여덟 줄), 그 문장의 각 절이 몸체의 한 줄에 대응한다:

def t_p(facts: set, rules: list) -> set:
    """One application of the immediate-consequence operator: the input facts
    plus every head derivable in a single step."""
    out = set(facts)
    for head, body in rules:
        for sub in _match_body(body, facts, {}):
            out.add(apply_sub(head, sub))
    return out

한 줄씩 보면: out = set(facts)는 현재 사실들을 복사해 들여온다(그래서 $T_P$는 결코 아무것도 지우지 않는다). rules에 대한 반복은 규칙 하나하나를 시도한다. _match_body는 현재 사실들 안에서 몸체 전체를 참으로 만드는 모든 변수-상수 치환(substitution)을 산출한다. 그리고 out.add(apply_sub(head, sub))는 그 치환 아래에서 머리를 더함으로써 규칙을 발화시킨다. 출력은 입력에 한 단계짜리 귀결들을 더한 것이며, 정확히 $T_P(X)$이다.

T_P는 단조적이다(정리들이 필요로 하는 단 하나의 성질)

크나스터–타르스키와 클레이니의 등반은 모두 $T_P$에게 단 한 가지, 즉 단조성만을 요구한다. 여기 그 증명이 있으며, 이는 규칙들의 단 하나의 특징에 기대고 있다.

$A \subseteq B$라고 가정하고, 임의의 원자 $h \in T_P(A)$를 잡자. $h$가 $T_P(A)$ 안에 들어오는 데는 두 가지 방법이 있다. $h$가 이미 입력 사실이었던 경우, $h \in A$이다. 그러면 $A \subseteq B$이므로 $h \in B$이고, $T_P$는 자신의 입력을 복사하므로 $h \in T_P(B)$이다. 아니면 $h$는 어떤 치환 아래서 $A$에 의해 몸체가 충족된 어떤 규칙의 머리이다 — 즉 그 (구체화된) 몸체의 모든 원자가 $A$의 원소라는 뜻이다. $A \subseteq B$이므로 그 몸체 원자들 하나하나는 역시 $B$의 원소이며, 따라서 바로 그 동일한 몸체가 바로 그 동일한 치환 아래서 $B$에 의해 충족되고, 따라서 같은 규칙이 $B$에서 발화되어 같은 머리를 만들어 낸다: $h \in T_P(B)$이다. 어느 경우든 $h \in T_P(B)$이므로, $T_P(A) \subseteq T_P(B)$이다. $\;\blacksquare$

이 증명을 떠받치는 단계는 "$A$의 모든 몸체 원자는 $B$에도 있다"이다. 이것이 성립하는 것은 오직 모든 규칙 몸체가 긍정 논리곱(positive conjunction)이기 때문이다 — 즉 부정이 없는 혼 절(Horn clause)이기 때문이다. 사실을 더하는 것은 더 많은 규칙 몸체를 충족시킬 수 있을 뿐 결코 더 적게 충족시키지 않으므로, 사실이 늘어날수록 귀결도 늘어난다. 만약 몸체에 "$X$는 교수가 아니다"와 같은 부정이 들어 있었다면, 사실 집합을 키우는 것이 그 조건을 꺼버려 이전에는 유도 가능했던 머리를 파괴할 수 있었을 것이고, 그러면 단조성이 깨지고 그와 함께 위의 모든 보장도 깨졌을 것이다. 이것이 바로 실행 예제가 순수하게 혼(Horn) 형태인 이유이며, 부정이 고정점 추론을 미묘하게 만드는 첫 번째 요소인 이유다. 코드에서 이 긍정성은 _match_body에서 눈에 보인다: 그것은 실제 fact를 찾아 unify함으로써 각 몸체 원자를 충족시키며(for fact in facts: ext = unify(first, fact, sub)), 사실이 아닌 유일한 검사인 내장된 neq 가드는 두 인자가 서로 다른지를 비교할 뿐, 어떤 원자가 부재하는지를 결코 묻지 않는다.

(별개로, $T_P$는 결코 사실을 지우지 않으므로 팽창적(inflationary)이기도 하다: out = set(facts)의 복사로부터 $X \subseteq T_P(X)$가 나온다. 팽창성과 단조성은 서로 다르다 — 팽창성은 하나의 입력을 그 자신의 출력과 비교하고, 단조성은 서로 다른 두 입력을 비교한다 — 그리고 정리들이 요구하는 것은 더 어려운 쪽인 단조성이다.)

단조성을 손에 넣고 나면, 최소 고정점에 도달하는 것은 상상할 수 있는 가장 단순한 루프이며, 이는 문자 그대로 위의 두 정리를 실행 가능하게 만든 것이다:

def least_fixpoint(facts, rules, trace: bool = False):
    current = set(facts)
    sizes = [len(current)]
    while True:
        nxt = t_p(current, rules)
        sizes.append(len(nxt))
        if nxt == current:
            return (current, sizes) if trace else current
        current = nxt

current = set(facts)는 등반을 기본 사실들에서 시작시키는데, 이는 클레이니의 등반을 한 단 위에서부터 시작한 것과 같다: 기본 사실들을 (공허하게 충족되는 빈 몸체를 가진) 규칙으로 상상해 본다면, $T_P(\bot)$은 이미 그것들을 포함할 것이므로, 기본 사실들로 씨앗을 뿌리는 것과 ⊥로 씨앗을 뿌리는 것은 같은 사슬에 도달한다. nxt = t_p(current, rules) 줄은 한 번의 적용 $X_{t+1} = T_P(X_t)$이다. 그리고 if nxt == current는 종료 증명을 if문으로 바꾸어 놓은 것이다: $T_P(X) = X$가 되는 바로 그 순간, 유한성 논증은 우리가 최소 고정점에 도달했다고 말해 주며, 루프는 멈춘다.

파동을 원자 단위로 풀어보기

이 모듈을 학계 세계에 대해 실행하면 그 등반을 보고한다(이것은 python3 forward_chain.py의 실제 출력이다):

least fixpoint reached in 3 rounds; sizes per round: [23, 41, 47, 47]
47 atoms total, 24 derived.

추적값 [23, 41, 47, 47]을 상승 사슬 그 자체, 즉 $X_0 \subseteq X_1 \subseteq X_2 \subseteq X_3$로 읽되, 그 크기 $|X_t|$가 단마다 출력된 것으로 읽어라. 마지막의 $47 = 47$은 아무것도 바꾸지 않는 라운드이며, 그래서 nxt == current에 의해 우리가 끝났음을 증명한다. 다음은 정확히 어느 원자가 어느 단에 들어오는지를 보여준다 — 아래의 모든 숫자와 원자는 실제 실행을 계측해서 얻은 것이며, 지어낸 것이 아니다:

라운드 $t$	단 $X_t = T_P^{\,t}(\text{base})$	$\lvert X_t\rvert$	이번 라운드에 더해진 원자	발화된 규칙
$0$	기본 사실들(씨앗)	$23$	23개의 진술된 사실	아직 없음(씨앗)
$1$	$T_P(X_0)$	$41$	$+18$: researcher×5, grandAdvisor×3, colleague×8, citesTransitively×2	몸체가 기본 사실을 읽는 모든 규칙
$2$	$T_P(X_1)$	$47$	$+6$: person×5, citesTransitively p3→p1 ×1	유도된 사실을 읽는 두 규칙
$3$	$T_P(X_2)$	$47$	$+0$	모든 발화가 이미 존재하는 원자를 반복함

전체 메커니즘은 마지막 열에 담겨 있다. 라운드 1은 이미 상 위에 있는 기본 사실들에 의해 몸체가 충족되는 규칙들만 발화시킨다. 다섯 개의 researcher 원자는 researcher(X) :- professor(X)와 researcher(X) :- student(X)에서 나온다(:-는 "…이면 성립한다"라고 읽는다: 왼쪽의 머리는 오른쪽의 몸체가 성립할 때마다 성립한다). 세 개의 grandAdvisor 원자는 advises를 자기 자신과 합성한 데서 나온다 — grandAdvisor(X,Z) :- advises(X,Y), advises(Y,Z) — 이는 alice→bob→carol, alice→bob→dave, bob→carol→erin 사슬 위에서 발화한다. 여덟 개의 colleague 원자는 같은 소속 기관을 공유하는 순서쌍들이며(mit에서 둘: alice–bob 양방향; cmu에서 여섯: carol, dave, erin 사이), neq 가드가 어떤 사람이 자기 자신의 동료가 되는 것을 막아 준다. 그리고 두 개의 citesTransitively 원자, p2→p1과 p3→p2는 기저 사례(base case) 규칙 citesTransitively(A,B) :- cites(A,B)에서 나온다.

라운드 2에서는 유도된 사실에 대한 의존이 드러난다. 여기서 새로 생긴 여섯 개의 원자는 모두 라운드 1에서는 발화될 수 없었던 결론들인데, 그 몸체들이 라운드 1이 막 만들어 낸 무언가를 필요로 했기 때문이다:

• 다섯 개의 person 원자는 person(X) :- researcher(X)에서 나온다. 그 몸체는 researcher 원자를 읽는데, 그 원자는 라운드 0에는 존재하지 않았고 라운드 1에 처음 나타났다. 그래서 person(alice)는 정확히 researcher(alice)보다 한 파동 뒤처져 있다. 라운드 2에서 더해진 여섯 개의 원자 가운데 다섯 개가 person(...)이다: 이 규칙 하나가 두 번째 파동의 대부분을 차지한다.
• 남은 하나의 원자, citesTransitively(p3, p1)은 재귀 규칙에서 나오며, 다음 절의 핵심이다.

라운드 3은 모든 규칙을 다시 발화시키지만 이미 $X_2$ 안에 있는 원자만을 만들어 내므로, $X_3 = X_2$이다: 고정점이다. 그 극한은 47개의 원자이며, 그 가운데 24개가 유도된 것이다. 이 집합에는 이 알고리즘보다도 더 오래된 이름이 있다: 바로 그 프로그램의 최소 허브랜드 모델(least Herbrand model), 즉 모든 규칙을 참으로 만드는 가장 작은 사실 모음이다. 논리 프로그래밍의 고전적인 결과는 전방 연쇄와 최소 모델 의미론(least-model semantics)이 같은 것을 계산한다는 것이며, 따라서 $\mathrm{lfp}(T_P)$는 그저 그 프로그램의 의미 그 자체이다 [3]. 절차와 의미가 일치하며, 그 일치가 바로 위의 두 증명이다.

재귀가 한 번의 훑기가 아니라 고정점을 필요로 하는 이유

서로 다른 두 가지가 이 루프를 한 번의 통과 이상으로 밀어붙이며, 이 둘을 구분해 두는 것이 값어치가 있다. 온건한 쪽은 일반 규칙들의 사슬이다: 유도된 사실을 읽는 규칙은 그것을 만들어 내는 통과를 기다려야 한다. 우리는 방금 그런 예를 하나 보았다 — person은 researcher를 기다리고, researcher는 professor나 student를 기다린다 — 그래서 person(alice)는 researcher(alice) 다음 파동이 되어서야 나타날 수 있다. 하지만 이런 규칙 사슬은 언제나 한정된(bounded) 횟수의 통과 안에서, 계층 구조의 층마다 하나씩 정착하며, 그 깊이(그것의 유도 깊이(derivation depth), 즉 술어 의존관계의 가장 긴 사슬)는 시작하기 전에 이미 고정되어 있다: professor/student, 그다음 researcher, 그다음 person, 세 개의 층, 끝이다. 만약 이것이 유일한 복잡함이었다면, 그저 알려진 횟수만큼 규칙을 펼쳐 두면 될 뿐 고정점을 언급할 필요조차 없었을 것이다.

까다로운 쪽은 재귀(recursion)다 — 머리가 자기 자신의 몸체로 다시 들어갈 수 있는 규칙이며, 여기서는 통과의 횟수가 미리 정해져 있지 않고 데이터에 실려 있다. 학계 세계에는 정확히 하나의 재귀 규칙, 즉 추이적 인용(transitive citation)이 있으며, kb.py(84–88행)는 이것을 이 모든 기계장치가 존재하는 이유로 표시해 둔다:

# Transitive closure of citation — the rule that *needs* a fixpoint, because
# its own head feeds its own body.
(("citesTransitively", "A", "B"), [("cites", "A", "B")]),
(("citesTransitively", "A", "C"),
 [("cites", "A", "B"), ("citesTransitively", "B", "C")]),

기본 사실들은 p3가 p2를 인용하고 p2가 p1을 인용하는 인용 사슬을 담고 있다. 한 번의 훑기가 무엇을 할 수 있고 무엇을 할 수 없는지 지켜보자. 라운드 1에서는 비재귀적인 첫 번째 절이 각각의 직접적인 cites 쌍을 citesTransitively 쌍으로 바꾸어, p2→p1과 p3→p2가 나타난다. 하지만 p3→p1은 아직 나타날 수 없다: 재귀적인 두 번째 절은 그 몸체 안에 citesTransitively("p2", "p1")이 놓여 있기를 필요로 하는데, 라운드 1이 시작될 때는 그 원자가 존재하지 않았기 때문이다. p2→p1이 이제 상 위에 놓인 라운드 2에 이르러서야 비로소 그 재귀적인 절이 발화되어 p3→p1을 만들어 낸다. 그 유도 과정은 두 단계짜리 증명 트리이며, 각 노드에 붙은 파동 이름표는 정확히 그것이 모델에 들어온 라운드다:

citesTransitively(p3, p1)            ← recursive clause, round 2
├── cites(p3, p2)                    ← base fact, round 0
└── citesTransitively(p2, p1)        ← base-case clause, round 1
    └── cites(p2, p1)                ← base fact, round 0

실행의 정렬된 출력은 완성된 폐쇄를 확인해 준다:

   ('citesTransitively', 'p2', 'p1')
   ('citesTransitively', 'p3', 'p1')
   ('citesTransitively', 'p3', 'p2')

그 지연된 단 하나의 원자, p3→p1이 바로 핵심이다. 두 홉(hop) 깊이의 결론은 그 아래에 있는 한 홉짜리 결론이 존재하기 전까지는 도달할 수 없으며, 인용 사슬은 어떤 길이든 될 수 있으므로, 미리 정해 둔 어떤 훑기 횟수도 안전하지 않다: $k$편의 논문으로 이루어진 사슬(즉 $k-1$개의 홉)은 가장 긴 도달 가능성 원자가 나타나기까지 $k-1$번의 라운드를 필요로 한다. 이것이 바로 깊이가 알려진 상수였던 person/researcher 사슬과의 차이다. 재귀에서는 깊이가 데이터에 실려 있으므로, 한 라운드가 아무 일도 하지 않을 때까지 반복해야만 한다. 재귀야말로 정확히 추론이 고정된 펼침이기를 멈추고 극한에 도달하는 것이 되는 지점이다.

추이 폐쇄: 같은 아이디어를, 한 번에 하나의 관계에

인용 예시는 너무나 흔해서 자기만의 이름을 가진 연산의 한 특수한 경우다: 어떤 관계의 추이 폐쇄(transitive closure)로, 원래의 관계를 포함하면서 "$a$가 $b$에 도달하고 $b$가 $c$에 도달하면 $a$도 $c$에 도달한다"에 대해 닫혀 있는 가장 작은 관계다. sets_relations.py에서는 논리 원자의 집합이 아니라 순서쌍의 집합에 적용된, 바로 그 동일한 루프로 이를 계산한다:

def transitive_closure(R: set) -> set:
    closure = set(R)
    while True:
        added = compose(closure, R) - closure
        if not added:
            return closure
        closure |= added

그 엔진은 관계 합성(composition)이며, $R \circ S$라고 쓴다(고리 ∘는 "…와 합성한"이라고 읽는다). 파일 안에서는 다음과 같이 정의된다

$$R \circ S \;=\; \{\, (a, c) : (a, b) \in R \text{ and } (b, c) \in S \,\},$$

이는 22–24행의 compose이며, 공유된 중간 원소 $b$를 통해 연결되는 쌍들이다. transitive_closure의 모양은 least_fixpoint와 동일하다: $R$에서 시작해, 단조적인 한 단계(즉 $R$과 합성한 뒤 새로운 쌍들을 합집합으로 더하는 closure |= added)를 적용하고, 한 라운드가 아무것도 더하지 않을 때 멈춘다. 검사 if not added(34행)는 nxt == current와 같은 고정점 검사인데, added = compose(closure, R) - closure(33행)가 비어 있는 것은 정확히 합성이 이미 존재하지 않는 쌍을 하나도 만들어 내지 못할 때이기 때문이다.

인용 관계 $R = \{(\text{p2},\text{p1}), (\text{p3},\text{p2})\}$ 위에서 손으로 직접 추적해 보자:

반복	진입 시점의 closure	compose(closure, R)	added(새로운 쌍)	동작
$1$	$\{(\text{p2},\text{p1}), (\text{p3},\text{p2})\}$	$\{(\text{p3},\text{p1})\}$, $(\text{p3},\text{p2}) \circ (\text{p2},\text{p1})$에서	$\{(\text{p3},\text{p1})\}$	더하고, 반복
$2$	$\{(\text{p2},\text{p1}), (\text{p3},\text{p2}), (\text{p3},\text{p1})\}$	$\{(\text{p3},\text{p1})\}$(이미 존재)	$\varnothing$	멈춤

반복 1에서, 합성은 새로운 쌍 하나를 찾아낸다: closure 안의 $(\text{p3},\text{p2})$가 p2를 거쳐 $R$ 안의 $(\text{p2},\text{p1})$로 연결되어, $(\text{p3},\text{p1})$을 낳는다. 반복 2에서 합성이 만들어 낼 수 있는 유일한 쌍은 바로 그 $(\text{p3},\text{p1})$인데, 이제는 이미 존재하므로 added는 비어 있고 루프는 돌아온다. 실제 출력은 정확히 일치한다:

transitive closure of cites: [('p2', 'p1'), ('p3', 'p1'), ('p3', 'p2')]

쌍 ('p3', 'p1')은 citesTransitively p3→p1과 동일한 유도된 진리이며, 규칙 엔진을 거치지 않고 날것의 순서쌍 위에서 계산된 것이다. 그리고 그것이 여기서는 반복 1에 나타나는 이유는 그곳에서 라운드 2에 나타났던 이유와 같다: 먼저 존재해야만 하는 한 홉짜리 사실에 의존하기 때문이다. 이것은 감탄하고는 잊어버릴 우연이 아니다. 이것은 데이터로그 평가가 곧 최소 고정점 반복이라는 데이터베이스 이론의 기초적인 결과이며, 추이 폐쇄는 어떤 고정된 관계 조인(join) 집합으로도 표현할 수 없는 진짜 재귀의 교과서적 예시다 [4]. 도달 가능성을 혼 규칙으로 표현하든 관계 합성으로 표현하든, 여러분은 하나의 상승 사슬을 타고 올라가 하나의 고정점을 계산하고 있는 것이다.

오름으로서의 추론: 전방 연쇄는 상승 사슬 23 ⊆ 41 ⊆ 47 ⊆ 47을 따라 사실 집합을 키워 나가다가 T_P가 그 집합을 자기 자신으로 사상하는 최소 고정점에서 멈추며, 두 홉짜리 인용 p3 → p1은 그것이 딛고 선 한 홉짜리 p2 → p1보다 한 파동 늦게 도착한다. Original diagram by the authors, created with AI assistance.

계속 되돌아오는 엔진

고정점에 이름을 붙여 두는 것이 값어치가 있는 까닭은, 바로 그 동일한 엔진이 이 시리즈의 모든 층에서 다시 나타나기 때문이며, 그래서 한 번 배우는 것이 그 전부를 배우는 것이 되기 때문이다.

2권에서는, 기술 논리(description logic) 추론기가 완성(completion, 또는 포화(saturation)) 알고리즘으로 포섭(subsumption)을 결정한다: 진술된 사실들에서 시작해, 고정된 완성 규칙들의 집합 — "어떤 개체가 $R$이고 모든 $R$이 $S$이면, 그것을 $S$로 표시한다" — 을 되풀이해서 적용하여, 한 라운드가 아무것도 더하지 않을 때까지 귀결된 멤버십과 간선(edge)을 더해 간다. 이것은 다른 이름을 쓴 $T_P$이다: 그 최소 고정점이 모든 포섭 관계를 읽어 낼 수 있는 완성된 모델이 되는 단조 연산자이며, 이는 정확히 이 장의 그 루프이자 그 두 정리다. 기술 논리의 EL 계열은 바로 이 고정점이 크기 면에서 다항식적(polynomial)으로 유지되도록 — 진술된 사실이 $n$개일 때 완성된 모델이 기껏해야 $n$, $n^2$, 또는 $n^3$ 정도의 규모로만 커지고, 결코 지수적으로 폭발하지 않도록 — 그리고 언제나 종료하도록 정확하게 설계되어 있으며, 이것이 바로 EL 추론기가 수십만 개의 클래스를 가진 생물의학 온톨로지(biomedical ontology)까지 규모를 늘릴 수 있는 이유다.

4권에서는, 미분 가능한 추론(differentiable reasoning)이 "이 원자가 집합 안에 있는가?"라는 명확한(crisp) 질문을 0에서 1 사이의 부드러운(soft) 점수로 대체하고, $T_P$를 매끄럽고 단조적인 업데이트 레이어로 대체한다. 그 레이어를 수렴할 때까지 실행하는 것이 바로 고정점 레이어(fixpoint layer)다: 점점 더 확신에 찬 사실 벡터들의 사슬을 점수가 더 이상 움직이지 않을 때까지 타고 올라가며, 이는 여기서 다룬 이산적(discrete) 등반의 연속적(continuous) 유사물이다. 이런 레이어를 처음부터 끝까지(end to end) 학습시킬 수 있는 이유는, 그 순전파(forward pass)가 정확히 고정점 반복이며, 고정점은 그것을 통과해 미분할 수 있기 때문이다. 심볼릭 완성과 신경망 고정점 레이어는 하나의 조리법 — 단조 연산자를 바닥에서부터 정착할 때까지 반복한다 — 을 구현한 두 가지 방식이다.

아직 풀리지 않은 부분

이 장이 주는 편안함은 유한성 증명 안에 자리한 하나의 조용한 가정 위에 놓여 있다: 정의역이 유한(finite)하고 고정(fixed)되어 있다는 가정이다. 학계 세계가 진술할 수 있는 모든 원자는 다섯 명의 사람과 세 편의 논문으로 이루어진 닫힌 풀(pool)에서 나온 것이었기에 $|H|$는 유한했고, 개수 $|X_t|$는 그 천장을 넘어 오를 수 없었으며, 그 사슬은 세 번의 파동 만에 정착했다. 이 가정을 걷어 내면, 그 보장은 정확히 그것을 사용했던 그 단계에서 금이 간다.

그 균열은 존재 규칙(existential rule)에서 온다 — 알려진 개체의 이름을 대는 대신 머리가 무언가가 존재한다고 주장하는 규칙으로, "모든 연구자는 지도교수를 가진다"처럼, 기록에 없는 경우조차 지도교수를 요구하는 규칙이다. 그런 규칙을 발화시키면 새로운 개체를 지어내게 되고, 그 새로운 개체는 그 자체가 다시 지도교수를 가져야 하는 연구자이므로, 같은 규칙이 방금 만든 것 위에서 다시 발화된다. 이런 의무들을 뒤쫓는 전방 연쇄 과정을 체이스(chase)라고 부르며, 그 상승 사슬은 결코 고정점에 도달할 필요조차 없다: 그것은 영원히 오를 수 있으며, 익명의 지도교수의 지도교수로 이루어진 무한한 탑을 계속 찍어 낼 수 있다. 유한성 논증은 정확히 그 하나의 산술적 단계에서 무너진다 — $|X_t|$는 더 이상 유한한 $|H|$로 상한이 잡히지 않으므로, "오르기만 하는 한정된 개수는 반드시 멈춰야 한다"는 더 이상 적용되지 않는다. 크나스터–타르스키는 여전히 최소 고정점이 존재한다고 약속하지만(연산자는 단조이고, 격자는 완비이므로), 그리고 체이스가 연속적이기 때문에 그것은 심지어 그 무한한 사슬의 극한이기도 하지만, least_fixpoint와 같은 어떤 종료하는 루프도 그것에 도달할 수 없으며, 그 밑바탕에 있는 질문 — 무언가가 귀결되는가? — 은 일반적으로 결정 불가능(undecidable)하다.

이것은 고쳐야 할 결함이 아니다. 이것은 이 분야가 지금과 같은 방식으로 조직된 이유이며, 여기서는 서로 다른 두 가지 보장을 구분해 두어야 한다. 어떤 단편(fragment)에서는 체이스가 증명 가능하게 유한(finite)하므로, least_fixpoint와 같은 루프가 답을 곧바로 계산해 낸다: 존재 규칙이 없는 데이터로그(우리의 경우), 2권의 EL 계열, 그리고 약비순환적(weakly-acyclic, 또는 비순환적) 존재 규칙 — 지어낸 개체가 되먹임되어 새로운 개체를 영원히 계속 낳을 수 없어서, 방금 설명한 끝없는 등반이 애초에 시작조차 되지 않는 경우 — 은 모두 종료한다. 다른 단편에서는 체이스가 영원히 실행될 수 있지만, 그럼에도 질의 응답(query answering)은 여전히 결정 가능(decidable)하다 — 가드(guarded, 각 규칙 몸체가 자신의 모든 변수를 담고 있는 원자 하나를 지니는 것)와 스티키(sticky, 규칙이 발화될 때 변수가 어떻게 전파되는지에 대한 제약; 2권에서 둘 다 정확하게 다룬다) 존재 규칙이 그 대표적인 경우이며, 이들은 진정으로 서로 다른 두 가지 경로로 그 결정 가능성을 사들인다. 가드 규칙은 어쩌면 무한할 수도 있는 체이스를 트리 형태(tree-like)로, 즉 유계 트리너비(bounded treewidth)를 갖도록 유지한다. 이는 트리 모양으로 배열된 서로 겹치는 조각들로 분해되는, 작고 반복되는 국소 패턴들의 고정된 재고에서 이어 붙여진 것이므로, 전체를 결코 다 만들지 않고도 그 규칙적인 모양을 이용해 질의에 답할 수 있다. 스티키 규칙은 그 대신 가드성이 금지하는 비가드(non-guarded) 조인을 허용하도록 설계되었으므로, 그 체이스는 일반적으로 트리 형태가 아니다. 이들은 1차 재작성 가능(first-order rewritable)함으로써 결정 가능성을 얻는다. 즉 질의를 주어진 기본 사실들 위에서 직접 평가되는 평범한 1차(SQL 방식의) 질의로 재작성함으로써 체이스를 통째로 건너뛸 수 있다는 뜻이다. 어느 쪽이든 그 보장을 얻는 대가로 표현력(expressive power)을 지불하며, 2권은 대체로 이 경계선이 어디에 놓이는지를 연구하는 것이다. 뉴로-심볼릭 AI의 정직하고 아직 풀리지 않은 긴장은 바로 여기에 있다: 우리가 가장 추론하고 싶어 하는 표현력 있는 논리들이야말로 정확히 그 고정점에 언제나 도달할 수는 없는 논리들이며, 결정 가능성을 도로 사들이는 데는 결코 공짜가 없다.

왜 중요한가

이 시리즈에서 만나게 될 거의 모든 기호적 추론기(symbolic reasoner)는, 그 밑바탕에서는, 우리가 옳음을 증명하고 나서 실행한 것과 동일한 루프다: 바닥에서 씨앗을 뿌리고, 단조 연산자를 적용하고, 한 라운드가 아무것도 바꾸지 않으면 멈춘다. 전방 연쇄, 데이터로그 평가, 추이 폐쇄, 그리고 기술 논리 완성을 하나의 구성 — 단조 연산자의 최소 고정점 — 으로 보는 것은, 그 패턴을 한 번 배워서 어디서나 그것을 알아본다는 뜻이며, 그 보장(최소이고 정형적인(canonical) 답이 크나스터–타르스키에 의해 존재하고, 그 등반이 클레이니에 의해 유한한 세계에서 그곳에 도달한다는 것)과 그 위험(비용이 클 수도, 끝이 없을 수도 있다는 것)을 하나의 묶음으로 함께 물려받는다는 뜻이기도 하다. 특히 뉴로-심볼릭(neuro-symbolic) 프로그램에게, 고정점은 다리(bridge)가 되어 준다: 그것은 미분 가능한 추론 레이어가 연속적인 점수로 흉내 내려 애쓰는, 명확하고(crisp) 증명 가능한 목표이며, 신경망 근사(neural approximation)가 올바른 극한에 도달했는지를 재는 잣대다. 학습된 추론기와 기호적 추론기가 같은 고정점으로 함께 오를 때, 그 하이브리드 시스템은 일관적(coherent)이다; 그렇지 않을 때, 바로 그 고정점이 그 사실을 알려준다.

핵심 용어

• 허브랜드 베이스(Herbrand base) $H$ — 세계가 진술할 수 있는 모든 접지 원자의 풀이다; ⊆로 순서가 매겨진 그 부분집합들은 추론이 그 위를 옮겨 다니는 완비 격자를 이루며, 최소원 ⊥ = ∅이고 최대원 ⊤ = $H$이다.
• 고정점(Fixpoint) — 연산자에 의해 변하지 않는 집합 $X$, 즉 $F(X) = X$이다; 연산자를 적용해도 아무것도 움직이지 않는다.
• 최소 고정점(Least fixpoint, $\mathrm{lfp}$) — 단조 연산자의 가장 작은 고정점으로, 다른 모든 고정점 안에 포함된다; 전방 연쇄에서 이것은 최소 모델, 즉 프로그램의 의미다.
• 크나스터–타르스키 정리(Knaster–Tarski theorem) — 완비 격자 위의 모든 단조 연산자는 최소 고정점을 가진다; 여기서는 $F$가 자기 자신 안으로 사상하는 모든 집합들의 교집합으로서 증명되었다. 존재 보장이며, 그것을 어떻게 계산하는지는 말하지 않는다.
• 클레이니 고정점 구성(Kleene fixed-point construction) — $F$를 ⊥에서부터 반복하며 그 극한을 취함으로써 그 최소 고정점에 도달한다; 상승 사슬은 유한한 격자 위에서 반드시 멈추며(오르기만 하는 한정된 개수이므로), 멈추는 순간 정확히 $\mathrm{lfp}(F)$ 위에 내려앉는다.
• 단조 연산자(Monotone operator) — $A \subseteq B$가 $F(A) \subseteq F(B)$를 함의하는 사상 $F$이다: 더 큰 입력이 더 큰 출력을 낳는다. $T_P$에서 이것이 성립하는 것은 규칙 몸체가 긍정적이기 때문이며, 부정은 이것을 깨뜨렸을 것이다. (사실을 결코 없애지 않는다는 뜻의 팽창적(inflationary), $X \subseteq F(X)$와는 다른 개념이며, $T_P$는 이것도 마침 만족한다.)
• 상승 사슬 / 최소상계(Ascending chain / least upper bound) — 오직 커지기만 하는 수열 $X_0 \subseteq X_1 \subseteq \cdots$과 그 전체 위에 있는 가장 작은 집합이다; 고정점은 이 사슬의 최소상계다.
• 즉각귀결 연산자(Immediate-consequence operator, $T_P$) — 몸체가 성립하는 모든 규칙을 발화시키고 그 머리들을 더한다; 전방 연쇄가 반복하는 단조 연산자다.
• 최소 허브랜드 모델(Least Herbrand model) — 모든 규칙을 충족시키는 가장 작은 사실 집합이다; $\mathrm{lfp}(T_P)$와 같다.
• 추이 폐쇄(Transitive closure) — 주어진 관계를 포함하는 가장 작은 추이적 관계다; 전방 연쇄와 동일한 루프로 한 번에 하나의 관계씩 계산되는, 교과서적인 재귀적 고정점이다.
• 완성 / 포화(Completion / saturation, 2권) — 기술 논리 추론기가 귀결 규칙들을 아무것도 새로 유도되지 않을 때까지 고정점 반복하는 것이다.
• 존재 규칙 / 체이스(Existential rule / the chase) — 머리가 무언가가 존재한다고 주장하며 새로운 개체를 지어내고, 전방 연쇄 사슬이 결코 종료하지 않고 오르게 만들 수 있는 규칙이다.
• 종료하는 체이스 단편(Terminating-chase fragment) — 체이스가 유한한 규칙 형태(존재 규칙이 없는 데이터로그, EL, 약비순환적 또는 비순환적 존재 규칙)로, least_fixpoint가 답을 곧바로 계산해 낸다.
• 결정 가능한 단편(Decidable fragment) — 체이스가 영원히 실행될 수 있어도 질의 응답이 결정 가능하게 유지되는 규칙 형태(가드 및 스티키 존재 규칙을 더한 것)이며, 표현력을 대가로 치르고 얻은 것이다.

이 장이 이어지는 곳

이제 우리에게는 완성된 추론 엔진이 있으며, 증명과 함께 완성되었다: 규칙으로 부호화된 지식, 단조 연산자의 최소 고정점(존재가 보장된)으로 정의된 그 의미, 그리고 한 라운드가 아무것도 바꾸지 않는 순간 멈추는, 바닥에서 시작한 등반으로 계산된 그 의미다. 하지만 지금까지의 모든 규칙은 우리에게 주어진 것이었다 — 누군가가 "교수는 연구자다", "인용은 추이적이다"라고 써 놓은 것이다. 당연히 다음에 떠오르는 질문은 이 권의 후반부를 여는 바로 그 질문이다: 아무도 규칙을 써 놓지 않을 때, 그 규칙은 어디에서 오는가? 다음 장인 학습이란 무엇인가: 데이터에 함수 맞추기는 알려진 규칙의 귀결을 유도하는 일에서 벗어나, 예시로부터 규칙과 패턴을 추론해 내는(infer) 일로 방향을 돌린다 — 이는 뉴로-심볼릭 프로젝트 전체가 화해시키고자 세워진, 추론에서 학습으로의 전환이다. 고정점은 기계가 가진 지식으로 계산하는 방법이었다; 학습은 기계가 갖지 못한 지식을 얻는 방법이다.

---

동반 코드: examples/logic/forward_chain.py는 t_p(즉각귀결 연산자)와 least_fixpoint(그 nxt == current 종료 검사를 갖춘 클레이니의 등반)를 구현하며, examples/logic/sets_relations.py는 관계 위에서 동일한 루프로 transitive_closure를 구현한다. python3 examples/logic/forward_chain.py를 실행하면 [23, 41, 47, 47] 파동과 인용 폐쇄를 재현할 수 있고, python3 examples/logic/sets_relations.py를 실행하면 cites의 추이 폐쇄를 재현할 수 있다; 둘 다 kb.py에서 실행 예제를 읽어 들인다.