Endpoint Sufficiency Behavioral Quotients

Sintesi Tecnica: Quando la dimenticanza della provenienza è lecita?

Problema
I sistemi generativi producono spesso oggetti che possono essere rappresentati a diversi livelli di astrazione. Una rappresentazione cattura solo l' "endpoint visibile" (l'oggetto finale), mentre un'altra conserva la piena "provenienza" (ascendenza, eventi di fusione, strutture di dipendenza). Sebbene le rappresentazioni dell'endpoint siano più piccole, esse rischiano di essere descrizioni di stato false se le leggi di ammissibilità del sistema dipendono dalla linea di discendenza. Il problema centrale affrontato è determinare esattamente quando le informazioni di provenienza possono essere rimosse in sicurezza senza alterare il comportamento futuro lecito del sistema. Nello specifico, il saggio si chiede: quando una proiezione dell'endpoint conserva informazioni sufficienti per determinare le transizioni lecite, e quale sia la quantità massima di provenienza che può essere scartata?

Il saggio contesta l'assunto informale secondo cui la "sufficienza dell'endpoint" sia un concetto unico e uniforme. Dimostra che tale nozione varia a seconda del livello di osservazione: se ci si cura solo delle regole immediatamente abilitate, delle sequenze finite di etichette di regole (tracce), o della piena struttura di ramificazione delle possibilità future.

Metodologia
L'autore formalizza il problema utilizzando i Sistemi di Transizione Generativa Legali (LGTS). Un LGTS è definito da una tupla $T = (S, \Sigma, \to, U, X, \cong_X)$, dove:

• $S$ è un insieme di occorrenze decorate con provenienza.
• $\Sigma$ è un insieme di etichette di regole.
• $\to$ è la relazione di transizione etichettata legale.
• $U: S \to X$ è una proiezione dell'endpoint che mappa le occorrenze su oggetti visibili.
• $\cong_X$ è una relazione di equivalenza sugli oggetti visibili.

Lo studio analizza la relazione tra la relazione di equivalenza dell'endpoint ($\equiv_U$, dove $s \equiv_U t \iff U(s) \cong_X U(t)$) e varie equivalenze comportamentali. L'analisi procede attraverso tre distinti livelli di osservazione:

1. Sufficienza di Abilitazione: preservare l'insieme delle etichette di regole immediatamente disponibili.
2. Sufficienza di Traccia: preservare l'insieme di tutte le tracce finite di etichette di regole.
3. Sufficienza di Quoziente (Branching): preservare la struttura di transizione di ramificazione rispetto all'equivalenza dell'endpoint.

Il saggio impiega strumenti standard della semantica dei processi, inclusi l'equivalenza di traccia, la bisimulazione forte, la coinduzione e il raffinamento delle partizioni, applicati specificamente al confine tra endpoint e provenienza.

Contributi Chiave e Risultati

1. Una Gerarchia a Tre Livelli Rigida
Il saggio stabilisce che i tre livelli di sufficienza sono distinti e formano una gerarchia rigida:
$$\text{Sufficienza di Quoziente} \implies \text{Sufficienza di Traccia} \implies \text{Sufficienza di Abilitazione}$$

• La Sufficienza di Abilitazione è la più debole; richiede solo che gli endpoint equivalenti abbiano lo stesso insieme di mosse successive abilitate.
• La Suffienza di Traccia richiede che gli endpoint equivalenti generino lo stesso insieme di sequenze finite di etichette di regole.
• La Sufficienza di Quoziente è la più forte; richiede che l'insieme delle classi di endpoint raggiungibili per qualsiasi etichetta dipenda solo dalla classe dell'endpoint corrente, non dalla specifica storia di provenienza.

2. Criteri Esatti di Sufficienza
Il saggio fornisce criteri matematici precisi per determinare quando una proiezione dell'endpoint è sufficiente a ciascun livello:

• Livello di Traccia: la proiezione è sufficiente per le tracce se e solo se l'equivalenza dell'endpoint è un sottoinsieme dell'equivalenza di traccia ($\equiv_U \subseteq \equiv_{tr}$).
• Livello di Branching: la proiezione è sufficiente per il quoziente se e solo se l'equivalenza dell'endpoint è una equivalenza di bisimulazione forte. Ciò significa che per ogni coppia di stati equivalenti per l'endpoint, ogni transizione da uno può essere corrisposta da una transizione dall'altro verso uno stato che sia anch'esso equivalente per l'endpoint.

3. Riparazioni Canoniche e Massima Dimenticanza
Quando l'equivalenza dell'endpoint grezza non è sufficiente, il saggio propone due "riparazioni canoniche" che identificano il più grossolano possibile raffinamento degli stati che preserva il comportamento desiderato rispettando gli endpoint visibili:

• Per il Tempo Lineare (Tracce): la relazione $E^U_{tr} = \equiv_U \cap \equiv_{tr}$ è la più grande relazione di equivalenza che rispetta gli endpoint e preserva le tracce finite. Identifica esattamente quelle occorrenze equivalenti per l'endpoint le cui potenzialità future sono indistinguibili come tracce di etichette di regole.
• Per il Tempo di Branching (Quozienti Esatti): la relazione $\approx_U$, definita come l'unione di tutte le bisimulazioni forti che rispettano l'endpoint, è la più grande bisimulazione forte che rispetta l'endpoint. Il sistema quoziente $T / \approx_U$ è il quoziente di branching esatto massimamente grossolano.
  • Proprietà Universale: ogni altro quoziente esatto che rispetta l'endpoint raffina questo quoziente canonico. Pertanto, $\approx_U$ rappresenta la quantità massima di provenienza che può essere dimenticata mantenendo una semantica di branching esatta.

4. Computazione Algoritmica
Per sistemi finiti, il saggio descrive una procedura di raffinamento delle partizioni terminante per computare $\approx_U$. L'algoritmo inizializza con la partizione delle classi di equivalenza dell'endpoint e la raffina iterativamente basandosi sulle "firme" dei blocchi successori (l'insieme dei blocchi raggiungibili per ogni etichetta). La procedura si stabilizza nella partizione corrispondente a $\approx_U$.

5. Applicazione alla Generazione Ricorsiva-Ricombinante Annidata (NRRG)
Il saggio applica questi risultati a un quadro specifico di NRRG decorato con provenienza. Presenta un caso testimone in cui due occorrenze ($e_G$ e $e_H$) condividono lo stesso endpoint di grafo visibile ($I \to A \to B$) ma differiscono nella loro ascendenza ricombinante.

• In $e_G$, l'ascendenza permette una regola di riscrittura che tocca il confine ($R_B$).
• In $e_H$, l'ascendenza proibisce $R_B$.
• Risultato: l'algoritmo di raffinamento delle partizioni separa $e_G$ ed $e_H$ nel primo round perché i loro insiemi di successori abilitati differiscono. Ciò dimostra che l'isomorfismo dell'endpoint non implica l'equivalenza comportamentale, anche al livello di abilitazione, e che la procedura di raffinamento proposta identifica correttamente la distinzione necessaria.

Significato e Rivendicazioni
Il saggio sostiene di sostituire la richiesta "tutto o niente" di dover o mantenere tutta la provenienza o scartarla interamente con un criterio esatto per la dimenticanza lecita.

• Residuo Operativo: la differenza tra le classi grezze dell'endpoint e le classi raffinate ($\approx_U$ o $E^U_{tr}$) costituisce il "residuo operativo" della provenienza — l'informazione storica che rimane attiva nello spazio delle transizioni future.
• Esattezza dell'Astrazione: il lavoro inquadra il problema dell'astrazione non semplicemente come correttezza (sovra-approssimazione), ma come esattezza per una semantica scelta. Un quoziente grezzo che unisce gli stati senza controllare la bisimulazione può creare comportamenti (inflazione) che non sono leciti per specifiche occorrenze.
• Agnosticismo del Dominio: i risultati sono presentati come criteri formali applicabili a qualsiasi sistema in cui l'ammissibilità dipenda dalla linea di discendenza (ad esempio, stati di software, strumenti legali, affermazioni scientifiche), purché il sistema possa essere modellato come un sistema di transizione etichettato con una proiezione dell'endpoint.

Il saggio conclude che la provenienza può essere cancellata esattamente attraverso quelle distinzioni di occorrenza che non alterano la scelta della semantica futura lecita. Ciò che rimane dopo la massima cancellazione sicura non è la decorazione storica, ma il vero stato generativo.