[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / notn_4_Re_Use_
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Sun Nov 14 16:23:24 PST 2010


    Re-use & Inheritance


      Because the MATHS notation includes the idea of naming a piece of documentation [ notn_15_Naming_Documentn.html ] [ notn_13_Docn_Syntax.html ] [ notn_14_Docn_Semantics.html ] it is possible to use the name as a reference to that documentation that implies its reuse in the current document. This page goes into the details of a natural an powerful idea.

      Re-using Documentation

      Named documentation is often used to construct elements, maps, sets etc..


         	X::=Net{ a:A, b:B, W(a,b...)}.
         	Y::=Net{ parts of Y, S:=$ X,  more parts of Y}.

        Then it is as if the definition of Y had been written:

         	Y::=Net{ parts of Y, S:={ a:A, b:B || W(a,b...) }, more parts of Y}.

        However, if the definition of X changes, then so does the definition of Y. There is no need for the definition of X to be in the same physical document if there is a ".See" directive:

         	.See X_s_URL#X
        or if there is link in the form of a remote_definition:

      (End of Net)

      The name of a piece of documentation can appear in other pieces of documentation referring to the original. This has an effect similar to that of 'inheritance' in object oriented programming languages - in essence the content of the named documentation replaces the name.
         	X::=Net{ a:A, b:B, W(a,b...)}
         	Z::=Net{ parts of Y, X, more parts of Y}.

        Then it is as if the definition of Z had been written:

         	Z::=Net{ parts of Y, a:A, b:B, W(a,b...), more parts of Y}.

        However, if the definition of X changes, then so does the definition of Z. The "X" in Z acts like a kind of "hot-linked macro". As above a ".See" directive permits the use of terms defined in other documents. A copy of the definition of X can also be imported or inherited in two ways:

         	W1::=Net{ parts of Y, definition(X), more parts of Y}.

         		parts of Y
         		more parts of Y

        Then it is as if the definition of W had been written:

         	W::=Net{ parts of Y, X:=Net{a:A, b:B, W(a,b...)}, more parts of Y}.

      (End of Net)

      When name of a piece of documentation is used in another piece of documentation then some of the declarations and definitions of the referenced documentation become part of the document that makes the reference. Other definitions and declarations may be redefined or redeclared and so be hidden. This follows the Rule of the Most Visible Meaning - symbols in an expression always refer to the most visible definition or declaration of the symbols that fits their particular context in the expression.

      When included documentation is inserted and includes a document that has already been included then this inclusion has no effect. Circular re-usage also has no effect.

      The key logical problem is that re-used documentation is quoted "out of context". This is similar to questions of dynamic and static scoping in programming language semantics. The formal semantics implies that identifers that appear in a piece of document but not defined in it can gain a meaning from the document in which they are re-used. This is close to dynamic scoping -- each re-use of a document may create a different binding for identifiers that are free in the re-used document. Therefore it wise to design documents for re-use that have no free variables: all variable should be bound as parameters or to terms. So, for example, given

       		WORSE::=Net{ a+b=c }.
       		BETTER::=Net{ Set:Sets, a,b,c:Set, a+b=c}.
      then WORSE has three free variables that can take on new meanings, but BETTER only has Sets free and this is defined in the MATHS's STANDARD package.

      Further, a re-used piece of documentation looses its original context. If a piece of documentation makes use of an assumption that is stated in its definition's environment, then it can not be validly used in another document unless that document recreates the context in which the original was defined. It is wise then to design special pieces of documentation (Nets) that state their assumptions explicitly. On the other hand: to insist that every re-usable piece of documentation explicitly states its contextual assumptions seems to be a heavy burden for the producer of the documentation. For example: suppose

      1. (1): For all a:A,b:B, if W(a,b) then W2(a).
      2. X::=Net{ a:A, b:B, W(a,b). |- W2(a) }
      3. Z::=Net{ parts of Y, X, more parts of Y}.

      (Close Let )
      Then Z's context consists of X's context plus the definition of X itself, and so the reuse of X within Z is valid. Similarly a document that makes use of an identifier that is declared in the environment rather than the document (A,B above for example) must also be defined (or declared) in the context in which the document is used. However in a context without a formula that at least implies (1) above, it is not valid to re-use Z. Notice that if a piece of documentation has no theorems or undeclared identifiers then it can be reused in any context.

      The declared variables in piece of documentation are effectively parameters for that documentation. One interesting question is what happens when a piece of documentation is re-used in a context where a parameter (declared variable) is bound to a fixed meaning. For example: M below has three variables { "Nat0", "0", "+" }

    1. M::=Net { Nat0:Sets, 0:Nat0, +:serial(Nat0), for all s:Nat0( s+0 = 0+s = s ) }.

      We don't expect to see the symbols "0" and "+" used like this, perhaps. But, this is equivalent to the basic definition that results by taking the generic monoid

    2. MONOID::= See http://cse.csusb.edu/dick/maths/math_31_One_Associative_Op.html#MONOID

      and substituting:

    3. MONOID( Set=>Nat0, op=> +, unit=>0). [ [ Modified Re-Use ] below] Now, we know that the natural numbers with zero form a monoid under addition, so, in any context where the natural numbers are available (the standard one), we could re-use M:
    4. |- (2): M. But to assert M like this means (apparently) that the declaration of M are added to our document and redefine 0, + and Nat0!

      Thus we have the following rule:

    5. When a piece of documentation D1 is re-used in document D2 and x is a variable declared in D1 like this
      for some set S and also appears as a constant in D2, then the declaration is converted into an axiom x in S in D2.

      So in any context where natural number exist, re-using or citing M above, effectively the following formulae:

    6. Nat0 in Sets.
    7. 0 in Nat0.
    8. + in serial(Nat0).
    9. for all s:Nat0( s+0 = 0+s = s ).

      Finally note that since these are all true in a context that define Nat0 as the natural numbers with 0, we would like assert M as a theorem:

    10. (above)|- (3): M. Meaning that the four formulae above are theorems.

      Proof of 3

      By inspection.

      A documentation system would help the users to disclose and hide the content quickly and easily. Either an 'out liner' or a hypertext model is an appropriate implementation. The system needs to also record the use of a given piece of documentation, and ensure that when the used documentation is changed then the all references to it are automatically kept in step - or (at least) protected from losing the linkage. When feasible a documentation system will make visible to a viewer the dependencies between documents buy placing two directives near the start of the document:

    11. .Uses list of names
    12. .Used_by list of names

      This ideal is difficult to reconcile with the freewheeling nature of the World-Wide Web. What happens if you refer to a document that someone else has written, and owns. How can they know? Can they be forced to maintain their end of the link? What happens if they need to revise their document -- formal documents evolve by a dialectical process of proposal, refutation, and improvement? I don't think there is any real solution to this problem. Clearly it means that it is best to link to documents that appear stable: well argued, reasonable, and based on stable assumptions. Clearly it means that it is necessary to regularly review links. Finally it is very wise to tell the author that you need the link and for authors to maintain a subscriber list who can be notified when changes are about to happen.

      Perhaps some form of deprecation process should be introduced. In standard deprecated features are likely not to be supported in a future version.

      Modified Re-Use

      A name can be followed by operations that describe modifications to the documentation to which it refers. These work as if they generated an edited copy that is inserted in place of the modified name.

      For example suppose

       	X::=Net{ a:A, b:B, W(a,b...)},
       	V::=Net{ parts of Y, X(a=>x, b=>c), more parts of Y},

      then it is as if the definition of V had been written:

       	Net{ parts of Y, x:A, x:B, W(x,y...), more parts of Y}.
       	V1::=Net{ parts of Y, X with P, more parts of Y},

      then it as if V1 was written

       	 Net{ parts of Y, a:A, b:B, W(a,b...). P.  more parts of Y}.


      Experience of object-oriented technology and methods provides convincing evidence of the need to take previous work and quickly extend it by adding new features and/or constraints. MATHS has two predefined notations to do this.

      First to add a constraint w to a document named N right 'N and w'. This is a simple reuse notation described earlier.

      To add a set of features (including both declarations and wffs) use: "with". This is again a simple abbreviation.

       	N with v:S
       	N with{ D }
       	N with following

      If a set S is defined as $ N then

    13. S and w::= $ Net{ N. w . }. S with {D}::=$ Net{ N. D. }.

      A common example:

    14. ALGEBRA::=Net{ Set:Sets }.
    15. SEMIGROUP::= ALGEBRA with op:associative(Set).
    16. MONOID::= SEMIGROUP with u:neuter(op).


      Notice that a new formal system can easily be created that inherits features from many different formal systems -- merely by asserting them:
    17. RING::=following,

      1. |- (r1): GROUP(Set, +, 0, -).
      2. |- (r2): MONOID(Set, *, 1).
      3. |- (r3): (*) distributes_over (+).
      4. ...

      (End of Net)

      The result is a system (a logic, an algebra, a model, ...) that satisfies the properties of both its parent systems. MATHS includes multiple inheritance... just like its less formal parent "mathematics" did.


      However there is a danger in combining a pair of systems like this. You may end up describing a class that can not exists - a triangle with four sides. Therefore it is important that whenever you reuse a mathematical system you always create an example that satisfies all the rules you have gathered together. For example the Natural numbers {0,1,2,3,...} satisfy the three axioms r1, r2, r3 above.

      This may also help your readers understand what you are getting at.


        Documentation is Data

        Documentation can be assigned names in definitions. The simplest document is a net of declarations, definitions, comments and assertions:
        or a name or term defined to equal one of these nets. It is reused by by using the name plus some simple changes
        The changes include applying substitutions, quantifications, and projections to the documentation (left to right).

        Variables and terms can be changed when referring to some documentation:

        	documentation(old=>new, ... )
        The above names the result of replacing all free occurrences of old in the documentation by new. New can be a constant, expression, or a variable.

        Terms can also be bound and so hidden:

        	documentation(for some list_of_hidden_terms)

      1. Similarly it is possible to hide all variables and terms except a specified subset, by using a projection.

      2. Parts can be added to a defined network as well:
         	documentation with element

      3. Two or more pieces of documentation can also be combined using the Boolean operations.

        If a document is basic (it has no definitions or theorems) then it is possible to remove axioms from it

        	basic_documentation without (list_of_axioms)
        However this is deprecated because it indicates that there is a simpler network of assumptions that could have been studied first.

        These (possibly modified) pieces of documentation can be combined as if they were propositions - MATHS defines the resulting documentation, it does not entail any logical calculus of documentation yet (unlike Z). The result of editing and combining can be used as a macro in any other piece of documentation. These structures can be used any where the name of a local piece of documentation can be used.

        The usage of terms needs be documented (automatically) in both the reference and also in the referred to documentation.

        Example -- Piping two specifications

        Suppose that N1 is the name of some documentation describing a variable called output and N2 is the name of documentation that describes a variable input then
      4. (N1 and N2 and output=input)(for some input, output), specifies a process that connects N1 to N2 and hides the connection.

        Beyond Re-use

        In MATHS combining documentation is merely a notational convenience. A full calculus could be developed in the future. The basis will be an equivalence relation or congruence on pieces of documentation. Two pieces of documentation are semantically equivalent if they have the same signature (variables and types) and for all values of the variables the constraints are equal. Thus D1 and D2 are equivalent if they are of the same type and define the same set of tuples:

      5. For Documentation D1,D2, if signature(D1)=signature(D2) then D1 equivalent D2::= ($ D1 = $ D2) else D1 equivalent D2::=false.

        In the example above, Z is equivalent to Y and X.

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

      Formal description of Reuse

        [ notn_15_Naming_Documentn.html ] [ notn_13_Docn_Syntax.html ] [ notn_14_Docn_Semantics.html ]


        1. elementary_piece_formal_documentation::=... | cross_reference,

        2. cross_reference::=(document_description | simple_reference) citation.

          PROPOSITION(elementary_proposition=>elementary_document, proposition=>document_description). [ logic_10_PC_LPC#PC] .

        3. elementary_document::=net | re_used_document.

        4. simple_reference::= "With" Name,

        5. directive::=(".Used_by" | ".See" |".Use" ) #Name EOLN.

        6. citation::= ".See" URL EOLN.

          A remote definition is a useful way to define a term by quote the definition of the same (or other) term in another documentation:

        7. remote_definition::= term_defined ":" ":" optional_type = URL.

        8. URL::=Uniform Resource Locator, A URL specifies a protocol, a host and further information identifying a resource on the World Wide Web.

        9. For s:Syntax, re_used(s)::= s #( (substitution | quantification)| "." projection | deletion ).
        10. reused_documentation::=re_used(name_of_documentation).

          Simple changes

        11. substitution::="(" L( term "=>" expression ) ")". -- All substitutions in the list are done simultaneously.
        12. quantification::="(" "for some" L(term ) ")".
        13. projection::= "." P(term).
        14. deletion::= "without" P(label).

          Examples of Substitution and Hiding

          Note. Below '=' is short for 'equivalent'.
           ABC2::=	Net{a:A, b:B(a),  c:=C(a,b), P(a,b,c)}, where C:A>< |B >->T.
           ABC2				=	Net{a:A, b:B(a),  c:T, c=C(a,b), P(a,b,c)}.
           ABC2(a=>x, b=>y, c=>z)		=	Net{x:A, y:B(x),  z:=C(x,y), P(x,y,z)}.
           If x in A, and y and a and y+a in B(x) then
           ABC2(a=>x, b=>y+a, c=>z)		=	ABC2(b=>y+a, a=>x, c=>z)
                                        		=	Net{x:A,   z:=C(x,y+a), P(x,y+a,z)}.
           ABC2(a=>x, c=>b)(for some b)	=	Net{x:A,  for some b:B(x)(b=C(x,b) and P(x,b,b))}.
           ABC2(a=>1,b=>2)(c=>z)	=	Net{z:=C(1,2), P(1,2,C(1,2))}.
           ABC2(a=>1,b=>2)(c=>z).z		=	z::=C(1,2). P(1,2,C(1,2))

          Example of unusual Substitution

           ABC2(a=>2, b=>3, c=>1)		=	Net{2 in A, 3 in B(2),  1 in T, 1=C(2,3), P(1,2,3)}.

          Example of deletion

           ABC3		=	Net{x:A, y:B(x),  (L): P(x,y)}.
           ABC3 without L	=	Net{x:A, y:B(x) }.

          A modification can be any sequence of operations:

        15. name_of_documentation operation operation ...


           R::=Net{ a:X, b:Y, W1(a,b)},  S::=Net{c:Y, d:Z, W2(c,d)}
          Formula Expansion
           (R(b=>u) and S(c=>u)).(a,d)	a::X, d::Z, for some u:Y ( W1(a,u) and W2(u,d) )

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



          Let X,Y, and Z be valid sets of documentation. Let Z be made by putting one or more copies of X's name into Y as an elementary pieces of formal documentation,
           	variables(Z) = variables(Y) | variables(X),
           	declarations(Z) = declarations(Y) | { (v,T1):declarations(X) || for no T2 ((v,T2):declarations(Y))},
           	definitions(Z) = definitions(Y) | { (t,T,e1):definitions(X) || for no e2 ((t,T,e2):definitions(Y))},
           	assertions(Z) = assertions(Y) | hide(variables(Y) & variables(X)) o substitute({ (t,T,e1):definitions(X)
           		| for some e2 ((t,T,e2):definitions(Y))})( assertions(X)),
        1. For V:@variables(X),a:assertion, hide(V)(a):assertion, hide({})(a)=(a),
        2. For v:variable, V:@variables(X),a:assertion, hide({v}|V)(a)=for some v:types(v,X)(hide(V)(a)),

        3. For D:@definitions(X), substitute(V)(a):assertion, substitute({})(a)=(a),
        4. For d:definitions(X), D:@definitions(X),a:assertion, substitute({(t,T,e)}|V)(a)=for t:T=e(v,X)(substitute(D)(a))

          Note that multiple (or even circular) re-use generates only one copy of definitions, assertions, etc..


          The normal modification is substituting a free variable for a defined term or declared variable(parameter). This a straight forward, almost syntactic operation.
        5. AB::=Net{ a:A, b:B=f(a) }.
        6. AB(x,y) = Net{ x:A, y:B=f(x)},

          When a general expression is substituted then some more complex things occur. So if a predefined term replaces a parameter it can not be redeclared. Instead the declaration becomes a constraint added to the term:

        7. AB(1,2) = Net{ 1 in A, 2 inB, 2=f(1)}.

          In other words when a globally defined expression replaces a term then the effect is to replace declarations by assertions. Further if these are already true they can be omitted. For example consider:

        8. EX::=AB(A=>Nat, B=>Nat, f=>++).
        9. =following,
          1. a:Nat.
          2. b:Nat= a+1.

          (End of Net)

          and so
        10. EX(1,2) = Net{ 1 in Nat, 2 in Nat, 2=1+1 } = Net{true}.

          Thus we can claim a theorem:

        11. (above)|-EX(1,2).

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

      . . . . . . . . . ( end of section Formal description of Reuse) <<Contents | End>>

      Combining named documentation

        Operations are shown as modifications to the names of pieces of documentation, but NOT on the named documents themselves. Referring to a piece of documentation with a modification does not change the original - the original is used as a basis for the new, inserted documentation.

        The simplest operation is to just add more elementary pieces of documentation to what already exists. This done by the 'and' operator.

        Boolean operations ({ not, and, or, if.then., iff...}) are used to combine pieces of documentation.


        The with operator is an abbreviation for combining a network with a simple list of declarations and axioms P:
      1. N with P::= N and Net{P}.


        The formal definition of the result of negating a name describes a structure:
      2. For X : name of pieces of documentation, declarations(not X ) = declarations(X) and definitions( not X ) = definitions(X) and assertions(not X) = not constraint(X)

        Example of negation

         Formula		Expansion
         not ABC2	a::A,
         		not P(a,b,c)

        Boolean combinations

        When two pieces of documentation are combined, common variables and terms must have compatible declarations or definitions. The formal definition of the result of a boolean operation between two named is:

      3. For X : name of piece of documentation, Y an elementary piece or another name, *:{and,or,iff,if__then__},
      4. declarations(X * Y) = declarations(X) | declarations(Y) and definitions(X * Y) = definitions(X) | definitions(Y) and assertions(X * Y) ={ constraint(X) * constraint(Y)}.

        The result will not be valid if X and Y give two different definitions to a term in a single context, or two different declarations to a variable. Sometimes one piece of documentation declares a variable that is defined as a term in the other piece. This is OK, as long as the type of the definition is that of the declaration.

        Example of Boolean Operations

         AB::=Net{ a:A, b:B},  XY::=Net{ x:A, y:B}.
         Formula		        Expansion
         AX and XY	        a,x:A, b,y:B
         AB and Net{x:X}       a:A, x:X, b:B(a), c:=C(a,b),  P(a,b,c)
         ABC2 or a=b	        a:A, b:B(a), c:=C(a,b), P(a,b,c) or a=b
         if ABC2 then a=c	        a:A, b:B(a), c:=C(a,b), if P(a,b,c) then a=c

      . . . . . . . . . ( end of section Modifying named documentation) <<Contents | End>>

      Noting and defining

      Section headings give a name to part of a document and also includes it as part of the document. A definition attaches a name to be bound to a piece of documentation but without the content being inserted in the document. To name a piece of documentation for future use,
       	Name "::=" cross_reference.
      Later the name can be used or modified and inserted.


         Net{a:A. ALEPH:=ABC2(x,y,z). aleph:=$ ALEPH(x=a). }
         		Net{	a:A.
         			aleph::=$ Net{ y:B(a), z:=C(a,y), P(a,y,z) }.

      Another variation is to import a copy of the definition of a named piece of documentation into another piece of documentation:

       .As_is 	Use N
       	With N
      inserts the original
       	N::=Net{... x:X. ...}.
      Thus the effect is like 'with' in Ada: Terms defined in N's documentation can only be referred to by qualifying by the name N by their name:

      Example of Use/With

         Net{ a:X. Use ABC2. Y(ABC2.a, a)}
         			ABC2::=Net{ a:A, b:B(a), c:=C(a,b), P(a,b,c) }.
         			Y(ABC2.a, a)

      Parametric or Generic Documentation

      In MATHS we create documentation with declared terms so that it can be used for similar purposes by substituting and/or hiding the them.

      Example of Generic Documentation

         	   This defines a generalized pre/post/infix expression.
               b::=basis::@#char, -- a parameter
               e::=expression::= b | p "." f | f p | b #(f b),
               p::=parameter_pack::= b | left b #(separator b) right.
         For all x,y,z:@#char,SERIAL(x,y,z) ::=SERIAL(b=>x, f=>y, e=>z, for some p).


         	SERIAL(b=>primary,f=>(times|divide),e=>term,for some p),
         	SERIAL(b=>expression,f=>(plus|minus),e=>primary,for some p).

        Or even

         	term:=SERIAL(b=>primary,f=>(times|divide), for some p).e
         	primary::=SERIAL(b=>expression,f=>(plus|minus),for some p).e

      Formulae defined as documentation

      MATHS lets the writer define an expression whose meaning is a piece of documentation, once certain substitutions are carried out:
       	"For" declare_arguments "," model_expression "::=" "Net{" documentation "}"
      An example,
    18. For A,B:variable, Either A or B::=Net{ A,B:@. A iff not B.},
    19. For A,B,C:variable, Either A, B, or C::=Net{ A,B,C:@. if A then not B and not C else Either B or C.}.

      Quantified Documentation.

      If N is the name of documentation s, n::= |declarations(s)| and d is a list of all declarations(s) in some order and Q a list of n quantifiers, and v is the list of variables in d (in the same order) and X is declared to be of type @N then

      @{N ||for (Q1 v1, Q2 v2, Q3 v3,...,Q[n] v[n])}::= {X:@$ N|| for Q1 d1, Q2 d2, ..., Q[n] d[n] ( constraint(s)) }.

      Notice that X:@$ N, so X satisfies the constraints of N.

      (for Q1 v1, Q2 v2, Q3 v3,...,Q[n] v[n](N)) ::= for Q1 d1, Q2 d2, ..., Q[n] d[n] ( constraint(s)).

      Notice that this is meaningless whenever there are no constraints defined in N.

    20. For X:@$ D then (for Q1 v1, Q2 v2, ...(X)) ::= Q1 d1, Q2 d2,...($(N) in X).

      A useful abbreviation is to use the name of the documentation rather than listing all the remaining variables.

      (for Q1 v1, Q2 v2,...Q[p] v[p], Q[q] N) ::= for Q1 d1, Q2 d2, ..., Q[p] d[p], Q[q] d[p+1],..., Q[q] d[n](N).


      A dynamic proposition is any proposition with a primed variable in it. The primed variables are said to be dynamic variables, and the remainder static. Such predicates a not completely specified until the types of the variables are specified. A piece of documentation that declares the variables and includes a dynamic predicate describes a change of state. The space of states is defined by the declarations. Additional static propositions state any invariants that are maintained. A prime is used only in wffs, and not used in declarations because a primed variable is implicitly declared as being the same type as the unprimed version.

      There follows a summary, for more details see: [ math_14_Dynamics,html ]

      A dynamic proposition in a piece of documentation means that the '$' operator forms a set of pairs or binary relation rather than a set of single states. For example, if

       	X::=Net{ a:A, W1(a) },
       	Y::=Net{ a:A, W2(a, a')}
      	$ X={a:A || W1(a) }
      and has type @A but
      	$ Y=rel[a,a':A](W2(a,a') )
      and has type @(A,A).

      If 'D2' is a piece of documentation with one or more dynamic variables in it then

      $ D2=rel[ declarations(D2), primed(declarations(D2)] (constraint(D2) and static variable do not change)

      The declarations(D2) are list of the declarations of D2.The primed(declarations(D2) are declarations of D2 with a prime added to each variable. So (unlike Z) the primed variables are implicitly in the same state space as the unprimed variables.

      Consider a piece of documentation D1 with no dynamic propositions in it and documentation

      	D2 ::=Net{D1, W(x1',x2',x3',...,x1,x2,x3,...)}
      		where x1,... in variables(D1).
      	assertions(D2)=assertions(D1)|{`W(x1',...,x1, ...)`}

      Let z=(z1,z2,...)=variables(D)~{x1,x2,x3,...} then in D2

       (1) A duplicate set of `x`s are implicitly added to D1's variables.
       	variables(D2) =variables(D) | {x1,...} | {x1',...}  | {z1',...}
       (2) The relation is constrained by the requirement that static variables do not change.
       	constraint(D2) = constraint(D1) and z1'=z1 and z2'=z2 and ...

      The Z idiom of defining the state space separately is also used in MATHS. Here is an example from recreational mathematics:

    21. HAILSTONE::=following.

      1. State::=Net{ n: Nat },
      2. Op1::=Net{ State, 2*n'=3*n+1},
      3. Op2::=Net{ State, 2*n'=n},
      4. End::=Net{ State, n=1}.
      5. Delta::= Op1 or Op2.
      6. (above)|-pre($ Delta) = pre ($ Op1) | pre ($ Op2) =State.
      7. (above)|-no pre($ Op1) & pre ($ Op2).
      8. (above)|-State >== {pre($ Op1) , pre($ Op2)},
      9. (above)|-$ End.$ Op1.$ Op2=$ End.
      10. ??{ Nat. do($ Delta) = $ End. }??
      11. Loop::=Net{State, n'=n}.
      12. ??{ For all n0, if $ Net{State, n=n0}==>$ Net{State, n=n0}. do($ Op1 | $ Op2) then n0 in {1,2}. }??

      (End of Net)


      There is a suitable theory of the MATHS re_use in [Wirsing90].

    . . . . . . . . . ( end of section Re-use & Inheritance) <<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


  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.