Funktsionaalprogrammeerimine - Kursused

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]

            

        
      
Funktsionaalprogrammeerimine 2022/23 sügis

13. Praktikum
