Path ordering (term rewriting)

Last updated

In theoretical computer science, in particular in term rewriting, a path ordering is a well-founded strict total order (>) on the set of all terms such that

f(...) > g(s1,...,sn)   if  f.>g  and  f(...) > si for i=1,...,n,

where (.>) is a user-given total precedence order on the set of all function symbols.

Intuitively, a term f(...) is bigger than any term g(...) built from terms si smaller than f(...) using a lower-precedence root symbol g. In particular, by structural induction, a term f(...) is bigger than any term containing only symbols smaller than f.

A path ordering is often used as reduction ordering in term rewriting, in particular in the Knuth–Bendix completion algorithm. As an example, a term rewriting system for "multiplying out" mathematical expressions could contain a rule x*(y+z) → (x*y) + (x*z). In order to prove termination, a reduction ordering (>) must be found with respect to which the term x*(y+z) is greater than the term (x*y)+(x*z). This is not trivial, since the former term contains both fewer function symbols and fewer variables than the latter. However, setting the precedence (*) .> (+), a path ordering can be used, since both x*(y+z) > x*y and x*(y+z) > x*z is easy to achieve.

There may also be systems for certain general recursive functions, for example a system for the Ackermann function may contain the rule A(a+, b+) → A(a, A(a+, b)), [1] where b+ denotes the successor of b.

Given two terms s and t, with a root symbol f and g, respectively, to decide their relation their root symbols are compared first.

The latter variations include:

Dershowitz, Okada (1988) list more variants, and relate them to Ackermann's system of ordinal notations. In particular, an upper bound given on the order types of recursive path orderings with n function symbols is φ(n,0), using Veblen's function for large countable ordinals. [7]

Formal definitions

The multiset path ordering (>) can be defined as follows: [9]

s = f(s1,...,sm) > t = g(t1,...,tn)if
f.>gands>tjfor eachj∈{1,...,n},   or
si≥tfor somei∈{1,...,m},or
f=gand{s1,...,sm} >> {t1,...,tn}

where

More generally, an order functional is a function O mapping an ordering to another one, and satisfying the following properties: [11]

The multiset extension, mapping (>) above to (>>) above is one example of an order functional: (>>)=O(>). Another order functional is the lexicographic extension, leading to the lexicographic path ordering.

Related Research Articles

Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation that can be used to simulate any Turing machine. It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics.

In computability theory, a primitive recursive function is roughly speaking a function that can be computed by a computer program whose loops are all "for" loops. Primitive recursive functions form a strict subset of those general recursive functions that are also total functions.

In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions.

In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems. In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.

In mathematics, the lexicographic or lexicographical order is a generalization of the alphabetical order of the dictionaries to sequences of ordered symbols or, more generally, of elements of a totally ordered set.

The Knuth–Bendix completion algorithm is a semi-decision algorithm for transforming a set of equations into a confluent term rewriting system. When the algorithm succeeds, it effectively solves the word problem for the specified algebra.

Constraint logic programming is a form of constraint programming, in which logic programming is extended to include concepts from constraint satisfaction. A constraint logic program is a logic program that contains constraints in the body of clauses. An example of a clause including a constraint is A(X,Y):-X+Y>0,B(X),C(Y). In this clause, X+Y>0 is a constraint; A(X,Y), B(X), and C(Y) are literals as in regular logic programming. This clause states one condition under which the statement A(X,Y) holds: X+Y is greater than zero and both B(X) and C(Y) are true.

In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems relate to normal forms.

Substitution is a fundamental concept in logic. A substitution is a syntactic transformation on formal expressions. To apply a substitution to an expression means to consistently replace its variable, or placeholder, symbols by other expressions. The resulting expression is called a substitution instance, or instance for short, of the original expression.

Primitive recursive arithmetic (PRA) is a quantifier-free formalization of the natural numbers. It was first proposed by Norwegian mathematician Skolem (1923), as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist. Many also believe that all of finitism is captured by PRA, but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to ε0, which is the proof-theoretic ordinal of Peano arithmetic. PRA's proof theoretic ordinal is ωω, where ω is the smallest transfinite ordinal. PRA is sometimes called Skolem arithmetic.

In mathematical logic and theoretical computer science, an abstract rewriting system is a formalism that captures the quintessential notion and properties of rewriting systems. In its simplest form, an ARS is simply a set together with a binary relation, traditionally denoted with ; this definition can be further refined if we index (label) subsets of the binary relation. Despite its simplicity, an ARS is sufficient to describe important properties of rewriting systems like normal forms, termination, and various notions of confluence.

In computer science, more specifically in automata and formal language theory, nested words are a concept proposed by Alur and Madhusudan as a joint generalization of words, as traditionally used for modelling linearly ordered structures, and of ordered unranked trees, as traditionally used for modelling hierarchical structures. Finite-state acceptors for nested words, so-called nested word automata, then give a more expressive generalization of finite automata on words. The linear encodings of languages accepted by finite nested word automata gives the class of visibly pushdown languages. The latter language class lies properly between the regular languages and the deterministic context-free languages. Since their introduction in 2004, these concepts have triggered much research in that area.

In mathematical logic, a term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula. This is analogous to natural language, where a noun phrase refers to an object and a whole sentence refers to a fact.

Jan Willem Klop is a professor of applied logic at Vrije Universiteit in Amsterdam. He holds a Ph.D. in mathematical logic from Utrecht University. Klop is known for his work on the Algebra of Communicating Processes, co-author of TeReSe and his fixed point combinator

In mathematics, the Dershowitz–Manna ordering is a well-founded ordering on multisets named after Nachum Dershowitz and Zohar Manna. It is often used in context of termination of programs or term rewriting systems.

In rewriting, a reduction strategy or rewriting strategy is a relation specifying a rewrite for each object or term, compatible with a given reduction relation. Some authors use the term to refer to an evaluation strategy.

<span class="mw-page-title-main">Encompassment ordering</span>

In theoretical computer science, in particular in automated theorem proving and term rewriting, the containment, or encompassment, preorder (≤) on the set of terms, is defined by

<span class="mw-page-title-main">Rewrite order</span>

In theoretical computer science, in particular in automated reasoning about formal equations, reduction orderings are used to prevent endless loops. Rewrite orders, and, in turn, rewrite relations, are generalizations of this concept that have turned out to be useful in theoretical investigations.

<span class="mw-page-title-main">Jean-Pierre Jouannaud</span> French computer scientist (born 1947)

Jean-Pierre Jouannaud is a French computer scientist, known for his work in the area of term rewriting.

Nachum Dershowitz is an Israeli computer scientist, known e.g. for the Dershowitz–Manna ordering and the multiset path ordering used to prove termination of term rewrite systems.

References

  1. ↑ N. Dershowitz, "Termination" (1995). p. 207
  2. ↑ Nachum Dershowitz, Jean-Pierre Jouannaud (1990). Jan van Leeuwen (ed.). Rewrite Systems. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320. Here: sect.5.3, p.275
  3. ↑ Gerard Huet (May 1986). Formal Structures for Computation and Deduction. International Summer School on Logic of Programming and Calculi of Discrete Design. Archived from the original on 2014-07-14. Here: chapter 4, p.55-64
  4. ↑ N. Dershowitz (1982). "Orderings for Term-Rewriting Systems" (PDF). Theoret. Comput. Sci. 17 (3): 279–301. doi:10.1016/0304-3975(82)90026-3. S2CID   6070052.
  5. ↑ S. Kamin, J.-J. Levy (1980). Two Generalizations of the Recursive Path Ordering (Technical report). Univ. of Illinois, Urbana/IL.
  6. ↑ Kamin, Levy (1980)
  7. 1 2 N. Dershowitz, M. Okada (1988). "Proof-Theoretic Techniques for Term Rewriting Theory". Proc. 3rd IEEE Symp. on Logic in Computer Science (PDF). pp. 104–111.
  8. ↑ Mitsuhiro Okada, Adam Steele (1988). "Ordering Structures and the Knuth–Bendix Completion Algorithm". Proc. of the Allerton Conf. on Communication, Control, and Computing.
  9. ↑ Huet (1986), sect.4.3, def.1, p.57
  10. ↑ Huet (1986), sect.4.1.3, p.56
  11. ↑ Huet (1986), sect.4.3, p. 58
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.