This commit is contained in:
Michael Zhang 2024-06-05 10:23:33 -04:00
parent ecb3ad58e3
commit 2a2e7d279b
2 changed files with 162 additions and 1 deletions

BIN
silva/lec2.jpg Normal file

Binary file not shown.

After

Width:  |  Height:  |  Size: 706 KiB

View file

@ -6,6 +6,7 @@
#let tru = $"true"$ #let tru = $"true"$
#let fls = $"false"$ #let fls = $"false"$
#let star(x) = $#x^*$
== Lecture 1 == Lecture 1
@ -329,4 +330,164 @@ Subset of $K$: $(B, 0, 1, +, ;, overline((..)))$ is a boolean algebra. _Sub-alge
This is only true of language without effects or concurrency. This is only true of language without effects or concurrency.
- Threads can be reasoned about in a partially distributive commutative lattice - Threads can be reasoned about in a partially distributive commutative lattice
#image("lec2.jpg")
#pagebreak()
== Lecture 3
- _what is the semantics of $K A(T)$_?
- Examples (such as how to tell if while loops are the same)
- Net KAT (syntax and examples)
Two types of semantics for Kleene algebra are the denotational semantics and the operational semantics.
Having a conversion between both representations lets you pick the best of both worlds.
- Denotational better for describing the gist of the language
- Operational better for implementation
=== KAT syntax
- $e ::= 0 | 1 | p in P | e + e | e ; e | star(e) | b in B$
- b is read "assert b", a kind of test
- $b ::= t in T | 0 | 1 | b or b | b and b | overline(b)$
- split alphabet $A$ into two parts, $T union.plus P$ where $T$ describes the basic tests
- this is embedded in the programs part
After writing down assertion, everything after the assertion can be assumed to be true.
If you have $alpha :equiv t_1 overline(t_2) t_3 ... overline(t_1) t_2 overline(t_3) ...$ including all basic tests $t$ and their complements this is considered a _full test_.
For example, if $t_1 t_2 overline(t_1) overline(t_2)$, then there are 4 options for $alpha$:
- $alpha_0 :equiv t_1 t_2$
- $alpha_1 :equiv t_1 overline(t_2)$
- $alpha_2 :equiv overline(t_1) t_2$
- $alpha_3 :equiv overline(t_1) overline(t_2)$
Any other expression is a subset of this full test, $2^T$. So the semantics of booleans is $db(b) equiv 2^(2^T)$
Interleave programs between atoms, used to be $star(A)$, now $star((A t ; P)) ; A t$. There is an option of where to refine the $P$. So now we have:
#rect[$db(e) : 2^star((A t ; P)) ; A t$]
Also, $db(b) = {alpha | alpha <= b}$ (boolean satisfiability). For example, $t_1 t_2 <= t_1$ and $t_1 t_2 <= t_2$ but it doesn't $<= overline(t_2)$.
Also $db(p) = {alpha p beta | alpha_1 beta in A t}$. With $p$ uninterpreted, we only know that $p$ can transform any $alpha$ into any $beta$
- $db(e + f) equiv db(e) union db(f)$
- $db(e \; f) equiv db(e) diamond.small db(f)$
- $alpha_0 p_0 alpha_k diamond.small beta_0 ...$ the $alpha_k diamond.small beta_0$ must match.
Otherwise the program cannot continue; this operation is undefined.
Then it deletes the repeated atoms so it is the same.
(Because $alpha$ and $beta$ are atoms, they are not expressions that can contain other atoms so it's based on exact matching)
- Star is the same as before, but also using the diamond
=== KAT Example
For $ifthenelse(b,p,q)$ which is $b;p+overline(b);q$:
$&db(ifthenelse(b,p,q)) \
equiv &db(b\;p) union db(overline(b\;q)) \
equiv & db(b) diamond.small db(p) union ... \
equiv & {alpha | alpha <= b } diamond.small {alpha p beta | alpha beta in A t} union ... \
equiv & {alpha p beta | alpha <= b} union {alpha q beta | alpha <= overline(b)}
$
The semantics of this expression has 2 types of traces.
One where I start in b, where $p$ is executed.
Another is where I started in a state where the condition $b$ is false, so I executed the $q$ branch.
For $"while" b "do" p$ which is $star((b ; p)) ; overline(b)$
$&db("while" b "do" p) \
equiv & { beta , alpha_0 p beta , alpha_0 p alpha_1 p beta , ... | alpha_i <= b, beta <= overline(b)}$
For traces that don't terminate: $"while true do skip" equiv 0$. (there are alternate semantics where you record infinite traces) With non-termination, your observation power is 0.
=== Connection to Hoare triples
For ${b} C {c}$, the validity of the Hoare triple is the same thing as the KAT equation $b C overline(c) equiv 0$ (filtering out all the postconditions that render the condition false would result in empty)
Another one is $b C <= C c$. This is equivalent to the previous one #TODO Show this
=== Exercise solutions
$star(x + y) equiv star((star(x) y)) star(x)$
Need to prove it in two steps, $<=$ and $>=$:
- Use the fixpoint rule: $1 <= star((star(x) y)) star(x)$.
- This is true because $1 <= star(x)$ for any $x$
- $x star(x) star((y star(x))) <= star(x) star((y star(x)))$.
- This uses the fact that $x star(x) <= star(x)$.
- This is true because unfold the star to get $x star(x) <= 1 + x star(x)$
- $star((y star(x))) star((y star(x))) <= star((y star(x))) <= star(x) star((y star(x)))$
- $1 <= star(x)$, so add this to both sides
- Taking the sum of the previous 3 things: $1 + (x+y) star(x) star((y star(x))) <= star(x) star((y star(x)))$
- let $cal(x) = star(x) star((y star(x)))$. THen $1 + (x + y) cal(x) <= cal(x)$
- Apply fix point rule here: $star((x + y)) <= star(x) star((y star(x)))$
=== Summary
- Soundness + Completeness (KA + BA) are all you need to prove that 2 programs are equivalent
- Automaton model is where transitions are (atoms ; programs) and the final state is what atoms to validate. This is known as a KAT automaton.
- Equivalece of these automata is decidable, using BDDs (Pous), matrices (Kozen) and these are all $in$ PSPACE.
- Some of these algorithms are very efficient despite PSPACE and they use the Union-find datastructure (Hopcroft, Tarjan)
- $O(n log_c n)$ where $c$ is the inverse of the ackermann function, so the log part is _very_ small (in fact the original conjecture was that it was linear)
- Improvement "Coinduction up-to" on NFA, DFA, Brz. derivatives, can improve the theoretical limit (?)
=== While loop example
#table(
columns: (1fr, 1fr),
```
while a do
p;
while c do
q;
```,
```
if b then
p;
while b or c do
if c then
q;
else
p;
```,
$star((b p star((c q)) overline(c))) b$,
$b ; p ; star(((b + c) (c q + overline(c) p))) overline(b) overline(c) + overline(b)$
)
Show these are the same by applying denesting and sliding.
=== Net KAT
Net KAT is a special KAT. Think of networks as boxes the only thing they can do is get packets in, change something about the packet, and then sends the packet on.
Packets are records of fields $f_1, ..., f_k$ mapping to values $v_1, ..., v_k$. Program actions ($p = f arrow.l n$) and tests ($f = n$) come in pairs.
For example:
#quote(block: true)[
Sw - switch \
Type - { SSH, ... } \
Pt - port \
Dst - destination
$("Sw" = 2); ("Type" = "SSH"); ("Pt" <- 4) ; ("Dst" <- "10.2.10.2")$
For any packet that comes in, it filters using the test. If they pass the test, then you can set the fields on them.
Using KAT, you can perform network reachability.
]