[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / math_12_Structure
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Jun 26 16:09:41 PDT 2012

Contents


    Structures

      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)
      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.
    1. the SQUARE ( number=>4 ) = (number=>4, square=>16).
    2. 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
    3. SQUARE::= Net{ number, square:Int. square = number * number } then
    4. $(SQUARE) = (number=>number, square=>square).

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

       		the name_of_documentation(P,Q,R,...)
    6. --- 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

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

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

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

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

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

    11. For S:documentation, (f,F):declarations(S), X=S, f in F^X and X.f ::= F.
    12. For S:documentation, (f,F):declarations(S),W(a,b,...)=constraint(S), X=S, x:X, x.f::= f(x).

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


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


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


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

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

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

      Constraints

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

    24. 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:
    25. QUADRATIC_EQUATION::=Net{ x:numeric, a*x*x+b*x+c=0 },
    26. (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
    27. (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:
    28. 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:
    29. |- (key1): Name(keys)->(determined).
    30. |- (key2): For all keys, one determined(Name).
    31. |- (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:

    32. SIMPLE::=Net{ a,b,c:Real}.
    33. SAMPLE::=Net{ SIMPLE. c=a+b}.
    34. (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:

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


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

    38. (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
    39. 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

    40. t with (a=>1).

      Partly Baked Idea -- Operations on Objects

      The following was added Nov/20/2010 and is under review... [click here [socket symbol] 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:

    41. 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 net
       	For x:parameters, f(x)::@($ N, $ N)= following,
       	.Net
       		|- N and N'.
       		p.
       	.Close.Net
      Similarly with
       		f::operation = p.
      for some predicate p to a net called N, is to create a new net
       	f::@($ 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 net
       	f::@($ N, $ N)= following,
       	.Net
       		|- N and N'.
       		p.
       	.Close.Net

      Notice we already have a way to write queries

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

    . . . . . . . . . ( end of section Structures) <<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 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 ]

    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

  1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

    Glossary

  2. 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).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. 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.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

End