Mechanizing Domain Theory

F. Bartels, H. Pfeifer, F.W. v. Henke, H. Rueß

We describe an encoding of major parts of domain theory and fixed-point theory in the PVS extension of the simply-typed lambda-calculus; these formalizations comprise the encoding of mathematical structures like complete partial orders (domains), domain constructions, the Knaster-Tarski fixed-point theorem for monotonic functions, and variations of fixed-point induction. Altogether, these encodings form a conservative extension of the underlying PVS logic. 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 devices of predicate subtypes and 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. We illustrate the applicability of our encodings by means of simple examples including a mechanized fixed-point induction proof in the context of relating different semantics of imperative programming constructs.

Online Copy

Available as Postscript (217 KB) or compressed Postscript (83 KB)

@TechReport{BPvHR97,
  author = {F. Bartels and F. W. v. Henke and H. Pfeifer and H. Rue{\ss}},
  title =  {Mechanizing Domain Theory},
  institution =  {Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik},
  year    = {1997},
  number =  {96-10},
  type   = {Ulmer Informatik-Berichte},
  note = {This is a major revision of the Technical Report UIB-96-10
          with the title "Formalizing Fixed-Point Theory in PVS".
          The original version can still be found at
          \url{http://www.informatik.uni-ulm.de/ki/PVS/fixpoints.html}},
}