Abstract
This paper compares the finitary three-valued logic LPF and the
infinitary two-valued logic MPLomega, the logics underlying VDM SL and
COLD-K.
These logics reflect different approaches to reasoning about partial
functions and bringing recursive function definitions into proofs.
The purpose of the comparison is to acquire insight into the
relationship between these approaches.
A natural translation from LPF to MPLomega is given.
It is shown that what can be proved remains the same after translation,
in case strictness axioms are added to LPF or removed from MPLomega.
The translation from LPF to MPLomega is extended to recursive function
definitions and this translation is next used to justify some ways of
bringing the definitions of partial functions into proofs using LPF.
Preprint available here.