[Skip Navigation] [Remove Frame] [CS320] [Text Version] math.syntax.html Sat Dec 23 08:00:25 PST 2006

# MATHS - Discrete mathematics in ASCII

This document is a syntax summary of the notation. There is are less formal introductions [ intro_characters.html ] [ intro_ebnf.html ]

## 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"::"(context | )"="expression ender,
7. gloss::= term "::"(context | )"=" (balanced ~ expression) ender.
8. balanced::= See http://cse.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::=indented O(name) expression.
14. theorem::= O(indented) 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::=one or more spaces and tabs at start of a line.
22. directive::=a line starting with a dot indicating structure and/or meaning.

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

## Grammars

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

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

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

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

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

65. For x,n x^0="", x^1=1, x^n=x^(n-1).

## Shorthand and Algebra

66. mathematical_identifier::=letter (superscript|)(subscript|).
67. superscript::=prime::="'".
68. subscript::=(digit # digit| "[" expression "]").

Notice that shorthand is inherently personal, and not prepared for others to read. It is useful 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:

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

70. POSTFIX::=P((1st)) (2nd),
71. PREFIX::=(2nd) P((1st)),
72. CAMBRIDGE::="(" (2nd) #(1st) ")",
73. UNARY::= POSTFIX((1st), (2nd)) | PREFIX((1st), (2nd)),
74. INFIX::= "(" (1st) #((2nd) (1st)) ")" . In the following the 1st and 2nd arguments are expressions and the 3rd will be an operator:
75. RPN::=reverse_polish_notation::=(1st) (2nd) (3rd),
76. LISP2::=Cambridge_polish_notation::="(" (3rd) (1st) (2nd) ")",
77. BINARY::= "(" (1st) (3rd) (2nd) ")". In the next definition the argument is an expression
78. EXTENSION::="{" List((_)) "}",
79. EXTENSION::=Set described by listing elements.

The 1st argument is set_of_declarations, and the 2nd a set of expression,

80. LAMBDA::= "map" "[" (1st) "]" "(" (2nd) ")" .
81. INTENSION::= "{" (1st) "||" (2nd) "}",
82. INTENSION::=Set described by giving a rule rather than a list of elements.

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

## Syntax and Semantics of logical symbols

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

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

85. not::@->@=if (_) is true then false else true.
Ptruefalse
not Pfalsetrue
86. and::infix(@,@,@)=True iff both (1st) and (2nd) are true.
87. or::infix(@,@,@)=True if either (1st) or (2nd) is true.
88. iff::infix(@,@,@)=True when (1st) = (2nd).
89. if__then__::@><@->@=False only when the (1st) is true and (2nd) is false.
Ptruetruefalsefalse
Qtruefalsetruefalse
P and Qtruefalsefalsefalse
P or Qtruetruetruefalse
if P then Qtruefalsetruetrue

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

91. |- (E1): {and,or} are serial.
92. (E1)|-p and q and r = and(p,q,r) = (p and q) and r.
93. (E1)|-p or q or r = or(p,q,r) = (p or q) or r.

94. |- (E2): iff is_in parallel.
95. (E2)|-P1 iff P2 iff P3 = (P1 iff P2) and (P2 iff P3) = iff(P1, P2, P3).

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

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

98. Natural::={1,2,3,...}.
99. Nat::=Natural.

100. Nat0::={0,1,2,3,...}.
101. Unsigned::=Nat0.

102. Integer::={...,-3,-2,-1,0,1,2,3,...}.
103. int::=Integer.
104. Int::=Integer.

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

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

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

108. For Type T, A,B:@T, A & B::={c || c in A and c in B},
109. For Type T, A,B:@T, A | B::={c || c in A or c in B},
110. For Type T, A,B:@T, A ~ B::={c || c in A and not( c in B) },
111. For Type T, A,B:@T, A = B iff A==>B and B==>A,
112. For Type T, A,B:@T, A==>B::= for all a:A(a in B),
113. For Type T, A,B:@T, A=>>B::= A==>B and not A=B.
114. For Type T, A,B:@T, A>==B::=( |B=A and for all X,Y:B(X=Y or X&Y={}) ),

115. For Type T, A,B:@T, A>==B iff for all a:A, one X in B(a in X).
116. For A:Sets, a:Elements, A|a::=A|{a},
117. For A:Sets, a:Elements, a|A::={a}|A, etc

118. For A,B:Sets, A><B::= \$ Net{1st:A, 2nd:B}, -- -- --(set of pairs)
119. For A,B:Sets, a:A, b:B, (a, b)::=(1st=>a, 2nd=>b),
120. |-For a,b, (a,b).1st=a, (a,b).2nd=b.
121. For A,B,C:Sets, A><B><C::= \$ Net{1st:A, 2nd:B, 3rd:C }.

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

## Lists

123. CAR::=1st,
124. CDR::=2nd,
125. CONS::=map[a,b](a,b).

## Functions

126. For A,B:Sets, functions(A,B)::= A->B ::=Set of functions taking objects of type A and returning objects of type B,
127. For A,B:Sets, A->B::=Functions returning a B when given an argument A.
128. For A,B:Sets, A><B->C::=Functions returning a C given an A and a B.
129. For A,B:Sets, A><B><C->D::=Functions returning a D given an A, B, and C.

## Families of Sets

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

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

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

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

135. For A:Sets, Q :quantifiers, Q A::=for Q x:T (x in A)

## Relations

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

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

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

141. For R, post(R)::=rng(R)::=img(R)::=dom(R).R = |(R)
142. For R, pre(R)::=cor(R)::=cod(R)./R = |(/R)

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

146. For R, inv(R)::={ Q:@dom(R) || all Q.R ==> Q}.
147. For R, S, inv(R)::= the invariant sets of R:@(T1,T1).

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

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

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

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

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

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

## Functions and maps

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

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

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

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

160. For A,B, x,y, x+>y::={(x,y)} maplet
161. 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.

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

## Concatenation

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

## Documentation and Nets

165. \$ Net{x:X, y:Y, ...}:= { (x=>a, y=>b,...) || a in X and b in Y and ...}

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

167. \$(N)::=tpl of variables in documentation,
168. \$ N::=set of \$(N) that fit the documentation,
169. the N(P)::=the( \$ N and P)::=the unique \$ N that also fits P,
170. @N::=collection of sets of objects that fit N,
171. %N::=lists of objects that fit the documentation,
172. #N::=strings of objects that fit the documentation,
173. Uses N::=Inserts a copy of N into current document.
174. definition(N)::=inserts a copy of the definition of N.
175. By N::=Derivation of theorem from axioms in N
176. For Q N::=Assert contents of named documentation
177. for Q N(wff)::=for Q x: \$ N (wff where x=\$(N)), @{N || for Q1 v1, ...}::= Set of sets of @N satisfying the Qs,
178. N(x=>a, y=>b,...)::=substitute in N,
179. N(for some x,...)::=hide x.. in N,
180. N.(x,y,z,...)::=hide all but x,y,z,....
181. For N1, N2:Name_of_documentation|set_of_documentation,
182. not N1::= complementary documentation to N1,
183. N1 o N2::=combine pieces of documentation,
184. N1 and w::={D. w } where N is the name of {D},
185. N1->N2::=Sets in @(N1 and N2) with N1 as an indentifier,
186. N1^N2::=maps from type \$ N2 to type \$ N1, N1(Q1)-(Q2)N1::= Relations between N1 and N2.

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

For s: documentation | name_of_documentation,

188. terms(s)::Sets=terms defined in s,
189. expressions(s)::Sets=expressions used to define terms in s,
190. definitions(s)::@(terms(s), types(s), expressions(s))= definitions in s,
191. declarations(s)::@(variables(s), types(s))= declared and defined types of variables in s,
192. types(s)::=types in declarations and definitions in s,
193. variables(s)::=symbols bound in declarations in s,
194. axioms(s)::=wffs assumed to be true | defined equalities,
195. assertions(s)::=(axioms(s) | theorems(s))

## Operators

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

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

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

For *:infix(X).

199. associative(X)::={* || for all x,y,z:X(x*(y*z)=(x*y)*z)},
200. commutative(X)::={* || for all x,y:X (x*y = y*x)},
201. idempotent(X)::={* || for all x:X (x*x = x)}.

202. For *:infix(X), units(X,*)::={u:X || x * u = u * x = x},
203. zeroes(X,*)::={z:X || for all x:X( z*x = x*z= z},
204. idempotents(X,*)::={i:X || i * i = i},

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

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

206. |-For *:infix(X), x:X, y:X, (x*_)(y)=y.(x*_)=(_*y)(x)=x.(_*y)=x*y in X,

## Types of Relations

207. For X:sets, Y:=@(X,X).
208. For X, Y, Transitive(X)::={R:Y || R;R ==> R },
209. For X, Y, Reflexive(X)::={R:Y || R = /R },
210. For X, Y, Irreflexive(X)::={R:Y || 0 = I & /R },
211. For X, Y, Antireflexive(X)::={R:Y || 0 = R & /R },
212. For X, Y, Dichotomettic(X)::={R:Y || Y >== {R, /R }},
213. For X, Y, Trichotomettic(X)::={R:Y || Y >== {R, /R, I}},
214. For X, Y, Symmetric(X)::= {R:Y || R = /R },
215. For X, Y, Antisymmetric(X)::={R:Y || R & /R = I},
216. For X, Y, Asymmetric(X)::={R:Y || R ==> Y~/R },
217. For X, Y, Total(X)::={R:Y || Y~R = /R },
218. For X, Y, Connected(X)::={R || Y~R= /R and R | /R = Y},
219. For X, Y, Regular(X)::= {R:Y || R; /R; R ==> R }.

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

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

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

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

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

226. 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). [Mili et al. 89]

## Strings

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

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

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

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

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

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

233. head::=(_)(1)::=the first symbol in (_),
234. tail::=all symbols except the first in (_),
235. (s1): if |s|>=1 then s=head(s)!tail(s) ,
236. last::=(_)(|(_)|).

237. For Set S, %(%S)::=two dimensional arrays of S's,
238. #(%S)::=%(S),
239. (note): %(%S) <> %(S),
240. lists(S)::=S| %S | %%S | %%%S | ... .