.Open Summary of More advanced Systems
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.
.Open Numbers
. Practice
MATHS includes standard number theory and algebra as givens:
READYMADE::=following
.Net
.See http://www.csci.csusb.edu/dick/maths/math_45_Three_Operators.html
.See http://www.csci.csusb.edu/dick/maths/math_42_Numbers.html
.See http://www.csci.csusb.edu/dick/maths/math_43_Algebras.html
.See http://www.csci.csusb.edu/dick/maths/math_49_Dimensioned_numbers.html
.Close.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::=http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html#INFIX
.Open Models of numbers
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 nNat,
|-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/---,...}.
.See [WhiteheadRussell63]
.See [RamseyFP60]
.See [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...
.Else
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
.Close Models of numbers
. Finite Sets
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.
. Example The natural numbers is not a finite set
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|.
. Arrays
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).
. Pairs
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>a, 2nd=>b).
. Sequences
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.
. Finite Sequences
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).
. Lists and n-tuples
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].
. Strings
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)
. Sets of Lists
It is convenient to note this result from the theory of languages here.
(str_reg): RegularAlgebra(@#A, |, {},(), {()}, #).
. Intervals as Sets and Lists
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.
.Open Complexity of Sets
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:
. Table: Subsets of a Type
.As_is Name Property (of S)
.As_is Finite for some n, S(1)-(1)1..n
.As_is Regular/FiniteState (FiniteAutomata)S->@, (RLin)Nat->S,
.As_is Deterministic (DeterministicPushDownAutomata)S->@
.As_is ContextFree (PushDownAutomata)S->@, (CFG)Nat->S
.As_is ParaContextFree (n PushDownAutomata)S->@
.As_is ContextSensitive/LinearBound (LinearBoundTM)S->@
.As_is ... Time/Space limited computations
.As_is Hard (NPComplete)
.As_is Decidable (Turing Machine) S->@
.As_is Enumerable/RE (Turing Machine) Nat---S
.As_is Countable Nat---S
.As_is Sets @S
For more information see any good book on Computabillity, Complexity of Computation, formal language theory etc.
.Close Complexity of Sets
. Computer Subsets of Abstract Types
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, ...
.Close Subsets of Abstract Types
.Close Summary of More advanced Systems