Skip to main contentCal State San Bernardino
>> [CNS] >> [Comp Sci Dept] >> [R J Botting] >> [MATHS] >> notn_6_Algebra
[Contents] || [Source] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Apr 12 08:13:53 PDT 2005

Contents

    Making Use of Algebras

     Uses theory of documentation [ notn_14_Docn_Semantics.html ]

    Certain patterns turn up when using algebraic systems. For example the system declares a set and certain operators and axioms. The user wants to declare the set and have the standard operations and axioms added to their document.

    It is useful to be able to useful to import from other documentation the properties of a variable by declaring it. For example suppose we have alread defined the system:

  1. MONOID::=Net{Set:Sets, op:associative, u:units(S,+),....}.

    Then it would help reuse if we could automatically write declarations like the following to create specific examples:

  2. X:monoid(op=>*, u=>1),
  3. Y:monoid. Notice that it if monoid is defined as $ MONOID.S then op and u are hidden by the projection operation and so can not be assumed to be any other operation.

    The best system would be to always create a set of definitions for the normal way people use algebras. For example:

  4. XYZ::=Net{x:X, y:Y,... z:Z},
  5. Xyz::=$ XYZ, -- set of tupls
  6. xyz::={x:X || XYZ(x=>x, y=>y, ..., z=>z)}, -- set of x's fitting XYZ...
  7. For b,..., c, xyz(y=>b, ..., z=>c)::={x:X || XYZ(x=>x, y=>b, ..., z=>c)},
  8. For b,...,c, xyz(b,...,c)::=xyz(y=>b,..., z=>c).

    As a result we have: (x=>a, y=>b, ..., z=>c ) :: Xyz can declare variables a::X, b::Y,...,c::Z. (a, b, ..., c) :: Xyz can declare variables a::X, b::Y,...,c::Z.

  9. a:: xyz(y=>b, ..., z=>c, ) declares a::X (given b,... ,c ).
  10. a::xyz(b, ... ,c) declares a::X (given b,..., c ).
  11. a:: xyz declares (x=>a, y=>y, z=>z,...) ::xyz. and as in Ada:
  12. |-xyz(b,..., z=>c) = xyz(y=>b,... , z=>c)

    For a single sorted algebra like a group, poset, etc we can formalize the relation as follows -

  13. ALGEBRA::=
    Net{
    1. DOC::name_of_documentation,
    2. Set::variables(DOC).
    3. Name::=$ XYZ,
    4. name::={ Set:Type(DOC)(Set) || DOC }, for X, name(X) ::={ Set:Type(DOC)(Set) || (DOC(X))($(DOC(X))

    }=::ALGEBRA.

    .Example

  14. ALGEBRA(DOC=>MONOID, Set=>Set, Name=>Monoid, name=>monoid),

    .Example

  15. ALGEBRA(DOC=>SEMIGROUP, Set=>Set, Name=>Semigroup, name=>semigroup).

    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%20Structure in logic_2_Proofs ] for more on the structure and rules.

    The notation also allows you to create a new network of variables and constraints, and give them a name. 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.

End