Associative-commutative reduction orderings
type: Item
instance of: scholarly article
title: Associative-commutative reduction orderings
zbMATH Open document ID: 0759.68043
DOI: 10.1016/0020-0190(92)90024-P
author: Leo Bachmair
published in: Information Processing Letters
publication date: 1993-01-16T00:00:00Z
review text: A rewrite system terminates if the rewrite rules define a relation which is contained in a well-founded ordering, called a reduction ordering. The paper shows how the lexicographic path ordering can be modified so as to make it compatible with associativity and commutativity, i.e. to ensure that if \(v\) is derivable from \(u\) and \(s\), \(t\) are terms obtained from \(v\), respectively \(u\), by computative or associative rules, then \(s\) is derivable from \(t\).
Mathematics Subject Classification ID: 68Q42
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 92078
zbMATH Keywords: rewrite system
zbMATH Keywords: reduction ordering
zbMATH Keywords: associativity
zbMATH Keywords: commutativity
reviewed by: Marius Zimand
MaRDI profile type: Publication
cites work: Q3783521
cites work: Termination orderings for associative-commutative rewriting systems
cites work: Termination of rewriting
cites work: Q3976057
full work available at URL: 0020-0190(92)90024-p
OpenAlex ID: W1991759334
description: scientific article; zbMATH DE number 92078