<abstract xmlns="http://www.w3.org/1999/xhtml"><p> 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.</p></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.

Definition of Flat Poset and Existence Theorems for Recursive Call

Institute of Informatics University of Białystok Akademicka 2, 15-267 Białystok Poland

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

{"article-title":"Definition of Flat Poset and Existence Theorems for Recursive Call"}

This text includes the definition and basic notions of product of posets, chain-complete and flat posets, flattening operation, and the existence theorems of...

Definition of Flat Poset and Existence Theorems for Recursive Call

Data publikacji: 30 mar 2014

Zakres stron: 1 - 10

DOI: https://doi.org/10.2478/forma-2014-0001

Słowa kluczowe
flat posets, recursive calls for posets, flattening operator

© by Kazuhisa Ishida

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

Definition of Flat Poset and Existence Theorems for Recursive Call

Data publikacji: 30 mar 2014

Zakres stron: 1 - 10

DOI: https://doi.org/10.2478/forma-2014-0001

Słowa kluczoweflat posets, recursive calls for posets, flattening operator

© by Kazuhisa Ishida

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

Słowa kluczowe
flat posets, recursive calls for posets, flattening operator