Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
FLP záloha sbírky z https://hackmd.io/s/BkOp5w4T4

FLP studentská sbírka úloh

Přehlednější sbírka oficiálních řešení + zadání z fitušky od studentů. Upravujte, přidávejte dle libosti. Jen prosím držte nějakou strukturu, ať se v tom dá vyznat. Pro diskuzi se dají použít komentáře u odstavců/kódů.

Haskell

2018/2019

Řádný termín

(btw priecinok == složka) Nadefinovat strukturu pre DirTree. Urobit funkciu, ktora spocita velkost obsahu priecinka. Urobit funkciu ktora vrati zoznam suborov a priecinkov, ktory obsahuju zadany prefix. Funkcia na rekurzivny vypis obsahu priecinka, nieco ako:

(tohle je soucast zadani jeste)
-* Root
+ +-* SubDir
+ + + file2
+ file1
+
data DirTree a
    = File String Integer a
    | Dir String Integer a [DirTree a]
    deriving (Show,Eq)

dirSize (File _ s _) = s
dirSize (Dir _ s _ dir) = foldr (+) s $ map dirSize dir

findAllPref file dir =
    findPath "" dir
    where
        cmpp [] _ = True
        cmpp _ [] = False
        cmpp (p:ps) (f:fs) = p==f && cmpp ps fs
        findPath p (File name _ _) =
            if cmpp file name then [p++name] else []
        findPath p (Dir name _ _ dir) =
            let
                cur = if cmpp file name then [p++name++"/"] else []
                other = concatMap (findPath $ p++name++"/") dir
            in
                cur++other
printDir (File name size _) = putStrLn $ "+ " ++name++" "++show size
printDir d@(Dir _ _ _ _) =
    prd "" d
    where
        prd pref (File name size _) = putStrLn $ pref++" "++name++" "++show size
        prd pref (Dir name _ _ dir) = do
            putStrLn $ pref++"-* "++name
            mapM_ (prd $ pref++" +") dir
            putStrLn $ pref++" ."
-------------
data Color
    = Black
    | Red
    deriving (Show,Eq,Ord,Bounded,Read,Enum)
data RBT a
    = Nil
    | Nd Color a (RBT a) (RBT a)
    deriving (Show,Eq)
    
countBlack Nil = Just 1
countBlack (Nd Red _ l r) =
    cmpLR 0 (countBlack l) (countBlack r)
countBlack (Nd _ _ l r) =
    cmpLR 1 (countBlack l) (countBlack r)
cmpLR x (Just lv) (Just rv) = if lv == rv then Just $ x+lv else Nothing
cmpLR _ _ _ = Nothing

2017/2018

Řádný termín

/13b/ Nadefinovat funkciu pt, ktora berie nazov suboru ako argument. Z tohoto suboru nacita zaznamy ve formatu Cislo_typu_Integer#String, pripadne prazdny riadok. Zaznam reprezentovat datovym typom DLog. Vypsat zaznamy s cisly, ktere jsou nasobkem 5 (cislo mod 5 == 0). Odelene budu tentoraz dvojbodkou (:). Je potrebne uviest typove defincie pre kazdu pouzitu funkciu. Zadane byly typove definicie nekterych funkci pro praci s IO (openFile, hGetContents, lines, unlines, ReadMode, WriteMode, atp.).

data DLog
    = Empty
    | IT Integer String
    deriving (Show,Eq)
    
pr :: [DLog] -> IO ()
pr [] = return ()
pr (Empty:xs) = pr xs
pr ((IT i s):xs) =
    if i `mod` 5 == 0
    then putStrLn (show i ++ ":" ++ s) >> pr xs
    else pr xs
    
pl :: String -> IO ()
pl fn = do
    h <- openFile fn ReadMode
    c <- hGetContents h
    pr $ proc $ lines c
    hClose h
    
proc :: [String] -> [DLog]
proc [] = []
proc (l:ls) =
    if null l
    then Empty : proc ls
    else (mk l) : proc ls
    
mk :: String -> DLog
mk l = IT ((read (takeWhile (/='#') l))::Integer)
    (tail $ dropWhile (/='#') l)

/6b/ BONUS otazka - Vytvorit datovou strukturu pro reprezentaci stromu. Vytvorit funkci initTree, ktera dostane jako parametr hodnotu a vytvori nekonecny strom, kde vsechny uzly obsahuji tuto hodnotu. Vytvorit funkci takeLev, ktera vrati strom az po urcitou uroven danou parametrem.

pl' :: String -> IO()
pl' fn = do
    h <- openFile fn ReadMode
    c <- hGetContents h
    pr $ map mkDL $ lines c
    hClose h
    
mkDL :: String -> DLog
mkDL [] = Empty
mkDL l = let (n,s) = span (/='#') l
    in IT ((read n)::Integer) (tail s)

1. opravný termín

Vytvořit nekonečný seznam prvočísel.

primes = 2:[x | x <- [3,5..], isPrime x primes]
    where
        isPrime x (p:ps) =
            (p*p > x) || (x `mod` p /= 0 && isPrime x ps)

Haskell s dostupnými IO funkcemi. Napsat funkci mkR, která dostane jméno souboru. V řádcích souboru se nachází buď FIT login, nebo prázdný řádek, nebo nějaký jiný text. Funkce má vypsat nejdříve počet řádků s validními loginy, pak počet textových řádků, pak počet prázdných řádku a nakonec vypsat všechny tyto validní loginy v náhodném pořadí. Pro generování náhodných čísel je k dispozici funkce randomRIO :: Random a => (a, a) -> IO a.

mkR :: String -> IO ()
mkR file = do
    h <- openFile file ReadMode
    c <- hGetContents h
    let alllogs = lines c
    let empty = length $ filter (=="") alllogs
    let wempty = filter (/="") alllogs
    let notLogs = length $ filter (not . isLogin) wempty
    let correct = filter isLogin wempty
    putStrLn $ show (length correct) ++ "/" ++ show notLogs ++ "/" ++ show empty
    randLog <- genRand correct
    putStrLn $ unlines randLog
    hClose h
    
isLogin :: String -> Bool
isLogin x =
    length x == 8 && head x == 'x' &&
    (all (\x -> elem x ['a'..'z']) $ take 5 $ tail x) &&
    (all (\x -> elem x (['0'..'9']++['a'..'z'])) $ drop 6 x)
    
genRand :: [a] -> IO [a]
genRand [] = return []
genRand l = do
    ir <- randomRIO (0,length l - 1) :: IO Int
    let (h,t) = splitAt ir l
    let v = head t
    let r = tail t
    mkr <- genRand (h++r)
    return (v:mkr)

2016/2017

Řádný termín

Holý Haskell. Definovat datový typ pro asociativní pole. Dále napsat funkci test, která ověří, že klíče v asociativním poli jsou unikátní. (7b)

data AL k d
    = Val k d (AL k d)
    | Nil
    deriving (Show,Eq)
    
test Nil = True
test (Val k _ rest) = noKey k rest && test rest

noKey _ Nil = True
noKey k (Val k' _ rest) = k/=k' && noKey k rest

Haskell + prelude (kromě readFile) + nějaké IO funkce jako (hGetContents, hClose, openFile, hPutStr). Napsat funkci fdup, která načte soubor jehož nazev je v jejím parametru a potom tento soubor vypíše na výstup, ale s tím, že pokud jsou na začátku řádku dva znaky +, tak se tento řádek vypíše 2x, ale už bez těchto dvou plusových znaků. Nesmí se změnit pořadí řádků. (6b)

import System.IO

fdup :: FilePath -> IO ()
fdup file = do
    h <- openFile file ReadMode
    c <- hGetContents h
    putStr $ unlines $ dl $ lines c
    hClose h
    
dl :: [String] -> [String]
dl (('+':'+':l):ls) = l:l:dl ls
dl (l:ls) = l : dl ls
dl [] = []

Bonus: Definujte strukturu pro termy v prologu a následně funkci unify s dvěma parametry, která vratí nejobecnější unifikátor dvou termu (8b)

data Term
    = Var String
    | ValI Integer
    | Term String [Term]
    deriving (Show,Eq)
    
unify (ValI a) (ValI b) =
    if a==b then Just [] else Nothing
unify (Term a as) (Term b bs) =
    if a==b && length as==length bs then comb [] as bs
    else Nothing
    where
        comb res [] [] = Just res
        comb res (a:as) (b:bs) =
unify a b >>=
    (\s -> comb (res++s) (map (lapp s) as) (map (lapp s) bs))
unify w@(Var a) t =
    if w==t then Just [] else Just [(a,t)]
unify t w@(Var a) = unify w t

lapp ss t = foldl (flip app) t ss

app (v,t) w@(Var v') =
    if v==v' then t else w
app s (Term t ts) = Term t (map (app s) ts)
app _ x = x

Prolog

2018/2019

Řádný termín

  1. Napsat predikaty pro zjisteni, jestli je prvek v seznamu a pro odstraneni hodnoty ze seznamu. Dat si bacha na to, ze seznam muze obsahovat nenavazane promenne a prvek se s nima nesmi zunifikovat.
  2. Transpozice matice.
  3. Predikat, ktery bere sudoku reprezentovane matici 9x9 a vytvori seznam bloku 3x3.
  4. Predikat, ktery pro danou pozici v sudoku zjisti seznam moznych hodnot, ktere se na to policko daji doplnit. Mame k dispozici predikat getIth(X,M,L), ktery z matice M vytahne radek X do seznamu L. A meli jsme napsane, jak se z pozice [X,Y] v matici urci cislo bloku.
  5. Predikat solves, ktery s vyuzitim definovanych predikatu vyresi sudoku, ktere ma na vstupu zadane matici 9x9. Neobsazene policka jsou reprezentovana volnou promennou. Muzem pouzit getIth, getRC, ktery pro zadanou pozici a matici vrati prvek na tech souradnicich a setRC, ktery nastavi prvek v matici na nejakou hodnotu.
/* -- vv -- */
elemNV(X,[V|_]) :- nonvar(V), V=X, !.
elemNV(X,[_|VS]) :- elemNV(X,VS).

remVals([],_,[]).
remVals([X|XS],L,R) :- elemNV(X,L), !, remVals(XS,L,R).
remVals([X|XS],L,[X|R]) :- remVals(XS,L,R).

/* -- vv -- */
trp([[]|_],[]) :- !.
trp(XSS,[L|LS]) :- heads(XSS,L,YSS), trp(YSS,LS).

heads([[H|TS]|XSS],[H|T],[TS|YSS]) :- heads(XSS,T,YSS).
heads([],[],[]).

/* -- vv -- */
blocks([[A,B,C|CS],[D,E,F|FS],[G,H,I|IS]|XSS],[[A,B,C,D,E,F,G,H,I]|LS]) :- blocks([CS,FS,IS|XSS],LS).
blocks([[],[],[]|XSS],LS) :- blocks(XSS,LS).
blocks([],[]).

/* -- vv -- */
valsFor(X,Y,M,[V|VS]) :-
    getIth(X,M,L),
    remVals([1,2,3,4,5,6,7,8,9],L,[H|T]),
    trp(M,TM),
    getIth(Y,TM,R),
    remVals([H|T],R,[HH|TT]),
    blocks(M,BM),
    P is (3*((X-1)//3)) + (1+((Y-1)//3)),
    getIth(P,BM,B),
    remVals([HH|TT],B,[V|VS]).

/* -- vv -- */
solves(M) :- search(1,1,M).

search(R,C,M) :-
    getRC(R,C,M,V),
    nonvar(V), !,
    goNonvar(R,C,M).
search(R,C,M) :-
    valsFor(R,C,M,VS),
    testVals(R,C,M,VS).
    
goNonvar(9,9,_) :- !.
goNonvar(R,C,M) :-
    newRC(R,C,RR,CC),
    search(RR,CC,M).

testVals(9,9,M,[X]) :-
    getRC(9,9,M,X), !.
testVals(R,C,M,[X|_]) :-
    getRC(R,C,M,X),
    newRC(R,C,RR,CC),
    search(RR,CC,M).
testVals(R,C,M,[_|XS]) :-
    testVals(R,C,M,XS).
    
/* co bylo k dispozici jako hotove, pro uplnost */
newRC(R,C,R,CC) :-
    C<9, !, CC is C+1.
newRC(R,9,RR,1) :-
    R<9, RR is R+1.
    
getIth(1,[X|_],X) :- !.
getIth(N,[_|XS],X) :- N1 is N-1, getIth(N1,XS,X).

getRC(R,C,M,V) :-
    getIth(R,M,L),
    getIth(C,L,V).

2017/2018

Řádný termín

  1. /6b/ Flatten seznamu - vytvorit predikat e, ktery bere 2 argumenty. Prvni je seznam libovolne zanorenych seznamu (i prazdnych), napr. [[], [1, 2], [[[[]]],[atom, atom]]]. Druhy argument je vysledny seznam bez zanoreni.
  2. /7b/ Funkce XOR, ktera vraci symterickou diferenci dvou mnozin (sjednoceni mnozin bez jejich pruseciku). Bere prvni a druhy parametr mnozinu reprezentovanou seznamem, treti parametr je vysledna mnozina reprezentovana seznamem.
  3. /9b/ Napisat predikat search(PocatecniPozice, SeznamCest), ktory najde vsechny cesty z dane pozice zpet do teto pozice, delky 20 az 22 kroku (netrapit se tim, jestli vracet prvni/posledni prvek ci ne). Kazdy prvok je mozne nastivit len jeden krat vyjma prveho (== posledneho). Definicia pozicie je neznama, napiste funkci nextStep(Pos, NewPos) nad neznamym a NEKONECNYM stavovym priestorom. Mozno pouzit retract*, assert*, bagof, setof, length.
  4. /8b/ Napisat predikat lookup. Prvy arguement vhodne reprezentovana tabulka symbolov, 2-hy argument kluc, 3-ty argument hodnota. A posledny a vysledny argument je modifikovana, pripadne vstupna tabulka symbolov.

Predikat pracuje v dvoch rezimoch. Ak je zadana hodnota, tak sa modifikuje pripadne modifikuje zaznam (klic -> hodnota?) v tabulke symbolov. Ak nie je zadana hodnota, tak vyhladavame v tabulku hodnotu so zadanym klucom. Ak sa nemylim, tak bolo mozne pouzit vsetko zo zakladnej kniznice Prologu. Ja som pouzil var(), nonvar() na zistenie, ci (nie) je zadana hodnota a nemyslim si, ze by to bolo v zadani spomenute. -- priklad byl mozna lehce modifikovany?

:- dynamic
pos/1.
/* ---------------------------------- */
e([],[]).
e([[]|R],Res) :- !, e(R,Res).
e([[X|XS]|YS],Res) :- !, e([X,XS|YS],Res).
e([V|XS],[V|Res]) :- e(XS,Res).
/* ---------------------------------- */
xor([],L,L) :- !.
xor(L,[],L) :- !.
xor(L,R,Res) :- sub(L,R,L1),sub(R,L,R1),app(L1,R1,Res).

sub([],_,[]).
sub([X|XS],YS,RS) :- elem(X,YS),!,sub(XS,YS,RS).
sub([X|XS],YS,[X|RS]) :- sub(XS,YS,RS).

elem(X,[X|_]) :- !.
elem(X,[_|XS]) :- elem(X,XS).

app([],L,L).
app([X|XS],L,[X|RS]) :- app(XS,L,RS).
/* ---------------------------------- */
search(P,Res) :-
    setof(Path,s(P,P,0,Path),Res).

s(P,P,N,[P]) :- N =< 22, N >= 20, !.
s(_,_,N,_) :- N > 22, !, fail.
s(P,P,N,_) :- N \= 0, !, fail.
s(A,P,N,[A|R]) :-
    assertz(pos(A)),
    NN is N+1,
    nextStep(A,AA),
    ( not(pos(AA)) ; AA=P ) ,
    s(AA,P,NN,R).
s(A,_,_,_) :-
    pos(A),
    retract(pos(A)),
    !,fail.

nextStep(p(X,Y),p(XX,Y)) :- XX is X+1.
nextStep(p(X,Y),p(XX,Y)) :- XX is X-1.
nextStep(p(X,Y),p(X,YY)) :- YY is Y+1.
nextStep(p(X,Y),p(X,YY)) :- YY is Y-1.
/* ---------------------------------- */
emptyT([]).

lookup(T,_,_,_) :- var(T), !, fail.
lookup(T,Var,Val,NT) :- nonvar(Var),nonvar(Val), !, iT(T,Var,Val,NT).
lookup(T,Var,Val,T) :- nonvar(Var), lT(T,Var,Val).

iT([], R, L, [p(R,L)]).
iT([p(R,_)|PS], R, L, [p(R,L)|PS]) :- !.
iT([p(RR,LL)|PS], R, L, [p(RR,LL)|PPS]) :- iT(PS,R,L,PPS).

lT([p(R,L)|_],R,L) :- !.
lT([_|PS],R,L) :- lT(PS,R,L).

/* EOF */

1. opravny termín

  1. Holý Prolog. Napsat predikát mkTrans(ListOfLists,ListOfLists), která dostane v 1. argumentu matici, kterou transponovanou unifikuje do 2. argumentu.
  2. Holý Prolog. Napsat predikát subseq, který v 1. argumentu dostane seznam a do 2. argumentu unifikuje seznam všech jeho podseznamů, tedy jde tam o prefix a suffix matching.
  3. Prolog s bagof, setof, assert, retract atp. Prohledávání stavového prostoru. Napsat predikát search(Start,Cíl, Nejkratší_cesta), který dostane nějakou startovní a koncovou pozici a unifikuje do 3. argumentu nejkratší cestu mezi nimi. Napsat také predikát nextStep, který bude vracet další novou pozici. úkolem není napsat optimální řešení, ale využít elegantnosti Prologu.
  4. Prolog s celočíselným dělením, dělením a is. Napsat Prologovou reprezentaci racionálních čísel a operaci násobení a sčítání nad nimi.
:- dynamic
pos/1.
/* ---------------------------------- */
mkTrans([],[]).
mkTrans([[]|_],[]).
mkTrans(LS,[HS|HHS]) :-
    trans(LS,HS,TS),
    mkTrans(TS,HHS).

trans([],[],[]).
trans([[H|T]|LS],[H|HS],[T|TS]) :-
    trans(LS,HS,TS).
/* ---------------------------------- */
suff([],[[]]).
suff([H|T],[[H|T]|R]) :-
    suff(T,R).

subseq(S,[[]|SS]) :-
    suff(S,SUFS),
    proc(SUFS,SS).

proc([],[]).
proc([S|SS],RES) :-
    pref(S,[_|PS]),
    proc(SS,PSS),
    append(PS,PSS,RES).

pref([H|T],[[]|R]) :-
    pref(T,PS),
    prepAll(H,PS,R).
pref([],[[]]).

prepAll(_,[],[]).
prepAll(X,[L|LS],[[X|L]|XS]) :-
    prepAll(X,LS,XS).
/* ---------------------------------- */
search(S,E,Res) :-
    retractall(pos(_)),
    steptry(S,E,0,Res).
    
steptry(S,E,N,Res) :-
    s(S,E,N,Res), !.
steptry(S,E,N,Res) :-
    NN is N+1,
    steptry(S,E,NN,Res).
    
s(E,E,0,[E]) :- !.
s(_,_,N,_) :- N < 0, !, fail.
s(A,E,N,[A|R]) :-
    assertz(pos(A)),
    NN is N-1,
    nextStep(A,AA),
    not(pos(AA)) ,
    s(AA,E,NN,R).
s(A,_,_,_) :-
    pos(A),
    retract(pos(A)),
    !,fail.
    
nextStep(p(X,Y),p(XX,Y)) :- XX is X+1.
nextStep(p(X,Y),p(XX,Y)) :- XX is X-1.
nextStep(p(X,Y),p(X,YY)) :- YY is Y+1.
nextStep(p(X,Y),p(X,YY)) :- YY is Y-1.
/* ---------------------------------- */
/* rac(numerartor,denominator) */
/* op('+',L,R).
* op('*',L,R).
* rac(N,D).
*/
gcd(N,N,N) :- !.
gcd(N,M,M) :-
    N > M,
    NN is mod(N,M),
    NN==0, !.
gcd(N,M,D) :-
    N > M, !,
    NN is mod(N,M),
    gcd(M,NN,D).
gcd(N,M,N) :-
    M > N,
    MM is mod(M,N),
    MM is 0, !.
gcd(N,M,D) :-
    MM is mod(M,N),
    gcd(N,MM,D).
    
ev(op('+',L,R),rac(NN,DD)) :-
    ev(L,rac(LN,LD)),
    ev(R,rac(RN,RD)),
    N1 is LN*RD + RN*LD,
    D1 is LD*RD,
    norm(N1,D1,NN,DD).
ev(op('*',L,R),rac(NN,DD)) :-
    ev(L,rac(LN,LD)),
    ev(R,rac(RN,RD)),
    N1 is LN*RN,
    D1 is LD*RD,
    norm(N1,D1,NN,DD).
ev(rac(X,Y),rac(X,Y)).

norm(N,D,NN,DD) :-
    gcd(N,D,G), G>1,!,
    NN is div(N,G),
    DD is div(D,G).
norm(N,D,N,D).
/* EOF */

Lambda kalkul

2018/2019

E k = k
Y E = k
Y E = E (Y E)

LET True = \ x y. x
LET False = \ x y. y

LET LT = Y(\f x y. iszero y False (iszero x True (f (prev x) (prev y))))

2017/2018

/6b/ Op. pevneho bodu - MINUS x y. Nadefinovat True + False. K dispozici isZero, prev. Pripadne si dodefinovat dalsi funkce.

LET True = \ x y . x
LET False = \ x y . y
LET (?:) = \ c t f . c t f

    Y E = k
    E k = k
    Y E = E k = E (Y E)
    
LET minus = Y (\ f x y . iszero x ? 0 : (iszero y ? x : f (prev x) (prev y) ))

2016/2017

Ukázat vlastnost operátoru pevného bodu. V lamda kalkulu definovat násobení (MUL) s dvěma parametry pomocí prev, add, iszero a ternárního operátoru (6b)

k - pevny bod
E - vyraz
Y - operator pevneho bodu

    Y E = k
    E k = k
    E (Y E) = Y E
    
LET mul = \ a b . (iszero a ? 0 : (iszero b ? 0 : mf a b 0))
LET mf = Y (\ f a b r . iszero a ? r : f (pred a) b (add r b))

Důkazy

2018/2019

any [] = False -- 1
any (x:xs) = x || any xs -- 2

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f z [] = z -- 3
foldr f z (x:xs) = f x (foldr f z xs) -- 4

any xs = foldr (||) False xs

1) xs = []

L = any [] =|1
  = False
P = foldr (||) False [] =|3
  = False
  
L = P

I.H.: any xs = foldr (||) False xs

2) xs = (a:as)

L = any (a:as) =|2
  = a || any as
P = foldr (||) False (a:as) =| 4
  = (||) a (foldr (||) False as) =|I.H.
  = (||) a (any as) =|prefix->infi
  = a || (any as) =|priorita
  = a || any as
L=P
Q.E.D.

2017/2018

Radny

Ukazat:
foldr (&&) True xs = all xs

1)
xs = []

L = foldr (&&) True [] =|3
  = True
P = all [] =|1
  = True
  
L = P

2)
I.H.: foldr (&&) True as = all as

xs = (a:as)

L = foldr (&&) True (a:as) =|4
  = (&&) a (foldr (&&) True as) =|IH
  = (&&) a (all as) =|prefix->infix
  = a && (all as) =|priorita
  = a && all as
  
P = all (a:as) =|2
  = a && all as
L = P
Q.E.D.

Opravny

length 0 xs = foldl (\ a _ -> a+1) 0 xs

1)
xs = []

L = length 0 [] =|1
  = 0
P = foldl (\ a -> a+1) 0 [] =|3
  = 0

L = P

2)
I.P.
forall k in N: length k as = foldl (\ a _ -> a+1) k as

xs = (a:as)

L = length 0 (a:as) =|2
    = length (0+1) as =|soucet
    = length (1) as =|prebytecne zavorky
    = length 1 as =|I.P.
    = foldl (\ a _ -> a+1) 1 as
    
P = foldl (\ a _ -> a+1) 0 (a:as) =|4
    = foldl (\ a _ -> a+1) ((\ a _ -> a+1) 0 a) as =|beta_redukce
    = foldl (\ a _ -> a+1) ((\ _ -> 0+1) a) as =|beta_redukce
    = foldl (\ a _ -> a+1) (0+1) as =|soucet
    = foldl (\ a _ -> a+1) (1) as =|prebytecne zavorky
    = foldl (\ a _ -> a+1) 1 as
L = P
Q.E.D.

2016/2017

-- apostrofy pouze pro akceptaci v ghci
sum' [] = 0 -- 1
sum' (x:xs) = x + sum' xs -- 2
foldr' f a [] = a -- 3
foldr' f a (x:xs) = f x (foldr' f a xs) -- 4

sum xs = foldr (+) 0 xs

(1) xs = []

L = sum [] =|1
  = 0
P = foldr (+) 0 [] =|3
  = 0
L=P

2) xs = (a:as)

I.H.
sum as = foldr (+) 0 as

L = sum (a:as) =|2
  = a + sum as
P = foldr (+) 0 (a:as) =|4
  = (+) a (foldr (+) 0 as) =|I.H.
  = (+) a (sum as) =|prefix->infix
  = a + (sum as) =|priorita aplikace nejvyssi -> eliminace zavorek
  = a + sum as
L = P
Q.E.D.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment