Ordered Adjoint Logic (Extended Version)

Sintesi Tecnica di "Ordered Adjoint Logic"

Enunciato del Problema
Le logiche ordinate e i sistemi di tipi sono essenziali per applicazioni che spaziano dalla linguistica computazionale all'applicazione di protocolli di sicurezza, dove l'ordine di utilizzo delle risorse è significativo. Nella maggior parte delle formulazioni, i tipi ordinati sono anche lineari, richiedendo che le risorse siano utilizzate esattamente una volta. Sebbene lavori precedenti di Kanovich et al. abbiano indagato calcoli che rilassano questo vincolo tramite subesponenziali all'interno di una logica lineare ordinata, questo approccio si basa su una "modalità base" in cui avvengono tutte le inferenze. Per le logiche ordinate, questa modalità base deve proibire tutte le regole strutturali (indebolimento, contrazione, scambio), costringendo le applicazioni a passare frequentemente dentro e fuori da questa modalità restrittiva. Inoltre, i sistemi subesponenziali esistenti non esplorano appieno la possibilità di proprietà strutturali unilaterali (ad esempio, mobilità a sinistra senza mobilità a destra). Gli autori mirano a generalizzare questi framework per supportare un preordine di modalità con proprietà strutturali variabili e di alta granularità — incluso il controllo indipendente su indebolimento, contrazione a sinistra/destra e mobilità a sinistra/destra — senza fare affidamento su una singola modalità base restrittiva.

Metodologia
Gli autori introducono la Ordered Adjoint Logic, un sistema che combina la flessibilità strutturale delle modalità adjoint con i vincoli di ordinamento delle logiche ordinate. La metodologia procede in due fasi principali:

1. Formulazione del Calcolo dei Sequenti:
   Gli autori definiscono un calcolo dei sequenti in cui gli antecedenti sono sequenze ordinate di ipotesi etichettate. Le regole strutturali non sono globali, ma sono governate da un preordine di modalità ($k \geq m$). Ogni modalità $m$ è associata a un insieme di proprietà strutturali $\sigma(m) \subseteq \{W, C, M_{\leftarrow}, M_{\rightarrow}\}$ (Indebolimento, Contrazione, Mobilità a Sinistra, Mobilità a Destra).

   • Modalità di Spostamento: Invece di una modalità base, il sistema utilizza modalità di spostamento ($\downarrow^k_m$ e $\uparrow^m_l$) per passare dal ragionamento a diverse modalità. Questi spostamenti sono derivati dalla logica adjoint di Benton ma generalizzati per gestire contesti ordinati.
   • Regole Strutturali: Gli autori decompongono la mobilità e la contrazione in varianti unilaterali. Le regole di mobilità permettono a una singola proposizione di spostarsi arbitrariamente a sinistra o a destra all'interno della sequenza degli antecedenti, a condizione che la modalità della proposizione ammetta la corrispondente mobilità direzionale. La contrazione è permessa in modo non locale (unendo duplicati non adiacenti) per garantire l'eliminazione del taglio, distinguendosi dalla contrazione locale nella logica lineare standard.
   • Connettivi Logici: Il linguaggio include implicazioni ordinate ($\multimap$ e $\multimap$), congiunzioni fuse e attorcigliate, e spostamenti. Le regole sono parametriche nelle loro modalità, con condizioni specifiche che garantiscono la preservazione dell'indipendenza delle modalità (ad esempio, $k \geq m \geq r$) quando si leggono le regole dalla conclusione alle premesse.

2. Deduzione Naturale e Decidibilità:
   Gli autori passano a una formulazione in deduzione naturale in cui le regole strutturali sono implicite, mirando a una fondazione adatta ai linguaggi di programmazione.

   • Esplicito vs Implicito: Inizialmente, presentano un sistema con regole strutturali esplicite per colmare il divario con il calcolo dei sequenti. Successivamente, definiscono un sistema in cui le regole strutturali (indebolimento, contrazione, mobilità) sono implicite.
   • Algoritmo per la Verifica delle Dimostrazioni: Per affrontare la non-determinismo introdotto dalle regole strutturali implicite (in particolare l'applicazione illimitata dell'indebolimento e il posizionamento delle variabili nelle regole di eliminazione), gli autori definiscono un giudizio di "forma normale" ($\Omega \gg_{\Gamma, r} \Omega_{nf}$). Questo algoritmo calcola l'insieme di tutte le possibili forme normali (contesti senza variabili ripetute) per un dato contesto $\Omega$, insieme di ipotesi $\Gamma$ e modalità $r$.
   • Giudizi Basati su Insiemi: Le regole di deduzione naturale sono elevate per operare su insiemi di contesti in forma normale ($\Xi$). Ad esempio, l'introduzione della congiunzione calcola il prodotto cartesiano degli insiemi di contesti, mentre l'intersezione è utilizzata per le regole che richiedono l'accordo dei contesti (come la congiunzione additiva).

Contributi Chiave

• Logica Adjoint Generalizzata: Il documento generalizza la logica adjoint a contesti ordinati, introducendo un preordine di modalità in cui ogni modalità controlla indipendentemente indebolimento, contrazione e mobilità unilaterale.
• Proprietà Strutturali Unilaterali: Il sistema modella esplicitamente e dimostra proprietà per la mobilità e la contrazione a sinistra e a destra come proprietà strutturali separate e indipendenti, una caratteristica anticipata ma non esplorata nei lavori precedenti sui subesponenziali.
• Eliminazione del Taglio: Gli autori dimostrano che il calcolo dei sequenti ordered adjoint ammette l'eliminazione del taglio (tramite multicut) e l'eliminazione dell'identità, stabilendo il sistema come un framework logico ben comportato.
• Decidibilità della Verifica delle Dimostrazioni: Il documento fornisce un sistema di deduzione naturale con regole strutturali implicite e dimostra che la verifica delle dimostrazioni per questo sistema è decidibile. Ciò è ottenuto costruendo un algoritmo terminante che calcola l'insieme dei contesti in forma normale.

Risultati

• Correttezza Teorica: Il calcolo dei sequenti è mostrato come soddisfacente l'eliminazione del taglio e dell'identità. Il sistema di deduzione naturale è dimostrato essere corretto e completo rispetto al calcolo dei sequenti.
• Decidibilità: L'algoritmo per il calcolo delle forme normali ($NF_{\Gamma, r}(\Omega)$) è dimostrato terminante. Di conseguenza, il problema della verifica delle dimostrazioni nel sistema di deduzione naturale implicito è decidibile.
• Sussunzione Substrutturale: I risultati implicano la decidibilità della sussunzione substrutturale, un componente fondamentale degli algoritmi di controllo dei tipi per linguaggi come QRTT (che utilizza la semantica di Kripke con mondi espliciti).

Significato e Affermazioni
Gli autori affermano che la Ordered Adjoint Logic fornisce una fondazione adatta per un linguaggio di programmazione adjoint espressivo o un framework logico. Disaccoppiando le proprietà strutturali da una singola modalità base e utilizzando spostamenti adjoint, il sistema permette un ragionamento nativo in varie discipline (lineare, ordinata, illimitata) con un passaggio senza soluzione di continuità. La decidibilità della verifica delle dimostrazioni con regole strutturali implicite è evidenziata come un passo critico verso l'implementazione di type checker bidirezionali per linguaggi di programmazione funzionale in grado di gestire proprietà strutturali di alta granularità del codice. Il documento nota che, sebbene la procedura decisionale sia stabilita, l'efficienza pratica (ad esempio, evitare la complessità esponenziale derivante da indebolimenti non necessari) rimane un argomento per future ottimizzazioni. Il lavoro è posizionato come una generalizzazione diretta della logica ordinata subesponenziale di Kanovich et al. e un'estensione dei tipi adjoint di Jang et al. per includere l'ordine.