Hypersequent Calculi Have Ackermannian Complexity

1. Il Problema

Il lavoro si concentra sulla complessità computazionale del problema della decidibilità (provabilità) per le estensioni delle logiche substrutturali, in particolare il calcolo di Full Lambek con contrazione ($FL_{ec}$) e con indebolimento ($FL_{ew}$).

• Contesto: Le logiche substrutturali (come la logica lineare, le logiche della rilevanza e le logiche fuzzy) sono caratterizzate dall'assenza o modifica di regole strutturali come contrazione e indebolimento.
• Stato dell'arte: Per $FL_{ec}$, è noto che la complessità è Ackermanniana (classe $F_\omega$), basata su argomenti di sequenze "cattive" (bad sequences) su ordini ben-quasi (wqo) definiti su $\mathbb{N}^d$ (Lemma di Dickson).
• La sfida: Molte estensioni di queste logiche non ammettono calcoli di sequenti senza taglio (cut-free), ma ammettono calcoli di ipersequenti (hypersequents). Un ipersequente è un multiset di sequenti.
• L'ipotesi errata: Analisi precedenti (es. Balasubramanian et al.) avevano sollevato l'ordine ben-quasi dal livello delle sequenti ($\mathbb{N}^d$) a quello dell'insieme delle parti (powerset) dei sequenti, poiché un ipersequente è un insieme di sequenti. Poiché la lunghezza delle sequenze controllate su ordini powerset cresce a un livello iper-Ackermanniano ($F_{\omega^\omega}$), si pensava che l'uso di calcoli di ipersequenti implicasse inevitabilmente un salto di complessità verso l'iper-Ackermannianità.

L'obiettivo del paper è dimostrare che questa intuizione è falsa: anche per le estensioni di $FL_{ec}$ e $FL_{ew}$ che richiedono calcoli di ipersequenti, la complessità rimane Ackermanniana.

2. Metodologia

Gli autori sviluppano nuove tecniche di ricerca di prove che evitano il salto al powerset, sfruttando le dipendenze interne tra i componenti di un ipersequente.

A. Caso della Contrazione ($FL_{ec}$)

Per le logiche con contrazione, gli autori combinano due trasformazioni sui calcoli:

1. Calcoli Invertibili: Modificano i calcoli di ipersequenti in modo che i componenti principali delle regole persistano nelle premesse (calcoli invertibili), permettendo di tracciare le dipendenze.
2. Calcoli Raffinati (Refined Calculi): Introducono un numero limitato e controllato di applicazioni delle regole di contrazione e indebolimento esterno all'interno delle istanze delle regole, basandosi su parametri sintattici (formula multiplicity e active component number).
3. Sequenze Cattive Controllate: Invece di trattare l'intero ipersequente come un elemento di un ordine powerset, linearizzano l'ipsersequente come una sequenza di sequenti nell'ordine in cui vengono aggiunti durante la ricerca all'indietro. Dimostrano che questa sequenza di sequenti forma una sequenza cattiva controllata rispetto all'ordine ben-quasi standard sulle sequenti ($\mathbb{N}^d$).
4. Risultato: Poiché la lunghezza delle sequenze cattive controllate su $\mathbb{N}^d$ è limitata da funzioni Ackermanniane, la complessità della ricerca di prove rimane in $F_\omega$.

B. Caso dell'Indebolimento ($FL_{ew}$) e Logiche Fuzzy

Il caso dell'indebolimento è più complesso perché la ricerca di prove all'indietro non termina naturalmente (l'indebolimento può generare sequenze infinite).

1. Accelerazione di Karp-Miller: Gli autori introducono una tecnica ispirata all'algoritmo di Karp-Miller per i sistemi di addizione vettoriale. Se un componente attivo in una premessa ha una molteplicità strettamente maggiore rispetto a un componente precedente, la molteplicità viene sostituita da un simbolo $\omega$ (formule $\omega$).
2. Calcolo $\omega$-Raffinato: Viene definito un calcolo esteso ($HFL_{ew}^\omega$) che opera su sequenti $\omega$ (dove le formule possono avere molteplicità finite o $\omega$).
3. Rifinitura $\omega$ ($\omega$-refinement): Durante la ricerca di prove, se viene rilevato un incremento significativo, si applica una trasformazione che "promuove" le formule a $\omega$-formule, garantendo che l'ordine ben-quasi venga mantenuto anche con l'aggiunta di queste nuove coordinate.
4. Albero di Ricerca: Viene costruito un albero di ricerca di prove ($T_\omega$) su ipersequenti indicizzati e relazionali. Gli autori dimostrano che ogni ramo di questo albero è una sequenza cattiva controllata su un nuovo ordine ben-quoso ($W(\omega, d)$), la cui lunghezza è ancora limitata da funzioni Ackermanniane.

3. Contributi Chiave

• Rottura del limite Iper-Ackermanniano: Dimostrazione che il passaggio da sequenti a ipersequenti non comporta necessariamente un aumento della complessità da $F_\omega$ a $F_{\omega^\omega}$.
• Nuova Tecnica di Analisi: Sfruttamento delle dipendenze tra i componenti di un ipersequente per mantenere l'analisi all'interno dell'ordine delle sequenti, evitando il lifting al powerset.
• Accelerazione $\omega$ per Logiche Substrutturali: Adattamento e generalizzazione della tecnica di accelerazione di Karp-Miller (tipica dei sistemi di Petri) al contesto dei calcoli di ipersequenti per gestire l'indebolimento.
• Ottimalità: Il limite superiore Ackermanniano è mostrato come ottimale per il caso della contrazione, poiché $FL_{ec}$ realizza già questa complessità.

4. Risultati Principali

1. Teorema Principale I: La provabilità in qualsiasi estensione analitica strutturale di $FL_{ec}$ (aggiunta di assiomi aciclici di livello $P'_3$) ha complessità Ackermanniana ($F_\omega$).
2. Teorema Principale II: La provabilità in qualsiasi estensione analitica strutturale di $FL_{ew}$ (aggiunta di assiomi di livello $P_3$) ha complessità Ackermanniana ($F_\omega$).
3. Corollario per MTL: La logica fuzzy fondamentale MTL (Monoidal T-norm based Logic), che è un'estensione di $FL_{ew}$, ha complessità Ackermanniana. Questo risolve una questione aperta di lunga data (prima nota solo come upper bound iper-Ackermanniano).
4. Algoritmo di Decisione: Viene presentato un algoritmo ($Wkn$) che decide la provabilità in tempo $F^\star_\omega$ (classe di funzioni che definisce la complessità Ackermanniana).

5. Significato

• Teoria della Complessità: Il lavoro chiarisce la gerarchia di complessità delle logiche substrutturali, mostrando che la necessità di ipersequenti per la cut-eliminazione non degrada la complessità computazionale oltre i limiti già noti per i calcoli di sequenti.
• Logiche Fuzzy: Fornisce il primo limite superiore preciso (Ackermanniano) per la logica MTL e le sue estensioni, chiudendo un gap significativo nella letteratura sulle logiche fuzzy.
• Sistemi a Stato Infinito: Le tecniche sviluppate (in particolare l'uso di accelerazioni e l'analisi di sequenze cattive su strutture complesse) sono rilevanti per la comunità dei sistemi a stato infinito, offrendo nuovi strumenti per l'analisi di sistemi come i BVASS (Branching Vector Addition Systems with States) con interazioni tra configurazioni.

In sintesi, il paper ribalta l'assunzione comune secondo cui gli ipersequenti implicano automaticamente una complessità iper-Ackermanniana, fornendo invece algoritmi e prove che mantengono la complessità al livello Ackermanniano, ottimizzando così la nostra comprensione della decidibilità di una vasta classe di logiche non-classiche.