请输入您要查询的百科知识：

　

词条 Rewrite order
释义

  1. Properties

  2. Notes

  3. References

{{technical|date=July 2014}}

In theoretical computer science, in particular in automated theorem proving and term rewriting,

a binary relation (→) on the set of terms is called a rewrite relation if it is closed under contextual embedding and under instantiation; formally: if l→r implies u[lσ]p→u[rσ]p for all terms l, r, u, each path p of u, and each substitution σ. If (→) is also irreflexive and transitive, then it is called a rewrite ordering,[1] or rewrite preorder. If the latter (→) is moreover well-founded, it is called a reduction ordering,[2] or a reduction preorder.

Given a binary relation R, its rewrite closure is the smallest rewrite relation containing R.[3] A transitive and reflexive rewrite relation that contains the subterm ordering is called a simplification ordering.[4]

Overview of rewrite relations}}[5]
rewrite
relation		 rewrite
order		 reduction
order		 simplification
order
closed under context
x R y implies u[x]p R u[y]p		 {{yes}} {{yes}} {{yes}} {{yes}}
closed under instantiation
x R y implies xσ R yσ		 {{yes}} {{yes}} {{yes}} {{yes}}
contains subterm relation
y subterm of x implies x R y		 {{yes}}
reflexive
always x R x		(No)(No) {{yes}}
irreflexive
never x R x		 {{yes}} {{yes}}(No)
transitive
x R y and y R z implies x R z		 {{yes}} {{yes}} {{yes}}
well-founded
no infinite chain x1 R x2 R x3 R ...[6]		 {{yes}}(Yes)

Properties

  • The converse, the symmetric closure, the reflexive closure, and the transitive closure of a rewrite relation is again a rewrite relation, as are the union and the intersection of two rewrite relations.[7]
  • The converse of a rewrite order is again a rewrite order.
  • While rewrite orders exist that are total on the set of ground terms ("ground-total" for short), no rewrite order can be total on the set of all terms.[8][9]
  • A term rewriting system {{math|{{mset|1= l1::=r1,...,ln::=rn, ... }}}} is terminating if its rules are a subset of a reduction ordering.[10][2]
  • Conversely, for every terminating term rewriting system, the transitive closure of (::=) is a reduction ordering,[2] which needn't be extendable to a ground-total one, however. For example, the ground term rewriting system { f(a)::=f(b), g(b)::=g(a) } is terminating, but can be shown so using a reduction ordering only if the constants a and b are incomparable.[11][12]
  • A ground-total and well-founded rewrite ordering[13] necessarily contains the proper subterm relation on ground terms.{{#tag:ref|Else, t|p > t for some term t and position p, implying an infinite descending chain t > t[t]p > t[t[t]p]p > ... [12][14]}}
  • Conversely, a rewrite ordering that contains the subterm relation[15] is necessarily well-founded, when the set of function symbols is finite.[9][16]
  • A finite term rewriting system {{math|{{mset|1= l1::=r1,...,ln::=rn, ... }}}} is terminating if its rules are subset of the strict part of a simplification ordering.[4][17]

Notes

1. ^Dershowitz, Jouannaud (1990), sect.2.1, p.251
2. ^1 2 Dershowitz, Jouannaud (1990), sect.5.1, p.270
3. ^Dershowitz, Jouannaud (1990), sect.2.2, p.252
4. ^1 Dershowitz, Jouannaud (1990), sect.5.2, p.274
5. ^Parenthesized entries indicate inferred properties which are not part of the definition. For example, an irreflexive relation can't be reflexive (on a nonempty domain set).
6. ^except all xi are equal for all i beyond some n, for a reflexive relation
7. ^Dershowitz, Jouannaud (1990), sect.2.1, p.251
8. ^Since x<y implies y<x, since the latter is an instance of the former, for variables x, y.
9. ^1 Dershowitz, Jouannaud (1990), sect.5.1, p.272
10. ^i.e. if {{math|li > ri}} for all i, where (>) is a reduction ordering; the system needn't have finitely many rules
11. ^Since e.g. {{math|a>b}} implied {{math|g(a)>g(b)}}, meaning the second rewrite rule was not decreasing.
12. ^1 Dershowitz, Jouannaud (1990), sect.5.1, p.271
13. ^i.e. a ground-total reduction ordering
14. ^{{cite techreport| author=David A. Plaisted| title=A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems| year=1978| number=R-78-943| pages=52| institution=Univ. of Illinois, Dept. of Comp. Sc.| url=https://archive.org/details/recursivelydefin943plai}}
15. ^i.e. a simplification ordering
16. ^The proof of this property is based on Higman's lemma, or, more generally, Kruskal's tree theorem.
17. ^{{cite journal | author=N. Dershowitz | title=Orderings for Term-Rewriting Systems | journal=Theoret. Comput. Sci. | volume=17 | number=3 | pages=279--301 | url=http://www.cs.tau.ac.il/~nachum/papers/Orderings4TRS.pdf | year=1982 }} Here: p.287; the notions are named slightly different.

References

{{cite book| author1=Nachum Dershowitz |author2= Jean-Pierre Jouannaud| title=Rewrite Systems| year=1990| volume=B| pages=243–320| publisher=Elsevier| editor=Jan van Leeuwen| series=Handbook of Theoretical Computer Science}}{{reflist}}{{comp-sci-stub}}

2 : Rewriting systems|Order theory
随便看

　

开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。

　

Copyright © 2023 OENC.NET All Rights Reserved
京ICP备2021023879号 更新时间：2024/11/11 4:12:47