New Posts

content/blog/intensional-logic-extends-first-order.md

@@ -0,0 +1,23 @@
+---
+title: "Intensional Logic Extends First Order"
+date: 2022-02-26T20:33:38-05:00
+draft: false
+tags: []
+math: true
+---
+
+The second brightest object in the sky is known as the morgensteorra (morning star) and æfensteorra (evening star). Later on this object became known as Venus. [(Wikipedia)](https://en.wikipedia.org/wiki/Venus_in_culture)
+$$
+\text{morgensteorra} = \text{æfensteorra} = \text{venus}
+$$
+Gottlob Frege asks in 1892  whether we should make a distinction between a sense and a reference. [(SEP)](https://plato.stanford.edu/entries/logic-intensional/#Fre) [(Wikipedia)](https://en.wikipedia.org/wiki/Sense_and_reference)
+
+One might be tempted to think that traditional first order logic can handle this. To show how we'll need to extend it, let us think of this problem from a cognitive perspective. Lets say that we have a relation $B$ that stands for belief. Now lets say that an agent has a belief that Venus is the evening star.
+$$
+B(\text{æfensteorra} = \text{venus})
+$$
+In first order logic, we can then deduce the following:
+$$
+B(\text{morgensteorra} = \text{venus})
+$$
+But does that make sense? It is possible to hold a belief that Venus is the evening star while not holding a belief that Venus is the morning star. Therefore, we cannot treat belief as a traditional relation symbol. Issues like these give birth to intensional reasoning and from that modal logic.

content/blog/junit-script.md

@@ -0,0 +1,34 @@
+---
+title: "JUnit Script"
+date: 2022-02-26T20:02:53-05:00
+draft: false
+tags: ["Java"]
+math: false
+---
+
+Running a JUnit test on the terminal is a little annoying. Here is a quick script to make it easier, make it executable and drop it in [`~/.local/bin`](/blog/customexec/) for easy use.
+
+```bash
+#!/bin/sh
+
+set -o errexit
+set -o nounset
+set -o pipefail
+
+JUNIT_PATH="/usr/share/java/junit4.jar"
+
+show_usage() {
+    echo "Usage: junit [class file path]"
+    exit 1
+}
+
+# Check argument count
+if [ "$#" -ne 1 ]; then
+    show_usage
+fi
+
+java -cp "$JUNIT_PATH":. org.junit.runner.JUnitCore "$1"
+
+```
+
+ Replacing `JUNIT_PATH` with the location of the `junit4.jar` on your system.

content/blog/proving-loop-invariants.md

@@ -0,0 +1,91 @@
+---
+title: "Loop Invariants"
+date: 2022-02-26T19:17:21-05:00
+draft: false
+tags: []
+math: true
+---
+
+Loop invariants are one of the more complicated concepts in Hoare Logic. One might say that we can simply unroll the loop, but there are many loops where we don't know the number of iterations in advanced. Therefore, we often consider what is called the loop invariant. These are statements that are true before, during, and after the loop. A useful loop invariant in combination of the negation of the loop condition can also prove some postcondition. Lets look at a multiplication example
+
+```java
+int mul(int a, int b) {
+    int x = 0;
+    int p = 0;
+    while (p < b) {
+        x = x + a;
+        p = p + 1;
+    }
+}
+```
+
+## Choosing the Loop Invariant
+
+A useful postcondition in this case would be `x == a * b`. Which loop invariant would help us prove this? Often when crafting loop invariants I have two pieces of advice:
+
+- The loop invariant should involve some part of the postcondition
+- The loop invariant should involve the iterator
+
+For the example above, the loop invariant should be `x == a * p`.
+
+If you are using a verifier like Dafny, there are [additional invariants](/blog/dafny-loops/) you'll likely need to add.
+
+## Proving the Loop Invariant
+
+Often we'll use induction to prove the loop invariant. As a reminder induction has four steps:
+
+1. Show the base case holds.
+2. State the induction hypothesis.
+3. State the propositions from the code.
+4. Substitute (3) into (2) until the inductive step is proved. 
+
+Below is a proof for the loop invariant `x == a * p` using induction.
+
+Consider the base case `x = 0; p = 0`
+$$
+\begin{align*}
+x &== a * 0 \\\\
+0 &== 0 \checkmark
+\end{align*}
+$$
+Let us assume the inductive hypothesis holds. That is, `x_n = a * p_n`. Notice that `a` does not change during the loop so there is no need to add a subscript to it.
+
+Now we need to know what `x_n` and `p_n` are at any point during the loop. Looking at the code we come up with the following two propositions:
+$$
+p_{n + 1} == p_n + 1 \\\\
+x_{n + 1} == x_n + a
+$$
+Then solving for the nth iteration:
+$$
+p_n == p_{n + 1} - 1 \\\\
+x_n == x_{n + 1} - a
+$$
+We can then plug that into our inductive hypothesis and simplify.
+$$
+\begin{align*}
+x_n &== a * p_n \\\\
+x_{n + 1} - a &== a * (p_{n + 1} - 1) \\\\
+x_{n + 1} - a &== a * p_{n + 1} - a \\\\
+x_{n + 1} &== a * p_{n + 1} \checkmark
+\end{align*}
+$$
+With that we've proved using induction that our loop invariant holds.
+
+## Proving the Postcondition
+
+To show that a postcondition holds, we need to show that the loop invariant and the negation of the loop condition imply the postcondition.
+$$
+(x_n == a * p_n) \wedge \neg(p < b) \implies_? x == a * b
+$$
+Simplifying...
+$$
+(x_n == a * p_n) \wedge \neg(p < b) \\\\
+\implies (x_n == a * p_n) \wedge (p \ge b) \\\\
+\implies (x_n \ge a * b)
+$$
+We need another loop invariant to show us that $p$ would never be greater than $b$. That is $0 \le p \le b$. That gives us:
+$$
+(x_n == a * p_n) \wedge (p \ge b) \wedge (p \le b) \\\\
+ \implies (x_n == a * p_n) \wedge (p == b) \\\\
+ \implies (x_n == a * b) \checkmark \\
+$$