[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci ] / [R J Botting] / [ MATHS ] / math_15_Unary_Algebra
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Sep 18 15:18:14 PDT 2007

Contents


    Unary Algebras

    A unary algebra is a set of objects with a single unary operation. The operation is modelled as a mapping from the set to the set. As far as I can tell it was introduced in Birkhoff and Bartee's "Modern Applied Mathematics" as an introduction to the "binary" algebras based on a set and a binary operation: semigroups, monoids, and groups.

    Partial unary algebras are needed to model finite ordinal data types.

  1. PARTIAL_UNARY_ALGEBRA::=
    Net{
    1. Set::Sets,
    2. op::Set<>->Set.

    3. finite::@ = Set in FiniteSets.
    4. trivial::@ = Set={}.
    5. nontrivial::@ = some Set.

    6. terminal::=Set~ddef(op), -- set of elements that the operator can not operate on.


    }=::PARTIAL_UNARY_ALGEBRA.

  2. UNARY_ALGEBRA::=
    Net{
    1. Set::Sets,
    2. f::Set>->Set.

    3. finite::@ = Set in FiniteSets.
    4. trivial::@ = Set={}.
    5. nontrivial::@ = some Set.

    6. fixedpoints::={ x:Set || f(x)=x },
    7. symmetry(f)::@(Set---Set)={ a:Set---Set || f o a =a o f }.


    8. (above)|- (eternal_recurrence_1): For all a:Set, i:0.., j:i+1..( if f^i(a)=f^j(a) then for all k:0.., f^(i+k)(a)=f^(j+k)(a)).


    9. (above)|- (eternal_recurrence_2): For all a:Set, i:0.., j:i+1..( if a.f^i=a.f^j then for all p:0.., a.f^i=a.f^(i+p*(j-i)) ).

      These are proved under more restrictive conditions as a result in the theory of relations in Gries and Schneider's "A Logical Approach to Discrete Mathematics".


    }=::UNARY_ALGEBRA.
  3. Unary::=$ UNARY_ALGEBRA.
  4. unary::=Unary.Set,
  5. For X, unary(X)::=Unary(Set=>X).Set.

    Note. The above definitions follow conventions suggested in [ notn_6_Algebra.html ]

  6. Dynamic_System::=following,
    Net

    1. |-UNARY_ALGEBRA.
    2. For Y:Sets, Invariant::@(Set->Y)={g||g o f = g },
    3. For Y:Sets, Invariant::@(Y->Set)={g||for all y:Y, some y':Y(f(g(y))=g(y')) },
    4. Invariant::@@Set={I:@S||f(I)==>I}.
    5. (above)|-fixed_points = {x:Set || {x0}in Invariants}.
    6. (above)|-for A,B:Invariants, A|B in Invariants.

    7. For N:@Nat0, f^N=map[x]{x.(f^n) || n:N},


    8. (above)|-for x0 in fixed_points, N:@Nat~{}, f^N(x0)=x0.
    9. cyclic::={x:Set || for some p (f^(p*Nat0)={x} }.

    10. equifinal::={(x,y)||f^Nat0(x)&f^Nat0(y)},
    11. (above)|-equifinal in EquivalenceRelations(Set),
    12. Basins::= Set/equifinal.
    13. ...See W Ross Ashby's "Introduction to Cybernetics"[RossAshby56]. [click here [socket symbol] if you can fill this hole]

    (End of Net Dynamic_system)

  7. For Set:Sets, a:Set---Set, symetrical(a)={f:Set->Set||f o a =a o f}.

  8. Convergence::=
    Net{

    1. |-UNARY_ALGEBRA.
    2. |-Topology(Set).
    3. LimitSets::@@Set={X:@S || for all N:open, if X==>N the for abf i(f^i(X)==>N)). [click here [socket symbol] if you can fill this hole] ...

    }=::Convergence.

    Unary Morphisms

  9. For (S,a),(T,b):Unary, arrow:{->,>--,>==,---,==>,-->,...}, (Unary)(S,a)->(T,b) ::= {f:S arrow T|| f o a = b o f}

  10. Unary_congruence(Set,f)::= {E:equivalence_relation||E ==>f;E;/f}.

  11. SP_partition(Set,f)::= {Set/E||E in unary_congruence(Set,f)}.
  12. Note - can be generalised to a machine.

    [ Also - Automata and Systems Theory ]

    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

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

    Glossary

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

End