Fondamenti formali

Scopo e ambito

Questo documento fornisce il fondamento matematico formale del sistema di corrispondenza e dispatch degli URN di CapDAG. Definisce:

• Il dominio semantico dei tagged URN
• La relazione di base e i predicati derivati
• La costruzione del cap URN come prodotto
• La relazione di dispatch
• Il ranking come livello di policy separato
• Gli obblighi di prova e le proprietà di coerenza

Questo è il riferimento formale autorevole. I dettagli di implementazione si trovano nei documenti numerati della specifica (01–11).

Il problema centrale

CapDAG usa gli URN come descrittori semantici strutturati, non come semplici nomi. Il sistema deve rispondere a domande distinte:

Un singolo accepts o conforms_to non può rispondere a tutte, perché i cap URN hanno una varianza mista lungo quattro coordinate strutturali.

Dominio di base

Sia U l’insieme dei tagged URN normalizzati.

Ogni elemento u ∈ U ha:

• Una rappresentazione canonica normalizzata
• Una semantica ben definita di wildcard e valori
• Un punteggio di specificità
• Una relazione semantica di base

Relazione primitiva

Si definisce una relazione binaria su U:

⪯ ⊆ U × U

Con il significato:

a ⪯ b  sse  a è almeno tanto specifico quanto b

In modo equivalente: b è almeno tanto generale quanto a.

Orientamento del reticolo:

• In basso = più specifico (più vincolato)
• In alto = più generico (meno vincolato)

Predicati derivati

Per a, b ∈ U:

Accettazione

accepts(a, b)  :⟺  b ⪯ a

Significato: a sussume b. Il pattern a accetta l’istanza b.

Conformità

conforms_to(a, b)  :⟺  a ⪯ b

Significato: a soddisfa o raffina b. L’istanza a è conforme al pattern b.

Comparabilità

is_comparable(a, b)  :⟺  a ⪯ b ∨ b ⪯ a

Significato: uno sussume l’altro. Si trovano sulla stessa catena di specializzazione.

Equivalenza

is_equivalent(a, b)  :⟺  a ⪯ b ∧ b ⪯ a

Significato: a e b denotano la stessa posizione semantica.

Funzione di specificità

Si definisce:

spec_U : U → ℕ

tale che una specificità maggiore produca un punteggio maggiore.

Questa funzione si usa solo per il ranking, non per la validità semantica primaria.

Obblighi semantici su U

Il sistema assume che U, ⪯ e spec_U siano ben definiti da ciò che ciascuna forma di tag significa (l’insieme degli stati in cui può trovarsi la sua chiave), con ⪯ come inclusione di questi significati (Predicati). Queste proprietà sono dimostrate, non assunte, in tagged-urn/formal.

Riflessività

∀u ∈ U,  u ⪯ u

Transitività

∀a,b,c ∈ U,  (a ⪯ b ∧ b ⪯ c) ⟹ a ⪯ c

Se queste valgono, ⪯ è un preordine su U.

Antisimmetria (a meno della normalizzazione)

(a ⪯ b ∧ b ⪯ a) ⟹ a ≡ b

Se vale anche questa, le classi di equivalenza di U formano un ordine parziale.

I cap URN come prodotto

Un cap URN è un prodotto a quattro coordinate sul dominio dei tagged URN:

C = U × U × U × E

Per c ∈ C, si scrive:

c = (i, o, y, e)

dove:

• i = dimensione di input (il valore del tag in)
• o = dimensione di output (il valore del tag out)
• y = dimensione dei tag della cap diversi dalla direzione
• e = coordinata dell’effetto

Le dimensioni in, out e y riusano il dominio di base U e la relazione ⪯. La coordinata effect è un asse strutturale con corrispondenza esatta, a meno che la richiesta non usi esplicitamente la forma non vincolata ?effect.

Media URN distinti: top e unità

Due media URN hanno ruoli distinti negli assi direzionali di C. Sono elementi formalmente distinti di U; il resto della specifica si basa su questa distinzione.

Top (media:). Il massimo dell’ordine dei media URN rispetto a ⪯:

∀ m ∈ MediaUrn,    m ⪯ media:

Una specifica direzionale di una cap impostata a media: è il tipo top, letto come “qualsiasi A”: una cap che accetta media: accetta qualsiasi cosa, e una che fornisce media: non promette alcun output particolare.

Il tipo top non è la stessa cosa di un lato lasciato aperto in una richiesta. Una richiesta è una domanda sulle cap, e un lato che essa non stabilisce è un’incognita (“un qualche A”, non “qualsiasi A”) (Dispatch: l’incognita non è “qualsiasi cosa”).

Unità (media:void). Una foglia che porta il tag marcatore void. È atomica: il parser rifiuta qualsiasi combinazione di void con un altro tag:

media:void ∈ MediaUrn,    media:void ⪯ media:,    ¬(m ⪯ media:void) per ogni m concreto

Una specifica direzionale impostata a media:void è il tipo unità, letto come “()”. Non è il top, non è “invalido”, non è “assente”. È un tipo distinto di prima classe il cui significato è “su questo lato non scorre alcun payload”.

La regola di atomicità è strutturale: sotto l’unità non c’è alcun reticolo. media:void;warmup, media:void;heartbeat, media:void;reason=foo sono errori di parsing, non raffinamenti. Le distinzioni sul perché o sul come si usa uno slot void appartengono all’asse non direzionale y del cap URN o agli argomenti della cap, mai al media URN stesso. Questo preclude un’intera famiglia di ambiguità di dispatch (valori unità diversi? effetti diversi? comandi diversi?) rifiutando la sintassi che le esprimerebbe. Vedi Media URN: il tipo unità.

La relazione di dispatch tratta media:void esattamente come qualsiasi altro media URN. Il fatto che ammetta una lettura logica come tipo unità è una proprietà che il classificatore CapKind sfrutta per etichettare le cap; non entra mai nel predicato di dispatch come caso speciale.

Generi di cap (livello logico)

Il prodotto C ammette una classificazione in cinque generi, esaminando (i, o) e se y è vuoto:

Questa classificazione è solo logica. La relazione di dispatch definita in La relazione di dispatch non si dirama in base al genere; il genere è una descrizione del morfismo risultante, non una dimensione di instradamento. Vedi Struttura del cap URN: generi di cap per la tassonomia completa.

Specificità della cap

Si definisce:

spec_C : C → ℕ

come:

spec_C(i, o, y, e) = 10_000 * spec_U(o)
                    +    100 * spec_U(i)
                    +          spec_U(y)

Gli assi in, out e y passano per la stessa funzione di specificità dei tagged URN spec_U per la somma per asse. Gli assi differiscono nel loro peso nel totale del cap URN: due ordini di grandezza separano out da in e da y, dando un unico intero con priorità lessicografica (out, in, y). Questo riflette l’intento di instradamento: produrre cose diverse è la differenza semantica più grande fra due cap, consumare cose diverse viene subito dopo, e i metadati dell’asse y contano meno di tutto.

Punteggio per tag (la stessa scala a sei forme applicata in modo uniforme su ogni asse):

Questo è uno scalare derivato, usato solo per il ranking fra candidati già validi. Vedi Specificità per tutti i dettagli ed esempi svolti.

La relazione di dispatch

Un candidato è una cap. Una richiesta è una query, una domanda sulle cap che chiede qualcosa a ciascun lato o lo lascia incognito (Dispatch: query). Il dispatch è la richiesta, letta come query, che ammette il candidato.

Siano:

• il candidato p = (i_p, o_p, y_p, e_p)
• la richiesta r = (i_r, o_r, y_r, e_r)

Dispatch(p, r)  ⟺  (i_r open ∨ i_r ⪯ i_p)  ∧  o_p ⪯ o_r  ∧  (e_r = ? ∨ e_p = e_r)  ∧  y_p satisfies y_r

dove i_r open significa che l’input della richiesta non vincola nulla, e y_p satisfies y_r legge i tag propri del candidato come completi (Predicati: cose complete).

Questo è il predicato di instradamento primario. Alla sua base c’è la relazione tipizzata fra due cap intese come descrizioni (sottotipizzazione delle frecce):

CapRefines(a, b)  ⟺  i_b ⪯ i_a  ∧  o_a ⪯ o_b  ∧  (e_b = ? ∨ e_a = e_b)  ∧  y_a ⪯ y_b

CapRefines(p, r) ⟹ Dispatch(p, r), e le due coincidono ogni volta che la richiesta dichiara il suo input e i tag di nessuno dei due lati chiedono un’assenza.

Interpretazione del dispatch

Ammissibilità dell’input (controvariante)

i_r open  ∨  i_r ⪯ i_p

Un input che la richiesta non ha stabilito non chiede nulla. Altrimenti l’input della richiesta deve essere almeno tanto specifico quanto l’input accettato dal candidato.

Punto di vista della teoria dei tipi: i parametri delle funzioni sono controvarianti. Il candidato può accettare input più generali.

Ammissibilità dell’output (covariante)

o_p ⪯ o_r

L’output del candidato deve essere almeno tanto specifico quanto l’output richiesto dalla richiesta.

Punto di vista della teoria dei tipi: i valori di ritorno delle funzioni sono covarianti. Il candidato deve garantire almeno ciò che la richiesta pretende.

Raffinamento comportamentale (i tag del candidato, completi)

y_p satisfies y_r

I tag non direzionali della richiesta sono un pattern; quelli del candidato sono i tag che possiede. Il candidato deve avere ogni tag che la richiesta chiede, può portare tag che la richiesta non menziona e, poiché il suo elenco è completo, non possiede i tag che omette: una richiesta di !x è servita da un candidato che non dice nulla su x.

Riepilogo della varianza

Il dispatch è direzionale

In generale:

Dispatch(p, r)  ⟹̸  Dispatch(r, p)

Il dispatch non è simmetrico.

Un candidato specifico può gestire una richiesta generica, ma una richiesta generica non può “gestire” un candidato specifico.

Relazioni derivate a livello di cap

Usando i predicati di base componente per componente:

Equivalenza di cap

CapEq(c₁, c₂)  ⟺  is_equivalent(i₁, i₂) ∧ is_equivalent(o₁, o₂) ∧ is_equivalent(y₁, y₂)

Comparabilità di cap

CapComparable(c₁, c₂)  ⟺  is_comparable(i₁, i₂) ∧ is_comparable(o₁, o₂) ∧ is_comparable(y₁, y₂)

Utile per la scoperta, non sufficiente per il dispatch.

Ruoli corretti dei predicati

Policy di ranking

Il ranking è definito solo sull’insieme valido:

Valid(r) = { p ∈ C | Dispatch(p, r) }

Una policy di ranking è un qualsiasi preordine totale su Valid(r).

Distanza di specificità

dist(p, r) = spec_C(p) - spec_C(r)

Preferenza tipica

1. dist = 0 (equivalente), il più preferito
2. La dist positiva più piccola (raffinamento)
3. Dist negativa solo come ripiego (candidato generico)

Questa è policy, non semantica. Il dispatch definisce la validità; il ranking definisce la selezione.

Proprietà fondamentali di coerenza

Riflessività del dispatch

∀c ∈ C,  Dispatch(c, c)

Segue dalla riflessività di ⪯.

Transitività del dispatch

∀a,b,c ∈ C,  (CapRefines(a, b) ∧ CapRefines(b, c)) ⟹ CapRefines(a, c)

Segue dalla transitività di ⪯ (capRefines_trans). La legge di composizione è una legge delle cap intese come descrizioni, e delle query (Query.narrower_trans: una domanda più stretta ha meno risposte). Non è una legge di Dispatch, che mette in relazione una cap con una domanda: un candidato solo-pdf serve una richiesta il cui input è aperto; quella richiesta, letta come candidato, serve una richiesta di immagini; e il candidato solo-pdf non serve la richiesta di immagini. Dispatch: proprietà dice dove vive ciascuna legge.

Monotonia del raffinamento del candidato

Se il candidato p’ raffina p:

• i_p ⪯ i_p’ (input più permissivo)
• o_p’ ⪯ o_p (output più specifico)
• y_p’ ⪯ y_p (tag y più specifici)

e vale CapRefines(p, r), allora:

CapRefines(p', r)

Il raffinamento preserva l’idoneità (capRefines_monotone).

Rifiuto delle contraddizioni

¬(i_r open ∨ i_r ⪯ i_p) ∨ ¬(o_p ⪯ o_r) ∨ ¬(e_r = ? ∨ e_p = e_r) ∨ ¬(y_p satisfies y_r)  ⟹  ¬Dispatch(p, r)

Se un qualsiasi congiunto fallisce, il dispatch fallisce.

Errori comuni

Usare accepts per il dispatch

Sbagliato: appiattisce un problema tridimensionale a varianza mista in una sola direzione.

Usare conforms_to per il dispatch

Sbagliato: per lo stesso motivo.

Usare is_comparable per il dispatch

Sbagliato: l’essere correlati non è validità. Due URN possono essere comparabili ma non idonei al dispatch.

Fare il ranking prima della validità

Sbagliato: la specificità da sola non implica la legittimità semantica.

Trattare i cap URN come unidimensionali

Sbagliato: i cap URN sono oggetti prodotto strutturati con varianza mista.

Separazione fra validità e preferenza

La specifica distingue:

• Validità semantica: se un candidato può legittimamente servire una richiesta (Dispatch)
• Preferenza di selezione: quale candidato valido dovrebbe essere scelto (Ranking)

Le due non devono essere confuse.

Conformità delle implementazioni

Ogni implementazione conforme a questa specifica deve garantire che:

1. Tutti i tagged URN si normalizzino in U
2. Tutte le verifiche a livello di dimensione si riducano alla stessa relazione di base ⪯
3. Il dispatch delle cap usi esattamente la regola a direzione mista (sezione 10)
4. Il ranking venga applicato solo dopo che la validità del dispatch è stata stabilita

Riepilogo

L’intero sistema è definito a partire da un’unica base semantica:

• Un dominio di tagged URN U
• Una relazione di specificità ⪯
• Un punteggio di specificità spec_U

I cap URN sono elementi di un prodotto a quattro coordinate in U × U × U × E.

Il dispatch è una richiesta, letta come domanda sulle cap, che ammette un candidato:

Dispatch((i_p, o_p, y_p, e_p), (i_r, o_r, y_r, e_r))
  ⟺  (i_r open ∨ i_r ⪯ i_p) ∧ o_p ⪯ o_r ∧ (e_r = ? ∨ e_p = e_r) ∧ y_p satisfies y_r

Ne derivano:

• Un’interpretazione in termini di teoria degli ordini
• Un’interpretazione in termini di teoria dei tipi
• La separazione fra instradamento, pianificazione, scoperta e corrispondenza esatta
• Un fondamento per la verifica formale