Records and Labeled Tuples

Records/tuples/structures/object_states are shown using the notation of Ada. Here is a record with fields a,b,... and values xa,xb, respectively:

           (a=>xa, b=>xb, ...).

The set of all objects with fields a,b,... of type A,B, .. (respectively) is shown like this:

 	$ Net{ a:A,  b:B,  ... }.

Usually however it pays to give a name to the abstract structure

 	RECORD::=Net{ a:A,  b:B,  ... }.

This allows the structure itself to be referred to, extendded, used, inherritted in the definitions of other structures. The dollar sign is put infront of the name to indicate the set of object that fit the named structure:

 	$ $RECORD

Example

Class or Set:

 	phones::=$ Net{name:Strings, number:Strings}.

Object in phones:

 	(name=>"John Smith", number=>"714-123-5678") in phones.

Formally such a set of structures defines (and is defined by) a collection of functions: one for each component. If X=$ Net{a:A,b:B,c:C,... } then

 	a in X -> A,

 	b in X -> B,

 	c in X -> C,

and if x:X then

 	a(x)=x.a=`the a of x`,

 	b(x)=x.b=`the b of x`,

 	c(x)=x.c=`the c of x`.

Example - Phone numbers

(name=>"John Smith", number=>"714-123-5678").name ="John Smith" (name=>"John Smith", number=>"714-123-5678").number ="714-123-5678" or name(name=>"John Smith", number=>"714-123-5678") ="John Smith" number(name=>"John Smith",number=>"714-123-5678") ="714-123-5678"

UML

In UML terms the field names (a,b,c,...) are role names in the class X which would be linked to classes representing A,B,C, ... The link normally has cardinality (0..*) at the X end. The link must have cardinallity 1 at the other end. The reverse role is not (usually) named in MATHS. There is a slight abuse of notation in that the name of the role is also used as the name of the relationship.

At the conceptual level it is best to not indicate whether the links are aggregations, generalisations, etc. These physical properties are not shown in the simpler MATHS model.

Example - pairs

1. A><B::=$ Net{1st:A, 2nd:B}, (a,b) ::=(1st=>a, 2nd=>b), So we can deduce the following formulae must also hold:
2. (a,b).1st=a,
3. (a,b).2nd=b.
4. 1st in A><B->A,
5. 2nd in A><B->B.

   Example - LISP functions

6. CAR::=1st,
7. CDR::=2nd,
8. CONS::=fun[a,b](a,b).

   Example - triples

9. A><B><C::=$ Net{1st:A, 2nd:B, 3rd:C }. (a,b,c) ::A><B><C=(1st=>a, 2nd=>b, 3rd=>c).

   Triples and Pairs

   Notice that A><B><C is equivalent to A><(B><C) in the sense that we can construct a one-one function from any (a,b,c) in A><B><C into A><(B><C). The function M that does this is defined by:
10. For all a:A, b:b, c:C, M(a,b,c)::= CONS( a , CONS( b, c) ).
    
11. (M) |- CAR(M(x))=x.1st and CAR(CDR(M(x)))=x.2nd and CAR(CDR(CDR(M(x))))=x.3rd.

    The symbols

     	(M)|-

    are short for "Because of the definition of M the following statemnt is true".

    This is the theoretical justification for

    ---

    1. LISP's notation for lists
    2. Computer Science's obssession with binary trees.

    ---

    Sets of Tuples

    Let $ X be a type of tuple with variables x,y,z,... then the predicates in the variables x,y,z,... define susbsets of the set of all possible tuples. If the predicate is P(x,y,z,...) then
12. $ Net{X, P(x,y,z) } can be written for the set of tuples satisfying P.

    Example - a set of tuples

13. circle1::= $ Net{x,y:real, r:Real&Positive, x^2+y^2<=r^2}.

    It is convenient to give a name to a collection of declarations, predicates and definitions. There are two forms - short and long:

    Short form

     S::=Net{ a:A, b:B, c:C, ..., P, Q, ..., x:=e,... }

    Long Form

     S::=following

     .Net

     	a::A,

     	b::B,

     	c::C,

     	...

     	|-P,

     	|-Q,

     	...,

     	x::=e,

     	...

     .Close.Net

    Comments and theorems can also be included in the long form.

     		(reasons)|- Theorem.

    Anything that is not recognised as a declaraction, definition, assumption(axiom), formula, or theorem is a comment.

    Example - CIRCLE

14. LONG_CIRCULAR::=following
    Net
    1. x::Real.
    2. y::Real.
    3. r::Real & Positive.
       
    4. |- (circle_axiom): x^2+y^2 <= r^2.
       
    5. (above) |- (circle_theorem): if r=0 then x=y=0.

    
    (End of Net)
    
15. CIRCULAR::=Net{x,y:real, r:Real&Positive, x^2+y^2<=r^2},
16. circle::=$ CIRCULAR. So this definition of circle has the same effect as the definition of circle1 above. We can even prove this be substituting equal eaxpressions:
    
17. (circle, circle1) |- circle1 = circle.

    Either-Or

    There is another way to make structures from components - the discriminated union.

     U::=\/{ a:A, b:B, c:C,.... z:Z}

    means that for any x:A, (a=>x) in U, for any x in B, (b=>x) in U, and so on. Further, if x:U then

     	type(x) = the Tag t such that (t=>x.t)=x.

    Also if S is one of the sets A,B,C,....Z and s:S then

     	s.U = ( t=>s) in U for the 'tag' t.

    Inheritance

    There is a simple notation when we want to say that one set is a subset of another set, but with certain extra properties:

     		Extended_set::= Super_set with{ Extra_component and properties}

    Specifying Unique Objects

    Given a structure S=$ N, where

     	N=Net{a:A, b:B, c:C, ..., P, Q, R,  x:=e,...}

    it is not always necessary to specify all the components to determine an unique object. For example if N=Net{ a,b:Real, a=2*b+1} then there is exactly one object in $ N which has a=3, namely the one with b=1. So

     	(a=>3, b=>1) = the n:$ $N( n.a=3 ).

    A shorthand notation can be used:

     	the N(a=3) = (a=>3, b=>1).

    In general

     	the N(W) = the $(N and W) = the N with(W).

    whenever there is exactly one object in $(N and W).

    Constrained Structures are Subsets of Type

    MATHS lets you include constraints in a structure definition. For example the mathematical structure of a point in a plane as something that has both Cartesian(x,y) and Polar(arg,abs) coordinates, as long as they both refer to the same point:

18. POINT::=following
    Net
    x,y::Real.
    1. arg::Angle.
    2. abs::Positive&Real.

       
       

    3. |-abs^2=x^2+y^2.
       
    4. |-tan(arg)=x/y.
    
    (End of Net)
    The symbol

     		|-

    used above include an unproved assumption into the meaning of POINT.

    This means that

    	the POINT(x=>1,y=>1) = the POINT(abs=>1, arg=45.degrees).

    Thus at the conceptual, logical, and mathematical level we can document properties that must be true - without describing any means for this to be done.

    This and some other more advanced techniques makes it possible to document the properties of real life entities.

. . . . . . . . . ( end of section Records and Labeled Tuples) <<Contents | Index>>