Term ordering for permutative rewriting

[msaaltink]

This issue is a reminder that there should be a more careful choice of term ordering in support of permutative rewriting.

PR GaloisInc/saw-core#173 adds very preliminary support for rewriting with permutative rules. A rule is "permutative" if the left and right sides are instances of one another, as in, for example, a commutative law \ x y -> f x y == f y x. Prior to this PR, the SAW rewriter would enter an infinite loop when applying this rule, then applying it again, and again ad infinitum. The PR breaks this loop; an ordering relation is used to decide whether to apply the rule or not.

Permutative rules are supported in many other proof systems, e.g. ACL2 and Isabelle. Isabell allows the user to select an ordering; some examples are in https://github.com/isabelle-prover/mirror-isabelle/blob/master/src/Pure/term_ord.ML.

The current ordering looks at the "fringe" of arguments in possibly-nested calls to a function; specifically, for a call f x1 ... xn or f (x1, x2 , ..., xn) the fringe is the concatenation of the fringes of all the x_i, if f is the top-level function, and otherwise is a singleton list of the term itself. So the fringe of f (f a b) (g c) is [a, b, g c]. A permutative rule is applied iff the fringe of the replacement term is less than the fringe of the original term, using SAW's existing ordering on terms.

This ordering has one thing going for it: the user can associate to the right or to the left, as desired, and still have a rewrite rule for commutativity. That's because reassociating does not change the fringe. Its major flaw is the lack of any theory behind it.

[msaaltink]

The term ordering is not always a success. Here's a simplification of a case that came up recently

let {{
  type F t = { f: t -> t -> t }
  F0: F Integer
  F0 = { f = (+) }
  add: {t} F t -> t -> t -> t
  add R x y =  R.f x y
  }};

F0_laws  <- for
  [ {{ \ x y -> add F0 x y == add F0 y x }} // commutative
  , {{ \ x y z -> add F0 (add F0 x y) z == add F0 x (add F0 y z) }} // associative
  , {{ \ x y z -> add F0 x (add F0 y z) == add F0 y (add F0 x z) }} // commutative, again
  ] (prove_print z3);

prove do { simplify (addsimps F0_laws empty_ss); print_goal; w4_unint_z3 ["F0"]; }
    {{ add F0 (add F0 3 1) 2 == add F0 1 (add F0 3 2) }} ;

That prove goes into an infinite loop. I think the issue is the extra parameters of the function, here both a type and a record.

Recall that the associative law is not permutative, so it is important that it does not rewrite a term to something larger in the term order. The "fringe" idea was supposed to make that so, but here it fails: the fringe for the LHS is [Integer, F0, Integer, F0, x, y, z] and for the RHS is [Integer, F0, x, Integer, F0, y, z]. That's not the same, and if Integer is a smaller term than x, the LHS is smaller than the RHS.

So, when the simplify step happens, we eventually get the term add F0 1 (add F0 2 3) with fringe [Integer, F0, 1, Integer, F0, 2, 3] which commutativity might rewrite to add F0 (add F0 2 3) 1 with fringe [Integer, F0, Integer, F0, 2, 3, 1]. Evidently, Integer is less than 1 in the term order, so we commute to the right-associated form, and then the associative law reassociates it to the right.

Isabelle's term_ord ordering would be an improvement, so long as we right-associate, as then the associative law always makes a term smaller.