Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

**Yatsuka Nakamura**- Shinshu University, Nagano
**Piotr Rudnicki**- University of Alberta, Edmonton
**Andrzej Trybulec**- Warsaw University, Bialystok
**Pauline N. Kawamoto**- Shinshu University, Nagano

- This article is the second in a series of four articles (started with [19] and continued in [18], [20]) about modelling circuits by many sorted algebras.\par First, we introduce some additional terminology for many sorted signatures. The vertices of such signatures are divided into input vertices and inner vertices. A many sorted signature is called {\em circuit like} if each sort is a result sort of at most one operation. Next, we introduce some notions for many sorted algebras and many sorted free algebras. Free envelope of an algebra is a free algebra generated by the sorts of the algebra. Evaluation of an algebra is defined as a homomorphism from the free envelope of the algebra into the algebra. We define depth of elements of free many sorted algebras.\par A many sorted signature is said to be monotonic if every finitely generated algebra over it is locally finite (finite in each sort). Monotonic signatures are used (see [18],[20]) in modelling backbones of circuits without directed cycles.

Partial funding for this work has been provided by: Shinshu Endowment Fund for Information Science, NSERC Grant OGP9207, JSTF award 651-93-S009.

- Many Sorted Signatures
- Free Many Sorted Algebras

- [1]
Grzegorz Bancerek.
Cardinal numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Grzegorz Bancerek.
Introduction to trees.
*Journal of Formalized Mathematics*, 1, 1989. - [3]
Grzegorz Bancerek.
K\"onig's theorem.
*Journal of Formalized Mathematics*, 2, 1990. - [4]
Grzegorz Bancerek.
K\"onig's Lemma.
*Journal of Formalized Mathematics*, 3, 1991. - [5]
Grzegorz Bancerek.
Sets and functions of trees and joining operations of trees.
*Journal of Formalized Mathematics*, 4, 1992. - [6]
Grzegorz Bancerek.
Joining of decorated trees.
*Journal of Formalized Mathematics*, 5, 1993. - [7]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
*Journal of Formalized Mathematics*, 1, 1989. - [8]
Grzegorz Bancerek and Piotr Rudnicki.
On defining functions on trees.
*Journal of Formalized Mathematics*, 5, 1993. - [9]
Ewa Burakowska.
Subalgebras of many sorted algebra. Lattice of subalgebras.
*Journal of Formalized Mathematics*, 6, 1994. - [10]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [11]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [12]
Czeslaw Bylinski.
Some basic properties of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [13]
Czeslaw Bylinski.
Finite sequences and tuples of elements of a non-empty sets.
*Journal of Formalized Mathematics*, 2, 1990. - [14]
Patricia L. Carlson and Grzegorz Bancerek.
Context-free grammar --- part I.
*Journal of Formalized Mathematics*, 4, 1992. - [15]
Agata Darmochwal.
Finite sets.
*Journal of Formalized Mathematics*, 1, 1989. - [16]
Malgorzata Korolkiewicz.
Homomorphisms of many sorted algebras.
*Journal of Formalized Mathematics*, 6, 1994. - [17]
Beata Madras.
Product of family of universal algebras.
*Journal of Formalized Mathematics*, 5, 1993. - [18]
Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto.
Introduction to circuits, I.
*Journal of Formalized Mathematics*, 6, 1994. - [19]
Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto.
Preliminaries to circuits, I.
*Journal of Formalized Mathematics*, 6, 1994. - [20]
Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto.
Introduction to circuits, II.
*Journal of Formalized Mathematics*, 7, 1995. - [21]
Andrzej Nedzusiak.
$\sigma$-fields and probability.
*Journal of Formalized Mathematics*, 1, 1989. - [22]
Beata Perkowska.
Free many sorted universal algebra.
*Journal of Formalized Mathematics*, 6, 1994. - [23]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [24]
Andrzej Trybulec.
Many-sorted sets.
*Journal of Formalized Mathematics*, 5, 1993. - [25]
Andrzej Trybulec.
Many sorted algebras.
*Journal of Formalized Mathematics*, 6, 1994. - [26]
Wojciech A. Trybulec.
Pigeon hole principle.
*Journal of Formalized Mathematics*, 2, 1990. - [27]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [28]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [29]
Edmund Woronowicz.
Relations defined on sets.
*Journal of Formalized Mathematics*, 1, 1989.

[ Download a postscript version, MML identifier index, Mizar home page]