.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