Toto je starší verze dokumentu!
Zápisky
Slovník pojmů
Silná normalizace
Slabá normalizace
Konfluence
když přepíši konfiguraci E na dva další přepisy, musí vždy existovat pravidlo, které tyto dva přepisy spojí (relace)
Jinak: když můžu nedeterministicky přepsat konfiguraci A na konfiguraci B a C, existuje konfigurace D, na kterou se můžou B a C přepsat (a tím se jejich cesty zase spojí). Tohle ale nevylučuje, že z B a C nemůžou vést další přepisy někam jinam, z toho důvodu nám konfluence zajišťuje pouze slabou normalizaci a ne silnou.
Determinismus
Konfigurace
Stav, ve kterém se může program nacházet (čili v případě aritmetických výrazů všechny možné kombinace jako (1+2), (2+1), (2+(5*6)+3), …). Konfigurací tedy může být (a většinou i je) nekonečně mnoho.
u PostFixu je to (CommandSeq, Stack)
Přepisovací funkce
Finální konfigurace
u PostFixu je to ([], S) → již není s čím pracovat, množina příkazů je prázdná
Finální konfigurace je konfigurace, která se již nemůže přepsat pomocí přepisovacího pravidlo (neexistuje na ní přepisovací pravidlo)
Operační sémantika
(konfigurace, přepisovací funkce, finální konfigurace, vstupní funkce, výstupní funkce)
DEF(Turband): Operační sémantika vysvětluje význam jednotlivých konstruktů programovacího jazyka pomocí „navazujících“ kroků abstract machine.
EN DEF: An operational semantics explains the meaning of programming language constructs in terms of the step-by-step process of an abstract machine.
Operační sémantika malého kroku (SOS - Small Step Operational Semantics)
Operační sémantika velkého kroku (BOS - Big Step Operational Semantics)
Denotační sémantika
Denotační sémantika je založená na tom, že výrazy v naší gramatice převádíme do již známé algebry (například počítání s celými čísly), tím pádem už máme všechny operace v té algebře dokázané a můžeme použít algebru jako hotový aparát (analogie s programováním - použijeme framework, který už někdo napsal, je otestovaný a dobře funguje a nebudeme si muset psát vlastní).
Analogií denotační sémantiky je spíše bijekce mezi prvky konečného uspořádaného listu velikosti N a sekvencí přirozených čísel „1, 2, … N“, kdy pozice listu převedeme na ekvivalentní čísla a ukazatel next převedeme na operaci + 1.
DEF(Turband): Denotační sémantika vysvětluje význam konstruktů programovacího jazyka pomocí významu jednotlivých částí termů.
EN DEF: A denotational semantics explains the meaning of programming language constructs in terms of the meaning of their subparts.
Energie a důkaz konečnosti
To je věc, kterou používáme při důkazech konečnosti sémantik. Pokud chceme dokázat konečnost nějaké sémantiky, musíme si vymyslet (najít) nějakou funkci, která nám bude převádět konfiguraci na celé číslo - energii. Když máme hotovou funkci, musíme zajistit, že energie má nějakou minimální hodnotu, na které se zastaví (čili zřejmě se bude jednat o nejmenší hodnotu energie ze všech energií finálních konfigurací). No a pak potřebujeme dokázat pro každé přepisovací pravidlo, že snižuje energii (může to být komplikovanější, například jedno pravidlo energii nesnižuje ale po něm vždycky musí být aplikováno pravidlo, které energii snižuje apod).
Potenční množina
Množina všech podmnožin - Př. P{0, 1} = {{}, {0}, {1}, {0, 1}}
Množina
Klasická množina jak jí známe, nemá žádné uspořádání a každý prvek se zde vyskytuje jen jednou - př. {0, 1, 2} == {2, 0, 1}
Pozor, když máme množinu A = {0, 1, 2}, tak A* = (0, 1, 2, 1, 2, 0, 1, …) čili sekvence
Sekvence
Sekvence prvků, sekvence už je uspořádaná a může obsahovat více stejných prvků - př. (0, 1, 2, 1) != (1, 2, 1, 0)
MultiSet
Multimnožina - stejné jako množina, akorát může obsahovat více stejných prvků - př. {0, 1, 2, 1} == {1, 2, 1, 0}
->*
Jedná se o reflexivní tranzitivní uzávěr, čili je to relace, která říká, že se jedná o konečný počet přechodů (0 až N)
Příklady
Příklad: mějme gramatiku a vytvořme na ní sémantiky (SOS, BOS a DS)
E = E | (E+E) | (E*E) | N
* Pozn.: Uvědomme si, že znaménko + u výrazů(je za nimi znak přepisovací relace - šipka) vyjadřuje něco jiného než u N, u E znamená opravdu jen character, zatímco u N znamená klasické sčítání. Stejně tak pro * (násobení). Pokud jej píšeme na papír, měli bychom tato znaménka u E psát v kolečku (tady v dokuwiki je to aspoň tučným písmem). V denotační sémantice už je jejich rozdílný význam díky hranatým závorkám vidět lépe.
* Pozn.2: Opravujte nám to, pokud si myslíte, že máme něco špatně (v ničem si nejsme 100% jistí).
SOS
E → N
(N1+N2) → N3 kde N3=N1+N2
(N1 * N2) → N3 kde N3=N1*N2
E1 → E2
(E3 + E1) → (E3 + E2)
E1 → E2
(E3*E1) → (E3*E2)
E1 → E2
(E1 + E3) → (E2 + E3)
E1 → E2
(E1*E3) → (E2*E3)
BOS
E → N
(N1 + N2) → N3 kde N3 = N1 + N2
(N1 * N2) → N3 kde N3 = N1*N2
E1 →* N1 , E2 →* N2 , N = N1 + N2
(E1 + E2) →* N
E1 →* N1 , E2 →* N2 , N = N1 * N2
(E1* E2) →* N
DS
* [ [E]] = [ [N]]
* [ [N]] = N
* [ [ + ]] = +
* [ [*]] = *
* [ [E1 + E2]] = [ [E1]] [ [ + ]] [ [E2]]
* [ [E1*E2]] = [ [E1]] [ [*]] [ [E2]]
Vyhodnocovací strom pomocí naší primitivní SOS
Máme výraz: (3 + (6 * (4 + 8)) + (4 * 8))
Při vyhodnocování postupujeme odspodu
4 8
-------
6 (4 + 8)
-------------
3 (6 * (4 + 8)) 4 8
------------------- -------
(3 + (6 * (4 + 8))) (4 * 8)
-------------------------------
((3 + (6 * (4 + 8))) + (4 * 8))
Studenti a rozvrhy - chceme seřazený rozvrh studenta
x1(S, Z) = {(P, U, D, H, M)* | (P, U, D, H, M, S1) ∈ Z ∧ S∈S1} funkce dostane studenta a všechny záznamy a vrátí všechny hodiny, ve kterých student je (i tam kde není sám)
x3 = {(Po, 1), (Ut, 2), (St, 3), (Ct, 4), (Pa, 5)}
x(S, Z) = {(P, U, D, H, M)* | (P, U, D, H, M) ∈ x1(S, Z) ∧ ∀(P1, U1, D1, H1, M1) ∈ x1(S, Z); x2(D, H)≤x2(D1, H1)} dostane studenta a všechny rozvrhy a vyfiltruje je pomocí x1 a seřadí pomocí x2
Quicksort
Dokuwiki neumí matematickou syntaxi, takže ε je epsilon a · je symbol zřetězení.
Zápis relací
QSORT({A1, A2, …, An}) = QSORT(A|A ∈ {A1, A2, …, An} AND A < A1)·A1·QSORT(A|A ∈ {A1, A2, …, An} AND A > A1)
QSORT({}) = ε
Velký krok
A = {A1, A2, …, An} - vstupní neseřazená množina
B - výstupní seřazená množina
QSORT({}) = ε
QSORT(A) → B
B = QSORT(A)·A1·QSORT(A)
Malý krok
QSORT(A) → QSORT(ε, ε, A, A1)
QSORT(A, B, C, p)
QSORT(A·C1, B, {C2, C3, …, Cn}, p) pokud C1 ≤ p
QSORT(A, B·C1, {C2, C3, …, Cn}, p) pokud C1 > p
QSORT(A, B, ε, p) = QSORT(ε, ε, A, A1)·A1·QSORT(ε, ε, B, B1)
QSORT(ε, ε, ε, p) = ε
QSORT(A, ε, ε, p) → QSORT(ε, ε, A, A1)
QSORT(ε, A, ε, p) → QSORT(A, ε, ε, p)
QSORT(A, B, ε, p) = A·QSORT(ε, ε, B, B1) pokud length(A) = 1
QSORT(A, B, ε, p) = QSORT(ε, ε, A, A1)·B pokud length(B) = 1
Mergesort
Velký krok
MSORT({}) -> ε
MSORT(A) -> A if len(A) = 1
D-> MSORT(B)·MSORT(C) pro všechny x ∈ B: pro všechny y ∈ C: x < y
-----------------------------------------------------------
MSORT(A) -> D
Selectsort
Malý krok
A = {..,-1, 0, 1, ...}
SSORT: A* -> A*
FMIN: (A*->A) -> A
FMIN({A_1 , .., A_n}, ε} -> FMIN({A_2, .., A_n}, A_1}
FMIN({A_1, .., A_n}, min} -> FMIN({A_2, .., A_n}, min} if min<A_1
FMIN({A_1, .., A_n}, min} -> FMIN({A_2, .., A_n}, A_1} if min>A_1
FMIN(ε, min} -> ε
//A-FMIN(A,ε) - odstraní prvek, který vrátí funkce FMIN z A
SSORT(C,D) -> SSORT(C-FMIN(C,ε), D·FMIN(C,ε))
SSORT(e,D) -> D
Příklady z knihy
2.2
v následujícím odstavci je podtržítko dolní index a [ [ jsou dvě závorky bez mezery, neboť dvě bez mezery jsou otevírající tag
popis gramatiky je v knize v první kapitole viz cvičení 2.2 str 38
nrange: NumExp → (Nat, Nat)
brange: NumExp → (Nat, Nat)
N = int
B = bool
nrange[ [N]] = (e, e)
nrange[ [(arg N)]] = (N, N)
nrange[ [(A NE_1 NE_2)]] = (max(nrange[ [NE_1]]_1,nrange[ [NE_2]]_1), min(nrange[ [NE_1]]_2,nrange[ [NE_2]]_2)
nrange[ [(if BE NE_t NE_f)]] = (max(brange[ [BE]]_1, nrange[ [NE_t]]_1, nrange[ [NE_2]]_t), min(brange[ [BE]]_2, nrange[ [NE_1]]_2,nrange[ [NE_2]]_2)
brange[ [B]] = (e, e)
brange[ [(R NE_1 NE_2)]] = (max(nrange[ [NE_1]]_1,nrange[ [NE_2]]_1), min(nrange[ [NE_1]]_2,nrange[ [NE_2]]_2)
brange[ [(L BE_1 BE_2)]] = (max(brange[ [BE_1]]_1,brange[ [BE_2]]_1), min(brange[ [BE_1]]_2,brange[ [BE_2]]_2)
3.2
IF<(postfix 0 23 1 and mul sel), []> = <(23 1 and mul sel), []> → <(and mul sel), [1, 23]> → <(mul sel), [24]> → stuck neleží v FC (finální stav) takže nemá žádnou OF
3.3
a - je to rotace, vezmu prvek z vrcholu zásobníku a dám ho na konec
b - 432432
d - program by se zasekl na prázném zásobníku, např. (postfix 0 rot)
3.4
//udělám jen velmi jednoduše pro mul
<mul.Q, e> -> <Q, 1>
<mul.Q, N> -> <Q, N>
3.8
možná nebude úplně dokonalé, ale je to náznak toho jak na to
chybí mi tam exec, ale na to jsem moc línej a dalo by se to snadno dodělat (díky tomu moje RPN terminuje, s execem by to už nefungovalo, problém je v kopírování spodku zásobníku, když uděláme pop)
RPN
Domains:
Comand = {pop, add, intLit, mul, swap, div, sub}
ComandSeq = Command*
S∈Stack = int*
AnsExp = intLit
SOS
CF = ComandSeq x Stack
FC = {[]} x Stack
IF: Prog → CF = λ<Q>.<Q, [0, 0, 0, 0]>
OF: FC → AnsExp = λ<Q, [N_1, N_2, N_3, N_4]>.N_1
<N.Q,[N_1, N_2, N_3, N_4]> ⇒ <Q,[N, N_1, N_2, N_3]>
<pop.Q,[N_1, N_2, N_3, N_4]> ⇒ <Q,[N_2, N_3, N_4, N_4]>
<swap.Q,[N_1, N_2, N_3, N_4]> ⇒ <Q,[N_2, N_1, N_3, N_4]>
<A.Q,[N_1, N_2, N_3, N_4]> ⇒ <Q,[N_ans, N_3, N_4, N_4]> aritmetické oprerace N_ans = N_1 A N_2
A={add, sub, div,…}
3.9
mám pocit že bylo za úkol, tady si nejsem tak úplně jistej, takže jenom náznak
Q je celý seznam příkazů Q = com*, kde com = {intLit, +, -, *, = }, operandy budu zjednodušovat do op = {+, -, /, *, ..}
N_1 op = Q → N_ans Q if N_ans = N_1 op N_1
N_1 op N_2 = Q → N_ans Q if N_ans = N_1 op N_2
N_1 op N_2 op Q → N_ans op Q if N_ans = N_1 op N_2
N_1 op N_2 → N_2
N_1 op N_2 N_3 Q → N_3 Q
3.12
tak ještě příklad postfixu pomocí SOS, tentokrát máme vytvořit postfix, který nebude mít zásobník (překvapivě to jde), tady je malá ukázka, která zas není 100% hotová
předpokládám, že jste všichni četli knížku takže víte co znamená Q, V, N, … (Q = com*, V = intLit + com*, N= int)
(Q_1.V_1.V_2.swap.Q_2) → (Q_1.V_2.V_1.Q_2)
(Q_1.N_1.N_2.add.Q_2) → (Q_1.N_ans.Q_2) stejně tak i pro mul, sub, ..
* (Q_1.(Q_exec).exec.Q_2) → (Q_1.Q_exec.Q_2)
* (Q_1.V_1.V_2.N.sel.Q_2) → (Q_1.V_1.Q_2) if N = 0
* (Q_1.V_1.V_2.N.sel.Q_2) → (Q_1.V_2.Q_2) if N != 0
* na 100% to terminuje, otázka je jestli je to deterministické, protože pořadí příkazů není jasně dané (tak jako v postfixu)
* celkový program deterministický je, ale jednotlivé kroky ne
===== BOS =====
==== 3.16 ====
doplňujeme ELM o if a operace s booleanem
E = NE
NE = (NE_1 op NE_2) | (if BE NE_1 NE_2) | N
BE = (NE_1 Rop NE_2) | (BE_1 Lop BE_2) | B
N = int
B - {true, false}
BOS
E -> NE
N_1 op N_2 -> N
NE_1 -> N_1;NE_2 -> N_2; N = N_1 op N_2
----------------------------------------
(NE_1 op NE_2) -> N
BE_1 -> B_1;BE_2 -> B_2; B = B_1 op B_2
----------------------------------------
(BE_1 Rop BE_2) -> B
NE_1 -> N_1;NE_2 -> N_2; N = N_1 Lop N_2
----------------------------------------
(NE_1 Lop NE_2) -> B
NE_1 -> N_1;NE_2 -> N_2; BE -> B; B = true
----------------------------------------
(if BE NE_1 NE_2) -> NE_1
NE_1 -> N_1;NE_2 -> N_2; BE -> B; B = false
----------------------------------------
(if BE NE_1 NE_2) -> NE_2
Denotační sémantika
4.1 Prepis Signed a Unsigned Int literalu na cisla
D : intLit → int D - převedeme na integer
UN [ [@ UD D]] → 10 * [ [UD]] + [ [D]]
SN [ [+ UD]] → [ [UD]]
SN [ [- UD]] → -1 * [ [UD]]
Nahoru