06 - rekurzív függvények helyességigazolása

Folytassuk a tail callos összegző függvényünk vizsgálatát:

1
2
def tailSum(n: Int, s: Int): Int = 
  if( n <= 0 ) s else tailSum(n-1, s+n)

Erről azt állítottuk, hogy 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, mint 0, vagyis ha n>0-val hívjuk, akkor visszakapjuk tailSum(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.

Utolsó frissítés: 2020-12-22 21:04:26