.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 reference::=#(lexeme~(l_bracket | r_bracket)) | "$" 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 (like this [Botting89]). A reference to an electronic document is "["file_path_name"@"node#("."domain"]". As a rule the removal of all references should result in no change of meaning. A reference can also be a dollar sign followed by an identifier. When writing formulas from another source (1) take time to give the reference and (2) be careful to avoid ambiguity or misinterpretation: .As_is "E=M*c^2,[Einstein35]" refers to Einstein's famous formula. .As_is "E=M*c^2[Einstein35]," is a strange formula. . 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/notin_16_Clasification.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. . 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