<abstract xmlns="http://www.w3.org/1999/xhtml">We show that the set of all partial predicates over a set <italic>D</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 [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_017_w2aab3b7b1b1b6b1ab1ac17Aa">17</xref>], forms a Kleene algebra. A Kleene algebra is a De Morgan algebra [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_003_w2aab3b7b1b1b6b1ab1ab3Aa">3</xref>] (also called quasi-Boolean algebra) which satisfies the condition <italic>x</italic> ∧<italic>¬:x</italic> ⩽ <italic>y</italic> ∨<italic>¬ :y</italic> (sometimes called the normality axiom). We use the formalization of De Morgan algebras from [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_008_w2aab3b7b1b1b6b1ab1ab8Aa">8</xref>].The term “Kleene algebra” was introduced by A. Monteiro and D. Brignole in [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_003_w2aab3b7b1b1b6b1ab1ab3Aa">3</xref>]. A similar notion of a “normal i-lattice” had been previously studied by J.A. Kalman [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_016_w2aab3b7b1b1b6b1ab1ac16Aa">16</xref>]. More details about the origin of this notion and its relation to other notions can be found in [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_024_w2aab3b7b1b1b6b1ab1ac24Aa">24</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_004_w2aab3b7b1b1b6b1ab1ab4Aa">4</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_001_w2aab3b7b1b1b6b1ab1ab1Aa">1</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_002_w2aab3b7b1b1b6b1ab1ab2Aa">2</xref>]. It should be noted that there is a different widely known class of algebras, also called Kleene algebras [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_022_w2aab3b7b1b1b6b1ab1ac22Aa">22</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_006_w2aab3b7b1b1b6b1ab1ab6Aa">6</xref>], which generalize the algebra of regular expressions, however, the term “Kleene algebra” used in this paper does not refer to them.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 [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_017_w2aab3b7b1b1b6b1ab1ac17Aa">17</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_005_w2aab3b7b1b1b6b1ab1ab5Aa">5</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_018_w2aab3b7b1b1b6b1ab1ac18Aa">18</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_032_w2aab3b7b1b1b6b1ab1ac32Aa">32</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_029_w2aab3b7b1b1b6b1ab1ac29Aa">29</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_030_w2aab3b7b1b1b6b1ab1ac30Aa">30</xref>]. A partial predicate also corresponds to the notion of a partial set [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_026_w2aab3b7b1b1b6b1ab1ac26Aa">26</xref>] 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, <italic>n</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) [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_025_w2aab3b7b1b1b6b1ab1ac25Aa">25</xref>]. In [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_027_w2aab3b7b1b1b6b1ab1ac27Aa">27</xref>] partial sets and DMF-algebras were considered as a basis for unification of set-theoretic and linguistic approaches to probability.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 [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_031_w2aab3b7b1b1b6b1ab1ac31Aa">31</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_028_w2aab3b7b1b1b6b1ab1ac28Aa">28</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_033_w2aab3b7b1b1b6b1ab1ac33Aa">33</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_015_w2aab3b7b1b1b6b1ab1ac15Aa">15</xref>], for formalizing extensions of the Floyd-Hoare logic [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_007_w2aab3b7b1b1b6b1ab1ab7Aa">7</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_009_w2aab3b7b1b1b6b1ab1ab9Aa">9</xref>] which allow reasoning about properties of programs in the case of partial pre- and postconditions [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_023_w2aab3b7b1b1b6b1ab1ac23Aa">23</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_020_w2aab3b7b1b1b6b1ab1ac20Aa">20</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_019_w2aab3b7b1b1b6b1ab1ac19Aa">19</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_021_w2aab3b7b1b1b6b1ab1ac21Aa">21</xref>], for formalizing dynamical models with partial behaviors in the context of the mathematical systems theory [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_011_w2aab3b7b1b1b6b1ab1ac11Aa">11</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_013_w2aab3b7b1b1b6b1ab1ac13Aa">13</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_014_w2aab3b7b1b1b6b1ab1ac14Aa">14</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_012_w2aab3b7b1b1b6b1ab1ac12Aa">12</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_010_w2aab3b7b1b1b6b1ab1ac10Aa">10</xref>].</abstract>

We show that the set of all partial predicates over a set D 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 x ∧¬:x ⩽ y ∨¬ :y (sometimes called the normality axiom). We use the formalization of De Morgan algebras from [8].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.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, n 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.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].

Kleene Algebra of Partial Predicates

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"Kleene Algebra of Partial Predicates"}

We show that the set of all partial predicates over a set D together with the disjunction, conjunction, and negation operations, defined in accordance with the...

Kleene Algebra of Partial Predicates

Data publikacji: 28 lip 2018

Zakres stron: 11 - 20

Otrzymano: 27 mar 2018

DOI: https://doi.org/10.2478/forma-2018-0002

Słowa kluczowe
partial predicate, Kleene algebra

© 2018 Artur Korniłowicz et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Kleene Algebra of Partial Predicates

Data publikacji: 28 lip 2018

Zakres stron: 11 - 20

Otrzymano: 27 mar 2018

DOI: https://doi.org/10.2478/forma-2018-0002

Słowa kluczowepartial predicate, Kleene algebra

© 2018 Artur Korniłowicz et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Słowa kluczowe
partial predicate, Kleene algebra