The classification of polynomial orderings on monadic terms

被引:0
|
作者
Cropper, N [1 ]
Martin, U
机构
[1] Univ York, Dept Comp Sci, York YO1 5DD, N Yorkshire, England
[2] Univ St Andrews, Sch Comp Sci, St Andrews KY16 9SS, Fife, Scotland
关键词
termination; term rewriting systems; ordinals;
D O I
10.1007/s002000000044
中图分类号
TP39 [计算机的应用];
学科分类号
081203 ; 0835 ;
摘要
We investigate, for the case of unary function symbols, polynomial orderings on term algebras, that is reduction orderings determined by polynomial interpretations of the function symbols. Any total reduction ordering over unary function symbols can be characterised in terms of numerical invariants determined by the ordering alone: we show that for polynomial orderings these invariants, and in some cases the ordering itself, are essentially determined by the degrees and leading coefficients of the polynomial interpretations. Hence any polynomial ordering has a much simpler description, and thus the apparent complexity and variety of these orderings is less than it might seem at first sight. In the case of two function symbols each of the three possible order types, omega, omega (2) and omega (omega), may be achieved by a polynomial ordering, as may any permitted value of the invariants. For more function symbols polynomial orderings cease to have this universality as the order type is again omega, omega (2) or omega (omega), although there exist reduction orderings on n letters of order type up to omega (omegan-1).
引用
收藏
页码:197 / 226
页数:30
相关论文
共 50 条