Partial Functions in a Total Setting

Simon Finn, Michael Fourman and John Longley

Abstract: 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:

Previous | Index | Next