• více větví se sejde do stejného výstupu (výsledku), nemůže se zacyklit
• je terminující a konfluentní

• větve se vždy sejdou do stejného výsledku, ale může dojít k zacyklení
• je konfluentní

• 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.

• z jedné konfigurace je pouze jedna další konfigurace, na kterou se dá přepsat

• 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)
• DEF EN: Each state of the abstract machine is called a configuration.

• definuje jeden krok
• vezme konfiguraci, která splňuje nějaké podmínky a přepíše jí na jinou konfiguraci

• 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 pravidla (neexistuje pro ni přepisovací pravidlo)
• Pro finální konfiguraci existuje výstup z výstupní funkce OF

• Je stav, který nelze dále přepsat, ale zároveň pro něj výstupní funkce OF nemá žádný výstup
• Dá se odstranit tím, že výstupní funkci předefinujeme přidáním stavu error
• Př: [pop, ε] příkaz pop na prázdném zásobníku
• Př odstranění: Postfixový stav se přepíše na chybový výstup, [pop, ε] → error, po této úpravě se stav [pop, ε] změní ze stuck state na finální konfiguraci

• (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.

• Definujeme přepisovací pravidla, která mají v předpokladech jiné JEDNOKROKOVÉ relace

• Přepisovací pravidla, která mohou mít v předpokladech

• 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.

• 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).

• Množina všech podmnožin - Př. P{0, 1} = {{}, {0}, {1}, {0, 1}}

• 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, …) je 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)

• 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)

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.

E → N

(N₁ + N₂) → N₃ kde N₃ = N₁+N₂

(N₁ * N₂) → N₃ kde N₃ = N₁ * N₂

E₁ → E₂

(E₃ + E₁) → (E₃ + E₂)

E₁ → E₂

(E₃ * E₁) → (E₃ * E₂)

E₁ → E₂

(E₁ + E₃) → (E₂ + E₃)

E₁ → E₂

(E₁ * E₃) → (E₂*E₃)

E → N

(N₁ + N₂) → N₃ kde N₃ = N₁ + N₂

(N₁ * N₂) → N₃ kde N₃ = N₁*N₂

E₁ →* N₁ , E₂ →* N₂ , N = N₁ + N₂

(E₁ + E₂) →* N

E₁ →* N₁ , E₂ →* N₂ , N = N₁ * N₂

(E₁* E₂) →* N

• [ [E]] = [ [N]]

• [ [N]] = N

• [ [ + ]] = +

• [ [*]] = *

• [ [E₁ + E₂]] = [ [E₁]] [ [ + ]] [ [E₂]]

• [ [E₁*E₂]] = [ [E₁]] [ [*]] [ [E₂]]

Máme výraz: (3 + (6 * (4 + 8)) + (4 * 8))

Při vyhodnocování postupujeme odspodu, bacha, mezi cisly s mezery neni znamenko, ta jsou rovnou vyhodnocena napr radek 4 8 jsou dve vetve : prvni: (char)4 →(int) 4 a druha: (char)8 →(int) 8

4 8

1. ——

6 (4 + 8)

1. ————

3 (6 * (4 + 8)) 4 8

1. —————— ——-

(3 + (6 * (4 + 8))) (4 * 8)

1. ——————————

¹⁾) + (4 * 8))

• R = P(PxDxUxHxMxP(S))

• 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)

• x2(D, H) = x3(D)*15+H funkce slouzici pro razeni hodin

• 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

malé epsilon - ε je prázdná množina a · je symbol zřetězení.

QSORT({A₁, A₂, …, A_n}) = QSORT(A|A ∈ {A₁, A₂, …, A_n} AND A < A₁)·A₁·QSORT(A|A ∈ {A₁, A₂, …, A_n} AND A > A₁) QSORT({}) = ε

• A = {A₁, A₂, …, A_n} - vstupní neseřazená množina
• B - výstupní seřazená množina

QSORT({}) = ε

QSORT(A) → B

znak ā neznamena nic podstatneho, jde jen o to, aby se rozlisily podmnoziny

B = QSORT(ā)·A₁·QSORT(a)

• ā ⊂ A, a ⊂ A
• x ∈ ā: x > A₁
• x ∈ a: x ≤ A₁ AND x != A₁

QSORT(A) → QSORT(ε, ε, A, A₁)

QSORT(A, B, C, p)

• QSORT(A·C₁, B, {C₂, C₃, …, C_n}, p) pokud C₁ ≤ p
• QSORT(A, B·C₁, {C₂, C₃, …, C_n}, p) pokud C₁ > p

QSORT(A, B, ε, p) = QSORT(ε, ε, A, A₁)·A₁·QSORT(ε, ε, B, B₁)

QSORT(ε, ε, ε, p) = ε

QSORT(A, ε, ε, p) → QSORT(ε, ε, A, A₁)

QSORT(ε, A, ε, p) → QSORT(A, ε, ε, p)

QSORT(A, B, ε, p) = A·QSORT(ε, ε, B, B₁) pokud length(A) = 1

QSORT(A, B, ε, p) = QSORT(ε, ε, A, A₁)·B pokud length(B) = 1

 MSORT({}) -> ε
 MSORT(A) -> A  if len(A) = 1

 MSORT(B)·MSORT(C) -> D pro všechny x ∈ B: pro všechny y ∈ C: x < y
 -----------------------------------------------------------
                    MSORT(A) -> D 

 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

• 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)

• 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

• a - je to rotace, vezmu prvek z vrcholu zásobníku a dám ho na konec
  1. je to rotace, vyjmu prvek (pop()) z vrcholu zásobníku a pokud je to cislo > 1 posunu prvek na vrcholu zasobniku (prvek hned za cislem, ktere jsem vyjmul) o N - 1 pozic dolu v zasobniku
• b - 432432
  1. IF(postfix 0 2 3 4 2 3 4 rot rot rot, [])
  2. = (2 3 4 2 3 4 rot rot rot, [])
  3. ⇒⁶ (rot rot rot, [4 3 2 4 3 2]) [num]
  4. ⇒ (rot rot, [2 4 3 3 2]) [rot] (4 > 1, posunu 3 o 3 dolu)
  5. ⇒ (rot, [3 3 4 2]) [rot] (2 > 1, posunu 4 o 1 dolu) nemělo by to tedy být [3 4 3 2] ?
  6. ⇒ (, [4 2 3]) [rot] (3 > 1, posunu 3 o 2 dolu)
  7. Odpoved je [4 2 3] pokud bychom pokracovali dal
  8. (, [4 2 3]) nalezi do FC a tedy muzeme OF(, [4 2 3]) = 4
• d - program by se zasekl na prázném zásobníku, např. (postfix 0 rot)
  1. (rot . Q, N . S) kde N neni cislo nebo N < 2 nebo |S| < N

//udělám jen velmi jednoduše pro mul
<mul.Q, e> -> <Q, 1>
<mul.Q, N> -> <Q, N> 

• 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,…}

• 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

• více operátorů zasebou můžeme vyřešit jednoduše op* a bude se vybírat ten poslední op_n
• je tam ale problém s = ten nevím jak vyřešit (něco s konstantou). Nápady?

• 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

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

• D : intLit → int D - převedeme na integer
• UN [ [@ UD D]] → 10 * [ [UD]] + [ [D]]
• SN [ [+ UD]] → [ [UD]]
• SN [ [- UD]] → -1 * [ [UD]]

• relaci pro výstupní funkci a význam denotační algebry si snad dokáže každej udělat sám