Erschienen in:
Formalized Mathematics, 26 (2018) 1, Seite 11-20
Sprache:
Englisch
DOI:
10.2478/forma-2018-0002
ISSN:
1898-9934;
1426-2630
Entstehung:
Anmerkungen:
Beschreibung:
<jats:title>Summary</jats:title>
<jats:p>We show that the set of all partial predicates over a set <jats:italic>D</jats:italic> together with the disjunction, conjunction, and negation operations, defined in accordance with the truth tables of S.C. Kleene’s strong logic of indeterminacy [17], forms a Kleene algebra. A Kleene algebra is a De Morgan algebra [3] (also called quasi-Boolean algebra) which satisfies the condition <jats:italic>x</jats:italic> ∧<jats:italic>¬:x</jats:italic> ⩽ <jats:italic>y</jats:italic> ∨<jats:italic>¬ :y</jats:italic> (sometimes called the normality axiom). We use the formalization of De Morgan algebras from [8].</jats:p>
<jats:p>The term “Kleene algebra” was introduced by A. Monteiro and D. Brignole in [3]. A similar notion of a “normal i-lattice” had been previously studied by J.A. Kalman [16]. More details about the origin of this notion and its relation to other notions can be found in [24, 4, 1, 2]. It should be noted that there is a different widely known class of algebras, also called Kleene algebras [22, 6], which generalize the algebra of regular expressions, however, the term “Kleene algebra” used in this paper does not refer to them.</jats:p>
<jats:p>Algebras of partial predicates naturally arise in computability theory in the study on partial recursive predicates. They were studied in connection with non-classical logics [17, 5, 18, 32, 29, 30]. A partial predicate also corresponds to the notion of a partial set [26] on a given domain, which represents a (partial) property which for any given element of this domain may hold, not hold, or neither hold nor not hold. The field of all partial sets on a given domain is an algebra with generalized operations of union, intersection, complement, and three constants (0, 1, <jats:italic>n</jats:italic> which is the fixed point of complement) which can be generalized to an equational class of algebras called DMF-algebras (De Morgan algebras with a single fixed point of involution) [25]. In [27] partial sets and DMF-algebras were considered as a basis for unification of set-theoretic and linguistic approaches to probability.</jats:p>
<jats:p>Partial predicates over classes of mathematical models of data were used for formalizing semantics of computer programs in the composition-nominative approach to program formalization [31, 28, 33, 15], for formalizing extensions of the Floyd-Hoare logic [7, 9] which allow reasoning about properties of programs in the case of partial pre- and postconditions [23, 20, 19, 21], for formalizing dynamical models with partial behaviors in the context of the mathematical systems theory [11, 13, 14, 12, 10].</jats:p>