Tse Algebra

[Tse91]
1. Tse_algebra::=$ TSE.
2. TSE::=STRUCTURED_SYSTEM.
3. STRUCTURED_SYSTEM::=
   Net{

   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.

   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

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

For a more rigorous description of the standard notations see