- Named Documentation
- : Introduction
- : Syntax
- : Defining a piece of documentation
- : Using named documentation to describe sets and objects
- : Example 1
- : Example 2
- : How to re-use nets
- : Operations on Nets
- : Extension
- : Formal model
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS
- Glossary

- 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

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

A definition can be imported into a document. For example the page [ comp.html.syntax.html ] defines the syntax for a uniform resource locator or URL. I can add this definition to this document by writing

URL::=http://www/dick/samples/comp.html.syntax.html#URL

- URL::= See http://cse.csusb.edu/dick/samples/comp.html.syntax.html#URL
These names can refer to complex pieces of documentation with many variables, axioms, and even theorems. Ideally these should be rendered so that one click/touch taks you from the reference to the definition.

Names defined or labels placed in a document can be refered to like this

$name

or.See name

However these follow the normal (static) scope rules of a high level programming language -- a label inside a proof may refer to a result that depends on an assumption and so can not used outside the proof. Further in a proof forward references to labels and defintions later in the proof should not be used -- this leads to paradoxes.These names can also be used as evidence in steps in an argument:

(..., name, ...) |- (result) : proposition.

For example - (Einstein35)|-E = M c**2.
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.

References to printed documents. Inside a document the "name" syntax can be used. The clasic form is a short_citation below.

- short_citation::=Author_abreviation Year O(letter).
These short_citations should be defined in a list of references, authorities or bibliography at the end of the document. These reference may take the form:

- reference_to_printed_document::= (short_citation) #author title date chapter_number #(dot section_header) dot paragraph_identifier l_parenthesis element_identifier r_parenthesis.
The long citation is an informal description but must provide enough information to obtain a copy.

A standard format for a bibliography has evolved:

.Open short_citation

Authors

Where found

=TYPE TAGS

Notes...

.Close

When such a bibliography exists for a site, this format

.See [short_citation]

indicates a reference to the item in the bibliography... and is rendered as a script to extract the entry. Similarly.Lookup string

can be used to refer informally to a collection of pieces of documents whose name contains the string. Notice that this includes headlines, theorems, and definitions.The older notation for hard copy refereences

.Source [citation]

is depecated. Lately the ".Source" directive has being used to indicate who submitted a piece of a document. It applies to the previous piece of documentation:.Source RJBotting

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

- The older form was like this
Name::=Net{

documentation

}=::Name.

Name::=OldName with following

.Net

documentation

.Close.Net

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

## 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},...
## 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

[ 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 of N,
- Uses N::=Clone a copy of N's definition 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: [ 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

[ notn_4_Re_Use.html ]

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.

(Close But )

. . . . . . . . . ( end of section Named Documentation) <<Contents | End>>

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 ]

For a more rigorous description of the standard notations see