Analysis of Algorithms: An Example of a Sort Algorithm

Grzegorz Bancerek

Formalized Mathematics (2013)

  • Volume: 21, Issue: 1, page 1-23
  • ISSN: 1426-2630

Abstract

top
We analyse three algorithms: exponentiation by squaring, calculation of maximum, and sorting by exchanging in terms of program algebra over an algebra.

How to cite

top

Grzegorz Bancerek. "Analysis of Algorithms: An Example of a Sort Algorithm." Formalized Mathematics 21.1 (2013): 1-23. <http://eudml.org/doc/267163>.

@article{GrzegorzBancerek2013,
abstract = {We analyse three algorithms: exponentiation by squaring, calculation of maximum, and sorting by exchanging in terms of program algebra over an algebra.},
author = {Grzegorz Bancerek},
journal = {Formalized Mathematics},
keywords = {algorithms; sorting},
language = {eng},
number = {1},
pages = {1-23},
title = {Analysis of Algorithms: An Example of a Sort Algorithm},
url = {http://eudml.org/doc/267163},
volume = {21},
year = {2013},
}

TY - JOUR
AU - Grzegorz Bancerek
TI - Analysis of Algorithms: An Example of a Sort Algorithm
JO - Formalized Mathematics
PY - 2013
VL - 21
IS - 1
SP - 1
EP - 23
AB - We analyse three algorithms: exponentiation by squaring, calculation of maximum, and sorting by exchanging in terms of program algebra over an algebra.
LA - eng
KW - algorithms; sorting
UR - http://eudml.org/doc/267163
ER -

References

top
  1. [1] Grzegorz Bancerek. Mizar analysis of algorithms: Preliminaries. Formalized Mathematics, 15(3):87-110, 2007. doi:10.2478/v10037-007-0011-x.[Crossref] 
  2. [2] Grzegorz Bancerek. Program algebra over an algebra. Formalized Mathematics, 20(4): 309-341, 2012. doi:10.2478/v10037-012-0037-6.[Crossref] Zbl06213852
  3. [3] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990. 
  4. [4] Grzegorz Bancerek. Sorting by exchanging. Formalized Mathematics, 19(2):93-102, 2011. doi:10.2478/v10037-011-0015-4.[Crossref] Zbl1276.68065
  5. [5] Grzegorz Bancerek. Institution of many sorted algebras. Part I: Signature reduct of an algebra. Formalized Mathematics, 6(2):279-287, 1997. 
  6. [6] Grzegorz Bancerek. Complete lattices. Formalized Mathematics, 2(5):719-725, 1991. 
  7. [7] Grzegorz Bancerek. Free term algebras. Formalized Mathematics, 20(3):239-256, 2012. doi:10.2478/v10037-012-0029-6.[Crossref] Zbl1296.68085
  8. [8] Grzegorz Bancerek. Terms over many sorted universal algebra. Formalized Mathematics, 5(2):191-198, 1996. 
  9. [9] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  10. [10] Grzegorz Bancerek. König’s lemma. Formalized Mathematics, 2(3):397-402, 1991. 
  11. [11] Grzegorz Bancerek. Joining of decorated trees. Formalized Mathematics, 4(1):77-82, 1993. 
  12. [12] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Formalized Mathematics, 6(1):93-107, 1997. 
  13. [13] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990. 
  14. [14] Grzegorz Bancerek and Artur Korniłowicz. Yet another construction of free algebra. Formalized Mathematics, 9(4):779-785, 2001. 
  15. [15] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. FormalizedMathematics, 5(4):485-492, 1996. 
  16. [16] Ewa Burakowska. Subalgebras of many sorted algebra. Lattice of subalgebras. FormalizedMathematics, 5(1):47-54, 1996. 
  17. [17] Czesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180, 1990. 
  18. [18] Czesław Bylinski. Finite sequences and tuples of elements of a non-empty sets. FormalizedMathematics, 1(3):529-536, 1990. 
  19. [19] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990. 
  20. [20] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  21. [21] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  22. [22] Czesław Bylinski. Galois connections. Formalized Mathematics, 6(1):131-143, 1997. 
  23. [23] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990. 
  24. [24] Małgorzata Korolkiewicz. Homomorphisms of many sorted algebras. Formalized Mathematics, 5(1):61-65, 1996. 
  25. [25] Jarosław Kotowicz, Beata Madras, and Małgorzata Korolkiewicz. Basic notation of universal algebra. Formalized Mathematics, 3(2):251-253, 1992. 
  26. [26] Rafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887-890, 1990. 
  27. [27] Takashi Mitsuishi and Grzegorz Bancerek. Lattice of fuzzy sets. Formalized Mathematics, 11(4):393-398, 2003. 
  28. [28] Beata Perkowska. Free many sorted universal algebra. Formalized Mathematics, 5(1): 67-74, 1996. 
  29. [29] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329-334, 1990. 
  30. [30] Andrzej Trybulec. A scheme for extensions of homomorphisms of many sorted algebras. Formalized Mathematics, 5(2):205-209, 1996. 
  31. [31] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37-42, 1996. 
  32. [32] Andrzej Trybulec. Many sorted sets. Formalized Mathematics, 4(1):15-22, 1993. 
  33. [33] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990. 
  34. [34] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575-579, 1990. 
  35. [35] Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski - Zorn lemma. FormalizedMathematics, 1(2):387-393, 1990. 
  36. [36] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  37. [37] Tetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura. Zero-based finite sequences. Formalized Mathematics, 9(4):825-829, 2001. 
  38. [38] Edmund Woronowicz. Many argument relations. Formalized Mathematics, 1(4):733-737, 1990. 
  39. [39] 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.