상태 공간(State Spaces) 상의 연산을 위한 술어 기반 모델

많은 주류 프로그래밍 인터페이스는 명령의 시퀀스, 제어 흐름 구조(control-flow constructs), 그리고 명시적인 실행 단계로서 절차적(procedurally)으로 연산을 표현합니다. 그러나 몇몇 중요한 문제 클래스들은 선언적(declaratively)으로 기술하는 것이 더 자연스럽습니다. 즉, 후보 상태(candidate states)의 집합과 특정 상태를 유효하게 만드는 조건을 지정하는 방식입니다. 본 논문은 상태 공간(state spaces) 상의 연산을 위한 술어 기반 추상화(predicate-based abstraction)를 공식화합니다. 연산 문제는 상태 공간 $S$와 술어 $C: S
ightarrow {0,1}$에 의해 표현됩니다. 솔루션은 술어를 만족하는 상태들이며, 실행은 이 솔루션 집합을 평가(evaluating), 샘플링(sampling), 탐색(searching) 또는 기타 방식으로 특징짓는 구현 전략(realization strategy)에 위임됩니다. 우리는 문제 명세(problem specification)를 백엔드 특정 평가기(backend-specific evaluators)와 구분하고, 결합된 술어들이 구현(realizations) 전반에 걸쳐 그 의미를 보존하는 조건을 확립하는 최소한의 의미 보존 계약(semantic-preservation contract)을 도입합니다. 본 연구의 기여는 새로운 클래스의 제약 문제(constraint problems)를 제시하거나 술어 평가가 항상 효율적이라고 주장하는 것이 아니라, 통합된 추상화와 보존 계약을 제공하는 것입니다. 절차적 알고리즘(Procedural algorithms), 솔버(solvers), 확률적 방법(probabilistic methods), 그리고 양자 오라클(quantum oracles)은 동일한 의미론적 명세의 가능한 구현체로 취급됩니다. 이 모델은 제약 충족(constraint satisfaction), 충족 가능성(satisfiability), 논리 프로그래밍(logic programming), 관계형 쿼리 처리(relational query processing), 모델 체킹(model checking), 고수준 양자 언어(high-level quantum languages), 그리고 양자 중간 표현(quantum intermediate representations)과 관련이 있습니다. 양자 컴퓨팅(quantum computation)과의 관련성은, 불리언 술어(Boolean predicate)가 유한하고 효율적으로 표현 가능할 때, 계산 기저 상태(computational basis states)에 대한 가역적 또는 위상 오라클(reversible or phase oracle)로 구체화될 수 있다는 사실에서 기인합니다. 이는 이 추상화가 문제를 회로(circuit)로 기술할 필요 없이, 선언적 문제 명세와 양자 지향적 실행 사이를 잇는 가교 역할을 하게 합니다.