Introduction

Named Documentation is a powerful kind of macro: A name is attached to a collection of declarations, definitions, assertions, and commentary. This name then becomes available for use in other pieces of documentation. This makes the MATHS system much easier to use. The goal is to allow previous work to be re-used rather than re-invented. This includes linking to pre-existing documents on the Internet and reffereing to published books and papers.

In MATHS, declarations, assumptions, theorems etc are imported into a new piece of documentation by refering to the name of the documentation in which they are originally declared. As a matter of style, all exportable names must be spelt out as a natural name. This makes it easier to use documentation. It is simple to include abreviated names when developing the documentation. Ideally a defined name should be linked to all its occurences either by storing a hypertext reference (as in HTML) or by a dynamic search of the documentation for the definition.

Sometimes it is useful to both name a set of documentation and also include it in the current document. This is done by quoting the name and also giving a definition. The order is not important. This leaves the name bound to a piece of the document in which it is defined. It is less confusing to separate the packaging of a set of peices from their definition when this is feasible. An example is Maths.11 STANDARD. Similarly the definition of a structure by a pieceof documentation is separated from any statement of the properties of the set of objects that satisfy it - for example whether they exist or not.

.Precedent The inspiration for the naming and re-using formal documentation comes from the Z language. MATHS goes further than Z: (1) all documentation is modeled as a set of elements and (2) there are rules for naming and combining documentation, (3) The syntax is designed to be used on any ASCII system, (4) The syntax is much less restricted.

Syntax

1. Named_piece_of_documentation::=document | section | Named_paragraph | definition | labeled_formula.

   A named piece of documentation has a name. A complete name would follow the URL syntax and so looks like

2. element_identifier(piece_specification)[author date_of_last_modification]

    		.See protocol://system/path/file#section,

   [ URL in comp.html.syntax ] or

    		part(piece)[reference_to_printed_document]

3. full_name::=l_bracket piece_specification O(l_parenthesis element_identifier r_parenthesis ) r_bracket.

4. reference_to_printed_document::= l_bracket short_citation comma chapter_number #(dot section_header) dot paragraph_identifier l_parenthesis element_identifier r_parenthesis r_bracket.

5. short_citation::=Author_abreviation Year O(letter). In any the document the set of short citations in references to printed documents should be a subset of the set of short citations in the long citations in the same document. The long citation, or "Source" directive providing enough information to obtain a copy. Notice that in non-linear documents or hypertext citations like "ibid." and "op cit." are likely to make sense to all readers and so should not be used. Perhaps they could be pre-processed out of a text when it is entered into the system.

6. long_citation::=".Source " short_citation comma author_s_full_names comma title comma ( periodical_citation | book_publisher date ).

7. piece_specification::=O(#(dot section_header) O(dot paragraph_name)).

8. element_identifier::= #( defined_term dot) (defined_term | label ).

   An operating system can handle the association between complete document and its name. Implicit in MATHS is the concept of internet cross-refferences - reffering to work by others on a different machine - possibly a different country even. Math formatting, definitions, and formaula labels are designed to work internally. A special format documents the linking of documents and allows the names used in the original piece of documentation to be used in the document that "See"s it.:

9. X_ref::=".See" URL | ".Used"("_in" | "_by") URL.

   Defining a piece of documentation

   A simple way to name a small set of documentation is write a definition that assigns a name to a structured set of elements: Examples

   ---

   2. CIRCLE::=Net{r:Real & Positive, x:Real, y:Real, x^2+y^2=r},

   3. unit_circles::=CIRCLE(r=>1).

   ---

   Long definitions are also useful:

    	Name::=following

    	.Box

    		documentation

    	.Close.Box

    	Name::=following

    	.Let

    		documentation

    	.Close.Let

    	Name::=following

    	.Net

    		documentation

    	.Close.Net

10. The older form was like this

     	Name::=Net{

     		documentation

     	}=::Name.

     	Name::=OldName with following

     	.Net

     		documentation

     	.Close.Net

11. The older form was like this

     	Name::=OldName with {documentation}

    As a rule, a small set of documentation is no longer than the maximum length of line that can be handled in popular software tools. This effectively means that a definition that needs more than 255 characters must be split accross several lines and should be written in the long form. Email standards require no more than 78 characters per line.

    Documentation is work in progress. Automatic cross-refferencing is needed so that changing the named documentation alerts and/or protects the person who has used it. It is an important function to allow the viewer and author of documentation to either see the name of the documentation with or without the documentation it refers to, as they wish, quickly and easily - a one touch toggle should open and close the documentation. Similarly a "button" or hypertext link is essential to allow quick cross refferal to other pieces of text. Crossreferences, indexes, searches, etc are helpful as well. However - automatic links can only be given for local defined terms - not for parts of terms. When there is a formal refference to another document then these (ideally) should be treated as part of the document as well.

    The terms and variables introduced in a named piece of documentation, can appear as-is inside the documentation. The name of the documentation is used to export the terms, variables and constraints into other pieces of documentation.

    [ notn_13_Docn_Syntax.html ]

    Using named documentation to describe sets and objects

    Named documentation is useful for defining sets, maps and relations.

    For declarations and definitions D, Net{D}::=Class of objects described by D, Net{D. W(v)}::= set v:Net{D} satisfying W(v), Net{D. W(v',v)}::=relation v,v':Net{D} satisfying W(v',v).

    For N=Net{D}, where D:documentation,

12. $(N)::=tpl (a=>a,...) of variables in N, Type(N)::=Type of $(N), N::=Class of $(N) that fit N.

    For N:proposition(elementary_piece_of_formal_documentation), N::=Class of $(N) that fit N.

    For N=Net{D}:documentation,

13. @N::=subsets of N,
14. %N::=lists of objects that fit N,
15. #N::=strings of objects that fit N,
16. N(x=>a, y=>b,...)::=substitute in N,
17. N(for some x,...)::=hide x.. in N,
18. N.(x,y,z,...)::=hide all but x,y,z,...`.

    For N=Net{D}:documentation,

19. the N(W)::= the (N and W),
20. the N(x=>a,y=>b,...)::= the N(x=a,y=b)::=the(N and (x=a and y=b and ...)),
21. the N(a,b,c,...)::=the N(v1=>a, v2=>b,v3=>c,...).

22. For S:@N, the S(W)::=the{$(N):N || $(N) in S and W},...

    [ notn_13_Docn_Syntax.html ]

    Example 1

23. X::=ABC.
    
24. |-X = { (a=>v[1], b=>v[2], c=>v[3]) || v: A><B><C},
    
25. |-a=map[x](x.a) in A^X,
    
26. |-b=map[x](x.b) in B^X,
    
27. |-c=map[x](x.c) in C^X,
    
28. |-|X|=|A|*|B|*|C|,
    
29. |-|{x:X || x.b=b}| = |A|*|C|,
    
30. |-for all (a,b,c):A><B><C, one x:X(x.b=a & x.c=c & a.b=b},
    
31. |-for all x1,x2:X( x1=x2 iff x1.b=x2.b & x1.c=x2.c & x1.d=x2.d)

    Example 2

    [ ABC2 ]
    
32. |-u:ABC2= u:ABC2.
    
33. |-ABC2={u || for some u.a:A, u.b:B(u.a) ( P(u.a, u.b, C(u.a,u.b)))}.
    
34. |-$(ABC2)= (a=>a, b=>b).
    
35. |-ABC2= {$(ABC2)||constraint(ABC2)}.
    
36. |-For all ABC2( Q(a,b,c) )
37. =For all u:example(Q(u.a,u.b,C(u.a,u.b))
38. = For all u.a:A, u.b:B(u.a), if P(u.a, u.b, C(u.a,u.b) then Q(u.a,u.b,C(u.a,u.b)

    How to re-use nets

    The ".See", ".Uses" and ".Source" directive indicate connections between paarts of documents. The ".See" directive effectively including pieces of other documents in side the current one. These may contain Nets of variables and assertions. The named nets in a document (or included in it) are reused by as follows:

    For D1, D2, N=Net{D}, quantifier Q,

39. Net{D1. N. D2}=Net{D1. D. D2},
40. With N::=Clone the definition N::=Net{D},
41. Uses N::=Clone a copy of N's defintion and its contents D,
    Note. Uses N is like With N. N. (N)|-(l):T ::=Derivation of theoremT labelled l from axioms in N (N)|-d ::=Quotation of definition, assertion, or other element d from N
42. For Q N::=Assert N is for cases quantified by Q
43. for Q N(wff)::=for Q x:N (wff where x:=$(N)).

    Given a general definition of N as an expression E then

44. definition(N)::= N::=E.

    Operations on Nets

    Given one or more names of nets we can indicate nets that can be constructed from them by formula that look like the boolean operations, the arrow operator, and quantification.

45. For N1, N2:documentation, o:{and,or,...} N1 o N2 ::documentation=combine N1 with N2 using o.
46. For N1:documentation, not N1::documentation= complementary documentation to N1.
47. For N1, N2:documentation, N1^N2::=maps from type(N2) to type(N1),
48. For N1, N2, N1->N2::=relations @Net{N1,N2} that define a map from N1 to N2. Note. Net{a,b:X}->Net{c,d:Y} in Net{a,b::X,c,d::Y} and not in @(Net{a,b::X}><Net{c,d::Y})
49. For N1, N2:documentation, Q1,Q2:quantifiers, (N1(Q1)-(Q2)N1) ::= N1(Q1)-(Q2)N2,
50. For N:documentation, Q:%quantifiers, v:signature(N), @{N || for Q1 v1, ...}::=Sets in @N satisfying the Qs,.

    There is also a short hand form that is useful for working out the static images of objects as a normalized data base: [ math_13_Data_Bases.html ]

    Extension

51. For N1:documentation, w:wff, N1 and w::documentation=N with added axiom w.
52. For D1,D2:documentation, N1:=Net{D1}, N1 with{D2} ::= Net { D1. D2}.

    Formal model

    [ notn_4_Re-use.html ]

. . . . . . . . . ( end of section Named Documentation) <<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