[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / notn_13_Docn_Syntax
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Fri Feb 22 11:51:48 PST 2013

Contents


    Documentation in MATHS

      Introduction

      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.

      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:


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

      Syntax

      Uses
    1. GRAMMAR::= See http://cse.csusb.edu/dick/maths/math_65_Meta_Linguistics.mth#GRAMMAR
    2. expression::= See http://cse.csusb.edu/dick/maths/notn_12_Expressions.html#expression
    3. structure::= See http://cse.csusb.edu/dick/maths/notn_2_Structure.html

      A MATHS document has many pieces,

    4. document::= #piece_of_documentation.

      Some pieces are sections (see structure) and other are elementary:

    5. piece_of_documentation::= section | elementary_documentation.
    6. 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.

    7. formal::=formula | formal_definition | declaration | assertion.
    8. definition::=formal_definition | gloss.
    9. formal_definition::=(for_clause (condition | ) | )term"::"(context | )"="expression ender,
       		pi ::real= 3.14159.
       		paragraph_tag ::= "<p>".
       		cos ::trig_function= sqrt(1-(sin)^2).

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

    11. Let{
        I am using [ logic_8_Natural_Language.html ] to experiment with this notation.
        }

      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

    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.
  1. comment::= sentence #(period sentence).
  2. sentence::=item #(comma item).
  3. item::=(#piece_of_comment)~piece_of_formal_documentation,

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

  5. gloss::= term ":" ":"(context | )"=" (balanced ~ expression) ender.
     		pi ::real= ratio of circumference divided by radius.
  6. balanced::= See http://www.csci.csusb.edu/dick/maths/notn_12_Expressions.html#balanced.
  7. ender::= "." | ",".

    References

    A reference is a dollar sign followed by an identifier.
  8. 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

    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.

  9. 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:
  10. 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.

  11. assertion::= axiom | theorem | conjecture.
  12. axiom::= optional_indentation "|" "-" "(" label "):" wff

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

  14. 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":
  15. A Miracle Happens.

  16. paragraph_indentation::= ASCII.SP #white_space_char.
  17. A space is used to indicate the beginning of bullet points, paragraphs, items in lists, elements in sets, etc.

  18. white_space_char::=( ASCII.SP| ASCII.HT), spaces and tabs.
  19. ASCII::= See http://cse.csusb.edu/samples/samples/comp.text.ASCII.html.

  20. wff::=well_formed_formula.

  21. theorem::= P(evidence) conclusion ,
  22. conclusion::="|" "-" optional_label derived_wff, -- compare with ISO Standard Z.
  23. derived_wff::=wff & derivation leads to wff, [ Arguments and proofs ]

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

  25. 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:
  26. . Proof of l
  27. .Let
  28. |- (l1): Assumption,
  29. (let)|- (l2): Assumption.
  30. ...
  31. (reasons)|- (ln): Result
  32. .Close.Let Typically all proofs would be gathered at the end of a piece of documentation.

  33. well_formed_formula::= O(("For"|"for") #(givens comma) givens comma) proposition(@.expression),

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

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

  36. set_of_documentation::=balanced & ( flag l_brace documentation r_brace).
  37. Flags indicate the part played by the set of documentation - an argument (flagged by ( "Po", "Let" or "Consider,",...), an assertion
  38. (Flagged by "|-"), or a quotation/reference - with no flag. Directives giving Road signs can also be used.
  39. 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

      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.

    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

          (Long Definition):
          1. ALGEBRA::=following,

            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.

            . . . . . . . . . ( end of section Algebra) <<Contents | End>>



          (Schematic Form):
          1. ALGEBRA::= Net{ Set:Sets. }.


          (Inheritance):
          1. SEMIGROUP::= ALGEBRA with {op:associative(Set)}.
          2. UNARY::=ALGEBRA with {function:Set->Set}.


        (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
        1. definition::= short_definition | (format |) long_definition.
        2. older_short_definition::=optional_shorthand defined_term ( definer expression | "::=""Net{" documentation "}",

        3. 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:

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

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

    Glossary

  41. 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).
  42. given::reason="I've been told that...", used to describe a problem.
  43. given::variable="I'll be given a value or object like this...", used to describe a problem.
  44. goal::theorem="The result I'm trying to prove right now".
  45. goal::variable="The value or object I'm trying to find or construct".
  46. 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.
  47. hyp::reason="I assumed this in my last Let/Case/Po/...".
  48. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  49. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  50. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

( End of document ) <<Contents | Top