About: Path ordering (term rewriting)     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : dbo:Eukaryote, within Data Space : el.dbpedia.org associated with source document(s)

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:

AttributesValues
rdf:type
rdfs:label
  • Path ordering (term rewriting) (en)
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)
sameAs
dbp:wikiPageUsesTemplate
Subject
gold:hypernym
prov:wasDerivedFrom
Wikipage page ID
page length (characters) of wiki page
Wikipage revision ID
has 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. 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 ordinals. (en)
foaf:isPrimaryTopicOf
is Wikipage redirect of
is Link from a Wikipage to another Wikipage of
Faceted Search & Find service v1.17_git151 as of Feb 20 2025


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
OpenLink Virtuoso version 07.20.3240 as of Nov 11 2024, on Linux (x86_64-ubuntu_focal-linux-gnu), Single-Server Edition (72 GB total memory, 1 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2025 OpenLink Software