[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci & Eng Dept] / [R J Botting] / [ ] / types
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Fri Jun 27 08:30:10 PDT 2008

• Introduction to Types
• : Introduction
• : Standard Types
• : Basic Types
• : Type descriptions
• : Syntax
• : Partly Baked Idea
• : Semantics.
• : Standard subsets/classes
• : : Finite_Sets
• : : Integers
• : : Numbers
• : : Standard subsets/classes
• : : : Expressions and Overloading
• : : Theory of Types
• : : : Examples of theoretical types
• : : Meta-theory of types
• : : : Babel-Aleph-Null
• : : : Consistency and Non-empty types
• : : : Avoiding paradoxes
• : : Deriving New types
• : : : Products
• : : : Quotient types
• : : : Example Quotient Type
• : : Typed Expressions
• : : : Expressions
• : : Types as a Data Model
• : : : Formal Model
• : : : : Entities and Maps
• : : : : Paths Through the DataBase.
• : : : : Categorical Model
• : : : : Conceptual Model
• : : : : Relationships with a key
• : : : : Example -- university
• : : : Equivalence of Models
• : : : Rationalisation
• : : : Data
• : : : Data Base Notation
• : : Normalisation of data.
• : : : Purpose
• : : : 0NF, 1NF, 2NF, and 3NF
• : : : Formal model
• : : : Notation
• : : : Example Data Base: Shopping
• : : : : Example -- Universal Product coding
• : : : Multi-valued Dependencies
• : : : : Example -- Hospital
• : : Quantification and Verification ...
• : Types as Object-oriented objects
• : Notes on MATHS Notation
• : Notes on the Underlying Logic of MATHS
• : Glossary

Introduction to Types

Introduction

In any project there will be a number of more less defined types. Some of these are standard well known types and are described below. Then there are the types that are peculiar to the domain being studied. This set of types is called the basis of the domain. Finally there are the types that can be constructed from the basic and standard types to give structured types (sets, tuples, relations, ...). This collection of basic, standard and constructed types is called the universe of discourse of the project.

The key discovery by Whitehead and Russell in their work on "The Principles of Mathematics" was that the idea of type could be used to avoid paradoxes as long as it was a syntactic concept. This means that each type defines those expressions that are valid or meaningful as well as what meaning can be attached. The Type system outlaws from the logic any discussions of expressions that involve contradictions in terms and paradoxes like the Russell Set. Thus any theory of types is a metalinguistic activity and taks place in yet another universe of discourse.

Simply put: Each type is linked to a set of expressions and a set of meanings and connects them together. And each type does this in its own way. Types are the main way that MATHS is extended.

All types must define a non-empty set of objects -- a valid universe of discourse -- so that we can use the predicate calculus to reason about objects of that type.

Standard Types

The following are common descriptions of types


(Alphabets):

1. Generic finite set. Probably characters or symbols.
2. Operations=>{(!), (1st), (rest),...}

   
   (@):

3. The propositions, Values=>{true,false},
4. Operations=>{and,or,not,...}

   
   (Char):

5. The ASCII characters, See [ Main%20Content in comp.text.ASCII ]
6. Values: "a", "b", char(26),...

   
   (Documents):

7. Pieces of Documentation,
8. Operations=>{$,...and,or,...}, see below.

   
   (Events):

9. A finite set of elements written in a different language.

   
   (Numbers):

10. Type that includes real,integer, etc types,
11. Operations=>{+,-,*,...}

    
    (Dimensions):

12. Length, Mass, Time, Information, Area, Angle,...
13. Dimensions, each is a separtate type.
14. Operations=>{+,-},
15. For all D:Dimension, some units:@(Number->D). (eg 60.sec=1.hr,8.bit=1.byte)

    
    (Sets):

16. Generic, For S:Sets is short for For T:Types, S:@T,
17. Operations=>{&, |, ~, ...}

    
    (Times):

18. A special ordered set with elements written in a different language

    
    (Types):

19. Generic

    Basic Types

    In real systems we work with universes of discouses like: Employees, Products, Animals, Telephones,... Michael Jackson notes that we need to be able to designate individuals in these domains. Terry Halpin has noted that the individuals/elements/objects/"values" can be described by a definite description like this

     		the Employee with SSN 123-45-6789

     		the[e:Employee](e.SSN="123-45-6789")

    It seems wise to introduce -- as a partly-baked idea -- a standard way to dessignate objects of a type:

     		Employee("123-45-6789")

    Here is a possible formalization:

20. BASIC_TYPE::=following,
    Net
    1. T::Types.
    2. identifier::Set=given.
    3. designation::identifier >-> T.
       
    4. |-designation in identifier --- T, a one to one mapping.
    5. For i:indentifier, T(i)::T= designation(i).

    
    (End of Net)
    
    

    So we might define, as an example,

21. example::=
    Net{

    1. SSN::Sets.
    2. ...
    3. Employee::Types.
       
    4. |-BASIC_TYPE(Employee, identifier=>SSN).

    
    }=::example.

    By further defining functions, predictaes, sets, relations, etc. we can easily model the types of objects in the real world. This conceptual model is an excellent guide to designing data bases, a natural ontology for the domain, and a source of ideas for classes in object-oriented programming.

    Type descriptions

    A Type is defined to have two key attributes attributes:

22. |-TYPE::=Net{
23. description::=symbolic representation of the type::#lexeme.
24. objects::=set of values or things of this type::Sets.
25. ...

}=::TYPE.
1. Type_descriptions::=
   Net{

   Notice that a type T is not a member of a type.

   Syntax

   1. type_description::= type_power | type_product,
   2. type_power::=type_product "^" type_product,
   3. type_product::= type_factor | type_factor "><" type_product,
   4. type_factor::= "@" type_element |type_element,
   5. type_element::=name_of_a_type | "(" type_description ")".

      Partly Baked Idea

      Discriminated unions are useful for decribing data bases and partial tples. A possible semantics is found in the theory of co-products in Category Theory(CATEGORY).
   6. CATEGORY::= See http://cse.csusb.edu/dick/maths/math_25_Categories.html.

      If D is a list of declarations then \/{D} is a discriminated union or co-product:

   7. type_disciminated_union::=co_product.
   8. co_product::="\/" "{" list_of_declarations "}".
   9. list_of_declarations::= declaration #( "," declaration).
   10. declaration::= identifier ":" type_description.

       Semantics.

       As a rule the description is a string that describes the objects in the following way:
       
   11. |- (desc-objects): For all T1,T2:Types, if T1.description= T2.description then T1.objects=T2.objects.
       
   12. |- (hat_means_power): For all T1, T2, T3:Types, if T1.description=T2.description "^" T3.description then T1.objects=(T2.objects)^(T3.objects).
       
   13. |- (at_means_subsets): For all T1, T2:Types, if T1.description="@" T2.description then T1.objects=@(T2.objects).
       
   14. |- (cross_means_product): For all T1, T2, T3:Types, if T1.description= T2.description "><" T3.description and T1.description in type_factor then T1.objects=(T2.objects) >< (T3.objects).
       
   15. |- (parentheses_mean_parentheses): For all T1,T2:Types, if T1.description="(" T2.description ")" then T1.objects=T2.objects.

   
   }=::Type_descriptions.

   Standard subsets/classes

   Finite_Sets

   1. Finite_sets::=sets which are not isomorphic to a proper subset of themselves.

      Integers

   2. Int, Z
   3. Integers,Whole Numbers,
   4. Values=>{...-3,-2,-1,0,1,2,3...},

      Numbers

   5. Rational, Q Quotients/Ratios
   6. Fractions $(numerator:Nat0,denominator:Nat,...}
   7. Real, R The Real Numbers,
   8. n..m::={i:Z || n<=i<=m}.
   9. Bit::=0..1.
   10. n..::={i:Z || n<=i}.
   11. ..m::={i:Z || i<=m}.
   12. Natural::={n:Z || n>=0}.
   13. Nat0:=Natural.
   14. Positive::={n:Nat0 || n>0}.
   15. Nat::=Positive.
       
   16. (above)|-Nat0 = Nat | {0} = 0.. .
   17. Fixed(n)::==-2^(n-1)..2^(n-1)-1.
   18. Float(p,s) A finite subset of the Rational numbers (denominators=2^-i where i:Fixed(s),...) Decimal(p,n):@Rational::=(-10^n+1..10^n-1)/(10^p),
   19. Money::=Int/100.

       Hence
       

   20. |-n..m in @Z.
   21. |- T^n::= T^(1..n).
       
   22. |-for n:Nat0, T^n ==> #T. So if x is in T^n then x has type #T.

       Standard subsets/classes

       Expressions and Overloading

       As a generallity the type of an expression can always be determined (sometimes relative to certain assumed types), from the type of the parts and the operators that make it up. Even so a modicum of overloading is allowed - an symbols can be defined to carry out different operations, (and return different types, depending on the context. Such a definition is written: term::context=expression For example, here are three different views of an assignment:

       1. assignment::syntactic= variable ":=" expression,
       2. assignment::parsed= Net{v:variable, e:expression,...},
       3. assignment::semantic= map [v:variable, e:expression]( s'.v=e(s) and for all u:variable~{v}(s'.u=s.u)).

          Standard examples of overloading:
          (casts):

       4. For T:Types, a:T, a::@T={a}, a::#T=(a), a::%T=(1+>a).

          
          (set extensions):

       5. For T1,T2:Types, f:T1->T2, f::@T1->@T2={f(x) || x:T1(x in (_) },
       6. For T:Types, op:infix(T), op::infix(@T)={x+y||x in (1st), y in (2nd)}.

          As a rule: An overloading can not take an existing valid meaning in the given context. So (|) is given a meaning for all sets and so can not be extended to operate on sets as well.

          Polymorphic and generic terms have definitions written like this:

       7. For T:Types, term::t(T)=expression(t(T))

          where t(T) is some formula that contains T as a free variable. If the symbol T appears in the expression then it is interpreted as the universal set of a generic type T. In general T can be any list of symbolic variables. Completely generic terms ( "macros") can be defined but are rare. If v1,v2,v3,... are previously undeclared variables then

       8. For v1,v2,v3,..., M(v1,v2,v3,...)::= e,

          creates a function that applies to all types of operands and is short for

       9. For T1, T2, T3,...:Types, v1:T1,v2:T2,v3:T3,...,
       10. M(v1,v2,v3,...)::= e.

       . . . . . . . . . ( end of section Introduction to Types) <<Contents | End>>

       Theory of Types

       1. Theory_of_types::=
          Net{

          Uses SEMANTICS [ logic_7_Semantics.mth ]
          1. Types::@TYPE. We have a set of types, each one structured as a TYPE.

          2. TYPE::=
             Net{

             1. description::=symbolic representation of the type::#lexeme.
             2. objects::=set of values or things of this type::Sets.

                Note. If T is this type then x in T.objects iff x has type T.

                Symbols for types have two meanings, one of these is in a normal part of an expression where it represents the set of objects or an identity map from objects to objects depending on the context.

             3. (dual_meaning): 2 symbols o /representation(description).

             4. (description_is_symbol)): symbol(description, @objects, objects).

                The other meaning is when the description identifies the type in a declaration.

             5. elements::@meaning_in(objects),
             6. elementary_expression::=elements.syntax.
                
             7. |- (elem): elements in element.syntax->objects.

             8. expressions::@#lexeme. The expressions of this type are defined in terms of objects in other types and so is not a property of this type alone. [See EXPRESSION below]
             9. (elem_in_expr): elements.syntax==>expressions.

             10. equality::equivalence_relation(objects). [STANDARD.relations]

             11. infix_pairs::@meaning_in(infix(objects)). [STANDARD.infix]
             12. infixes::=Lexemes referring to binary operations.
             13. infixes::=infix_pairs.syntax

                 EXPRESSION uses infixes(T) to define expressions(T).

             14. (precedence): STRICT_ORDER(infixes, has_precedence_over)Chapter 4, section 8]

                 Used in EXPRESSION.

             15. propositional_functions::@references(@^objects).

                 Used in Proposition Calculus.

             16. parallels::@meaning_in(@(objects, objects)).
             17. parallel::=parallels.syntax.
             18. (equals_is_parallel): ("=",equality) in parallels.

             19. serial::@infixes={s.syn || for some s:infix_pairs( associative(s.sem)) }~parallel.

             20. other_operators::=operators giving results of this type:@symbols~infix~parallel.

             21. (operators_mean_maps): For all o:other_operators, some domain:Types, o.type=domain->objects.

             22. operators::={(representation=>i.syntax, type=>infix(objects), meaning=>i.semantics) || for some i:infix_pairs} | other_operators.

                 See Also Expressions. [ Expressions ]

             
             }=::TYPE.

             
             (syntax_symbolizes_semantics): For all T:Types, e:T.elements, symbol(e.syntax, T, e.semantics).
             (descriptions_symbolise_types): For all T:Types, symbol(T.description, Types, T).
             

          3. |- (type_symbol_means_universal): For all T:Types, symbol(T.description, @T.objects, T.objects).

             
             (different_types_do_not_overlap): For all T1, T2:Types, T1=T2 iff some (T1.objects&T2.objects).

             
             (parallels): For T:Types, P:T.parallels, PARALLEL(expressions(@), T.expressions, P.syntax, P.semantics).

             
             (serials): For T:Types, s:T.serial, SERIAL(T.expressions, T.expressions, s, T.infix_pairs(s)).

          4. ??{take precedence into account}?

          
          }=::Theory_of_types.

          Examples of theoretical types

          (Example_PC):Types::=
       2. (
       3. description=>"@",
       4. elements=>{("true", true), ("false", false)},
       5. equality=>( (true, true) +>true | else+>false),
       6. infix_pairs=>{("and", and), ("or", or), ...},
       7. serial=>{"and", "or"},
       8. parallel_pairs=>{("iff", iff), ("=", equality), ...},
       9. other_operators=>{("=", T><T->@, T.equality) || for some T:Types}
       10. |{("in", T><@T->@, in) || for some T:Types}
       11. |...,
       12. ...
       13. )

           or even

       14. For T:Types, Example_Sets(T)::Types=
       15. (description=>"@"! T.description,
       16. elements=>{("{}",{}), (T.description, T.objects)}
       17. |{ "{"!e!"}" || e:T.elementary_expressions},
       18. infix_pairs=>{("&", &), ("|", |),...},
       19. serial=>{"&", "|"},
       20. parallel_pairs=>{("=", =), ("==>", ==>), ...}, ...
       21. ):Types.

       . . . . . . . . . ( end of section Theory of Types) <<Contents | End>>

       Meta-theory of types

       Babel-Aleph-Null

       The definition of the type '@' in terms of type theory is an interesting test case of the system, and is rather like attempting to build the foundation of a building on its roof. The inabillity to this suggests limits to the system. The successful construction of a model of logic, on a theory of types, expressed in terms of that logic, establishes the power but not the consistency of the system.

       1. @::Types=following,
          
          1. symbol=>"@",
          2. elementary_expression=>"true"+>true|"false"+>false,
          3. infix_pairs=>"and"+>((true,true)+>true |+> false) |"or"+>((false,false)+>false |+> true),
          4. parallels=>"="+>({(true,true),(false,false)}+>true |+> false) |"iff"+>({(true,true),(false,false)}+>true |+> false),
          5. serial=>{"and","or"},
          6. other_operators=> | following
             • { ("not",@->@,true+>false|false+>true)}
             • {("if_then_",distfix(@,@,@),(true,false)+>false |+> true)}
             • {("in", @T, in) ||T:Types}
             • {("==>", @T><@T->@,==>)||for T:Types}
             • {("=", @T><@T->@,=)||for T:Types~"@"}
             • {("all", @^T->@, map F:@^T(img(F)=true)) ||for T:Types }
          
          

       2. @.operators::=following,
          Table

          representation	Type	meaning
          not	@->@	true+>false|false+>true,
          and	@><@->@	(true,true)+>true |+> false,
          or	@><@->@	(false,false)+>false |+> true,
          iff	@><@->@	{(true,true),(false,false)}+>true |+> false,
          if_then_	@><@->@	(true,false)+>false |+> true,
          in	T><@T->@	map x,X(x.X),
          =	T><T->@	map x,y((x,y).(equality(T))),
          all	@^T->@	map F:@^T(img(F)=true),
          ==>	(@^T)><(@^T)->@	map [A,B] (all(map x(if x.A then x.B))).
          ...

          
          (Close Table)
          
       3. quantified_wff::={( ("for" Q B "(" P ")"), (Q "(" "map" "[" B "]" "(" P ")" ")" )) || Q:{all,no,...}, B: (variable (colon | equals) set_expression), P:@.representation}

          Consistency and Non-empty types

          Types must always define a non-empty set of objects. And a simple way to prove this is give a finite example.

          Consistency is demonstrated by exhibitting a finite model.

          Another techniqu is to use the simplest (non-recursive) constructions.

          Avoiding paradoxes

          Notice that sets are defined by a formula
       4. {x:T||B}, which explicitly assigns a type to the variable. But the collection of all types is not a type so we can not define a set of all sets and so should avoid the paradoxes discovered at the beginning of the 20th century. Notations like X:Type or Type X can only be used to set of a generic formula.

          We can prove that the set of data types leads to a consistent theory by constructing a model in terms of naive set theory and n-tples. The data types are those generated from @ and Nat by operations of fnite Products and coproducts. The proof of relative consistency is done by using Codd normalizations. Model each type as a set of n-tpls of elementary object. Replace T2^T1 by (T1><T2). The result is the Third Normal Form Model.

          When defining new types recursion must not be combined with power and subset operators because these lead to paradoxes. Cantor Russell... [click here if you can fill this hole]

          Care also needs to be taken with using generic operators (defined with an implicit type for convenence) in a way that the actual types involved are made explicit. This is the problem as found in C++ templates. In MATHS one example was the original definition of the function that returns the cardinality or size of a set:

       5. Card:@T->Nat0= map[X](|X|).

          So, this is true

       6. Card{} = 0,
       7. Card{"x"} = 1,
       8. Card{"x","y"} = 2

          The following expression

       9. /Card(1) has an ambiguous type -- the set of singletons of unknown type. Instead make the type explicit
       10. Strings@1 = sets of strings with one element.

       . . . . . . . . . ( end of section Meta-theory of types) <<Contents | End>>

       Deriving New types

       Wechler presents an extensive theory of univeral algebras [Wechler 93, Section 3.1].

       Products

       [ Notation $Net{a:T1, b:T2 ...} ]

       Quotient types

       If there is a map from one type to another then there is an easy way to generate a new type - by grouping the elements of the second type according to their values under the mapping - this is called the quotient type with respect to the mapping. Given f:T1^T2 we can always derive a new type (symbolized T2/f) isomorphic to a sub-set of @T2 where
       1. X:T2/f iff for some y:T1, all x:X(f(x)=y). This called the quotient type of T2 with respect to f.

          Given a R:@(T1><T1) which is reflexive, transitive and symmetric (an equivalence relation) then there is a subset of @T1, symbolised T1/R, defined by T1/R::={X:@T1||for all x,y:X( x R y)}. Then there is a map (T1/R)^T1 from x:T1 to x/R:T1/R

       2. x/R = {y:T1|| x R y}
       3. ./R = map x:T1(x/R) Notice that
       4. T1/(./R)=T1/R

          We can define a relation equivalence modulo f x = y wrt f ::= f(x)=f(y) which leads to the same "quotient type".

          Example Quotient Type

          Constructing Q (the rational numbers) from Z (the integers).
       5. Q::= ( (1st=>Z, 2nd=>Z)/equiv
       6. where ( (a,b) equiv (c,d) iff d a = b c)
       7. ).

          [ Notation] .

       . . . . . . . . . ( end of section Deriving New types) <<Contents | End>>

       Typed Expressions

       Expressions

       To complete this section here are the definitions of the syntax of expressions. A string of lexemes that is not terminated by a comma or period occurring outside parenthesis of some kind or other, can be expression. But an expression can not contain a comma or period outside of parenthesis. You can therefore use punctuation to recognised balanced expressions. A second cut needs a set of operators - those symbols that only make sense when accompanying other symbols - and defines whether an expression is functional. The final check makes sure that the types of actual parameters match the operators on them. These will be presented in reverse order.
       1. EXPRESSIONS::=
          Net{

          Uses SEMANTICS. Uses Type_Theory. Uses ASCII_code.
          1. expression::= balanced & functional & ( |[T:Types] typed_expression(T) ).

             We start be defining the set of fully parenthesized expressions(p_expressions) of a given type and then state circumstances under which parentheses can be removed without change of meaning.

             [ Math.64 Standard Forms.Standard Forms in Programming Languages.Macros ]

          2. p_expression::=fully_parenthesized_expression:Types->@#lexeme.

          3. For T1: Types, p_expression(T1)::= ( elementary_expression(T1) | variable(T1) | UNARY(representation(T1), other_language_string) | |{UNARY(p_expression(T2), p_expression(T1^T2)) || T2:Types} | |{BINARY(p_expression(T2), p_expression(T3), p_expression(T1^(T2><T3)) || T2,T3:Types} | |{INFIX(p_expression(T1), f) || f:T1.infix)} | |{LAMBDA(representation(T2), p_expression(T3)) || T2,T3:Types(T1=T3^T2)} | |{INTENTION(representation(T2)) || T2:Types(T1=@T2)} | |{EXTENSION(p_expression(T2)) || T2:Types(T1=@T2)} | |{N_TUPLE(p_expression o t) || t:#Types(T1= ><(t))} | |{UNARY(p_expression(@T2), p_expression(@(T2><T3))) || T2,T3:Types(T1=@T3)} | |{UNARY(p_expression(T2), p_expression(@(T2><T3))) || T2,T3:Types(T1=@T3)} )

             The above defines fully parenthesized expressions.

          4. parenthesis_removal::={(X ! a ! B ! a ! Y , X ! a ! "(" ! B! ")" ! a ! Y) || T:type, X, Y:#char,
          5. a:infix(T),b:infix(T),B:INFIX(p_expression(T),b)( b has_precedence_over a ) }

             Example: "1+(2*3*4)+5" parenthesis_removal "1+2*3*4+5" and not "(1+2)*3" parenthesis_removal "1+2*3".

          6. typed_expression(T)::=p_expression.do( parenthesis_removal).

             
             

          7. |-p_expression(T)==>typed_expression(T).

             The semantics of MATHS expressions are trivial when formalized in MATHS. The correct meaning of a MATHS expression looks (in MATHS) like itself . Spivey has remarked on a similar phenomena in the attempt to define Z in terms of set theory and set theory using Z. The denotation (map from syntax into semantics) is the identity mapping. Such a circular definition can be shown to be useless for ignorant readers because ignorance is a trivial fixed point[Spivey 88]. Luckily, complete definition is not essential for a human being to learn a language.

             Future research can establish the semantics in terms of other languages - such as Z, Larch, .... The syntax and a prossibly feasible way to parse expressions is a notational problem. [ Notation.12 Expressions ]

             }=::EXPRESSIONS

          . . . . . . . . . ( end of section Typed Expressions) <<Contents | End>>

          Types as a Data Model

          Formal Model

          Entities and Maps

          1. DATABASE::=
             Net{

             Collection of named types, objects, and maps.
             1. Uses lexemes, type_theory, EXPRESSION.
             2. T::=Entity types:Finite(Types).
                
             3. |-For all t:Types, t.μ=t.denotation in
             4. expressions(t)->objects(t).
             5. D::=Entity descriptions ::= `Object classes`::=Finite(|[t:T]expressions(@t)).
             6. For A:D, E(A)::=Named objects in A:Finite(expressions(A)).

             7. For A,B:D, F(A,B)::=`Named maps from A to
             8. B`:Finite(expressions(B^A)).
                For no A, Id(A) in F(A,A).

                Paths Through the DataBase.

             9. For A,B:D, S(A,B)::@(A,B)=μ(F(A,B)) | {R:@(A,B)|| /R in μ(F(B,A))}.
             10. For A,B, P(A,B)::@(A,B)=paths from A to B::=S(A,B) | { s;p ||for some C:D, s:S(A,T3), p:P(C,B)},
             11. L(A,B)::@(expressions(B^A))=/μ( { s1;s2;p || for some C1,C2:D, s1:S(A,C1), s2:S(C1,
             12. C2), p:P(C2,B)}~Id(A)
             13. ). ...
             14. connected::@=for all A,B, if A<>B then some(P(A,B)).
             15. For A,B, redundant(A,B)::@=some(F(A,B) & L(A,B)).
             16. redundant::@=for some A,B(redundant(A,B)). ).
             17. For A,B, M(A,B)::basic maps=F(A,B)~L(A,B) . ...
             18. conceptual_model::=Bachman Diagram,
             19. conceptual_model::=digraph(
             20. vertices=>D ,
             21. edges=> {(v1,v2) || for some A,B:D, m:M(A,B)(v1=names(A) and
             22. v2=names(B) )
             23. ). ...
             24. conceptual_graph::=digraph(
             25. vertices=>D | |[A:D]E(A) | |[A,B:D]F(A,B),
             26. edges=> { (e, A) || for some A:D, e:E(A) }
             27. | {(m,B) || for some A,B:D, m:M(A,B) }
             28. | {(A, m) || for some A,B:D, m:M(A,B) }
             29. }
             30. ). ...

                 paths, prime_links, links::(names(D))^( names(D)><names(D)). For T1,T2, prime_links(names(T1), names(T2)=names(F(T1,T2))| { "("! l1 ! ![i:2..pre(l)](","!l[i])! ")"||for some C:#D, f:F(T1,T2), l:#char(l=names o f and T2= ><C)}.

                 For T1,T2, links(names(T1), names(T2))=prime_links(T1,T2)|prime_links(T2,T1)

                 For n1,n2:names(D), paths(n1,n2)=links(n1,n2) |{ l!".."!p || for some n3:names(D), l:links(n1,n3), p:paths(n3,n2)}.

                 ??|-paths(T1,T2) in regular_expression(|(links)).?

                 For T2,

             31. retrieval(T2)::=|[T1:D](entries(T1)!".."!paths(T1,T2)).

                 It is easy to set up a map from paths into relations.

                 Categorical Model

             32. For T1,T2, p:P(T1,T2), arrow(p)::=(T1, p, T2). CATEGORY(Objects=>names(D),
             33. Arrows=>{arrow(p)||for some T1 ,T2:D (T1=T2 and p=Id(T1)
             34. or p in paths(T1,T2
             35. )}.

                 Conceptual Model

             36. conceptual_model::=digraph(vertices=> names(D)| |[T:D]names(E(T))|
             37. |[T1,T2:D]names(T1,T2),
             38. edges=>{(v1,v2) || objects(v1)in classes(v2)
             39. or maps(v1) in B(dom(v1),cod(v1) and
             40. cod(maps(v1))=classes(v2)
             41. or maps(v2) in B(dom(v2), cod(v2)) and
             42. dom(maps(v2))=classes(v1)
             43. }
             44. ).
             45. rationalized::@=no cycles( conceptual_model).

                 if rationalized then conceptual_model in DAG.

             
             }=::DATABASE.

             Relationships with a key

             Suppose we have a network
          2. N:=Net{v1:V1, v2:V2,...}, and k and d are two lists of variables in v1,v2,v3,...
          3. k,d:#|(v). where k do not overlap:
          4. no |k & |d. Define T:=${k1:k1(N),...d1:d1(N),...}, then (@N k -> d) ::=sets in @T with k determining d.

             The above is sometimes called a functional dependency. These are worth noticing since they indicate the logical structure that underlies the original design.

             The process starts with a set S:@N and finding a k and d such that

          5. S in (@N k->d). If k is large as possible and d is all the other variables then k is a suitable key or identifier for a database. If niether S.k nor S.d themselves contain any functional dependencies then the set S is in third normal form(TNF, 3NF,...). k nor

             Example -- university

          6. U::=
             Net{

             sid, name, address, sched_number, course, time, course_number, course_name, dept, units,...::string.

             
             }=::U.
             The following would some of the dependencies that we can use to argise a model of this university:
          7. courses::@U(course)->(course_number, course_name, dept, units).
          8. students::@U(sid)->(name,address).
          9. enrolment::@U(sched_number,sid)->().
          10. class::@U(sched_number)->(course, time).

          Equivalence of Models

          1. ...

             Rationalisation

             It is possible to express any finite collection of structured sets as a network database by applying rules like those in the LDST step in SSADM. Here are some examples,
          2. For all A:D, C:#D, if A= ><(C) then for all i:pre(C), some
          3. I:/μ(i.th)( I in F(A, C[i])).
          4. For all A:D, s:Documentation, (v,B):declarations(s), if A=s then v
          5. in F(T,B).
          6. For all A,B:D, if A==>B then "Id" in F(A,B).
          7. For all A,B:D, I:/μ(in.@(A,B)), if B==>@A then I in D and "1st"
          8. in F(I, A) and "2nd" in F(I, B).
          9. For all A,B:D,T:@@(A,B) then "1st" in F(T,A) and "2nd" in F(T,B).
          10. For all A,B:D,X:Sets, if A=X->B then A in @@(X,B) and
          11. "2nd" in F(T,B) and for some I:/μ(X)(I in D and "1st" in
          12. F(I, A).
          13. This last rule also applies when A=B^n, A=#B, ...

              Data

              For D1,D2:documentation, a:Arrow,
          14. Net{D1} a Net{D1}={R:@${D1, D2}| (R) ${D1} a ${D2}.

              For two lists of declarations D1, D2, Data{D1. D2}::=Net{D1}->Net{D2}.

              Since D1 and D2 have no definitions or wffs then

          15. Data{D1. D2}=@{ Net{D1. D2} | for all D1, one D2}

              If we are discussing fixed set of variables and types with unique identifiers then this is abreviated further - suppose we have a DICTIONARY; DICTIONARY=Net{ v1:T1, ...} and let type(v[i])=t[i], then Data{ k1,k2,...,k[n]. d1,d2,..., d[m]} ::=@DICTIONARY(k1,k2,...,k[n])->(d1,d2,...,d[m]).

              Data Base Notation

              If D is a list of declarations then \/{D} is a discriminated union and so a natural model for a data base. The components of D are the different types of data/entities.

              Open Example Data Base -- University

          16. U::=Net{from previous example ...}.
          17. UNIVERSITY::=\/{
          18. student::@U(sid)->(name,address,..).
          19. section::@U(sched_number)->(course, time).
          20. class::@U(courses)->(dept, course_number, course_name, units, ...).
          21. enrollment::@U(sid,sched_number)->(...).

          
          }=::UNIVERSITY.

          { student(123-45-6789, "John Doe", ...),

       2. student(234-56-6789, "Jane Roe", ...),
       3. section(12345, CS121, (MWF, 0800..0910)),
       4. section(13244, CS121, (TT, 0800..1000)),
       5. course(CS121, CS, 121, "Computers and Society", 2),
       6. enrollment(234-56-6789, 12345, ...),
       7. ... } in @UNIVERSITY.

       . . . . . . . . . ( end of section Example Data Base -- University) <<Contents | End>>

       Normalisation of data.

       Purpose

       The aim of normalization is to document all the structure in some given data in terms of simple sets and mappings. Or, in McCathy's terminology, the purpose is to derive the abstract syntax from the concrete syntax. A third view is that we wish to discover and name all the implicit relationships. Finally we can say that normalization derives a standard semantic domain to model what is known about some data. The effect is a repeated partioning of an initially homogeneous set of n-tuples into different classes and types.

       Normalization is an analytical tool more than a design tool. The goal is to model part of the problem not to work out detailed solutions. Design has to be concerned with performance, physical limitations, and ways to encode the necessary data. Relational data is a starting place for design and a useful user interface. They are simple to understand and use but tend to not use machinary efficiently. The relational retrieval systems are also limmitted in power[]. However they are a high powered analytical tool separating an area into many simple relations. These relations are a canonical basis for design work.

       0NF, 1NF, 2NF, and 3NF

       First, second, and third normalization steps operate on a set of sets of simple types by repeatedly replacing one type by two or more types with the subsets of the variables. The names of the variables are unique and their domains don't change. Often the domains are strings. Hence the domains are omitted.

       One starts with samples, displays, or existing data structures. Abstraction starts by naming component data and their domains. Then a plausible key is postulated and the result normalized until all functional dependencies are represented by key->data relationships. The 3 step process goes thru an easy to recall pattern : the key, the whole key, and nothing key.

       1. NORMALIZATION::=following,
          
          1. (0NF): A set of dictionaries, each listing a set of variables describing some sample forms, records, data structures, ... No duplicated variable names.
          2. (1NF): For each dictionary choose a subset of the variables that can act as a primary key for that set of data. Extract repeating groups of data into new dictionaries. Make sure that each key (set of variable values) identifies a unique item in the data set.
          3. (2NF): The Whole key. Make sure that for each key no part of the key can identify part of the data.
          4. (3NF): Nothing But the Key. Make sure that no part of the key identifies another part of the key.
          
          Notice there are further normalization steps that can be applied to further expose more hidden data structures.

          Formal model

          1. DICTIONARY::=Net{v1:D[1], v2:D[2], v3:D[3], ..., v[n]:D[n]}.
          2. samples::@DICTIONARY.
          3. @DICTIONARY(k1, k2, ...)?-?(d1, d2, ..).
          4. samples >--\/{
          5. a::@DICTIONARY(...)->(...).
          6. b::@DICTIONARY(...)->(...).
          7. c::@DICTIONARY(...)->(...).
          8. ...
             }

       . . . . . . . . . ( end of section Formal model) <<Contents | End>>

       Notation

   23. Data{ key1, key2, key3, ... . non_key1, non_key2, ...}

       Example Data Base: Shopping

       Consider the data collected when grocery shopping. Here is the analysis of a shopping list as part of the work leading upto a "shoppers assistant" for an electronic organizer or personal digital assistant.

       The data on the list are

       1. shopping_list_data::=
          Net{

          product_name, shop::string. price, tax, total::money.
          1. quantity::Nat0.
          2. date::Dates. time::Times.
          3. bought::@.

          
          }=::shopping_list_data.

          Now select a key: product_name samples>-- \/{

       2. s0::Data{product_name. shop, price, tax, total,quantity, date, time, bought}
          }.
       Then remove repeating data/many-many relations: samples>-- \/{
   24. s1::Data{product_name.}.
   25. s2::Data{product_name, date, shop. quantity, price, bought}.
   26. s3::Data{date, shop. tax, total, time}.
       }
   There are no part key dependencies. There are no non-key dependencies.
2. database::=\/{
3. Products::Data{product_name:string.}.
4. Orders::Data{product_name::string, date::Date, shop::string.
5. quantity::Nat0, price::money, bought::@}.
6. Shopping_trips::Data{date:Dates, shop:string. total, tax:Money, time:Times}.

   
   

7. |-product_name in Orders->Products.
   
8. |-(date,shop) in Orders->Shopping_trips.

   
   }

Here is the analysis of a receipt from a cashier at a local supermarket: