- Basic Notation of MATHS
- : Introduction
- : Case Sensitivity
- : List of ASCII codes used in MATHS
- : Use of ASCII Characters
- : Useful macro $non
- : Design of a Lexer for MATHS
- : Strings
- : Identifiers
- : Symbols
- : See Also
- : Footnotes
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS
- Glossary

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

(End of Net LEXICON)

- 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:
\" 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

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

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

- Po{ * in commutative(S). X*Y*X^-1 = X*X^-1*Y=Y.
- }
[ logic_2_Proofs.html ]
"with" adds new pieces of documentaion to an existing named piece.

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

"Consider{...}"

### 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}.

"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 all Real x, if x>0 then for 2 Real y ( y*y = x )

- Introduces an expression that is manipulated by algebra.
[ logic_2_Proofs.html ]
[ notn_13_Docn_Syntax.html ]
- 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

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

|-

- 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

### 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.### 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. - 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:
- 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 <options> <regular expression> <files>.
### Example of BNF parser

- ( <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

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

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

- Identifiers and variables [ notn_11_Names.html ]
- Expressions [ notn_12_Expressions.html ]
- Documentation [ notn_13_Docn_Syntax.html ]
- Conceptual Structure [ notn_2_Structure.html ]
- 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

- and3::= See http://cse.csusb.edu/dick/maths/logic_2_Proofs.html#and3.

### Proof of Tautology

Let

(Close Let )

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

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

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

. . . . . . . . . ( end of section Basic Notation of MATHS) <<Contents | End>>

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 ]

For a more rigorous description of the standard notations see