.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::={(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, students, teachers:: @PERSON(id)->(...).
	classes:: @CLASS(Schedule_number, quarter_number)->(...), 
	enrolments:: @ENROLLMENT(student, class)->(grade),
	departments:: departments.
}=::college_universe.

.  Typical function

 For i: SSN(teachers), those_taught_by(i) ::= i.people..teachers..classes..enrollments..students.

.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