
The Library
Metric domains for completeness
Tools
Matthews, Stephen G. (1985) Metric domains for completeness. PhD thesis, University of Warwick.
|
PDF
WRAP_THESIS_Matthews_1985.pdf - Submitted Version - Requires a PDF viewer. 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 (PhD) | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
Library of Congress Subject Headings (LCSH): | Completeness theorem | ||||
Publisher: | University of Warwick. Department of Computer Science | ||||
Official Date: | March 1985 | ||||
Dates: |
|
||||
DOI: | 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 |
Request changes or add full text files to a record
Repository staff actions (login required)
![]() |
View Item |
Downloads
Downloads per month over past year