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

📍 현재 위치: 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보다 한 파동 늦게 도착합니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

계속 되돌아오는 엔진

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

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에서 실행 예제를 읽어 들입니다.