LPF AND MPL-OMEGA - A LOGICAL COMPARISON OF VDM SL AND COLD-K

This paper compares the finitary three-valued logic LPF and the infinitary two-valued logic MPL(omega), 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 MPL(omega) 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 MPL(omega). The translation from LPF to MPL(omega) 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.