[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / math_13_Data_Bases
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Nov 30 14:51:58 PST 2010

Contents


    Sets of Structures and Data Bases

      Basics

    1. 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.

    2. R::@$ Net{a: A, b: B, c: C, ... } implies that R is a set of tpls / entity type / table / class / relation

    3. 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, ... } ),

      Example

      1. phonebook::=Data{name, number: #char} ==>@$ Net{name,number: #char}.

      2. P::=following, {
      3. (name=>"John Doe", number=>"714-123-5678"),
      4. (name=>"John Doe", number=>"3678"),
      5. (name=>"Joan Roe", number=>"714-123-5878"),
      6. (name=>"Joan Roe", number=>"3878")
        }.

    4. |-P in phonebook

      or in tabular form using either ASCII (P1 below) or HTML tables (P2 below).

    5. P1::Data{name, number}=following

      Table P

       ---------------------
       name            number
       ---------------------
       John Doe        714-123-5678
       John Doe        3678
       Joan Roe        714-123-5878
       Joan Roe        3878
       ---------------------
    6. P2::=following
      Table
      namenumber
      John Doe714-123-5678
      John Doe3678
      Joan Roe714-123-5878
      Joan Roe3878

      (Close Table)


    7. (above)|-P = P1 = P2.

    . . . . . . . . . ( end of section Example) <<Contents | End>>

    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

  1. For Sets K, is_id::|[R:Sets](@(R->K, R))
  2. For sets R, K, p:R->K, p is_id R iff for all k:R.p, one r:R( r.p =k ).
  3. ids::=/is_ids


  4. (above)|-for all R, ids(R) = |[K:Sets](R-->K).

    An Entity Type is a set of structures with a specified key:

  5. ENTITY::=
    Net{
    1. structure::documentation,
    2. key::#variables(structure), ...

    }=::ENTITY.

  6. Entities:: Finite_sets(Sets)= { E:Finite_sets || for some D:documentation, k:#variables(D) ( E=Data{D} and k in ids(E) ) }.
  7. Entity_type:: ENTITY->Entities= map[e:ENTITY] { R: Sets || R=Data{documentation(e)} and key(e) in ids(R) }.
  8. 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) ) }.

  9. 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.

    Example of Entities and classes

    1. PHONE::=Net{name: #char, type: {home,office}, number: #char }.
    2. phones::Class((name, type), (number)) & Phonebooks.
    3. Phonebooks::=@PHONE, phone in @PHONE(name,type)->(number)<==Data{name: #char, type: {home,office}, number: #char }.

      Table P2

       ----------------------------------------
       Name 		type 	number
       ----------------------------------------
       "John Doe"	home	"714-123-5678"
       "John Doe"	work	"3678"
       "Joan Roe"	home	"714-123-5878"
       "Joan Roe"	work	"3878"
       -----------------------------------------
      The above indicates the more formal description
    4. P::={
    5. (name=>"John Doe",type=>home, number=>"714-123-5678"),
    6. (name=>"John Doe",type=>work, number=>"3678"),
    7. (name=>"Joan Roe",type=>home, number=>"714-123-5878"),
    8. (name=>"Joan Roe",type=>work, number=>"3878")
      }
    The definition implies
  10. |-P in phones.

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 qthe 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)

    Example of Functional Dependency

    1. phone_books::=$ Net{name: names, type: {home,office}}->$ Net{number: numbers},

      P={(name=>"John Doe",type=> home, number=>"714-123-5678"),

    2. (name=>"John Doe",type=>work, number=>"3678"),
    3. (name=>"Joan Roe",type=>home, number=>"714-123-5878"),
    4. (name=>"Joan Roe",type=>work, number=>"3878") } in phone_books

      Table P3

       ----------------------------------------
       Name 		type 	number
       ----------------------------------------
       "John Doe"	home	"714-123-5678"
       "John Doe"	work	"3678"
       "Joan Roe"	home	"714-123-5878"
       "Joan Roe"	work	"3878"
       -----------------------------------------


    5. (above)|-P---$ Net{name: names, type: {home,office}},
    6. (above)|-P in $ Net{name: names, type: {home,office}} -> $ Net{number: numbers},
    7. (above)|-(P)(name,type)->(number),
    8. (above)|-not (P)(name)->(number) and not (P)(type)->(number) and not (P)(number)->(name) and ....

      In general for all phones:phone_books,

    9. (above)|-phones---$ Net{name: names, type: {home,office}},
    10. (above)|-phones in $ Net{name: names, type: {home,office}} -> $ Net{number: numbers},
    11. (above)|-(phones)(name,type)->(number).

  • 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.

    Example Data Base

    1. college_DB::={people, students, teachers, classes, enrolments,departments}.

      PERSON=$ Net{ id: SSN, name: names, address: addresses,...},

    2. people:: Entity_type(structure=>PERSON, key=>id),

    3. teachers::PERSON->$ Net{ rank, step, dept: departments}.

    4. students::=PERSON->$ following,
      Net
      1. class_level::FR|SO|JR|SR,
      2. units::Real,
      3. GPA::Real

      (End of Net)

    5. departments::Finite_Sets.

    6. names::=@NAME,
    7. NAME::=$ Net{ family_name, personal_name: #char, initial: char}.

    8. classes::=@CLASS.
    9. CLASS::=$
      Net{
      1. teacher::teachers,
      2. schedule_number::numbers,
      3. department::departments,
      4. catalog_number::numbers,
      5. quarter::{F,W,S,V},
      6. units::Positive.

      }=::CLASS.
      schedule_number in ids(classes).

    10. enrollments::= @ENROLLMENT,

    11. 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.

    12. college_universe::=\/
      Net{
      1. people::@PERSON(id)->(...).
      2. students::@PERSON(id)->(...).
      3. teachers::@PERSON(id)->(...).
      4. classes::@CLASS(Schedule_number, quarter_number)->(...),
      5. enrolments::@ENROLLMENT(student, class)->(grade),
      6. departments::departments.

      }=::college_universe.

      Typical function -- who do you teach

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

      Example event -- Student enrolls in class

    14. For s:students, c:classes, enroll(s,c)::@(college_universe,college_universe)= (enrolments' = enrolments | (s,c,{})).

    See_Also

    The theory of Types [ types.html ]

    How to describe dynamic relationships [ math_14_Dynamics.html ]

    The theory of Relationships [ logic_44_n-aryrelations.html ]

    . . . . . . . . . ( end of section Sets of Structures and Data Bases) <<Contents | End>>

    Acknowledgements

      I'd like to thank Ulf Sch?nemann [ http://www.cs.mun.ca/~ulf/ ] for helping to correct several typing mistakes in this document.

    . . . . . . . . . ( end of section Acknowledgements) <<Contents | End>>

    Notes on MATHS Notation

    Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

    Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

    The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

    For a complete listing of pages in this part of my site by topic see [ home.html ]

    Notes on the Underlying Logic of MATHS

    The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

    For a more rigorous description of the standard notations see

  • STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

    Glossary

  • above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  • given::reason="I've been told that...", used to describe a problem.
  • given::variable="I'll be given a value or object like this...", used to describe a problem.
  • goal::theorem="The result I'm trying to prove right now".
  • goal::variable="The value or object I'm trying to find or construct".
  • let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  • hyp::reason="I assumed this in my last Let/Case/Po/...".
  • QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  • QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  • RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

    End