Documentation in MATHS

Introduction

This document describes the elementary pieces of documentation.

Philosophy

The idea that philosophical statements have an (elegant) structure independently of whether they refer to anything real or not goes back to at least Sir Francis Bacon's New Organum:

[...] These I call Idols of the Theatre, because in my judgment all received systems are but so many stage plays, representing worlds of their own creation after an unreal & scenic fashion. Nor is it only of the systems now in vogue or only of the ancient sects and philosophies that I speak, for many more plays of same kind may yet be composed and in like artificial manner set forth [...]

A test of good documentation is its validity. This term is defined later - See [ notn_14_Docn_Semantics.html ] elsewhere.

However a piece of documentation can be part of a formula that can be true or false. It can also imply that a formula has a particular value. It can also be matched up as a model of a data or observations. See Notation.15 Using Documentation and Notation.8 Evidence and Notation.9 Structure.

Two special kinds of document occur often. A simple piece of documentation has variables (parameters) but no definitions or axioms (and so no theorems). A basic piece of documentation has no theorems or definitions. A simple piece of documentation defines an unconstrained or universal set. A basic piece of document has the property that it is easy to predict the effect of removing an axiom.

Syntax

GRAMMAR::= See http://cse.csusb.edu/dick/maths/math_65_Meta_Linguistics.mth#GRAMMAR
expression::= See http://cse.csusb.edu/dick/maths/notn_12_Expressions.html#expression
structure::= See http://cse.csusb.edu/dick/maths/notn_2_Structure.html
A MATHS document has many pieces,
document::= #piece_of_documentation.
Some pieces are sections (see structure) and other are elementary:
piece_of_documentation::= section | elementary_documentation.
elementary_documentation::=#(formal | break | directive | gloss | (label| ) comment ).
This is one of the few areas where layout is important in MATHS. All formal parts have simple, recognizable patterns. Definitions and declarations have two adjacent colons, formulas are either labeled, indented or have an "|-" in front of them.
formal::=formula | formal_definition | declaration | assertion.
definition::=formal_definition | gloss.

formal_definition::=(for_clause (condition | ) | )term"::"(context | )"="expression ender,

 		pi ::real= 3.14159.

 		paragraph_tag ::= "<p>".

 		cos ::trig_function= sqrt(1-(sin)^2).

declaration::= (for_clause (condition | ) | )term"::"context.

Here are some example forms.

  For v1:T1, v2:T2, A.		Abbreviation for		For (v1,v2):T1><T2, A

  For v:T, A,B,C.		Abbreviation for		For v:T, A.  For v:T, B.  For v:T, C.

  For v:T, W(v).		Universal proposition	for all v:T ( W(v) ).

  For v:T, t::=e.		Definition of term		For v:T, e::`type of e`, For v:T, t=e.

  For v:T, e::S.		Type inference - the type of expression e is S whenever v is  of type T

  For T:Types, v:T, e::S.	Generic type inference, S will have T in it and e will have v

.Road_works_ahead

Let{
Conditional documentation
1. elementary_piece_of_documentation::= ... | conditional_declaration.
2. conditional_declaration::= "If" expression(@)"," List(declaration) ".".
  Conditional assertions are wffs anyway!
  If a piece of documentation D contains the following conditional documentation:
```
 		If E then L.
```
  and L contains a declaration
```
 		v:T
```
  1. In $ D, v is a partial map from $ D<>->T. The pre-image pre(v)={x:D. E}.
  2. In proofs and arguments the condition E must be established before the variables declared in L can be used.
  3. In reusing D, the condition E should be established before variable v is used.
  4. Notice that using v can not automatically assert E because there can be other conditional definitions with other conditions that declare v.
  5. Do not use conditional documentation to describe special cases, define a boolean:
```
 		Abelian::=for all x,y(x+y=y+x).
```
  Hence conditional_definition
```
 		If E then V::T=e.
```
  Hence the form
```
 		If E then N.
```
  where N is the name of of another piece of documentation.
  Also
```
 		If E then either a or b.
```
  which introduces to mutually exclusive boolean variables a:@ and b:@.
. . . . . . . . . ( end of section Conditional documentation) <<Contents | End>>
}

Comments

comment::= sentence #(period sentence).
sentence::=item #(comma item).
item::=(#piece_of_comment)~piece_of_formal_documentation,
piece_of_comment::=l_bracket reference r_bracket | term | variable | lexeme~(l_bracket| r_bracket| term | variable | gloss ),
In an ideal typesetting system the occurrences of variables and terms inside commentary text will be automatically typeset in italics. For example in English comments it is only necessary to mark the words "a" and "I" as variables, all other words of form (letter #digit #prime) is a clearly a mathematical variable.

Glosses
A gloss provides useful clues as to the meaning of a term without giving a formal definition of the term. The only difference between a formal definition and the less formal or informal gloss is that a gloss can link a term to any balanced text -- one with balance open and close brackets and with no unbracketed commas or periods.
gloss::= term ":" ":"(context | )"=" (balanced ~ expression) ender.
```
 		pi ::real= ratio of circumference divided by radius.
```
balanced::= See http://www.csci.csusb.edu/dick/maths/notn_12_Expressions.html#balanced.
ender::= "." | ",".

References
A reference is a dollar sign followed by an identifier.
reference::= "$" identifier. In MATHS document references are usually pointers to a list of references and citations at the end of the document. The pointer usually consists of the family name of the author and the last two digits in the year, and an optional letter
```
 	$Botting89
```
A reference to an electronic document is via its URL. As a rule the removal of all references should result in no change of meaning.
Commonly references to hardcopy are listed at the end of the document in a special format like this
```
 	(identifier): authors, title, source.
```
References to URLs can be written as definitions of using this format:
```
 	(identifier): tag
```
```
 	.See URL
```
This notation
```
 .See [identifier]
```
should link to a sitewide bibliography.
deprecated notation.
Net
(End of Net)
Declarations
Declarations introduce a new variable. Unlike a variable in a program however it has a fixed, but unknown, value. In fact all declared variables act more like parameters in a generic piece of code than program variables. A variable can be replaced by an expression of the same type throughout its scope and if the expression satisfies the resulting assumptions then a new and correct document is produced.
declaration::= declared_term #(comma declared_term) ":" ":" set_expression | optional_shorthand declared_term colon set_expression,
A declaration, say t::S, means that t is a member of S. Each set determines the type of its elements, so if S is of type @T then t is of type T - but with an unspecified value. In essence, t is declared to be of type T and the axiom t ∈ S is simultaneously asserted.
Multiple declarations - notice that it is legal for the same identifier t to appear in more than one declaration. Suppose that a piece of documentation has both t::S1 and t::S2 in it. First, when S1 and S2 have differing types T1 and T2 respectively then t is a polymorphic identifier with disambiguated forms t.T1 and 't.T2`. Second when S1 and S2 have the the same type of element(T say), then the effect is of a single declaration of type t::T plus the two axioms: `t ∈ S1 and t ∈ S2`. So in this case it as if there is the single declaration: t::S1 & S2.
It might seem simpler to disallow multiple declarations, but the question comes up the moment we allow the reuse of documentation with declared variables. Rather than complicate the rules for reuse, it seems more basic to resolve the issue as a question of multiple declarations at this level. It is part of the general idea that the parts of a document are conjoined together with a logical and. This helps for handling some context dependent definitions and for interpreting the meaning of so called 'recursive' definitions as simultaneous equations.
For more see [ notn_16_Classification.html ]
Declarations and Definitions
Definitions - t::S=e and t::=e - are in essence, short hand for a declaration ( t::S and t:type(e) respectively) and an axiom t=e. Similarly for parameterized definitions For x, t::S=e which is short for For x, t::S. For x(t=e). and conditional (partial) definitions.
Constrained Declarations
One common way to introduce a new term is to declare it and add enough constraints that it is well defined. This needs care and knowledge of how the type of term works:
```
 	x::Real where 3*x+1 = 2.
```
These are essentially the same as a normal definition. The above can be rewritten:
```
 	x::Real=the{x:real || 3*x+1 =2}.
```
So
```
 		v :: T where P.
```
means
```
 		v::T = the{v:T. P}.
```
Here is a more complex example:
```
 	x::Complex where following
```
Net
1. x^2+3*x-1 =0.
2. Re(x) > 0
(End of Net)
Remote Definitions
There is a specialized but useful notation that quotes and reuses a definition that is given elsewhere on the World Wide Web:
remote_definition::= term_defined ":" ":" optional_type = URL.
This is really a specialized short_definition. A remote_definition like
```
 		t::T=u
```
can be considered an abbreviation for
```
 		t::T= following
```
```
 		.See R
```
Assertions
An assertion is a proposition that is taken to be true throughout a piece of documentation. It should not be taken as true outside this context. Indeed some times the sole purpose of introducing and assertion is to demonstrate that it is inconsistent with the surrounding context and so prove the contrary formula: [ reducto_ad_absurdum in logic_2_Proofs ]
One the other hand the existing evidence can allow to deduce or prove an assertion from what we have already assumed and/or proved. Then we call the result a theorem. Non-theorems are conjectures and axioms. An axiom is a proposition that is assumed to be true without providing any formal justification. In other words it is a premise.
assertion::= axiom | theorem | conjecture.
axiom::= optional_indentation "|" "-" "(" label "):" wff
formula::= indentation optional_label expression. Formulas without the assertion sign are being quoted and are not taken to be true, or to have any value.
indentation::= ASCII.HT #white_space_char. The tab makes a formula easy to spot by both human readers and computer programs. The assertion symbol is used to distinguish various kinds of assertion. Notice that a formula does not have to be well-formed. However, it is hard to reason formally with badly formed formulae. On the other hand early drafts of proofs and proof outlines tend to include informal "formula":
A Miracle Happens.
paragraph_indentation::= ASCII.SP #white_space_char.
A space is used to indicate the beginning of bullet points, paragraphs, items in lists, elements in sets, etc.
white_space_char::=( ASCII.SP| ASCII.HT), spaces and tabs.
ASCII::= See http://cse.csusb.edu/samples/samples/comp.text.ASCII.html.
wff::=well_formed_formula.
theorem::= P(evidence) conclusion ,
conclusion::="|" "-" optional_label derived_wff, -- compare with ISO Standard Z.
derived_wff::=wff & derivation leads to wff, [ Arguments and proofs ]
optional_label::=O ( "(" label "):" ). Putting a label in front of an axiom, definition or theorem allows it to be referred to in comments, as evidence, and when reusing the document that contains it.
Explicitly labeling axioms makes it easier to process MATHS documentation.
If a term t has a definition D then implicitly the definition D is labeled definition(t). If a term t has a definition in context T then the definition is labeled (automatically and implicitly) definition(t:T). The effect is similar to writing a nested definition of the expression and then using the label:
```
	(L): Axiom.
```
is rather like:
```
 			L::=Axiom.
```
```
 		  	L.
```
However... there is no definition(L) here in reality
```
	|-(L): Axiom
```
is rather like:
```
 			L::=Axiom
```
```
 			|-L.
```
Again... there is no definition(L) here in reality,
```
	(premises) |-(L): Theorem.
```
is rather like:
```
 			L::=Theorem.
```
```
 			(premises)|-L.
```
Again... there is no definition(L). Better documentation will have a section named "Proof of L" for most if not all of its theorems. There should be hypertext links between the assertion symbol "|-" and the proof.
conjecture::=optional_label "??{" formula documentation "}??". Also
```
 		.Po $formula
```
```
 		...
```
```
 		.Close.Po
```
Proof
Theorems, by definition require proofs. A theorem labeled l must have a section of documentation called proof of l that is in the form of an argument:
. Proof of l
.Let
|- (l1): Assumption,
(let)|- (l2): Assumption.
...
(reasons)|- (ln): Result
.Close.Let Typically all proofs would be gathered at the end of a piece of documentation.
well_formed_formula::= O(("For"|"for") #(givens comma) givens comma) proposition(@.expression),
givens::= binding | simple_proposition.

Lexicons and Grammars
MATHS is designed to be used in defining the syntax and semantics of formal languages --- for example C++ or XML. A variation of the classic EBNF is used
```
 		word::lexeme, purpose.
```
```
 		word::lexeme=string, purpose.
```
```
 		word::syntax=expression.
```
```
 		word::parsing=expression.
```
```
 		word::semantics=expression.
```
These ideas are used in the formal definition of MATHS itself.
.Road_works_ahead Hopefully it will be possible to extend MATHS by using these notations.

Wffs and propositions
A wff is mapped into a proposition by first replacing "for" by "for all" plus bindings for all free variables in the following propositions. Second a pair of matching parentheses are put round the final proposition. Third, every other simple proposition has "if" is put in front of it, and "then" after it, and the comma deleted. Finally where ever a "then" is followed by a binding then "for all" is inserted between the "then" and the binding. For example, "for x=y+1, y=x-1" becomes "for all x,y, if x=y+1 then (y=x-1)".

Resolving ambiguous labels.
If a wff has label 'l' inside one piece of documentation called N and also another wff has the same label inside document M then outside N N's version can be referred to as N.l and M's as M.l. If two wffs have the same label (commonly something like '*') then the label refers to the first occurrence up to where the second one appears. After that, it refers to the second one. And so on if there are more... Outside that piece of documentation, both labels are invisible - hidden by the ambiguity. A helpful feature would be a system to spot and highlight such attempts to refer to something inside a document which does not have a unique identifier, and help the user resolve the difficulty.

Arguments and proofs
argument::= set_of_documentation &... , [ logic_2_Proofs.html ]
Proof and arguments are a special type of documentation which are essential in any project that involves matters of life and death. In MATHS an argument often proceeds by documenting some assumptions, defining some terms and deriving an assertion that is true in that context. This proves that the assumptions imply the derived conclusions ... thus
```
	Given ".Let" x:S,  P, ... "|- " Q ".Close.Let"
```
```
	Therefore "for all" x:S,  "if" P "then" Q.
```
A useful feature to include in a MATHS environment is to quickly show and hide arguments at the viewer's request.
set_of_documentation::=balanced & ( flag l_brace documentation r_brace).
Flags indicate the part played by the set of documentation - an argument (flagged by ( "Po", "Let" or "Consider,",...), an assertion
(Flagged by "|-"), or a quotation/reference - with no flag. Directives giving Road signs can also be used.
proposition::=following. [ proposition in logic_10_PC_LPC ]
In theory and mathematical research any set of assumptions can be considered, as long as they are interesting or lead to new consequence. In the design of complex systems however some reason should be supplied for assumptions. So some explanation should be given of assertions that are made about real situations. For example some of the following might be used:
1. Experiments designed to falsify this assumption have failed to give reason to doubt it (for instance see....)
2. I have observed that .... , on ... at..., when.....
3. The documentation/data/code found in ...in the current system assumes...
4. On ...date, Mr/Ms J Doe stated that...
5. A sample of N items were taken at random and...
[ notn_8_Evidence.html ]

Definitions
1. context_free_definer::= colon colon equals.
2. contextual_definer::= colon colon context equals.
3. definer::= context_free_definer | contextual_definer.
  Definers and binders are very similar to binders, see [ binding ]
4. formal_definition::= short_definition | long_definition.
  The sole purpose of a long_definition is to give a name to set of documentation. A useful convention is that these names of documentation are natural identifiers made of capital letters. See Conveniences and Re-use.
  A short definition must be short enough for tools (like grep for example) and mailers to handle in a line. There are four typical forms:
  1. syntactic definitions using XBNF.
  2. abbreviations and functions defined be expressions,
  3. structural definitions that state the generic form and extend it by adding structure to it.
  4. Short, schematic definitions that list the declarations, definitions, and axioms of a system as bindings rather than full declarations etc. in schematic form
    In theory the forms are equivalent and can be translated from one to the other. In practice it is more writable and readable to use the long form for complex structure and systems. The short form is best used for quick reference. Ideally a piece of documentation should have both.
    
    Example of definitions
    
    Net
    (End of Net)
  5. short_definition::=optional_shorthand defined_term definer (expression | structure | schematic_form | URL).
  6. |-remote_definition ==> short_definition.
  7. leftb::="{".
  8. rightb::="}".
  9. structure::= generic_form "with" leftb binding_or_axiom #( "," binding_or_axiom) rightb.
  10. schematic_form::= form leftb binding_or_axiom #( "," binding_or_axiom) rightb.
  11. form::= "Net" | "Set" | "Map" | "Rel" | ... .
  12. simple_structure::= simple_generic_form "with" leftb loose_binding #( "," loose_binding) rightb.
  13. simple_generic_form::=a term defined by a simple structure.
  14. binding_or_axiom::= binding | predicate.
  15. generic_form::= "Standard" | "Logical" | ... | defined_term.
  16. long_definition::= term definer "following," closed_piece_of_documentation.
  17. closed_piece_of_documentation::= set | table | box | net | section | reference.
  18. box::=".Box" ... ".Close.Box".
  19. set::= ".Set" ... ".Close.Set". [ notn_5_Form.html ] This is a longer version of the mathematical formula
  20. {element, element, ..., element}.
  21. list::=".List" ... ".Close.List". There is a corresponding short form
  22. (item, item, ... )
  23. section::=".Open" Name ... ".Close" Name. [ notn_2_Structure.html ]
  24. reference::= ".See " (URL | headline). [ notn_4_Re_Use_.html ]
  25. table::=following, [ notn_9_Tables.html ]
  26. net::=".Net" ... ".Close.Net". There is a corresponding short form
  27. Net{ item, item, ... }
    In this form the items can be simple declarations ( id:type ) or simple well-formed-formulae. Declarations can be abreviated if the type is "Sets". Example
  28. Net{ Set, op:Set><Set->Set, associative(op) }
    
    Older form
    The older form made it harder to recognize short definitions unambiguously from documentation. Deprecated
    2. definition::= short_definition | (format |) long_definition.
    3. older_short_definition::=optional_shorthand defined_term ( definer expression | "::=""Net{" documentation "}",
    4. older_long_definition::= |{ t "::=""Net{" documentation "}=::" t || t:defined_term}. This means that a long definition begins and ends with the same term. It is obvious that:
    5. |- long_definition ==> defined_term "::=" "Net{" documentation "}" "=::" defined_term.
  29. context::= expression_indicating_a_type.
  30. optional_shorthand::= #(defined_term":" ":" "=").
    A definition simultaneously declares a variable and also asserts that it equals a particular value depending on various parameters in the term defined.
    Here are some examples.
    Table of Definition types
```
 Definition		Declaration	Assertion	Notes
```
```
 t::= e			t::Te		t=e		e has type
```
    Te
```
 t::T= e			t.T::T		t.T=e		t.T
```
    replaces t in a context that needs a T
```
 Parameterized Definition
```
```
 For v:T, t(v) ::S=e		t::(S^T)=map [v:T](e)
```
```
 For v:T, t(v) ::=e		t::(Te^T)=map [v:T](e)
```
  31. binding::= loose_binding | tight_binding,
  32. tight_binding::= variable O(colon type) equals expression,
  33. term::= (name | formal_expression | other_language_string) & (declared_term | defined_term),
  34. declared_term::=term & term_in_scope_of_some_declaration,
  35. defined_term::=term & term_in_scope_of_some_definition,
  36. formal_expression::= expression & #(bound_symbolic_name | lexeme).
    Notice that MATHS allows the simultaneous definition of all the parts of a structured term. This can be used to simultaneously develop the concrete and abstract syntax of a language, or to define a translation from one (grammatical) structure to another one, for example.
  . . . . . . . . . ( end of section Definitions) <<Contents | End>>
  
  Semantics of a piece of documentation
  [ notn_14_Docn_Semantics.html ]
  
  Cross References
5. O::=optional (_). [ O in notn_12_Expressions ]
6. P::=parenthesized list of (). [ P in notn_12_Expressions ]
. . . . . . . . . ( end of section Documentation in MATHS) <<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.

Contents

Documentation in MATHS

Introduction

Philosophy

Syntax

Conditional documentation

Comments

Glosses

References

Declarations

Declarations and Definitions

Constrained Declarations

Remote Definitions

Assertions

Proof

Lexicons and Grammars

Wffs and propositions

Resolving ambiguous labels.

Arguments and proofs

Definitions

Example of definitions

Algebra

Older form

Table of Definition types

Semantics of a piece of documentation

Cross References

Notes on MATHS Notation

Notes on the Underlying Logic of MATHS

Glossary

( End of document ) <<Contents | Top