Väitös: Kaavan pituuspeleillä uutta ymmärrystä logiikoiden tiiviydestä

Matemaattisen logiikan alalla tehdään paljon tutkimusta logiikoiden ilmaisuvoimasta eli siitä, mitä mallien ominaisuuksia logiikan kaavoilla voidaan ilmaista. Annetun ominaisuuden ilmaisemiseen käytetty kaava voi kuitenkin olla kohtuuttoman pitkä. Väitöskirjassaan Miikka Vilander tutkii logiikoiden tiiviyttä eli ominaisuuksien ilmaisemiseen tarvittavien kaavojen pituutta.

– Erityisen vaikea ongelma tiiviyden tutkimisessa on alarajan osoittaminen. Vaikka kaikki mieleen tulevat kaavat, jotka määrittelevät annetun ominaisuuden, olisivat pitkiä, on pystyttävä todistamaan, että lyhyempää kaavaa ei ole olemassa. Kehitän väitöskirjassani useille logiikoille kaavan pituuspelit, jotka toimivat todistusmenetelmänä alarajojen osoittamiseen, Vilander kiteyttää.

Useat väitöskirjassa todistetut alarajat ovat suuruusluokaltaan eksponenttitorneja. Eksponenttitorni on funktio, jonka seuraava arvo on aina kaksi potenssiin edellinen arvo. Näin syntyy erittäin nopeasti kasvava lukujono.

– Eksponenttitorni kasvaa todella nopeasti. Jo viiden korkuinen eksponenttitorni ylittää atomien määrän universumissa. Tämän pituisen kaavan kirjoittaminen on selvästi mahdotonta käytännössä, Miikka Vilander toteaa.

Eri logiikoille kehitetty omat pituuspelit

Vilander kehittää väitöskirjassaan uudet kaavan pituuspelit modaalilogiikalle, modaaliselle myy-kalkyylille, propositionaaliselle tiimilogiikalle sekä yleistetyille säännöllisille lausekkeille. Näistä erityisesti myy-kalkyylin kaavan pituuspeli on erittäin monimutkainen. Tämän pelin avulla Vilander osoittaa epäelementaarisen eron tiiviydessä predikaattilogiikan ja modaalisen myy-kalkyylin välillä.

Propositionaalinen tiimilogiikka liittyy Suomessa paljon tutkittuun tiimisemantiikan aihepiiriin. Tiimilogiikat mallintavat esimerkiksi tietokantateoriassa käytettyjä riippuvuuksia datan muuttujien välillä.

– Tutkin Hannoverissa toimineen kollegani Martin Lückin kanssa perusteellisesti propositionaalisten tiimilogiikoiden yleisimpien atomien määriteltävyyttä muiden operaatioiden avulla. Huomasimme esimerkiksi, että atomien negaatiot ovat usein helpompia määritellä, kuin atomit itse, Vilander kertoo.

Mikkelistä kotoisin oleva Miikka Vilander asuu tällä hetkellä Tampereella ja työskentelee tutkijana Tampereen yliopistossa informaatioteknologian ja viestinnän tiedekunnassa akatemiatutkija Antti Kuusiston johtamassa projektissa Explaining AI via Logic.

Filosofian maisteri Miikka Vilanderin matematiikan alaan kuuluva väitöskirja Succinctness and Formula Size Games tarkastetaan julkisesti Tampereen yliopiston tekniikan ja luonnontieteiden tiedekunnassa perjantaina 23.9.2022 klo 12 alkaen Keskustakampuksella Pinni B -rakennuksen salissa B1096 (Kanslerinrinne 1, Tampere). Vastaväittäjänä toimii professori Juha Kontinen Helsingin yliopistosta. Kustoksena toimii professori Lauri Hella informaatioteknologian ja viestinnän tiedekunnasta.