- Records and Labeled Tuples
- : Basics of records and structures
- : Example
- : Formal definition
- : Example - Phone numbers
- : UML and MATHS Nets
- : Example - pairs
- : Example - LISP functions
- : Example - triples
- : Triples and Pairs
- : Sets of Tuples and Constraints
- : Example - a set of tuples
- : Short form
- : Long Form
- : Example - CIRCLE
- : Multiple parts in a Structure or Record
- : Example -- Days in a Month
- : Example -- 7 days in a week
- : Optional parts in a Structure or Record
- : Example -- optional area code in a phone number
- : Example -- optional air bag in an automobile
- : Inheritance
- : Specifying Unique Objects with a Structure
- : Constrained Structures are Subsets of Type
- : Either-Or Structures
- : More
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS
- Glossary

- 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

(M)|-

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

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

## 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

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

## 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

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

(End of 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

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

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.

## Example -- optional air bag in an automobile

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

## Specifying Unique Objects with a Structure

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 generalthe 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:

- POINT::=following

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.

## 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 thentype(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 thens.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 ]

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

(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

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

Object in phones:

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

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

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.

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

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 ]

For a more rigorous description of the standard notations see