Succinctness and Formula Size Games

Abstract

Tämä väitöskirja tutkii erilaisten logiikoiden tiiviyttä kaavan pituuspelien avulla. Logiikan tiiviys viittaa ominaisuuksien ilmaisemiseen tarvittavien kaavojen kokoon. Kaavan pituuspelit ovat hyväksi todettu menetelmä tiiviystulosten todistamiseen. Väitöskirjan kontribuutio on kaksiosainen. Ensinnäkin väitöskirjassa määritellään kaavan pituuspeli useille logiikoille ja tarjotaan näin uusia menetelmiä tulevaan tutkimukseen. Toiseksi näitä pelejä ja muita menetelmiä käytetään tiiviystulosten todistamiseen tutkituille logiikoille.

Tarkemmin sanottuna väitöskirjassa määritellään uudet parametrisoidut kaavan pituuspelit perusmodaalilogiikalle, modaaliselle μ-kalkyylille, tiimilauselogiikalle ja yleistetyille säännöllisille lausekkeille. Yleistettyjen säännöllisten lausekkeiden pelistä esitellään myös variantit, jotka vastaavat säännöllisiä lausekkeita ja uusia “RE over star-free” -lausekkeita, joissa tähtiä ei esiinny komplementtien sisällä.

Pelejä käytetään useiden tiiviystulosten todistamiseen. Predikaattilogiikan näytetään olevan epäelementaarisesti tiiviimpi kuin perusmodaalilogiikka ja modaalinen μ-kalkyyli. Tiimilauselogiikassa tutkitaan systemaattisesti yleisten riippuvuuksia ilmaisevien atomien määrittelemisen tiiviyttä. Klassinen epäelementaarinen tiiviysero predikaattilogiikan ja säännöllisten lausekkeiden välillä osoitetaan uudelleen yksinkertaisemmalla tavalla ja saadaan tähtien lukumäärälle “RE over star-free” -lausekkeissa hierarkia ilmaisuvoiman suhteen.

Monissa yllämainituista tuloksista hyödynnetään eksplisiittisiä kaavoja peliargumenttien lisäksi. Tällaisia kaavoja ja tyyppien laskemista hyödyntäen saadaan epäelementaarisia ala- ja ylärajoja yksittäisten sanojen määrittelemisen tiiviydelle predikaattilogiikassa ja monadisessa toisen kertaluvun logiikassa.

This thesis studies the succinctness of various logics using formula size games. The succinctness of a logic refers to the size of formulas required to express properties. Formula size games are some of the most successful methods of proof for results on succinctness. The contribution of the thesis is twofold. Firstly, we define formula size games for several logics, providing methods for future research. Secondly, we use these games and other methods to prove results on the succinctness of the studied logics.

More precisely, we develop new parameterized formula size games for basic modal logic, modal μ-calculus, propositional team logic and generalized regular expressions. For the generalized regular expression game we introduce variants that correspond to regular expressions and the newly defined RE over star-free expressions, where stars do not occur inside complements.

We use the games to prove a number of succinctness results. We show that first-order logic is non-elementarily more succinct than both basic modal logic and modal μ-calculus. We conduct a systematic study of the succinctness of defining common atoms of dependency in propositional team logic. We reprove a classic non-elementary succinctness gap between first-order logic and regular expressions in a much simpler way and establish a hierarchy of expressive power for the number of stars in RE over star-free expressions.

Many of the above results utilize explicit formulas in addition to game arguments. We use such formulas and a type counting argument to obtain non-elementary lower and upper bounds for the succinctness of defining single words in first-order logic and monadic second-order logic.