A Complete Propositional Dynamic Logic for Regular Expressions with Lookahead

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

**전통적인 정규 표현식(Regular Expressions, RE)**은 결합(concatenation), 합집합(union), 클레이니 스타(Kleene star) 연산자로 구성되며, 이들의 언어적 동등성(language equivalence)을 다루는 '클레이니 대수(Kleene Algebra)'라는 완전한 대수적 체계가 존재합니다.

그러나 현대의 실용적인 정규 표현식 엔진(예: PCRE)은 **Lookahead(전방 탐색)**와 같은 확장 연산자를 포함합니다. Lookahead가 포함된 정규 표현식(REwLA)은 다음과 같은 복잡한 특성을 가집니다:

• 대치 불변성(Substitution-closedness)의 결여: REwLA의 언어적 동등성은 변수를 다른 표현식으로 치환했을 때 유지되지 않을 수 있습니다. (예: ((?!ab)(a|b))*와 b*a*는 동일한 언어를 갖지만, b를 a로 치환하면 결과가 달라짐)
• 완전한 공리계의 부재: 기존 연구에서 일부 대수적 성질은 조사되었으나, REwLA의 동등성을 모두 포괄하는 완전한 힐베르트 스타일(Hilbert-style)의 유한 공리계는 아직 제시되지 않았습니다.

본 논문은 REwLA의 언어적 동등성과, 이를 포함하면서도 대치 불변성을 갖는 **가장 큰 대치 불변 동등성(largest substitution-closed equivalence)**을 모두 설명할 수 있는 완전한 논리 체계를 구축하는 것을 목표로 합니다.

2. 연구 방법론 (Methodology)

저자는 REwLA의 복잡성을 다루기 위해 **명제 동적 논리(Propositional Dynamic Logic, PDL)**를 확장하는 전략을 사용합니다.

1. PDL의 확장 ($PDL_{REwLA+}$):
   기존 PDL에 두 가지 새로운 연산자를 도입하여 유한 선형 순서(finite linear orders) 상의 관계를 제어합니다.

   • $\cdot \cap 1$ (Identity restriction): 관계를 항등 관계(identity relation)로 제한.
   • $\cdot \cap \overline{1}$ (Complement of identity restriction): 항등 관계의 보집합으로 제한.
     이 연산자들을 통해 관계를 '항등 부분(identity-part)'과 '항등이 없는 부분(identity-free-part)'으로 분해할 수 있습니다.

2. 완전성 증명을 위한 환원(Reduction) 전략:
   직접적인 증명이 어렵기 때문에, 다음과 같은 단계적 환원 방식을 채택합니다.

   • 단계 1: $PDL_{REwLA+}$의 완전성을 증명하기 위해, 항등 관계가 없는 변형된 PDL($PDL^-$)로 문제를 환원합니다.
   • 단계 2: $PDL^-$를 유한 엄격 선형 순서(finite strict linear orders) 상의 논리로 정의하고, 여기에 **Löb의 공리(Löb's axiom)**를 적용하여 완전성을 증명합니다.
   • 단계 3: REwLA의 표준 동등성과 대치 불변 동등성을 $PDL_{REwLA+}$의 이론으로 임베딩(embedding)하여 최종적인 완전성을 도출합니다.

3. 주요 기여 (Key Contributions)

• 완전한 공리계 제시: REwLA의 두 가지 핵심 동등성(표준 언어 동등성 및 대치 불변 동등성)을 모두 포괄하는 유한한 힐베르트 스타일 공리계를 최초로 제시하였습니다.
• 새로운 논리 프레임워크 구축: 항등 관계 제한 연산자를 포함한 확장된 PDL($PDL_{REwLA+}$)을 도입하여, 복잡한 정규 표현식의 관계론적 의미론을 체계적으로 다룰 수 있게 했습니다.
• 복잡도 분석: 제안된 논리 체계가 REwLA의 계산 복잡도와 동일함을 증명하여, 논리적 추론이 실용적인 계산 범위를 벗어나지 않음을 보였습니다.

4. 연구 결과 (Results)

1. 완전성 정리 (Completeness Theorems):
   • 정리 3.3: $PDL_{REwLA+}$는 유한 선형 순서 상의 대치 불변 동등성에 대해 완전합니다.
   • 정리 7.2: 추가적인 결정론적(deterministic) 공리를 포함한 시스템은 REwLA의 표준 매칭 언어 동등성에 대해 완전합니다.
2. 계산 복잡도 (Computational Complexity):
   • 대치 불변 동등성 문제: ExpTime-complete임을 증명하였습니다.
   • 표준 언어 동등성 문제: PSpace-complete임을 증명하였습니다.
     이는 확장된 PDL의 이론적 복잡도가 REwLA의 실제 복잡도와 일치함을 의미합니다.

5. 연구의 의의 (Significance)

본 연구는 이론적 측면과 실용적 측면 모두에서 중요한 의미를 갖습니다.

• 이론적 측면: 정규 표현식의 확장(Lookahead)이 가져오는 대수적 불연속성(대치 불변성 상실) 문제를 PDL이라는 강력한 논리적 도구를 통해 해결하였습니다. 특히, Löb의 공리를 활용하여 유한 구조에서의 완전성을 확보한 접근 방식은 논리학 및 이론 컴퓨터 과학 분야에 기여하는 바가 큽니다.
• 실용적 측면: 정규 표현식 최적화(Optimization)는 표현식의 길이를 줄이거나 매칭 알고리즘의 효율성을 높이기 위해 필수적입니다. 본 논문에서 제시한 완전한 공리계는 **"두 정규 표현식이 논리적으로 동일한가?"**를 판별하는 자동화된 도구(Automated Theorem Prover)를 설계할 수 있는 수학적 토대를 제공합니다.