Re: [Hol-info] permutations of {0,1,...,n-1}

[John R H. <jr...@gm...>]

Hi Dan,

| 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}?

There are a couple of HOL Light library files defining notions of
permutation, the first giving permutations on sets:

        Library/permutations.ml

and the second giving permutations on lists

        Permutations/*.ml

In your application I think the set one may be more relevant. This
tries to get a somewhat natural and well-behaved notion while sticking
to total functions (exactly the problematic issue you noted). This
is done by specifying that the function be the identity outside the
"domain". Thus, the main notion  is "p permutes s", defined as:

  p permutes s <=> (!x. ~(x IN s) ==> p(x) = x) /\ (!y. ?!x. p x = y)

For example, you could say in your setting

  p permutes {i:num | i < n}

or if you don't mind offsetting the indices:

  p permutes (1..n)

Alas "p permutes (0..n-1)" doesn't quite mean what one might hope
in the case n=0 since subtraction over N gives 0-1=0. One could use
Z instead as the indexing type but this looks uglier and has less
pre-proved machinery about number segments. Or maybe you never
want n-0 anyway, in which case it's fine.

John.


On Wed, Sep 9, 2020 at 3:10 AM D. J. Bernstein <dj...@ma...> wrote:

> 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.
> _______________________________________________
> hol-info mailing list
> hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info
>