[metis-users] KBO vs. LPO

[Jasmin Blanchette]

Hi Joe,

KBO is hard-coded in Metis. Although KBO is generally acknowledged to "order more things" than LPO, there are some advantages to LPO, such as the possibility of orienting

    map f (Cons x xs) = Cons (f x) (map f xs)

(and in general equations where variables occur several times on the right-hand side) left-to-right. Combined with an appropriate precedence function (that reflects the order in which symbols are defined in HOL), this could do wonders.

From what I understand, it would be fairly straightforward to adapt Metis's code to support LPO as well -- or am I mistaken? What are your views on this? Would you be ready to consider an eventual patch that adds LPO, or at least the possibility of plugging-in non-KBO term orderings, for integration in the Metis repository?

Thanks in advance.

Cheers,

Jasmin