The Logic of Partial Functions (LPF) is used to reason about propositions that include terms that can fail to denote values: this paper provides two semantic descriptions for LPF. A Structural Operational Semantics (SOS) gives an intuitive introduction; this is followed by a denotational semantics where relations are chosen for denotations offering an intuitive model of undefined terms. Finally, we illustrate how the denotational semantics can be used as a basis for proofs about propositions that include terms that can fail to denote.
Cliff B. Jones, Matthew J. Lovert. Semantic Models for a Logic of Partial Functions. International Journal of Software and Informatics, 2011,5(1-2Part1):55~76Copy