. Making Use of Algebras
Uses theory of documentation
.See http://www.csci.csusb.edu/dick/maths/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:
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:
X:monoid(op=>*, u=>1),
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:
XYZ::=Net{x:X, y:Y,... z:Z},
Xyz::=$ $XYZ, -- set of tupls
xyz::={x:X || XYZ(x=>x, y=>y, ..., z=>z)}, -- set of x's fitting XYZ...
For b,..., c, xyz(y=>b, ..., z=>c) ::={x:X || XYZ(x=>x, y=>b, ..., z=>c)},
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.
a :: xyz(y=>b, ..., z=>c, ) declares a::X (given b,... ,c ).
a :: xyz(b, ... ,c) declares a::X (given b,..., c ).
a :: xyz declares (x=>a, y=>y, z=>z,...) ::xyz.
and as in Ada:
|- 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 -
ALGEBRA::=Net{
DOC::name_of_documentation,
Set::variables($DOC).
Name::=$ $XYZ,
name::={ Set:Type($DOC)(Set) || $DOC },
for X, name(X) ::={ Set:Type($DOC)(Set) || (DOC(X))($(DOC(X))
}=::ALGEBRA.
.Example
ALGEBRA(DOC=>MONOID, Set=>Set, Name=>Monoid, name=>monoid),
.Example
ALGEBRA(DOC=>SEMIGROUP, Set=>Set, Name=>Semigroup, name=>semigroup).