University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence | up: Our Papers |

**Technical Report UIB 96-10, Universität Ulm, Fakultät
für Informatik, Dec. 1996**

Abstract |

We describe an encoding of major parts of domain theory in the PVS extension of the simply-typed lambda-calculus; these encodings consist of:

- Formalizations of basic structures like partial orders and complete partial orders (domains).
- Various domain constructions.
- Notions related to monotonic functions and continuous functions.
- Knaster-Tarski fixed-point theorems for monotonic and continuous functions; the proof of this theorem requires Zorn's lemma which has been derived from Hilbert's choice operator.
- Scott's fixed-point induction for admissible predicates and various variations of fixed-point induction like Park's lemma.

Altogether, these encodings form a conservative extension of the underlying PVS logic, since all developments are purely definitional. Most of our proofs are straightforward transcriptions of textbook knowledge. The purpose of this work, however, was not to merely reproduce textbook knowledge. To the contrary, our main motivation derived from our work on fully mechanized compiler correctness proofs, which requires a full treatment of fixed-point induction in PVS; these requirements guided our selection of which elements of domain theory were formalized.

A major problem of embedding mathematical theories like domain theory
lies in the fact that developing and working with those theories usually
generates myriads of applicability and type-correctness conditions. Our
approach to exploiting the PVS device of *judgements *to establish
many applicability conditions *behind the scenes* leads to a considerable
reduction in the number of the conditions that actually need to be proved.

Finally, we exemplify the application of mechanized fixed-point induction in PVS by a mechanized proof in the context of relating different semantics of imperative programming constructs.

Online Copy |

Available as Postscript (352 KB) or compressed Postscript (132 KB)

PVS specification files: `fixpoints.dmp
`or compressed `fixpoints.dmp.gz`.

To unpack the theories type `M-x undump-pvs-files` in PVS. The
top-level theory is `all_theories.pvs`.

BibTeX Entry |

@TechReport{BDvH+96, author = "F. Bartels and A. Dold and F. W. v. Henke and H. Pfeifer and H. Rue{\ss}", title = "{Formalizing Fixed-Point Theory in PVS}", institution = "Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik", year = "1996", number = "96-10", type = "Ulmer Informatik-Berichte" }

Dept. of AI Homepage | Research | Help | Mail to Webmaster | H. Pfeifer - Mar. 3, 1997 |