Skip to main content


eCommons@Cornell

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

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/6946
Title: Convergence Measures
Authors: Klarlund, Nils
Keywords: computer science
technical report
Issue Date: Mar-1990
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1106
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.
URI: http://hdl.handle.net/1813/6946
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