Non-Termination of Logic Programs Using Patterns

기술 요약: 패턴을 이용한 논리 프로그램의 비종료성(Non-Termination)

문제 정의
본 논문은 논리 프로그램(Logic Programs, LPs)의 비종료성을 자동으로 탐지하는 문제를 다룬다. 기존 연구의 상당 부분은 루프(무한히 반복될 수 있는 유한한 리라이트 시퀀스)를 탐지하는 데 집중하고 있으나, 본 연구는 '비루핑 비종료성(non-looping non-termination)'을 목표로 한다. 이는 어떠한 루프도 포함하지 않는 무한한 리라이트 시퀀스로, 본질적으로 비주기적이며 탐지가 매우 어렵다. 저자는 이러한 시퀀스가 단순한 논리 프로그램에서도 발생할 수 있음을 지적하며, 표준적인 루프 탐지 방법들은 이를 식별하는 데 실패하는 경우가 많다고 언급한다. 연구의 동기는 두 가지이다. 이론적으로는 놀라운 형태의 무한 시퀀스를 연구하는 것과, 실용적으로는 프로그래머가 무한 루프에 빠지는 쿼리를 식별하도록 돕는 것이다.

방법론
저자는 Emmes 등(2012)이 용어 리라이팅(term rewriting) 분야에서 도입한 접근 방식을 논리 프로그래밍 영역으로 적응시킨다. 핵심 방법론은 잠재적으로 무한한 유한 리라이트 시퀀스의 집합을 기술하는 "패턴(patterns)"을 생성하는 새로운 언폴딩(unfolding) 기법을 정의하는 것이다.

1. 패턴 정의:

   • 패턴 대입(Pattern Substitutions): 대입 쌍 $\theta = (\sigma, \mu)$로 정의되며, $\sigma \star \mu$로 표기된다. 이는 대입 집합 $\{\theta(n) = \sigma^n\mu \mid n \in \mathbb{N}\}$을 기술한다.
   • 패턴 용어(Pattern Terms): 쌍 $(s, \theta)$로 정의되며, 집합 $\{s\theta(n) \mid n \in \mathbb{N}\}$을 기술한다.
   • 패턴 규칙(Pattern Rules): 패턴 용어의 쌍 $(p, q)$로 정의되며, 이진 규칙 집합 $\{(p(n), q(n)) \mid n \in \mathbb{N}\}$을 기술한다.

2. 정확성 및 언폴딩:

   • 패턴 규칙이 프로그램 $P$에 대해 **정확(correct)**하다는 것은, 해당 규칙이 기술하는 규칙의 집합이 $P$의 이진 언폴딩($binunf(P)$)의 부분집합임을 의미한다.
   • 저자는 프로그램 $P$와 올바른 패턴 규칙의 기저 집합 $B$로부터 패턴 규칙을 계산하는 새로운 언폴딩 연산자 $T^\pi_{P,B}$를 도입한다. 이 연산자는 패턴 용어에 대한 유니피케이션(unification) 알고리즘을 사용하여 규칙을 결합하며, 이를 통해 전통적인 이진 언폴딩보다 더 빠르게 프로그램을 "언폴딩"하여 $binunf(P)$의 무한한 부분집합을 유한한 표현으로 포착한다.

3. 단순 패턴 및 유니피케이션:

   • 이 접근 방식을 자동화하기 위해, 저자는 단항 컨텍스트(unary contexts)를 포함하는 특정 구조를 따르는 대입을 사용하는 **단순 패턴 용어(simple pattern terms)**로 도메인을 제한한다.
   • 단순 용어에 대한 유니피케이션 알고리즘이 제공된다. 이 알고리즘은 단순 패턴 용어를 특수 시그니처 $\Upsilon$(반복되는 임베딩을 나타내는 단항 심볼 $c_{a,b}$ 사용) 상의 용어로 매핑하고, 고전적인 유니피케이션 알고리즘(예: Robinson, Martelli-Montanari)을 적용한다.
     본 알고리즘은 부분적 정확성(partially correct)이 증명되었다. 즉, 성공적으로 종료될 경우 입력된 패턴 시퀀스에 대한 가장 일반적인 유니파이어(mgu)를 생성한다.

4. 비종료 기준:

   • 일반 기준 (정리 3): Emmes 등의 연구를 채택한 것으로, 만약 패턴 언폴딩에 $(u \star \sigma \star \mu, u\sigma^a \star \sigma^b\sigma' \star \mu\mu')$ 형태의 규칙(여기서 $\sigma'$는 $\sigma$ 및 $\mu$와 교환 가능)이 포함되어 있다면 무한 체인이 존재함을 명시한다.
   • 특수 기준 (정리 5): 특수 패턴 규칙(단순 규칙의 하위 집합)에 대해 더 쉽게 검사 가능한 조건이다. 언폴딩 내에 그러한 규칙이 존재하면, 해당 규칙의 좌측 항(left-hand side)의 특정 인스턴스들로부터 무한 체인이 존재함이 증명된다.

주요 기여
본 논문의 주요 기여는 다음과 같이 네 가지이다:

1. 새로운 언폴딩 기법: 논리 프로그래밍을 위한 올바른 패턴 규칙을 생성하는 방법을 제시하며, 이는 용어 리라이팅에서 사용되는 9개의 추론 규칙보다 더 간결한 표현을 제공하고 복잡한 적용 전략의 필요성을 제거한다.
2. 단순 패턴 용어 및 유니피케이션: 제한된 형태의 패턴 용어("단순")를 정의하고 그에 대응하는 올바름이 증명된 유니피케이션 알고리즘을 제시한다.
3. 자동화 가능한 충분 조건: 단순 패턴 규칙으로부터 비루핑 비종료성을 탐지하기 위한 용이하게 검사 가능한 조건(정리 5)을 제공한다.
4. 구현 (NTI): 이 접근 방식을 NTI라는 도구로 구현하였다.

실험 결과
저자는 TPDB(Termination Problem Data Base)의 비루핑 비종료 용어 리라이팅 시스템(TRS)에서 유래한 41개의 논리 프로그램을 대상으로 NTI를 평가하였다.

• 성공: 이 도구는 41개 프로그램 중 36개에 대해 비종료성을 입증하는 데 성공했다. 특히, 2024년까지의 국제 종료 경쟁(International Termination Competition)에서 다른 TRS 분석기에 의해 비종료성이 입증되지 않았던 4개의 프로그램(표의 † 표시)에 대해 성공을 거두었다.
• 실패: 주로 용어 대표자를 결정하는 "자연스러운 선택(natural choice)"을 사용할 때의 유니피케이션 알고리즘의 불완전성(예시 12)이나 단순 패턴으로의 제한(예시 9)으로 인해 5개의 프로그램에서 실패하였다.
• 성능: 실행 시간은 일반적으로 낮았으나(성공 사례의 경우 300ms 미만), 일부 복잡한 사례에서는 타임아웃이 발생했다.

의의 및 주장
저자는 자신의 접근 방식이 논리 프로그램의 종료를 부정(disprove)할 수 있는 국제 종료 경쟁에 참여하는 유일한 도구라고 주장한다. 저자는 비루핑 비종료성을 증명하는 Payet(2024)의 다른 접근 방식이 존재하지만, 그것은 다른 클래스의 비루핑성을 다루며 본 논문에서 테스트된 특정 프로그램들의 종료를 부정할 수 없다고 언급한다. 반대로, Payet(2024)의 방식은 본 방법론이 실패하는 프로그램들의 종료를 부정할 수 있다. 따라서 두 접근 방식은 상호 보완적인 것으로 제시된다.

저자는 유니피케이션 알고리즘이 현재 불완전하며, 단순 패턴으로의 제한이 범위(예: 변수를 포함하는 1-컨텍스트가 필요한 경우)를 제한한다는 점을 인정하며 겸허하게 결론을 맺는다. 향-후 과제로 완전성 해결, 초기 패턴 생성(Prop. 2) 확장, 그리고 Emmes 등(2012)과의 직접적인 비교를 위한 TRS로의 접근 방식 적응을 계획하고 있다.