. 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.
PARTIAL_UNARY_ALGEBRA::=Net{
	Set::Sets,
	op::Set<>->Set.

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

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

}=::PARTIAL_UNARY_ALGEBRA.

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

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

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

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

 ()|- (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.
Unary::=$ $UNARY_ALGEBRA.
unary::=Unary.Set,
For X, unary(X) ::=Unary(Set=>X).Set.

Note.  The above definitions follow conventions suggested
in
.See http://www/dick/maths/notn_6_Algebra.html

Dynamic_System::=following,
.Net
 |- UNARY_ALGEBRA.
 For Y:Sets, Invariant::@(Set->Y)={g||g o f = g },
 For Y:Sets, Invariant::@(Y->Set)={g||for all y:Y, some y':Y(f(g(y))=g(y')) },
            Invariant::@@Set={I:@S||f(I)==>I}.
()|- fixed_points = {x:Set || {x0}in Invariants}.
()|- for A,B:Invariants, A|B in Invariants.


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


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

equifinal::={(x,y)||f^Nat0(x)&f^Nat0(y)},
()|-equifinal in EquivalenceRelations(Set),
Basins::= Set/equifinal.
	...See W Ross Ashby's "Introduction to Cybernetics"[RossAshby56].
.Hole
.Close.Net Dynamic_system

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

Convergence::=Net{
  |- UNARY_ALGEBRA.
  |- Topology(Set).
LimitSets::@@Set={X:@S || for all N:open, if X==>N the for abf i(f^i(X)==>N)).
.Hole
...
}=::Convergence.


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

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

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

.See Also - Automata and Systems Theory