Database Reference
In-Depth Information
X ar(o i )
o i
0
X ar(o i )
}
Σ P (X)
=
Σ P |
ar(o i )
=
×{
i
o i Σ P
o i
Σ P & ar(o i )
1
n
X
where X is the set of variables and the finite Cartesian products X n
=
×···×
X
are used as a domain for the finitary n -ary operator o i
ar(o i ) .More
formally, for a signature Σ P we define the endofunctor (denoted by the same sym-
bol) Σ P :
Σ P with n
=
o i Σ P B ar(o i ) ,
−→
Set
Set such that for any object B in Set , Σ P (B)
o i Σ P f ar(o i ) .
Moreover, for each set of variables X (an object in Set ) we define the endo-
functor (X
and any arrow in Set (a function) f
:
B
−→
C , Σ P (f )
:
−→
Σ P )
Set
Set such that for any object B in Set , (X
Σ P )(B)
o i Σ P B ar(o i ) , and any arrow in Set (a function) f
X
:
B
−→
C , (X
Σ P )(f )
id X } o i Σ P f ar(o i ) , where id X is the identity function for the set X .
Consequently, the free Σ P -algebra
{
T P X on a set of variables X ( X is called a set
of free generators , and
T P X is said to be freely generated by X ) may be computed
as the union of the chain (so that the initial X
Σ P -algebra defined below is the
least fixed point (lfp) of the functor X
Σ P :
Set
Set , with the isomorphism
T P X
I X
Σ P (
T P X) ):
)
X Σ P X Σ P X Σ P ( ) ⊆···
Σ P X
∅⊆
X
Σ P (
)
X
Σ P (
obtained by iterating the functor X
) equal
to the set of nullary operators (i.e., constants) in Σ P . Hence, in Set we have the
inclusion of variables in terms, inl X : X T P X , and the injective mapping inr X :
Σ P ( T P X) T P X which represents the composition of more complex terms from
themoresimpletermsin
Σ P on the empty set
, with Σ P (
T P X , that is, by using the operations o i
Σ P with n
=
ar(o i )
1 and hence for t 1 ,...,t n T P X , inr X ((t 1 ,...,t n ),i)
=
o i (t 1 ,...,t n )
T P X (if ar(o i )
o i T P X ).
The fact that standard mathematical constructions are inductive is mirrored by
the common assumption the axioms of set theory include the 'axiom of foundation'
which postulates that the set-membership relation '
=
0, inr X (o i )
=
' is well-founded: for every
set X , there is no infinitely descending chain
X . The axiom
of foundation allows an inductive (idealized) construction of sets starting from the
empty set
···∈
X 2
X 1
X 0 =
(the base) and recursively applying the powerset operator mapping a
set to all its subsets. For example, the inductive construction of natural (ordinal)
numbers.
If instead of the ordinary category Set of sets we want to work with the classes
(i.e., large sets) then we have to use the superlarge category SET with objects that
can be classes as well and arrows the class-functions. We can form the class V of
all sets in this case, namely the universe of sets. This class is a (strict) fixed point
P S (V )
P S mapping a class (i.e., possibly large set) to the class
of all its (small) subsets. This operator can be extended to the endofunctor
=
V of the operator
P S :
SET
: P S (V )
V of this endofunctor. It is shown that the axiom of foundation is equivalent to
SET so that
P S (V ) = V can be seen as an algebra structure id
Search WWH ::




Custom Search