Definition of Flat Poset and Existence Theorems for Recursive Call

Kazuhisa Ishida; Yasunari Shidama; Adam Grabowski

Formalized Mathematics (2014)

  • Volume: 22, Issue: 1, page 1-10
  • ISSN: 1426-2630

Abstract

top
This text includes the definition and basic notions of product of posets, chain-complete and flat posets, flattening operation, and the existence theorems of recursive call using the flattening operator. First part of the article, devoted to product and flat posets has a purely mathematical quality. Definition 3 allows to construct a flat poset from arbitrary non-empty set [12] in order to provide formal apparatus which eanbles to work with recursive calls within the Mizar langauge. To achieve this we extensively use technical Mizar functors like BaseFunc or RecFunc. The remaining part builds the background for information engineering approach for lists, namely recursive call for posets [21].We formalized some facts from Chapter 8 of this book as an introduction to the next two sections where we concentrate on binary product of posets rather than on a more general case.

How to cite

top

Kazuhisa Ishida, Yasunari Shidama, and Adam Grabowski. "Definition of Flat Poset and Existence Theorems for Recursive Call." Formalized Mathematics 22.1 (2014): 1-10. <http://eudml.org/doc/266832>.

@article{KazuhisaIshida2014,
abstract = {This text includes the definition and basic notions of product of posets, chain-complete and flat posets, flattening operation, and the existence theorems of recursive call using the flattening operator. First part of the article, devoted to product and flat posets has a purely mathematical quality. Definition 3 allows to construct a flat poset from arbitrary non-empty set [12] in order to provide formal apparatus which eanbles to work with recursive calls within the Mizar langauge. To achieve this we extensively use technical Mizar functors like BaseFunc or RecFunc. The remaining part builds the background for information engineering approach for lists, namely recursive call for posets [21].We formalized some facts from Chapter 8 of this book as an introduction to the next two sections where we concentrate on binary product of posets rather than on a more general case.},
author = {Kazuhisa Ishida, Yasunari Shidama, Adam Grabowski},
journal = {Formalized Mathematics},
keywords = {flat posets; recursive calls for posets; flattening operator},
language = {eng},
number = {1},
pages = {1-10},
title = {Definition of Flat Poset and Existence Theorems for Recursive Call},
url = {http://eudml.org/doc/266832},
volume = {22},
year = {2014},
}

TY - JOUR
AU - Kazuhisa Ishida
AU - Yasunari Shidama
AU - Adam Grabowski
TI - Definition of Flat Poset and Existence Theorems for Recursive Call
JO - Formalized Mathematics
PY - 2014
VL - 22
IS - 1
SP - 1
EP - 10
AB - This text includes the definition and basic notions of product of posets, chain-complete and flat posets, flattening operation, and the existence theorems of recursive call using the flattening operator. First part of the article, devoted to product and flat posets has a purely mathematical quality. Definition 3 allows to construct a flat poset from arbitrary non-empty set [12] in order to provide formal apparatus which eanbles to work with recursive calls within the Mizar langauge. To achieve this we extensively use technical Mizar functors like BaseFunc or RecFunc. The remaining part builds the background for information engineering approach for lists, namely recursive call for posets [21].We formalized some facts from Chapter 8 of this book as an introduction to the next two sections where we concentrate on binary product of posets rather than on a more general case.
LA - eng
KW - flat posets; recursive calls for posets; flattening operator
UR - http://eudml.org/doc/266832
ER -

References

top
  1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990. 
  2. [2] Grzegorz Bancerek. Complete lattices. Formalized Mathematics, 2(5):719-725, 1991. 
  3. [3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  4. [4] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  5. [5] Grzegorz Bancerek. Bounds in posets and relational substructures. Formalized Mathematics, 6(1):81-91, 1997. 
  6. [6] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990. 
  7. [7] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  8. [8] Czesław Bylinski. Basic functions and operations on functions. Formalized Mathematics, 1(1):245-254, 1990. 
  9. [9] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  10. [10] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  11. [11] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990. 
  12. [12] B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 2002. Zbl1002.06001
  13. [13] Marek Dudzicz. Representation theorem for finite distributive lattices. Formalized Mathematics, 9(2):261-264, 2001. 
  14. [14] Adam Grabowski. On the category of posets. Formalized Mathematics, 5(4):501-505, 1996.[WoS] 
  15. [15] Kazuhisa Ishida and Yasunari Shidama. Fixpoint theorem for continuous functions on chain-complete posets. Formalized Mathematics, 18(1):47-51, 2010. doi:10.2478/v10037-010-0006-x.[Crossref] 
  16. [16] Artur Korniłowicz. Cartesian products of relations and relational structures. Formalized Mathematics, 6(1):145-152, 1997. 
  17. [17] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1): 115-122, 1990. 
  18. [18] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97-105, 1990. 
  19. [19] Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski - Zorn lemma. Formalized Mathematics, 1(2):387-393, 1990. 
  20. [20] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  21. [21] Glynn Winskel. The Formal Semantics of Programming Languages. The MIT Press, 1993. 
  22. [22] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990. 
  23. [23] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990. 
  24. [24] Mariusz Zynel and Czesław Bylinski. Properties of relational structures, posets, lattices and maps. Formalized Mathematics, 6(1):123-130, 1997. 

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.