Formalized Mathematics    (ISSN 1426-2630)
Volume 5, Number 4 (1996): pdf, ps, dvi.
  1. Andrzej Trybulec. Left and Right Component of the Complement of a Special Closed Curve, Formalized Mathematics 5(4), pages 465-468, 1996. MML Identifier: GOBOARD9
    Summary: In the article the concept of the left and right component are introduced. These are the auxiliary notions needed in the proof of Jordan Curve Theorem.
  2. Grzegorz Bancerek. Reduction Relations, Formalized Mathematics 5(4), pages 469-478, 1996. MML Identifier: REWRITE1
    Summary: The goal of the article is to start the formalization of Knuth-Bendix completion method (see \cite{BachmairDershowitz}, \cite{KlopMiddeldorp} or \cite{HofLinCS}; see also \cite{KnuthBendix},\cite{Huet81}), i.e. to formalize the concept of the completion of a reduction relation. The completion of a reduction relation $R$ is a complete reduction relation equivalent to $R$ such that convertible elements have the same normal forms. The theory formalized in the article includes concepts and facts concerning normal forms, terminating reductions, Church-Rosser property, and equivalence of reduction relations.
  3. Robert Milewski. Lattice of Congruences in Many Sorted Algebra, Formalized Mathematics 5(4), pages 479-483, 1996. MML Identifier: MSUALG_5
    Summary:
  4. Grzegorz Bancerek, Andrzej Trybulec. Miscellaneous Facts about Functions, Formalized Mathematics 5(4), pages 485-492, 1996. MML Identifier: FUNCT_7
    Summary:
  5. Andrzej Trybulec. Examples of Category Structures, Formalized Mathematics 5(4), pages 493-500, 1996. MML Identifier: ALTCAT_2
    Summary: We continue the formalization of the category theory.
  6. Adam Grabowski. On the Category of Posets, Formalized Mathematics 5(4), pages 501-505, 1996. MML Identifier: ORDERS_3
    Summary: In the paper the construction of a category of partially ordered sets is shown: in the second section according to \cite{CAT_1.ABS} and in the third section according to the definition given in \cite{ALTCAT_1.ABS}. Some of useful notions such as monotone map and the set of monotone maps between relational structures are given.
  7. Andrzej Trybulec, Yatsuka Nakamura, Piotr Rudnicki. An Extension of \bf SCM, Formalized Mathematics 5(4), pages 507-512, 1996. MML Identifier: SCMFSA_1
    Summary:
  8. Yatsuka Nakamura, Andrzej Trybulec. Components and Unions of Components, Formalized Mathematics 5(4), pages 513-517, 1996. MML Identifier: CONNSP_3
    Summary: First, we generalized {\bf skl} function for a subset of topological spaces the value of which is the component including the set. Second, we introduced a concept of union of components a family of which has good algebraic properties. At the end, we discuss relationship between connectivity of a set as a subset in the whole space and as a subset of a subspace.
  9. Andrzej Trybulec, Yatsuka Nakamura, Piotr Rudnicki. The \SCMFSA Computer, Formalized Mathematics 5(4), pages 519-528, 1996. MML Identifier: SCMFSA_2
    Summary:
  10. Artur Kornilowicz. On the Many Sorted Closure Operator and the Many Sorted Closure System, Formalized Mathematics 5(4), pages 529-536, 1996. MML Identifier: CLOSURE1
    Summary:
  11. Andrzej Trybulec, Yatsuka Nakamura. Computation in \SCMFSA, Formalized Mathematics 5(4), pages 537-542, 1996. MML Identifier: SCMFSA_3
    Summary: The properties of computations in ${\bf SCM}_{\rm FSA}$ are investigated.
  12. Artur Kornilowicz. On the Closure Operator and the Closure System of Many Sorted Sets, Formalized Mathematics 5(4), pages 543-551, 1996. MML Identifier: CLOSURE2
    Summary: In this paper definitions of many sorted closure system and many sorted closure operator are introduced. These notations are also introduced in \cite{CLOSURE1.ABS}, but in another meaning. In this article closure system is absolutely multiplicative subset family of many sorted sets and in \cite{CLOSURE1.ABS} is many sorted absolutely multiplicative subset family of many sorted sets. Analogously, closure operator is function between many sorted sets and in \cite{CLOSURE1.ABS} is many sorted function from a many sorted set into a many sorted set.
  13. Grzegorz Bancerek. Translations, Endomorphisms, and Stable Equational Theories, Formalized Mathematics 5(4), pages 553-564, 1996. MML Identifier: MSUALG_6
    Summary: Equational theories of an algebra, i.e. the equivalence relation closed under translations and endomorphisms, are formalized. The correspondence between equational theories and term rewriting systems is discussed in the paper. We get as the main result that any pair of elements of an algebra belongs to the equational theory generated by a set $A$ of axioms iff the elements are convertible w.r.t. term rewriting reduction determined by $A$.\par The theory is developed according to \cite{WECHLER}.
  14. Robert Milewski. More on the Lattice of Many Sorted Equivalence Relations, Formalized Mathematics 5(4), pages 565-569, 1996. MML Identifier: MSUALG_7
    Summary:
  15. Andrzej Trybulec, Yatsuka Nakamura. Modifying Addresses of Instructions of \SCMFSA, Formalized Mathematics 5(4), pages 571-576, 1996. MML Identifier: SCMFSA_4
    Summary:
  16. Czeslaw Bylinski, Piotr Rudnicki. The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. Part I, Formalized Mathematics 5(4), pages 577-582, 1996. MML Identifier: MSSCYC_1
    Summary: We prove a number of auxiliary facts about graphs, mainly about vertex sequences of chains and oriented chains. Then we define a graph to be {\em well-founded} if for each vertex in the graph the length of oriented chains ending at the vertex is bounded. A {\em well-founded} graph does not have directed cycles or infinite descending chains. In the second part of the article we prove some auxiliary facts about free algebras and locally-finite algebras.
  17. Andrzej Trybulec, Yatsuka Nakamura. Relocability for \SCMFSA, Formalized Mathematics 5(4), pages 583-586, 1996. MML Identifier: SCMFSA_5
    Summary:
  18. Robert Milewski. More on the Lattice of Congruences in Many Sorted Algebra, Formalized Mathematics 5(4), pages 587-590, 1996. MML Identifier: MSUALG_8
    Summary:
  19. Czeslaw Bylinski, Piotr Rudnicki. The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. Part II, Formalized Mathematics 5(4), pages 591-593, 1996. MML Identifier: MSSCYC_2
    Summary: The graph induced by a many sorted signature is defined as follows: the vertices are the symbols of sorts, and if a sort $s$ is an argument of an operation with result sort $t$, then a directed edge $[s, t]$ is in the graph. The key lemma states relationship between the depth of elements of a free many sorted algebra over a signature and the length of directed chains in the graph induced by the signature. Then we prove that a monotonic many sorted signature (every finitely-generated algebra over it is locally-finite) induces a {\em well-founded} graph. The converse holds with an additional assumption that the signature is finitely operated, i.e. there is only a finite number of operations with the given result sort.
  20. Andrzej Trybulec. Functors for Alternative Categories, Formalized Mathematics 5(4), pages 595-608, 1996. MML Identifier: FUNCTOR0
    Summary: An attempt to define the concept of a functor covering both cases (covariant and contravariant) resulted in a structure consisting of two fields: the object map and the morphism map, the first one mapping the Cartesian squares of the set of objects rather than the set of objects. We start with an auxiliary notion of {\em bifunction}, i.e. a function mapping the Cartesian square of a set $A$ into the Cartesian square of a set $B$. A {\em bifunction} $f$ is said to be {\em covariant} if there is a function $g$ from $A$ into $B$ that $f$ is the Cartesian square of $g$ and $f$ is {\em contravariant} if there is a function $g$ such that $f(o_1,o_2) = \langle g(o_2),g(o_1) \rangle$. The term {\em transformation}, another auxiliary notion, might be misleading. It is not related to natural transformations. A transformation from a many sorted set $A$ indexed by $I$ into a many sorted set $B$ indexed by $J$ w.r.t. a function $f$ from $I$ into $J$ is a (many sorted) function from $A$ into $B \cdot f$. Eventually, the morphism map of a functor from $C_1$ into $C_2$ is a transformation from the arrows of the category $C_1$ into the composition of the object map of the functor and the arrows of $C_2$.\par Several kinds of functor structures have been defined: one-to-one, faithful, onto, full and id-preserving. We were pressed to split property that the composition be preserved into two: comp-preserving (for covariant functors) and comp-reversing (for contravariant functors). We defined also some operation on functors, e.g. the composition, the inverse functor. In the last section it is defined what is meant that two categories are isomorphic (anti-isomorphic).
  21. Claus Zinn, Wolfgang Jaksch. Basic Properties of Functor Structures, Formalized Mathematics 5(4), pages 609-613, 1996. MML Identifier: FUNCTOR1
    Summary: This article presents some theorems about functor structures. We start with some basic lemmata concerning the composition of functor structures. Then, two theorems about the restriction operator are formulated. Later we show two theorems concerning the properties 'full' and 'faithful' of functor structures which are equivalent to the 'onto' and 'one-to-one' properties of their morphmaps, respectively. Furthermore, we prove some theorems about the inversion of functor structures.
  22. Noriko Asamoto. Some Multi Instructions Defined by Sequence of Instructions of \SCMFSA, Formalized Mathematics 5(4), pages 615-619, 1996. MML Identifier: SCMFSA_7
    Summary:
  23. Mariusz Giero. More on Products of Many Sorted Algebras, Formalized Mathematics 5(4), pages 621-626, 1996. MML Identifier: PRALG_3
    Summary: This article is continuation of an article defining products of many sorted algebras \cite{PRALG_2.ABS}. Some properties of notions such as commute, Frege, Args() are shown in this article. Notions of constant of operations in many sorted algebras and projection of products of family of many sorted algebras are defined. There is also introduced the notion of class of family of many sorted algebras. The main theorem states that product of family of many sorted algebras and product of class of family of many sorted algebras are isomorphic.