- Algebraic System Theory
- : Tse Algebra
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS
- Glossary

- Tse_algebra::=$ TSE.
- TSE::=STRUCTURED_SYSTEM.
- STRUCTURED_SYSTEM::= Net{
- task::Types,
- procname::Types, process names.
- struct::Types, structures,
- event::Types,
- dataname::Types.
- task::procname><event><event><struct -> task.
- P::@procname.
- null::procname
- sequ::task><task->struct. sequence.
- seln::task><task->struct. selection.
- para::task><task->struct. parallel composition.
- iter::task->struct. Iteration.
- elem::@struct. Elementary structured tasks.
- indata::dataname->event,
- inflag::dataname->event,
- infile::dataname->event,
- source::dataname->event,
- outdata::dataname->event,
- outflag::dataname->event,
- outfile::dataname->event,
- sink::dataname->event.
- E::@dataname. (+) ::infix(event).
- nil::event.
- commute::={f:task><task->struct || for all task u,v ( f(u,v)=f(v,u) )}.
- |- (comm): seln and para in commute.
- 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)) )}.
- |- (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:

- term_algebra::initial_algebra(STRUCTURED_SYSTEM).
- 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:

- Yourdon_Algebra::$ STRUCTURED_SYSTEM.
- DeMarco_algebra::$ STRUCTURED_SYSTEM.
- Jackson_Algebra::$ STRUCTURED_SYSTEM.
- STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
# Glossary

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

. . . . . . . . . ( end of section Algebraic System Theory) <<Contents | End>>

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 ]

For a more rigorous description of the standard notations see