Revisiting average case complexity of multilevel syllogistic: From the 1995 Courant Technical Report to Lean 4 Formalization

Sintesi Tecnica: Revisione della Complessità del Caso Medio del Silogismo Multilivello

Enunciato del Probleo
Questo lavoro rivisita il rapporto tecnico Courant TR1995-711 del 1995, "The average case complexity of multilevel syllogistic," di Cox, Ericson e Mishra. Il rapporto originale indagava se i sottolinguaggi decidibili della teoria degli insiemi — specificamente il Silogismo Multilivello (MLS) e il Silogismo Multilivello Elementare (EMLS) — fossero trattabili in media, nonostante siano NP-completi nel caso peggiore. Il rapporto sosteneva che questi problemi siano NP-average complete, implicando che, sotto semplici distribuzioni di probabilità classificabili, non esista un algoritmo efficiente per il caso medio a meno che le classi di complessità NEXP e EXP non collassino.

Sebbene il rapporto originale fornisse prove matematiche, mancava di una verifica verificata tramite macchina. Inoltre, il campo della dimostrazione automatica dei teoremi si è successivamente orientato verso i solver SMT e i benchmark empirici piuttosto che verso l'analisi formale del caso medio di frammenti della teoria degli insiemi. Questo articolo affronta il divario tra le originali rivendicazioni teoriche e gli standard moderni di verifica formale, reimplementando la logica, le definizioni e i teoremi del rapporto in Lean 4.

Metodologia
Gli autori adottano una rigorosa strategia di "programma di prova", dando priorità alle definizioni formali rispetto ai teoremi ed evitando l'uso di sorry (assunzioni non provate) nelle definizioni finali. Lo sviluppo è strutturato in cinque fasi:

1. Infrastruttura (Fase 0): Configurazione del progetto Lake e dell'ambiente Lean.
2. Vocabolario della Complessità del Caso Medio (AvCom) (Fase 1): Formalizzazione del framework Reischuk–Schindelhauer (1993) e delle definizioni della complessità del caso medio di Levin (1986). Ciò include la definizione di:
   • Distribuzioni: Distribuzioni di probabilità a supporto finito su stringhe di bit.
   • Funzioni di Rango: Conteggio degli input con probabilità maggiore o uguale a un dato input.
   • Classi di Complessità: Definizione di AvP (Tempo Polinomiale in Media), distNP (NP distributivo) e AvDTime (Tempo Deterministico in Media) utilizzando la disuguaglianza somma-rango di RS93.
   • Riduzioni: Formalizzazione delle riduzioni distributive con la condizione di dominazione per preservare la trattabilità del caso medio.
3. Embedding MLS (Fase 2): Embedding profondo della sintassi e della semantica di MLS ed EMLS.
   • Sintassi: Definizioni induttive per termini (variabili, unione, intersezione, differenza), relazioni (appartenenza, uguaglianza) e formule.
   • Semantica: Una semantica ZF della teoria degli insiemi (ZFSet) con funzioni di valutazione non computabili.
   • Procedura Decisionale: Implementazione di una procedura decisionale parziale basata su Ferro–Omodeo–Schwartz (1980). Gli autori dimostrano la correttezza (soundness) e la completezza parziale per un frammento privo di appartenenza, pur riconoscendo che la completezza totale (che richiede la sostituzione dello Step 1 e la ricerca completa del modello dello Step 4) rimane aperta.
4. Serializzazione e Appartenenza a NP (Fase 3): Definizione di codifiche binarie per le formule MLS e dimostrazione che il problema della soddisfacibilità (SatMLS) appartiene a NP tramite un verificatore basato su certificati.
5. Durezza e Completezza (Fasi 4–5):
   • Riduzioni: Costruzione di una riduzione distributiva da Bounded Halting (NBH) a SatMLS. A causa della complessità della traduzione completa TM-to-MLS, la mappa di riduzione generale è assiomatizzata (nbhToMlsMap), mentre la condizione di dominazione è verificata per una specifica distribuzione di supporto.
   • Completezza: Dimostrazione che SatMLS è NP-average complete, condizionata all'assioma secondo cui ogni problema distNP si riduce a NBH.
   • Corollari di Durezza: Deduzione che SatMLS non è in AvP a meno che NEXP = EXP, utilizzando la completezza stabilita e l'ipotesi di collasso.

Contributi Chiave

• Formalizzazione di TR1995-711: La prima formalizzazione verificata da macchina dei risultati della complessità del caso medio per MLS ed EMLS.
• Libreria Lean 4 per AvCom: La creazione di una libreria dedicata (AvgCaseMls) che implementa le classi di Reischuk–Schindelhauer, le riduzioni distributive e le distribuzioni classificabili, colmando una lacuna nell'ecosistema Mathlib4 che attualmente si concentra sulla complessità del caso peggiore.
• Verifica di Correttezza e Completezza Parziale: Dimostrazioni rigorose che la procedura decisionale implementata è corretta e completa per lo specifico frammento di MLS senza letterali di appartenenza.
• Trasparenza Assiomatica: Gli autori documentano esplicitamente le "fork" (scelte di design) e gli assiomi (ad esempio, la mappa di riduzione generale TM-to-MLS e l'ipotesi NEXP ≠ EXP) in DEFINITION_FORKS.md, distinguendo tra teoremi provati e impalcature necessarie.

Risultati
Il documento riporta i seguenti esiti per il piano di fasi:

• Fasi 1A–1D (Definizioni AvCom): Tutte le definizioni compilano senza sorry. La formalizzazione di input, distribuzioni, funzioni di rango e classi di complessità corrisponde alla letteratura.
• Fasi 2A–2D (MLS & Decisione): Sintassi, semantica e la procedura decisionale parziale sono verificate. La correttezza è dimostrata; la completezza è dimostrata solo per il frammento privo di appartenenza.
• Fasi 3A–3B (Codifica): I limiti polinomiali sulla dimensione della codifica e l'appartenenza a NP del verificatore sono verificati.
• Fasi 4A–4C (Riduzioni & Completezza): La riduzione da NBH a SatMLS è verificata modulo la mappa di traduzione generale assiomatizzata. La NP-average completezza di SatMLS è dimostrata modulo l'assioma che tutti i problemi distNP si riducono a NBH.
• Fasi 5A–5B (Durezza): La durezza condizionale non-AvP di SatMLS è derivata, subordinata all'assioma NEXP ≠ EXP.

Significato e Rivendicazioni
Il documento non sostiene di aver "risolto" la complessità del caso medio di MLS in un modo che cambi l'ingegneria del software pratica. Invece, il suo significato è storico e metodologico:

1. Sopravvivenza della Teoria: Testa se le rivendicazioni matematiche del rapporto del 1995 sopravvivano al contatto con un moderno assistente di prova. I risultati indicano che la logica centrale regge, a patto che vengano accettati specifici assiomi strutturali (come l'esistenza di una riduzione universale a NBH).
2. Chiarificazione delle Assunzioni: Formalizzando il lavoro, gli autori espongono le precise dipendenze della prova originale, come la dipendenza dall'ipotesi NEXP ≠ EXP per i risultati di durezza e la necessità di specifiche proprietà di riduzione distributiva.
3. Fondamenta per il Lavoro Futuro: Il documento sostiene che, sebbene l'applicazione specifica di AvCom alle procedure decisionali di MLS sia stata ampiamente abbandonata in favore dei solver SMT negli anni '90, il framework formale sviluppato qui fornisce un'infrastruttura necessaria per rivisitare l'analisi del caso medio in altri domini, come l'analisi smoothed o la crittografia post-quantistica, all'interno dell'ecosistema Lean.

Gli autori dichiarano esplicitamente che non trattano sorry o gli assiomi come un successo; piuttosto, essi servono come "impalcatura temporanea" con ticket per rimuoverli nel lavoro futuro. Il documento conclude che la visione del rapporto del 1995 di utilizzare la complessità del caso medio per caratterizzare la trattabilità dei problemi di verifica rimane matematicamente coerente, anche se il percorso pratico verso l'implementazione si è spostato.