1  x := 1
2  while n > 0 do
3      if n mod 2 = 1 then
4          n := n−1
5          x := x·a
6      n := ⌊n/2⌋
7      a := a·a

Tehtävä:
Binääripotenssi

Lyhyt MathCheck-ohje (uuteen välilehteen)

Turvallinen asiointi verkko­pankissa edellyttää tiedon salausta. Yksi lasku­toimitus, jota nyky­aikaisissa salaus­menetelmissä tarvitaan, on an mod M, missä kaikki kolme lukua ovat isoja (esimerkiksi 300-numeroisia). Sen suorittaminen laskemalla n−1 eli noin 10300 kerto­laskua ja modulo-operaatiota veisi aikaa melko monta maailman­kaikkeuden ikää. Tässä tehtävässä tutustutaan keinoon suorittaa lasku tarpeeksi nopeasti. Yksin­kertaisuuden vuoksi modulon ottaminen jätetään näyttämättä, mutta se on helppo lisätä algoritmin joka kierrokselle.

Binääripotenssi näyttää tältä. Ruskealla kirjoitettua riviä 4 ei oikeasti tarvita, mutta sen lisääminen helpottaa algoritmista päättelemistä. Sen pois jättä­minen ei muuta sitä arvoa, mikä rivillä 6 sijoitetaan n:ään, koska rivin 3 ehdon vuoksi se suoritetaan vain kun n on pariton. Rivien 4 ja 6 välissä n:n arvoa ei käytetä mihinkään.

1  x := 1
2  while n > 0 do
3      if n mod 2 = 1 then
4          n := n−1
5          x := x·a
6      n := ⌊n/2⌋
7      a := a·a

Algoritmi on kopioitu oikealle alas, jotta se olisi käsillä myös kun yllä oleva kopio on kadonnut ruudun yläreunan yläpuolelle.

Merkitään muuttujien n ja a arvoja algoritmin alussa symboleilla N ja A. Algoritmin tehtävänä on siis laskea AN, missä N on luonnollinen luku. Ensin todistamme, että algoritmi laskee oikean loppu­tuloksen ja sen jälkeen selvitämme, kuinka nopeasti se toimii.

Binääripotenssin toiminnan ytimessä on yhtälö AN = xan. Kutsumme sitä invariantiksi. Todistamme, että se on voimassa aina rivin 2 alussa ja että siitä seuraa, että algoritmi laskee oikean loppu­tuloksen. Koska potenssi­lasku ei ole määritelty esimerkiksi silloin kun kanta­luku on nolla ja eksponentti negatiivinen, meidän on pidettävä tarkkaan huoli, että väitteissämme eksponentit ovat aina ei-negatiivisia.

Kun riville 2 tullaan ensimmäisen kerran x = , a = , n = ja xan = . Ilmaise vastaukset symbolien N ja A avulla.
tai

Silmukoiden oikeaksi todistamisessa oletetaan, että invari­antti pätee silmukan alussa, ja todistetaan, että se pätee silmukan vartalon lopussa. Niinpä oletamme, että invariantti pätee rivin 2 alussa, ja alamme käydä silmukkaa läpi.

Rivin 3 alussa tiedetään varmasti, että n. Tämän tiedon ansiosta rivi 4 ei voi johtaa kiellettyyn n:n arvoon.
tai

Koska n muuttuu rivillä 4, rivin 5 alussa invariantti ei päde sellaisenaan, vaan muutetussa muodossa:
AN = .
tai

Vastatessasi edelliseen kohtaan huomasit ehkä, että tämän muodon voi päätellä suoraan, mutta voi olla vaikeaa miettiä pitääkö sijoituksen n := n−1 vaikutus ottaa huomioon lisäämällä vai vähentämällä invariantissa n:ään ykkönen. Jos sijoituslauseen oikealla puolella on jotain moni­mutkai­sempaa, vaikeus kasvaa. Siksi opettelemme kikan. Ennen sijoitus­lausetta pätevä kaava kannattaa muuttaa muotoon, jossa sijoitus­lauseen oikea puoli esiintyy sellaisenaan. Tyypillisesti se esiintyy yhden kerran, mutta muutkin määrät ovat mahdollisia. Sijoituksen kohteena oleva muuttuja ei saa esiintyä muualla kuin näissä oikeissa puolissa. Sijoitus­lauseen jälkeinen tilanne saadaan korvaamalla ne muuttujalla, johon sijoitetaan.

Rivin 4 tapauksessa se tarkoittaa, että AN = xan muutetaan muotoon, jossa n esiintyy vain osakaavoissa muotoa n−1. Töihin! Olen lisännyt kovat sulut osakaavan n−1 ympärille havainnollisuuden vuoksi, mutta oikeasti se ei ole tarpeen jos kaavan sisältö säilyy ehjänä ilmankin. Ehkä huomaat, että a voidaan ottaa tekijäksi, mutta älä vielä tee niin.
AN = .
Kun osakaavan n−1 paikalle laitetaan sijoituksen kohteena oleva muuttuja n, saadaan se minkä toivottavasti sait edellä:
AN = .
tai

Rivin 5 käsittelyä varten muutamme tämän muotoon, jossa x·a on tekijänä ja x ei esiinny muuten:
AN = .
Rivin 5 mukaisesti x·a korvataan x:llä, joten rivin 5 lopussa AN = .
tai

Seuraavaksi tarkastelemme tilannetta rivin 6 alussa. Näimme, että jos mentiin then-haaran kautta, niin invariantti oli välillä pois voimasta mutta astui uudelleen voimaan then-haaran lopussa. Jos then-haara ohitettiin, minkään muuttujan arvo ei muuttunut, joten invariantti pätee koska se päti rivin 2 alussa. Muuttujan n arvosta rivin 6 alussa tiedetään seuraavaa (valitse oikeat):
n > 0
n ≥ 0
n ≥ −1
Jos mentiin then-haaran kautta, niin n on pariton.
Jos mentiin then-haaran kautta, niin n on parillinen.
Jos ei menty then-haaran kautta, niin n on pariton.
Jos ei menty then-haaran kautta, niin n on parillinen.
n on pariton.
n on parillinen.
tai

Rivin 6 käsittelemiseksi muunnamme rivin 6 alun tilanteen sellaiseksi, että n esiintyy siinä vain muodossa n/2. Voimme käsitellä rivin 6 ikään kuin lattiafunktio ⌊…⌋ ei olisi siinä mukana, koska edellä olevan perusteella sillä ei ole vaikutusta.
AN =
tai

Edellä olevan perusteella tilanne on seuraava rivin 7 alussa:
AN = = .
Rivin 7 lopussa AN = .
tai

Olemme todistaneet, että jos invariantti on voimassa silmukan vartalon alussa, se on voimassa myös silmukan vartalon lopussa. Sitä ennen todistimme, että invariantti on voimassa kun riville 2 tullaan ensimmäisen kerran. Näistä seuraa, että invariantti on voimassa joka kerran kun tullaan riville 2.

Kun algoritmi on lopettanut, n = , joten xan = (ilmaise pienten kirjainten avulla). Toisaalta invariantin vuoksi xan = (ilmaise suurten kirjainten avulla). Siksi algoritmin tuottama vastaus on oikein.
tai

Lopuksi kerro, kuinka monta kierrosta algoritmi suorittaa. Jotta sinun ei tarvitsisi miettiä ja kirjoittaa hieman hankalaa tarkkaa kaavaa, MathCheck tarkastaa vain positiivisilla n:n arvoilla ja hyväksyy kaiken mikä poikkeaa vähemmän kuin 1 tarkasta arvosta.
tai

Ai haluat yrittää tarkkaakin kaavaa? Ei olisi tarpeen, mutta totta kai se sopii, jos intoa riittää!
tai

Ai haluat vain nähdä tarkan kaavan ja sen selityksen? Sekin sopii.
tai