Invariantti

Olen kirjoittanut aiemminkin invarianteista. Olen tutkinut jonkin verran ns. Craig:in interpolantteja ja niiden induktiivisia invariantteja, ja yksi julkaisuni käsittelee induktiivisten interpolanttien löytämistä.

Olen tehnyt jonkin verran käytännön ohjelmointityötä (sellaista josta joku muu jopa maksaa). Muutoin kokemukseni rajoittuu pitkälti akateemisiin ympyröihin ja melko simppeleihin pikkunäppäriin koodinpätkiin. Käytännön työssä havaitsin hyvin nopeasti hyödylliseksi ajattelutavan, jonka opin Ralph-Johan Backin luennolla.  Tästä on aikaa liki 15 vuotta, joten en muista tilannetta tarkkaan; Olin Turussa konferenssissa jossa yksi workshop käsitteli ohjelmoinnin opettamista. Back kertoi heidän kokeilleen sellaista pedagogista tyyliä, jossa opiskelijoiden kehotettiin aina ennen minkäänlaisen silmukkarakenteen kirjoittamista ensin miettimään kyseisen silmukan silmukkainvariantin.

Ihmisen ajattelu on luonteeltaan abstraktia ja usein rekursiivista. Rekursiivisuus on kuitenkin yleensä tiedostamatonta, ja sen nouseminen tietoisuuteen synnyttää usein kokemattomalla ihmisellä hämmenystä. Merkittävä osa huumorista perustuu itse asiassa rekursiivisuuteen, ja rekursiovitsit ovat nörttivitsien aatelia. Klassinen vitsi on, että kun kysytään "Mikä on rekursiivinen määritelmä?", niin vastaus on "Perustapaus, jota seuraa rekursiivinen määritelmä".

Ihmisillä on voimakas tarve operationalisoida rekursio iteraatioksi, prosessilla jota kutsun usein aukikelaamiseksi. Esimerkiksi jos joku kysyy miten löydämme polun paikasta A paikkaan B, niin voimme vastata "Jos A = B, ollaan jo perillä. Muutoin otetaan A:sta yksi askel kohti B:tä, ja etsitään tästä uudesta paikasta polku B:hen". Tämä on rekursiivinen määritelmä, mutta se ei tietenkään aina toimi, koska termi "Kohti B:tä" on epämääräinen. Jos me kelaamme tämän implisiittisen prosessin auki, niin usein teemme sen niin, että samalla esimerkiksi kiellämme käymästä samassa paikassa kahdesti.

Jos lähdemme oletuksesta että polku aina löytyy, niin tässä aukikelauksessa voidaan ilmaista invariantti  joka sanoo, että missä ikinä olemmekin, sieltä pääsee paikkaan B. Jotta se tapa jolla toteutamme tämän iteraation olisi oikea, sen täytyy säilyttää tämä invariantti. Näinollen, jos kiellämme esimerkiksi käymästä samassa paikassa kahdesti, voi invariantti helposti mennä rikki: Kuvitellaan että meillä on polku A-->C --> D ---> B, ja sen lisäksi polku C --> E ja E--> C. Jos me lähdemme C:stä tä E:hen, emmekä saa palata C:hen, on invariantti efektiivisesti rikki kun olemme E:ssä.

Tätä ongelmaa ei korjaa esimerkiksi se, että tarkennamme "askel kohti B:tä" siten, että sanomme että pisteen johon siirrymme pitää olla "lähempänä" B;tä. Jos esimerkiksi piste E esimerkissämme on aivan B:n vieressä, mutta näiden välillä vain on ylipääsemätön este, emme tiedä tätä ennen kuin tulemme pisteeseen E ja huomaamme että olisi palattava pisteeseen C, mikä puolestaan on kiellettyä.

Olen jumissa työssäni seuraavanlaisen ongelman kanssa. Meillä on graafi -- sivuutan ison läjän itse ongelman kannalta merkityksettömiä yksityiskohtia -- jossa on solmuja ja kaaria. Kaarilla on jonkinlainen pituus ja jokainen kaari yhdistää kaksi solmua, sillä on siis alku- ja loppupää. Teemme graafille kontraktiohierarkian. Tämä tarkoittaa että "poistamme" solmuja iteratiivisesti ja aina poistaessamme lisäämme oikopolun kahden sen naapurin välille, jos näiden välinen lyhin polku (jäljellä olevassa graafissa) kulki poistetun solmun kautta.

Invariantti tässä prosessissa on, että vielä poistamattomien solmujen väliset lyhimmät polut ovat saman pituisia kuin alkuperäisessä graafissa. Tämän invariantin voimassaolo on helppo todeta: Jos invariantti on voimassa ja poistamme solmun x, niin jokainen lyhin polku kahden solmun a ja b välillä joka ei kulkenut x:n kautta, säilyy sellaisenaan. Jos taas se kulki x:n kautta, niin se kulki ensin johonkin solmuun u, sieltä x:ään ja sieltä v:hen, missä u ja v jäävät graafiin. Jos u:n ja v:n välinen lyhin reitti kulkee u->x->v, niin jokainen polku joka kulkee siten että se käy ensin u:ssa ja sitten v:ssä, voidaan tehdä lyhyemmäksi vaihtamalla osareittu u:sta v:hen reitiksi u->x->v. Tässä tilanteessa lisäämme oikopolun u-->v, ja tämä reitti on yhtä pitkä kuin ennenkin. Toisaalta jos lyhin reitti ei kulje x:n kautta, niin x:n poistaminen ei vaikuta mitenkään.

Solmut muodostavat poistamisjärjestyksensä mukaisen hierarkian. Solmu, joka poistetaan aiemmin, on hierarkiassa alempana, ja myöhemmin poistettu solmu ylempänä. Kun estimme kahden solmun välistä lyhintä polkua, etsimme  ns konkaavin polun. Tämä polku on sellainen, että sen alkuosa kulkee lähtösolmusta aina hierarkiassa ylöspäin, ja kun se saavuttaa polun "korkeimman" solmun, se tämän jälkeen kulkee aina alaspäin kunnes se saavuttaa maalisolmun.

Voimme todistaa että tällainen polku on olemassa ja se vastaa alkuperäisen graafin lyhintä polkua: olkoon lähtösolmu u ja maalisolmu v. Näiden välillä on alkuperäisessa graafissa jokin lyhin polku v1, v2, ... , vn, missä v1 = u ja vn =v. Olkoon vk näistä se, joka on hierarkiassa korkeimmalla. Voimme osoittaa, että meillä on oikopolkuja hierarkiassa ylöspäin kulkeva polku u:sta vk:hon (ja samalla tavalla voimme osoittaa että sellainen on alaspäin vk:stä v:hen) seuraavasti:

olkoon vi se solmu, joka on hierarkiassa korkeimmalla välillä v1..vk-1. Edellä mainitun invariantin nojalla, ennen vi:n poistamista, meillä oli jäjellä lyhin polku vi-->vk. Koska välissä ei voinut tuolloin olla muita solmuja, meillä on oltava oikokaari vi-->vk. Nyt voimme rekursiivisesti todeta taas, että saman argumentin nojalla meillä on jokin solmu välillä v1 ... vi-1 jne.

Kirjoitin tämän blogikirjoituksen, koska kaikesta tästä huolimatta, testiaineistossa on tapaus, jossa erään sillan yli kulkevaa lyhintä polkua ei hierarkia säilytä. Se on olemassa alla olevassa graafissa, mutta sitä ei löydy hierarkian avulla. Jossakin kohtaa koodia siis jokin näistä asioista tehdään siten, että invariantti rikkoutuu.

Kun kirjoitin koodin, mielestäni pidin koko ajan tämän invariantin mielessä ja pidin huolen ettei mikään operaatio riko sitä. Tyypillisesti tällaisissa tapauksissa on kyse joko abstraktiorikosta -- esimerkiksi jokin tieto viittaa johonkin mikä on muuttunut välissä -- tai ns reunatapauksesta. Olen mielestäni eliminoinut kummankin vaihtoehdon. Jäljelle jää muutama vaihtoehto. Kyseessä voi olla logiikkavirhe: Jokin ehto on kirjoitettu tavalla, jonka semantiikka on eri kuin se, mitä tarkoitin. Tämä on epätodennäköisen tuntuinen selitys siksi, että virhe on niin harvinainen. Kyseessä voi olla toki jonkin rakenteellinen poikkeama jostain tekemästäni oletuksesta, joka on riittävän harvinainen tuottamaan tällaisen ongelman.

Tämä on kiusallista.

EDIT: Vika liittyi tietorakenteeseen ja algoritmiin. Erässä kohtaa kun graafin kaaria järjesteltiin uudelleen, osa tiedosta jäi päivittämättä. Tietty invariantin kannalta olennainen informaatio ei ollut siellä missä pitää. Virhe myös "piilotti itsensä", sillä kun konstruktion jälkeen graafi luettiin, informaatio meni oikeaan paikkaan. Lopulta löysin sen ja sain korjattua tänä aamuna, useamman tunnin buginmetsästyksen jälkeen.

Huomenna lähden lomalle.