Teorema Myhill-Nerode

În informatică teoretică , și în special în teoria limbajelor formale și a automatelor , teorema Myhill-Nerode oferă o condiție necesară și suficientă pentru ca un limbaj formal să fie un limbaj rațional, adică recunoscut de un automat finit . Această teoremă poartă numele lui John Myhill și Anil Nerode care au dovedit-o în 1958 ( Nerode 1958 ).

Interesul acestei afirmații este că condiția necesară și suficientă se referă la limbajul în sine și nu necesită construirea unui automat. Dovada este, pe de altă parte, constructivă și face posibilă obținerea eficientă a unui automat care, în plus, se dovedește a fi minim.

Enunțarea teoremei

Având în vedere un limbaj și două cuvinte și , spunem că un cuvânt separă și dacă unul și numai unul dintre cuvinte și se află în limbă . Două cuvinte și sunt inseparabile ( nedistinguibile în engleză) dacă nu există niciun cuvânt care să le separe. L{\ displaystyle L}X{\ displaystyle x}y{\ displaystyle y}z{\ displaystyle z} X{\ displaystyle x}y{\ displaystyle y}Xz{\ displaystyle xz}yz{\ displaystyle yz}L{\ displaystyle L}X{\ displaystyle x}y{\ displaystyle y}z{\ displaystyle z}

Definim o relație pe cuvinte, numită relația Myhill-Nerode , prin regula: dacă și numai dacă și sunt inseparabile. Este ușor să arătăm că relația este o relație de echivalență a cuvintelor și, prin urmare, împarte setul tuturor cuvintelor în clase de echivalențe . Numărul de clase se numește indicele relației. Poate fi finit sau infinit. RL{\ displaystyle R_ {L}}XRLy{\ displaystyle xR_ {L} y}X{\ displaystyle x}y{\ displaystyle y}RL{\ displaystyle R_ {L}}

Teorema Myhill-Nerode  -  Un limbaj este rațional dacă și numai dacă relația este de index finit; în acest caz, numărul stărilor celui mai mic automat recunoscător determinist complet este egal cu indicele relației. În special, aceasta implică faptul că există un singur automat determinist cu un număr minim de stări. L{\ displaystyle L}RL{\ displaystyle R_ {L}}L{\ displaystyle L}

Demonstrație

Fie un limbaj rațional. Există un automat finit determinist complet care recunoaște . Pentru fiecare stare a acestui automat, adică setul de cuvinte care conduc de la starea inițială la . Dacă și sunt două cuvinte , atunci pentru orice cuvânt , cuvintele și conduc la aceeași stare, fie că este de a accepta sau nu. Astfel, nici un cuvânt nu poate separa și , prin urmare, sunt inseparabile. Aceasta arată că mulțimea este conținută într-o clasă a echivalenței și, deoarece orice cuvânt se află într-unul dintre mulțimi , indicele relației este mai mic sau egal cu numărul de stări ale automatului și, prin urmare, este finit. L{\ displaystyle L}L{\ displaystyle L}q{\ displaystyle q}Pq{\ displaystyle P_ {q}}w{\ displaystyle w}q{\ displaystyle q}X{\ displaystyle x}y{\ displaystyle y}Pq{\ displaystyle P_ {q}}z{\ displaystyle z}Xz{\ displaystyle xz}yz{\ displaystyle yz}z{\ displaystyle z}X{\ displaystyle x}y{\ displaystyle y}Pq{\ displaystyle P_ {q}}RL{\ displaystyle R_ {L}}Pq{\ displaystyle P_ {q}}

În schimb, să presupunem că relația Myhill-Nerode este de indice finit. În acest caz, construim un automat finit de recunoaștere după cum urmează. Statele sunt clasele de echivalență . Starea inițială este clasa de echivalență a cuvântului gol, iar funcția de tranziție conduce, pentru o stare și o literă , la starea care conține cuvântul , unde este orice cuvânt de . Definiția echivalenței asigură faptul că funcția de tranziție este bine definită: dacă , atunci pentru orice literă , deoarece dacă un cuvânt ar fi un separator al și , atunci ar separa și . O stare a automatului este definitivă dacă conține un cuvânt de . La fel ca înainte, definiția relației implică faptul că toate elementele acestei clase se află , altfel cuvântul gol ar putea separa cuvintele acestei clase. RL{\ displaystyle R_ {L}}L{\ displaystyle L}RL{\ displaystyle R_ {L}}p{\ displaystyle p}la{\ displaystyle a}q{\ displaystyle q}Xla{\ displaystyle xa}X{\ displaystyle x}p{\ displaystyle p}RL{\ displaystyle R_ {L}}XRLy{\ displaystyle xR_ {L} y}XlaRLyla{\ displaystyle xaR_ {L} ya}la{\ displaystyle a}z{\ displaystyle z}Xla{\ displaystyle xa}yla{\ displaystyle ya}laz{\ displaystyle az}X{\ displaystyle x}y{\ displaystyle y}L{\ displaystyle L}RL{\ displaystyle R_ {L}}L{\ displaystyle L}

Astfel, existența unui automat finit recunoscător implică faptul că relația este de index finit și de index cel mult egal cu numărul de stări ale automatului, iar finitudinea indicelui de implică existența unui automat având acest număr de stări. L{\ displaystyle L}RL{\ displaystyle R_ {L}}RL{\ displaystyle R_ {L}}

Relația Myhill-Nerode și reziduuri

Având în vedere o limbă de și un cuvânt , coeficientul stâng al par , sau rezidual de par , este setul denotat definit de L{\ displaystyle L}LA∗{\ displaystyle A ^ {*}}X{\ displaystyle x}L{\ displaystyle L}X{\ displaystyle x}L{\ displaystyle L}X{\ displaystyle x}X-1L{\ displaystyle x ^ {- 1} L}

X-1L={z∈LA∗∣Xz∈L}{\ displaystyle x ^ {- 1} L = \ {z \ în A ^ {*} \ mid xz \ în L \}} .

Cu această notație, două cuvinte și sunt inseparabile dacă și numai dacă . Clasele echivalenței Myhill-Nerode sunt deci în bijecție cu reziduurile de . Rezultă că un limbaj este rațional dacă și numai dacă mulțimea reziduurilor sale este finită. În această formă teorema este enunțată în tratatul lui Eilenberg. X{\ displaystyle x}y{\ displaystyle y}X-1L=y-1L{\ displaystyle x ^ {- 1} L = y ^ {- 1} L}L{\ displaystyle L}

Aplicații

Putem folosi teorema pentru a demonstra că un limbaj este rațional arătând că relația este de index finit. Acest lucru se face printr-o explorare sistematică a cuvintelor din cuvântul gol: pentru fiecare cuvânt, căutăm o clasă deja existentă sau creăm o clasă nouă. De exemplu, luați în considerare limba cuvintelor binare care reprezintă numere întregi divizibile cu 3. Cuvântul gol (de valoare 0) și cuvântul 1 sunt separate de cuvântul gol, cuvântul 0 separă cuvântul gol de 1. Avem deja trei clase corespunzând numerelor de repaus 0, 1 și 2 modulo 3. Rămâne să verificăm dacă nu există altă clasă. RL{\ displaystyle R_ {L}}

O utilizare mai frecventă este dovada că un limbaj nu este rațional arătând că indicele relației Myhill-Nerode este infinit. Dacă luăm de exemplu limba cunoscută , atunci două cuvinte și , cu , sunt separabile și separate prin cuvântul (sau ). Deci acest limbaj nu este rațional. L={lanubnu∣nu≥1}{\ displaystyle L = \ {a ^ {n} b ^ {n} \ mid n \ geq 1 \}}X=lanu{\ displaystyle x = a ^ {n}}y=lam{\ displaystyle y = a ^ {m}}nu≠m{\ displaystyle n \ neq m}bnu{\ displaystyle b ^ {n}}bm{\ displaystyle b ^ {m}}

Extensie

Teorema Myhill-Nerode se generalizează în copaci. Vezi automatul copac .

Note și referințe

Note

1. Eilenberg 1974 , Teorema 8.1 (Criteriul coeficientului), pagina 55.

(fr) Acest articol este preluat parțial sau în întregime din articolul din Wikipedia engleză intitulat „  Myhill - Nerode teorema  ” (a se vedea lista autorilor ) .

Literatură

Majoritatea cărților formale de predare a limbajului expun această teoremă.

• Olivier Carton , Limbaje formale, calculabilitate și complexitate: licență și master în matematică sau informatică, opțiunea informatică a agregării matematicii , Paris, Vuibert ,2008, 237  p. ( ISBN  978-2-7117-2077-4 , prezentare online )
• Jacques Sakarovitch , Elements of automata theory , Vuibert ,2003, 816  p. ( ISBN  978-2-7117-4807-5 )Traducere în engleză cu corecții: Elements of Automata Theory , Cambridge University Press 2009, ( ISBN  9780521844253 ) .

• (ro) Samuel Eilenberg , Automate, Limbi și mașini, vol. A , New York, Academic Press , col.  „Matematică pură și aplicată” ( nr .  58)1974, xvi + 451  p. ( ISBN  978-0-12-234001-7 )

Articolul original este:

• Anil Nerode , „  Linear Automaton Transformations  ” , Proceedings of the American Mathematical Society , vol.  9, n o  4,August 1958, p.  541-544.

Articole similare

• Lemă de iterație , o altă metodă pentru a demonstra că un limbaj nu este rațional.
• Monoid sintactic , monoidul de tranziție al automatului minim.
• Automat de copac .

<img src="https://fr.wikipedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" title="" width="1" height="1" style="border: none; position: absolute;">