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 sciencetechnical 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