Properties of well founded relationsIn PVS, well founded relations are defined as relations such that every non empty set has a minimal element. Mathematicians tend to use a different definition: a relation is well founded iff there is no infinitely strictly decreasing sequence.
Strictly speaking, both definitions are not equivalent, since for PVS a well founded relation is necessarily irreflexive, which is not the case of the other definition. However, both definitions become equivalent if we replace “strictly decreasing” with “decreasing”.
This library, developed by Paul Y Gloess at LaBRI & ENSEIRB-MATMECA, essentially establishes the following results, often useful to prove the termination of functions:
- the lexical combination of two well founded relations is well founded;
- a well founded relation is irreflexive (obvious);
- a well founded relation subset is well founded (proof given to me by Bruno Dutertre while at SDL, from CSL, SRI International);
- the PVS and the mathematical definition of well foundedness are equivalent (proof also given to me by Bruno Dutertre);
- the transitive closure of a well founded relation is well founded: the heart of the proof uses the mathematical definition of well foundedness; then Bruno Dutertre equivalence result is applied to suit PVS definition;
- the strict subset relation among finite sets is well founded: this result is quite convenient, as it avoids having to resort to cardinality of finite sets.
Dump and PVS Status