Monadična logika drugega reda in prepoznavni jeziki

Končne avtomate se lahko obravnava kot matematične modele, ki berejo besede in odločajo o pripadnosti besed jeziku; monadično logiko drugega reda pa kot logični formalizem za izražanje lastnosti besed z uporabo relacij med pozicijami črk v besedah. Čeprav gre na prvi pogled za različna matematična pojma, ju povezuje presenetljiv rezultat, znan kot Büchijev izrek. Ta pravi, da so jeziki, ki jih prepoznavajo končni avtomati, natanko jeziki, ki se jih lahko opiše s stavki monadične logike drugega reda. V članku so predstavljeni osnovni pojmi teorije avtomatov in monadične logike drugega reda ter podan dokaz Büchijevega izreka v obeh smereh.

Monadic second order logic and recognisable languages

Finite automata can be viewed as mathematical models that read words and decide whether they belong to a given language, while monadic second-order logic can be viewed as a logical formalism for expressing properties of words using relations between positions of letters in words. Although these notions appear to be quite different at first sight, they are connected by a remarkable result known as Büchi’s theorem. This theorem states that the languages recognised by finite automata are precisely the languages that can be defined by sentences of monadic second-order logic. This article introduces the basic concepts of automata theory and monadic second-order logic and presents a proof of Büchi’s theorem in both directions.