Layered Monoidal Theories II: Fibrational Semantics

1. Il Problema

Il lavoro affronta la necessità di fornire una semantica rigorosa per le teorie monoidali stratificate (layered monoidal theories), introdotte nella Parte I dello stesso progetto [19].

• Contesto: Le teorie monoidali stratificate permettono di combinare diverse teorie monoidali (livelli di astrazione) e le traduzioni funtoriali tra di esse all'interno di un unico linguaggio diagrammatico (string diagram). Questo è utile per modellare sistemi che ammettono descrizioni a diversi livelli di granularità (es. reazioni chimiche come reti di reazione vs grafi molecolari, o architetture informatiche come circuiti microelettronici).
• La sfida: Mentre la Parte I ha definito la sintassi (i termini e le equazioni strutturali), mancava una interpretazione semantica solida. In particolare, era necessario capire come interpretare i "confini funtoriali" (functor boundaries) che permettono di far scorrere i termini da un livello all'altro, e come formalizzare le traduzioni bidirezionali tra livelli.
• Obiettivo: Definire modelli categorici per tre classi di teorie stratificate (opfibrational, fibrational e deflational) e dimostrare la correttezza (soundness) e la completezza di queste teorie rispetto ai rispettivi modelli.

2. Metodologia

Gli autori adottano un approccio basato sulla teoria delle categorie, utilizzando costruzioni universali e dualità.

• Classificazione delle Teorie: Vengono definite tre classi di teorie basate su procedure di ordinamento ricorsivo (recursive sorting procedures) che determinano quali termini sono ammessi:
  1. Teorie Opfibrational: Contengono solo confini funtoriali diretti (da sinistra a destra).
  2. Teorie Fibrational: Sono il duale delle opfibrational, con confini diretti inversi.
  3. Teorie Deflational: La classe più espressiva, ottenuta "incollando" le versioni opfibrational e fibrational lungo i termini interni, permettendo confini bidirezionali.
• Strumenti Categoricali:
  • Fibrations e Opfibrations: Utilizzate per modellare l'indicizzazione e le traduzioni tra livelli.
  • Monoidi Indicizzati (Indexed Monoids): Strutture che assegnano una struttura monoidale a ogni fibra di una opfibration.
  • Deflazioni (Deflations): Una nuova struttura introdotta dagli autori. Una deflazione è un "local retrofunctor" verso una 2-categoria a zigzag (Zigzag 2-category), che è ottenuta aggiungendo liberamente un aggiunto destro a ogni morfismo di una categoria base. Questo permette di gestire la bidirezionalità in modo coerente.
  • Costruzione di Grothendieck e Collages: Utilizzati per collegare le strutture indicizzate alle fibrations e per generalizzare la costruzione dei modelli.
• Dimostrazione di Correttezza e Completezza: Per ogni classe di teorie, gli autori costruiscono un modello libero (term model) ottenendo una coppia di adjunzione libera-forgetful (free-forgetful adjunction) tra la categoria delle teorie e la categoria dei modelli.

3. Contributi Chiave

A. Semantica delle Teorie Stratificate

Il paper stabilisce una corrispondenza precisa tra le teorie sintattiche e strutture categoriali specifiche:

1. Teorie Opfibrational $\leftrightarrow$ Opfibrations con Monoidi Indicizzati: I modelli sono opfibrations split dove la categoria base ha una struttura di monoidi indicizzati (che implica che la base è cartesiana monoidale).
2. Teorie Fibrational $\leftrightarrow$ Fibrations con Comonoidi Indicizzati: Il duale categorico del caso precedente.
3. Teorie Deflational $\leftrightarrow$ Deflazioni Monoidali: I modelli sono deflazioni monoidali split verso la 2-categoria a zigzag della categoria libera con monoidi indicizzati. Questa è la struttura più generale e potente.

B. Introduzione delle Deflazioni

Un contributo originale significativo è la definizione di deflazione monoidale.

• Le deflazioni permettono di trattare le traduzioni bidirezionali tra livelli senza dover specificare manualmente le equazioni di adjunzione per ogni generatore.
• La struttura a zigzag della categoria base ($Zg(X)$) cattura automaticamente le relazioni di adjunzione tra i confini funtoriali diretti e inversi.
• Questo risolve il problema di come formalizzare l'interazione tra i confini funtoriali in entrambe le direzioni in modo simmetrico e assiomatico.

C. Risultati di Completezza

Gli autori dimostrano che:

• Il modello termico (costruito quotando i termini per le equazioni strutturali) è il oggetto iniziale nella fibra dei modelli.
• Esiste un'equivalenza tra la categoria dei modelli di una teoria $T$ e la categoria dei funtori dal modello termico $F(T)$ alla categoria dei modelli (es. $MonOpFib_{sp}$ o $MonDefl_{sp}$).
• Questo garantisce che un'equazione è derivabile nella teoria sintattica se e solo se vale in tutti i modelli semantici (completezza).

D. Relazione con le Categorie Monoidali Indicizzate

Il lavoro chiarisce il rapporto tra le teorie stratificate e le categorie monoidali indicizzate (opindexed monoidal categories).

• Le teorie opfibrational corrispondono esattamente alle categorie monoidali indicizzate (tramite la costruzione di Grothendieck).
• Le teorie deflational sono una generalizzazione: mentre le categorie monoidali indicizzate catturano solo la direzione "in avanti", le deflazioni catturano anche la direzione "indietro" e le trasformazioni 2-dimensionali non banali tra morfismi, che le categorie indicizzate standard non riescono a distinguere adeguatamente.

4. Risultati Principali

1. Teorema 4.16: Equivalenza tra le opfibrations split con monoidi su una base $X$ e le opfibrations split con monoidi indicizzati sulla categoria libera $Fim(X)$.
2. Teorema 5.14: Equivalenza tra le deflazioni monoidali split minime e le opfibrations split con monoidi indicizzati. Questo collega la nuova semantica delle deflazioni alle strutture esistenti.
3. Teoremi 6.10 e 6.22: Costruzione dell'adjunzione libera-forgetful per le teorie opfibrational e deflational, dimostrando che i modelli liberi sono costruiti quotando i termini per le equazioni strutturali.
4. Corollario 6.23: Caratterizzazione dei modelli delle teorie deflational come categorie di modelli liberi rispetto alle deflazioni monoidali split.

5. Significato e Impatto

• Unificazione Categorical: Il lavoro unifica concetti apparentemente distinti (fibrations, indexed categories, adjunctions) in un unico quadro coerente per la semantica dei diagrammi a stringa stratificati.
• Gestione della Bidirezionalità: Fornisce il primo quadro semantico rigoroso per le traduzioni bidirezionali tra livelli di astrazione, superando i limiti delle sole categorie indicizzate. Le "deflazioni" offrono un dominio semantico naturale per le teorie che richiedono un flusso di informazioni in entrambe le direzioni.
• Fondamenti per Applicazioni: Poiché le teorie stratificate sono state motivate da applicazioni in chimica, fisica e informatica (Parte I), questo lavoro fornisce la base matematica solida necessaria per implementare strumenti di verifica, ottimizzazione e traduzione automatica tra diversi livelli di astrazione di sistemi complessi.
• Estendibilità: Il framework è progettato per essere esteso a casi non-strict (non rigorosi) e a strutture monoidali globali, aprendo la strada a future ricerche su diagrammi a stringa più complessi.

In sintesi, il paper risolve il problema della semantica per le teorie monoidali stratificate introducendo le "deflazioni monoidali" come struttura chiave, dimostrando la completezza del sistema e collegandolo profondamente alla teoria delle fibrations e delle categorie indicizzate.