06 - rekurzív függvények helyességigazolása¶
Folytassuk a tail callos összegző függvényünk vizsgálatát:
1 2 |
|
tailSum(n,s) = s + 1 + 2 + ... + n
lesz minden s,n >= 0
egészek esetén.
Hogy egy ilyet megmutassunk (és ezzel meggyőzzük magunkat tesztesetek nélkül, hogy a kódunk helyes), a következőt lehet pl. csinálni:
- keresünk valami olyan ,,leszállási feltételt'', amit hozzá tudunk rendelni az argumentumokhoz, minden rekurzív hívásnál csökken, és nem csökkenhet végtelen sokáig
- az állítást leellenőrizzük ennek a leszállási feltételnek a ,,legegyszerűbb'' esetére
- eztán a leszállási feltételre vonatkozó indukcióval megmutatjuk, hogy az állítás továbbra is igaz marad.
Ez elég misztikusan hangozhat, bár progalapon is szokott lenni ilyesmi. Most maga az n
paraméter jó
lesz leszállási feltételnek, hiszen a rekurzív hívásban az első argumentumot mindig csökkentjük eggyel,
és 0
alá nem fog menni, ha eredetileg nemnegatív volt (az állítás pedig n >= 0
-ról beszél, tehát
eredetileg nemnegatív volt). Ezzel akkor az első pont letudva, van leszállási feltételünk.
(Abból, hogy van leszállási feltételünk, egyébként az is következik mindig, hogy a kód nem eshet végtelen rekurzióba.)
Eztán leellenőrizzük a legegyszerűbb esetre az állítást: mivel n
a leszállási feltételünk,
ez azt jelenti, hogy n=0
-ra kell ellenőriznünk. Ha pedig megnézzük a tailSum(0,s)
alakú
hívásokat, azok az if( n<=0 ) s
rész miatt s
-re fognak kiértékelődni, ami ugyanannyi, mint
s + 1 + 2 + ... + n
, ha n=0
, tehát ez a rész is pipa.
Eztán pedig következik az indukció, ami szintén nem olyan nagy ördöngösség:
- ha
tailSum(n,s)
-t értékeljük ki egy ,,bonyolultabb'', avagy ,,nagyobb értékű'' leszállási feltételre, mint0
, vagyis han>0
-val hívjuk, akkor visszakapjuktailSum(n-1,s+n)
-t. - ennek indukció szerint az értéke
(s+n) + 1 + 2 + ... + (n-1)
lesz (második argumentum, plusz az első argumentumig a pozitív egészek összege) - amit átrendezve tényleg az
s + 1 + 2 + ... + n
-t kapjuk, tehát a függvény tényleg azt számolja, amit szeretnénk.
Kérdések, feladatok¶
- Vajon miért fontos, hogy ne legyen végtelen csökkenésre lehetőség egy leszállási feltételnél? Tudsz erre készíteni egy példát? Mi történhet ilyenkor?
- Írd meg a faktoriális függvényt is tail rekurzívan, és igazold a kódod helyességét.