13. Praktikum
Selles praktikumis harjutame teise kontrolltöö ülesandeid.
Teemad:
- reedeksite tuvastamine
- redutseerimine normaalkujule
- tüübituletus
- programmeerimine sõltuvate tüüpidega
- tüübisüsteemi abil tõestamine
- 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]