Adding constants to string rewriting

René Thiemann*, Hans Zantema, Jürgen Giesl, Peter Schneider-Kamp

*Kontaktforfatter for dette arbejde

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Resumé

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.

OriginalsprogEngelsk
TidsskriftApplicable Algebra in Engineering, Communications and Computing
Vol/bind19
Udgave nummer1
Sider (fra-til)27-38
Antal sider12
ISSN0938-1279
DOI
StatusUdgivet - 1. feb. 2008

Fingeraftryk

Unary
Rewriting
Strings
Termination
Term Rewriting
Signature
Term
Confluence
Preservation
Normal Form
Normalization
If and only if

Citer dette

Thiemann, René ; Zantema, Hans ; Giesl, Jürgen ; Schneider-Kamp, Peter. / Adding constants to string rewriting. I: Applicable Algebra in Engineering, Communications and Computing. 2008 ; Bind 19, Nr. 1. s. 27-38.
@article{ed1ffde2077c4fc7b604433be29775a9,
title = "Adding constants to string rewriting",
abstract = "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.",
keywords = "Confluence, String rewriting, Term rewriting, Termination",
author = "Ren{\'e} Thiemann and Hans Zantema and J{\"u}rgen Giesl and Peter Schneider-Kamp",
year = "2008",
month = "2",
day = "1",
doi = "10.1007/s00200-008-0060-6",
language = "English",
volume = "19",
pages = "27--38",
journal = "Applicable Algebra in Engineering, Communications and Computing",
issn = "0938-1279",
number = "1",

}

Adding constants to string rewriting. / Thiemann, René; Zantema, Hans; Giesl, Jürgen; Schneider-Kamp, Peter.

I: Applicable Algebra in Engineering, Communications and Computing, Bind 19, Nr. 1, 01.02.2008, s. 27-38.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Adding constants to string rewriting

AU - Thiemann, René

AU - Zantema, Hans

AU - Giesl, Jürgen

AU - Schneider-Kamp, Peter

PY - 2008/2/1

Y1 - 2008/2/1

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.

KW - Confluence

KW - String rewriting

KW - Term rewriting

KW - Termination

UR - http://www.scopus.com/inward/record.url?scp=39149129616&partnerID=8YFLogxK

U2 - 10.1007/s00200-008-0060-6

DO - 10.1007/s00200-008-0060-6

M3 - Journal article

AN - SCOPUS:39149129616

VL - 19

SP - 27

EP - 38

JO - Applicable Algebra in Engineering, Communications and Computing

JF - Applicable Algebra in Engineering, Communications and Computing

SN - 0938-1279

IS - 1

ER -