Convergence Measures
| dc.contributor.author | Klarlund, Nils | en_US |
| dc.date.accessioned | 2007-04-23T17:46:07Z | |
| dc.date.available | 2007-04-23T17:46:07Z | |
| dc.date.issued | 1990-03 | en_US |
| dc.description.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. | en_US |
| dc.format.extent | 1257498 bytes | |
| dc.format.extent | 270176 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.format.mimetype | application/postscript | |
| dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1106 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/6946 | |
| dc.language.iso | en_US | en_US |
| dc.publisher | Cornell University | en_US |
| dc.subject | computer science | en_US |
| dc.subject | technical report | en_US |
| dc.title | Convergence Measures | en_US |
| dc.type | technical report | en_US |