.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