[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / math.syntax
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Thu Nov 10 05:50:38 PST 2011

Contents


    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: [ intro_characters.html ] and [ intro_ebnf.html ] elsewhere.

      Lexemes

      [ math.lexicon.html ]

      Syntax of Documentation

    1. documentation::=#(formal | break | directive | gloss | (label| ) comment ).
    2. formal::=formula | formal_definition | declaration | assertion.
    3. double_colon::=colon colon.
    4. colon::=":".
    5. definition::=formal_definition | gloss.
    6. formal_definition::=(for_clause (condition | ) | )term double_colon (context | )"="expression ender,
    7. gloss::= term double_colon (context | )"=" (balanced ~ expression) ender.
    8. balanced::= See http://www.csci.csusb.edu/dick/maths/notn_12_Expressions.html#balanced.
    9. ender::= "." | ",".
    10. declaration::= O(for_clause O(condition ))term double_colon context ender.
    11. assertion::= axiom | theorem.
    12. axiom::= "|" "-" O(name)well_formed_formula.
    13. formula::=indentation O(name) expression.
    14. theorem::= O(indentation) why "|" "-" O(name)well_formed_formula.
    15. why::="(" L(reason) ")".
    16. name::="(" label ")" ":" .
    17. reason::= label | term | ... .
    18. for_clause::= "For" bindings ",".
    19. condition::= ("If"|"if") wff "," .

    20. break::=two or more end of lines.
    21. indentation::= a tab at the start of a line followed by other white space.
    22. 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,...
    23. directive::=a line starting with a dot indicating structure and/or meaning.

    24. well_formed_formula::=wff.
    25. wff::= See http://cse.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.
    26. glossary::= #(gloss).

      Grammars

    27. grammar::= #( simple_definition | comment ),
    28. simple_definition::=(defined_term":"":="set_expression),
    29. set_expression::= item #("&" item ),
    30. each item expresses a different constraint on the set of ok strings
    31. item::= element | defined_term | "("selection ")" | syntax_macro,
    32. selection::= alternative #( "|" alternative ),
    33. any alternative is a possible form for the set of ok strings.
    34. alternative::= complementary_form | sequence,
    35. sequence::= #phase ,
    36. each phase is part of the whole sequence, in the same order.
    37. phase::= item | option | any_number_of | syntax_macro,
    38. option::= "O" item ,
    39. any_number_of::="#" item, -- including zero.
    40. complementary_form::= item "~" item,
    41. it must satisfy the first item but not the second.
    42. comment::= (#character )~formal,

    43. syntax_macro::= option | any_number_of | ..., [ Syntax Macros ] below.

    44. element::lexeme=quote #(char~(quote| backslash)|backslash char) quote,
    45. element::syntax=element.lexeme | defined_term_in_lexical_dictionary,
    46. element::=Things which are not defined elsewhere.
    47. defined_term::= (natural_identifier | mathematical_identifier).
    48. natural_identifier::=( (letter | digit) #identifier_character) & ( #identifier_character (letter|digit)) & correctly_spelled & defined.
    49. identifier_character::=(letter | digit | underscore).

    50. correctly_spelled::=#(word | number | underscore).

    51. 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).
    52. non::= character~{(_)},
    53. O::= ((_)|),
    54. O::=an optional (_).
    55. #::=O((_) #(_)),
    56. #::= any number of (_).
    57. N::= (_) #(_),
    58. N::=one or more of (_).
    59. P::= "(" (_) #(comma (_)) ")". -- parameter package
    60. R::="(" identifier "=>" (_) #( comma identifier "=>" (_) ) ")".
    61. R::=record of (_).
    62. L::= (1st)#((2nd) (1st)).
    63. L::= List of (1st) separated by (2nd).
    64. List::=(_) #( comma (_)),
    65. List::=List of (_) separated by commas.

    66. For x:string, x^0::="".
    67. For x, x^1::=x.
    68. For x, x^2::=x x.
    69. For x,n:3..*, x^n::=x x^(n-1).
    70. For x,N:@Nat0, x^N::= |[n:N]x^n.
    71. (above)|-#x = x^Nat0.

      Shorthand and Algebra

    72. mathematical_identifier::=letter (superscript|)(subscript|).
    73. superscript::=prime,
    74. prime::="'".
    75. subscript::=(digit # digit| "[" expression "]").

      Notice that shorthand is inherently local, and not prepared for others to use.

      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:

    76. |- P(e)::= "(" (e) #(comma (e)) ")".

    77. POSTFIX::=P((1st)) (2nd),
    78. PREFIX::=(2nd) P((1st)),
    79. CAMBRIDGE::="(" (2nd) #(1st) ")",
    80. UNARY::= POSTFIX((1st), (2nd)) | PREFIX((1st), (2nd)),
    81. INFIX::= "(" (1st) #((2nd) (1st)) ")" . In the following the 1st and 2nd arguments are expressions and the 3rd will be an operator:
    82. RPN::=reverse_polish_notation,
    83. RPN::=(1st) (2nd) (3rd),
    84. LISP2::=Cambridge_polish_notation,
    85. LISP2::="(" (3rd) (1st) (2nd) ")",
    86. BINARY::= "(" (1st) (3rd) (2nd) ")". In the next definition the argument is an expression
    87. EXTENSION::="{" List((_)) "}",
    88. EXTENSION::=Set described by listing elements.

    89. LAMBDA::= "map" "[" (1st) "]" "(" (2nd) ")" . The 1st argument is set_of_declarations, and the 2nd a set of expression,
    90. INTENSION::= "{" (1st) "||" (2nd) "}", The 1st argument is set_of_declarations, and the 2nd a proposition,
    91. INTENSION::=Set described by giving a rule rather than a list of elements.

    92. For e:expressions, p:@(char><char), BRA-KET(e,p)::={ b e k || (b,k) :p }.

      Semantics of logical symbols

    93. @::={true, false}.

    94. not::@->@.

      and, or, not,iff::infix(@,@,@).

      if(1st)then(2nd) ::@><@->@.

    95. if__then__::=False only when the (1st) is true and (2nd) is false.
    96. not::=if (_) is true then false else true.
    97. and::=True iff both (1st) and (2nd) are true.
    98. or::=True if either (1st) or (2nd) is true.
    99. iff::=True when (1st) = (2nd).

    100. priority::= /(not, and, or, iff).


    101. |- (E1): {and,or} are serial.


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


    103. (above)|-(@,or,false,and,true,not) in Boolean_algebra

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

    105. Natural::={1,2,3,...}.
    106. Nat::=Natural.

    107. Nat0::={0,1,2,3,...}.
    108. Unsigned::=Nat0.

    109. Integer::={...,-3,-2,-1,0,1,2,3,...}.
    110. int::=Integer.
    111. Int::=Integer.

    112. Rational::=A Fraction with a numerator and a denominator that are integers.

    113. Real::=The set of all possible numbers with decimals etc.

    114. For i,j, i..j::={ k || i<=k<=j }.

    115. For Type T, @T::= The sets of elements of type T.
    116. For Type T, SetOf(T)::= @T.

    117. For Type T, A,B:@T, A & B::={c || c in A and c in B},
    118. For Type T, A,B:@T, A | B::={c || c in A or c in B},
    119. For Type T, A,B:@T, A ~ B::={c || c in A and not( c in B) },

    120. For Type T, A,B:@T, A==>B::= for all a:A(a in B),
    121. |-For Type T, A,B:@T, A = B iff A==>B and B==>A,

    122. For Type T, A,B:@T, A=>>B::= A==>B and not A=B.
    123. For Type T, A,B:@T, A>==B::=( |B=A and for all X,Y:B(X=Y or X&Y={}) ),
    124. For Type T, A,B:@T, A>==B iff for all a:A, one X in B(a in X).

    125. For A:Sets, a:Elements, A|a::=A|{a},
    126. For A:Sets, a:Elements, a|A::={a}|A, etc

    127. For S:@T, @S::= { A:@T. A==>S}, the subsets of S.
    128. For S, SetOf(S)::= @S.

    129. For A,B:Sets, A><B::= $ Net{1st:A, 2nd:B}, -- -- --(set of pairs)
    130. For A,B:Sets, a:A, b:B, (a, b) ::=(1st=>a, 2nd=>b).
    131. (above)|-For a,b, (a,b).1st=a and (a,b).2nd=b.
    132. For A,B,C:Sets, A><B><C::= $ Net{1st:A, 2nd:B, 3rd:C }.

    133. For A,B,C:Sets,a:A,b:B,c:C, (a,b, c) ::A><B><C=(1st=>a, 2nd=>b, 3rd=>c).

      Lists

    134. CAR::=1st,
    135. CDR::=2nd,
    136. CONS::=map[a,b](a,b).

      Functions

    137. For A,B:Sets, functions(A,B)::= A->B
    138. A->B::=Set of functions taking objects of type A and returning objects of type B,
    139. For A,B:Sets, A->B::=Functions returning a B when given an argument A.
    140. For A,B:Sets, A><B->C::=Functions returning a C given an A and a B.
    141. For A,B:Sets, A><B><C->D::=Functions returning a D given an A, B, and C.

      Families of Sets

    142. For α:@Sets, |(α)::={a||for some A:α(a in A)}.
    143. For α:@Sets, &(α)::={a||for all A:α( a in A )}.

    144. For A,B:Sets, A are B::= A ==>B.
    145. For A,B:Sets, A ==> B::= for all x:A (x in B).

    146. For A,B:Sets, @B::= { A | A ==> B }.

    147. For A,B:Sets, A=>>B::= A==>B and not A=B.

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

    149. For Types T1,T2, R::@(T1><T2)={ (x,y) || x R y}.

    150. For Types T1,T2, x:T1, R:@(T1,T2), x.R::= { y || x R y } .
    151. For Types T1,T2, y:T2, R:@(T1,T2), y./R::= { x || x R y } .

    152. For Types T1,T2, A:@T1, A.R::= { y || some a:A ( aRy) } .
    153. For Types T1,T2, B:@T2, B./R::= { x || some b:B ( x R b) } .

    154. For R, post(R)::=rng(R).
    155. For R, rng(R)::=img(R).
    156. For R, img(R)::=dom(R).R .
    157. (above)|-post(R) = rng(R) = img(R) = |(R).
    158. For R, pre(R)::=cor(R).
    159. For R, cor(R)::=cod(R)./R.
    160. (above)|-pre(R)=cor(R)=cod(R)./R = |(/R)

    161. 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) )
    162. For R, S, R | S::=rel[x:T1,y:T3] (x R y or x S y)
    163. For R, S, R & S::=rel[x:T1,y:T3] (x R y and x S y)

    164. For R, inv(R)::={ Q:@dom(R) || Q.R ==> Q }.
    165. For R, inv(R)::= the invariant sets of R:@(T1,T1).

    166. For R, do(R)::=reflexive transitive closure of R.
    167. For R, do(R)::=rel[x,y:dom(R)] for all Q:inv(R) (if x in Q then y in Q),

    168. For R, no(R)::=rel[x,y:dom(R)](x=y and 0 x.R),

    169. For T:Type, Id(T)::=rel[x,y:dom(R)](x=y ),

    170. For T1,T2, abort::@(T1,T2)=T1><T2,
    171. For T1,T2, fail::@(T1,T1)=rel[x,y:T1](false).

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

    173. total::=(any)-(some).

      Functions and maps

    174. many_1::= (any)-(0..1).

    175. For A,B:Sets, A -> B::= A (any)-(1)B.

    176. For x:binding, e:expression(T), map [x]e::=The map taking x into e,

    177. Id::=map[x](x).identity mapping or function. (_) ::=Id.

    178. For A,B, x,y, x+>y::={(x,y)} maplet.
    179. For A,B, x,y, A+>y::={(x,y)||for some x:A}.

    180. For f:A->B, f(x)=x.f=the f of x= the image of x under f.

    181. f is one-one iff f in dom(f)(1)-(1)cod(f)

      Concatenation

    182. A^n::= if n=0 then 1 else A A^(n-1).
    183. #A::= {()}| A | A A | A A A | ... #A =|[i:0..]A^i = min{ B || (A B | ())==>B}

      Documentation and Nets

    184. Net{ D } -- network of declarations, comments, assertions, definitions etc.
    185. $ Net{x:X, y:Y, ...}:= { (x=>a, y=>b,...) || a in X and b in Y and ...}

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

    187. $(N)::=tpl of variables in documentation,
    188. $ N::=set of $(N) that fit the documentation,
    189. the N(P)::=the( $ N and P),the unique $ N that also fits P,
    190. @N::=collection of sets of objects that fit N,
    191. %N::=lists of objects that fit the documentation,
    192. #N::=strings of objects that fit the documentation,
    193. Uses N::=Inserts a copy of N into current document.
    194. definition(N)::=inserts a copy of the definition of N.
    195. By N::=Derivation of theorem from axioms in N.
    196. For Q N::=Assert contents of named documentation.
    197. for Q N(wff)::=for Q x: $ N (wff where x=$(N)), @{N || for Q1 v1, ...}::= Set of sets of @N satisfying the Qs,
    198. N(x=>a, y=>b,...)::=substitute in N,
    199. N(for some x,...)::=hide x.. in N,
    200. N.(x,y,z,...)::=hide all but x,y,z,....
    201. For N1, N2:Name_of_documentation|set_of_documentation,
    202. not N1::= complementary documentation to N1,
    203. N1 o N2::=combine pieces of documentation,-- o is or,and,...
    204. 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},
    205. N1->N2::=Sets in @(N1 and N2) with N1 as an indentifier,
    206. N1^N2::=maps from type $ N2 to type $ N1, N1(Q1)-(Q2)N1::= Relations between N1 and N2.

      Metaproperties of Documentation

    207. symbol::@( Strings, Types, Values).

      For s: documentation | name_of_documentation,

    208. terms(s)::Sets=terms defined in s,
    209. expressions(s)::Sets=expressions used to define terms in s,
    210. definitions(s)::@(terms(s), types(s), expressions(s))= definitions in s,
    211. declarations(s)::@(variables(s), types(s))= declared and defined types of variables in s,
    212. types(s)::=types in declarations and definitions in s,
    213. variables(s)::=symbols bound in declarations in s,
    214. axioms(s)::=wffs assumed to be true | defined equalities,
    215. assertions(s)::=(axioms(s) | theorems(s)).

      Operators

    216. For X:Set, unary(X)::=X^X.

    217. For X:Set, For f:unary(X), fix(f)::={ x:X || f(x)=x }.

    218. infix(X)::= X^( X><X ).

      For *:infix(X).

    219. associative(X)::={* || for all x,y,z:X(x*(y*z)=(x*y)*z)},
    220. commutative(X)::={* || for all x,y:X (x*y = y*x)},
    221. idempotent(X)::={* || for all x:X (x*x = x)}.

    222. For *:infix(X), units(X,*)::={u:X || x * u = u * x = x},
    223. zeroes(X,*)::={z:X || for all x:X( z*x = x*z= z},
    224. idempotents(X,*)::={i:X || i * i = i}.

      For *:infix(X), x, y:X, (x*y) = (*)(x,y) = (x,y).(*).

    225. For *:infix(X), x:X, (x*_) ::= map y:X(x*y), (_*x) ::= map y:X(y*x),


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

    227. For X:Sets, Y:=@(X,X), I:=Id(X), O:=fail.

    228. For X, Y, Transitive(X)::={R:Y || R;R ==> R },
    229. For X, Y, Reflexive(X)::={R:Y || I ==> R },
    230. For X, Y, Irreflexive(X)::={R:Y || O = I & /R },
    231. For X, Y, Antireflexive(X)::={R:Y || O = R & /R },
    232. For X, Y, Dichotomettic(X)::={R:Y || Y >== {R, /R }},
    233. For X, Y, Trichotomettic(X)::={R:Y || Y >== {R, /R, I}},
    234. For X, Y, Symmetric(X)::= {R:Y || R = /R },
    235. For X, Y, Antisymmetric(X)::={R:Y || R & /R = I},
    236. For X, Y, Asymmetric(X)::={R:Y || R ==> Y~/R },
    237. For X, Y, Total(X)::={R:Y || Y~R = /R },
    238. For X, Y, Connected(X)::={R || Y~R= /R and R | /R = Y},
    239. For X, Y, Regular(X)::= {R:Y || R; /R; R ==> R }.

    240. For X:Sets, Right_limited(X)::= {R:Y || for no S:Nat-->X (R(S) ) }.
    241. For X:Sets, Left_limited(X)::= {R:Y || for no S:Nat-->X ( /R(S) ) }.

    242. For X:Sets, Serial(X)::= (Transitive(X)&Connected(X))~Reflexive( X).

    243. For X:Sets, Strict_partial_order(X)::= Irreflexive(X) & Transitive(X).

    244. For X:Sets, Partial_order(X)::= Reflexive(X) & Transitive(X) & Antisymmetric(X).

    245. For X:Sets, Equivalences(X)::= Reflexive(X) & Symmetric(X) & Transitive(X).

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

    247. For x,y:strings, x!y::string=concatenation of x and y.

    248. For x:string, c:char, c?x::string=prefix c to x,

    249. For x:string, c:char, x?c::string=put c at end of x.

    250. For A,B: sets of strings, A B::={c | c=a!b and a in A and b in B},
    251. For A: sets of strings, #A::=least{ X | X=({""} | A X) }.

    252. For string s, s::@#char={s} .

      Given a string s with n symbols in it then |s| ::=n,

    253. head::=(_)(1), the first symbol in (_),
    254. tail::=all symbols except the first in (_),
    255. |- (s1): if |s|>=1 then s=head(s)!tail(s) ,
    256. last::=(_)(|(_)|).

    257. For Set S, %(%S)::=two dimensional arrays of S's,
    258. #(%S)::=%(S),
    259. (note): %(%S) <> %(S),
    260. lists(S)::=S| %S | %%S | %%%S | ... .

      Aesthetics and Pragmatics

      .Road_Works_Ahead
    261. directive::= blank_line | O(".Open" | ".Close" | "." format) whitespace name EOLN ,
    262. blank_line::=#whitespace EOLN,
    263. format::=#non(whitespace),
    264. name::=#non(EOLN).

    . . . . . . . . . ( end of section MATHS - Discrete mathematics in ASCII) <<Contents | End>>

    Notes on MATHS Notation

    Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

    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 ]

    Notes on the Underlying Logic of MATHS

    The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

    For a more rigorous description of the standard notations see

  1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

    Glossary

  2. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

End