Reduction system

In mathematical logic and theoretical computer science , the term reduction system , or abstract reduction system , or ARS for short , stands for a generalization of term rewriting systems . In its simplest form, an ARS is a set of objects together with a binary relation , which is commonly referred to as. Despite its simplicity, an ARS is sufficient to describe important properties of term rewriting systems, such as B. normal forms , termination and various concepts of confluence . ${\displaystyle \rightarrow }$

Historically, there have been several different abstractions of term rewriting, each with its own specifics. The formalization most used today, which is followed here, is based on the work of Gérard Huet (1980).

definition

An ARS consists of a set A , the objects, together with a binary relation on A , usually denoted by. This relation is called the reduction relation or simply reduction . ${\displaystyle \rightarrow }$

As a mathematical object, an ARS is the same as an unmarked transition system . Nevertheless, the focus and terminology differ in these two areas: In a transition system one is interested in interpreting the markings as actions, while in an ARS the focus is on how objects are transformed (reduced) into others.

example

The set of objects is T = { a , b , c } and the binary relation → is defined as follows: → ; this is usually written as ${\displaystyle =\{(a,b),(b,a),(a,c),(b,c)\}}$

a → b , b → a , a → c , b → c .

If one reads this as rules by which elements can be transformed into others, then one sees that both a and b can be transformed (reduced) into c . Apparently this is an important property of the system. In a way, c is a "simplest" object in the system, as none of the rules can be applied to c to further transform this element.

Basic terms

The above example leads to some important terms in the context of an ARS.

• ${\displaystyle {\stackrel {*}{\rightarrow }}}$is the transitive shell of , where = is the identity ; d. H. is the smallest quasi-order ( reflexive and transitive relation) that contains. It is also the reflexive and transitive shell of . ${\displaystyle \rightarrow \cup =}$ ${\displaystyle {\stackrel {*}{\rightarrow }}}$ ${\displaystyle \rightarrow }$ ${\displaystyle \rightarrow }$

• ${\displaystyle \leftrightarrow }$is , d. H. the union of the relation with its inverse relation ; is also known as the symmetrical envelope of . ${\displaystyle \rightarrow \cup \rightarrow ^{-1}}$ ${\displaystyle \rightarrow }$ ${\displaystyle \leftrightarrow }$ ${\displaystyle \rightarrow }$
• ${\displaystyle {\stackrel {*}{\leftrightarrow }}}$is the transitive hull of , i.e. H. is the smallest equivalence relation that contains. It is also known as the reflexive transitive symmetric envelope of . ${\displaystyle \leftrightarrow \cup =}$ ${\displaystyle {\stackrel {*}{\leftrightarrow }}}$ ${\displaystyle \rightarrow }$ ${\displaystyle \rightarrow }$

Normal forms and the word problem

An object x in A is said to be reducible if there is an object y in A that is different from x with ; otherwise it is called irreducible or a normal form . An object y is called the normal form of x if it holds and y is irreducible. If x has a unique normal form, then this is denoted by. ${\displaystyle x\rightarrow y}$ ${\displaystyle x{\stackrel {*}{\rightarrow }}y}$ ${\displaystyle x\downarrow }$

In the example above, c is a normal form of a and b . Since a and b are reducible is c even the only normal form of these elements . If every object has at least one normal form, the ARS is called normalizing . ${\displaystyle c=a\downarrow =b\downarrow }$

One of the important problems that can be formulated in the context of an ARS is the word problem : Given x and y , are these two objects equivalent under the relation ? This is a very general framework for the word problem; so is z. B. the word problem for groups is a special case of the ARS word problem. The word problem is easier to deal with when there are unique normal forms: in this case, two objects with the same normal form are equivalent below . The word problem for an ARS is generally un decidable . ${\displaystyle {\stackrel {*}{\leftrightarrow }}}$ ${\displaystyle {\stackrel {*}{\leftrightarrow }}}$

For the investigation of the question of whether normal forms exist, the terms Church-Rosser property and confluence are of central importance.

swell

• Franz Baader, Tobias Nipkow: Term Rewriting and All That. Cambridge University Press, 1998. Suitable for beginners.
• Nachum Dershowitz and Jean-Pierre Jouannaud Rewrite Systems , Chapter 6 in Jan van Leeuwen (Ed.), Handbook of Theoretical Computer Science. Volume B: Formal Models and Semantics. Elsevier / MIT Press, 1990, ISBN 0-444-88074-7 , pp. 243-320.
• Ronald V. Book , Friedrich Otto: String rewriting systems. Springer, Berlin 1993. Chapter 1: Abstract reduction systems. ISBN 0-387-97965-4 .
• Marc Bezem, JW Klop, Roel de Vrijer: Term rewriting systems. Cambridge University Press, 2003, ISBN 0-521-39115-6 , Chapter 1. (This is an extensive monograph).
• John Harrison: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009, ISBN 978-0-521-89957-4 , Chapter 4: Equality.
• Gérard Huet: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. In: Journal of the ACM (JACM), Vol. 27, No. 4, October 1980, pp. 797-821.

Individual evidence

1. ^ Ronald V. Book, Friedrich Otto: String rewriting systems. P. 9.
2. ^ Ronald V. Book, Friedrich Otto: String rewriting systems. P. 10.
3. ↑ Marc Bezem, JW Klop, Roel de Vrijer: Term rewriting systems. Pp. 7-8.
4. ^ Franz Baader, Tobias Nipkow: Term Rewriting and All That. Pp. 8-9.
5. ^ Franz Baader, Tobias Nipkow: Term Rewriting and All That. P. 11 f.