[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] lexigraphical ordering

Hi Dave,

This seems like a reasonable request.  I discussed it with Shankar, and
it looks like there are two things needed: a term-ordering function for
PVS terms, and a hook into auto-rewrite that allows a lexicographic
ordering condition on a given rewrite.  I imagine auto-rewrite would
take an extra argument, e.g.,
 (auto-rewrite "foo" :lex-order ("a" "b"))
Which would only trigger the rewrite if the term substituted for "a" was
smaller than the term for "b".

We discussed allowing any lisp function to be given as a filter, but
right now all dependencies on lisp function calls in proofs (e.g., using
'if' or 'let') can be replaced by primitive proof steps not involving
calls to arbitrary lisp functions.  This is why in principle one only
has to believe in the soundness of the primitive rules.  If we allow
arbitrary lisp code as filters, then it would need to be invoked in
order to rerun the proof from primitive rules, and the issue of
soundness then extends to this code.

I started writing a lexical-ordering function for PVS terms a while
back, but got interrupted.  It shouldn't be too difficult to finish.
I don't think the modification to auto-rewrite would be too

Does this sound like what you have in mind?


<dagreve@rockwellcollins.com> wrote:

> Is there any way to suggest or impose a lexigraphical ordering
> on PVS terms?  Perhaps using strategies?
> I would like to apply a rule such as:
> set(a,set(b,x)) = set(b,set(a,x))
> but only if I can establish that 'a' is somehow smaller than 'b'.
> I would like to avoid a logical ordering, as that seems to lead
> to excessive case-splitting.
> Dave Greve