.Author Dr. Richard J. Botting, <dick@silicon.csci.csusb.edu>
Computer Science Dept., California State University, San Bernardino
.EMail rbotting@Wiley.csusb.edu
This poster describes a notation for discrete mathematics which is easy to
use with any computer and needs no software except a simple ASCII editor.
The name of the notation is MATHS and stems from my research into why
software is expensive, late and low quality.
Problems in Software Engineering
The literature on Software Engineering makes it clear that mistakes are
made in understanding and expressing the problem, which is then solved
(sometimes incorrectly), The solution is then coded as a complex piece of
software - at which time the errors are discovered. Some mistakes remain
hidden until the system is used. The results can be wide spread
inconvenience and damage - as when the New York Telephone Exchanges ceased
to work last year... More specific analysis of methods shows that this 'Art
of Computer Programming' can be replaced by a process based on science and
mathematics - See Figure 1.
- Software_engineering::=following
Net
Analysis, Design, Implementation :: Process.
- P1:=Analysis. P2:=Design. P3:=Implementation.
Models, Systems, Designs, Proposals,Problems::Flow.
- Clients, Discrete_mathematics,Scientific_method, Concrete_mathematics,
Computer_Science, C_A_S_E, Computing, Software_tools :: Entities.
- P1.Input::=(Models).
- P1.Outputs::= (Models).
- P1.Controls::=(Systems, Clients, Proposals).
- P1.Mechanisms::=(Discrete_mathematics, Scientific_method, C_A_S_E).
- P2.Inputs::=(Designs).
- P2.Outputs::=(Proposals, Computer_science, Designs).
- P2.Controls::=(Models, Problems).
- P2.Mechanisms::=(Concrete_mathematics, Computer_Science, C_A_S_E).
- P3.Inputs::=(Systems).
- P3.Outputs::=(Problems, Software_tools, Systems).
- P3.Controls::=(Designs).
- P3.Mechanisms::=(Computing, Software_tools).
- Notes::=("P1, P2, P3 are concurrent processes").
(End of Net
Software_engineering.)
Logic, mathematics, and proofs should be a part of project documentation
from the initial stages. Set Theory and Logic are important for defining
the problem area. In general Formal Analysis proceeds by stating the
obvious. Simple facts determine the set of logically correct structures.
Grammar theory is useful for documenting sequential data. The same theory
helps define the dynamics (entities, events and patterns) in a situation.
Sets and functions describe the structure of the problem domain and are
used to document requirements and specifications. These sets and functions
define entity types, abstract data types, classes of objects, and/or paths
through the data structures and data base. Thus maps and sets define the
structure shared by the solution and the problem's environment.
Design involves other mathematical methods - The calculus of relations
plus an extension to the lower predicate calculus can be used for
specifying designs. Statistical analysis and simulations are needed to
ensure satisfactory performance as well. Projects that use mathematics and
logic can "zero-in" on the best software. First: Define things that appear
in the description of the problem and (1) are outside the software, (2)
interact with the software, and (3) are individually identifiable by the
software. Second: Define events, entities, identifiers, relationships,
attributes, facts, and patterns. These initial steps are an exercise in
stating the obvious. The Scientific Method is an effective way to develop
a mathematical theory or model of the situation. Abstracting a formal
model reveals a natural internal structure and so a structure for a
design. The models are used to validate requirements, specifications,
designs, algorithms, data structures, and data bases.
However there is a problem which is not noticeable in the typical discrete
mathematical model: A digraph G is a pair (N, A ) where N is a set and A
is a subset of N ><N....
If we model a typical problem area then we might see:
- A university U is a 17-tple ( P, S, F, C, E, N, D, Q, ...)
where...
One problem is obvious - there are too many components! The computer
professional is further struck by the informality of the language and the
difficult of processing it with a computer. The typical client will be
dumb founded, of course.
My research has focussed on putting together a formal language, that can be
handled by any computer and even translated into 'client friendly' language
and graphics. I have designed a prototype formal language that uses ASCII.
I call it the Multi-purpose Abstraction, Terminology, Heuristic Symbology
(MATHS).
. . . . . . . . . ( end of section Introduction) <<Contents | End>>
In MATHS documentation the following are important parts:
Declarations Identifier :: Set
- (Introduce name/variable and bind to type)
Definition Term ::= Expression
- (Equivalent to declaring term and asserting '=')
- Term::Context=Expression
- Variable:=Term.
- (introduces Mathematical shorthand)
Axiom|-(label): Well Formed Formula
- Theorem (reasons)|- (label): Well Formed Formula
- Proofs, etc See
[ logic_2_Proofs.html ]
- Comments Anything that is not formal.
If D is a collection of declarations, definitions, axioms, theorems etc.
then Net{ D } is called a set of documentation and Net{ D } is the set
of objects that satisfies the documentation. A degenerate case is when D
contains nothing recognisably formal - it is then treated as a natural
language comment - with perhaps some variables/parameters embedded in it.
- For all Sets A, B, A---B::= { f:B^A || for all b:B, one a:A ( f(a)=b)}.
- For all Sets X,
- infix(X)::= X^( X><X ),
- associative(X)::={ *:infix(X)||for x,y,z:X (x*(y*z)=(x*y)*z)},
- commutative(X)::={ *:infix(X)||for x,y:X (x*y = y*x)},
- For X, *, units(X,*)::={ u:X||x*u = u*x = x},
- Semigroup::=SEMIGROUP,
- SEMIGROUP::=Net{ Set::Sets, op::associative(Set) }.
- |-Semigroup = { (Set=>X, op=>(*))|| X:Sets, (*) :associative(X)}.
- ABELIAN::=Net{ Set::Sets, op::commutative(Set). }.
- Abelian_semigroup::=Net{ SEMIGROUP. ABELIAN. }.
- Monoid::=MONOID,
- MONOID::=Net{ SEMIGROUP. u::units(Set, op). }.
- Group::=GROUP,
- GROUP::=following
Net
- |-MONOID.
- i::=inversion::Set---Set.
- |- (inverse): for all x:Set(x op i(x)=i(x) op x =u).
(End of Net
GROUP.)
- UNIVERSITY::=following,
Net
This is a model of a college or university that illustrate the above ideas.
- People::Finite_Sets.
- P::=People.
- Students::@P,
- S::=Students,
- (S, P)|-S in Finite_Sets.
- Faculty::@P,
- F::=Faculty,
- (F, P)|-F in Finite_Sets.
- Courses::Finite_Sets,
- C::=Courses,
- Sets_of_electives::@C,
- E::=Sets_of_electives,
- (E, C)|-E in Finite_Sets.
- Sections::Finite_Sets,
- N::=Sections,
- Departments::Finite_Sets,
- D::=Departments,
- Qualification::Finite_Sets,
- Q::=Qualification,
- dept::C->D. Each course is offered by one dept.
- dept::Q->D. Each qualification belongs to a department.
- d::=dept.
- course::N->C. Each section covers one course.
- c::=course.
(S, P) |-(=) ::S->P. - by definition Students are people.
(F, P) |-(=) ::F ->P. - by definition Faculty are people.
- Teacher::F(1..4)-(0..)N.
- T::=Teacher.
- For f:F, s:S, f T s::@=f teaches s .
- Enrolled::S(10..200)-(0..15)N.
- L::=Enrolled.
- For t:S, n:N, t L n::@=t is enrolled in n .
- Member::F(1..)-(0..1)D.
- M::=Member.
- For f:F, d:D, f M d::@=f is member of d .
- Electives::E(0..)-(1..)Q.
- V::=Electives.
- For e:E, q:Q, e V q::@=e is set of electives in q .
- Declared::S(0..)-(0..)Q.
- W::=Declared.
- For t:S, q:Q, t W q::@=t declared major q .
- Required::C(1..)-(0..)Q.
- R::=Required.
- For c:C, q:Q, c R q::@= { c} is required in q .
- (above) |- in::C(1..)-(0..)E.
- For c:C,e:E, c in e::@=c is an elective in set e .
- |-For f:F, s:N, if f T s then f M d(c(s))
After some manipulation this can be turned into a data base or an object
oriented design (also in ASCII) :
--------------People-----------
"1 "1
" "
"0..1 "
Faculty Department "
"1 "1 |1 |1 |1 "
" " | | | "
" "0,1 |1.. | |0.. "0..1
" Member | Qualification Student
" | |1 |1 |1 |1
" | | |0..|0..|
" |0.. | Declared |
" Course |1.. |
" |1 |1 Electives |
" | | |1 |
" | | | |
" |0.. |0.. |1.. |
" Section --in--- |
" |1 |1 |
"0.. |1..4 |10..200 |0..15
Teacher ------Enrolled---------
(Each vertical line is a mapping. Ditto marks show a subset of the upper one.)
- ...(Further concepts)
(End of Net
UNIVERSITY.)
MATHS Notation
Propositions
A proposition can have two possible meanings - true and false. In MATHS the
symbol @ represents the Boolean type with two standard values { true,
false}. Here are the operators
- not P
- P and Q
- P or Q
- P iff Q
- if P then Q
Unlike most programming languages mathematics has two kinds of infix operator.
- (Serial): P1 and P2 and P3 = (P1 and P2) and P3
- (Parallel): P1 iff P2 iff P3 = (P1 iff P2) and (P2 iff P3).
For more see
[ logic_0_Intro.html ]
A predicate can have variables, quantifiers and equalities as well the
propositions listed above. MATHS spells quantifiers out and includes
numerical quantifiers like "one", "no", "0..1". The syntax attempts to make
the writing of formal statements as natural as possible. In the following
X is a set or a type, x is a variable and W(x) a proposition containing x
in a number of places.
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 x:X(W(x)) ::=for no x:X(W(x) ),
for 1 x:X(W(x)) ::=for some x:X(W(x) and for 0 y:X(x<>y and 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))).
- . . .
for 0..1 x:X(W(x)) ::=for all y,z:X( if W(y) and W(z) then y=z),
- . . .
[ logic_10_Props_+_Predicates_.html ]
[ logic_11_Equality_etc.html ]
[ logic_2_Proofs.html ]
Sets
For any type T there is an another type symbolized by @T with objects that
are sets of objects of type T. In MATHS a subset of a type is not a type,
but a subset (or set for short) does belong to a particular type and so
determines the type of an element in it: If a set A is of type @T then
As elements must be of type T. It is therefore unambiguous to use sets
to declare the type of a variable. In MATHS the symbol for the type is
also symbol for the universal set of that type. It can also be used to
indicate the type of a value - if e can have values of different types
then T(e)=(e).T is the value in T.
Here are some typical expressions
- { } -- the null set
- T -- the universal set (the name ofthe type)
- {e} -- a singleton set
- {e1,e2,e3,...} -- set with listed elements
- { x:T || P } -- set of x's of type T defined by P
- Net{ D } -- Set satisfying documentation D tupls defined by D
- n..m -- Range, closed interval @T (T must have a linear order)
Predicates
- e1 in S1 -- membership
- S1<> S2 -- inequality
- S1 = S2 -- equality
- S1==>S2 -- subset or equal
- S1=>>S2 -- proper subset
- S1 >==S2 -- S1 partitions into S2
Operators
- S1 & S2 -- intersection
- S1 | S2 -- union
- S1 ~ S2 -- complement
Forthe full details see:
[ logic_30_Sets.html ]
[ logic_31_Families_of_Sets.html ]
[ logic_32_Set_Theory.html ]
MATHS uses both the traditional functional notation (f(x)) and a dot
notation(x.f). So
- For x:X and f:X>-Y, f(x)=x.f= the f of x in Y.
The dot notation fits with Ada, C, Pascal,... where item names map record
values into item values. In mathematics '.' projects a vector into a
scalar. MATHS uses functions to project structured objects to their
components.
The symbol fun (and also 'map') is used to abstract functions from
expressions:
- fun[x:Domain] ( Expression ).
For more see:
[ logic_5_Maps.html ]
[ logic_6_Numbers..Strings.html ]
All modern formal notations from Ada to Z provide means for creating a new
type of object by listing components and specifying constraints and
operations on these components. In MATHS a special set of declarations can
be interpreted as defining a set of labeled tupls. If D is a list of
declarations then
- Net{ D }
is a set of documentation and
- Net{ D }
is the
set of labelled tupls that satisfy the documentation. A name can be given
to documentation (
- N::=Net{ D }
) and if N is the name then N represents
the set of objects that satisfy the documentation.
The formal meaning of a structure is as a collection of maps. Thus
- A><B::=Net{ 1st::A, 2nd::B }
implies 1st: (A><B)->A and 2nd:(A><B)->B. Formally, A><B is the
universal (free, initial, or universally repelling) object in the category
of all types with 1st and 2nd. This means that all types with two maps
called 1st and 2nd into the A and B respectively, is modeled by A><B.
This means that we can map A><B into any other type without loosing the
information about 1st and 2nd items. Therefore A><B encodes all
sets of objects with two components.
Given a structured type T=N then we can talk about its subsets (@T). Sets
of structures are universal. Edgar Codd has shown that any set of data can be
expressed as simple structured tables. This justifies modeling all
abstract objects as tuples. A collection of sets of tuples is a relational
data base and forms a category. The objects in an object oriented design
also forms a similar category. These collection form a conceptual model of
the area being studied that is readily implemented using modern techniques
such as data bases, logic programming, and object oriented programming.
A special kind of relationship is one with two components - equivalent to a
set of 2-tuples. They are turn up in all formal and natural settings. A
relation is typically defined like this
- For x:A, y:B, x R y::=W(x,y) ,
where W(x,y) is a well formed formula. Given the above definition then
- rel[x:A,y:B](W(x,y)) = R.
The set of all relations between sets A and B is written @(A,B) but can be
treated as a subset of A><B:
- R = { (x, y) :A><B || x R y }
Thus relations inherit set operations of intersection, union, and complement.
They have their own operators as well:
- a+>b =rel[x,y](x=a and y=b)={ (a,b)} Maplet(Z)
- A+>b =rel[x,y](x in A and y=b) Constant Map
- Id(X) =rel[x,y](x=y in X) Identity
- Net{ D, D' } =Relation between D and D' Dynamic Predicate
- R; S =rel[x,y] (for some z(x R z S y)) Product
- /R =rel[x,y]( y R x ) Inverse
- R^n =R;R^(n-1) when n>0,
- = (/R)^(-n) when n<0, Power
- = Id when n=0.
- do(R) =Id | R; do(R) Closure
- no(R) =rel[x,y] (x=y and for no z(x R z)) Complement
Functions
- R(x)=x.R ={ y || x R y }
- R(A)=A.R ={ y || for some x:A( x R y) }
- /R(y)=y./R =y.(/R)={ x || x R Y}
For more see
[ logic_40_Relations.html ]
[ logic_41_HomogenRelations.html ]
[ logic_42_Properties_of_Relation.html ]
[ logic_44_n-aryrelations.html ]
See
[ logic_7_Semantics.html ]
[ logic_8_Natural_Language.html ]
[ logic_9_Modalities.html ]