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

Problema
La verifica di programmi quantistici si basa fortemente sulle precondizioni deboli (wp) per ragionare sul comportamento dei programmi. Gli attuali framework, come quelli di D'Hondt e Panangaden [11] e le estensioni per l'analisi del tempo di esecuzione atteso di Liu et al. [25], richiedono fondamentalmente che i predicati o le aspettative utilizzati nel calcolo siano limitati (specificamente, limitati dall'operatore identità $I$). Questa restrizione limita l'analisi dei programmi quantistici a spazi di Hilbert a dimensione finita e a programmi quasi certamente terminanti (AST).

Esiste una lacuna critica nell'analisi di programmi che sono AST ma possiedono un tempo di esecuzione atteso infinito. Negli scenari a dimensione infinita (ad esempio, interi quantistici), un programma può terminare con probabilità 1 mentre il suo tempo di esecuzione atteso diverge all'infinito. Il calcolo wp standard fallisce qui perché la precondizione debole di un ciclo non terminante è 0, il che non può catturare il costo infinito accumulato prima della terminazione. Inoltre, gli esistenti calcoli del tempo di esecuzione atteso (ERT) sono limitati alle dimensioni finite e ai programmi AST, impedendo l'analisi di operatori non limitati e di comportamenti non-AST dove la probabilità di terminazione è inferiore a 1.

Metodologia
Gli autori propongono un nuovo framework basato su pre-aspettative che rimuove il requisito di limitatezza. La metodologia prevede:

1. Ridefinizione delle Aspettative: Il documento introduce una nuova classe di operatori chiamati "aspettative" ($E(H)$) definiti come operatori positivi, $\infty$-auto-adiunti su uno spazio di Hilbert separabile. A differenza degli standard operatori auto-adiunti, questi permettono domini non densi e valori non limitati. Gli autori definiscono un ordine specifico ($\sqsubseteq$) basato sulle radici quadrate di questi operatori e sui loro domini, dimostrando che l'insieme delle aspettative forma un ordine parziale $\omega$-completo ($\omega$-cpo). Questa struttura è essenziale per definire la semantica dei cicli while tramite estremi superiori.
2. Definizioni Semantiche e Sintattiche: Gli autori definiscono un linguaggio di programmazione quantistica concreto, qrWhile, che include istruzioni di ricompensa (reward(c)). Forniscono una semantica denotazionale che separa l'evoluzione dello stato quantistico (operatori di densità) dall'accumulo delle ricompense attese.
3. Calcolo della Precondizione Debole (wp) di Pre-aspettativa: Viene definito un trasformatore di precondizione debole sintattico per i programmi qrWhile. Questo trasformatore mappa una post-aspettativa in una pre-aspettativa. Crucialmente, il calcolo gestisce operatori e ricompense non limitati, permettendo l'espressione di tempi di esecuzione attesi anche quando sono infiniti.
4. Analisi del Tempo di Esecuzione tramite Trasformazione: Per analizzare il tempo di esecuzione atteso, gli autori propongono una trasformazione sintattica $T(S)$ che inserisce istruzioni reward(1) in un programma privo di ricompense $S$. Il tempo di esecuzione atteso di $S$ è quindi equivalente alla ricompensa attesa di $T(S)$.
5. Trasformatori Forward e Backward: Il documento definisce sia un trasformatore del tempo di esecuzione atteso in avanti (forward $ERT$) sia un trasformatore all'indietro (backward $ert$). Dimostrano che il trasformatore $ert$ all'indietro è equivalente alla precondizione debole del programma trasformato $T(S)$.
6. Regole di Induzione: Gli autori adattano l'induzione di Park per fornire regole di prova per stabilire limiti superiori sui tempi di esecuzione attesi e sulle probabilità di terminazione senza calcolare esattamente gli estremi superiori minimi.

Contributi Chiave

• Aspettative Non Limitate: La definizione di una nuova classe di aspettative ($E(H)$) che supporta operatori non limitati e valori infiniti, formando un $\omega$-cpo sotto un nuovo ordine. Ciò consente di ragionare su programmi in spazi di Hilbert a dimensione infinita (ad esempio, interi quantistici).
• Precondizione Debole Generalizzata: Un calcolo di precondizione debole sintattica e semantica per programmi qrWhile con ricompense. Questo framework abbandona la condizione di limitatezza richiesta nei lavori precedenti [11, 38], rendendolo strettamente più espressivo.
• Analisi del Tempo di Esecuzione per Programmi Non-AST e a Dimensione Infinita: La capacità di analizzare i tempi di esecuzione attesi per programmi che non sono quasi certamente terminanti e per quelli con tempi di esecuzione attesi infiniti. Il documento dimostra che AST non implica un tempo di esecuzione atteso finito nelle dimensioni infinite.
• Equivalenza degli Approcci: Una prova che il trasformatore del tempo di esecuzione atteso in avanti, il trasformatore $ert$ all'indietro e la precondizione debole del programma trasformato coincidono tutti.
• Regole di Prova: L'introduzione di regole di induzione di Park per limitare le precondizioni deboli e i tempi di esecuzione attesi nel caso non limitato.

Risultati
Il documento valida il framework attraverso due programmi di esempio:

1. Composizione Sequenziale di Cicli: Viene analizzato un programma composto da due cicli. Il primo ciclo ha un tempo di esecuzione atteso finito, mentre il secondo ha un tempo di esecuzione atteso infinito per certe sovrapposizioni, nonostante sia AST per tutti gli stati base. Il framework identifica correttamente il programma totale come avente un tempo di esecuzione atteso infinito, un risultato non derivabile utilizzando gli esistenti calcoli limitati.
2. Camminata Quantistica Unilaterale: Una variante di una camminata quantistica in cui il camminatore si muove a sinistra o resta fermo. L'analisi rivela un comportamento di terminazione sfumato:
   • Per stati con posizione negativa ($n < 0$), il programma non è AST.
   • Per stati con posizione non negativa ($n \ge 0$), il programma è AST.
   • Tuttavia, per sovrapposizioni di stati non negativi, il programma è AST ma non è PAST (Positive Almost Surely Terminating), il che significa che ha un tempo di esecuzione atteso infinito.
     Il framework caratterizza con successo queste distinte proprietà di terminazione e tempo di esecuzione, mostrando che lo spazio degli stati AST è chiuso, mentre lo spazio degli stati PAST non è necessariamente chiuso.

Significatività
Il documento afferma che la sua principale significatività risiede nel fornire un framework completo ed espressivo per analizzare il tempo di esecuzione atteso dei programmi quantistici senza limitarsi a spazi a dimensione finita o a programmi quasi certamente terminanti. Introducendo pre-aspettative non limitate, gli autori consentono la verifica di programmi che erano precedentemente intrattabili, in particolare quelli che coinvolgono interi quantistici e tempi di esecuzione attesi infiniti. Il lavoro affronta una sfida specifica evidenziata nella letteratura precedente [25] riguardante il caso a dimensione infinita ed estende il paradigma della verifica deduttiva per gestire naturalmente costi e ricompense non limitati. Gli autori sottolineano che il loro approccio mantiene lo stile delle precondizioni deboli del caso a dimensione finita, generalizzando al contempo gli oggetti matematici sottostanti per supportare la non-limitatezza.