[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / math_43_Algebras
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Fri Dec 7 07:01:58 PST 2012



      Conventional algebras

      [ notn_6_Algebra.html ]

    1. ALGEBRA::=
        An algebra is a set of objects (called Set here) plus other documentation (named DOC here) defining constants, operations and axioms. In Mathematics the lagebra is represented by an n-tple which lists the parameters defining the particular algebra. The Integers for example with the operations of addition and subtraction with unit 0 is said to be a group ( Integer, +, 0, -).

        Conventionally similar names are given to the set of ntples:

      1. (GROUP(Set=>Integers, op=>(+), id=>(0), inv=>(-) ) and to the Set itself:
      2. ( Integers in Group ).

        This network of propositions (ALGEBRA), formalizes the relationship between the documentation of an algebra, the name of the set of ntples, and the type of the objects that fit the algebra.

      3. DOC::name_of_documentation,
      4. |-Set in variables(DOC).
      5. Name::=$ DOC,
      6. name::={ Set:Type(DOC).Set || DOC },
      7. For X:modification, name(X)::={ $(DOC(X)).Set || $(DOC(X)) in $ DOC(X) }


      Examples of algebras

    2. ALGEBRA(SEMIGROUP, Semigroup, semigroup).
    3. ALGEBRA(MONOID, Monoid, monoid).
    4. ALGEBRA(GROUP, Group, group).
    5. ALGEBRA(SEMILATTICE, Semilattice, semilattice).

      For more information on the above family of algebras see [ math_31_One_Associative_Op.html ] with the formal definitions:

    6. SEMIGROUP::= See http://cse.csusb.edu/dick/maths/math_31_One_Associative_Op.html#SEMIGROUP.
    7. MONOID::= See http://cse.csusb.edu/dick/maths/math_31_One_Associative_Op.html#MONOID.
    8. GROUP::= See http://cse.csusb.edu/dick/maths/math_31_One_Associative_Op.html#GROUP.
    9. SEMILATTICE::= See http://cse.csusb.edu/dick/maths/math_31_One_Associative_Op.html#SEMILATTICE.

      Sigma Algebras

      Often expressed in mathematics as Σ Algebras, in MATHS expressed using to "Sigma" to make this term easy to search. Wikipedia hase σ algebras as a part of measure theory. Σ algebras develop from the theory of formal specifications in computer science.

      The idea is that the Σ describes a collection of data types(sorts) plus a collection of operations (functions) that operate on them. However these are not the actual functions, but a description of the abstract functions.

      [click here [socket symbol] if you can fill this hole]


    10. SIGNATURE::=following,
      1. Sorts::Sets.
      2. Operators::Sets.
      3. templates::=%Sorts><Sorts.
      4. (above)|-templates=$ Net{1st:%Sorts, 2nd:Sorts}.
      5. signature::=Operators->templates.
      6. For f:Operators,
      7. cod(f)::Sorts=2nd(signature(f)),
      8. dom(f)::Sorts=1st(signature(f)).

      (End of Net SIGNATURE)

      Example signature

        Ξ:$ SIGNATURE::=(Sorts=>{X}, Operators=>{a,b}, signature=>(a+>((X,X),X)|b+>((),X))).


    11. For Sigma:$ SIGNATURE,
    12. Sigma.ASSIGNMENT::=
        Assigns types to the sorts and operators of Sigma.
      1. A::Sigma.Sorts->Types.
      2. F::Sigma.Operators->Types.


      Universal Algebras

      [click here [socket symbol] if you can fill this hole]


      1. |-SIGNATURE.
      2. Sigma::$ SIGNATURE.
      3. s::=Sigma.signature.
      4. Sigma.ASSIGNMENT. [ Sigma.ASSIGNMENT ]
      5. carriers::@Types=img(A).
      6. functions::@Types=img(F).
      7. (above)|-A in Sigma.Sorts>--carriers and F in Sigma.Operators>--functions.

      8. |-For all f:Sigma.Operators, F(f)=(A o Sigma.dom(f))->A(Sigma.cod(f)).

      9. (above)|-For all f:F(Sigma.Operators), dom(f) in carriers and for some c:%carriers(cod(f)= ><c).


    14. For Sigma:$ SIGNATURE, Sigma.algebra::={ a:$ ASSIGNMENT(Sigma) || UNIVERSAL_ALGEBRA(Sigma=>Sigma, A=>a.A, F=>a.F) }.

      Example Algebra

      [ Example signature ]

      1. (above)|-Ξ=( Sorts=>{X}, Operators=>{a,b}, signature=> (a+>((X,X),X) |b+>((),X))) in $ SIGNATURE.

      2. (A=>X+>2^Nat, F=>(a+>(*).Nat|b+>1.Nat)) and (A=>X+>Nat0, F=>(a+>(+).Nat0|b+>0.Nat0)) in Ξ.algebra.

      Morphisms between Similar algebras

    15. For Sigma:$ SIGNATURE, a:Arrows, A1,A2:Sigma.algebra, ((Sigma.maps)A1 a A2) ::= |[s:Sigma.Sorts](A1.A(s) a A2.A.(s))

      ((Sigma.algebra)A1 a A2) ::= {h:Sigma.Sorts->Sigma.maps(A1 a A2)

    16. | for all s:Sigma.sorts(h(s) in A1.A(s) a A2.A(s))
    17. and for all (d,c):Sigma.signature(h(c)(F(A1)(d,c))=(F(A2)(d,c)) o (h o d))

    Example morphism

      [ Example Algebra ] Let
    1. h:=map[n:Nat0](2^n)


    2. (above)|-h(0)=1 and h(a+b)=h(a)*f(b).

      So since

    3. (above)|-Ξ=(Sorts=>{X}, Operators=>{a,b}, signature=>(a+>((X,X),X)|b+>((),X))).
    4. (above)|-(X+>h) in (Ξ.algebra)(A=>Nat0, F=>(a+>(+).Nat0|b+>0.Nat0))-->(A=>Nat, F=>(a+>(*).Nat|b+>1.Nat)).

  1. (above)|-For Sigma, Category(Objects=>Sigma.algebra, Arrows=>map[A,B]( (Sigma.algebra)A->B).

  2. Sigma.Initial_algebra::=Initial_object(Sigma.algebra).

    Example initial algebra

      [ Example morphism ]
    1. (above)|-Ξ.initial_algebra---(A=>X+>Lists, F=>(a+>cons|b+>null),
    2. cons::=map[x,y](x,y),
    3. null::=().
    4. Lists::={(),((),()),((),((),())),...}.
    5. Grammar::=${a+>(), a+>(a,a)}.
    6. GENESYS(basis=>(), generator=>map[X]{(x,y) || x,y:X}).

    In general, the GENESYS with generator being the union of all operators of a Sigma.algebra will be an Sigma.initial_algebra iff it is a free GENESYS.

    Category Theory

    [ math_25_Categories.html ]

. . . . . . . . . ( end of section Algebras) <<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 might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

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

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


  • 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 document ) <<Contents | Top