Completeness of Relational Algebra via Cylindric Algebra

1. 연구 배경 및 문제 제기 (Problem)

• 관계 대수와 일차 논리의 관계: 관계 대수 (Relational Algebra) 는 관계형 데이터베이스를 위한 절차적 질의 언어이며, 일차 논리 (First-Order Logic) 는 선언적 질의 언어로 간주됩니다. 이론적으로 모든 관계 대수 식은 일차 논리 공식으로 변환 가능하지만, 그 역은 성립하지 않습니다. 예를 들어, ¬r(x) 와 같은 공식은 관계 대수 식으로 변환할 수 없습니다.
• 허용된 공식 (Allowed Formulas): 모든 일차 논리 공식을 관계 대수로 변환할 수는 없지만, 특정 구조적 조건을 만족하는 "허용된 공식 (Allowed Formulas)"은 관계 대수와 동치인 식으로 변환 가능합니다. 기존 연구 (VGT91) 에서 이 변환 알고리즘과 완전성 (Completeness) 정리가 증명되었습니다.
• 기존 방법의 한계: 기존 proofs 는 주로 논리적 변환에 의존했으며, 불완전하거나 모호한 정보를 다루는 일반화된 관계 모델 (Generalized Relational Models) 로의 확장에 한계가 있었습니다. 또한, 등호 (=) 를 제거하는 전처리 과정이 필요하거나 부정 (Negation) 을 논리 연결사로 온전히 다루지 못하는 경우가 있었습니다.
• 연구 목표: 원통 대수 (Cylindric Algebra) 의 성질을 활용하여 허용된 공식의 완전성을 증명하고, 이를 통해 일반화된 관계 모델 (불완전 정보, 유사성 기반 모델 등) 로 확장 가능한 새로운 증명 및 변환 알고리즘을 제시하는 것.

2. 방법론 (Methodology)

저자는 관계 대수를 원통 대수에 자연스럽게 임베딩 (Embedding) 하는 Imieliński 와 Lipski 의 결과를 기반으로 다음과 같은 방법론을 사용합니다.

• 원통 대수 (Cylindric Algebra) 활용:
  • 일차 논리의 의미론을 원통 대수의 대수적 구조 (불 대수, 원통화 연산 $C_x$, 대각선 원소 $D_{xy}$ 등) 로 재정의합니다.
  • 관계 대수 연산 (합집합, 차집합, 조인, 투영, 선택, 재명명) 을 원통 대수의 연산과 대응시킵니다 (Theorem 3.1).
• 허용된 공식의 정의 및 분석:
  • 변수의 등가성 (Equality) 과 비등가성 (Coequality) 을 정의하는 eq(φ) 와 coeq(φ) 함수를 도입하여 공식의 구조적 속성을 분석합니다.
  • 생성자 (Generator, gen(φ)) 와 공생성자 (Cogenerator, cogen(φ)) 를 정의하여 공식이 활성 도메인 (Active Domain) 내에서만 값을 가지는지 여부를 분석합니다.
• 정규화 (Normalization) 알고리즘:
  • 주어진 허용된 공식을 **정규화된 공식 (Normalized Formula)**으로 변환하는 알고리즘을 제시합니다.
  • 이 과정은 공식을 "생성자"로 제한하고, 변수 정렬 (Alignment) 을 수행하며, 이중 부정 등을 처리하여 관계 대수 식으로 직접 변환 가능한 형태로 만듭니다.
  • 변환 과정은 두 단계로 이루어집니다:
    1. 허용된 공식을 정규화된 공식으로 변환.
    2. 정규화된 공식을 관계 대수 식 (expr(φ)) 으로 변환.

3. 주요 기여 (Key Contributions)

1. 대수적 완전성 증명 (Algebraic Completeness Proof):

   • 기존 논리적 접근 대신 원통 대수 내부에서 완전성 정리를 증명했습니다. 이는 논리식과 관계 대수 식의 동치성을 대수적 연산 (원통화, 교집합 등) 을 통해 엄밀하게 보여줍니다.
   • 이 증명 기법은 불완전 정보나 값의 유사성을 다루는 일반화된 관계 모델로 쉽게 확장 가능함을 시사합니다.

2. 새로운 변환 알고리즘 제시:

   • 허용된 공식을 관계 대수 식으로 변환하는 새로운 알고리즘을 제안했습니다.
   • 부정 (Negation) 의 명확한 처리: 부정을 완전한 논리 연결사로 취급하여 허용된 공식의 정의를 더 명확하게 했습니다.
   • 등호 (Equality) 처리: 등호를 미리 제거할 필요가 없으며, 정규화 과정에서 자연스럽게 처리됩니다.
   • 구조 보존: 첫 번째 정규화 단계가 입력 공식의 구조를 보존하여 실용적인 이점을 제공합니다.

3. 정규화 이론의 정립:

   • gen(φ) 와 cogen(φ) 개념을 도입하여 공식이 활성 도메인 내에서만 정의됨을 보장하는 조건을 체계화했습니다.
   • norm(φ, ψ) 함수를 통해 허용된 공식을 정규화된 형태로 변환하고, 이 변환이 원래 공식과 의미적으로 동치임을 증명했습니다 (Theorem 6.8).

4. 주요 결과 (Results)

• 완성성 정리 (Theorem 6.8 & 6.9):
  • 모든 허용된 공식은 의미적으로 동치인 정규화된 공식을 가지며, 이는 다시 의미적으로 동치인 관계 대수 식으로 변환 가능합니다.
  • 허용된 공식은 모두 **도메인 독립적 (Domain Independent)**임을 증명했습니다. 즉, 도메인의 크기에 관계없이 동일한 결과를 반환합니다.
• 알고리즘의 정확성:
  • 제시된 정규화 알고리즘이 허용된 공식을 올바르게 변환하며, 변환된 관계 대수 식이 원래 논리식과 동일한 관계를 산출함을 Lemma 6.7 및 Theorem 6.8 을 통해 증명했습니다.
  • 예시 (관계 나눗셈, Relational Division) 를 통해 알고리즘이 복잡한 논리식을 표준 관계 대수 연산으로 변환하는 과정을 시연했습니다.

5. 의의 및 중요성 (Significance)

• 이론적 확장성: 이 연구의 가장 큰 의의는 증명 기법이 **일반화된 관계 모델 (Generalized Relational Models)**에 적용 가능하다는 점입니다. 불완전 정보 (Incomplete Information) 나 도메인 내 값의 유사성 (Similarity) 을 다루는 모델에서도 원통 대수의 일반화를 통해 유사한 완전성 결과를 도출할 수 있는 토대를 마련했습니다.
• 실용적 알고리즘: 허용된 공식을 효율적으로 관계 대수 식으로 변환하는 알고리즘을 제공함으로써, 선언적 질의 (SQL 등) 를 내부적으로 효율적으로 실행 가능한 절차적 계획으로 변환하는 데 이론적 기반을 강화했습니다.
• 논리 - 대수 통합: 일차 논리와 관계 대수 사이의 간극을 원통 대수라는 강력한 대수적 도구를 통해 메꾸었으며, 부정과 등호 처리에 있어 기존 연구보다 더 유연하고 명확한 접근법을 제시했습니다.

결론적으로, Jan Laštovicka 의 논문은 원통 대수를 매개로 하여 관계 대수의 완전성을 대수적으로 재증명하고, 이를 통해 더 넓은 범주의 데이터 모델로 확장 가능한 새로운 변환 알고리즘을 제시함으로써 데이터베이스 이론과 논리학의 중요한 연결고리를 강화한 연구입니다.