E3: A logic for reasoning equationally in the presence of partiality

摘要

Partiality abounds in specifications and programs. We present a three-valued typed logic for reasoning equationally about programming in the presence of partial functions. The logic in essence is a combination of the equational logic E and typed LPF. Of course, there are already many logics in which some classical theorems acquire the status of neither-true--nor-false. What is distinctive here is that we preserve the equational reasoning style of E, as well as most of its main theorems. The principal losses among the theorems are the law of the excluded middle, the anti-symmetry of implication, a small complication in the trading law for existential quantification, and the requirement to show definedness when using instantiation. The main loss among proof methods is proof by mutual implication; we present some new proof strategies that make up for this loss. Some proofs are longer than in E, but the heuristics commonly used in the proof methodology of E remain valid. We present a Hilbert-style axiomatisation of the logic in which modus ponens and generalisation are the only inference rules. The axiomatisation is easily modified to yield a classical axiomatisation of E itself We suggest that the logic may be readily extended to a many-valued logic, and that this will have its uses.