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.

Numbers

Practice

MATHS includes standard number theory and algebra as givens:
1. READYMADE::=following
   Net
   [ math_45_Three_Operators.html ]

   [ math_42_Numbers.html ] [ math_43_Algebras.html ]

   [ math_49_Dimensioned_numbers.html ]

   
   (End of Net)
   
   

   
   

2. |-READYMADE.

   The following are all defined or derived elsewhere (see references above).

3. (READYMADE) |- Nat::=Natural::={1,2,3,...},
4. (READYMADE) |- Neg::={-1,-2,-3,...},

5. (READYMADE) |- Nat0::=Positive::=Nat | {0},
6. (READYMADE) |- Int::=Integer::=Nat0 | Neg,

   
   

7. (READYMADE) |- Integral_domain(Int,+,0,-,*,1,/).

   MATHS uses the C notation for incrementation and decrementation - but without changing the value of the argument.

8. For n:Int, ++(n)::=n+1,
9. --(n)::=n-1. Brackets are typically omitted after "++" and "--".

   
   

10. (STANDARD) |- For n:Int, (_+n)=map i(i+n)=++^n and (_-n)=map i(i-n)=--^n,
11. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html#INFIX

    Models of numbers

    Theory

    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:

    There are several ways of modelling the numbers in simpler terms. Here are some popular ones for refference purposes.

    Principia Mathematica [ Whitehead & Russell]

    1. PM_MODEL::=Net{For T:Sets, Numbers(T): =@T/---,...}

       A second idea is to contruct a model of the natural numbers, possibly like this:

    2. 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}}. Instead 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:

    3. PEANO_S_MODEL::=
       Net{

       1. Nat::Sets, 1::Nat,

       2. ++::Nat-->Nat, -- notice that this is a 1-1 map.
          
       3. |- (closure): do(++)(1)=Nat,
          
       4. |- (Induction): For S:@Nat, if 1 in S and S in inv(++) then S=Nat.
       5. >=::=do(++),
       6. >::=(++);(>=),
          
       7. |-for no n,m:Nat, n>m and n<m,
       8. +::Nat><Nat->Nat,
          
       9. |-for all n:Nat, n+1=++n,
          
       10. |-for all n,m:Nat, n+(++m)=++(n+m),
       11. ...

       
       }=::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.

    . . . . . . . . . ( end of section Models of numbers) <<Contents | End>>

    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

12. Nat_infinite::=
    Net{

    
    
    1. (map) |- map i:Nat(i+i) is in Nat --> Nat. Its image is the set of even numbers so

       
       

    2. (above) |- img((_)+(_))=>>Nat, a proper subset of Nat.
       
    3. (above) |- Nat not in finite

    
    }=::Nat_infinite.

13. For all S:@T, finite(S)::= {X:@S||for all f:X-->X ( img(f)=X ) }.

    
    

14. (?) |- 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:

    
    

15. (?) |- For X,Y:finite(S),for f:X->Y, if |X|>|Y| then for some x1,x2:X (f(x1)=f(x2)).

    
    

16. (?) |- 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: .
17. For T1, T2:Types, array:(finite(T1), finite(T2))->(finite(T1^T2)) ::= map[D:finite(T1),C:finite(T2)]( D->C ).

18. For D:finite(T1), C:finite(T2), array D of C::=array(D,C).
19. For a:array(A,B), i:A, a[i]::=a(i).
20. For i:A, i.th:array(A, B)->B::=map[a:array(A,B)](a(i)).
21. 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".

22. 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).

    
    

23. (def) |- (x,y)=z iff z.1st=x and z.2nd=y,
    
24. (def) |- (1st,2nd) = (_).

    The MATHS structured sets in $ Net{1st:A, 2nd:B}have the above properties: So

25. A><B::=$ Net{1st:A, 2nd:B}.

26. For a,b, (a, b) ::= (1st=>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).

27. For S:Sets, Seq(S)::=Nat->S. Some [Dijkstra in particular!] prefer to use
28. For S, Seq0(S)::=Nat0->S.

    Finite Sequences

29. For S, finite_sequence(S)::@Seq(S)= {s || pre(s) in Finite_sets}.

    
    

30. |-For n:Nat, 1..n={i:Nat||1<=i<=n}.
31. For A:@T, a:A, n:Nat0, A^n::=A^(1..n).
    
32. (def) |- For all A,n, A^n==>#A==>#T.
    
33. (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:

34. For T:Types, %T::= lists of objects of type T,

35. %T::=| [I:@Nat0](I->T).

    %{a,b,c} includes (a,b), (b,a), (a,,b,c),(a,a,a,a,b),...

    
    

36. |-A^n = A^(1..n) ==>%A.

37. For a:A^n, if n>0 then 1st(a)::=a(1),
38. For a:A^n, if n>1 then 2nd(a)::=a(2),
39. For a:A^n, if n>2 then 3rd(a)::=a(3),

40. th::Nat0->(%T->T),
41. For T:Types, a:%T, n:0..|a|, n.th(a)=a(n).

    
    

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

43. %T = $ Net{0th,1st,2nd,3rd,4.th,5.th,...:T}

    
    

44. |-%T==>T^Nat0

45. For n:Nat0, a:A, a^n::=map i:1..n (a).

    
    

46. (above) |- a^n = 1..n+>a in A^n.

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

48. For S:Finite(T), #S:@#T, #S::=strings of S's,
49. #S=|{1..n->S || n:Nat0},
50. Languages(S)=@#S=sets of lists of elements of A
51. For all a,b:#S, a!b::=Concatenation of a and b,
52. SERIAL(!),
53. 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)
54. |- a..b::= { x || a<=x<=b}. Distinguish this from
55. |-(a,..b)::= (a,a+1,a+2, ..., b).
56. |-(a,..b)::= map[ i:1..b-a+1] ( i+a-1 ).

    Also from the open and closed intervals used with real numbers.

    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

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

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

. . . . . . . . . ( end of section Subsets of Abstract Types) <<Contents | End>>

. . . . . . . . . ( end of section Summary of More advanced Systems) <<Contents | End>>

Notes on MATHS Notation

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_2_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints, and give them a name. 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.

Notes on the Underlying Logic of MATHS

For a complete listing of pages by topic see [ home.html ]