Učinki in čistost

Računalniške funkcije so podobne matematičnim v tem, da iz vhodnih vrednosti izračunajo izhodno, vendar se tu podobnost neha. Računalniške funkcije dajo lahko ob enakih vhodih tudi različne izhodne vrednosti, poleg izračuna vrednosti pa včasih še kaj izpišejo na zaslon, preberejo s tipkovnice, sprožijo izjeme, spreminjajo datoteke, pošiljajo podatke in podobno. Vsem odklonom od čistih matematični vrednosti pravimo stranski ali računski učinki.

Učinki v OCamlu

Poglejmo si nekaj primerov takih funkcij v OCamlu. Prva (in zelo pogosto uporabljana) je print_endline, ki sprejme niz ter ga izpiše na zaslon in vrne prazen nabor. V splošnem nam prisotnost tipa unit v OCamlu sporoča, da se bodo sprožili stranski učinki, saj sicer funkcija, ki bi vrnila unit, ne bi storila ničesar koristnega.

print_endline
- : string -> unit = <fun>
print_endline "Hello, world!"
- : unit = ()

Pri klicu funkcij z učinki je včasih uporabna tudi funkcija List.iter, ki dano funkcijo pokliče na vseh elementih seznama. Podobna je funkciji List.map, le da seznam vrnjenih praznih naborov zavrže, saj ga redkokdaj uporabljamo.

List.map print_endline ["am"; "bam"; "pet"; "podgan"]
am
bam
pet
podgan
- : unit list = [(); (); (); ()]
List.iter print_endline ["am"; "bam"; "pet"; "podgan"]
am
bam
pet
podgan
- : unit = ()

Za delo z psevdonaključnimi vrednostmi je na voljo knjižnica Random. Pogosto uporabljani funkciji tam sta Random.bool, ki ob vsakem klicu vrne naključno logično vrednost, in Random.int, ki za neko število \(m\) vrne naključno celo število med 0 in \(m - 1\). Pri uporabi psevdonaključnih števil moramo paziti, da na začetku nastavimo ustrezno seme, saj sicer OCaml vedno začne z enakim. Na primer, spodnji klic bo ob prvem klicu vedno vrnil število 9344.

Random.int 100000
- : int = 9344

Seme lahko najbolj enostavno nastavimo z Random.self_init, ki ga nastavi glede na trenuten čas, stanje procesov, …, skratka dovolj naključno.

Random.self_init ()
- : unit = ()
Random.int 100000 (* tu je nemogoče napovedati, kaj bo klic vrnil *)
- : int = 32774

Za branje s konzole uporabimo funkcijo read_line.

read_line
- : unit -> string = <fun>

Tudi tu nam prisotnost tipa unit nakazuje, da se bodo najverjetneje zgodili učinki, saj bi funkcija samo iz praznega nabora težko izračunala kakšno zanimivo vrednost. Žal v učbeniku te funkcije ne moremo smiselno poklicati.

raise
- : exn -> 'a = <fun>

Čiste funkcije

Nasprotje funkcij, ki sprožajo učinke, so čiste funkcije. Kljub temu, da z njimi lahko postorimo manj, imajo prednost, da o njih lažje razmišljamo, saj:

  1. jih vedno lahko zamenjamo z njihovimi definicijami

  2. ob enakih argumentih vedno vrnejo enake rezultate

S funkcijami, ki sprožajo učinke, to ni nujno res. Na primer, če v Pythonu definiramo:

seznam = [1, 2, 3]
def f(x):
    seznam.append(x)
    return len(seznam)
def g(x):
    return f(x) + f(x)

bomo ob klicu g(3) dobili

>>> g(3)
9

če to zamenjamo z definicijo f(3) + f(3), dobimo:

>>> f(3) + f(3)
13

in če še enkrat pokličemo g(3), dobimo:

>>> g(3)
17

Ker funkcija f ob klicu spreminja seznam, bomo vsakič dobili drugačen odgovor. O tem, kaj vračata funkciji f in g tako zelo težko sklepamo. Če pa imamo čiste funkcije (na primer spodnjo, ki ne spreminja obstoječega seznama, temveč vrača novega), potem ob vsakem klicu dobimo enak odgovor.

let seznam = [1; 2; 3]
let f x =
    let seznam = x :: seznam in
    List.length seznam
let g x =
    f x + f x
val seznam : int list = [1; 2; 3]
val f : int -> int = <fun>
val g : int -> int = <fun>
g 3
- : int = 8
f 3 + f 3
- : int = 8
g 3
- : int = 8

Zaradi tega je v splošnem dobro, da v naših programih napišemo čimveč čistih funkcij, funkcije z učinki pa omejimo kolikor se da. Tako bodo naši programi jasnejši in z manj napakami. Poleg tega pa si lahko ob čistih funkcijah privoščimo čisto prave matematične dokaze. Da bomo imeli kaj, s čimer bomo lahko delali, si definirajmo sledeče tri funkcije:

let rec (@) xs ys =
  match xs with
  | [] -> ys
  | x :: xs' -> x :: (xs' @ ys)
val ( @ ) : 'a list -> 'a list -> 'a list = <fun>
let rec obrni = function
  | [] -> []
  | x :: xs -> obrni xs @ [x]
val obrni : 'a list -> 'a list = <fun>
let rec dolzina = function
  | [] -> 0
  | _ :: xs -> 1 + dolzina xs
val dolzina : 'a list -> int = <fun>

Iz definicij takoj sledijo enačbe

  1. [] @ ys = ys

  2. (x :: xs) @ ys = x :: (xs @ ys)

  3. obrni [] = []

  4. obrni (x :: xs) = obrni xs @ [x]

  5. dolzina [] = 0

  6. dolzina (x :: xs) = 1 + dolzina xs

Iz teh enačb na primer takoj sledi trditev obrni [x] = [x].

obrni [x]
= obrni (x :: [])
    (ker je `[x]` okrajšava za `x :: []`)
= [] @ [x]
    (po (3))
= [x]
    (po (1))

Indukcija na seznamih

Trditev: dolzina (xs @ ys) = dolzina xs + dolzina ys

Tukaj enostavno odvijanje definicij ne bo pomagalo, saj izraz dolzina (xs @ ys) ne ustreza ne levi ne desni strani nobene od zgoraj naštetih definicij. Namesto tega uporabimo načelo indukcije za sezname:

P([]) ∧ (∀ z, zs. P(zs) ⇒ P(z :: zs)) ⟹ ∀ ws. P(ws)

Torej, lastnost P velja za vse sezname ws, kadar (1) velja za prazen seznam [] in (2) velja za sestavljen seznam z :: zs ob predpostavki, da velja za rep zs. Načelo indukcije je podobno načelu indukcije za naravna števila:

P(0) ∧ (∀ m. P(m) ⇒ P(m⁺)) ⟹ ∀ n. P(n)

Torej, lastnost P velja za vsa naravna števila n, kadar (1) velja za 0 in (2) velja za naslednika m⁺ ob predpostavki, da velja za m. Izjavo dokažemo z indukcijo na levi seznam. Indukcija poteka v dveh korakih:

Osnovni korak

V osnovnem koraku pokažemo, da enakost velja, kadar je levi seznam prazen, torej oblike []:

dolzina ([] @ ys)
= dolzina ys
    (po (1))
= 0 + dolzina ys
    (po Peanovih aksiomih)
= dolzina [] + dolzina ys
    (po (5))

Indukcijski korak

V indukcijskem koraku pokažemo, da enakost velja za sestavljeni seznam x :: xs ob predpostavki, da enakost velja za seznam xs:

dolzina ((x :: xs) @ ys)
= dolzina (x :: (xs @ ys))
    (po (2))
= 1 + dolzina (xs @ ys)
    (po (6))
= 1 + (dolzina xs + dolzina ys)
    (po indukcijski prepostavki)
= (1 + dolzina xs) + dolzina ys)
    (po Peanovih aksiomih)
= dolzina (x :: xs) + dolzina ys
    (po (6))

Pravilnost načela indukcije na seznamih

Zakaj sploh smemo uporabiti načelo indukcije? Recimo, da velja

P([]) ∧ (∀ z, zs. P(zs) ⇒ P(z :: zs))

Zakaj potem velja P(ws) za poljuben seznam ws? Vzemimo nek konkreten seznam, na primer [1; 2; 3], in pokažimo, da velja P([1; 2; 3]). Res, po prvem delu predpostavke velja P([]). Zato po drugem delu predpostavke velja P([3]), saj velja P([]) in je [3] = 3 :: []. Podobno potem iz P([3]) sledi P([2; 3]) in na koncu tudi P([1; 2; 3]). Tak dokaz bi lahko ponovili za vsak konkreten seznam.

V splošnem pa se naslonimo na načelo indukcije za naravna števila. Definirajmo:

Q(n) :=  ∀ ws. |ws| = n ⇒ P(ws)

Torej, Q(n) velja, če velja P(ws) za vse sezname ws dolžine n. Iz Peanovih aksiomov potem sledi:

Q(0) ∧ (∀m. Q(m) ⇒ Q(m+)) ⟹ ∀n. Q(n)

Pokažimo, da velja Q(0) in ∀m. Q(m) Q(m+). Ker velja P([]) in je [] edini seznam dolžine 0, velja tudi Q(0). Vzemimo poljuben m in predpostavimo Q(m). Torej za poljuben seznam zs dolžine m velja P(zs). Iz predpostavke potem sledi, da velja tudi P(z :: zs). Ker so vsi seznami dolžine m⁺ take oblike, smo pokazali Q(m⁺). Po indukciji na naravnih številih torej sledi ∀n. Q(n). Ker je vsak seznam ws končen, ima za dolžino neko naravno število, zato velja P(ws) za vse sezname ws.

Trditev: xs @ [] = xs

Po (1) vemo, da je [] @ xs = xs, torej je [] leva enota za @. To, da je [] tudi desna enota, pa ni samoumevno — za dokaz uporabimo indukcijo.

Osnovni korak

Po (1) velja [] @ [] = [], kar dokaže osnovni korak.

Indukcijski korak

Prepostavimo, da velja xs @ [] = xs. Tedaj velja

(x :: xs) @ []
= x :: (xs @ [])
    (po (2))
= x :: xs
    (po indukcijski prepostavki)

kar zaključi tudi indukcijski korak.

Trditev xs @ (ys @ zs) = (xs @ ys) @ zs

Operacija stikanja seznamov @ je tudi asociativna, kar dokažemo z indukcijo na xs. Če zapišete dokaz asociativnosti seštevanja, lahko vidite, da poteka podobno, le da se namesto [] pojavlja 0, namesto x :: xs pa naslednik n⁺.

Osnovni korak

[] @ (ys @ zs)
= ys @ zs
    (po (1))
= ([] @ ys) @ zs
    (po (1))

Indukcijski korak

Prepostavimo, da velja xs @ (ys @ zs) = (xs @ ys) @ zs. Tedaj velja

(x :: xs) @ (ys @ zs)
= x :: (xs @ (ys @ zs))
    (po (2))
= x :: ((xs @ ys) @ zs)
    (po indukcijski predpostavki)
= (x :: (xs @ ys)) @ zs
    (po (2))
= ((x :: xs) @ ys) @ zs
    (po (2))

Trditev obrni (xs @ ys) = obrni ys @ obrni xs

Osnovni korak

obrni ([] @ ys)
= obrni ys
    (po (1))
= obrni ys @ []
    (po prej dokazani trditvi ∀ xs. xs @ [] = xs)
= obrni ys @ obrni []
    (po (3))

Indukcijski korak

obrni ((x :: xs) @ ys)
= obrni (x :: (xs @ ys))
    (po (2))
= obrni (xs @ ys) @ [x]
    (po (4))
= (obrni ys @ obrni xs) @ [x]
    (po indukcijski predpostavki)
= obrni ys @ (obrni xs @ [x])
    (po prej dokazani trditvi ∀ xs, ys, zs. xs @ (ys @ zs) = (xs @ ys) @ zs)
= obrni ys @ obrni (x :: xs)
    (po (4))

Trditev dolzina (obrni xs) = dolzina xs

Osnovni korak

Iz definicije (3) sledi dolzina (obrni []) = dolzina [],

Indukcijski korak

Za indukcijski korak moramo pokazati, da velja dolzina (obrni (x :: xs)) = dolzina (x :: xs) ob indukcijski predpostavki dolzina (obrni xs) = dolzina xs. Velja:

dolzina (obrni (x :: xs))
= dolzina (obrni xs @ [x])
    (po definiciji (4))
= dolzina (obrni xs) + dolzina [x]
    (po zgornji lemi)
= dolzina xs + dolzina [x]
    (po indukcijski predpostavki)
= dolzina xs + 1
    (po definicijah (5) in (6))
= 1 + dolzina xs
    (zaradi komutativnosti seštevanja)
= dolzina (x :: xs)
    (po definiciji (6))

s čimer zaključimo tudi indukcijski korak.

Indukcija na drevesih

Načela indukcije imamo na voljo tudi na drugih vsotah. Na primer, če definiramo tip dvojiških dreves:

type 'a drevo =
  | Prazno
  | Sest of 'a drevo * 'a * 'a drevo

zanj velja načelo indukcije:

P(Prazno) ∧ (∀ l, x, d. P(l) ∧ P(d) ⇒ P(Sest (l, x, d))) ⟹ ∀ t. P(t)

Torej, lastnost P velja za vsa drevesa t, kadar (1) velja za prazno drevo Prazno in (2) velja za sestavljeno drevo Sest (l, x, d) ob predpostavki, da velja za otroka l in d.

Definirajmo funkciji:

let rec zrcali = function
  | Prazno -> Prazno
  | Sest (l, x, d) -> Sest (zrcali d, x, zrcali l)

let rec globina = function
  | Prazno -> 0
  | Sest (l, _, d) -> 1 + max (globina l) (globina d)

Iz definicij sledijo enačbe

  1. zrcali Prazno = Prazno

  2. zrcali (Sest (l, x, d)) = Sest (zrcali d, x, zrcali l)

  3. globina Prazno = 0

  4. globina (Sest (l, x, d)) = 1 + max (globina l) (globina d)

Trditev globina (zrcali t) = globina t

Osnovni korak

globina (zrcali Prazno)
= globina Prazno
    (po (1))

Indukcijski korak

globina (zrcali (Sest (l, x, d)))
= globina (Sest (zrcali d, x, zrcali l))
    (po (2))
= 1 + max (globina (zrcali d)) (globina (zrcali l))
    (po (4))
= 1 + max (globina d) (globina (zrcali l))
    (po prvi indukcijski predpostavki)
= 1 + max (globina d) (globina l)
    (po drugi indukcijski predpostavki)
= 1 + max (globina l) (globina d)
    (zaradi komutativnosti max)
= globina (Sest (l, x, d))
    (po (4))

Vaje za utrjevanje

Trditev obrni (obrni xs) = xs

Trditev zrcali (zrcali t) = t

Trditev obrni xs = obrni' xs (težja)

Kot vemo, ima funkcija obrni, definirana kot:

let rec obrni = function
  | [] -> []
  | x :: xs -> obrni xs @ [x]

časovno zahtevnost \(O(n^2)\), saj se mora zapeljati čez ves seznam, da mu na konec doda x.

Bolje je, če uporabimo funkcijo obrni', ki uporablja akumulator in je definirana kot:

let obrni' =
  let rec aux acc = function
    | [] -> acc
    | x :: xs -> aux (x :: acc) xs
  in
  aux []

Pokažite, da za vse sezname xs velja obrni xs = obrni' xs.

Indukcija na drugih tipih

Definirajmo tipe

type naravno = Zero | Succ of naravno
type boole = Resnica | Laz
type 'a mogoce = Nic | Nekaj of 'a

Kakšni sta videti načeli indukcije za te tipe?