Peitos.

Peittävyys on käsite, joka esiintyy eri abstraktiotasoilla hyvin samaan tapaan, jopa arkikielessä. Matematiikassa (pistejoukkojen tapauksessa) esimerkiksi kokoelma joukkoja on peite jollekin joukolle, jos kaikki joukon alkiot kuuluvat johonkin kokoelman joukkoon. Useimmissa logiikoissa voidaan myös sanoa, että väittämä A peittää väittämän B jos A on B:n looginen seuraus. Huomatkaa: tämä menee tähän suuntaan totuuden säilyttävässä päättelyss, koska jos A on B:n looginen seuraus, niin A on yleisempi väittämä, siis useammin tosi kuin B. 

Kripke-rakenne on modaalilogiikoiden (yleensä aikalogiikka) laskennassa yleensä käytetty malli, joka on periaatteessa graafi, jonka jokaisessa solmussa pätee jokin (esimerkiksi ensimmäisen kertaluokan) logiikan väittämäjoukko eli teoria. Esimerkiksi edellisessä kirjoituksessani käsittelemäni kontrollivuon analyysi voidaan ajatella Kripke-rakenteena, jossa siirrytään tilasta toiseen ja abstraktion määräämät väittämät joko pätevät tai eivät päde.

Rakennetta ei tunneta kokonaan, eikä sitä edes (yleisessä tapauksessa) voida tuntea, koska se voi olla ääretön. Abstraktio toisaalta yleensä takaa, että se on äärellinen. Esimerkiksi tietokoneohjelmaa analysoitaessa malli voidaan rakentaa jokaisella käytettävällä abstraktiotasolla kokonaan, mutta joissain tapauksissa se saattaa olla niin suuri, ettei sitä voi laskea. Tähän on olemassa keinoja, joilla ongelmaa helpotetaan. Yksi näistä on peittävyys.

Peittävyyttä käytetään seuraavalla tavalla: Oletetaan, että päädymme abstraktiin tilaan, jossa pätee väittämä P(x), ja kontrollin tila on a.  Symboli "x" tässä nyt viittaa vain yleisesti kaikkeen siihen, mitä osaamme sanoa tilasta. Merkitään tätä parilla (a, P(x)). Tätä varten olemme lisänneet Kripke-rakenteeseemme (emme välttämättä tosiasiassa koskaan tee tätä rakennetta, se on matemaattinen abstraktio, jonka on tarkoitus kuvata prosessin eteneminen, ei välttämättä mikään todellinen ilmiö) uuden tilan. Olemme päätyneet tähän erinäisten vaiheiden kautta alkutilasta. Ja matkalla kontrolli on saattanut kulkea myös tilan a kautta. Tutkimme tilan historian (joka on tallessa joko osittain tai kokonaan) ja löydämme sieltä tilan (a, Q(x)). Jos kuitenkin huomaamme, että Q(x) on P(x):n looginen seuraus, meidän ei tarvitse tutkia pidemmälle, sillä tila (a, Q(x)) peittää tilan (a, P(x)). Siis, kaikki, mitä voimme sanoa voivan tapahtua tilassa (a, P(x)), voi tapahtua myös tilassa (a, Q(x)), koska jälkimmäinen on edellistä yleisempi tapaus. Se on siis abstraktimpi. Jos tila (a, Q(x)) on turvallinen, siis jos siitä ei voi suorittaa mitään virhettä, ei tällaista ole myöskään tilasta (a, P(x)). Kääntäen, jos tilasta (a, P(x)) voidaan tehdä virhe, sellainen voidaan tehdä myös tilasta  (a, Q(x)).