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

13. Praktikum

Selles praktikumis harjutame teise kontrolltöö ülesandeid.

Teemad:

  1. reedeksite tuvastamine
  2. redutseerimine normaalkujule
  3. tüübituletus
  4. programmeerimine sõltuvate tüüpidega
  5. tüübisüsteemi abil tõestamine
  6. programmeerimine lineaarsete tüüpidega

Kontrolltöös on kuus ülesannet. Esimesed kolm saab esitada ka paberil. (Anname paberit aga teie tooge pastakas, pliiats vms.)

%default total 

-- 1) leia kõik reedeksid
-- 
-- a) (λf. f((λx.x) 3)) (λx.x)
--           --------
--    ------------------------      


-- b) (λf. (λy. (λx.x) y) x)

-- c) (λa. (λb. c) a) ((λx.x) c)


-- 2) beeta-redutseeri normaalkujule normaal- ja aplikatiivjärjekorras
-- 

-- a) (λf. (λg. g f)) ((λx.x) a) (λx.b)
-- N: (λf. (λg. g f)) ((λx.x) a) (λx.b) 
--    --> (λg. g ((λx.x) a))  (λx.b) 
--    --> (λx.b) ((λx.x) a)  
--    --> b
-- A: (λf. (λg. g f)) ((λx.x) a) (λx.b) 
--    --> (λf. (λg. g f)) a (λx.b) 
--    --> (λg. g a) (λx.b) 
--    --> (λx.b) a  
--    --> b

-- b) (λx. (λx.x)) ((λx. x) x)

-- c) (λf. f f f) ((λx.x) (λx.b))


-- 3) tüübi tuletamine
-- "Joonista" tüübituletuspuu, kirjuta välja kõik kitsendused ja 
-- lahenda kogu avaldise tüüp ɣ2.
-- 
-- Lihtsustuseks: 
--  * ei pea kirjutama xᵅ ∈ Γ
--  * kitsendusi ei pea kirjutama puu sisse  (mis oli slaididel roheline)
-- 
-- a) ⊢ (λxᵅ¹. ((λyᵅ². yᵅ³)ˠ¹ xᵅ⁴)ᵝ¹)ˠ²

-- -------------
-- xᵅ¹,yᵅ² ⊢ yᵅ³
-----------------------    ----------   
-- xᵅ¹ ⊢ (λyᵅ². yᵅ³)ˠ¹     xᵅ¹ ⊢ xᵅ⁴
-- ----------------------------------
-- xᵅ¹ ⊢ ((λyᵅ². yᵅ³)ˠ¹ xᵅ⁴)ᵝ¹
-- -------------------------------
-- (λxᵅ¹. ((λyᵅ². yᵅ³)ˠ¹ xᵅ⁴)ᵝ¹)ˠ²

-- ɑ2=ɑ3, ɣ1=ɑ2→ɑ3, ɑ1=ɑ4, ɣ1=ɑ4→β1, ɣ2=ɑ1→β1

-- Lahendus: ɣ2 = ɑ→ɑ


-- b) ⊢ (λxᵅ¹. (xᵅ² (λyᵅ³. yᵅ⁴)ˠ¹)ᵝ¹)ˠ²

-- c) ⊢ (λxᵅ¹. ((λyᵅ². (λzᵅ³. yᵅ⁴)ˠ¹)ˠ³ xᵅ⁵)ᵝ¹)ˠ²

-- d) ⊢ (λxᵅ¹. ((λyᵅ². (λzᵅ³. zᵅ⁴)ˠ¹)ˠ³ xᵅ⁵)ᵝ¹)ˠ²




-- 4) sõltuvate tüüpidega programmeerimine

data Vect : Nat -> Type -> Type where
    Nil  : Vect 0 a
    (::) : a -> Vect n a -> Vect (1+n) a 

topelt : Nat -> Nat 
topelt 0 = 0
topelt (S k) = S (S (topelt k))

-- ex1 -- pane elemendid vaheldumisi  (NB! Kalmeril siin plugin juksib.)
sega : Vect n a -> Vect n a -> Vect (topelt n) a
sega xs ys = ?sega_r

-- Main> sega [1,2,3] [30,20,10]
-- [1, 30, 2, 20, 3, 10]

concat : Vect n a -> Vect m a -> Vect (n+m) a
concat [] ys = ys
concat (x :: y) ys = x :: concat y ys

-- ex2 -- lamenda tabel
flatten : Vect n (Vect m a) -> Vect (n*m) a
flatten xs = ?flatten_r

-- Main> flatten [[1,2,3],[30,20,10]]
-- [1, 2, 3, 30, 20, 10]

-- ex3 -- viimane element
last : Vect (S n) a -> a
last xs = ?last_r

-- Main> last [1,2,3]
-- 3

-- ex4 -- korda n korda
repeat : (n:Nat) -> a -> Vect n a 
repeat n x = ?repeat_r

-- Main> repeat 3 'a'
-- ['a', 'a', 'a']

-- ex5 -- lisa kõigile üks ette
appendAll : (n:Nat) -> Vect n a -> Vect n (Vect m a) -> Vect n (Vect (S m) a)
appendAll n xs yss = ?appendAll_r

-- Main> appendAll 3 [1,2,3] [[30],[20],[10]]
-- [[1, 30], [2, 20], [3, 10]]

-- ex6 -- transponeeri
transpose : (n:Nat) -> (m:Nat) -> Vect n (Vect m a) -> Vect m (Vect n a)
transpose n m xss = ?transpose_r

-- Main> transpose 3 2 [[1,2],[3,4],[5,6]]
-- [[1, 3, 5], [2, 4, 6]]



-- 5) tõestamine Idris2-s

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

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

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

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

--ex7 -- lausearvutus
test1 : (a \/ b) /\ (a -> b) 
        --------------------
    ->          b
test1 = ?test1_r

--ex8 -- lausearvutus
test2 : (a \/ b \/ c) /\ (b -> c) 
        -------------------------
    ->         (a \/ c)
test2 = ?test2_r


-- tuleb kasuks test3-s
mult0 : (k:Nat) -> 0 = k*0
mult0 0 = Refl
mult0 (S k) = mult0 k

-- NB! Nat ei ole tegelikult piiratud ressurss.
add : (1 _ : Nat) -> (1 _: Nat) -> Nat
add x 0 = x 
add 0 (S k) = S k
add (S j) (S k) = 2+j+k

mul : (1 _ : Nat) -> (1 _: Nat) -> Nat
mul 0 0 = 0
mul (S k) 0 = 0
mul 0 (S k) = 0
mul (S j) (S k) = (S j)*(S k)

--ex9 -- mul on korrutamine
test3 : (a:Nat) -> (b:Nat)
        ------------------
    ->     mul a b = a*b
test3 a b = ?test3_r

--ex9 -- liitmisel S paremal
plus_n_Sm : (n:Nat)  ->  (m:Nat)
            --------------------
         -> n + (S m) = S (n+m)
plus_n_Sm n m = ?plus_n_Sm_r


--ex10 -- topelt n arvutab n+n
topeltOk :    (n:Nat) 
            --------------
        -> topelt n = n+n
topeltOk n = ?topeltOk_r

--ex11 -- foldr (::) [] on identsusfunktsioon
foldr_id : (xs:List a) -> foldr (::) [] xs = xs
foldr_id xs = ?foldr_id_r

-- 6) lineaarsed tüübid

namespace Lin
    public export
    data List : Type -> Type where
        Nil  : Lin.List a
        (::) : (1 _ : a) -> (1 _ : Lin.List a) -> Lin.List a

--ex12 -- rakendab funktsioonid järjest
seqL : (1 _: Lin.List ((1 _ : a) -> a)) -> (1 _: a) -> a
seqL fs x = ?seqL_r

-- Main> seqL [add 1, add 2] 0
-- 3
-- Main> seqL [add 3, mul 0, add 4] 0
-- 4

--ex13 -- foldr, kus akumulaator on lineaarne
foldLf : ((1 _: a) -> b -> a) -> Prelude.List b -> (1 _: a) -> a
foldLf f xs y = ?foldLf_r

-- Main> foldLf (\ x, y => add x y) [1,3] 0
-- 4
-- Main> foldLf (\ x, y => add x y) [2,3] 1
-- 6

--ex14 -- foldr, kus akumulaator ja list on lineaarsed
foldLl : ((1 _ : a) -> (1 _ : b) -> a) -> (1 _ : Lin.List b) -> a -> a
foldLl f xs y = ?foldLl_r

-- Main> foldLl (\ x, y => mul x y) [2,0] 1
-- 0
-- Main> foldLl (\ x, y => mul x y) [2,5] 1
-- 10

append : (1 _ : Lin.List a) -> (1 _ : Lin.List a) -> Lin.List a
append xs ys = ?append_r

--ex15 -- lineaarse listi lamendamine
concatL : (1 _ : Lin.List (Lin.List a)) -> Lin.List a
concatL xss = ?concatL_r

-- Main> concatL [[],[],[]]
-- []
-- Main> concatL [[1,2,3],[],[4,5]]
-- [1, 2, 3, 4, 5]
  • 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