A Constructive Proof of the Topological Kruskal Theorem

被引：0
作者：
Goubault-Larrecq, Jean [1 ]
机构：
[1] CNRS, ENS Cachan, INRIA, LSV, F-75700 Paris, France
来源：
MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2013 | 2013年 / 8087卷
关键词：
LINEARLY ORDERED DOMAINS; DEPTH-BOUNDED PROCESSES; REWRITING-SYSTEMS; WELL-FOUNDEDNESS; INDEFINITE DATA; PI-CALCULUS; TERMINATION; ORDERINGS; VERIFICATION; TREES;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We give a constructive proof of Kruskal's Tree Theoremprecisely, 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 mu-terms. This all came from recent research on Noetherian spaces, and serves as a teaser for their theory.
引用
收藏
页码：22 / 41
页数：20
相关论文
共 47 条
  • [1] Abdulla P.A., 1993, LICS, P160
  • [2] Using forward reachability analysis for verification of lossy channel systems
    Abdulla, PA
    Collomb-Annichini, A
    Bouajjani, A
    Jonsson, B
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2004, 25 (01) : 39 - 65
  • [3] Algorithmic analysis of programs with well quasi-ordered domains
    Abdulla, PA
    Cerans, K
    Jonsson, B
    Tsay, YK
    [J]. INFORMATION AND COMPUTATION, 2000, 160 (1-2) : 109 - 127
  • [4] Acciai L, 2009, LECT NOTES COMPUT SC, V5556, P31, DOI 10.1007/978-3-642-02930-1_3
  • [5] [Anonymous], 1969, J COMPUT SYST SCI, DOI DOI 10.1016/S0022-0000(69)80011-5
  • [6] [Anonymous], 1960, Trans. Amer. Math. Soc., DOI DOI 10.1090/S0002-9947-1960-0111704-1
  • [7] [Anonymous], 2013, NEW MATH MONOGR
  • [8] Berghofer S, 2004, ANN NY ACAD SCI, V3085, P66
  • [9] Bertot Y., 2004, TEXTS THEOR COMP SCI, VXXV
  • [10] Coquand T., 2003, PROOF HIGMANS UNPUB
12345