Arvutiteaduse instituut
  1. Kursused
  2. 2021/22 sügis
  3. Funktsionaalprogrammeerimine (LTAT.03.019)
EN
Logi sisse

Funktsionaalprogrammeerimine 2021/22 sügis

  • Üldinfo
    • Õppekorraldus
  • Loengud ja Praksid
    • Installimine
    • 1. Praktikum
    • 2. Praktikum
    • 3. Praktikum
    • 4. Praktikum
    • 5. Praktikum
    • 6. - 7. Praktikum
    • 9. Praktikum
    • 10. Praktikum
    • 11. Praktikum
    • 12. Praktikum
    • 13. Praktikum
    • Projektid
  • Moodle
  • Fleep

Praktikum 11

Tõestused Idris2-s. NB! Koodi sees on mitmed väikesed ülesanded.

Lausearvutus

data abil loodud andmestruktuuridega saame lisada uusi loogika-reegleid, kus kontruktoriteks on sissetoomise reeglid.

Konjunktsioon

-- ainult täielikud funktsioonid tagavad turvalisuse
%default total  

infixl 10 /\
data (/\) : Type -> Type -> Type where
    ConI : a -> b 
           ------
        -> a /\ b

-- Lisaks võime (aga ei pea) funktsioonidena 
-- defineerida väljaviimise reeglid
conEl : a /\ b
        ------
     ->   a

-- ... mille väärtus on leitud mustrisobituse abil.
conEl = ?conEl_v

conEr : a /\ b
        ------
     ->   b

conEr = ?conEr_v

Disjunktsioon

infixl 11 \/
data (\/) : Type -> Type -> Type where
    DisjIl :   a 
             ------
          -> a \/ b

    DisjIr :   b 
             ------
          -> a \/ b

disjE : (a\/b)  ->  (a -> c)  ->  (b -> c)  
        ----------------------------------
    ->               c
disjE x f g = ?disjE_v

Eitus ja väärus

%hide Not  -- juba std. teegis olemas 

data Not : Type -> Type where
    NotI :   (a -> Void) 
             -----------
          ->    Not a

NotE : Not a -> a
       ----------
    ->    Void

NotE x = ?NotE_v

--data Void : Type where
---- meelega jäetud tühjaks


VoidE : Void
        ----
    ->    b
VoidE q impossible

Lausearvutuse ülesanne ex1


ex1 :  a /\ (b -> c) /\ (a -> b) 
       -------------------------
    ->            c
ex1 = ?ex1_v

Kalmeri lemmikväide:

Klassikalises loogikas a "põhjustab" b-d või b "põhjustab" a-d -- iga a ja b korral. (Näiteks a:="Täna on reede", b:="vihma sajab".)

--(Vihje: kasuta lambdat)
ex2 :      a \/ Not a
       --------------------
    -> (a -> b) \/ (b -> a)
ex2 a = ?ex2_v

Paaris

Mingi oma teooria lisamiseks tuleb defineerida data vastavate aksioomidega. Näiteks teooria paarisarvudest.

data Even : Nat -> Type where
    Even_Zero : --------
                 Even 0

    Even_Succ :    Even n 
                ------------
              -> Even (2+n)

even4 : Even 4
even4 = ?even4_v

even8 : Even 8
even8 = ?even8_v

plusEvenEven :  Even n -> Even m 
               ------------------
             ->    Even (n+m)
plusEvenEven a b = ?plusEvenEven_v


multEvenEven :  Even n -> Even m 
               ------------------
             ->    Even (n*m)
multEvenEven a b = ?multEvenEven_v

Paaris/Paaritu

data Odd : Nat -> Type where
    Odd_one : --------
               Odd 1

    Odd_Succ :    Odd n 
                -----------
              -> Odd (2+n)

odd7 : Odd 7
odd7 = ?odd7_v

evenOdd :   Even n
          ----------
        -> Odd (1+n)
evenOdd e = ?evenOdd_v


plusOddOdd :  Odd n  ->  Odd m 
             -------------------
           ->     Even (n+m)
plusOddOdd a b = ?plusOddOdd_v


plusEvenOdd :  Even n  ->  Odd m 
             -------------------
           ->     Odd (n+m)
plusEvenOdd a b = ?plusEvenOdd_v

plusNullOdd :    Odd m
              ------------
            -> Odd (m+0)
plusNullOdd a = ?plusNullOdd_v

Võrdused ja rewrite

Võrdus on standardteegis defineeritud põhimõtteliselt nii:

 data (=) : Type -> Type -> Type where
     Refl : {a:Type}
           ----------
          -> a = a

Nii saame defineerida üldisi võrdusi ja ei pea enam iga kasutuse jaoks uut teoreemi (nagu idVec loengust) tõestama.

Näidis

Proovi ka ise seda lahendada, et aru saada, kuidas rewrite töötab.

plusNull :   (n:Nat) 
            ---------
          -> n+0 = n
plusNull 0 = Refl 
plusNull (S k) = rewrite plusNull k in Refl

Ülesanne: liitmise assotsiatiivsus

Kasuta rewrite-i.

plusAssoc : (m:Nat) -> (n:Nat) -> (q:Nat)
            ------------------------------
          ->  m + (n + q) = (m + n) + q
plusAssoc m n q = ?plusAssoc_v

Tärnülesanne: multOddOdd

-- Vihjed: case-split a ja b (tuleb kolm juhtu)
-- Esimene juht on triviaalne, teised vajavad natuke vaeva. 
-- 
-- Märkus: Idrise poolt genereeritud 2+n asemel tuleb 
-- käsitsi panna S (S n) selleks, et muutuja n oleks kättesaadav.
multOddOdd :  (n:Nat)  ->  (m:Nat)  ->  Odd n  ->  Odd m 
             -------------------------------------------
           ->                Odd (n*m)
multOddOdd n m a b = ?multOddOdd_v

  • Arvutiteaduse instituut
  • Loodus- ja täppisteaduste valdkond
  • Tartu Ülikool
Tehniliste probleemide või küsimuste korral kirjuta:

Kursuse sisu ja korralduslike küsimustega pöörduge kursuse korraldajate poole.
Õppematerjalide varalised autoriõigused kuuluvad Tartu Ülikoolile. Õppematerjalide kasutamine on lubatud autoriõiguse seaduses ettenähtud teose vaba kasutamise eesmärkidel ja tingimustel. Õppematerjalide kasutamisel on kasutaja kohustatud viitama õppematerjalide autorile.
Õppematerjalide kasutamine muudel eesmärkidel on lubatud ainult Tartu Ülikooli eelneval kirjalikul nõusolekul.
Tartu Ülikooli arvutiteaduse instituudi kursuste läbiviimist toetavad järgmised programmid:
euroopa sotsiaalfondi logo