keskiviikko 19. elokuuta 2009

Metodi ja Abstraktio.

Abstraktio voidaan - ja on usein hyödyllistä - kuvitella eräänlaiseksi "kuplaksi" tai "kaivoksi", jossa majailee joukko erilaisia havaintokäsitteitä, joista abstraktio muodostuu.

Esimerkiksi "pyörän" abstraktio sisältää havainnon "ympyrästä" ja sen keskipisteessä sijaitsevasta navasta tai akselista. Abstraktio sisältää kaikki ne tavat muodostaa "pyörä" niin, että ympyrän kehä kiertää tätä napaa tai akselia.

Jokaisen abstraktion ongelma on kuitenkin se, että se vuotaa. Tässä yhteydessä tarkoitan, että kun sovellamme abstraktiota johonkin partikulaariseen ilmentymistapaan, kuten vaikkapa polkupyörän pyörään, se ei täysin noudata sitä, mitä abstraktiolta odotamme. Ensiksikin, sen toiminnassa on jotain aivan olennaista, jota abstraktiomme ei ilmaise. Polkupyörän pyörässä
on olennaista esimerkiksi se, että pyörä pyörii akselin ympäri; tämä voidaan tietenkin ottaa
mukaan alkuperäiseenkin abstraktioon.

Tällä tavalla abstraktiota voidaan tarkentaa. Tarkentaminen kuplametaforassa tarkoittaa, että jaamme kuplan osiin tai leikkaamme siitä paloja pois. Oletamme siis enemmän abstraktiostamme. Tietyssä mielessä abstraktiosta tulee "vähemmän abstrakti", kaivometaforalla ilmaistuna matalampi. Tarkentaminen tukkii yhden vuodon, mutta tarkentaminen voi luoda uusia vuotoja siten, että jokin intuitiivisesti "pyöränä" pitämämme ei tarkennuksen jälkeen olekaan enää pyörä.

Verifiointitutkimuksessa abstraktiota tarvitaan, koska "konkreettinen" verifioitava järjestelmä on aivan liian kompleksinen. Sen abstrahoitu versio on yksinkertaisempi toiminnaltaan. Abstraktio tehdään, kuten olen jo aiemmin esittänyt, jonkin samuuskäsitteen, eli semantiikan avulla. Abstraktimpi semantiikka pitää alkuperäistä järjestelmää "samana" alati yksinkertaisempien järjestelmien kanssa.

Verifionnissa käytetään joskus menetelmää, joka perustuu abstraktion tarkentamiseen. Menetelmä toimii siten, että valitaan ominaisuus P(), jonka paikkansapitävyyttä koko järjestelmässä S tutkitaan. Ominaisuus ilmaistaan sopivalla logiikalla, mutta se on epäolennaista. P(S) pätee tai ei päde, mutta emme tiedä tätä etukäteen. Abstraktion tarkentaminen toimii niin, että valitsemme abstraktiohierarkian Ai(), joka on kuvaus S:ltä sen "abstrahoidulle" versiolle. Ai(S). A0 on kaikkein abstraktein ja jollakin k:n arvolla Ak(S) = S. (Tarkalleenottaen tässäkin välissä on samuuskäsite eikä varsinainen yhtäsuuruus, mutta samuuskäsite on sellainen, että samanlaisille järjestelmille pätevät tarkalleen samat valitun logiikan väittämät)

Abstraktiohierarkia valitaan lisäksi siten, että kaikilla i pätee: P(Ai(S)) &rarr P(Ai+1(S)). Verifionti tapahtuu niin, että kaikkein abstrakteimmasta lähtien
tarkastamme päteekö P(Ai(S)), jos se ei päde, tarkennamme abstraktiota. Tämä siksi, että "ei päde" on helppo todeta, kun taas "pätee" vaatii koko järjestelmän
tutkimisen. Aivan kuin on yleisestikin tieteessä.

Kaikessa tieteessä, jossa käytetään abstraktiota, pyritään tällaiseen merkitysten hierarkiaan vähintäin implisiittisesti. Falsifikointiin perustuva empiirinen tiede suorastaan edellyttää tällaista. Usein toki mallinnuksessa myönnetään, että abstraktiohierarkia on joko ääretön (jolloin selkeä falsifiointi epäonnistuu aina) tai se ei oikeasti ole monotoninen. Epämonotonisuus, niin epäilen, johtuu siitä, että toisin kuin idealisoiduissa järjestelmissä, tosimaailmassa kaikki abstraktiot vuotavat aina.

Tämä ei ole ainoa tapa ajatella abstraktiohierarkiaa empiirisessä tieteessä. Sen voi ajatella myös "takaperin", niin, että lisäabstraktio itseasiassa tekee useammat ominaisuudet tosiksi ja
falsifiointiprosessi on sitä, että sukellamme abstraktiohierarkiaan löytääksemme kohdan, jossa väittämä muuttuu epätodeksi. Näin voidaan ajatella esimerkiksi Newtonin mekaniikalle käyvän kun mittakaavaa pienennetään (kvanttimekaniikka) taikka kun nopeutta tai tiheyttä kasvatetaan (suhteellisuusteoria).

(EDIT: Mistä saisi lukijoita, joita tällaiset asiat kiinnostavat, ja jotka viitsivät kommentoida?)

6 kommenttia:

kpkoskin kirjoitti...

"Jokainen kaava puolittaa lukijamäärän" :-)

Jos nyt pysyin kärryillä tuossa päättelyssäsi, niin malli A_{\infty} olisi "todellinen" ja A_0 "abstraktein" taso. Nyt sitten malli on "oikea" ominaisuuden P suhteen jollakin abstraktiotasolla A_k ja siitä eteenpäin (kaikilla k:ta suuremmilla arvoilla), koska abstraktiotasot on siten järjestetty (monotoonisuus olettama).

Minua jäi tuossa vaivaamaan nimenomaan tuo monotoonisuus-olettama. Mihin se perustuu? Onko meillä olemassa jokin yksikäsitteinen menetelmä luokitella abstraktiotasoja se. voimme sanoa abstraktiotasojen kasvavan monotonisesti? Kumpi on abstraktimpi tulkinta sähkömagneettiselle säteilylle aaltotulkinta vai hiukkastulkinta?

Mielestäni tässä on fundamentisti kyse eri asiasta kuin viittaamastasi "vuotamisesta", koska se kai liittyy nimenomaan abstraktion implementointiin (ei niinkään "ideaan")

Tiedemies kirjoitti...

Joo, voi ajatella niin, että on A_\infty, mutta käytännössä näissä tuo abstraktiohierarkia on äärellinen, eli on joku raja.

Monotonisuusolettaman perustelu omissa jutuissani on vähän hankala esittää lyhyesti, mutta annan esimerkin:

Meillä on tarkasteltavana "laskuri", joka aloittaa nollasta ja johon on kaksi operaatiota, +1 ja -1. Pitäisi verifioida, ettei laskuri koskaan mene alle nollan tietyssä käyttötarkoituksessa.

Laskurin "oikea" tilajoukko on tietenkin ääretön, ja kontekstista riippuen se voi kasvattaa tilojen määrää hurjasti, mutta "oikeasti" emme ole kiinnostuneita tästä.

Abstrahoidaan: Oletetaan, että laskurilla onkin vain äärellinen määrä arvoja: 0,1,...,k, "enemmän".

A_0 on siis laskuri, jossa on arvo "nolla tai enemmän". Jokainen inkrementointi saattaa sen arvoon "enemmän" ja jokainen vähentäminen on epädeterministisesti joko "nolla" tai "enemmän" (koska abstraktio hukkaa tiedon tästä). Vähentäminen tilassa "nolla" on virhe.

Tällaisessa järjestelmässä, jos konteksti takaa, että inkrementointeja ei tehdä enempää kuin 5, niin mikä tahansa abstraktiotaso 5:stä ylöspäin takaa, että P pätee, jos järjestelmä ei oikeasti yritä vähentää laskurista nollassa.

---

Käytin "vuotamista" hieman yleisemmässä mielessä kuin implementaatiossa käytetään. Tarkoitin sitä, että abstraktion rajat huomataan epätarkoituksenmukaiseksi kun yritetään soveltaa abstraktiota jollakin tavalla.

Tämä "vuotaminen" johtaa siihen, että kiltisti käyttäytyvää abstraktiohierarkiaa ei ole.

Kumpi on abstraktimpi tulkinta sähkömagneettiselle säteilylle aaltotulkinta vai hiukkastulkinta?

Mielestäni ei kumpikaan. Ne ovat eri abstraktioita.

kpkoskin kirjoitti...

Niin, joissakin suhteellisen yksinkertaisissa tapauksissa tuo varmaan toimii. Minusta vain vaikutti siltä, että vähäistä monimutkaisemmassa tapauksessa tuo rakennelmasi on enemmän ja vähemmän hyödytön, koska abstraktiotasoa ei ole helppo määritellä "oikein".

Eli epäilen, että noiden abstraktiotasojen luokittelu on useimmissa tapauksissa työläämpää kuin asioiden osoittaminen jollain muulla tavoin.

Abstraktioissa "monotoonisuus" on kyseenalainen muutenkin, koska on vähintään kyseenalaista, voiko malleja järjestää muuten kuin luokitteluasteikolla (ei esimerkiksi järjestysasteikolla)


----
En tiedä, mihin tuota oikeasti käytät, mutta jos kyseessä on tuollainen algoritmien verifiointi, niin mikset mielummin käytä esim. Turingin konetta? Sekin toki on hankala, jos kyseessä on monimutkaisempi malli, mutta kuvittelisin, että sen avulla on ainakin teoreettisesti vahvemmalla pohjalla.

ankyrimato kirjoitti...

Ehkä en nyt tajunnut jotain, mutta päättely voi olla monotonista tai ei-monotonista. Tämä ei liity millään tavalla abstraktioon käsitteenmuodostuksessa, joka on korkeamman tyypin luokkaominaisuuden määrittelyä alempien perusteella.

http://plato.stanford.edu/entries/logic-nonmonotonic/

Tiedemies kirjoitti...

Tässä ei ollut kyse päättelyn monotonisuudesta. Ajatellaan näin:
Meillä on struktuuri S, joka on tai on olematta jonkin (esim lineaarisen aikalogiikan) kaavan P malli. Haluamme siis tietää päteekö S |= P.

Meillä on S:n "rakennusohje", mutta emme halua rakentaa S:ää, kun se on niin kauhean kauhean iso.

Otamme käyttöön "abstraktion", joka on vain kuvaus S:n "rakennusohjeilta" S:n domainiin. Se "abstrahoi", so. poistaa rakennusohjeista jotain yksityiskohtia ja rakentaa "abstraktin" version S:stä, S_i:n

Meillä on hierarkia näitä abstraktioita, "karkeasta" hienompaan. S_0 on karkein jne.

Tällä hierarkialla on sellainen monotonisuusominaisuus jos S_i |= P, niin myös S_{i+1} |= P.

Siis, jos löydetään hierarkiasta joku kohta, jossa väittämän havaitaan pätevän, niin voidaan lopettaa.

Verifioitaesssa esimerkiksi lineaarista aikalogiikkaa, tämä on tavattoman kätevää, koska "ei päde" löytyy usein nopeasti, jos se on totta, mutta "pätee" on kallis todeta, kun se vaatii koko S:n (tai siis S_i:n) rakentamisen.

Tästä on tavattoman käteviä yleistyksiä myös, koska abstraktiohierarkian ei tarvitse olla edes tuolla tavalla suoraviivainen, vaan se voi olla hila, esim. meillä on joukko abstrahoitavia ominaisuuksia p_1....p_n ja näillä on 2^n erilaista vaihtoehtoa; "kaikki" on ilmeisesti A_bottom ja "ei mitään" A_top. Ns. vastaesimerkkiohjatussa abstraktiontarkennuksessa (counter-example guided abstraction refinement) vastaesimerkistä bongataan abstraktit askeleet ja tarkennetaan abstraktiota niiltä osin. Tällöin, jos jossain vaiheessa (vielä abstrahoidusta) mallista löytyy vastaesimerkki, jonka jokainen askel on abstrahoimaton, se on vastaesimerkki myös koko S:ssä, ja voimme todeta virheellisyyden jo tässä vaiheessa.

Esitykseni oli hölmö, huomaan nyt, että tästä puhuminen on vaikeaa yleistajuisesti. Oikeasti nämä hommat ovat tavattoman yksinkertaisia, mutta niitä käytetään sen verran vähän, että niistä puhumiseen käytetty kieli on kömpelöä.

Tiedemies kirjoitti...

Mihin näitä käytetään, niin meillä on yleensä joku järjestelmänkuvauskieli, esimerkiksi vaikka promela:
http://spinroot.com/spin/Man/promela.html
Tai DiVinE:
http://divine.fi.muni.cz/page.php?page=language

Idea on siis se, että otetaan kielellä annettu "ohjelma" ja muutetaan se (suuren suureksi) graafiksi, joka kuvaa kaikkea sitä, mitä "ohjelma" voi tehdä.

Yleisessä tapauksessa tietenkin graafi on ääretön, joten sitä ei voi rakentaa edes periaatteessa. Esimerkiksi jos sillä on inputtina "kokonaisluku", niin ensimmäinen askel on "syötä kokonaisluku" ja luonnollisesti seuraajatiloja on äärettömästi. Siksi tarvitaan aina jotain abstraktiota.

Graafin rakentaminen on jossain määrin pelkkää mielikuvitusta. Se on "olemassa" vain jotenkin implisiittisesti, rakennusohjeen muodossa, esimerkiksi juuri ohjelmakoodina.

Graafista etsitään usein jotain, mikä rikkoo annettua vaatimusta. Esim lineaarisen aikalogiikan ominaisuuksia tutkittaessa on ideana se, että etsitään äärettömiä suorituspolkuja (so. sellaisia, joissa on silmukka) jotka rikkovat annetun suorituspoluista puhuvan kaavan. Se on siis "bugi" järjestelmässä. Sopivasti rakennusohjetta ja kaavaa vierekkäin tulkitsemalla ei tarvitse koko roskaa rakentaa. Joskus kuitenkin täytyy ja silloin loppuu aika tai muisti kesken.