.Open Records and Labeled Tuples
. Basics of records and structures
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:
.As_is           (a=>xa, b=>xb, ...).
The set of all objects with fields a,b,... of type
A,B, .. (respectively) is shown like this:
.As_is 	$ Net{ a:A,  b:B,  ... }.
Usually however it pays to give a name to the abstract structure
.As_is 	RECORD::=Net{ a:A,  b:B,  ... }.
This allows the structure itself to be referred to, extended, used,
inherritted in the definitions of other structures.

For complex record structures/classes/signatures/... the long form can be used
.As_is 	RECORD::=following
.As_is 	.Net
.As_is 		...
.As_is 		a::A.
.As_is 		...
.As_is 		b::B.
.As_is 		...
.As_is 	.Close.Net
(You can add constraints and comments to these descriptions...)

The dollar sign is put in front of the name to indicate the set of
object that fit the named structure:
.As_is 	$ $RECORD

. Example
Class or Set:
.As_is 	phones::=$ Net{name:Strings, number:Strings}.

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

. Formal definition
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
.As_is 	a in X -> A,
.As_is 	b in X -> B,
.As_is 	c in X -> C,
and if x:X then
.As_is 	a(x)=x.a=`the a of x`,
.As_is 	b(x)=x.b=`the b of x`,
.As_is 	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 and MATHS Nets
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
	A><B::=$ Net{1st:A, 2nd:B},
	(a,b) ::=(1st=>a, 2nd=>b),
So we can deduce the following formulae must also hold:
	(a,b).1st=a,
	(a,b).2nd=b.
	1st in A><B->A,
	2nd in A><B->B.


. Example - LISP functions
	CAR::=1st, 
	CDR::=2nd, 
	CONS::=fun[a,b](a,b).

. Example - triples
	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:
 For all a:A, b:b, c:C, M(a,b,c) ::= $CONS( a , $CONS( b, c) ).
 (M)|- $CAR($M(x))=x.1st and $CAR($CDR(M(x)))=x.2nd and $CAR($CDR($CDR($M(x))))=x.3rd.

The symbols
.As_is 	(M)|-
are short for "Because of the definition of M the following statemnt is true".

This is the theoretical justification for
.Box
 LISP's notation for lists
 Computer Science's obssession with binary trees.
.Close.Box
. Sets of Tuples and Constraints
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
	$ Net{X, P(x,y,z) }
can be written for the set of tuples satisfying P.

. Example - a set of tuples
	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
.As_is S::=Net{ a:A, b:B, c:C, ..., P, Q, ..., x:=e,... }

In this short form all the types can be omitted and then default to
being "Sets":
.As_is	REA::=Net{ Resources, Entities, Agents }.

. Long Form
.As_is S::=following
.As_is .Net
.As_is 	a::A,
.As_is 	b::B,
.As_is 	c::C,
.As_is 	...
.As_is 	|-P,
.As_is 	|-Q,
.As_is 	...,
.As_is 	x::=e,
.As_is 	...
.As_is .Close.Net

Comments and theorems can also be included in the long form.
.As_is 		(reasons)|- Theorem.
Anything that is not recognised as a declaraction, definition, assumption(axiom), formula, or theorem is a comment.

. Example - CIRCLE
LONG_CIRCULAR::=following
.Net
	x::Real.
	y::Real.
	r::Real & Positive.
	|- (circle_axiom): x^2+y^2 <= r^2.
	(above)|-(circle_theorem): if r=0 then x=y=0.

.Close.Net
	CIRCULAR::=Net{x,y:Real, r:Real&Positive, x^2+y^2<=r^2},
	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:
	(circle,circle1)|- circle1 = circle.
. Multiple parts in a Structure or Record
MATHS doesn't provide a special notation for optional and multiple
parts in a structure/signature/class/record.   Instead there are
types and standard sets that can be used.
. Example -- Days in a Month
A month can have a number of days between 27 and 31 -- in the Western calendar.
Here are some ways of noting this structure
	MONTH_HAS_SET_OF_DAYS::= Net{ ..., day: @DAY, 27<= Card(day) <=31, ....}.
Days in a month are a set with between 27..31 DAYs.
This means that the days are not in order but don't repeat.

	MONTH_HAS_A_SEQUENCE_OF_DAYS::= Net{ ..., day: #DAY, 27<= Card(day) <=31, ....}.
Days in a month are a sequence with between 27..31 DAYs.
This means that the days are in order and are numbered 1,2,3,...


	MONTH_HAS_AN_ARRAY_OF_DAYS::= Net{ ..., ndays:27..31, day: 0..ndays-1>->$ DAY,  ....}.
Days in a month are an array (map) indexed by a number from
0 to the number of days. 

You can abbreviate this to
	MONTH_HAS_AN_ARRAY_OF_DAYS::= Net{ ..., ndays:27..31, day: $ DAYS^0..ndays-1,  ....}.
. Example -- 7 days in a week
.As_is 		WEEK::= Net{... day: Days^7, ..., 1st(day)=sunday, ...}.
. Optional parts in a Structure or Record
MATHS doesn't provide a special notation for optional 
parts in a structure/signature/class/record.   Instead there are
types and standard sets that can be used.  

When defining data the notation defined
in XBNF for option is very helpful:
	For X:@strings, O(X) = {""} | X.

In less concrete cases then one can use a set with no more than one element.

. Example -- optional area code in a phone number
.As_is 	phones::=$ Net{name:Strings, number:Strings, area_code: O(Strings)}.
.As_is 	(name=>"John Doe", number=>"123-4567", area_code=>"") \in phones.
.As_is 	(name=>"John Doe", number=>"123-4567", area_code=>"909") \in phones.
. Example -- optional air bag in an automobile
.As_is 	AUTO ::= Net{ ..., air_bag: @ABU, Card(air_bag) in 0..1, ...}.
.As_is 	the AUTO ( make=Ford, model=Escort, air_bag=>{}, ...).
.As_is 	the AUTO ( make=Ford, model=Escort, air_bag=>{ford_airbag_17}, ...).

Notice in the above examples the "optional" component is not omitted
but is given a null value -- "" or {}.  There is a way to define a special
kind of object that has extra components.
See $Inheritance below.


. 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:
.As_is 		Extended_set::= Super_set with{ Extra_component and properties}

For example: 
.As_is 	AUTO::= Net{ make:Manufacters, model=Models, ...}.
.As_is 	AUTO_WITH_BAG::= AUTO with { air_bag: ABU }.
. Specifying Unique Objects with a Structure

Given a structure S=$ $N, where 
.As_is 	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
.As_is 	(a=>3, b=>1) = the n:$ $N( n.a=3 ).
A shorthand notation can be used:
.As_is 	the N(a=3) = (a=>3, b=>1).
In general
.As_is 	the N(W) = the $(N and W) = the N with(W).
whenever there is exactly one object in $(N and W).

.As_is 	the AUTO ( make=Ford, model=Escort, ...) \in $ AUTO.
.As_is 	the AUTO_WITH_BAG ( make=Ford, model=Escort, air_bag=>{ford_airbag_17}, ...)  \in $ AUTO_WITH_BAG.

However, notice that an AUTO_WITH_BAG is not an AUTO.  It contains an AUTO
with in it.   So, if a \in $ AUTO_WITH_BAG then, a.AUTO \in $ AUTO.

. 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:
POINT::=following
.Net
		x,y::Real.
		arg::Angle.
		abs::Positive&Real.

		|- abs^2=x^2+y^2.
		|- tan(arg)=x/y.
.Close.Net
The symbol
.As_is 		|-
used above include an unproved assumption into the meaning of $POINT.

This means that
.As_is	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.

. Either-Or Structures
There is another way to make structures from components - the discriminated
union.  This allows an object to have different structures.

.As_is 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
.As_is 	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
.As_is 	s.U = ( t=>s) in U for the 'tag' t.

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

Here are the links into the formal documentation of th notations

Introduction
.See ./notn_00_README.html

Lexemes and Basic Syntax
.See ./notn_10_Lexicon.html
.See ./notn_11_Names.html
.See ./notn_12_Expressions.html
.See ./notn_9_Tables.html
.See ./notn_8_Evidence.html

Documentation and Ontologies
.See ./notn_13_Docn_Syntax.html
.See ./notn_14_Docn_Semantics.html
.See ./notn_15_Naming_Documentn.html
.See ./notn_16_Classification.html

Advanced techniques
.See ./notn_2_Structure.html
.See ./notn_3_Conveniences.html
.See ./notn_4_Re_Use_.html
.See ./notn_5_Form.html
.See ./notn_6_Algebra.html
.See ./notn_7_OO_vs_Algebra.html
.Close Records and Labeled Tuples