.Open 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 .See http://www.csci.csusb.edu/dick/samples/comp.text.ASCII.html .Open Use of ASCII Characters LEXICON::=following .Net SP::=" ", one kind of $whitespace exclam::="!", string concatenation, serial output, in C... not. quotation::="\"", delimits strings of literal characters hash::="#", iteration of strings, Kleene star, Power Types sharp::=$hash. dollar::="$", set of documentation, Structured set, Set of/where percent::="%", Lists ampersand::="&", intersection of two sets apostrophe::="'", Next value of variable left_parenthesis::="(",expression right_parenthesis::=")",expression star::="*", infix operator in expression, often multiply numbers plus::="+", infix operator in expressions, adds numbers comma::=",", used in extension, bindings, lists, parameters minus::="-", used in expressions and as part of arrows dot::=".", symbol, expression, identifier, see period below slash::="/",symbol, expression, converse, inverse divide::=$slash. colon::=":", symbol, local declarations, definitions, and binding double_colon::=":"":", global/exported declarations and definitions, binding semicolon::=";", punctuator, relational composition, less_than::="<", symbol, ORDER equal::="=" , symbol, logic.equality greater_than::=">",symbol, ORDER query::="?", string pre/postfix, serial input at_sign::="@", collection, sets, Type l_bracket::="[", lexeme indicating subscript, Scheme, binding, interval backslash::="\", escaped_character, backslashed_symbol r_bracket::="]", end of binding etc..., interval circumflex::="^", Types, Maps underline::="_", name grave::="`", formula_in_a_different_language l_brace::="{", set, structure, documentation bar::="|", set_expression, union assert::=$bar $minus, indicates an axiom or theorem. double_bar::="||", set defined by extension, `where` r_brace::="}", set, structure, documentation tilde::="~" , symbol, set_expression: complement whitespace_character::= SP| ASCII.HT | ASCII.CR | ASCII.LF | ASCII.FF | ASCII.VT| ..., whitespace::= # $whitespace_character, eoln::= (ASCII.CR | ASCII.LF)whitespace, break::=(ASCII.CR | ASCII.LF)$whitespace_character whitespace, period::="." whitespace, A dot followed by white space is treated as a period. .Close.Net LEXICON .Close Use of ASCII Characters . Useful macro $non non::@character->@character = character ~ (_), non:: character->@character = $non({(_)}). . Design of a Lexer for MATHS lexer::= (i=>{lexical_input}, o=>{ lexer_output, contents},...). Note - i is short for inputs and o for outputs. lexical_input::= #line, line::= (directive | O($whitespace_character) #(lexeme | whitespace) ) EOLN, lexical_output::= O(break) # lexeme, contents::=# directive_information. The break lexeme aids in distingushing and separating comments, assertions, theorems and definitions. lexeme::= non_punctuation_lexeme | punctuator | break, 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++. char_string::= $quotation #( escaped_char | $non($quotation | $backspace) ) $quotation, 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: .As_is \" indicates a quotation mark inside inside a string .As_is \\ 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 .See Tex and Nroff Symbols .Open Identifiers identifier::= (letter|digit) # id_character, id_character::= letter | under_line | prime | digit, 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. .See http://www.csci.csusb.edu/dick/maths/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: 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) (above)|-GROUP = [ G:Sets, o:G^(G>x,y=>y) || x^2+y^2=1}. .Close.Set .See http://www.csci.csusb.edu/dick/maths/logic_30_Sets.html "map", "fun", or "\lambda" .Set Indicates a mathematical mapping or function. square=map[i:Natural](i*i) .See http://www.csci.csusb.edu/dick/maths/logic_5_Maps.html .Close.Set "rel" .Set Indicates a relationship. is_square_of=rel[x,y:Real](x=y*y). .See http://www.csci.csusb.edu/dick/maths/logic_40_Relations.html .Close.Set . Identifiers used in Well Formed Formulae Some special identifiers are used to construct well formed formula: .Set "for", "For" Introduce a series of quantifiers and bindings "all", "some", "one", "no", "most", ... Quantifiers "and", "or", "not", "if"/"If", "then",... Logical operators .Close.Set For example: .As_is For all Real x, if x>0 then for 2 Real y ( y*y = x ) For all Real x, if x>0 then for 2 Real y ( y*y = x ) .See http://www/dick/maths/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: .See http://www/dick/maths/math_11_STANDARD.html . Other Documented Identifiers Each mathematical system, when documented in MATHS and linked into a MATHS document can introduce further identifiers: .See http://www/dick/maths/home.html . Half_baked identifiers Perhaps the end of the alphabet could be used as instant variables in definitions and formula? .Close Identifiers .Open 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. 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: .See http://www/dick/samples/comp.text.TeX.html .See http://www/dick/samples/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. symbol::= $symbol_character # $symbol_character, 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: .Set .As_is |- 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. .See http://www.csci.csusb.edu/dick/maths/logic_2_Proofs.htm (Tautology, subs)|- if x>0 then (x>0 and x>0). .As_is :. Therefore, short hand for very simplest deductions. x>0 :. x*x>0 .As_is -> Set of functions Series::=Natural->Real. not in @->@. .As_is => Indicates a substitution. Associates a value with an attribute in a structured object. i=complex(re=>0, im=>1). .As_is := 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 .As_is == 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. .As_is +> Forms a maplet: a singleton set containing a pair, not = true+>false | false+>true. .As_is :: Declarations of variables/parameters of the piece of document .As_is ::= Definitions of terms used in the document .Close.Set . Othe Standard Symbols Other special identifiers and symbols are defined in the standard net: .See http://www/dick/maths/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. 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 \lambda calculus). Two other special forms are used to describe maps and sets of strings in a natural way: analysed_other_language_string::=open_quote # (bound_variable | lexeme~bound_variable) open_quote | other_language_map | other_language_syntax | other_language_parser. other_language_map::=open_quote # (function_symbol | lexeme~function_symbol) open_quote. function_symbol::="(" |[t1,t2:Type]variable(t1^t2) ")". Examples_other_language_map::={ `the (1st) sat on the (2nd)`, `the parents of (_)`, ...} other_language_syntax::= open_quote # ( BNF_symbol | lexeme~ BNF_symbol ) open_quote. BNF_symbol::= less_than (| identifier colon) #identifiers greater_than. . Example of BNF syntax `grep `. . Example of BNF parser `( )`. .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 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. 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 left::= pre(bracket_pair), right::= post(bracket_pair), bracket_pair:@(left>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). l_semantic_bracket::=backslash l_bracket. r_semantic_bracket::=backslash r_bracket. l_brocket::=backslash "<". r_brocket::=backslash ">". l_TeX_brace::=backslash "{". 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: 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. 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 .See http://www.csci.csusb.edu/dick/maths/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 .See Proof of Tautology below. .See http://www.csci.csusb.edu/dick/maths/logic_2_Proofs.html#Natural Proof ".Case": Introduces a demonstration, a block of text with several alternative local assumptions and declarations. .See http://www.csci.csusb.edu/dick/maths/logic_2_Proofs.html#Proof by Cases ".Consider": Introduces an expression that is manipulated by algebra. .See http://www.csci.csusb.edu/dick/maths/logic_2_Proofs.html#Algebra & Calculation .See http://www.csci.csusb.edu/dick/maths/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). .See http://www.csci.csusb.edu/dick/maths/notn_14_Docn_Semantics.html .See http://www.csci.csusb.edu/dick/maths/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. .See http://www.csci.csusb.edu/dick/maths/logic_2_Proofs.html#Trying Ideas Out 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. .Close Symbols . See Also More information on elementary syntax will be found: Identifiers and variables .See http://www.csci.csusb.edu/dick/maths/notn_11_Names.html Expressions .See http://www.csci.csusb.edu/dick/maths/notn_12_Expressions.html Documentation .See http://www.csci.csusb.edu/dick/maths/notn_13_Docn_Syntax.html Conceptual Structure .See http://www.csci.csusb.edu/dick/maths/notn_2_Structure.html Documenting Evidence .See http://www.csci.csusb.edu/dick/maths/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. .See http://www/dick/maths/home.html .Open Footnotes . Proof of Tautology .Let |-(T1): P. (T1,T1,and3)|-(T2): P and P. .Close.Let and3::=http://www/dick/maths/logic_2_Proofs.html#and3. .Close Footnotes .Close Basic Notation of MATHS