This looks good to me, I'll start to incorporate this into my
code/documentation as I get time.
related issues:
You haven’t included the Heyting type algebras, such as
intuitionisticLogic, on your diagram but I guess there are no issues
with this?
One difference is 'pseudo complement' vs. 'implication' vs. 'not'. I
believe that these algebras could equivalently be defined in terms of
either 'pseudo complement' or 'implication'. I get the impression that
the usual style in FriCAS/Axiom is to include all options in a single
category although I think it would be confusing to include the 'not'
operation in Heyting algebras?
The other difference seems to be that the the Heyting algebras tend to
be infinite, or should I say 'free' in meet or join or both? That is
they are defined like an expression with variables. I guess there could
also be a Boolean algebra implemented in this way? Would this be
worthwhile, if only for completeness? As we discussed in an earlier
thread, I was considering implementing this using 'Kernel' but if I
understood your reply correctly the extra complexity would not be
worthwhile (I don't want to delve into undocumented stuff if I can avoid
it).
According to the Steven Vickers book, terminology around concepts like
'frame' is not fixed amongst different authors. His definition (which
follows Johnstone) is:
1) every subset has a join
2) every finite subset has a meet
3) binary meets distribute over joins
So frames are only different for infinite subsets, therefore its not
good enough to define meets of a subset,as I did, like this:
/\(List %) -> %
I need a way to define infinite subsets, I guess it would have to be an
expression? I will continue to read and experiment on the subject but
any pointers from anyone here would be welcome. The aim is to represent
topology concepts, especially where these concepts are used in computer
science.
I'm not sure what to do about the naming of operators in Preorder and
poset. I suspect its the same issue as mentioned by prof. Grabmeier that
these operators need to be renamed depending on context. Would it be
acceptable if I defined both '<=' and 'implies'? I would have liked to
use '=>' for implies but that’s used by SPAD for other things.
Martin
On 17/08/15 13:03, Waldek Hebisch wrote:
Martin Baker wrote:
What I would like to see is the powerful capabilities in FriCAS/Axiom
for equation solving and so on in "classic mostly commutative algebra"
to be packaged in such a way that they could be adapted for other
axiomatic systems.
Most useful to me would be the ability to write equation solvers in
matrix, quaternion, Clifford algebras where the variables represent, not
real/complex numbers, but elements of these algebras.
I think lot can be done in this direction. However, it is a big
topic, so let me postpone it a bit.
Another example is that I am writing code for different types of logic
(Heyting, frames, etc.) and this includes domains for poset, lattice and
so on.
I have documented this here:
http://www.euclideanspace.com/prog/scratchpad/mycode/discrete/logic/
or, if you don't like documentation, you can go straight to the code here:
https://github.com/martinbaker/multivector/blob/master/logic.spad
So could you include this in any changes you are making, in particular:
1) Include poset, frame, lattice, etc. into the category hierarchy.
2) Generalise equation solving capabilities to allow use for other
structures.
3) Include axioms in category definitions.
Concerning logic.spad, I think it needs some changes/corrections:
1) In Preorder the Axiom lines mention '<=' as operation
name but the only exports 'implies'. Actually, in
FriCAS the 'PartialOrder' category represents the
same concept (unlike many expositions of orders
'PartialOrder' does not assume weak antysymmetry).
2) AFAICS usual definiton of lattice does on include top
and bottom elements. If they are present we have special
kind of lattice (Wikipedia calls it bounded lattice, but
other names also seem to be in common use).
3) IMO FiniteLattice should be a category. Such lattice
automatically has top and bottom elements.
4) I am not sure if we want to use name 'true' for top
element of a lattice (and 'false' for bottom). It is
natural in context of logic, but not so natural in
other contexts.
5) It is not clear for me what you want to represnt by
Frame. Namely, due to associativity in a lattice
there is naturally defined join and meet for any
finite subset. IIRC frames used in logic have
a bit richer structure than what you define in Frame.
6) Once we have Lattice current Logic should inherit from
Lattice. Given that we want to represnt nonclassical
logics we need separate BooleanAlgebra for classical
case.
So I think we should have something like:
MeetSemilattice JoinSemilattice
| | / |
| V / V
| BoundedMeetSemilattice / BoundedJoinSemilattice
| \ / |
V \ / |
Lattice <--------------X |
\ \ V
---------------------- > ---> BoundedLattice
\ / |
\ / V
\ / Logic
\ / |
DistributiveLattice / |
\ / |
BoundedDistributiveLattice |
\ |
\ V
BooleanAlgebra
--
You received this message because you are subscribed to the Google Groups "FriCAS -
computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
