Named Documentation

Introduction

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

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.
[ 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},...
[ 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
[ 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 ]

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

STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

Glossary

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

given::reason="I've been told that...", used to describe a problem.

given::variable="I'll be given a value or object like this...", used to describe a problem.

goal::theorem="The result I'm trying to prove right now".

goal::variable="The value or object I'm trying to find or construct".

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.

hyp::reason="I assumed this in my last Let/Case/Po/...".

QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.

QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.

RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.