<abstract xmlns="http://www.w3.org/1999/xhtml">This paper continues formalization in the Mizar system <xref ref-type="bibr" rid="j_forma-2018-0012_ref_002_w2aab3b7b4b1b6b1ab1ab2Aa">[2</xref>, <xref ref-type="bibr" rid="j_forma-2018-0012_ref_001_w2aab3b7b4b1b6b1ab1ab1Aa">1</xref>] of basic notions of the composition-nominative approach to program semantics <xref ref-type="bibr" rid="j_forma-2018-0012_ref_014_w2aab3b7b4b1b6b1ab1ac14Aa">[14]</xref> which was started in <xref ref-type="bibr" rid="j_forma-2018-0012_ref_008_w2aab3b7b4b1b6b1ab1ab8Aa">[8</xref>, <xref ref-type="bibr" rid="j_forma-2018-0012_ref_012_w2aab3b7b4b1b6b1ab1ac12Aa">12</xref>, <xref ref-type="bibr" rid="j_forma-2018-0012_ref_010_w2aab3b7b4b1b6b1ab1ac10Aa">10</xref>].The composition-nominative approach studies mathematical models of computer programs and data on various levels of abstraction and generality and provides tools for reasoning about their properties. In particular, data in computer systems are modeled as nominative data <xref ref-type="bibr" rid="j_forma-2018-0012_ref_015_w2aab3b7b4b1b6b1ab1ac15Aa">[15]</xref>. Besides formalization of semantics of programs, certain elements of the composition-nominative approach were applied to abstract systems in a mathematical systems theory <xref ref-type="bibr" rid="j_forma-2018-0012_ref_004_w2aab3b7b4b1b6b1ab1ab4Aa">[4</xref>, <xref ref-type="bibr" rid="j_forma-2018-0012_ref_006_w2aab3b7b4b1b6b1ab1ab6Aa">6</xref>, <xref ref-type="bibr" rid="j_forma-2018-0012_ref_007_w2aab3b7b4b1b6b1ab1ab7Aa">7</xref>, <xref ref-type="bibr" rid="j_forma-2018-0012_ref_005_w2aab3b7b4b1b6b1ab1ab5Aa">5</xref>, <xref ref-type="bibr" rid="j_forma-2018-0012_ref_003_w2aab3b7b4b1b6b1ab1ab3Aa">3</xref>].In the paper we give a formal definition of the notions of a binominative function over given sets of names and values (i.e. a partial function which maps simple-named complex-valued nominative data to such data) and a nominative predicate (a partial predicate on simple-named complex-valued nominative data). The sets of such binominative functions and nominative predicates form the carrier of the generalized Glushkov algorithmic algebra for simple-named complex-valued nominative data <xref ref-type="bibr" rid="j_forma-2018-0012_ref_015_w2aab3b7b4b1b6b1ab1ac15Aa">[15]</xref>. This algebra can be used to formalize algorithms which operate on various data structures (such as multidimensional arrays, lists, etc.) and reason about their properties.In particular, we formalize the operations of this algebra which require a specification of a data domain and which include the existential quantifier, the assignment composition, the composition of superposition into a predicate, the composition of superposition into a binominative function, the name checking predicate. The details on formalization of nominative data and the operations of the algorithmic algebra over them are described in [<xref ref-type="bibr" rid="j_forma-2018-0012_ref_011_w2aab3b7b4b1b6b1ab1ac11Aa">11</xref>, <xref ref-type="bibr" rid="j_forma-2018-0012_ref_013_w2aab3b7b4b1b6b1ab1ac13Aa">13</xref>, <xref ref-type="bibr" rid="j_forma-2018-0012_ref_009_w2aab3b7b4b1b6b1ab1ab9Aa">9</xref>].</abstract>

This paper continues formalization in the Mizar system [2, 1] of basic notions of the composition-nominative approach to program semantics [14] which was started in [8, 12, 10].The composition-nominative approach studies mathematical models of computer programs and data on various levels of abstraction and generality and provides tools for reasoning about their properties. In particular, data in computer systems are modeled as nominative data [15]. Besides formalization of semantics of programs, certain elements of the composition-nominative approach were applied to abstract systems in a mathematical systems theory [4, 6, 7, 5, 3].In the paper we give a formal definition of the notions of a binominative function over given sets of names and values (i.e. a partial function which maps simple-named complex-valued nominative data to such data) and a nominative predicate (a partial predicate on simple-named complex-valued nominative data). The sets of such binominative functions and nominative predicates form the carrier of the generalized Glushkov algorithmic algebra for simple-named complex-valued nominative data [15]. This algebra can be used to formalize algorithms which operate on various data structures (such as multidimensional arrays, lists, etc.) and reason about their properties.In particular, we formalize the operations of this algebra which require a specification of a data domain and which include the existential quantifier, the assignment composition, the composition of superposition into a predicate, the composition of superposition into a binominative function, the name checking predicate. The details on formalization of nominative data and the operations of the algorithmic algebra over them are described in [11, 13, 9].

On an Algorithmic Algebra over Simple-Named Complex-Valued Nominative Data

Formalized Mathematics

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

{"article-title":"On an Algorithmic Algebra over Simple-Named Complex-Valued Nominative Data"}

This paper continues formalization in the Mizar system [2, 1] of basic notions of the composition-nominative approach to program semantics [14] which was...

On an Algorithmic Algebra over Simple-Named Complex-Valued Nominative Data

Pubblicato online: 24 dic 2018

Pagine: 149 - 158

Accettato: 29 giu 2018

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

Parole chiave
Glushkov algorithmic algebra, nominative data

© 2018 Ievgen Ivanov et al., published by Sciendo

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

On an Algorithmic Algebra over Simple-Named Complex-Valued Nominative Data

Pubblicato online: 24 dic 2018

Pagine: 149 - 158

Accettato: 29 giu 2018

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

Parole chiaveGlushkov algorithmic algebra, nominative data

© 2018 Ievgen Ivanov et al., published by Sciendo

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

Parole chiave
Glushkov algorithmic algebra, nominative data