구체화 대 재작성: 규모 확장의 두 길

📍 현재 위치: IV부 · 규모와 시스템 — 9장. 기권은 "모른다"고 말할 권리에 값을 매김으로써 III부를 닫았습니다; IV부는 프론티어의 또 다른 장부인 규모를 열며, 가장 오래된 질문에서 시작합니다: 추론 비용을 적재 시점에 한 번만 치를 것인가, 아니면 매 질의마다 다시 치를 것인가?

이 시리즈의 모든 권은 귀결을 계산해 왔습니다: 1권은 고정점(fixpoint)을 돌렸고, 2권은 온톨로지를 포화시켰으며, 4권은 질의 응답을 관통해 미분했습니다. 그중 어느 것도 그 계산이 언제 일어나야 하는지는 묻지 않았습니다. 이 질문은 구현상의 세부 사항처럼 들리지만 실은 정반대입니다: 이것은 연역 데이터베이스와 온톨로지 추론 시스템 문헌 전체가 조직되는 축이며, 한 줄로 적을 수 있을 만큼 단순한 산술 하나가 그것을 지배합니다. 구체화(materialization)는 적재 시점에 값을 치릅니다: 규칙들을 그 최소 고정점까지 한 번 돌려 모든 귀결을 저장해 두고, 각 질의에는 조회로 답합니다. 재작성(rewriting)은 질의 시점에 값을 치릅니다: 기본 사실 말고는 아무것도 저장하지 않고, 각 질의를 규칙들을 거슬러 후방으로 펼쳐, 날것의 데이터가 직접 답할 수 있는 질의들의 합집합으로 바꿉니다. 둘 다 같은 확실한 답(certain answers), 즉 단 하나의 모형이 아니라 데이터의 모든 가능한 완성에서 사실과 규칙이 보장하는 답을 돌려줍니다; 동반 모듈은 그것을 자신이 실행하는 모든 질의에 대해 세 가지 방식으로 정확히 그렇게 단언합니다. 다른 것은 청구서이며, 이 장은 학계 세계 위에서 그 청구서를 탐침 단위로 셉니다: 폐쇄의 적재 비용, 각 전략의 질의당 비용, 승자가 뒤바뀌는 교차 작업 부하, 표제 항등식이 감추는 유지보수 비용, 그리고 마지막으로 이 장에서 가장 깊은 사실, 즉 그 선택이 언제나 여러분의 몫은 아니라는 것입니다: 여러분이 추론하는 논리 조각(fragment)이 재작성이 애초에 가능한지 자체를 결정하기 때문입니다.

쉽게 말하면

어느 식당이 채소를 언제 썰지를 정한다고 상상해 보십시오. 한 주방은 새벽에 모든 것을 미리 준비합니다: 양파는 모두 다지고 소스는 모두 졸여 두어서, 각 주문이 몇 초 만에 조립됩니다. 다른 주방은 재료를 통째로 두었다가 주문표가 들어오면 그때부터 요리를 처음부터 만듭니다. 주문이 이백 개 들어오면 새벽 준비가 압도적으로 이깁니다; 주문이 세 개만 들어오면, 아무도 찾지 않은 음식을 위해 아침 내내 썰어 댄 셈이 됩니다. 이제 숨은 비용을 더해 봅시다: 공급업체가 토마토 한 상자를 리콜합니다. 즉석 요리 주방은 어깨를 으쓱하고는 그 토마토를 그냥 쓰지 않으면 그만입니다. 미리 준비하는 주방은 모든 준비된 소스를 뒤지며 "이 배치가 그 상자를 썼던가, 그리고 썼다면 다른 상자로도 만들 수 있었을까?"를 물어야 하는데, 이는 진짜로 신경 써야 하는 일입니다. 그리고 한 가지 요리, 오랫동안 뭉근히 끓인 육수는 주문받고 나서는 도무지 만들 수가 없습니다: 막판에 아무리 애를 써도 몇 시간의 뭉근한 끓임을 대신할 수 없으므로, 즉석 요리 주방은 그것을 아예 낼 수 없습니다. 구체화는 새벽 준비이고, 재작성은 주문받고 요리하는 것이며, 리콜은 삭제이고, 육수는 재귀입니다.

이 장에서 다루는 내용

• 회계 항등식: 전체 추론 비용을 적재 비용에 질의당 비용 곱하기 작업 부하 크기를 더한 것으로 나타내고, 그 각 항을 해독하며, 그로부터 따라 나오는 교차 주장을 살핍니다: 승자는 여러분이 앞으로 몇 번의 질의를 던질 것인가의 함수입니다.
• 셈해진 구체화: 눈에 보이는 탐침 계수기와 함께 구현된 단순 고정점(naive fixpoint, 23개의 사실이 2번의 파동, 236번의 탐침으로 47개까지 닫힙니다), 그 단순 전략의 낭비에 이름을 붙이는 일, 그리고 처음부터 유도된 준단순 델타 규칙(semi-naive delta rule): 새로운 사실에 닿는 규칙 인스턴스만이 새로운 무언가를 도출할 수 있으므로, 어떤 인스턴스도 결코 두 번 발화하지 않습니다.
• 셈해진 재작성: 혼 규칙(Horn rule)들을 거쳐 질의 원자를 후방으로 펼쳐 기본 술어들에 대한 논리곱 질의들의 합집합으로 만드는 일, 인용된 재귀, 순위 논증(rank argument)으로 비재귀적 규칙 형태에 대해 증명된 종료성, 그리고 단 하나의 재귀 규칙에서 나타나는 정직한 경계를 다룹니다.
• 계산된 교차점: 커밋된 질의당 탐침 수를 항등식에 대입하고, 손익분기 작업 부하를 정확히 풀어내며(다섯 질의짜리 장부의 열세 번째 통과), 이를 의미론이 아니라 오직 비용에 관한 통제된 실험으로 만들어 주는 동일 답 단언을 다룹니다.
• 유지보수, 세 번째 축: 지도 사실 하나를 더하는 데는 구체화 쪽에서 12번의 탐침짜리 준단순 델타가 들지만 재작성 쪽에서는 아무 비용도 들지 않으며; 인용 하나를 지우면 DRed의 과잉 삭제 후 재도출 춤이 강제되는데, 그 셈해진 실행(과잉 삭제 2건, 복원 1건)은 어째서 삭제가 삽입보다 더 어려운지를 정확히 보여줍니다.
• 조각 의존성: 커밋된 8홉짜리 재귀 벽, DL-Lite 질의는 1차 질의로 완전히 재작성되지만 EL의 PTIME-완전(PTIME-complete) 추론은 그럴 수 없다는 정리(PTIME: 입력 크기의 고정된 거듭제곱으로 시간이 유계인, 다항 시간 안에 풀 수 있는 문제들의 클래스), 그리고 이것이 논리를 선택할 때 무엇을 뜻하는지를 다룹니다: 여러분은 곧 시스템 선택지를 고르고 있는 것입니다.

회계 항등식

지식 베이스 하나와 작업 부하 하나를 고정해 둡시다. $q$를 작업 부하 크기(workload size)라고 씁니다: 저장소가 평생 동안 답하게 될 질의의 수(던져진 질의마다 하나씩 세는 단순한 개수)입니다. $C_{\text{load}}$는 어떤 질의가 도착하기도 전에, 데이터가 적재될 때 한 전략이 한 번만 치르는 비용이라고 쓰고, $C_{\text{query}}$는 그 전략이 질의마다 치르는 비용이라고 씁니다. 그러면 그 작업 부하에 응대하는 전체 비용은 한 줄입니다:

$$\mathrm{Total}(q) \;=\; C_{\text{load}} \;+\; q \cdot C_{\text{query}}.$$

이것을 가로축이 $q$이고 세로축이 전체 작업량인 평면 위의 하나의 직선으로 읽으십시오: $C_{\text{load}}$는 절편(intercept)이고, $C_{\text{query}}$는 기울기(slope)입니다. 구체화는 절편이 높고 기울기가 완만한 직선입니다: 전체 고정점 값을 미리 치러 두어서 각 질의가 조회 하나로 끝나게 만듭니다. 재작성은 절편이 0이고 기울기가 가파른 직선입니다: 적재는 공짜입니다(기본 사실들은 도착하는 그대로 저장될 뿐 아무것도 도출되지 않습니다), 그리고 모든 질의는 자신에게 필요한 추론의 값을 스스로 치릅니다. 절편과 기울기가 다른 두 직선은 정확히 한 점에서 교차합니다. 그 점을 찾기 위해, 구체화에는 위 첨자 $m$을, 재작성에는 위 첨자 $r$을 붙여 전체 비용을 같다고 놓으면:

$$C^{m}_{\text{load}} + q\, C^{m}_{\text{query}} \;=\; q\, C^{r}_{\text{query}} .$$

양변에서 $q\, C^{m}_{\text{query}}$를 빼고, 우변에서 $q$를 묶어내면:

$$C^{m}_{\text{load}} \;=\; q\,\bigl(C^{r}_{\text{query}} - C^{m}_{\text{query}}\bigr).$$

양변을 괄호 안의 차이로 나누면 교차점이 나옵니다:

$$q^{*} \;=\; \frac{C^{m}_{\text{load}}}{C^{r}_{\text{query}} - C^{m}_{\text{query}}},$$

이는 재작성의 질의당 비용이 구체화의 그것을 넘어설 때, 즉 괄호 안의 분모가 양수일 때에만 유효합니다; 동반 모듈은 질의 하나하나에 대해 조회가 결코 재작성보다 많이 탐침하지 않음을, 그리고 재작성이 실제로 결합(join)을 수행할 때마다 엄격히 그러함을 단언하며, 바로 이것이 장부의 분모를 양수로 만들어 줍니다. $q^{*}$ 질의 미만에서는 재작성이 더 적은 전체 작업을 한 것이고, 그 이상에서는 적재 비용이 상각(amortized, 질의당 절감으로 되갚아짐)되어 그 이후로는 영원히 구체화가 이깁니다. 이 장의 나머지 전부는 이 세 상수를 조심스럽게 측정하는 일이며, 여기에 이 항등식이 감추는 두 가지 복잡한 사정이 더해집니다: 데이터가 변한다는 것(유지보수는 이 항등식에 그 항이 전혀 없는 비용입니다), 그리고 어떤 하나의 규칙 형태에 대해서는 비교의 재작성 쪽 자체가 아예 존재하지 않는다는 것입니다.

이를 재는 도구는 동반 모듈 mat_vs_rewrite.py이며, 1권의 학계 세계 위에서 두 전략을 모두 실행합니다. 가져다 쓸 뿐 다시 타이핑하지 않습니다: examples/logic/kb.py의 기본 사실 23개와 혼 규칙 7개, 구체화기로서의 forward_chain.least_fixpoint, 그리고 두 전략 모두가 그에 맞대어 검사되는 독립 오라클로서의, 1권이 만든 후방 연쇄 엔진인 examples/logic/sld.py의 SLD(선택적 선형 확정절 귀결, Selective Linear Definite-clause resolution) 증명기입니다. 그 하나의 비용 단위는 탐침(probe)입니다: 저장소는 술어별로 색인이 매겨져 있고, 질의를 평가하면 원자의 술어 색인 아래에서 훑어본 후보 사실 하나당 탐침 하나가, 그리고 접지 부등호 검사 하나당 탐침 하나가 부과됩니다(mat_vs_rewrite.py 37–40행). 어디에도 실제 시계 시간 숫자는 나타나지 않습니다; 탐침은 실제 규모에서 지배적인 I/O 비용과 조인 비용을 대신하며, 그 실행은 바이트 단위까지 결정론적입니다.

하나의 항등식, 두 개의 극: 구체화는 높은 절편과 완만한 기울기를 사들이고, 재작성은 영(0)의 절편과 가파른 기울기를 사들이며, 커밋된 탐침 수는 그 둘의 교차점을 질의 장부의 약 12.5번째 통과 지점에 놓습니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

구체화: 한 번 치르고 영원히 조회하기

구체화는 규칙들의 최소 고정점(least fixpoint)을 기본 사실들 위에서 계산합니다: 기본 사실들을 포함하며 모든 규칙 아래에서 닫혀 있는 가장 작은 원자 집합입니다. 1권은 그 엔진을 만들었습니다; 여기서는 그것이 비용 중심(cost center)이 됩니다. 그 연산자를 되짚어 봅시다. $P$는 규칙 프로그램을, $I$는 접지 원자들의 집합(현재 저장소)을, $\sigma$는 치환(substitution), 즉 변수에서 상수로의 대응을 나타냅니다. 즉각귀결 연산자(immediate-consequence operator) $T_P$는 저장소를 그 저장소에 한 단계로 도출 가능한 모든 것을 더한 것으로 사상합니다:

$$T_P(I) \;=\; I \,\cup\, \{\, h\sigma \;:\; (h \leftarrow b_1, \ldots, b_m) \in P,\;\; b_1\sigma, \ldots, b_m\sigma \in I \,\},$$

이렇게 읽으십시오: 머리 $h$와 몸체 원자 $b_1$부터 $b_m$까지를 가진(문자 $m$은 그 규칙의 몸체 원자 개수를 셉니다) 모든 규칙에 대해, 그리고 인스턴스화된 몸체 원자 $b_i\sigma$ $m$개 전부를 $I$의 원소로 만드는 모든 치환 $\sigma$에 대해, 인스턴스화된 머리 $h\sigma$를 더합니다. 기본 사실들로부터 $T_P$를 반복하면 사슬 $I_0 \subseteq I_1 \subseteq I_2 \subseteq \cdots$(기호 $\subseteq$는 각 저장소가 바로 앞 저장소의 모든 것을 담고 있다는 뜻입니다: 아무것도 제거되지 않고 오직 더해질 뿐입니다)을 오르며, 이는 유한하게 많은 파동 뒤에 성장을 멈추는데, 더해지는 모든 것이 이미 있는 유한한 상수 공급으로부터 만들어지기 때문입니다. 그 안정된 집합이 폐쇄(closure)입니다. 동반 모듈의 셈해진 구현은 일부러 단순(naive) 버전이며, 그래서 그 낭비가 눈에 보입니다(mat_vs_rewrite.py 128–142행):

    store = set(edb)
    waves = probes = 0
    while True:
        new: set[tuple] = set()
        for head, body in rules:
            subs, p = eval_cq(body, index(store))
            probes += p
            for s in subs:
                h = apply_sub(head, s)
                if h not in store:
                    new.add(h)
        if not new:
            return store, waves, probes
        store |= new
        waves += 1

매 파동은 모든 규칙 몸체를 저장소 전체에 대해 다시 평가합니다. 이는 정확하지만 정밀하게 규정할 수 있는 방식으로 낭비적입니다: 파동 $t$에서 이미 몸체가 충족되었던 규칙 인스턴스가 파동 $t+1$에서 다시 발견되고, 그 이후의 모든 파동에서도, 이미 저장되어 있는 머리를 계속해서 도출합니다. 학계 세계에서는 그 낭비를 감당할 만하며, 커밋된 실행은 청구서 전체를 보고합니다:

[1] one closure, two bills — load once vs rewrite per query
  materialize: 23 facts → 47 (24 derived) in 2 waves, 236 probes at LOAD time
  rewrite    : store stays 23 facts; every query below pays at QUERY time

두 숫자는 잠시 멈추어 볼 가치가 있습니다. 첫째, 저장 공간입니다: 폐쇄는 23개의 기본 사실에 대해 47개의 사실이므로, 이 규칙 집합은 저장소를 두 배를 약간 웃도는 수준으로 불립니다. 그 비율이 구체화가 영원히 치르는 임대료이며, 이는 장난감 수준의 인공물이 아닙니다: 이 전략의 생산 라인은 설계상 그것을 받아들여 전체 폐쇄를 주기억장치 안에 통째로 짓고 [1], 벤치마크 규모에서는 같은 규율이 LUBM-50K(Lehigh University Benchmark를 5만 개 대학 규모로 키운 벤치마크)의 67억 개의 명시적 트리플을 92억 개의 저장된 트리플로 바꾸어 놓습니다 [2]. 둘째, 236번의 탐침은 첫 질의가 도착하기도 전에 치러지는데, 이는 정확히 그 항등식의 절편 $C^{m}_{\text{load}}$입니다. 하니스는 그런 다음 이 셈해진 폐쇄가 1권 자신의 엔진이 계산하는 폐쇄와 사실 하나하나까지 같다는 것을 단언하므로(mat_vs_rewrite.py 343–344행), 셈하는 계측 장치는 가시성 말고는 아무것도 바꾸지 않은 셈입니다. 구체화된 저장소는 원자 조회 하나로 질의에 답합니다: 질의 원자를 그 술어 색인에 맞대어 일치시키고 치환들을 모읍니다(mat_vs_rewrite.py 224–229행). grandAdvisor(alice, Z)에 대해서는 이것이 3번의 탐침이며, 저장된 grandAdvisor 사실 하나당 한 번씩입니다.

유도된 델타 규칙

실제 엔진들은 단순 루프를 돌리지 않습니다; 그것들은 준단순 평가(semi-naive evaluation)를 돌리며, 그 정확성은 단언만 하고 넘어가기보다 증명할 가치가 있는 두 줄짜리 정리입니다. 파동 $t$에서의 델타(delta)를 새로 도출된 원자들, $\Delta_t = I_t \setminus I_{t-1}$로 정의합시다(차집합 기호 $\setminus$는 "첫 번째 집합의 원소이면서 두 번째 집합의 원소는 아닌 것"이라는 뜻입니다). 주장은 이렇습니다: 파동 $t+1$에서 처음으로 발화하는 어떤 규칙 인스턴스든 그 몸체 원자 중 적어도 하나는 $\Delta_t$ 안에 있습니다. 대우에 의한 증명입니다. 몸체 원자가 모두 $I_t$ 안에 있지만 $\Delta_t$ 안에는 하나도 없는 인스턴스 $(h \leftarrow b_1, \ldots, b_m)\sigma$를 잡아 봅시다. 그러면 모든 $b_i\sigma$는 $I_t \setminus \Delta_t = I_{t-1}$ 안에 놓이므로, 그 인스턴스의 몸체는 한 파동 앞서 이미 충족되어 있었고, 그 인스턴스는 이미 파동 $t$에서 발화했으며, 그 머리는 이미 $I_t$ 안에 있습니다: 이는 첫 발화가 아닙니다. 대우를 취하면 델타 규칙이 나옵니다: 파동 $t+1$에서 진정으로 새로운 귀결을 전부 찾으려면, 각 규칙과 각 몸체 위치 $i$(1부터 $m$까지 도는 지표)에 대해, $i$번째 원자가 $\Delta_t$ 안의 어떤 사실과 일치하는 인스턴스들을 나머지 $m-1$개의 원자를 저장소 전체에 대해 결합(join)시키며 나열하는 것으로 충분합니다. 어떤 규칙 인스턴스도 결코 두 번 발화하지 않는데, 이는 RDFox 계열의 후속 연구가 나중에 비반복성(non-repetition property)이라고 이름 붙인 보장이며, 전체 병렬 엔진이 그 위에 지어져, 규칙이 아니라 새로 도출된 사실별로 작업을 나누어 스레드가 스스로 균형을 맞추도록 합니다 [1]. 동반 모듈은 자신의 증분 추가 절차 안에서 정확히 이 규율을 구현하며, 각 몸체 위치에 델타 사실을 씨앗으로 놓고 나머지를 결합합니다(mat_vs_rewrite.py 249–261행):

    while delta:
        idx = index(total)
        new: set[tuple] = set()
        for head, body in rules:
            for i, pat in enumerate(body):
                for d in sorted(delta):
                    s = unify(pat, d, {})
                    if s is None:
                        continue
                    probes += 1  # the delta seed is itself one probe
                    rest = body[:i] + body[i + 1:]
                    subs, p = eval_cq(rest, idx, sub=s)
                    probes += p

우리는 이 셈해진 숫자들을 유지보수 절에서 다시 읽을 것인데, 그곳에서는 델타가 삽입된 사실 하나뿐이어서 236번짜리 탐침으로 처음부터 짓는 폐쇄와의 대비가 극명해집니다. 이 극의 산업적 닻은 RDFox이며, 그 락이 가벼운(lock-light), 사실별로 분할된 준단순 엔진은 LUBM-50K 폐쇄를 구체화하며 새로 도출된 25억 개의 트리플을 초당 610만 트리플의 속도로 도출했고, 스레드 16개에서는 자신의 단일 스레드보다 15.7배, 128개에서는 69.6배 더 빠르게 실행되었습니다 [2]: 상용 코어 수에서의 거의 선형적인 멀티코어 규모 확장이, 위에서 인용한 바로 그 루프 위에서, 다 자란 모습으로 나타난 것입니다.

재작성: 질의 시점의 귀결

재작성은 기본 사실 말고는 아무것도 저장하지 않고, 모든 추론을 질의 안으로 옮깁니다. 데이터 안에 나타나는 기본 술어들은 EDB(외연 데이터베이스, extensional database)이고, 규칙의 머리인 도출된 술어들은 IDB(내포 데이터베이스, intensional database)입니다; 동반 모듈은 그 구분을 한 줄로 계산합니다, IDB: frozenset[str] = frozenset(head[0] for head, _ in RULES)(mat_vs_rewrite.py 69행). IDB 술어에 대한 질의 원자는 조회할 수 없는데, 그 술어를 가진 것이 아무것도 저장되어 있지 않기 때문입니다. 그것은 펼쳐져야(unfolded) 합니다: 그것을 도출할 수 있는 규칙들의 몸체로, 오직 EDB 원자만 남을 때까지 재귀적으로 치환되어야 합니다. 그 결과가 논리곱 질의들의 합집합(union of conjunctive queries, UCQ)입니다: 기본 술어들에 대한 평범한 결합(join)들의 유한한 목록으로, 그 하나하나가 논리곱 질의(conjunctive query, CQ)이며, 그 답들의 합집합이 원래 질의의 답이 됩니다.

펼침 한 단계는 정확히 귀결(resolution) 한 단계이며, 적재 시점 대신 질의 시점에 실행됩니다. 부분 질의 $A_1, \ldots, A_i, \ldots, A_n$($n$개 원자의 논리곱이며, $A_i$는 술어가 IDB인 가장 왼쪽 원자입니다)과, 질의의 변수와 충돌하지 않도록 변수 이름이 새롭게 바뀐 규칙 $H \leftarrow B_1, \ldots, B_m$을 잡아 봅시다. $A_i$와 $H$가 단일화된다면, $\sigma$를 그 둘의 최대 일반 단일자(most general unifier, mgu), 즉 둘을 동일하게 만드는 가장 덜 구속적인 치환이라고 둡시다. 그 단계는 원자를 $\sigma$ 아래의 몸체로 치환합니다:

$$A_1 \ldots A_i \ldots A_n \;\;\leadsto\;\; (A_1 \ldots A_{i-1}\; B_1 \ldots B_m\; A_{i+1} \ldots A_n)\,\sigma .$$

이 단계의 건전성은 규칙을 오른쪽에서 왼쪽으로 읽는 논리 그 자체입니다: 어떤 치환 아래서 새 논리곱을 충족하는 저장소는 무엇이든 규칙의 몸체를 충족하고, 따라서 규칙의 머리 $H\sigma = A_i\sigma$를 충족하며, 따라서 옛 논리곱을 충족합니다. 혼 규칙에 대한 완전성은 SLD 귀결의 완전성이며, 이는 1권이 바로 이 규칙 형식에 대해 확립한 바입니다; 여기서 새로운 것은 오직 완전히 펼쳐진 모든 가지를 하나의 답으로 경주시키는 대신 UCQ로 모아 두는 장부 정리뿐입니다. 이것이 바로 DL-Lite 계열의 핵심 재작성 알고리즘인 PerfectRef의 재정식화 단계를, 혼 규칙의 옷을 입혀 놓은 것입니다 [3]. 동반 모듈의 구현은 부분 질의들에 대한 너비 우선 프런티어(frontier)입니다(mat_vs_rewrite.py 185–206행):

    frontier: list[tuple[int, tuple, list[tuple]]] = [(0, goal, [goal])]
    seen: set[tuple] = set()
    ucq: list[tuple[tuple, tuple]] = []
    while frontier:
        d, g, cq = frontier.pop(0)
        i = next((j for j, a in enumerate(cq) if a[0] in IDB), None)
        if i is None:
            key = _canon(g, cq)
            if key not in seen:
                seen.add(key)
                ucq.append((key[0], list(key[1])))
            continue
        if d == max_unfold:
            continue  # truncated: this branch's answers are given up
        for rule in rules:
            head, body = rename(rule, counter)
            s = unify(head, cq[i], {})
            if s is None:
                continue
            new_cq = [apply_sub(a, s) for a in cq[:i] + body + cq[i + 1:]]
            frontier.append((d + 1, apply_sub(g, s), new_cq))
    return ucq

IDB 원자가 하나도 남지 않은 부분 질의는 완결되어 UCQ에 합류합니다(정준 이름 재부여로 중복이 제거됩니다); 목표에 답한다는 것은 그런 다음 각 CQ를 기본 색인 위에서 평가하고 인스턴스화된 목표들을 합집합으로 묶는 것을 뜻합니다(mat_vs_rewrite.py 209–221행).

프런티어는 결국 비게 될까요? 비재귀적 술어들에 대해서는 그렇고, 그 논증은 명시적으로 짚어 둘 가치가 있는 순위 귀납(rank induction)입니다. 모든 EDB 술어에 순위(rank) 0을 매기고, 모든 비재귀적 IDB 술어에는 그 규칙 몸체 어디에서든 나타나는 가장 큰 순위보다 하나 큰 순위를 매깁니다: researcher는 순위 1입니다(그 몸체들은 기본 술어 professor와 student만을 언급합니다), person은 순위 2입니다(그 몸체는 researcher를 언급합니다), grandAdvisor와 colleague는 순위 1입니다. 각 펼침 단계는 어떤 순위 $r \ge 1$의 원자 하나를 없애고 $r$보다 엄격히 낮은 순위의 원자들을 유한하게 많이 끼워 넣습니다. 여기서는 어떤 순위도 2를 넘지 않으므로, (부분 질의 안의 순위 2 원자의 개수, 순위 1 원자의 개수)라는 쌍을 추적해 봅시다. 순위 2 원자에 대한 단계는 첫 번째 개수를 하나 줄입니다; 두 번째 개수는 늘어날 수 있지만 그것은 문제가 되지 않습니다. 순위 1 원자에 대한 단계는 첫 번째 개수를 그대로 두고 두 번째 개수를 하나 줄이는데, 오직 순위 0 원자만 들어오기 때문입니다. 따라서 모든 단계는 이 쌍을 사전식 순서(dictionary order)에서 엄격히 감소시킵니다: 첫 번째 개수가 줄어들거나, 아니면 그것이 그대로인 채 두 번째 개수가 줄어듭니다. 단계들의 무한한 연쇄는 불가능합니다: 그런 연쇄가 있다면, 결코 늘어나지 않는 음이 아닌 정수인 첫 번째 개수는 결국 변하기를 멈출 것이고, 그 시점부터는 두 번째 개수가 영원히 감소해야만 하는데, 음이 아닌 정수는 그럴 수 없습니다. 그러므로 펼침의 모든 가지는 멈추고, 프런티어는 스스로 비며, UCQ는 유한하고 완전합니다. 규칙 citesTransitively(A, C) ← cites(A, B), citesTransitively(B, C)는 이 순위 배정을 깨뜨립니다: 그 머리 술어가 자기 자신의 몸체 안에 나타나므로 유한한 순위가 존재하지 않고, 재귀적 원자를 펼칠 때마다 한 홉 더 바깥의 또 다른 사본이 만들어집니다. 구현은 이에 대해 정직합니다: max_unfold 상한이 그런 가지들을 잘라 내며, 잘려 나간 가지의 답들은 그냥 포기됩니다. 기본 학계 세계에 대해서는 이 모듈이 재작성기를 상한 3으로 실행하며, 이는 인용 사슬의 지름 2를 넘어서므로, 그곳에서는 잘림이 아무 비용도 들지 않습니다; 재귀 벽 절에서는 데이터가 그 상한을 넘어설 때 정확히 얼마의 비용이 드는지를 측정합니다.

커밋된 상수로부터 계산한 교차점

이 실험의 규율이 먼저 옵니다. 이것이 없으면 비용 비교는 무의미해질 것이기 때문입니다: 두 전략 모두 모든 질의에 대해 동일한 답을 돌려주어야 하며, 그래야 비용이 거래되는 유일한 것이 됩니다. 하니스는 다섯 질의짜리 장부를 실행하는데, 규칙 계열별로 질의 하나씩이며, 각 목표에 대해 구체화된 조회를 재작성된 UCQ와, 그리고 다른 파일에 있는 독립적인 후방 연쇄 엔진인 1권의 SLD 증명기와 맞대어 검사합니다(mat_vs_rewrite.py 352–356행):

        a_mat, p_mat = answers_mat(goal, index(mat))
        a_rew, n_cq, p_rew = answers_rewrite(goal, base_idx, RULES, 3)
        a_sld = set(sld.answers(goal))
        # Three-way agreement: lookup, UCQ, and the backward-chaining oracle.
        assert a_mat == a_rew == a_sld, f"{goal}: strategies disagree"

삼중 일치이지, 결코 자기 자신과의 비교가 아닙니다: 구체화기와 재작성기가 같은 버그를 공유한다면, 오라클이 그것을 잡아낼 것입니다. 의미론이 고정된 채로, 커밋된 장부는 순수한 회계입니다:

  query                              answers  CQs  probes mat  probes rew
  person(X)                                5    2          5           5
  researcher(X)                            5    2          5           5
  grandAdvisor(alice, Z)                   2    1          3           8
  colleague(carol, Y)                      2    1          8          13
  citesTransitively(p3, X)                 2    3          3          12

각 행을 읽어 보십시오. 저마다 서로 다른 것을 가르쳐 주기 때문입니다. 두 개의 단항 질의는 각각 5번의 탐침으로 동점입니다: 그 UCQ들(person은 researcher를 거쳐 professor와 student의 합집합으로 펼쳐집니다)은 오직 단일 원자 CQ만을 담고 있으므로, 그것들을 평가하는 것은 폐쇄 조회가 도출된 색인에서 훑어볼 것과 정확히 같은 기본 사실들을 훑어봅니다. 펼침이 모든 결합을 없애 버릴 때는 재작성이 아무것도 잃지 않습니다. 세 개의 이항 질의는 결합 비용이 떨어지는 곳입니다: grandAdvisor(alice, Z)는 하나의 CQ, advises(alice, Y), advises(Y, Z)이며, 그 왼쪽에서 오른쪽으로의 결합은 4개 사실짜리 advises 색인을 한 번은 Y를 묶기 위해, 그리고 각 묶음마다 한 번 더 훑어보아, 조회의 3번에 대비해 8번의 탐침이 듭니다. 하니스는 이 패턴을 일반적으로 단언합니다, p_mat <= p_rew가 언제나 성립하고, 재작성 안의 어떤 CQ가 원자를 하나보다 많이 가질 때는 엄격하게 성립합니다(mat_vs_rewrite.py 359–361행): 결합이 구체화 아래서 사라진 것이 아니라, 적재 시점에 값이 치러지고 그 결과가 저장되었을 뿐입니다.

이제 항등식을 조립해 봅시다. 장부 전체를 한 번 통과하는 데는 구체화가 $5+5+3+8+3 = 24$번의 탐침을, 재작성이 $5+5+8+13+12 = 43$번의 탐침을 씁니다; 구체화는 또한 236번의 적재 탐침이라는 절편을 짊어집니다. 장부 한 번의 통과를 작업 부하 단위 $q$로 취급합시다(모듈은 질의당 상수들을 출력합니다; 아래의 합계는 그 커밋된 숫자들에 대한 산술일 뿐, 별도의 실험이 아닙니다):

$$\mathrm{Total}^{m}(q) = 236 + 24\,q, \qquad \mathrm{Total}^{r}(q) = 43\,q,$$

그리고 두 직선의 교차점은

$$q^{*} \;=\; \frac{236}{43 - 24} \;=\; \frac{236}{19} \;\approx\; 12.42 .$$

장부 통과 횟수 $q$	구체화: $236 + 24q$	재작성: $43q$	더 저렴한 전략
1	260	43	재작성, 6배
5	356	215	재작성
12	524	516	재작성, 근소하게
13	548	559	구체화, 근소하게
100	2,636	4,300	구체화, 1.6배

이 표는 이 장의 논지를 다섯 줄로 담고 있습니다. 장부를 한 번 물으면 구체화는 여섯 배나 지나치게 많은 작업을 한 셈입니다: 아무도 묻지 않은 colleague 사실과 person 사실을 도출했으니, 새벽 준비 주방이 결코 오지 않을 주문을 위해 양파를 썰어 댄 것입니다. 백 번 물으면 재작성은 같은 grandAdvisor 결합을 백 번 다시 도출한 반면, 구체화된 저장소는 반복될 때마다 3번의 탐침으로 응대했습니다. 뒤바뀜은 열세 번째 통과에 자리 잡고 있으며, 그 위치가 조율 가능한 통찰입니다: 더 큰 폐쇄나 더 값비싼 규칙은 절편을 높여 $q^{*}$를 오른쪽으로 밀어내고; 더 깊은 결합을 가진 더 무거운 질의는 기울기 격차를 넓혀 그것을 왼쪽으로 끌어당깁니다. 질의가 적고 데이터가 무거우며 갱신이 잦은 체제는 교차점 왼쪽에 살며 재작성을 원합니다; 질의가 많고 대부분 읽기만 하는 체제는 그 오른쪽에 살며 구체화를 원합니다. 이 축소판의 규모에 관한 그 무엇도 이 모양을 바꾸지 않으며, 오직 상수만이 바뀝니다: 10억 트리플 규모에서는 절편이 236번의 탐침이 아니라 단일 스레드로는 몇 시간, 128코어로는 몇 분의 작업이며 [2], 단 한 번, 혹은 결코 질의되지 않을 차가운 데이터야말로 정확히 그 절편을 치르는 것이 실수인 경우이며, 이것이 바로 재작성 엔진들이 적재는 공짜이고 차가운 데이터는 차가운 채로 남는다고 광고하는 이유입니다.

유지보수: 항등식이 감추는 비용

항등식 $\mathrm{Total}(q) = C_{\text{load}} + q\,C_{\text{query}}$에는 변화에 대한 항이 전혀 없으며, 변화야말로 두 전략이 더 이상 서로의 거울상이 아니게 되는 지점입니다. 현대의 구체화 엔진들은 증분 갱신을 일급 알고리즘 문제로 다루는데, 모든 편집마다 처음부터 고정점을 다시 돌리는 것은 이 전략 전체가 존재하는 이유인 상각을 몰수하는 셈이기 때문입니다 [4]. 동반 모듈은 학계 세계 위에서 변화의 두 방향 모두에 값을 매깁니다:

[2] updates break the symmetry
  add advises(alice, carol):
    materialized: semi-naive delta, 1 round, 12 probes → +1 derived grandAdvisor(alice, erin)
    rewriting   : ZERO maintenance — the same UCQ over the grown
                  base already answers grandAdvisor(alice, erin)
  delete cites(p3, p2) with the diamond cites(p3, p1) asserted:
    naive drop leaves a STALE fact: citesTransitively(p3, p2)
    DRed overdeletes 2 derived facts (both citesTransitively above p3) ...
    ... and re-derives 1: citesTransitively(p3, p1) has a second proof via the diamond
    result == the from-scratch fixpoint, fact for fact

삽입은 쉬운 방향이며, 그 이유는 이미 유도해 둔 델타 규칙입니다. advises(alice, carol)를 더하면 $\Delta_0$에 사실 하나가 씨앗으로 놓입니다; 앞서 인용한 준단순 루프는 그것을 저장소에 대해 결합하여, grandAdvisor(alice, erin)을 도출하고(이제 alice는 carol을 지도하고, carol은 erin을 지도합니다), 더 이상 아무것도 찾지 못한 채 멈춥니다: 원래 폐쇄가 처음부터 치렀던 236번에 대비해, 1라운드, 12번의 탐침이며, 하니스는 이 증분적으로 유지된 폐쇄가 커진 기본 사실 집합의 처음부터 다시 지은 고정점과 정확히 같다는 것을 단언합니다(mat_vs_rewrite.py 366–368행). 단조성이 모든 일을 해냅니다: 혼 규칙은 오직 귀결을 더할 뿐이므로, 옛 도출들은 여전히 유효하고 새 사실의 귀결들은 순수한 추가분일 뿐입니다. 재작성 쪽은 그보다도 낫습니다: 유지보수할 것이 아무것도 없는데, 도출된 것을 아무것도 저장하지 않기 때문입니다. 커진 기본 사실 집합 위에서 평가된 같은 UCQ는 새로운 조합을 즉시 알아채며, 하니스는 이 역시 오라클에 맞대어 단언합니다(mat_vs_rewrite.py 375–380행).

삭제는 어려운 방향이며, 그 이유는 이 모듈이 일부러 공학적으로 설계해 둔 계수(counting) 사실입니다: 도출된 사실은 도출 방법을 하나보다 많이 가질 수 있습니다. 삭제하기에 앞서, 이 모듈은 추가 기본 사실 cites(p3, p1)을 단언하여 citesTransitively(p3, p1)에 두 개의 독립적인 증명, 즉 직접 엣지와 p2를 거치는 두 홉짜리 경로를 부여합니다. 이제 기본 사실 cites(p3, p2)를 지워 봅시다. 그것을 폐쇄에서 단순하게 떨어뜨리면 저장소가 진부해집니다(stale): citesTransitively(p3, p2)는 어떤 살아남은 도출도 그것을 뒷받침하지 않는데도 여전히 색인 안에 앉아 있으며, 하니스는 정확히 이 사실을 유일하게 진부한 생존자로 못박습니다(mat_vs_rewrite.py 386–390행). 구체화된 저장소는 기본 사실 하나를 그냥 잊어버릴 수 없습니다; 그것은 하류의 모든 도출된 사실에 대해, 다른 어떤 근거가 그것을 계속 살려 두는지를 결정해야 합니다. 고전적인 답은 삭제 후 재도출을 뜻하는 DRed(delete-and-rederive)이며 [5], 과잉 삭제 후 복구하는 규율입니다(mat_vs_rewrite.py 291–308행):

    old_idx = index(closure)
    deleted: set[tuple] = {fact}
    while True:
        new: set[tuple] = set()
        for head, body in rules:
            subs, _ = eval_cq(body, old_idx)
            for s in subs:
                if any(apply_sub(a, s) in deleted
                       for a in body if a[0] != "neq"):
                    h = apply_sub(head, s)
                    if h not in deleted:
                        new.add(h)
        if not new:
            break
        deleted |= new
    survivors = closure - deleted
    final = fc.least_fixpoint(survivors, rules)
    return final, deleted, final & deleted

1단계는 삭제된 집합을 위쪽으로 닫습니다: 삭제된 사실을 사용해 옛 폐쇄 위에서 어떤 한 단계 도출이라도 가진 머리는 그 집합에 합류합니다. 이는 일부러 과잉 근사한 것입니다. 그 정확성의 방향은 도출 높이에 대한 귀납입니다: 어떤 사실의 모든 도출이 삭제된 기본 사실을 쓴다면, 각 도출의 꼭대기에서 어떤 몸체 원자가 (귀납적으로) 삭제되어 있으므로, 그 사실은 그 집합에 들어갑니다; 따라서 모든 근거를 진정으로 잃은 것치고 1단계에서 살아남는 것은 없습니다. 하지만 그 역은 성립하지 않으며, 다이아몬드가 그것이 실패하는 모습을 보여 줍니다: citesTransitively(p3, p2)와 citesTransitively(p3, p1) 둘 다 삭제된 엣지를 거치는 도출을 하나 가지고 있으므로, 둘 다 과잉 삭제되는데, 후자는 여전히 온전한 대안 증명을 가지고 있는데도 그렇습니다. 2단계는 그 부수적 피해를 복구합니다: 생존자들로부터 규칙을 고정점까지 다시 돌리면, 독립적인 도출을 가진 과잉 삭제된 사실은 모두 되돌아옵니다. 커밋된 계수가 그 전시물입니다: 과잉 삭제 2건, 재도출 1건, 최종 폐쇄는 처음부터 다시 지은 고정점과 사실 하나하나까지 같으며, 세 집합 모두가 정확히 단언되어 있습니다(mat_vs_rewrite.py 391–401행). 발췌의 마지막 두 줄에 있는 즐거운 절약을 눈여겨보십시오: 그 복구 단계는 1권 자신의 least_fixpoint이며(examples/logic/forward_chain.py 52–63행), 유지보수 알고리즘이 말 그대로 적재 시점 엔진을 재사용하는 것입니다.

사실들이 풍부하게 뒷받침될 때 과잉 삭제 후 복구를 오가는 이 소모는 DRed의 알려진 약점이며, 이 분야의 더 정교한 답은 그 단계들을 뒤집습니다: Backward/Forward 알고리즘은 후보를 삭제하기 전에, 생존한 사실들로부터 대안적인 도출이 존재하는지를 근거를 찾는 후방 탐색과 전방 검사를 결합해 확인하고, 아무것도 찾지 못할 때에만 삭제합니다 [4]. 다이아몬드 사실은 정확히 그것이 대비해 지어진 경우입니다: 후방 탐침 한 번이면 생존한 엣지 cites(p3, p1)을 찾아내어 citesTransitively(p3, p1)이 삭제와 부활을 오가는 왕복을 겪지 않도록 해 줄 것입니다. 동반 모듈은 DRed만을 구현하고 Backward/Forward는 인용만 합니다; 그 셈해진 실행이 기여하는 것은 그 이유입니다: 대안-도출 검사가 존재하는 목적인 바로 그 왕복의 실측 사례입니다. 재작성 쪽에서는 삽입과 마찬가지로 삭제도 공짜입니다: 기본 사실을 떨어뜨리면, 다음 질의의 UCQ는 그저 더 이상 그것을 찾지 못할 뿐입니다. 따라서 이 거래의 유지보수 항목은 이렇게 읽힙니다: 재작성은 결코 아무것도 치르지 않고; 구체화는 삽입에는 작은 델타를, 삭제에는 진정으로 미묘한 알고리즘을 치릅니다. 갱신이 잦은 작업 부하는 질의가 적은 작업 부하만큼이나 확실하게 교차점을 오른쪽으로 옮깁니다.

재귀 벽과 조각 의존성

지금까지는 두 전략을 의미상 상호 교환 가능하며 오직 비용에서만 다르다고 다루어 왔습니다. 이 장에서 가장 깊은 지점은 이 대칭성이 논리의 성질이라는 것이며, 그것이 깨진다는 것입니다. 동반 모듈은 그 깨지는 지점을 하나의 매개변수로 규모를 조절할 수 있는 합성 인용 사슬로 지어 냅니다(mat_vs_rewrite.py 316–318행):

CHAIN_M: int = 8
CHAIN_FACTS: list[tuple] = [
    ("cites", f"c{i}", f"c{i + 1}") for i in range(CHAIN_M)]

여덟 개의 사실, $c_0 \to c_1 \to \cdots \to c_8$이므로, 목표 citesTransitively(c0, X)는 여덟 개의 답을 가지며, 그중 가장 먼 것은 재귀 깊이 8을 필요로 합니다. 구체화는 이를 전혀 알아채지 못합니다: 같은 두 개의 데이터로그 규칙이 어떤 길이에서든 사슬을 닫는데, 고정점은 "끝났다"는 것이 아무리 깊이 밝혀지든 끝날 때까지 돌아가기 때문입니다. 이와 대조적으로 재작성은 데이터를 보기 전에 펼침 깊이 $k$를 고정해야 하며, 재귀 규칙을 한 번 펼칠 때마다 정확히 한 홉 더 멀리 도달합니다. $k$에 대한 커밋된 스윕은 다음과 같습니다:

[3] the recursion wall — citesTransitively(c0, ?) on the 8-hop chain
  a depth-k UCQ holds one CQ per path length ≤ k: sound at every
  k, complete only when k reaches the data's diameter
     k   CQs  answers/8  probes  complete?
     1     1      1/8       8   no
     2     2      2/8      24   no
     3     3      3/8      48   no
     4     4      4/8      80   no
     5     5      5/8     120   no
     6     6      6/8     168   no
     7     7      7/8     224   no
     8     8      8/8     288   yes

하니스는 각 행의 형태를 단언합니다: 깊이-$k$ UCQ는 경로 길이가 $k$ 이하인 것마다 하나의 CQ를 담고 있고, 정확히 가장 가까운 $k$개의 답을 돌려주며(건전하며, 결코 답을 지어내지 않습니다), 오직 $k = 8$, 즉 데이터의 지름에서만 완전합니다(mat_vs_rewrite.py 411–423행). 사슬을 늘리면 그 벽도 함께 움직입니다: 미리 골라 둔 어떤 고정된 $k$도 모든 데이터셋에서 살아남지 못합니다. 이는 실제 정리의 유한한 그림자입니다. 정리(도입) [6]: 추이 폐쇄는 1차 논리로 표현될 수 없습니다: 이항 관계 기호 $E$에 대한 1차 논리식 $\varphi(x, y)$ 중, 모든 유한 그래프 위에서 $\varphi$가 정확히 방향이 있는 $E$-경로로 연결된 쌍들에 대해서만 성립하게 만드는 것은 존재하지 않습니다. 해독하면: "1차"란 오직 개체에 대해서만 양화한다는 뜻이며, 이는 정확히 UCQ의 표현력이자, 사실 재귀가 없는 평범한 SQL 질의의 표현력입니다; 이 정리는 그런 질의는 아무리 크더라도 모든 입력에서 도달 가능성을 계산할 수 없다고 말합니다. 그 증명은, 어떤 고정된 1차 논리식이든 자신의 인자들 주위 유한 반경의 이웃만을 볼 수 있는 반면 도달 가능성은 무제한 반경을 필요로 함을 보이는 유한 모델 이론의 국소성(locality) 논증이며, 이 권의 범위를 넘어섭니다; 동반 모듈이 대신 보여 주는 것은 유한한 인스턴스가 제공할 수 있는 전시물입니다. 깊이-$k$ 재작성이 지름보다 낮은 모든 $k$에서 실패한다는 것이며, 이는 그 정리를 예시할 뿐 증명하지는 않습니다.

시스템적 귀결은 조각 의존성이며, 이는 양쪽 모두에 대해 정밀한 진술을 받을 가치가 있습니다. 정리(도입) [3]: 모든 DL-Lite TBox $\mathcal{T}$(용어 공리들)와 모든 논리곱 질의 $q$에 대해, PerfectRef 알고리즘은 유한한 UCQ $q_{\mathcal{T}}$를 계산하며, 이는 $\mathcal{T}$와 일관된(consistent) 모든 ABox $\mathcal{A}$(단언적 데이터)에 대해 $(\mathcal{T}, \mathcal{A})$ 위에서의 $q$의 확실한 답이, 평범한 데이터베이스로 저장된 $\mathcal{A}$ 위에서 직접 평가된 $q_{\mathcal{T}}$의 답과 같도록 해 줍니다. (이 일관성 단서는 아무 비용도 들지 않습니다: DL-Lite 지식 베이스가 일관된지 자체도 데이터 위에서 고정된 1차 질의 하나를 평가하는 것으로 판정되므로, 과제 전체는 여전히 1차에 머뭅니다.) 이 성질이 1차 재작성 가능성(FO-rewritability)입니다: TBox가 질의 안으로 완전히 컴파일되므로, DL-Lite에서의 질의 응답은 적재 시점 추론이 전혀 없는 평범한 테이블 위의 평범한 SQL로 실행되며, 그 데이터 복잡도(data complexity, 질의와 TBox를 고정해 둔 채 데이터가 커질 때의 비용)는 고정된 관계형 질의로 평가될 수 있는 클래스 안에 놓입니다. 이는 운이 좋아서가 아니라 설계된 결과입니다: DL-Lite의 공리 형태는 정확히 1차 재작성이 흡수할 수 있는 것이 되도록 골라졌으며, 그 위에 지어진 웹 온톨로지 프로파일인 OWL 2 QL은 정확히 그 사슬이 보여 주는 이유로 추이성과 재귀를 금지하는 반면, 규칙 엔진을 위해 지어진 프로파일인 OWL 2 RL은 구체화가 그것들을 다룰 수 있으므로 그것들을 유지합니다. 반대쪽에서는, 같은 출처가 그 경계를 정확히 그어 둡니다: 공리에 EL 방식의 구성자(포섭의 왼쪽에 놓이는 한정된 존재 제한)를 더하면 질의 응답은 데이터 복잡도에서 PTIME-난해(PTIME-hard)해지며 [3], 2권은 이미 EL 분류가 PTIME-완전임을 보였습니다. PTIME-난해 문제는 고정된 1차 질의로 풀 수 없는데, 그 평가는 고정된 1차 질의를 포착하는 상수 깊이 불리언 회로 클래스인 $\mathrm{AC}^0$ 안에 놓이며 이는 PTIME보다 증명 가능하게 약하기 때문입니다; 그 분리의 증명 역시 이 권의 범위를 넘어섭니다. 결론은 이 장이 정당하게 얻어 내려는 바로 그 문장입니다: 논리를 선택하는 것은 여러분의 시스템 선택지를 선택하는 것입니다. DL-Lite에서는 재작성이 정리에 의해 완전하므로, 작업 부하가 지시하는 대로 어느 극에든 앉을 수 있습니다. EL과 그보다 풍부한 혼 조각들에서는 순수한 질의 재작성만으로는 원리적으로 불충분하며, 구체화(또는 한정된 핵심부를 구체화하고 그 위에서 재작성하는 하이브리드인 "결합 접근법(combined approach)" 계열)가 완전성을 위해 필수적이며, 앞 절의 유지보수 장치 전체가 그와 함께 따라옵니다.

시스템의 닻

이 축소판의 각 극에는 그 위에 서 있는 실제 생산 시스템이 있으며, 이미 인용한 숫자들은 바로 그것들의 것입니다. 구체화 극의 닻은 RDFox입니다: 위에서 유도한 준단순, 비반복 규율을 새로 도출된 사실별로 작업을 나누어 병렬화함으로써 부하 균형이 예약되는 것이 아니라 저절로 나타나게 하며 [1], LUBM-50K에서 규모에 맞게 보고되었습니다: 67억 개의 명시적 트리플이 92억 개로 닫히고, 초당 610만 트리플의 구체화 속도를 내며, 128스레드 실행이 단일 스레드보다 69.6배 더 빠릅니다 [2]. 재작성 극의 닻은 두 개입니다. DL-Lite 계열에서는 PerfectRef 방식의 엔진들(온톨로지 기반 데이터 접근, 즉 OBDA 계열)이 TBox를 SQL로 컴파일하여 모든 질의를 손대지 않은 관계형 데이터베이스로 보내며, 이것이 위 정리가 완전성을 보장하는 그 전략입니다 [3]; 이들의 본거지는 질의가 적고, 갱신이 잦으며, 데이터가 남의 방화벽 뒤에 있는 체제입니다. 표현력이 풍부한 DL 계열에서는, 혼을 훨씬 넘어서는 논리를 위한 타블로(tableau) 추론기인 Konclude가 흡수(absorption)에 의지합니다: 일반 공리를 트리거 형태로 다시 써서, 개체의 알려진 소속이 그 공리를 관련 있게 만들 때에만 각 공리가 결정론적으로 적용되도록 하고, 모든 곳에서 투기적인 경우 나누기를 강제하지 않게 하는 전처리입니다 [7]. 출처는 흡수를 타블로 최적화로 제시합니다; 이 장의 렌즈로 읽으면, 이는 다른 기계 장치를 걸친 같은 회계적 직감입니다: 아무 개체도 건드리지 않는 공리에는 값을 치르지 마십시오.

극	닻	설계 특징	본거지 체제
구체화	RDFox [1] [2]	병렬 준단순 폐쇄, 사실별 분할, 증분 유지보수	대부분 읽기, 질의가 많음, 재귀를 지님(OWL 2 RL / 데이터로그)
재작성	PerfectRef / OBDA 엔진 [3]	TBox가 UCQ로 컴파일되어 날것의 데이터 위에서 SQL로 평가됨	질의가 적음, 갱신이 잦음, 1차 재작성 가능(DL-Lite / OWL 2 QL)
재작성(표현력이 풍부한 경우)	Konclude [7]	흡수: 공리가 게으르게, 관련될 때에만 발동되도록 다시 쓰임	완전한 구체화가 불가능한 표현력이 풍부한 DL

뉴로-심볼릭의 메아리: 벡터를 걸친 같은 거래

4권은 이름을 붙이지 않은 채 정확히 이 거래를 실행했습니다. 퍼지 및 훈련 없는 복합 논리 질의 응답(CLQA) 장의 훈련이 필요 없는 질의 최적화기인 QTO(Query computation Tree Optimization)는 무엇에도 답하기 전에 자신의 신경망 인접 행렬들을, 관계마다 하나씩의 조밀한 개체 대 개체 점수표를, 미리 계산했습니다: 1홉 예측기의 믿음을 적재 시점에 폐쇄한 것으로, 한 번만 값을 치러 두어 모든 다홉 질의가 저장된 점수들에 대한 텐서 조회와 최댓값-곱으로 바뀌게 만들었습니다. 이는 절편까지 포함한, 임베딩 공간 안의 구체화입니다(그 행렬들의 메모리 사용량이 폐쇄의 저장 임대료입니다). 같은 장에 나온 CQD(Continuous Query Decomposition)는 그 반대로 했습니다: 훈련된 링크 예측기만 남겨 두고 답하는 시점에 각 질의를 t-노름으로 이어붙인 1홉 호출들의 수열로 펼쳤으며, 질의마다 값을 치르되 도출된 것은 아무것도 저장하지 않았습니다. 이는 가파른 기울기까지 포함한, 임베딩 공간 안의 재작성입니다(깊은 질의는 톡톡히 비용을 치르는데, 정확히 장부의 결합 행들이 아파하던 바로 그 지점입니다). 유지보수 항목까지도 그대로 넘어옵니다: 다시 훈련된 예측기로 갈아 끼우면 CQD는 다음 질의에서 그것을 공짜로 받아들이는 반면, QTO는 모든 인접 행렬을 다시 구체화해야 하고, 처음부터 다시 계산하는 것보다 더 영리한 방법은 제시되어 있지 않습니다. 결국 이 고전적인 회계 항등식은, 사들이는 귀결이 명확한 사실인지 점수인지 신경 쓰지 않는 것으로 드러납니다.

아직 풀리지 않은 부분

깔끔한 두 극의 그림은 교육적인 배려입니다; 실무는 두 극 사이에 살고 있으며, 그 사이에는 깔끔한 이론이 없습니다. 부분 구체화(partial materialization)는 어떤 도출된 술어, 또는 그 조각들 중 어느 것이 저장될 가치가 있는지를 묻습니다: 작업 부하가 grandAdvisor를 두들겨 대니 그것은 구체화하고, 아무도 묻지 않으니 colleague는 재작성합니다. 형식적으로 이는 뷰 선택(view selection)이며, 저장 예산 아래에서 항등식의 총합을 최소화하는 구체화된 뷰들의 집합을 고르는 문제이고, 이는 작업 부하에 의존하는 조합 최적화 문제인데, 그 입력(미래의 작업 부하, 미래의 갱신 스트림)이 바로 시스템이 미리 알 수 없는 것들입니다. 엔진들은 발견적 방법(heuristic)을 내놓을 뿐, 누구도 정리를 내놓지는 못합니다. 스트리밍 데이터와 시간에 따라 변하는 데이터는 두 극 모두에 동시에 부담을 줍니다: 구체화된 저장소는 만료되는 사실마다 삭제 하나에 직면하고(3권의 시간적 주석을, 유효 구간으로 읽으면, 모든 사실이 예정된 삭제가 됩니다), 재작성 엔진은 답변 도중 바뀐 데이터에 맞서 자신의 UCQ들을 다시 실행하는 문제에 직면합니다. 그리고 이 권 자신의 궤적은 가장 새로운 미해결 전선을 더합니다: QTO의 미리 계산된 인접 행렬이 그랬듯 "규칙"이 신경망 가중치일 때는, DRed가 없습니다. 1홉 예측기를 바꾸는 미세 조정 하나가 모든 구체화된 점수 중 알 수 없고 구조화되지 않은 부분집합을 무효화하는데, 어떤 도출 그래프도 어느 것이 무효화되는지 기록해 두지 않으며, 알려진 유일하게 건전한 유지보수는 전면 재계산뿐입니다. 도출 대신 그래디언트를 위한 다이아몬드 전시물의 장부 정리 같은, 학습된 폐쇄를 위한 삭제 후 재도출 규율은 아직 존재하지 않으며, 앞으로 이어질 시스템 관련 장들은 계속해서 그 부재와 부딪힙니다.

왜 중요한가

이 장은 이 시리즈의 의미론과 시스템 사이를 잇는 경첩입니다. 1권의 고정점, 2권의 EL 완성, 4권의 접지된 회로는 모두, 이 장의 용어로 말하면, 소리 없이 내려진 구체화 결정이었습니다; 4권의 CQD는 소리 없이 내려진 재작성 결정이었습니다. 그 축에 이름을 붙이는 일은 그 기본값들을 값이 매겨진 선택으로 바꾸어 놓으며, 그 값은 여러분 자신의 연구가 치르게 될 바로 그것입니다: 여러분의 벤치마크가 고정된 지식 그래프에 대해 백만 번의 질의를 던진다면, 여러분은 $q \gg q^{*}$(기호 $\gg$는 "훨씬 크다"라고 읽으며, 교차점을 훨씬 웃도는 작업 부하를 뜻합니다)에 있는 것이고 사전 계산은 반칙이 아니라 산술입니다; 여러분의 시스템이 실시간 스트림을 받아들이며 이따금 질문에만 답한다면, 여러분은 작은 $q$에 있는 것이고 구체화된 텐서 하나하나가 저장 임대료이자 예산에 없는 유지보수 부채입니다. 조각 의존성은 더 깊은 연구 도구입니다. 이는 표현력에 관한 주장과 시스템에 관한 주장이 같은 주장이라고 말합니다: 여러분의 논리에 공리 형태 하나를 더하는 것만으로 질의 응답이 "정리에 의해 SQL로 컴파일된다"에서 "정리에 의해 유지보수되는 폐쇄가 필요하다"로 옮겨 갈 수 있으며, 모든 고정-레이어 네트워크가 그러하듯 펼침 깊이를 미리 고정하는 뉴로-심볼릭 아키텍처는, 그 저자들이 알아챘든 아니든, 이 축 위에서 하나의 입장을 이미 취한 것입니다. 다음 두 장은 그 관찰을 정량적으로 만드는데, 먼저 추론기에 대해, 그다음 트랜스포머에 대해 그렇게 합니다.

핵심 용어

• 구체화(Materialization): 규칙들의 최소 고정점을 기본 사실들 위에서 적재 시점에 계산하고 저장하여, 질의가 색인 조회가 되도록 하는 것; OWL 2 RL / 데이터로그 엔진의 전략입니다.
• 질의 재작성(Query rewriting): 질의를 규칙들을 거슬러 후방으로 펼쳐 기본 술어들에 대한 논리곱 질의들의 합집합으로 만들고, 날것의 데이터에 맞대어 평가하는 것; 적재는 공짜이고, 질의마다 값을 치릅니다.
• 논리곱 질의들의 합집합(Union of conjunctive queries, UCQ): 결합(join)들의 유한한 논리합; 재작성의 목표 형식이며, 정확히 재귀가 없는 1차 질의의 표현력입니다.
• EDB / IDB: 기본 사실로 저장된 술어들로 이루어진 외연 데이터베이스와 규칙의 머리로 정의된 술어들로 이루어진 내포 데이터베이스; 재작성은 오직 EDB 원자만 남을 때 종료합니다.
• 준단순 평가 / 델타 규칙(Semi-naive evaluation / delta rule): 새로 도출된 몸체 사실을 적어도 하나 가진 규칙 인스턴스만을 결합하는 규율로, 위에서 모든 첫 발화를 찾아낸다는 것이 증명되었습니다; 비반복성(non-repetition property)은 어떤 인스턴스도 결코 두 번 발화하지 않는다는 그 보장입니다.
• 상각(Amortization): 질의당 절감을 통한 적재 시점 절편의 되갚음; 교차 작업 부하 $q^{*} = C^{m}_{\text{load}} / (C^{r}_{\text{query}} - C^{m}_{\text{query}})$에서 완결됩니다.
• DRed(삭제 후 재도출, delete-and-rederive): 삭제된 사실을 거치는 도출을 하나라도 가진 모든 것을 과잉 삭제한 다음, 나머지로부터 생존자들을 재도출하는 삭제 유지보수; 정확하지만, 사실들이 대안적인 도출을 가질 때 정확히 낭비적입니다.
• Backward/Forward 알고리즘: 후보를 삭제하기 전에 대안적인 도출을 탐색하여, DRed의 과잉 삭제 후 복구 왕복을 피하는 삭제 유지보수입니다.
• 1차 재작성 가능성(FO-rewritability): TBox 추론이 모든 질의에 대한 유한한 1차(UCQ) 재작성으로 완전히 컴파일된다는 성질; DL-Lite에서는 정리에 의해 성립하고, EL과 추이 폐쇄에서는 원리적으로 성립하지 않습니다.
• 탐침(Probe): 동반 모듈의 비용 단위입니다: 술어 색인 아래에서 훑어본 후보 사실 하나, 또는 접지 부등호 검사 하나입니다.

다음으로 이어지는 것

구체화는 이 장의 모든 표에서 오른쪽 절반을 이겼으며, 이는 그 절편을 다음 병목으로 만듭니다: 폐쇄가 여러분이 치르는 값이라면, 그 폐쇄 자체는 얼마나 빨리 지어질 수 있을까요? GPU 추론은 2권의 EL 완성을 가져와 규칙 계산법 전체를 불리언 행렬 대수로 다시 표현하고, 백 개의 온톨로지에 걸쳐 고정점을 한꺼번에 배치 처리하는데, 이 장의 준단순 델타 규율이 행렬 마스크로 다시 나타나고 모든 폐쇄가 기호적 오라클에 맞대어 칸 하나하나까지 검사됩니다.

---

동반 코드: examples/frontier/mat_vs_rewrite.py는 셈해진 단순 고정점, 귀결 기반 UCQ 재작성기, 준단순 추가 델타, DRed 삭제, 그리고 재귀 벽을, 1권의 examples/logic/kb.py, forward_chain.py, sld.py, unify.py 위에서 구현합니다. 이 장의 모든 숫자를 재현하려면 python3 examples/frontier/mat_vs_rewrite.py를 실행하십시오; 그 실행은 결정론적이며 모든 주장은 assert에 의해 지켜지고, 질의 장부는 독립적인 SLD 오라클에 맞대어 삼중으로 검사됩니다.