Quantum Weakest Preconditions Revisited: Pre-expectations for Expected Runtime Analysis

문제점
양자 프로그램 검증은 프로그램의 동작을 추론하기 위해 최약 전조건(weakest preconditions, wp)에 크게 의존한다. D'Hondt와 Panangaden [11]의 프레임워크와 기대 런타임 분석을 위한 Liu 등의 확장 연구 [25]와 같은 기존 프레임워크는, 계산에 사용되는 술어(predicate) 또는 기대치(expectation)가 반드시 유계(bounded)여야 한다(구체적으로 항등 연산자 $I$에 의해 유계)는 근본적인 제약을 가진다. 이러한 제한은 양자 프로그램의 분석을 유한 차원 힐베르트 공간과 거의 확실히 종료되는(almost surely terminating, AST) 프로그램으로 한정시킨다.

종료가 확실하지만 기대 런타임이 무한한 프로그램을 분석하는 데에는 결정적인 격차가 존재한다. 무한 차원 설정(예: 양자 정수)에서, 프로그램은 확률 1로 종료될 수 있지만 기대 런타임은 무한히 발산할 수 있다. 표준 wp-계산법은 여기서 종료 전까지 축적된 무한한 비용을 포착할 수 없기 때문에, 비종료 루프의 최약 전조건을 0으로 처리하며 실패한다. 또한, 기존의 기대 런타임 계산법(ERT)은 유한 차원 및 AST 프로그램에 국한되어 있어, 비유계 연산자와 종료 확률이 1 미만인 비-AST 동작을 분석하는 것을 방지한다.

방법론
저자들은 유계 요구 사항을 제거하는 **전-기대치(pre-expectations)**에 기반한 새로운 프레임워크를 제안한다. 방법론은 다음과 같다:

1. 기대치의 재정의: 본 논문은 가분 힐베르트 공간(separable Hilbert space) 상에서 정의된 양의 $\infty$-자기 수반 연산자(positive, $\infty$-self-adjoint operators)인 "기대치"($E(H)$)라는 새로운 클래스의 연산자를 도입한다. 표준 자기 수반 연산자와 달리, 이는 밀도가 낮은 도메인(non-dense domains)과 비유계 값을 허용한다. 저자들은 이 연산자들의 제곱근과 도메인을 기반으로 한 특정 순서($\sqsubseteq$)를 정의하고, 기대치의 집합이 $\omega$-완전 부분 순서 집합($\omega$-cpo)을 형성함을 증명한다. 이 구조는 최소 상계(least upper bounds)를 통해 while-루프의 의미론을 정의하는 데 필수적이다.
2. 의미론 및 구문론적 정의: 저자들은 보상 문(reward(c))을 포함하는 구체적인 양자 프로그래밍 언어 qrWhile을 정의한다. 이들은 양자 상태(밀도 연산자)의 진화와 기대 보상의 축적을 분리하는 데노테이션 의미론(denotational semantics)을 제공한다.
3. 최약 전-기대치(wp) 계산법: qrWhile 프로그램에 대한 구문론적 최약 전-기대치 변환기를 정의한다. 이 변환기는 사후-기대치(post-expectation)를 전-기대치(pre-expectation)로 매핑한다. 결정적으로, 이 계산법은 비유계 연산자와 보상을 처리하여 무한한 기대 런타임을 표현할 수 있게 한다.
4. 변환을 통한 런타임 분석: 기대 런타임을 분석하기 위해, 저자들은 보상이 없는 프로그램 $S$에 reward(1) 문을 삽inserting 하는 구문론적 변환 $T(S)$를 제안한다. $S$의 기대 런타임은 $T(S)$의 기대 보상과 동일하다.
5. 순방향 및 역방향 변환기: 논문은 순방향 기대 런타임 변환기($ERT$)와 역방향 변환기($ert$)를 정의한다. 저자들은 역방향$ert$변환기가 변환된 프로그램$T(S)$의 최약 전-기대치와 동일함을 증명한다.
6. 귀납 규칙: 저자들은 정확한 최소 상계를 계산하지 않고도 기대 런타임의 상한을 설정하기 위해 Park 귀납법을 적응시켜 증명 규칙을 제공한다.

주요 기여

• 비유계 기대치: 비유계 연산자와 무한한 값을 지원하며, 새로운 순서 하에서 $\omega$-cpo를 형성하는 새로운 기대치($E(H)$) 클래스의 정의. 이를 통해 양자 정수와 같은 무한 차원 힐베르트 공간에서의 프로그램 추론이 가능하다.
• 일반화된 최약 전-기대치: 보상이 있는 qrWhile 프로그램을 위한 구문론적 및 의미론적 최약 전-기대치 계산법. 이 프레임워크는 기존 연구[11, 38]에서 요구되었던 유계 조건을 제거하여 엄격히 더 높은 표현력을 갖는다.
• 비-AST 및 무한 차원 프로그램에 대한 런타임 분석: 거의 확실히 종료되지 않는 프로그램 및 기대 런타임이 무한한 프로그램을 분석할 수 있는 능력. 본 논문은 무한 차원에서 AST가 반드시 유한한 기대 런타임을 의미하지 않음을 보여준다.
• 접근 방식의 동등성: 순방향 기대 런타임 변환기, 역방향 $ert$ 변환기, 그리고 변환된 프로그램의 최약 전-기대치가 모두 일치한다는 증명.
• 증명 규칙: 비유계 사례에서 최약 전-기대치와 기대 런타임을 바운딩하기 위한 Park 귀납 규칙의 도입.

결과
논문은 두 가지 예제 프로그램을 통해 프레임워크를 검증한다:

1. 루프의 순차적 구성: 두 개의 루프로 구성된 프로그램이 분석된다. 첫 번째 루프는 유한한 기대 런타임을 가지는 반면, 두 번째 루프은 모든 기저 상태(basis states)에 대해 AST임에도 불구하고 특정 중첩 상태에 대해 무한한 기대 런타임을 가진다. 프레임워크는 전체 프로그램이 무한한 기대 런타임을 가진다는 것을 올바르게 식별하며, 이는 기존의 유계 계산법으로는 도출할 수 없는 결과이다.
2. 단방향 양자 워크(One-Sided Quantum Walk): 워커(walker)가 왼쪽으로 이동하거나 머무르는 변형된 양자 워크이다. 분석 결과 다음과 같은 미묘한 종료 동작이 드러난다:
   • 음의 위치($n < 0$)를 가진 상태에 대해, 프로그램은 AST가 아니다.
   • 비음의 위치($n \ge 0$)를 가진 상태에 대해, 프로그램은 AST이다.
   • 그러나 비음의 상태들의 중첩에 대해, 프로그램은 AST이지만 PAST(Positive Almost Surely Terminating)는 아니다. 즉, 무한한 기대 런타임을 가진다.
     프레임워크는 이러한 뚜렷한 종료 및 런타임 특성을 성공적으로 규명하며, AST 상태의 공간은 닫혀 있는 반면, PAST 상태의 공간은 반드시 닫혀 있지는 않음을 보여준다.

의의
본 논문의 주요 의의는 유한 차원으로 제한하거나 거의 확실히 종료되는 프로그램에 국한하지 않고, 양자 프로그램의 기대 런타임을 분석할 수 있는 포괄적이고 표현력이 풍부한 프레임워크를 제공하는 데 있다고 주장한다. 비유계 전-기대치를 도입함으로써, 저자들은 특히 양자 정수와 무한한 기대 런타임을 포함하는, 이전에는 다루기 어려웠던 프로그램의 검증을 가능하게 했다. 이 작업은 무한 차원 사례와 관련하여 선행 문헌[25]에서 지적된 문제를 해결하며, 연역적 검증 패러다임을 비유계 비용 및 보상을 자연스럽게 처리하도록 확장한다. 저자들은 자신들의 접근 방식이 유한 차원 사례의 최약 전조건 스타일을 유지하면서도, 비유계성을 지원하기 위해 기초가 되는 수학적 객체를 일반화한다는 점을 강조한다.