|
Well-Quasi-Orders
Title: |
Well-Quasi-Orders |
Author:
|
Christian Sternagel
|
Submission date: |
2012-04-13 |
Abstract: |
Based on Isabelle/HOL's type class for preorders,
we introduce a type class for well-quasi-orders (wqo)
which is characterized by the absence of "bad" sequences
(our proofs are along the lines of the proof of Nash-Williams,
from which we also borrow terminology). Our main results are
instantiations for the product type, the list type, and a type of finite trees,
which (almost) directly follow from our proofs of (1) Dickson's Lemma, (2)
Higman's Lemma, and (3) Kruskal's Tree Theorem. More concretely:
- If the sets A and B are wqo then their Cartesian product is wqo.
- If the set A is wqo then the set of finite lists over A is wqo.
- If the set A is wqo then the set of finite trees over A is wqo.
The research was funded by the Austrian Science Fund (FWF): J3202. |
Change history: |
[2012-06-11]: Added Kruskal's Tree Theorem.
[2012-12-19]: New variant of Kruskal's tree theorem for terms (as opposed to
variadic terms, i.e., trees), plus finite version of the tree theorem as
corollary.
[2013-05-16]: Simplified construction of minimal bad sequences.
[2014-07-09]: Simplified proofs of Higman's lemma and Kruskal's tree theorem,
based on homogeneous sequences.
[2016-01-03]: An alternative proof of Higman's lemma by open induction.
[2017-06-08]: Proved (classical) equivalence to inductive definition of
almost-full relations according to the ITP 2012 paper "Stop When You Are
Almost-Full" by Vytiniotis, Coquand, and Wahlstedt. |
BibTeX: |
@article{Well_Quasi_Orders-AFP,
author = {Christian Sternagel},
title = {Well-Quasi-Orders},
journal = {Archive of Formal Proofs},
month = apr,
year = 2012,
note = {\url{http://isa-afp.org/entries/Well_Quasi_Orders.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Abstract-Rewriting, Open_Induction, Regular-Sets |
Used by: |
Decreasing-Diagrams-II, Myhill-Nerode |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|