- Structures
- : Introduction
- : Older form
- : Free Nets
- : Syntax
- : Equivalent forms
- : Example Net
- : Constraints
- : Note
- : Abbreviation
- : Note
- : Partly baked idea -- extending tuples
- : Partly Baked Idea -- Operations on Objects
- : Link to Data Bases
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS
- Glossary

- the SQUARE ( number=>4 ) = (number=>4, square=>16).
- the SQUARE (square=>9) = (number=>3, square=>9).
The following

$(name_of_documentation)

Creates a standard tuple where each id comes from the documentation and refers to a variable with the same name. If - SQUARE::= Net{ number, square:Int. square = number * number } then
- $(SQUARE) = (number=>number, square=>square).
the name_of_documentation(p, q, ...)

- -- p,q, are values for a,b,c in order of declaration.
the name_of_documentation(P,Q,R,...)

- --- P,Q, R,... are properties of the variables etc...
The set of all tpls satisfying some documentation is written as follows:

$ Net{ some_documentation }

$ name_of_documentation...

Documentation is named like this:

name_of_documentation::=following.

.Net

declarations, definitions, and assertions

.Close.Net

## Older form

In older documentation this form was used:name_of_documentation::=Net{

declarations, definitions, and assertions

}=::name_of_documentation.

There is is also an old short form:

Net{....}

designed to be embedded in expressions rather than named.These are like the structures, tuples, plexes, records, logical data groups, structs, etc found in most programming languages and computing methods. They are the basis for defining classes of objects. Objects also possess behaviors however. Behaviors these can be modeled using mappings and relations. However, MATHS structures do have a form of inheritance and polymorphism.

## Free Nets

When the constraint in a Net is "true" then it is omitted.If each set mentioned is also a type (and so also unconstained) then the Net is a free Net. The free net is the type of its objects.

## Syntax

- structured_set::= #("$" |"@" |"#" | simple_set_expression"^" ) structure_description ).
- structure_description::= ( ( Name | documentation) #( "(" List(predicates) | L((variable"=>"value | "for" quantifier variable), comma) ")" | "." variable |"." "(" L(variable, comma) ")") ).
- operations::="and" | "or" | "not" | "iff" |...
A piece of formal documentation is, after deleting comments, proofs, and formatting, a set of declarations, definitions and assertions:

- documentation::="Net{"element #(", "element) "}"
- For S:documentation, (f,F):declarations(S), X=S, f in F^X and X.f ::= F.
- For S:documentation, (f,F):declarations(S),W(a,b,...)=constraint(S), X=S, x:X, x.f::= f(x).
- For S:documentation, (f,F):declarations(S),(a,b,...)=variables(S), W(a,b,...)=constraint(S), X=S, x:X, for x,y:X, if for all f:variables(s) (x.f=y.f) then x=y.
- (above)|- (S0): for x,y:X, (for all f:variables(s) (x.f=y.f) iff x=y).
- (above)|- (S1): For x:X, x.f in X.f.
- (above)|- (S2): for y:F, y./f={x:X||x.f=y}.
- (above)|- (S3): x in X iff x=(a=>x.a, b=>x.b,...) and W(x.a, x.b, ...).
- For l:=(u,v,...):#variables(s), x.l::=(u=>x.u, v=>x.v,...).
- For l:=(u,v,...):#variables(s), X.l::=$ Net{u:X.u, v:X.v,...}.
## Equivalent forms

$ Net{a:A, b:B, ... z:Z, W(a,b,...z),...}={(a=>xa,b=>xb,...)||for some xa:A, xb:B,... (W(xa,xb,xc,...) ) } =$[a:A,b:B,c:C,...z:Z](W(a,b,c,...,z)and ...).

$ Net{a:A, b:B, ... z:Z, W(a,b,...z)...} --- {(xa,xb,...,xz):A><B><C...><Z || W((xa,xb,xc,...)}.

Since the two forms are isomorphic, either can be used to describe an element.

## Example Net

- phone::=$ Net{name:$ NAME, number:$ NUMBER. }.
- (above)|-(name=>"John Smith", number=>"714-123-5678") in phone.
- (above)|-phone;(name,number) in phone --> $ NAME><$ NUMBER.
## Constraints

- For N:name_of_documentation, S:N./name, (P,Q,R,...) :#predicates, N(P,Q,R, ...) ::= $ Net{ N. P. Q. R. ...}.
- For N:name_of_documentation, S:N./name, (P,Q,R,...) :#predicates, the N(P,Q,R,...)::= the $ Net{ N. P. Q. R. ...}.
The above is only defined when a single element is selected by the adding
constraints P, Q, R,... to the documentation called N.
.Dangerous_bend The following expressions are not the same:

**Table**{x:A||W(x)} Set of objects in A satisfying W. $ Net{x:A, W(x)} Set of objects (x=>a) where a in A and W(a). {x in A, W(x)} Set with two elements, both being either true or false. Net{x in A, W(x)} Set of documentation with variable x and constraint W(x).

(Close Table)

## Note

The formula D is the set satisfying D and so finding the '$' can be thought of as solving the relationships embedded in D: - QUADRATIC_EQUATION::=Net{ x:numeric, a*x*x+b*x+c=0 },
- (above)|-QUADRATIC_EQUATION={ (x=>(-b+sqrt(b^2-4*a*c))/(2*a)), (x=>(-b-sqrt(b^2-4*a*c))/(2*a))}.
If there is a unique solution we can write
- (above)|-the QUADRATIC_EQUATION(a=1,b=2,c=1) = (a=>1, b=>2, c=>1, x=>-2).
## Abbreviation

After a dollar sign the word "Net" can be omitted: - For X, ${X} ::= $ Net{X}.
## Note

The type of a tuple is determined by (1) what elements are shown or (2) the name of the documentation, or (3) the set used in a declaration. This means that it is ambiguous to permit default values for missing elements unless the type is indicated by naming the documentation or the declaration. In the the second two forms there is often enough information to make it unnecessary to give values of all the declared parts. In other words a subset of the parts determines a unique object. This property is written in several ways: - |- (key1): Name(keys)->(determined).
- |- (key2): For all keys, one determined(Name).
- |- (key3): (keys) in ids(Set).
This can result from internal axioms and definitions, or can be assumed as
the defining property of the normal set of data. In this second case any
operation on the data needs to preserve the uniqueness of the keys.
To indicate that such a property is used the ellipsis symbol(...) can be used to indicate the object (when unique) that is formed by filling in the missing parts by using the definitions and axioms in the named documentation:

- SIMPLE::=Net{ a,b,c:Real}.
- SAMPLE::=Net{ SIMPLE. c=a+b}.
- (above)|-the SIMPLE(a=>1, b=>2, c=>3)= the SAMPLE(a=>1, b=>2, ...) = the SAMPLE(a=1, b=2).
There is no ready made concept of a default value in MATHS - this leads to many ambiguities. However, for any given structured set, it is possible to define another structured set which describes the default or standard situation as a special embedding of parts of its structure. For example suppose we want to talk about quadratic equations, and most of them have the coefficient of x^2 equal to 1, then we can define:

- QUADRATIC_EQUATION::=Net{ a, b, c, x:numeric, a*x*x+b*x+c=0 },
- STANDARD_QUADRATIC_EQUATION::=Net{ b, c, x:numeric, x*x+b*x+c=0 },
Then we set up a context dependent definition that embeds any Standard quadratic in the class of general quadratics:

- |-For t:STANDARD_QUADRATIC_EQUATION, t:QUADRATIC_EQUATION=(a=>1, b=>t.b, c=>t.c, x=>t.x).
The above states that any standard quadratic equation is to be interpreted as a general quadratic equation with a=1 whenever the context demands it. So for example:

- (above)|-(b=>2,c=>1,x=>-1);QUADRATIC_EQUATION =(a=>1, b=>2, c=>1, x=>-1).
Notice that this is a safe and explicit form of polymorphism or sub-typing.

## Partly baked idea -- extending tuples

Given a tuple t=(a=>x, b=>y, c=>z, ... ) in $ Net{a...} then Date and Darwen [DateDarwen07] propose an operator that adds a new element to t (and so changes its type). Let v be an identifier that is not used in t, and e(a,b,c,...) be an expression with type T containing the variables a,b,c,.... t with (v=>e(a,b,c,...)) :: $ Net{... , v:T}, and value - t with (v=>e(a,b,c,...)) = (a=>x,b=>y,c=>z, ..., v=>e(x,y,z,...)).
Thus the map from t:$ STANDARD_QUADRATIC_EQUATION into $ QUADRATIC_EQUATION can be rewritten

- t with (a=>1).
## Partly Baked Idea -- Operations on Objects

The following was added Nov/20/2010 and is under review... [click here OperationsOnObjectDefintion if you can fill this hole]To define object-oriented operations within the Net. It must mean a relation between the state of an object before and after the operation. We need syntax like this (inside POINT=Net{x,y:Real...}):

For x0:real, setX(x0)::operation = (x'=x0).

For y0:real, setY(y0)::operation = (y'=y0).

For x0,y0:real, move(x0,y0)::operation = (x'=x+x0 and y'=y0+y).

Inside COUNTER=Net{ count::Nat0 }increment::operation=(count'=count+1).

Then if p:$ POINT, then if q=p.setX(2) then q.x=2, for example.

If c:$ COUNTER and c increment d then d.count=c.count+1.

This requires a new symbol/reserved word in the MATHS language:

- operation::lexeme, indicates an operation acting on objects defined in the containing Net.
The usual conventions on dynamic predicates hold in the definition of the operation. So free variables that are not primed somewhere are static and invariant. The existence of a prime on a variable lets it change.

We don't have to be sure that every operation leads to an existing state since in MATHS dynamic predicates are also conditions with "false" acting as "fails".

The effect of adding

For x:parameters, f(x)::operation=p.

for some predicate p to a net called N, is to create a new netFor x:parameters, f(x)::@($ N, $ N)= following,

.Net

|- N and N'.

p.

.Close.Net

Similarly withf::operation = p.

for some predicate p to a net called N, is to create a new netf::@($ N, $ N)= following,

.Net

|- N and N'.

p.

.Close.Net

Similarly it is possible to declare an operation and have its meaning defined later. For example if,

f::operation.

is in a net called N, then it is possible to create a new net by defining f. If p is a predicate then N(f=p), is to create a new netf::@($ N, $ N)= following,

.Net

|- N and N'.

p.

.Close.Net

Notice we already have a way to write queries

- For x:parameter, query(x)::Set = e.
However, unlike the Z notation there is no convenient way in MATHS to both change the state of an object and get a response from it. MATHS enforces the separation of operations and query. But operations -- even queries -- can fail and so be use to test the state of an object.

## Link to Data Bases

Tuples a naturally considered to be elements of a database: [ math_13_Data_Bases.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.

(number=>3, square=>9)which fits the formal structure:

Net{ number, square:Int. square = number * number }

However the type off the above object is the free or onconstrained net:

Net{ number, square:Int }

There are many convenient forms of structured objects however.

(a=>p, b=>q, ..., z=>t)

.List

a=>p,

b=>q,

....

z=>t

.Close.List

We can describe objects in terms of the net to which the belong:

the SQUARE (number=>3, square=>9)

the name_of_documentation(a=>p, b=>q, ...)This places p,q,... in place of a,b, ... respectively to create an object that fits the documentation.

. . . . . . . . . ( end of section Structures) <<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 might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

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