Completeness of Synthesis under Realizability Assumptions using Superposition

기술적 요약: 초위치를 이용한 실현 가능성 가정 하의 합성 완전성

문제 제기
본 논문은 1 차 논리 명세로부터 재귀가 없는 프로그램을 유도하는 자동 프로그램 합성 문제를 다룬다. 핵심적인 난제는 명세 내에 존재하는 "비계산 가능 심볼"에 있다. 이러한 심볼은 증명 탐색 과정에서 도입된 사용자 주석 붙인 술어나 스코렘 함수를 포함할 수 있으며, 최종 합성된 프로그램에는 나타날 수 없다. 합성된 프로그램은 계산 가능 심볼 (예: 표준 산술, 사용자 정의 함수) 로만 구성되어야 하지만, 계산 가능 심볼과 비계산 가능 심볼이 모두 혼합될 수 있는 명세를 만족해야 한다.

Hozzová 외 [14] 의 이전 연구는 초위치 (superposition) 계산을 기반으로 한 포화 (saturation) 기반 프레임워크를 도입하여 이 문제를 해결했다. 해당 접근법은 건전성 (derivation 된 모든 프로그램이 정확함) 이 입증되었으나, 그 완전성은 여전히 미해결 과제였다. 구체적으로, 해가 존재한다면 (실현 가능성 가정) 해당 계산이 해를 찾을 수 있는지 여부는 불분명했다. 본 논문은 계산 가능한 프로그램이 존재함에도 불구하고 [14] 의 계산이 해를 유도하지 못하는 특정 시나리오를 식별했는데, 이는 주로 항 순서 (term orderings), 선택 함수 (selection functions), 그리고 계산 가능 및 비계산 가능 리터럴 간의 상호작용을 처리하는 방식의 한계로 인해 발생한다.

방법론: SUPRA 계산
저자들은 이전 프레임워크의 불완전성을 해결하기 위해 SUPRA(Realizability Assumptions with Superposition) 라는 정제된 계산을 제안한다. 방법론은 표준 초위치 기반 합성 접근법에 세 가지 주요 기술적 조정을 포함한다:

1. 분할된 순서 및 선택 (Partitioned Orderings and Selection):
   본 논문은 "분할된" 단순화 순서를 도입한다. 이 순서에서 모든 기본 (ground) 비계산 가능 항은 모든 기본 계산 가능 항보다 엄격하게 크다. 결과적으로 선택 함수는 절 (clause) 내의 모든 최대 리터럴을 항상 선택하도록 제한된다. 이는 비계산 가능 리터럴 (더 큰 값) 이 관련된 추론이 계산 가능 리터럴만 포함된 추론보다 우선시되도록 보장한다. 이로 인해 비계산 가능 제약이 계산 가능한 분기의 해결을 방해하는 추론에서 계산이 멈추는 것을 방지한다.

2. 추상화 규칙 (Abs):
   비계산 가능 리터럴이 처리되기 전에 해결되어야 하는 계산 가능 부분항을 포함하는 비계산 가능 방정식이 발생하는 경우를 처리하기 위해, 저자들은 Abs라는 보조 추론 규칙을 도입한다. 이 규칙은 비계산 가능 리터럴 내의 계산 가능 부분항을 새로운 변수로 대체하고 부등식 제약 (예: $s[k] \approx t$를 $s[x] \approx t \land x \neq k$로 변환) 을 추가함으로써 추상화한다. 이 메커니즘은 비계산 가능 심볼에 대한 추론을 계산 가능 심볼에 대한 추론과 분리하여, 답변 항의 계산 가능성 제약을 위반하지 않으면서 비계산 가능 리터럴을 해결할 수 있게 한다.

3. 정제된 추론 규칙:
   해당 계산은 초위치 규칙의 두 가지 변형을 활용한다:

   • SupC: 등식 리터럴에 대한 분기 시 답변 항에 ite(if-then-else) 생성자를 도입한다.
   • SupU: 제약 조건을 추가하여 비계산 가능 조건으로 이어질 수 있는 것을 피하면서 전제에서 직접 답변 항을 통일 (unify) 한다.
     또한 해당 계산은 [14] 에서 사용된 "계산 가능 통일자"를 표준 최일반 통일자 (MGU) 로 대체하며, 분할된 순서와 Abs 규칙에 의존하여 결과적인 답변 항이 계산 가능하도록 보장한다.

주요 기여

• 불완전성 식별: 본 논문은 워크샵 스케줄링 시나리오와 상수 조작 시나리오와 같은 반례를 통해 [14] 의 계산이 실현 가능성 가정 하에서 완전하지 않음을 입증한다. 리터럴의 선택이나 항의 순서가 비계산 가능 심볼에 대한 필수 추론을 방해할 때 해를 찾지 못한다.
• SUPRA 프레임워크: 저자들은 분할된 순서, Abs 규칙, 그리고 특정 선택 제약을 통합한 SUPRA 계산을 정의한다.
• 건전성 증명: 본 논문은 답변 절의 의미론에 대해 SUPRA 가 건전함을 증명하여, 유도된 모든 프로그램이 합성 명세의 유효한 해임을 보장한다.
• 완전성 증명: 주요 이론적 기여는 실현 가능성 가정 하에서 SUPRA 가 완전함을 증명하는 것이다. 저자들은 명세를 만족하는 계산 가능한 프로그램이 존재한다면, Abs 규칙을 사용하여 포화 상태까지 사용하는 SUPRA 계산이 해를 유도할 것임을 보인다. 이 증명은 포화된 절 집합에 대한 모델을 구성하고, 해가 유도되지 않는다면 부명세의 만족 가능성에 관한 모순이 발생함을 보여준다.

결과 및 의의
본 논문은 계산 가능 및 비계산 가능 심볼 간의 상호작용을 신중하게 관리함으로써 실현 가능성 가정 하에서 포화 기반 정리 증명에 의한 프로그램 합성을 완전하게 만들 수 있음을 확립한다. 이 연구의 의의는 이전 연구 [14] 가 남긴 이론적 간극을 메우고, 계산 가능 시그니처 내에 해가 존재한다면 합성 과정이 성공할 것이라는 형식적 보장을 제공한다는 점에 있다.

저자들은 그들의 실현 가능성 개념이 재귀가 없는 프로그램에 적용된다고 지적한다. 재귀 프로그램의 구성은 현재 계산이 다루지 않는 (예: 귀납법과 같은) 메커니즘이 필요하다. 또한, 완전성 결과는 조건부이다. 즉, 모든 명세에 대해 해의 존재를 증명하는 것이 아니라, 만약 해가 존재한다면 그것을 찾는 것을 보장한다. 이 작업은 등식이 포함된 표준 1 차 논리에 의존하며, 선형 산술과 같은 양소 제거가 필요한 이론을 포함하는 합성 문제를 해결한다고 주장하지는 않는다 (단, 해당 이론이 기본 증명기의 이론 추론 기능으로 처리되는 경우 제외).

요약하자면, 본 논문은 분할된 순서와 추상화 메커니즘을 도입하여 합성을 위한 초위치 계산을 정제하고, 이러한 수정이 비계산 가능 심볼이 존재하는 상황에서 재귀가 없는 프로그램 합성의 완전성을 보장하기에 충분함을 증명한다.