Design of a Lexer for MATHS

Strings

	\"	indicates a quotation mark inside inside a string

 	\\	indicates a backslash when inside a string.

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.
      1. GROUP::=
         Net{

         G::Sets, o::infix(G), associative(o,G). u::units(o), ...

         
         }=::GROUP.
      2. Formally equivalent to form like this: [ signature ] (constraint)
         
      3. |-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.

      4. Po{ * in commutative(S). X*Y*X^-1 = X*X^-1*Y=Y.
      5. } [ 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"

      • Indicates a relationship.
      • is_square_of=rel[x,y:Real](x=y*y). [ logic_40_Relations.html ]

      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 )

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

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

       Example of BNF parser

       
       ( <car:list> <cdr:list> ). 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

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

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

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

   14. l_semantic_bracket::=backslash l_bracket.
   15. r_semantic_bracket::=backslash r_bracket.
   16. l_brocket::=backslash "<".
   17. r_brocket::=backslash ">".
   18. l_TeX_brace::=backslash "{".
   19. 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:

   20. 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.
   21. 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:
6. Identifiers and variables [ notn_11_Names.html ]
7. Expressions [ notn_12_Expressions.html ]
8. Documentation [ notn_13_Docn_Syntax.html ]
9. Conceptual Structure [ notn_2_Structure.html ]
10. 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://csci.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

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

For a more rigorous description of the standard notations see