.Open MATHS - Discrete mathematics in ASCII
. 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:
.See http://www.csci.csusb.edu/dick/maths/intro_characters.html
and
.See http://www.csci.csusb.edu/dick/maths/intro_ebnf.html
elsewhere.
. Lexemes
.See http://www.csci.csusb.edu/dick/samples/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::=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`.
.As_is Start of line (continuation of paragraph)
.As_is (label): display and name a formula
.As_is tab displays a formula, if at start of line
.As_is Space starts a paragraph, item,...
directive::=`a line starting with a dot indicating structure and/or meaning`.
well_formed_formula::=$wff.
wff::=http://www/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 | ...,
.See 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>@.
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>a, 2nd=>b).
()|- For a,b, (a,b).1st=a and (a,b).2nd=b.
For A,B,C:Sets, A>**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>C::=`Functions returning a C given an A and a B`.
For A,B:Sets, A>****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> 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> 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> 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).
.See [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).
.Close MATHS - Discrete mathematics in ASCII
**