2025-11-11T14:52:08.882681

Non-commutative linear logic fragments with sub-context-free complexity

Nishimiya, Taniguchi
We present new descriptive complexity characterisations of classes REG (regular languages), LCFL (linear context-free languages) and CFL (context-free languages) as restrictions on inference rules, size of formulae and permitted connectives in the Lambek calculus; fragments of the intuitionistic non-commutative linear logic with direction-sensitive implication connectives. Our identification of the Lambek calculus fragments with proof complexity REG and LCFL is the first result of its kind. We further show the CFL complexity of one of the strictly `weakest' possible variants of the logic, admitting only a single inference rule. The proof thereof, moreover, is based on a direct translation between type-logical and formal grammar and structural induction on provable sequents; a simpler and more intuitive method than those employed in prior works. We thereby establish a clear conceptual utility of the Cut-elimination theorem for comparing formal grammar and sequent calculus, and identify the exact analogue of the Greibach Normal Form in Lambek grammar. We believe the result presented herein constitutes a first step toward a more extensive and richer characterisation of the interaction between computation and logic, as well as a finer-grained complexity separation of various sequent calculi.
academic

Frammenti di logica lineare non-commutativa con complessità sub-context-free

Informazioni Fondamentali

  • ID Articolo: 2511.02348
  • Titolo: Non-commutative linear logic fragments with sub-context-free complexity
  • Autori: Yusaku Nishimiya (University of Illinois Springfield & RIKEN AIP), Masaya Taniguchi (RIKEN AIP)
  • Classificazione: cs.LO (Logica in Informatica), cs.CC (Complessità Computazionale), cs.FL (Linguaggi Formali), math.LO (Logica Matematica)
  • Data di Pubblicazione: 4 novembre 2025 (preprint arXiv)
  • Link Articolo: https://arxiv.org/abs/2511.02348

Riassunto

Questo articolo propone nuove caratterizzazioni di complessità descrittiva per tre classi di linguaggi: linguaggi regolari (REG), linguaggi context-free lineari (LCFL) e linguaggi context-free (CFL), ottenute attraverso restrizioni sulle regole di inferenza, sulla dimensione delle formule e sui connettivi ammessi nel calcolo di Lambek. Il calcolo di Lambek è un frammento della logica lineare non-commutativa intuizionista con implicazioni sensibili alla direzione. Gli autori identificano per la prima volta frammenti del calcolo di Lambek con complessità di prova REG e LCFL, e dimostrano la complessità CFL per le varianti logiche "più deboli" che ammettono una sola regola di inferenza. Le dimostrazioni si basano su traduzioni dirette tra grammatiche di logica di tipo e grammatiche formali e su induzione strutturale su sequenti provabili, utilizzando metodi più semplici e intuitivi rispetto ai lavori precedenti.

Contesto di Ricerca e Motivazione

Contesto del Problema

  1. Studio della Logica Sottostrutturale: I teorici della prova studiano la logica sottostrutturale per comprendere gli effetti dell'ammissione o dell'eliminazione di regole strutturali sulle proprietà dei sistemi di prova, tipicamente presentati in forma di calcolo dei sequenti.
  2. Significato Computazionale della Logica Lineare: La logica lineare (LL) limita le regole di contrazione e indebolimento, rendendo le prove più consapevoli delle risorse rispetto alla logica classica, e quindi più rilevanti dal punto di vista computazionale. È noto che MALL è PSPACE-completo e MLL è NP-completo.
  3. Potenza Espressiva del Calcolo di Lambek: Il calcolo di Lambek L è il frammento intuizionista, non-commutativo e moltiplicativo di LL, con implicazioni sensibili alla direzione. Pentus ha provato l'equivalenza tra grammatiche di Lambek e grammatiche context-free, ma non sono stati ancora identificati frammenti di L corrispondenti a classi di linguaggi inferiori nella gerarchia di Chomsky.

Motivazione della Ricerca

La ricerca esistente conosce poco sulla complessità computazionale dei frammenti "più deboli" di LL, in particolare mancano caratterizzazioni di frammenti del calcolo di Lambek corrispondenti a linguaggi regolari e linguaggi context-free lineari. Questo articolo mira a colmare questa lacuna, stabilendo corrispondenze precise tra le restrizioni sulla dimensione delle formule e sulla direzionalità e i cambiamenti nella potenza espressiva delle grammatiche.

Contributi Fondamentali

  1. Prima Identificazione: Identificazione per la prima volta di frammenti del calcolo di Lambek con complessità di prova REG e LCFL
  2. Complessità CFL della Variante Più Debole: Dimostrazione che le varianti logiche che ammettono una sola regola di inferenza hanno complessità CFL
  3. Metodo di Traduzione Diretta: Fornitura di traduzioni dirette tra grammatiche di logica di tipo e grammatiche formali con metodi di induzione strutturale
  4. Applicazione del Teorema di Eliminazione del Taglio: Stabilimento dell'utilità concettuale del teorema di eliminazione del taglio nel confronto tra grammatiche formali e calcolo dei sequenti
  5. Analogo della Forma Normale di Greibach: Identificazione dell'esatto analogo della forma normale di Greibach nelle grammatiche di Lambek

Dettagli del Metodo

Definizione del Compito

Questo articolo studia come caratterizzare classi di linguaggi formali di diversa complessità attraverso restrizioni sulle regole di inferenza, sulla dimensione delle formule e sui connettivi del calcolo di Lambek. Il compito specifico è stabilire relazioni di equivalenza tra frammenti del calcolo di Lambek e classi di linguaggi nella gerarchia di Chomsky.

Quadro Teorico

Definizione del Calcolo di Lambek

Il calcolo di Lambek L contiene:

  • Assioma: α → α
  • Regola del Taglio: da Γ,α,Θ → β e Δ → α si deduce Γ,Δ,Θ → β
  • Sei Regole di Inferenza: coinvolgenti i tre connettivi binari /, \ e ·

Concetti Chiave

  1. Grado di Tipo d(α): Numero di occorrenze distinte di connettivi nel tipo α
  2. Insiemi di Tipi: Tp(/) denota l'insieme di tipi contenenti solo il connettivo /, Tpn denota l'insieme di tipi con grado ≤ n
  3. Grammatica di Lambek: Quadrupla (Pr, V, SG, f), dove f è una funzione di assegnazione di tipi

Teoremi Fondamentali

Teorema 2 (Risultato Principale): I seguenti tre coppie di frammenti di grammatiche di Lambek e grammatiche formali hanno potenza espressiva equivalente:

  • Grammatiche L(/ →) con Tp(/) ⇔ CFG
  • Grammatiche L(/ →, \ →) con Tp1(/, ) ⇔ LCFG
  • Grammatiche L(/ →) con Tp1(/) ⇔ REG

Strategia di Dimostrazione

Condizioni di Riducibilità (Lemma 3)

Per una sequenza di tipi non-vuota Γ in Tp(/), L(/ →) ⊢ Γ → SG se e solo se:

  1. Γ = α,Δ1,...,Δn, dove α ha la forma (···((S/βn)/βn-1)/···)/β1
  2. Per tutti 1≤k≤n, L(/ →) ⊢ Δk → βk

Metodo di Costruzione

  1. Da CFG a Grammatica di Lambek: Assumendo la forma normale di Greibach, convertire le regole di produzione A → aB1···Bn in assegnazioni di tipi (···((A/Bn)/Bn-1)/···)/B1 ∈ f(a)
  2. Da Grammatica di Lambek a CFG: Convertire le assegnazioni di tipi (···((α/βn)/βn-1)/···)/β1 ∈ f(a) in regole di produzione α → aβ1β2···βn

Configurazione Sperimentale

Questo articolo è una ricerca puramente teorica che non comporta verifiche sperimentali, ma stabilisce relazioni di equivalenza attraverso dimostrazioni matematiche rigorose.

Metodi di Dimostrazione

  1. Induzione Strutturale: Induzione strutturale su sequenti provabili
  2. Eliminazione del Taglio: Utilizzo del teorema di Gentzen per garantire l'esistenza di prove senza taglio
  3. Costruzione Bidirezionale: Dimostrazione separata dell'equivalenza dei linguaggi in entrambe le direzioni

Risultati Sperimentali

Risultati Principali

Proposizione 4 (Linguaggi Context-Free)

Le grammatiche di Lambek basate su L(/ →) con Tp(/) riconoscono esattamente i linguaggi context-free senza stringa vuota.

Punti Chiave della Dimostrazione:

  • CFG → Grammatica L(/ →): Utilizzo della forma normale di Greibach, costruzione delle corrispondenti assegnazioni di tipi
  • Grammatica L(/ →) → CFG: Conversione delle assegnazioni di tipi in regole di produzione, dimostrazione dell'equivalenza dei linguaggi per induzione

Proposizione 6 (Linguaggi Context-Free Lineari)

Le grammatiche L(/ →, \ →) ristrette a Tp1(/, ) riconoscono esattamente i linguaggi lineari.

Metodo di Costruzione:

  • A/B ∈ f(a) ⟺ A → aB ∈ P (lineare a destra)
  • B\A ∈ f(a) ⟺ A → Ba ∈ P (lineare a sinistra)
  • A ∈ f(a) ⟺ A → a ∈ P (terminale)

Corollario 7 (Linguaggi Regolari)

Le grammatiche L(/ →) ristrette a Tp1(/) riconoscono esattamente i linguaggi regolari.

Scoperte Chiave

  1. Importanza della Direzionalità: Le grammatiche L(/ →) unidirezionali corrispondono a grammatiche regolari a destra, mentre le grammatiche L(/ →, \ →) bidirezionali corrispondono a grammatiche lineari
  2. Effetto delle Restrizioni di Grado: Le restrizioni sul grado di tipo a 1 corrispondono naturalmente alla (bi)linearità delle regole di produzione
  3. Analogo della Forma Normale di Greibach: Le grammatiche L(/ →) unidirezionali possono essere viste come l'analogo teorico-dimostrativo della forma normale di Greibach

Lavori Correlati

Ricerca sulla Complessità della Logica Lineare

  • MALL: PSPACE-completo LMSS92
  • MLL: NP-completo Kan91
  • Calcolo di Lambek: NP-completo Pen06

Grammatiche di Lambek e Grammatiche Formali

  • Congettura di Chomsky: Equivalenza tra grammatiche di logica di tipo e grammatiche context-free Cho63
  • Risultato di Pentus: Conferma della congettura di Chomsky, dimostrazione che le grammatiche di Lambek senza prodotto rimangono context-free Pen93, Pen97
  • Abrusci: Stabilimento della connessione tra il calcolo di Lambek e la logica lineare Abr90

Conclusioni e Discussione

Conclusioni Principali

  1. Caratterizzazione Precisa: Stabilimento di corrispondenze precise tra frammenti del calcolo di Lambek e tre importanti classi di linguaggi nella gerarchia di Chomsky
  2. Metodi Semplificati: Fornitura di metodi di dimostrazione più diretti e intuitivi rispetto ai lavori precedenti
  3. Intuizioni Teoriche: Rivelazione dei legami profondi tra le regole di inferenza logica e le regole di produzione delle grammatiche formali

Limitazioni

  1. Restrizioni di Ambito: Considerazione di solo alcune classi di linguaggi nella gerarchia di Chomsky
  2. Gestione della Stringa Vuota: Le grammatiche costruite non includono la stringa vuota
  3. Applicazioni Pratiche: Principalmente risultati teorici, il valore applicativo pratico rimane da esplorare ulteriormente

Direzioni Future

Gli autori propongono tre promettenti direzioni di ricerca:

  1. Ricerca di complessità descrittiva a grana fine di altri frammenti di logica lineare (non-commutativa)
  2. Identificazione di grammatiche di Lambek equivalenti a linguaggi privi di stelle, linguaggi debolmente sensibili al contesto, sistemi di Lindenmayer, ecc.
  3. Interazione tra la semantica della logica lineare e le caratterizzazioni della teoria geometrica dei gruppi dei linguaggi formali

Valutazione Approfondita

Punti di Forza

  1. Innovazione Teorica: Prima stabilimento di corrispondenze tra REG, LCFL e frammenti del calcolo di Lambek, colmamento di un importante vuoto teorico
  2. Semplicità del Metodo: Il metodo di dimostrazione basato su traduzioni dirette e induzione strutturale è più semplice e intuitivo rispetto ai lavori precedenti
  3. Completezza dei Risultati: Fornitura di caratterizzazioni complete di tre importanti classi di linguaggi, formazione di un quadro teorico unificato
  4. Chiarezza Concettuale: L'applicazione del teorema di eliminazione del taglio e l'analogo della forma normale di Greibach forniscono intuizioni teoriche profonde

Insufficienze

  1. Limitazioni Applicative: Come ricerca puramente teorica, manca la discussione di scenari di applicazione pratica
  2. Ambito Limitato: Coinvolge solo parte della gerarchia di Chomsky, non affronta classi di linguaggi di livello superiore
  3. Dettagli Tecnici: Alcuni passaggi di dimostrazione potrebbero essere più dettagliati, in particolare l'implementazione specifica dell'induzione strutturale

Impatto

  1. Contributo Teorico: Fornitura di nuovi strumenti teorici per la ricerca interdisciplinare tra logica sottostrutturale e teoria dei linguaggi formali
  2. Valore Metodologico: Il metodo di traduzione diretta potrebbe essere applicabile allo studio di corrispondenze tra altri sistemi logici e modelli computazionali
  3. Sviluppo della Disciplina: Promozione della fusione ulteriore tra logica e teoria della complessità computazionale

Scenari Applicabili

  1. Informatica Teorica: Fornitura di nuovi metodi per lo studio della complessità computazionale dei sistemi logici
  2. Teoria dei Linguaggi Formali: Fornitura di nuove prospettive per la caratterizzazione logica delle classi di linguaggi
  3. Elaborazione del Linguaggio Naturale: Possibile fornitura di fondamenti teorici per l'analisi sintattica basata su logica di tipo
  4. Ricerca sulla Teoria della Prova: Fornitura di strumenti tecnici per la ricerca ulteriore della logica sottostrutturale

Riferimenti Bibliografici

L'articolo cita i riferimenti chiave del campo, inclusi:

  • Lavori fondamentali di Girard sulla logica lineare Gir87
  • Lavori originali di Lambek Lam58
  • Importanti risultati di Pentus sulla potenza espressiva delle grammatiche di Lambek Pen93, Pen97
  • Risultati classici sulla complessità della logica lineare LMSS92, Kan91

Questo articolo fornisce importanti contributi teorici alla ricerca interdisciplinare tra logica sottostrutturale e teoria dei linguaggi formali. Attraverso l'stabilimento di corrispondenze precise, non solo risolve problemi teorici di lunga data, ma pone anche solide fondamenta per ricerche ulteriori. I suoi metodi di dimostrazione concisi e le intuizioni teoriche profonde lo rendono un importante progresso nel campo.