.Open Sets of Structures and Data Bases
. Basics
t:: $ Net{a: A, b: B, c: C, ... }
implies that `t` is a tpl / entity / object / logical data group / record
/ struct a,b,c,... are field/component/role names. In UML terms the
a,b,c,...
can be attributes, roles, or even constant operations that return a value.
R:: @$ Net{a: A, b: B, c: C, ... }
implies that R is a set of tpls / entity type / table / class / relation
T::=$ Net{a: A, b: B, c: C, ... }
implies that T is the type of all classes/entity types/tables...
Data{a: A, b: B, c: C, ... }::=Finite_sets( $ Net{a: A, b: B, c: C, ... } ),
.Open Example
phonebook::=Data{name, number: #char} ==>@$ Net{name,number: #char}.
P::=following,
{
(name=>"John Doe", number=>"714-123-5678"),
(name=>"John Doe", number=>"3678"),
(name=>"Joan Roe", number=>"714-123-5878"),
(name=>"Joan Roe", number=>"3878")
}.
|- P in phonebook
or in tabular form using either ASCII ($P1 below) or HTML tables ($P2 below).
P1::Data{name, number}=following
. Table P
.As_is ---------------------
.As_is name number
.As_is ---------------------
.As_is John Doe 714-123-5678
.As_is John Doe 3678
.As_is Joan Roe 714-123-5878
.As_is Joan Roe 3878
.As_is ---------------------
P2::=following
.Table name number
.Row John Doe 714-123-5678
.Row John Doe 3678
.Row Joan Roe 714-123-5878
.Row Joan Roe 3878
.Close.Table
()|- P = $P1 = $P2.
.Close Example
. Subsets of Sets of structures
$ Net{a1: A1, b1: B1,...W1(a1,b1...)}and $ Net{a2: A2, b2: B2,...W2(a2,b2...)} = $ Net{a1: A1, b1: B1,...a2: A2, b2: B2...(W1(a,b...) and W2(a2,b2...))}.
$ Net{A, B, C, ...W1}&$ Net{A, B, C, ...W2} = $ Net{A, B, C, ... W1 and W2}.
$ Net{A, B, C, ...W1}|$ Net{A, B, C, ...W2} = $ Net{A, B, C, ... W1 or W2}.
. Identifiers and Keys
For Sets K, is_id::|[R:Sets](@(R->K, R))
For sets R, K, p:R->K, p is_id R iff for all k:R.p, one r:R( r.p =k ).
ids::=/is_ids
()|- for all R, ids(R) = |[K:Sets](R-->K).
An Entity Type is a set of structures with a specified key:
ENTITY::=Net{
structure:: documentation,
key:: #variables(structure), ...
}=::ENTITY.
Entities:: Finite_sets(Sets)= { E:Finite_sets || for some D:documentation, k:#variables(D) ( E=Data{D} and k in ids(E) ) }.
Entity_type:: $ENTITY->Entities= map[e:$ENTITY] { R: Sets || R=Data{documentation(e)} and key(e) in ids(R) }.
Class:: #variables><#variables->@Entities= map[(k,d)] { E:Entity_type(key=>k, structure=>D) || for some D:documentation ( variables(D) = img(k)|img(d) and k in ids(E) ) }.
For D:documentation, k,d:#variables(D), @D k->d ::= @D & Class(k, d).
This kind of class is more general those used in object-oriented languages.
encapsulated dynamics. It is essentially a set of all possible static
snapshots of an object. However the use of general documentation to define
ENTITY implies that inheritance is possible because documents can inherit
structures and properties form each other. Documentation also always the
statement of properties that are invariant over the life time of an object
of that class. This tends to be related to the possible dynamics of the
object with out giving clues as to how it will be implemented.
.Open Example of Entities and classes
PHONE::=Net{name: #char, type: {home,office}, number: #char }.
phones:: Class((name, type), (number)) & Phonebooks.
Phonebooks::=@$PHONE,
phone in @PHONE(name,type)->(number)<==Data{name: #char, type: {home,office}, number: #char }.
. Table P2
.As_is ----------------------------------------
.As_is Name type number
.As_is ----------------------------------------
.As_is "John Doe" home "714-123-5678"
.As_is "John Doe" work "3678"
.As_is "Joan Roe" home "714-123-5878"
.As_is "Joan Roe" work "3878"
.As_is -----------------------------------------
The above indicates the more formal description
P::={
(name=>"John Doe",type=>home, number=>"714-123-5678"),
(name=>"John Doe",type=>work, number=>"3678"),
(name=>"Joan Roe",type=>home, number=>"714-123-5878"),
(name=>"Joan Roe",type=>work, number=>"3878")
}
The definition implies
|- P in phones.
.Close
. Primary Keys
We can define relationships by documenting the primary keys and the other attributes:
For N1,N2 pieces of documentation and N1 has variable v=(v1, v2,...) then N1->N2 = { R : @(N1 and N2) || v is_id R }
|-For s1, s2:documentation, R:s1->s2, some F:$s1^$s2, F---R.
Notice that since |- X in ids(X), it follows |- for all D ( @D = @^$D).
Thus all sets of n-tpls are tables with identifying columns.
. Functional Dependencies
Another form of redundancy occurs when partial information about elements in a set permits the deduction of other parts of the set. Suppose that R is a set and p:R->P and q: R->Q with the properties that
|- (FD1): p<>q
|- (FD2): /p;q in p(R)->q(R)
(FD1, FD2)|-(FD3): For all k:p(R), one q(/p(k)).
In general if we have an arrow `a`: { ->, <>->, ...) we symbolize by `(R) p a q`the fact that `R` defines a relation `p(R) a q(R)`. By `@(R)p a q` we indicate
the set of subrelations of `R` with that particular reduncancy:
For arrows a, R,P,Q:Sets, p:R->P, q:R->Q, p<>q, (R) p a q ::= /p;q in p(R) a q(R).
For a, R,P,Q, p, q, p<>q, @(R) p a q ::= {S:@R|| /p;q in p(S) a q(S).
If `(R)p->q` and `p` is not in `ids(R)` then part of the structure of the problem is hidden inside `R` and will tend to cause problems when changes made to `R`. Normalisation separates out these dependancies into separate relations.
When there are two disjoint subsets of variables (`p` and `q` say) in a structure `N` and for all `R:@N` we know that the values of `p` determine the values of `q` then we say that `q` is functionally dependant on `p`.
|- (FD4): (R) p->q iff for all i:R.p one j:R.q some r:R (r.p=i and r.q=j)
.Open Example of Functional Dependency
phone_books::=$ Net{name: names, type: {home,office}}->$ Net{number: numbers},
P={(name=>"John Doe",type=> home, number=>"714-123-5678"),
(name=>"John Doe",type=>work, number=>"3678"),
(name=>"Joan Roe",type=>home, number=>"714-123-5878"),
(name=>"Joan Roe",type=>work, number=>"3878") } in phone_books
. Table P3
.As_is ----------------------------------------
.As_is Name type number
.As_is ----------------------------------------
.As_is "John Doe" home "714-123-5678"
.As_is "John Doe" work "3678"
.As_is "Joan Roe" home "714-123-5878"
.As_is "Joan Roe" work "3878"
.As_is -----------------------------------------
()|- P---$ Net{name: names, type: {home,office}},
()|- P in $ Net{name: names, type: {home,office}} -> $ Net{number: numbers},
()|- (P)(name,type)->(number),
()|- not (P)(name)->(number) and not (P)(type)->(number) and not (P)(number)->(name) and ....
In general for all phones:phone_books,
()|- phones---$ Net{name: names, type: {home,office}},
()|- phones in $ Net{name: names, type: {home,office}} -> $ Net{number: numbers},
()|- (phones)(name,type)->(number).
.Close
DataBase:: Finite_sets(Finite_sets($Type)) -- see Types.3 Type Systems
A Finite Collection of tables is a data base. The universe is the associated collection of distinguished objects.
.Open Example Data Base
college_DB::={people, students, teachers, classes, enrolments,departments}.
PERSON=$ Net{ id: SSN, name: names, address: addresses,...},
people:: Entity_type(structure=>PERSON, key=>id),
teachers:: PERSON->$ Net{ rank, step, dept: departments}.
students::=PERSON->$ following,
.Net
class_level:: FR|SO|JR|SR,
units:: Real,
GPA:: Real
.Close.Net
departments:: Finite_Sets.
names::=@NAME,
NAME::=$ Net{ family_name, personal_name: #char, initial: char}.
classes::=@CLASS.
CLASS::=$ Net{
teacher:: teachers,
schedule_number:: numbers,
department:: departments,
catalog_number:: numbers,
quarter:: {F,W,S,V},
units:: Positive.
}=::CLASS.
schedule_number in ids(classes).
enrollments::= @ENROLLMENT,
ENROLLMENT::=$ Net{ student: students, class: classes, grade: optional(grades)},
(student, class) in ids(enrollments).
A Discriminated union is a useful way to describe a database.
college_universe::=\/Net{
people:: @PERSON(id)->(...).
students:: @PERSON(id)->(...).
teachers:: @PERSON(id)->(...).
classes:: @CLASS(Schedule_number, quarter_number)->(...),
enrolments:: @ENROLLMENT(student, class)->(grade),
departments:: departments.
}=::college_universe.
. Typical function -- who do you teach
For i: SSN(teachers), those_taught_by(i) ::= i.people..teachers..classes..enrollments..students.
. Example event -- Student enrolls in class
For s:students, c:classes, enroll(s,c)::@(college_universe,college_universe)= (enrolments' = enrolments | (s,c,{})).
.Close
. See_Also
The theory of Types
.See http://www/dick/maths/types.html
How to describe dynamic relationships
.See http://www/dick/maths/math_14_Dynamics.html
The theory of Relationships
.See http://www/dick/maths/logic_44_n-aryrelations.html
.Close Sets of Structures and Data Bases
.Open Acknowledgements
I'd like to thank
Ulf Sch?nemann
.See http://www.cs.mun.ca/~ulf/
for helping to correct several typing mistakes in this document.
.Close Acknowledgements