University of Cambridge

 Logic
&
Semantics

Better-Quasi-orders and Coinduction

By Thomas Forster (11th June 1999)

A quasiorder is a symmetrical reflexive relation. $\langle X, \leq\rangle$ is a well quasi order (WQO) if in addition for every sequence $\{x_i: i < \omega\}$ from X there is i < j s.t. $x_i \leq x_j$. WQOs are important in proving termination. If X is WQO the power set of X is not always WQO by the Egli-Milner ordering. The class of Better Quasi-orders is a class of WQOs designed to be closed under this operation. It turns out that the class of BQOs can be given a coinductive definition which is equivalent to the usual combinatorial definition.

As a result, one can give smooth proofs of results whose standard combinatorial proofs are ...not for fainthearts.

LS Home page or Talks in 1998/99

This abstract was produced with the help of the LaTeX2HTML translator Version 98.1p1 release (March 2nd, 1998)
Copyright © 1993, 1994, 1995, 1996, 1997, Nikos Drakos, Computer Based Learning Unit, University of Leeds.