Logiikka ja tiede

Tilasin Ben-Arin Mathematical Logic for Computer Science oppikirjaksi syksyn matemaattisen logiikan kurssille. Kyseisen kirjan sisältö on melko tarkalleen sama kuin mikä oman tutkimusalani perusta. Ainoa puuttuva palanen, jonka olisin oppikirjalta halunnut, olisi ollut SMT, jota kirjassa ei ilmeisesti käsitellä.

Logiikalla viitataan arkikielessä usein kaikenlaiseen systemaattisen oloiseen päättelyyn, eli prosessiin, jolla tietyistä lähtökohdista tai oletuksista lähtien perustellaan jotakin muuta. Antiikin aikaan logiikalla tarkoitettiinkin lähinnä laadukasta argumentaatiota. Matemaattinen logiikka on periaatteessa joukko abstraktioita, joiden avulla tutkitaan matemaattisen tarkasti, mitä voidaan päätellä ylipäätään. Laskettavuuden teoria nivoutuu yhteen tähän kysymykseen, koska laskettavuus tarkoittaa kysymyksiä siitä miten voidaan päätellä, ja kuinka paljon resursseja (aikaa, muistia, jne) täytyy käyttää jotta päättely voidaan suorittaa loppuun.

Tietojenkäsittelyn ja laskettavuuden teoriaa on joskus vähättelevästi nimitetty "tietokoneohjelmien tutkimiseksi". Tämä on kuitenkin pitkälti virheellinen käsitys asiasta. Pikemminkin kyse on totuuden säilyttävistä siirtymistä erilaisten struktuurien välillä, ja siitä, missä määrin nämä siirtymät on mahdollista toteuttaa ns. normaaleja luonnolakeja noudattavien mekanismien avulla. On esitetty, että ko. ala ei ole "tiedettä", koska siinä ei tutkita mitään tosiasioita, vaan ainoastaan keksitään tai konstruoidaan sellaisia ja sitten tutkitaan näin konstruktioita.

Church-Turingin teesi on eräänlainen paradigmaattinen väittämä, jota pidetään alan jonkinlaisena teoreettisena pohjaoletuksena. Väittämä menee jotakuinkin niin, että jokainen mielekäs laskentaa tai päättelyä tekevä järjestelmä joka on ilmaisu- ja ratkaisuvoimaltaan Turing-vahva, on ekvivalentti Turingin koneen (ja melko suuren joukon muita laskennan malleja) kanssa. Teesi saa jonkin verran vahvistusta siitä, että Chomskyn hierarkia päättyy tyypin nolla kielioppeihin, ja nämä ovat ilmaisuvoimaltaan ekvivalentteja Turingin koneen kanssa.

Päättelyn automatisointi on eräs tärkeä matemaattisen logiikan ja laskettavuuden risteyskohdassa olevaa tutkimusaihetta. Oma tutkimukseni on ollut tällaisen automaattisen päättelyn soveltamista, ja teoreettinen kytkös on melko heikko. Suurimmaksi osaksi työni on keskittynyt tiettyjen modaalilogiikoiden mallintarkastukseen. Mallintarkastus ei viittaa tässä siihen, että rakennetaan malli ja tarkastetaan se (vaikka tällainen tulkinta onkin helppo tehdä, eikä olekaan täysin väärä!), vaan siihen, että tarkastetaan että annettu järjestelmän kuvaus on malli jollekin modaalilogiikan teorialle.  Selitän tarkemmin.

Malliteoria toimii logiikassa osapuilleen näin: Meillä on jokin (formaali) logiikan ilmaisutapa. Esimerkiksi ensimmäisen kertaluvun predikaattilogiikka, tai sitten jokin modaalilogiikka tms. Tällä logiikalla ilmaistaan jokin väittämä, eli käytännössä, kirjoitetaan jokin kaava. Olkoon se "p tai q". Kun meillä on tällainen kaava, kaavassa esiintyville symboleille voidaan antaa tulkinta, esimerkiksi "p" tarkoittaa "ulkona sataa" ja q tarkoittaa "ulkona tuulee". Tulkinta on logiikassa se, mitä olen tieteenfilosofiassa nimittänyt operationalisoinniksi. Tulkinta tehdään jonkin struktuurin suhteen; käytännössä tulkinta on kuvaus, joka antaa symboleille merkityksen struktuurissa. Struktuurimme tässä voisi olla esimerkiksi kaksi mittasuuretta: Ensimmäinen on anturi joka rekisteröi sen päälle putoavia sadepisaroita ja toinen mittari, joka mittaa tuulen voimakkuutta. "Sataa" esimerkiksi operationalisoituu niin, että pisaroita tulee 5 sekunnin sisällä vähintään kolme, ja "tuulee" niin, että tuulen nopeus on vähintään 4 metriä sekunnissa. Ulkona vallitseva säätila on jollakin ajanhetkellä malli tälle kaavalle.

Aikalogiikassa on yksinkertaisten propositiosymbolien lisäksi modaalioperaattoreita. Yksi tällainen (jonka avulla voidaan jo ilmaista paljon) voisi olla binäärinen modaalioperaattori "kunnes". "p kunnes q" tulkittaisiin niin, että "tuulee kunnes sataa". Ulkona vallitseva säätila olisi tämän kaavan malli, jos tuuli ei tyynny ennen sadetta. Tätä voidaan soveltaa moneen asiaan, mutta sitä on perinteisesti sovellettu rinnakkaisten ja reaktiivisten järjestelmien spesifioimiseen. Esimerkkispesifikaatioita voisi olla vaikkapa "asiakas odottaa kunnes asiakasta palvellaan" ´ja "asiakasta palvellaan lopulta, jos asiakas odottaa".  Mallintarkastuksessa siis selvitetään, päteekö annetun systeemin sisällä annettu kaava.

Mitään periaatteellista syytää rajoittua "konstruktioihin" aikalogiikan ja sitä sivuavien menetelmien kanssa ei kuitenkaan ole. Esimerkiksi probabilistista versiota mallintarkastuksesta on sovellettu systeemibiologiaan. Probabilistisessa versiossa aikalogiikasta on modaalioperaattoreita jotka antavat jonkin väittämän paikkansapitävyydelle todennäköisyyden. Esimerkiksi kaava voi olla muotoa "proteiinin X pitoisuus ylittää kynnysarvon Y todennäköisyydellä p, ennenkuin proteiinin Z pitoisuus laskee alle arvon A". Mallintarkastuksessa rakennetaan tällöin jonkinlainen matemaattinen struktuuri, joka itsessään on operationaalisessa suhteessa tutkittavaan kohteeseen - vaikkapa soluun - ja tämän struktuurin vastaavuutta voidaan empiirisesti arvioida. Konstruktio voidaan tehdä käsin teorian pohjalta tai mallinnos voi olla täysin automaattinen mittaustulosten perusteella. Mallintarkastus antaa joukon hypoteeseja, jotka voidaan myöhemmin falsifikoida empiirisesti itse kohteesta.  Takaisinkytkentä malliin voi olla myös täysin automatisoitu.


Opetus jatkuu keväällä tietojenkäsittelyn teorian kurssilla, joka paneutuu logiikan sijaan kompleksisuusteoriaan. Siitä kirjoitan toisella kertaa.