A Machine-Checked Cost Analysis of the BMSSP Recurrence in Isabelle/HOL With a Non-Vacuous Size-Parametric Runtime Witness

Sintesi Tecnica: Un'Analisi del Costo Verificata da Macchina della Ricorrenza BMSSP

Definizione del Problema
Il saggio affronta la verifica formale della ricorrenza BMSSP (Bounded Multi-Source Shortest Path), il motore centrale dell'algoritmo deterministico del 2025 di Duan, Mao, Mao, Shu e Yin che rompe il secolare limite di $O(m + n \log n)$ per i cammini minimi a sorgente singola (SSSP) in grafi diretti. Sebbene l'algoritmo originale raggiunga un tempo di esecuzione di $O(m \log^{2/3} n)$, la formalizzazione della sua correttezza e, crucialmente, della sua analisi del costo ammortizzato in un assistente alla dimostrazione presenta sfide significative. Queste includono la complessità degli argomenti di correttezza ricorsiva riguardanti insiemi di sorgenti e intervalli di distanza limitati, la delicatezza del conteggio ammortizzato su strutture dati di partizione personalizzate e il rischio di teoremi asintotici "vacui"—enunciati che sono tecnicamente veri ma privi di significato perché la famiglia di input è limitata o le esecuzioni richieste non esistono.

Metodologia
Gli autori presentano una formalizzazione completa in Isabelle/HOL (Isabelle2025-2) strutturata in sei teorie distinte e stratificate per garantire la modularità e una rigorosa separazione delle responsabilità. Lo sviluppo importa solo HOL e HOL-Library, senza assiomi esterni, sorry o oops.

1. Fondamenta Semantiche: Gli autori definiscono grafi diretti pesati finiti, cammini semplici e metriche di distanza. Stabiliscono lemmi strutturali riguardanti cammini minimi unici e l'arbitrarietà rigorosa dei legami (tie-breaking), che costituiscono la base per tutti gli argomenti successivi.
2. Correttezza Ricorsiva: Un modello astratto della ricorrenza BMSSP viene formalizzato, inclusi le routine FindPivots, i casi base e il ciclo di partizione. Una dimostrazione verificata da macchina stabilisce che l'algoritmo astratto calcola correttamente le distanze minime per qualsiasi grafo ben formato.
3. Artefatto Eseguibile: Il modello astratto viene raffinato in una funzione eseguibile (bmssp_distances) utilizzando vertici e pesi di numeri naturali. Gli autori dimostrano bmssp_correct_strong, confermando che l'output eseguibile corrisponde alla definizione semantica delle distanze minime, verificata tramite valutazione su un esempio specifico a cinque vertici.
4. Modello di Costo: Un'interfaccia di partizione astratta (Insert, BatchPrepend, Pull) viene definita con predicati di costo. Gli autori dimostrano un inviluppo di costo ammortizzato di $O(m \log^{2/3} n)$ per questa ricorrenza astratta. Crucialmente, implementano una struttura dati di partizione a secchielli (bucketed partition) che realizza fedelmente lo schema logaritmico del saggio, dimostrando la decisiva scala di inserimento $O(\log(N/M))$ necessaria per l'accelerazione.
5. Raffinamenti Operativi: Sono definiti due livelli operativi:
   • Exact-Concrete: Accoppia strettamente l'output del figlio ricorsivo allo slice dell'intervallo incrementale.
   • Charged: Disaccoppia l'output, addebitando solo lo slice incrementale.
     Gli autori verificano tramite macchina che la relazione exact-concrete è non totale sugli input previsti (specificamente sulle famiglie di cammini), forzando un'ostruzione dove le esecuzioni complete non possono esistere.
6. Livello Parametrico per Dimensione: Gli autori costruiscono una famiglia illimitata di cammini diretti a peso unitario ($P_n$). Dimostrano che la relazione charged è totale e che esiste un'esecuzione completa. Per garantire la totalità senza alterare la classe asintotica, impiegano un indice di schema "gonfiato" ($N = n \cdot n$), che assicura che la capacità del secchiello copra il cammino preservando il fattore $O(\log^{2/3} n)$.

Contributi Chiave

• Prima Formalizzazione Meccanizzata: Questa è la prima formalizzazione verificata da macchina della ricorrenza BMSSP e della sua analisi del tempo di esecuzione.
• Testimone Size-Parametric Non-Vacuo: Il saggio fornisce un teorema completamente incondizionato che testimonia come, sulla famiglia illimitata di cammini diretti a peso unitario, il tempo di esecuzione charged sia $O(|V| \cdot (\ln |V|)^{2/3})$. Questo risultato è non-vacuo perché gli autori dimostrano esplicitamente (tramite un "registro di non-vacuità") che la famiglia cresce senza limiti, un'esecuzione completa esiste provabilmente e il regime operativo è realizzato.
• Diagnosi Formale di un'Ostruzione di Accoppiamento: Gli autori identificano e dimostrano formalmente un difetto in una relazione di costo debolmente accoppiata (il modello exact-concrete). Dimostrano che tale relazione forza l'algoritmo a compiere al massimo un passo sulle famiglie di cammini, rendendo qualsiasi limite parametrico per dimensione basato su di essa vacuo. Questa ostruzione è registrata come un lemma verificato da macchina, e il risultato principale è derivato utilizzando la relazione charged disaccoppiata per aggirarla.
• Verifica dell'Eseguibile: Lo sviluppo include una funzione di distanza minima eseguibile con una prova di correttezza che è validata dall'valutazione del codice all'interno del processo di build.

Risultati
Il teorema principale, path_nonvac_runtime_bigo_card_V_unconditional, afferma:
$$(\lambda n. \text{real}(\text{path\_nonvac\_time } n)) \in O(\lambda n. \text{real}(\text{card}(\text{path\_k\_V } n)) \cdot (\ln(\text{real}(\text{card}(\text{path\_k\_V } n)) + 2))^{2/3})$$
Questo limite è:

• Incondizionato: Non porta ipotesi riguardanti l'esistenza di esecuzioni o proprietà dei grafi oltre alla definizione della famiglia di cammini.
• Size-Parametric: La variabile asintotica è la vera dimensione del grafo ($|V|$), non un parametro fisso.
• Non-Vacuo: Limita il costo di un'esecuzione a costo minimo che è provata esistere.

Il saggio stabilisce anche il limite $O(m \log^{2/3} n)$ per il modello di costo astratto realizzato dalla struttura concreta a secchielli, confermando la scala di inserimento $O(\log(N/M))$.

Significato e Ambito
Gli autori inquadrano esplicitamente la significatività di questo lavoro come una formalizzazione rigorosa della correttezza della ricorrenza BMSSP e della sua analisi del tempo di esecuzione charged, piuttosto che una verifica completa end-to-end dell'implementazione SSSP di Duan–Mao–Mao–Shu–Yin.

• Cosa viene rivendicato: Il saggio afferma di aver verificato la correttezza della logica della ricorrenza e la validità dell'analisi del costo delle operazioni charged, incluso un limite asintotico non-vacuo per una specifica famiglia illimitata.
• Cosa NON viene rivendicato: Gli autori non pretendono di aver verificato la complessità dei passi di macchina del codice SML esportato, né pretendono di avere un limite universale per tutti i grafi o per tutte le esecuzioni. Dichiarano esplicitamente che il limite size-parametric vincola l'esecuzione a costo minimo di una specifica famiglia, poiché un limite universale è falso per questa famiglia.
• Contributo Metodologico: Il saggio evidenzia l'importanza della "non-vacuità" come un obbligo di prova di primo livello nella complessità meccanizzata. Dimostra che i teoremi asintotici possono essere logicamente validi ma vuoti se la famiglia di input è limitata o se le esecuzioni non esistono. Il "registro di non-vacuità" (dimostrare crescita, esistenza di esecuzione e realizzazione del regime) è presentato come un template riutilizzabile per future formalizzazioni di argomenti di complessità ricorsiva.

In sintesi, il lavoro fornisce una base ad alta affidabilità e verificata da macchina per la ricorrenza BMSSP, separando rigorosamente la correttezza funzionale dall'analisi del costo e diagnosticando con cura le insidie della formalizzazione della complessità ammortizzata per garantire che i limiti asintotici risultanti siano significativi.