Huh? We're on day 8? What happened to days 2 through 7?
Well, for the most part, I didn't think they were that interesting from the Coq point of view.
Day 7 got close, but not close enough to inspire me to create a formalization. Day 8, on the other
hand, is
{{<sidenote"right""pl-note""quiteinteresting,">}}
Especially to someone like me who's interested in programming languages!
{{</sidenote>}} and took quite some time to formalize.
As before, here's an (abridged) description of the problem:
> Given a tiny assembly-like language, determine the state of its accumulator
> when the same instruction is executed twice.
Before we start on the Coq formalization, let's talk about an idea from
Programming Language Theory (PLT), _big step operational semantics_.
### Big Step Operational Semantics
What we have in Advent of Code's Day 8 is, undeniably, a small programming language.
We are tasked with executing this language, or, in PLT lingo, defining its _semantics_.
There are many ways of doing this - at university, I've been taught of [denotational](https://en.wikipedia.org/wiki/Denotational_semantics), [axiomatic](https://en.wikipedia.org/wiki/Axiomatic_semantics),
and [operational](https://en.wikipedia.org/wiki/Operational_semantics) semantics.
I believe that Coq's mechanism of inductive definitions lends itself very well
to operational semantics, so we'll take that route. But even "operational semantics"
doesn't refer to a concrete technique - we have a choice between small-step (structural) and
big-step (natural) operational semantics. The former describe the minimal "steps" a program
takes as it's being evaluated, while the latter define the final results of evaluating a program.
I decided to go with big-step operational semantics, since they're more intutive (natural!).
So, how does one go about "[defining] the final results of evaluating a program?" Most commonly,
we go about using _inference rules_. Let's talk about those next.
#### Inference Rules
Inference rules are a very general notion. The describe how we can determine (infer) a conclusion
from a set of assumption. It helps to look at an example. Here's a silly little inference rule:
{{<latex>}}
\frac
{\text{I'm allergic to cats} \quad \text{My friend has a cat}}
{\text{I will not visit my friend very much}}
{{</latex>}}
It reads, "if I'm allergic to cats, and if my friend has a cat, then I will not visit my friend very much".
Here, "I'm allergic to cats" and "my friend has a cat" are _premises_, and "I will not visit my friend very much" is
a _conclusion_. An inference rule states that if all its premises are true, then its conclusion must be true.
Here's another inference rule, this time with some mathematical notation instead of words:
{{<latex>}}
\frac
{n <m}
{n + 1 <m+1}
{{</latex>}}
This one reads, "if \\(n\\) is less than \\(m\\), then \\(n+1\\) is less than \\(m+1\\)". We can use inference
rules to define various constructs. As an example, let's define what it means for a natural number to be even.
It takes two rules:
{{<latex>}}
\frac
{}
{0 \; \text{is even}}
\quad
\frac
{n \; \text{is even}}
{n+2 \; \text{is even}}
{{</latex>}}
First of all, zero is even. We take this as fact - there are no premises for the first rule, so they
are all trivially true. Next, if a number is even, then adding 2 to that number results in another
even number. Using the two of these rules together, we can correctly determine whether any number
is or isn't even. We start knowing that 0 is even. Adding 2 we learn that 2 is even, and adding 2
again we see that 4 is even, as well. We can continue this to determine that 6, 8, 10, and so on
are even too. Never in this process will we visit the numbers 1 or 3 or 5, and that's good - they're not even!
Let's now extend this notion to programming languages, starting with a simple arithmetic language.
This language is made up of natural numbers and the \\(\square\\) operation, which represents the addition
Whereas the set of "visited" program counters keeps growing as our evaluation continues,
the set of "allowed" program counters keeps shrinking. Because the "allowed" set never stops shrinking,
assuming we're starting with a finite set, our execution will eventually terminate.
{{</sidenote>}}
Now we have all the elements of our evaluation. Let's define some notation. A program starts at some state,
and terminates in another, possibly different state. In the course of a regular evaluation, the program
never changes; only the state does. So I propose this (rather unorthodox) notation:
{{<latex>}}
(c, a, v) \Rightarrow_p (c', a', v')
{{</latex>}}
This reads, "after starting at program counter \\(c\\), accumulator \\(a\\), and set of valid addresses \\(v\\),
the program \\(p\\) terminates with program counter \\(c'\\), accumulator \\(a'\\), and set of valid addresses \\(v'\\)".
Before creating the inference rules for this evaluation relation, let's define the effect of evaluating a single
instruction, using notation \\((c, a) \rightarrow_i (c', a')\\). An addition instruction changes the accumulator,
and increases the program counter by 1.
{{<latex>}}
\frac{}
{(c, a) \rightarrow_{\texttt{add} \; n} (c+1, a+n)}
{{</latex>}}
A no-op instruction does even less. All it does is increment the program counter.
{{<latex>}}
\frac{}
{(c, a) \rightarrow_{\texttt{nop} \; n} (c+1, a)}
{{</latex>}}
Finally, a jump instruction leaves the accumulator intact, but adds a number to the program counter itself!
{{<latex>}}
\frac{}
{(c, a) \rightarrow_{\texttt{jmp} \; n} (c+n, a)}
{{</latex>}}
None of these rules have any premises, and they really are quite simple. Now, let's define the rules
for evaluating a program. First of all, a program starting in a state that is not considered "valid"
is done evaluating, and is in a "failed" state.
{{<latex>}}
\frac{c \not \in v \quad c \not= \text{length}(p)}
{(c, a, v) \Rightarrow_{p} (c, a, v)}
{{</latex>}}
We use \\(\\text{length}(p)\\) to represent the number of instructions in \\(p\\). Note the second premise:
even if our program counter \\(c\\) is not included in the valid set, if it's "past the end of the program",
the program terminates in an "ok" state. Here's a rule for terminating in the "ok" state:
{{<latex>}}
\frac{c = \text{length}(p)}
{(c, a, v) \Rightarrow_{p} (c, a, v)}
{{</latex>}}
When our program counter reaches the end of the program, we are also done evaluating it. Even though
both rules {{<sidenote"right""redundant-note""leadtothesameconclusion,">}}
In fact, if the end of the program is never included in the valid set, the second rule is completely redundant.
{{</sidenote>}}
it helps to distinguish the two possible outcomes. Finally, if neither of the termination conditions are met,
our program can take a step, and continue evaluating from there.
{{<latex>}}
\frac{c \in v \quad p[c] = i \quad (c, a) \rightarrow_i (c', a') \quad (c', a', v - \{c\}) \Rightarrow_p (c'', a'', v'')}
{(c, a, v) \Rightarrow_{p} (c'', a'', v'')}
{{</latex>}}
This is quite a rule. A lot of things need to work out for a program to evauate from a state that isn't
currently the final state:
* The current program counter \\(c\\) must be valid. That is, it must be an element of \\(v\\).
* This program counter must correspond to an instruction \\(i\\) in \\(p\\), which we write as \\(p[c] = i\\).
* This instruction must be executed, changing our program counter from \\(c\\) to \\(c'\\) and our
accumulator from \\(a\\) to \\(a'\\). The set of valid instructions will no longer include \\(c\\),
and will become \\(v - \\{c\\}\\).
* Our program must then finish executing, starting at state
\\((c', a', v - \\{c\\})\\), and ending in some (unknown) state \\((c'', a'', v'')\\).
If all of these conditions are met, our program, starting at \\((c, a, v)\\), will terminate in the state \\((c'', a'', v'')\\). This third rule completes our semantics; a program being executed will keep running instructions using the third rule, until it finally
hits an invalid program counter (terminating with the first rule) or gets to the end of the program (terminating with the second rule).