[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci ] / [R J Botting] / [ MATHS ] / intro_characters
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Fri Nov 16 11:12:00 PST 2007


    Introduction to Syntax of MATHS

      Special Characters

       @	prefix: Subsets of/Subsets defined by/SetOf
       @	prefix: Relations between...
       @	 - also  @={true,false}
       %	prefix: Numbered sequences of
       #	prefix: Strings of | any number of
       $	prefix: Set/tuple defined by documenting its structure and properties
       &	infix and prefix: intersection of sets
       |	infix and prefix: union of sets, alternative forms of syntax a la BNF
       ^	infix and prefix: Power, superscript
       !	infix and prefix: Concatenation  of sequences/strings/files/lists/...
       ?	Prefix/postfix items  to sequences/strings/...
       :>=-<	Used to build identifiers: arrows, operators, etc
       *	infix and prefix: Multiplication
       +	infix and prefix: Addition
       -	infix and prefix: subtraction and negate
       \	Nroff  or TEX symbols for strange characters: \Sigma
       {....}	Sets defined by extension(listing) or intension(property)
       ()	Algebraic precedence, function parameters, lists
       []	Lower/subscript/\lambda/Schema
       /	infix: division
       / 	prefix: inverts functions and relations.
       ,	separate parameters, elements in lists, sets, schema,...
       .	infix: apply.  Also separates sentences in schema.
       ::=     `is defined to be the same as`
       ::      `is declared to be of type`
       :       `has type`
       |-      `It is asserted that...`.  `It is assumed`,  or `It can be shown`

      For more see [ notn_10_Lexicon.html ] , and [ math.syntax.html ] or below.


      Here is a quick list of key words used in MATHS
      key wordpurpose
      CloseTerminate the last Net, Set, Let, List, Open
      For, forIntroduses quantifiers: all, some, 1, 0..1, ...
      LetIntroduces a temporary assumption used to prove something else
      ListStart an ordered sequential list
      mapIndicates a map, function, λ
      NetIntroduces a collection of variables and constraints
      OpenOpen a subsection of the document
      RowAn n-tpl of items separated by tabs in a Table
      Set, setIntroduces an unordered set of items
      TableA table: an relation defined as a set of rows

      TeX Symbols

      Maths permits the TeX convention of putting "\" before a word to indicate a symbol. Some of these are handled correctly when mapped to HTML, see [ ../samples/tex2html.html ] for the mapping.


      A MATHS document has many pieces,
    1. document::= #piece_of_documentation.

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

    2. piece_of_documentation::= section | elementary_documentation.
    3. elementary_documentation::=#(formal | break | directive | gloss | (label| ) comment ).
    4. formal::=formula | formal_definition | declaration | assertion.
    5. definition::=formal_definition | gloss.
    6. formal_definition::=(for_clause (condition | ) | )term"::"(context | )"="expression ender,
       		pi ::real= 3.14159.
       		paragraph_tag ::= "<p>".
    7. gloss::= term "::"(context | )"=" (balanced ~ expression) ender.
       		pi ::real= ratio of circumference divided by radius.
    8. balanced::= See http://www.csci.csusb.edu/dick/maths/notn_12_Expressions.html#balanced.
    9. ender::= "." | ",".
    10. declaration::= (for_clause (condition | ) | )term"::"context.
    11. assertion::=axiom | theorem.
    12. formula::= indentation ( label | ) well_formed_formula.
    13. axiom::= (indentation | ) "|-"( label | ) well_formed_formula.
    14. theorem::= (| indentation ) ( evidence ) "|-" ( label | ) well_formed_formula.
    15. label::= "(" identifier "):".
    16. context::=expression describing a type or set of possibilities.
    17. break::= blank line.
    18. indentation::=a tab at the start of the line followed by spaces and tabs.
    19. paragraph_indentation::= a space indicates an item, element, or bullet point.
    20. comment::=just about anything.

      For more see [ math.syntax.html ] and [ notn_13_Docn_Syntax.html ] and [ notn_14_Docn_Semantics.html ] and [ notn_15_Naming_Documentn.html ]


    21. section::=simple_section | open_close_section | local_section. simple_section::= header_line #(paragraph | blank_line | insertion).

    22. header_line::="." white_space name #whitespace eoln,
    23. header::syntax->syntax="." whitespace (_) eoln.
    24. |-header_line= |[H:name](header(H)).

    25. open_close_section::= |[H:name](open(H) #piece_of_documentation close(H))
    26. open::syntax->syntax=".Open" SP (_) eoln,
    27. close::syntax=".Close" O(SP (_)) eoln.

    28. local_section::= |[T:"." type_of_section]( T eoln #piece ".Close" T eoln).
    29. type_of_section::= {"Let", "Net", "Box", "List", "Set", "Table", ...}.


      (expressions): All functions can be used in prefix, postfix, and infix form. Functions are overloaded. In particular predefined operators are apply to sequences and sets. Some are serial (for example +(1,2,3)=1+2+3), while others act in a parallel (for example <(1,2,3)=1<2 and 2<3 and 3<4).

      For more see [ notn_11_Names.html ] and [ notn_12_Expressions.html ]

    . . . . . . . . . ( end of section Introduction to Syntax of 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 = Net{radius:Positive Real, center:Point}.

    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

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


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