Pelisemantiikka

Pelisemantiikka on logiikassa ja tietojenkäsittelyssä käytetty malli sille, miten esimerkiksi kaavojen totuusarvo tai ohjelman toiminta tai vastaava tulkitaan. Noin yleisemmin "semantiikka" formaaleissa yhteyksissä voidaan ymmärtää kuvauksena joltakin ilmaisuformalismilta matemaattisille objekteille.

Helpoin esimerkki lienee logiikan kaava jossa on konnektiivit "ja" eli && ja "tai" eli ||, sekä "ei", eli !. Nämä konnektiivit voidaan perinteiseen tapaan tulkita eräänlaisiksi algebrallisiksi operaatioiksi jotka kompositionaalisesti sitten määrittelevät totuusarvon alkaen yksittäisten propositioiden totuusarvoista.

Esimerkiksi p && (q || r) pätee, jos p on tosi ja jompi kumpi q:sta ja r:stä on tosi. Jos propositioille on annettu totuusarvo, niin se voidaan yksikäsitteisesti laskea. Pelisemantiikassa ajatellaan toisin, vaikkakin kaavojen totuusarvo tässä tapauksessa on sama kuin perinteisessä semantiikassa. Jokaisen kaavan voidaan ajatella muodostavan pelin, jossa on kaksi pelaajaa, verifioija ja falsifioija. Koska nämä ovat suomalaiselle kömpelöitä ilmaisuja, käytän itse keksimiäni suomennoksia tarkastaja ja kiistäjä. Jos joku lukija on perehtynyt asiaan siinä määrin että tietää paremmat suomennokset, niin korjaan.

Kaava jäsennetään aivan normaalisti, ja pelitilanne ajatellaan muodostuvan osakaavoista P ja Q (negaation tapauksessa vain P) sekä niitä yhdistävästä konnektiivista. Jos kaava on muotoa P && Q, niin tämä tulkitaan olevan kiistäjän pelivuoro, ja kiistäjä valitsee kumpi osakaava otetaan. Jos kaava on muotoa P || Q, niin tarkastaja valitsee kaavan. Kaava !P tarkoittaa että kiistäjä ja tarkastaja vaihtavat päikseen roolia ja peli jatkuu kaavasta P. Jos jäljellä on vain yksi propositio p, niin tarkastaja voittaa jos p on tosi, ja kiistäjä voittaa jos p on epätosi.

Alkuperäisen kaavan katsotaan olevan tosi, jos tarkastajalla on varman voiton strategia. Jos kiistäjällä on varman voiton strategia, kaavan katsotaan olevan epätosi. Propositiologiikassa pelillä on aina yksikäsitteinen varma voittaja, ja kaavan pelisemantiikan mukainen totuusarvo ja perinteinen totuustauluihin perustuva totuusarvo ovat aina samat. Jos propositioiden totuusarvoja ei ole sanottu etukäteen, voidana pelistä muodostaa ns TQBF (totally quantified boolean formula) jossa ensin pelataan peli jossa vuorotellen valitaan propositioille totuusarvot; tällöin kaavan totuusarvo riippuu siitä, kuka saa valita mitkäkin propositioiden totuusarvot.


Ensimmäisen kertaluvun predikaattilogiikassa on pitkälti samanlainen tilanne. Sen selvittäminen, onko annetulla kaavalla malli (ns. satisfiability- ongelma) on pelisemantiikassa sama kuin malliteoriassa, kun valinta-aksiooma on käytössä. Predikaattilogiikan kaavassa pelaajat "omistavat" kvanttorit, ja kiistäjä valitsee universaalikvantifioidut muuttuja, kun taas tarkastaja valitsee eksistentiaalikvantifioidut muuttujat. Eksistentiaalikvanttorien poisto tuottaa ns skolemin funktioita, jotka siis kertovat mikä muuttujan arvo valitaan, rippuen siitä mitä aiemmin on jo valittu; Peliteorian mukainen tulkinta skolemisoinnille itseasiassa on, että skolemin funktiot kuvaavat tarkastajan pelistrategiaa; Jos löytyy ei-tyhjä joukko jolle mainitut funktiot löytyvät, niin kaava on toteutettavissa, ja tarkastaja voittaa pelin.

Formaalissa verifioinnissa tilanne on vielä toinen. Jos verifioimme esimerkiksi tapahtumapohjaista reaktiivista järjestelmää, tämä mallinnetaan usein niin että jos ylipäätään on tapahtumasekvenssi joka vie "pahaan" tilaan, järjestelmässä on virhe. Toisaalta, tämä voidaan ajatella erikoistapauksena pelisemantiikassa: Perinteisessä verifioinnissa on vain kiistäjä, ei tarkastajaa. Jos järjestelmällä on "tarkastaja", niin osa tilosta on tarkastajan hallinnassa, ja tarkastaja voi näissä tiloissa valita tapahtuman, jolla virhetila pyritään välttämään. Erilaisia tietoturvaprotokollia voidaan esimerkiksi verifioida näin. Itse en ole pelisemantiikkaa käyttänyt tai tutkinut työssäni, joten en osaa tästä aspektista kertoa juuri enempää.