Datalog 해체하기

2022년 9월, 두 차례의 수정 끝에 나는 내 박사학위 논문 Deconstructing Datalog의 최종본을 제출했다. Datalog는 1980년대의 논리 프로그래밍 언어로, 관계 대수에 재귀 질의를 덧붙인 것이다. 이 언어는 의미론이 단순하면서도 구현 전략이 효율적이다. Lisp와 Velvet Underground처럼, 인기도보다 영향력이 더 크며, 그 아이디어는 지금도 주류 속으로 계속 흡수되고 있다.

Datalog는 아주 높은 가성비를 지녔지만, 상당히 제한적이기도 하다. 우선 함수나 프로시저가 없다. 즉, 반복되는 코드를 추상화할 방법이 없다. 타입드 함수형 프로그래밍의 팬으로서 나는 이렇게 생각했다. 얼마나 어렵겠어? 우리에게는 x (상향식 논리 프로그래밍)가 있고, y (함수형 프로그래밍)가 있다. 그렇다면 x+y 는 무엇일까? 레고를 가지고 노는 아이처럼, 나는 두 가지 멋진 것을 한데 뭉쳐 더 크고 더 멋진 것을 만들겠다고 나섰다. 바로 Datafun이다.

성공했다!

하지만,

문제들도 있었다.

그리고 그 전체 이야기를 알고 싶다면, 그냥 읽어보면 된다. 비교적 짧은 논문이다. 97쪽에 말미 부록이 조금 더 붙는다. 하지만 핵심 결과는 주로 두 가지다. (i) 이 괴상한 아이디어가 실제로 작동한다는 것, 그리고 (ii) 점근적 의미에서 그것을 제법 빠르게 만들 수 있다는 것이다.

Datalog를 분해했다가 다시 조립하기

내 논문의 중심 아이디어는, Datalog의 기능들을 그 의미론 에서 거꾸로 출발해 타입드 함수형 언어에 매끄럽게 통합할 수 있다는 것이다. Datalog의 가장 두드러진 특징인 재귀 질의 를 보자. 예를 들어 그래프에서의 도달 가능성이다.

reachable(start).
reachable(Y) :- reachable(X), edge(X,Y).

이것은 reachable 이 다음 두 조건을 만족하는 가장 작은 집합이 되도록 찾는다. 즉, (1) start 는 도달 가능하고, (2) X 가 도달 가능하며 Y 로 가는 간선을 가지면, Y 역시 도달 가능하다. 이 조건들을 집합에 대한 하나의 부등식으로 다시 쓸 수 있다.

reachable ⊇ {start} ∪ {y : x ∈ reachable, (x,y) ∈ edge}

이제 오른쪽을 묶어 빼내도록 다시 쓸 수 있다.

reachable ⊇ f(reachable)
where f(R) = {start} ∪ {y : x ∈ R, (x,y) ∈ edge}

이것은 최소 전고정점, 즉 어떤 관계 위의 함수 f 에 대해 적어도 f(R) 를 포함하는 가장 작은 R 을 구하라는 뜻이다. 사실 Datalog의 모든 재귀 질의는 이 패턴에 들어맞는다. 따라서 재귀 질의를 함수형 언어로 포착하려면, (a) 관계 위의 함수들을 표현할 수 있는 표현력 있는 언어와, (b) 최소 전고정점 연산자 fix 가 필요하다. 그러면 위 질의는 다음과 같이 된다.

fix (λR. {start} ∪ {y | x ∈ R, (x,y) ∈ edge})

아주 짧은 몇 단계 만에, 우리는 술어와 논리를 집합과 함수로 바꾸어 놓았다.

2장에서는 이 과정을 자세히 전개한다. 그중에서도 특히 독특한 점은, 재귀 질의가 잘 정의되도록 보장하는 Datalog의 층화 조건을 포착하기 위해 Datafun이 타입 시스템 안에서 단조성을 추적해야 한다는 것이다. 이것은 합성적으로 작동한다. 두 함수의 합성이 단조적이려면 두 함수 모두 단조적이어야 하고, 그렇지 않으면 단조적이지 않다. 좀 더 기술적으로 말하면, 비단조성은 그 밖에는 단조적인 세계 안에서 (범주론에서는) 모노이달 코모나드, 혹은 (타입 이론에서는) 필연성 양상, 혹은 (컴파일러에서는) 어떤 변수를 비단조적으로 사용해도 안전한지 세심하게 추적하는 방식으로 표현될 수 있다. 대부분의 타입 시스템과 마찬가지로 이것은 안전하지만 불완전하다. 즉, 타입 검사기는 실제로는 단조적인 몇몇 프로그램을 비단조적이라고 거부한다. 하지만 Datalog가 할 수 있는 일은 모두 처리하며, 어쩌면 그보다 더 많은 것도 처리한다.

고정점을 더 빠르게 찾는 법

위에서 빠뜨린 중요한 세부사항 하나는 fix 의 구현, 즉 R ⊇ f(R) 를 만족하는 가장 작은 집합 R 을 어떻게 찾느냐이다. 예를 들어 그래프 도달 가능성을 다시 보자.

f(R) = {start} ∪ {y | x ∈ R, (x,y) ∈ edge}

순진한 방법은 f 를 반복하는 것이다.

R₀ = ∅          = 아무것도 없음
R₁ = f(∅)       = {start}
R₂ = f(f(∅))    = start에서 간선 1개 이내의 노드들
R₃ = f(f(f(∅))) = start에서 간선 2개 이내의 노드들
...
Rᵢ = fⁱ(∅)      = start에서 간선 i-1개 이내의 노드들
...

결국 가장 멀리 도달 가능한 노드들을 찾게 되면 Rᵢ = Rᵢ₊₁ 이 되어 멈출 때까지 반복한다.

이것은 극도로 비효율적인 너비 우선 탐색인데, 중복된 일을 하기 때문이다. f(Rᵢ) 를 계산하는 데 필요한 집합 내포 {y | x ∈ Rᵢ, (x,y) ∈ edges} 를 생각해 보자. 이것은 Rᵢ 의 모든 노드를 조사한다. 따라서 전체적으로는 각 Rᵢ 의 크기들의 합만큼은 적어도 일을 하게 된다. 이제 수열 Rᵢ 가 R₀ ⊆ R₁ ⊆ R₂ ⊆ ... 처럼 단조적으로 커진다는 점을 보자. 왜냐하면 start 에서 간선 1개 이내의 노드는 간선 2개 이내에도 역시 들어가기 때문이다. 기타 등등. 따라서 어떤 노드에 이른 반복에서 도달했다면, 그 뒤의 모든 반복에서 그것을 쓸데없이 다시 조사하게 된다. 어떤 그래프에서는 이것이 이차적 폭증을 낳는다. (예를 들어 edge = {(i, i+1) | i ∈ [1..n]} 라고 하자.) 평균적으로 각 노드를 선형 횟수만큼 조사하게 되는 것이다!

해결책은 각 노드를 딱 한 번만 조사하는 것이다. 순진한 반복은 반복적으로 증가하는 n 에 대해 “최대 n 단계 안에 무엇을 추론할 수 있는가?”를 묻는다. 반순진 반복은 “n 단계 안에 무엇을 새롭게 추론할 수 있는가, 즉 그 전에는 추론할 수 없었던 것은 무엇인가?”를 묻는다. 다시 말해, 순진한 반복의 각 단계 사이의 변화, 즉 지식의 전선을 묻는 것이다. 이런 전선은 우리의 추론 함수 f 를 증분화함으로써 계산할 수 있다. 즉, 입력의 변화에 대해 출력이 어떻게 변하는지를 알아내는 것이다. 다시 말해, 이전 전선이 주어졌을 때 다음 전선은 무엇인가? 이것은 다시 우리 프로그램의 이산 미분 을 취함으로써 할 수 있는데, 그 의미는 incremental λ-calculus 에 관한 선행 연구에서 엄밀하게 다듬어져 있다. 3장에서는 이 작업을 Datafun에 적용하여, 단조적(증가하는) 변화에 대해 그것을 증분화하는 방법을 보여준다.

없어서는 안 될 사람들

내 논문에는 감사의 말이 없다. 쓰기가 어려웠기 때문이다. 실제로 누군가를 고르면 누군가를 빠뜨리게 되고, 모두를 한꺼번에 넣는 비선택은 성의 없고 지치게 느껴졌다. 그래서 쉬운 길을 택해 아무 말도 하지 않았다. 이 글에서는 아주 단호한 기준을 택했다. 이 논문을 내가 쓰지 못했을 사람들이다. 그러니 목록은 꽤 짧다.

• Neel Krishnaswami, 내 지도교수. 이 사람이 없었다면 나는 어떤 논문도, 하물며 이 논문은 더더욱 쓰지 못했을지도 모른다. 결국 Datafun이 된 더듬거림들을 격려해 주었고, 지금까지 함께한 두 편의 논문을 가능하게 했으며, 그 밖의 모든 것에도 감사한다.

• Eve/Kodowa (당시에는 Chris Granger, Rob Attorri, 그리고 Jamie Brandon)에게도 감사한다. 이들은 나에게 Datalog를 소개해 주었고, 내 꿈의 직장에서 나를 떨어뜨림으로써 내가 학계에서 계속 버티게 만들었다. Jamie가 계속 연락해 준 데에도 감사한다.

• 내 논문 심사위원들인 Achim Jung과 Jeremy Gibbons에게도 감사한다. 그들은 내가 3장의 서론을 다시 쓰도록 이끌어 범주론적 접근을 복권하게 했고, 결론(6장, “Looking Back and Forward”)을 꼭 쓰라고 insist했다.

• nwf, 최종 원고에 대한 피드백에 감사한다.

박사과정 동안 더 많은 사람들이 나를 도와주었다. 하지만 대체로 그들은 내가 어떤 논문을 쓰든지 간에 나를 지지했을 것이다. 그렇다고 그들의 도움이 덜 소중해지는 것은 아니다. 그들이 자신이 누구인지 알고 있기를 바란다.