The Library
Metric domains for completeness
Tools
Tools
Tools
Matthews, S. G. (1985) Metric domains for completeness. PhD thesis, University of Warwick.
|
PDF
WRAP_THESIS_Matthews_1985.pdf - Submitted Version - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader Download (3938Kb) | Preview |
Official URL: http://webcat.warwick.ac.uk/record=b1444790~S1
Abstract
Completeness is a semantic non-operational notion of program correctness suggested (but not pursued) by W.W.Wadge. Program verification can be simplified using completeness, firstly by removing the approximation relation from proofs, and secondly by removing partial objects from proofs. The dissertation proves the validity of this approach by demonstrating how it can work in the class of metric domains. We show how the use of Tarski's least fixed point theorem can be replaced by a non-operational unique fixed point theorem for many well behaved Programs. The proof of this theorem is also non-operational. After this we consider the problem of deciding what it means f or a function to be "complete". It is shown that combinators such as function composition are not complete, although they are traditionally assumed to be so. Complete versions for these combinators are given. Absolute functions are proposed as a general model for the notion of a complete function. The theory of mategories is introduced as a vehicle for studying absolute functions.
| Item Type: | Thesis or Dissertation (PhD) | ||||
|---|---|---|---|---|---|
| Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
| Divisions: | Faculty of Science > Computer Science | ||||
| Library of Congress Subject Headings (LCSH): | Completeness theorem | ||||
| Publisher: | University of Warwick. Department of Computer Science | ||||
| Official Date: | March 1985 | ||||
| Dates: |
|
||||
| Identification Number: | CS-RR-076 | ||||
| Institution: | University of Warwick | ||||
| Theses Department: | Department of Computer Science | ||||
| Thesis Type: | PhD | ||||
| Status: | Not Peer Reviewed | ||||
| Publication Status: | Unpublished | ||||
| Supervisor(s)/Advisor: | Wadge, Bill | ||||
| Extent: | 127 leaves | ||||
| Language: | en | ||||
| URI: | http://wrap.warwick.ac.uk/id/eprint/60775 |
Request changes or add full text files to a record
Actions (login required)
 |
View Item |
Downloads
Downloads per month over past year
