[metis-users] KBO vs. LPO

[Joe Hurd]

Hi Jasmine,

Sorry for the delay in replying.

Around ten(!) years ago I carried out some experiments with term
orderings in Metis, specifically the "stickiness" of constraints on
clauses resulting from KBO comparisons. I wrote them up in a Cambridge
CL technical report:

http://www.gilith.com/research/papers/ordering.pdf

However, that reference was just for interest's sake. To answer your
specific question, I would certainly consider adding different
orderings to Metis. In Clause.sig the order is explicitly
parameterized:

type parameters =
     {ordering : KnuthBendixOrder.kbo,
      orderLiterals : literalOrder,
      orderTerms : bool}

If someone were to create a new module LexicographicPathOrder with the
same signature as KnuthBendixOrder I would happily hook pull it in to
the Metis sources and offer it as an option to Clause.parameters.

Cheers,

Joe

On Mon, Mar 19, 2012 at 5:16 PM, Jasmin Blanchette
<jasmin.blanchette at gmail.com> wrote:
> 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
>
>
> _______________________________________________
> metis-users mailing list
> metis-users at gilith.com
> http://www.gilith.com/metis/mailing-list