International Journal of Software and Informatics
1673-7288
2011
5
1-2Part1
55
76
article
Semantic Models for a Logic of Partial Functions
Semantic Models for a Logic of Partial Functions
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.
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.
logic of partial functions; non-denoting terms; structural operational semantics; denotational semantics
logic of partial functions; non-denoting terms; structural operational semantics; denotational semantics
Cliff B. Jones,Matthew J. Lovert
Cliff B. Jones and Matthew J. Lovert
ijsi/article/abstract/i76