finite.spad.pamphlet

\documentclass{article}
\usepackage{axiom}
\usepackage{url}
\newcommand{\File}[1]{\url{#1}}

\begin{document}
\title{Some basic finite mathematical structures}
\author{Martin J Baker}
\maketitle
\begin{abstract}
I would like to investigate 'domain theory' using FriCAS.
\url{http://en.wikipedia.org/wiki/Domain_theory/}
I am not yet sure how to build this in FriCAS but I think a good starting
point is to build finite versions of some common abstract structures:
\begin{itemize}
\item finite preorder.
\item partially ordered sets (posets).
\item chain.
\item directed set (directed preorder)
\item directed complete partial orders (dcpo or dcpos)
\item w-continuous poset (wcpos)
\item lattices
\item join-semilattice
\item meet-semilattice
\item totally ordered set
\end{itemize}
The aim is to build finite versions of these structures which can be
configured by the user or by a program to hold any valid instance of these
structures.

For more information and diagrams see:
\url{http : //www.euclideanspace.com/maths/standards/program/mycode/discrete/graph/}
\end{abstract}
\eject
\tableofcontents
\eject
\section{Requirements used to Design the Following Code}
1) The code needs to be able to represent the following finite structures:
\begin{itemize}
\item finite preorder.
\item partially ordered sets (posets).
\item chain.
\item directed set (directed preorder)
\item directed complete partial orders (dcpo or dcpos)
\item w-continuous poset (wcpos)
\item lattices
\item join-semilattice
\item meet-semilattice
\item totally ordered set
\end{itemize}

2) These finite structures must be user definable over any set and be of
arbitary complexity.

3) We need to be able to define, not only elements of these sets, but
also subsets. That is, not only do we want to model and work with the
structure defined by the '<=' relation, but we want to combine this with
the subset structure.

4) We need to be able to draw (Hasse like) diagrams of these
structures. The command line interface is not very good for
building potentially complex finite structures. For these
structures it requires users to enter and try to interpret
complicated strings of characters. I suspect that not many users
will find it worthwhile to work with such a clunky interface.
Ideally FriCAS would have a graphical interface in addition to
the command line interface but I can't see any sign of that
happening in the forseable future. As a second best option a
minimal reqirement is the ability to export to SVG diagrams.
By using the existing graph theory code we get that ability.

\section{Design Ideas}
So how do we design code to represent these structures, the operations
on them and also the sub-object structure. We need a design that can
represent, not only  all these things individually, but also how they
interact.

An old question is: Do we think of sets in terms of the elements being
the main focus with the set being a collection of them? Or do we think
of the set being the main focus and the elements being part of it?

In FriCAS terms, is the representation '\%' the set or is it an
element of the set?

For instance we need to be able to define operations on the
set:
\begin{verbatim}
a:% <= b:%
\end{verbatim}
In this case '\%' is an element of the set.

We also need to define operation on the whole set, like:
\begin{verbatim}
subset:% := clasifier(x,set:%)
\end{verbatim}
In this case '\%' is the whole set.
\section{Some classes of ordered sets}
Below we define the ordered sets that we are going to implement in this
pamphlet.
\subsection{Preorder}
A (finite in this case) set equiped with a binary relation '<=' which is
\begin{itemize}
\item reflexive: a<=a
\item transitive: if a<=b and b<=c then a<=c
\end{itemize}

\subsection{Poset}
A (finite in this case) set equiped with a binary relations '=' and '<=' which
obey the following axioms:
\begin{itemize}
\item reflexive: a<=a
\item transitive: if a<=b and b<=c then a<=c
\item antisymmetric: if a<=b and b<=a then a=b
\end{itemize}
That is, it is a preorder which is antisymmetric. So it has an equals '='
relation which is defined by the '<=' relation.

Some definitions for posets which involve subsets:
If 'A' is a subset of 'X' then:
\begin{itemize}
\item upperBound - This is an element 'x' where for every element 'a'
then a<=x. 
\item lowerBound - This is an element 'x' where for every element 'a'
then x<=a.
\item greatestElement - This is an element 'x' where it is an upperBound
and it is a member of A
\item leastElement - This is an element 'x' where it is an lowerBound
and it is a member of A
\item maximal - an element 'a' if for every element 'b' of A then if
b<=a implies b=a
\item minimal - an element 'a' if for every element 'b' of A then if
a<=b implies b=a
\item meet - a meet of two, or more, elements (in the general case the
subset A) if it exists is the greatest lowerBound or infirmum.
\item join - of A , if it exists, is the least element in the set
of upperBounds for A.
\end{itemize}
The existance of meets and joins for subsets of preordered sets is known
as:
\begin{itemize}
\item if meet exists - called completeness.
\item if join exists - called cocompleteness.
\end{itemize}
\subsection{Chain}
A chain is a preorder if for every x and y we have either x<=y or y<=x.
\subsection{Lattice}
A lattice is a preorder which has finite meets and joins.
\subsection{Join-semilattice}
A join-semilattice is a preorder which has finite joins.
\subsection{Meet-semilattice}
A meet-semilattice is a preorder which has finite meets.
\subsection{Boolean lattice}
A boolean lattice is a distributive lattice which also has compliments of
all elements.
\subsection{Heyting lattice}
A Heyting lattice is a lattice for which each pair of elements: y,z there
is an element y=>z such that:
x <=y => z iff x /\\y <= z.

Every boolean lattice is a Heyting lattice.

\subsection{directed set (directed preorder)}
A subset 'A' of a preorder 'X' is 'directed' if it is non empty and each
pair of elements in 'A' has an upperBound in 'A'.

A subset 'A' of a preorder 'X' is 'ideal' if it is non empty and each
pair of elements in 'A' has an lowerBound in 'A'.

\subsection{directed complete partial orders (dcpo or dcpos)}
A partially ordered set is a directed-complete partial order (dcpo) if
each of its directed subsets has a supremum.

Every finite poset is a dcpo

\subsection{w-continuous poset (wcpos)}
w-continuous poset (wcpos) is a poset in which every w-chain
(x1<=x2<=x3<=x4<=...) has a supremum.
Every dcpo is an wcpos, since every w-chain is a directed set.

\section{Implementation Issues}
Before attemping this code I looked at the existing codebase in case I was
duplicating anything that I could use. I found the following:
In catdef.spad.pamphlet I found:
\begin{itemize}
\item category PORDER PartialOrder
\item category ORDSET OrderedSet
\end{itemize}
PORDER is transitive and reflexive but no mention of antisymmetric, should
it really be preorder?
These categories do not allow an arbitary finite set to be defined so I
don't think that I can use them?

In setorder.spad.pamphlet:
\begin{itemize}
\item package UDPO UserDefinedPartialOrdering
\item package UDVO UserDefinedVariableOrdering
\end{itemize}
These packages have the usual minimal level of documentation so I don't
really know how they are intended to be used. They are packages rather than
domains so I don't really think I can use them?

In set.spad.pamphlet:
The domain SET Set has complete sets as its representations so, although
it can contain OrderedSet, I don't see how to use it here?

I think we need the representations here to be elements of the
set so that we can have operations like '<=' and '<'.

Here we implement all these finite order relations as finite graphs with
various constrains added. It would have been good to build the domains
constructivly but I can only think of a way to do it by starting with the
very general case of a graph and subtracting capability (adding constraints)
to build the more specific structures.

We map the '<=' relation to the edges in the directed graph as follows:
\begin{verbatim}
a    b    (a<=b)=false (b<=a)=false
a--->b    (a<=b)=false (b<=a)=true
a<---b    (a<=b)=true  (b<=a)=false
a<-->b    (a<=b)=true  (b<=a)=true
\end{verbatim}

I would have liked to use '<=' for 'less than or equal' and '<' for
'less than' and so on, but we need to specify the set that it is
applied to and these are binary operations, so that won't work.

My next thought was to define it like this:
\begin{verbatim}
"<=": (n:S,%, %) -> Boolean
\end{verbatim}
but that fails with the following (unhelpful) error message:
\begin{verbatim}
   >> Apparent user error:
   bad == form
\end{verbatim}
So I had to use the following notation:
\begin{itemize}
\item 'lt(n,x,y)' means 'x < y' in set 'n'
\item 'gt(n,x,y)' means 'x > y' in set 'n'
\item 'ge(n,x,y)' means 'x >= y' in set 'n'
\item 'le(n,x,y)' means 'x <= y' in set 'n'
\end{itemize}
Which is horrible notation but it is the best that I can do with the
current version of FriCAS
\section{FPORDER FinitePreOrder}
<<category FPORDER FinitePreOrder>>=
)abbrev category FPREORD FinitePreOrder
++ Author: Martin Baker
++ Description:
++ based on PORDER in catdef.spad.pamphlet which is a
++ class of partially ordered sets, that is sets equipped with
++ transitive and reflexive relation \spad{<=}.

FinitePreOrder(S) : Category == Definition where
 S : SetCategory

 Definition ==> Join(CoercibleTo(OutputForm), SetCategory) with

    lt: (n:S,%,%) -> Boolean
      ++ x < y is a less than test.
    gt: (n:S,%, %) -> Boolean
      ++ x > y is a greater than test.
    ge: (n:S,%, %) -> Boolean
      ++ x >= y is a greater than or equal test.
    le: (n:S,%, %) -> Boolean
      ++ x <= y is a less than or equal test.

  add

     ge(n:S,x:%,y:%) == le(n,y,x)
       -- impliments x >= y == y <= x

     gt(n:S,x:%,y:%) == lt(n,y,x)
       -- impliments x > y == y < x

     lt(n:S,x:%,y:%) == le(n,x,y) and not(le(n,y,x))
       -- impliments x < y == x <= y and not(y <= x)

@

\section{FPORDER FinitePartialOrder}
<<category FPORDER FinitePartialOrder>>=
)abbrev category FPORDER FinitePartialOrder
++ Author: Martin Baker
++ Description:
++ based on PORDER in catdef.spad.pamphlet which is a
++ class of partially ordered sets, that is sets equipped with
++ transitive, reflexive and antisymmetric relation \spad{<=}.

PartialOrder(S) : Category == Definition where
 S : SetCategory

 Definition ==> FinitePreOrder(S) with

    eq: (n:S,%,%) -> Boolean
      ++ antisymmetric: if x<=y and y<=x then x=y

  add

     eq(n:S,x:%,y:%) == le(n,x,y) and le(n,y,x)
      -- x = y == x <= y and y <= x
      -- antisymmetric: if x<=y and y<=x then x=y

@

\section{domain FPO FinPreOrd}
<<domain FPO FinPreOrd>>=
)abbrev domain FPO FinPreOrd
++ Author: Martin Baker
++ Date Created: November 2013
++ Date Last Updated: November 2013
++ Basic Operations:
++ Related Constructors:
++ Keywords: finite pre order poset
++ Description:
++  finite partial order
++
++ References:
++ http: //www.euclideanspace.com/maths/standards/program/mycode/discrete/graph/

FinPreOrd(S) : Exports == Implementation where

 S : SetCategory

 --Exports ==> Join(DirectedGraph(S),FinitePreOrder(S))
 Exports ==> FinitePreOrder(S)

 Implementation ==> DirectedGraph(S) add

     --le(n:S,x:%,y:%) == routeNodes(s, x, y) ~= []
     --le(n:S,x:%,y:%) == routeNodeRecursive(s, x, y, []) ~= []
     le(n:S,x:%,y:%) == true()

@

\section{License}
<<license>>=
--Copyright (c) 2013, Martin J Baker.
--All rights reserved.
--
--Redistribution and use in source and binary forms, with or without
--modification, are permitted provided that the following conditions are
--met:
--
--    - Redistributions of source code must retain the above copyright
--      notice, this list of conditions and the following disclaimer.
--
--    - Redistributions in binary form must reproduce the above copyright
--      notice, this list of conditions and the following disclaimer in
--      the documentation and/or other materials provided with the
--      distribution.
--
--    - Neither the name of Martin J Baker. nor the
--      names of its contributors may be used to endorse or promote products
--      derived from this software without specific prior written permission.
--
--THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
--IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
--TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
--PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
--OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
--EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
--PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
--PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
--LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
--NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
--SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
@
<<*>>=
<<license>>
@
\eject
\begin{thebibliography}{99}
For more details see:
[1] Floyd's algorithm
\url{http : //en.wikipedia.org/wiki/Floyd–Warshall_algorithm}
[2] Wiki page about 2-categories
\url{http : //en.wikipedia.org/wiki/2-category}

\end{thebibliography}
\end{document}