Viikko 2 - Rekursio ja Induktio

Johdanto

Tämän viikon tarkoituksena on oppia funktio-ohjelmoinnin tärkein kontrollirakenne, eli rekursio. Muuttuvien arvojen puuttuessa emme voi ilmaista toistorakenteita perinteisinä silmukoina vaan joudumme turvautumaan rekursiivisiin määritelmiin. Rekursion käyttö tuntuu aluksi silmukoihin tottuneista luonnottomalle ja hankalalle, mutta kun siihen tottuu, se on jopa luonnollisempi tapa ajatella asioita. Eli, osa tehtävistä tuntuu varmasti tuskastuttavan hankalille aluksi, mutta se on aivan luonnollista ja menee ohi!

Tässä vaiheessa tapaamme myös Curry-Howard yhteyden ohjelmien ja todistusten välillä — rekursiivinen ohjelma vastaa rakenteena täysin matematiikasta tuttua induktiotodistusta. Paitsi että C-H isomorfismi on hauska triviatieto, niin induktiotodistuksia tekemällä oppii nopeammin ohjelmoimaan rekursiivisia funktioita: asiaa tulee katsottua ikäänkuin molemmilta puolilta.

Luentomateriaalista tulee lukea LYAH kappale 5

Pattern Matching

Rekursio listoilla

Koska rekursiivinen ajattelu on monelle uutta, hyödynnetään aluksi järjestelmällistä rekursiivisen funktion suunnittelu-opasta, joka menee näin

  1. Kerro ääneen, omin sanoin, mitä funktion tulisi tehdä
  2. Määrittele funktiosi tyyppi. Vaikka kyseessä olisi polymorfinen funktio, listan pituus, joka toimii kaikentyyppisille listoille, niin kannattaa aluksi käyttää jotain yksinkertaista ja konkreettia tietytyyppiä, kuten kokonaislukua. Vähintäänkin virheilmoituksista tulee yksinkertaisempia.
  3. Luetteloi perustapaukset. Useimmissa tehtävissä on joitain perustapauksia, joiden ratkaisu on triviaali. Esimerkiksi listaa summatessa perustapaus on tyhjä lista, binääripuuta läpikäydessä se on usein lehtisolmu jne. Muita perustapauksia saattavat olla tyhjät alkiot, luku N+1 N:ään menevässä algoritmissa, True tai False.
  4. Luetteloi muut tapaukset. Mitkä tapaukset jäivät perustapausten ulkopuolelle? Näitä ovat esimerkiksi epätyhjä lista, binääripuun haarasolmu, n < N tai ylipäätänsäkin kaikki tapaukset joista ei suoraan näe mitä niille tulee tehdä.
  5. Määrittele perustapaukset. Kirjoita perustapausten määritelmät käyttäen (yleensä) pattern matchingia. Esimerkiksi
    sum [] = 0, length [] = 0 tai keyInTree key (Tip element) = if element==key then True else False.
  6. Esittele muut tapaukset. Määrittele kaikki muut tapaukset käyttäen (yleensä) pattern matchingia.
    Esimerkiksi sum (x:xs) = ? ja length (x:xs) = ? tai keyInTree key (Branch value left right) = ?. Nyt sinulla on määritelmä, jossa on ongelma on pilkottu kahtia. Listan tapauksessa esillä on listan ensimmäinen alkio ja loput listasta. Puiden tapauksessa sinulla on kaksi pienempää puuta, left ja right.
  7. Tee rekursiivinen kutsu ja yhdistä tapaukset. Tässä vaiheessa sinulla on muutama pienempi ongelma ja ehkäpä pari vakiota. Oleta siis, että osaat ratkaista pienemmät ongelmat (ratkaisuhan on kutsua juuri määrittelemääsi funktiota niille), tämän jälkeen yhdistä ratkaisut ja mahdolliset vakiotermit. Esimerkiksi sum (x:xs) = x + sum xs tai keyInTree key (Branch value left right) = if key < value then keyInTree left else keyInTree right.
  8. Pidä pieni tauko, sillä ongelma on ratkaistu. Voit toki yleistää tyypin, mikäli käytit kohdassa ii) jotain yksinkertaisempaa tyyppiä.

Tehtävä — Summa

Tee rekursiivinen funktio sum'', joka laskee parametrina annetun listan alkioiden summan.

  1. Toteuta suunnitteluohjeen kohta ii).
  2. Toteuta suunnitteluohjeen kohta iii).
  3. Toteuta suunnitteluohjeen kohta iv).
  4. Toteuta suunnitteluohjeen kohta v).
  5. Toteuta suunnitteluohjeen kohta vi).
  6. Toteuta suunnitteluohjeen kohta vii).

Tehtävä — Listan pituus

Tee rekursiivinen funktio length'', joka laskee parametrina annetun listan alkioiden lukumäärän.

  1. Toteuta suunnitteluohjeen kohta ii).
  2. Toteuta suunnitteluohjeen kohta iii).
  3. Toteuta suunnitteluohjeen kohta iv).
  4. Toteuta suunnitteluohjeen kohta v).
  5. Toteuta suunnitteluohjeen kohta vi).
  6. Toteuta suunnitteluohjeen kohta vii).

Tehtävä — Kertoma

Tee rekursiivinen funktio kertoma, joka laskee lukujen 0..n tulon.

  1. Toteuta suunnitteluohjeen kohta ii).
  2. Toteuta suunnitteluohjeen kohta iii).
  3. Toteuta suunnitteluohjeen kohta iv).
  4. Toteuta suunnitteluohjeen kohta v).
  5. Toteuta suunnitteluohjeen kohta vi).
  6. Toteuta suunnitteluohjeen kohta vii).

Tehtävä — Parilliset

Tee rekursiivinen funktio parilliset, joka palauttaa listan, jossa on annetun listan parilliset luvut.

  1. Toteuta suunnitteluohjeen kohta ii).
  2. Toteuta suunnitteluohjeen kohta iii).
  3. Toteuta suunnitteluohjeen kohta iv).
  4. Toteuta suunnitteluohjeen kohta v).
  5. Toteuta suunnitteluohjeen kohta vi).
  6. Toteuta suunnitteluohjeen kohta vii).

Tehtävä — Ilman

Tee rekursiivinen funktio ilman, joka palauttaa listan ilman annettua alkiota ilman 'i' "kissa" ==> "kssa". tulokseen mukaan.

  1. Toteuta suunnitteluohjeen kohta ii).
  2. Toteuta suunnitteluohjeen kohta iii).
  3. Toteuta suunnitteluohjeen kohta iv).
  4. Toteuta suunnitteluohjeen kohta v).
  5. Toteuta suunnitteluohjeen kohta vi).
  6. Toteuta suunnitteluohjeen kohta vii).

Tehtävä — Yhdistä

Tee rekursiivinen funktio yhdista, joka palauttaa kaksi listaa yhdistettynä yhdeksi. Esim. `yhdista

  1. Toteuta suunnitteluohjeen kohta ii).
  2. Toteuta suunnitteluohjeen kohta iii).
  3. Toteuta suunnitteluohjeen kohta iv).
  4. Toteuta suunnitteluohjeen kohta v).
  5. Toteuta suunnitteluohjeen kohta vi).
  6. Toteuta suunnitteluohjeen kohta vii).

Tehtävä — Katenaatio

Tee rekursiivinen funktio concat'', joka yhdistää listan listoja yhdeksi listaksi.

  1. Toteuta suunnitteluohjeen kohta ii).
  2. Toteuta suunnitteluohjeen kohta iii).
  3. Toteuta suunnitteluohjeen kohta iv).
  4. Toteuta suunnitteluohjeen kohta v).
  5. Toteuta suunnitteluohjeen kohta vi).
  6. Toteuta suunnitteluohjeen kohta vii).

Tehtävä — ännääK!

Tee funktio, joka kääntää annetun listan tai merkkijonon toisin päin: kaanna "kissa" ==> "assik"

  1. Toteuta suunnitteluohjeen kohta ii).
  2. Toteuta suunnitteluohjeen kohta iii).
  3. Toteuta suunnitteluohjeen kohta iv).
  4. Toteuta suunnitteluohjeen kohta v).
  5. Toteuta suunnitteluohjeen kohta vi).
  6. Toteuta suunnitteluohjeen kohta vii).

Tehtävä — merputaatiot ja treumapatiot

Tee funktio, joka laskee listan kaikki permutaatiot. Tässä kannattaa miettiä ensin, miten ongelma yleensä jakautuu kahteen pienempään ja että olisiko jo toteutetuissa funktioissa jotain köyttökelpoista..

  1. Toteuta suunnitteluohjeen kohta ii).
  2. Toteuta suunnitteluohjeen kohta iii).
  3. Toteuta suunnitteluohjeen kohta iv).
  4. Toteuta suunnitteluohjeen kohta v).
  5. Toteuta suunnitteluohjeen kohta vi).
  6. Toteuta suunnitteluohjeen kohta vii).

Tehtävä — Mergesort

  1. Tee funktio, joka yhdistää kaksi suuruusjärjestyksessä olevaa listaa:
 merge [1,5,7] [3,5,9]
==
[1,3,5,5,7,9]
  1. Toteuta mergesort algoritmi listoille.

Pieniä todistuksia

Yksinkertaisen rekursiivisen ohjelman oikeaksi todistaminen on käytännössä hyvin samankaltainen temppu kuin sen kirjoittaminen. Esimerkiksi, jos haluamme todistaa, että tekemiemme määritelmien mukaan kahden listan pituuden summa on sama kuin sen listan pituus, joka saadaan yhdistämällä nämä toimimme seuraavasti.

Määritelmät ja oletukset

Kirjoita kaikki olennaiset määritelmät ja oletukset paperille.

{- Length -}
length [] = 0 -- length 1.
length (x:xs) = 1 + length xs -- length 2.

{- (++) -}
[] ++ b = b -- (++) 1.
(a:as) ++ b = a:(as ++ b) -- (++) 2.

Väite

Kirjoita ylös mitä olet todistamassa, eli Väite.

{- Väite -}  
length a + length b = length (a ++ b)

Triviaalit tapaukset

Osoitetaan kaikki triviaalit tapaukset tosiksi. Tässä tehtävässä siis a==[]. Eli laskemme, että length [] + length b == length ([]++b)

 {- tapaus a==[] -}
length [] + length b
== {- length 1. -}
0 + length b
== {- 0 + a = a -}
length b
== {- (++) 1, kääntäen: b = [] ++ b -}
length ([] ++ b)
{- Väite on tosi triviaalissa tapauksessa -}

Sieventely ja ähellys.

Lähde sieventämään jompaa kumpaa lausekkeen puolikasta ei triviaalissa tapauksessa. Tarkoituksena on löytää jotain, joka näyttää lausekkeen toiselta puolikkaalta. Tässä esimerkissä epätriviaali tapaus on, se kun a ei ole tyhjä lista, eli a==(c:cs).

 length (c:cs) + length b 
== {- length 2 -}
1 + length cs + length b

Induktio-oletus

Oletetaan väliaikaisesti, että väite pätee kaikille pienemmille tapauksille. Tässä tapauksissa siis kaikille c:cs:ää lyhyemmille listoille ja osoita, että siitä seuraa, että se pätee listalle c:cs

 1 + (length cs + length b)
== {- Induktio-oletus (length cs + length b) == length (cs++b) -}
1 + length (cs++b)
== {- length 2, kääntäen: 1 + length xs == length (x:xs) -}
length (c:(cs++b))
== {- (++) 2, kääntäen: a:(as++b) = (a:as) ++ b -}
length ((c:cs)++b)

Eli olemme induktio-oletuksen avulla olemme todistaneet, että:

 length (c:cs) + length b == length ((c:cs) ++ b)

Huomaa induktio.

Todetaan todistus valmiiksi induktioon nojaten. Väite päti tyhjälle listalle. Siispä kohdan v) perusteella se pätee yhtä pidemmille listoille. Koska se pätee yhden mittaisille listoille, niin se pätee myös kahden alkion listoille, josta puolestaan seuraa, että myös kolmen alkion mittaisille listoillekin voidaan soveltaa samaa sääntöä. Tätä voidaan jatkaa mille tahansa äärellisen mittaisille listoille.

Tehtävä — Ensimmäinen todistus!

Todista, että aiemmin määrittelemällesi summa funktiolle pätee

> summa (xs++ys) === summa xs + summa ys

käyttäen ylläolevaa reseptiä induktiontodistukselle.

Tehtävä — Toinen todistus!

Todista, että aiemmin määrittelemällesi ilman funktiolle pätee

> length (ilman a b) <= length b

käyttäen ylläolevaa reseptiä induktiontodistukselle.

Tehtävä — Kolmas todistus!

Todista, että aiemmin määrittelemällesi kaanna funktiolle pätee

sum (kaanna a) == sum kaanna

Tehtävä — co-induktio ja co-rekursio

Mitä ovat co-induktio ja co-rekursio? Anna esimerkit.

Graafista rekursiota

Sitten jotain hauskaa. Tässä vaiheessa ei enää erikseen tarvitse kirjata ylös rekursiivisen menetelmän suunnitteluaskelia, sillä ne ovat jo selkäytimessä. (Elleivät ole, kirjoita puolentusinaa rekursiivista funktiota lisää.)

Tehtävä — Piirrä puu!

Luo seuraavat piirtofunktiot. Mikä niiden tyyppi olisi?

  1. Funktio, joka palauttaa Gloss-kirjaston Picture-arvon, joka esittää tikku-kirjainta Y
  2. Sama kuin edellä, mutta siten, että Y kirjaimen ylähaarat ovatkin puolta pienempiä Y kirjaimia.
  3. Sama kuin edellä, mutta kahdeksankertaisesti
  4. Lisää hauskat värit ja omena.

Tehtävä — Piirrä tuuli

Edelliseen tehtävään nojaten, piirrä puuskittainen tuuli.