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 Learn You a Haskellin kappale 5
Koska rekursiivinen ajattelu on monelle uutta, hyödynnetään aluksi järjestelmällistä rekursiivisen funktion suunnittelumenetelmää:
Kerro ääneen, omin sanoin, mitä funktion tulisi tehdä.
Määrittele funktiosi tyyppi. Vaikka kyseessä olisi polymorfinen funktio, joka toimii kaikentyyppisille listoille, niin aluksi voit käyttää jotain konkreettia tietytyyppiä, kuten kokonaislukua. Virheilmoituksista tulee yksinkertaisempia.
Luetteloi perustapaukset. Useimmissa tehtävissä on perustapauksia, joiden ratkaisu on triviaali. Esimerkiksi listan pituutta laskettaessa perustapaus on tyhjä lista ja binääripuuta läpikäydessä se on lehtisolmu Muita perustapauksia saattavat olla esimerkiksi tyhjät alkiot, luku n+1, True tai False.
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ä.
Ohjelmoi 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
.
Esittele muut tapaukset. Esittele 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ääritelmiä, joissa on ongelma on pilkottu useampaan osaan. Listan tapauksessa esillä on listan ensimmäinen alkio ja loput listasta. Puiden tapauksessa sinulla on solmun arvoa ja kaksi pienempää puuta, left
ja right
.
Esimerkiksi summan tapauksessa oletamme, että osaisimme laskea listan xs
summan. Siitä seuraa tietysti, että sum (x:xs) = x + sum xs
. Binääripuun tapauksessa oletamme osaavamme löytää avaimen joko oikeasta tai vasemmasta alipuusta, joten tehtäväksi jää vain valita kummasta se etsitään: keyInTree key (Branch value left right) = if key < value then keyInTree left else keyInTree right
.
Tee rekursiivinen funktio summaa
, joka laskee parametrina annetun listan alkioiden summan.
Tee rekursiivinen funktio parilliset
, joka palauttaa listan, jossa on annetun listan parilliset luvut.
Tee rekursiivinen funktio ilman
, joka palauttaa listan ilman annettua alkiota. Esimerkiksi ilman 'i' "kissa istuu" == "kssa stuu"
.
Tee rekursiivinen funktio (++)
, joka palauttaa kaksi listaa yhdistettynä yhdeksi. Esim. [1,2,3] ++ [4,5,6] == [1,2,3,4,5,6]
. Varuskirjastossa on jo samanniminen funktio, joten keksi uusi nimi, tai kirjoita import Prelude hiding ((++))
ohjelmasi alkuun.
Tee rekursiivinen määritelmä puu
, joka esittää (oikeaa) puuta ja jonka voi piirtää seuraavalla Gloss
-kirjastoa käyttävällä ohjelmalla:
module Main where
import Graphics.Gloss
main = displayInWindow "Puu" (500,500) (20,20) blue puu
Vinkki: Gloss
kirjasto sisältää seuraavat hyödylliset funktiot.
green :: Color
rectangleSolid :: Float -> Float -> Picture
rotate :: Float -> Picture -> Picture
scale :: Float -> Float -> Picture -> Picture
color :: Color -> Picture -> Picture
green :: Color
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. Tässä yhteydessä käytämme lukiosta tuttua [induktiotodistus]ta. Induktiotodistuksen idea on osoittaa, että
ja tehdä niistä johtopäätös
Voimme esimerkiksi todistaa, että aikaisemmissa tehtävissä tekemiemme määritelmien mukaan kahden listan pituuden summa on sama kuin sen listan pituus, joka saadaan yhdistämällä ne yhdeksi listaksi.
Tämä voidaan tehdä hyvin mekaanisesti käymällä seuraavat vaiheet läpi:
Kirjoita kaikki olennaiset määritelmät ja oletukset paperille.
Esimerkki:
{- 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.
Esimerkki:
{- Väite -}
length a + length b = length (a ++ b)
Osoitetaan kaikki triviaalit tapaukset tosiksi.
Esimerkki:
Tässä tehtävässä triviaali tapaus on a==[]
. Siispä 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 -}
Osoitetaan, että jos väite pätee jollekin tapaukselle, se pätee myös ‘seuraavalle’. Tätä voi verrata rekursiivisen ohjelman suunnitteluun, jossa askel otetaan jakamalla tehtävä pienempiin osiin. Induktion kanssa puolestaan otetaan pienemmät osat ja koostetaan niistä suurempi kokonaisuus.
Esimerkki:
Tässä tapauksessa tarkastelemme siis listoja c:cs
ja cs
ja osoitamme, että jos (length cs + length b) == length (cs++b)
pätee, niin length (c:cs) + length b == length ((c:cs) ++ b)
pätee myös.
length (c:cs) + length b
== {- length 2 -}
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, osoitimme, että
length (cs) + length b == length ((cs) ++ b)
=> {- Ks. edellinen todistus -}
length (c:cs) + length b == length ((c:cs) ++ b)
Suomeksi sanottuna siis sen, että jos väite pätee jonkin kokoiselle listalle, se pätee myös yhtä pidemmälle listalle.
Todetaan todistus valmiiksi induktioon nojaten. Väite pätee tyhjälle listalle. Induktio-askeleen mukaan sen täytyy päteä silloin yhden alkion mittaiselle listalle. Edelleen, koska se pätee yhden mittaisille listoille, niin se pätee myös kahden alkion mittaisille listoille. Tätä voidaan jatkaa loputtomiin, joten väite pätee kaikille ää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
summa (kaanna a) == summa a
Mitä yhteistä rekursiolla ja induktiotodistuksilla siis oli?
blog comments powered by Disqus