Uusia alkuja

Hallinnollinen sekamelska joka yliopistojen yhdistymisestä seurasi, on ollut surkuhupaisaa katseltavaa. Ympärillä monet ihmiset ovat panikoineet ja hyperventiloineet milloin minkäkin organisatorisen yksityiskohdan vuoksi. Yksi asia joka tapahtui vuoden alusta oli, että käytännössä kaikki esimiessuhteet päättyivät, eli vuoden vaihteesta monikaan ei tiennyt kuka oma esimies on. Moni ei myöskään tiennyt lainkaan millaisessa organisaatiossa työskentelee.

Esimieheni tiedän nyt, mutta organisaatiosta minulla ei ole ollut tietoa vuosiin, enkä edes piittaa. Työtehoni on paljon parempi kun yksinkertaisesti en ajattele koko asiaa. Minulle "yliopisto" tarkoittaa kahta eri asiaa. Yhtäältä se tarkoittaa sitä hallinnollista hirviötä, joka maksaa palkkani ja jossa minun työni resurssointi muutoinkin tapahtuu. Tämä sisältää myös sen fyysiset rakennukset, tietojärjestelmät jne. Olen lopulta aika vähän kiinnostunut tästä yliopistosta. Tiedän sen olevan tärkeä edellytys minun työni jatkuvuudelle, ja ehkä jonakin päivänä tämä piittaamattomuuteni siitä mitä siellä tapahtuu ja mitä siellä "pitäisi" tehdä kostautuu.

Toisaalta se tarkoittaa jotakin korkeampaa ideaalia, academiaa. Tämä merkitys kattaa kaiken sen tiedon, jaetut tiedonintressit, akateemiset hyveet ja arvot, joiden palvelukseen olen elämäni omistanut. Se ei riipu sinänsä fyysisistä rakennuksista, eivätkä hallintovirkailijat, tietojärjestelmät, jne ole osa tätä "yliopistoa". Tässä kontekstissa tehtäväni on jakaa, tuottaa, ja käsitellä inhimillistä tietoa.

Viime vuosina on ollut hieman tapetilla ns. grievance studies- alat. En mene tästä nyt kirjoittamaan sen kummemmin; niihin kohdistettu "sokalistinen" hyökkäys taannoin herätti kaikenlaista keskustelua. En ota kantaa keskustelun sisältöön, mutta ilmiönä se, että joku kirjoittaa ilmeistä puppua joka läpäisee seulan (vaikkei pitäisi, ideaalien mukaan) on kiehtova. Keskustelu joka siitä on seurannut ei ole ollut kovin nättiä, mutta se on ollut tarpeellista.

Korostan vielä sivuhuomautuksena että nämä enemmän humanistisen perinteen jatkajina toimivat alat kuuluvat kyllä sinänsä academia-käsitteen alle. Meillä ns kovempien tieteiden edustajilla on usein sellainen hiukan ylimielinen ethos, jonka mukaan humanistinen perinne ei ole arvokas, tai vaikka olisi, ei kuulu samaan instituutioon. Olen tästä eri mieltä. Meidän toki tulee erottaa erilaiset tiedonintressit ja tiedon ja merkitysten käsittelyn tavat -- joskin niiden rajojen yli tulee tarpeen tullen kävellä päättäväisesti -- ja tehdä selväksi se ero,  yhtäältä asiantiloja ja tosiasioita käsittelevien alojen ja tekstien, ja toisaalta merkityksiä, arvoja, ja kokemuksellisuutta käsittelevien alojen ja tekstien välillä.

Mutta jaarittelen. Siis asiaan. Tapasin uuden esimieheni tänään lounaalla. Keskustelumme oli virkistävä ja innostava. Liityin hänen tutkimusryhmäänsä opportunistisesti, sillä tässä kaaoksessa satuin olemaan asemassa jossa sain itse vaikuttaa asemoitumiseeni. Minulla on juuri riittävästi senioriteettiä tutkijana ja opettajana, että minua ei tulla suoranaisesti komentelemaan, ja juuri riittävän vähän, etten joudu tällaisten hallinnollisten myrskyjen keskellä tekemään päätöksiä muiden puolesta. Tällä kertaa tilanne näyttää kehittyvän erittäin otollisesti.

Tutkimusryhmällä on häkellyttävä määrä dataa erittäin mielenkiintoisista ilmiöistä. Heillä on pulaa mallintamisen ja kirjoittamisen hallitsevista henkilöistä -- useimmat tällaiset ihmiset kun ennen pitkää päätyvät johtaviin asemiin joissa aika menee muuhun kuin siihen mikä heidän vahvuutensa on. En nyt ala ruotimaan yksityiskohtia, mutta miellyttävän asiantilasta tekee se, että tutkimusaiheena on tällä kertaa oikeasti talous. Tämä on sikäli hauskaa, että amatööritaloustieteilijänä olen harrastuksekseni pyöritellyt matemaattisia malleja. Nyt voin tehdä sitä yhdessä ammattilaisten kanssa ja vieläpä estimoida parametrejä. Työni tulee olemaan empiiristä, mikä lämmittää sieluani.

Olen ollut elämässäni hävyttömän onnekas. Olen pohjimmiltani tavattoman laiska. Tahtoo sanoa, muutun hyvin nopeasti kyvyttömäksi tekemään jotakin mikä ei kiinnosta tippaakaan. Tällä kertaa voin vaihtaa alaa johonkin mistä olen, jos nyt en varsinaisesti haaveillut, niin ainakin leikitellyt ajatuksella hieman mielessäni idealisoiden. Minulle on useimmissa asioissa elämässäni käynyt näin. Toisin kuin monet muut minun tilanteessani, en ole muodostanut tästä sellaista identiteettiä että minä olisin "saavuttanut" jotain "omilla ansioillani". Olen vain sattunut olemaan oikeassa paikassa oikeaan aikaan varsin usein. 

Oikea Työ

Ihmisillä on yleensä jonkinlainen intuitiivinen käsitys siitä, mikä juuri heidän mielestään on oikeaa työtä. Olen joskus käsitellyt asiaa taloustieteen keinoin tässäkin blogissa, enkä nyt ole tekemässä syvällisempää analyysiä asiasta. Mainitsen kuitenkin siitä hieman, ennen varsinaista asiaa.

Markkinatalousyhteiskunnassa työksi katsotaan usein sellainen toiminta, josta joku maksaa tai ainakin periaatteessa olisi valmis maksamaan, tai josta on jokin selkeä hyöty, joka ainakin teoriassa olisi siirrettävissä jollekin muulle kuin tekijälle itselleen esimerkiksi myymällä se. Esimerkkinä työstä voisi olla auton korjaaminen. Vaikka auton korjaaminen tehtäisiin itseä varten, siitä on silti taloudellinen hyöty (vaihtoehtoiskustannuksen muodossa).

Toisaalta esimerkiksi kuntosaliharjoittelu ei ole "työtä", vaikka siitä hyötyä onkin, sillä kyseinen hyöty ei ole sinänsä mitenkään myytävissä. Toki voimme ajatella ammattimaisen kehonrakentajan tai valokuvamallin treenaamista "työnä", mutta tällöin se on pikemminkin investointi, ja verrattavissa esimerkiksi opiskeluun.

En tässä käy erittelemään sen laajemmin, olkoon tämä riittävä taustoitus.

Olen ollut palkkatyössä yksityisellä sektorilla nyt reilu vuoden. Vaikka olen tehnyt kokoaikaista työtä palkkaa vastaan käytännössä yhtäjaksoisesti (vanhempainvapaita lukuunottamatta) nyt 19 vuotta, on käytännössä kaikki muu työni tehty erilaisille yliopistoille tai tutkimuslaitoksille, joissa palkanmaksajana on viime kädessä ollut valtio tai muu veroja keräävä instanssi. Nytkin suurin osa palkastani päätoimestani tulee tällaiselta taholta, mutta sivutoimeni on yksityisessä yrityksessä.

Työ on mielenkiintoista ja palkitsevaa. Ei sillä, etteikö yliopistossa työskentely olisi. Esimerkiksi opinnäytetöiden ohjaaminen ja opettaminen, samoin kuin aika-ajoin iso osa tutkimustyöstäkin on mielenkiintoista ja tunnetasolla palkitsevaa. Tutkimuksen ongelma julkisella puolella minulle on ollut se, että minun on ollut vaikea uskoa että se kohdistuu asioihin joilla on suurempi kokonaismerkitys. Jos olen nostanut abstraktiotason riittävän korkealle, olen voinut ajatella palvelevani ihmiskunnan korkeampia hyveitä, tieteellisen tiedon edistämistä, säilyttämistä, ja elävöittämistä. Tarkoitan elävöittämisellä sitä, että sen sijaan että jokin teoreettinen tieto säilytettäisiin kirjoissa ja kansissa puhtaana abstraktiona, sen soveltaminen ja toistaminen uudelleen hieman toisenlaisena pitää sen "elossa", eli että on ihmisiä jotka uudelleen ja uudelleen kokevat "löytäneensä" samat ilmiöt.

Tällainen tuntuu toki helposti haihattelulta, mutta inhimillinen tieto joka on vain kirjoissa ja tiedostoissa, ei ole "tietoa" vaan ainoastaan jonkinlainen indeksi tai avain tietoon; siitä tulee tietoa vasta, kun tietoinen (sic) olento kuten ihminen omaksuu sen ja asettaa kontekstiin jossa se vaikuttaa tämän olennon käyttäytymiseen ja ajatteluun. Mutta jaarittelen jälleen.

Kaikesta ylevästä ajattelusta huolimatta, tutkimus jota olen tehnyt, on vain vähäisessä määrin ollut oikeaa työtä markkinatalouden kontekstissa. En varsinaisesti pidä tätä minään suurena rikoksena, mutta kokisin olevani antisosiaalinen ja moraaliton jos en lainkaan kokisi tätä ongelmaksi. Kovin äänekäs ja vaikutusvaltainen vähemmistö akateemisista ihmisistä käyttää merkittävässä määrin paukkuja julkisuudessa sellaisen ajatuksen ylläpitoon, että koska tieto itsessään on tärkeää, on eräänlainen puhdas arvovalinta, kuinka paljon julkinen valta panostaa akateemiseen tutkimukseen, ja että tämä arvovalinta on valinta jonkinlaisen näköalattoman "taloudellisen" vääjäämättömyyspuheen ja korkeampien inhimillisten ideaalien välillä.

En pidä tätä täysin rehellisenä, vaikka itse peräänkuulutankin näitä korkeampia inhimillisiä ideaaleja. Olen opiskellut aikanaan sosiologiaa, kansantaloustiedettä ja matematiikkaa, olen nuorempana lukenut kaikki vähänkään mielenkiintoiselta kuulostavat tai vaikuttavat teoriaopukset, kohtuullisen määrän kaunokirjallisuutta ja paljon asioita jotka olen jo enemmän tai vähemmän unohtanut. Olen tehnyt keskinkertaisen akateemisen uran, jonka seurauksena olen tällä hetkellä matemaattisen logiikan ja tietojenkäsittelyn dosentti ja yliopistonlehtori; Tutkimukseni ovat perinteisesti keskittyneet siihen, miten logiikkaa voi soveltaa algoritmisesti erilaisten formaalisti määriteltävissä olevien järjestelmien ominaisuuksien spesifiointiin ja verifiointiin (eli suomeksi, sen tarkastamiseen toimiiko jokin kone tai tietokoneohjelma "oikein"). Korkeammat ideaalit joita olen koettanut näistä tutkimuksista jalostaa, ovat epistemologisia: Miten voimme ylipäätään tietää, että olemme tutkimassa oikeaa asiaa, miten voimme tietää että ominaisuus jonka toteamme olevan voimassa, takaa sen toiminnan jota intuitiivisesti toivomme? Miten voimme saada tämän tiedon ulos ja mikä on se "tieto" johon vertaamme?

Nämä asiat ovat inhimillisesti tietämisen arvoisia, mutta ne ovat arvokkaita minulle kokemuksena. Ne eivät ole siirrettävissä kuin hyvin hyvin rajallisesti muille. Olen tätä blogia kirjoittaessani usein ajatellut että kirjoittamani teksti kommunikoi tätä korkeampaa ideaalia ja tietoa muille tai edes dokumentoi sen johonkin muotoon, mutta epäilen että suurin osa lukijoistani ei koskaan lue näitä tekstejä, eikä tällä tiedolla todellisuudessa ole mitään muuta arvoa kuin se arvo joka minulla on henkilökohtaisena kokemuksena. Ja tämä kalvaa minua. Epäilen sen kalvavan monia suulla suuremmalla puhuvia julkkis- ja huippututkijoita, joiden kaunopuheiset akateemisen ajattelun puolustuspuheet "arvovalinnoista" ja pinnallinen kritiikki "taloudellisten arvojen hirmuvaltaa" vastaan herättävät ihastusta. Korkeampien inhimillisten ideaalien puolustajat jakavat näitä puheenvuoroja sosiaalisessa mediassa ja näin viestittävät viiteryhmälleen jakavansa nämä arvot.

En puhu näitä arvoja vastaan. En edes erityisemmin haasta sitä kritiikkiä. Karsastan yksisilmäistä hyötyajattelua ja ajatusta siitä, että akateemisen tutkimuksen tulisi tähdätä taloudelliseen hyötyyn. En esitä että rahoitusta pitäisi suunnata teollisuusyhteistyöhön tai että pitäisi tiukentaa kriteerejä tai esittää lisää vaatimuksia. Mutta puhun sitä vastaan, että näitä puheenvuoroja toistetaan papukaijan lailla pysähtymättä miettimään, mikä inhimillinen kustannus näiden korkeampien ideaalien tavoittelulla on, ja mikä on meidän vastuumme muista ihmisistä ja yhteiskunnasta.

Työni yksityisellä sektorilla tähtää taloudelliseen hyötyyn. Markkinatalous toimii siten, että kun teen jotain jolla on arvoa muille, nämä muut maksavat siitä. Yritys jolle teen työtä, laittaa toteuttamani algoritmin tuotteeseensa. Tuotteen käyttäjät saavat tästä hyötyä itselleen ja ovat siksi valmiita maksamaan yritykselle enemmän. Ketjun päässä jonkun elämä hieman helpottuu. Joku pääsee kotiin viitisen minuuttia aikaisemmin ja on valmis maksamaan tästä muutaman euron viikossa. Tämä tapahtuu tuhansille ihmisille, ja osa tuosta rahasta virtaa yritykselle, joka sitten maksaa minulle palkkaa.

Olemme sokeita arvoille jotka eivät kosketa omaa elämäämme. Korkeita ideaaleja ja meille tärkeitä asioita tavoitellessamme usein jätämme huomiotta kaikki ne, jotka mahdollistavat meille tämän tavoittelun. Saatamme kirjoittaa nasevan kolumnin karvaisista miehistä jotka pitävät infran toiminnassa, muttemme pysähdy miettimään sitä, missä määrin omassa elämässämme vedämme niitä köysiä jotka liikuttavat koko tätä koneistoa. Emmekä me edes teoriassa pysty siihen; Tämän tiedän niistä perustuloksista, joiden parissa olen painiskellut tutkimusta tehdessäni, juuri näitä korkeampia ideaaleja tavoitellessani.

Maailma on monimutkainen paikka. En paheksu hedonisteja. Se ei ole minun tehtäväni. Mutta kummeksun sitä, miten joku voisi edes teoriassa kokea elämänsä merkitykselliseksi ja itsensä arvokkaaksi pelkästään näiden korkeiden ideaalien tavoittelussa, ilman että osallistuu. Enkä sano edes että ihmisen tarvitsee työskennellä yksityiselle sektorille, tai edes yliopistomaailman ulkopuolella tehdäkseen niin. Osallistua voi monella tavalla.

Olen tällä viikolla arvostellut kaksi opinnäytetyötä, antanut 6 tuntia opetusta luokkahuoneessa, ja nyt etsin koodista virheitä (käännös näyttää olevan valmis ja testiajo ohi, joten joudun lopettamaan). Huomenna opetan taas pari tuntia, laadin koko joukon harjoitustehtäviä ensi viikoksi ja kirjoitan vastineen alkusyksyn opiskelijapalautteeseen. En tiedä onko mikään tästä hyödyksi kenellekään muulle. Toivon niin.

Syyt ja seuraukset.

Mielenkiintoinen kirja, jota olen hiljakseen lukenut kesän aikana on "The Book of Why". Kirja ei rehellisesti sanoen ole kovin hyvä, koska se hypettää ja selittää vaikeasti asiaa, joka on lopulta aika yksinkertainen. Alla kirjoitan aiheesta mutten ota sitä suoraan kirjasta, vaan se on kirjan inspiroimaa, ja lopussa kommentoin kirjaa suoremmin. 

Me kaikki "tiedämme", että korrelaatiosta ei voi päätellä kausaalisuutta. Jäätelön syönti kasvaa kesällä samaa tahtia hukkumiskuolemien kanssa, mutta ymmärrämme kaikki, ettei jäätelön syömisen kieltäminen vähennä hukkumiskuolemia. Kukko laulaa aina hieman ennen auringonnousua, mutta aurinko nousee varsin hyvin vaikka kukko ei laulaisikaan.

Muistetaan vanha kunnon bayesilainen päättely. En nyt ala tässä sitä kampaamaan sen enempää, siinä keskiössä on ehdollisen todennäköisyyden käsite. Jos meillä on tapahtuma A, jonka todennäköisyydestä olemme kiinnostuneita, ja olemme tehneet havainnon B, niin merkitään P(A | B):llä ehdollista todennäköisyytta, eli todennäköisyyttä että A tapahtuu kun tiedämme että B on tapahtunut. Esimerkiksi, jos tiedämme (tämä on esimerkki, en tiedä onko oikeasti näin, huom), että 75% autokolareista jompi kumpi osapuoli on ajanut ylinopeutta, niin nähdessämme kolarin (B), arvelemme että todennäköisyys on noin 75% että toinen tai molemmat ovat ajaneet ylinopeutta (A).

Tämä ei kerro tietenkään sitä, kuinka todennäköistä on että ylinopeutta ajava joutuu kolariin. Tätä todennäköisyyttä merkittäisiin P(B | A).  Näillä on kuitenkin yhteys, ja se tunnetaan Bayesin kaavan nimellä, eli P(B | A) = P(A | B)*P(B)/P(A).  Tämän tietääksemme meidän pitää siis tietää myös kuinka yleistä ylinopeus on, ja kuinka yleisiä kolarit ovat.  Ja jos ylinopeus on hyvin yleistä, mutta kolarit hyvin harvinaisia, niin tämä todennäköisyys voi olla paljonkin pienempi kuin P(A|B).

Bayesilainen päättely ei kuitenkaan itsessään vangitse varsinaisesti mitään tietoa kausaalisuudesta. Voimme aivan hyvin arvioida ym. todennäköisyyksiä ilman minkäänlaista käsitystä mikä seuraa mistäkin, eikä toisaalta tällaista todennäköisyyksien tunteminen itsessään auta meitä mitenkään päättelemään mikä on syy ja mikä seuraus.

Esimerkiksi Tampereella vuosittain arvuutellaan päivämäärää, jolloin Näsijärvi jäätyy, ja toisaaltaa päivämäärää, jolloin Näsijärvestä lähtee jäät. Kevään mittaan voimme olla kokolailla varmoja, että jos meillä on lämpömittari sopivassa paikassa Näsijärven rannalla, niin sopivina päivinä mitatut lämpötilat paljastavat meille paljonkin siitä, milloin jäät ovat lähdössä. Emme kuitenkaan voi nopeuttaa jäiden lähtöä esimerkiksi pitämällä tulitikkua tällaisen lämpömittarin alla. Ymmärrämme intuitiivisesti, että lämpömittarin lukema ei vaikuta jäiden sulamiseen, vaan lämpömittarin lukemaan ja jäiden sulamiseen vaikuttaa yhteinen tekijä, ilman lämpötila.

Merkitään tätä lämpömittariin (tai johonkin muuhun tapahtumaan B) vaikuttamista uudella operaattorilla, do(B). Tämä tarkoittaa, että jonkin (eksplisiittisen tai implisiittisen) mallimme ulkopuolelta tulevan tekijän avulla pakotamme B:n tapahtumaan.  P(A | B) on eri asia kuin P(A | do(B)), koska edellisessä me havaitsemme B:n tapahtuvan, ja jälkimmäisessä me aiheutamme B:n tapahtumisen.

Miten me voimme karakterisoida kausaalisuutta? Jos P(A | do(B) ) > P(A | do(!B)), niin tämä tarkoittaa että kun pistämme B:n tapahtumaan "väkisin", niin A:n todennäköisyys kasvaa. Tällöin B:n tapahtumisella on jokin kausaalinen suhde A:han. Se ei kuitenkaan tietenkään tarkoita että B jotenkin suoraan aiheuttaa A:n. Välissä voi olla montakin mekanismia.

En nyt tässä lähde kampaamaan kaikki erilaisia kausaalisia suhteita joita erilaisilla muuttujilla voi olla; Pearlin keskeinen argumentti on, että vaikka emme sinänsä voi päätellä pelkän datan perusteella kausaalisuutta, voimme päätellä, onko kausaalisuutta suhteessa tiettyihin oletuksiin. Lisäksi oletukset joita täytyy tehdä, eivät ole kovin vahvoja, eivätkä ne ole kovin "epätieteellisiä", eikä niitä tarvitse vetää hatusta.

Tämä tapahtuu ns. kausaalisten verkkojen avulla. Siinä relevantit muuttujat otetaan mukaan ja niistä muodostetaan graafi. Kaikkien teoriassa mahdollisten suorien kausaalisten suhteiden kohdalla piiretään nuoli. Otetaan tässä nyt kaksi esimerkkiä, tupakointi-syöpä ja hiilidioksidipäästöt-maapallon keskilämpötila, joiden kausaalista suhdetta haluamme selvittää.

Jos esitämme että jokin tupakoinnista riippumaton syy on sekä tupakoinnin että keuhkosyövän syy, niin voimme piirtää verkon jossa tämä (tuntematon) syy aiheuttaa molempia, ja tupakointi vain potentiaalisesti aiheuttaa syöpää. Me emme kuitenkaan voi tästä vielä päätellä vielä paljokaan, vaan tarvitsemme joko jonkin muuttujan joka taatusti liittyy tupakointiin mutta ei (suoraan) tähän ulkopuoliseen tekijään, tai sitten muuttujan joka liittyy tähän ulkopuoliseen tekijään, muttei (suoraan) tupakointiin.

Tällaisia muuttujia on muutama. Ensinnäkin, tupakoivilla ihmisillä keuhkoihin kertyy pieniä määriä tervaa. Tietenkään kaikille tupakoiville ei näitä tervajäämiä tule, mutta tällä ei ole merkitystä, kunhan korrelaatio on riittävän suuri.  Toisekseen, tiedetään että tupakointi ja turvavyön käyttö ovat tilastollisessa yhteydessä siten, että tupakoivat ihmiset käyttävät turvavöitä vähemmän kuin tupakoimattomat. Tässä korrelaatio ei ole kovin suuri, mutta se on riittävän suuri, että tilastoissa se, että henkilö ei käytä turvavyötä, on riskitekijä keuhkosyövälle jos mitään muuta ei huomioida. 

Jos meillä on kuvitteellinen mekanismi joka aiheuttaa sekä tupakointia että keuhkosyöpää, niin kysymys kuuluu a) onko mielekästä olettaa, että tämä mekanismi aiheuttaa tervan kertymistä keuhkoihin ja b) onko mielekästä että tämä mekanismi aiheuttaa sitä, että henkilö ei käytä turvavyötä. Oli mekanismi mikä hyvänsä, niin a)-kohdassa voimme postuloida esimerkiksi että syöpää aiheuttaa geeni, joka vähentää vierasaineiden poistumista keuhkoista ja siten saa tervaa kertymään keuhkoihin, ja että tämä toisaalta saa nikotiinin yms imeytymään keuhkoista herkemmin ja näin lisää todennäköisyyttä että henkilö alkaa tupakoida. b)-kohdassa on paljon vaikeampaa keksiä yhteyttä.

Ja katso: Tilastollisesti keuhkosyövän ja turvavyön käytön korrelaatio katoaa täysin, jos tehdään regressioanalyysi jossa keuhkosyöpää selitetään tupakoinnilla ja turvavyön käytöllä.  Tervajäämien kohdalla tilanne on hieman toisenlainen. Siinä voimme tehdä muutamia erilaisia "temppuja", joilla voimme tutkia riippumatonta suhdetta näiden välillä; En mene tässä kaavasulkeisiin, mutta Pearl:in do-kalkyylin avulla pystymme näyttämään, että jos oletus on ettei ulkopuolinen tekijä suoraan vaikuta tervan määrään keuhkoissa (vaan ainoastaan tupakoinnin välityksellä), niin tupakointi aivan yksiselitteisesti aiheuttaa keuhkosyöpää.

Tästä saamme siis myös falsifikaatiokriteerin. Jos todella löydämme esimerkiksi yllä postuloidun syöpää ja nikotiininhimoa aiheuttavan geenin, niin voimme todellakin vielä löytää keinon kumota johtopäätös. Niin kauan kun tällaista geeniä tms mekanismia ei löydy, paras arvauksemme on että tupakointi todella aiheuttaa syöpää.

Maapallon keskilämpötilaa tutkiessa taas otamme relevantiksi muuttujaksi hiilidioksidipäästöt -- tämä on ainoa asia johon voimme edes teoriassa soveltaa do- operaattoria. Tämän lisäksi otamme esimerkiksi vulkaanisen toiminnan ja erilaiset biologiset prosessit jotka myös tuottavat hiilidioksidia. Näistä kaikista tulee vetää nuoli ilmakehän hiilidioksidipitoisuuteen, joka on yksi relevantti muuttuja. Tämän lisäksi otetaan muuttujiksi auringon aktiivisuus, muunlaiset hiukkaset ilmakehässä,  maan pinnan albedo, jne. Näiden välille piirretään kaari jos on mitään syytä olettaa, että muuttuja vaikuttaa toiseen. Esimerkiksi ei ole mielekästä vetää viivaa hiilidioksidipäästöistä auringon aktiivisuuteen. 

Nyt voimme tutkia aikasarjoista näiden muuttujien välisiä suhteita. Pearlin do-kalkyylin avulla voimme laskea esimerkiksi hiilidioksidin kausaalisen suhteen lämpötilaan, kun tunnemme potentiaaliset muut syyt. En ala tässä nyt kampaamaan sitä, miten näin voimme todistaa hiilidioksidipäästöjen todella lämmittävän maapalloa, sillä do-kalkyyli on varsin työläs viedä läpi. Lopputulos on kuitenkin hyvin samanlainen kuin syövän ja tupakoinnin kohdalla: Olettaen että tunnemme relevantit juurisyyt, meidän ei tarvitse tuntea todellakaan kaikkia välittäviä mekanismeja voidaksemme päätellä kausaalisen yhteyden. Se, että esimerkiksi meret sitovat enemmän tai vähemmän lämpöä tai merivirrat jakavat lämmön eri tavoin maapallolla kuin mallit ennustavat, on epäolennaista; olennaista on se, onko meillä kaikki mahdolliset kausaaliset tekijät tiedossa. Näistä me yksinkertaisesti tiedämme että jos mahdollisia tekijöitä ovat hiilidioksidipitoisuus, erilaiset hiukkasjäämät, vesihöyry ja pilvisyys, ja auringon aktiivisuus, niin on täysin varmaa, että hiilidioksidipäästöt lämmittävät maapalloa.

Tietenkin, on mahdollista, kuten yllä, että on jokin tuntematon luonnonvoima joka lämmittää maapalloa. Esimerkiksi maapallon ytimestä vapautuu jostain syystä lämpöä joka pääsee jostain maankuoressa olevasta reiästä ilmakehään. Tai ehkä maapallo on ontto ja etelänavalla olevasta luukusta päästetään aika-ajoin lämmintä ilmaa maapallon sisuksista ilmakehään. Tai ehkä kuu lämmittää enemmän kuin aiemmin osasimme arvioida. Jne.

Monelle -- myös minulle -- Pearlin argumentaatio ja esitystapa tuntuvat ylenpalttiselta hypetykseltä. Tämä ei tarkoita etteivätkö kausaalisten verkkojen käyttö ja do-kalkyyli olisi hyödyllisiä innovaatioita. Aikanaan kun opiskelin ekonometriaa, osa näistä menetelmistä opetettiin, osaa taas ei. Esimerkiksi Pearlin "Back-door"-kriteeri oli minulle uusi. Esimerkiksi ns instrumentti-muuttujien käytölle löytyy perustelu aika hyvin Pearlin do-kalkyylistä, joskin Pearl antaa hieman eri kriteerit instrumenttimuuttujien käytölle.

Perinteisesti instrumenttimuuttujia käytetään kun meillä on kausaalinen suhde A:sta B:hen, mutta selittävässä muuttujassa A:ssa on mittausvirhettä, joka voi korreloida tuntemattomalla tavalla B:n kanssa, ja jolle ei mallissa ole selittäjiä. Tällöin "instrumentoidaan" etsimällä muuttuja(t) X siten, että A:n sijaan käytämme X:n avulla estimoitua Â:ta. Tässä oletus on, että siinä määrin kuin  ja A eroavat toisistaan, tämä heijastelee mittausvirhettä, ja Â:n ja B:n välinen suhde paljastaa "todellisen" vaikutuksen. Tämän perusteluna on, että jos todella kontrolloisimme A:n, niin havaintodatassa läsnä oleva kohina joka voi vaikutta B:hen ei tulisi enää kontrolloinnin jälkeen näkymään do(A):ssa; Â:n katsotaan vastaavan lähemmin do(A):ta.  Pearl esittää asian hieman toisin, mutta ero on minusta pitkälti filosofinen. En ole katsonut varsinaista matematiikkaa läpi, sillä Book of Why ei sisällä matemaattista esitystä tässä kohtaa sillä tasolla että voisin verrata.

Kaikenkaikkiaan tilastollinen kausaalinen päättely on kiehtova laji. Pearlin keskeinen "argumentti" on, että vanha nyrkkisääntö "correlation does not imply causality" on otettu liiaksi aksiomaksi ja se on tulkittu puritaanisesti  niin, ettei havaintoaineistosta voisi päätellä mitään kausaalisuudesta, korkeintaan kumota yksittäisiä hypoteeseja muttei koskaan validoida mitään. Olen tästä samaa mieltä. Havaintoaineistosta voidaan tehdä johtopääksiä suhteessa kausaalisiin oletuksiin. Kausaalisia oletuksia puolestaan voidaan tehdä varsin paljon aivan arkisen tietämyksen ja ymmärryksen varassa, ja joka tapauksessa, kun ei voida olla varmoja, on (epistemologisesti) turvallista olettaa kausaalisuus joka sitten voidaan (joskus) osoittaa vääräksi havaintoaineiston perusteella. Toisalta Pearl minusta sotkee pakkaa liiaksi esittämällä monimutkaisen "kausaalisuuden portaat"- argumentin.

Pearl esittelee kolme "kausaalisuuden porrasta", joista ensimmäinen on puhtaat havainnot. Tämä on taso jolle perinteinen tilastollinen analyysi jää, sillä korrelaatiot, ehdolliset todennäköisyydet, yms ovat kaikki matemaattisesti symmetrisiä siinä mielessä, ettei ole mitään keinoa pelkän tilastomatematiikan keinoin sanoa että mikä on kausaalinen suhde ja mikä ei. Toisella tasolla Pearl esittää interventiot eli kontrolloidut koejärjestelyt. Siinä havainnon lisäksi voidaan tehdä koe,  jossa muuttujia manipuloidaan. Tämä on taso jossa do-operaattoreita sovelletaan yksittäisiin suhteisiin, kuten esimerkiksi kun tehdään kaksoissokkokoe jonkin lääkkeen tehon tutkimiseksi. Toinen taso kykenee jo vastaamaan kysymyksiin kuten "mitä (todennäköisesti) tapahtuu jos teemme asian X".  Kausaalisuuden kolmas porras on ns kontrafaktuaalien taso. Siinä vastataan kysymyksiin kuten "X tapahtui, mutta mitä jos se ei olisi tapahtunut?". Tämä taso on se, joka minusta jäi vähän hämäräksi, sillä ensiksikään, en näe miksi eteenpäin suuntautuva hypoteesi ja menneisyyteen suuntautuva kontrafaktuaali olisivat mitenkään eri asemassa analyysin suhteen; Kausaalisessa verkossa kyse on vain suunnasta johon laskenta etenee, eikä siten mitenkään syvällisestä filosofisesta erosta.

Ymmärrän näiden kahden jälkimmäisen tason eron lähinnä psykologisena; Taso 2 viittaa yksittäisiin suhteisiin, se on eräänlainen feed-forward tarkastelu yhden kontrolloidun muuttujan kausaalisuuden suhteen (mitä tapahtuu jos painan tästä), kun taas taso 3 mahdollistaa laajan suunnittelun, jossa tutkitaan useita haluttuja ulostuloja, ja ratkaistaan kysymyksiä kuten "mitä kaikkia pitää painaa tai vetää jotta saamme tämän ylös ja tuon alas".

Kaikenkaikkiaan ihan viihdyttävää lukemista. En suosittele vakavaksi kirjaksi ihmisille jotka haluavat soveltaa asioita teknisesti omiin analyyseihin, mutta suosittelen kaikille niille, jotka kuvittelevat ettei havaintoaineistosta voi tehdä mitään johtopäätöksiä.

Reiluus

Reiluus (engl. fairness) viittaa rinnakkaisten järjestelmien teoriassa suunnilleen sitä, että järjestelmän mallissa otetaan huomioon vain sellaiset äärettömät suoritukset, joissa kaikki komponentit etenevät jossain vaiheessa. Esimerkiksi, jos meillä on kaksi toimijaa, jotka tahtovat käyttää jotain jaettua resurssia (esimerkiksi tulostin, jolla kahdelta eri koneelta tulostetaan) jatkuvasti, niin järjestelmä on reilu, jos molemmat pääsevät halutessaan lopulta tulostamaan.

Käsite on intuitiivisesti ensialkuun selkeä, mutta analysoitaessa tarkemmin, se hajoaa käsiin. Käytetään esimerkkiä jossa kahdelta eri tietokoneelta tulostetaan samalla tulostimella.  Protokolla on seuraavanlainen: Koneelta tulee yksi pyyntö kerrallaan tulostaa paperi. Tulostin valitsee jomman kumman pyynnön ja palvelee sitä. Toinen pyyntö jää voimaan ja tulostamisen jälkeen tulostin valitsee uudelleen. On kuitenkin mahdollista, että ensimmäinen kone on tällä aikaa päättänyt pyytää uuden paperin tulostamista, ja tulostin valitsee sen jäälleen. Toisen koneen pyyntö on koko ajan voimassa, mutta sitä ei koskaan toteuteta. Niin sanottu heikko reiluus sanoo, että jos jokin toiminto on koko ajan mahdollinen, järjestelmä lopulta todella suorittaa sen, eli että järjestelmässä ei ole sellaista ääretöntä suoritusta, jossa pyyntö olisi koko ajan (teoriassa) mahdollista toteuttaa, mutta sitä ei toteuteta.


Todellisuudessa kuitenkin pyyntö menee tulostimen jonoon. Tulostin ottaa jonosta pyynnön ja tulostaa sen. Jos jono toimii niin, että sinne mahtuu "paljon" pyyntöjä, ja ne käsitellään aina järjestyksessä, ongelmaa ei juurikaan ole. Mutta oletetaan että jonoon mahtuukin vain yksi pyyntö (tai jokin pieni määrä). Jos jonossa on yksi pyyntö, tulostin ottaa sen käsittelyyn ja jono tyhjenee (tai sinne mahtuu yksi lisää).  Nyt kuitenkin ensimmäinen kone ehtii tulla takaisin pyytämään ja laittaa oman pyyntönsä jonoon ennen kuin toinen ehtii sitä esittää. 


Nyt siis pyynnön esittäminen ei ole mahdollista silloin, kun jono on täynnä.  Vaikka jokainen todella esitetty pyyntö tulee käsitellyksi, toinen koneista ei pääse esittämään pyyntöään koska se ei ole mahdollista välillä. Järjestelmä ei intuitiivisesti katsottuna ole reilu, mutta heikko reiluus ei tätä mahdollisuutta tavoita. Vahva reiluus taas sanoo, että jos jokin tapahtuma on äärettömän usein mahdollinen (vaikka se välillä olisikin mahdoton), niin se lopulta tapahtuu. Eli vaikka jono välillä on täynnä eikä pyyntöjä voi esittää, vahvasti reilu järjestelmä takaa että toinenkin kone lopulta pääsee esittämään pyyntönsä.

Reiluuden ongelmana on, että se on erittäin hankala mallintaa, ja se on kiusallinen laskennallisesti, verrattuna sellaisiin ominaisuuksiin kuten turvallisuus ja lukkiumat. Turvallisuus viittaa siihen, että esimerkiksi pyynnöt eivät mene sekaisin, eli ei tapahdu tilannetta jossa molemmat koneet kuvittelevat tulostavansa samanaikaisesti (ja esimerkiksi sivulle tulisi kahta eri tekstiä päällekäin tms). Turvallisuusrikkomus voidaan havaita jos järjestelmä päätyy tilaan jossa molemmat koneet kuvittelevat tulostavansa.

Myös lukkiumat ovat helppo todeta; lukkiuma on järjestelmän tila, jossa se ei pääse lainkaan etenemään. Jos esimerkiksi tulostimen ja koneiden välinen jono menee rikki niin, että kumpikin kone näkee jonon olevan täynnä (ja näin jää odottamaan että saisi laittaa sinne pyynnön), ja tulostin kuvittelee että jono on tyhjä (ja näin odottaa pyyntöjä), järjestelmä lukkiutuu. 

Ajatellaan nyt protokollaa joka hoitaa jonkin tällaisen järjestelmän toimintaa. Siinä ei ole jonoa, mutta siinä on eräänlainen "odotushuone". Jokainen joka haluaa päästä tulostamaan -- nimitetään tätä asiakkaaksi -- ilmaisee halunsa tulostaa laittamalla "lipun" päälle. Kummallekin asiakkaalle on oma lippunsa.  Kun asiakas on laittanut lipun päälle, tämä menee "välitilaan"  kirjoittamaan "nimikirjaan" toisen asiakkaan nimen. Tämä tapahtuu riippumatta siitä, mitä nimikirjassa luki. Tämän jälkeen asiakas menee odottamaan. Odottaessaan asiakas tarkastaa, onko nimikirjassa tämän oma nimi vai joku muu. Jos kirjassa on oma nimi, niin asiakas pääsee tulostamaan. Jos siinä ei ole omaa nimeä, asiakas tarkastaa onko kenelläkään lippu päällä. Jos lippuja ei ole päällä, asiakas pääsee myös tulostamaan. Tulostettuaan asiakas laittaa lipun alas.

Tässä järjestelmässä asiakas ei voi "etuilla" muita. Jos joku muu on esittänyt pyynnön, niin kun asiakas esittää pyynnön (eli laittaa lipun päälle), hän samalla antaa vuoron toiselle. Asiakkaat eivät voi estää toisiaan laittamasta lippuja päälle. He voivat viivästyttää toista ainoastaan jäämällä välitilaan jossa lippu on laitettu päälle mutta nimikirjaan ei ole kirjoitettu mitään.  Järjestelmä ei kuitenkaan vaadi edes heikkoa reiluutta, ainoastaan oletuksen, että kumpikaan ei vapaaehtoisesti pysähdy välitilaan, odottamaan, tai tulostamaan.

Me tiedämme että tämä järjestelmä toimii ilman reiluusoletuksia. Vaan entä jos järjestelmä onkin rikki?

Kuvitallaan että asiakas ei tarkastakaan toisen lippua, vaan jää vain odottamaan, että toinen asiakas antaa vuoron. Tällöin asiakas jää odottamaan kunnes toinen asiakas on antanut vuoron ja siirtynyt itse odottamaan. On selvää, että tällainen järjestelmä ei toimi kunnolla -- kuvittele järjestelmä jossa voit tulostaa ainoastaan jos joku muu yrittää myös tulostaa.  Jos kuitenkin mallinnamme järjestelmän niin, että kukaan ei jää odottamaan minnekään, se näyttää toimivan oikein, koska kumpikin yrittää tulostaa uudelleen ja uudelleen. Me toki tiedämme että jos sallimme asiakkaan jäädä paikoilleen alkutilaan, niin virhe paljastuu.

Yleisemmin, ominaisuus joka tässä yleensä tarkastetaan on, että lopulta pyyntöön vastataan. Mutta tämä rikkinäinen järjestelmämme näyttää oikealta jos emme osaa huomioida sitä, että asiakas saattaa alkutilassa jäädä paikoilleen.  Heikko reiluuskaan ei auta suoraan, mutta me voimme saada virheen kiinni, jos laitamme alkutilaan silmukan, jossa asiakkaan on lupa junnata paikallaan. Tällöin saamme aikaan äärettömän suorituksen, jossa pyyntö on esitetty, mutta siihen ei ole mahdollista vastata (koska toinen asiakas pyörii loputtomiin eikä koskaan pyydä mitään), ja olettamalla että reiluus koskee vain välitilaa, odotusta, ja tulostamista. Tämä on kuitenkin varsin hankala mallintajalle, koska mallintajan täytyy ikään kuin tietää missä tilassa virhe voi syntyä ennen kuin hän edes sitä lähtee etsimään.

Ongelma tässä on se, että järjestelmän alkuperäinen malli näyttää oikealta, koska asiakkaalle ei olla mallinnettu muuta mahdollisuutta kuin se, että tämä jatkuvasti esittää pyyntöjä. Huomattavasti luontevampi malli olisi sellainen, jossa asiakas voi todeta että "olen saanut tarpeekseni" tulostettuaan, ja tämä siirtyy tilaan jossa ei enää voida tehdä mitään. Tällöin toki järjestelmä saattaa lukkiutua, mutta lukkiutumisen kohdalla riittää spesifioida erikseen se, onko lukkiuma sallittu vai ei. Eli, jos annamme asiakkaalle mahdollisuuden päättää "nyt loppui" ja parkkeerata itsensä, meidän pitää sallia sellainen lukkiuma (ja vain sellainen) jossa kaikki asiakkaat ovat lopettaneet tyytyväisinä.

Tämä siksi, että on intuitiivisesti selvää ettei asiakkaan pyyntöihin vastaamisen ehtona pitäisi olla se, että toinenkin asiakas pyytää jotain. Jos teemme näin, niin huomaamme, että kun toinen asiakas lopettaa tyytyväisenä, toinen on tuomittu jumittamaan odotustilaan; löydämme lukkiuman joka ei ole sallittu ja virhe paljastuu. Alkuperäisessä järjestelmässä näin ei käy, koska odottava asiakas näkee että toisen asiakkaan lippu on alhaalla, ja pääsee tulostamaan kaikessa rauhassa.

Kun tutkimme jonkin pyynnön toteutumista, nimitämme tällaista ominaisuutta ei-pakotetuksi pyynnöksi (unforced request). Se tarkoittaa, että asikkaalla tulisi olla mahdollisuus kieltäytyä esittämästä pyyntöjä, ja järjestelmän oikeellisuus tulisi säilyä. Pääsemme näin eroon reiluudesta ainakin tässä nimenomaisessa tapauksessa.

Kuvitellaan nyt että rikomme jo rikkonaista protokollaa lisäksi niin, että asiakas ei muistakaan kirjoittaa mitään nimikirjaan. Tällöin siis asiakas vain laittaa lipun päälle ja menee tarkastamaan onko nimikirjassa oma nimi. Nimikirjassa on jonkun nimi, ja tämä joku pääsee loputtomiin käsiksi resurssiin, mutta koska kukaan ei sitä muuta, toinen asiakas puolestaan jää odottamaan loputtomiin.  Huomaisimme tässä kyllä virheen, mutta tehdään lisäoletus: Kun asiakas päättää ettei se enää halua palvelua, se parkkeeraa itsensä, ja vasta sitten kirjoittaa nimikirjaan toisen asiakkaan nimen.

Tällöin käy niin, että niin kauan kun kumpikin asiakas haluaa resurssia, ensimmäinen saa sen käyttöönsä loputtomiin kun taas toinen ei saa sitä lainkaan. Vasta kun ensimmäinen lopettaa, toinen saa vuoron. Tässä kohtaa emme saa virhettä kiinni pelkästään lukkiumia ja turvallisuusominaisuuksia tarkastelemalla, mutta järjestelmällä on kuitenkin ääretön suoritus jossa toinen prosessi odottaa. Reiluutta ei kuitenkaan tarvita mihinkään, ainoastaan oletus että kumpikaan asiakas ei odota loputtomiin.

Nimitämme tällaista ominaisuutta englanninkielisellä ilmaisulla eventual access (en keksinyt hyvää suomennosta). Se tarkoittaa että spesifioimme tilapredikaatteja jotka eivät saa olla voimassa äärettömässä suorituksessa. Emme siis oleta mitään reiluudesta tässä kohtaa, vaan yksinkertaisesti sanomme että "ei ole lupa jättää asiakasta odottamaan äärettömästi". Tämä on hieman samanlaista kuin reiluus, mutta se on eri roolissa; Reiluus on oletus joka tehdään jotta voidaan erottaa aidot virheet silmukoiden alispesifioinnin tuottamista "artefakteista".

Rikkinäisessä järjestelmässä on eventual-access rikkomus, sillä niin kauan kun ensimmäinen asiakas hakee palvelua, tämä saa sitä loputtomiin ja toinen asiakas ei saa mitään. Vasta kun ensimmäinen lopettaa, toinen pääsee resurssiin. Käytännössä tämä näkyy niin, että järjestelmällä on silmukka jossa toinen asiakas odottaa.

Jos siis spesifioimme että järjestelmälle on spesifioitu sallitut lukkiumat, turvallisuus (eli se, ettei resurssia käytetä yhtä aikaa) sekä eventual access- ominaisuus ja varmistamme että mallinnoksessa on huomioitu unforced request, niin voimme saada kaikki em. virheet kiinni ilman mitään erillisiä reiluusoletuksia.

Tämä artikkeli on nyt kirjoituksen alla.

Todesta sen näköisyydestä.

Opetan tällä periodilla todennäköisyyslaskentaa. Tämä on vähän joillekin vaikeasti hahmotettava matematiikan haara. Ensiksikin täytyy erottaa toisistaan muutama asia. Tilastotiede tai tilastomatematiikka ja todennäköisyyslaskenta tai todennäköisyysteoria. Näillä on toki kytkös, mutta ne eivät ole sama asiaa. Todennäköisyysteoria on täysin koherentti matemaattinen teoria, jonka kytkös reaalimaailmaan (joka toki voidaan tehdä) on epäolennainen itse teorian kannalta. Todennäköisyysteoria on välttämätöntä mm. informaatioteorialle, mutta toki myös tilastotieteelle.

Tilastotiede puolestaan on matemaattisia menetelmiä käyttävä "työkalutiede", joka tutkii nimenomaan reaalimaailman ilmiöitä mm. todennäköisyysteorian tarjoamin keinoin. En puhu tilastotieteestä tässä. Olen sitäkin jonkin verran opiskellut ja tietoisena Dunning-Kruger-efektistä, en halua kommentoida asiaa muutoin kuin että kuten yleensäkin, kytkökset reaalimaailmaan ovat ongelmallisia ja ihmisten halu saada enemmän sanottua kuin on epistemologisesti perusteltua, on varsin suuri ja se näkyy tavassa jolla tilastotiedettä käytetään.

Todennäköisyyslaskenta voidaan kokonaisuudessaan johtaa erittäin vähäisestä määrästä aksiomia. Oletetaan että meillä on perusjoukko Omega, ja sille sigma-algebra F. Kuten nokkelimmat lukijani tietävät sigma-algebra on kokoelma perusjoukon osajoukkoja siten, että se sisältää tyhjän joukon ja on suljettu komplementin ja (numeroituvien) leikkausten ja unionien suhteen. Ns. Kolmogorovin aksiomat sanovat että meillä on todennäköisyysmitta P, joka on määritelty kaikille F:n joukoille, ja jolle pätee:

1.  Kaikille F:n joukoille E, P(E) on määritelty ja ei-negatiivinen reaaliluku.
2. P(Omega) = 1
3. Jos A on pistevieraiden joukkojen A_i yhdiste, niin P(A) on summa P(A_i):stä. 

Näistä aksiomista lähtien voidaan todistaa monia asioita. Esimerkiksi se, että jos  on A:n komplementti, niin P(A) = 1 - P(Â), sillä A ja  ovat pistevieraita ja niiden yhdiste on Omega. Käytän tässä yhdisteestä merkkiä + ja leikkauksesta merkkiä *, jolloin saamme että P(A+B) = P(A) + P(B) - P(A*B).

Sanomme sigma-algebran F alkioita tapahtumiksi. Tapahtumien todennäköisyyksistä voidaan johtaa uusia käsitteitä, esimerkiksi P(A | B) = P(A*B)/P(B), joka on niin kutsuttu ehdollinen todennäköisyys. Niin kauan kun pysytään todennäköisyyslaskennan puolella, kaikki toimii kiltisti eikä tarvitse huolehtia mistään reaalimaailman ilmiöistä kuten siitä, mitä todennäköisyys oikein tarkoittaa. 

Todennäköisyyslaskenta olisi kuitenkin tylsää, jos meillä ei olisi sille mitään sovelluksia. Se soveltuukin varsin hyvin sellaisten ilmiöiden ominaisuuksien tutkimiseen joissa kaikkea tietoa ei ole paljastettu, vaan jossa tunnemme vain joitain mahdollisia lopputuloksia ja vain osan mekanismista jolla lopputulos syntyy. Esimerkikisi nopanheitto on melko tyypillinen ilmiö jota mallinnetaan todennäköisyyslaskennan avulla. Kuusisivuisen nopan kohdalla "Omega" on joukko {1,2,3,4,5,6}, ja F on kaikkien Omegan osajoukkojen kokoelma. Olettaen että noppa todella on hyvin lähelle kuution muotoinen, ja että emme voi tietää nopanheiton olosuhteista mitään sellaista, minkä vuoksi uskoisimme nopan päätyvän tiettyyn asentoon ennemmin kuin johonkin toiseen, mallissa oletetaan että todennäköisyysmittta P antaa jokaiselle yhden alkion joukolle todennäkisyyden 1/6.

Yleensä kytkös reaalimaailmaan tehdään niin, että määritellään satunnaismuuttuja. Satunnaismuuttuja, vaikkapa x, ei ole luku sinänsä, vaan se voidaan ajatella jonkinlaisena "kurkistusluukkuna todellisuuteen". Se tuottaa jonkin Omegan alkion kun sen arvo "katsotaan". Tämä "katsominen" määritellään usein satunnaiskokeeksi, ja satunnaiskokeen kuvaus on olennaisilta osin todennäköisyysteorian mallin (joka siis sisältää Omegan ja todennäköisyysmitan P) operationalisointi. Esimerkiksi satunnaismuuttuja x noppaesimerkissämme on se luku, joka lukee nopan päällimmäisellä sivulla välittömästi nopanheiton jälkeen; jos haluamme uuden x:n arvon, täytyy noppaa heittää uudestaan. Jos meillä on tapahtuma A, niin se realisoituu annetussa kokeessa, jos x:n kokeessa saama arvo kuuluu joukkoon A.

Tässä operationalisoinnissa tarvitaan sitten tulkinta. Tulkinnalla tarkoitetaan tässä yhteydessä sitä,  millä kriteereillä todennäköisyysmittaa pidetään oikeana tai sopivana jos mallia verrataan todellisuuteen.

Todennäköisyyden niin kutsuttu frekventistinen tulkinta on seuraava: Satunnaismuuttuja x saa koejärjestelyissä arvot x_1, x_2, .... (näitä on loputtomiin). P(A)  on tapahtuman A suhteellinen esiintymisfrekvenssi, kun koetta toistetaan loputtomiin. Esimerkiksi frekventistinen tulkinta nopanheitosta on, että P({1}) = 1/6, koska jos noppaa heitettäisiin loputtomiin, ykkösiä olisi koko ajan tarkemmin ja tarkemmin kuudesosa kaikista heitoista; pieniä heilahduksia voisi toki tulla, mutta "ajan oloon" heittoja olisi niin paljon että kuudesosa olisi aina vain parempi ja parempi likiarvo ykkösten osuudelle.  Malli jossa jokaiselle luvulle on annettu todennäköisyys 1/6 on väärä, jos eri nopanheittojen suhteelliset osuudet eivät lähesty näitä arvoja.  Frekventistisessä tulkinnassa on tapana tehdä hypoteesi (mukamas) a priori, ja sitten tehdä jokin "riittävän" suuri määrä kokeita, ja todeta hypoteesi oli väärä, koska saatu tulos oli varsin epätodennäköinen. Tässä on ongelmansa, joihin en tässä kohtaa mene sen syvemmälle.

Bayesilainen tulkinta on hieman toisenlainen. Siinä todennäköisyysmitta kuvaa meidän käsitystämme ilmiöstä ja sitä tietoa mitä meillä on.  Esimerkiksi nopanheittojen todennäköisyyksiksi asetetaan a priori 1/6, koska emme yksinkertaisesti tiedä mitään syytä tai perustelua miksi jokin toinen nopanheitto esiintyisi useammin kuin toinen. Kun koetta sitten toistetaan riittävän monta kertaa, voimme muodostaa erilaisille hypoteeseille todennäköisyyksiä. Hypoteeseille annetaan etukäteen jonkinlaiset priorit eli todennäköisyydet tai uskottavuusmitat. Esimerkiksi, bayesilainen voisi todeta, että koska 99% nopista on varsin  laadukkaita eikä niitä ole painotettu, niin kautta linjan 1/6- todennäköisyydet antavan tuloksen priori P(H) = 0.99, ja muiden yhteensä 0.01. Jos nopanheittoja tehdään 100, ja suhdeluvut näyttävät että puolet tuloksista on kutosia, niin tämä on jo erittäin epätodennäköistä.  Tämän arvioimiseen käytetään Bayesin kaavaa, joka sanoo että
P(H | E) = P(E | H) P(H) / P(E). Eli, hypoteesin todennäköisyys tietäen että meillä on evidenssi E, saadaan laskettua kun meillä on todennäköisyys jolla H:n ollessa tottaa E todella tapahtuisi, kertaa H:n priori, jaettuna evidenssin todennäköisyydellä. Olennaista on, että tästä pitäisi tulla uusi H:n priori jatkossa.

Tähänkin liittyy tiettyjä ongelmia, joista vähäisin ei suinkaan ole priorien valinta. Suurin ongelma joka Bayesilaisuuteen liittyy on kuitenkin sosiaalinen: Bayesilaiset ovat pääsääntöisesti ylimielisiä mulkeroita, jotka sivuuttavat todelliset ongelmat ja kuittaavat ne kriitikioiden "ymmärtämättömyydellä". Itse pidän itseäni 80% bayesilaisena, 15% frekventistinä ja 5% skeptikkona, mutta tämä on vain seurausta siitä, että olen päivittänyt prioreitani evidenssin perusteella. Luvut saattavat vaihtua.

Homma menee teoriapuolellakin rumaksi, kun todennäköisyyslaskentaa aletaan soveltaa kapeammin. Esimerkiksi, alamme tehdä oletuksia siitä, että todennäköisyysmitta on esitettävissä ns. tiheysfunktion avulla. Tiheysfunktio on kuvaus Omegalta ei-negatiivisille reaaliluvuille siten, että summa (tai jokin yleistys summasta) F:n joukkojen yli tuottaa todennäköisyysmitan. Esimerkiksi jos Omega on jokin reaalilukujen osajoukko, niin F on niiden Omegan osajoukkojen kokoelma jotka ovat Borel-joukkoja, ja P(A) määritellään integraalina f:stä joukon A yli.

Vaikka matemaattisesti tällaiset teoriat toteuttavat toki Kolmogorovin aksiomat, ne synnyttävät reifikaatioita, eli sellaisia kognitiivisia vinoumia jotka kiinnittävät ajattelun näihin käsitteisiin. Aivan erityisen vaarallinen tällainen reifikaatio on odotusarvo. Odotusarvo -- jota kansanomaisemmin kutsutaan myös keskiarvoksi, vaikka keskiarvo tarkoittaakin eri asiaa -- on operaattori joka voidaan määritellä sellaiselle todennäköisyysmallille jossa on tiheysfunktio ja jossa Omegan alkioille on määritelty reaali- tai kompleksilukujen kertolasku. Omega voi siis olla aivan hyvin jokin vektoriavaruus tms, kunhan reaaliluvulla kertominen on mielekäs operaatio Omegan alkiolle.
Jos x on satunnaismuuttuja, niin merkitsemme sen odotusarvoa E(x). 

Odotusarvo saadaan kun lasketaan satunnaismuuttujan "todennäköisyydellä painotettu keskiarvo", eräänlainen todennäköisyysjakauman painopiste. Kiltisti käyttäytyvillä jakaumilla odotusarvo on varsin hyödyllinen työkalu. Esimerkiksi nopanheiton odotusarvo on 3.5. Jos pelaamme noppapeliä jossa nappulat siirtyvät silmäluvun verran eteenpäin, niin voimme saada aika hyvän arvion siitä, kuinka pitkälle nappulat liikkuvat tietyssä määrässä vuoroja, kun käytämme odotusarvoa, etenkin kun kierroksia on useita.  Odostusarvo on hyödyllinen myös uhkapeleissä yms, etenkin pelin järjestäjälle, sillä kun pelejä pelataan paljon, odotusarvon pitää olla pelin järjestäjälle suosiollinen. 

Toinen suure, joka voidaan tällaisissa malleissa määritellä -- joskin hieman harvemmin -- on varianssi. Kun saamme erilaisia tuloksia, ne eivät tietenkään osu tarkalleen odotusarvon kohdalle, mikäli ilmiö todella on satunnainen (eli satunnaismuuttuja ei saa samoja arvoja joka kerta). Jos muutujan arvoille on määritelty etäisyysmitta, niin määrittelemme uuden satunnaismuuttujan z,
joka on x:n etäisyys sen odotusarvosta. Tällöin varianssi on E(z²). Jos x saa reaalilukuarvoja, on tapana määritellä V(x) = E((x - E(x))²). Varianssin neliöjuuri on nimeltään keskihajonta.

Jos ja kun satunnaismuuttujalle on määritelty varianssi ja odotusarvo, niitä on tapana merkitä kreikkalaisilla kirjaimilla joita tässä blogissa on tuskallista käyttää. Niinpä käytän odotusarvosta merkintää mu ja keskihajonnasta merkintää sigma. Jos emme tiedä todennäköisyysmallista mitään muuta kuin odotusarvon ja varianssin, emme voi sanoa erilaisista todennäköisyyksistä kovin paljoa, mutta voimme sentään todeta jotain. Niin sanottu Tschebyshevin epäyhtälö (T-epäyhtälö tästedes) sanoo, että P(|x - mu| > t) on korkeintaan (sigma/t)². aivan erityisesti, jos t = k*sigma, niin P(|x - mu| > k*sigma) on korkeintaan 1/k:n neliö; esimerkiksi se, että jokin tapahtuma joka kokonaisuudessaan poikkeaa odotusarvosta yli 5 keskihajontaa, tapahtuu korkeintaan  4% todennäköisyydellä. Tämä kannattaa pitää mielessä.

Jakaumat joilla on odotusarvo ja varianssi ovat "yleisiä" sikäli, että jos tiedämme että ilmiön numeroarvot ovat rajoitettuja, niin mikä tahansa "kunnollinen" ilmiötä kuvaava malli on sellainen että odotusarvo ja varianssi löytyvät. Esimerkiksi ihmisten pituus ei voi alittaa 0 metriä, eikä ihminen voi olla pituudeltaan esimerkiksi yli 15 kilometriä, koska silloin hän ei pystyisi hengittämään seistessään.

Ehkä vaarallisin teoreema, joka tällaisia todennäköisyysmalleja koskee on niin sanottu keskeinen raja-arvolause. KRA sanoo, että jos meillä on ääretön jono toisistaan riippumattomia satunnaismuuttujia x_i, joiden odotusarvot ja varianssit ovat olemassa eivätkä ne käyttäydy "patologisesti", esimerkiksi, jonon odotusarvot ja varianssit ovat kaikki jotakin epsilonia suurempia ja jotakin ylärajaa K pienempiä, niin saadaan seuraavaa: olkoon y(n) = x_i:den summa n:ään asti, mu(n) = odotusarvojen summa n:ään asti  ja sigma(n) = keskihajontojen summa n:ään asti. Satunnaismuuttuja z(n) = (y(n) - mu(n))/sigma(n) lähestyy normaalijakaumaa N(0,1) kun n lähestyy ääretöntä.

KRA on vaarallinen, koska se saa ihmiset uskomaan, että kunhan n on riittävän suuri, niin normaalijakauma on riittävän hyvä. Tämä pätee toki tietyssä mielessä, mutta se pätee vain niillä muuttujien arvoilla jotka eivät ole liian kaukana alkuperäisten jakaumien häntäpäistä. Normaalijakauma on jatkuva jakauma ja se on täysin symmetrinen, ja siinä kaukana odotusarvosta olevat arvot käyvät hyvin nopeasti äärimmäisen epätodennäköisiksi.

Tästä ilmiöstä on omaan koprolaliaa ja huonoja käytöstapoja yhdistelevään tyyliinsa kirjoittanut mm. Nassim Taleb, sinänsä sisällöllisesti ansiokkaasti. Pidän miehestä ja hänen kirjoituksistaan, mutta kuten niin monet mielenkiintoiset ihmiset, hän on täysin vailla käytöstapoja, itseään täynnä ja muutenkin jonkin sortin ihmisperse. Tämä ei tietenkään tee hänen sanomisiaan mitenkään huonoiksi, vaan pikemminkin päinvastoin. Se osoittaa etteivät tällaiset asiat ole oikeasti kovin voimakkaasti kytköksissä toisiinsa. Joku vetänee johtopäätöksen että "nerot ovat vaikeita" -- tämä voi pitää paikkaansa sikäli, että todennäköisyys että joku on vaikea ihminen kasvaa, jos hän on nero.

Mutta kannattaa muistaa sanonta: Ekstraordinary claims require extraordinary evidence. Tämä sanonta voidaan palauttaa viime kädessä Bayesin kaavaan. P(A | B) = P(B|A)P(A)/P(B). Jos A on epätodennäköinen (esim, "henkilö on nero") ja B on varsin todennäköinen (henkilö on vaikea), ei suurikaan ehdollinen todennäköisyys toiseen suuntaan (nero on vaikea) tuota mitään kovin suurta evidenssiä toiseen suuntaan (vaikea ihminen on nero).

Blogivinkki.

Hyvä ystäväni, Oxfordin professori ja Royal Societyn jäsen, Stefan Kiefer on alkanut pitää Blogia. Stefan on miellyttävä tuttavuus, tutustuin häneen 2010 Oxfordissa ollessani. Tuolloin hän oli post-doc- tason tutkija kuten minäkin, mutta voin sanoa suoraan että selvästi lahjakkaampi ja omistautuneempi alalle.

Kävimme yhdessä pari kertaa jumalanpalveluksessa. Stefan on harras katolinen ja käy kirkossa useita kertoja viikossa. On erittäin palkitsevaa, että hän kirjoittaa juuri kyseisestä aiheesta, sillä Oxfordissa ollessani tutkin oikeastaan juurikin ensimmäisen blogikirjoituksen aihetta yhdessä Hongyang Qu:n kanssa.

Stefanin blogikirjoitus esittää Markovin mallin, joka eroaa hieman siitä, jota me tarkastelimme, eli niin sanotun Markovin ketjun. Markovin ketju on stokastinen prosessi joka siirtyy diskreetin aika-askeleen välein tilasta toiseen tietyllä todennäköisyydellä.  Omassa tutkimuksessani keskityimme Markovin päätösprosesseihin. Ero näiden mallien välillä on, että Markovin ketju liikkuu "itsestään" ja sen siirtymistä tilasta toiseen ei voi ulkopuolelta säätää. Tällainen malli on generatiivinen, eli se vain synnyttää tietyn jakauman käyttäytymisiä.  Markovin päätösprosessissa puolestaan kussakin tilassa ulkomaailma ja malli vaikuttavat niin, että ulkomaailma voi "tönäistä" järjestelmää. Siinä missä Markovin ketjun tilasta lähtevät siirtymät todennäköisyyksineen summautuvat ykköseksi, Markovin päätösprosessissa ulkomaailma antaa jonkin signaalin ja näin valitsee useista eri jakaumista.

Blogikirjoituksella on myös toinen kytkös omaan työhöni, sillä se käsittelee myös ns Büchi-automaattia, joka on yksi ns. omega-automaattien tyyppi. Büchi-automaatti tunnistaa äärettömiä merkkijonoja hieman samaan tapaan kuin äärellinen automaatti tunnistaa äärellisiä merkkijonoja. Erona on, että ääretön merkkijono tunnistetaan jos se saa automaatin käymään jossakin hyväksymistilassa äärettömän monta kertaa. Büchi-automaatti on käytännöllinen tässä suhteessa, mutta se on tietyssä mielessä hieman -- en oikein keksi parempaa sanaa -- autistinen, eli sen avulla ei ole helppo vangita vuorovaikutukseen liittyviä äärettömien suorituksen kysymyksiä.

Esimerkiksi jos meillä on malli joka tuottaa merkkijonon jossa vain toistuu ababab.... loputtomiin, ja Büchi-automaati sisältää kaksi tilaa (1 ja 2), ja se siirtyy tilasta 1 tilaan kaksi aina kun se saa syötteen "a" ja tilasta 2 tilaan 1 kun se saa syötteen "b", niin jos toinen tiloista on hyväksyvä, automaatti hyväksyy kyseisen merkkijonon. En nyt mene yksityiskohtiin enempää, mutta tällainen automaatti ei kykene ilmaisemaan sellaisia asioita kuin että "tutkittava järjestelmä lakkaa tuottamasta merkkijonoja". Siksi Büchi-automaatin kanssa toimittaessa yksinkertaisesti oletetaan ettei näin koskaan käy. Tämä puolestaan asettaa mallintajalle tietynlaisia suitsia, ja tämä puolestaan rajoittaa sellaisten asioiden ilmaisua kuten "järjestelmä voidaan ajaa alas kontrolloidusti". Tein aiheesta väitoskirjan kymmenen vuotta sitten, enkä ala tässä nyt enempää asiaa ruotimaan.

On aina ilo nähdä kuinka ihmiset kirjoittavat mielenkiinnosta aiheeseen. Stefan on keskustelijana ja opettajana ensiluokkainen, ja ennen kaikkea hän on alan rautainen asiantuntija. Odotan mielenkiinnolla mitä muuta hän kirjoittaa.

Deskriptiivinen kompleksisuus

Kompleksisuusteoria on tietojenkäsittelytieteen osa-alue, joka käsittelee sitä, miten tehokkaasti tietynlaiset ongelmat voidaan ratkaista, kun käytössä on jokin tietty formalismi jolla laskentaa tms suoritetaan. Esimerkiksi, meillä on taulukko (tai muu vastaava tietorakenne) A, jossa on lukuja.  Emme nyt problematisoi lukujen esittämisen vaatimia resursseja (suuren luvun esittäminen vaatii paljon bittejä), vaan abstrahoimme tässä nyt sen osan pois. Oletetaan, että taulukon koko on n, ja me pääsemme käsiksi taulukon i:nteen alkioon vakioajassa. Viittaamme tähän alkioon A[i].  Oletamme että kaikki taulukon alkiot ovat erisuuria. (Tämä oletus ei ole olennainen tai välttämätön, mutta teen sen typografisista syistä...)

Tehtävämme on siirrellä taulukon alkioita siten, että siirtelyn jälkeen taulukko on järjestyksessä. Tämä tarkoittaa sitä, että jokaisella kokonaisluvulla i välillä 1 < i < n+1 pätee että A[i-1] < A[i]. Tämä ei siis päde alussa. Meillä on käytössämme kaksi operaatiota, V(i,j), joka vaihtaa taulukon alkiot i ja j keskenään, sekä vertailuoperaatio A[i] < A[j].

Emme nyt keskustele siitä, miten tarkalleenottaen toteutamme taulukon järjestämisen. Oletamme että taulukko on alussa täysin sekaisin, emmekä tiedä mitään esimerkiksi siitä, mitä arvoja taulukossa on ja miten ne ovat jakautuneet. Voimme ilmaista taulukon järjestämisen permutaation etsimisenä, ja tarkastelemme ongelman kompleksisuutta tästä näkökulmasta.

Koska alkiot ovat erisuuria, on keskenään erilaisia tapoja laittaa alkiot taulukkoon n! kappaletta, missä n! = 1*2*...*n. Tämä tulee siitä, että ensimmäinen alkio voi olla mikä hyvänsä n:stä alkiosta, tämän jälkeen toinen voi olla mikä hyvänsä jäljellä olevista, jne. Näistä n!-kappaleesta permutaatioita meidän tulee löytää se, joka vastaa taulkon järjestyksessä olemista.

Jokainen vertailu, jonka taulukolle teemme, paljastaa meille jotain siitä, minkälaisen permutaation tarvitsemme. Tarkalleenottaen, kaikkien vielä mahdollisten permutaatioiden joukosta yksi vertailu sulkee pois tarkalleen puolet. Nimittäin, vertaamalla A[i] < A[j], (missä i < j) tulos on "kyllä" tasan silloin kun nämä alkiot ovat oikeassa järjestyksesä ja "ei" silloin kun oikeassa permutaatiossa ne ovat eri järjestyksessä. Muuta informaatiota emme yksittäisestä vertailusta (yleisessä tapauksessa) saa. Yhden vertailun (ja mahdollisen vaihdon) jälkeen permutaatiota on jäljellä n!/2, ja jokainen vertailu vastaavasti puolittaa permutaatioiden määrän. Tätä puolittamista on pahimmassa tapauksessa jatkettava kunnes permutaatioita on enää yksi. Tiedämme, että tällöin olemme tehneet log(n!) puolitusta. log(n!) on suunnilleen n*log(n), mikä tarkoittaa, että pahimmassa tapauksessa taulukon järjestämiseksi täytyy tehdä (osapuilleen) tämän verran vertailuja ja vaihtoja.

Tämä on yksinkertaisimpia analyysejä joilla voidaan tarkastella miten kompleksinen jokin ongelma on; tämä paljasti siis, että taulukon järjestäminen ei onnistu (aivan) suoraan taulukon kokoon verrannollisessa ajassa.

Vaikeampien kysymysten analysoiminen on usein -- niin -- vaikeampaa.  Deskriptiivinen kompleksisuusteoria on teoria, joka yksittäisten ongelmien kompleksisuuden sijaan pyrkii luokittelemaan ongelmia sen mukaan, millä tavoin ne ovat ilmaistavissa. Oletetaan, että meillä on syötteenä jokin struktuuri ja jollakin logiikalla ilmaistu ominaisuus, ja tehtävänä on selvittää, onko annetulla struktuurilla tämä ominaisuus. Ongelman vaikeus riippuu siitä, millaisia ilmaisutapoja logiikassa on käytössä.

Esimerkiksi, jos meillä on annettu syötteenä graafi (eli suomeksi "verkko", mutta käytän tätä termiä välttääkseni sekaannusta) ja jokin ensimmäisen kertaluvun predikaattilogiikan kaava ja annettu joukko predikaatteja, voimme itseasiassa hyvinkin helposti tarkastaa onko kaava tosi. Tässä siis oletamme, että nämä predikaatit todella on annettu, eli pystymme suoraan laskemaan niiden arvon mille tahansa alkioille. Esimerkiksi "Kaikille solmuille x,y, pätee että niiden välillä on kaari" Tai "on olemassa solmut x, y, z siten, että (x,y) on kaari ja (y,z) on kaari".

Tätä ei pidä sekoittaa siis sellaiseen tilanteeseen jossa on annettu kaava, ja pitää selvittää päteekö kyseinen kaava ylipäätään jollekin mallille, eikä myöskään tilanteeseen, jossa predikaattien arvoja ei tunneta, ja pitäisi tietää voidaanko predikaateille antaa sellainen tulkinta, jolla kaava pätee annetulle struktuurille.

Ongelmat, jotka on ilmaistavissa tällä tavalla, ovat luokassa FO (sanoista First Order), ja deskriptiivisen kompleksisuusteorian yksi tulos on, että tämä luokka on sama kuin AC0, joka puolestaan tarkoittaa ongelmia jotka voidaan ratkaista hyvin tehokkaasti; Jokaiselle tällaiselle ominaisuudelle on olemassa hierarkia ongelman ratkaisevia logiikkapiirejä, joiden syvyys (perättäisten porttien määrä) on rajoitettu.  On huomattava, että tämän luokan yksittäisen ongelman karakterisoi nimenomaan yksittäinen predikaattilogiikan kaava (joka kullekin ongelmalle on kiinteä), ja mahdollisten struktuurien joukko.

FO ongelmat eivät ole esimerkiksi graafeille kovin mielenkiintoisia, koska vaikkapa kysymystä "Onko kahden annetun solmun välillä polku" ei voidan ilmaista ensimmäisen kertaluvun predikaattilogiikalla.

Jos haluamme nimittäin karakterisoida jälkimmäisen tapauksen, niin tarvitsemme toisen kertaluvun logiikkaa. Täysi toisen kertaluvun logiikka antaa meille mahdollisuuden ilmaista esimerkiksi sen, että "on olemassa predikaatti P(x,y) siten, että...". Aivan vielä emme kuitenkaan ota näin vahvaa ilmaisuvoimaa mukaan.

Transitiivinen sulkeuma on operaatio, jonka lisääminen FO:iin tuo sopivasti ilmaisuvoimaa. Esimerkiksi, jos syötteenä on suunnattu graafi, niin meillä on automaattisesti käytössämme predikaatti p(x,y), joka sanoo että solmusta x on solmuun y vievä kaari. Lisäämme logiikkaamme operaattorin TC, joka toimii siten, että jos Q(x,y) on osakaava jossa on kaksi vapaata muuttujaa, niin TC(Q)(x,y) määrittelee tämän osakaavan Transitiivisen sulkeuman. Sen totuusarvo käyttäytyy seuraavalla tavalla: TC(Q(x,y)) tulkitaan itseasiassa siten, että joko Q(x,y) pätee, tai pitää löytyä jokin ei-tyhjä jono alkioita z1, z2, ..., zk siten, että Q(x,z1) pätee, Q(z1,z2) pätee, jne, ja Q(zk, y) pätee.

FO[TC] on niiden ongelmien joukko, jotka voidaan ilmaista käyttäen ensimmäisen kertaluvun logiikkaa ja transitiivista sulkeumaa. Esimerkiksi "Graafissa on polku solmusta s solmuun t" on ilmaistavissa tällä; jos p(x,y) on (annettu) predikaatti, joka pätee kun on kaari solmusta x solmuun y, niin polku solmusta s solmuun t on olemassa, jos pätee TC(p)(s,t). Tämä kompleksisuusluokka on sama kuin luokka NL, joka on niiden ongelmien luokka, jotka voidaan ratkaista "arvaamalla" ratkaisu askel kerrallaan ilman että koko ratkaisua täytyy muistaa.

Least fixpoint, eli pienimmän kiintopisteen operaattori taas mahdollistaa yksinkertaisen rekursiivisen ilmaisun, jolla määritellään uusi predikaatti. Muistutan tässä kohtaa, että olemassaolevat predikaatit ovat kiinteitä ja tunnettuja; TC yllä mahdollisti "uuden" predikaatin luomisen vanhojen predikaattien avulla hyvin yksinkertaisesti. LFP-operaattori on jo selvästi monimutkaisempi. Luodaksemme "toisen kertaluvun" predikaatin P -- eli predikaatin jonka tulkinta ei ole kiinnitetty -- ilmaisemme sen muodossa LFP(Q(P,x)) Tässä siis LFP-operaattorin sisään tulee kaava Q, jossa käytetään predikaattia P, muuttujia x ja olemassaolevia predikaatteja. Tämä tulkitaan tarkoittavan "pienintä" sellaista predikaattia P, joka toteuttaa kaavan P(x) = Q(P(x),x) kaikilla x; Rajoituksena on, että P(x) ei saa esiintyä negatiivisena kaavassa Q (so. kun kaava Q kirjoitetaan konjunktiiviseen normaalimuotoon, P:n negaatio ei saa esiintyä kaavassa). 

Esimerkiksi relaation p(x,y) transitiivinen sulkeuma voidaan ilmaista LFP-operaattorilla kaavasta  LFP(p(x,y) || \exists z: P(x,z) && p(z,y)). Eli, P(x,y) on p:n transitiivinen sulkeuma, kun se on "pienin" relaatio joka toteuttaa em rekursiivisen määritelmän. Pienin tässä yhteydessä tarkoittaa, että se joukko pareja, joka yhtälön toteuttaa, on minimaalinen; mikään sen aito osajoukko ei voisi toteuttaa yhtälöä.  FO[LFP] = P, eli polynomisessa ajassa ratkeavat ongelmat ovat karakterisoitavissa LFP-operaattorilla rikastetussa ensimmäisen kertaluvun predikaattilogiikassa. Tämä teoreema on hankalahko todistaa, joten en tässä ala sitä nyt käymään läpi.

Jos siirrymme toisen kertaluvun logiikkaan "aidosti", eli sallimme uusien predikaattimuuttujien esittelyn, mutta rajoitumme eksistentiaaliseen kvantifiointiin, saamme mielenkiintoisen luokan, SO[E]. Tässä siis on kyse ensimmäisen kertaluvun logiikasta, jossa saa luoda predikaattimuuttujia, kunhan ne on sidottu olemassaolokvanttorilla. Käytän tässä merkintää \E, koska en jaksa kaivaa symboleja.

Tällöin voidaan sanoa vaikkapa että \E(P(x,y): P(x,y) <=> (p(x,y) || (\Ez: P(x,z) && p(z,y) && \Ez: p(x,z) && O(z,y)). Tämä siis vain postuloi, että on olemassa predikaatti joka on tosi tasan silloin kun... jne. Tämä osakaava karakterisoi jälleen transitiivisen sulkeuman.

Tällä operaattorilla voidaan tehdä jo paljon muutakin. Esimerkiksi, voidaan karakterisoida graafissa ns. klikki. Jos p(x,y) on (suuntaamaton) kaarirelaatio, niin \E P(x): \Ax \Ay: (P(x) && P(y)) => p(x,y) && \Ay (\Ax: P(x) => p(x,y)) => P(y). Tämä on tosi predikaatille P(x), jos ja vain jos P(x) on tosi maksimaalisessa sellaisessa joukossa jonka kaikkien solmujen välillä on kaari. Tämän lisäksi täytyy voida jotenkin sanoa että P(x) pätee vähintään jollekin tietylle määrälle alkioita, sivuutan sen tässä teknisenä yksityiskohtana, toivon että lukija luottaa minuun tässä.

On siis mahdollista spesifioida tällä SO[E]-loogikalla se, että graafissa on tietyn kokoinen klikki. Tämä taas on tunnettu NP-täydellinen ongelma, joten SO[E] karakterisoi luokan joka on vähintään NP.

Pienen pohdinnan jälkeen oivalletaan, että jokainen SO[E]-luokan kaava joka on tosi annetulle struktuurille, voidaan osoittaa todeksi ensin arvaamalla tarkalleen milloin nämä uudet predikaatit ovat tosia. Koska jokaisen predikaatin määrittelyssä on jokin vakiomäärä parametrejä (esim k), ja koska syötteenä saadussa struktuurissa on alkioita joihin muuttuja voi viitata vain korkeintaan n kappaletta, on predikaatin totuusarvojoukko kooltaan korkeintaan n^k. Voimme siis arvaamalla nämä uudet predikaatit luoda polynomisessa ajassa FO-kaavan, jonka päteminen alkuperäiselle struktuurille on helppo todeta. Tiedämme siis, että SO[E] = NP.


Kompleksisuushierarkiassa on tästä kompleksisempiakin luokkia, ja lisäksi P-luokan sisällä on paljon alaluokkia. Mutta idea tulee ehkä jo tästä selväksi.

Myhill-Neroden teoreema

Olen vuosikaudet opettanut tietojenkäsittelyteorian erilaisia kursseja, ja yksi asia joka useimmilla alan peruskursseilla käsitellään on niin kutsutut säännölliset kielet. Formaalien kielten teoriassa ei ole samalla tavalla kyse kielistä kuin vaikkapa lingvistiikassa, vaikka yhtymäkohtia tieyiltä osin tietenkin on. Pääosin näitä asioita käsitellään siten että "kieli" ymmärretään joukoksi merkkijonoja; vaihtoehtoisesti voidaan ajatella että "kieli" on merkkijonojen predikaatti; jotkut merkkijonot toteuttavat kyseisen ominaisuuden ja jotkut eivät.

Säännölliset kielet ovat kaikkein yksinkertaisin jollain tavalla relevantti formalismi. Kielen säännöllisyys voidaan määritellä monella tavalla ja päätyä samaan lopputulokseen. Yksi tapa määritellä säännölliset kielet on siten, että kun on annettu aakkosto E, niin määritellään säännölliset lausekkeet aakkoston yli. Oletamme että meillä on tyhjän joukon symboli ø ja tyhjän merkkijonon symboli e, jotka eivät kuulu aakkostoon. Säännöllinen lauseke muodostetaan seuraavasti:

1. ø ja e ovat säännöllisiä lausekkeita
2. jokainen aakkoston E symboli a on yksinään säännöllinen lauseke
3. Jos R ja S ovat säännöllisiä lausekkeita, niin RS on säännöllinen lauseke
4. Samoin R+S on säännöllinen lauseke,
5. R* on säännöllinen lauseke kun R on säännöllinen lauseke. 

Kukin säännöllinen lauseke R määrittelee joukon L(R) merkkijonoja. L(ø) ei sisällä mitään merkkijonoa, L(e) = {e}, eli sisältää vain tyhjän merkkijonon, ja L(a) = {a} jokaiselle yksittäiselle aakkossymbolille. L(R+S) määrittelee joukon joka on L(R):n ja L(S):n yhdiste. L(RS) määrittelee joukon L(R)*L(S), joka muodostuu kaikista L(R):n merkkijonoista joiden perään on laitettu mielivaltainen L(S):n merkkijono. L(R*) määrittelee joukon jossa on kaikki sellaiset merkkijonot jotka saadaan muodostettua laittamalla R:n mielivaltaisia merkkijonoja perätysten mielivaltainen määrä. (Myös nolla kertaa, eli L(R*) sisältää aina tyhjän merkkijonon)

Yhtäpitävä määritelmä saadaan kun sovitaan että kieli on säännöllinen jos on olemassa jokin äärellinen automaatti joka hyväksyy kielen. Äärellinen automaatti on yksinkertainen kone, jossa on äärellinen määrä tiloja. Ennen merkkijonon lukemista automaatti on alkutilassaan. Aina kun automaatti lukee syötteenään aakkoston symbolin, se siirtyy johonkin tilaan; siirtymä riippuu tilasta jossa ollaan ja symbolista joka luetaan. Osa tiloista on ns hyväksymistiloja, ja jos merkkijono päättyy kun automaatti on hyväksymistilassa, automaatti hyväksyy kyseisen merkkijonon.

Formaalien kielten teoriassa on niin sanottu erottavan jatkeen käsite. Jos meillä on kaksi merkkijonoa x ja y, niin kolmas merkkijono z on erottava jatke kielen L suhteen, jos tasan toinen merkkijonoista xz ja yz kuuluu kieleen L. Jos kahdelle merkkijonolle ei ole erottavaa jatketta, niin riippumatta merkkijonon z valinnasta xz ja yz molemmat joko kuuluvat tai eivät kuulu kieleen L.

Esimerkiksi, jos aakkosto koostuu merkeistä a ja b, ja kieli L koostuu kaikista niistä merkkijonoista joissa on yhtä monta a- ja b-merkkiä, niin jos x:ssä ja y:ssä on yhtä monta a:ta ja b:tä, niin x:llä ja y:llä ei ole erottavaa jatketta. Itse asiassa tämä pätee jos a- ja b-merkkien määrän erotus on x:ssä ja y:ssä sama.

Sanomme, että merkkijonot x ja y ovat ekvivalentit kielen L suhteen, jos niille ei ole erottavaa jatketta. Tämä ekvivalenssirelaatio jakaa kaikki merkkijonot ekvivalenssiluokkiin. Myhill-Neroden teoreema sanoo, että kieli L on säännöllinen jos ja vain jos kielen L suhteen on olemassa vain äärellinen määrä ekvivalenssiluokkia.

Koska kieli on säännöllinen jos ja vain jos sille löytyy äärellinen automaatti, niin voimme todistaa tämän väitteen toiseen suuntaan melko helposti: Jos kaksi merkkijonoa vie automaatin samaan tilaan, niin merkkijonojen on oltava automaatin kielen suhteen ekvivalentteja; ekvivalenssiluokkia ei voi olla enempää kuin kielen hyväksyvässä automaatissa on tiloja.

Kääntäen, jos ekvivalenssiluokkia on äärellinen määrä, voimme muodostaa automaatin joka hyväksyy kielen. Automaatissa on yksi tila jokaista ekvivalenssiluokkaa kohden. Alkutila vastaa ekvivalenssiluokkaa, johon tyhjä merkkijono kuuluu. Tilasiirtymä tapahtuu ekvivalenssiluokkien välillä siten, että jos x on mielivaltainen tilaan q liittyvän ekvivalenssiluokan alkio, niin tilasiirtymä a vie tilasta q tilaan q' siten että q':a vastaava ekvivalenssiluokka sisältää merkkijonon xa.  Tämä toimii, sillä jos x ja y ovat ekvivalentteja, niillä ei ole erottavaa jatketta. Koska niillä ei ole erottavaa jatketta, ei myöskään merkkijonoilla xa ja ya voi olla erottavaa jatketta.

Hyväksymistiloiksi valitaan tilat joita vastaavan ekvivalenssiluokan alkiot kuuluvat kieleen. Kaikki ekvivalenssiluokan alkiot tietenkin kuuluvat tai mikään ei kuulu, sillä tyhjä merkkijono ei ole kyseisten merkkijonojen erottava jatke.

Tällä tavalla rakennettu automaatti on itseasiassa pienin mahdollinen äärellinen automaatti joka kyseisen kielen hyväksyy. Tilojen määrää voidaan pitää alkeellisena kielen kompleksisuuden mittarina, joskin tämä ei vastaa perinteisemmän kompleksisuusteorian kompleksisuusmittoja. Jokainen säännöllinen kieli ratkeaa ilman lisämuistia ajassa, joka kuluu merkkijonon lukemiseen, joten jokainen säännöllinen kieli on laskennallisesti äärimmäisen yksinkertainen. Nimitämme tätä suuretta kielen indeksiksi.

Jokaiselle (myös ei-säännölliselle) kielelle A voidaan esittää pari säännöllisiä kieliä (L,U) siten, että L ja U ovat säännöllisiä, L on A:n osajoukko, joka puolestaan on U:n osajoukko. No, tämä on triviaalisti totta, koska tyhjä joukko ja kaikkien merkkijonojen joukko ovat säännöllisiä. Mielenkiintoisempi kysymys -- johon vastaaminen kertoo paljon kielen A monimutkaisuudesta -- on se, miten tarkkoja approksimaatioita voidaan löytää, kun kielten L ja U indeksien summa (esimerkiksi) on n. Approksimaation tarkkuutta voidaan esimerkiksi mitata siten, että kun otetaan mielivaltainen merkkijono x, mikä on todennäköisyys että x kuuluu L:ään ja A:han tai ei kuulu A:han eikä U:hun, eli kääntäen, mikä on todennäköisyys että x:stä päätellään "väärin" se, kuuluuko se A:han. Mutta tämä teoria menee jo sitten vähän pidemmälle.

Legacy (kerrankin muuta kuin nostelua)

I am hoping that I can be known as a great writer and actor some day, rather than a sex symbol. 
  -Steven Seagal

Jätin hakemuksen dosentuurin myöntämisestä. Minun piti tehdä tämä viisi (5) vuotta sitten, mutta olen lykännyt asiaa koska en ole kokenut sen olevan ajankohtainen. Teoriassa ja käytännössä sovellettujen kriteerien mukaan olisin ollut pätevä jo tuolloin mutta koin etten tarvitse sellaista titteliä mihinkään, ja se käytännössä velvoittaisi minut tiettyihin asioihin. Esimerkiksi Suomen Akatemian tutkimushankkeissa hankkeen vetäjän tulee olla dosentti tai professori suomalaisessa yliopistossa. Koska minä en ole, olen voinut perustellusti jättää esimerkiksi hankehakemukset tekemättä. Olen kuitenkin viime vuodet haamukirjoittanut hankehakemuksia muille, ja esimiehen kanssa käydyn keskustelun perusteella tulimme johtopäätökseen ettei tässä ole mitään järkeä.

Tutkimusurani on ollut melko tylsämielinen. Aloitin aikanaan -- 16 vuotta sitten -- tutkimaan optimointialgoritmeja ja siirryin siitä graafialgoritmeihin ja 2001 alussa perustutkinnon tehtyäni siirryin Verifiointialgoritmien tutkimusryhmään. Verifiointi viittaa siis menetelmiin joilla jonkin järjestelmän kuvauksesta päätellään virheettömyys. Ala on varsin laaja ja "poikkitieteellinen" ja  käyttää laajasti logiikkaa, graafiteoriaa, automaattiteoriaa, algebraa, jne.

Alalla on monta eri tutkimussuuntaa, mutta yhdessä nurkassa on kaksi suuntaa jotka puhuvat samoista asioista eri termein; järjestelmän toiminta voidaan yhtäältä nähdä siten että sen tila on havaittavissa ja ajan yli järjestelmän toiminnan kannalta olennaiset asiat päätellään siitä millaisissa tiloissa järjestelmä on ollut. Toisaalta järjestelmä voidaan ajatella koostuvan tapahtumista (event, action) ilman että tilaa voidaan oikeastaan havainnoida mitenkään. Näiden välillä vallitsee tietyssä mielessä duaalisuus, koska "tila" voidaan karakterisoida jälkimmäisessä niiden tapahtumien joukkona jotka ovat mahdollisia kunakin hetkenä ja "tapahtuma" ensimmäisessä yksinkertaisesti tilan muutoksena.

Tilapohjaisessa hahmotuksessa on helpompi käyttää erilaisia logiikoita, jokaisessa tilassa pätee jokin kaava ja esimerkiksi aikalogiikka kertoo sellaisista asioista kuin "ennen pitkää pätee että X" tai "koskaan ei päde Y" tai "X pätee kunnes Y tulee voimaan" jne. Tapahtumapohjaisissa menetelmissä on helpompaa konstruoida erilaisia algebrallisia relaatioita järjestelmien välille, kuten että "tämä järjestelmä ei tee mitään sellaista mitä tuokaan ei tee" (ns. refinement) ja näiden päälle voidaan rakentaa esimerkiksi induktiivista päättelyä. Kummassakin on omat erilaiset abstrahoinnin menetelmänsä. Olen kirjoittanut aikanaan paljon abstraktiosta koska se on äärimmäisen mielenkiintoinen käsite tässä yhteydessä.

Tilapohjaisissa malleissa on ns. änkytys (engl. stuttering) mikä tarkoittaa tilannetta jossa järjestelmän tila kyllä muuttuu mutta tilan ominaisuudet ovat loogisessa ja malli-teoreettisessa mielessä samat. Tapahtumapohjaisessa maailmassa tätä vastaa ns silent action, tai näkymätön tapahtuma, joka voi muuttaa järjestelmän tilaa, mutta jota ei ulospäin voida havaita.  Abstrahoinnin voidaan ajatella tilapohjaisessa maailmassa tuottavan änkytystä ja tapahtumapohjaisessa maailmassa se taas tuottaa joko näkymättömiä tapahtumia tai epädeterminismiä. Epädeterminismi viittaa siis siihen että tapahtuu jotain mutta lopputuloksena voi olla erilaisia asioita.

Tein väitöskirjani oikeastaan siitä, miten aikalogiikka-tyyppistä spesifiointia voidaan hyödyntää malleissa joissa on myös tapahtumapohjaista informaatiota. Lineaarisen aikalogiikan (LTL) mallintarkastuksessa käytetään hyväksi sitä tosiasiaa että jokainen LTL-kaava voidaan muuttaa ns Büchi- automaatiksi. Automaatti toimii kivasti tilapohjaisten mallien (kuten Kripke-rakenteiden) kanssa, mutta tapahtumapohjaisen mallin erityispiirteet taas hieman tökkivät. Änkytys on yksi ongelmakohta. Lineaarinen aikalogiikka sisältää operaation "seuraavaksi P" (merkitään usein X.P), mikä tarkoittaa että jos järjestelmä vaihtaa tilaa, niin vaihdon jälkeen pätee P. Jos tämä operaattori jätetään pois, niin LTL-kaavat jotka voidaan ilmaista, eivät erottele toimintoja jotka erovat toisistaan (äärellisen) änkytyksen suhteen. Väitöskirjassani "Alternatives to Büchi automata" käsittelin erästä toista, paremmin tapahtumapohjaiseen maailmaan istuvaa, automaattia, ja lisäksi erilaisia algoritmeja, sekä vertailin Büchi-automaatin ja tämän automaatin välistä suorituskykyä käytännössä.

Kun siirryin post-doc tutkimukseeni, halusin tehdä "jotain muuta". Väitöstilaisuudessa vastaväittäjäni esitti erään kysymyksen väitöstutkimukseni ja erään toisen menetelmän (ns Partial Order Reduction) yhdistämisestä, joka jäi vaivaamaan minua. Tutkittuani determinismiä hetken aikaa, siirryin tämän toisen menetelmän pariin vuonna 2008. Nyt, kahdeksan vuotta myöhemmin olen vihdoin kirjoittamassa artikkelia joka vastaa teoriatasolla vastaväittäjäni esittämään kysymykseen. Olin 2014 alamme johtavassa konferenssissa esittelemässä erästä paperiani. Samaan aikaan esimieheni sai palkinnon 90-luvulla tekemästään pioneerityöstä juurikin tämän partial order reduction-aiheen parissa. Kun eräs kaverini esitteli minut joillekin että "He is the new Mr Partial Order Reduction" tajusin että olen mennyt liian pitkälle tähän aiheeseen, minun on pakko vaihtaa alaa.

Toivon mukaan tämä artikkeli on viimeinen jonka aiheesta kirjoitan. Tiedän kyllä ettei se tule olemaan, koska jo nyt kun olen kirjoittanut pari lukua, tajuan että kirjoitettavaa ja tutkittavaa on vaikka kuinka paljon. Tunnen itseni linnuksi (oliko se Harakka vai Varis?) vanhassa Aapisessa, jonka nokka ja pyrstö vuoron perään tarttuvat tervaan.

Täytän 40 kesällä, kuten edellisessä kirjoituksessani sanoin. Minulla on tilastojen valossa vielä 10 vuotta aikaikkunaa jossa voin tehdä merkittäviä uusia avauksia ja 25-30 vuotta aikaa lypsää tutkimustuloksia. En halua hautakiveeni tekstiä "Mr Partial Order Reduction".

Induktio.

Mallintarkastus (model checking) tarkoittaa tekniikkaa, jossa jonkin järjestelmän virheettömyys osoitetaan ns. malliteoreettisella argumentilla. Jos meillä on järjestelmä M ja ominaisuus P, niin mallintarkastus pyrkii toteamaan, päteekö M |= P, eli että järjestelmän kuvaus M on ominaisuuden P malli. 

Vaihtoehtoja järjestelmän mallille on monia, samoin ominaisuus voi olla monella eri tavalla esitetty. Niin kutsutussa eksplisiittisessä mallintarkastuksessa järjestelmä esitetään tilakoneena tms, jonka kaikki tilat tutkitaan ja tarkastetaan että ominaisuus P pätee, tai sitten löydetään virhe, eli jokin järjestelmän suoritus jossa P rikkoutuu.

Symbolisesta mallintarkastuksesta puhutaan usein silloin, kun järjestelmä on esitetty symbolisesti, eli esimerkiksi jonkinlaisten logiikan kaavojen tms avulla siten, että yksittäiselle tilalle ei välttämättä ole mitään esitystä. Symbolinen mallintarkastus oli suosittua 80- ja 90-luvulla ns. binääristen päätöskaavioiden (BDD) ansiosta.  BDD kykenee esittämään joukon järjestelmän tiloja kompaktisti, jos järjestelmä on riittävän säännönmukainen. Järjestelmän tilasiirtymät esitetään symbolisesti loogisena funktiona T ja kun meillä on jokin joukko tiloja S (esitetty esimerkiksi BDD:n avulla), T(S) kuvaa ne tilat joihin voidaan päätyä jos tehdään siirtymiä joukosta S.  Kun BDD:ille on annettu jokin kanoninen esitystapa, niin kahden BDD:n ekvivalenssi on helppo laskea, samoin implikaatio -- eli käytännössä osajoukkorelaatio. Jos T(S) on S:n osajoukko, niin sanomme että S on kiintopiste eli ns. fixed point. Tämä tarkoittaa sitä, että jos tiedämme järjestelmän olevan jossakin S:n tilassa, ja T(S) on S:n osajoukko, niin tiedämme että S sisältää kaikki sellaiset tilat johon järjestelmä voi ylipäätään päätyä.

90-luvun lopulla alkoi tapahtua tietojenkäsittelyssä, kun yhtä aikaa tietokoneet olivat tulleet nopeammiksi ja tehokkaammiksi, ja toisaalta algoritmit kehittyneet. Tunnettu NP-täydellinen ongelma on niin sanottu SAT-ongelma. SAT tarkoittaa ongelmaa, jossa jos meille on annettu propositiologiikan kaava X, niin kysytään, voidaanko propositioille löytää sellaiset arvot että kaava on tosi. Huolimatta ongelman NP-täydellisyydestä, valtavan moni yksittäinen SAT-ongelma itseasiassa ratkeaa hyvinkin tehokkaasti, eli patologiset tapaukset ovat varsin harvinaisia. Armin Biere ja muutama muu keksivät mallintaa järjestelmän propositiologiikan avulla ja keksivät ns. rajoitetun mallintarkastuksen (Bounded Model Checking,BMC). Siinä järjestelmän toiminta esitetään tiettyyn askelmäärärajaan k asti propositiologiikan kaavana X(k), ja tarkastettava ominaisuus P esitetään myös kaavana, ja kysytään, onko kaava (X(k) & !P) SAT instanssi. Jos se on, niin olemme löytäneet virheen, jos ei, niin olemme osoittaneet että virhettä ei ole ensimmäisen k-askeleen jälkeen.

BMC:n ongelma on, että kaavan pituus kasvaa koko ajan eikä siinä sellaisenaan ole mitään fixed point- karakterisointia. Jokainen askel tuo kaavaan lisää muuttujia, ja sitäpaitsi, järjestelmän toiminta voi hyvinkin olla ääretön, jolloin mitään kiintopistettä ei edes teoriassa voi löytää.

Ken McMillan ja muutamat muut keksivät jossain kohtaa soveltaa ns. Craigin interpolantteja BMC:hen. Interpolantti toimii suunnilleen niin, että jos meillä on kaava A & B, joka ei ole SAT, eli se on ristiriitainen, niin löytyy kaava I (vasen interpolantti), jolla on ominaisuudet 1) A => I, 2) I & B ei ole SAT ja 3) I:ssä esiintyy vain sellaisia propositioita jotka ovat yhteisiä A:lle ja B:lle.  Oikea interpolantti olisi symmetrisesti sellainen jossa B => I jne.

Kun järjestelmän toimintaa mallinnetaan jollakin kaavalla, erityisesti, jos A on kaava joka sisältää sekä propositioita joiden on tarkoitus kuvata tiloja että propositioita jotka kuvaavat transitioiden ominaisuuksia ja B kuvaa pelkästään tilojen ominaisuuksia, niin interpolantti esittää jonkin joukon tiloja. Koska A => I pätee, niin ne tilat joista A puhuu, muodostavat niiden tilojen osajoukon joista I puhuu. I on tietyssä mielessä abstraktio joka vangitsee A:n tiloista jotain siitä miksi A & B ei ole SAT. Koska A kuvaa järjestelmän suoritusta johonkin rajaan asti, I on eräänlainen selitys sille, miksi A ei sisällä virhettä. 

Vedän tässä hieman oikoiseksi mutkia, mutta jos suoritamme BMC:tä johonkin rajaan k asti, emmekä löydä virhettä, niin X(k) & !P ei ole SAT. Jos tässä kohtaa etsimme interpolantin I, niin I & !P ei ole SAT ja I esittää joukon tiloja. Kun käytämme propositio- tai predikaattilogiikkaa tilasiirtymien esittämiseen, joudumme aina esittämään joka askelella uusia muuttujia. Jos meillä on joukko muuttujia V, niin tilasiirtymät esitetään kaavalla T(V,V') niin, että joukon V' muuttujat kuvaavat muuttujien arvoja tämän siirtymän jälkeen. Koska interpolantti I esittää myöskin joukon tiloja, yleensä ajattelemme että se on muotoa I(V), mutta V':n muuttujia siinä ei tietenkään esiinny.  Kaava (I(V) & T(V,V')) kuvaa sitä joukkoa tiloja joihin päästään jos lähtötiloina ovat tarkalleen ne tilat joissa pätee I(V). Nyt, jos (I(V) & T(V,V')) implikoi kaavan I(V'), niin olemme itseasiassa löytäneet jällleen kiintopisteen.  Sanotaan myös, että I on induktiivinen relaation T(V,V') suhteen.

Ilman BDD:itäkin mallintarkastus voidaan siis tehdä sellaiseksi että se myös voi todistaa järjestelmän oikeaksi kokonaan, ei vain johonkin rajaan saakka, jos löydämme induktiivisen interpolantin. Voimme tällöin jakaa mallintarkastuksen kolmeen vaiheeseen: 1) Meidän pitää löytää kaava joka esittää jonkin joukon tiloja joista ainakin osaan alkutilasta voidaan päästä, 2) Virheen ja kaavan konjunktion pitää olla ristiriitainen 3) Kaavan pitää olla induktiivinen tilasiirtymärelaation suhteen. BMC-pohjainen mallintarkastus lähtee alkutilasta ja kasvattaa kaavaa johonkin rajaan asti, tämän jälkeen se muodostaa interpolantin. Tämä prosessi takaa että kaksi ensimmäistä ominaisuutta toteutuvat, mutta induktiivisuutta se ei takaa.

Niin sanottu CEGAR (counterexample-guided abstraction refinement) taas perustuu ajatukseen, että tutkimme koko ajan kaavaa joka on sekä induktiivinen että sisältää alkutilan. Alussa tällainen kaava on tautologinen, ja esittää siten kaikkien mahdollisten (ja mahdottomien) tilojen joukon. Se kuitenkin esittää myös virheen. Kaava on siis "liian abstrakti" eikä ota huomioon järjestelmän toiminnan rajoitteita. Algoritmi toimii niin, että tähän reagoidaan lisäämällä jokin rajoite joka varmasti on voimassa transitiorelaatiossa, ja joka ei riko induktiivisuutta, ja tarkastetaan uudelleen. Tässä rikon hieman rajoja, koska näen prosessit samoina, oli kyse sitten eksplisiittisestä tai symbolisesta mallintarkastuksesta. Minulla kesti melkein 14 vuotta ymmärtää että sillä ei ole oikeastaan tässä kohtaa mitään merkitystä; Eksplisiittinen mallintarkastus tavallaan perustuu siihen että järjestelmänkuvauksesta tutkittavana oleva osa on aina "induktiivinen", se vain on niin suuri ettei sitä voida kokonaan tarkastella. Abstraktiolla tuotetaan pienempi malli joka on takuulla induktiivinen mutta saattaa tuoda virhetilan vahingossa malliin.

Kaikkien kaavojen joukossa, joita voimme muodostaa -- tämä on hyvinmääritelty, jos kohta ääretön joukko -- annetun järjestelmän atomisista ominaisuuksista, on mielenkiintoinen rakenne malliteoreettisessa ja algebrallisessa mielessä. Tässä kohtaa olen hyvin mielissäni, että sain opettaa pari vuotta matemaattista logiikkaa,  kumpa olisin saanut tehdä niin jo vuosia aiemmin, olisin ymmärtänyt tämän jo ennen kuin matalalla roikkuvat hedelmät aihepiiristä oli poimittu. Nimittäin, kaavoilla on ns. hilarakenne. Otetaan kaavojen sijaan niiden ekvivalenssiluokat, eli samastetaan kaavat jotka ovat loogisesti yhtäpitäviä. Hilassa on maksimaalinen ja minimaalinen alkio: Identtisesti todet kaavat ja identtisesti epätodet kaavat, eli [T] ja [F].  Osittaisjärjestyrelaationa on se, että jos [P => Q] = [T], niin P < Q.  Kahdella kaavalla A ja B on supremum, [A || B] (A or B) ja infimum [A && B].

Tässä hilassa on monta mielenkiintoista alihilaa. Esimerkiksi jos T(V,V') -- transitiorelaatio -- on fiksattu, niin induktiivisten kaavojen joukko muodostaa alihilan: Sekä True että False ovat induktiivisia, mikä ei ole vaikea todistaa. Myös kahden induktiivisen kaavan disjunktio ja konjunktio ovat induktiivisia. Negaatio ei ole induktiivinen yleisessä tapauksessa, mutta negaation suhteen suljettujen induktiivisten kaavojen joukko on itsessään tämän alihilan alihila, ja se ei ole vaike nähdä myöskään; kyseinen alihila sisältää aina vähintäänkin kaavat True ja False (jotka ovat siis toistensa negaatioita). Joka tapauksessa, merkitään T(V,V'):n suhteen induktiivisten kaavojen alihilaa IL(T).

Ja tästä -- anteeksi pitkä johdanto -- pääsemmekin mielenkiintoiseen asiaan, eli siihen, miten T(V,V') vaikuttaa tähän hilarakenteeseen jos voimme "häiritä" sitä. Nimittäin, oma erikoisalani osittaisjärjestyreduktio (POR, partial order reduction) toimii niin, että tietyissä oloissa voimme eliminoida joitakin transitioita järjestelmästä. Käytännössä tämä tarkoittaa, että luomme kaavan R(V,V') jolla on se ominaisuus että R(V,V') => T(V,V') ja että M(T) |= P jos ja vain jos M(R) |= P. Tässä siis M(T) viittaa malliin joka on rakennettu käyttäen relaatiota T ja M(R) käyttäen relaatiota R.

Kansanviisaus alalla on sanonut, että POR on hyödyllistä eksplisiittisessä mallintarkastuksessa, muttei juurikaan symbolisessa. Kaiken muun huvittavan lisäksi, niiltä osin kun sitä on symbolisessa mallintarkastuksessa ylipäätään käytetty, sen on ajateltu soveltuvan vain asyklisten järjestelmien mallintarkastukseen, koska syklisyys aiheuttaa tietyissä tilanteissa ongelmia oikeellisuuden kannalta. Tämä ongelma kuitenkin ratkaistiin vajaa vuosi sitten käytännössä kokonaan uudella tavalla, jota en nyt tässä ala referoimaan, ja tämä tapa poisti käytännössä ongelman kokonaan.

On helppo todistaa, että jos R(V,V') on rajoittavampi kaava kuin T(V,V'), IL(T) on IL(R):n alihila. Se, mitä aiomme nyt seuraavaksi tehdä, on tutkia jos voisimme löytää IL(R)-alihilalle (tai sen jollekin alihilalle) joukon eräänlaisia kanta-alkoita, joita yhdistämällä konjunktiivisesti ja disjunktiivisesti voimme löytää sellaisen induktiivisen kaavan, joka sisältää alkutilan mutta ei sisällä virhetilaa, ja, jonka avulla vielä voisimme nopeasti löytää todisteet sille että tällaista kaavaa ei ole, mikäli tämä todella on tilanne.

.. Valista kasvosi meidän puoleemme, ja ole meille armollinen...

Jätin eilen kaksi akatemiahakemusta. Toinen -- se jonka todennäköisyys tulla hyväksytyksi on astronomisen pieni -- oli hakemus akatemiatutkijan viisivuotisesta rahoituksesta. Raa'alla numeropelillä läpimenon todennäköisyys on 9 prosenttia, ja koska hakuikkuna on kuusi vuotta, voidaan tästä laskea että liki puolet sen lopulta saa, olettaen että hakijat hakevat joka vuosi. Jos porukan koko olisi kiinteä tuon kuusi vuotta, niin hakijoista 54 prosenttia saisi rahan, koska rahaa ei myönnetä samalle henkilölle kahdesti.

Akatemiatutkijan rahoitus on ns. lohi, eli niin hyvä kala, että sitä kannattaa pyytää vaikkei saisikaan. Tämä siksi, että tutkimussuunnitelman tekeminen on virkistävää ajatuksille ja CV ja julkaisuluettelo on syytä pitää kunnossa muutenkin. Lisäksi se pistää miettimään omat yhteistyökuviot aina uusiksi ja priorisoimaan. Tässä on kuitenkin ongelmansa, esimerkiksi se, että tämä priorisointi tapahtuu sellaisilla kriteereillä, jotka eivät mitenkään itsestäänselvästi ole itse tutkimuksen kannalta parhaimmat. Ns. Matteus-vaikutus on erityisesti tutkimusrahoituksessa hyvin voimakas; osa rahoittajista jopa pitää merkittävänä kriteerinä sitä, että henkilö on uran varhaisessa vaiheessa onnistunut hankkimaan muuta rahoitusta. Tämä on esimerkki yleisemmin mekanismeista jotka johtavat ns. winner-take-all- lopputuloksiin.

En valita tai protestoi kriteerien epäreiluutta. Pidän kuitenkin takaisinkytkentää sikäli ongelmallisena, että sen merkityksen kasvaessa itse laadun merkitys pienenee ja sattuman osuus kasvaa: Jos sattumalta päätyy oikeaan paikkaan oikeaan aikaan, saa homman ns. rullaamaan, muutoin ei.

Se toinen, jolla on suurempi todennäköisyys tulla hyväksytyksi, on hankehakemus, jonka tein ns. haamukirjoittajan ominaisuudessa. Tämä kuuluu pelin henkeen, eli ryhmän seniorimmat hakijat hoitavat muut hallinnolliset tehtävät ja minä luonnostelen tutkimussuunnitelmia. Tässäkin rahoituksessa on riskinsä. Jos ja kun se tulee, niin pääsemme viemään läpi tutkimusprojektia jota olemme hautoneet kohta kymmenen vuotta. Henkilöresurssien kanssa tulee kuitenkin ongelma, koska toisin kuin vuosituhannen vaihteessa, nyt ei ole isoa joukkoa lahjakkaita nuoria tutkijanalkuja hinkuamassa tekemään väitöskirjaa, eikä hankerahaa oikein nykyään edes sellaiseen voisi edes pääosin laittaakaan. Postdocit taas ovat joko katkeroituneita ja urautuneita (kuten minä viisi vuotta sitten) tai jos ovat kyvykkäitä, paljon halukkaampia menemään jonnekin ihan muualle töihin.

En kuitenkaan,  yllä sanotusta huolimatta, ole lainkaan epätoivoinen, sen paremmin rahoituksen saamisen kuin sen käyttämisenkään suhteen. Todennäköisesti kupongeilla ei tule mitään, ja jos tuleekin, niin kyllä sille rahalle aina ottajansa löytyy. Ja kyllä se tutkimuskin sieltä sitten tulee. Ja jos ei tule, niin en itke tai yöuniani aio menettää senkään vuoksi. Karavaani kulkee jne.

Ajolähtö, Reunahuomautus.

Hesarissa ollut kolumni käsitteli samaa problematiikkaa, joka liittyy aiempaan kirjoitukseeni.

Yliopisto-organisaation ja sen kultivoiman uramallin ongelmana näyttäisi todellakin olevan se, että mitä pidemmälle etenet, sitä vähemmän työkuvaan kuuluu oikeasti niitä asioita, joissa ansioituminen vie eteenpäin. Tämä on tavallaan "onneksi" muuttunut niin, että uramallissa etenemisen kriteereihin on jo käytännössä lisätty vaatimus rahoituksen hankkimisesta niillä uran vaiheilla,  joissa työhön nimellisesti kuuluu mukamas vain tutkiminen.

Tämä problematiikka ei kuitenkaan poista sitä syvintä ongelmaa, eli että tutkimus ei ole tutkijan päätyö. Mitään sellaista uramallia ei nimittäin ole olemassa, jossa tutkija vain tutkii (ja mahdollisesti opettaa jonkin verran) ja tulee koko ajan paremmaksi tutkijana. Tutkija joka tutkii, on pian entinen tutkija; ainoa poikkeus on se, jos tutkija onnistuu saamaan tutkimuksiaan läpi sellaisilla foorumeilla joilla on merkittävää julkisuusarvoa. Siinäkin tapauksessa tutkija yleensä "palkitaan" siirtämällä hänet tehtäviin jossa ei enää tutkita.

Isäni on tehnyt aikanaan pitkän ja arvostetun uran auto- ja moottoripyörämekaanikkona. Leipänsä hän ansaitsi korjaamalla autoja, ennen eläkkeelle päätymistään. Varsinaisen erityisasiantuntemuksensa hän oli kuitenkin hankkinut kilpamoottoripyörien, erityisesti vanhempien TT/RR-pyörien moottoreista; tämä on ollut hänen harrastuksensa nuoresta miehestä asti, ja hän on harrastuspiireissään hyvin kysytty mekaanikko tiettyjen ongelmien ratkaisussa.  Kuvittelen välillä mielessäni, miten irvokasta olisi, jos työnantaja palkkaisi mekaanikon jolla on erityistä asiantuntemusta tietynlaisista moottoreista. Tämän työnkuvaan kuuluisi ensin nimellisesti esimerkiksi moottorien korjaaminen ja nuorempien mekaanikkojen opastaminen työssään, mutta kun huomattaisiin, että mekaanikko on erittäin kyvykäs työssään, työnantaja siirtäisi tämän työhön jossa markkinoidaan moottorien korjauspalveluita. Mitä parempi mekaanikko olisi kyseessä, sitä suuremman korjaamon markkinointia hänen oletettaisiin hoitavan. Jos hän onnistuisi kehittämään jonkun mullistavan tekniikan tietynlaisen kilpamoottorin virittämiseksi, hänet siirrettäisiin hallinnollisiin tehtäviin neuvottelemaan moottorivalmistajien ja kilpatallien kanssa sponsorisopimuksia.

Näin kuitenkin toimii yliopistomaailma. Tämä on vähän... kummallista, jos nyt kiltisti sanotaan. Samaan aikaan yliopistoissa nimittäin häärää alati kasvava joukko exel-apinoita laskeskelemassa miten tutkijoiden ja opettajien työpanoksesta saadaan enemmän "tulosta". Esimerkiksi eräässä nimeltämainitsemattomassa yliopistossa Suomen isoimmassa sisämaakaupungissa nämä exel-taitajat ovat huomanneet että (tyhjänä seisova) parkkihalli on "kuollutta pääomaa", ja se pitää "laittaa tuottamaan". Koska se ei tuota niin kauan kun parkkipaikkoja on ilmaiseksikin saatavilla, on kaikki parkkipaikat muutettu maksullisiksi. Tässä ei sinänsä tietenkään olisi mitään kummallista, jos a) parkkipaikoista olisi pulaa ja b) jos parkkipaikkojen maa-alalle olisi jokin merkittävä vaihtoehtoiskustannus. Myönnän, että olen hämmästynyt siitä, miten laajasti työntekijät tässä nimeltämainitsemattomassa oppilaitoksessa ovat parkkilupia ostaneet. Olen jopa sitä mieltä, että siinä on jotain hivenen moraalitonta, vähän samaan tapaan kuin jonottamisessakin.

Katselin Eurojackpot mainosta, jossa päävoittona on 60 miljoonaa euroa. Leikin ajatusleikkiä, "mitä jos". Pidän työstäni, joten tavallaan en lopettaisi työntekoa jos saisin 60 miljoonaa euroa. Samaan tapaan kuin isäni, joka eläkkellä ollessaan huvikseen korjailee moottoripyöriä, jatkaisin varmaankin tutkimustani. Toki irtisanoutuisin työstäni, ja ehkä perustaisin oman tutkimuslaboratorion, johon palkkaisin muutaman hyvän tyypin työskentelemään. Jos budjetti olisi noin miljoona vuodessa, ja saisin pääomalle noin 4 prosentin tuoton, niin 60 miljoonasta pitäisi irrottaa 25 miljoonaa pääomaksi. Pystyisin todennäköisesti tekemään kertaluokkaa tuottoisampaa tutkimusta kuin jos saisin samat henkilöt palkattua projektiin yliopistolla.

Logiikka ja laskenta.

Olettakaamme että olemme tutkimassa jonkinlaisen systeemin S käyttäytymistä. Systeemissä on erilaisia muuttujia, joita voimme ehkä mitata, emme ehkä täydellisesti mutta voimme kuitenkin saada jotain tietoa. Oletetaan että nämä muuttujat ilmaistaan symbolilla x. Tämä on siis periaatteessa vektori kaikesta siitä, mikä systeemissä on olennaista. Oletan tässä että meillä on lisäksi käsite aika, joka on yksi muuttuja, mutta yksinkertaisuuden vuoksi oletan että se ei ole mukana mainitussa x:ssä.

Systeemin tila on jollakin ajanhetkellä muuttujan x arvo. Jos tunnemme systeemin tilan kahtena ajanhetkenä, niin oletamme että systeemi on siirtynyt ensimmäisestä tilasta toiseen; se, miten systeemi siirtyy tilasta toiseen, määrittää systeemin dynamiikan. Melko yleisiä systeemien dynamiikan kuvaamiseen käytettyjä formalismeja ovat esimerkiksi differentiaaliyhtälöt. Jos x koostuu komponenteista x1, x2, ..., xn, niin meillä on tyypillisesti useampia differentiaaliyhtälöitä jotka kuvaavat sitä miten muuttujien kehitys ajan suhteen riippuu toisistaan. Esimerkiksi voisi olla vaikkapa kahden muuttujan systeemi, jossa x1' = x2 ja x2' = -x1. Tämä on hyvin yksinkertainen systeemi, jossa siis x1 kasvaa sitä nopeammin mitä suurempi x2 on ja x2 taas pienenee sitä nopeammin mitä suurempi x1 on; tällainen systeemi on oskilloiva, mutta se ei nyt ole olennaista.

Differentiaaliyhtälöillä kuvataan järjestelmiä, jotka ovat jatkuvia. Jatkuvuus viittaa siis siihen, että aika etenee tasaista tahtia ja muuttujat ovat tyypillisesti reaali- tai kompleksilukuja. Differentiaaliyhtälöillä kuvataan lisäksi järjestelmiä jotka ovat deterministisiä, eli niiden toiminta on tarkalleen määrätty kun tila tunnetaan. Deterministisen sijaan järjestelmä voi olla esimerkiksi stokastinen, jolloin sen toimintaan liittyy jokin satunnainen komponentti, esimerkiksi differentiaaliyhtälössä voi esiintyä satunnaismuuttujia, jolloin saatu yhtälö ei kuvaakaan järjestelmän tilaa ajan funktiona vaan ainoastaan tilan jakaumaa. Kolmas vaihtoehto on, että järjestelmä on epädeterministinen, mikä tarkoittaa että sillä on aidosti useita eri polkuja; tätä käytetään erotuksena stokastisesta siten, että epädeterminismi tulee esimerkiksi mukaan malliin tuntemattomien vuorovaikutusten kautta.

Jatkuvan sijaan järjestelmä voi olla myös diskreetti. Diskreetin järjestelmän tilan määrittämät muuttujat saavat diskreettejä arvoja kuten kokonaisluku- tai boolean arvoja (tosi/epätosi). Järjestelmää jossa on sekä diskreettejä että jatkuvia muuttujia nimitetään hybridijärjestelmiksi. Diskreetin järjestelmän dynamiikkaa voidaan aina kuvat tilasiirtymärelaatiolla, joka kertoo mihin muihin tiloihin jostakin tietystä tilasta voidaan päätyä. Tämä relaatio on funktio jos järjestelmä ei ole epädeterministinen, ja jos järjestelmä on stokastinen, niin funktion arvoina ovat jakaumat tilojen yli. 

Predikaattiabstraktio viittaa siihen, että osa muuttujista korvataan predikaateilla. Predikaatti on totuusarvoinen väittämä joka koskee muuttujaa tai muuttujajoukkoa. Esimerkiksi jos meillä on muuttujat x ja y, niin väittämät x < y, x+y > 3, x < 0 jne ovat predikaatteja jotka puhuvat muuttujista x ja y. Tyypillisesti jos me käsittelemme jatkuvaa järjestelmää, predikaattiabstraktio on yksi tapa muuttaa järjestelmä diskreetiksi. Jos esimerkiksi x ja y ovat jatkuvia muuttujia, järjestelmän tilaa saatettaisiin abstrahoida esittämällä se kolmen predikaatin avulla: x < 0, y < 0 ja x² + y² < 9. Tällöin meillä olisi kahdeksan erilaista "tilaa" sen mukaan, missä kvadrantissa x ja y ovat ja sen mukaan ovatko ne 3-säteisen ympyrän sisällä vai eivät. Predikaattiabstraktio tuottaa epädeterminismiä vaikka alkuperäinen järjestelmä olisi kuvattu deterministisellä differentiaaliyhtälöllä. Esimerkiksi kun x = 5 ja y = 1, järjestelmä kehittyy niin, että y muuttuu negatiiviseksi, mutta pysyy ympyrän ulkopuolella ja kun x = 1 ja y = 5, y pienenee mutta pysyy positiivisena niin, että järjestelmä siirtyy ympyrän sisäpuolelle. Kumpikin arvoiyhdistelmä on kuitenkin mainittujen predikaattien kannalta "sama", eli abstraktio samastaa eri tavoin käyttäytyviä tiloja.

Jos tunnemme järjestelmän "riittävän hyvin" ja meillä on "riittävän hyvät" abstraktiot siten, että laadullisesti abstraktion tuottama malli kertoo meille "riittävästi", voimme luoda järjestelmän toiminnasta diskreetin mallin ja ennustaa, onko alkuperäisellä systeemillä jokin tietty abstrakti tila johon se päätyisi. Esimerkiksi voiko käydä niin, että sekä x että y ovat negatiivisia ja ympyrän ulkopuolella.

Sivuutan tässä nyt sen problematiikan joka liittyy tilasiirtymärelaation esittämiseen. Huomautan lisäksi että yleisessä tapauksessa tällaiset abstraktiot sisältävät potentiaalisesti satoja tai tuhansia predikaatteja siten, että järjestelmän diskreettienkin tilojen määrä on suurempi kuin koko maailmankaikkeudessa olevien atomien määrä; tällaisen järjestelmän kaikkien tilojen tutkiminen on yksinkertaisesti mahdotonta.

Voimme kuitenkin käyttää tähän logiikkaa, niin erikoiselta kuin se kuulostaakin. Yksi takavuosien menestyksekäs metodi oli niin kutsuttu rajoitettu mallintarkastus eli bounded model checking. Sen ideana on, että me esitämme järjestelmän alkutilan predikaattien avulla, esimerkiksi p1 & p2 & not p3 jne. Tämän lisäksi esitämme tilasiirtymärelaation logiikan kaavana siten, että jos tämänhetkisessä tilassa puhutaan predikaatista p, niin jälkimmäisessä puhutaan predikaatista p'. Esimerkiksi jos p on predikaatti joka vaihtaa totuusarvoaan jokaisessa siirtymässä, tätä merkitään p -> p', joka taas sievenee muotoon  not p or p'.

Oletetaan, että "virheellinen tila" voidaan ilmaista kaavalla Y. Jos meillä on jotakin tilajoukkoa kuvaava kaava X ja tilasiirtymän kaava P( ), niin sitä tilajoukkoa joka saavutetaan joukosta X käsin, voidaan ilmaista P(X). (Tämä on siis taas kaava). Kaikki predikaatit esiintyvät tässä kaavassa (se voi olla hyvinkin suuri) pelkkinä propositioina. alkutilan ollessa x, tarkistamme onko kaava X = (x tai P(x) tai P(P(x)) tai ....) yhdessä kaavan Y kanssa mahdollista tehdä todeksi, eli onko kyseinen kaava X ja Y satisfiable eli SAT. Valitettavasti X voi kuvata vain äärellisen määrän askelia (siitä nimitys "bounded") joten tämä menetelmä voi kyllä löytää virheitä, muttei voi todistaa että järjestelmässä ei sellaisia ole.

SAT on NP-täydellinen ongelma, mutta modernit SAT-ratkaisijat ovat niin tehokkaita, ja todellisista järjestelmistä peräisin olevat mallit ovat niin strukturoituja että SAT-ratkaisijat kykenevät ratkomaan tuhansien ja jopa miljoonien klausuulien mittaisia kaavoja, joissa on kymmeniä tuhansia tai satoja tuhansia muuttujia. Toki on aina patologisia tapauksia jotka tyystin tukahduttavat ratkaisijat, mutta ne ovat todellisen maailman malleissa hyvin harvinaisia.

Meidän ei ole kuitenkaan aivan pakko tyytyä siihen ettemme koskaan saisi todistettua järjestelmää täysin oikeaksi. On nimittäin mahdollista toisinaan löytää induktiivisia invariantteja jos sovelletaan abstraktiota luovasti.

Ensimmäinen, yksinkertainen tapa on yrittää löytää ns kiintopiste. Jos kaava X kuvaa kaikkia niitä tiloja joihin voidaan päästä n:llä tai sitä pienemmällä määrällä askelia, ja jos kaava (P(X) tai X) on yhtäpitävä kaavan X kanssa, tiedämme, että kaava X itseasissa kuvaa jo kaikki mahdolliset saavutettavat tilat; jos kaava (X ja Y) on ristiriitainen, ei järjestelmä voi saavuttaa tilaa jossa Y pätee. 

Tällainen kiintopiste voi olla kuitenkin niin monen askeleen päässä -- tai mikä pahempaa, järjestelmällä voi olla ääretön määrä mahdollisia tiloja (mikä tosin ei ole mahdollista jos käytämme tiukkaa predikaattiabstraktiota, mutta sivuutan sen nyt) -- että meiltä loppuu muisti tai aika ennenkuin löydämme kiintopisteen. Jos olemme nyt -- jonkin askelmäärän jälkeen -- todenneet että X kuvaa siihen mennessä saavutettavia tiloja, ja X ja Y ei ole SAT, voimme aina löytää tälle kaavalle niinsanotun interpolantin. Interpolantti on kaava Z, joka sisältää vain X:lle ja Y:lle yhteisiä symboleja, X implikoi Z:n ja Z on ristiriidassa Y:n kanssa.

Interpolantti Z voidaan nyt abstrahoida, siis tehdä siitä heikompi, kunhan se on edelleen ristiriidassa Y:n kanssa. Jos tätä merkitään kaavalla Z' niin sopivalla abstraktion valinnalla saatamme esimerkiksi pystyä osoittamaan että kaava Z' onkin kiintopiste -- se on siis induktiivinen invariantti, kaava joka kerran todeksi tultuaan pätee vaikka tekisimme kuinka tilasiirtymiä. Jos tällainen abstraktio löydetään, olemme kertakaikkisesti osoittaneet että Y ei voi toteutua järjestelmässä.