이색적인 프로그래밍 아이디어, 4부 (Datalog)

2016년 3월 4일 · 태그: fp, logic-programming · 원문 · 한국어 번역(원문에서 변경됨)

이색적인 프로그래밍 아이디어 시리즈를 이어서, 이번에는 논리 프로그래밍이라는 주제와 그 특정한 형태인 datalog를 살펴보겠습니다.

• 1주차 - 모듈 시스템
• 2주차 - 항 재작성
• 3주차 - 이펙트 시스템
• 4주차 - Datalog

Datalog는 매우 단순한 형식 체계로, 단 두 가지로만 구성됩니다:

1. 사실(fact)들의 데이터베이스
2. 기존 사실로부터 새로운 사실을 도출하기 위한 규칙들의 집합

Datalog는 질의 처리기에 의해 실행되며, 질의 처리기는 이 두 입력이 주어지면 데이터베이스와 규칙 양쪽에 의해 함축되는 모든 사실의 인스턴스를 찾아냅니다. 예제는 Souffle 언어로 작성하겠습니다. 이 언어의 이름은 Systematic, Ontological, Undiscovered Fact Finding Logic Engine의 약자입니다. 많은 Linux 시스템에서 다음 명령으로 간단히 설치할 수 있습니다:

$ apt-get install souffle

Souffle는 대규모 코드베이스에 대한 정적 프로그램 분석을 수행하는 맥락에서 마주치는 것과 같은, 대규모 데이터 집합에 대한 복잡한 질의를 위해 설계된 미니멀리스트 datalog 시스템입니다. Souffle는 C++로 구현되어 있으며, C로의 컴파일을 통해 datalog 프로그램을 독립 실행 파일로 컴파일할 수 있습니다. 이는 현재까지 이러한 시스템 중 가장 단순하고 효율적인 구현 중 하나이며, 특히 논리 엔진 위에 단순한 타입 시스템을 갖추고 있습니다.

Datalog는 항(term)들의 유한한 유니버스 위에서 충족 여부를 직접 계산할 수 있는, 결정 가능한 논리의 일부분을 인코딩합니다. 이 항들은 세 부류의 표현식으로 구성됩니다. 사실은 구문적으로 마침표가 뒤에 붙은 표현식으로 나타냅니다.

fact.

규칙은 머리 항과 몸체 항 사이에 턴스타일(⊢) 기호를 두어 나타냅니다.

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 데이터베이스를 비롯한 다양한 소스에서 입력 사실을 읽을 수 있습니다. 기본 입력 소스는 관계에 대한 탭으로 구분된 파일이며, 파일의 각 행은 그 관계의 사실 하나를 나타냅니다. 이는 다음 형태의 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")

간단한 예제

간단한 처음부터 끝까지의 예제로는 단순한 일대일 대응을 통해 기호 입력 집합을 숫자 입력 집합과 연관시키는 프로그램을 들 수 있습니다. 이 간단한 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의 입력 사실을 읽어 B.csv를 출력하며, 다음 명령으로 Souffle를 실행하면 B.csv는 예상대로 다음과 같은 모습이 됩니다.

$ souffle hello.dl

출력은 hello.dl의 규칙에 따라 A를 B에 대응시킵니다.

관계 Datalog 내부의 논리는 관계(relation)로 지정되며, 관계는 양들을 서로 관련짓는 타입이 지정된 변수들의 순서 있는 튜플입니다. 예를 들어 (심볼로 표현된) 이름 있는 개체들의 집합이 있다면, 각 개체에 속성을 대응시키는 관계를 사실(fact)로 부여할 수 있습니다.

.decl Human(x : symbol)
.decl Klingon(x : symbol)
.decl Android(x : symbol)

Human("Picard").
Human("Riker").
Klingon("Worf").
Android("Data").

각 변수에는 var : type으로 표시되는 특정 타입이 주어지며, 여기서 type은 다음 내장 타입 중 하나입니다.

• symbol - 문자열로 표현되는 심볼 양입니다.
• number - 부호 있는 정수
• unsigned - 부호 없는 정수
• float - 부동소수점 값

관계는 여러 인자를 받을 수 있으며, 이 인자들은 해당 관계에 대한 규칙에 따라 심볼들의 모음에 속성을 부여합니다.

.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)로 알려져 있습니다. 혼 절은 논리곱(∧)(프로그래밍에서의 논리 AND)으로 결합된 하위 항들로 구성되며, 이것이 명제 u를 함의합니다. 다음 명제는 수학적으로 다음과 같이 읽을 수 있습니다.

if a and b and … and z all hold, then also u holds

$$u\leftarrow a\wedge b\wedge \dots \wedge z$$

위의 형태를 함의 형태(implicative form)라고 합니다. 논리적으로 이는 논리합(∨)(프로그래밍에서의 논리 OR)과 부정(¬)(프로그래밍에서의 논리 NOT)으로 쓰인 명제와 동치입니다.

$$\neg a\vee \neg b\vee \dots \vee z$$

Datalog 표기법에서는 이 혼 절을 다음 구문으로 작성합니다.

u :- a, c, ..., z.

절에서 결합된 식 내부에 나타나는 자유 변수는 암묵적으로 전칭 양화됩니다. 즉, 정의역 안에서 해당 변수의 모든(∀로 표기) 대입에 대해 성립해야 합니다. 이 경우 정의역은 주어진 타입(즉 symbol, unsigned 등)에 속하는 원소들의 집합입니다.

따라서 위의 Datalog 식은

A(x,y) :- B(x,y).

다음 혼 절과 동치입니다.

$$\forall x.\forall y.\neg B(x,y)\vee A(x,y)$$

예를 들어 클링온과 인간은 모두 음식을 먹지만, 안드로이드는 당연히 먹지 않는다는 것을 우리는 알고 있습니다. symbol 타입의 변수 항 X에 대해 다음 규칙을 작성합니다.

.decl Eats(x:symbol)

Eats(X) :- Human(X).
Eats(X) :- Klingon(X).
.output Eats

이 규칙은 종족에 대한 제약 조건이 주어졌을 때, 범위 내 심볼들에 관해 주어진 입력 사실 집합으로부터 다음 출력을 생성합니다.

항(term)은 부정할 수도 있습니다. 예를 들어 식사를 하는 모든 장교를 열거하고 싶다면, 안드로이드를 제외하는 다음 규칙을 작성할 수 있습니다.

InvitedToDinner(X) :- Rank("Officer", X), !Android(X).

더 복잡한 규칙은 쉼표로 구분된 여러 항으로 이루어질 수 있으며, 이 항들은 모두 참으로 평가되어야 합니다. 예를 들어 두 장교가 같은 계급이고 동일 인물이 아니라면 이 둘은 동료입니다. 이 관계에서는 계급이 같은지 검사하기 위해 중간 변수 Z를 사용합니다.

.decl Peers(x:symbol, y:symbol)
Peers(X, Y) :- Rank(Z, X), Rank(Z, Y),  X != Y.

규칙은 재귀적일 수도 있습니다. 예를 들어 주어진 사실 집합에서 1촌 친구 관계를 모두 찾는 질의를 작성하고 싶다면, 다음과 같은 재귀적 정의를 작성할 수 있습니다.

.decl Friend(x:symbol, y:symbol)
.decl FriendOfFriend(x:symbol, y:symbol)

FriendOfFriend(X, Y) :- Friend(X, Z), FriendOfFriend(Z, Y).

관계 중 중요한 부류로 동치 관계가 있습니다. 동치 관계는 두 항 사이의 관계 중에서 반사성, 대칭성, 추이성이라는 추가 제약 조건을 만족하는 관계입니다. 이런 형태의 관계는 대수학에서 등호를 다루는 방식과 비슷하게 동작합니다.

$$a=a$$

$$a=b\Rightarrow b=a$$

$$a=c,b=c\Rightarrow a=c$$

.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에는 절 표현식에서 한정된 변수의 타입을 추적하는 데 사용할 수 있는 제한적인 타입 시스템이 있습니다. 예를 들어 심볼과 부호 없는 정수를 동시에 담는 변수는 만들 수 없습니다. 그러나 언어의 기본 타입 위에 사용자 정의 타입 동의어를 정의할 수 있으며, 이를 통해 사용자가 정의한 서로 다른 종류의 심볼과 수치량을 의미적으로 구별할 수 있습니다. 예를 들면 다음과 같습니다.

.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

동의어들의 기반 타입이 같다면 타입 동의어의 합집합도 허용됩니다.

.type A <: number
.type B <: number
.type C = A | B    // Either in A or B
The language also has the ability to define both sum and product types which let us both options and records as terms in our clauses.

.type Sum = A { x: number } | B { x: symbol }
.type Prod = C { x: number, y : symbol }
For example we could build a linked list (or cons list) out of a product type which has both a head element and a tail element.

// Linked list
.type List = [ head : number, tail : List ]
.decl MyList(x : List)

MyList( [1, [2, nil]] ).

논리 프로그래밍은 추상적인 프로그램 의미론을 표현하는 매우 자연스러운 방법입니다. Souffle 같은 도구는 다른 정적 분석 애플리케이션에 내장할 수 있는 훌륭한 논리 엔진을 제공합니다. 이 엔진으로 코드에 관한 사실을 수집하고, 코드가 어떻게 구성되고 사용되는지에 관한 함의를 추론할 수 있습니다. 이는 강력한 기법이며, 앞으로의 정적 분석 도구는 코드를 추론하고 합성하는 완전히 새로운 방법을 만들어 낼 것입니다.

외부 참고 자료

• Souffle 언어 레퍼런스
• SWI-Prolog 온라인
• Z3의 μZ
• Tool Talk: Souffle
• Datalog을 이용한 도메인 모델링