(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, extended, used,
inherritted in the definitions of other structures.
For complex record structures/classes/signatures/... the long form can be used
RECORD::=following
.Net
...
a::A.
...
b::B.
...
.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:
$ $RECORD
Example
Class or Set:
phones::=$ Net{name:Strings, number:Strings}.
Object in phones:
(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
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 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.
The symbols
(M)|-are short for "Because of the definition of M the following statemnt is true".
This is the theoretical justification for
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,... }
In this short form all the types can be omitted and then default to being "Sets":
REA::=Net{ Resources, Entities, Agents }.
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.
You can abbreviate this to
WEEK::= Net{... day: Days^7, ..., 1st(day)=sunday, ...}.
When defining data the notation defined in XBNF for option is very helpful:
In less concrete cases then one can use a set with no more than one element.
Example -- optional area code in a phone number
phones::=$ Net{name:Strings, number:Strings, area_code: O(Strings)}.
(name=>"John Doe", number=>"123-4567", area_code=>"") \in phones.
(name=>"John Doe", number=>"123-4567", area_code=>"909") \in phones.
AUTO ::= Net{ ..., air_bag: @ABU, Card(air_bag) in 0..1, ...}.
the AUTO ( make=Ford, model=Escort, air_bag=>{}, ...).
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:
Extended_set::= Super_set with{ Extra_component and properties}
For example:
AUTO::= Net{ make:Manufacters, model=Models, ...}.
AUTO_WITH_BAG::= AUTO with { air_bag: ABU }.
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).
the AUTO ( make=Ford, model=Escort, ...) \in $ AUTO.
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 ∈ $ AUTO_WITH_BAG then, a.AUTO ∈ $ 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:
|-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.
Either-Or Structures
There is another way to make structures from components - the discriminated
union. This allows an object to have different structures.
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.
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 [ notn_00_README.html ]
Lexemes and Basic Syntax [ notn_10_Lexicon.html ] [ notn_11_Names.html ] [ notn_12_Expressions.html ] [ notn_9_Tables.html ] [ notn_8_Evidence.html ]
Documentation and Ontologies [ notn_13_Docn_Syntax.html ] [ notn_14_Docn_Semantics.html ] [ notn_15_Naming_Documentn.html ] [ notn_16_Classification.html ]
Advanced techniques [ notn_2_Structure.html ] [ notn_3_Conveniences.html ] [ notn_4_Re_Use_.html ] [ notn_5_Form.html ] [ notn_6_Algebra.html ] [ notn_7_OO_vs_Algebra.html ]
. . . . . . . . . ( end of section Records and Labeled Tuples) <<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 = Net{radius:Positive Real, center:Point}.
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