A Constructive Proof of the Topological Kruskal Theorem
Identifieur interne : 001673 ( Main/Exploration ); précédent : 001672; suivant : 001674A Constructive Proof of the Topological Kruskal Theorem
Auteurs : Jean Goubault-Larrecq [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We give a constructive proof of Kruskal’s Tree Theorem—precisely, of a topological extension of it. The proof is in the style of a constructive proof of Higman’s Lemma due to Murthy and Russell (1990), and illuminates the role of regular expressions there. In the process, we discover an extension of Dershowitz’ recursive path ordering to a form of cyclic terms which we call μ-terms. This all came from recent research on Noetherian spaces, and serves as a teaser for their theory.
Url:
DOI: 10.1007/978-3-642-40313-2_3
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003734
- to stream Istex, to step Curation: 003691
- to stream Istex, to step Checkpoint: 000299
- to stream Main, to step Merge: 001685
- to stream Main, to step Curation: 001673
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A Constructive Proof of the Topological Kruskal Theorem</title><author><name sortKey="Goubault Larrecq, Jean" sort="Goubault Larrecq, Jean" uniqKey="Goubault Larrecq J" first="Jean" last="Goubault-Larrecq">Jean Goubault-Larrecq</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:E6B1AD7DD64939E3A0C57996A58068E63795551A</idno><date when="2013" year="2013">2013</date><idno type="doi">10.1007/978-3-642-40313-2_3</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-0VWXG8F3-M/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003734</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003734</idno><idno type="wicri:Area/Istex/Curation">003691</idno><idno type="wicri:Area/Istex/Checkpoint">000299</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000299</idno><idno type="wicri:doubleKey">0302-9743:2013:Goubault Larrecq J:a:constructive:proof</idno><idno type="wicri:Area/Main/Merge">001685</idno><idno type="wicri:Area/Main/Curation">001673</idno><idno type="wicri:Area/Main/Exploration">001673</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A Constructive Proof of the Topological Kruskal Theorem</title><author><name sortKey="Goubault Larrecq, Jean" sort="Goubault Larrecq, Jean" uniqKey="Goubault Larrecq J" first="Jean" last="Goubault-Larrecq">Jean Goubault-Larrecq</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>LSV, ENS Cachan, CNRS, INRIA</wicri:regionArea><wicri:noRegion>INRIA</wicri:noRegion><wicri:noRegion>INRIA</wicri:noRegion></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We give a constructive proof of Kruskal’s Tree Theorem—precisely, of a topological extension of it. The proof is in the style of a constructive proof of Higman’s Lemma due to Murthy and Russell (1990), and illuminates the role of regular expressions there. In the process, we discover an extension of Dershowitz’ recursive path ordering to a form of cyclic terms which we call μ-terms. This all came from recent research on Noetherian spaces, and serves as a teaser for their theory.</div></front></TEI><affiliations><list><country><li>France</li></country></list><tree><country name="France"><noRegion><name sortKey="Goubault Larrecq, Jean" sort="Goubault Larrecq, Jean" uniqKey="Goubault Larrecq J" first="Jean" last="Goubault-Larrecq">Jean Goubault-Larrecq</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001673 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001673 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:E6B1AD7DD64939E3A0C57996A58068E63795551A
|texte= A Constructive Proof of the Topological Kruskal Theorem
}}
| This area was generated with Dilib version V0.6.33. |  |