LP, the Larch Prover -- Registered orderings: height

Height constraints define a partial ordering on operators that induces a partial ordering on terms. This ordering, along with status constraints, is used by LP's registered orderings to orient equations into provably terminating sets of rewrite rules.

Syntax

<height-constraint> ::= height <operator-set> ( <height> <operator-set> )+
                           | ( bottom | top ) <operator>+[,]
<height>            ::= > | = | >=
<operator-set>      ::= <operator> | "(" <operator>+[,] ")"

Note: The first word in a <height-constraint> can be abbreviated.

Examples

height f > g
height => > (/\, \/) > true = false
bottom f

Usage

The height constraint f > g suggests that terms involving f are ``more complicated,'' and should be rewritten to, terms containing g. The height constraint f = g suggests that terms involving f and g are equally complicated. The height constraint f >= g can be strengthened to either f > g or to f = g; it is inconsistent with the constraint g > f. A compound height constraint, such as the second example, suggests that => is higher than /\ and \/, both of which are higher than true, which has the same height as false.

The transitive closure of the height constraints in LP's registry defines a partial order on operators, which is used by the dsmpos ordering. The register command will reject any height constraint that is not a consistent extension to its registry.

The bottom (top) constraints suggest that LP extend its registry when it needs information about a listed operator by giving that operator a lower (higher) height than any non-bottom (non-top) operator. LP does not actually extend its registry until it needs this information. In general, putting operators at the bottom (top) of the registry causes terms to be reduced toward (away from) ones made out of these operators.