.Open 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
.As_is (number=>3, square=>9)
which fits the formal structure:
.As_is Net{ number, square:Int. square = number * number }
However the type off the above object is the free or onconstrained
net:
.As_is Net{ number, square:Int }
There are many convenient forms of structured objects however.
.As_is (a=>p, b=>q, ..., z=>t)
.As_is .List
.As_is a=>p,
.As_is b=>q,
.As_is ....
.As_is z=>t
.As_is .Close.List
We can describe objects in terms of the net to which the belong:
.As_is the SQUARE (number=>3, square=>9)
.As_is 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 SQUARE ( number=>4 ) = (number=>4, square=>16).
the SQUARE (square=>9) = (number=>3, square=>9).
The following
.As_is $(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).
.As_is the name_of_documentation(p, q, ...)
-- p,q, are values for a,b,c in order of declaration.
.As_is 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:
.As_is $ Net{ some_documentation }
.As_is
.As_is $ name_of_documentation...
Documentation is named like this:
.As_is name_of_documentation::=following.
.As_is .Net
.As_is declarations, definitions, and assertions
.As_is .Close.Net
. Older form
In older documentation this form was used:
.As_is name_of_documentation::=Net{
.As_is declarations, definitions, and assertions
.As_is }=::name_of_documentation.
There is is also an old short form:
.As_is 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.
()|-(S0): for x,y:X, (for all f:variables(s) (x.f=y.f) iff x=y).
()|-(S1): For x:X, x.f in X.f.
()|-(S2): for y:F, y./f={x:X||x.f=y}.
()|-(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>**"John Smith", number=>"714-123-5678") in phone.
()|- 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
.Row {x:A||W(x)} Set of objects in A satisfying W.
.Row $ Net{x:A, W(x)} Set of objects (x=>a) where a in A and W(a).
.Row {x in A, W(x)} Set with two elements, both being either true or false.
.Row 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 },
()|-$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
()|- 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}.
()|- 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:
()|- (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
.See [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...
.Hole OperationsOnObjectDefintion
To define
.Key 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...}):
.As_is For x0:real, setX(x0)::operation = (x'=x0).
.As_is For y0:real, setY(y0)::operation = (y'=y0).
.As_is For x0,y0:real, move(x0,y0)::operation = (x'=x+x0 and y'=y0+y).
Inside COUNTER=Net{ count::Nat0 }
.As_is 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
.As_is For x:parameters, f(x)::operation=p.
for some predicate `p` to a net called `N`, is to create a new net
.As_is For x:parameters, f(x)::@($ N, $ N)= following,
.As_is .Net
.As_is |- N and N'.
.As_is p.
.As_is .Close.Net
Similarly with
.As_is f::operation = p.
for some predicate `p` to a net called `N`, is to create a new net
.As_is f::@($ N, $ N)= following,
.As_is .Net
.As_is |- N and N'.
.As_is p.
.As_is .Close.Net
Similarly it is possible to declare an operation and have its meaning
defined later. For example if,
.As_is 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
.As_is f::@($ N, $ N)= following,
.As_is .Net
.As_is |- N and N'.
.As_is p.
.As_is .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:
.See http://www.csci.csusb.edu/dick/maths/math_13_Data_Bases.html
.Close Structures
**