le dimostrazioni

[le definizioni]
[lemma 0]
[lemma 1]
[osservazioni]
[teorema 0]
[teorema 1]

le definizioni

top

I nodi sono entità del grafo con un identificatore id, un label indicante il carattere che essi rappresentano e possono avere assegnati degli archi uscenti.

Gli archi sono entità del grafo che collegano due nodi, hanno un identificatore id, un label che indica il carattere rappresentato dal nodo al quale puntano, sono assegnati al nodo da cui partono ed hanno un campo from che limita il loro utilizzo come percorsi ammissibili.
Gli archi con campo from=0 sono detti diretti e possono sempre essere percorsi, gli altri sono detti laterali.

STARTS è un array di indici con dimensione pari al numero di caratteri dell'alfabeto.
STARTS[c] contiene l'id del nodo in cui un cursore che inizia il suo percorso con il carattere c viene posto al momento del suo ingrasso nel grafo.

I cursori sono gli oggetti che percorrono il grafo, cercando un arco che li porti dal nodo su cui sono posizionati ad un altro nodo che rappresenti il giusto carattere, essi sono necessari sia per la creazione del grafo che per il suo utilizzo. Come campi ha nodeId (l'id del nodo su cui si trova) e from, che tiene memoria dell'id dell'ultimo arco laterale percorso, oppure, se non ha ancora percorso archi laterali, contiene il calore del carattere dell'alfabeto tramite il quale è stato inserito nel grafo.

Def 0 :
I nodi Na e Nb sono collegati (da un arco L) in relazione al cursore C posto su Na se e solo se
esiste un arco L uscente dal nodo Na che porta a Nb e L è diretto oppure è laterale ma con L.from=C.from.

Def 1 :
I nodi N0 N1 ... Nn sono un percorso per il cursore C0 posto su N0 se e solo se
ogni coppia di nodi successivi Ni Ni+1 sono collegati tra di loro (da un arco Li) in relazione ad un cursore Ci posto su Ni definito come Ci.nodeId=Ni.id e Ci.from=Ci-1.from se Li-1 è diretto, Ci.from=Li-1.id se Li-1 è laterale.

Def 2 :
Il grafo G accetta la stringa S (S=s0 s1 ... sn) se e solo se
esiste un percorso N0 N1 ... Nn con N0=G.STARTS[s0] per un cursore posto su N0 con from=s0 e tale che per ogni indice i, 0<=i<=n, Ni.label=si.

lemma 0

top

TESI :
Se i nodi Na e Nb sono collegati (da un arco L1) in relazione ad un cursore C posto su Na, allora non esiste un terzo nodo Nc con lo stesso label di Nb tale che Na e Nc siano collegati (da un arco L2) in relazione allo stesso cursore C, posto su Na.

DIM :
Dall'[algoritmo di costruzione del grafo] risulta che un arco L viene aggiunto a Na in due soli casi:
-inserendo l'arco diretto tra Na e Na+1, in questo caso Na non aveva ancora nessun altro arco uscente assegnato di esso ([DIRECT])
-quando non esiste ancora un arco che porta da Na ad un nodo con un determinato label, per un certo cursore C ([LATERAL])
Ne deriva banalmente la tesi.

lemma 1

top

TESI :
Se il grafo G accetta la stringa S (S=s0 s1 ... sn) allora esiste unico il percorso N0 N1 ... Nn della definizione 2.

DIM :
L'esistenza viene dalla definizione 2, l'unicità deriva banalmente dal lemma 0

osservazioni

top

Oss 0 :
Se un cursore C, partito da uno degli STARTS, si trova in un certo nodo N con from=f, allora l'ultimo arco che ha percorso (se N non è il nodo indicato da STARTS[f]) è l'arco laterale con id=f se tale arco porta a N, altrimenti proviene dall'arco diretto uscente dal nodo precedente.

Oss 1 :
Un cursore con un determinato campo from, partito da uno degli STARTS, che si trova in un determinato nodo, ha potuto seguire un unico percorso possibile.

Oss 2 :
Data la stringa S ed il grafo G, se G' è stato creato dalla stessa stringa usata per creare G ma leggendola al contrario, allora S è accettata da G se e solo se S letta al contrario è accettata da G'.

teorema 0

top

TESI :
Se S (S=s0 s1 ... sn) è una sottostringa di S' e G è il grafo generato da S' (seguendo l'[algoritmo di costruzione del grafo]), allora G accetta S.

DIM :
Durante la generazione di G, avrò n+1 cicli [READ][ADD][WALK][CURSOR] in cui [READ] legge, in sequenza, s0, s1, ... sn.
A [CURSOR]0 o aggiungo un cursore C o segnalo il nodo creato come STARTS[s0] (in quest'ultimo caso la tesi ne deriva banalmente, S verrà riconosciuta perchè si ha un semplice percorso formato da archi diretti che parte dal punto di ingresso per s0).
Se al passo 0 ho inserito un nuovo cursore (posto sul nodo N0), ad ogni successivo passo i (se il cursore non è già stato eliminato) per quel cursore dovrò verificare la guardia dell'IF contenuto nel ciclo [WALK].
Se la guardia è vera allora Ni-1 e Ni sono collegati (da un arco Li) in relazione al cursore C posto su Ni-1 e se Li.from!=0 allora modifico C.from=Li.from.
Se la guardia invece è falsa si aggiunge un arco laterale che rende Ni-1 e Ni collegati (da tale arco) in relazione al cursore C posto su Ni-1, poi elimino il cursore C.
Se, iterando in questo modo, restando sempre con la guardia dell'IF vera riesco a raggiungere anche l'ultimo carattere di S, allora il percorso seguito da C è quello che fa accettare a G la stringa S, se invece ad un certo punto ho la creazione di un arco laterale, con la conseguente eliminazione del cursore C, ho che fino a quel punto esiste una strada fatta di archi o diretti o laterali e che da li in poi, avendo creato un arco che manda nel nodo di testa durante la creazione del grafo, mi assicuro una strada di archi diretti e quindi sicuramente percorribili da qualsiasi cursore che li arriva, che porta fino all'ultimo sn, tale strada assicura l'accettazione di S da parte di G.

teorema 1

top

TESI :
Se S (S=s0 s1 ... sn) NON è una sottostringa di S' e G è il grafo generato da S' (seguendo l'[algoritmo di costruzione del grafo]), allora G NON accetta S.

DIM :
Se S non è sottostringa di S' allora esiste un j tale che:
s0 s1 ... sj è sottostringa di S'
ma s0 s1 ... sj+1 non è sottostringa di S'
Dal [teorema 0] si ha che s0 s1 ... sj è accettato da G.
Dal [lemma 1] si ha che esiste unico il percorso N0 N1 ... Nj che accetta la stringa S.
Tutti i cursori che partendo da N0 (=STARTS[s0]) con from=s0 percorrono j-1 nodi con label nell'ordine s1 s2 ... sj passano per gli stessi archi, quindi quando raggiungono Nj hanno lo stesso campo from=f.
N0 N1 ... Nj Nj+1, con Nj+1.label=sj+1 sono un percorso (essendolo N0 N1 ... Nj) solo se Nj e Nj+1 sono collegati da un arco L.
Un arco L con questa caratteristica può essere diretto o laterale, iniziamo a considerare l'ipotesi che esso sia laterale.
L, per collegare lateralmente Nj e Nj+1 in relazione ad un cursore con from=f, deve avere L.from=f, ma tale arco esiste solo se un cursore con from=f si è trovato in Nj ed il carattere letto è stato sj+1.
Ma dall'osservazione 1 un cursore su Nj individua univocamente un percorso, nel nostro caso formato da nodi con label s0 s1 ... sj.
Non essendo s0 s1 ... sj+1 sottostringa di S', tale sequenza di lettere non si presenta mai durante la creazione di G e quindi non esiste un L laterale che collega Nj ad un Nj+1 con Nj+1.label=sj+1 in relazione ad un cursore con from=f.
L non può essere laterale, se esiste allora deve essere diretto.
Denominando Li l'arco che collega i nodi Ni e Ni+1 nel percorso N0 N1 ... Nj (percorso la cui esistenza è garantita dal dal teorema 1 in quanto la sequenza s0 s1 ... sj è accettata da G), considero l'arco Lk, 0<=k<j, tale che Lk sia laterale e non esista un altro arco Lk' laterale con indice k' maggiore (ma minore comunque di j, tenendo conto che Lj è L).
Lk deve esistere altrimenti significherebbe avere un percorso N0 N1 ... Nj+1 formato da soli archi diretti, il che è falso perchè deriva banalmente dall'algoritmo di creazione del grafo che ciò può avvenire se e solo se la sequenza s0 s1 ... sj+1 compare in S', falso per ipotesi.
In pratica il percorso Nk+1 Nk+2 ... Nj Nj+1 è formato da soli archi diretti, quindi significa, come banale deduzione dell'algoritmo di costruzione del grafo, che la sequenza di caratteri sk+1 sk+2 ... sj sj+1 è presente in S'.
Un cursore che raggiunge Nk+1 dopo aver percorso N0 N1 ... Nk partendo da N0 con con from=s0 può avere un unico possibile campo from=f' (partendo con from=s0 e seguendo forzatamente la sequenza di archi L0 L1 ... Lk-1).
Ma l'esistenza di Lk laterale percorribile da cursori con from=f' posto sul nodo Nk che porta a Nk+1 è possibile solo se durante la creazione del grafo un cursore con from=f' si è trovato su Nk e ha incontrato il carattere sk+1.
Ma dall'osservazione 1 un cursore su Nk individua univocamente un percorso, nel nostro caso formato da nodi con label s0 s1 ... sk.
A quel punto per generare Lk laterale è stato passato sk+1 e quindi si deve essere incontrata in S' la sequenza s0 s1 ... sk sk+1.
La presenza di un percorso Nk+1 Nk+2 ... Nj Nj+1 diretto significa però che dopo aver incontrato s0 s1 ... sk la lettura di S' è proseguita non solo con sk+1, ma con sk+1 sk+2 ... sj sj+1 e quindi s0 s1 ... sj sj+1 deve essere presente in S', il che è falso per l'ipotesi e quindi L non può essere neanche diretto, quindi non esiste.
E quindi non esiste un percorso N0 N1 ... Nj+1, Ni.label=si, N0=STARTS[s0], per C posto su N0 con C.from=s0.
Quindi dalla definizione 2 G NON accetta S.