Program Algebra over an Algebra
Grzegorz Bancerek
Formalized Mathematics, Tome 20 (2012), p. 309-341 / Harvested from The Polish Digital Mathematics Library
Access to full text
Full (PDF)

We introduce an algebra with free variables, an algebra with undefined values, a program algebra over a term algebra, an algebra with integers, and an algebra with arrays. Program algebra is defined as universal algebra with assignments. Programs depend on the set of generators with supporting variables and supporting terms which determine the value of free variables in the next state. The execution of a program is changing state according to successor function using supporting terms.

Publié le : 2012-01-01
EUDML-ID : urn:eudml:doc:268077 
@article{bwmeta1.element.doi-10_2478_v10037-012-0037-6,
     author = {Grzegorz Bancerek},
     title = {Program Algebra over an Algebra},
     journal = {Formalized Mathematics},
     volume = {20},
     year = {2012},
     pages = {309-341},
     zbl = {06213852},
     language = {en},
     url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_v10037-012-0037-6}
}

Grzegorz Bancerek. Program Algebra over an Algebra. Formalized Mathematics, Tome 20 (2012) pp. 309-341. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_v10037-012-0037-6/

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.

[2] Grzegorz Bancerek. Introduction to trees. Formalized Mathematics, 1(2):421-427, 1990.

[3] Grzegorz Bancerek. K¨onig’s theorem. Formalized Mathematics, 1(3):589-593, 1990.

[4] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.

[5] Grzegorz Bancerek. Cartesian product of functions. Formalized Mathematics, 2(4):547-552, 1991.

[6] Grzegorz Bancerek. K¨onig’s lemma. Formalized Mathematics, 2(3):397-402, 1991.

[7] Grzegorz Bancerek. Algebra of morphisms. Formalized Mathematics, 6(2):303-310, 1997.

[8] Grzegorz Bancerek. Institution of many sorted algebras. Part I: Signature reduct of an algebra. Formalized Mathematics, 6(2):279-287, 1997.

[9] Grzegorz Bancerek. Mizar analysis of algorithms: Preliminaries. Formalized Mathematics, 15(3):87-110, 2007, doi:10.2478/v10037-007-0011-x.[Crossref]

[10] Grzegorz Bancerek. Sorting by exchanging. Formalized Mathematics, 19(2):93-102, 2011, doi: 10.2478/v10037-011-0015-4.[Crossref] | Zbl 1276.68065

[11] Grzegorz Bancerek. Free term algebras. Formalized Mathematics, 20(3):239-256, 2012, doi: 10.2478/v10037-012-0029-6.[Crossref] | Zbl 1296.68085

[12] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.

[13] Grzegorz Bancerek and Piotr Rudnicki. The set of primitive recursive functions. FormalizedMathematics, 9(4):705-720, 2001.

[14] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. FormalizedMathematics, 5(4):485-492, 1996.

[15] Ewa Burakowska. Subalgebras of the universal algebra. Lattices of subalgebras. FormalizedMathematics, 4(1):23-27, 1993.

[16] Czesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180, 1990.

[17] Czesław Bylinski. Finite sequences and tuples of elements of a non-empty sets. FormalizedMathematics, 1(3):529-536, 1990.

[18] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990.

[19] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.

[20] Czesław Bylinski. The modification of a function by a function and the iteration of the composition of a function. Formalized Mathematics, 1(3):521-527, 1990.

[21] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.

[22] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.

[23] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.

[24] Artur Korniłowicz. On the group of automorphisms of universal algebra & many sorted algebra. Formalized Mathematics, 5(2):221-226, 1996.

[25] Artur Korniłowicz and Marco Riccardi. The Borsuk-Ulam theorem. Formalized Mathematics, 20(2):105-112, 2012, doi: 10.2478/v10037-012-0014-0.[Crossref][WoS] | Zbl 06213829

[26] Małgorzata Korolkiewicz. Homomorphisms of many sorted algebras. Formalized Mathematics, 5(1):61-65, 1996.

[27] Jarosław Kotowicz, Beata Madras, and Małgorzata Korolkiewicz. Basic notation of universal algebra. Formalized Mathematics, 3(2):251-253, 1992.

[28] Yatsuka Nakamura and Grzegorz Bancerek. Combining of circuits. Formalized Mathematics, 5(2):283-295, 1996.

[29] Andrzej Nedzusiak. Probability. Formalized Mathematics, 1(4):745-749, 1990.

[30] Beata Perkowska. Free many sorted universal algebra. Formalized Mathematics, 5(1):67-74, 1996.

[31] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329-334, 1990.

[32] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25-34, 1990.

[33] Andrzej Trybulec. Many sorted sets. Formalized Mathematics, 4(1):15-22, 1993.

[34] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37-42, 1996.

[35] Andrzej Trybulec. A scheme for extensions of homomorphisms of many sorted algebras. Formalized Mathematics, 5(2):205-209, 1996.

[36] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4):341-347, 2003.

[37] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.

[38] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575-579, 1990.

[39] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.

[40] Tetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura. Zero-based finite sequences. Formalized Mathematics, 9(4):825-829, 2001.

[41] Edmund Woronowicz. Many argument relations. Formalized Mathematics, 1(4):733-737, 1990.

[42] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990.