Partial Functions in a Total Setting
Simon Finn, Michael Fourman and John LongleyAbstract: We discuss a scheme for defining and reasoning about partial recursive functions within a classical two-valued logic in which all terms denote. We show how a total extension of the partial function introduced by a recursive declaration may be axiomatised within a classical logic, and illustrate by an example the kind of reasoning that our scheme supports. By presenting a naive set-theoretic semantics, we show that the system we propose is logically consistent. We discuss some of the practical advantages and limitations of our approach in the context of mechanical theorem-proving.
ECS-LFCS-96-341, January 1996.
This report is available in the following formats:
- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file