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

Contents


    Basic Notation of MATHS

      Introduction

      MATHS is not a just programming language. MATHS helps all stages in the development of sofyware. It extends EBNF to include discrete mathematics and symbolic logic. MATHS uses ASCII. People are invited to develop and either market or share MATHS-to-Other translators. The MATHS specifications and tools can be distributed with these - as long as they are not charged for and are complete. In other words a VAR can include MATHS as part of their system - but should only charge for their own work.

      Case Sensitivity

      MATHS is highly case sensitive: "net" and "Net" are different.

      List of ASCII codes used in MATHS

      [ comp.text.ASCII.html ]

      Use of ASCII Characters

      1. LEXICON::=following
        Net
        1. SP::=" ", one kind of whitespace
        2. exclam::="!", string concatenation, serial output, in C... not.
        3. quotation::="\"", delimits strings of literal characters
        4. hash::="#", iteration of strings, Kleene star, Power Types
        5. sharp::=hash.
        6. dollar::="$", set of documentation, Structured set, Set of/where
        7. percent::="%", Lists
        8. ampersand::="&", intersection of two sets
        9. apostrophe::="'", Next value of variable
        10. left_parenthesis::="(",expression
        11. right_parenthesis::=")",expression
        12. star::="*", infix operator in expression, often multiply numbers
        13. plus::="+", infix operator in expressions, adds numbers
        14. comma::=",", used in extension, bindings, lists, parameters
        15. minus::="-", used in expressions and as part of arrows
        16. dot::=".", symbol, expression, identifier, see period below
        17. slash::="/",symbol, expression, converse, inverse
        18. divide::=slash.
        19. colon::=":", symbol, local declarations, definitions, and binding
        20. double_colon::=":"":", global/exported declarations and definitions, binding
        21. semicolon::=";", punctuator, relational composition,
        22. less_than::="<", symbol, ORDER
        23. equal::="=" , symbol, logic.equality
        24. greater_than::=">",symbol, ORDER
        25. query::="?", string pre/postfix, serial input
        26. at_sign::="@", collection, sets, Type
        27. l_bracket::="[", lexeme indicating subscript, Scheme, binding, interval
        28. backslash::="\", escaped_character, backslashed_symbol
        29. r_bracket::="]", end of binding etc..., interval
        30. circumflex::="^", Types, Maps
        31. underline::="_", name
        32. grave::="`", formula_in_a_different_language
        33. l_brace::="{", set, structure, documentation
        34. bar::="|", set_expression, union
        35. assert::=bar minus, indicates an axiom or theorem.
        36. double_bar::="||", set defined by extension, where
        37. r_brace::="}", set, structure, documentation
        38. tilde::="~" , symbol, set_expression: complement
        39. whitespace_character::= SP| ASCII.HT | ASCII.CR | ASCII.LF | ASCII.FF | ASCII.VT| ...,
        40. whitespace::= # whitespace_character,
        41. eoln::= (ASCII.CR | ASCII.LF)whitespace,
        42. break::=(ASCII.CR | ASCII.LF)whitespace_character whitespace,
        43. period::="." whitespace, A dot followed by white space is treated as a period.

        (End of Net LEXICON)

      . . . . . . . . . ( end of section Use of ASCII Characters) <<Contents | End>>

      non">Useful macro non

    1. non::@character->@character = character ~ (_),
    2. non:: character->@character = non({(_)}).

      Design of a Lexer for MATHS

    3. lexer::= (i=>{lexical_input}, o=>{ lexer_output, contents},...). Note - i is short for inputs and o for outputs.

    4. lexical_input::= #line,
    5. line::= (directive | O(whitespace_character) #(lexeme | whitespace) ) EOLN,

    6. lexical_output::= O(break) # lexeme,
    7. contents::=# directive_information. The break lexeme aids in distingushing and separating comments, assertions, theorems and definitions.

    8. lexeme::= non_punctuation_lexeme | punctuator | break,

    9. non_punctuation_lexeme::= symbol | identifier | char_string | other_language_string | back_slashed_symbol,

      Strings

      Strings are used to represents sequences or arrays of ASCII characters and follow the same rules as C or C++.
    10. char_string::= quotation #( escaped_char | non(quotation | backspace) ) quotation,
    11. escaped_char::= backslash character. Character strings are written as in the C programming language. However the escape symbols which are much simplified. Only two are actually needed:
      	\"	indicates a quotation mark inside inside a string
       	\\	indicates a backslash when inside a string.
      The backslash character is also used in MATHS, outside of strings to in much the way that it is in TeX and nroff [ Tex and Nroff Symbols ]

      Identifiers

      1. identifier::= (letter|digit) # id_character,
      2. id_character::= letter | under_line | prime | digit,
      3. prime::= apostrophe.

        Identifiers are use to identifier things and are classified as mathematical or algebraic variables and terms. Some identiers have predefined or standard meanings. A properly formed identifier is made up of recognisable words separated by under_line symbols. This ensures that the majority of MATHS documents can be spell checked.

        Special Identifiers

        Some identifiers and symbols are used in a special way in the syntax. [ notn_13_Docn_Syntax.html ]

        Many of these prefix a block of text in the C-like syntax "{...}". For example "Net" prefixes a schematic summary of a piece of documentation:

      4. GROUP::=Net{ G:Sets, o:infix(G), associative(o,G). u:units(o), ...}.

        The above attaches a name to a collection of variables/parameters and constraints. Think of these as a network of statements that work logically and yet may not apply to any known reality. In Sir Francis Bacons terms: a piece of theatre, fictional and scenic. This allows people to play creatively with ideas to see what they imply. They can be mapped onto a class of objects in a program. They may reflect some situation in the real world. These are not a necessary property. However it is wise to always include an example of the "Net".

        Formally the above "Net" is equivalent to a form like this: [ signature ] (constraint)

      5. (above)|-GROUP = [ G:Sets, o:G^(G><G), u:G]( o in infix(G) and associative(o,G) and u in units(G,o) and ...) [ notn_14_Docn_Semantics.html ] [ notn_15_Naming_Documentn.html ] [ logic_2_Proofs.html ]

        Older Notation

        Prior to February 1997 there were several extended schematic forms. These are now handled as Directives.
          "Let{" Introduces a demonstration, a block of text with one or more local assumptions and declarations. [ Proof of Tautology ] below.

          "Case{...}" Introduces a demonstration, a block of text with several alternative local assumptions and declarations.

          "Consider{...}"

        1. Introduces an expression that is manipulated by algebra. [ logic_2_Proofs.html ] [ notn_13_Docn_Syntax.html ]

          "Net{...}" Indicates a piece of documentation connecting some comments, terms, assumptions etc.

        2. GROUP::=
          Net{
            G::Sets, o::infix(G), associative(o,G). u::units(o), ...

          }=::GROUP.
        3. Formally equivalent to form like this: [ signature ] (constraint)
        4. |-GROUP = [ G:Sets, o:G^(G><G), u:G]( o in infix(G) and associative(o,G) and u in units(G,o) and ...) [ notn_14_Docn_Semantics.html ] [ notn_15_Naming_Documentn.html ]

          "Po{...}" Introduces a block of text with one or more local assumptions.

        5. Po{ * in commutative(S). X*Y*X^-1 = X*X^-1*Y=Y.
        6. } [ logic_2_Proofs.html ]

          "with" adds new pieces of documentaion to an existing named piece.


        Mathematical Identifiers

        Some identifiers are used to indicate discrete mathematical objects like sets, functions, and relations.

        "set" or "$"

        • Indicates a mathematical set.
        • $(1,2,3)=set(1,2,3) = set[i:Natural](1<=i<=3)=1..3.
        • ${x,y:Real. x^2+y^2=1}={ (x=>x,y=>y) || x^2+y^2=1}.
        [ logic_30_Sets.html ]

        "map", "fun", or "λ"

        • Indicates a mathematical mapping or function.
        • square=map[i:Natural](i*i) [ logic_5_Maps.html ]

        "rel"

        Identifiers used in Well Formed Formulae

        Some special identifiers are used to construct well formed formula:
        • "for", "For" Introduce a series of quantifiers and bindings
        • "all", "some", "one", "no", "most", ... Quantifiers
        • "and", "or", "not", "if"/"If", "then",... Logical operators
        For example:
         	For all Real x, if x>0 then for 2 Real y ( y*y = x )
      6. For all Real x, if x>0 then for 2 Real y ( y*y = x ) [ logic_10_PC_LPC.html ] The capitalized "If" and "For" are used at the start of statements to make the result closer to English traditions. These are the only lexemes where MATHS ignores case.

        Other Standard Identifers

        Other special identifiers are defined in the standard net: [ math_11_STANDARD.html ]

        Other Documented Identifiers

        Each mathematical system, when documented in MATHS and linked into a MATHS document can introduce further identifiers: [ home.html ]

        Half_baked identifiers

        Perhaps the end of the alphabet could be used as instant variables in definitions and formula?

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

      Symbols

        TeX and Nroff Symbols

        There are two well established notations for special symbols: Donald Knuth's TeX and the UNIX nroff family. These both use the backslash character. This nottion is therefore absorbed into MATHS.
      1. back_slashed_symbol::= back_slash #non(whitespace_character),

        Nroff, troff, TeX etc., use backslash followed by string of printable characters to indicate non-ascii characters such as Greek letters and mathematical symbols: [ comp.text.TeX.html ] [ comp.text.TeX.Mathematical.html ]

        MATHS Symbols

        It is natural to type ">->" to indicate an arrow. A notation like this has recently been suggested for the Z specification language... but it has been part of MATHS since it birth on a Frieden Flexowriter in the 1960's.
      2. symbol::= symbol_character # symbol_character,
      3. symbol_character::= equals | lessthan | greaterthan | tilde | asterisk | plus | minus | ampersand | bar | slash | colon | dot.

        Symbols can be used together or alone. At different points in a piece of documentation different symbols are defined. If whitespace is omitted then even sophisticated context dependant syntactic analysis may fail to divide a symbol up into meaningful sub_symbols (Example "x+++++x" in C).

        Some symbols are used in a special way in the syntax:

            |-
        • Indicates that a formula has been asserted. Similar to ISO Z theorem symbol.
        • |-dogs are barkers.
        • Separates the evidence from the consequence: (evidence)|- (label): theorem
        • Prefixed by the reasons for belief (if any) otherwise it is an axiom.
        • (and3)|- (Tautology): if P then (P and P).
        • If it acts as a link to the proof then the wff is a theorem.
        • Indicates use of earlier formula to derive next one. [ logic_2_Proofs.htm ]
        • (Tautology, subs)|-if x>0 then (x>0 and x>0).
           	:.
        • Therefore, short hand for very simplest deductions.
        • x>0 :. x*x>0
          	->
        • Set of functions
        • Series::=Natural->Real.
        • not in @->@.
           	=>
        • Indicates a substitution.
        • Associates a value with an attribute in a structured object.
        • i=complex(re=>0, im=>1).
           	:=
        • Binds a variable to a value. Creates a tight binding.
        • Always local. Inside expression in which it occurs.
        • Or the document if not inside an expression.
        • for x;=(-b+\sqrt(b^2-4*a*c))/(2*a), a*x^2+b*x+c = 0
           	==
        • Indicates strong identity between two terms
        • Suppose x=y then its not true that x==y or x*x==y*y but x*x=y*y.
           	+>
        • Forms a maplet: a singleton set containing a pair,
        • not = true+>false | false+>true.
           	::
        • Declarations of variables/parameters of the piece of document
           	::=
        • Definitions of terms used in the document

        Othe Standard Symbols

        Other special identifiers and symbols are defined in the standard net: [ math_11_STANDARD.html ]

        Incorporating other languages

        One problem with designing language that has many areas of application is allowing it to act as a metalanguage for other languages - as well as for itself. There is a need to suspend some, but not all of the rules in certain contexts. I have chosen to use a string delimitted by reversed quotes to indicate this.

      4. other_language_string::= (open_quote # non(open_quote) open_quote ), This allows any piece of natural language to placed into MATHS text and left undisturbed as lexical element. MATHS is designed so that formulae can be translated into the user's terminology or relate to another formal language. A formula can be defined to be an other_language_string with bound variables. The translation may be replace the variables by other strings (as in the λ calculus). Two other special forms are used to describe maps and sets of strings in a natural way:

      5. analysed_other_language_string::=open_quote # (bound_variable | lexeme~bound_variable) open_quote | other_language_map | other_language_syntax | other_language_parser.

      6. other_language_map::=open_quote # (function_symbol | lexeme~function_symbol) open_quote.
      7. function_symbol::="(" |[t1,t2:Type]variable(t1^t2) ")".
      8. Examples_other_language_map::={ the (1st) sat on the (2nd), the parents of (_), ...}

      9. other_language_syntax::= open_quote # ( BNF_symbol | lexeme~ BNF_symbol ) open_quote.
      10. BNF_symbol::= less_than (| identifier colon) #identifiers greater_than.

        Example of BNF syntax

      11. grep <options> <regular expression> <files>.

        Example of BNF parser

      12. ( <car:list> <cdr:list> ).

        Source: Mark & Cochrane 92, Leo Mark & Roberta Cochrane, Grammars and Relations, IEEE Trans SE-V18 n9(Sep 92)pp840-849

        .Dangerous_bend BNF-style brackets (brockets) are shouldn't be used outside these special strings withot an escape symbol since the less-than and greater-than symbols are used for other purposes in mathematics.

        Punctuation Symbols

      13. punctuator::= left | right | comma | semicolon | hash | dollar | at_sign | circumflex | percent | query | exclamation | period, Punctuators tend to be used by themselves.

        .RoadWorksAhead At this time the dollar sign can be used in front of an identifier to create a hypertext link to the definition of the identifier. This is a stopgap until a proper parser is available that automatically links defined terms to their definitions.

      14. period::= dot whitespace, Notice that a "." that is inside a string, or is not followed by white space is not a period but a symbol character.

        .RoadWorksAhead Some notations use a big dot to separate a list of declarations from the expression in which they apply. I'm considering using " . " for this purpose. At this time a double bar is used instead "||".

        Parentheses, Brackets, and Braces

      15. left::= pre(bracket_pair), right::= post(bracket_pair),

        bracket_pair:@(left><right) ::=(l_parenthesis+>r_parenthesis) | (l_brace+>r_brace) | (l_bracket+>r_bracket) | (l_semantic_bracket+>r_semantic_bracket) | (l_brocket+>r_brocket) | (l_TeX_brace+>r_TeX_brace).

      16. l_semantic_bracket::=backslash l_bracket.
      17. r_semantic_bracket::=backslash r_bracket.
      18. l_brocket::=backslash "<".
      19. r_brocket::=backslash ">".
      20. l_TeX_brace::=backslash "{".
      21. r_TeX_brace::=backslash "}".

        Parentheses are used disambuguate expressions and to indicate structure.

        A common form are the generic schema that is used for many purposes:

      22. scheme::= |[(l,r):bracket_pair] ( l list #( "||" list ) r ).

        For example, set( x:X || p(x) ) is a schema.

        Note. An alternate syntax uses a period in place of "||". For example: 'set(x:X. p(x) )`. This is experimental.

        Strange Formulae

        A strange formula is one that has been formalized according to a different system.
      23. formula_in_a_different_language::= other_language_string.

        Directives

        A raw MATHS document has the absolute minimum collection of directives that are used to express the logical structure of a document (a croos-linked distributed labelled hierarchy) and guide mark up and display systems. The directives that define the overall structure and intent of a MATHS document are in [ notn_5_Form.html ]

        Some directives are used to to allow pieces of documentation to be treated as formal statements or formulae. A piece of documentation that starts with directive .D will end with directive .Close.D where D is "Let", "Set", "Net", "Box", "Table", ... These pieces of documentation include local assumptions, definitions, and declarations. In other words MATHS has a block structure. They have a multiple of formal purposes. The underlying goal is readabillity.

        The following are new (1997) notations which are being introduced to the online documentation. The older forms are still in use in some documentation and uses braces: Let{...}, Case{.... }, and so instead.

        ".Let": Introduces a demonstration, a block of text with one or more local assumptions and declarations, see [ Proof of Tautology ] below. [ Natural Proof in logic_2_Proofs ]

        ".Case": Introduces a demonstration, a block of text with several alternative local assumptions and declarations. [ Proof by Cases in logic_2_Proofs ]

        ".Consider": Introduces an expression that is manipulated by algebra. [ Algebra & Calculation in logic_2_Proofs ] [ notn_13_Docn_Syntax.html ]

        ".Net": Indicates a piece of documentation connecting some comments, terms, assumptions etc. This is used to define complex formal systems. It is important that the content of a net be written with plenty of relevant commentary. Associated with a net is a summary in terms of a list of variable declarations (the signature of the net) and assumptions (the constraint). [ notn_14_Docn_Semantics.html ] [ notn_15_Naming_Documentn.html ]

        ".Box" is formally like a net, but invites any rendering agent to place the content in a box. Also in a net the contents are not added to the surrounding context. The content of a box is.

        ".Po": Introduces a block of text with one or more local assumptions. The purpose of "Po" is to give the author permission to try out any hyPOthesis that they wish. It invites the reader to suspend judgement of the content of the block of statement until it completed. Formmally it implies the suspension of evaluation in terms of truth and falsehood. [ Trying Ideas Out in logic_2_Proofs ]

        The directives ".Set", ".Table", etc (TBA) define sets of elements in an extended form and invite special rendering.

        ".Image" indicates the inclusion of a graphic image + a textual alternative form.

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

      See Also

      More information on elementary syntax will be found:
    12. Identifiers and variables [ notn_11_Names.html ]
    13. Expressions [ notn_12_Expressions.html ]
    14. Documentation [ notn_13_Docn_Syntax.html ]
    15. Conceptual Structure [ notn_2_Structure.html ]
    16. Documenting Evidence [ notn_8_Evidence.html ]

      Each branch of mathematics also introduces its own syntax, in particular the work done bu logicians and meta-mathematicians in the first half of the 20th century has given rise to several notations for a fairly consistent set of ideas. [ home.html ]

      Footnotes

        Proof of Tautology


        Let

        1. |- (T1): P.
        2. (T1, T1, and3)|- (T2): P and P.

        (Close Let )
      1. and3::= See http://cse.csusb.edu/dick/maths/logic_2_Proofs.html#and3.

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

    . . . . . . . . . ( end of section Basic Notation 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 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

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

    Glossary

  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.

( End of document ) <<Contents | Top