Termination of Term Rewriting: From Many-Sorted to One-Sorted

摘要

A property of many sorted term rewriting systems is called persistent if it isnot affected by removing the corresponding typing restriction. Persistency turns out to be a generalization of direct sum modularity. Strong normalization is shown to be persistent for the class of term rewriting systems for which both duplicating rules and collapsing rules do not occur, generalizing a similar result of Rusinowitch for modularity.