논리 프로그래밍과 그중 datalog라는 형태를 소개하고, Souffle 언어로 사실과 규칙, 관계, 재귀, 동치 관계, 타입 시스템을 통해 예제를 살펴본다.
이색적인 프로그래밍 아이디어 시리즈를 이어가며, 이번에는 논리 프로그래밍과 그중에서도 datalog로 알려진 특정 형태를 살펴보겠습니다.
Datalog는 매우 단순한 형식 체계로, 다음 두 가지만으로 구성됩니다:
Datalog는 질의 처리기에 의해 실행되며, 이 처리기는 위 두 입력이 주어졌을 때 데이터베이스와 규칙 모두로부터 함의되는 모든 사실의 인스턴스를 찾아냅니다. 예제에서는 Souffle 언어로 코딩해 보겠습니다. 이 언어의 이름은 Systematic, Ontological, Undiscovered Fact Finding Logic Engine의 약자입니다. 많은 Linux 시스템에서는 다음 명령으로 간단히 설치할 수 있습니다.
$ apt-get install souffle
Souffle는 대규모 데이터셋에 대한 복잡한 질의를 위해 설계된 미니멀한 datalog 시스템으로, 대형 코드베이스에 대한 정적 프로그램 분석 같은 맥락에서 마주치는 질의에 적합합니다. Souffle는 C++로 구현되어 있으며, C로 컴파일하는 방식으로 datalog 프로그램을 독립 실행형 실행 파일로 컴파일할 수 있습니다. 현재까지의 이러한 시스템 구현 중에서도 더 단순하면서도 매우 효율적인 편에 속하고, 특히 로직 엔진 위에 단순한 타입 시스템을 갖추고 있다는 점이 주목할 만합니다.
Datalog는 유한한 항(term)의 우주(universe) 위에서 만족 가능성이 직접 계산 가능한, 결정 가능한(decidable) 논리의 한 부분(fragment)을 인코딩합니다. 이 항들은 세 가지 종류의 표현으로 이뤄집니다. 첫째는 마침표로 끝나는 표현으로, 문법적으로 사실을 나타냅니다.
fact.
둘째는 머리(head)와 본문(body) 항이 있고 그 사이에 턴스타일(⊢) 기호가 있는 규칙입니다.
head :- body.
셋째는 데이터베이스 안에서 사실의 진릿값을 질의하는 질의 항입니다.
?- body.
이 항들의 예로는 그리스 철학자 소크라테스에 대한 “고전적” 범주적 삼단논법이 있습니다. 소크라테스는 인간이고, 모든 인간은 죽는다. 따라서 소크라테스는 죽는다는 결론을 도출할 수 있습니다.
# All men are mortal / valar morghulis
mortal(X) :- human(X).
# Socrates is a man.
human("Socrates").
# Is Socrates mortal?
?- mortal("Socrates").
Souffle 프로그램의 실행은 사실상 입력 사실을 규칙의 명세에 따라 변환하여, 도출된 출력 사실로 만드는 일련의 변환 과정입니다.
Souffle는 stdin, CSV 파일, SQLite 데이터베이스 등 다양한 소스로부터 입력 사실을 읽을 수 있습니다. 기본 입력 소스는 관계(relation)에 대한 탭 구분 파일이며, 파일의 각 행은 그 관계 안의 하나의 사실을 나타냅니다. 이는 다음 형태의 IO 입력 선언으로 지정합니다.
.decl A (n: symbol)
.input A
이는 상징 값 n에 대해 탭으로 구분된 값을 담은 A.facts 파일을 읽습니다. 하지만 명시적인 IO 파라미터를 넘겨 입력을 수정할 수도 있습니다.
.input A(IO=file, filename="fact_database.csv", delimiter=",")
.input A(IO=stdin, delimiter=",")
.input A(IO=sqlite, dbname="fact_database.db")
간단한 end-to-end 예로, 상징 입력 집합을 숫자 입력 집합과 간단한 일대일 매핑으로 연결하는 프로그램을 생각해 봅시다. 다음 규칙처럼 A에서 B로의 간단한 변환을 작성할 수 있습니다.
# Input from A.facts
.decl A (n: symbol)
.input A
# Output to B.csv
.decl B (n: number)
B(0) :- A("Hello").
B(1) :- A("World").
.output B
이 프로그램은 A.facts의 입력 사실을 읽어들이고, 다음 명령으로 Souffle를 실행하면(당연하게도) B.csv를 출력합니다.
$ souffle hello.dl
출력은 hello.dl의 규칙에 따라 A를 B에 매칭한 결과입니다.
| A | B |
|---|---|
| Hello | 0 |
| World | 1 |
Relations
datalog 내부의 논리는 관계(relation)로 지정되며, 관계는 타입이 지정된 변수들의 순서 있는 튜플로서 여러 양(quantities)을 연관시킵니다. 예를 들어 이름 있는 엔티티들의 집합(심벌로 표현됨)이 있다면, 각 엔티티에 속성을 매핑하는 관계를 사실로 부여할 수 있습니다.
.decl Human(x : symbol)
.decl Klingon(x : symbol)
.decl Android(x : symbol)
Human("Picard").
Human("Riker").
Klingon("Worf").
Android("Data").
각 변수는 로 특정 타입이 주어지며, 여기서 type은 다음 내장 타입 중 하나입니다.
관계는 여러 인자를 가질 수 있으며, 해당 관계 위의 규칙에 따라 심벌들의 모음에 속성을 부여할 수 있습니다.
.decl Rank(x:symbol, y:symbol)
.decl Peers(x:symbol, y:symbol)
Rank("Captain", "Picard").
Rank("Officer", "Riker").
Rank("Officer", "Worf").
Rank("Officer", "Data").
이 관계들 위의 규칙은 절(clause)로 정의됩니다. 다음은 (x,y) 쌍이 B 관계에 속한다면 A 관계에도 속한다는 뜻으로 읽을 수 있습니다.
A(x,y) :- B(x,y).
Souffle에서의 절은 논리학에서 혼 절(Horn clause)로 알려져 있습니다. 혼 절은 여러 하위 항이 논리곱(conjunction) (프로그래밍에서의 논리 AND)으로 결합되어 어떤 명제 u를 함의하는 형태로 구성됩니다. 수학적으로 다음과 같이 읽을 수 있습니다.
a와 b와 …와 z가 모두 성립하면, u도 성립한다
위 형태는 함의형(implicative form)으로 알려져 있습니다. 논리적으로 이는 논리합(disjunction) (프로그래밍에서의 논리 OR)과 부정(negation) (프로그래밍에서의 논리 NOT)으로 표현한 문장과 동치입니다.
Datalog 표기에서는 이 혼 절을 다음 문법으로 씁니다.
u :- a, c, ..., z.
절에서, 결합된 표현 안에 등장하는 자유 변수는 암묵적으로 전칭 양화(universally quantified)됩니다. 즉, 어떤 영역(domain)에서 그 변수의 모든 치환에 대해 성립해야 합니다(이는 로 표기). 이때 영역은 주어진 타입의 거주자들의 집합입니다(예: symbol, unsigned 등).
따라서 위 datalog 표현
A(x,y) :- B(x,y).
은 혼 절과 동치입니다.
예를 들어, 클링온과 인간은 둘 다 음식을 먹지만, 안드로이드는 (명백히) 먹지 않는다고 해 봅시다. 다음 규칙을 symbol 타입 변수 X에 대해 작성할 수 있습니다.
.decl Eats(x:symbol)
Eats(X) :- Human(X).
Eats(X) :- Klingon(X).
.output Eats
이는 종(species)에 대한 제약을 고려하여, 범위에 포함된 심벌들에 대한 입력 사실 집합으로부터 다음 출력을 만듭니다.
| Eats |
|---|
| Riker |
| Picard |
| Worf |
항은 부정될 수도 있습니다. 예를 들어, 먹는 장교(officer)들을 모두 열거하고 싶다면, 안드로이드를 제외하는 다음 규칙을 쓸 수 있습니다.
InvitedToDinner(X) :- Rank("Officer", X), !Android(X).
| InvitedToDinner |
|---|
| Riker |
| Worf |
더 복잡한 규칙은 쉼표로 구분된 여러 항들로 구성될 수 있으며, 이 항들은 모두 참으로 평가되어야 합니다. 예를 들어 두 장교가 같은 계급을 가지면서 동일 인물이 아니라면 서로 동료(peers)라고 합시다. 이 관계에서 계급의 동등성을 테스트하기 위해 중간 변수 Z를 사용합니다.
.decl Peers(x:symbol, y:symbol)
Peers(X, Y) :- Rank(Z, X), Rank(Z, Y), X != Y.
| Peers |
|---|
| Riker |
| Worf |
| Riker |
| Data |
| Worf |
| Data |
| Riker |
| Worf |
규칙은 재귀적일 수도 있습니다. 예를 들어, 어떤 사실 집합이 주어졌을 때 1단계 친구 관계를 모두 찾는 질의를 작성하고 싶다면, 다음과 같은 재귀 정의를 쓸 수 있습니다.
.decl Friend(x:symbol, y:symbol)
.decl FriendOfFriend(x:symbol, y:symbol)
FriendOfFriend(X, Y) :- Friend(X, Z), FriendOfFriend(Z, Y).
| FriendOfFriend |
|---|
| Riker |
| Worf |
관계의 중요한 한 부류는 동치 관계(equivalence relation)입니다. 이는 두 항 사이의 관계로서 추가적인 제약 집합(반사성, 대칭성, 추이성)을 만족합니다. 이런 형태의 관계는 대수학에서 등호 기호가 다뤄지는 방식과 비슷하게 동작합니다.
.decl equivalence(x:number, y:number)
equivalence(a, b) :- R(a), R(b).
// reflexivity
equivalence(a, a) :- equivalence(a, _).
// symmetry
equivalence(a, b) :- equivalence(b, a).
// transitivity
equivalence(a, c) :- equivalence(a, b), equivalence(b, c).
이 관계 구현에서 데이터와 중간 도출 결과는 공통 B-트리 자료구조에 저장됩니다. 하지만 특정 사용 사례에 대해, 명시적인 인자를 넘겨 분리 집합(disjoint-set) 또는 trie 자료구조를 강제하도록 수정할 수 있습니다.
.decl A(x : number, y : number) eqrel // Disjoint-set
.decl B(x : number, y : symbol) btree // B-tree
.decl C(x : number, y : symbol) brie // Dense trie
정수 계열 타입(number, unsigned, float)을 다룰 때 산술 표현식은 기대한 대로 동작하며, 패턴 매칭도 가능합니다. 예를 들어 피보나치 함수를 자기 자신에 대한 관계로 다음처럼 쓸 수 있습니다.
fib(0, 0).
fib(1, 1).
fib(n+1, x+y) :- fib(n, x), fib(n-1, y), n < 15.
Souffle에는 절 표현에서 양화되는 변수들의 타입을 추적하는 데 사용할 수 있는 제한적인 타입 시스템이 있습니다. 예를 들어 한 변수가 동시에 symbol과 unsigned 정수를 담을 수는 없습니다. 다만 언어의 기반 타입 위에 사용자 정의 타입 동의어(synonym)를 정의하여, 심벌과 수치량을 의미적으로 구분할 수는 있습니다. 예를 들면 다음과 같습니다.
.type Person <: symbol
.type Food <: symbol
.decl Eats(x : Person, y : Food)
.decl Dinner(x : Person, y : Food)
Dinner(x, y) :- Eats(x, y). // Well-typed
Dinner(x, y) :- Eats(y, x). // Not well-typed, Person != Food
동의어의 바탕 타입이 동등하기만 하다면, 타입 동의어의 합집합(union)도 허용됩니다.
.type A <: number
.type B <: number
.type C = A | B // Either in A or B
또한 이 언어는 합(sum) 타입과 곱(product) 타입도 정의할 수 있어, 절에서 항으로 옵션과 레코드를 모두 표현할 수 있습니다.
.type Sum = A { x: number } | B { x: symbol }
.type Prod = C { x: number, y : symbol }
예를 들어, 머리(head) 원소와 꼬리(tail) 원소를 모두 갖는 곱 타입으로 연결 리스트(또는 cons 리스트)를 만들 수 있습니다.
// Linked list
.type List = [ head : number, tail : List ]
.decl MyList(x : List)
MyList( [1, [2, nil]] ).
논리 프로그래밍은 추상적인 프로그램 의미론을 표현하는 매우 자연스러운 방법이며, Souffle 같은 도구를 사용하면 다른 정적 분석 애플리케이션에 내장할 수 있는 훌륭한 로직 엔진을 얻을 수 있습니다. 이를 통해 코드에 대한 사실을 수집하고, 코드 구성과 사용에 대한 함의를 도출할 수 있습니다. 이는 강력한 기법이며, 미래의 정적 분석 도구들은 앞으로 코드에 대해 추론하고 합성하는 완전히 새로운 방식들을 만들어낼 것입니다.