TY - JOUR

T1 - Adding constants to string rewriting

AU - Thiemann, R.

AU - Zantema, H.

AU - Giesl, J.

AU - Schneider-Kamp, P.

PY - 2008

Y1 - 2008

N2 - We consider unary term rewriting, i.e., term rewriting with unary signatures where all function symbols are either unary or constants. Terms over such signatures can be transformed into strings by just reading all symbols in the term from left to right, ignoring the optional variable. By lifting this transformation to rewrite rules, any unary term rewrite system (TRS) is transformed into a corresponding string rewrite system (SRS). We investigate which properties are preserved by this transformation. It turns out that any TRS over a unary signature is terminating if and only if the corresponding SRS is terminating. In this way tools for proving termination of string rewriting can be applied for proving termination of unary TRSs. For other rewriting properties including confluence, unique normal form property, weak normalization and relative termination, we show that a similar corresponding preservation property does not hold.

AB - We consider unary term rewriting, i.e., term rewriting with unary signatures where all function symbols are either unary or constants. Terms over such signatures can be transformed into strings by just reading all symbols in the term from left to right, ignoring the optional variable. By lifting this transformation to rewrite rules, any unary term rewrite system (TRS) is transformed into a corresponding string rewrite system (SRS). We investigate which properties are preserved by this transformation. It turns out that any TRS over a unary signature is terminating if and only if the corresponding SRS is terminating. In this way tools for proving termination of string rewriting can be applied for proving termination of unary TRSs. For other rewriting properties including confluence, unique normal form property, weak normalization and relative termination, we show that a similar corresponding preservation property does not hold.

U2 - 10.1007/s00200-008-0060-6

DO - 10.1007/s00200-008-0060-6

M3 - Article

VL - 19

SP - 27

EP - 38

JO - Applicable Algebra in Engineering, Communication and Computing

JF - Applicable Algebra in Engineering, Communication and Computing

SN - 0938-1279

IS - 1

ER -