recents

src/dependently_typed_languages/coq/program_verification.md

@@ -4,9 +4,16 @@ We finished `Imp.v` knowing:
 1. We can write fixpoints (total functions) for `aeval` and `beval`,
 2. However, `ceval` can not be a fixpoint, since 
 there is no way of totally unfolding a while expression.
-3. The solution is to write `ceval` as a relation (not even a function).
-In Coq, this means to make `ceval`'s result a `Prop`, which is allowed
-to not terminate.
+3. The solution is to write `ceval` as a relation.
+In Coq, we construct `ceval` as an inductive proposition: `ceval`'s result is a `Prop`, which is allowed
+to never terminate.
+4. Although `ceval` is defined as a relation, it is in fact a partial function. This is captured in the following theorem:
+```coq
+Theorem ceval_deterministic: forall c st st1 st2,
+     st =[ c ]=> st1  ->
+     st =[ c ]=> st2 ->
+     st1 = st2.
+```
 
 `Prop`s can be thought of in many ways:
 1. In the lens of decidability, `Prop` is a vaguer `Bool`: If the `Prop`
@@ -19,7 +26,7 @@ we would need a dependent pair, which is a `Type`: `Definition fooable P := {b :
 3. In the lens of extractability. `Prop`s get erased during Coq extraction.
 
 Since `ceval` is not a fixpoint, the property that two cprograms are the same
-becomes not so obvious. We need this: Two commands are behaviorally equivalent
+(call it `cequiv`) becomes less obvious: Two commands are behaviorally equivalent
 if, for any starting state, they either both diverge and they both terminate in the
 same final state.
 
@@ -29,11 +36,11 @@ Definition cequiv (c1 c2 : com) : Prop :=
     (st =[ c1 ]=> st') <-> (st =[ c2 ]=> st').
 ```
 
-Implications capture the divergence possibility. Since, a divergent program `c` 
+Implications capture the scenario where both programs diverge. Since, a divergent program `c` 
 has the precise property of
 ```coq
 forall (st st' : state),
-  ~ (st =[ c ]=> st')å
+  ~ (st =[ c ]=> st')
 ```
 
 We can now prove behavioral equivalences between different programs. Here is one such interesting 
@@ -71,4 +78,61 @@ This showcases just one embedding: The embedding of smaller programs into a larg
 There are five constructors that builds larger programs out of smaller ones: `E_Seq`, `E_WhileTrue`, `E_WhileFalse`,
 `E_IfTrue` and `E_IfFalse`. We need to show congruence for each of these separately.
 
-TODO: Though `ceval` is a relation, it is a partial function! But what if we add non-determinism to it?
+### Extension 1: Non-determinism
+
+As of now, our language Imp has a deterministic, partial evaluation function.
+The struggle thus far has been in wrestling with this partiality. Proving
+program equivalence is not a simple `reflexivity` call. Instead,
+we must use `ceval`'s constructors.
+
+Let's complicate the picture even more: What if we added non-determinism 
+to Imp? This is a realistic feature of programming languages. For example,
+
+```c
+x = 0;
+f(++x, x);
+```
+This demonstrates an undefined behavior in C: The order in which function
+arguments are evaluated is unspecified.
+The compiler could choose to evaluate either of the arguments first
+depending on which is more optimized on the target machine.
+So, `f` could be invoked with either `f(1, 1)` or `f(1, 0)`.
+
+Evidently, we can't model such nondeterminism in our language Imp yet.
+To support general nondeterminism, we add a `HAVOC` keyword, such that after 
+executing the program
+```
+HAVOC Y;
+Z := Y * 2
+```
+the value of [Y] can be *any* number, while the value of [Z] is
+twice that of [Y].
+
+Question: How should we extend `Inductive ceval` to build a havoc
+command?
+
+Answer: We allow `x` to take on any value after `havoc x`. So
+our definition uses a `forall n`:
+
+```coq
+| E_Havoc : forall st n x,
+    st =[ havoc x ]=> (x !-> n ; st)
+```
+
+In Imp, some programs always terminate and some programs always diverge.
+But in our new language which we call Himp, some programs can
+nondeterministically terminate in some runs and diverge in others.
+
+A simpler program demonstrating this spirit is `p5`:
+
+```coq
+Definition p5 : com :=
+  <{ while X <> 1 do
+       havoc X
+     end }>.
+```
+
+(TODO: I don't think this is true...)
+Behaviorally, `p5` actually always terminates since there is a 
+nonzero probability of assigning `X := 1`. But, the "sometimes terminate and sometimes diverge" 
+trait can be seen in each iteration of the loop.

src/smt_solvers/front.md

@@ -35,6 +35,10 @@ Satisfiability: $ \set{p_1, \dots, p_n} $ is satisfiable if and only if for some
 The two branches of logic are systematically related. Most languages have syntactic 
 and semantic concepts that coincide exactly ($\vdash$ corresponds to $\vDash$) — such an axiom system is said to be complete.
 
+### A solid example of proof theory vs model theory
+
+
+
 ### 1.2 Syllogism -> Boolean
 ```admonish info title="Take away one thing"
 Boole married algebra into logic, ending the two millennium reign of Aristotelian syllogisms.