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
Koska rekursiivinen ajattelu on monelle uutta, hyödynnetään aluksi järjestelmällistä rekursiivisen funktion suunnittelu-opasta, joka menee näin
sum [] = 0, length [] = 0 tai keyInTree key (Tip element) = if element==key then True else False.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.sum (x:xs) = x + sum xs tai keyInTree key (Branch value left right) = if key < value then keyInTree left else keyInTree right.Tee rekursiivinen funktio sum'', joka laskee parametrina annetun listan alkioiden summan.
Tee rekursiivinen funktio length'', joka laskee parametrina annetun listan alkioiden lukumäärän.
Tee rekursiivinen funktio kertoma, joka laskee lukujen 0..n tulon.
Tee rekursiivinen funktio parilliset, joka palauttaa listan, jossa on annetun listan parilliset luvut.
Tee rekursiivinen funktio ilman, joka palauttaa listan ilman annettua alkiota ilman 'i' "kissa" ==> "kssa". tulokseen mukaan.
Tee rekursiivinen funktio yhdista, joka palauttaa kaksi listaa yhdistettynä yhdeksi. Esim. `yhdista
Tee rekursiivinen funktio concat'', joka yhdistää listan listoja yhdeksi listaksi.
Tee funktio, joka kääntää annetun listan tai merkkijonon toisin päin: kaanna "kissa" ==> "assik"
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..
merge [1,5,7] [3,5,9]
==
[1,3,5,5,7,9]
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.
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.
Kirjoita ylös mitä olet todistamassa, eli Väite.
{- Väite -}
length a + length b = length (a ++ b)
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 -}
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
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)
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.
Todista, että aiemmin määrittelemällesi summa funktiolle pätee
> summa (xs++ys) === summa xs + summa ys
käyttäen ylläolevaa reseptiä induktiontodistukselle.
Todista, että aiemmin määrittelemällesi ilman funktiolle pätee
> length (ilman a b) <= length b
käyttäen ylläolevaa reseptiä induktiontodistukselle.
Todista, että aiemmin määrittelemällesi kaanna funktiolle pätee
sum (kaanna a) == sum kaanna
Mitä ovat co-induktio ja co-rekursio? Anna esimerkit.
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ää.)
Luo seuraavat piirtofunktiot. Mikä niiden tyyppi olisi?
Picture-arvon, joka esittää tikku-kirjainta YEdelliseen tehtävään nojaten, piirrä puuskittainen tuuli.