Make more progress on Coq post.

This commit is contained in:
Danila Fedorin 2021-01-01 18:39:30 -08:00
parent 60eb50737d
commit 6f92a50c83

View File

@ -274,3 +274,84 @@ and will become \\(v - \\{c\\}\\).
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).
#### Aside: Vectors and Finite \\(\mathbb{N}\\)
We'll be getting to the Coq implementation of our semantics soon, but before we do:
what type should \\(c\\) be? It's entirely possible for an instruction like \\(\\texttt{jmp} \\; -10000\\)
to throw our program counter way before the first instruction of our program, so at first, it seems
as though we should use an integer. But the prompt doesn't even specify what should happen in this
case - it only says an instruction shouldn't be run twice. The "valid set", although it may help resolve
this debate, is our invention, and isn't part of the original specification.
There is, however, something we can infer from this problem. Since the problem of jumping "too far behind" or
"too far ahead" is never mentioned, we can assume that _all jumps will lead either to a valid instruction,
or right to the end of a program_. This means that \\(c\\) is a natural number, with
{{< latex >}}
0 \leq c \leq \text{length}(p)
{{< /latex >}}
In a language like Coq, it's possible to represent such a number. Since we've gotten familliar with
inference rules, let's present two rules that define such a number:
{{< latex >}}
{n \in \mathbb{N}^+}
{Z : \text{Fin} \; n}
{f : \text{Fin} \; n}
{S f : \text{Fin} \; (n+1)}
{{< /latex >}}
This is a variation of the [Peano encoding]( of natural numbers.
It reads as follows: zero (\\(Z\\)) is a finite natural number less than any positive natural number \\(n\\). Then, if a finite natural number
\\(f\\) is less than \\(n\\), then adding one to that number (using the successor function \\(S\\))
will create a natural number less than \\(n+1\\). We encode this in Coq as follows
([originally from here](
Inductive t : nat -> Set :=
| F1 : forall {n}, t (S n)
| FS : forall {n}, t n -> t (S n).
The `F1` constructor here is equivalent to our \\(Z\\), and `FS` is equivalent to our \\(S\\).
To represent positive natural numbers \\(\\mathbb{N}^+\\), we simply take a regular natural
number from \\(\mathbb{N}\\) and find its successor using `S` (simply adding 1). Again, we have
to explicitly use `forall` in our type signatures.
We can use a similar technique to represent a list with a known number of elements, known
in the Idris and Coq world as a vector. Again, we only need two inference rules to define such
a vector:
{{< latex >}}
{t : \text{Type}}
{[] : \text{Vec} \; t \; 0}
{x : \text{t} \quad \textit{xs} : \text{Vec} \; t \; n}
{(x::\textit{xs}) : \text{Vec} \; t \; (n+1)}
{{< /latex >}}
These rules read: the empty list \\([]\\) is zero-length vector of any type \\(t\\). Then,
if we take an element \\(x\\) of type \\(t\\), and an \\(n\\)-long vector \\(\textit{xs}\\) of \\(t\\),
then we can prepend \\(x\\) to \\(\textit{xs}\\) and get an \\((n+1)\\)-long vector of \\(t\\).
In Coq, we write this as follows ([originally from here](
Inductive t A : nat -> Type :=
| nil : t A 0
| cons : forall (h:A) (n:nat), t A n -> t A (S n).
The `nil` constructor represents the empty list \\([]\\), and `cons` represents
the operation of prepending an element (called `h` in the code in \\(x\\) in our inference rules)
to another vector of length \\(n\\), which is remains unnamed in the code but is called \\(\\textit{xs}\\) in our rules.
These two definitions work together quite well. For instance, suppose we have a vector of length \\(n\\).
If we were to access its elements by indices starting at 0, we'd be allowed to access indices 0 through \\(n-1\\).
These are precisely the values of the finite natural numbers less than \\(n\\), \\(\\text{Fin} \\; n \\).
Thus, given such an index \\(\\text{Fin} \\; n\\) and a vector \\(\\text{Vec} \\; t \\; n\\), we are guaranteed
to be able to retrieve the element at the given index! In our code, we will not have to worry about bounds checking.