Abstract rewriting system

In mathematical logic and theoretical computer science is the term reduction system, or abstract reduction system, abbreviated ARS, for a generalization of term rewriting systems. In its simplest form, an ARS is a set of objects with a binary relation that is commonly referred to. Despite its simplicity, an ARS is sufficient to describe important properties of term rewriting systems, such as Normal forms, scheduling, and various notions of confluence.

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

Definition

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

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

Example

Be the set of objects t = {a, b, c }, and the binary relation → is defined as follows: →; the one usually writes as

If you read this as rules, can be transformed by the elements in others, then you can see that both a and b transformed into c ( reduced) can be. This is obviously an important feature of the system. c is in a sense a " simplest " Object of the system, since none of the rules can be applied to C in order to transform this further element.

Basic concepts

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

  • Is the transitive closure of, where = is the identity; ie. , the smallest quasi-ordering ( reflexive and transitive relation ) containing. She is also the reflexive and transitive closure of.
  • , i.e. the union of the relation with its inverse relation; is also called symmetric closure of.
  • Is the transitive closure of, that is, is the smallest equivalence relation containing. It is also referred to as reflexive transitive symmetric closure of.

Normal forms and the word problem

An object x in A is called reducible if there is a different object x of y in A with; otherwise it is called irreducible or a normal form. An object y is called the normal form of x when y is true and is irreducible. If x has a unique normal form, then this is denoted by.

C in the example above is a normal form of a and b. If each object has at least one normal form, does ARS normalizing.

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 are equivalent under the relation? This is a very general framework for the word problem; as is for example the word problem for groups is a special case of the ARS - word problem. The word problem is easier to treat when there are clear normal forms: applicable in this case that two objects are the same normal form equivalent under. The word problem for an ARS is undecidable in general.

To study the question of whether normal forms exist, the terms of the Church - Rosser property and the confluence of central importance.

Comments

Swell

  • Franz Baader and Tobias Nipkow, Term Rewriting and All That, Cambridge University Press,. Suitable for beginners 1998.
  • Nachum Dershowitz and Jouannaud, Jean-Pierre Rewrite Systems, Chapter 6 in Jan van Leeuwen ( Ed. ), Handbook of Theoretical Computer Science, Volume B:. Formal Models and Sematics, Elsevier and MIT Press, 1990, ISBN 0-444-88074 - 7, pp. 243-320.
  • Ronald V. Book and Friedrich Otto, String - rewriting Systems, Springer (1993). Chapter 1, " Abstract reduction systems"
  • Marc Bezem, JW Klop, Roel de Vrijer ( " Terese " ), term rewriting systems, Cambridge University Press, 2003, ISBN 0521391156, Chapter 1 This is a comprehensive monograph.
  • John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009, ISBN 9780521899574, chapter 4 " Equality".
  • Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM ( JACM ), October 1980, Volume 27, Issue 4, pp. 797 - 821
  • Logic
  • Theoretical computer science
Confluence (abstract rewriting) State transition system Transitivity Word problem (computability) Recursive set
675445
de