.Open Named Documentation

. 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
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
	element_identifier(piece_specification)[author date_of_last_modification]
.As_is 		.See protocol://system/path/file#section,
.See http://www/dick/samples/comp.html.syntax.html#URL
or
.As_is 		part(piece)[reference_to_printed_document]

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

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.

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

long_citation::=".Source " short_citation comma author_s_full_names comma title comma ( periodical_citation | book_publisher date ).
.But
A different notation evolved in the MATHS bibliography of Software Development.
.As_is .Open short_citation
.As_is  Authors
.As_is  Where found
.As_is  =TYPE TAGS
.As_is  Notes...
.As_is .Close

Informally the ".Source" directive is being used to indicate who submitted a piece of
a document.  It applies to the previous piece of documentation:
.As_is 	.Source RJBotting
.Close.But

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

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.:
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:
.Box Examples
CIRCLE::=Net{r:Real & Positive, x:Real, y:Real, x^2+y^2=r},

unit_circles::=$CIRCLE(r=>1).
.Close.Box
Long definitions are also useful:
.As_is 	Name::=following
.As_is 	.Box
.As_is 		documentation
.As_is 	.Close.Box

.As_is 	Name::=following
.As_is 	.Let
.As_is 		documentation
.As_is 	.Close.Let

.As_is 	Name::=following
.As_is 	.Net
.As_is 		documentation
.As_is 	.Close.Net
 The older form was like this
.As_is 	Name::=Net{
.As_is 		documentation
.As_is 	}=::Name.

.As_is 	Name::=OldName with following
.As_is 	.Net
.As_is 		documentation
.As_is 	.Close.Net
 The older form was like this
.As_is 	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.

.See http://www.csci.csusb.edu/dick/maths/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,
  $(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,
  @N::=`subsets of $N`,
  %N::=`lists of objects that fit N`,
  #N::=`strings of objects that fit N`,
  N(x=>a, y=>b,...) ::=`substitute in N`,
  N(for some x,...) ::=`hide x.. in N`,
  N.(x,y,z,...) ::=hide all but x,y,z,...`.

For N=Net{D}:documentation,
  the N(W) ::= the ($N and W),
  the N(x=>a,y=>b,...) ::=  the N(x=a,y=b)::=the($N and (x=a and y=b and ...)),
  the N(a,b,c,...) ::=the N(v1=>a, v2=>b,v3=>c,...).

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

.See http://www.csci.csusb.edu/dick/maths/notn_13_Docn_Syntax.html

. Example 1
X::=$ABC.
|- X = { (a=>v[1], b=>v[2], c=>v[3]) || v: A><B><C},
|- a=map[x](x.a) in A^X,
|- b=map[x](x.b) in B^X,
|- c=map[x](x.c) in C^X,
|- |X|=|A|*|B|*|C|,
|-  |{x:X || x.b=b}| = |A|*|C|,
|- for all (a,b,c):A><B><C, one x:X(x.b=a & x.c=c & a.b=b},
|- for all x1,x2:X( x1=x2 iff x1.b=x2.b & x1.c=x2.c & x1.d=x2.d)


. Example 2
.See ABC2
	|- `u:ABC2`=	`u:$ABC2`.
	|- $ABC2={u || for some u.a:A, u.b:B(u.a) ( P(u.a, u.b, C(u.a,u.b)))}.
	|-$(ABC2)=	(a=>a, b=>b).
	|- $ABC2=	{$(ABC2)||constraint(ABC2)}.
	|- For all ABC2( Q(a,b,c) )
		=For all u:example(Q(u.a,u.b,C(u.a,u.b))
		= 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,
   Net{D1. N. D2}=Net{D1.  D.  D2},
   With N::=`Clone the definition N::=Net{D}`,
   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`
  For Q N::=`Assert N is for cases quantified by Q `
  for Q N(wff) ::=for Q x:$N (wff where x:=$(N)).

Given a general definition of N as an expression E then
	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.

 For N1, N2:documentation,  o:{and,or,...} N1 o N2 ::documentation=`combine N1 with N2 using o`.
 For N1:documentation,  not N1::documentation= `complementary documentation to N1`.
 For N1, N2:documentation,  N1^N2::=`maps from type(N2) to type(N1)`,
 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})
 For N1, N2:documentation, Q1,Q2:quantifiers, (N1(Q1)-(Q2)N1) ::= $N1(Q1)-(Q2)$N2,
 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:
.See http://www/dick/maths/math_13_Data_Bases.html
. Extension
 For N1:documentation, w:wff,  N1 and w::documentation=`N with added axiom w`.
 For D1,D2:documentation, N1:=Net{D1}, N1 with{D2} ::= Net { D1. D2}.
. Formal model
.See http://www.csci.csusb.edu/dick/maths/notn_4_Re-use.html

.Close Named Documentation