LP, the Larch Prover -- Registered orderings: status

The status of an operator determines which of its arguments is given the most weight when using a registered ordering to orient an equation containing that operator into a provably terminating rewrite rule.


<status-constraint> ::= status <status> <operator>+[,]
<status>            ::= left-to-right | right-to-left | multiset
Note: The word status and the <status> can be abbreviated.


status left-to-right f, g
status multiset +


LP assigns a status to operators, if necessary, when using a registered ordering to orient equations into rewrite rules. Users can assign a status to an operator with the register status command.

The left-to-right and right-to-left statuses are called lexicographic statuses. The assign more weight, respectively, to the leftmost or rightmost arguments of an operator. They are useful when orienting the associativity equation f(f(x,y),z) = f(x,f(y,z)). If f has left-to-right, this equation would be oriented from left to right. If f has right-to-left status, it would be would be oriented from right to left.

The multiset status is appropriate for ac and commutative operators, because it gives all arguments equal weight.

The dsmpos ordering is defined on terms containing an operator without a defined status if the ordering would produce the same results no matter what status was given to that operator. This property allows LP or the user to define the status of an operator without invalidating the proof of termination for previously oriented rewrite rules.