Nopeat ja hitaat.

Aloin vihdoin lukea Kahnemanin kirjaa Thinking, Fast and Slow. Ensimmäiset vajaa sata sivua ovat ainakin täyttä dynamiittia. Eräs ystäväni viittasi Kahnemaniin yhtenä "parhaimmista". En voi olla eri mieltä.

Karkeastiottaen kirjassa käsitellään kahta "systeemiä" ajattelussa, Systeemi 1:ä ja  Systeemi 2:a. Systeemi 1 on intuitiivinen ja nopea ja perustuu hahmontunnistukseen. Systeemi 2 on hidas ja perustuu strukturoituun ja eksplisiittiseen vertailuun. Kahnemanin esitys, esimerkkeineen ja koukkuineen, on erittän vangitseva ja vakuuttava. Hän tosin korostaa että kyse on metaforista tai abstraktioista, joiden ei voi olettaa olevan aivan täysin tarkkarajaisia, mutta abstraktio on erittäin toimiva, ja jo 24 tuntia sen omaksumisen jälkeen olen huomannut selkeän vaikutuksen omaan tietoiseen ajatteluuni ja huomioni suuntautumiseen.

Luin myös ns. laiskasta abstraktiosta, joka on aivan eri asia. Teen kytköksen kohta. Laiska abstraktio on menetelmä, jossa järjestelmää tutkitaan niin, että abstraktiotasoa karkeistetaan tarpeen mukaan ja vain niiltä osin kuin havaitaan jokin puute tai vuoto abstraktiossa. Konteksti, jossa sitä joudun tutkimaan, on tietokoneohjelman käyttäytyminen, mutta se toimii myös ajattelussa ja argumentaatiossa vallan hyvin. Esimerkkiohjelma on seuraavanlainen:
1 do {
2   lock();
3   old = new;
4   if(x){
5     unlock();
6     new++;
7   }
8 }while (new != old)

Tässä esimerkissä "x" on ehto, jota ei tulkita; se on abstraktio jota emme voi purkaa (tässä yhteydessä), vaan se on tosi tai sitten ei ole. lock() on funktio, joka asettaa "lukon" päälle ja unlock() asettaa sen pois. Haluamme osoittaa turvallisuusominaisuuden, joka sanoo, että poistumme tästä silmukasta vain, jos lukko on päällä. Oletuksena on myös että operaation "++" jäljiltä olio "new" ei ole koskaan sama kuin ennen. Jokainen ohjelmoinnista jotain ymmärtävä näkee kyllä, että väittämä pitää paikkansa.

Verifiointia varten ohjelma muunnetaan kontrollivuota kuvaavaksi graafiksi, jonka solmuina ovat ohjelman kontrollilausekkeet ja näiden lisäksi alkusolmu, joka kuvaa lähtötilannetta, ja loppusolmu, joka kuvaa lopussa (mahdollisesti) tapahtuvaa virhettä. Graafin kaaret eli tilasiirtymät taas ovat operationaalisia lausekkeita. Alustuksessa lukko laitetaan  pois päältä, ja siirrytään silmukkaan.
Laiska abstraktio aloittaa oletuksesta, että  mitä tahansa voi tapahtua, eli kontrollivuo voi edetä miten tahansa. Kun se päätyy virheeseen, virhe tarkastetaan. Alkuoletuksen voimassaollessa silmukka ajetaan loppuun ja siitä poistutaan riippumatta siitä, mitä aiemmin on tehty.  Saadaan aikaan "virhe".

Virhetilaan siirtymiselle on kuitenkin ehto, ja se ehto pitäisi pystyä osoittamaan todeksi niiden askelien perusteella, joilla virhetilaan päästään. Jos tämä ei onnistu, voidaan välissä tutkituille solmuille tietyt invariantit, joiden avulla voidaan todistaa ettei virhetilaan päästä. Abstraktio muuttuu karkeammaksi, koska nyt informaatiota on enemmän. Informaatiota etsitään kuitenkin vain juuri sen verran, että virhetilaan päätyminen tulee estetyksi.   Tätä tekniikkaa on tässä turha nyt käydä sen kummemmin erittelemään.

Olennaista on, että löydetään "tulos", joka tarkastetaan, ja tarkastuksen seurauksena todetaan, että tulos on väärä, joten abstraktiota pitää muuttaa. Tämä eroaa CEGAR:ista siinä, että prosessia ei aloiteta alusta, vaan polku vain merkitään uudelleen ja prosessia jatketaan. Tästä nimitys "laiska abstraktio".

Graafi kasvaa kun abstraktio muuttuu hienojakoisemmaksi, koska kontrollivuo vie eri tilaan; esimerkiksi jos ehto "x" on tosi, ja absraktiota on hienonnettu sen verran, että lukon tila tunnistetaan, riviä 8 vastaavia tiloja on kaksi: toisessa lukko on päällä ja toisessa ei. Jälleen saamme uuden virhetilan, ja huomaamme, että vertailun new != old  tuloksen säilyttämiseksi abstraktiota täytyy jälleen hienorakeistaa. Jne.


On mielenkiintoista huomata, että tässä käytetään tavallaan samantapaista jaottelua kuin Kahnemanin systeemit 1 ja 2. Virheen löytäminen on nopeaa, koska kontrollivuon läpikäynti on hyvin tehokasta nykyisillä tietokoneilla. Virheen tarkastaminen ja abstraktion tarkentaminen puolestaan on melko kallista, koska siinä pitää käsitellä (pahimmillaan) monimutkaisia loogisia lausekkeita. Tämä rakenne myös vastaa hyvin sitä intuitiota, joista ihmisen Systeemi 1:n tekemät virheet usein kumpuavat. Kahneman ottaa esimerkkinä kirjassaan seuraavan tehtävän; lukijaa pyydetään vastaamaan intuition perusteella, eikä edes yrittämään ratkaisemaan ongelmaa ensin:

Tennismaila ja pallo maksavat yhteensä 11 euroa. Tennismaila maksaa 10 euroa enemmän kuin pallo. Paljonko pallo maksaa?

Intuitiivinen ratkaisu on tässä melkein kaikilla väärä. Fiksummat ihmiset kuitenkin ratkaisevat ongelman melko helposti yksinkertaisesti tarkastamalla vastauksensa: jos pallo maksaisi todellakin sen yhden euron, niin mailahan maksaisi 11 euroa, ja vastauksen olisi silloin pakko olla väärä. Systeemi 1 generoi vastauksia. Aivan kuten laiska abstraktio.

Päätöksenteko sellaisessa maailmassa, jossa likiarvovastauksen nopea saaminen on usein tärkeämpää kuin vastauksen oikeellisuus, tuottaa valintapaineen juuri tällaisen ajattelun kehittymiselle. Tämä aihe on hyvin mielenkiintoinen, ja on aikalailla onnenkantamoinen, että oman tutkimukseni ja huvikseni lukeman tekstin välillä on näinkin vahva yhteys.