Invariants, Patterns and Weights for Ordering Terms
Identifieur interne : 002065 ( Istex/Curation ); précédent : 002064; suivant : 002066Invariants, Patterns and Weights for Ordering Terms
Auteurs : Ursula Martin [Royaume-Uni] ; Duncan Shand [Royaume-Uni]Source :
- Journal of Symbolic Computation [ 0747-7171 ] ; 2000.
English descriptors
- Teeft :
- Algebra, Arity, Arity terms, Certain conditions, Comput, Cropper, Disjoint union, Division order, Dpoly, Embedding, Embeds, Equivalence relation, Function symbol, Function symbols, General framework, Greatest element, Homeomorphic, Homeomorphic embedding relation, Lexicographic, Linearizable, Main result, Main theorem, Matrix, Monadic, Monadic terms, Monotonic, Monotonic family, Monotonic order, Monotonic orders, More detail, Nite, Orthogonal matrix, Partial order, Pattern class, Pattern classes, Poly, Polynomial interpretation, Polynomial order, Polynomial orders, Principal subterm, Principal subterms, Real numbers, Recursive, Recursive path order, Shand, Skeleton, Stable order, Subset, Substitution, Subterm, Subterm property, Subterms, Term algebra, Term orders, Termination proofs, Topological space, Total order, Unary, Unary function symbols, Variable arity terms, Varyadic, Varyadic embedding, Vector space, Vector spaces, Weight function, Weight order, Weight sequence, Weight sequences.
Abstract
Abstract: We prove that any simplification order over arbitrary terms is an extension of an order by weight, by considering a related monadic term algebra called the spine. We show that any total ground-stable simplification order on the spine lifts to an order on the full term algebra. Conversely, under certain restrictions, a simplification ordering on the term algebra defines a weight function on the spine, which in turn can be lifted to a weight order on the original ground terms which contains the original order. We investigate the Knuth–Bendix and polynomial orders in this light. We provide a general framework for ordering terms by counting embedded patterns, which gives rise to many new orderings. We examine the recursive path order in this context.
Url:
DOI: 10.1006/jsco.1999.0333
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :002093
Links to Exploration step
ISTEX:8DE42AC82983BB10B4FB3BE52B88422D9348ED24Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Invariants, Patterns and Weights for Ordering Terms</title><author><name sortKey="Martin, Ursula" sort="Martin, Ursula" uniqKey="Martin U" first="Ursula" last="Martin">Ursula Martin</name><affiliation wicri:level="1"><mods:affiliation>School of Computer Science, University of St Andrews, St Andrews, Fife, KY16 9SS, U.K.</mods:affiliation><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>School of Computer Science, University of St Andrews, St Andrews, Fife, KY16 9SS</wicri:regionArea></affiliation></author><author><name sortKey="Shand, Duncan" sort="Shand, Duncan" uniqKey="Shand D" first="Duncan" last="Shand">Duncan Shand</name><affiliation wicri:level="1"><mods:affiliation>School of Computer Science, University of St Andrews, St Andrews, Fife, KY16 9SS, U.K.</mods:affiliation><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>School of Computer Science, University of St Andrews, St Andrews, Fife, KY16 9SS</wicri:regionArea></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:8DE42AC82983BB10B4FB3BE52B88422D9348ED24</idno><date when="2000" year="2000">2000</date><idno type="doi">10.1006/jsco.1999.0333</idno><idno type="url">https://api.istex.fr/ark:/67375/6H6-K7HGD3CK-Q/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002093</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002093</idno><idno type="wicri:Area/Istex/Curation">002065</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Invariants, Patterns and Weights for Ordering Terms</title><author><name sortKey="Martin, Ursula" sort="Martin, Ursula" uniqKey="Martin U" first="Ursula" last="Martin">Ursula Martin</name><affiliation wicri:level="1"><mods:affiliation>School of Computer Science, University of St Andrews, St Andrews, Fife, KY16 9SS, U.K.</mods:affiliation><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>School of Computer Science, University of St Andrews, St Andrews, Fife, KY16 9SS</wicri:regionArea></affiliation></author><author><name sortKey="Shand, Duncan" sort="Shand, Duncan" uniqKey="Shand D" first="Duncan" last="Shand">Duncan Shand</name><affiliation wicri:level="1"><mods:affiliation>School of Computer Science, University of St Andrews, St Andrews, Fife, KY16 9SS, U.K.</mods:affiliation><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>School of Computer Science, University of St Andrews, St Andrews, Fife, KY16 9SS</wicri:regionArea></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Symbolic Computation</title><title level="j" type="abbrev">YJSCO</title><idno type="ISSN">0747-7171</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="2000">2000</date><biblScope unit="volume">29</biblScope><biblScope unit="issue">6</biblScope><biblScope unit="page" from="921">921</biblScope><biblScope unit="page" to="957">957</biblScope></imprint><idno type="ISSN">0747-7171</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0747-7171</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Algebra</term><term>Arity</term><term>Arity terms</term><term>Certain conditions</term><term>Comput</term><term>Cropper</term><term>Disjoint union</term><term>Division order</term><term>Dpoly</term><term>Embedding</term><term>Embeds</term><term>Equivalence relation</term><term>Function symbol</term><term>Function symbols</term><term>General framework</term><term>Greatest element</term><term>Homeomorphic</term><term>Homeomorphic embedding relation</term><term>Lexicographic</term><term>Linearizable</term><term>Main result</term><term>Main theorem</term><term>Matrix</term><term>Monadic</term><term>Monadic terms</term><term>Monotonic</term><term>Monotonic family</term><term>Monotonic order</term><term>Monotonic orders</term><term>More detail</term><term>Nite</term><term>Orthogonal matrix</term><term>Partial order</term><term>Pattern class</term><term>Pattern classes</term><term>Poly</term><term>Polynomial interpretation</term><term>Polynomial order</term><term>Polynomial orders</term><term>Principal subterm</term><term>Principal subterms</term><term>Real numbers</term><term>Recursive</term><term>Recursive path order</term><term>Shand</term><term>Skeleton</term><term>Stable order</term><term>Subset</term><term>Substitution</term><term>Subterm</term><term>Subterm property</term><term>Subterms</term><term>Term algebra</term><term>Term orders</term><term>Termination proofs</term><term>Topological space</term><term>Total order</term><term>Unary</term><term>Unary function symbols</term><term>Variable arity terms</term><term>Varyadic</term><term>Varyadic embedding</term><term>Vector space</term><term>Vector spaces</term><term>Weight function</term><term>Weight order</term><term>Weight sequence</term><term>Weight sequences</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We prove that any simplification order over arbitrary terms is an extension of an order by weight, by considering a related monadic term algebra called the spine. We show that any total ground-stable simplification order on the spine lifts to an order on the full term algebra. Conversely, under certain restrictions, a simplification ordering on the term algebra defines a weight function on the spine, which in turn can be lifted to a weight order on the original ground terms which contains the original order. We investigate the Knuth–Bendix and polynomial orders in this light. We provide a general framework for ordering terms by counting embedded patterns, which gives rise to many new orderings. We examine the recursive path order in this context.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002065 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 002065 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Curation
|type= RBID
|clé= ISTEX:8DE42AC82983BB10B4FB3BE52B88422D9348ED24
|texte= Invariants, Patterns and Weights for Ordering Terms
}}
| This area was generated with Dilib version V0.6.33. |  |