Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: Convergence Measures
Authors: Klarlund, Nils
Keywords: computer science
technical report
Issue Date: Mar-1990
Publisher: Cornell University
Abstract: General methods of verification for programs defining infinite computataions rely on measuring progress or convergence of finite computations towards satisfying the specification. Traditionally, progress is measured using well-founded orderings, but this often involves syntactic transformations. Our main result is that program verification can take place by direct measurement of convergence for programs that are analytic ($\sum^{1}_{1}$) sets and specifications that are coanalytic ($\prod^{1}_{1}$) sets. We use orderings that are not well-founded, but that ensure well-foundedness of limits of finite trees. Our results can also be seen as a new approach to parts of descriptive set theory. In fact, Souslin's Theorem-that every set in $\sum^{1}_{1} \cap \prod^{1}_{1}$ is Borel-is a simple corollary of our main result.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
90-1106.pdf1.23 MBAdobe PDFView/Open
90-1106.ps263.84 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us