Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994
Association of Mizar Users
Preliminaries to Circuits, II
-
Yatsuka Nakamura
-
Shinshu University, Nagano
-
Piotr Rudnicki
-
University of Alberta, Edmonton
-
Andrzej Trybulec
-
Warsaw University, Bialystok
-
Pauline N. Kawamoto
-
Shinshu University, Nagano
Summary.
-
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.
The terminology and notation used in this paper have been
introduced in the following articles
[23]
[12]
[27]
[1]
[28]
[10]
[15]
[7]
[11]
[21]
[3]
[2]
[4]
[5]
[6]
[24]
[17]
[25]
[13]
[22]
[9]
[8]
[14]
[29]
[16]
[26]
[19]
-
Many Sorted Signatures
-
Free Many Sorted Algebras
Bibliography
- [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.
Received December 13, 1994
[
Download a postscript version,
MML identifier index,
Mizar home page]