Introduction

In MATHS a piece of documentation can be interpreted as defining a labeled tpl. In other words a sequence of values (expressions) each with a unique identifier. An example might be

 		(number=>3, square=>9)

There are many convenient forms however.

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

 	.List

 	 a=>p,

 	 b=>q,

      ....

 	 z=>t

 	.Close.List

 		$(name_of_documentation)

Creates a standard tuple where each id comes from the documentation and refers to a variable with the same name.

 		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.

 		the name_of_documentation(p, q, ...)

1. -- p,q, are values for a,b,c...

    		the name_of_documentation(P,Q,R,...)

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

   Syntax

3. structured_set::= #("$" |"@" |"#" | simple_set_expression"^" ) structure_description ).

4. structure_description::= ( ( Name | documentation) #( "(" List(predicates) | L((variable"=>"value | "for" quantifier variable), comma) ")" | "." variable |"." "(" L(variable, comma) ")") ).

5. operations::="and" | "or" | "not" | "iff" |...

   A piece of formal documentation is, after deleting comments, proofs, and formatting, a set of declarations, definitions and assertions:

6. documentation::="Net{"element #(", "element) "}"

7. For S:documentation, (f,F):declarations(S), X=S, f in F^X and X.f ::= F.
8. 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.

   
   

9. (above)|- (S0): for x,y:X, (for all f:variables(s) (x.f=y.f) iff x=y)

   
   

10. (above)|- (S1): x.f in X.f
    
11. (above)|- (S2): for y:F, y./f={x:X||x.f=y}

    
    

12. (above)|- (S3): x in X iff x=(a=>x.a, b=>x.b,...) and W(x.a, x.b, ...)

13. For l:=(u,v,...):#variables(s), x.l::=(u=>x.u, v=>x.v,...).
14. 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

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

    Constraints

18. For N:name_of_documentation, S:N./name, (P,Q,R,...) :#predicates, N(P,Q,R, ...) ::= $ Net{ N. P. Q. R. ...}.

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

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

    Note

    The formula D is the set satisfying D and so finding the '$' can be thought of as solving the relationships embedded in D:
20. QUADRATIC_EQUATION::=Net{ x:numeric, a*x*x+b*x+c=0 },
    
21. (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
    
22. (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:
23. 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:
    
24. |- (key1): Name(keys)->(determined)
    
25. |- (key2): For all keys, one determined(Name).
    
26. |- (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:

27. SIMPLE::=Net{ a,b,c:Real}.
28. SAMPLE::=Net{ SIMPLE. c=a+b}.
    
29. (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:

30. QUADRATIC_EQUATION::=Net{ a, b, c, x:numeric, a*x*x+b*x+c=0 },
31. 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:

    
    

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

33. (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 variable a,b,c,....
34. t with(v=>e(a,b,c,...):: $ Net{... , v:T} and value
35. 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 rewriten

36. t with (a=>1).

    Link to Data Bases

    Tuples a naturally considered to be elements of a database: [ math_13_Data_Bases.html ]

. . . . . . . . . ( end of section Structures) <<Contents | End>>

Notes on MATHS Notation

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

For a more rigorous description of the standard notations see