This file summarises some of the more complex logical systems that are used and needed in software engineering. This basially lists the ideas that are taken for granted by the engineer. The principle of not re-inventing the wheel suggests that a practical formal system shouldn't force its
users to provide unnecesary formal definitions.
MATHS includes standard number theory and algebra as givens:
- READYMADE::=following
Net
- |-READYMADE.
The following are all defined or derived elsewhere (see references above).
- (READYMADE) |- Nat::=Natural,
- Natural::={1,2,3,...},
- (READYMADE) |- Neg::={-1,-2,-3,...},
- (READYMADE) |- Nat0::=Nat |{0},
- Positive::=Nat0,
- (READYMADE) |- Int::=Integer,
- Integer::=Nat0 | Neg,
- (READYMADE)|-Integral_domain(Int,+,0,-,*,1,/).
MATHS uses the C notation for incrementation and decrementation - but without changing the value of the argument.
- For n:Int, ++(n)::=n+1,
- --(n)::=n-1.
Brackets are typically omitted after "++" and "--".
- (STANDARD)|-For n:Int, (_+n)=map i(i+n)=++^n and (_-n)=map i(i-n)=--^n,
- STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html#INFIX
The idea is that MATHS contains enough numbers already. But the following speculation
is about how you might, if philosopically inclined, try to model numbers
with the MATHS language.
We merely assume we have an endless supply of different objects for counting...
A third alternative is to make an axiomatic model of the natural numbers - for example Peano's system, expressed as follows in MATHS:
- PEANO_S_MODEL::=
Net{
- Nat::Sets,
- 1::Nat,
- ++::Nat-->Nat, -- notice that this is a 1-1 map.
- |- (closure): do(++)(1)=Nat,
- |- (Induction): For S:@Nat, if 1 in S and S in inv(++) then S=Nat.
- >=::=do(++),
- >::=(++);(>=),
- |-for no n,m:Nat, n>m and n<m,
- +::Nat><Nat->Nat,
- |-for all n:Nat, n+1=++n,
- |-for all n,m:Nat, n+(++m)=++(n+m),
- ...
}=::
PEANO_S_MODEL.
The Peano model of numbers is clearly an abstract data type.
Notice that the (Induction) axiom has the effect of restricting the system to those objects generated by the ++ operation starting from 0. This does allow transfinite induction etc.
There are several ways of modelling the numbers in simpler terms. Here are some popular ones for reference purposes.
The following is pure speculation, not for practice.
Notice the "Let" box that encloses a speculation that hides the contained logics.
Let
Case
One-to-one maps are intimately related to the concept of number. For example one definition of number starts from
defining two sets as having the same number if they can be put into one-one
correspondence. So Numbers are sets of equivalent subsets:
- PM_MODEL::=Net{For Type T, Numbers(T):=@T/---,...}.
[WhiteheadRussell63]
[RamseyFP60]
[WhiteheadRussell97]
The problem with this is that it generates a separate number system for each type of object and we have to work out ways to inter-connect them.
- For Type S,T, A:@S, B:@T, A eq B::= some A---B.
This starts to look like an incomplete sytem of arithmetic...
(End of Case)
Case
A second idea is to contruct a model of the natural numbers, possibly like this:
- SET_THEORY_MODEL::=Net{ 0:={}, 1:={0}, 2:={0, {0}},...}
This would be invalid in MATHS because the sets contain elements of several type - {0, {0}}.
These sets would have to be subsets of a type, T, with definition
- T::= Elements | @T.
Since we have numbers and cardinality we have, if N= |T| and n= |ELements|,
- N = n + 2**N,
which is always false.
This is therefore an inconsistent model of arithmetic.
(Close Case )
Thus we see an example of Goedel's theorem: any logical system that includes
arithmetic is either inconsistent or incomplete.
(Close Let )
. . . . . . . . . ( end of section Models of numbers) <<Contents | End>>
A finite set can not be put into a one-one correspondence with a part of itself. An infinite set can be mapped into a subset of itself.
- Nat_infinite::=
Net{
- (map)|-map i:Nat(i+i) is in Nat --> Nat. Its image is the set of even numbers so
- (above)|-img((_)+(_))=>>Nat,
a proper subset of Nat.
- (above)|-Nat not in finite
}=::
Nat_infinite.
- For all S:@T, finite(S)::= {X:@S||for all f:X-->X ( img(f)=X ) }.
- (?)|-if X:finite(S) then X-->X = X---X.
In a finite set we have the Pigeon_hole Principle - that if you put more
letters into a set of boxes (pigeonholes) than there are boxes then there will
be boxes with more than one letter in them:
- (?)|-For X,Y:finite(S),for f:X->Y, if |X|>|Y| then for some x1,x2:X (f(x1)=f(x2)).
- (?)|-For X:finite(T1), Y:finite(T2), |Y->X|=|X|^|Y|.
In the Vienna Definition Method [VDM] there is a distinction between finite maps and non-finite functions because a computer can store a finite map as an 'array'. In MATHS the word 'array' serves to document finite mappings:
.
- For T1, T2:Types, D:finite(T1), C: @T1, array(D,C)::=( D->C ).
- For T1,T2,D,C, array D of C::=array(D,C).
- For a:array(A,B), i:A, a[i]::=a(i).
- For i:A, i.th:array(A, B)->B::=map[a:array(A,B)](a(i)).
- For a:array(A,B), i:A, (i.th)(a)=(a).(i.th)=a(i).
Normally we take the idea of a pair of objects as given. In MATHS a pair has two components that can be accessed by using subscripts or by to functions (1st and 2nd). Alternately a pair can be defined as the type of objects that are decomposed into two "orthogonal" parts by "Projection" mappings. In MATHS these maps are symbolised "1st" and "2nd".
- For all x:T1, y:T2, one (u,v):T1><T2 ( (x,y)=(u,v) ).
1st:T1^(T1><T2) ::=map[(x,y)](x),
2nd:T2^(T1><T2) ::=map[(x,y)](y).
- (def)|-(x,y)=z iff z.1st=x and z.2nd=y,
- (def)|-(1st,2nd) = (_).
The MATHS structured sets in $ Net{1st:A, 2nd:B}have the above properties:
So
- A><B::=$ Net{1st:A, 2nd:B}.
- For a,b, (a, b) ::= (1st=>a, 2nd=>b).
T^Nat is the type of all sequences of Ts. It includes T^n for all n, and so #T.
Typical values can not be written down, however when all but a finite number of elements are undefined then the sequence is a member of #T and can be written down. Working out ways to discuss the infinite in terms of the finite is a matter for topology (QV).
- For S:Sets, Seq(S)::=Nat->S.
Some [Dijkstra in particular!] prefer to use
- For S, Seq0(S)::=Nat0->S.
- For S, finite_sequence(S)::@Seq(S)= {s || pre(s) in Finite_sets}.
- |-For n:Nat, 1..n={i:Nat||1<=i<=n}.
- For A:@T, a:A, n:Nat0, A^n::=A^(1..n).
- (def)|-For all A,n, A^n==>#A==>#T.
- (def)|-For all A,n, A^n in finite_sequences(A)==>finite_sequences(T).
A particular type of object are the lists of objects of similar type. The MATHS definition includes most common models:
- For T:Types, %T::= lists of objects of type T,
- %T::=| [I:@Nat0](I->T).
%{a,b,c} includes (a,b), (b,a), (a,,b,c),(a,a,a,a,b),...
- |-A^n = A^(1..n) ==>%A.
- For a:A^n, if n>0 then 1st(a)::=a(1),
- For a:A^n, if n>1 then 2nd(a)::=a(2),
- For a:A^n, if n>2 then 3rd(a)::=a(3),
- th::Nat0->(%T->T),
- For T:Types, a:%T, n:0..|a|, n.th(a)=a(n).
- |-1.th=1st and 2.th=2nd and 3rd=3.th.
MATHS could define A^n by the existence of n projection maps (1st,2nd,3rd,4.th,5.th...,n.th) with the property that they uniquely identify the object in A^n:
Hence
- %T = $ Net{0th,1st,2nd,3rd,4.th,5.th,...:T}
- |-%T==>T^Nat0
- For n:Nat0, a:A, a^n::=map i:1..n (a).
- (above)|-a^n = 1..n+>a in A^n.
- For N:@Nat, x:T^N, i:N, x[i]:T::=x(i).
Note. [i] should be typeset/printed as a subscript rather than in brackets
if possible [Naur et al 64].
The symbol # is reserved for finite lists, n-tpls, and strings generated by
an associative concatenation operation. For S:@T, #S has many of the
properties of S^Nat, but is best treated as a special algebra a free
Monoid.
If T is finite then #T is a made of strings defined in Math.Strings.Theory.
The notation for sets of strings (@#T) is defined in Notation'GRAMMAR. The
semantics of strings is defined as a free monoid in Mathematics. Here are
a few facts.
- For S:Finite(T), #S:@#T, #S::=strings of S's,
- #S=|{1..n->S || n:Nat0},
- Languages(S)=@#S=sets of lists of elements of A
- For all a,b:#S, a!b::=Concatenation of a and b,
- SERIAL(!),
- len in (#S,!,{()})->(Nat0,+,0)
It is convenient to note this result from the theory of languages here.
(str_reg): RegularAlgebra(@#A, |, {},(), {()}, #).
In the context of numbers (or other linearly ordered set)
- |- a..b::= { x || a<=x<=b}.
Distinguish this from
- |-(a,..b)::= (a,a+1,a+2, ..., b).
- |-(a,..b)::= map[ i:1..b-a+1] ( i+a-1 ).
Also from the open and closed intervals used with real numbers.
Mathematicians distinguish several broad classes of sets - the finite, the
countable and the transfinite for example. Computer scientists further
classify sets according to the power/space/time needed to generate and/or
recognise them. Without going into too much detail here is a short list of
sets of sets according to the problems involved in handling them:
Name Property (of S)
Finite for some n, S(1)-(1)1..n
Regular/FiniteState (FiniteAutomata)S->@, (RLin)Nat->S,
Deterministic (DeterministicPushDownAutomata)S->@
ContextFree (PushDownAutomata)S->@, (CFG)Nat->S
ParaContextFree (n PushDownAutomata)S->@
ContextSensitive/LinearBound (LinearBoundTM)S->@
... Time/Space limited computations
Hard (NPComplete)
Decidable (Turing Machine) S->@
Enumerable/RE (Turing Machine) Nat---S
Countable Nat---S
Sets @S
For more information see any good book on Computabillity, Complexity of Computation, formal language theory etc.
. . . . . . . . . ( end of section Complexity of Sets) <<Contents | End>>
Few computers provide their users with the abstract data types as defined
above. Instead the typical 'Integer' is implemented as a finite
"approximation" to the abstract. This sometimes becomes a dangerous
conceit. In MATHS names are provide for the common subsets of the integers
and real numbers: fixed, float, decimal, money, ... . The transition from a
correct algorithm in the abstract to a program that uses finite data
requires skill and knowledge - Colman, Aberth, Wilkinson, ...
. . . . . . . . . ( end of section Subsets of Abstract Types) <<Contents | End>>
. . . . . . . . . ( end of section Summary of More advanced Systems) <<Contents | End>>
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 ]
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
- STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
- 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).
- given::reason="I've been told that...", used to describe a problem.
- given::variable="I'll be given a value or object like this...", used to describe a problem.
- goal::theorem="The result I'm trying to prove right now".
- goal::variable="The value or object I'm trying to find or construct".
- 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.
- hyp::reason="I assumed this in my last Let/Case/Po/...".
- QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
- QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
- RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last
assumption (let) that you introduced.