시간에서 공간으로: 고차 Datalog (Higher-Order Datalog)에서의 선형성 (Linearity)의 영향

우리는 부정 (negation)이 포함된 고차 Datalog (Higher-Order Datalog)의 한 파편 (fragment)을 고려하며, 이것이 친숙하고 중요한 선형 Datalog (Linear Datalog) 파편을 일반화한다고 주장합니다. 우리는 이 파편의 표현력 (expressive power)을 조사하여, 공간 복잡도 클래스 (space complexity classes)의 계층 구조와 긴밀한 연결 고리를 확립합니다. 특히, 모든 $k \ge 1$에 대해, 계층화된 선형 고차 Datalog$^\neg$ (Stratified Linear Higher-Order Datalog$^\neg$)의 $(k+1)$차 파편이 $(k-1)$-EXPSPACE를 포착함을 입증합니다. 이 결과는 프로그램을 선형 재귀 (linear recursion)로 제한하는 것이 해당 파편들의 표현력을 시간 (time)에서 공간 (space)으로 전환시킨다는 것을 시사하며, (계층화된) 선형 Datalog가 NL을 포착한다는 고전적인 결과를 일반화합니다. NL을 포착하기 위해 순서 가정 (ordering assumption)이 필요한 1차 논리 (first-order) 설정과 달리, 우리의 결과는 입력 데이터베이스에 대한 그러한 가정 없이도 성립합니다. 증명은 Stratified Linear Higher-Order Datalog$^\neg$ 프로그램을 사용하여 공간 제한이 있는 튜링 머신 (Turing machines)을 시뮬레이션하고, 쿼리 프로그램의 공간 효율적인 평가 (evaluation)를 제공하는 것에 기반합니다. 우리는 이와 같이 계산적으로 잘 동작하는 파편들을 식별하는 것이 고차 Datalog의 실질적인 구현을 위한 길을 닦는 데 있어 중요한 단계라고 주장합니다.