Newbie question: In HOL Light (or in another variant of HOL if that has
an easier answer), how should I define permutations of {0,1,...,n-1}?
The context I'm starting from is that a "Benes network" is a particular
map from fixed-length bit sequences to permutations of {0,1,...,n-1}
when n is a power of 2. It starts with conditionally swapping 0<->1,
2<->3, etc., then 0<->2 etc., continuing up and then down powers of 2.
I've written detailed proofs for a fast parallel algorithm that computes
suitable bits given a permutation. I'm trying to figure out how easily
these proofs can be computer-verified with current tools.
The definition of a Benes network is most easily expressed in terms of
{0,1,...,n-1}. The algorithm has special roles for the even and odd
elements of {0,1,...,n-1}, and uses comparisons to compute the minimum
element of each cycle of a permutation, and then in the recursion
divides indices by 2, so it seems pointless to generalize beyond
{0,1,...,n-1}; the numbers have useful roles here.
So far the four answers I've found that seem to be local minima in the
"how complicated is the theorem statement" metric are the following:
* Follow the usual mathematical definition, where a permutation of X
is a function from X to X having an inverse. My understanding is
that HOL variants generally don't support dependent types such as
{0,1,...,n-1} depending on n; ergo, set-theoretically build these
functions as subsets of num^2 satisfying certain conditions, define
compositions of such functions, and define inverses.
* Reformulate the theorems as being about permutations of any set X
that has a specified bijection to {0,...,n-1}. I see that there's
machinery _sort of_ handling this, the arbitrary $ bijection from
{1,...,dimindex(:X)} to X when X is finite, and it's not a big deal
to shift the indices by 1; but an arbitrary bijection is not a
specified bijection, so matching this up to (say) software would
then require another step to invert the arbitrary bijection. More
to the point, whether it's specified or arbitrary, the bijection is
making the theorem statement conceptually more complicated.
* Describe permutations as lists satisfying certain conditions, as in
Permutation/permutation.ml. This is a good match to the simplest
software representation of a permutation as a list of its values,
but again it seems to require separately defining composition etc.
In set theory I'd expect the list (pi(0),pi(1),...,pi(n-1)) to be
defined as the function x|->pi(x), which is exactly pi, and I don't
terribly mind setting this up as a correspondence instead of an
identity, but again the function wants the type {0,1,...,n-1}.
* The applications I have in mind actually need only specific values
of n such as n=8192. I understand that for each specific n I can
build an explicit type with n elements, and then unroll the
recursion across n. This would require the basic features of
integers to be replicated across each of the explicit types.
My objective here is high assurance, so I like what HOL Light and HOL
Zero say about small kernels increasing the assurance level for the
proofs, but I also want high assurance that the theorem statements are
what's desired. Even a complete chain of
* verifying that an algorithm computes b |-> Benes(b),
* verifying that software implements this algorithm,
* verifying that an algorithm computes pi |-> Bits(pi),
* verifying that software implements this algorithm, and
* verifying that Benes(Bits(pi)) = pi
would merely say that the composition of the two software pieces
computes pi |-> pi _if_ pi is the software view of whatever is defined
as a permutation---but what if, as an extreme, that definition turns out
to be vacuous? Okay, the reader would then check that some software
inputs satisfy the hypotheses, and I could add something like
* verifying that sorting any (i_0,0),(i_1,1),...,(i_{n-1},n-1)
produces values of a permutation in the second coordinate,
but what I really want is for errors to be caught earlier in the
process, which I think wants the mathematical concept of a permutation
on {0,1,...,n-1} as a function, which in turn seems to want dependent
types or replacing type theory with set theory.
Am I missing simpler ways to handle this in HOL Light?
---Dan
P.S. I noticed that on Debian bullseye the hol-light package is broken,
and the repo version is also broken (ending with "Unbound value
theorems"), apparently because it doesn't deal with some sort of ocaml
instability. On Debian stretch the package and repo version both work.
The size and instability of ocaml make me want to export the proofs to a
simpler verifier, but I gather from https://arxiv.org/pdf/2005.03089.pdf
that this isn't super-easy.
signature.asc
Description: PGP signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
