Path ordering (term rewriting) (original) (raw)
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 alower-precedence root symbol g.In particular, by structural induction, a term f(...) is bigger than any term containing only symbols smaller than f. The latter variations include:
| Property | Value |
|---|---|
| dbo:abstract | 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 alower-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)), 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. * If f <. g, then s can dominate t only if one of s's subterms does. * If f .> g, then s dominates t if s dominates each of t's subterms. * If f = g, then the immediate subterms of s and t need to be compared recursively. Depending on the particular method, different variations of path orderings exist. The latter variations include: * the multiset path ordering (mpo), originally called recursive path ordering (rpo) * the lexicographic path ordering (lpo) * a combination of mpo and lpo, called recursive path ordering by Dershowitz, Jouannaud (1990) 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. (en) |
| dbo:wikiPageID | 42973489 (xsd:integer) |
| dbo:wikiPageLength | 7642 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1119587803 (xsd:integer) |
| dbo:wikiPageWikiLink | dbc:Order_theory dbr:Elementary_algebra dbr:General_recursive_function dbr:Multiset dbr:Continuous_function_(set_theory) dbr:Strict_total_order dbr:Structural_induction dbr:Successor_function dbr:Theoretical_computer_science dbr:Transitive_relation dbr:Well-founded dbr:Wilhelm_Ackermann dbr:Higher-order_function dbr:Irreflexive dbr:Term_(logic) dbr:Term_rewriting dbr:Ackermann_function dbr:Ackermann_ordinal dbc:Rewriting_systems dbr:Termination_(term_rewriting) dbr:Reduction_ordering dbr:Reflexive_closure dbr:Knuth–Bendix_completion_algorithm dbr:Lexicographical_order dbr:Veblen_function |
| dbp:b | i=0 (en) |
| dbp:wikiPageUsesTemplate | dbt:Redirect dbt:Reflist dbt:Su |
| dct:subject | dbc:Order_theory dbc:Rewriting_systems |
| gold:hypernym | dbr:Order |
| rdf:type | dbo:Eukaryote yago:Artifact100021939 yago:Instrumentality103575240 yago:Object100002684 yago:PhysicalEntity100001930 yago:System104377057 yago:Whole100003553 yago:WikicatRewritingSystems |
| rdfs:comment | 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 alower-precedence root symbol g.In particular, by structural induction, a term f(...) is bigger than any term containing only symbols smaller than f. The latter variations include: (en) |
| rdfs:label | Path ordering (term rewriting) (en) |
| owl:sameAs | freebase:Path ordering (term rewriting) yago-res:Path ordering (term rewriting) wikidata:Path ordering (term rewriting) https://global.dbpedia.org/id/n1zy |
| prov:wasDerivedFrom | wikipedia-en:Path_ordering_(term_rewriting)?oldid=1119587803&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Path_ordering_(term_rewriting) |
| is dbo:wikiPageRedirects of | dbr:MPO_(term_rewriting) dbr:Recursive_path_ordering dbr:LPO_(term_rewriting) dbr:Multiset_path_ordering dbr:Lexicographic_path_ordering dbr:RPO_(term_rewriting) |
| is dbo:wikiPageWikiLink of | dbr:MPO_(term_rewriting) dbr:Rewriting dbr:Nachum_Dershowitz dbr:Recursive_path_ordering dbr:LPO_(term_rewriting) dbr:Multiset_path_ordering dbr:Lexicographic_path_ordering dbr:Veblen_function dbr:RPO_(term_rewriting) |
| is foaf:primaryTopic of | wikipedia-en:Path_ordering_(term_rewriting) |