V&V-Monadic Second Order theory of One's Successor

Monadic Second Order theory of One’s Successor

Partiamo con il dire perchè c’è bisogno di capire:

• la monadic second order theory of one’s successor (S1S)
• la relazione tra automi di Büchi e S1S

S1S è un modo per tradurre i Buchi automata in una forma più “manipolabile”, ossia il formalismo logico. Se giocassimo con i Buchi automata, capiremmo subito che per più diventano grandi, più gli occhi iniziano a girare, la testa diventare rossa, il sangue uscire da ogni orifizio corporeo. Ecco quindi che trovare un formalismo più succinto rende le cose più maneggevoli e meno pericolose per la nostra salute.

Quindi, cosa sarebbe un linguaggio del $S1S_\mathcal{A}$? Sicuramente qualcosa in cui compariranno i classici simboli della logica matematica.

Un linguaggio $S1S_{\mathcal{A}}$ è un linguaggio composto a partire da:

• termini: sarebbero i simboli di costante costruiti a partire da 0 e usando la funzione successore (+1) e le variabili $x,y,…$ (su cui possono essere applicate le funzioni successore)
• formule atomiche: si formano a partire dai termini e possono essere nelle forme (con $t_{1}$ e $t_{2}$ due termini)
  • $t_{1}=t_{2}$
  • $t_{1}<t_{2}$
  • $t_1 \in X$ con X una variabile al second’ordine
  • $t_{1} \in Q_a$ con Q simbolo di predicato unario (uno per ogni $a \in A$)
• formule: possono comparire quantificatori $\forall, \exists$ e operatori booleani come $\lnot,\wedge,\lor$ applicati su variabili individuali o variabili insiemistiche ($\forall x$ o $\forall X$)

formula chiusa (enunciato): una formula priva di variabili libere

👁️ Osservazione::

la definizione del simbolo 0 e del predicato < non è necessario in S1S. Difatti è sufficiente usare l’operatore successore e la logica del second’ordine:

• lo zero può essere definito come

oppure (senza predicato <)

• il predicato < può essere riscritto come

Come rappresento una $\omega$-parola usando la logica?

Semplicemente creiamo una sorta di “stampino” $\underline{\alpha}$ definito come

dove

• il dominio $\omega$ corrisponde ai naturali e
• $Q_a$ è definito come l’insieme degli indici delle posizioni della $\omega$-parola $\alpha$ in cui il simbolo è $a$

Come rappresento un linguaggio usando delle parole S1S?

È possibile definire un linguaggio a partire da una formula logica che dev’essere soddisfatta da ogni $\omega$-parola. In particolare data una formula $\varphi$, il linguaggio descritto da tale formula è definito come

\[L(\varphi) = \{\alpha \in A^{\omega}\; |\; \underline{\alpha} \models \varphi \}\]

Facciamo degli esempi:

1. Sia L il linguaggio sull’alfabeto ${a, b, c}$ che contiene tutte e sole le $\omega$-parole tali che ogni occorrenza del simbolo $a$ sia seguita da un’occorrenza del simbolo $b$. $L$ è catturato dal seguente enunciato al prim’ordine:

1. Sia L il linguaggio sull’alfabeto ${a, b, c}$ che contiene tutte e sole le $\omega$-parole tali che tra ogni coppia di occorrenze successive del simbolo $a$ vi sia un numero pari di occorrenze dei simboli b e c. L è catturato dal seguente enunciato al second’ordine:

la clausola

serve per escludere che siano presenti simboli $a$ tra altri due simboli $a$. L’ultima implicazione invece controlla la parità.

La cosa interessante è che possiamo fare in modo di rendere irrilevante l’alfabeto usato. Come? Semplicemente convertendo ogni simbolo in A nella corrispettiva codifica binaria (ad esempio se $A={ a,b,c,d }$ posso considerare il nuovo alfabeto $A’=${ 0,1} $^n$ con $n = \log|A|$), rimpiazzando i predicati $Q_{a}$ con variabili libere del second’ordine $X_1, \dots, X_n$ e rimpiazzando l’insieme dei $Q_a$ con l’insieme dei $P_k$ definito come

Praticamente l’insieme $P_k$ è l’insieme degli indici dei simboli di $\alpha$ tali per cui il k-esimo bit è 1.

ESEMPIO: Assumiamo $\alpha = \text{“ciao”}$ con $A=\text{{a,b,c,d,e,f,g,h,i,l,m,n,o }}$. La versione $S1S_A$ di $\alpha$ è rappresentata da

Mentre la versione alphabet-agnostic per prima cosa convertirà l’alfabeto in binario e quindi la parola iniziale diventerà:

Successivamente rappresenterà $\alpha_{bin}$ come:

A questo punto quindi diventa anche più facile definire il linguaggio $\mathcal{L}$ a partire da una formula S1S $\varphi(X_1,\dots,X_n)$

Da notare che le variabili $X_i$ sono tutte variabili del second’ordine, quindi da intendersi come insiemi di bit. In particolare ciascun $X_i$ è l’insieme degli indici dei caratteri della parola $\alpha$ per cui l’i-esimo bit è 1. Sostanzialmente da $X_1, \dots, X_n$ riesco a ricondurmi alla parola $\alpha$ e viceversa.

👁️ Osservazione: $S1S_\mathcal{A}$ vs $S1S$

Qualcuno potrebbe aver obiettato dicendo “ma perchè hai scritto $S1S_{\mathcal{A}}$ invece di $S1S$? Sono sinonimi?”. La risposta è NO. $S1S_\mathcal{A}$ si riferisce a una Monadic Second-Order Theory of Ones’s Successor che lavora su $\omega$-parole costruite su un alfabeto $A$.

S1S invece si riferisce alla versione “generica” che non fa uso di un alfabeto, ma di indici delle lettere dell’alfabeto (quella traduzione che avevamo visto prima). A questo punto quindi le lettere dell’alfabeto vengono sostituite da variabili del second’ordine che rappresentano l’insieme di posizioni associate ai simboli dell’alfabeto di partenza.

Lemma: Chiusura per proiezione

Il lemma sulla chiusura per proiezione stabilisce che, se ho una formula S1S $\varphi(X_1​,\dots,X_n​)$ che definisce un linguaggio $\omega$-regolare $\mathcal{L}(\varphi)\subseteq A^\omega$, allora posso “proiettare via” (cioè esistenzializzare) una delle variabili di secondo ordine (ad esempio $X_i$​) per ottenere una nuova formula

\[\psi(X_1,\dots,X_{i−1},X_{i+1},\dots,X_n)=\exists X_i \varphi(X_1,\dots,X_n)\]

che definisce un linguaggio $\mathcal{L}(\psi)$ anch’esso $\omega$-regolare.

Ciò significa che, anche se originariamente la formula $\varphi$ opera su $n$ variabili (ognuna associata ad una “coordinata” di un alfabeto strutturato, tipicamente ${0,1}^n$), possiamo eliminare una delle variabili e rimanere entro la classe degli $\omega$-linguaggi regolari. La variabile mancante (qui $X_i$​) corrisponde a una componente che viene “proiettata via”. A livello di automi, questo corrisponde al fatto che, dato un automa di Büchi $\mathcal{A}$ su ${0,1}^n$ che riconosce $\mathcal{L}(\varphi)$, possiamo costruire un automa di Büchi A′ su ${0,1}^{n−1}$ che riconosce $\mathcal{L}(\psi)$ sostituendo ogni simbolo $(j_1​,\dots,j_n​)$ con il simbolo $(j_1​,\dots,j_{i−1}​,j_{i+1}​,\dots,j_n​)$. Una parola $\alpha$ sul nuovo alfabeto viene accettata da $\mathcal{A}’$ se e solo se esiste una scelta per la i-esima componente (un “complemento” $\beta$) tale che la parola ricostruita $\alpha’$ (ossia inserendo $\beta$ come i-esima coordinata) è accettata da $\mathcal{A}$.

👁️ Nella formula $\psi$ bisogna osservare che tra le variabili di second’ordine espresse come argomento manca la variabile $X_{i}$

Il lemma dice una cosa importante. Dice che se ho una formula $\psi$ che opera su $n$ variabili del second’ordine, posso sempre riuscire a ridurre il numero di variabili usate mediante una riscrittura della formula rimanendo comunque all’interno del potere espressivo di S1S. Perciò se posso esprimere mediante una formula S1S un certo linguaggio che usa n variabili, posso fare lo stesso anche con una formula che ne usa meno di n.

Ad esempio se consideriamo $A = {a, b, c}$ e un linguaggio $L \subseteq A^\omega$ definito da:
“Ogni occorrenza di $a$ è seguita da un $b$ prima di un $c$”.

La formula in S1S per L è:

Se ora vogliamo proiettare L sull’alfabeto $B = {a, c}$ eliminando $b$, il nuovo linguaggio $\pi(L)$ richiede una nuova formula che verifica implicitamente la condizione rimossa.

La nuova formula potrebbe essere:

\(\forall x. (x \in X_a \implies \exists y. (y > x \land y \in X_c))\) Questo dimostra che possiamo tradurre la proiezione in una nuova formula S1S.

Dimostrazione

1. Si consideri un automa di Büchi non deterministico $\mathcal{A}$ definito sull’alfabeto ${0,1}^n$ che riconosce il linguaggio $\mathcal{L}(\varphi)$. Qui ogni simbolo è un vettore $(j_1​,j_2​,\dots,j_n​)$ che codifica, ad esempio, l’assegnamento a $n$ variabili di secondo ordine.

2. Per ottenere l’automa $\mathcal{A}’$ corrispondente alla formula $\psi$, si modifica $\mathcal{A}$ sostituendo ogni simbolo $(j_1,…,j_i,\dots,j_n)$ con il nuovo simbolo $(j_1,\dots,j_{i−1},j_{i+1},\dots,j_n)$. Questa operazione riduce la codifica dei simboli da $n$ componenti a $n−1$.

3. Una $\omega$-parola $\alpha$ sull’alfabeto ${0,1}^{n−1}$ viene accettata da $\mathcal{A}’$ se e solo se esiste almeno una sequenza (o scelta) per la componente “mancante” (che chiameremo $\beta$) tale che la parola $\alpha’$, ottenuta reinserendo $\beta$ come $i$-esima coordinata (ossia, $\alpha’ =(\alpha_1,\dots,\alpha_{i-1},\beta,\alpha_{i+1},\dots,\alpha_n)$), sia accettata da $\mathcal{A}$.

Questa costruzione mostra che, proiettando via una variabile, si ottiene un linguaggio $\mathcal{L}(\psi)$ sull’alfabeto ridotto che resta $\omega$-regolare, poiché è riconosciuto da un automa di Büchi (anche se definito su ${0,1}^{n−1}$). L’idea è dimostrare che a partire da un automa di Büchi $\cal{A}$ sull’alfabeto ${0,1}^n$ che riconosce un linguaggio $L(\varphi)$ è possibile generare un automa di Büchi $\cal{A}’$ che riconosce il linguaggio $L(\psi)$ sull’alfabeto ${0,1}^{n-1}$. Se tale automa esiste sappiamo che anche il linguaggio $L(\psi)$ è $\omega$-regolare.

Quindi riassumendo, l’automa $\cal{A}’$ viene costruito considerando l’automa $\cal{A}$ e rimpiazzando ogni simbolo $(j_{1},\dots,j_{i},\dots,j_{n})$ con un nuovo simbolo $( j_{1},\dots,j_{i-1}, j_{i+1},\dots ,j_{n})$. In pratica non si fa altro che ridurre la codifica dei simboli. Una parola $\alpha = ( \alpha_{1},\dots,\alpha_{i-1}, \alpha_{i+1},\dots ,\alpha_{n})$ è accettata da $\cal{A}’$ se e solo se esiste una componente $\beta$ tale che $\alpha’ = ( \alpha_{1},\dots,\alpha_{i-1}, \beta, \alpha_{i+1},\dots ,\alpha_{n})$ è accettata da $\cal{A}$.

$\square$

Possibili domande

Che differenza c’è tra monadic second order theory of one’s successor e monadic first order theory of one’s successor?

1. Linguaggio con occorrenza obbligatoria

Definisci un enunciato che cattura il linguaggio delle $\omega$-parole sull’alfabeto ${a,b,c}$ in cui ogni simbolo c è preceduto da almeno un simbolo b.

2. Parità delle occorrenze

Definisci un enunciato per il linguaggio di $\omega$-parole sull’alfabeto ${0,1}$ in cui ogni prefisso finito della parola contiene un numero pari di occorrenze del simbolo 1.

3. Evento ciclico

Trova l’enunciato che descrive il linguaggio delle $\omega$-parole sull’alfabeto ${x, y, z}$ in cui il simbolo x appare infinitamente spesso e ogni occorrenza di x è seguita (prima o poi) da un’ulteriore occorrenza di y.

4. Alternanza tra simboli

Definisci un enunciato per il linguaggio delle $\omega$-parole sull’alfabeto ${a, b}$ in cui a e b compaiono in modo alternato, senza che ci siano due a o due b consecutivi.

5. Suffisso infinito

Definisci il linguaggio delle ω\omegaω-parole sull’alfabeto ${p, q, r}$ in cui, a partire da un certo punto della parola, appaiono solo i simboli p e q.

6. Mai ripetizione consecutiva

Trova l’enunciato per il linguaggio delle $\omega$-parole sull’alfabeto ${a, b}$ in cui il simbolo a non compare mai due volte consecutive.

7. Prefissi validi

Definisci un linguaggio L sull’alfabeto ${0, 1, 2}$ in cui ogni prefisso finito di una parola $\alpha$ ha almeno tante occorrenze del simbolo 0 quante del simbolo 1.

8. Eventuale periodicità

Trova l’enunciato che descrive le $\omega$-parole sull’alfabeto ${a, b}$ che a partire da un certo punto diventano periodiche con il ciclo ab.

9. Posizioni specifiche

Definisci un linguaggio L sull’alfabeto ${x, y, z}$ in cui le occorrenze di x appaiono solo in posizioni pari.

10. Infinitamente molti simboli

Trova l’enunciato che descrive le $\omega$-parole sull’alfabeto ${a, b, c}$ in cui appaiono infinitamente molte b e c, ma solo un numero finito di a.