Atomistinen kaava

Wikipediasta
Siirry navigaatioon Siirry hakuun

Atomistinen sääntö eli atomistinen kaava on matemaattisessa logiikassa käytetty erikoistapaus kaavasta, jolla ei ole syvempiä sisärakenteita. Sitä kutsutaan lyhyesti myös atomiksi. Atomistisessa kaavassa ei siis ole alakaavoja sisällään. Atomit ovat siten yksinkertaisimpia hyvin-määriteltyjä logiikan kaavoja. Yhdistettyjä kaavoja voidaan muodostaa yhdistämällä atomistisia sääntöjä keskenään tyypillisillä logiikan konnektiiveilla.

Atomististen kaavojen tarkka muoto riippuu käsiteltävästä logiikasta. Esimerkiksi propositiologiikassa atomistiset kaavat ovat muuttujia, jotka viittaavat propositioihin. Predikaattilogiikassa atomit ovat predikaattisymboleita, joihin voi liittyä argumenttejakin. Tällöin kukin argumentti on luonteeltaan termi, joka voi edelleen sisältää atomistisia kaavoja. Prolog-ohjelmointikielessä on käytettävissä edellä kuvatut predikaattilogiikan piirteet, mutta niiden lisäksi vielä rekursio, peräytys ja samastus, joiden ansiosta Prologia voidaan pitää tyypillisenä Turing-vahvana ohjelmointikielenä.

Atomistinen kaava on ensimmäisen kertaluvun logiikkaa

[muokkaa | muokkaa wikitekstiä]

Hyvin määritellyille ensimmäisen kertaluvun logiikan termeille ja proposioitioille pätee seuraava syntaksi:

Termit ovat muotoa:

t ::= c | x | f (t1, …, tn),

joten termi on määritelty rekursiivisesti joko vakioksi c (nimetty objekti), tai muuttujaksi x, tai funktiksi f, johon liittyy n kappaletta argumentteja. Funktiot sovittavat objektien joukkoja ja viittauksia itse objekteihin.

Propositiot ovat muotoa:

A, B, …  ::= P (t1, …, tn) | A ∧ B | ⊤ | A ∨ B | ⊥ | A ⊃ B | ∀x. A | ∃x. A ,

joten propositio määritellään rekursiivisesti n-argumenttiseksi predikaatiksi P, jonka argumentteina ovat termit tk, mutta myös lausekkeeksi, joka koostuu loogisista konnektiiveista (and, or) sekä kvanttoreista (for-all, there-exists), joita käytetään yhdessä muiden propositioiden kanssa.

Atomistinen kaava (atomi) on yksinkertaisesti predikaatti, jota on sovellettu viittaamaan termien muodostamaan monikkoon. Atomistinen kaava on siten muotoa P (t1, …, tn) predikaatille P ja termeille tk.

Muita hyvin määriteltyjä kaavioja saadaan kokoamalla atomeja yhteen kvanttoreiden ja konnektiivien avulla.

Esimerkiksi kaava ∀x, P(x) ∧ ∃y, Q(y,f(x))∨ ∃z. R(z) sisältää atomit

  • P(x)
  • Q(y, f(x))
  • R(z)

Kun kaikki atomin termit ovat maadoitettuja, silloin atomia kutsutaan maadoitetuksi atomiksi tai maadoitetuksi predikaatiksi.

Atomistinen kaava lähdekoodin analysoinnissa

[muokkaa | muokkaa wikitekstiä]

Atomistinen kaava on olennainen määrittely ohjelmistoatomille, joka muodostaa symbolisen analyysin metakäsitteen, symboli, toiminnallisuuden. Tulkinta tarkoittaa symbolisessa analyysissä maadoitetun predikaatin käyttämistä kyselyn paluuarvona, mahdollisimman pitkälle yksinkertaistettuna.

Kirjallisuutta

[muokkaa | muokkaa wikitekstiä]