Ranked MSO-enumeration over compressed words

기술 요약: 압축된 단어에 대한 순위가 지정된 MSO 열거

문제 정의
본 논문은 압축된 형식으로 제공되는 문자열에 대해 고정된 단일 논리식 제2차(Monadic Second-Order, MSO) 쿼리의 해답을 열거하는 문제를 다룬다. 입력 문자열 $w$는 하나의 문자열만을 생성하는 문맥 자유 문법인 직선형 프로그램(Straight-Line Program, SLP)에 의해 주어진다. 목표는 $w$ 내에서 고정된 MSO 공식 $\Phi(x_1, \dots, x_k)$를 만족하는 위치들의 튜플 $(a_1, \dots, a_k)$를 모두 계산하는 것이다.

이 연구의 핵심적인 제약 조건은 **순위가 지정된 열거(ranked enumeration)**이다. 출력 순서가 불투명한 표준 열거 알고리즘과 달리, 순위가 지정된 열거는 사용자 정의에 따라 정해진 특정 순서(예: 위치 튜플에 대한 사전식 순서)로 출력되는 튜플을 요구한다. 이러한 알고리즘의 효율성 지표는 선형 전처리 시간(SLP의 크기 $|G|$에 비례하는 시간)과 그 뒤를 잇는 상수 지연 시간(연속된 튜플을 출력하는 사이의 시간에 대한 상수 상한)이다.

이 연구 이전에는 압축되지 않은 문자열과 트리에서는 MSO 쿼리에 대한 순위 지정 열거가 알려져 있었으나, 압축된 데이터에 대해서는 결과가 존재하지 않았다. 또한, 압축된 문자열에 대한 기존의 열거 결과(예: [29])는 출력 선형 지연(output-linear delay)만을 달야성했을 뿐 순위 지정 열거를 지원하지 못했다.

방법론
해결책은 세 가지 주요 기술적 구성 요소를 결합한다:

1. 인수 분해 트리(Factorization Trees)와 Simon SLP:
   핵심적인 구조적 도구는 인수 분해 트리이다. 이는 유한 모노이드로의 준동형(morphism)에 대한 단어의 파스 트리(parse tree)이며, 자식이 3개 이상인 노드는 동일한 멱등 원소(idempotent element)로 평가된다. Simon의 정리는 이러한 트리의 높이가 모노이드 크기에 의존하는 상수로 제한됨을 보장한다.
   본 논문은 **Simon SLP (SSLP)**라는 개념을 도입한다: 이는 생성되는 단어의 인수 분해 트리와 구조적으로 호환되는 SLP이다. 저자들은 임의의 SLP가 선형 시간에 동등한 SSLP로 변환될 수 있음을 증명한다(정리 3.1). 이 변환은 인수 분해 트리를 생성하는 비결정적 트랜스듀서를 구축하고, 트리의 계층 구조를 반영하도록 문법을 재구성하여 SLP의 "멱등 축소 깊이(idempotent-contracted depth)"가 상수($3|M|$)로 제한되도록 하는 과정을 포함한다.

2. 압축된 문자열에서의 상수 시간 순회:
   압축된 문자열을 효율적으로 탐색하기 위해, 본 논문은 [26]의 양방향 상수 시간 순회 기법을 활용하고 확장한다. 저자들은 압축된 경로(SLP의 DAG 내에서 좌/우 이동을 나타내는 트리플의 시퀀스)를 정의하고, "활성" 경로의 상수 개수를 저장하는 동적 데이터 구조(이진 트리 $B$)를 유지한다.
   결정적으로, 저자들은 압축된 표현 내의 경로가 주어졌을 때 그 사전식 후속자 또는 선행자를 상수 시간에 계산하는 right 및 left 절차를 정의한다. 이는 순회 트리에서 에지를 분할하고 특정 SLP 부분(e-parts) 내의 "멱등 축소된" 하위 경로를 관리하는 과정을 포함한다.

3. MSO 해석 및 후속자 계산:
   열거 알고리즘은 다항 정규 함수(polyregular function)(또는 더 일반적으로, MSO-문자열-대-문자열 해석)의 이미지를 계산하는 것으로 프레임화된다. 알고리즘은 현재 튜플의 "후속자"를 MSO로 정의 가능한 선형 순서에 따라 반복적으로 계산한다.
   증명 과정은 MSO 공식을 비결정적 유한 오토마타(NFA)로 변환하고 유한 모노이드 $M$을 도출하는 것을 포함한다. 인수 분해 트리(또는 동등한 SSLP)의 노드들에 대한 모노이드 원소를 미리 계산함으로써, 알고리즘은 열거 시퀀스의 다음 위치를 상수 시간에 결정할 수 있다. 현재 위치들 사이의 전이를 처리하기 위해, 구간 사이의 모노이드 원소를 분석하고 인수 분해 트리의 구조를 사용하여 문자열을 압축 해제하지 않고도 다음 유효한 위치로 이동한다.

주요 기여 및 결과

• 주요 정리 (정리 5.1): 고정된 $k$개의 자유 1차 변수를 가진 MSO 공식과 $k$-튜플에 대한 MSO 정의 선형 순서에 대하여, SLP 압축 문자열 상의 쿼리 해답은 선형 전처리 시간($O(|G|)$)과 상수 지연 시간으로 열거될 수 있다. 이는 압축된 데이터에 대한 순위 지정 열거에서 최초의 결과이다.
• 다항 정규 함수에 대한 따름정리 (따름정리 5.3): 이 결과는 다항 정규 문자열-대-문자열 함수로 일반화된다. 고정된 다항 정규 함수 $f$와 $w$를 생성하는 SLP $G$에 대하여, $f(w)$의 심볼들을 왼쪽에서 오른쪽으로 선형 전처리 및 상수 지연 시간으로 열거할 수 있다. 이는 다항 정규 함수가 일반적으로 압축 크기를 보존하지 않음에도 불구하고, 압축되지 않은 입력을 가정했던 Bojanczyk [8]의 결과를 압축된 환경으로 확장한 것이다.
• Successor-MSO에 대한 따름정리 (따름정리 5.5): 이 결과는 다항 정규 함수보다 엄격히 더 큰 클래스인 successor-MSO 문자열-대-문자열 해석에 대해서도 성립한다.
• 기술적 기여 (Simon SLPs): 본 논문은 모든 SLP가 선형 시간에 Simon SLP로 변환될 수 있음을 확립한다. 이는 인수 분해 트리를 문법 압축 환경에서도 사용할 수 있게 만드는 것으로, 독립적인 가치가 있는 기여로 언급된다.

의의 및 주장
본 논문은 압축된 데이터에 대한 순위 지정 열거의 방향으로 향하는 "첫 걸음"을 내디뎠다고 주장한다. 저자들은 기존의 압축된 열거 알고리즘(예: [29])은 출력 순서를 제어할 수 없었고, 기존의 순위 지정 열거 알고리즘(예: [2, 12, 19])은 압축된 입력을 다룰 수 없었다는 점을 지적하며 이 간극을 해결한다.

저자들은 자신들의 접근 방식이 인수 분해 트리의 특정한 구조와 SLP 상에서의 상수 시간 탐색 능력에 의존함을 강조한다. 또한 다음과 같은 한계를 명시한다:

• 현재 결과는 자유 1차 변수를 가진 쿼리에만 적용된다. 자유 집합 변수(이는 상수 지연이 아닌 출력 선형 지연을 요구함)를 다루는 것은 열린 문제인데, 이는 인수 분해 트리 접근 방식이 현재 집합 변수로 확장되지 않기 때문이다.
• 본 연구는 현재 문자열에 국한되어 있다. 인수 분해 트리 기술과 포레스트 SLP 순회 기술의 결합이 선행되어야 하는 포레스트(forests)로의 확장은 향후 과제로 남겨두었다.
• 순위 지정은 MSO 정의 선형 순서로 제한된다. 이 모델과 비용 트랜스듀서를 사용하는 가중치 기반 순위 사이의 관계는 아직 불분명하다.

요약하자면, 본 논문은 고도로 압축된 데이터에 대한 효율적이고 정렬된 쿼리 처리를 위한 이론적 토대를 제공하며, 출력 순서가 MSO로 정의 가능하다면 SLP 상의 MSO 쿼리에 대해 "골드 스탠다드"인 선형 전처리 및 상수 지연 달성이 가능함을 입증한다.