Introduction
This document is a syntax summary of the MATHS notation.
The MATHS notation is designed so that mathemtical formulae and
definitions can be expressed in a palatable form by software developers
in ASCII.
It contains more than the norml Bachus-Normal-Form grammar because
a lot of special names need to be given meaning as well as syntax.
This document is a collection of formal (mathematical BNF-style)
definitions and assertions.
There are less formal introductions that may be easier to understand:
[ intro_characters.html ]
and
[ intro_ebnf.html ]
elsewhere.
Lexemes
[ math.lexicon.html ]
Syntax of Documentation
- documentation::=#(formal | break | directive | gloss | (label| ) comment ).
- formal::=formula | formal_definition | declaration | assertion.
- double_colon::=colon colon.
- colon::=":".
- definition::=formal_definition | gloss.
- formal_definition::=(for_clause (condition | ) | )term double_colon (context | )"="expression ender,
- gloss::= term double_colon (context | )"=" (balanced ~ expression) ender.
- balanced
::= See http://www.csci.csusb.edu/dick/maths/notn_12_Expressions.html#balanced.
- ender::= "." | ",".
- declaration::= O(for_clause O(condition ))term double_colon context ender.
- assertion::= axiom | theorem.
- axiom::= "|" "-" O(name)well_formed_formula.
- formula::=indentation O(name) expression.
- theorem::= O(indentation) why "|" "-" O(name)well_formed_formula.
- why::="(" L(reason) ")".
- name::="(" label ")" ":" .
- reason::= label | term | ... .
- for_clause::= "For" bindings ",".
- condition::= ("If"|"if") wff "," .
- break::=two or more end of lines.
- indentation::= a tab at the start of a line followed by other white space.
- paragraph_indentation::= A space at the start of a line.
Start of line (continuation of paragraph)
(label): display and name a formula
tab displays a formula, if at start of line
Space starts a paragraph, item,...
- directive::=a line starting with a dot indicating structure and/or meaning.
- well_formed_formula::=wff.
- wff::= See http://www.csci.csusb.edu/dick/maths/notn_13_Docn_Syntax.html#wff.
Glossaries
A glossary describes a set of words in terms of other words. The syntax
similar to that of a dictionary or grammar, but with less restricted definitions.
- glossary::= #(gloss).
Grammars
- grammar::= #( simple_definition | comment ),
- simple_definition::=(defined_term"::="set_expression),
- set_expression::= item #("&" item ),
- each item expresses a different constraint on the set of ok strings
- item::= element | defined_term | "("selection ")" | syntax_macro,
- selection::= alternative #( "|" alternative ),
- any alternative is a possible form for the set of ok strings.
- alternative::= complementary_form | sequence,
- sequence::= #phase ,
- each phase is part of the whole sequence, in the same order.
- phase::= item | option | any_number_of | syntax_macro,
- option::= "O" item ,
- any_number_of::="#" item, -- including zero.
- complementary_form::= item "~" item,
- it must satisfy the first item but not the second.
- comment::= (#character )~formal,
- syntax_macro::= option | any_number_of | ...,
[ Syntax Macros ]
below.
- element::lexeme=quote #(char~(quote| backslash)|backslash char) quote,
- element::syntax=element.lexeme | defined_term_in_lexical_dictionary,
- element::=Things which are not defined elsewhere.
- defined_term::= (natural_identifier | mathematical_identifier).
- natural_identifier::=( (letter | digit) #identifier_character) & ( #identifier_character (letter|digit)) & correctly_spelled & defined.
- identifier_character::=(letter | digit | underscore).
- correctly_spelled::=#(word | number | underscore).
- word::=(letter letter #letter) & dictionary.
Syntax Macros
The following are syntactic macroes - they map one or two sets
of strings into a more complex set. The argument is shown as an
underscore (_). When there are two arguments they are (1st) and (2nd).
- non::= character~{(_)},
- O::= ((_)|),
- O::=an optional (_).
- #::=O((_) #(_)),
- #::= any number of (_).
- N::= (_) #(_),
- N::=one or more of (_).
- P::= "(" (_) #(comma (_)) ")". -- parameter package
- R::="(" identifier "=>" (_) #( comma identifier "=>" (_) ) ")".
- R::=record of (_).
- L::= (1st)#((2nd) (1st)).
- L::= List of (1st) separated by (2nd).
- List::=(_) #( comma (_)),
- List::=List of (_) separated by commas.
- For x,n x^0="", x^1=1, x^n=x^(n-1).
Shorthand and Algebra
- mathematical_identifier::=letter (superscript|)(subscript|).
- superscript::=prime::="'".
- subscript::=(digit # digit| "[" expression "]").
Notice that shorthand is inherently personal, and not prepared for others
to read. It is used as a personal Aide memoir.
Expressions
MATHS has a number of predefined forms that are used to construct and define
new kinds of expressions: infix, prefix, unary, infix, functional, ... .
In the following (1st) stands for an expression and (2nd) for a
set of operators or functions. Each definition defines a set
of syntax forms like this PREFIX("-",numbers)="-" P(numbers).
Previous defined:
- |- P(e)::= "(" (e) #(comma (e)) ")".
- POSTFIX::=P((1st)) (2nd),
- PREFIX::=(2nd) P((1st)),
- CAMBRIDGE::="(" (2nd) #(1st) ")",
- UNARY::= POSTFIX((1st), (2nd)) | PREFIX((1st), (2nd)),
- INFIX::= "(" (1st) #((2nd) (1st)) ")" .
In the following the 1st and 2nd arguments are expressions and the
3rd will be an operator:
- RPN::=reverse_polish_notation::=(1st) (2nd) (3rd),
- LISP2::=Cambridge_polish_notation::="(" (3rd) (1st) (2nd) ")",
- BINARY::= "(" (1st) (3rd) (2nd) ")".
In the next definition the argument is an expression
- EXTENSION::="{" List((_)) "}",
- EXTENSION::=Set described by listing elements.
The 1st argument is set_of_declarations, and the 2nd a set of expression,
- LAMBDA::= "map" "[" (1st) "]" "(" (2nd) ")" .
- INTENSION::= "{" (1st) "||" (2nd) "}",
- INTENSION::=Set described by giving a rule rather than a list of elements.
- For e:expressions, p:@(char><char), BRA-KET(e,p) ::={ b e k || (b,k) :p }.
Semantics of logical symbols
- @::={true, false}.
- not::@->@.
and, or, not,iff::infix(@,@,@).
if(1st)then(2nd) ::@><@->@.
- not::=if (_) is true then false else true.
- and::=True iff both (1st) and (2nd) are true.
- or::=True if either (1st) or (2nd) is true.
- iff::=True when (1st) = (2nd).
- if__then__::=False only when the (1st) is true and (2nd) is false.
- priority::= /(not, and, or, iff).
- |- (E1): {and,or} are serial.
- |- (E2): iff is_in parallel.
Note - serial and parallel operators associate differently:
Serial: P1 and P2 and P3 = (P1 and P2) and P3 = and(P1, P2, P3).
Parallel: P1 iff P2 iff P3 = (P1 iff P2) and (P2 iff P3) = iff(P1, P2, P3).
- (above) |-(@,or,false,and,true,not) in Boolean_algebra
- For P=(P1 or P2 or P3 or,...) and Q =(Q1 and Q2,...) then P :- Q ::= if Q then P.
(for all x:X(W(x))) ::=For all x of type X , W(x) is true,
(for x:X(W(x))) ::= for all x:X(W(x)),
(for no x:X(W(x))) ::=for all x:X(not W(x)),
(for some x:X(W(x))) ::=not for no x:X(W(x)).
(for 0..1 x:X(W(x))) ::=for all y,z:X(if W(y) and W(z) then y=z),
(for 1 x:X(W(x))) ::= for some x:X(W(x)) and for 0..1 x:X(W(x)),
(for 2 x:X(W(x))) ::= for some x:X(W(x)) and for 1 y:X(x<>y and W(y)).
(for 3 x:X(W(x))) ::= for some x:X(W(x)) and for 2 y:X(x<>y and W(y)).
etc.
Sets
- Natural::={1,2,3,...}.
- Nat::=Natural.
- Nat0::={0,1,2,3,...}.
- Unsigned::=Nat0.
- Integer::={...,-3,-2,-1,0,1,2,3,...}.
- int::=Integer.
- Int::=Integer.
- Rational::=A Fraction with a numerator and a denominator that are integers.
- Real::=The set of all possible numbers with decimals etc.
- For i,j, i..j::={ k || i<=k<=j }.
- For Type T, @T::= The sets of elements of type T.
- For Type T, SetOf(T) ::= @T.
- For Type T, A,B:@T, A & B::={c || c in A and c in B},
- For Type T, A,B:@T, A | B::={c || c in A or c in B},
- For Type T, A,B:@T, A ~ B::={c || c in A and not( c in B) },
- For Type T, A,B:@T, A==>B::= for all a:A(a in B),
- |-For Type T, A,B:@T, A = B iff A==>B and B==>A,
- For Type T, A,B:@T, A=>>B::= A==>B and not A=B.
- For Type T, A,B:@T, A>==B::=( |B=A and for all X,Y:B(X=Y or X&Y={}) ),
- For Type T, A,B:@T, A>==B iff for all a:A, one X in B(a in X).
- For A:Sets, a:Elements, A|a::=A|{a},
- For A:Sets, a:Elements, a|A::={a}|A, etc
- For S:@T, @S ::= { A:@T. A==>S}, the subsets of S.
- For S, SetOf(S) ::= @S.
- For A,B:Sets, A><B::= $ Net{1st:A, 2nd:B}, -- -- --(set of pairs)
- For A,B:Sets, a:A, b:B, (a,b) ::=(1st=>a, 2nd=>b).
- (above) |-For a,b, (a,b).1st=a and (a,b).2nd=b.
- For A,B,C:Sets, A><B><C::= $ Net{1st:A, 2nd:B, 3rd:C }.
- For A,B,C:Sets,a:A,b:B,c:C, (a,b,c) ::A><B><C=(1st=>a, 2nd=>b, 3rd=>c).
Lists
- CAR::=1st,
- CDR::=2nd,
- CONS::=map[a,b](a,b).
Functions
- For A,B:Sets, functions(A,B)::= A->B ::=Set of functions taking objects of type A and returning objects of type B,
- For A,B:Sets, A->B::=Functions returning a B when given an argument A.
- For A,B:Sets, A><B->C::=Functions returning a C given an A and a B.
- For A,B:Sets, A><B><C->D::=Functions returning a D given an A, B, and C.
Families of Sets
- For \alpha:@Sets, |(\alpha) ::={a||for some A:\alpha(a in A)}.
- For \alpha:@Sets, &(\alpha) ::={a||for all A:\alpha( a in A )}.
- For A,B:Sets, A are B::= A ==>B.
- For A,B:Sets, A ==> B::= for all x:A (x in B).
- For A,B:Sets, @B::= { A | A ==> B }.
- For A,B:Sets, A=>>B::= A==>B and not A=B.
- For T:Types, A:@T, Q :quantifiers, Q A::=for Q x:T (x in A).
-- examples: no A, all A, some A indicate that A is empty, universal and has at
least one item respectively.
Relations
- For Types T1,T2, R::@(T1><T2)={ (x,y) || x R y}.
- For Types T1,T2, x:T1, R:@(T1,T2), x.R ::= { y || x R y } .
- For Types T1,T2, y:T2, R:@(T1,T2), y./R ::= { x || x R y } .
- For Types T1,T2, A:@T1, A.R ::= { y || some a:A ( aRy) } .
- For Types T1,T2, B:@T2, B./R::= { x || some b:B ( x R b) } .
- For R, post(R) ::=rng(R).
- For R, rng(R) ::=img(R).
- For R, img(R) ::=dom(R).R .
- (above) |-post(R) = rng(R) = img(R) = |(R).
- For R, pre(R) ::=cor(R).
- For R, cor(R) ::=cod(R)./R.
- (above) |-pre(R)=cor(R)=cod(R)./R = |(/R)
- For R, S, (R; S) ::=rel[x:T1,y:T3] for some z(x R z and z S y) (where R :@(T1,T2), S:@(T2,T3) )
- For R, S, R | S::=rel[x:T1,y:T3] (x R y or x S y)
- For R, S, R & S::=rel[x:T1,y:T3] (x R y and x S y)
- For R, inv(R) ::={ Q:@dom(R) || Q.R ==> Q }.
- For R, inv(R)::= the invariant sets of R:@(T1,T1).
- For R, do(R)::=reflexive transitive closure of R.
- For R, do(R) ::=rel[x,y:dom(R)] for all Q:inv(R) (if x in Q then y in Q),
- For R, no(R) ::=rel[x,y:dom(R)](x=y and 0 x.R),
- For T:Type, Id(T) ::=rel[x,y:dom(R)](x=y ),
- For T1,T2, abort::@(T1,T2)=T1><T2,
- For T1,T2, fail::@(T1,T1)=rel[x,y:T1](false).
- For T1,T2, R is nondeterministic::= for some x:dom(R), 2.. y:cod(R) ( x R y ).
- ForU,V, U(Q1)-(Q2)V::= {R || for all x:U, Q2 y (x R y) & all y:V, Q1 x (x R y) }.
- total::=(any)-(some).
Functions and maps
- many_1::= (any)-(0..1).
- For A,B:Sets, A -> B::= A (any)-(1)B.
- For x:binding, e:expression(T), map [x]e::=The map taking x into e,
- Id::=map[x](x).identity mapping or function.
(_) ::=Id.
- For A,B, x,y, x+>y::={(x,y)} maplet.
- For A,B, x,y, A+>y::={(x,y)||for some x:A}.
For f:A->B, f(x)=x.f=the f of x= the image of x under f.
- f is one-one iff f in dom(f)(1)-(1)cod(f)
Concatenation
- A^n::= if n=0 then 1 else A A^(n-1).
- #A::= {()}| A | A A | A A A | ...
#A =|[i:0..]A^i = min{ B || (A B | ())==>B}
Documentation and Nets
- Net{ D } -- network of declarations, comments, assertions, definitions etc.
- $ Net{x:X, y:Y, ...}:= { (x=>a, y=>b,...) || a in X and b in Y and ...}
- variables(U)::= {x,y,z,...}, the names of parts of U, variables act as maps.
For string D where Net{D} in documentation,
$ Net{D, W(v)}::= set v: $ Net{D} satisfying W(v),
$ Net{D, W(v',v)}::= relation v,v': $ Net{D} satisfying W(v',v).
For Name_of_documentation N,
- $(N)::=tpl of variables in documentation,
- $ N::=set of $(N) that fit the documentation,
- the N(P)::=the( $ N and P) ::=the unique $ N that also fits P,
- @N::=collection of sets of objects that fit N,
- %N::=lists of objects that fit the documentation,
- #N::=strings of objects that fit the documentation,
- Uses N::=Inserts a copy of N into current document.
- definition(N)::=inserts a copy of the definition of N.
- By N::=Derivation of theorem from axioms in N.
- For Q N::=Assert contents of named documentation.
- for Q N(wff) ::=for Q x: $ N (wff where x=$(N)),
@{N || for Q1 v1, ...}::= Set of sets of @N satisfying the Qs,
- N(x=>a, y=>b,...)::=substitute in N,
- N(for some x,...)::=hide x.. in N,
- N.(x,y,z,...)::=hide all but x,y,z,....
- For N1, N2:Name_of_documentation|set_of_documentation,
- not N1::= complementary documentation to N1,
- N1 o N2::=combine pieces of documentation,-- o is or,and,...
- N1 and w::={D. w } where N is the name of Net{D},
N1 with { D2 } ::={D. D2 } where N is the name of Net{D},
S with { D2 } ::={D. D2 } where S is $ N and N is the name of Net{D},
- N1->N2::=Sets in @(N1 and N2) with N1 as an indentifier,
- N1^N2::=maps from type $ N2 to type $ N1,
- N1(Q1)-(Q2)N1::= Relations between N1 and N2.
Metaproperties of Documentation
- symbol::@( Strings, Types, Values).
For s: documentation | name_of_documentation,
- terms(s)::Sets=terms defined in s,
- expressions(s)::Sets=expressions used to define terms in s,
- definitions(s)::@(terms(s), types(s), expressions(s))= definitions in s,
- declarations(s)::@(variables(s), types(s))= declared and defined types of variables in s,
- types(s)::=types in declarations and definitions in s,
- variables(s)::=symbols bound in declarations in s,
- axioms(s)::=wffs assumed to be true | defined equalities,
- assertions(s) ::=(axioms(s) | theorems(s)).
Operators
- For X:Set, unary(X) ::=X^X.
- For X:Set, For f:unary(X), fix(f) ::={ x:X || f(x)=x }.
- infix(X)::= X^( X><X ).
For *:infix(X).
- associative(X) ::={* || for all x,y,z:X(x*(y*z)=(x*y)*z)},
- commutative(X) ::={* || for all x,y:X (x*y = y*x)},
- idempotent(X) ::={* || for all x:X (x*x = x)}.
- For *:infix(X), units(X,*)::={u:X || x * u = u * x = x},
- zeroes(X,*) ::={z:X || for all x:X( z*x = x*z= z},
- idempotents(X,*) ::={i:X || i * i = i}.
For *:infix(X), x, y:X, (x*y) = (*)(x,y) = (x,y).(*).
- For *:infix(X), x:X, (x*_) ::= map y:X(x*y),
- (_*x) ::= map y:X(y*x),
- |-For *:infix(X), x:X, y:X, (x*_)(y)=y.(x*_)=(_*y)(x)=x.(_*y)=x*y in X,
Types of Relations
Over the years various books and papers have defined
a lot of different types of relations. The following are
most of the ones I've collected in the last 35 year.
In the following, X is any set and Y is the set of all
relations linking objects in X to objects in X. I is
the identity relation, and 0 the empty relation.
- For X:Sets, Y:=@(X,X), I:=Id(X), O:=fail.
- For X, Y, Transitive(X) ::={R:Y || R;R ==> R },
- For X, Y, Reflexive(X) ::={R:Y || I ==> R },
- For X, Y, Irreflexive(X) ::={R:Y || O = I & /R },
- For X, Y, Antireflexive(X) ::={R:Y || O = R & /R },
- For X, Y, Dichotomettic(X) ::={R:Y || Y >== {R, /R }},
- For X, Y, Trichotomettic(X) ::={R:Y || Y >== {R, /R, I}},
- For X, Y, Symmetric(X) ::= {R:Y || R = /R },
- For X, Y, Antisymmetric(X) ::={R:Y || R & /R = I},
- For X, Y, Asymmetric(X) ::={R:Y || R ==> Y~/R },
- For X, Y, Total(X) ::={R:Y || Y~R = /R },
- For X, Y, Connected(X) ::={R || Y~R= /R and R | /R = Y},
- For X, Y, Regular(X) ::= {R:Y || R; /R; R ==> R }.
- For X:Sets, Right_limited(X) ::= {R:Y || for no S:Nat-->X (R(S) ) }.
- For X:Sets, Left_limited(X) ::= {R:Y || for no S:Nat-->X ( /R(S) ) }.
- For X:Sets, Serial(X) ::= (Transitive(X)&Connected(X))~Reflexive( X).
- For X:Sets, Strict_partial_order(X) ::= Irreflexive(X) & Transitive(X).
- For X:Sets, Partial_order(X) ::= Reflexive(X) & Transitive(X) & Antisymmetric(X).
- For X:Sets, Equivalences(X) ::= Reflexive(X) & Symmetric(X) & Transitive(X).
- For X,Y: Sets, R,S: @(X,Y), R is_more_defined_than S::= pre(S)==>pre(R) and for all x:pre(S) (x.R==>x.S).
[Milietal89]
Strings
- For x,y:strings, x!y::string=concatenation of x and y.
- For x:string, c:char, c?x::string=prefix c to x,
- For x:string, c:char, x?c::string=put c at end of x.
- For A,B: sets of strings, A B ::={c | c=a!b and a in A and b in B},
- For A: sets of strings, #A ::=least{ X | X=({""} | A X) }.
- For string s, s::@#char={s} .
Given a string s with n symbols in it then |s| ::=n,
- head::=(_)(1) ::=the first symbol in (_),
- tail::=all symbols except the first in (_),
- |- (s1): if |s|>=1 then s=head(s)!tail(s) ,
- last::=(_)(|(_)|).
- For Set S, %(%S)::=two dimensional arrays of S's,
- #(%S) ::=%(S),
- (note): %(%S) <> %(S),
- lists(S) ::=S| %S | %%S | %%%S | ... .
Aesthetics and Pragmatics
.Road_Works_Ahead
- directive::= blank_line | O(".Open" | ".Close" | "." format) whitespace name EOLN ,
- blank_line::=#whitespace EOLN,
- format::=#non(whitespace),
- name::=#non(EOLN).