Leanest Quasi-orderings

A convenient method for defining a quasi-ordering, such as those used for proving termination of rewriting, is to choose the minimum of a set of quasi-orderings satisfying some desired traits. Unfortunately, a minimum in terms of set inclusion can be non-existent even when an intuitive “minimum” exists. We suggest an alternative to set inclusion, called “leanness”, show that leanness is a partial order on quasiorderings, and provide sufficient conditions for the existence of a “leanest” member of a set of total well-founded quasi-orderings. Key words: Quasi-ordering, well-quasi-ordering, lexicographic path ordering In my poor, lean lank face nobody has ever seen that any cabbages were sprouting. —Abraham Lincoln

• Type: Conference
• Year: 2005
• Where: RTA
• Authors: Nachum Dershowitz, E. Castedo Ellerman
• Keywords: Convenient Method, Lean Lank Face, RTA 2005, Set Inclusion, Theoretical Computer Science