.Open Documentation in MATHS
. Introduction
A document is made up of pieces of documentation,
.See http://www/dick/maths/notn_2_Structure.html
and each of these is either a section or an elementary piece of documentation.
This document describes the elementary pieces of documentation.
. Philosophy
A piece of documentation may be informal and define no more than a structured
object -- one that can be referred to in other pieces of documentation but
not manipulated with any reliable results.
A formal piece of documentation is not true or false as such - it is a named
collection of assumptions plus the conclusions that are entailed by those
assumptions. In other words it is a logic, logistic system, axiomatic
system, algebra,... It is like a building - it exists and has a
structure. The structure determines what it can be used for. It is built
on a foundation. It may be beautiful or ugly, simple or complex, useful or
useless, boring or entertaining,... Like a building it must be made so that
it it fits together - if the foundations are in solid ground than it is
guaranteed to stand tall.
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`:
.Box
[...] 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 [...]
.Close.Box
Aphorism XLIV, book I, BaconF1620, Magna Instautio
A test of good documentation is its validity.
This term is defined later - See
.See http://www/dick/maths/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
Uses
GRAMMAR::=http://www/dick/maths/math_65_Meta_Linguistics.mth#GRAMMAR
expression::=http://www/dick/maths/notn_12_Expressions.html#expression
structure::=http://www/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,
.As_is pi ::real= 3.14159.
.As_is paragraph_tag ::= "".
.As_is cos ::trig_function= sqrt(1-(sin)^2).
declaration::= ($for_clause ($condition | ) | )$term"::"$context.
Here are some example forms.
.As_is For v1:T1, v2:T2, A. Abbreviation for For (v1,v2):T1>->T. The pre-image pre(v)={x:D. E}.
In proofs and arguments the condition E must be established before the
variables declared in L can be used.
In reusing D, the condition E should be established
before variable v is used.
Notice that using v can not automatically assert E because there can
be other conditional definitions with other conditions that declare v.
Do not use conditional documentation to describe special cases, define
a boolean:
.As_is Abelian::=for all x,y(x+y=y+x).
.Close.List
Hence conditional_definition
.As_is If E then V::T=e.
Hence the form
.As_is If E then N.
where N is the name of of another piece of documentation.
Also
.As_is If E then either a or b.
which introduces to mutually exclusive boolean variables a:@ and b:@.
.Close Conditional documentation
}
. Comments
For many readers the comments are the most important parts
of a MATHS document. Comments should relate the formulas to
wider contexts - the why and wherefore of the situation and the
authors thinking.
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.
.As_is pi ::real= ratio of circumference divided by radius.
balanced::=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
.As_is $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
.As_is (identifier): authors, title, source.
References to URLs can be written as definitions of using this format:
.As_is (identifier): tag
.As_is .See URL
This notation
.As_is .See [identifier]
should link to a sitewide bibliography.
deprecated notation.
.Net
The older notation using square brackets was hard to render:
.As_is "E=M*c^2,[Einstein35]"
refers to Einstein's famous formula.
.As_is "E=M*c^2[Einstein35],"
was a strange formula.
.Close.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 \in 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 \in
S1` and `t \in 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
.See http://www/dick/maths/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:
.As_is x::Real where 3*x+1 = 2.
These are essentially the same as a normal definition. The above can
be rewritten:
.As_is x::Real=the{x:real || 3*x+1 =2}.
So
.As_is v :: T where P.
means
.As_is v::T = the{v:T. P}.
Here is a more complex example:
.As_is x::Complex where following
.Net
x^2+3*x-1 =0.
Re(x) > 0
.Close.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
.As_is t::T=u
can be considered an abbreviation for
.As_is t::T= following
.As_is .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:
.See http://www/dick/maths/logic_2_Proofs.html#reducto_ad_absurdum
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::=http://www/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`,
.See 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:
.As_is (L): Axiom.
is rather like:
.As_is L::=Axiom.
.As_is L.
However... there is no `definition(L)` here in reality
.As_is |-(L): Axiom
is rather like:
.As_is L::=Axiom
.As_is |-L.
Again... there is no `definition(L)` here in reality,
.As_is (premises) |-(L): Theorem.
is rather like:
.As_is L::=Theorem.
.As_is (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
.As_is .Po $formula
.As_is ...
.As_is .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
.As_is word::lexeme, purpose.
.As_is word::lexeme=string, purpose.
.As_is word::syntax=expression.
.As_is word::parsing=expression.
.As_is 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 &... ,
.See http://www/dick/maths/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
.As_is Given ".Let" x:S, P, ... "|- " Q ".Close.Let"
.As_is 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.
.See http://www/dick/maths/logic_10_PC_LPC.html#proposition
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:
.Box
Experiments designed to falsify this assumption have failed to give
reason to doubt it (for instance see....)
I have observed that .... , on ... at..., when.....
The documentation/data/code found in ...in the current system
assumes...
On ...date, Mr/Ms J Doe stated that...
A sample of N items were taken at random and...
.Close.Box
.See http://www/dick/maths/notn_8_Evidence.html
.Open Definitions
Definitions declare a new variable and also postulate that
it is equal to some expression. Normally this does not
change the complexity of the system. Only when the expression
is not always defined, or when the expression contains references
back to the term being defined does a definition change the underlying system.
They are highly useful however.
A special kind of definition is used to attach a formal term to
a piece of documentation.
.Warning
Work is in progress in this area.
All definitions use two colons and an equal sign.
context_free_definer::= colon colon equals.
contextual_definer::= colon colon context equals.
definer::= context_free_definer | contextual_definer.
Definers and binders are very similar to binders, see
.See binding
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:
.Box
syntactic
definitions using XBNF.
abbreviations and functions defined be expressions,
structural definitions that state the generic
form and extend it by adding structure to it.
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
(Long Definition):
.Box
ALGEBRA::=following,
.Open Algebra
Set:Sets.
All algebraic systems have one or more operators that
operate on a set of elements. This structure is used as the generic
basis of all algebras such as groups, monoids, and also for
Posets.
.Close Algebra
.Close.Box
(Schematic Form):
.Box
ALGEBRA::= Net{ Set:Sets. }.
.Close.Box
(Inheritance):
.Box
SEMIGROUP::= ALGEBRA with {op:associative(Set)}.
UNARY::=ALGEBRA with {function:Set->Set}.
.Close.Box
.Close.Net
short_definition::=optional_shorthand defined_term definer (expression | structure | schematic_form | URL).
|- $remote_definition ==> $short_definition.
leftb::="{".
rightb::="}".
structure::= generic_form "with" leftb binding_or_axiom #( "," binding_or_axiom) rightb.
schematic_form::= form leftb binding_or_axiom #( "," binding_or_axiom) rightb.
form ::= "Net" | "Set" | "Map" | "Rel" | ... .
simple_structure::= simple_generic_form "with" leftb loose_binding #( "," loose_binding) rightb.
simple_generic_form::=`a term defined by a simple structure`.
binding_or_axiom::= binding | predicate.
generic_form::= "Standard" | "Logical" | ... | defined_term.
long_definition::= term definer "following," closed_piece_of_documentation.
closed_piece_of_documentation::= set | table | box | net | section |
reference.
box::=".Box" ... ".Close.Box".
set::= ".Set" ... ".Close.Set".
.See http://www/dick/maths/notn_5_Form.html
This is a longer version of the mathematical formula
{element, element, ..., element}.
list::=".List" ... ".Close.List".
There is a corresponding short form
(item, item, ... )
section::=".Open" Name ... ".Close" Name.
.See http://www/dick/maths/notn_2_Structure.html
reference::= ".See " (URL | headline).
.See http://www/dick/maths/notn_4_Re_Use_.html
table::=following,
.See http://www/dick/maths/notn_9_Tables.html
net::=".Net" ... ".Close.Net".
There is a corresponding short form
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
Net{ Set, op:Set>Set, associative(op) }
. Older form
The older form made it harder to recognize short definitions unambiguously
from documentation.
.Box Deprecated
definition::= short_definition | (format |) long_definition.
older_short_definition::=optional_shorthand defined_term ( definer expression | "::=""Net{" documentation "}",
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:
|- long_definition ==> defined_term "::=" "Net{" documentation "}" "=::" defined_term.
.Close.Box
context::= expression_indicating_a_type.
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
.As_is Definition Declaration Assertion Notes
.As_is t::= e t::Te t=e e has type
Te
.As_is t::T= e t.T::T t.T=e t.T
replaces t in a context that needs a T
.As_is Parameterized Definition
.As_is For v:T, t(v) ::S=e t::(S^T)=map [v:T](e)
.As_is For v:T, t(v) ::=e t::(Te^T)=map [v:T](e)
binding::= loose_binding | tight_binding,
tight_binding::= variable O(colon type) equals expression,
term::= (name | formal_expression | other_language_string) & (declared_term | defined_term),
declared_term::=term & term_in_scope_of_some_declaration,
defined_term::=term & term_in_scope_of_some_definition,
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.
.Close Definitions
. Semantics of a piece of documentation
.See http://www/dick/maths/notn_14_Docn_Semantics.html
. Cross References
O::=optional (_).
.See http://www.csci.csusb.edu/dick/maths/notn_12_Expressions.html#O
P::=parenthesized list of ().
.See http://www.csci.csusb.edu/dick/maths/notn_12_Expressions.html#P
.Close Documentation in MATHS