Arvutusjärjekord
Meil on kaks standardset lambda-arvutuse reduktsioonijärjekorda:
- normaaljärjekord (~ Haskell, Idrise REPL )
- aplikatiivjärjekord (~ kompileeritud Idris (:exec))
Tekib küsimus, kumb on parem/õigem? Kumba kasutada?
Teoorias normaaljärjekord töötab paremini:
- normaaljärjekord alati leiab normaalkuju, kui see eksisteerib,
- aplikatiivjärjekord alati ei leia (aga kui leiab siis sama mis normaaljärjekord).
Normaaljärjekord ei väärtusta funktsiooni argumente, mida funktsioon ei kasuta. Seetõttu, kui funktsiooni argumendil pole normaalkuju siis võib funktsiooni kutse normaalkuju leida vaid normaaljärjekorra abil.
Seetõttu on normaaljärjekorras arvutades võimalik kasutada väga üldiseid definitsioone. Näiteks saame Haskellis defineerida kõikide algarvude listi:
sieve (p:xs) = [x | x<-xs, x `mod` p /= 0] primes = map head (iterate sieve [2..])
Normaaljärjekorras arvutades saame leida iga listit primes mingi alguse.
Esimese tuhande algarvu leidmine on Haskellis üpriski kiire:
Main> take 1000 primes [2,3,5,7,11,13,17,19, ...
Sellise kiiruse saavutamiseks pole puhas normaaljärjekord piisav -- vaja on graafireduktsiooni, ehk laiska väärtustamist.
Laisk väärtustamine
Normaaljärjekord võib osutuda aeglaseks, kui funktsiooni keha sisaldab parameetrit samas harus mitu korda. Näiteks topelt x = x+x. Normaaljärjekord väärtustab funktsiooni argumenti mitu korda, kuid aplikatiivjärjekord vaid üks kord.
Tore oleks, kui saaksime normaal- ja aplikatiivjärjekorra head omadused ühendada.
Vaatame järgnevat näided, kus meil on selline funktsiooni f definitsioon
f x y = (x+x)+3
ja soovime väärtustada avaldist
f (2+2) (3+3+3)
Aplikatiivjärjekord väärtustab selle kuue sammuga, kus kaks sammu läheb teise parameetri väärtustamiseks, mida lõpuks vaja ei lähe:
f (2+2) (3+3+3) => f 4 (3+3+3) => f 4 (6+3) => f 4 9 => (4+4)+3 => 8+3 => 11
Normaaljärjekord väärtustab selle viie sammuga, kus esimest parameetrit väärtustatakse sisuliselt kaks korda:
f (2+2) (3+3+3) => ((2+2)+(2+2))+3 => (4+(2+2))+3 => (4+4)+3 => 8+3 => 11
Normaaljärjekorras graafireduktsiooni ehk laisa väärtustamise puhul on süntaksipuu asemel tsükliteta graaf, s.t., saame viidata mitu korda samale alamavaldisele.
Laisk väärtustamine toimub nelja sammuga -- ei väärtusta kasutamata parameetrit ja esimest parameetrit arvutatakse ühe korra:
f (2+2) (3+3) => (x+x)+3 where x = 2+2 => (x+x)+3 where x = 4 => 8+3 => 11
Graafireduktsiooni leiutamine 70ndatel, põhjustas laiskade keelte (sh Haskelli) vaimustuse 80ndate lõpus ja 90ndatel.
Kahjuks, kõiki seoseid ei graafireduktsioon automaatselt ei leia. Veel hullem -- laisa väärtustuse optimeerimine käsitsi märgendamise abil on väga raske ja aeganõudev. Enamasti peetakse lihtsamaks agarale väärtustusele laiskuse lisamise.
Agar väärtustamine + Lazy tüübid
Idris on otsustanud vaikimisi agara väärtustamise kasuks, kus laiska arvutust kasutatakse Lazy a tüüpi väärtuste puhul. S.t. Int tüüpi muutujas on päriselt täisarv aga Lazy Int sees võib olla nii täisarv kui ka avaldis/kood, mis selle arvutab.
Lihtsustatult, on Lazy selline andmestruktuur:
data Lazy : Type -> Type where
Delay : (val : a) -> Lazy a -- delay
... ja lisaks funktsioon
Force : Lazy a -> a
Idris oskab ise tüübi järgi panna Delay & Force, et teisendasa A -> Lazy A ja Lazy A -> A.
Eelmine "lihtsustatult", on seepärast, et tegelikult on kaks sellist tüüpi:
Lazy-- laisk aga lõplik ja termineeruv arvutusInf-- laisk lõpmatu arvutus, mille täielikkust mõne teise konstruktori all ei kontrollita
Selgitav näide:
-- lõpmatu tsükkel
inf : () -> Nat
inf () = inf ()
--total -- ei ole täielik, termineeruvuse kontroll avastab probleemi
test2 : Maybe (Lazy Nat)
test2 = Just (inf())
total -- on täielik konstruktori all, (peame olema ettevaatlikud)
test3 : Maybe (Inf Nat)
test3 = Just (inf())
total -- see on rumalus -- tegelikult ei termineeru
test4 : Nat
test4 = case test3 of Just n => n
Nothing => 0
Stream-id ehk lõpmatud (laisad) listid
Lõpmatuid liste kutsutakse striimideks. Nende jaoks on vaja laiskust.
data Stream : Type -> Type where
(::) : a -> Inf (Stream a) -> Stream a
ones : Stream Nat ones = 1 :: ones fib : Integer -> Integer fib 0 = 1 fib 1 = 1 fib n = fib (n-1) + fib (n-2) fibs : Stream Integer fibs = 1 :: 1 :: zipWith (+) fibs (tail fibs) infixl 9 !! (!!) : Stream a -> Nat -> a (x :: y) !! 0 = x (x :: y) !! (S k) = y !! k
NB! Idrises pole (veel?) graafireduktsiooni.
S.t. fibs on väga aeglane.