[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / logic_6_Numbers..Strings
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Dec 13 14:24:20 PST 2011


    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.



        MATHS includes standard number theory and algebra as givens:
      1. READYMADE::=following

      2. |-READYMADE.

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

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

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

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

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

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

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

        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:

        1. PEANO_S_MODEL::=
          1. Nat::Sets,
          2. 1::Nat,

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


          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.

              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:

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

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

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

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

            2. T::= Elements | @T.

              Since we have numbers and cardinality we have, if N= |T| and n= |ELements|,

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

        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

      15. Nat_infinite::=

        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


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

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

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

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

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

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

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

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

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

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

        Finite Sequences

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

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

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

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

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

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

      40. For a:A^n, if n>0 then 1st(a)::=a(1),
      41. For a:A^n, if n>1 then 2nd(a)::=a(2),
      42. For a:A^n, if n>2 then 3rd(a)::=a(3),

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

      45. |-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:


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

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

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

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

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

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

    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 ]

    Notes on the Underlying Logic of MATHS

    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

  1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html


  2. 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).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. 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.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.