Program Algebra over an Algebra

Grzegorz Bancerek

Formalized Mathematics (2012)

  • Volume: 20, Issue: 4, page 309-341
  • ISSN: 1426-2630

Abstract

top
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.

How to cite

top

Grzegorz Bancerek. "Program Algebra over an Algebra." Formalized Mathematics 20.4 (2012): 309-341. <http://eudml.org/doc/268077>.

@article{GrzegorzBancerek2012,
abstract = {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.},
author = {Grzegorz Bancerek},
journal = {Formalized Mathematics},
language = {eng},
number = {4},
pages = {309-341},
title = {Program Algebra over an Algebra},
url = {http://eudml.org/doc/268077},
volume = {20},
year = {2012},
}

TY - JOUR
AU - Grzegorz Bancerek
TI - Program Algebra over an Algebra
JO - Formalized Mathematics
PY - 2012
VL - 20
IS - 4
SP - 309
EP - 341
AB - 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.
LA - eng
UR - http://eudml.org/doc/268077
ER -

References

top
  1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990. 
  2. [2] Grzegorz Bancerek. Introduction to trees. Formalized Mathematics, 1(2):421-427, 1990. 
  3. [3] Grzegorz Bancerek. K¨onig’s theorem. Formalized Mathematics, 1(3):589-593, 1990. 
  4. [4] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  5. [5] Grzegorz Bancerek. Cartesian product of functions. Formalized Mathematics, 2(4):547-552, 1991. 
  6. [6] Grzegorz Bancerek. K¨onig’s lemma. Formalized Mathematics, 2(3):397-402, 1991. 
  7. [7] Grzegorz Bancerek. Algebra of morphisms. Formalized Mathematics, 6(2):303-310, 1997. 
  8. [8] Grzegorz Bancerek. Institution of many sorted algebras. Part I: Signature reduct of an algebra. Formalized Mathematics, 6(2):279-287, 1997. 
  9. [9] Grzegorz Bancerek. Mizar analysis of algorithms: Preliminaries. Formalized Mathematics, 15(3):87-110, 2007, doi:10.2478/v10037-007-0011-x.[Crossref] 
  10. [10] Grzegorz Bancerek. Sorting by exchanging. Formalized Mathematics, 19(2):93-102, 2011, doi: 10.2478/v10037-011-0015-4.[Crossref] Zbl1276.68065
  11. [11] Grzegorz Bancerek. Free term algebras. Formalized Mathematics, 20(3):239-256, 2012, doi: 10.2478/v10037-012-0029-6.[Crossref] Zbl1296.68085
  12. [12] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990. 
  13. [13] Grzegorz Bancerek and Piotr Rudnicki. The set of primitive recursive functions. FormalizedMathematics, 9(4):705-720, 2001. 
  14. [14] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. FormalizedMathematics, 5(4):485-492, 1996. 
  15. [15] Ewa Burakowska. Subalgebras of the universal algebra. Lattices of subalgebras. FormalizedMathematics, 4(1):23-27, 1993. 
  16. [16] Czesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180, 1990. 
  17. [17] Czesław Bylinski. Finite sequences and tuples of elements of a non-empty sets. FormalizedMathematics, 1(3):529-536, 1990. 
  18. [18] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990. 
  19. [19] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  20. [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. [21] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  22. [22] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  23. [23] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990. 
  24. [24] Artur Korniłowicz. On the group of automorphisms of universal algebra & many sorted algebra. Formalized Mathematics, 5(2):221-226, 1996. 
  25. [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] Zbl06213829
  26. [26] Małgorzata Korolkiewicz. Homomorphisms of many sorted algebras. Formalized Mathematics, 5(1):61-65, 1996. 
  27. [27] Jarosław Kotowicz, Beata Madras, and Małgorzata Korolkiewicz. Basic notation of universal algebra. Formalized Mathematics, 3(2):251-253, 1992. 
  28. [28] Yatsuka Nakamura and Grzegorz Bancerek. Combining of circuits. Formalized Mathematics, 5(2):283-295, 1996. 
  29. [29] Andrzej Nedzusiak. Probability. Formalized Mathematics, 1(4):745-749, 1990. 
  30. [30] Beata Perkowska. Free many sorted universal algebra. Formalized Mathematics, 5(1):67-74, 1996. 
  31. [31] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329-334, 1990. 
  32. [32] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25-34, 1990. 
  33. [33] Andrzej Trybulec. Many sorted sets. Formalized Mathematics, 4(1):15-22, 1993. 
  34. [34] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37-42, 1996. 
  35. [35] Andrzej Trybulec. A scheme for extensions of homomorphisms of many sorted algebras. Formalized Mathematics, 5(2):205-209, 1996. 
  36. [36] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4):341-347, 2003. 
  37. [37] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990. 
  38. [38] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575-579, 1990. 
  39. [39] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  40. [40] Tetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura. Zero-based finite sequences. Formalized Mathematics, 9(4):825-829, 2001. 
  41. [41] Edmund Woronowicz. Many argument relations. Formalized Mathematics, 1(4):733-737, 1990. 
  42. [42] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.