首页 | 本学科首页   官方微博 | 高级检索  
     


The Classification of Polynomial Orderings on Monadic Terms
Authors:Nick Cropper  Ursula Martin
Affiliation:(1) Computer Science Department, University of York, Heslington, Y01 5DD, UK (e-mail: nic@minster.york.ac.uk), GB;(2) School of Computer Science, University of St Andrews, St Andrews, Fife KY16 9SS, UK (e-mail: um@dcs.st-and.ac.uk), GB
Abstract: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, ω, ω2 and ωω, 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 ω, ω2 or ωω, although there exist reduction orderings on n letters of order type up to ωωn − 1. Received: June 1, 1998; revised version: September 18, 1999
Keywords:: Termination   Term rewriting systems   Ordinals.
本文献已被 SpringerLink 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号