[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci & Eng ] / [R J Botting] / [ MATHS ] / math_72_Systems_Algebra
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Mon Sep 29 14:53:40 PDT 2008


    Algebraic System Theory

      Tse Algebra

    1. Tse_algebra::=$ TSE.
      1. task::Types,
      2. procname::Types, process names.
      3. struct::Types, structures,
      4. event::Types,
      5. dataname::Types.

      6. task::procname><event><event><struct -> task.
      7. P::@procname.
      8. null::procname
      9. sequ::task><task->struct. sequence.
      10. seln::task><task->struct. selection.
      11. para::task><task->struct. parallel composition.
      12. iter::task->struct. Iteration.
      13. elem::@struct. Elementary structured tasks.

      14. indata::dataname->event,
      15. inflag::dataname->event,
      16. infile::dataname->event,
      17. source::dataname->event,
      18. outdata::dataname->event,
      19. outflag::dataname->event,
      20. outfile::dataname->event,
      21. sink::dataname->event.
      22. E::@dataname. (+) ::infix(event).
      23. nil::event.

      24. commute::={f:task><task->struct || for all task u,v ( f(u,v)=f(v,u) )}.
      25. |- (comm): seln and para in commute.
      26. associative::={f:task><task->struct || for all task u,v,w ( f(task(null, f(u,v)),w) = f(u, task(null,f(v,w)) )}.
      27. |- (assoc): seqn and seln and para in associative.


      STRUCTURED_SYSTEM defines a Σ_algebra [ maths_43_algebras.html ] and so a "term_algebra" is the free algebra:

    4. term_algebra::initial_algebra(STRUCTURED_SYSTEM).
    5. term_algebra.carriers::= σ ("(" L(term_algebra.carriers, ";") ")"|).

      The various structured methods of the 1970s and 1980s can all be mapped into algebras that fit Tse's model:

    6. Yourdon_Algebra::$ STRUCTURED_SYSTEM.
    7. DeMarco_algebra::$ STRUCTURED_SYSTEM.
    8. Jackson_Algebra::$ STRUCTURED_SYSTEM.

    . . . . . . . . . ( end of section Algebraic System Theory) <<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 = Net{radius:Positive Real, center:Point}.

    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.