A document is made up of pieces of documentation,
[ 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.
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:
[...] 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 [...]
Aphorism XLIV, book I, BaconF1620, Magna Instautio
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.
Uses
- 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{
I am using
[ logic_8_Natural_Language.html ]
to experiment with this notation.
}
- elementary_piece_of_documentation::= ... | conditional_declaration.
- 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
- In $ D, v is a partial map from $ D<>->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:
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>>
}
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.
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::= "." | ",".
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
The older notation using square brackets was hard to render:
"E=M*c^2,[Einstein35]"
refers to Einstein's famous formula.
"E=M*c^2[Einstein35],"
was a strange formula.
(End of Net)
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 ]
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.
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
- x^2+3*x-1 =0.
- Re(x) > 0
(End of Net)
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
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
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.
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.
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)".
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.
- 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:
- 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...
[ notn_8_Evidence.html ]
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
[ 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:
- 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.
Net
(Long Definition):
- ALGEBRA::=following,
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.
. . . . . . . . . ( end of section Algebra) <<Contents | End>>
(Schematic Form):
- ALGEBRA::= Net{ Set:Sets. }.
(Inheritance):
- SEMIGROUP::= ALGEBRA with {op:associative(Set)}.
- UNARY::=ALGEBRA with {function:Set->Set}.
(End of 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".
[ 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.
[ notn_2_Structure.html ]
- reference::= ".See " (URL | headline).
[ notn_4_Re_Use_.html ]
- table::=following,
[ 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->Set, associative(op) }
The older form made it harder to recognize short definitions unambiguously
from documentation.
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.
- 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.
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)
- 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.
. . . . . . . . . ( end of section Definitions) <<Contents | End>>
[ notn_14_Docn_Semantics.html ]
- O::=optional (_).
[ O in notn_12_Expressions ]
- P::=parenthesized list of ().
[ P in notn_12_Expressions ]
. . . . . . . . . ( end of section Documentation in MATHS) <<Contents | End>>
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 ]
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
- 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.